Require Import Peano_dec List Vbase Relations ExtraRelations.
Require Import actions c11 opsemsets coherence.
Set Implicit Arguments.

Section AccessIn.

Variable acts : list actid.
Variable lab : actid -> act.
Variables (sb asw : relation actid).
Hypothesis (EF: ExecutionFinite acts lab sb asw).

Lemma is_access_In a : is_access (lab a) -> In a acts.
Proof. by ins; eapply (proj1 EF); destruct (lab a). Qed.

Lemma is_fence_In a : is_fence (lab a) -> In a acts.
Proof. by ins; eapply (proj1 EF); destruct (lab a). Qed.

Lemma is_sc_In a : is_sc (lab a) -> In a acts.
Proof. by ins; eapply (proj1 EF); destruct (lab a). Qed.

Lemma is_na_In a : is_na (lab a) -> In a acts.
Proof. by ins; eapply (proj1 EF); destruct (lab a). Qed.

Lemma is_write_In a : is_write (lab a) -> In a acts.
Proof. by eauto using is_access_In with access. Qed.

Lemma is_writeL_In a l : is_writeL (lab a) l -> In a acts.
Proof. by eauto using is_access_In with access. Qed.

Lemma is_readL_In a l : is_readL (lab a) l -> In a acts.
Proof. by eauto using is_access_In with access. Qed.

Lemma is_rmw_In a : is_rmw (lab a) -> In a acts.
Proof. by eauto using is_access_In with access. Qed.

Lemma is_release_write_In:
  forall a (ACC: is_release_write (lab a)), In a acts.
Proof. by eauto using is_access_In with access. Qed.

Lemma is_acquire_read_In:
  forall a (ACC: is_acquire_read (lab a)), In a acts.
Proof. by eauto using is_access_In with access. Qed.

Lemma is_release_fence_In:
  forall a (ACC: is_release_fence (lab a)), In a acts.
Proof. by eauto using is_fence_In with access. Qed.

Lemma is_acquire_fence_In:
  forall a (ACC: is_acquire_fence (lab a)), In a acts.
Proof. by eauto using is_fence_In with access. Qed.

End AccessIn.

Hint Immediate
     is_access_In is_fence_In is_sc_In
     is_write_In is_writeL_In
      is_readL_In
     is_na_In is_rmw_In
     is_release_write_In is_acquire_read_In
     is_release_fence_In is_acquire_fence_In
: is_in.


Lemma pref_LabIn:
  forall o1 o2 (Pref: pref_opsem o1 o2)
         a (IN: In a (Acts o1)),
    Lab o1 a = Lab o2 a.
Proof.
  ins; dupdes Pref; by eauto.
Qed.


Lemma clos_trans_sb_In1:
  forall acts lab sb asw (EF: ExecutionFinite acts lab sb asw)
         a b (SB: clos_trans _ sb a b),
    In a acts.
Proof.
  unfold ExecutionFinite; ins; desf.
  eapply clos_trans_t1n in SB. destruct SB.
  exploit CLOsb; eauto; intuition.
  exploit CLOsb; eauto; intuition.
Qed.

Lemma clos_trans_sb_In2:
  forall acts lab sb asw (EF: ExecutionFinite acts lab sb asw)
         a b (SB: clos_trans _ sb a b),
    In b acts.
Proof.
  unfold ExecutionFinite; ins; desf.
  eapply clos_trans_tn1 in SB. destruct SB.
  exploit CLOsb; eauto; intuition.
  exploit CLOsb; eauto; intuition.
Qed.

Hint Immediate
     clos_trans_sb_In1 clos_trans_sb_In2 : in_acts.

Lemma Pref_clos_trans :
  forall o1 o2 (Pref: pref_opsem o1 o2),
    clos_trans _ (Sb o1)
    <--> restr_rel (fun x => In x (Acts o1)) (clos_trans _ (Sb o2)).
Proof.
  ins; red in Pref; desc.
  rewrite Pref_Sb, clos_trans_restr; ins; reflexivity.
Qed.

Lemma Pref_release_seq_elem1:
  forall o1 (EF: ExecutionFinite (Acts o1) (Lab o1) (Sb o1) (Asw o1))
         o2 (Pref: pref_opsem o1 o2) mt2,
    inclusion _
              (restr_rel (fun x => In x (Acts o1)) (release_seq_elem mt2 (Lab o2) (Sb o2)))
              (release_seq_elem mt2 (Lab o1) (Sb o1)).
