Require Import List Vbase Varith Vlist extralib.
Require Import Classical ClassicalDescription IndefiniteDescription.
Require Import Permutation.

Set Implicit Arguments.

Definition mydec (P: Prop) :=
  if (excluded_middle_informative P) then true else false.

Definition val := nat.

Inductive assn :=
  | Afalse
  | Aemp
  | Aimplies (P Q: assn)
  | Aforall (PP : val → assn)
  | Apt (E E´ : val)
  | Aptu (E : val)
  | Astar (P Q: assn)
  | Arainit (E : val)
  | Arel (E : val) (Q : val → assn)
  | Aacq (E: val) (Q : val → assn)
  | Armwacq (E: val) (Q : val → assn)
  | Atriangle (P: assn)
  | Anabla (P: assn).

Definition Atrue := Aimplies Afalse Afalse.

Inductive Asim : assn → assn → Prop :=
  | Asim_star_false : Asim (Astar Afalse Afalse) Afalse
  | Asim_star_emp P : Asim (Astar P Aemp) P
  | Asim_starC P Q : Asim (Astar P Q) (Astar Q P)
  | Asim_starA P Q R : Asim (Astar (Astar P Q) R) (Astar P (Astar Q R))
  | Asim_refl P : Asim P P
  | Asim_sym P Q (H: Asim P Q) : Asim Q P
  | Asim_trans P Q (H: Asim P Q) R (H´: Asim Q R) : Asim P R
  | Asim_implies P1 P2 (H1: Asim P1 P2) Q1 Q2 (H2: Asim Q1 Q2) :
      Asim (Aimplies P1 Q1) (Aimplies P2 Q2)
  | Asim_forall Q1 Q2 (H1: ∀ v, Asim (Q1 v) (Q2 v)) :
      Asim (Aforall Q1) (Aforall Q2)
  | Asim_star P1 P2 (H1: Asim P1 P2) Q1 Q2 (H2: Asim Q1 Q2) :
      Asim (Astar P1 Q1) (Astar P2 Q2)
  | Asim_rel E P1 P2 (H1: ∀ v, Asim (P1 v) (P2 v)) :
      Asim (Arel E P1) (Arel E P2)
  | Asim_acq E Q1 Q2 (H1: ∀ v, Asim (Q1 v) (Q2 v)) :
      Asim (Aacq E Q1) (Aacq E Q2)
  | Asim_rmwacq E Q1 Q2 (H1: ∀ v, Asim (Q1 v) (Q2 v)) :
      Asim (Armwacq E Q1) (Armwacq E Q2)
  | Asim_triangle P Q (H: Asim P Q) : Asim (Atriangle P) (Atriangle Q)
  | Asim_nabla P Q (H: Asim P Q) : Asim (Anabla P) (Anabla Q).

Lemma lenT e1 e2: (e1 ≤ e2) = false → e2 ≤ e1.

Lemma lenAS e1 e2 : e1 ≤ e2 → e2 ≤ e1 → e1 = e2.

Lemma assn_eqP : Equality.axiom (fun x y : assn ⇒ mydec (x = y)).

Canonical Structure assn_eqMixin := EqMixin assn_eqP.
Canonical Structure assn_eqType := Eval hnf in EqType _ assn_eqMixin.

Definition leq_fun A (leq : A → A → bool) PP PP´ :=
  mydec (PP = PP´ ∨ ∃ n,
          leq (PP n) (PP´ n) ∧ PP n ≠ PP´ n ∧ ∀ x (LT: x < n), PP x = PP´ x).

Fixpoint assn_leq p q :=
  match p, q with
    | Afalse , _ ⇒ true
    | _ , Afalse ⇒ false
    | Aemp , _ ⇒ true
    | _ , Aemp ⇒ false
    | Aimplies P Q, Aimplies P´ Q´ ⇒ if P == P´ then assn_leq Q Q´ else assn_leq P P´
    | Aimplies _ _, _ ⇒ true
    | _ , Aimplies _ _ ⇒ false
    | Aforall PP , Aforall PP´ ⇒ leq_fun assn_leq PP PP´
    | Aforall _ , _ ⇒ true
    | _ , Aforall _ ⇒ false
    | Apt E1 E2 , Apt E1´ E2´ ⇒ if E1 == E1´ then E2 ≤ E2´ else E1 ≤ E1´
    | Apt _ _ , _ ⇒ true
    | _ , Apt _ _ ⇒ false
    | Aptu E1 , Aptu E1´ ⇒ E1 ≤ E1´
    | Aptu _ , _ ⇒ true
    | _ , Aptu _ ⇒ false
    | Astar P Q , Astar P´ Q´ ⇒ if P == P´ then assn_leq Q Q´ else assn_leq P P´
    | Astar _ _ , _ ⇒ true
    | _ , Astar _ _ ⇒ false
    | Arainit E , Arainit E´ ⇒ E ≤ E´
    | Arainit _ , _ ⇒ true
    | _ , Arainit _ ⇒ false
    | Arel E PP , Arel E´ PP´ ⇒ if E == E´ then leq_fun assn_leq PP PP´ else E ≤ E´
    | Arel _ _ , _ ⇒ true
    | _ , Arel _ _ ⇒ false
    | Aacq E PP , Aacq E´ PP´ ⇒ if E == E´ then leq_fun assn_leq PP PP´ else E ≤ E´
    | Aacq _ _ , _ ⇒ true
    | _ , Aacq _ _ ⇒ false
    | Armwacq E PP, Armwacq E´ PP´ ⇒ if E == E´ then leq_fun assn_leq PP PP´ else E ≤ E´
    | Armwacq _ _ , _ ⇒ true
    | _ , Armwacq _ _ ⇒ false
    | Atriangle P , Atriangle P´ ⇒ assn_leq P P´
    | Atriangle _ , _ ⇒ true
    | _ , Atriangle _ ⇒ false
    | Anabla P , Anabla P´ ⇒ assn_leq P P´
    end.

