Require Import Classical List Relations Vbase.
Require Import ExtraRelations cactions RAmodels.
Set Implicit Arguments.
Remove Hints plus_n_O.

Section PowerModel.

Variable acts : list actid.
Variable lab : actid → act.
Variable po : actid → actid → Prop.
Variable rf : actid → option actid.
Variable rmw : actid → actid → Prop.
Variable co : actid → actid → Prop.

Definition ctrlisync x y := po x y ∧ is_read_only (lab x).

Definition lwsync x y := ∃ z, po x z ∧ clos_refl po z y ∧ is_write_only (lab z).

Definition rfe x y := rf y = Some x ∧ ¬ po x y.

Definition fr x y := ∃ z, rf x = Some z ∧ co z y.

Definition fre x y := ∃ z, rf x = Some z ∧ co z y ∧ ¬ po x y.

Definition coe x y := co x y ∧ ¬ po x y.

Definition ppo := ctrlisync.

Definition fence :=
  union (fun x y ⇒ is_read_only (lab x) ∧ lwsync x y)
        (fun x y ⇒ is_write_only (lab y) ∧ po x y).

Definition hb_power := union ppo (union fence rfe).

Definition prop_base :=
  (seq (clos_refl rfe) (seq fence (clos_refl_trans hb_power))).

Definition prop :=
  restr_rel (fun x ⇒ is_write_only (lab x)) prop_base.

Definition eqloc rel x y :=
  rel x y ∧ is_access (lab x) ∧ is_access (lab y) ∧ loc (lab x) = loc (lab y).

Definition uniproc_condition :=
  ∀ l, acyclic (union (restr_rel (fun x ⇒ is_access (lab x) ∧
                                                loc (lab x) = l) po)
                           (union (fun x y ⇒ rf y = Some x) (union co fr))).

Definition uniproc_condition_eqloc :=
  acyclic (union (eqloc po) (union (fun x y ⇒ rf y = Some x) (union co fr))).

Definition ConsistentPowerRA :=
  << FIN : ExecutionFinite acts lab po >> ∧
  << NOU : ∀ x (RMW: is_rmw (lab x)), False >> ∧
  << CsbT: transitive po >> ∧
  << CsbI: irreflexive po >> ∧
  << CrfD: ConsistentRF_dom lab rf >> ∧
  << COrf: CompleteRF lab rf >> ∧
  << Crmw: ConsistentRMW_dom lab po rmw >> ∧
  << CcoD: ConsistentMO_dom lab co >> ∧
  << CcoF: ∀ l, is_total (fun a ⇒ is_writeL (lab a) l) co >> ∧
  << CcoT: transitive co >> ∧
  << CcoI: irreflexive co >> ∧
  << LOC_SC : uniproc_condition >> ∧
  << ATOM : ∀ x y (RMW: rmw x y) z (FRE: fre x z) (COE: coe z y), False >> ∧
  << NTA : acyclic hb_power >> ∧
  << OBS : ∀ x y (FRE: fre x y) z (PROP: prop y z)
                  (HB: clos_refl_trans hb_power z x), False >> ∧
  << PROP: acyclic (union co prop) >>.

Lemma uniproc_condition_alt :
  ∀
    (CrfD: ConsistentRF_dom lab rf)
    (CcoD: ConsistentMO_dom lab co),
  uniproc_condition ↔ uniproc_condition_eqloc.
Proof.
  split; repeat red; ins.
  2: by eapply clos_trans_mon in H0; eauto;
        unfold union, eqloc, restr_rel; ins; desf; eauto.

  eapply (H (loc (lab x)) x).
  revert H0; generalize x at 1 3 4.
  intros ? K; apply clos_trans_t1n in K; induction K;
  red in H0; desf; vauto.
    by apply t_step; left; unfold eqloc, restr_rel in *; desf.
    by unfold eqloc, restr_rel in *; desf; rewrite H3;
       eapply t_trans with y; eauto; apply t_step; left;
       unfold eqloc, restr_rel in *; desf.
  assert (loc (lab x) = loc (lab y)) as ->; [|by eapply t_trans; vauto].
  clear - CrfD CcoD H0; unfold union, fr in *; desf;
  eauto using eq_sym, loceq_rf, loceq_mo.
  eapply loceq_rf in H0; eauto;
  eapply loceq_mo with (mo:=co) in H1; eauto; instantiate; congruence.