Proof.
  unfold inclusion, release_seq_elem, restr_rel, same_thread;
    ins; desf; intuition;
  repeat rewrite (pref_LabIn Pref); eauto with in_acts.
  by left; eapply Pref_clos_trans; try red; eauto.
Qed.


Lemma Pref_release_seq_elem2:
  forall o1 (EF: ExecutionFinite (Acts o1) (Lab o1) (Sb o1) (Asw o1))
         o2 (Pref: pref_opsem o1 o2) mt2
         x y (RS: release_seq_elem mt2 (Lab o1) (Sb o1) x y)
             (AX: In x (Acts o1))
             (AY: In y (Acts o1)),
    restr_rel (fun x => In x (Acts o1)) (release_seq_elem mt2 (Lab o2) (Sb o2)) x y.
Proof.
  unfold inclusion, release_seq_elem, restr_rel; ins; desf; intuition.
  left; unfold same_thread in *; desf.
    by repeat rewrite <- (pref_LabIn Pref); eauto.
    desf; eapply Pref_clos_trans in RS; eauto.
    by unfold restr_rel in *; desf; eauto.
  by rewrite <- (pref_LabIn Pref); eauto.
Qed.

Lemma Pref_release_seq1:
  forall o1 (EF: ExecutionFinite (Acts o1) (Lab o1) (Sb o1) (Asw o1))
         o2 (Pref: pref_opsem o1 o2)
         rf1 rf2 (PrefRF: same_relation _ (fun x y => rf1 y = Some x)
                          (restr_rel (fun x => In x (Acts o1)) (fun x y => rf2 y = Some x)))
                 (Pref_UCRF: upward_closed (fun x y => rf2 y = Some x)
                                           (fun x => In x (Acts o1)))
         mo1 mo2 (PrefMO: same_relation _ mo1 (restr_rel (fun x => In x (Acts o1)) mo2)) mt2,
    inclusion _
              (restr_rel (fun x => In x (Acts o1)) (release_seq mt2 (Lab o2) (Sb o2) rf2 mo2))
              (release_seq mt2 (Lab o1) (Sb o1) rf1 mo1).
Proof.
  unfold inclusion, release_seq, restr_rel; ins; desf; desf; unnw; intuition.
  right; intuition.
    by eapply PrefMO.
    eby eapply Pref_release_seq_elem1.
    eapply PrefMO in MA; eapply PrefMO in MB; desf.
    by eapply Pref_release_seq_elem1; unfold restr_rel; eauto.
  induction H; unfold same_thread in *; desf; eauto using release_seq_alt.
    by eapply RS_thr; unfold same_thread; try (by eapply PrefMO); desf;
       rewrite !(pref_LabIn Pref); ins; eauto with is_in.
    eby eapply RS_thr; unfold same_thread; try (by eapply PrefMO); desf;
        eapply Pref_clos_trans.
  eapply RS_rmw; eauto.
    by eapply PrefRF; eauto.
  by rewrite !(pref_LabIn Pref); ins; eauto with is_in.
Qed.

Lemma Pref_release_seq3:
  forall o1 (EF: ExecutionFinite (Acts o1) (Lab o1) (Sb o1) (Asw o1))
         o2 (Pref: pref_opsem o1 o2)
         rf1 rf2 (PrefRF: same_relation _ (fun x y => rf1 y = Some x)
                          (restr_rel (fun x => In x (Acts o1)) (fun x y => rf2 y = Some x)))
         mo1 mo2 (PrefMO: same_relation _ mo1 (restr_rel (fun x => In x (Acts o1)) mo2))
         mt2 (Pref_UCMO: snd mt2 = MT3orig -> upward_closed mo2 (fun x => In x (Acts o1)))
         x y (RS: release_seq mt2 (Lab o1) (Sb o1) rf1 mo1 x y)
             (AX: In x (Acts o1)),
    restr_rel (fun x => In x (Acts o1)) (release_seq mt2 (Lab o2) (Sb o2) rf2 mo2) x y.