Lemma leq_funAS A leq (AS: antisymmetric leq) p q :
  leq_fun (A:=A) leq p q → leq_fun leq q p → p = q.

Lemma leq_fun_trans A (leq : A → A → bool) p q r
  (AS: ∀ p q, leq p q → leq q p → p = q)
  (T: ∀ x, leq (p x) (q x) → leq (q x) (r x) → leq (p x) (r x)) :
  leq_fun (A:=A) leq p q → leq_fun leq q r → leq_fun leq p r.

Lemma assn_leqAS :
  ∀ p q, assn_leq p q → assn_leq q p → p = q.

Lemma assn_leq_refl :
  ∀ p, assn_leq p p.

Lemma assn_leq_trans :
  ∀ p q r (H: assn_leq p q) (H´: assn_leq q r), assn_leq p r.

Lemma neq_min_neq A (f g : nat → A) (NEQ: f ≠ g) :
  ∃ m, f m ≠ g m ∧ (∀ x, x < m → f x = g x).

Lemma assn_leqT :
  ∀ p q, assn_leq p q = false → assn_leq q p.

Lemma assn_leq_false_ne :
  ∀ p q, assn_leq p q = false → p ≠ q.

Lemma assn_leqTT :
  ∀ p q, assn_leq p q = false → p ≠ q ∧ assn_leq q p = true.

Lemma assn_leq_AfalseD P : assn_leq P Afalse → P = Afalse.

Opaque assn_leq.

Fixpoint assn_merge_size P :=
  match P with
    | Astar p q ⇒ S (assn_merge_size q)
    | _ ⇒ 0
  end.

Definition assn_merge_fst P :=
  match P with
    | Astar p q ⇒ p
    | _ ⇒ P
  end.

Definition assn_merge_snd P :=
  match P with
    | Astar p q ⇒ Some q
    | _ ⇒ None
  end.

Definition assn_not_star P :=
  match P with
    | Astar _ _ ⇒ false
    | _ ⇒ true
  end.

Fixpoint assn_wf P :=
  match P with
    | Afalse | Aemp | Apt _ _ | Aptu _ | Arainit _ ⇒ True
    | Astar p q ⇒ assn_wf p ∧ assn_wf q
                   ∧ assn_not_star p ∧ p ≠ Aemp ∧ q ≠ Aemp
                   ∧ assn_leq p (assn_merge_fst q)
                   ∧ ¬ (p = Afalse ∧ assn_merge_fst q = Afalse)
    | Aimplies p q ⇒ assn_wf p ∧ assn_wf q
    | Arel _ pp
    | Aacq _ pp
    | Armwacq _ pp
    | Aforall pp ⇒ ∀ x, assn_wf (pp x)
    | Atriangle p ⇒ assn_wf p
    | Anabla p ⇒ assn_wf p
  end.

Fixpoint assn_merge_rec P Q SZ :=
  match SZ with
      0 ⇒ Aemp
    | S sz ⇒
      if assn_leq (assn_merge_fst P) (assn_merge_fst Q) then
        if (assn_merge_fst P == Afalse) && (assn_merge_fst Q == Afalse) then
              (match assn_merge_snd Q with
                 | None ⇒ P
                 | Some Q´ ⇒ @assn_merge_rec P Q´ sz
               end)
        else
        Astar (assn_merge_fst P)
              (match assn_merge_snd P with
                 | None ⇒ Q
                 | Some P´ ⇒ @assn_merge_rec P´ Q sz
               end)
      else
        Astar (assn_merge_fst Q)
              (match assn_merge_snd Q with
                 | None ⇒ P
                 | Some Q´ ⇒ @assn_merge_rec P Q´ sz
               end)
  end.

Definition assn_star_rdf P Q :=
  if (P == Afalse) && (assn_merge_fst Q == Afalse) then Q
  else Astar P Q.

Definition assn_merge P Q :=
  assn_merge_rec P Q (S (assn_merge_size P + assn_merge_size Q)).

Fixpoint assn_norm p := match p with
  | Afalse ⇒ Afalse
  | Aemp ⇒ Aemp
  | Aimplies P Q ⇒ Aimplies (assn_norm P) (assn_norm Q)
  | Aforall PP ⇒ Aforall (fun x ⇒ assn_norm (PP x))
  | Apt E E´ ⇒ Apt E E´
  | Aptu E ⇒ Aptu E
  | Astar P Q ⇒
      let P´ := assn_norm P in
      let Q´ := assn_norm Q in
      if P´ == Aemp then Q´
      else if Q´ == Aemp then P´
      else assn_merge P´ Q´
  | Arainit E ⇒ Arainit E
  | Arel E QQ ⇒ Arel E (fun v ⇒ assn_norm (QQ v))
  | Aacq E QQ ⇒ Aacq E (fun v ⇒ assn_norm (QQ v))
  | Armwacq E QQ ⇒ Armwacq E (fun v ⇒ assn_norm (QQ v))
  | Atriangle P ⇒ Atriangle (assn_norm P)
  | Anabla P ⇒ Anabla (assn_norm P)
  end.

