Library Assertions

Require Import HahnBase.
Require Import Heaps.
Require Import HeapSolver.
Require Import List.
Require Import Permissions.
Require Import PermSolver.
Require Import Permutation.
Require Import PermutationTactic.
Require Import Prelude.
Require Import Process.
Require Import ProcMap.
Require Import ProcMapSolver.
Require Import Programs.
Require Import QArith Qcanon.

Import ListNotations.

Set Implicit Arguments.

Assertions


Module Type Assertions
  (domains : Domains)
  (heaps : Heaps domains)
  (hsolver : HeapSolver domains heaps)
  (procs : Processes domains)
  (procmaps : ProcMaps domains heaps procs)
  (progs : Programs domains heaps procs procmaps)
  (pmsolver : ProcMapSolver domains heaps procs procmaps).

Export domains heaps hsolver procs procmaps pmsolver progs.

Statics

Below is the syntax of assertions of the program logic.

Inductive Assn :=
  | Aplain(B : Cond)
  | Aex(A : Val -> Assn)
  | Adisj(A1 A2 : Assn)
  | Astar(A1 A2 : Assn)
  | Awand(A1 A2 : Assn)
  | Apointsto(t : PointsToType)(q : Qc)(E1 E2 : Expr)
  | Aproc(x : Var)(q : Qc)(P : HProc)(xs : list ProcVar)(f : ProcVar -> Expr)
  | Abisim(P Q : HProc)
  | Aterm(P : HProc)
with
  PointsToType := PTTstd | PTTproc | PTTact.

Add Search Blacklist "Assn_rect".
Add Search Blacklist "Assn_ind".
Add Search Blacklist "Assn_rec".
Add Search Blacklist "Assn_sind".
Add Search Blacklist "PointsToType_rect".
Add Search Blacklist "PointsToType_ind".
Add Search Blacklist "PointsToType_rec".
Add Search Blacklist "PointsToType_sind".

Below is a helper tactic for doing induction on the structure of assertions.

Ltac assn_induction A :=
  induction A as [
    
    B|
    
    A IH|
    
    A1 IH1 A2 IH2|
    
    A1 IH1 A2 IH2|
    
    A1 IH1 A2 IH2|
    
    t q E1 E2|
    
    x q P xs f|
    
    P Q|
    
    P
  ].

Some sugar.

Definition Atrue : Assn := Aplain (Bconst true).
Definition Afalse : Assn := Aplain (Bconst false).

Definition Apointsto_procact (q : Qc)(E1 E2 : Expr) : Assn :=
  if Qc_eq_dec q 1
  then Apointsto PTTact q E1 E2
  else Apointsto PTTproc q E1 E2.

Iterated separating conjunction

The iterated separating conjunction is derived from the syntax.

Fixpoint Aiter (xs : list Assn) : Assn :=
  match xs with
    | nil => Atrue
    | A :: xs' => Astar A (Aiter xs')
  end.

Two helper definitions for iterated separating conjunctions over points-to ownership predicates:

Definition ApointstoIter {T} (xs : list T)(F : T -> Qc)(f1 f2 : T -> Expr)(t : PointsToType) : list Assn :=
  map (fun x : T => Apointsto t (F x) (f1 x) (f2 x)) xs.

Definition ApointstoIter_procact {T} (xs : list T)(F : T -> Qc)(f1 f2 : T -> Expr) : list Assn :=
  map (fun x : T => Apointsto_procact (F x) (f1 x) (f2 x)) xs.

Below are several properties of iterated separating conjunctions.

Lemma ApointstoIter_cons {T} :
  forall (xs : list T)(x : T) F f1 f2 t,
  ApointstoIter (x :: xs) F f1 f2 t =
  Apointsto t (F x) (f1 x) (f2 x) :: ApointstoIter xs F f1 f2 t.

Lemma ApointstoIter_app {T} :
  forall (xs ys : list T)(fq : T -> Qc)(f1 f2 : T -> Expr)(t : PointsToType),
  ApointstoIter xs fq f1 f2 t ++ ApointstoIter ys fq f1 f2 t =
  ApointstoIter (xs ++ ys) fq f1 f2 t.

Lemma ApointstoIter_procact_app {T} :
  forall (xs ys : list T)(fq : T -> Qc)(f1 f2 : T -> Expr),
  ApointstoIter_procact xs fq f1 f2 ++ ApointstoIter_procact ys fq f1 f2 =
  ApointstoIter_procact (xs ++ ys) fq f1 f2.

