Assertions


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 : valassn)
  | Apt (E : val)
  | Aptu (E : val)
  | Astar (P Q: assn)
  | Arainit (E : val)
  | Arel (E : val) (Q : valassn)
  | Aacq (E: val) (Q : valassn)
  | Armwacq (E: val) (Q : valassn)
  | Atriangle (P: assn)
  | Anabla (P: assn).

Definition Atrue := Aimplies Afalse Afalse.

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

Inductive Asim : assnassnProp :=
  | 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 (: 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) = falsee2 e1.
Proof. by case cmpP. Qed.

Lemma lenAS e1 e2 : e1 e2e2 e1e1 = 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 leq_fun A (leq : AAbool) 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 if P == then assn_leq Q else assn_leq 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 if P == then assn_leq Q else assn_leq P
    | Astar _ _ , _true
    | _ , Astar _ _false
    | Arainit E , Arainit E
    | Arainit _ , _true
    | _ , Arainit _false
    | Arel E PP , Arel PP´if E == then leq_fun assn_leq PP PP´ else E
    | Arel _ _ , _true
    | _ , Arel _ _false
    | Aacq E PP , Aacq PP´if E == then leq_fun assn_leq PP PP´ else E
    | Aacq _ _ , _true
    | _ , Aacq _ _false
    | Armwacq E PP, Armwacq PP´if E == then leq_fun assn_leq PP PP´ else E
    | Armwacq _ _ , _true
    | _ , Armwacq _ _false
    | Atriangle P , Atriangle assn_leq P
    | Atriangle _ , _true
    | _ , Atriangle _false
    | Anabla P , Anabla assn_leq P
    end.

Lemma leq_funAS A leq (AS: antisymmetric leq) p q :
  leq_fun (A:=A) leq p qleq_fun leq q pp = 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 : AAbool) p q r
  (AS: p q, leq p qleq q pp = q)
  (T: x, leq (p x) (q x) → leq (q x) (r x) → leq (p x) (r x)) :
  leq_fun (A:=A) leq p qleq_fun leq q rleq_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 qassn_leq q pp = q.
Proof.
  induction p; destruct q; ins; try rewrite beq_sym in H0; try rewrite (beq_sym _ ) 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) (: 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 : natA) (NEQ: f g) :
   m, f m g m ( x, x < mf 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 = falseassn_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 = falsep 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 = falsep 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 AfalseP = 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 _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 ⇒ @assn_merge_rec P sz
               end)
        else
        Astar (assn_merge_fst P)
              (match assn_merge_snd P with
                 | NoneQ
                 | Some ⇒ @assn_merge_rec Q sz
               end)
      else
        Astar (assn_merge_fst Q)
              (match assn_merge_snd Q with
                 | NoneP
                 | Some ⇒ @assn_merge_rec P 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 E Apt E
  | Aptu EAptu E
  | Astar P Q
      let := assn_norm P in
      let := assn_norm Q in
      if == Aemp then
      else if == Aemp then
      else assn_merge
  | 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)
  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 passn_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
      if assn_leq p then assn_star_rdf p q
      else Astar (assn_insert p )
    | _
      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 passn_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, : assn_leq ?q ?p = true |- _
      eapply assn_leqAS in H; eauto; try subst p; try subst q
    | H : assn_leq ?p ?q = true, : 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 passn_not_star qassn_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 passn_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 assn_insert (assn_merge_fst p) (assn_merge_rec 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 rr 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_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 = AfalseP = 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.

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.

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 R :
  Asim (Astar P R) (Astar ) →
  Asim (Astar (Astar P Q) R)
       (Astar (Astar Q) ).
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 = Astar
   (Asim Afalse Asim Aemp
    Asim Aemp Asim Afalse
    Asim Afalse Asim 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 AempQ Aemp
   , assn_merge_rec P Q n = Astar .
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
  ( , R = Astar )
  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))
    (NF´: ¬ (p = Afalse assn_merge_fst (assn_norm ) = Afalse))
    (EQ: assn_insert p q = assn_insert p ),
   assn_wf qassn_wf q = .
Proof.
  ins; case_eq (assn_not_star ); 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 ; 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))
    (NF´: ¬ (p = Afalse assn_merge_fst (assn_norm ) = Afalse))
    (EQ: assn_insert p q = assn_insert p )
    (WF: assn_wf q) (WF´: assn_wf ),
  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 ; 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 p
    (LT: assn_merge_size p + assn_merge_size q < n)
    (LT´: assn_merge_size p + assn_merge_size < 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 ) = Afalse))
    (EQ: assn_merge_rec p q n = assn_merge_rec p m),
    p Aempq Aemp Aemp
    assn_wf passn_wf qassn_wf 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 , Asim P (Astar Afalse ).