Lemma assn_merge_notemp:
  ∀ SZ p1 p2 (PF: assn_merge_size p1 + assn_merge_size p2 < SZ),
    assn_merge_rec p1 p2 SZ ≠ Aemp.

Lemma assn_merge_fst_merge_rec p1 p2 SZ :
  assn_merge_size p1 + assn_merge_size p2 < SZ →
  assn_merge_fst (assn_merge_rec p1 p2 SZ) =
    if assn_leq (assn_merge_fst p1) (assn_merge_fst p2) then
      assn_merge_fst p1
    else
      assn_merge_fst p2.

Lemma assn_merge_leq:
  ∀ r SZ p (WFp : assn_wf p) (Lp : assn_leq r (assn_merge_fst p))
              q (WFq : assn_wf q) (Lq : assn_leq r (assn_merge_fst q))
         (PF: assn_merge_size p + assn_merge_size q < SZ),
    assn_leq r (assn_merge_fst (assn_merge_rec p q SZ)).

Lemma assn_merge_wf:
  ∀ SZ p1 (WF1: assn_wf p1) (NE1: p1 ≠ Aemp)
            p2 (WF2: assn_wf p2) (NE2: p2 ≠ Aemp)
         (PF: assn_merge_size p1 + assn_merge_size p2 < SZ),
    assn_wf (assn_merge_rec p1 p2 SZ).

Lemma assn_merge_wf2:
  ∀ SZ p1 (WF1: assn_wf p1) (NE1: assn_not_star p1)
            p2 (WF2: assn_wf p2) (NE2: p2 ≠ Aemp)
            (LT: assn_leq p1 (assn_merge_fst p2))
            (NP: ¬ (p1 = Afalse ∧ assn_merge_fst p2 = Afalse))
            (PF: assn_merge_size p1 + assn_merge_size p2 < SZ),
    assn_merge_rec p1 p2 SZ = Astar p1 p2.

Lemma assn_norm_wf p : assn_wf (assn_norm p).

Lemma assn_norm_wf2 p : assn_wf p → assn_norm p = p.

Lemma assn_merge_recC :
  ∀ n p (WFp: assn_wf p) q (WF : assn_wf q)
    (PF : assn_merge_size p + assn_merge_size q < n),
    assn_merge_rec p q n = assn_merge_rec q p n.

Lemma assn_mergeC :
  ∀ p (WFp: assn_wf p) q (WF : assn_wf q),
    assn_merge p q = assn_merge q p.

Lemma assn_merge_size_merge :
  ∀ n p (WFp: assn_wf p) (NEp: p ≠ Aemp)
         q (WFq: assn_wf q) (NEq: q ≠ Aemp)
         (LT : assn_merge_size p + assn_merge_size q < n),
    assn_merge_size (assn_merge_rec p q n) ≤
    S (assn_merge_size p + assn_merge_size q).

Definition assn_rdf P Q :=
  if (P == Afalse) && (Q == Afalse) then Q
  else Astar P Q.

Fixpoint assn_insert p q :=
  match q with
    | Astar p´ q´ ⇒
      if assn_leq p p´ then assn_star_rdf p q
      else Astar p´ (assn_insert p q´)
    | _ ⇒
      if assn_leq p q then assn_star_rdf p q
      else Astar q p
  end.

Lemma assn_merge_fst_not_star p : assn_not_star p → assn_merge_fst p = p.

Ltac assn_merge_clarify :=
  repeat (clarify; match goal with
    | H: assn_merge_snd ?p = Some _ |- _ ⇒
      destruct p; ins; inv H; clear H; try rewrite addnS in *; desf
    | H: assn_merge_snd ?p = None |- _ ⇒
      cut (assn_not_star p); [|by clear -H; destruct p]; clear H; intro H
    | H : assn_leq ?p ?q = true, H´ : assn_leq ?q ?p = true |- _ ⇒
      eapply assn_leqAS in H; eauto; try subst p; try subst q
    | H : assn_leq ?p ?q = true, H´ : assn_leq ?q ?r = true, H´´: assn_leq ?r ?p = true |- _ ⇒
      eapply assn_leqAS in H; eauto using assn_leq_trans; try subst p; try subst q
    | H : assn_leq ?p ?q = false |- _ ⇒
      eapply assn_leqTT in H; desc
    | H : is_true (assn_not_star ?p) |- _ ⇒
      rewrite (@assn_merge_fst_not_star p H) in *; try done
    | H : ¬ (_ ∧ _) |- _ ⇒ destruct H; done
  end); eauto using assn_leqAS.

Lemma assn_merge_ins :
  ∀ n p (WFp: assn_wf p) (NEp: assn_not_star p)
         q (WFq: assn_wf q) (NEq: q ≠ Aemp)
         (LTn : assn_merge_size p + assn_merge_size q < n),
  assn_merge_rec p q n = assn_insert p q.

Lemma assn_insertC_base p q :
  assn_not_star p → assn_not_star q → assn_insert p q = assn_insert q p.

Lemma assn_insertC r p q :
  assn_not_star p → assn_not_star q →
  assn_insert p (assn_insert q r) =
  assn_insert q (assn_insert p r).

Lemma assn_insert_before p q:
  assn_leq p (assn_merge_fst q) →
  assn_insert p q =
    if (p == Afalse) && (assn_merge_fst q == Afalse) then q else Astar p q.

