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.
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 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.
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;

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

Lemma assn_leq_refl :
  ∀ p, assn_leq p p.
Proof.
  induction p; ins; desf; unfold leq_fun, mydec; desf; try solve[exfalso; eauto].
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].
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 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.
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 rewrite lenn 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 _ ⇒ 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.
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 desf; ins; rewrite assn_leq_refl; 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.
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 unfold assn_star_rdf; ins; rewrite !eqxx, assn_merge_wf2; ins.

  by ins; rewrite addn0 in *; rewrite <- assn_merge_recC, IHn; ins; desf;
     rewrite assn_insert_ff, assn_insert_before;
     desf; desf; assn_merge_clarify.

  ins; rewrite assn_leq_refl.
  by unfold assn_star_rdf; ins; rewrite !eqxx; ins.

  by rewrite assn_insert_before; rewrite assn_merge_fst_merge_rec;
     ins; desf; desf; assn_merge_clarify.

  by rewrite assn_insert_before;
     ins; desf; desf; assn_merge_clarify.

  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.

  by f_equal; rewrite IHn; desf; assn_merge_clarify.

  rewrite assn_merge_recC, assn_merge_ins, assn_insertC;
    eauto; try (by rewrite addnC).
  rewrite (assn_insert_before p1); desf; desf; assn_merge_clarify.
  by rewrite assn_insert_before; ins; desf; desf.

  by destruct q; ins; desf; assn_merge_clarify.
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_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.
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);
  assn_merge_clarify; eapply assn_merge_rec_not_false in H; ins; desf.
  assn_merge_clarify.
Qed.

Lemma Asim_star_emp_l P : Asim P (Astar Aemp P).
Proof. eauto using Asim. Qed.

Lemma Asim_star_emp_r P : Asim P (Astar P Aemp).
Proof. eauto using Asim. Qed.

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.
Proof. split; eauto using Asim, Asim_assn_norm. Qed.

Lemma Asim_norm_r P Q: Asim P (assn_norm Q) ↔ Asim P Q.
Proof. split; eauto using Asim, Asim_assn_norm. Qed.

Lemma Asim_starAC P Q R :
  Asim (Astar P (Astar Q R)) (Astar Q (Astar P R)).
Proof.
  eauto using Asim.
Qed.

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´).
Proof.
  intros.
  eapply Asim_trans, Asim_trans, Asim_starC; [eapply Asim_starC|].
  eapply Asim_trans, Asim_trans, Asim_starA; [eapply Asim_sym, Asim_starA|].
  eapply Asim_star; vauto.
  by eapply Asim_trans, Asim_trans, Asim_starC; [eapply Asim_starC|].
Qed.

Lemma Asim_foldr_simpl l Q :
  Asim (foldr Astar l Q) (Astar (foldr Astar l Aemp) Q).
Proof.
  induction l; ins; eauto using Asim.
Qed.

Lemma Asim_foldr_pull l P Q :
   Asim (foldr Astar l (Astar P Q))
        (Astar P (foldr Astar l Q)).
Proof.
  induction l; ins; [apply Asim_refl|].
  eapply Asim_trans, Asim_starA.
  eapply Asim_trans, Asim_star, Asim_refl; [|apply Asim_starC].
  eapply Asim_trans, Asim_sym, Asim_starA.
  eapply Asim_star, IHl; apply Asim_refl.
Qed.

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).
Proof.
  ins; apply assn_norm_ok, eq_sym in H; ins.
  destruct P; ins; desf; eauto; right; repeat eexists.
  by right; left; split; apply assn_norm_ok; ins.
  by left; split; apply assn_norm_ok; ins.
  by right; right; eapply assn_merge_rec_not_false in H; desf;
     auto using assn_norm_wf; split; apply assn_norm_ok.
Qed.

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´.
Proof.
  induction[P Q] n; ins; desf; desf; eauto.
    by destruct Q; ins; desf; rewrite addnS in *; eapply IHn; eauto.
  destruct Q; ins; destruct P; ins; eauto.
