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.


Lemma Apt_equal Perm psIn p SANE x v Perm' psIn' p' SANE' x' v' (EQ: Perm = Perm'):
   (@eq_rect Permission Perm (fun x ⇒ x) p Perm' EQ) = p' → x = x' → v = v'
  → Apt Perm psIn p SANE x v = Apt Perm' psIn' p' SANE' x' v'.

Lemma Aghost_equal PCM pcmIN E g PCM' pcmIN' E' g' (EQ: PCM = PCM'):
  (@eq_rect salg_mod PCM (fun x ⇒ x) g PCM' EQ) = g' → E = E'
  → Aghost PCM pcmIN E g = Aghost PCM' pcmIN' E' g'.

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

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

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

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

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


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

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

Lemma Perm_leq_helperAS Perm Perm' p p':
  In Perm PS → In Perm' PS → Perm_leq_helper Perm Perm' p p' → Perm_leq_helper Perm' Perm p' p
  → Perm = Perm' ∧ ∃ EQ, (eq_rect Perm (fun x ⇒ x) p Perm' EQ) = p'.

Lemma PCM_leq_helperAS PCM PCM' g g':
  In PCM PSg → In PCM' PSg → PCM_leq_helper PCM PCM' g g' → PCM_leq_helper PCM' PCM g' g
  → PCM = PCM' ∧ ∃ EQ, (eq_rect PCM (fun x ⇒ x) g PCM' EQ) = g'.

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

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

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

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

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

Lemma assn_leq_refl :
  ∀ p, assn_leq p p.

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

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

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

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

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

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

Opaque assn_leq.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Lemma assn_norm_wf p : assn_wf (assn_norm p).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Lemma Asim_assn_norm p : Asim p (assn_norm p).

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

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

Lemma assn_norm_emp : assn_norm Aemp = Aemp.

Lemma assn_norm_false : assn_norm Afalse = Afalse.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Lemma assn_norm_star_intro:
  ∀ P Q, assn_norm (Astar P Q) = assn_norm (Astar (assn_norm P) (assn_norm Q)).

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








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