Qed.

End PowerModel.

Lemma is_read_only_access a : is_read_only a → is_access a.
Proof. by destruct a. Qed.

Lemma is_write_only_access a : is_write_only a → is_access a.
Proof. by destruct a. Qed.

Lemma is_read_only_read a : is_read_only a → is_read a.
Proof. by destruct a. Qed.

Lemma is_write_only_write a : is_write_only a → is_write a.
Proof. by destruct a. Qed.

Hint Resolve is_read_only_read is_read_only_access
     is_write_only_write is_write_only_access : caccess.

Lemma power_rfe_dom :
  ∀ lab po rf
         (NOU : ∀ x (RMW: is_rmw (lab x)), False)
         (CrfD: ConsistentRF_dom lab rf) x y
         (RFE: rfe po rf x y),
  is_write_only (lab x) ∧ is_read_only (lab y).
Proof.
  unfold rfe; ins; desc; eapply CrfD in RFE; desc.
  generalize (NOU x), (NOU y); ins;
  split; [destruct (lab x)|destruct (lab y)]; ins; exfalso; eauto.
Qed.

Lemma power_fre_dom :
  ∀ lab po rf co
         (NOU : ∀ x (RMW: is_rmw (lab x)), False)
         (CrfD: ConsistentRF_dom lab rf)
         (CcoD: ConsistentMO_dom lab co) x y
         (FRE: fre po rf co x y),
  is_read_only (lab x) ∧ is_write_only (lab y).
Proof.
  unfold fre; ins; desc; eapply CrfD in FRE; desc.
  eapply CcoD in FRE0; desc.
  generalize (NOU x), (NOU y); ins;
  split; [destruct (lab x)|destruct (lab y)]; ins; exfalso; eauto.
Qed.

Lemma ppo_trans lab po (T: transitive po) a b c :
  ppo lab po a b →
  ppo lab po b c →
  ppo lab po a c.
Proof.
  unfold ppo, ctrlisync; ins; desf; eauto.
Qed.

Lemma ppo_in_fence lab po a b :
  ppo lab po a b →
  is_write_only (lab b) →
  fence lab po a b.
Proof.
  unfold fence, ppo, ctrlisync, lwsync, union; ins; desf; eauto.
Qed.

Lemma ppo_fence_trans lab po (T: transitive po) a b c :
  ppo lab po a b →
  fence lab po b c →
  fence lab po a c.
Proof.
  unfold fence, ppo, ctrlisync, lwsync, union; ins; desf; eauto 8.
Qed.

Lemma fence_trans lab po (T: transitive po) a b c :
  fence lab po a b →
  fence lab po b c →
  fence lab po a c.
Proof.
  unfold fence, ppo, ctrlisync, lwsync, union, clos_refl; ins; desf; desf; eauto 9.
  by destruct (lab b); ins.
Qed.

Lemma fence_ppo_trans lab po (T: transitive po) a b c :
  fence lab po a b →
  ppo lab po b c →
  fence lab po a c.
Proof.
  unfold fence, ppo, ctrlisync, lwsync, union, clos_refl; ins; desf; desf; eauto 9.
  by destruct (lab b); ins.
Qed.

Lemma power_hb2 :
  ∀ acts lab po rf rmw co
    (CONS: ConsistentPowerRA acts lab po rf rmw co) a b
    (HB: clos_trans (hb_power lab po rf) a b),
  ppo lab po a b ∧ ¬ is_write_only (lab b) ∨
  seq (rfe po rf) (clos_refl (ppo lab po)) a b ∧ ¬ is_write_only (lab b) ∨
  seq (clos_refl (rfe po rf))
      (seq (fence lab po) (clos_refl_trans (hb_power lab po rf))) a b.