Lemma assn_insert_ff p :
  assn_insert Afalse (assn_insert Afalse p) = assn_insert Afalse p.

Lemma assn_merge_fst_insert p q :
  assn_not_star p →
  assn_merge_fst (assn_insert p q) =
    if assn_leq p (assn_merge_fst q) then p
    else assn_merge_fst q.

Lemma assn_merge_ins2 :
  ∀ n p (WFp: assn_wf p) (NEp: p ≠ Aemp)
         q (WFq: assn_wf q) (NEq: q ≠ Aemp)
         (LTn : assn_merge_size p + assn_merge_size q < n),
  assn_merge_rec p q n =
    match assn_merge_snd p with
    | None ⇒ assn_insert p q
    | Some p´ ⇒ assn_insert (assn_merge_fst p) (assn_merge_rec p´ q (Peano.pred n))
    end.

Lemma assn_merge_star :
  ∀ p (WFp: assn_wf p) (NEp: p ≠ Aemp)
         q (WFq: assn_wf q) (NEq: q ≠ Aemp) (NSq: assn_not_star q)
         r (WFr: assn_wf r) (NEr: r ≠ Aemp) (LT: assn_leq q (assn_merge_fst r))
         (NFF: ¬ (q = Afalse ∧ assn_merge_fst r = Afalse)),
    assn_merge p (Astar q r) = assn_insert q (assn_merge p r).

Lemma assn_merge_not_star :
  ∀ q p (WFp: assn_wf p) (NEp: p ≠ Aemp)
         (WFq: assn_wf q) (NEq: q ≠ Aemp) (NSq: assn_not_star q),
    assn_merge p q = assn_insert q p.

Lemma assn_merge_rdf :
  ∀ p (WFp: assn_wf p) (NEp: p ≠ Aemp)
         q (WFq: assn_wf q) (NEq: q ≠ Aemp) (NSq: assn_not_star q)
         r (WFr: assn_wf r) (NEr: r ≠ Aemp) (LT: assn_leq q (assn_merge_fst r)),
    assn_merge p (assn_star_rdf q r) = assn_insert q (assn_merge p r).

Lemma assn_merge_insert :
  ∀ p (WFp: assn_wf p) (NEp: p ≠ Aemp)
         q (WFq: assn_wf q) (NEq: q ≠ Aemp) (NSq: assn_not_star q)
         r (WFr: assn_wf r) (NEr: r ≠ Aemp),
    assn_merge p (assn_insert q r) = assn_insert q (assn_merge p r).

Lemma assn_mergeA :
  ∀ p (WFp: assn_wf p) (NEp: p ≠ Aemp)
         q (WFq: assn_wf q) (NEq: q ≠ Aemp)
         r (WFr: assn_wf r) (NEr: r ≠ Aemp),
    assn_merge p (assn_merge q r) = assn_merge (assn_merge p q) r.

Lemma Asim_assn_norm p : Asim p (assn_norm p).

Lemma assn_norm_ok : ∀ P Q, Asim P Q ↔ assn_norm P = assn_norm Q.

Lemma assn_norm_idemp P : assn_norm (assn_norm P) = assn_norm P.

Lemma assn_norm_emp : assn_norm Aemp = Aemp.

Lemma assn_norm_star_emp P : assn_norm (Astar Aemp P) = assn_norm P.

Lemma assn_norm_star_emp_r P : assn_norm (Astar P Aemp) = assn_norm P.

Lemma assn_norm_star_eq_emp P Q :
  assn_norm (Astar P Q) = Aemp →
  assn_norm P = Aemp ∧ assn_norm Q = Aemp.

Lemma assn_merge_rec_not_false P Q n :
  assn_wf Q →
  assn_merge_rec P Q n = Afalse → P = Afalse ∧ Q = Afalse.

Lemma assn_norm_star_eq_false P Q :
  assn_norm (Astar P Q) = Afalse →
  assn_norm P = Aemp ∧ assn_norm Q = Afalse
  ∨ assn_norm P = Afalse ∧ assn_norm Q = Aemp
  ∨ assn_norm P = Afalse ∧ assn_norm Q = Afalse.

Lemma Asim_star_emp_l P : Asim P (Astar Aemp P).

Lemma Asim_star_emp_r P : Asim P (Astar P Aemp).

Ltac Asim_simpl_loop :=
 repeat
   first [eapply Asim_trans, Asim_assn_norm|
          eapply Asim_trans, Asim_star_emp_l|
          eapply Asim_trans, Asim_star_emp_r|
          apply Asim_star|
          apply Asim_refl].

Ltac Asim_simpl :=
 do 2 (eapply Asim_trans;[apply Asim_sym|Asim_simpl_loop]);
   try apply Asim_refl; try done.

Ltac Asim_simpl_asm H :=
 do 2 (eapply Asim_trans in H;[apply Asim_sym in H|Asim_simpl_loop]).

Lemma Asim_norm_l P Q: Asim (assn_norm P) Q ↔ Asim P Q.

Lemma Asim_norm_r P Q: Asim P (assn_norm Q) ↔ Asim P Q.

Lemma Asim_starAC P Q R :
  Asim (Astar P (Astar Q R)) (Astar Q (Astar P R)).

Lemma Asim_rem2 Q P P´ R R´:
  Asim (Astar P R) (Astar P´ R´) →
  Asim (Astar (Astar P Q) R)
       (Astar (Astar P´ Q) R´).

