Require Import Vbase Classical extralib.
Require Import fslassn fslassnsem fslassnlemmas fslmodel.
Require Import permission GpsSepAlg.
Require Import Setoid Program.
Open Scope string_scope.

Set Implicit Arguments.

Opaque Aexists.

Lemma exact_label_emp PS PSg: ∀ lbl, HlabeledExact (@hemp PS PSg) lbl.

Lemma assn_sem_star PS PSg (P Q: assn PS PSg) h:
  assn_sem (P &*& Q) h ↔ h ≠ Hundef ∧ ∃ hp hq, h = hp +!+ hq ∧ assn_sem P hp ∧ assn_sem Q hq.

Lemma implies_refl PS PSg (P: assn PS PSg) : implies P P.

Lemma implies_star_l PS PSg (P Q R: assn PS PSg) : implies P Q → implies (Astar P R) (Astar Q R).

Lemma implies_star_r PS PSg (P Q R: assn PS PSg) : implies P Q → implies (Astar R P) (Astar R Q).

Lemma implies_star PS PSg (P Q P' Q': assn PS PSg):
  implies P P' → implies Q Q' → implies (P &*& Q) (P' &*& Q').

Lemma implies_trans2 PS PSg: ∀ x y z : assn PS PSg, implies x y → implies y z → implies x z.




Ltac fold_implies :=
  match goal with |- ∀ _ : heap ?PS ?PSg, assn_sem ?P _ → assn_sem ?Q _ ⇒ fold (@implies PS PSg P Q) end.

Ltac refl_implies :=
  match goal with |- implies ?A ?B ⇒ let X := fresh in cut (A = B); [by intro X; rewrite X | ] end.

Definition equivalent PS PSg (P Q: assn PS PSg) := implies P Q ∧ implies Q P.

Lemma equivalent_refl PS PSg (P: assn PS PSg): equivalent P P.

Lemma equivalent_trans PS PSg: ∀ x y z : assn PS PSg, equivalent x y → equivalent y z → equivalent x z.

Lemma equivalent_sym PS PSg (P Q: assn PS PSg): equivalent P Q → equivalent Q P.

Lemma false_implies PS PSg (P: assn PS PSg): implies Afalse P.

Lemma implies_true PS PSg (P: assn PS PSg): implies P Atrue.

Lemma implies_sim PS PSg (P Q: assn PS PSg) : Asim P Q → implies P Q.

Lemma Arel_split1 PS PSg x v PP :
  @implies PS PSg (Arel x PP)
                  (Astar (Arel x PP) (Arel x (mupd (fun _ ⇒ Afalse) v (PP v)))).

Lemma Arainit_split1 PS PSg x :
  @implies PS PSg (Arainit x)
                  (Astar (Arainit x) (Arainit x)).

Lemma Arainit_split2 PS PSg x :
  @implies PS PSg (Astar (Arainit x) (Arainit x)) (Arainit x).

Lemma Arel_split11 PS PSg x PP :
  implies (Arel x PP)
          (@Astar PS PSg (Arel x PP) (Arel x PP)).

Lemma Armw_acq_split1 PS PSg x PP QQ :
  (∀ v, QQ v = Aemp ∨ PP v = Afalse ∧ QQ v = Afalse) →
  @implies PS PSg (Armwacq x PP) (Astar (Armwacq x PP) (Aacq x QQ)).

Lemma Armw_acq_split2 PS PSg x PP QQ :
  (∀ v, QQ v = Aemp ∨ PP v = Afalse ∧ QQ v = Afalse) →
  @implies PS PSg (Astar (Armwacq x PP) (Aacq x QQ)) (Armwacq x PP).

Lemma star_false PS PSg (P: assn PS PSg): equivalent (P &*& Afalse) Afalse.

Lemma false_star PS PSg (P: assn PS PSg): equivalent (Afalse &*& P) Afalse.

Lemma equivalent_sim PS PSg (P Q: assn PS PSg) : Asim P Q → equivalent P Q.

Lemma equivalent_starC PS PSg (A B: assn PS PSg): equivalent (A &*& B) (B &*& A).

Lemma equivalent_starA PS PSg (A B C: assn PS PSg): equivalent ((A &*& B) &*& C) (A &*& B &*& C).

