Require Import List Vbase Varith Vlist extralib.
Require Import Classical ClassicalDescription IndefiniteDescription.
Require Import ProofIrrelevance.
Require Import Permutation.
Require Import permission.
Require Import Omega.
Require Import GpsSepAlg.

Set Implicit Arguments.

Section Assertions.

Variable PS : list Permission.
Variable PSg: list salg_mod.
Definition val := nat.

Inductive assn :=
  | Afalse
  | Aemp
  | Aimplies (P Q: assn)
  | Aforall (PP : val → assn)
  | Apt (Perm: Permission) (psIN: In Perm PS)
        (p: Perm) (SANE: p ≠ Pundef Perm ∧ p ≠ Pzero Perm) (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)
  | Aghost (PCM : salg_mod) (pcmIN: In PCM PSg) (E: val) (g: PCM).

Definition Atrue := Aimplies Afalse Afalse.

Global Arguments Apt : clear implicits.
Global Arguments Aptu : clear implicits.
Global Arguments Aghost : clear implicits.

Lemma Apt_equal Perm psIn p SANE x v Perm' psIn' p' SANE' x' v' (EQ: Perm = Perm'):
   (@eq_rect Permission Perm (fun x ⇒ x) p Perm' EQ) = p' → x = x' → v = v'
  → Apt Perm psIn p SANE x v = Apt Perm' psIn' p' SANE' x' v'.
Proof.
  ins; subst; f_equal; apply proof_irrelevance.
Qed.

Lemma Aghost_equal PCM pcmIN E g PCM' pcmIN' E' g' (EQ: PCM = PCM'):
  (@eq_rect salg_mod PCM (fun x ⇒ x) g PCM' EQ) = g' → E = E'
  → Aghost PCM pcmIN E g = Aghost PCM' pcmIN' E' g'.
Proof.
  ins; subst; f_equal; apply proof_irrelevance.
Qed.

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.
Proof. by case cmpP. Qed.

Lemma lenAS e1 e2 : e1 ≤ e2 → e2 ≤ e1 → e1 = e2.
Proof. by case cmpP. Qed.

Lemma assn_eqP : Equality.axiom (fun x y : assn ⇒ mydec (x = y)).
Proof. unfold Equality.axiom, mydec; ins; desf; vauto. Qed.

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


Definition Perm_leq_helper (Perm Perm': Permission) (p : Perm) (p' : Perm') :=
  match excluded_middle_informative (Perm = Perm') with
    | right _ ⇒ index_of Perm PS ≤ index_of Perm' PS
    | left EQ ⇒ (eq_rect Perm (fun x ⇒ x) p Perm' EQ) <# p'
  end.

Definition PCM_leq_helper (PCM PCM': salg_mod) (g : PCM) (g' : PCM') :=
  match excluded_middle_informative (PCM = PCM') with
    | right _ ⇒ index_of PCM PSg ≤ index_of PCM' PSg
    | left EQ ⇒ salg_leq PCM' (eq_rect PCM (fun x ⇒ x) g PCM' EQ) g'
  end.

Lemma Perm_leq_helperAS Perm Perm' p p':
  In Perm PS → In Perm' PS → Perm_leq_helper Perm Perm' p p' → Perm_leq_helper Perm' Perm p' p
  → Perm = Perm' ∧ ∃ EQ, (eq_rect Perm (fun x ⇒ x) p Perm' EQ) = p'.
Proof.
  unfold Perm_leq_helper; ins; desf.
    by split; [done | ∃ e]; rewrite <- eq_rect_eq in *; eauto using (permission_leq_as Perm).
  destruct n0.
  eapply equal_index_of; try edone.
  by apply lenAS.
Qed.

Lemma PCM_leq_helperAS PCM PCM' g g':
  In PCM PSg → In PCM' PSg → PCM_leq_helper PCM PCM' g g' → PCM_leq_helper PCM' PCM g' g
  → PCM = PCM' ∧ ∃ EQ, (eq_rect PCM (fun x ⇒ x) g PCM' EQ) = g'.
Proof.
  unfold PCM_leq_helper; ins; desf.
    by split; [done | ∃ e]; rewrite <- eq_rect_eq in *; eauto using (salg_leq_as PCM).
  destruct n0.
  eapply equal_index_of; try edone.
  by apply lenAS.
Qed.

Definition leq_fun A (leq : rel A) 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 Perm _ p _ E1 E2 , Apt Perm' _ p' _ E1' E2' ⇒ if E1 == E1' then
                                                            if E2 == E2'
                                                            then Perm_leq_helper Perm Perm' p p'
                                                            else 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'
    | Anabla _ , _ ⇒ true
    | _ , Anabla _ ⇒ false
    | Aghost PCM _ E g , Aghost PCM' _ E' g' ⇒ if E == E'
                                                     then PCM_leq_helper PCM PCM' g g'
                                                     else E ≤ E'
    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.
Proof.
  unfold leq_fun, mydec; ins; desf; des; eauto; exten; intro m.
  exfalso; case (cmpP n n0); ins; subst; eauto 6 using eq_sym.
Qed.

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.
Proof.
  unfold leq_fun, mydec in *; desf; desf; exfalso; eauto 6; eauto using eq_trans.
  destruct n; eauto; right.
  case (cmpP n0 n1); ins; eauto.
  1: by eexists n0; repeat split; ins; rewrite o4; eauto using ltn_trans.
  2: by eexists n1; repeat split; ins; rewrite <- o2; eauto using ltn_trans.
  subst; ∃ n1; repeat split; ins; eauto using eq_trans.
  intros X; rewrite X in *; eauto.
Qed.

Lemma assn_leqAS :
  ∀ p q, assn_leq p q → assn_leq q p → p = q.
Proof.
  induction p; destruct q; ins; try rewrite beq_sym in H0; try rewrite (beq_sym _ E') in H0;
    desf; ins; f_equal; try destruct Heq; try destruct Heq0; eauto using lenAS ;

  try (by unfold leq_fun, mydec in *; desf; des; eauto; exten; intro m;
      exfalso; case (cmpP n n0); ins; subst; eauto 6 using eq_sym).

  by exploit (Perm_leq_helperAS Perm Perm0); try edone; ins; desf; eapply Apt_equal.

  by exploit (PCM_leq_helperAS PCM PCM0); try edone; ins; desf; eapply Aghost_equal.
Qed.

Lemma assn_leq_refl :
  ∀ p, assn_leq p p.
Proof.
  induction p; ins; desf; unfold leq_fun, mydec; desf; try solve[exfalso; eauto].
  by unfold Perm_leq_helper; desf; rewrite <- eq_rect_eq; apply permission_leq_refl.
  by unfold PCM_leq_helper; desf; rewrite <- eq_rect_eq; apply salg_leq_refl.
Qed.

Lemma assn_leq_trans :
  ∀ p q r (H: assn_leq p q) (H': assn_leq q r), assn_leq p r.
Proof.
  induction p; ins; destruct q, r; ins; desf; subst;
    eauto using len_trans, leq_fun_trans, assn_leqAS;
    try solve [congruence|exfalso; eauto using assn_leqAS, lenAS].
  × unfold Perm_leq_helper in *; desf.
    eby rewrite <- eq_rect_eq in *; eapply permission_leq_trans.
    by destruct n; eapply equal_index_of; try edone; apply lenAS.
    eby eapply len_trans.
  × unfold PCM_leq_helper in *; desf.
    eby rewrite <- eq_rect_eq in *; eapply salg_leq_trans.
    by destruct n; eapply equal_index_of; try edone; apply lenAS.
    eby eapply len_trans.
Qed.

Lemma neq_min_neq A (f g : nat → A) (NEQ: f ≠ g) :
  ∃ m, f m ≠ g m ∧ (∀ x, x < m → f x = g x).
Proof.
  assert (H: ∃ n, f n ≠ g n); desf.
   by apply NNPP; intro H; destruct NEQ; exten; eapply not_ex_not_all.
  induction n using (well_founded_ind (Wf_nat.lt_wf)).
  destruct (classic (∃ m, m < n ∧ f m ≠ g m)).
    by des; apply (H0 m); eauto using ltn_complete.
  eapply NNPP; intro X.
  destruct (not_ex_all_not _ _ X n); split; ins.
  apply NNPP; eauto.
Qed.

Lemma assn_leqT :
  ∀ p q, assn_leq p q = false → assn_leq q p.
Proof.
  induction p; destruct q; ins; f_equal; desf; ins; auto using lenT; try congruence.

  × unfold leq_fun, mydec in *; desf. exfalso; apply not_or_and in n0; apply not_or_and in n; desf.
    destruct (neq_min_neq n0) as (m &?&?); case_eq (assn_leq (PP m) (PP0 m));
      ins; eauto 8 using eq_sym.

  × unfold Perm_leq_helper in *; desf; try subst Perm0.
    by rewrite <- eq_rect_eq in *; specialize (permission_leq_total Perm p p0); ins; desf.
    by apply lenT.

  × unfold leq_fun, mydec in *; desf.
    exfalso; apply not_or_and in n0; apply not_or_and in n; desf.
    destruct (neq_min_neq n0) as (m &?&?); case_eq (assn_leq (Q m) (Q0 m));
    ins; eauto 8 using eq_sym.

  × unfold leq_fun, mydec in *; desf.
    exfalso; apply not_or_and in n0; apply not_or_and in n; desf.
    destruct (neq_min_neq n0) as (m &?&?); case_eq (assn_leq (Q m) (Q0 m));
    ins; eauto 8 using eq_sym.

  × unfold leq_fun, mydec in *; desf.
    exfalso; apply not_or_and in n0; apply not_or_and in n; desf.
    destruct (neq_min_neq n0) as (m &?&?); case_eq (assn_leq (Q m) (Q0 m));
    ins; eauto 8 using eq_sym.

  × unfold PCM_leq_helper in *; desf; try subst PCM0.
    by rewrite <- eq_rect_eq in *; exploit salg_leq_total; ins; desf.
    by apply lenT.
Qed.

Lemma assn_leq_false_ne :
  ∀ p q, assn_leq p q = false → p ≠ q.
Proof.
  induction p; destruct q; ins; f_equal; desf; intro; ins;
    unfold leq_fun, mydec in *; desf; intuition eauto;
  by unfold Perm_leq_helper, PCM_leq_helper in *; desf;
     rewrite <- ?eq_rect_eq, ?lenn, ?permission_leq_refl, ?salg_leq_refl in ×.
Qed.

Lemma assn_leqTT :
  ∀ p q, assn_leq p q = false → p ≠ q ∧ assn_leq q p = true.
Proof.
  by split; [apply assn_leq_false_ne | apply assn_leqT].
Qed.

Lemma assn_leq_AfalseD P : assn_leq P Afalse → P = Afalse.
Proof.
  destruct P; ins.
Qed.

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 _ | Aghost _ _ _ _ ⇒ 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 Perm pIn prm SANE E E' ⇒ Apt Perm pIn prm SANE 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)
  | Aghost PCM pcmIN E g ⇒ Aghost PCM pcmIN E g
  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.
Proof.
  induction SZ; ins; desf; destruct p2; ins; desf; rewrite ?addnS in *; eauto.
  by destruct p1.
Qed.

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.
Proof.
  induction[p1 p2] SZ; ins; desf; desf.
  destruct p2; ins; desf; rewrite addnS in ×.
  rewrite IHSZ; ins; desf; rewrite Heq0 in *; ins.
Qed.

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)).
Proof.
  induction SZ; ins; desf; ins; desf; try congruence.
  destruct q; ins; desf; rewrite addnS in ×.
  rewrite assn_merge_fst_merge_rec; des_if.
  rewrite Heq0 in *; ins.
Qed.

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).
Proof.
  induction SZ; ins; desf; ins; try eapply assn_leqTT in Heq; desc; eauto;
    try solve [destruct p1; ins | destruct p2; ins].
  - ins; repeat split; eauto; try solve [destruct p1; ins; desf].
      eapply IHSZ; eauto; destruct p2; ins; rewrite ?addnS in *; desf.
  - ins; repeat split; eauto; try solve [destruct p1; ins; desf].
      eapply IHSZ; eauto; destruct p1; ins; desf.
      by eapply assn_merge_notemp; ins; destruct p1; ins; vauto.
      by destruct p1; ins; desf; eapply assn_merge_leq.
    destruct p1; ins; desf; intro; desf.
    rewrite assn_merge_fst_merge_rec in H0; ins; desf; eauto.
    rewrite H0 in *; destruct Heq0; split; try done.
  - ins; repeat split; eauto; try solve [destruct p1; ins; desf].
    by intro; desf; destruct Heq0; repeat case eqP; ins.
  - ins; repeat split; eauto; try solve [destruct p2; ins; desf].
      eapply IHSZ; eauto; destruct p2; ins; rewrite addnS in *; desf.
      by eapply assn_merge_notemp; ins; destruct p2; ins; rewrite addnS in *; vauto.
    by destruct p2; ins; rewrite addnS in *; desf; eapply assn_merge_leq.
    destruct p2; ins; rewrite addnS in *; desf; intro; desf.
   rewrite assn_merge_fst_merge_rec in H0; ins; desf; eauto.
  - ins; repeat split; eauto; try solve [destruct p2; ins; desf].
    intro; desc; congruence.
Qed.

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.
Proof.
  induction SZ; ins; desf; try eapply assn_leqT in Heq; eauto;
    try solve [destruct p1; ins | destruct p2; ins];
    assert (X: assn_merge_fst p1 = p1) by (destruct p1; ins);
    rewrite X in *; clear X.
      exploit assn_leqAS; eauto; ins; desf; [by rewrite Heq2|].
      destruct p2; ins; desf; rewrite addnS in *; eauto.
      by destruct NP.

      by desf; destruct NP; ins.

      exploit assn_leqAS; eauto; ins; desf.
      by destruct p2; ins; desf; rewrite addnS in *; f_equal; eapply IHSZ; eauto.

    assert (X: assn_merge_fst p2 = p2) by (destruct p2; ins);
    rewrite X in *; clear X; exploit assn_leqAS; eauto; ins; desf.
Qed.

Lemma assn_norm_wf p : assn_wf (assn_norm p).
Proof. induction p; ins; desf; eauto using assn_merge_wf. Qed.

Lemma assn_norm_wf2 p : assn_wf p → assn_norm p = p.
Proof.
  induction p; ins; desf; rewrite ?IHp1, ?IHp2, ?IHp;
    eauto using assn_merge_wf2;
    try solve [f_equal; eapply functional_extensionality; eauto].
  by destruct p1.
  by rewrite IHp2 in *; desf.
Qed.

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.
Proof.
  induction n; ins.
  case_eq (assn_leq (assn_merge_fst p) (assn_merge_fst q));
    [|intro X; rewrite (assn_leqT _ _ X); revert X];
    [case_eq (assn_leq (assn_merge_fst q) (assn_merge_fst p));
      [|intro X; rewrite (assn_leqT _ _ X); revert X; try done]|]; ins.

  {
    rewrite andbC; case ifP; intro M; rewrite M; [|clear M].
    clear H H0; desf; eauto using assn_leqAS;
  repeat 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_merge_fst p = p); [|by clear -H; destruct p]; clear H; intro H;
      rewrite H in *; try done
  end; eauto using assn_leqAS; ins; desf; ins.

rewrite IHn; ins; repeat (split; try done).
clear IHn; destruct n; ins; ins.
rewrite WFp4, eqxx; ins.
case eqP; [by intro; destruct WF5|intros _].
case eqP; [by intro; destruct WFp5|intros _]; ins.
by case ifP; ins; destruct WF5; split; ins; eauto using assn_leqAS.

clear IHn; destruct n; ins; rewrite WF4, eqxx; ins.
by case eqP; [by intro; destruct WF5|intros _].

clear IHn; destruct n; ins; rewrite WFp4, eqxx; ins.
by case eqP; [by intro; destruct WFp5|intros _].

  f_equal; eauto using assn_leqAS; desf;
  repeat 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_merge_fst p = p); [|by clear -H; destruct p]; clear H; intro H;
      rewrite H in *; try done
  end; eauto using assn_leqAS.

  × rewrite ltSS in ×.
    exploit (assn_leqAS p1 q1); ins; subst; rewrite IHn; ins; try rewrite addnS; ins;
       repeat (split; try done).
    clear IHn WFp WFp1 H H0.
    revert WF1 a0 a WF0 WF2 WF3 WF4 WF5 WFp0 WFp2 WFp3 WFp4 WFp5 PF.
    induction n; ins; clarify.

case ifP; [by intro; destruct WFp5; ins; desf|intros _].
case ifP; ins.
case ifP; [by intro; destruct WF5; ins; desf|intros _].
exploit (assn_leqAS q1 (assn_merge_fst a0)); ins; subst.
  f_equal; desf;
  repeat 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_merge_fst p = p); [|by clear -H; destruct p]; clear H; intro H;
      rewrite H in *; try done
  end; eauto.
destruct n; ins.
rewrite Heq, WFp4; case ifP; [|intros _;f_equal].
by intro; destruct WFp5; desf.

by desf; destruct a0.

  × rewrite (assn_leqAS _ _ H H0) in *; rewrite IHn; ins.
    by apply assn_merge_wf2; auto; rewrite addnC.
  × rewrite (assn_leqAS _ _ H H0) in *; rewrite IHn; ins; try rewrite addnC; ins.
    by symmetry; apply assn_merge_wf2; auto.
}


case ifP; [|by intros _; desf; destruct p; ins; desf; f_equal; apply IHn].
by ins; exfalso; desc; destruct p; ins; destruct q; ins; desf.

case ifP; [intro|intros _].
by ins; exfalso; desc; destruct p; ins; destruct q; ins; desf.
by desf; ins; f_equal; destruct q; ins; rewrite addnS in *; desf; apply IHn.
Qed.

Lemma assn_mergeC :
  ∀ p (WFp: assn_wf p) q (WF : assn_wf q),
    assn_merge p q = assn_merge q p.
Proof.
  by ins; unfold assn_merge; rewrite assn_merge_recC, addnC.
Qed.

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).
Proof.
  induction n; ins; desf; ins;
  repeat 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 |- _ ⇒
      try (by destruct p; ins);
      cut (assn_merge_fst p = p); [|by clear -H; destruct p]; clear H; intro H;
      rewrite H in *; try done
  end; eauto using assn_leqAS; rewrite ?leSS; auto using lenW, len_addr, len_addl.
Qed.

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.
Proof. by destruct p. Qed.

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.
Proof.
  induction n; ins; desf; assn_merge_clarify; clarify.
  by unfold assn_star_rdf; ins; desf; desf; assn_merge_clarify;
     apply assn_merge_wf2; ins.
  by destruct q; ins; desf; unfold assn_star_rdf; rewrite !eqxx; ins.
  by destruct q; ins; unfold assn_star_rdf; desf; desf.
  by f_equal; apply IHn; eauto.
  by destruct q; ins; desf; desf; assn_merge_clarify.
Qed.

Lemma assn_insertC_base p q :
  assn_not_star p → assn_not_star q → assn_insert p q = assn_insert q p.
Proof.
  destruct p, q; ins; unfold assn_star_rdf; desf; desf; assn_merge_clarify;
    desf; repeat f_equal; apply proof_irrelevance.
Qed.

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).
Proof.
  induction r; ins; unfold assn_star_rdf; desf; desf; ins;
  unfold assn_star_rdf; desf; desf; assn_merge_clarify;
  eauto using f_equal, assn_insertC_base.