Proof.
  ins; red in CONS; desc.
  apply clos_trans_t1n in HB; induction HB; unfold hb_power, union in H;
  destruct H as [|[]]; eauto.
    case_eq (is_write_only (lab y)) as R; eauto.
    by right; right; ∃ x; split; vauto;
        ∃ y; eauto using rt_refl, ppo_in_fence.

    by right; right; ∃ x; repeat (eexists; vauto).

    edestruct power_rfe_dom; eauto.
    by right; left; repeat (eexists; try edone); vauto; destruct (lab y).

{
    desf; eauto using ppo_trans.
      red in IHHB; desc; eapply power_rfe_dom in IHHB; desc; eauto.
      eapply ppo_in_fence in H; eauto.
      right; right; eexists; split; vauto; eexists; split; vauto.
      by apply clos_t1n_trans in HB; eauto using clos_trans_in_rt.
    right; right; red in IHHB; desc; inv IHHB; clear IHHB.
      by red in IHHB0; desc; eexists; split; vauto; red; eauto using ppo_fence_trans.
    eapply power_rfe_dom in H0; eauto; desc; eapply ppo_in_fence in H; eauto.
    by eexists; split; [by vauto|]; eexists;
       eauto using clos_trans_in_rt, clos_t1n_trans.
}

  apply clos_t1n_trans in HB; clear IHHB.
  by right; right; ∃ x; repeat (eexists; vauto); auto using clos_trans_in_rt.

  edestruct power_rfe_dom; eauto.
  desf.
    by right; left; split; ins; eexists; eauto using r_step.

    by unfold seq in *; desf; eapply power_rfe_dom in IHHB; eauto; desc; destruct (lab y).

    right; right; red; red in IHHB; desf.
    inv IHHB; [by eexists; eauto; vauto|].
    by eapply power_rfe_dom in H2; eauto; desc; destruct (lab y); ins.
Qed.

Lemma power_hb_prop :
  ∀ acts lab po rf rmw co
    (CONS: ConsistentPowerRA acts lab po rf rmw co) a b
    (HB: clos_trans (hb_power lab po rf) a b)
    (A : is_write_only (lab a))
    (B : is_write_only (lab b)),
  prop lab po rf a b.
Proof.
  ins; assert (K:=CONS); red in K; desc.
  eapply power_hb2 in HB; eauto; desf.
Qed.

Lemma power_hb :
  ∀ acts lab po rf rmw co
    (CONS: ConsistentPowerRA acts lab po rf rmw co) a b
    (HB: happens_before po rf a b)
    (COND: is_read_only (lab a) ∨ is_write_only (lab b) ∨ ¬ po a b),
  clos_trans (hb_power lab po rf) a b.
