Require Import Classical List Permutation Relations Peano_dec Setoid Omega.
Require Import Vbase extralib ExtraRelations cactions WMModels.
Set Implicit Arguments.
Remove Hints plus_n_O.

Lemma ConsistentMO_dom_restr_eq lab mo :
  ConsistentMO_big_dom lab mo →
  ConsistentMO_dom lab (restr_eq_rel (fun x : actid ⇒ loc (lab x)) mo).
Proof.
  unfold ConsistentMO_dom, ConsistentMO_big_dom, restr_eq_rel; intuition.
  exploit H; eauto; ins; desf; destruct (lab a); ins; destruct (lab b); ins; vauto.
Qed.

Lemma is_total_restr_eq X lab (mo : relation X) l :
  is_total (fun a ⇒ is_write (lab a)) mo →
  is_total (fun a ⇒ is_writeL (lab a) l) (restr_eq_rel (fun x ⇒ loc (lab x)) mo).
Proof.
  unfold restr_eq_rel; red; ins; apply H in NEQ; eauto with caccess;
  destruct (lab a); ins; destruct (lab b); ins; desf; vauto.
Qed.

Theorem ModelSC_total_mo lab sb rf :
  (∃ mo, ModelSC_total lab sb rf mo) ↔
  (∃ mo, ModelSC_mo lab sb rf mo).