Lemma ApointstoIter_ext_in {T} :
  forall (xs : list T)(fq fq' : T -> Qc)(f1 f1' f2 f2' : T -> Expr) t,
    (forall x : T, In x xs -> fq x = fq' x) ->
    (forall x : T, In x xs -> f1 x = f1' x) ->
    (forall x : T, In x xs -> f2 x = f2' x) ->
  ApointstoIter xs fq f1 f2 t = ApointstoIter xs fq' f1' f2' t.

Lemma ApointstoIter_procact_ext_in {T} :
  forall (xs : list T)(fq fq' : T -> Qc)(f1 f1' f2 f2' : T -> Expr),
    (forall x : T, In x xs -> fq x = fq' x) ->
    (forall x : T, In x xs -> f1 x = f1' x) ->
    (forall x : T, In x xs -> f2 x = f2' x) ->
  ApointstoIter_procact xs fq f1 f2 = ApointstoIter_procact xs fq' f1' f2'.

Free variables

The predicate assn_fv A x determines whether the program variable x occurs freely in A. The definition of assn_fv is as expected.

Fixpoint assn_fv (A : Assn)(x : Var) : Prop :=
  match A with
    | Aplain B => In x (cond_fv B)
    | Aex A => exists v, assn_fv (A v) x
    | Adisj A1 A2
    | Astar A1 A2
    | Awand A1 A2 => assn_fv A1 x \/ assn_fv A2 x
    | Apointsto _ _ E1 E2 => In x (expr_fv E1) \/ In x (expr_fv E2)
    | Aproc y _ P _ f => x = y \/ hproc_fv P x \/ expr_map_fv f x
    | Abisim P Q => hproc_fv P x \/ hproc_fv Q x
    | Aterm P => hproc_fv P x
  end.

Several useful properties related to free variables:

Lemma assn_fv_iter :
  forall xs x,
  assn_fv (Aiter xs) x <-> exists A, In A xs /\ assn_fv A x.

Lemma assn_fv_ApointstoIter {T} :
  forall (xs : list T) F f1 f2 t x,
  assn_fv (Aiter (ApointstoIter xs F f1 f2 t)) x <->
  exists e : T, In e xs /\ (In x (expr_fv (f1 e)) \/ In x (expr_fv (f2 e))).

Substitution

The operation assn_subst x E A substitutes every occurence of the program variable x by E in the assertion A. The definition of assn_subst is as expected.

Fixpoint assn_subst (x : Var)(E : Expr)(A : Assn) : Assn :=
  match A with
    | Aplain B => Aplain (cond_subst x E B)
    | Aex A => Aex (fun v => assn_subst x E (A v))
    | Adisj A1 A2 => Adisj (assn_subst x E A1) (assn_subst x E A2)
    | Astar A1 A2 => Astar (assn_subst x E A1) (assn_subst x E A2)
    | Awand A1 A2 => Awand (assn_subst x E A1) (assn_subst x E A2)
    | Apointsto t q E1 E2 => Apointsto t q (expr_subst x E E1) (expr_subst x E E2)
    | Aproc y q P xs f => Aproc y q (hproc_subst x E P) xs (expr_subst_map x E f)
    | Abisim P Q => Abisim (hproc_subst x E P) (hproc_subst x E Q)
    | Aterm P => Aterm (hproc_subst x E P)
  end.

Existential quantification as is written in the paper (with a variable instead of a mapping) can be defined using the definition of substitution.

Definition Aexists (x : Var)(A : Assn) : Assn :=
  Aex (fun v => assn_subst x (Econst v) A).

The substitution of any variable not occuring in the targetted assertion does not change the assertion.

Lemma assn_subst_pres :
  forall A x E, ~ assn_fv A x -> assn_subst x E A = A.

Dynamics

The following satisfaction relation, sat, defines the semantic meaning of assertions.

Fixpoint sat (ph : PermHeap)(pm : ProcMap)(s g : Store)(A : Assn) : Prop :=
  match A with
    
    | Aplain B => cond_eval B s = true
    
    | Aex A => exists v, sat ph pm s g (A v)
    
    | Adisj A1 A2 =>
        sat ph pm s g A1 \/ sat ph pm s g A2
    
    | Astar A1 A2 =>
        exists ph1 ph2,
          phDisj ph1 ph2 /\
          phUnion ph1 ph2 = ph /\
        exists pm1 pm2,
          pmDisj pm1 pm2 /\
          pmBisim (pmUnion pm1 pm2) pm /\
          sat ph1 pm1 s g A1 /\
          sat ph2 pm2 s g A2
    
    | Awand A1 A2 =>
        forall ph' pm',
        phDisj ph ph' ->
        pmDisj pm pm' ->
        sat ph' pm' s g A1 ->
        sat (phUnion ph ph') (pmUnion pm pm') s g A2
    
    | Apointsto PTTstd q E1 E2 =>
        let l := expr_eval E1 s in
        let v := expr_eval E2 s in
        perm_valid q /\ phcLe (PHCstd q v) (ph l)
    
    | Apointsto PTTproc q E1 E2 =>
        let l := expr_eval E1 s in
        let v := expr_eval E2 s in
        perm_valid q /\ phcLe (PHCproc q v) (ph l)
    
    | Apointsto PTTact q E1 E2 =>
        let l := expr_eval E1 s in
        let v := expr_eval E2 s in
        perm_valid q /\ exists v', phcLe (PHCact q v v') (ph l)
    
    | Aproc x q HP xs f =>
        let P := pDehybridise HP s in
        let F := expr_eval_map f s in
        let c := PEelem q P xs F in
        exists c',
          pmeDisj c c' /\
          pmeBisim (pm (g x)) (pmeUnion c c')
    
    | Abisim P Q =>
        bisim (pDehybridise P s) (pDehybridise Q s)
    
    | Aterm P => pterm (pDehybridise P s)
  end.

Process maps can always be replaced by bisimilar ones (and therefore also by equal ones, since process map equality is a subrelation of bisimilarity).

Lemma sat_procmap_bisim :
  forall A ph pm1 pm2 s g,
  pmBisim pm1 pm2 -> sat ph pm1 s g A -> sat ph pm2 s g A.
Add Parametric Morphism : sat
  with signature eq ==> pmBisim ==> eq ==> eq ==> eq ==> iff
    as sat_bisim_mor.

The following lemma relates substitution in assertions with the satisfiability of that assertion.

Lemma sat_subst :
  forall A ph pm s g x E,
  sat ph pm s g (assn_subst x E A) <->
  sat ph pm (sUpdate s x (expr_eval E s)) g A.

The satisfiability of any assertion A only depends on the variables occuring freely in A.

Lemma sat_agree :
  forall A ph pm s1 s2 g,
  sAgree (assn_fv A) s1 s2 -> sat ph pm s1 g A <-> sat ph pm s2 g A.
Lemma sat_agree_ghost :
  forall A ph pm s g1 g2,
  sAgree (assn_fv A) g1 g2 -> sat ph pm s g1 A <-> sat ph pm s g2 A.

Satisfiability of any assertion A is insensitive to updating variables not occuring freely in A.

Lemma sat_update :
  forall A ph pm s g x v,
  ~ assn_fv A x -> sat ph pm (sUpdate s x v) g A <-> sat ph pm s g A.
Lemma sat_update_ghost :
  forall A ph pm s g x v,
  ~ assn_fv A x -> sat ph pm s (sUpdate g x v) A <-> sat ph pm s g A.

Satisfiability of assertions is monotonic with respect to permission heaps and process maps.

Lemma sat_weaken :
  forall A ph1 ph2 pm1 pm2 s g,
  phDisj ph1 ph2 ->
  pmDisj pm1 pm2 ->
  sat ph1 pm1 s g A ->
  sat (phUnion ph1 ph2) (pmUnion pm1 pm2) s g A.

The satisfiability of iterated separating conjunctions is insensitive to permutations.

Lemma sat_iter_permut :
  forall xs ys,
  Permutation xs ys ->
  forall ph pm s g,
  sat ph pm s g (Aiter xs) ->
  sat ph pm s g (Aiter ys).

The satisfiability of points-to predicates is independent of the process map.

Lemma sat_pointsto_indep :
  forall ph pm1 pm2 s g t q E1 E2,
  sat ph pm1 s g (Apointsto t q E1 E2) ->
  sat ph pm2 s g (Apointsto t q E1 E2).

Logical consequence

The relation entails defines semantic consequence of two assertions. That is, A is a logical consequence of A' if there is no model that distinguishes A from A'.
Logical equivalence aEquiv of any two assertions is defined to be a logical entailment in both directions.

Definition aEntails (A1 A2 : Assn) : Prop :=
  forall ph pm s g,
    phValid ph -> pmValid pm -> sat ph pm s g A1 -> sat ph pm s g A2.
Definition aEntails_rev (A1 A2 : Assn) : Prop :=
  aEntails A2 A1.
Definition aEquiv (A1 A2 : Assn) : Prop :=
  aEntails A1 A2 /\ aEntails A2 A1.

Notation "A1 ⊢ A2":=(aEntails A1 A2) (only printing, at level 80).
Notation "A1 ⊣ A2":=(aEntails_rev A1 A2) (only printing, at level 80).
Notation "A1 ⊣⊢ A2":=(aEquiv A1 A2) (only printing, at level 80).

Lemma aEntails_flip :
  forall A1 A2, aEntails A1 A2 <-> aEntails_rev A2 A1.

Logical consequence is a consequence relation.

Instance aEntails_refl : Reflexive aEntails.
Instance aEntails_trans : Transitive aEntails.
Instance aEntails_preorder : PreOrder aEntails.

Instance aEntails_rev_refl : Reflexive aEntails_rev.
Instance aEntails_rev_trans : Transitive aEntails_rev.
Instance aEntails_rev_preorder : PreOrder aEntails_rev.

Hint Resolve aEntails_refl aEntails_rev_refl : core.

Logical equivalence is an equivalence relation.

Instance aEquiv_refl : Reflexive aEquiv.
Instance aEquiv_symm : Symmetric aEquiv.
Instance aEquiv_trans : Transitive aEquiv.
Instance aEquiv_eq : Equivalence aEquiv.

Hint Resolve aEquiv_refl : core.

Logical equivalence is a subrelation of entailment.

Instance aEntails_subrel : subrelation aEquiv aEntails.
Instance aEntails_rev_subrel : subrelation aEquiv aEntails_rev.

Logical consequence is a congruence for all connectives of the program logic.

Add Parametric Morphism : Adisj
  with signature aEntails ==> aEntails ==> aEntails
    as Adisj_entails_mor.
Add Parametric Morphism : Astar
  with signature aEntails ==> aEntails ==> aEntails
    as Astar_entails_mor.
Add Parametric Morphism : Awand
  with signature aEntails_rev ==> aEntails ==> aEntails
    as Awand_entails_mor.

Add Parametric Morphism : Adisj
  with signature aEquiv ==> aEquiv ==> aEquiv
    as Adisj_equiv_mor.
Add Parametric Morphism : Astar
  with signature aEquiv ==> aEquiv ==> aEquiv
    as Astar_equiv_mor.
Add Parametric Morphism : Awand
  with signature aEquiv ==> aEquiv ==> aEquiv
    as Awand_equiv_mor.

Weakening rule


Lemma sat_star_combine :
  forall ph1 ph2 pm1 pm2 s g A1 A2,
  phDisj ph1 ph2 ->
  pmDisj pm1 pm2 ->
  sat ph1 pm1 s g A1 ->
  sat ph2 pm2 s g A2 ->
  sat (phUnion ph1 ph2) (pmUnion pm1 pm2) s g (Astar A1 A2).

Lemma sat_star_weaken :
  forall ph pm s g A1 A2,
  sat ph pm s g (Astar A1 A2) ->
  sat ph pm s g A1.

The following rule shows that our separation logic is intuitionistic.

Theorem assn_weaken :
  forall A1 A2, aEntails (Astar A1 A2) A1.

Separating conjunction

Soundness of the axioms of associativity and commutativity.

Lemma sat_star_assoc_l :
  forall ph pm s g A1 A2 A3,
  sat ph pm s g (Astar A1 (Astar A2 A3)) ->
  sat ph pm s g (Astar (Astar A1 A2) A3).
Theorem Astar_assoc_l :
  forall A1 A2 A3,
  aEntails (Astar A1 (Astar A2 A3)) (Astar (Astar A1 A2) A3).
Lemma sat_star_assoc_r :
  forall ph pm s g A1 A2 A3,
  sat ph pm s g (Astar (Astar A1 A2) A3) ->
  sat ph pm s g (Astar A1 (Astar A2 A3)).
Theorem Astar_assoc_r :
  forall A1 A2 A3,
  aEntails (Astar (Astar A1 A2) A3) (Astar A1 (Astar A2 A3)).
Theorem Astar_assoc :
  forall A1 A2 A3,
  aEquiv (Astar (Astar A1 A2) A3) (Astar A1 (Astar A2 A3)).

Lemma sat_star_comm :
  forall ph pm s g A1 A2,
  sat ph pm s g (Astar A1 A2) ->
  sat ph pm s g (Astar A2 A1).
Theorem Astar_comm :
  forall A1 A2, aEntails (Astar A1 A2) (Astar A2 A1).
Theorem Astar_comm_equiv :
  forall A1 A2, aEquiv (Astar A1 A2) (Astar A2 A1).

One can always forget about resources.

Corollary assn_weaken_r :
  forall A1 A2, aEntails (Astar A1 A2) A2.
Corollary assn_weaken_l :
  forall A1 A2, aEntails (Astar A1 A2) A1.

One can always introduce a Atrue.

Lemma sat_star_true :
  forall ph pm s g A,
  phValid ph -> pmValid pm ->
  sat ph pm s g A -> sat ph pm s g (Astar A Atrue).
Theorem Astar_true :
  forall A, aEntails A (Astar A Atrue).

The following properties allow "swapping" separate resources.

Lemma sat_star_swap_l :
  forall ph pm s g A1 A2 A3,
  sat ph pm s g (Astar A1 (Astar A2 A3)) ->
  sat ph pm s g (Astar A2 (Astar A1 A3)).
Lemma Astar_swap_l :
  forall A1 A2 A3,
  aEntails (Astar A1 (Astar A2 A3)) (Astar A2 (Astar A1 A3)).
Lemma sat_star_swap_r :
  forall ph pm s g A1 A2 A3,
  sat ph pm s g (Astar (Astar A1 A2) A3) ->
  sat ph pm s g (Astar (Astar A1 A3) A2).
Lemma Astar_swap_r :
  forall A1 A2 A3,
  aEntails (Astar (Astar A1 A2) A3) (Astar (Astar A1 A3) A2).

A property that combines logical entailment with separating conjunction.

Corollary Astar_add_l :
  forall A1 A2 A3,
  aEntails A2 A3 -> aEntails (Astar A1 A2) (Astar A1 A3).
Corollary Astar_add_r :
  forall A1 A2 A3,
  aEntails A2 A3 -> aEntails (Astar A2 A1) (Astar A3 A1).

Separating conjunction distributes over disjunction.

Lemma Astar_disj_l :
  forall A1 A2 A3,
  aEntails (Astar A1 (Adisj A2 A3)) (Adisj (Astar A1 A2) (Astar A1 A3)).
Lemma Astar_disj_r :
  forall A1 A2 A3,
  aEntails (Adisj (Astar A1 A2) (Astar A1 A3)) (Astar A1 (Adisj A2 A3)).
Lemma Astar_disj :
  forall A1 A2 A3,
  aEquiv (Astar A1 (Adisj A2 A3)) (Adisj (Astar A1 A2) (Astar A1 A3)).

Iterated separating conjunction

The following properties cover entailment rules with iterated separating conjunctions.
First, iterated separating conjunctions are insensitive to permutation.

Theorem Aiter_permut :
  forall xs ys, Permutation xs ys -> aEntails (Aiter xs) (Aiter ys).
Add Parametric Morphism : Aiter
  with signature @Permutation Assn ==> aEntails
    as Aiter_permut_mor.

Iterated separating conjunction allows "pulling out" the head resource (or unfolding once).

Lemma sat_iter_cons_l :
  forall ph pm s g A xs,
  sat ph pm s g (Astar A (Aiter xs)) ->
  sat ph pm s g (Aiter (A :: xs)).
Theorem Aiter_cons_l :
  forall A xs, aEntails (Astar A (Aiter xs)) (Aiter (A :: xs)).
Lemma sat_iter_cons_r :
  forall ph pm s g A xs,
  sat ph pm s g (Aiter (A :: xs)) ->
  sat ph pm s g (Astar A (Aiter xs)).
Theorem Aiter_cons_r :
  forall A xs, aEntails (Aiter (A :: xs)) (Astar A (Aiter xs)).

Two iterated separating conjunctions can be combined into a single one.

Lemma sat_iter_add_l :
  forall (xs ys : list Assn) ph pm s g,
  sat ph pm s g (Astar (Aiter xs) (Aiter ys)) ->
  sat ph pm s g (Aiter (xs ++ ys)).
Theorem Aiter_add_l :
  forall xs ys,
  aEntails (Astar (Aiter xs) (Aiter ys)) (Aiter (xs ++ ys)).
Lemma sat_iter_add_r :
  forall (xs ys : list Assn) ph pm s g,
  phValid ph -> pmValid pm ->
  sat ph pm s g (Aiter (xs ++ ys)) ->
  sat ph pm s g (Astar (Aiter xs) (Aiter ys)).
Theorem Aiter_add_r :
  forall xs ys,
  aEntails (Aiter (xs ++ ys)) (Astar (Aiter xs) (Aiter ys)).

Binary separating conjunctions that occur inside iterated separating conjuncations can always be eliminated (and also introduced).

Lemma sat_iter_star_l :
  forall ph pm s g A1 A2 (xs : list Assn),
  sat ph pm s g (Aiter (Astar A1 A2 :: xs)) ->
  sat ph pm s g (Aiter (A1 :: A2 :: xs)).
Theorem Aiter_star_l :
  forall A1 A2 xs,
  aEntails (Aiter (Astar A1 A2 :: xs)) (Aiter (A1 :: A2 :: xs)).
Lemma sat_iter_star_r :
  forall ph pm s g A1 A2 (xs : list Assn),
  sat ph pm s g (Aiter (A1 :: A2 :: xs)) ->
  sat ph pm s g (Aiter (Astar A1 A2 :: xs)).
Theorem Aiter_star_r :
  forall A1 A2 xs,
  aEntails (Aiter (A1 :: A2 :: xs)) (Aiter (Astar A1 A2 :: xs)).

Iterated resources can always be forgotten.

Lemma sat_iter_weaken :
  forall ph pm s g A (xs : list Assn),
  sat ph pm s g (Aiter (A :: xs)) ->
  sat ph pm s g (Aiter xs).
Corollary Aiter_weaken :
  forall A xs,
  aEntails (Aiter (A :: xs)) (Aiter xs).

Iterated heap ownership assertions (i.e., ApointstoIter and ApointstoIter_procact) are insensitive to permutations, likewise to ordinary iterated separating conjunctions.
Note, some helper lemmas are needed in order to prove this.

Lemma sat_iter_In_l {T} (eq_dec : forall x y : T, { x = y } + { x <> y }) :
  forall (xs : list T) ph pm s g (f : T -> Assn)(x : T),
  In x xs ->
  sat ph pm s g (Aiter (map f xs)) ->
  sat ph pm s g (Astar (f x) (Aiter (map f (removeFirst eq_dec x xs)))).

Lemma Aiter_In_l {T} (eq_dec : forall x y : T, { x = y } + { x <> y }) :
  forall (xs : list T)(f : T -> Assn)(x : T),
  In x xs ->
  aEntails (Aiter (map f xs)) (Astar (f x) (Aiter (map f (removeFirst eq_dec x xs)))).

Lemma sat_iter_In_r {T} (eq_dec : forall x y : T, { x = y } + { x <> y }) :
  forall (xs : list T) ph pm s g (f : T -> Assn)(x : T),
  In x xs ->
  sat ph pm s g (Astar (f x) (Aiter (map f (removeFirst eq_dec x xs)))) ->
  sat ph pm s g (Aiter (map f xs)).

Lemma Aiter_In_r {T} (eq_dec : forall x y : T, { x = y } + { x <> y }) :
  forall (xs : list T)(f : T -> Assn)(x : T),
  In x xs ->
  aEntails (Astar (f x) (Aiter (map f (removeFirst eq_dec x xs)))) (Aiter (map f xs)).

Lemma sat_ApointstoIter_permut {T} :
  forall (xs ys : list T) ph pm s g (fq : T -> Qc)(f1 f2 : T -> Expr) t,
  Permutation xs ys ->
  sat ph pm s g (Aiter (ApointstoIter xs fq f1 f2 t)) ->
  sat ph pm s g (Aiter (ApointstoIter ys fq f1 f2 t)).

Lemma sat_procact_iter_permut {T} :
  forall (xs ys : list T) ph pm s g (fq : T -> Qc)(f1 f2 : T -> Expr),
  Permutation xs ys ->
  sat ph pm s g (Aiter (ApointstoIter_procact xs fq f1 f2)) ->
  sat ph pm s g (Aiter (ApointstoIter_procact ys fq f1 f2)).

Plain assertions

Introduction and elimination rules for plain assertions.

Theorem Atrue_intro :
  forall A, aEntails A Atrue.

Theorem Afalse_elim :
  forall A1 A2, aEntails A1 Afalse -> aEntails A1 A2.

Lemma assn_plain_tauto :
  forall E,
  aEntails (Aplain (Beq E E)) Atrue /\
  aEntails Atrue (Aplain (Beq E E)).

Lemma Aplain_equiv :
  forall B1 B2,
  aEquiv (Aplain B1) (Aplain B2) <->
  forall s, cond_eval B1 s = cond_eval B2 s.

Existential quantifiers

Introduction rule for existential quantification.

Theorem Aexists_intro :
  forall A1 A2 x v,
  aEntails A1 (assn_subst x (Econst v) A2) ->
  aEntails A1 (Aexists x A2).

Disjunction

Standard elimination rules for disjunction.

Lemma sat_elim_l :
  forall ph pm s g A1 A2,
  sat ph pm s g A1 ->
  sat ph pm s g (Adisj A1 A2).
Lemma sat_elim_r :
  forall ph pm s g A1 A2,
  sat ph pm s g A2 ->
  sat ph pm s g (Adisj A1 A2).

Theorem Adisj_elim_l :
  forall A A1 A2,
  aEntails A A1 ->
  aEntails A (Adisj A1 A2).
Theorem Adisj_elim_r :
  forall A A1 A2,
  aEntails A A2 ->
  aEntails A (Adisj A1 A2).

Disjunction is idempotent.

Lemma Adisj_idemp :
  forall A,
  aEntails A (Adisj A A) /\ aEntails (Adisj A A) A.

Magic wand

Introduction and elimination rules for magic wands.

Theorem Awand_intro :
  forall A1 A2 A3,
  aEntails (Astar A1 A2) A3 -> aEntails A1 (Awand A2 A3).

Theorem Awand_elim :
  forall A1 A2 A A',
  aEntails A1 (Awand A A') ->
  aEntails A2 A ->
  aEntails (Astar A1 A2) A'.

Heap ownership predicates

The following rules cover points-to assertions.
Heap ownership predicates with invalid fractional permissions are meaningless.

Theorem Apointsto_valid :
  forall t q E1 E2,
  ~ perm_valid q -> aEntails (Apointsto t q E1 E2) Afalse.

Lemma Apointsto_entire :
  forall ph pm s g t E1 E2,
  phValid ph ->
  sat ph pm s g (Apointsto t 1 E1 E2) ->
  phcEntire (ph (expr_eval E1 s)).

Lemma ApointstoIter_perm_full {T} :
  forall (xs : list T)(fq : T -> Qc)(f1 f2 : T -> Expr)(l : Val) ph pm s g t,
    (forall x : T, In x xs -> fq x = 1) ->
  sat ph pm s g (Aiter (ApointstoIter xs fq f1 f2 t)) ->
  In l (map (expr_eval_map f1 s) xs) ->
  phcEntire (ph l).

Heap ownership predicates of different types cannot coexist if they target the same heap location.

Lemma Apointsto_diff :
  forall q1 q2 E1 E2 t1 t2,
  t1 <> t2 ->
  aEntails (Astar (Apointsto t1 q1 E1 E2) (Apointsto t2 q2 E1 E2)) Afalse.

Heap ownership predicates may be split.

Lemma Apointsto_split_std :
  forall q1 q2 E1 E2,
  perm_disj q1 q2 ->
  aEntails
    (Apointsto PTTstd (q1 + q2) E1 E2)
    (Astar (Apointsto PTTstd q1 E1 E2) (Apointsto PTTstd q2 E1 E2)).

Lemma Apointsto_split_proc :
  forall q1 q2 E1 E2,
  perm_disj q1 q2 ->
  aEntails
    (Apointsto PTTproc (q1 + q2) E1 E2)
    (Astar (Apointsto PTTproc q1 E1 E2) (Apointsto PTTproc q2 E1 E2)).

Lemma Apointsto_split_act :
  forall q1 q2 E1 E2,
  perm_disj q1 q2 ->
  aEntails
    (Apointsto PTTact (q1 + q2) E1 E2)
    (Astar (Apointsto PTTact q1 E1 E2) (Apointsto PTTact q2 E1 E2)).

Theorem Apointsto_split :
  forall q1 q2 E1 E2 t,
  perm_disj q1 q2 ->
  aEntails
    (Apointsto t (q1 + q2) E1 E2)
    (Astar (Apointsto t q1 E1 E2) (Apointsto t q2 E1 E2)).

Heap ownership predicates may be merged.

Lemma Apointsto_merge_std :
  forall q1 q2 E1 E2,
  perm_disj q1 q2 ->
  aEntails
    (Astar (Apointsto PTTstd q1 E1 E2) (Apointsto PTTstd q2 E1 E2))
    (Apointsto PTTstd (q1 + q2) E1 E2).

Lemma Apointsto_merge_proc :
  forall q1 q2 E1 E2,
  perm_disj q1 q2 ->
  aEntails
    (Astar (Apointsto PTTproc q1 E1 E2) (Apointsto PTTproc q2 E1 E2))
    (Apointsto PTTproc (q1 + q2) E1 E2).

Lemma Apointsto_merge_act :
  forall q1 q2 E1 E2,
  perm_disj q1 q2 ->
  aEntails
    (Astar (Apointsto PTTact q1 E1 E2) (Apointsto PTTact q2 E1 E2))
    (Apointsto PTTact (q1 + q2) E1 E2).

Theorem Apointsto_merge :
  forall q1 q2 E1 E2 t,
  perm_disj q1 q2 ->
  aEntails
    (Astar (Apointsto t q1 E1 E2) (Apointsto t q2 E1 E2))
    (Apointsto t (q1 + q2) E1 E2).

Below are the rules for 'process-action' ownership predicates, which allow using such predicates as abbreviations for process- and action ownership predicates

Lemma assn_proc_procact_l :
  forall q E1 E2,
  q <> 1 ->
  aEntails (Apointsto_procact q E1 E2) (Apointsto PTTproc q E1 E2).
Lemma assn_proc_procact_r :
  forall q E1 E2,
  q <> 1 ->
  aEntails (Apointsto PTTproc q E1 E2) (Apointsto_procact q E1 E2).
Lemma assn_act_procact_l :
  forall E1 E2,
  aEntails (Apointsto_procact 1 E1 E2) (Apointsto PTTact 1 E1 E2).
Lemma assn_act_procact_r :
  forall E1 E2,
  aEntails (Apointsto PTTact 1 E1 E2) (Apointsto_procact 1 E1 E2).

Lemma Aiter_proc_procact_l {T} :
  forall (xs : list T)(f1 f2 : T -> Expr)(fq : T -> Qc),
    (forall x : T, In x xs -> fq x <> 1) ->
  aEntails (Aiter (ApointstoIter_procact xs fq f1 f2)) (Aiter (ApointstoIter xs fq f1 f2 PTTproc)).
Lemma Aiter_proc_procact_r {T} :
  forall (xs : list T)(f1 f2 : T -> Expr)(fq : T -> Qc),
    (forall x : T, In x xs -> fq x <> 1) ->
  aEntails (Aiter (ApointstoIter xs fq f1 f2 PTTproc)) (Aiter (ApointstoIter_procact xs fq f1 f2)).
Lemma Aiter_act_procact_l {T} :
  forall (xs : list T)(f1 f2 : T -> Expr)(fq : T -> Qc),
    (forall x : T, In x xs -> fq x = 1) ->
  aEntails (Aiter (ApointstoIter_procact xs fq f1 f2)) (Aiter (ApointstoIter xs fq f1 f2 PTTact)).
Lemma Aiter_act_procact_r {T} :
  forall (xs : list T)(f1 f2 : T -> Expr)(fq : T -> Qc),
    (forall x : T, In x xs -> fq x = 1) ->
  aEntails (Aiter (ApointstoIter xs fq f1 f2 PTTact)) (Aiter (ApointstoIter_procact xs fq f1 f2)).

Theorem ApointstoIter_procact_split {T} :
  forall (xs ys : list T)(f1 f2 : T -> Expr)(fq : T -> Qc),
    (forall x : T, In x xs -> fq x <> 1) ->
    (forall x : T, In x ys -> fq x = 1) ->
  aEntails
    (Aiter (ApointstoIter_procact (xs ++ ys) fq f1 f2))
    (Astar (Aiter (ApointstoIter xs fq f1 f2 PTTproc)) (Aiter (ApointstoIter ys fq f1 f2 PTTact))).

Theorem ApointstoIter_procact_merge {T} :
  forall (xs ys : list T)(f1 f2 : T -> Expr)(fq : T -> Qc),
    (forall x : T, In x xs -> fq x <> 1) ->
    (forall x : T, In x ys -> fq x = 1) ->
  aEntails
    (Astar (Aiter (ApointstoIter xs fq f1 f2 PTTproc)) (Aiter (ApointstoIter ys fq f1 f2 PTTact)))
    (Aiter (ApointstoIter_procact (xs ++ ys) fq f1 f2)).

Corollary ApointstoIter_procact_partition {T} :
  forall (xs ys1 ys2 : list T)(f1 f2 : T -> Expr)(fq : T -> Qc),
  let f := fun x : T => if Qc_eq_dec (fq x) 1 then false else true in
  partition f xs = (ys1, ys2) ->
  aEntails
    (Aiter (ApointstoIter_procact xs fq f1 f2))
    (Astar (Aiter (ApointstoIter ys1 fq f1 f2 PTTproc)) (Aiter (ApointstoIter ys2 fq f1 f2 PTTact))).

Process ownership predicates

Process ownership predicates with invalid fractional permissions are meaningless.

Theorem assn_proc_valid :
  forall x q P xs f,
  ~ perm_valid q -> aEntails (Aproc x q P xs f) Afalse.

Processes may always be replaced by bisimilar ones.

Theorem assn_proc :
  forall P1 P2 x q xs f,
  hbisim P1 P2 ->
  aEntails (Aproc x q P1 xs f) (Aproc x q P2 xs f).

Processes ownership may always be split.

Theorem assn_proc_split :
  forall q1 q2 x P1 P2 xs f,
  perm_disj q1 q2 ->
  aEntails
    (Aproc x (q1 + q2) (HPpar P1 P2) xs f)
    (Astar (Aproc x q1 P1 xs f) (Aproc x q2 P2 xs f)).

Processes ownership may always be merged.

Theorem assn_proc_merge :
  forall q1 q2 x P1 P2 xs f,
  perm_disj q1 q2 ->
  aEntails
    (Astar (Aproc x q1 P1 xs f) (Aproc x q2 P2 xs f))
    (Aproc x (q1 + q2) (HPpar P1 P2) xs f).

One can always dispose of parts of an abstraction.

Theorem assn_proc_weaken :
  forall q1 q2 x P1 P2 xs f,
  perm_disj q1 q2 ->
  aEntails
    (Aproc x (q1 + q2) (HPpar P1 P2) xs f)
    (Aproc x q1 P1 xs f).

Bisimilarity

Any bisimilarity from hbisim can be introduced via Abisim.

Theorem aBisim_hbisim :
  forall P Q, hbisim P Q -> aEntails Atrue (Abisim P Q).

Bisimilarity is an equivalence relation with respect to separating conjunction and entailment.

Theorem aBisim_refl :
  forall P, aEntails Atrue (Abisim P P).
Theorem aBisim_symm :
  forall P Q, aEntails (Abisim P Q) (Abisim Q P).
Theorem aBisim_trans :
  forall P Q R, aEntails (Astar (Abisim P Q) (Abisim Q R)) (Abisim P R).

Bisimilarity is a congruence for all connectives.

Theorem aBisim_seq :
  forall P1 P2 Q1 Q2,
  aEntails (Astar (Abisim P1 P2) (Abisim Q1 Q2)) (Abisim (HPseq P1 Q1) (HPseq P2 Q2)).

Theorem aBisim_alt :
  forall P1 P2 Q1 Q2,
  aEntails (Astar (Abisim P1 P2) (Abisim Q1 Q2)) (Abisim (HPalt P1 Q1) (HPalt P2 Q2)).

Theorem aBisim_par :
  forall P1 P2 Q1 Q2,
  aEntails (Astar (Abisim P1 P2) (Abisim Q1 Q2)) (Abisim (HPpar P1 Q1) (HPpar P2 Q2)).

Theorem aBisim_lmerge :
  forall P1 P2 Q1 Q2,
  aEntails (Astar (Abisim P1 P2) (Abisim Q1 Q2)) (Abisim (HPlmerge P1 Q1) (HPlmerge P2 Q2)).

Theorem aBisim_sum :
  forall P Q x,
  ~ hproc_fv P x ->
  ~ hproc_fv Q x ->
  aEntails (Abisim P Q) (Abisim (HPsigma x P) (HPsigma x Q)).

Corollary aBisim_sum_alt :
  forall x E P,
  aEntails Atrue (Abisim (HPsigma x P) (HPalt (hproc_subst x E P) (HPsigma x P))).

Theorem aBisim_cond :
  forall P Q B1 B2,
  aEquiv (Aplain B1) (Aplain B2) ->
  aEntails (Abisim P Q) (Abisim (HPcond B1 P) (HPcond B2 Q)).

Theorem aBisim_cond_true :
  forall B1 B2 P,
  aEntails (Aplain B1) (Aplain B2) ->
  aEntails (Aplain B1) (Abisim (HPcond B2 P) P).

Theorem aBisim_cond_false :
  forall B1 B2 P,
  aEntails (Aplain B1) (Aplain B2) ->
  aEntails (Aplain B1) (Abisim (HPcond (Bnot B2) P) HPdelta).

Theorem aBisim_iter :
  forall P Q,
  aEntails (Abisim P Q) (Abisim (HPiter P) (HPiter Q)).

Theorem aBisim_term :
  forall P, aEntails (Aterm P) (Abisim P (HPalt P HPepsilon)).

Bisimilarity assertions are duplicable.

Theorem aBisim_dupl :
  forall P Q,
  aEntails (Abisim P Q) (Astar (Abisim P Q) (Abisim P Q)).

Termination

Termination according to pterm can be lifted to Aterm.

Theorem aTerm_intro :
  forall P, pterm P -> aEntails Atrue (Aterm (pHybridise P)).

Terminating processes can always be replaced by bisimilar ones.

Theorem aTerm_bisim :
  forall P Q,
  aEntails (Astar (Aterm P) (Abisim P Q)) (Aterm Q).

Termination assertions are duplicable.

Theorem aTerm_dupl :
  forall P, aEntails (Aterm P) (Astar (Aterm P) (Aterm P)).

Iterated points-to predicates

The properties below are for iterated heap ownership assertions.
First, the evaluation of heap ownership assertions in independent of any process maps:

Lemma sat_ApointstoIter_indep {T} :
  forall (xs : list T)(fq : T -> Qc)(f1 f2 : T -> Expr) ph pm1 pm2 s g t,
  pmValid pm2 ->
  sat ph pm1 s g (Aiter (ApointstoIter xs fq f1 f2 t)) ->
  sat ph pm2 s g (Aiter (ApointstoIter xs fq f1 f2 t)).

The satisfiability of iterated points-to predicates implies the satisfiability of a single points-to predicate.

Lemma ApointstoIter_sat_single_std {T} :
  forall (xs : list T)(x : T) ph pm s g F f1 f2,
  In x xs ->
  sat ph pm s g (Aiter (ApointstoIter xs F f1 f2 PTTstd)) ->
  let q := F x in
  let l := expr_eval (f1 x) s in
  let v := expr_eval (f2 x) s in
  phcLe (PHCstd q v) (ph l).
Lemma ApointstoIter_sat_single_proc {T} :
  forall (xs : list T)(x : T) ph pm s g F f1 f2,
  In x xs ->
  sat ph pm s g (Aiter (ApointstoIter xs F f1 f2 PTTproc)) ->
  let q := F x in
  let l := expr_eval (f1 x) s in
  let v := expr_eval (f2 x) s in
  phcLe (PHCproc q v) (ph l).
Lemma ApointstoIter_sat_single_act {T} :
  forall (xs : list T)(x : T) ph pm s g F f1 f2,
  In x xs ->
  sat ph pm s g (Aiter (ApointstoIter xs F f1 f2 PTTact)) ->
  let q := F x in
  let l := expr_eval (f1 x) s in
  let v := expr_eval (f2 x) s in
  exists v', phcLe (PHCact q v v') (ph l).

Relations between the satisfiability of assertions and converted heap cells:

Lemma sat_pointsto_conv_std :
  forall ph pm s g q E1 E2 l,
  phValid ph ->
  sat ph pm s g (Apointsto PTTstd q E1 E2) ->
  sat (phConvStd ph l) pm s g (Apointsto PTTstd q E1 E2).
Lemma sat_pointsto_conv_proc :
  forall ph pm s g q E1 E2 l,
  phValid ph ->
  sat ph pm s g (Apointsto PTTproc q E1 E2) ->
  sat (phConvProc ph l) pm s g (Apointsto PTTproc q E1 E2).
Lemma sat_pointsto_conv_act :
  forall ph pm s g q E1 E2 l,
  phValid ph ->
  sat ph pm s g (Apointsto PTTact q E1 E2) ->
  sat (phConvAct ph l) pm s g (Apointsto PTTact q E1 E2).

Lemma sat_pointsto_conv_std_mult :
  forall (ls : list Val) ph pm s g q E1 E2,
  phValid ph ->
  sat ph pm s g (Apointsto PTTstd q E1 E2) ->
  sat (phConvStdMult ph ls) pm s g (Apointsto PTTstd q E1 E2).
Lemma sat_pointsto_conv_proc_mult :
  forall (ls : list Val) ph pm s g q E1 E2,
  phValid ph ->
  sat ph pm s g (Apointsto PTTproc q E1 E2) ->
  sat (phConvProcMult ph ls) pm s g (Apointsto PTTproc q E1 E2).
Lemma sat_pointsto_conv_act_mult :
  forall (ls : list Val) ph pm s g q E1 E2,
  phValid ph ->
  sat ph pm s g (Apointsto PTTact q E1 E2) ->
  sat (phConvActMult ph ls) pm s g (Apointsto PTTact q E1 E2).

Lemma sat_iter_conv_std {T} :
  forall (xs : list T)(l : Val) ph pm s g (f1 f2 : T -> Expr)(fq : T -> Qc),
  sat ph pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTstd)) ->
  sat (phConvStd ph l) pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTstd)).
Lemma sat_iter_conv_proc {T} :
  forall (xs : list T)(l : Val) ph pm s g (f1 f2 : T -> Expr)(fq : T -> Qc),
  sat ph pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTproc)) ->
  sat (phConvProc ph l) pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTproc)).