Qed.

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.
Proof.
  ins; subst; apply assn_norm_ok in H; rewrite !assn_norm_ok; ins; desf; eauto.
  destruct (eqP (assn_norm R) Afalse) as [EQ|NEQ].
    rewrite EQ in *; apply assn_merge_rec_not_false in H; desf; eauto using assn_norm_wf.
    by apply (assn_norm_ok R Afalse), Asim_sym, Asim_falseD in EQ; desf; eauto 6.
  rewrite <- H in NEQ; apply assn_merge_not_false2 in NEQ; auto using assn_norm_wf.
  desf; unfold assn_merge in H; rewrite H in NEQ; clear H.
  by left; destruct R; ins; eauto.
Qed.

Lemma Asim_star_empD P Q :
  Asim (Astar P Q) Aemp ↔ Asim P Aemp ∧ Asim Q Aemp.
Proof.
  split; intros; desf.
    by destruct (Asim_starD H); desf; eauto; split; auto.
  by rewrite assn_norm_ok in *; simpl; rewrite H, H0; ins; rewrite eqxx.
Qed.

Lemma Asim_emp_starD P Q :
  Asim Aemp (Astar P Q) ↔ Asim Aemp P ∧ Asim Aemp Q.
Proof.
  split; intros; desf.
    by apply Asim_sym in H; destruct (Asim_starD H); desf; eauto; split;
       auto using Asim_sym.
  by rewrite assn_norm_ok in *; simpl; rewrite <- H, <- H0; ins; rewrite eqxx.
Qed.

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

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).
Proof.
  induction q; ins; desf; ins; try omega; try (by destruct p; ins);
  try rewrite IHq2; try rewrite assn_rdf_size; try intro; desf; desf; ins; desf; ins.
  by destruct H; ins.
  by destruct H; unfold assn_merge; rewrite assn_merge_fst_merge_rec; ins.
Qed.

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.
Proof.
  intros; eapply (f_equal assn_merge_size) in H1; ins.
  rewrite assn_insert_size in *; try done.
  destruct p; ins.
Qed.

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

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´.
Proof.
  ins; case_eq (assn_not_star q´); intros.
    rewrite !assn_insert_not_star_eq in EQ; ins.
    by unfold assn_star_rdf in *; desf; desf.
  generalize (f_equal assn_merge_size EQ); rewrite !assn_insert_size; ins.
  by destruct q´; ins; destruct q; ins.
Qed.

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´.
Proof.
  intros until q.
  induction q; intros; eauto using assn_insert_cancel1.
    pose proof (f_equal assn_merge_size EQ) as S; rewrite !assn_insert_size in S; clarify.
    destruct q´; ins; desc.
  rewrite !assn_norm_wf2 in *; ins.
  repeat (revert NF; case eqP; try done; intros _ ?).
  repeat (revert NF´; case eqP; try done; intros _ ?).
  assert (X: assn_star_rdf p (Astar q1 q2) = Astar p (Astar q1 q2)).
    clear EQ IHq1 IHq2.
    unfold assn_merge in NF; rewrite assn_merge_fst_merge_rec in NF; ins.
    unfold assn_star_rdf; ins; desf; desf; destruct NF; ins.
  rewrite X in *; clear X.
  assert (X: assn_star_rdf p (Astar q´1 q´2) = Astar p (Astar q´1 q´2)).
    clear EQ IHq1 IHq2.
    unfold assn_merge in NF´; rewrite assn_merge_fst_merge_rec in NF´; ins.
    unfold assn_star_rdf; ins; desf; desf; destruct NF´; ins.
  rewrite X in *; clear X.
  desf.
by rewrite ?assn_leq_refl in ×.
by rewrite ?assn_leq_refl in ×.
by f_equal; eauto; eapply IHq2; eauto; intro; desf.
Qed.

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´.
Proof.
  induction n; try done; destruct m; intros; try done.
  rewrite !(assn_merge_ins2 (S _)) in EQ; ins; desf;
  [destruct p; ins; desc; clarify; rewrite !assn_norm_wf2 in *; ins; desf; ins|];
  eapply assn_insert_cancel in EQ; eauto using assn_merge_wf;
  try (unfold assn_merge in NF, NF´; rewrite assn_merge_ins, assn_insert_before in NF, NF´; ins);
  try rewrite assn_norm_wf2; eauto using assn_merge_wf.
  4: by destruct p.
  by eapply IHn in EQ; ins; clear IHn LT LT´; rewrite !assn_norm_wf2; ins; desf; desf; ins;
     intros [A B]; rewrite A, B in *; exploit assn_leq_AfalseD; eauto.

  revert NF NF´; case ifP; ins; desc; clarify; try tauto.
  rewrite assn_merge_fst_merge_rec; desf.

  revert NF NF´; case ifP; ins; desc; clarify; try tauto.
  rewrite assn_merge_fst_merge_rec; desf.

  rewrite !assn_norm_wf2 in *; ins; intro; desf; ins; tauto.
  rewrite !assn_norm_wf2 in *; ins; intro; desf; ins; tauto.
