Library bipl
This file provides:
- a module "var" for the variables of a programming language
- a module "Store" for the set of variables of a programming language; it is parameterized by some "integral type"; by default, variables are to zero
- a module "Expr" for the arithmetic expressions of a programming language
- a module "Sep" for the BI formulas underlying Separation Logic
Require Import ssreflect ssrbool eqtype.
Require Import Bool_ext EqNat_ext ZArith_ext Max_ext.
Require Import order.
Require Import finmap.
Require Import integral_type.
Require Import Lists_ext.
Module Type VAR.
Parameter v : Set.
Parameter eqdec : forall (x y : v), {x = y} + {x <> y}.
End VAR.
Module var <: VAR with Definition v := nat.
Definition v := nat.
Definition eqdec := eq_nat_dec.
End var.
Module Type STORE.
type of stored data
default value for stored data
type of stores
Parameter t : Type.
Parameter dom : t -> list var.v.
Parameter emp : t.
Parameter get : var.v -> t -> u.
Parameter upd : var.v -> u -> t -> t.
Parameter upds : list var.v -> list u -> t -> t.
Parameter get_emp : forall x, get x emp = u0.
Parameter get_upd : forall x y z s, x <> y -> get x (upd y z s) = get x s.
Parameter get_upds : forall x ys zs s, ~ In x ys -> get x (upds ys zs s) = get x s.
Parameter get_upd' : forall x z s, get x (upd x z s) = z.
Parameter upd_upd : forall s x x' v v', x <> x' -> upd x v (upd x' v' s) = upd x' v' (upd x v s).
Parameter upd_upd_eq : forall s x v v', upd x v (upd x v' s) = upd x v s.
Parameter upd_get : forall s x, upd x (get x s) s = s.
Parameter upd_get_upd: forall x v s, upd x (get x s) (upd x v s) = s.
End STORE.
Module Store (A : IntegralType) <: STORE.
Definition u : eqType := A.t.
Definition u0 := A.nat2t O.
Canonical Structure t_non_zero_eqMixin := EqMixin A.t_non_zeroP.
Canonical Structure t_non_zero_eqType := Eval hnf in EqType _ t_non_zero_eqMixin.
Module non_null_integer <: EQTYPE.
Definition A : eqType := t_non_zero_eqType.
End non_null_integer.
Module store_heap := finmap.map NatOrder non_null_integer.
Definition t := store_heap.t.
Definition dom (st : t) : list var.v := seq_ext.s2l (store_heap.dom st).
Definition emp : t := store_heap.emp.
Parameter dom : t -> list var.v.
Parameter emp : t.
Parameter get : var.v -> t -> u.
Parameter upd : var.v -> u -> t -> t.
Parameter upds : list var.v -> list u -> t -> t.
Parameter get_emp : forall x, get x emp = u0.
Parameter get_upd : forall x y z s, x <> y -> get x (upd y z s) = get x s.
Parameter get_upds : forall x ys zs s, ~ In x ys -> get x (upds ys zs s) = get x s.
Parameter get_upd' : forall x z s, get x (upd x z s) = z.
Parameter upd_upd : forall s x x' v v', x <> x' -> upd x v (upd x' v' s) = upd x' v' (upd x v s).
Parameter upd_upd_eq : forall s x v v', upd x v (upd x v' s) = upd x v s.
Parameter upd_get : forall s x, upd x (get x s) s = s.
Parameter upd_get_upd: forall x v s, upd x (get x s) (upd x v s) = s.
End STORE.
Module Store (A : IntegralType) <: STORE.
Definition u : eqType := A.t.
Definition u0 := A.nat2t O.
Canonical Structure t_non_zero_eqMixin := EqMixin A.t_non_zeroP.
Canonical Structure t_non_zero_eqType := Eval hnf in EqType _ t_non_zero_eqMixin.
Module non_null_integer <: EQTYPE.
Definition A : eqType := t_non_zero_eqType.
End non_null_integer.
Module store_heap := finmap.map NatOrder non_null_integer.
Definition t := store_heap.t.
Definition dom (st : t) : list var.v := seq_ext.s2l (store_heap.dom st).
Definition emp : t := store_heap.emp.
warning: default value is t0
Definition get (w : var.v) (st : t) : A.t :=
match store_heap.get w st with Some i => A.t_non_zero2t i | None => A.nat2t O end.
Definition upd (i : var.v) (w : A.t) (st : t) : t.
Fixpoint upds (xs : list var.v) (vs : list u) (st : t) {struct xs} : t :=
match xs with
| nil => st
| hx :: tx =>
match vs with
| nil => st
| hv :: tv =>
let st' := upds tx tv st in
upd hx hv st'
end
end.
Lemma get_emp : forall x, get x emp = A.nat2t O.
Lemma get_upd : forall x y z st, x <> y -> get x (upd y z st) = get x st.
Lemma get_upds : forall x ys zs st, ~ In x ys -> get x (upds ys zs st) = get x st.
Lemma get_upd' : forall w z st, get w (upd w z st) = z.
Lemma extensionality: forall st1 st2, (forall x, get x st1 = get x st2) -> st1 = st2.
Lemma upd_upd: forall s x x' v v', x <> x' -> upd x v (upd x' v' s) = upd x' v' (upd x v s).
Lemma upd_upd_eq : forall s x v v', upd x v (upd x v' s) = upd x v s.
Lemma upd_get : forall s x, upd x (get x s) s = s.
Lemma upd_get_upd: forall x v s, upd x (get x s) (upd x v s) = s.
Lemma get_proj' : forall (d : seq.seq store_heap.l) k n, n \notin d -> get n (store_heap.proj k d) = u0.
Lemma get_proj : forall (d : seq.seq store_heap.l) k n, n \in d -> get n (store_heap.proj k d) = get n k.
Lemma get_difs : forall k x (d : seq.seq store_heap.l), x \notin d -> get x (store_heap.difs k d) = get x k.
Lemma get_difs' : forall k x (d : seq.seq store_heap.l), x \in d -> get x (store_heap.difs k d) = u0.
End Store.
Module Expr (A : IntegralType).
Inductive binop_e : Set :=
| add_e | min_e | mul_e | div_e | mod_e.
Definition binop_e_interp (bo : binop_e) : A.t -> A.t -> A.t :=
match bo with
| add_e => A.t_plus
| min_e => A.t_minus
| mul_e => A.t_mult
| div_e => A.t_div
| mod_e => A.t_mod
end.
Definition binop_e_eq b1 b2 :=
match b1 with
| add_e => match b2 with add_e => true | _ => false end
| min_e => match b2 with min_e => true | _ => false end
| mul_e => match b2 with mul_e => true | _ => false end
| div_e => match b2 with div_e => true | _ => false end
| mod_e => match b2 with mod_e => true | _ => false end
end.
Inductive unaop_e : Set := valabs_e | negate_e.
Definition unaop_e_eq b1 b2 :=
match b1 with
| valabs_e => match b2 with valabs_e => true | _ => false end
| negate_e => match b2 with negate_e => true | _ => false end
end.
Definition unaop_e_interp uo :=
match uo with
| valabs_e => A.t_valabs
| negate_e => fun x => A.t_minus (A.nat2t 0) x
end.
match store_heap.get w st with Some i => A.t_non_zero2t i | None => A.nat2t O end.
Definition upd (i : var.v) (w : A.t) (st : t) : t.
Fixpoint upds (xs : list var.v) (vs : list u) (st : t) {struct xs} : t :=
match xs with
| nil => st
| hx :: tx =>
match vs with
| nil => st
| hv :: tv =>
let st' := upds tx tv st in
upd hx hv st'
end
end.
Lemma get_emp : forall x, get x emp = A.nat2t O.
Lemma get_upd : forall x y z st, x <> y -> get x (upd y z st) = get x st.
Lemma get_upds : forall x ys zs st, ~ In x ys -> get x (upds ys zs st) = get x st.
Lemma get_upd' : forall w z st, get w (upd w z st) = z.
Lemma extensionality: forall st1 st2, (forall x, get x st1 = get x st2) -> st1 = st2.
Lemma upd_upd: forall s x x' v v', x <> x' -> upd x v (upd x' v' s) = upd x' v' (upd x v s).
Lemma upd_upd_eq : forall s x v v', upd x v (upd x v' s) = upd x v s.
Lemma upd_get : forall s x, upd x (get x s) s = s.
Lemma upd_get_upd: forall x v s, upd x (get x s) (upd x v s) = s.
Lemma get_proj' : forall (d : seq.seq store_heap.l) k n, n \notin d -> get n (store_heap.proj k d) = u0.
Lemma get_proj : forall (d : seq.seq store_heap.l) k n, n \in d -> get n (store_heap.proj k d) = get n k.
Lemma get_difs : forall k x (d : seq.seq store_heap.l), x \notin d -> get x (store_heap.difs k d) = get x k.
Lemma get_difs' : forall k x (d : seq.seq store_heap.l), x \in d -> get x (store_heap.difs k d) = u0.
End Store.
Module Expr (A : IntegralType).
Inductive binop_e : Set :=
| add_e | min_e | mul_e | div_e | mod_e.
Definition binop_e_interp (bo : binop_e) : A.t -> A.t -> A.t :=
match bo with
| add_e => A.t_plus
| min_e => A.t_minus
| mul_e => A.t_mult
| div_e => A.t_div
| mod_e => A.t_mod
end.
Definition binop_e_eq b1 b2 :=
match b1 with
| add_e => match b2 with add_e => true | _ => false end
| min_e => match b2 with min_e => true | _ => false end
| mul_e => match b2 with mul_e => true | _ => false end
| div_e => match b2 with div_e => true | _ => false end
| mod_e => match b2 with mod_e => true | _ => false end
end.
Inductive unaop_e : Set := valabs_e | negate_e.
Definition unaop_e_eq b1 b2 :=
match b1 with
| valabs_e => match b2 with valabs_e => true | _ => false end
| negate_e => match b2 with negate_e => true | _ => false end
end.
Definition unaop_e_interp uo :=
match uo with
| valabs_e => A.t_valabs
| negate_e => fun x => A.t_minus (A.nat2t 0) x
end.
Definition of expressions
Inductive expr : Type :=
| var_e : var.v -> expr
| cst_e : A.t -> expr
| bop_e : binop_e -> expr -> expr -> expr
| uop_e : unaop_e -> expr -> expr.
Definition nat_e x := cst_e (A.nat2t x).
Definition null := cst_e (A.nat2t O).
Notation "e1 '+e' e2" := (bop_e add_e e1 e2) (at level 75) : seplog_expr_scope.
Notation "e1 '.-e' e2" := (bop_e min_e e1 e2) (at level 75) : seplog_expr_scope.
Notation "e1 '*e' e2" := (bop_e mul_e e1 e2) (at level 75) : seplog_expr_scope.
Notation "e1 './e' e2" := (bop_e div_e e1 e2) (at level 75) : seplog_expr_scope.
Notation "e1 'mode' e2" := (bop_e mod_e e1 e2) (at level 75) : seplog_expr_scope.
Notation ".--e e" := (uop_e negate_e e) (at level 75) : seplog_expr_scope.
Local Open Scope seplog_expr_scope.
Delimit Scope seplog_expr_scope with seplog_expr.
| var_e : var.v -> expr
| cst_e : A.t -> expr
| bop_e : binop_e -> expr -> expr -> expr
| uop_e : unaop_e -> expr -> expr.
Definition nat_e x := cst_e (A.nat2t x).
Definition null := cst_e (A.nat2t O).
Notation "e1 '+e' e2" := (bop_e add_e e1 e2) (at level 75) : seplog_expr_scope.
Notation "e1 '.-e' e2" := (bop_e min_e e1 e2) (at level 75) : seplog_expr_scope.
Notation "e1 '*e' e2" := (bop_e mul_e e1 e2) (at level 75) : seplog_expr_scope.
Notation "e1 './e' e2" := (bop_e div_e e1 e2) (at level 75) : seplog_expr_scope.
Notation "e1 'mode' e2" := (bop_e mod_e e1 e2) (at level 75) : seplog_expr_scope.
Notation ".--e e" := (uop_e negate_e e) (at level 75) : seplog_expr_scope.
Local Open Scope seplog_expr_scope.
Delimit Scope seplog_expr_scope with seplog_expr.
Notation for structures
Definition field x f := var_e x +e cst_e f.
Notation "x '-.>' f " := (field x f) (at level 75) : seplog_expr_scope.
Fixpoint vars (e : expr) : list var.v :=
match e with
| var_e x => x :: List.nil
| cst_e z => List.nil
| bop_e _ e1 e2 => vars e1 ++ vars e2
| uop_e _ e' => vars e'
end.
Definition fresh_e x e := (max_lst (vars e) < x)%nat.
Lemma fresh_e_var_e_neq : forall x y, fresh_e x (var_e y) -> x <> y.
Fixpoint var_max_lst (l : list (var.v * expr)) : var.v :=
match l with
| nil => O
| (v, e) :: tl => max (max v (max_lst (vars e))) (var_max_lst tl)
end.
Definition fresh_lst x l := (var_max_lst l < x)%nat.
Lemma fresh_lst_inv : forall x h0 h1 t, fresh_lst x ((h0, h1) :: t) ->
fresh_e x h1 /\ x <> h0 /\ fresh_lst x t.
Notation "x '-.>' f " := (field x f) (at level 75) : seplog_expr_scope.
Fixpoint vars (e : expr) : list var.v :=
match e with
| var_e x => x :: List.nil
| cst_e z => List.nil
| bop_e _ e1 e2 => vars e1 ++ vars e2
| uop_e _ e' => vars e'
end.
Definition fresh_e x e := (max_lst (vars e) < x)%nat.
Lemma fresh_e_var_e_neq : forall x y, fresh_e x (var_e y) -> x <> y.
Fixpoint var_max_lst (l : list (var.v * expr)) : var.v :=
match l with
| nil => O
| (v, e) :: tl => max (max v (max_lst (vars e))) (var_max_lst tl)
end.
Definition fresh_lst x l := (var_max_lst l < x)%nat.
Lemma fresh_lst_inv : forall x h0 h1 t, fresh_lst x ((h0, h1) :: t) ->
fresh_e x h1 /\ x <> h0 /\ fresh_lst x t.
the list (without redundancies) of free vars of an expr
Fixpoint vars_set (e : expr) : list var.v :=
match e with
| var_e x => x :: nil
| cst_e z => nil
| bop_e _ e1 e2 => Lists_ext.app_set beq_nat (vars_set e1) (vars_set e2)
| uop_e _ e' => vars_set e'
end.
Lemma incl_vars_vars_set : forall e, incl (vars e) (vars_set e).
Fixpoint expr_eq (e1 e2 : expr) {struct e1} : bool :=
match e1 with
| var_e w1 =>
match e2 with var_e w2 => beq_nat w1 w2 | _ => false end
| cst_e i1 =>
match e2 with cst_e i2 => A.t_eqb i1 i2 | _ => false end
| bop_e bo e11 e12 =>
match e2 with
| bop_e bo' e21 e22 =>
binop_e_eq bo bo' && expr_eq e11 e21 && expr_eq e12 e22
| _ => false
end
| uop_e uo e11 =>
match e2 with
| uop_e uo' e22 => unaop_e_eq uo uo' && expr_eq e11 e22 | _ => false
end
end.
match e with
| var_e x => x :: nil
| cst_e z => nil
| bop_e _ e1 e2 => Lists_ext.app_set beq_nat (vars_set e1) (vars_set e2)
| uop_e _ e' => vars_set e'
end.
Lemma incl_vars_vars_set : forall e, incl (vars e) (vars_set e).
Fixpoint expr_eq (e1 e2 : expr) {struct e1} : bool :=
match e1 with
| var_e w1 =>
match e2 with var_e w2 => beq_nat w1 w2 | _ => false end
| cst_e i1 =>
match e2 with cst_e i2 => A.t_eqb i1 i2 | _ => false end
| bop_e bo e11 e12 =>
match e2 with
| bop_e bo' e21 e22 =>
binop_e_eq bo bo' && expr_eq e11 e21 && expr_eq e12 e22
| _ => false
end
| uop_e uo e11 =>
match e2 with
| uop_e uo' e22 => unaop_e_eq uo uo' && expr_eq e11 e22 | _ => false
end
end.
substitute "pattern" for "replacement" in "e"
Fixpoint subst_e (e patt repl : expr) {struct e} : expr :=
match e with
| var_e w => match expr_eq e patt with
| true => repl
| _ => e
end
| cst_e i => match expr_eq e patt with
| true => repl
| _ => e
end
| bop_e bo e1 e2 =>
match expr_eq e patt with
| true => repl
| _ => bop_e bo (subst_e e1 patt repl) (subst_e e2 patt repl)
end
| uop_e uo e' => match expr_eq e patt with
| true => repl
| _ => uop_e uo (subst_e e' patt repl)
end
end.
match e with
| var_e w => match expr_eq e patt with
| true => repl
| _ => e
end
| cst_e i => match expr_eq e patt with
| true => repl
| _ => e
end
| bop_e bo e1 e2 =>
match expr_eq e patt with
| true => repl
| _ => bop_e bo (subst_e e1 patt repl) (subst_e e2 patt repl)
end
| uop_e uo e' => match expr_eq e patt with
| true => repl
| _ => uop_e uo (subst_e e' patt repl)
end
end.
Boolean expressions
neq_b and ge_b are redundant (<> =def= ~ _ = _ and >= =def= > \/ =) but defining then as such slows down evaluation (e.g., by a factor 2.5 for ge_b)
neq_b and ge_b are redundant (<> =def= ~ _ = _ and >= =def= > \/ =) but defining then as such slows down evaluation (e.g., by a factor 2.5 for ge_b)
Inductive binop_b : Set := eq_b | neq_b | ge_b | gt_b.
Definition binop_b_interp (bo : binop_b) : A.t -> A.t -> bool :=
match bo with
| eq_b => A.t_eqb
| neq_b => fun a b => negb (A.t_eqb a b)
| ge_b => A.t_geb
| gt_b => A.t_gtb
end.
Definition binop_b_eq b1 b2 :=
match b1 with
| eq_b => match b2 with eq_b => true | _ => false end
| neq_b => match b2 with neq_b => true | _ => false end
| ge_b => match b2 with ge_b => true | _ => false end
| gt_b => match b2 with gt_b => true | _ => false end
end.
Inductive binop_b2 : Set := and_b | or_b.
Definition binop_b2_interp (bo : binop_b2) : bool -> bool -> bool :=
match bo with
| and_b => andb
| or_b => orb
end.
Definition binop_b2_eq b1 b2 :=
match b1 with
| and_b => match b2 with and_b => true | _ => false end
| or_b => match b2 with or_b => true | _ => false end
end.
Inductive expr_b : Type :=
| true_b: expr_b
| bop_b : binop_b -> expr -> expr -> expr_b
| neg_b : expr_b -> expr_b
| bop_b2 : binop_b2 -> expr_b -> expr_b -> expr_b.
Definition binop_b_interp (bo : binop_b) : A.t -> A.t -> bool :=
match bo with
| eq_b => A.t_eqb
| neq_b => fun a b => negb (A.t_eqb a b)
| ge_b => A.t_geb
| gt_b => A.t_gtb
end.
Definition binop_b_eq b1 b2 :=
match b1 with
| eq_b => match b2 with eq_b => true | _ => false end
| neq_b => match b2 with neq_b => true | _ => false end
| ge_b => match b2 with ge_b => true | _ => false end
| gt_b => match b2 with gt_b => true | _ => false end
end.
Inductive binop_b2 : Set := and_b | or_b.
Definition binop_b2_interp (bo : binop_b2) : bool -> bool -> bool :=
match bo with
| and_b => andb
| or_b => orb
end.
Definition binop_b2_eq b1 b2 :=
match b1 with
| and_b => match b2 with and_b => true | _ => false end
| or_b => match b2 with or_b => true | _ => false end
end.
Inductive expr_b : Type :=
| true_b: expr_b
| bop_b : binop_b -> expr -> expr -> expr_b
| neg_b : expr_b -> expr_b
| bop_b2 : binop_b2 -> expr_b -> expr_b -> expr_b.
Number of constructors in an expr_b formula
Fixpoint Expr_B_size (e : expr_b) : nat :=
match e with
| true_b => 1%nat
| bop_b _ e1 e2 => 1%nat
| bop_b2 _ e1 e2 => (1 + (Expr_B_size e1) + (Expr_B_size e2))%nat
| neg_b e => (1 + Expr_B_size e)%nat
end.
Lemma expr_b_min_size: forall b, (Expr_B_size b >= 1)%nat.
Notation "e =e e'" := (bop_b eq_b e e') (at level 76) : seplog_expr_scope.
Notation "e <>e e'" := (bop_b neq_b e e') (at level 76) : seplog_expr_scope.
Notation "e >>= e'" := (bop_b ge_b e e') (at level 76) : seplog_expr_scope.
Notation "e >> e'" := (bop_b gt_b e e') (at level 76) : seplog_expr_scope.
Notation "e &e e'" := (bop_b2 and_b e e') (at level 77) : seplog_expr_scope.
Notation "e |e e'" := (bop_b2 or_b e e') (at level 77) : seplog_expr_scope.
match e with
| true_b => 1%nat
| bop_b _ e1 e2 => 1%nat
| bop_b2 _ e1 e2 => (1 + (Expr_B_size e1) + (Expr_B_size e2))%nat
| neg_b e => (1 + Expr_B_size e)%nat
end.
Lemma expr_b_min_size: forall b, (Expr_B_size b >= 1)%nat.
Notation "e =e e'" := (bop_b eq_b e e') (at level 76) : seplog_expr_scope.
Notation "e <>e e'" := (bop_b neq_b e e') (at level 76) : seplog_expr_scope.
Notation "e >>= e'" := (bop_b ge_b e e') (at level 76) : seplog_expr_scope.
Notation "e >> e'" := (bop_b gt_b e e') (at level 76) : seplog_expr_scope.
Notation "e &e e'" := (bop_b2 and_b e e') (at level 77) : seplog_expr_scope.
Notation "e |e e'" := (bop_b2 or_b e e') (at level 77) : seplog_expr_scope.
additional notations
Notation "e << e'" := (neg_b (bop_b ge_b e e')) (at level 76) : seplog_expr_scope.
Notation "e <<= e'" := (neg_b (bop_b gt_b e e')) (at level 76) : seplog_expr_scope.
Notation "~e e" := (neg_b e) (at level 77) : seplog_expr_scope.
Fixpoint vars_b (e : expr_b) : list var.v :=
match e with
| true_b => List.nil
| bop_b _ e1 e2 => vars e1 ++ vars e2
| bop_b2 _ e1 e2 => vars_b e1 ++ vars_b e2
| ~e e => vars_b e
end.
Definition fresh_b x b := (max_lst (vars_b b) < x)%nat.
Notation "e <<= e'" := (neg_b (bop_b gt_b e e')) (at level 76) : seplog_expr_scope.
Notation "~e e" := (neg_b e) (at level 77) : seplog_expr_scope.
Fixpoint vars_b (e : expr_b) : list var.v :=
match e with
| true_b => List.nil
| bop_b _ e1 e2 => vars e1 ++ vars e2
| bop_b2 _ e1 e2 => vars_b e1 ++ vars_b e2
| ~e e => vars_b e
end.
Definition fresh_b x b := (max_lst (vars_b b) < x)%nat.
the list (without redundancies) of free vars of an expr_b
Fixpoint vars_b_set (e : expr_b) : list var.v :=
match e with
| true_b => nil
| bop_b _ e1 e2 => Lists_ext.app_set beq_nat (vars_set e1) (vars_set e2)
| bop_b2 _ e1 e2 => Lists_ext.app_set beq_nat (vars_b_set e1) (vars_b_set e2)
| ~e e => vars_b_set e
end.
Lemma incl_vars_b_vars_b_set : forall e, incl (vars_b e) (vars_b_set e).
Fixpoint expr_b_eq (e1 e2 : expr_b) : bool :=
match e1 with
| true_b => match e2 with true_b => true | _ => false end
| bop_b bo f g =>
match e2 with
| bop_b bo' f' g' =>
binop_b_eq bo bo' && expr_eq f f' && expr_eq g g'
| _ => false
end
| bop_b2 bo f g =>
match e2 with
| bop_b2 bo' f' g' =>
binop_b2_eq bo bo' && expr_b_eq f f' && expr_b_eq g g'
| _ => false
end
| ~e e => match e2 with ~e e' => expr_b_eq e e' | _ => false end
end.
match e with
| true_b => nil
| bop_b _ e1 e2 => Lists_ext.app_set beq_nat (vars_set e1) (vars_set e2)
| bop_b2 _ e1 e2 => Lists_ext.app_set beq_nat (vars_b_set e1) (vars_b_set e2)
| ~e e => vars_b_set e
end.
Lemma incl_vars_b_vars_b_set : forall e, incl (vars_b e) (vars_b_set e).
Fixpoint expr_b_eq (e1 e2 : expr_b) : bool :=
match e1 with
| true_b => match e2 with true_b => true | _ => false end
| bop_b bo f g =>
match e2 with
| bop_b bo' f' g' =>
binop_b_eq bo bo' && expr_eq f f' && expr_eq g g'
| _ => false
end
| bop_b2 bo f g =>
match e2 with
| bop_b2 bo' f' g' =>
binop_b2_eq bo bo' && expr_b_eq f f' && expr_b_eq g g'
| _ => false
end
| ~e e => match e2 with ~e e' => expr_b_eq e e' | _ => false end
end.
substitute "pattern" for "replacement" in "e"
Fixpoint subst_b (e : expr_b) (patt repl : expr) {struct e} : expr_b :=
match e with
| true_b => true_b
| bop_b bo f g =>
bop_b bo (subst_e f patt repl) (subst_e g patt repl)
| bop_b2 bo f g =>
bop_b2 bo (subst_b f patt repl) (subst_b g patt repl)
| ~e e => ~e (subst_b e patt repl)
end.
Module store := Store A.
match e with
| true_b => true_b
| bop_b bo f g =>
bop_b bo (subst_e f patt repl) (subst_e g patt repl)
| bop_b2 bo f g =>
bop_b2 bo (subst_b f patt repl) (subst_b g patt repl)
| ~e e => ~e (subst_b e patt repl)
end.
Module store := Store A.
this tactic resolves some simple goals over store_upd
Require Import nodup.
Ltac Store_upd :=
match goal with
| |- context [store.get ?x (store.upd ?x ?z ?s)] =>
rewrite -> (store.get_upd' x z s)
| |- context [store.get ?x (store.upd ?x' ?z ?s)] =>
rewrite -> (store.get_upd x x' z s); [ idtac | Nodup_neq]
| |- _ => fail
end.
Ltac Store_upd :=
match goal with
| |- context [store.get ?x (store.upd ?x ?z ?s)] =>
rewrite -> (store.get_upd' x z s)
| |- context [store.get ?x (store.upd ?x' ?z ?s)] =>
rewrite -> (store.get_upd x x' z s); [ idtac | Nodup_neq]
| |- _ => fail
end.
Compute the value of an expression in a store
Fixpoint eval (e : expr) (s : store.t) : A.t :=
match e with
| var_e w => store.get w s
| cst_e i => i
| bop_e bo e1 e2 => binop_e_interp bo (eval e1 s) (eval e2 s)
| uop_e uo e' => unaop_e_interp uo (eval e' s)
end.
Notation "'[' x ']_' s" := (store.get x s) (at level 9) : seplog_expr_scope.
Notation "'[' e ']e_' s" := (eval e s) (at level 9) : seplog_expr_scope.
Lemma store_get_proj : forall s x d, In x (seq_ext.s2l d) ->
[ x ]_ (store.store_heap.proj s d) = [ x ]_ s.
Lemma eval_upd : forall e s v x, ~ In x (vars e) ->
[ e ]e_ (store.upd x v s) = [ e ]e_ s.
Lemma eval_upds : forall e xs, disj (vars e) xs ->
forall s zs, [ e ]e_ (store.upds xs zs s) = [ e ]e_ s.
Ltac open_fresh :=
open_fresh_hypo; open_fresh_goal
with
open_fresh_hypo := match goal with
| H: fresh_e _ _ |- _ => unfold fresh_e in H; simpl in H; open_fresh_hypo
| H: fresh_b _ _ |- _ => unfold fresh_b in H; simpl in H; open_fresh_hypo
| H: fresh_lst _ _ |- _ => unfold fresh_lst in H; simpl in H; open_fresh_hypo
| |- _ => idtac
end
with
open_fresh_goal := match goal with
| |- fresh_e _ _ => unfold fresh_e; simpl; open_fresh_goal
| |- fresh_b _ _ => unfold fresh_b; simpl; open_fresh_goal
| |- fresh_lst _ _ => unfold fresh_lst; simpl; open_fresh_goal
| |- _ => idtac
end.
Ltac maxinf_resolve := open_fresh; Resolve_lt_max.
Lemma fresh_e_eval : forall e x v s, fresh_e x e ->
[ e ]e_(store.upd x v s) = [ e ]e_s.
Lemma eval_upd_subst : forall e s x v,
[ e ]e_ (store.upd x ([ v ]e_s) s) = [ subst_e e (var_e x) v ]e_ s.
Lemma eval_proj : forall e s d, incl (vars e) (seq_ext.s2l d) ->
[ e ]e_ (store.store_heap.proj s d) = [ e ]e_ s.
Lemma store_proj_upd : forall (x:var.v) v (s:store.store_heap.t) (d : seq.seq var.v),
In x (seq_ext.s2l d) ->
store.store_heap.proj (store.upd x v s) d = store.upd x v (store.store_heap.proj s d).
Lemma abstract_subst_e : forall e x v s,
exists e', [ e ]e_ s = [ subst_e e' (var_e x) v ]e_ s.
Lemma fresh_e_subst_e : forall e x v0 e0,
fresh_e x e -> x <> v0 -> fresh_e x e0 ->
fresh_e x (subst_e e (var_e v0) e0).
match e with
| var_e w => store.get w s
| cst_e i => i
| bop_e bo e1 e2 => binop_e_interp bo (eval e1 s) (eval e2 s)
| uop_e uo e' => unaop_e_interp uo (eval e' s)
end.
Notation "'[' x ']_' s" := (store.get x s) (at level 9) : seplog_expr_scope.
Notation "'[' e ']e_' s" := (eval e s) (at level 9) : seplog_expr_scope.
Lemma store_get_proj : forall s x d, In x (seq_ext.s2l d) ->
[ x ]_ (store.store_heap.proj s d) = [ x ]_ s.
Lemma eval_upd : forall e s v x, ~ In x (vars e) ->
[ e ]e_ (store.upd x v s) = [ e ]e_ s.
Lemma eval_upds : forall e xs, disj (vars e) xs ->
forall s zs, [ e ]e_ (store.upds xs zs s) = [ e ]e_ s.
Ltac open_fresh :=
open_fresh_hypo; open_fresh_goal
with
open_fresh_hypo := match goal with
| H: fresh_e _ _ |- _ => unfold fresh_e in H; simpl in H; open_fresh_hypo
| H: fresh_b _ _ |- _ => unfold fresh_b in H; simpl in H; open_fresh_hypo
| H: fresh_lst _ _ |- _ => unfold fresh_lst in H; simpl in H; open_fresh_hypo
| |- _ => idtac
end
with
open_fresh_goal := match goal with
| |- fresh_e _ _ => unfold fresh_e; simpl; open_fresh_goal
| |- fresh_b _ _ => unfold fresh_b; simpl; open_fresh_goal
| |- fresh_lst _ _ => unfold fresh_lst; simpl; open_fresh_goal
| |- _ => idtac
end.
Ltac maxinf_resolve := open_fresh; Resolve_lt_max.
Lemma fresh_e_eval : forall e x v s, fresh_e x e ->
[ e ]e_(store.upd x v s) = [ e ]e_s.
Lemma eval_upd_subst : forall e s x v,
[ e ]e_ (store.upd x ([ v ]e_s) s) = [ subst_e e (var_e x) v ]e_ s.
Lemma eval_proj : forall e s d, incl (vars e) (seq_ext.s2l d) ->
[ e ]e_ (store.store_heap.proj s d) = [ e ]e_ s.
Lemma store_proj_upd : forall (x:var.v) v (s:store.store_heap.t) (d : seq.seq var.v),
In x (seq_ext.s2l d) ->
store.store_heap.proj (store.upd x v s) d = store.upd x v (store.store_heap.proj s d).
Lemma abstract_subst_e : forall e x v s,
exists e', [ e ]e_ s = [ subst_e e' (var_e x) v ]e_ s.
Lemma fresh_e_subst_e : forall e x v0 e0,
fresh_e x e -> x <> v0 -> fresh_e x e0 ->
fresh_e x (subst_e e (var_e v0) e0).
simultaneous substitutionss
Fixpoint subst_e_lst (l : list (var.v * expr)) (e: expr) {struct l} : expr :=
match l with
| nil => e
| (x, e') :: tl => subst_e_lst tl (subst_e e (var_e x) e')
end.
Lemma subst_e_lst_cst_e : forall l v s, [ subst_e_lst l (cst_e v) ]e_ s = v.
Lemma subst_e_lst_eval : forall l e x v s, fresh_e x e -> fresh_lst x l ->
[ subst_e_lst l e ]e_(store.upd x v s) = [ subst_e_lst l e ]e_s.
match l with
| nil => e
| (x, e') :: tl => subst_e_lst tl (subst_e e (var_e x) e')
end.
Lemma subst_e_lst_cst_e : forall l v s, [ subst_e_lst l (cst_e v) ]e_ s = v.
Lemma subst_e_lst_eval : forall l e x v s, fresh_e x e -> fresh_lst x l ->
[ subst_e_lst l e ]e_(store.upd x v s) = [ subst_e_lst l e ]e_s.
Compute the value of a boolean expression
Fixpoint eval_b (e : expr_b) (s : store.t) : bool :=
match e with
| true_b => true
| bop_b bo e1 e2 => binop_b_interp bo ([ e1 ]e_ s) ([ e2 ]e_ s)
| bop_b2 bo e1 e2 => binop_b2_interp bo (eval_b e1 s) (eval_b e2 s)
| ~e e => ~~ eval_b e s
end.
Notation "'[' e ']b_' s" := (eval_b e s) (at level 9) : seplog_expr_scope.
Notation " b1 =b> b2 " := ((~e b1) |e b2) (right associativity, at level 80) : seplog_expr_scope.
Lemma eval_b_neg : forall t s, [ ~e t ]b_s = ~~ [ t ]b_ s.
Lemma expr_b_neg_involutive : forall a s, [ ~e ~e a ]b_ s = [ a ]b_s.
Lemma expr_b_impl_intro: forall b1 b2 s, [ b1 ]b_s -> [ b1 =b> b2 ]b_s -> [ b2 ]b_s.
Fixpoint subst_b_lst (l : list (var.v * expr)) (e : expr_b) {struct l}: expr_b :=
match l with
| nil => e
| (x, e') :: tl => subst_b_lst tl (subst_b e (var_e x) e')
end.
Lemma eval_b_upd : forall b s v x, ~ In x (vars_b b) ->
[ b ]b_ (store.upd x v s) = [ b ]b_ s.
Lemma eval_b_proj : forall e s d, incl (vars_b e) (seq_ext.s2l d) ->
[ e ]b_ (store.store_heap.proj s d) = [ e ]b_ s.
Lemma eval_b_upds : forall e xs, disj (vars_b e) xs ->
forall s zs, [ e ]b_ (store.upds xs zs s) = [ e ]b_ s.
Lemma eval_b_upd_subst : forall b s x v,
[ b ]b_ (store.upd x ([ v ]e_ s) s) = [ subst_b b (var_e x) v ]b_s.
Fixpoint eval_b_Prop (e : expr_b) (s : store.t) : Prop :=
match e with
| true_b => True
| f =e g => [ f ]e_ s = [ g ]e_ s
| f <>e g => [ f ]e_ s <> [ g ]e_ s
| f >>= g => A.t_ge ([ f ]e_ s) ([ g ]e_ s)
| f >> g => A.t_gt ([ f ]e_ s) ([ g ]e_ s)
| f &e g => eval_b_Prop f s /\ eval_b_Prop g s
| f |e g => eval_b_Prop f s \/ eval_b_Prop g s
| neg_b e => ~ eval_b_Prop e s
end.
Lemma expr_bP : forall e s, [ e ]b_ s <-> eval_b_Prop e s.
Lemma expr_b_reflect: forall b1 b2 s,
([ b1 ]b_s <-> [ b2 ]b_s) -> [ b1 ]b_ s = [ b2 ]b_ s.
Lemma expr_b_reflect' : forall b1 b2 s,
[ b1 ]b_ s = [ b2 ]b_ s -> ([ b1 ]b_s <-> [ b2 ]b_s).
Ltac eval_b2Prop_hyp h :=
match goal with
| H : is_true (eval_b ?e ?s) |- _ =>
move: {H}(proj1 (expr_bP e _) H) => H; simpl in H
end.
Ltac eval_b2Prop_hyps :=
match goal with
| id : is_true (eval_b ?e ?s) |- _ => eval_b2Prop_hyp id; eval_b2Prop_hyps
| id : is_true (~~ eval_b ?e ?s) |- _ =>
rewrite <- eval_b_neg in id; eval_b2Prop_hyps
| |- _ => idtac
end.
Ltac eval_b2Prop_goal :=
match goal with
| |- is_true (eval_b ?e ?s) => apply (proj2 (expr_bP e s)); simpl
| |- is_true (~~ eval_b ?e ?s) =>
rewrite <- eval_b_neg;
eval_b2Prop_goal
| |- _ => idtac
end.
Ltac eval2Prop_hyp :=
match goal with
| h : context [ (eval (var_e ?e) ?s) ] |- _ =>
simpl in h
end.
Require Import omegaz.
Ltac omegab :=
eval_b2Prop_hyps ; eval_b2Prop_goal ;
repeat eval2Prop_hyp ;
(try tauto || omega ||
( (repeat open_integral_type_hyp);
open_integral_type_goal );
omegaz).
End Expr.
Module Assert (A : IntegralType).
Module Import expr_m := Expr A.
Local Open Scope seplog_expr_scope.
Canonical Structure t_eqMixin := EqMixin A.tP.
Canonical Structure t_eqType := Eval hnf in EqType _ t_eqMixin.
Module int_type <: EQTYPE.
Definition A : eqType := t_eqType.
End int_type.
Module AOrder <: ORDER.
Definition A := A.t.
Definition ltA : A -> A -> bool := fun a b => negb (A.t_geb a b).
Lemma ltA_trans : forall n m p, ltA m n -> ltA n p -> ltA m p.
Lemma ltA_irr : forall a, ltA a a = false.
Lemma ltA_total : forall m n, (m != n) = (ltA m n) || (ltA n m).
End AOrder.
Module heap := finmap.map AOrder int_type.
Notation "k '---' l" := (heap.dif k l) (at level 69) : heap_scope.
Notation "k '+++' m" := (heap.union k m) (at level 69) : heap_scope.
Notation "k '#' m" := (heap.disj k m) (at level 79) : heap_scope.
Local Open Scope heap_scope.
Definition assert := store.t -> heap.t -> Prop.
Require while.
Definition TT : assert := while.TT store.t heap.t.
Definition FF : assert := while.FF store.t heap.t.
Definition Not (P : assert) : assert := while.Not P.
Notation "P '//\\' Q" := (while.And store.t heap.t P Q) (at level 80, no associativity) : seplog_assert_scope.
Notation "P '\\//' Q" := (while.Or store.t heap.t P Q) (at level 80, no associativity) : seplog_assert_scope.
Notation "P ===> Q" := (while.entails store.t heap.t P Q) (at level 90, no associativity) : seplog_assert_scope.
Notation "P <==> Q" := (while.equiv store.t heap.t P Q) (at level 90, no associativity) : seplog_assert_scope.
Local Open Scope seplog_assert_scope.
Delimit Scope seplog_assert_scope with seplog_assert.
Definition x_EQ_y (x y : var.v) : assert := fun s _ => [ x ]_ s = [ y ]_ s.
match e with
| true_b => true
| bop_b bo e1 e2 => binop_b_interp bo ([ e1 ]e_ s) ([ e2 ]e_ s)
| bop_b2 bo e1 e2 => binop_b2_interp bo (eval_b e1 s) (eval_b e2 s)
| ~e e => ~~ eval_b e s
end.
Notation "'[' e ']b_' s" := (eval_b e s) (at level 9) : seplog_expr_scope.
Notation " b1 =b> b2 " := ((~e b1) |e b2) (right associativity, at level 80) : seplog_expr_scope.
Lemma eval_b_neg : forall t s, [ ~e t ]b_s = ~~ [ t ]b_ s.
Lemma expr_b_neg_involutive : forall a s, [ ~e ~e a ]b_ s = [ a ]b_s.
Lemma expr_b_impl_intro: forall b1 b2 s, [ b1 ]b_s -> [ b1 =b> b2 ]b_s -> [ b2 ]b_s.
Fixpoint subst_b_lst (l : list (var.v * expr)) (e : expr_b) {struct l}: expr_b :=
match l with
| nil => e
| (x, e') :: tl => subst_b_lst tl (subst_b e (var_e x) e')
end.
Lemma eval_b_upd : forall b s v x, ~ In x (vars_b b) ->
[ b ]b_ (store.upd x v s) = [ b ]b_ s.
Lemma eval_b_proj : forall e s d, incl (vars_b e) (seq_ext.s2l d) ->
[ e ]b_ (store.store_heap.proj s d) = [ e ]b_ s.
Lemma eval_b_upds : forall e xs, disj (vars_b e) xs ->
forall s zs, [ e ]b_ (store.upds xs zs s) = [ e ]b_ s.
Lemma eval_b_upd_subst : forall b s x v,
[ b ]b_ (store.upd x ([ v ]e_ s) s) = [ subst_b b (var_e x) v ]b_s.
Fixpoint eval_b_Prop (e : expr_b) (s : store.t) : Prop :=
match e with
| true_b => True
| f =e g => [ f ]e_ s = [ g ]e_ s
| f <>e g => [ f ]e_ s <> [ g ]e_ s
| f >>= g => A.t_ge ([ f ]e_ s) ([ g ]e_ s)
| f >> g => A.t_gt ([ f ]e_ s) ([ g ]e_ s)
| f &e g => eval_b_Prop f s /\ eval_b_Prop g s
| f |e g => eval_b_Prop f s \/ eval_b_Prop g s
| neg_b e => ~ eval_b_Prop e s
end.
Lemma expr_bP : forall e s, [ e ]b_ s <-> eval_b_Prop e s.
Lemma expr_b_reflect: forall b1 b2 s,
([ b1 ]b_s <-> [ b2 ]b_s) -> [ b1 ]b_ s = [ b2 ]b_ s.
Lemma expr_b_reflect' : forall b1 b2 s,
[ b1 ]b_ s = [ b2 ]b_ s -> ([ b1 ]b_s <-> [ b2 ]b_s).
Ltac eval_b2Prop_hyp h :=
match goal with
| H : is_true (eval_b ?e ?s) |- _ =>
move: {H}(proj1 (expr_bP e _) H) => H; simpl in H
end.
Ltac eval_b2Prop_hyps :=
match goal with
| id : is_true (eval_b ?e ?s) |- _ => eval_b2Prop_hyp id; eval_b2Prop_hyps
| id : is_true (~~ eval_b ?e ?s) |- _ =>
rewrite <- eval_b_neg in id; eval_b2Prop_hyps
| |- _ => idtac
end.
Ltac eval_b2Prop_goal :=
match goal with
| |- is_true (eval_b ?e ?s) => apply (proj2 (expr_bP e s)); simpl
| |- is_true (~~ eval_b ?e ?s) =>
rewrite <- eval_b_neg;
eval_b2Prop_goal
| |- _ => idtac
end.
Ltac eval2Prop_hyp :=
match goal with
| h : context [ (eval (var_e ?e) ?s) ] |- _ =>
simpl in h
end.
Require Import omegaz.
Ltac omegab :=
eval_b2Prop_hyps ; eval_b2Prop_goal ;
repeat eval2Prop_hyp ;
(try tauto || omega ||
( (repeat open_integral_type_hyp);
open_integral_type_goal );
omegaz).
End Expr.
Module Assert (A : IntegralType).
Module Import expr_m := Expr A.
Local Open Scope seplog_expr_scope.
Canonical Structure t_eqMixin := EqMixin A.tP.
Canonical Structure t_eqType := Eval hnf in EqType _ t_eqMixin.
Module int_type <: EQTYPE.
Definition A : eqType := t_eqType.
End int_type.
Module AOrder <: ORDER.
Definition A := A.t.
Definition ltA : A -> A -> bool := fun a b => negb (A.t_geb a b).
Lemma ltA_trans : forall n m p, ltA m n -> ltA n p -> ltA m p.
Lemma ltA_irr : forall a, ltA a a = false.
Lemma ltA_total : forall m n, (m != n) = (ltA m n) || (ltA n m).
End AOrder.
Module heap := finmap.map AOrder int_type.
Notation "k '---' l" := (heap.dif k l) (at level 69) : heap_scope.
Notation "k '+++' m" := (heap.union k m) (at level 69) : heap_scope.
Notation "k '#' m" := (heap.disj k m) (at level 79) : heap_scope.
Local Open Scope heap_scope.
Definition assert := store.t -> heap.t -> Prop.
Require while.
Definition TT : assert := while.TT store.t heap.t.
Definition FF : assert := while.FF store.t heap.t.
Definition Not (P : assert) : assert := while.Not P.
Notation "P '//\\' Q" := (while.And store.t heap.t P Q) (at level 80, no associativity) : seplog_assert_scope.
Notation "P '\\//' Q" := (while.Or store.t heap.t P Q) (at level 80, no associativity) : seplog_assert_scope.
Notation "P ===> Q" := (while.entails store.t heap.t P Q) (at level 90, no associativity) : seplog_assert_scope.
Notation "P <==> Q" := (while.equiv store.t heap.t P Q) (at level 90, no associativity) : seplog_assert_scope.
Local Open Scope seplog_assert_scope.
Delimit Scope seplog_assert_scope with seplog_assert.
Definition x_EQ_y (x y : var.v) : assert := fun s _ => [ x ]_ s = [ y ]_ s.
The separation conjunction
Definition con (P Q : assert) : assert := fun s h =>
exists h1, exists h2, h1 # h2 /\ h = h1 +++ h2 /\ P s h1 /\ Q s h2.
Notation "P ** Q" := (con P Q) (at level 80) : seplog_assert_scope.
Lemma con_cons : forall (P Q : assert) s h1 h2, h1 # h2 ->
P s h1 -> Q s h2 -> (P ** Q) s (h1 +++ h2).
Lemma semi_distributivity : forall (P1 P2 Q : assert), (P1 //\\ P2) ** Q ===> (P1 ** Q) //\\ (P2 ** Q).
exists h1, exists h2, h1 # h2 /\ h = h1 +++ h2 /\ P s h1 /\ Q s h2.
Notation "P ** Q" := (con P Q) (at level 80) : seplog_assert_scope.
Lemma con_cons : forall (P Q : assert) s h1 h2, h1 # h2 ->
P s h1 -> Q s h2 -> (P ** Q) s (h1 +++ h2).
Lemma semi_distributivity : forall (P1 P2 Q : assert), (P1 //\\ P2) ** Q ===> (P1 ** Q) //\\ (P2 ** Q).
an assertion is said to be pure if, for any store, it is independent of the heap
Definition pure (Q : assert) := forall s h h', Q s h <-> Q s h'.
Lemma con_and_pure : forall (P Q R : assert), pure R -> (P ** Q) //\\ R ===> P ** (Q //\\ R).
Lemma con_and_pure : forall (P Q R : assert), pure R -> (P ** Q) //\\ R ===> P ** (Q //\\ R).
Extensionality of predicates can be safely added to Coq (see Coq FAQ)
Axiom assert_ext: forall P Q, P <==> Q -> P = Q.
Lemma And_com_equiv : forall P Q, (P //\\ Q) = (Q //\\ P).
Lemma con_com : forall P Q, P ** Q ===> Q ** P.
Lemma con_com_equiv : forall P Q, (P ** Q) = (Q ** P).
Lemma con_assoc: forall P Q R, (P ** Q) ** R ===> P ** (Q ** R).
Lemma con_assoc_equiv : forall P Q R, ((Q ** P) ** R) = (Q ** (P ** R)).
Lemma con_TT : forall P, P ===> P ** TT.
Lemma monotony : forall s s' h (P Q P' Q' : assert),
(forall h, P s h -> P' s' h) -> (forall h, Q s h -> Q' s' h) ->
(P ** Q) s h -> (P' ** Q') s' h.
Lemma monotony' : forall P1 P2 P3 P4,
P1 ===> P2 -> P3 ===> P4 -> P1 ** P3 ===> P2 ** P4.
Definition emp : assert := fun s h => h = heap.emp.
Lemma con_emp: forall P, P ** emp ===> P .
Lemma con_emp': forall P, P ===> P ** emp.
Lemma con_emp_equiv : forall P, (P ** emp) = P .
Lemma And_com_equiv : forall P Q, (P //\\ Q) = (Q //\\ P).
Lemma con_com : forall P Q, P ** Q ===> Q ** P.
Lemma con_com_equiv : forall P Q, (P ** Q) = (Q ** P).
Lemma con_assoc: forall P Q R, (P ** Q) ** R ===> P ** (Q ** R).
Lemma con_assoc_equiv : forall P Q R, ((Q ** P) ** R) = (Q ** (P ** R)).
Lemma con_TT : forall P, P ===> P ** TT.
Lemma monotony : forall s s' h (P Q P' Q' : assert),
(forall h, P s h -> P' s' h) -> (forall h, Q s h -> Q' s' h) ->
(P ** Q) s h -> (P' ** Q') s' h.
Lemma monotony' : forall P1 P2 P3 P4,
P1 ===> P2 -> P3 ===> P4 -> P1 ** P3 ===> P2 ** P4.
Definition emp : assert := fun s h => h = heap.emp.
Lemma con_emp: forall P, P ** emp ===> P .
Lemma con_emp': forall P, P ===> P ** emp.
Lemma con_emp_equiv : forall P, (P ** emp) = P .
The separation implication
Definition imp (P Q : assert) : assert := fun s h =>
forall h', h # h' /\ P s h' -> forall h'', h'' = h +++ h' -> Q s h''.
Notation "P -* Q" := (imp P Q) (at level 80) : seplog_assert_scope.
Lemma emp_imp : forall s h (P : assert), P s h -> (emp -* P) s h.
Lemma emp_imp_inv: forall s h (P : assert), (emp -* P) s h -> P s h .
Lemma mp : forall P Q, Q ** (Q -* P) ===> P.
Lemma pm : forall P Q, Q ===> P -* (P ** Q).
Lemma monotony_imp : forall s s' h (P Q P' Q' : assert),
(forall h, P' s' h -> P s h) ->
(forall h, Q s h -> Q' s' h) ->
(P -* Q) s h -> (P' -* Q') s' h.
Lemma monotony_imp': forall P1 P2 P3 P4,
P2 ===> P1 -> P3 ===> P4 -> P1 -* P3 ===> P2 -* P4.
Lemma currying : forall (P1 P2 P3 : assert) s,
(forall h, (P1 ** P2) s h -> P3 s h) ->
forall h, P1 s h -> (P2 -* P3) s h.
Lemma uncurrying : forall (P1 P2 P3 : assert) s,
(forall h, P1 s h -> (P2 -* P3) s h) ->
forall h, (P1 ** P2) s h -> P3 s h.
forall h', h # h' /\ P s h' -> forall h'', h'' = h +++ h' -> Q s h''.
Notation "P -* Q" := (imp P Q) (at level 80) : seplog_assert_scope.
Lemma emp_imp : forall s h (P : assert), P s h -> (emp -* P) s h.
Lemma emp_imp_inv: forall s h (P : assert), (emp -* P) s h -> P s h .
Lemma mp : forall P Q, Q ** (Q -* P) ===> P.
Lemma pm : forall P Q, Q ===> P -* (P ** Q).
Lemma monotony_imp : forall s s' h (P Q P' Q' : assert),
(forall h, P' s' h -> P s h) ->
(forall h, Q s h -> Q' s' h) ->
(P -* Q) s h -> (P' -* Q') s' h.
Lemma monotony_imp': forall P1 P2 P3 P4,
P2 ===> P1 -> P3 ===> P4 -> P1 -* P3 ===> P2 -* P4.
Lemma currying : forall (P1 P2 P3 : assert) s,
(forall h, (P1 ** P2) s h -> P3 s h) ->
forall h, P1 s h -> (P2 -* P3) s h.
Lemma uncurrying : forall (P1 P2 P3 : assert) s,
(forall h, P1 s h -> (P2 -* P3) s h) ->
forall h, (P1 ** P2) s h -> P3 s h.
Tactics to decompose / compose heaps related by separating conjonction
Ltac Heap_emp_clean :=
match goal with
| id: ?h = heap.emp |- _ => subst h; Heap_emp_clean
| id: emp ?s ?h |- _ => red in id; Heap_emp_clean
| id: heap.emp = ?h |- _ => subst h; Heap_emp_clean
| _ => idtac
end.
Ltac case_sepcon H :=
move: H ;
match goal with
| |- (con _ _) ?s ?h -> _ =>
let h1 := fresh h "1" in
let h2 := fresh h "2" in
let Hdisj := fresh h1 "_d_" h2 in
let Hunion := fresh h1 "_U_" h2 in
let Hh1 := fresh H "_" h1 in
let Hh2 := fresh H "_" h2 in
case => h1 [h2 [Hdisj [Hunion [Hh1 Hh2]]]]
end.
Module map_tac_m := Map_Tac heap.
Ltac Compose_sepcon id1 id2:=
exists id1; exists id2; split;
[Heap_emp_clean ; map_tac_m.Disj |
(split; [Heap_emp_clean; map_tac_m.Equal | split; idtac])].
Definition mapsto e e' s h := exists p, [ e ]e_ s = p /\ h = heap.sing p ([ e' ]e_s).
Notation "e1 '|~>' e2" := (mapsto e1 e2) (at level 77, no associativity) : seplog_assert_scope.
Lemma singl_equal: forall s h1 h2 e1 e2 e3 e4,
(e1 |~> e2) s h1 -> (e3 |~> e4) s h2 ->
[ e1 ]e_ s = [ e3 ]e_ s -> [ e2 ]e_ s = [ e4 ]e_ s -> h1 = h2.
Lemma singl_disj_neq : forall e1 e2 e3 e4 h1 h2 s,
(e1 |~> e2) s h1 -> (e3 |~> e4) s h2 -> h1 # h2 ->
[ e1 ]e_ s <> [ e3 ]e_ s.
Lemma mapsto_strictly_exact : forall e v Q s h,
(e |~> v ** TT) s h /\ Q s h -> (e |~> v ** (e |~> v -* Q)) s h.
Lemma mapsto_strictly_exact' : forall e v (Q : assert) s h1 h2,
Q s (h1 +++ h2) -> h1 # h2 -> (e |~> v) s h1 -> (e |~> v -* Q) s h2.
Lemma mapsto_store_upd_subst : forall e1 e2 x p s h,
(subst_e e1 (var_e x) (cst_e p) |~> subst_e e2 (var_e x) (cst_e p)) s h ->
(e1 |~> e2) (store.upd x p s) h.
Lemma mapsto_ext : forall s s' h e1' e2' e1 e2,
[ e1' ]e_ s' = [ e1 ]e_ s -> [ e2' ]e_ s' = [ e2 ]e_ s ->
(e1' |~> e2') s' h -> (e1 |~> e2) s h.
Definition cell_exists (e1 : expr) : assert := fun s h => exists y, (e1 |~> y) s h.
Notation " e '|~>_' " := (cell_exists e) (right associativity, at level 77) : seplog_assert_scope.
Lemma cell_exists_ext : forall s s' h e1 e2,
(e1 |~>_) s' h -> [ e1 ]e_s' = [ e2 ]e_s -> (e2 |~>_) s h.
Tactic to solve goals of the form: (e |~> e') s h
Ltac Mapsto :=
match goal with
| id: (?e1 |~> ?e2) ?s1 ?h |- (?e3 |~> ?e4) ?s2 ?h =>
apply (mapsto_ext s2 s1 h e1 e2 e3 e4) ;
[simpl; (omegab || (repeat Store_upd => //) || auto)|
simpl; (omegab || (repeat Store_upd => //) || auto) |
exact id]
| id: (?e1 |~>_) ?s1 ?h |- (?e3 |~>_) ?s2 ?h =>
apply (cell_exists_ext s2 s1 h e1 e3 id);
(simpl; (omegab || (repeat Store_upd => //) || auto))
end.
tactics to apply monotony and adjunction
Ltac assocs_sepcon :=
match goal with
| |- ?P -> _ => repeat rewrite con_assoc_equiv
end.
Ltac rotate_sepcon :=
match goal with
| |- ?P -> _ => rewrite con_com_equiv; assocs_sepcon
end.
Ltac try_monotony :=
match goal with
| |- (?P ** ?PP) ?S ?SS ?M ?H -> (?P ** ?QQ) ?S ?H =>
apply monotony; [intros; auto | intros; idtac]
| |- ((?L |~> ?V) ** ?PP) ?S ?H -> ((?K |~> ?W) ** ?QQ) ?S ?H =>
apply monotony; [intros; Mapsto | intros; idtac]
| |- (?P -* ?PP) ?S ?H -> (?Q -* ?QQ) ?S ?H =>
apply monotony_imp';
[rewrite /while.entails; intros; Mapsto |
rewrite /while.entails; intros; idtac]
| |- (?P ** ?PP) ?S ?H -> (?Q ** ?QQ) ?S ?H =>
rotate_sepcon; try_monotony
end.
Ltac Monotony Hyp := generalize Hyp; clear Hyp; try_monotony.
Fixpoint mapstos (e : expr) (l : list expr) {struct l} : assert :=
match l with
| List.nil => emp
| e1 :: tl => e |~> e1 ** mapstos (e +e cst_e (A.nat2t 1)) tl
end.
Notation "x '|-->' l" := (mapstos x l) (at level 77) : seplog_assert_scope.
Lemma mapstos_ext : forall l s h e' e, [ e' ]e_s = [ e ]e_s ->
(e' |--> l) s h -> (e |--> l) s h.
A specialization version of mapstos for lists of integers
Definition mapstos' (e : expr) (lst : list A.t) :=
mapstos e (List.map (fun x => cst_e x) lst).
Notation "x '|--->' l" := (mapstos' x l) (at level 77).
Lemma mapstos'_app_sepcon : forall l1 l2 st s h, (st |---> l1 ++ l2) s h ->
(st |---> l1 ** (st +e nat_e (length l1)) |---> l2) s h.
Lemma mapstos'_cons_sepcon: forall a l st s h, (st |---> a :: l) s h ->
(st |~> cst_e a ** (st +e nat_e 1) |---> l) s h.
Lemma mapstos'_sepcon_app : forall l1 l2 st s h,
(st |---> l1 ** (st +e nat_e (length l1)) |---> l2) s h ->
(st |---> l1 ++ l2) s h.
mapstos e (List.map (fun x => cst_e x) lst).
Notation "x '|--->' l" := (mapstos' x l) (at level 77).
Lemma mapstos'_app_sepcon : forall l1 l2 st s h, (st |---> l1 ++ l2) s h ->
(st |---> l1 ** (st +e nat_e (length l1)) |---> l2) s h.
Lemma mapstos'_cons_sepcon: forall a l st s h, (st |---> a :: l) s h ->
(st |~> cst_e a ** (st +e nat_e 1) |---> l) s h.
Lemma mapstos'_sepcon_app : forall l1 l2 st s h,
(st |---> l1 ** (st +e nat_e (length l1)) |---> l2) s h ->
(st |---> l1 ++ l2) s h.
independence of an assertion w.r.t. a list of variables
Definition inde (l : list var.v) (P : assert) := forall s h,
(forall x v, In x l -> (P s h <-> P (store.upd x v s) h)).
Lemma inde_upd_store : forall (P : assert) x z s h,
inde (x :: List.nil) P -> P s h -> P (store.upd x z s) h.
Local Open Scope nat_scope.
Lemma fresh_b_inde: forall b x v, fresh_b x b ->
inde (x :: nil) (fun s h => eval_b b s = v).
Local Close Scope nat_scope.
Lemma inde_TT : forall l, inde l TT.
Lemma inde_sep_con : forall l P Q, inde l P -> inde l Q -> inde l (P ** Q).
Lemma inde_sep_imp : forall l P Q, inde l P -> inde l Q -> inde l (P -* Q).
Lemma inde_mapsto : forall lst e e',
disj (vars e) lst -> disj (vars e') lst -> inde lst (e |~> e').
Lemma inde_mapstos : forall (l : list expr) (xs : list var.v) e,
disj (fold_right (@app var.v) nil (map vars l)) xs ->
disj (vars e) xs -> inde xs (e |--> l).
Lemma map_vars_list_expr : forall (l : list expr),
(forall e, In e l -> vars e = nil) -> map vars l = map (fun _ => nil) l.
Lemma inde_mapstos' : forall l xs p, disj (vars p) xs -> inde xs (p |---> l).
End Assert.
(forall x v, In x l -> (P s h <-> P (store.upd x v s) h)).
Lemma inde_upd_store : forall (P : assert) x z s h,
inde (x :: List.nil) P -> P s h -> P (store.upd x z s) h.
Local Open Scope nat_scope.
Lemma fresh_b_inde: forall b x v, fresh_b x b ->
inde (x :: nil) (fun s h => eval_b b s = v).
Local Close Scope nat_scope.
Lemma inde_TT : forall l, inde l TT.
Lemma inde_sep_con : forall l P Q, inde l P -> inde l Q -> inde l (P ** Q).
Lemma inde_sep_imp : forall l P Q, inde l P -> inde l Q -> inde l (P -* Q).
Lemma inde_mapsto : forall lst e e',
disj (vars e) lst -> disj (vars e') lst -> inde lst (e |~> e').
Lemma inde_mapstos : forall (l : list expr) (xs : list var.v) e,
disj (fold_right (@app var.v) nil (map vars l)) xs ->
disj (vars e) xs -> inde xs (e |--> l).
Lemma map_vars_list_expr : forall (l : list expr),
(forall e, In e l -> vars e = nil) -> map vars l = map (fun _ => nil) l.
Lemma inde_mapstos' : forall l xs p, disj (vars p) xs -> inde xs (p |---> l).
End Assert.