Lemma sat_iter_conv_act {T} :
  forall (xs : list T)(l : Val) ph pm s g (f1 f2 : T -> Expr)(fq : T -> Qc),
  sat ph pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTact)) ->
  sat (phConvAct ph l) pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTact)).

Lemma sat_iter_conv_std_mult {T} :
  forall (ls : list Val)(xs : list T) ph pm s g (f1 f2 : T -> Expr)(fq : T -> Qc),
  sat ph pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTstd)) ->
  sat (phConvStdMult ph ls) pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTstd)).
Lemma sat_iter_conv_proc_mult {T} :
  forall (ls : list Val)(xs : list T) ph pm s g (f1 f2 : T -> Expr)(fq : T -> Qc),
  sat ph pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTproc)) ->
  sat (phConvProcMult ph ls) pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTproc)).
Lemma sat_iter_conv_act_mult {T} :
  forall (ls : list Val)(xs : list T) ph pm s g (f1 f2 : T -> Expr)(fq : T -> Qc),
  sat ph pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTact)) ->
  sat (phConvActMult ph ls) pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTact)).

Lemma pointsto_conv_std :
  forall ph pm s g E1 E2 q t,
  phValid ph ->
  sat ph pm s g (Apointsto t q E1 E2) ->
  let ph' := phConvStd ph (expr_eval E1 s) in
  sat ph' pm s g (Apointsto PTTstd q E1 E2).