Proof.
  unfold release_seq, restr_rel; ins; desf; desf; unnw; eauto.
  eapply PrefMO in RSMO; unfold restr_rel in RSMO; desf; intuition.
  right; repeat split; eauto; ins.
    by eapply Pref_release_seq_elem2; eauto.
    by eapply Pref_release_seq_elem2; eauto; eapply RSO;
       eapply PrefMO; eauto.
  induction RS; unfold same_thread in *; desf; eauto using release_seq_alt;
  try (apply PrefMO in RSmo; desf; intuition;
       apply RS_thr; unfold same_thread; desf; rewrite <- ?(pref_LabIn Pref); ins).
    by eapply Pref_clos_trans in RSthr; unfold restr_rel in *; desf; eauto.
  eapply PrefRF in RSrf; desf; repeat split; ins.
  eapply RS_rmw; eauto.
  rewrite <- ?(pref_LabIn Pref); ins.
Qed.

Lemma Pref_UCSbt :
  forall o1 o2 (Pref: pref_opsem o1 o2),
    upward_closed (clos_trans actid (Sb o2)) (fun x => In x (Acts o1)).
Proof.
  unfold pref_opsem; ins; desc.
  eapply upward_clos_trans in Pref_UCSb; eauto.
Qed.

Lemma hb_unfold mt2 lab sb asw rf mo :
  happens_before mt2 lab sb asw rf mo =
  clos_trans actid
        (union actid sb
           (union actid (synchronizes_with mt2 lab sb rf mo true) asw)).
Proof.
  done.
Qed.

Lemma rf_rel_none:
  forall (a: actid) (rf: actid -> option actid),
    rf a = None <-> forall b (RF: rf a = Some b), False.
Proof.
  ins; split; ins.
  rewrite RF in *; discriminate.
  destruct (rf a); eauto.
  exfalso; by eauto.
Qed.

Lemma rf_same_rel_fun:
  forall (P: actid -> Prop)
         (rf1 rf2: actid -> option actid)
         (PrefRF: same_relation _
                                (fun x y => rf1 y = Some x)
                                (restr_rel P (fun x y => rf2 y = Some x)))
         (Pref_UCRF: upward_closed (fun x y => rf2 y = Some x) P)
         a (PA: P a),
    rf1 a = rf2 a.
Proof.
  unfold same_relation, restr_rel; ins; desf.
  assert (RF: rf2 a = None \/ exists b, rf2 a = Some b).
    by destruct (rf2 a); eauto.
  desf; rewrite RF.
  eapply rf_rel_none. ins. eapply PrefRF in RF0. by desf.
  eapply PrefRF0; by intuition; eauto.
Qed.

Section Pref_Axioms.

  Variables o1 o2 : opsem.
  Hypothesis Pref : pref_opsem o1 o2.

  Variables rf1 rf2 : actid -> option actid.
  Hypothesis PrefRF : same_relation _ (fun x y => rf1 y = Some x)
                      (restr_rel (fun x => In x (Acts o1)) (fun x y => rf2 y = Some x)).
  Hypothesis Pref_UCRF: upward_closed (fun x y => rf2 y = Some x)
                                       (fun x => In x (Acts o1)).

  Variables mo1 mo2 : relation actid.
  Hypothesis PrefMO : same_relation _ mo1 (restr_rel (fun x => In x (Acts o1)) mo2).

  Variable mt2 : modeltyp_threadid * modeltyp_relseq.

  Definition condition_for_ucmo mt2 :=
    fst mt2 = MT2orig \/ snd mt2 = MT3orig.

  Hypothesis Pref_UCMO :
    condition_for_ucmo mt2 -> upward_closed mo2 (fun x => In x (Acts o1)).

  Variables sc1 sc2 : relation actid.
  Hypothesis PrefSC : same_relation _ sc1 (restr_rel (fun x => In x (Acts o1)) sc2).

Lemma Pref_ExecutionFinite :
  ExecutionFinite (Acts o1) (Lab o1) (Sb o1) (Asw o1).
Proof.
  dupdes Pref; split; unnw; ins.
  by destruct (in_dec eq_nat_dec a (Acts o1)); ins; destruct H; eauto.
  by destruct H as [H|H]; [eapply Pref_Sb in H | eapply Pref_Asw in H]; destruct H.
Qed.

Hint Resolve Pref_ExecutionFinite.

Lemma Pref_UCRS :
  upward_closed (release_seq mt2 (Lab o2) (Sb o2) rf2 mo2) (fun x => In x (Acts o1)).
Proof.
  destruct mt2; unfold condition_for_ucmo, upward_closed, release_seq in *; ins.
  desf; desf; intuition; eauto.
  induction REL; unfold same_thread in *; desf; eauto.
  eapply Pref_UCSbt; eauto.
