Require Import List Vbase Relations ExtraRelations actions c11 cmon reorder.
Set Implicit Arguments.

Lemma path_decomp_u1_pre :
  ∀ X rel a b x y
         (T: clos_trans X (rel UNION1 (a, b)) x y)
         (DOM : ∀ x, rel b x → rel a x),
    clos_trans X rel x y ∨ clos_refl_trans X rel x a ∧ y = b.

Lemma release_seq_u1_pre :
  ∀ mt2 lab sb rf mo a b x y
    (HB: release_seq mt2 lab (sb UNION1 (a,b)) rf mo x y)
    (NWRI: ¬ is_write (lab b))
    (DOM: ∀ x (SB: sb b x), sb a x)
    (NMO: ∀ x (MO: mo b x), False)
    (NMO': ∀ x (MO: mo x b), False),
    release_seq mt2 lab sb rf mo x y.

Lemma path_decomp_u1_post :
  ∀ X rel a b x y
         (T: clos_trans X (rel UNION1 (a, b)) x y)
         (DOM : ∀ x, rel x a → rel x b),
    clos_trans X rel x y ∨ x = a ∧ clos_refl_trans X rel b y.

Lemma release_seq_u1_post :
  ∀ mt2 lab sb rf mo a b x y
    (HB: release_seq mt2 lab (sb UNION1 (a,b)) rf mo x y)
    (NWRI: ¬ is_write (lab a))
    (DOM: ∀ x (SB: sb x a), sb x b)
    (NMO: ∀ x (MO: mo a x), False)
    (NMO': ∀ x (MO: mo x a), False),
    release_seq mt2 lab sb rf mo x y.

Lemma path_decomp_u1_both :
  ∀ X rel a b x y
         (T: clos_trans X (rel UNION1 (a, b)) x y)
         (DOM : ∀ x, rel b x → rel a x)
         (DOM' : ∀ x, rel x a → rel x b),
    clos_trans X rel x y ∨ x = a ∧ y = b.

Lemma RacqFacq_hb :
  ∀ mt2 lab (sb asw : relation actid) rf mo
    (Cmo: ConsistentMO lab mo) a b
    (DOM: ∀ x (SB: sb b x), sb a x)
    (DOM': ∀ x (SB: asw b x), asw a x)
    (DOM'': ∀ x (SB: sb x a), sb x b)
    (Aa: is_acquire_read (lab a))
    (Ab: lab b = Afence (thread (lab a)) FATacq) c d
    (HB: happens_before mt2 lab (sb UNION1 (a,b)) asw rf mo c d),
    happens_before mt2 lab sb asw rf mo c d
    ∨ c = a ∧ d = b
    ∨ happens_before mt2 lab sb asw rf mo c a ∧ d = b.

Lemma RacqFacq_acyclic :
  ∀ mt2 lab sb asw rf mo rel
    (Cmo: ConsistentMO lab mo)
    (ACYC : acyclic (fun x y ⇒ happens_before mt2 lab sb asw rf mo x y ∨ rel x y)) a b
    (Aa: is_acquire_read (lab a))
    (Ab: lab b = Afence (thread (lab a)) FATacq)
    (DOM: ∀ x (SB: sb b x), sb a x)
    (DOM': ∀ x (SB: asw b x), asw a x)
    (DOM'': ∀ x (SB: sb x a), sb x b)
    (NREL: ∀ z (REL: rel b z), False),
   acyclic (fun x y ⇒ happens_before mt2 lab (sb UNION1 (a, b)) asw rf mo x y ∨ rel x y).

Theorem RacqFacq_par :
  ∀ mt mt2 mtsc acts lab sb dsb asw rf mo sc
    (CONS: Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc)
    a (Aa: is_acquire_read (lab a))
    b (Ab: lab b = Afence (thread (lab a)) FATacq)
    (DOM: ∀ x (SB: sb b x), sb a x)
    (DOM': ∀ x (SB: asw b x), asw a x)
    (DOM'': ∀ x (SB: sb x a), sb x b),
    ≪ CONS': Consistent mt mt2 mtsc acts lab (sb UNION1 (a,b)) dsb asw rf mo sc ≫ ∧
    ≪ RACE: racy mt2 lab sb asw rf mo → racy mt2 lab (sb UNION1 (a,b)) asw rf mo ≫.

Corollary RacqFacq_par_paper :
  ∀ mt mt2 mtsc acts lab sb dsb asw rf mo sc a b,
    Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc →
    adjacent sb a b →
    adjacent asw a b →
    is_acquire_read (lab a) →
    lab b = Afence (thread (lab a)) FATacq →
  ≪ CONS': Consistent mt mt2 mtsc acts lab (sb UNION1 (a,b)) dsb asw rf mo sc ≫ ∧
  ≪ RACE: racy mt2 lab sb asw rf mo → racy mt2 lab (sb UNION1 (a,b)) asw rf mo ≫.

Lemma FrelWrel_hb :
  ∀ mt2 lab (sb asw : relation actid) rf mo a b
    (Cmo: ConsistentMO lab mo)
    (DOM: ∀ x (SB: sb b x), sb a x)
    (DOM': ∀ x (SB: asw x a), asw x b)
    (DOM'': ∀ x (SB: sb x a), sb x b)
    (Ab: is_release_write (lab b))
    (Aa: lab a = Afence (thread (lab b)) FATrel) c d
    (HB: happens_before mt2 lab (sb UNION1 (a,b)) asw rf mo c d),
    happens_before mt2 lab sb asw rf mo c d
    ∨ c = a ∧ d = b
    ∨ c = a ∧ happens_before mt2 lab sb asw rf mo b d.

Lemma FrelWrel_acyclic :
  ∀ mt2 lab sb asw rf mo rel
    (Cmo: ConsistentMO lab mo)
    (ACYC : acyclic (fun x y ⇒ happens_before mt2 lab sb asw rf mo x y ∨ rel x y))
    a b
    (Aa: lab a = Afence (thread (lab b)) FATrel)
    (Ab: is_release_write (lab b))
    (DOM: ∀ x (SB: sb b x), sb a x)
    (DOM': ∀ x (SB: asw x a), asw x b)
    (DOM'': ∀ x (SB: sb x a), sb x b)
    (NREL: ∀ z (REL: rel z a), False),
   acyclic (fun x y ⇒ happens_before mt2 lab (sb UNION1 (a, b)) asw rf mo x y ∨ rel x y).

Theorem FrelWrel_par :
  ∀ mt mt2 mtsc acts lab sb dsb asw rf mo sc
    (CONS: Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc) a b
    (Aa: lab a = Afence (thread (lab b)) FATrel)
    (Ab: is_release_write (lab b))
    (DOM: ∀ x (SB: sb b x), sb a x)
    (DOM': ∀ x (SB: asw x a), asw x b)
    (DOM'': ∀ x (SB: sb x a), sb x b),
    ≪ CONS': Consistent mt mt2 mtsc acts lab (sb UNION1 (a,b)) dsb asw rf mo sc ≫ ∧
    ≪ RACE: racy mt2 lab sb asw rf mo → racy mt2 lab (sb UNION1 (a,b)) asw rf mo ≫.

Corollary FrelWrel_par_paper :
  ∀ mt mt2 mtsc acts lab sb dsb asw rf mo sc a b,
    Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc →
    adjacent sb a b →
    adjacent asw a b →
    lab a = Afence (thread (lab b)) FATrel →
    is_release_write (lab b) →
  ≪ CONS': Consistent mt mt2 mtsc acts lab (sb UNION1 (a,b)) dsb asw rf mo sc ≫ ∧
  ≪ RACE: racy mt2 lab sb asw rf mo → racy mt2 lab (sb UNION1 (a,b)) asw rf mo ≫.