Lemma pointsto_conv_std_proc :
  forall ph pm s g E1 E2 q,
  phValid ph ->
  sat ph pm s g (Apointsto PTTstd q E1 E2) ->
  let ph' := phConvProc ph (expr_eval E1 s) in
  sat ph' pm s g (Apointsto PTTproc q E1 E2).
Lemma pointsto_conv_proc_act :
  forall ph pm s g E1 E2 q,
  phValid ph ->
  sat ph pm s g (Apointsto PTTproc q E1 E2) ->
  let ph' := phConvAct ph (expr_eval E1 s) in
  sat ph' pm s g (Apointsto PTTact q E1 E2).

Lemma pointsto_conv_act_proc :
  forall ph pm s g E1 E2 q,
  phValid ph ->
  sat ph pm s g (Apointsto PTTact q E1 E2) ->
  let ph' := phConvProc ph (expr_eval E1 s) in
  sat ph' pm s g (Apointsto PTTproc q E1 E2).

Lemma ApointstoIter_conv_std_proc {T} :
  forall (xs : list T) ph pm s g (f1 f2 : T -> Expr),
  let F := fun _ : T => 1 in
  sat ph pm s g (Aiter (ApointstoIter xs F f1 f2 PTTstd)) ->
  let xs' := map (expr_eval_map f1 s) xs in
  let ph' := phConvProcMult ph xs' in
  sat ph' pm s g (Aiter (ApointstoIter xs F f1 f2 PTTproc)).