Qed.

Lemma Pref_UCSW :
  upward_closed (synchronizes_with mt2 (Lab o2) (Sb o2) rf2 mo2 true)
                (fun x => In x (Acts o1)).
Proof.
  ins; unfold upward_closed, synchronizes_with in *; ins; des; unnw.
  * eapply Pref_UCRS; unfold upward_closed; eauto.
  * eapply Pref_UCRS; unfold upward_closed; eauto.
    eapply Pref_UCRF; unfold upward_closed; eauto.
    eapply Pref_UCSbt; unfold upward_closed; eauto.
  * eapply Pref_UCSbt; unfold upward_closed; eauto.
    eapply Pref_UCRS; unfold upward_closed; eauto.
  * eapply Pref_UCSbt; unfold upward_closed; eauto.
    eapply Pref_UCRS; unfold upward_closed; eauto.
    eapply Pref_UCRF; unfold upward_closed; eauto.
    eapply Pref_UCSbt; unfold upward_closed; eauto.
Qed.

Lemma Pref_UCHB:
  upward_closed (happens_before mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2)
                (fun x => In x (Acts o1)).
Proof.
  ins; eapply upward_clos_trans.
  unfold upward_closed; ins; desf; dupdes Pref; eauto 3.
  eapply Pref_UCSW; try eexact REL; eauto.
Qed.

Lemma Pref_synchronizes_with:
  synchronizes_with mt2 (Lab o1) (Sb o1) rf1 mo1 true
  <--> restr_rel (fun x => In x (Acts o1))
                 (synchronizes_with mt2 (Lab o2) (Sb o2) rf2 mo2 true).
Proof.
  split; unfold inclusion, synchronizes_with, restr_rel, diff_thread.
  intros x y hxy.
  assert (In x (Acts o1) /\ In y (Acts o1)).
    by intuition; eauto with is_in.
  des; unnw; repeat split; ins;
  [ left | right; left | do 2 right; left | do 3 right ];
  eapply PrefRF in RF; eauto;
  try (eapply Pref_clos_trans in SBR; eauto);
  try (eapply Pref_clos_trans in SBW; eauto);
  unfold restr_rel in *; desc; eauto;
  repeat rewrite <- (pref_LabIn Pref) by eauto;
    repeat eexists; eauto; try eapply PrefRF; eauto;
    try (eby eapply Pref_release_seq3; unfold diff_thread, condition_for_ucmo in *; eauto); eauto;
    try by instantiate; rewrite <- (pref_LabIn Pref); eauto.

  intros x y hxy; unfold restr_rel, diff_thread in *; des; unnw;
  [ left | right; left | do 2 right; left | do 3 right ];
  assert (PRF:= fun P => Pref_UCRF RF P); ins;
  try assert (PSBR := fun P => Pref_UCSbt Pref SBR P);
  try assert (PSBW := fun P => Pref_UCSbt Pref SBW P); ins;
  exploit Pref_UCRS; try eexact RS; eauto; intro;
  repeat rewrite (pref_LabIn Pref) by eauto;
    repeat eexists; eauto;
    try (match goal with
           | [ |- rf1 _ = _ ] =>
             eapply PrefRF; eauto; repeat split; try eexact RF; eauto
           | [ |- clos_trans _ _ _ _ ] =>
             eapply Pref_clos_trans; eauto; repeat split; eauto
           | |- release_seq _ _ _ _ _ _ _ =>
             eapply Pref_release_seq1; eauto; ins; repeat split; eauto
         end);
    try (by instantiate; rewrite (pref_LabIn Pref); eauto).
Qed.

Lemma Pref_happens_before:
  happens_before mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1
  <--> restr_rel (fun x => In x (Acts o1))
                 (happens_before mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2).
Proof.
  ins; dupdes Pref; rewrite !hb_unfold.
  rewrite Pref_Sb at 1; rewrite Pref_Asw, Pref_synchronizes_with; eauto.
  rewrite !union_restr, clos_trans_restr; eauto; try reflexivity.
  red; ins; eapply Pref_UCHB; try rewrite hb_unfold;
  try eapply (t_step _ _ _ _ REL); eauto.
Qed.


Lemma Pref_ConsistentMO:
  ConsistentMO (Lab o2) mo2 ->
  ConsistentMO (Lab o1) mo1.