Qed.

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.
Proof.
  destruct q; ins; desf; desf.
Qed.

Lemma assn_insert_ff p :
  assn_insert Afalse (assn_insert Afalse p) = assn_insert Afalse p.
Proof.
  destruct p; ins; unfold assn_star_rdf; rewrite ?assn_leq_refl; ins;
  repeat first [rewrite !eqxx; ins | rewrite assn_leq_refl; ins
                | unfold assn_star_rdf; ins; desf];
  assn_merge_clarify.
Qed.

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.
Proof.
  destruct q; ins; unfold assn_star_rdf; desf; desf.
Qed.

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.
Proof.
  induction n; ins; desf; desf; assn_merge_clarify; clarify.

  rewrite IHn, (assn_merge_recC n), IHn; ins; eauto;
    try solve [by rewrite addnC | by rewrite addnS|repeat split; done].

  {
    rewrite assn_insert_ff, assn_merge_recC; ins.
    by destruct n.
  }

  {
    by destruct p; ins; unfold assn_star_rdf; ins; rewrite !eqxx, assn_merge_wf2; ins.
  }
  
  {
    by destruct p; ins; rewrite addn0 in *; rewrite <- assn_merge_recC, IHn; ins; desf;
       rewrite assn_insert_ff, assn_insert_before;
       desf; desf; assn_merge_clarify.
  }
  
  {
    destruct q; ins. destruct n; ins.
    apply not_and_or in WFp5; desf; desf; try (by destruct (assn_merge_fst a); desf); ins.
    by rewrite assn_leq_refl; unfold assn_star_rdf; ins; rewrite !eqxx; ins.
  }
  
  {
    destruct p, q; ins.
    by rewrite assn_leq_refl; unfold assn_star_rdf; rewrite !eqxx.
  }

  {
    rewrite assn_insert_before, assn_merge_fst_merge_rec; ins; desf; desf; assn_merge_clarify.
    by apply assn_merge_leq.
  }
    
  {
    rewrite (assn_merge_fst_not_star p) in *; try by destruct p.
    by destruct q; ins; rewrite Heq; unfold assn_star_rdf; ins; desf.
  }
  
  {
    rewrite IHn, (assn_merge_recC n), IHn; ins; eauto;
    try solve [by rewrite addnC | by rewrite addnS|repeat split; done].
    rewrite assn_insertC, assn_merge_recC; ins; [|by destruct n].
    rewrite (assn_insert_before q1);
    rewrite assn_merge_fst_insert, assn_merge_fst_merge_rec; ins;
    try solve [by clear -LTn; rewrite addnC; destruct n]; desf; desf;
    assn_merge_clarify.
  }
  
  {
    exfalso; destruct p, q1; ins; exploit assn_leqAS; eauto.
  }
  
  {
    by f_equal; rewrite IHn; desf; assn_merge_clarify.
  }
  
  {
    rewrite assn_merge_recC, assn_merge_ins, assn_insertC;
    eauto; try (by rewrite addnC); try (by destruct q).
    rewrite (assn_insert_before p1); ins; desf.
      by destruct WFp5; desf.
    rewrite (assn_merge_fst_not_star q) in *; try by destruct q.
    rewrite assn_insert_before; ins; desf; desf.
  }

  {
    rewrite (assn_merge_fst_not_star q) in *; try by destruct q.
    rewrite assn_insertC_base; try by destruct p, q.
    rewrite assn_insert_before; try done; desf; desf.
  }