Proof.
  ins.
  cut (Asim Q Aemp Asim Q Afalse , Asim (assn_norm P) (Astar Afalse )).
    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 :
  Asim (Astar P Q) (Astar P ) →
  Asim Q
   ( , Asim Q (Astar Afalse ))
   ( , Asim (Astar Afalse )).
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 )) 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.

Model of heaps

Assertions modulo the syntactic rules

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

Labels for non-atomic locations

Inductive HeapLabel :=
  | HLnormal
  | HLtriangle
  | HLnabla.

Labels for atomic locations

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

Coercion label_to_combination (lbl: HeapLabel) :=
  match lbl with
    | HLnormalHLCnormal
    | HLtriangleHLCtriangle
    | HLnablaHLCnabla
  end.

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

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

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

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

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

Definition is_normalO olbl :=
  match olbl with
    | Some lblis_normal lbl
    | NoneFalse
  end.

Definition HLleq lbl1 lbl2 :=
  match lbl1, lbl2 with
    | HLCnormal , _is_normal lbl2
    | HLCtriangle , _is_triangle lbl2
    | HLCnabla , _is_nabla lbl2
    | HLCdiamond , _lbl2 = HLCdiamond lbl2 = HLCdiamonddot
    | HLCtriangledot, _lbl2 = HLCtriangledot lbl2 = HLCdiamonddot
    | HLCnabladot , _lbl2 = HLCnabladot lbl2 = HLCdiamonddot
    | HLCdiamonddot , _lbl2 = HLCdiamonddot
  end.

Definition oHLleq (olbl1 olbl2: option HeapLabelCombination) :=
  match olbl1, olbl2 with
    | None, _True
    | Some lbl1, Some lbl2HLleq lbl1 lbl2
    | _, _False
  end.

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

Inductive heap :=
  | Hundef
  | Hdef (hf: valHeapVal).

Definition HVlabeled hv (lbl: HeapLabel) :=
  match hv with
    | HVnoneTrue
    | HVuval lbl´lbl = lbl´
    | HVval _ lbl´lbl = lbl´
    | HVra _ _ _ None NoneFalse
    | HVra _ _ _ (Some permlbl) NoneHLleq lbl permlbl
    | HVra _ _ _ None (Some initlbl) ⇒ HLleq lbl initlbl
    | HVra _ _ _ (Some permlbl) (Some initlbl) ⇒ HLleq lbl permlbl HLleq lbl initlbl
  end.

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

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

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

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

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

Definition HVlabeledW hv (lbl: HeapLabel) :=
  match hv with
    | HVnoneFalse
    | HVuval lbl´lbl = lbl´
    | HVval _ lbl´lbl = lbl´
    | HVra _ _ _ (Some permlbl) _HLleq lbl permlbl
    | _False
  end.

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

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

Definition HVsim hv hv´ :=
  match hv, hv´ with
    | HVnone, HVnoneTrue
    | HVuval _, HVuval _True
    | HVval v _, HVval _v =
    | HVra RR QQ isrmwflag perm init, HVra RR´ QQ´ isrmwflag´ perm´ init´
                 ⇒ RR = RR´ QQ = QQ´ isrmwflag = isrmwflag´ HLCsim perm perm´ HLCsim init init´
    | _, _False
  end.

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

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

Definition lupd h lbl :=
  match h with
    | HundefHundef
    | Hdef hfHdef (fun lmatch hf l with
                                  | HVnoneHVnone
                                  | HVuval _HVuval lbl
                                  | HVval v _HVval v lbl
                                  | HVra PP QQ isrmw None NoneHVra PP QQ isrmw None None
                                  | HVra PP QQ isrmw (Some _) NoneHVra PP QQ isrmw lbl None
                                  | HVra PP QQ isrmw None (Some _) ⇒ HVra PP QQ isrmw None lbl
                                  | HVra PP QQ isrmw (Some _) (Some _) ⇒ HVra PP QQ isrmw lbl lbl
                                 end)
    end.

Definition is_val v :=
  match v with
      HVval _ HLnormal | HVuval HLnormaltrue
    | HVnone | HVra _ _ _ _ _ | _false
  end.

Definition has_value hv v :=
  match hv with
    | HVval _ = v
    | _False
  end.

Definition is_nonatomic hv :=
  match hv with
    | HVval _ _true
    | HVuval _true
    | _false
  end.