Lemma Asim_foldr_simpl l Q :
  Asim (foldr Astar l Q) (Astar (foldr Astar l Aemp) Q).

Lemma Asim_foldr_pull l P Q :
   Asim (foldr Astar l (Astar P Q))
        (Astar P (foldr Astar l Q)).

Lemma Asim_falseD P :
  Asim Afalse P →
  P = Afalse ∨ ∃ P´ Q´, P = Astar P´ Q´ ∧
   (Asim P´ Afalse ∧ Asim Q´ Aemp ∨
    Asim P´ Aemp ∧ Asim Q´ Afalse ∨
    Asim P´ Afalse ∧ Asim Q´ Afalse).

Lemma assn_merge_not_false2 P Q n :
  assn_merge_rec P Q n ≠ Afalse →
  assn_merge_size P + assn_merge_size Q < n →
  assn_wf Q →
  P ≠ Aemp → Q ≠ Aemp →
  ∃ P´ Q´, assn_merge_rec P Q n = Astar P´ Q´.

Lemma Asim_starD P Q R :
  Asim (Astar P Q) R →
  (∃ P´ Q´, R = Astar P´ Q´) ∨
  Asim P Aemp ∧ Asim Q R ∨
  Asim Q Aemp ∧ Asim P R ∨
  Asim P Afalse ∧ Asim Q Afalse ∧ R = Afalse.

Lemma Asim_star_empD P Q :
  Asim (Astar P Q) Aemp ↔ Asim P Aemp ∧ Asim Q Aemp.

Lemma Asim_emp_starD P Q :
  Asim Aemp (Astar P Q) ↔ Asim Aemp P ∧ Asim Aemp Q.

Lemma assn_rdf_size p q :
  ¬ (p = Afalse ∧ assn_merge_fst q = Afalse) →
  assn_merge_size (assn_star_rdf p q) = S (assn_merge_size q).

Lemma assn_insert_size p q :
  ¬ (p = Afalse ∧ assn_merge_fst (assn_norm q) = Afalse) →
  assn_not_star p →
  assn_merge_size (assn_insert p q) =
  S (assn_merge_size q).

Lemma assn_insert_neq p q :
  ¬ (p = Afalse ∧ assn_merge_fst (assn_norm q) = Afalse) →
  assn_not_star p →
  p = assn_insert p q →
  False.

Lemma assn_insert_not_star_eq :
  ∀ p q, assn_not_star q →
    assn_insert p q = if assn_leq p q then assn_star_rdf p q else Astar q p.

Lemma assn_insert_cancel1 :
  ∀ p (NS: assn_not_star p) (NE: p ≠ Aemp) q
         (NS´: assn_not_star q)
    (NF: ¬ (p = Afalse ∧ assn_merge_fst (assn_norm q) = Afalse)) q´
    (NF´: ¬ (p = Afalse ∧ assn_merge_fst (assn_norm q´) = Afalse))
    (EQ: assn_insert p q = assn_insert p q´),
   assn_wf q → assn_wf q´ → q = q´.

Lemma assn_insert_cancel :
  ∀ p (NS: assn_not_star p) (NE: p ≠ Aemp) q
    (NF: ¬ (p = Afalse ∧ assn_merge_fst (assn_norm q) = Afalse)) q´
    (NF´: ¬ (p = Afalse ∧ assn_merge_fst (assn_norm q´) = Afalse))
    (EQ: assn_insert p q = assn_insert p q´)
    (WF: assn_wf q) (WF´: assn_wf q´),
  q = q´.

Lemma assn_merge_cancel :
  ∀ n m q´ q p
    (LT: assn_merge_size p + assn_merge_size q < n)
    (LT´: assn_merge_size p + assn_merge_size q´ < m)
    (NF: ¬ (assn_merge_fst (assn_norm p) = Afalse ∧
            assn_merge_fst (assn_norm q) = Afalse))
    (NF´: ¬ (assn_merge_fst (assn_norm p) = Afalse ∧
            assn_merge_fst (assn_norm q´) = Afalse))
    (EQ: assn_merge_rec p q n = assn_merge_rec p q´ m),
    p ≠ Aemp → q ≠ Aemp → q´ ≠ Aemp →
    assn_wf p → assn_wf q → assn_wf q´ → q = q´.

Lemma assn_merge_size_merge2 :
  ∀ n p (WFp: assn_wf p) (NEp: p ≠ Aemp) (NFp: assn_merge_fst p ≠ Afalse)
         q (WFq: assn_wf q) (NEq: q ≠ Aemp)
         (LT : assn_merge_size p + assn_merge_size q < n),
    assn_merge_size (assn_merge_rec p q n) =
    S (assn_merge_size p + assn_merge_size q).

Lemma Asim1 P Q :
  Asim P (Astar P Q) →
  Asim Q Aemp ∨ Asim Q Afalse ∧ ∃ P´, Asim P (Astar Afalse P´).

Lemma Asim_star_cancel P Q Q´ :
  Asim (Astar P Q) (Astar P Q´) →
  Asim Q Q´
  ∨ (∃ P´, Asim Q (Astar Afalse P´))
  ∨ (∃ P´, Asim Q´ (Astar Afalse P´)).

Lemma assn_norm_star_false :
  assn_norm (Astar Afalse Afalse) = Afalse.

Global Opaque assn_norm.

Definition assn_mod := { P : assn | assn_norm P = P }.

Inductive HeapLabel :=
  | HLnormal
  | HLtriangle
  | HLnabla.