Qed.

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).
Proof.
  intros; unfold assn_merge.
  rewrite assn_merge_recC, assn_merge_ins2, assn_merge_recC; ins;
    repeat split; ins; rewrite ?addnS; ins.
  by rewrite addnC.
Qed.

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.
Proof.
  intros; rewrite assn_mergeC; unfold assn_merge; try done.
  rewrite assn_merge_ins2; ins; desf.
  by exfalso; destruct q; ins.
Qed.

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).
Proof.
  intros; unfold assn_star_rdf; desf; desf.
  2: by apply assn_merge_star; ins; intros [X Y]; rewrite X, Y in *; destruct Heq; ins.
  destruct r; try rewrite assn_merge_star; ins; desf;
  [rewrite assn_merge_not_star; ins|]; rewrite assn_insert_ff; ins.
Qed.

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).
Proof.
  intros until r; revert p WFp NEp q WFq NEq NSq.
  induction r; ins; desf; try apply assn_merge_star; ins;
   try solve [rewrite assn_merge_rdf, !assn_merge_not_star; ins;
              try apply assn_insertC; ins; assn_merge_clarify; intro; desf];
   try solve [rewrite assn_merge_star, !assn_merge_not_star; ins;
              try apply assn_insertC; ins; assn_merge_clarify; intro; desf].

  symmetry; rewrite assn_merge_star; ins.
  rewrite assn_insertC; ins.
  rewrite <- IHr2; ins.
  rewrite assn_merge_rdf, assn_merge_star; ins; eauto 8.
    rewrite assn_insertC; f_equal; eauto.

  symmetry; rewrite assn_merge_star; ins.
  rewrite assn_insertC; ins.
  rewrite <- IHr2; ins.
  rewrite assn_merge_star; ins; eauto.
    by rewrite <- assn_merge_not_star; ins; eauto using assn_merge_wf.
    by rewrite <- assn_merge_not_star; ins; eauto using assn_merge_notemp.
  apply assn_leqTT in Heq; desf.
  by rewrite assn_merge_fst_insert; desf.

  rewrite assn_merge_fst_insert; ins; intro; desf.
  by destruct WFr5; ins.