Proof.
  unfold ConsistentMO; ins; desf; unnw; repeat split; ins.
  eapply PrefMO in MO; unfold restr_rel in MO; desf.
  eapply CmoD in MO; desf; exists l.
  dupdes Pref; repeat rewrite Pref_LabIn by eauto.
  by intuition.
  intros x y z hxy hyz.
  eapply PrefMO in hxy; eapply PrefMO in hyz; eapply PrefMO;
    unfold restr_rel in *; desf; by intuition; eauto.
  unfold is_total; ins.
  assert (In a (Acts o1)).
    by eauto with is_in.
  assert (In b (Acts o1)).
    by eauto with is_in.
  dupdes Pref.
  rewrite Pref_LabIn in IWa by eauto.
  rewrite Pref_LabIn in IWb by eauto.
  exploit (CmoF l a IWa b IWb); eauto; intro HMO.
  destruct HMO as [HMO|HMO]; [left|right];
    eapply PrefMO; unfold restr_rel; by intuition.
  unfold irreflexive; intros x hxx; eapply PrefMO in hxx;
    unfold restr_rel in *; desf; eauto.
Qed.

Lemma Pref_ConsistentMOhb:
  forall (Cmohb : ConsistentMOhb mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    ConsistentMOhb mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.
Proof.
  unfold ConsistentMOhb; ins; desf.
  unfold restr_subset; ins.
  eapply PrefMO. unfold restr_rel. intuition; eauto with is_in.
  assert (In a (Acts o1)).
    by eauto with is_in.
  assert (In b (Acts o1)).
    by eauto with is_in.
  dupdes Pref.
  rewrite Pref_LabIn in IWa by eauto.
  rewrite Pref_LabIn in IWb by eauto.
  eapply Cmohb; eauto.
  eapply Pref_happens_before in REL; eauto. unfold restr_rel in REL; by intuition.
Qed.

Lemma Pref_ConsistentSC:
    ConsistentSC mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2 sc2 ->
    ConsistentSC mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1 sc1.
Proof.
  unfold ConsistentSC; ins; desf; intuition; red.
  ins. eapply PrefSC in MO. unfold restr_rel in MO; desf.
  repeat rewrite (pref_LabIn Pref); by eauto.
  intros x y z hxy hyz.
  eapply PrefSC in hxy; eapply PrefSC in hyz; eapply PrefSC;
    unfold restr_rel in *; desf; by intuition; eauto.
  unfold is_total; ins.
  assert (In a (Acts o1)).
    by eauto with is_in.
  assert (In b (Acts o1)).
    by eauto with is_in.
  erewrite pref_LabIn in IWa by eauto.
  erewrite pref_LabIn in IWb by eauto.
  exploit (CscF a IWa b IWb); eauto; intro HMO.
  destruct HMO as [HMO|HMO]; [left|right];
    eapply PrefSC; unfold restr_rel; by intuition.
  unfold irreflexive; intros x hxx; eapply PrefSC in hxx;
    unfold restr_rel in *; desf; eauto.
  unfold restr_subset; ins.
  eapply PrefSC. unfold restr_rel; intuition; eauto with is_in; dupdes Pref.
  eapply Chbsc.
  rewrite <- Pref_LabIn; eauto with is_in.
  rewrite <- Pref_LabIn; eauto with is_in.
  eapply Pref_happens_before in REL; eauto. unfold restr_rel in REL; intuition.
  unfold restr_subset; ins.
  eapply PrefSC. unfold restr_rel; intuition; eauto with is_in; dupdes Pref.
  eapply Cmosc.
  rewrite <- Pref_LabIn; eauto with is_in.
  rewrite <- Pref_LabIn; eauto with is_in.
  eapply PrefMO in REL; eauto. unfold restr_rel in REL; intuition.
Qed.

Lemma Pref_ConsistentRF_dom_none:
  forall (CrfN : ConsistentRF_dom_none mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    ConsistentRF_dom_none mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.
Proof.
  unfold ConsistentRF_dom_none; ins; dupdes Pref.
  eapply CrfN. symmetry. rewrite <- RF. eapply rf_same_rel_fun; eauto.
    eapply is_readL_In; by eauto.
  eapply Pref_happens_before in HB; eauto. unfold restr_rel in HB; desf; by eauto.
  rewrite <- Pref_LabIn; by eauto with is_in.
  rewrite <- Pref_LabIn; by eauto with is_in.
Qed.

Lemma Pref_ConsistentRF_dom_some:
  forall (CrfS : ConsistentRF_dom_some mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    ConsistentRF_dom_some mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.
Proof.
  unfold ConsistentRF_dom_some; ins.
  eapply PrefRF in RF; red in RF; des.
  eapply CrfS in RF; unnw; des.
  repeat eexists.
      eapply Pref_happens_before; unfold restr_rel; intuition; eauto.
      by eapply Pref_UCHB; eauto.
    by rewrite (pref_LabIn Pref); eauto.
  rewrite (pref_LabIn Pref); eauto.
  by eapply Pref_UCHB; eauto.
Qed.

Lemma Pref_ConsistentRF:
  forall (Crf : ConsistentRF (Lab o2) rf2),
    ConsistentRF (Lab o1) rf1.
Proof.
  unfold ConsistentRF; ins.
  eapply PrefRF in RF. unfold restr_rel in RF; desf.
  eapply Crf in RF. desf.
  repeat eexists; repeat split; red; dupdes Pref.
  by rewrite Pref_LabIn; eauto.
  by rewrite Pref_LabIn; eauto.
Qed.

Lemma Pref_ConsistentRFhb:
  forall (Crfhb : ConsistentRFhb mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    ConsistentRFhb mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.
Proof.
  unfold ConsistentRFhb; ins; dupdes Pref.
  eapply Crfhb.
  eapply PrefRF; by eauto.
  eapply Pref_happens_before in HB; eauto. unfold restr_rel in HB; by intuition.
Qed.

Lemma Pref_ConsistentRF_na:
  forall
    (Crfhb : ConsistentRF_na mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    ConsistentRF_na mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.
Proof.
  unfold ConsistentRF_na; ins.
  eapply Pref_happens_before; eauto.
  eapply PrefRF in RF. unfold restr_rel in RF.
  revert NA; desf; ins.
  dupdes Pref. do 2 rewrite Pref_LabIn in NA; eauto.
  unfold restr_rel; repeat split; eauto.
Qed.

Lemma Pref_sc_restr:
  same_relation _
    (sc_restr (Lab o1) sc1)
    (restr_rel (fun x => In x (Acts o1)) (sc_restr (Lab o2) sc2)).
Proof.
  ins; split; unfold inclusion, sc_restr, restr_rel.
  intros x y hxy. desf.
    eapply PrefSC in hxy; unfold restr_rel in hxy; desf.
    by repeat rewrite <- (pref_LabIn Pref); eauto.
  intros x y hxy. desf.
    repeat rewrite (pref_LabIn Pref); eauto; intuition.
    by eapply PrefSC; unfold restr_rel; eauto.
Qed.

Lemma Pref_SCrestriction:
  forall (Scr : SCrestriction mt2 MTSChb (Lab o2) (Sb o2) (Asw o2) rf2 mo2 sc2),
    SCrestriction mt2 MTSChb (Lab o1) (Sb o1) (Asw o1) rf1 mo1 sc1.
Proof.
  unfold SCrestriction; ins.
  eapply PrefRF in RF; unfold restr_rel in RF; desf.
  rewrite (pref_LabIn Pref) in SC; eauto.
  eapply Scr in RF; des; eauto.
  left; unfold immediate in *; desc; split; ins.
    by eapply Pref_sc_restr; unfold restr_rel; eauto.
    eapply Pref_sc_restr in R1; eauto.
    eapply Pref_sc_restr in R2; eauto.
    by unfold restr_rel in *; desf; eauto.
  right; split; ins.
    by rewrite (pref_LabIn Pref); eauto.
  eapply RF2.
    by eapply Pref_sc_restr in SC0; unfold restr_rel in *; desf; eauto.
    by eapply Pref_happens_before in HB; unfold restr_rel in *; desf; eauto.
Qed.

Lemma Pref_CoherentRR:
  forall (Crr : CoherentRR mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    CoherentRR mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.
Proof.
  unfold CoherentRR; ins; dupdes Pref.
  eapply Crr.
    eapply Pref_happens_before in HB; eauto. unfold restr_rel in HB; desf; by eauto.
    eapply PrefRF; by eauto.
    eapply PrefRF; by eauto.
    eapply PrefMO; by eauto.
Qed.

Lemma Pref_CoherentWR:
  forall (Cwr : CoherentWR mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    CoherentWR mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.
Proof.
  unfold CoherentWR; ins; dupdes Pref.
  eapply Cwr.
    eapply Pref_happens_before in HB; eauto. unfold restr_rel in HB; desf; by eauto.
    eapply PrefRF; by eauto.
    eapply PrefMO; by eauto.
Qed.

Lemma Pref_CoherentRW:
  forall (Crw : CoherentRW mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    CoherentRW mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.
Proof.
  unfold CoherentRW; ins; dupdes Pref.
  eapply Crw.
    eapply Pref_happens_before in HB; eauto. unfold restr_rel in HB; desf; by eauto.
    eapply PrefRF; by eauto.
    eapply PrefMO; by eauto.
Qed.

Lemma Pref_AtomicRMW:
  forall (Armw : AtomicRMW (Lab o2) rf2 mo2),
    AtomicRMW (Lab o1) rf1 mo1.
Proof.
  unfold AtomicRMW; ins.
  rewrite (pref_LabIn Pref) in RMW; eauto with is_in.
  eapply PrefRF in RF; eauto. unfold restr_rel in RF; desf.
  eapply Armw in RMW; eauto.
  unfold immediate in *. desf. split.
    eapply PrefMO; eauto. by unfold restr_rel; eauto.
    ins. eapply PrefMO in R1; eauto.
         eapply PrefMO in R2; eauto.
         by unfold restr_rel in *; desf; eauto.
Qed.

Lemma Pref_ConsistentAlloc:
  forall (Calloc: ConsistentAlloc (Lab o2)),
    ConsistentAlloc (Lab o1).
Proof.
  unfold ConsistentAlloc; ins; dupdes Pref.
  assert (EF := Pref_ExecutionFinite); red in EF; desc.
  by eapply Calloc; rewrite <- Pref_LabIn; eauto;
     eapply CLOlab; rewrite ?ALLOCa, ?ALLOCb.
Qed.

Lemma Pref_ConsistentDSB:
  forall (Cdsb : ConsistentDSB (Lab o2) (Sb o2) (Dsb o2)),
    ConsistentDSB (Lab o1) (Sb o1) (Dsb o1).
Proof.
  clear - Pref; unfold ConsistentDSB; ins; dupdes Pref.
  repeat split.
  intros x y hxy; eapply Pref_Dsb in hxy; eapply Pref_clos_trans; eauto.
    by unfold restr_rel in *; desf; eauto.
  ins. rewrite Pref_LabIn. eapply Cdsb0. eapply Pref_Dsb. by eauto.
    eapply Pref_Dsb in DSB. unfold restr_rel in DSB; by desf.
  ins. rewrite Pref_LabIn. eapply Cdsb1. eapply Pref_Dsb. by eauto.
    eapply Pref_Dsb in DSB. unfold restr_rel in DSB; by desf.
Qed.

Lemma Pref_ConsistentSB:
  forall (Csb : ConsistentSB (Lab o2) (Sb o2)),
    ConsistentSB (Lab o1) (Sb o1).
Proof.
  clear - Pref; unfold ConsistentSB; ins; dupdes Pref.
  eapply Pref_Sb in SB; red in SB; desc.
  rewrite !Pref_LabIn; ins; eauto.
Qed.





Lemma Pref_hbUrfnaAcyclic:
  acyclic (fun a b =>
             happens_before mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2 a b
             \/ rfna (Lab o2) rf2 a b) ->
  acyclic (fun a b =>
             happens_before mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1 a b
             \/ rfna (Lab o1) rf1 a b).
Proof.
  unfold rfna; ins; eapply acyclic_mon; eauto.
  red; ins; desf.
    by left; eapply Pref_happens_before.
  by right; split; [eapply PrefRF|left; rewrite <- (pref_LabIn Pref)]; eauto with is_in.
  by right; split; [eapply PrefRF|right; rewrite <- (pref_LabIn Pref)]; eauto with is_in.
Qed.

Lemma Pref_hbUrfAcyclic:
  acyclic (fun a b =>
             happens_before mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2 a b
             \/ rf2 b = Some a) ->
  acyclic (fun a b =>
             happens_before mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1 a b
             \/ rf1 b = Some a).
Proof.
  ins; eapply acyclic_mon; eauto.
  red; ins; desf.
    by left; eapply Pref_happens_before.
  by right; eapply PrefRF.
Qed.

Lemma Pref_dsbUrfAcyclic:
  acyclic (fun a b => Dsb o2 a b \/ rf2 b = Some a) ->
  acyclic (fun a b => Dsb o1 a b \/ rf1 b = Some a).
Proof.
  ins; eapply acyclic_mon; eauto.
  red; ins; desf.
    by left; dupdes Pref; eapply Pref_Dsb.
  by right; eapply PrefRF.
Qed.

Lemma Pref_AcyclicityAxiom :
  forall mt,
    AcyclicityAxiom mt mt2 (Lab o2) (Sb o2) (Dsb o2) (Asw o2) rf2 mo2 ->
    AcyclicityAxiom mt mt2 (Lab o1) (Sb o1) (Dsb o1) (Asw o1) rf1 mo1.
Proof.
  destruct mt; ins;
  eauto using Pref_ConsistentRF_na,
   Pref_hbUrfAcyclic,
   Pref_hbUrfnaAcyclic,
   Pref_dsbUrfAcyclic.
Qed.

Lemma Pref_Consistent :
  forall mt,
    Consistent mt mt2 MTSChb (Acts o2) (Lab o2) (Sb o2) (Dsb o2) (Asw o2) rf2 mo2 sc2 ->
    Consistent mt mt2 MTSChb (Acts o1) (Lab o1) (Sb o1) (Dsb o1) (Asw o1) rf1 mo1 sc1.
Proof.
  unfold Consistent; ins; desc; unnw; intuition;
    eauto using
          Pref_ConsistentMO, Pref_ConsistentMOhb,
          Pref_ConsistentRF, Pref_ConsistentRFhb,
          Pref_ConsistentRF_dom_some, Pref_ConsistentRF_dom_none,
          Pref_ConsistentDSB, Pref_ConsistentSB,
          Pref_ConsistentSC, Pref_SCrestriction,
          Pref_ConsistentAlloc, Pref_AtomicRMW,
          Pref_CoherentRR, Pref_CoherentRW, Pref_CoherentWR,
          Pref_AcyclicityAxiom.
  by intros x M; apply Pref_happens_before in M; red in M; desc; eauto.
Qed.

Lemma Pref_Semiconsistent :
  forall mt,
    Semiconsistent mt mt2 MTSChb (Acts o2) (Lab o2) (Sb o2) (Dsb o2) (Asw o2) rf2 mo2 sc2 ->
    Semiconsistent mt mt2 MTSChb (Acts o1) (Lab o1) (Sb o1) (Dsb o1) (Asw o1) rf1 mo1 sc1.
Proof.
  unfold Semiconsistent; ins; desc; unnw; intuition;
    eauto using
          Pref_ConsistentMO, Pref_ConsistentMOhb,
          Pref_ConsistentRF, Pref_ConsistentRFhb,
          Pref_ConsistentRF_dom_some, Pref_ConsistentRF_dom_none,
          Pref_ConsistentDSB, Pref_ConsistentSB,
          Pref_ConsistentSC, Pref_SCrestriction,
          Pref_ConsistentAlloc, Pref_AtomicRMW,
          Pref_CoherentRR, Pref_CoherentRW, Pref_CoherentWR,
          Pref_AcyclicityAxiom.
  by intros x M; apply Pref_happens_before in M; red in M; desc; eauto.
Qed.

End Pref_Axioms.

Theorem Pref_Consistent2 :
  forall mt o1 o2 w,
    pref_opsem o1 o2 ->
    upward_closed (fun x y : actid => Rf w y = Some x) ((In (A:=actid))^~ (Acts o1)) ->
    pre_execution mt (MT2sb,MT3rf) MTSChb o2 w ->
    exists w',
      pre_execution mt (MT2sb,MT3rf) MTSChb o1 w'.
Proof.
  unfold pre_execution; ins.
  exists {| Rf := fun x => if in_dec eq_nat_dec x (Acts o1) then Rf w x else None ;
            Mo := restr_rel (fun x => In x (Acts o1)) (Mo w) ;
            Sc := restr_rel (fun x => In x (Acts o1)) (Sc w) |}; ins.
  eapply Pref_Semiconsistent, H1; unfold condition_for_ucmo in *; ins; desf; intuition.
  red in H0; red in H1; desf.
  unfold restr_rel; split; red; ins; desf; repeat split; eauto.
Qed.