Inductive HeapLabelCombination :=
  | HLCnormal
  | HLCtriangle
  | HLCnabla
  | HLCdiamond
  | HLCtriangledot
  | HLCnabladot
  | HLCdiamonddot.

Coercion label_to_combination (lbl: HeapLabel) :=
  match lbl with
    | HLnormal ⇒ HLCnormal
    | HLtriangle ⇒ HLCtriangle
    | HLnabla ⇒ HLCnabla
  end.

Coercion label_to_combination_option (lbl: HeapLabel) := Some (label_to_combination lbl).

Definition is_basic lbl := lbl = HLCnormal ∨ lbl = HLCtriangle ∨ lbl = HLCnabla.

Definition is_normal lbl := lbl = HLCnormal ∨ lbl = HLCtriangledot ∨ lbl = HLCnabladot ∨ lbl = HLCdiamonddot.

Definition is_triangle lbl := lbl = HLCtriangle ∨ lbl = HLCtriangledot ∨ lbl = HLCdiamond ∨ lbl = HLCdiamonddot.

Definition is_nabla lbl := lbl = HLCnabla ∨ lbl = HLCnabladot ∨ lbl = HLCdiamond ∨ lbl = HLCdiamonddot.

Definition is_normalO olbl :=
  match olbl with
    | Some lbl ⇒ is_normal lbl
    | None ⇒ False
  end.

Definition HLleq lbl1 lbl2 :=
  match lbl1, lbl2 with
    | HLCnormal , _ ⇒ is_normal lbl2
    | HLCtriangle , _ ⇒ is_triangle lbl2
    | HLCnabla , _ ⇒ is_nabla lbl2
    | HLCdiamond , _ ⇒ lbl2 = HLCdiamond ∨ lbl2 = HLCdiamonddot
    | HLCtriangledot, _ ⇒ lbl2 = HLCtriangledot ∨ lbl2 = HLCdiamonddot
    | HLCnabladot , _ ⇒ lbl2 = HLCnabladot ∨ lbl2 = HLCdiamonddot
    | HLCdiamonddot , _ ⇒ lbl2 = HLCdiamonddot
  end.

Definition oHLleq (olbl1 olbl2: option HeapLabelCombination) :=
  match olbl1, olbl2 with
    | None, _ ⇒ True
    | Some lbl1, Some lbl2 ⇒ HLleq lbl1 lbl2
    | _, _ ⇒ False
  end.

Inductive HeapVal :=
  | HVnone
  | HVuval (lbl: HeapLabel)
  | HVval (v: val) (lbl: HeapLabel)
  | HVra (RR QQ: val → assn_mod) (isrmwflag: bool) (perm: option HeapLabelCombination)
          (init: option HeapLabelCombination).

Inductive heap :=
  | Hundef
  | Hdef (hf: val → HeapVal).

Definition HVlabeled hv (lbl: HeapLabel) :=
  match hv with
    | HVnone ⇒ True
    | HVuval lbl´ ⇒ lbl = lbl´
    | HVval _ lbl´ ⇒ lbl = lbl´
    | HVra _ _ _ None None ⇒ False
    | HVra _ _ _ (Some permlbl) None ⇒ HLleq lbl permlbl
    | HVra _ _ _ None (Some initlbl) ⇒ HLleq lbl initlbl
    | HVra _ _ _ (Some permlbl) (Some initlbl) ⇒ HLleq lbl permlbl ∨ HLleq lbl initlbl
  end.

Definition HFlabeled hf lbl := ∀ (l: val) , HVlabeled (hf l) lbl.

Definition Hlabeled h lbl := ∃ hf, h = Hdef hf ∧ HFlabeled hf lbl.

Definition HVlabeledExact hv (lbl: HeapLabel) :=
  match hv with
    | HVnone ⇒ True
    | HVuval lbl´ ⇒ lbl´ = lbl
    | HVval _ lbl´ ⇒ lbl´ = lbl
    | HVra _ _ _ None None ⇒ True
    | HVra _ _ _ (Some permlbl) None ⇒ permlbl = lbl
    | HVra _ _ _ None (Some initlbl) ⇒ initlbl = lbl
    | HVra _ _ _ (Some permlbl) (Some initlbl) ⇒ permlbl = lbl ∧ initlbl = lbl
  end.

Definition HFlabeledExact hf lbl := ∀ (l: val), HVlabeledExact (hf l) lbl.

Definition HlabeledExact h lbl := ∃ hf, h = Hdef hf ∧ HFlabeledExact hf lbl.

Definition HVlabeledW hv (lbl: HeapLabel) :=
  match hv with
    | HVnone ⇒ False
    | HVuval lbl´ ⇒ lbl = lbl´
    | HVval _ lbl´ ⇒ lbl = lbl´
    | HVra _ _ _ (Some permlbl) _ ⇒ HLleq lbl permlbl
    | _ ⇒ False
  end.

Definition HVlabeledR hv (lbl: HeapLabel) :=
  match hv with
    | HVnone ⇒ False
    | HVuval lbl´ ⇒ False
    | HVval _ lbl´ ⇒ lbl = lbl´
    | HVra _ _ _ _ (Some initlbl) ⇒ HLleq lbl initlbl
    | _ ⇒ False
  end.

Definition HLCsim (lbl1 lbl2: option HeapLabelCombination) :=
  match lbl1, lbl2 with
    | None, None ⇒ True
    | (Some _), (Some _) ⇒ True
    | _, _ ⇒ False
  end.