Proof.
  ins; assert (K:=CONS); red in K; desc.
  eapply clos_trans_mon with (r' := fun x y ⇒ po x y ∨ rf y = Some x ∧ ¬ po x y) in HB.
    2: by ins; destruct (classic (po a0 b0)); desf; eauto.
  eapply path_tur with (adom := fun x ⇒ is_write_only (lab x))
                       (bdom := fun x ⇒ is_read_only (lab x))
    in HB; eauto.
  2: by intros; desc; apply CrfD in R; desc; specialize (NOU x);
        destruct (lab x); ins; exfalso; eauto.
  2: by intros; desc; apply CrfD in R; desc; specialize (NOU y);
        destruct (lab y); ins; exfalso; eauto.
  destruct HB.
    by apply t_step; unfold hb_power, ppo, fence, lwsync, ctrlisync, union; desf; eauto.
  desc.
  eapply t_rt_trans.
    eapply clos_trans_mon; eauto.
    by clear; ins; unfold hb_power, ppo, fence, lwsync, ctrlisync, rfe, union; desf; eauto.
  clear - H0; desf; vauto.
Qed.

Lemma observation :
  ∀ acts lab po rf rmw co
    (CONS: ConsistentPowerRA acts lab po rf rmw co)
    x y (FRE: fre po rf co x y) (PROP: prop_base lab po rf y x),
    False.
Proof.
  ins; unfold ConsistentPowerRA, prop, restr_rel in *; desc.
  unfold prop, prop_base, seq in *; desf.
  rewrite uniproc_condition_alt in *; auto.
  exploit power_fre_dom; eauto; intro M; desc.
  destruct (classic (is_write_only (lab z0))).
    eapply OBS; eauto.
    by repeat eexists; eauto using clos_refl_trans.
  apply clos_rt_rt1n in PROP2.
  induction PROP2.
    assert (po z x).
      by clear - CsbT PROP1; unfold fence, union, lwsync, clos_refl in *; desf;
         desf; eauto.
    clear PROP1; red in FRE; desc.
    exploit loceq_rf; eauto; exploit loceq_mo; eauto; intros A B.
    rewrite A in B.
    unfold clos_refl in *; desf;
    [|red in PROP; desc; exploit loceq_rf; try exact PROP; eauto; intro C];
    eapply (LOC_SC z); unfold union, eqloc, fr.

    by eapply t_trans with x; eapply t_step; eauto 8 using eq_sym with caccess.

    rewrite <- B in C.
    exploit CrfD; try exact PROP; eauto; ins; desc.
    by eapply t_trans with x, t_trans with y; eapply t_step; eauto 8 with caccess.

  destruct (classic (is_write_only (lab y0))).
    eapply OBS with (z := y0); eauto using clos_rt1n_rt.
    by repeat eexists; eauto using clos_refl_trans.
  eapply IHPROP2; clear IHPROP2; eauto.
  unfold hb_power, union in *; desf; eauto using fence_trans, fence_ppo_trans.
  by eapply power_rfe_dom in H0; eauto; desf.
Qed.

Theorem ConsistentPowerRA_SRArmw :
  ∀ acts lab po rf rmw co
    (CONS: ConsistentPowerRA acts lab po rf rmw co),
  ConsistentSRArmw acts lab po rf rmw
    (restr_rel (fun x ⇒ is_write_only (lab x)) (tot_ext acts (union co (prop lab po rf)))).
Proof.
  ins; assert (K:=CONS); red in K; red; desf; unnw.
  rewrite uniproc_condition_alt in *; auto.
  intuition.

  red; unfold restr_rel; ins; desc; eauto.

  by eapply power_hb in H; eauto.

  by red; unfold restr_rel; ins; desc; eauto with caccess.

  by red; unfold restr_rel; ins;
    assert (is_write_only (lab a)) by (specialize (NOU a); destruct (lab a); ins; exfalso; eauto);
    assert (is_write_only (lab b)) by (specialize (NOU b); destruct (lab b); ins; exfalso; eauto);
    eapply (tot_ext_total acts (union co (prop lab po rf))) in NEQ;
    desf; eauto; apply FIN; intro X; rewrite X in *; ins.

  by eapply restr_rel_trans, tot_ext_trans.

  by red; unfold restr_rel; ins; desc; eapply tot_ext_irr; eauto.

  red; unfold restr_rel; ins; desc.
  eapply power_hb in HB; eauto.
  eapply power_hb_prop in HB; eauto.
  by eapply tot_ext_irr, tot_ext_trans, tot_ext_extends; try edone; vauto.

  red; unfold restr_rel; ins; desc.
  destruct (eqP a b) as [|NEQ]; [by subst; eapply tot_ext_irr; eauto|].
  exploit CrfD; eauto; ins; desf.
  assert (is_writeL (lab b) l).
    by destruct (lab b); ins; destruct (lab a); ins; destruct (lab c); ins; desf.
  eapply CcoF in NEQ; eauto with caccess; desf.
  2: by eapply tot_ext_irr, tot_ext_trans, tot_ext_extends; try edone; vauto.
  eapply power_hb in HB; eauto.

  assert (M:=HB); eapply power_hb2 in HB; eauto.
  desf.
    by repeat red in HB; desc; destruct (lab b).

    unfold seq, rfe, ppo, ctrlisync, clos_refl in HB; desc;
    desf; eauto.

  eapply (LOC_SC b); unfold union, eqloc, mofr.
  eapply t_trans with z, t_trans with c; eapply t_step; eauto 8 with caccess.
    left; repeat split; eauto with caccess.
    eapply loceq_rf in HB; eauto; eapply loceq_rf in RF; eauto; instantiate; congruence.
  by right; right; right; repeat eexists; eauto with caccess; intro; desf.

  eapply observation; eauto.
  repeat eexists; eauto; intro; red in HB; desc.
  eapply (NTA b), t_trans, t_step; eauto; left; split; ins.
  by specialize (NOU c); destruct (lab c); ins; exfalso; auto.

  right; right; intro.
  eapply (LOC_SC b); unfold union, eqloc, mofr.
  eapply t_trans with c; eapply t_step; eauto 8 with caccess.
    left; repeat split; eauto with caccess.
    by destruct (lab b); ins; destruct (lab c); ins; destruct (lab a); ins; desf.
  by right; right; right; repeat eexists; eauto with caccess; intro; desf; eauto.

  red; unfold restr_rel; ins; desf.
  destruct (eqP a b) as [|CO]; [by desf; eapply tot_ext_irr; eauto|].
  eapply CcoF with (l := loc (lab a)) in CO; eauto.
    2: by (destruct (lab a); ins; desf).
    2: by (destruct (lab b); ins; desf).
  desf; [|by eapply tot_ext_irr with (x:=a), tot_ext_trans, tot_ext_extends;
             try edone; vauto].
  exploit Crmw; eauto; ins; desc.
  destruct (eqP b d) as [|CO']; [by desf; eapply tot_ext_irr; eauto|].
  eapply CcoF with (l := loc (lab b)) in CO'; eauto.
    2: by (destruct (lab b); ins; desf).
    2: by eapply loceq_rf in RF; eauto; destruct (lab c); ins; desf; congruence.
  desf; [|by eapply tot_ext_irr with (x:=b), tot_ext_trans, tot_ext_extends;
             try edone; vauto].
  eapply ATOM with (z:=b); repeat eexists; eauto.

  assert (b ≠ d) by (intro; desf; eauto).
  intro X; eapply POI' in X; eauto.
  apply (LOC_SC d); unfold union, eqloc, mofr.
  eapply t_trans with b; apply t_step.
    by left; repeat split; eauto using eq_sym, loceq_mo with caccess.
  by right; right; left; repeat split; ins.

  assert (b ≠ c) by (intro; desf; destruct (lab c); ins).
  intro X; eapply POI in X; eauto.
  apply (LOC_SC c); unfold union, eqloc, mofr.
  eapply t_trans with b; apply t_step.
    by right; right; right; repeat eexists; eauto.
  left; repeat split; eauto with caccess; eapply loceq_rf in RF; eauto; instantiate; congruence.
Qed.

Lemma incl_hb_power_sra lab po (T: transitive po) rf a b :
  hb_power lab po rf a b →
  po a b ∨ rf b = Some a.
Proof.
  unfold hb_power, ppo, fence, rfe, ctrlisync, lwsync, union, clos_refl;
  ins; desf; eauto.
Qed.

Lemma incl_mhb_power_sra lab po (T: transitive po) rf a b :
  clos_refl_trans (hb_power lab po rf) a b →
  clos_refl_trans (fun x y ⇒ po x y ∨ rf y = Some x) a b.
Proof.
  ins; eapply clos_refl_trans_mon; eauto using incl_hb_power_sra.
Qed.

Lemma incl_prop_base_sra lab po (T: transitive po) rf a b :
  prop_base lab po rf a b →
  happens_before po rf a b.
Proof.
  unfold prop_base, seq, ppo, fence, rfe, ctrlisync, lwsync, union, clos_refl;
  ins; desf; eauto with hb;
  eapply t_rt_trans, incl_mhb_power_sra; eauto; eauto 8 using clos_trans.
Qed.

Ltac com_ext_trans_tac CmoF a :=
  let N := fresh in destruct a as [|N]; [|eapply CmoF in N];
  desf; eauto 10 with caccess;
  try (by exfalso; eauto using loceq_mo with hb).

Ltac com_ext_trans_tac' a :=
  destruct a; desf; eauto 9 with caccess;
  try (by exfalso; eauto using loceq_mo with hb).

Ltac add_locs CrfD CmoD :=
    repeat match goal with
      | [H: _ = Some _ |- _] ⇒ generalize (CrfD _ _ H); revert H
      | [H: _ |- _] ⇒ generalize (CmoD _ _ H); revert H
    end; ins; desf;
    repeat match goal with
      | H: is_writeL ?a ?l, H' : context[loc ?a] |- _ ⇒
        let EQ := fresh in assert (EQ: loc a = l) by (destruct a; ins; desf); rewrite EQ in *; clear EQ
      | H: is_readLV ?a ?l _, H' : context[loc ?a] |- _ ⇒
        let EQ := fresh in assert (EQ: loc a = l) by (destruct a; ins; desf); rewrite EQ in *; clear EQ
      | H: is_writeLV ?a ?l _, H' : is_readLV ?a ?l' _ |- _ ⇒
        assert (l = l') by (destruct a; ins; desf); subst; clear H'
      | H: is_writeL ?a ?l, H' : is_readLV ?a ?l' _ |- _ ⇒
        assert (l = l') by (destruct a; ins; desf); subst; clear H'
      | H: is_writeL ?a ?l, H' : is_writeLV ?a ?l' _ |- _ ⇒
        assert (l = l') by (destruct a; ins; desf); subst; clear H'
      | H: is_writeL ?a ?l, H' : is_writeL ?a ?l' |- _ ⇒
        assert (l = l') by (destruct a; ins; desf); subst; clear H'
      | H: is_readL ?a ?l, H' : is_readLV ?a ?l' _ |- _ ⇒
        assert (l = l') by (destruct a; ins; desf); subst; clear H'
    end.

Lemma mofr_trans :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo) l a b c,
    mofr lab rf mo l a b →
    mofr lab rf mo l b c →
    mofr lab rf mo l a c.
Proof.
  unfold mofr, ConsistentRA; ins; desf; unnw; eauto 10;
    add_locs CrfD CmoD.
    by com_ext_trans_tac' (eqP a c).
    by com_ext_trans_tac CmoF (eqP a c).
    by com_ext_trans_tac CmoF (eqP b c); com_ext_trans_tac' (eqP a c).
Qed.

Lemma mofr_shorten_hb :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo) l a b c d,
    mofr lab rf mo l a b →
    happens_before sb rf b c →
    mofr lab rf mo l c d →
    mofr lab rf mo l a d.
Proof.
  unfold mofr, ConsistentRA; ins; desf; unnw; add_locs CrfD CmoD; subst.
    by com_ext_trans_tac CmoF (eqP b c).
    by com_ext_trans_tac CmoF (eqP b d); com_ext_trans_tac' (eqP a d).
    by com_ext_trans_tac CmoF (eqP a d).
    by com_ext_trans_tac CmoF (eqP b d); com_ext_trans_tac' (eqP a d).
Qed.

Lemma mofr_shorten :
  ∀ acts lab sb rf mo
         (CONS: ConsistentRA acts lab sb rf mo) l a b c d,
    mofr lab rf mo l a b →
    clos_refl_trans (fun x y ⇒ sb x y ∨ rf y = Some x) b c →
    mofr lab rf mo l c d →
    mofr lab rf mo l a d.
Proof.
  ins; rewrite clos_refl_transE in *; desf;
  eauto using mofr_trans, mofr_shorten_hb.
Qed.

Lemma weaken_rmw :
  ∀ acts lab po rf rmw mo
    (CONS: ConsistentSRArmw acts lab po rf rmw mo),
    ConsistentSRA acts lab po rf mo.
Proof.
  unfold ConsistentSRA, ConsistentSRArmw; ins; desc; unnw; intuition.
  red; ins.
  apply CrfD in RF; apply CmoD in MO'; eapply (NOU c); desc.
  by destruct (lab c); ins.
Qed.

Require Import Setoid.
Add Morphism fr with signature
    eq ==> same_relation ==> same_relation as fr_mor.
Proof.
  unfold fr; split; red; ins; desf; eapply H in H1; eauto.
Qed.

Lemma rf_eqloc lab rf (CrfD: ConsistentRF_dom lab rf) :
  (fun x y ⇒ rf y = Some x) <--> eqloc lab (fun x y ⇒ rf y = Some x).
Proof.
  unfold eqloc; split; red; ins; desf.
  exploit CrfD; eauto; ins; desf.
  eauto 10 using eq_sym, loceq_rf with caccess.
Qed.

Lemma fr_eqloc lab rf mo
    (CrfD: ConsistentRF_dom lab rf) :
  fr rf (eqloc lab mo) <--> eqloc lab (fr rf mo).
Proof.
  unfold fr, eqloc; split; red; ins; desf; repeat (eexists; try edone);
  exploit loceq_rf; eauto; exploit CrfD; eauto; ins; desc; eauto with caccess;
  instantiate; congruence.
Qed.

Lemma union_eqloc lab r r' :
  union (eqloc lab r) (eqloc lab r') <--> eqloc lab (union r r').
Proof.
  unfold union, eqloc; split; red; ins; desf; eauto.
Qed.

Lemma acyclic_eqloc lab r :
  (∀ l, acyclic (restr_rel (fun x ⇒ is_access (lab x) ∧ loc (lab x) = l) r)) →
  acyclic (eqloc lab r).
Proof.
  repeat red; ins; eapply (H (loc (lab x)) x).
  revert H0; generalize x at 1 3 4; unfold eqloc, restr_rel; ins.
  apply clos_trans_t1n in H0; induction H0; desc; vauto.
  rewrite H4; eauto 8 using clos_trans.
Qed.

Lemma mofr_cycle1 :
  ∀ acts lab po rf mo
    (CONS: ConsistentRA acts lab po rf mo) l a b
    (MOFR: mofr lab rf mo l a b)
    (CRT: clos_refl_trans (fun x y ⇒ po x y ∨ rf y = Some x) b a),
  False.
Proof.
  unfold ConsistentRA, mofr; ins; desc;
  rewrite clos_refl_transE in *; desf; eauto.
Qed.

Lemma ConsistentSRA_uniproc :
  ∀ acts lab po rf mo
    (CONS: ConsistentSRA acts lab po rf mo)
    (NOU : ∀ x (RMW: is_rmw (lab x)), False),
   uniproc_condition lab po rf
     (fun x y : actid ⇒
      ∃ l : nat, mo x y ∧ is_writeL (lab x) l ∧ is_writeL (lab y) l).
Proof.
  ins; assert (K:=CONS); red in K; desc.

  assert (EQ: (fun x y ⇒ ∃ l, mo x y ∧ is_writeL (lab x) l ∧ is_writeL (lab y) l)
                <--> eqloc lab (fun x y ⇒ mo x y ∧ loc (lab x) = loc (lab y))).
    unfold eqloc; split; red; ins; desf; [|∃ (loc (lab x))]; repeat split; eauto;
    by eapply CmoD in H; desc; destruct (lab x); ins; destruct (lab y); ins; desf.
  eapply uniproc_condition_alt; ins.
    by red; ins; desf; eauto.
  red; ins; rewrite EQ, fr_eqloc, rf_eqloc, !union_eqloc; eauto.
  eapply acyclic_eqloc; clear EQ; ins.
  rewrite <- 2!union_restr.
  assert (EQ: restr_rel (fun x ⇒ is_access (lab x) ∧ loc (lab x) = l)
                        (union (fun x y ⇒ mo x y ∧ loc (lab x) = loc (lab y))
                               (fr rf (fun x y ⇒ mo x y ∧ loc (lab x) = loc (lab y))))
              <--> mofr lab rf (fun x y ⇒ mo x y ∧ loc (lab x) = loc (lab y)) l).
    unfold restr_rel, union, eqloc, mofr, fr; split; red; ins; desf; [left|right| |];
    repeat split; eauto 8 with caccess.
      by eapply CmoD in H; desc; destruct (lab x); ins.
      by eapply CmoD in H; desc; destruct (lab y); ins.
    exploit CrfD; eauto; exploit CmoD; eauto; ins; desf; desf;
    by repeat (eexists; try edone); eauto; try (intro; desf; eapply (NOU y));
       destruct (lab y); ins; destruct (lab x); ins.
  rewrite EQ; clear EQ.
  repeat red; ins.
  assert (RT: union (clos_refl_trans (fun x y ⇒ po x y ∨ rf y = Some x))
              (seq (clos_refl_trans (fun x y ⇒ po x y ∨ rf y = Some x))
                   (seq (mofr lab rf (fun x y ⇒ mo x y ∧ loc (lab x) = loc (lab y)) l)
                   (clos_refl_trans (fun x y ⇒ po x y ∨ rf y = Some x)))) x x).
   by vauto.
  apply ConsistentSRA_RA in CONS.
  revert H RT; generalize x at 2 3; unfold union, restr_rel, seq.
  intros ? P; ins; apply clos_trans_t1n in P; induction P; desf;
    try (by eapply ACYC, t_rt_trans; eauto using t_step);
    eauto 6 using mofr_cycle1, clos_refl_trans.
  by exploit mofr_shorten; eauto; eauto using mofr_cycle1.
  by eapply IHP; eauto 9 using clos_refl_trans.
  by eapply IHP; eauto 9 using clos_refl_trans.
  by eapply IHP; eauto 9 using clos_refl_trans.
  by exploit mofr_shorten; eauto; eauto using mofr_cycle1;
     ins; eapply IHP; eauto 9 using clos_refl_trans.
Qed.

Theorem ConsistentSRArmw_PowerRA :
  ∀ acts lab po rf rmw mo
    (CONS: ConsistentSRArmw acts lab po rf rmw mo),
  ConsistentPowerRA acts lab po rf rmw
     (fun x y ⇒ ∃ l, mo x y ∧ is_writeL (lab x) l ∧ is_writeL (lab y) l).
Proof.
  ins.
  assert (K:=CONS); red in K; red; desc; unnw; repeat (split; try done).
  by red; ins; eauto with hb.
  by red; ins; desf; eauto.
  by red; ins; eapply CmoF in NEQ; desf; eauto with caccess.
  by red; ins; desf; assert (l = l0) by (destruct (lab y); ins; desf); subst; eauto 6.
  by red; ins; desf; eauto.

  by eauto using ConsistentSRA_uniproc, weaken_rmw.

  unfold fre, coe; ins; desf.
  eapply Cat; try exact FRE; eauto.
  by destruct (lab z); ins; desf; destruct (lab z0); ins; desf.

  by eapply acyclic_mon; eauto; red; apply incl_hb_power_sra.

  unfold fre, prop, restr_rel; ins; desf.
  eapply incl_prop_base_sra in PROP; eauto.
  eapply incl_mhb_power_sra in HB; eauto.
  eapply Cwr; try eapply t_rt_trans; eauto.
  by destruct (lab z0); ins; destruct (lab y); ins; desf.

  unfold union, prop, restr_rel; eapply acyclic_mon with (rel:=mo);
  eauto using trans_irr_acyclic.
  red; ins; desf; apply incl_prop_base_sra in H; eauto.
  destruct (eqP x y) as [|NEQ]; [|apply CmoF in NEQ; desf; eauto with caccess];
  desf; exfalso; eauto.
Qed.

Theorem ConsistentPowerRA_iff_SRArmw :
  ∀ acts lab po rf rmw,
    (∃ co, ConsistentPowerRA acts lab po rf rmw co)
    ↔ (∃ mo, ConsistentSRArmw acts lab po rf rmw mo).
Proof.
  split; ins; desf;
  eauto using ConsistentPowerRA_SRArmw, ConsistentSRArmw_PowerRA.
Qed.