Lemma ApointstoIter_conv_proc_std {T} :
  forall (xs : list T) ph pm s g (f1 f2 : T -> Expr),
  let F := fun _ : T => 1 in
  sat ph pm s g (Aiter (ApointstoIter xs F f1 f2 PTTproc)) ->
  let xs' := map (expr_eval_map f1 s) xs in
  let ph' := phConvStdMult ph xs' in
  sat ph' pm s g (Aiter (ApointstoIter xs F f1 f2 PTTstd)).

Lemma ApointstoIter_conv_proc_act {T} :
  forall (xs : list T) ph pm s g (f1 f2 : T -> Expr)(F : T -> Qc),
  sat ph pm s g (Aiter (ApointstoIter xs F f1 f2 PTTproc)) ->
  let xs' := map (expr_eval_map f1 s) xs in
  let ph' := phConvActMult ph xs' in
  sat ph' pm s g (Aiter (ApointstoIter xs F f1 f2 PTTact)).

Lemma ApointstoIter_conv_act_proc {T} :
  forall (xs : list T) ph pm s g (f1 f2 : T -> Expr)(F : T -> Qc),
  sat ph pm s g (Aiter (ApointstoIter xs F f1 f2 PTTact)) ->
  let xs' := map (expr_eval_map f1 s) xs in
  let ph' := phConvProcMult ph xs' in
  sat ph' pm s g (Aiter (ApointstoIter xs F f1 f2 PTTproc)).