Definition HVsim hv hv´ :=
  match hv, hv´ with
    | HVnone, HVnone ⇒ True
    | HVuval _, HVuval _ ⇒ True
    | HVval v _, HVval v´ _ ⇒ v = v´
    | HVra RR QQ isrmwflag perm init, HVra RR´ QQ´ isrmwflag´ perm´ init´
                 ⇒ RR = RR´ ∧ QQ = QQ´ ∧ isrmwflag = isrmwflag´ ∧ HLCsim perm perm´ ∧ HLCsim init init´
    | _, _ ⇒ False
  end.

Definition HFsim hf hf´ := ∀ (l: nat), HVsim (hf l) (hf´ l).

Definition Hsim h h´ := ∃ hf hf´, h = Hdef hf ∧ h´ = Hdef hf´ ∧ HFsim hf hf´.

Definition lupd h lbl :=
  match h with
    | Hundef ⇒ Hundef
    | Hdef hf ⇒ Hdef (fun l ⇒ match hf l with
                                  | HVnone ⇒ HVnone
                                  | HVuval _ ⇒ HVuval lbl
                                  | HVval v _ ⇒ HVval v lbl
                                  | HVra PP QQ isrmw None None ⇒ HVra PP QQ isrmw None None
                                  | HVra PP QQ isrmw (Some _) None ⇒ HVra PP QQ isrmw lbl None
                                  | HVra PP QQ isrmw None (Some _) ⇒ HVra PP QQ isrmw None lbl
                                  | HVra PP QQ isrmw (Some _) (Some _) ⇒ HVra PP QQ isrmw lbl lbl
                                 end)
    end.

Definition is_val v :=
  match v with
      HVval _ HLnormal | HVuval HLnormal ⇒ true
    | HVnone | HVra _ _ _ _ _ | _ ⇒ false
  end.

Definition has_value hv v :=
  match hv with
    | HVval v´ _ ⇒ v´ = v
    | _ ⇒ False
  end.

Definition is_nonatomic hv :=
  match hv with
    | HVval _ _ ⇒ true
    | HVuval _ ⇒ true
    | _ ⇒ false
  end.

Definition is_atomic hv :=
  match hv with
    | HVra _ _ _ _ _ ⇒ true
    | _ ⇒ false
  end.

Definition mk_assn_mod (P: assn) : assn_mod := exist _ _ (assn_norm_idemp P).

Definition hemp : heap := Hdef (fun v ⇒ HVnone).

Definition Acombinable (P Q : assn) :=
  P = Afalse ∨ Q = Afalse ∨ P = Q.

Definition hv_rval isrmw P :=
  match isrmw with
    | true ⇒ P
    | false ⇒ Aemp
  end.

Definition hv_acq_def isrmw1 Q1 isrmw2 Q2 :=
  hv_rval isrmw2 Q1 = hv_rval isrmw1 Q2
  ∨ Q1 = Afalse ∧ Q2 = Afalse.

Definition hvplusDEF (hv hv´ : HeapVal) : Prop :=
  match hv, hv´ with
    | HVnone, _ ⇒ True
    | _, HVnone ⇒ True
    | HVra RR1 QQ1 isrmw1 perm1 init1, HVra RR2 QQ2 isrmw2 perm2 init2 ⇒
        (∀ v, hv_acq_def isrmw1 (sval (QQ1 v)) isrmw2 (sval (QQ2 v))) ∧
        (∀ v, Acombinable (sval (RR1 v)) (sval (RR2 v)))
    | _, _ ⇒ False
  end.

Definition hlplus lbl1 lbl2 :=
  match lbl1, lbl2 with
    | HLCdiamonddot , _ ⇒ HLCdiamonddot
    | _ , HLCdiamonddot ⇒ HLCdiamonddot
    | HLCnabladot , HLCtriangledot ⇒ HLCdiamonddot
    | HLCnabladot , HLCdiamond ⇒ HLCdiamonddot
    | HLCnabladot , HLCtriangle ⇒ HLCdiamonddot
    | HLCnabladot , _ ⇒ HLCnabladot
    | HLCtriangledot , HLCnabladot ⇒ HLCdiamonddot
    | HLCtriangledot , HLCdiamond ⇒ HLCdiamonddot
    | HLCtriangledot , HLCnabla ⇒ HLCdiamonddot
    | HLCtriangledot , _ ⇒ HLCtriangledot
    | HLCdiamond , HLCnabladot ⇒ HLCdiamonddot
    | HLCdiamond , HLCtriangledot ⇒ HLCdiamonddot
    | HLCdiamond , HLCnormal ⇒ HLCdiamonddot
    | HLCdiamond , _ ⇒ HLCdiamond
    | HLCnabla , HLCnabladot ⇒ HLCnabladot
    | HLCnabla , HLCtriangledot ⇒ HLCdiamonddot
    | HLCnabla , HLCdiamond ⇒ HLCdiamond
    | HLCnabla , HLCnabla ⇒ HLCnabla
    | HLCnabla , HLCtriangle ⇒ HLCdiamond
    | HLCnabla , HLCnormal ⇒ HLCnabladot
    | HLCtriangle , HLCnabladot ⇒ HLCdiamonddot
    | HLCtriangle , HLCtriangledot ⇒ HLCtriangledot
    | HLCtriangle , HLCdiamond ⇒ HLCdiamond
    | HLCtriangle , HLCnabla ⇒ HLCdiamond
    | HLCtriangle , HLCtriangle ⇒ HLCtriangle
    | HLCtriangle , HLCnormal ⇒ HLCtriangledot
    | HLCnormal , HLCnabladot ⇒ HLCnabladot
    | HLCnormal , HLCtriangledot ⇒ HLCtriangledot
    | HLCnormal , HLCdiamond ⇒ HLCdiamonddot
    | HLCnormal , HLCnabla ⇒ HLCnabladot
    | HLCnormal , HLCtriangle ⇒ HLCtriangledot
    | HLCnormal , HLCnormal ⇒ HLCnormal
  end.

