Assertions


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 xx) 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 xx) 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.

Syntactic assertion similarity: the smallest congruence relation containing the ACI rules for Astar.

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 : assnmydec (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 xx) 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 EQsalg_leq PCM' (eq_rect PCM (fun xx) 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 xx) 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 xx) 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
    | _ , Afalsefalse
    | Aemp , _true
    | _ , Aempfalse
    | 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.

Normalization


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

Definition assn_merge_fst P :=
  match P with
    | Astar p qp
    | _P
  end.

Definition assn_merge_snd P :=
  match P with
    | Astar p qSome 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 qassn_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 qassn_wf p assn_wf q
    | Arel _ pp
    | Aacq _ pp
    | Armwacq _ pp
    | Aforall pp x, assn_wf (pp x)
    | Atriangle passn_wf p
    | Anabla passn_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
                 | NoneP
                 | Some Q' ⇒ @assn_merge_rec P Q' sz
               end)
        else
        Astar (assn_merge_fst P)
              (match assn_merge_snd P with
                 | NoneQ
                 | Some P' ⇒ @assn_merge_rec P' Q sz
               end)
      else
        Astar (assn_merge_fst Q)
              (match assn_merge_snd Q with
                 | NoneP
                 | 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
  | AfalseAfalse
  | AempAemp
  | Aimplies P QAimplies (assn_norm P) (assn_norm Q)
  | Aforall PPAforall (fun xassn_norm (PP x))
  | Apt Perm pIn prm SANE E E'Apt Perm pIn prm SANE E E'
  | Aptu EAptu 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 EArainit E
  | Arel E QQArel E (fun vassn_norm (QQ v))
  | Aacq E QQAacq E (fun vassn_norm (QQ v))
  | Armwacq E QQArmwacq E (fun vassn_norm (QQ v))
  | Atriangle PAtriangle (assn_norm P)
  | Anabla PAnabla (assn_norm P)
  | Aghost PCM pcmIN E gAghost PCM pcmIN E g
  end.

Lemmas about assn_merge

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

Two assertions are syntactically similar iff they have the same normal form.

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.

Syntactic properties of assertions


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.

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.

Lemma assn_norm_star_intro:
   P Q, assn_norm (Astar P Q) = assn_norm (Astar (assn_norm P) (assn_norm Q)).
Proof.
  intros P Q; apply assn_norm_ok, Asim_star; apply Asim_assn_norm.
Qed.

Global Opaque assn_norm.

End Assertions.

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]).

Arguments Apt [PS] [PSg] _ _ _ _ _ _.

Arguments Aptu [PS] [PSg] _.

Arguments Aemp {PS} {PSg}.

Arguments Arainit [PS] [PSg] _.

Arguments Afalse {PS} {PSg}.

Arguments Atrue {PS} {PSg}.

Arguments Aghost [PS] [PSg] _ _ _ _.

Infix "&*&" := (@Astar _ _) (at level 35, right associativity).

This page has been generated by coqdoc