Definition is_atomic hv :=
  match hv with
    | HVra _ _ _ _ _true
    | _false
  end.

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

Definition hemp : heap := Hdef (fun vHVnone).

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

Definition hv_rval isrmw P :=
  match isrmw with
    | trueP
    | falseAemp
  end.

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

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

Definition hlplus lbl1 lbl2 :=
  match lbl1, lbl2 with
    | HLCdiamonddot , _HLCdiamonddot
    | _ , HLCdiamonddotHLCdiamonddot
    | HLCnabladot , HLCtriangledotHLCdiamonddot
    | HLCnabladot , HLCdiamondHLCdiamonddot
    | HLCnabladot , HLCtriangleHLCdiamonddot
    | HLCnabladot , _HLCnabladot
    | HLCtriangledot , HLCnabladotHLCdiamonddot
    | HLCtriangledot , HLCdiamondHLCdiamonddot
    | HLCtriangledot , HLCnablaHLCdiamonddot
    | HLCtriangledot , _HLCtriangledot
    | HLCdiamond , HLCnabladotHLCdiamonddot
    | HLCdiamond , HLCtriangledotHLCdiamonddot
    | HLCdiamond , HLCnormalHLCdiamonddot
    | HLCdiamond , _HLCdiamond
    | HLCnabla , HLCnabladotHLCnabladot
    | HLCnabla , HLCtriangledotHLCdiamonddot
    | HLCnabla , HLCdiamondHLCdiamond
    | HLCnabla , HLCnablaHLCnabla
    | HLCnabla , HLCtriangleHLCdiamond
    | HLCnabla , HLCnormalHLCnabladot
    | HLCtriangle , HLCnabladotHLCdiamonddot
    | HLCtriangle , HLCtriangledotHLCtriangledot
    | HLCtriangle , HLCdiamondHLCdiamond
    | HLCtriangle , HLCnablaHLCdiamond
    | HLCtriangle , HLCtriangleHLCtriangle
    | HLCtriangle , HLCnormalHLCtriangledot
    | HLCnormal , HLCnabladotHLCnabladot
    | HLCnormal , HLCtriangledotHLCtriangledot
    | HLCnormal , HLCdiamondHLCdiamonddot
    | HLCnormal , HLCnablaHLCnabladot
    | HLCnormal , HLCtriangleHLCtriangledot
    | HLCnormal , HLCnormalHLCnormal
  end.

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

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

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

hsum : iterated hplus

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

Definition hupd B (h : natB) y z := fun xif x == y then z else h x.

Singleton heap cell

Notation hsingl l v := (Hdef (hupd (fun _HVnone) l v)).

initialize : add HLnormal to the set of initialization labels of an atomic location

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

Global Opaque hplus.

Assertion semantics


Definition Wemp : valassn_mod := fun _mk_assn_mod Afalse.
Definition Remp : valassn_mod := fun _mk_assn_mod Aemp.

Fixpoint assn_sem (P : assn) (h : heap) :=
  match P with
    | AfalseFalse
    | Aemph = hemp
    | Aimplies P Qh Hundef (assn_sem P hassn_sem Q h)
    | Aforall PP x, assn_sem (PP x) h
    | Apt E h = hsingl E (HVval HLnormal)
    | Aptu Eh = hsingl E (HVuval HLnormal)
    | Astar P Q
         h1 h2, h Hundef hplus h1 h2 = h assn_sem P h1 assn_sem Q h2
    | Arainit Eh = Hdef (hupd (fun _HVnone) E (HVra Wemp Remp false None (Some HLCnormal)))
    | Arel E Ph = hsingl E (HVra (fun xmk_assn_mod (P x)) Remp false (Some HLCnormal) None)
    | Aacq E Qh = hsingl E (HVra Wemp (fun xmk_assn_mod (Q x)) false None None)
    | Armwacq E Qh = hsingl E (HVra Wemp (fun xmk_assn_mod (Q x)) true (Some HLCnormal) None)
    | Atriangle QHlabeledExact h HLtriangle
                      , assn_sem Q Hsim h HlabeledExact HLnormal
    | Anabla QHlabeledExact h HLnabla
                      , assn_sem Q Hsim h HlabeledExact HLnormal
  end.

Definition assn_sem_sim P h := , assn_sem P Hsim h .

Definition implies P Q := h, assn_sem P hassn_sem Q h.

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

Definition normalizable P :=
   h, assn_sem P h hN , assn_sem P hN HlabeledExact hN HLnormal h = hplus hN .

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


This page has been generated by coqdoc