Qed.

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.
Proof.
  intros until 4.
  assert (X: ∀ r, assn_not_star r →
    assn_wf r → r ≠ Aemp →
    assn_merge p (assn_merge q r) = assn_merge (assn_merge p q) r).
   by ins; rewrite !(@assn_merge_not_star r), assn_merge_insert; ins;
     eauto using assn_merge_wf, assn_merge_notemp.
  induction r; ins; desf; eauto; try (by eapply X).
  rewrite ?(assn_mergeC (Astar _ _)), !assn_merge_star, assn_merge_insert; ins;
  eauto using assn_merge_wf, assn_merge_notemp, f_equal.
Qed.

Lemma Asim_assn_norm p : Asim p (assn_norm p).
Proof.
  induction p; ins; vauto.
  desf; try rewrite Heq in *; try rewrite Heq0 in ×.
  × eapply Asim_trans; [eby eapply Asim_star|].
    by eapply Asim_trans, Asim_star_emp; vauto.
  × by eapply Asim_trans; [eby eapply Asim_star|]; vauto.
  × eapply Asim_trans; [eby eapply Asim_star|].
  unfold assn_merge.
  generalize (assn_norm p1), (assn_norm p2), (assn_norm_wf p1), (assn_norm_wf p2),
    Heq, Heq0; clear; intros p q.
  generalize (lenn (S (assn_merge_size p + assn_merge_size q))) as PF.
  rewrite leSn.
  generalize (assn_merge_size p + assn_merge_size q) at -1; intro n.
  generalize (S n); clear n; intro n.
  revert p q; induction n; ins; desf; desf;
    try solve [destruct p; vauto |
               generalize PF; rewrite addnC in PF; ins; destruct q; vauto].

  destruct q; ins; desc; destruct p; ins; vauto; rewrite ?addnS in ×.
  by eapply Asim_trans, IHn; eauto using Asim.
  by eapply Asim_trans, IHn; ins; eapply Asim_trans,
      (Asim_star (Asim_star Asim_star_false (Asim_refl _)) (Asim_refl _));
      eauto using Asim.

  destruct q; ins; destruct p; ins; vauto.
  by eapply Asim_trans, Asim_star; try apply Asim_star_false; eauto using Asim.

  by destruct p; ins; desf; eapply Asim_trans, Asim_star, IHn; eauto using Asim.
  by destruct q; ins; desf; rewrite addnS in *;
     eapply Asim_trans, Asim_star, IHn; eauto using Asim.