Relations between assertion satisfiability and heap disjointness, in combination with heap conversions.

Lemma Adisj_sat_conv_std :
  forall ph1 ph2 pm s g E1 E2 q,
  phValid ph1 ->
  sat ph1 pm s g (Apointsto PTTstd q E1 E2) ->
  phDisj (phConvStd ph1 (expr_eval E1 s)) ph2 <->
  phDisj ph1 ph2.
Lemma Adisj_sat_conv_proc :
  forall ph1 ph2 pm s g E1 E2 q,
  phValid ph1 ->
  sat ph1 pm s g (Apointsto PTTproc q E1 E2) ->
  phDisj (phConvProc ph1 (expr_eval E1 s)) ph2 <->
  phDisj ph1 ph2.
Lemma Adisj_sat_conv_act :
  forall ph1 ph2 pm s g E1 E2 q,
  phValid ph1 ->
  sat ph1 pm s g (Apointsto PTTact q E1 E2) ->
  phDisj (phConvAct ph1 (expr_eval E1 s)) ph2 <->
  phDisj ph1 ph2.

Lemma Adisj_sat_conv_std_In {T} :
  forall (xs : list T)(l : Val)(fq : T -> Qc)(f1 f2 : T -> Expr) ph1 ph2 pm s g,
  sat ph1 pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTstd)) ->
  let ls := map (expr_eval_map f1 s) xs in
  In l ls ->
  phDisj (phConvStd ph1 l) ph2 <->
  phDisj ph1 ph2.