Lemma equivalent_starAC PS PSg (B A C: assn PS PSg): equivalent (A &*& B &*& C) (B &*& A &*& C).

Lemma equivalent_star_l PS PSg (P Q R: assn PS PSg) : equivalent P Q → equivalent (Astar P R) (Astar Q R).

Lemma equivalent_star_r PS PSg (P Q R: assn PS PSg) : equivalent P Q → equivalent (Astar R P) (Astar R Q).

Lemma equivalent_star PS PSg (P Q P' Q': assn PS PSg):
  equivalent P P' → equivalent Q Q' → equivalent (P &*& Q) (P' &*& Q').

Lemma star_emp_l PS PSg (P: assn PS PSg): equivalent P (Aemp &*& P).

Lemma star_emp_r PS PSg (P: assn PS PSg): equivalent P (P &*& Aemp).

Lemma star_exists PS PSg (P: assn PS PSg) Q:
  equivalent (P &*& Aexists Q) (Aexists (fun x ⇒ P &*& Q x)).

Lemma star_exists2 PS PSg P (Q : assn PS PSg):
equivalent (Aexists P &*& Q) (Aexists (fun x ⇒ P x &*& Q)).

Lemma Arel_split PS PSg x v PP :
  @equivalent PS PSg (Arel x PP)
                     (Astar (Arel x PP) (Arel x (mupd (fun _ ⇒ Afalse) v (PP v)))).

Lemma Arainit_split PS PSg x :
  @equivalent PS PSg (Arainit x)
                     (Astar (Arainit x) (Arainit x)).

Lemma Arel_duplicate PS PSg x PP :
  equivalent (Arel x PP)
             (@Astar PS PSg (Arel x PP) (Arel x PP)).

Lemma Armw_acq_split PS PSg x PP QQ :
  (∀ v, QQ v = Aemp ∨ PP v = Afalse ∧ QQ v = Afalse) →
  @equivalent PS PSg (Armwacq x PP) (Astar (Armwacq x PP) (Aacq x QQ)).

Lemma Armw_duplicate PS PSg x PP :
  @equivalent PS PSg (Armwacq x PP) (Armwacq x PP &*& Armwacq x PP).

Lemma Aacq_split PS PSg x PP QQ :
  @equivalent PS PSg (Aacq x (fun x ⇒ PP x &*& QQ x)) (Aacq x PP &*& Aacq x QQ).

Lemma nabla_emp PS PSg: equivalent (Anabla (@Aemp PS PSg)) Aemp.

Lemma triangle_emp PS PSg: equivalent (Atriangle (@Aemp PS PSg)) Aemp.

Lemma triangle_exists PS PSg (P: val → assn PS PSg):
  equivalent (Atriangle (Aexists P)) (Aexists (fun x ⇒ Atriangle (P x))).

Lemma triangle_star_dist PS PSg (P Q: assn PS PSg):
  equivalent (Atriangle (Astar P Q)) (Astar (Atriangle P) (Atriangle Q)).

Definition RMW PS PSg l QQ := @Arel PS PSg l QQ &*& @Armwacq PS PSg l QQ &*& Arainit l.

Lemma RMW_split PS PSg x (QQ: val → assn PS PSg):
  equivalent (RMW x QQ) (RMW x QQ &*& RMW x QQ).

Lemma RMW_rel_split PS PSg v l (QQ: val → assn PS PSg):
  equivalent (RMW l QQ) (Arel l (mupd (fun _ ⇒ Afalse) v (QQ v)) &*& (RMW l QQ)).

Lemma RMW_acq_split PS PSg x (QQ: val → assn PS PSg):
  equivalent (RMW x QQ) ((Aacq x (fun _ ⇒ Aemp) &*& Arainit x) &*& RMW x QQ).

Lemma assn_sem_not PS PSg (P: assn PS PSg) h:
  assn_sem (Anot P) h ↔ (h ≠ Hundef ∧ ¬ assn_sem P h).

Lemma assn_sem_conj PS PSg (P Q: assn PS PSg) h:
  assn_sem (Aconj P Q) h ↔ assn_sem P h ∧ assn_sem Q h.