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.

Lemma is_fence_In a : is_fence (lab a) → In a acts.

Lemma is_sc_In a : is_sc (lab a) → In a acts.

Lemma is_na_In a : is_na (lab a) → In a acts.

Lemma is_write_In a : is_write (lab a) → In a acts.

Lemma is_writeL_In a l : is_writeL (lab a) l → In a acts.

Lemma is_readL_In a l : is_readL (lab a) l → In a acts.

Lemma is_rmw_In a : is_rmw (lab a) → In a acts.

Lemma is_release_write_In:
  ∀ a (ACC: is_release_write (lab a)), In a acts.

Lemma is_acquire_read_In:
  ∀ a (ACC: is_acquire_read (lab a)), In a acts.

Lemma is_release_fence_In:
  ∀ a (ACC: is_release_fence (lab a)), In a acts.

Lemma is_acquire_fence_In:
  ∀ a (ACC: is_acquire_fence (lab a)), In a acts.

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:
  ∀ o1 o2 (Pref: pref_opsem o1 o2)
         a (IN: In a (Acts o1)),
    Lab o1 a = Lab o2 a.


Lemma clos_trans_sb_In1:
  ∀ acts lab sb asw (EF: ExecutionFinite acts lab sb asw)
         a b (SB: clos_trans _ sb a b),
    In a acts.

Lemma clos_trans_sb_In2:
  ∀ acts lab sb asw (EF: ExecutionFinite acts lab sb asw)
         a b (SB: clos_trans _ sb a b),
    In b acts.

Hint Immediate
     clos_trans_sb_In1 clos_trans_sb_In2 : in_acts.

Lemma Pref_clos_trans :
  ∀ o1 o2 (Pref: pref_opsem o1 o2),
    clos_trans _ (Sb o1)
    <-→ restr_rel (fun x ⇒ In x (Acts o1)) (clos_trans _ (Sb o2)).

Lemma Pref_release_seq_elem1:
  ∀ 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)).


Lemma Pref_release_seq_elem2:
  ∀ 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.

Lemma Pref_release_seq1:
  ∀ 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).

Lemma Pref_release_seq3:
  ∀ 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.

Lemma Pref_UCSbt :
  ∀ o1 o2 (Pref: pref_opsem o1 o2),
    upward_closed (clos_trans actid (Sb o2)) (fun x ⇒ In x (Acts o1)).

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)).

Lemma rf_rel_none:
  ∀ (a: actid) (rf: actid → option actid),
    rf a = None ↔ ∀ b (RF: rf a = Some b), False.

Lemma rf_same_rel_fun:
  ∀ (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.

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).

Hint Resolve Pref_ExecutionFinite.

Lemma Pref_UCRS :
  upward_closed (release_seq mt2 (Lab o2) (Sb o2) rf2 mo2) (fun x ⇒ In x (Acts o1)).

Lemma Pref_UCSW :
  upward_closed (synchronizes_with mt2 (Lab o2) (Sb o2) rf2 mo2 true)
                (fun x ⇒ In x (Acts o1)).

Lemma Pref_UCHB:
  upward_closed (happens_before mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2)
                (fun x ⇒ In x (Acts o1)).

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).

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).


Lemma Pref_ConsistentMO:
  ConsistentMO (Lab o2) mo2 →
  ConsistentMO (Lab o1) mo1.

Lemma Pref_ConsistentMOhb:
  ∀ (Cmohb : ConsistentMOhb mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    ConsistentMOhb mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.

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.

Lemma Pref_ConsistentRF_dom_none:
  ∀ (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.

Lemma Pref_ConsistentRF_dom_some:
  ∀ (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.

Lemma Pref_ConsistentRF:
  ∀ (Crf : ConsistentRF (Lab o2) rf2),
    ConsistentRF (Lab o1) rf1.

Lemma Pref_ConsistentRFhb:
  ∀ (Crfhb : ConsistentRFhb mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    ConsistentRFhb mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.

Lemma Pref_ConsistentRF_na:
  ∀
    (Crfhb : ConsistentRF_na mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    ConsistentRF_na mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.

Lemma Pref_sc_restr:
  same_relation _
    (sc_restr (Lab o1) sc1)
    (restr_rel (fun x ⇒ In x (Acts o1)) (sc_restr (Lab o2) sc2)).

Lemma Pref_SCrestriction:
  ∀ (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.

Lemma Pref_CoherentRR:
  ∀ (Crr : CoherentRR mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    CoherentRR mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.

Lemma Pref_CoherentWR:
  ∀ (Cwr : CoherentWR mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    CoherentWR mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.

Lemma Pref_CoherentRW:
  ∀ (Crw : CoherentRW mt2 (Lab o2) (Sb o2) (Asw o2) rf2 mo2),
    CoherentRW mt2 (Lab o1) (Sb o1) (Asw o1) rf1 mo1.

Lemma Pref_AtomicRMW:
  ∀ (Armw : AtomicRMW (Lab o2) rf2 mo2),
    AtomicRMW (Lab o1) rf1 mo1.

Lemma Pref_ConsistentAlloc:
  ∀ (Calloc: ConsistentAlloc (Lab o2)),
    ConsistentAlloc (Lab o1).

Lemma Pref_ConsistentDSB:
  ∀ (Cdsb : ConsistentDSB (Lab o2) (Sb o2) (Dsb o2)),
    ConsistentDSB (Lab o1) (Sb o1) (Dsb o1).

Lemma Pref_ConsistentSB:
  ∀ (Csb : ConsistentSB (Lab o2) (Sb o2)),
    ConsistentSB (Lab o1) (Sb o1).





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).

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).

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).

Lemma Pref_AcyclicityAxiom :
  ∀ 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.

Lemma Pref_Consistent :
  ∀ 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.

Lemma Pref_Semiconsistent :
  ∀ 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.

End Pref_Axioms.

Theorem Pref_Consistent2 :
  ∀ 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 →
    ∃ w',
      pre_execution mt (MT2sb,MT3rf) MTSChb o1 w'.