Definition ohlplus lbl1 lbl2 :=
  match lbl1, lbl2 with
    | None, lbl ⇒ lbl
    | lbl, None ⇒ lbl
    | (Some lbl1´), (Some lbl2´) ⇒ Some (hlplus lbl1´ lbl2´)
  end.

Definition hvplus (hv hv´ : HeapVal) : HeapVal :=
  match hv, hv´ with
    | HVnone, _ ⇒ hv´
    | _, HVnone ⇒ hv
    | HVra RR1 QQ1 isrmw1 perm1 init1, HVra RR2 QQ2 isrmw2 perm2 init2 ⇒
        HVra (fun v ⇒ if excluded_middle_informative (sval (RR1 v) = Afalse) then RR2 v else RR1 v)
              (if isrmw1 then QQ1
                else if isrmw2 then QQ2
                else fun v ⇒ mk_assn_mod (Astar (sval (QQ1 v)) (sval (QQ2 v))))
              (isrmw1 || isrmw2)
              (ohlplus perm1 perm2)
              (ohlplus init1 init2)
    | _, _ ⇒ hv
  end.

Definition hplus (h1 h2: heap) : heap :=
  match h1, h2 with
    | Hundef, _ ⇒ Hundef
    | _, Hundef ⇒ Hundef
    | Hdef hf1, Hdef hf2 ⇒
      if excluded_middle_informative (∀ v, hvplusDEF (hf1 v) (hf2 v)) then
        Hdef (fun v ⇒ hvplus (hf1 v) (hf2 v))
      else Hundef
  end.

Definition hsum (l: list heap) := foldr hplus l hemp.

Definition hupd B (h : nat → B) y z := fun x ⇒ if x == y then z else h x.

Notation hsingl l v := (Hdef (hupd (fun _ ⇒ HVnone) l v)).

Definition initialize h l :=
  hupd h l (match h l with
              | HVra PP QQ perm isrmw init ⇒ HVra PP QQ perm isrmw (ohlplus init (Some HLCnormal))
              | _ ⇒ h l end).

Global Opaque hplus.

Definition Wemp : val → assn_mod := fun _ ⇒ mk_assn_mod Afalse.
Definition Remp : val → assn_mod := fun _ ⇒ mk_assn_mod Aemp.

Fixpoint assn_sem (P : assn) (h : heap) :=
  match P with
    | Afalse ⇒ False
    | Aemp ⇒ h = hemp
    | Aimplies P Q ⇒ h ≠ Hundef ∧ (assn_sem P h → assn_sem Q h)
    | Aforall PP ⇒ ∀ x, assn_sem (PP x) h
    | Apt E E´ ⇒ h = hsingl E (HVval E´ HLnormal)
    | Aptu E ⇒ h = hsingl E (HVuval HLnormal)
    | Astar P Q ⇒
        ∃ h1 h2, h ≠ Hundef ∧ hplus h1 h2 = h ∧ assn_sem P h1 ∧ assn_sem Q h2
    | Arainit E ⇒ h = Hdef (hupd (fun _ ⇒ HVnone) E (HVra Wemp Remp false None (Some HLCnormal)))
    | Arel E P ⇒ h = hsingl E (HVra (fun x ⇒ mk_assn_mod (P x)) Remp false (Some HLCnormal) None)
    | Aacq E Q ⇒ h = hsingl E (HVra Wemp (fun x ⇒ mk_assn_mod (Q x)) false None None)
    | Armwacq E Q ⇒ h = hsingl E (HVra Wemp (fun x ⇒ mk_assn_mod (Q x)) true (Some HLCnormal) None)
    | Atriangle Q ⇒ HlabeledExact h HLtriangle ∧
                     ∃ h´, assn_sem Q h´ ∧ Hsim h h´ ∧ HlabeledExact h´ HLnormal
    | Anabla Q ⇒ HlabeledExact h HLnabla ∧
                     ∃ h´, assn_sem Q h´ ∧ Hsim h h´ ∧ HlabeledExact h´ HLnormal
  end.

Definition assn_sem_sim P h := ∃ h´, assn_sem P h´ ∧ Hsim h h´.

Definition implies P Q := ∀ h, assn_sem P h → assn_sem Q h.

Definition precise P :=
  ∀ hP (SEM: assn_sem P hP) hP´ (SEM´: assn_sem P hP´)
         hF (DEF: hplus hP hF ≠ Hundef) hF´ (EQ: hplus hP hF = hplus hP´ hF´),
  hP = hP´ ∧ hF = hF´.

Definition normalizable P :=
  ∀ h, assn_sem P h → ∃ hN h´, assn_sem P hN ∧ HlabeledExact hN HLnormal ∧ h = hplus hN h´.

Definition Anot P := Aimplies P Afalse.
Definition Adisj P Q := Aimplies (Anot P) Q.
Definition Aexists PP := Anot (Aforall (fun x ⇒ Anot (PP x))).