Lemma Adisj_sat_conv_proc_In {T} :
  forall (xs : list T)(l : Val)(fq : T -> Qc)(f1 f2 : T -> Expr) ph1 ph2 pm s g,
  sat ph1 pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTproc)) ->
  let ls := map (expr_eval_map f1 s) xs in
  In l ls ->
  phDisj (phConvProc ph1 l) ph2 <-> phDisj ph1 ph2.
Lemma Adisj_sat_conv_act_In {T} :
  forall (xs : list T)(l : Val)(fq : T -> Qc)(f1 f2 : T -> Expr) ph1 ph2 pm s g,
  sat ph1 pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTact)) ->
  let ls := map (expr_eval_map f1 s) xs in
  In l ls ->
  phDisj (phConvAct ph1 l) ph2 <->
  phDisj ph1 ph2.

Lemma Adisj_sat_conv_std_mult {T} :
  forall (xs : list T)(fq : T -> Qc)(f1 f2 : T -> Expr) ph1 ph2 pm s g,
  sat ph1 pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTstd)) ->
  let ls := map (expr_eval_map f1 s) xs in
  phDisj (phConvStdMult ph1 ls) ph2 <->
  phDisj ph1 ph2.
Lemma Adisj_sat_conv_proc_mult {T} :
  forall (xs : list T)(fq : T -> Qc)(f1 f2 : T -> Expr) ph1 ph2 pm s g,
  sat ph1 pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTproc)) ->
  let ls := map (expr_eval_map f1 s) xs in
  phDisj (phConvProcMult ph1 ls) ph2 <->
  phDisj ph1 ph2.
Lemma Adisj_sat_conv_act_mult {T} :
  forall (xs : list T)(fq : T -> Qc)(f1 f2 : T -> Expr) ph1 ph2 pm s g,
  sat ph1 pm s g (Aiter (ApointstoIter xs fq f1 f2 PTTact)) ->
  let ls := map (expr_eval_map f1 s) xs in
  phDisj (phConvActMult ph1 ls) ph2 <->
  phDisj ph1 ph2.

End Assertions.