Qed.

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).
Proof.
  induction n; ins; desf; desf; ins;
  repeat match goal with
    | H: assn_merge_snd ?p = Some _ |- _ ⇒
      destruct p; ins; inv H; clear H; try rewrite addnS in *; desf
  end; eauto using assn_leqAS; f_equal; eauto.
  by apply IHn; ins; intro X; rewrite X in *; exploit assn_leq_AfalseD; eauto.
  by destruct p; ins.
  by destruct q; ins.
Qed.

Lemma Asim1 P Q :
  Asim P (Astar P Q) →
  Asim Q Aemp ∨ Asim Q Afalse ∧ ∃ P´, Asim P (Astar Afalse P´).
Proof.
  ins.
  cut (Asim Q Aemp ∨ Asim Q Afalse ∧ ∃ P´, Asim (assn_norm P) (Astar Afalse P´)).
    by ins; desf; eauto using Asim, Asim_assn_norm.
  rewrite !assn_norm_ok in *; ins; desf; try (left; congruence).
  rename H into EQ.
  generalize (f_equal assn_merge_size EQ) as SZ;
  revert EQ Heq Heq0; generalize (assn_norm_wf P) as WF, (assn_norm_wf Q) as WF´.
  generalize (assn_norm P) as p, (assn_norm Q) as q; clear; ins.

  destruct (eqP (assn_merge_fst p) Afalse) as [EQ´|].
  2: exfalso; ins; eauto 7; [];
     unfold assn_merge in SZ; rewrite assn_merge_size_merge2 in SZ;
     ins; repeat (split; try done); omega.

  destruct (eqP (assn_merge_fst q) Afalse) as [EQ´´|].
  2: exfalso; rewrite assn_mergeC in SZ; ins; eauto 7; [];
     unfold assn_merge in SZ; rewrite assn_merge_size_merge2 in SZ;
     ins; repeat (split; try done); omega.

  destruct q; ins.
    by destruct p; ins; subst; eauto using Asim.
  exfalso; clear EQ; subst q1.
  destruct p; ins; subst;
  revert SZ; unfold assn_merge; simpl; rewrite !eqxx; simpl;
  desc; desf; desf; try tauto.
  simpl; rewrite addnS, assn_merge_size_merge2; ins; try omega.
  tauto.
Qed.

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´)).
Proof.
  destruct (eqP (assn_merge_fst (assn_norm Q)) Afalse) as [EQ|NEQ].
    by right; left; clear -EQ; unfold assn_merge_fst in *; desf;
       eexists; eapply (Asim_trans (Asim_assn_norm _)); rewrite Heq; eauto using Asim.
  destruct (eqP (assn_merge_fst (assn_norm Q´)) Afalse) as [EQ|NEQ´].
    by right; right; clear -EQ; unfold assn_merge_fst in *; desf;
       eexists; eapply (Asim_trans (Asim_assn_norm _)); rewrite Heq; eauto using Asim.
  left.
  ins; rewrite assn_norm_ok in *; simpls; desf; try congruence.

    rewrite assn_mergeC in *; auto using assn_norm_wf;
    unfold assn_merge in H; eapply (f_equal assn_merge_size) in H;
    rewrite assn_merge_size_merge2 in H; eauto using assn_norm_wf; omega.

    rewrite assn_mergeC in *; auto using assn_norm_wf;
    unfold assn_merge in H; eapply (f_equal assn_merge_size) in H;
    rewrite assn_merge_size_merge2 in H; eauto using assn_norm_wf; omega.

  by apply assn_merge_cancel in H; ins; auto using assn_norm_wf;
     rewrite !assn_norm_idemp; intro; desf.
Qed.

Lemma assn_norm_star_false :
  assn_norm (Astar Afalse Afalse) = Afalse.
Proof.
  compute; desf.
Qed.

Global Opaque assn_norm.