Qed.

Lemma assn_norm_ok : ∀ P Q, Asim P Q ↔ assn_norm P = assn_norm Q.
Proof.
  split; [|by ins; eapply Asim_trans, Asim_sym, Asim_assn_norm; instantiate;
           rewrite <- H; apply Asim_assn_norm].
  induction 1; eauto; simpl; desf; try congruence; try solve [by f_equal; try exten];
    try eby edestruct assn_merge_notemp.
    by compute; rewrite assn_leq_refl; desf.
    by auto using assn_mergeC, assn_norm_wf.
  by rewrite assn_mergeA; auto using assn_norm_wf.
Qed.

Lemma assn_norm_idemp P : assn_norm (assn_norm P) = assn_norm P.
Proof. apply assn_norm_ok; eauto using Asim_assn_norm, Asim. Qed.

Lemma assn_norm_emp : assn_norm Aemp = Aemp.
Proof. done. Qed.

Lemma assn_norm_false : assn_norm Afalse = Afalse.
Proof. done. Qed.

Lemma assn_norm_star_emp P : assn_norm (Astar Aemp P) = assn_norm P.
Proof. simpl; desf; desf. Qed.

Lemma assn_norm_star_emp_r P : assn_norm (Astar P Aemp) = assn_norm P.
Proof. simpl; desf; desf. Qed.

Lemma assn_norm_star_eq_emp P Q :
  assn_norm (Astar P Q) = Aemp →
  assn_norm P = Aemp ∧ assn_norm Q = Aemp.
Proof.
  ins; desf; auto; unfold assn_merge in *; ins; desf.
  exfalso; eapply assn_merge_notemp in H; ins.
  by rewrite ltn_add2l; destruct (assn_norm Q); ins; desf.
Qed.

Lemma assn_merge_rec_not_false P Q n :
  assn_wf Q →
  assn_merge_rec P Q n = Afalse → P = Afalse ∧ Q = Afalse.
Proof.
  induction[P Q] n; ins; desf; desf; assn_merge_clarify.
  exfalso; eapply IHn in H0; ins; desf; ins; tauto.
  destruct Q; ins; eauto.
Qed.

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.
Proof.
  ins; desf; auto; unfold assn_merge in *; ins; desf; desf;
  assert (W := assn_norm_wf Q).
  by assn_merge_clarify; eapply assn_merge_rec_not_false in H; ins; desf; assn_merge_clarify.
  by destruct (assn_norm Q); ins; eauto.
Qed.