Proof.
  unfold ModelSC_total, ModelSC_mo; split; ins; desf; unnw.
  { ∃ (fun x y ⇒ ∃ l, mo x y ∧ is_writeL (lab x) l ∧ is_writeL (lab y) l);
      intuition; repeat red; ins; desf; eauto.
    by eapply CscF in NEQ; desf; eauto with caccess.
    by assert (l=l0) by (destruct (lab y); ins; desf); desf; eauto.
    eapply (CscI x); revert H; generalize x at 1 3; unfold reads_before, union;
    induction 1; desf; eauto.
    eapply CscF in H1; desf; eauto with caccess.
    exfalso; eapply Cwr; try exact H; eauto with caccess.
    destruct (lab y); ins; destruct (lab z); ins; desf.
  }
  { ∃ (tot_ext_nat (sb +++ rf_external sb rf +++ mo +++ reads_before lab rf mo));
    unfold inclusion; intuition; eauto using tot_ext_nat_trans, tot_ext_nat_irr;
      try solve [unfold union; eauto using tot_ext_nat_extends].
    by red; ins; eapply tot_ext_nat_total; eauto.
    red; ins; desf.
    exploit CrfD; eauto; ins; desf.
    destruct (eqP a b) as [|NEQ]; desf; [by eapply tot_ext_nat_irr in SC; eauto|].
    destruct (eqP c b); desf; [by eapply tot_ext_nat_irr in SC'; eauto|].
    assert (is_writeL (lab b) l).
      by destruct (lab b); ins; destruct (lab a); ins; desf.
    eapply CmoF in NEQ; desf; eauto with caccess.
      eapply tot_ext_nat_irr with (x:=b); eauto.
      eapply tot_ext_nat_trans, tot_ext_nat_extends; eauto.
      by unfold union, reads_before; eauto 10 with caccess.
    eapply tot_ext_nat_irr with (x:=a); eauto.
    eapply tot_ext_nat_trans, tot_ext_nat_extends; eauto.
    by unfold union; eauto with caccess.
  }
Qed.

Theorem ModelSC_total_bigmo lab sb rf :
  (∃ mo, ModelSC_total lab sb rf mo) ↔
  (∃ mo, ModelSC_bigmo lab sb rf mo).
Proof.
  split; intro X; desc.
  {
    ∃ (restr_rel (fun x ⇒ is_write (lab x)) mo).
    unfold ModelSC_bigmo, ModelSC_total, ConsistentMO_big_dom in *; desf; unnw.
    assert (HBSC: inclusion (happens_before sb rf) mo).
      by induction 1; unfold union in *; desf; eauto.
    assert (RB: inclusion (reads_before lab rf mo) mo).
      red; unfold reads_before; ins; desf.
      apply CscF in H1; desf; eauto with caccess.
      edestruct Cwr; try exact H; eauto with caccess.
      by eapply CrfD in H; desf; destruct (lab x); ins; desf;
         destruct (lab z); ins; desf; destruct (lab y); ins; desf.
    assert (MO: inclusion (mo;;mo) mo) by (red; unfold seq; ins; desf; eauto).
    rewrite HBSC.
    intuition;
        eauto using restr_rel_trans, irreflexive_restr;
        try solve [unfold restr_rel in *; desf].
    by apply is_total_restr; red; ins; apply CscF; eauto with caccess.
    all: by rewrite (inclusion_restr_rel_l (inclusion_refl _)), ?RB, ?MO.
  }
  {
    eapply ModelSC_total_mo; eauto.
    ∃ (restr_eq_rel (fun x ⇒ loc (lab x)) mo).
    unfold ModelSC_bigmo, ModelSC_mo in *; desf; unnw; intuition;
    eauto using transitive_restr_eq, ConsistentMO_dom_restr_eq,
                         is_total_restr_eq;
      try (by rewrite inclusion_restr_eq).
      rewrite inclusion_restr_eq.
      cut (acyclic (happens_before sb rf +++ mo +++ reads_before lab rf mo)).
        apply inclusion_acyclic; unfold happens_before, union;
        red; ins; desf; eauto 10 using t_step.
      eapply min_cycle with (rel':=mo); eauto.
      by unfold union; red; eauto using clos_trans.
      by unfold union, irreflexive, seq in *; ins; desf; eauto.
      assert (EQ: ∀ a b,
                    (restr_rel
                       (fun x ⇒ ¬ is_write (lab x))
                       (happens_before sb rf +++ mo +++ reads_before lab rf mo)) a b →
                    happens_before sb rf a b).
        by unfold restr_rel, union, reads_before; ins; desf;
           exfalso; exploit CmoD; eauto; ins; desf.

        repeat split.
          by eapply inclusion_acyclic; eauto;
             eapply trans_irr_acyclic; ins; vauto.
          by unfold union, reads_before; intuition; unfold irreflexive, seq in *;
             ins; desf; eauto.
        ins; eapply clos_refl_trans_mon in S'; eauto.
        unfold union, reads_before in R'; desf;
          try (by exploit CmoD; eauto; ins; desf).
        assert (happens_before sb rf b2 c1).
          by eapply t_rt_trans in S'; eauto using t_step;
             eapply clos_trans_of_clos_trans.
        clear R' S'.
        unfold union, irreflexive, seq, clos_refl in *; desf; eauto 6.
        by eapply ChbI, t_trans; eauto.
        by eapply Cww; repeat eexists; try eapply t_trans; eauto.
  }
Qed.

Theorem ModelSC_bigmo_simplify lab sb (T: transitive sb) rf mo :
  ModelSC_bigmo lab sb rf mo ↔
  ModelSC_bigmo_simpl lab sb rf mo.
Proof.
  unfold ModelSC_bigmo, ModelSC_bigmo_simpl; split; ins; desf; unnw; intuition.
  clear - CwrS.
  by unfold irreflexive, seq, happens_before, union in *; ins; desf;
     eauto 12 using clos_trans.
  by unfold irreflexive, seq, happens_before, union in *; ins; desf;
     eauto 8 using clos_trans.
  unfold irreflexive, seq; ins; desf.
  assert (M: clos_refl sb x x) by vauto.
  revert M H; generalize x at 2 3.
  eapply clos_trans_tn1 in H1; unfold union in ×.
  induction H1;
    ins; desf; unfold clos_refl, irreflexive, seq, union in *; desf; eauto 12;
    try apply clos_tn1_trans in H1;
    try solve [unfold rf_external, reads_before in *; desf; eauto].
  destruct (eqP z0 y) as [|NEQ]; desf; ins; eauto.
  eapply CmoF in NEQ; eauto.
  2: by eapply CmoD in H0; desf; eauto with caccess.
  2: by eapply proj1, CrfD in H; desf; eauto with caccess.
  desf; unfold irreflexive, seq, clos_refl, rf_external in *; desf; eauto.
  eauto 10.
Qed.

Corollary ConsistentSC_total_mo pe :
  Consistent ModelSC_total pe ↔
  Consistent ModelSC_mo pe.
Proof.
  unfold Consistent; split; intros (rf & H); ∃ rf;
  eapply ModelSC_total_mo; eauto.
Qed.

Corollary ConsistentSC_total_bigmo pe :
  Consistent ModelSC_total pe ↔
  Consistent ModelSC_bigmo pe.
Proof.
  unfold Consistent; split; intros (rf & H); ∃ rf;
  eapply ModelSC_total_bigmo; eauto.
Qed.