Hoare logic example : monotonicity proof

examples/hoare_logic/blocking_semantics3.mlw

@@ -23,6 +23,9 @@ type operator = Oplus | Ominus | Omult | Ole
 (** ident for mutable variables *)
 type mident
 
+axiom mident_decide :
+  forall m1 m2: mident. m1 = m2 \/ m1 <> m2
+
 (** ident for immutable variables *)
 type ident = {| ident_index : int |}
 
@@ -301,7 +304,7 @@ predicate fresh_in_term (id:ident) (t:term) =
   id.ident_index > t.term_maxvar
 
 lemma eval_msubst_term:
-  forall sigma:env, pi:stack, e:term, x:mident, v:ident.
+  forall e:term, sigma:env, pi:stack, x:mident, v:ident.
     fresh_in_term v e ->
     eval_term sigma pi (msubst_term e x v) =
     eval_term (IdMap.set sigma x (get_stack v pi)) pi e
@@ -355,6 +358,7 @@ lemma let_subst:
     forall t:term, f:fmla, x id':ident, id :mident.
     msubst (Flet x t f) id id' = Flet x (msubst_term t id id') (msubst f id id')
 
+(* Need it for monotonicity*)
 lemma eval_msubst:
   forall f:fmla, sigma:env, pi:stack, x:mident, v:ident.
     fresh_in_fmla v f ->
@@ -378,6 +382,7 @@ lemma eval_same_var:
     eval_fmla sigma (Cons (id,v1) (Cons (id,v2) pi)) f <->
     eval_fmla sigma (Cons (id,v1) pi) f
 
+  (* Need it for monotonicity*)
 lemma eval_change_free :
   forall f:fmla, sigma:env, pi:stack, id:ident, v:value.
     fresh_in_fmla id f ->
@@ -386,6 +391,7 @@ lemma eval_change_free :
 (** [valid_fmla f] is true when [f] is valid in any environment *)
   predicate valid_fmla (p:fmla) = forall sigma:env, pi:stack. eval_fmla sigma pi p
 
+(* Not needed *)
 axiom msubst_implies :
 forall p q:fmla.
   valid_fmla (Fimplies p q) ->
@@ -395,13 +401,6 @@ forall p q:fmla.
 
 (** let id' = t in f[id <- id'] <=> let id = t in f*)
 lemma let_equiv :
-  forall id:ident, id':ident, t:term, f:fmla.
-    forall sigma:env, pi:stack.
-      fresh_in_fmla id' f ->
-	(eval_fmla sigma pi (Flet id' t (subst f id id'))
-	 -> eval_fmla sigma pi (Flet id t f))
-
-lemma let_equiv2 :
   forall id:ident, id':ident, t:term, f:fmla.
     forall sigma:env, pi:stack.
       fresh_in_fmla id' f ->
@@ -666,6 +665,7 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
 
   function fresh_from (f:fmla) (s:stmt) : ident
 
+  (* Need it for monotonicity*)
   axiom fresh_from_fmla: forall s:stmt, f:fmla.
      fresh_in_fmla (fresh_from f s) f
 

examples/hoare_logic/blocking_semantics3/blocking_semantics3_ImpExpr_eval_bool_term_1.v

@@ -68,6 +68,9 @@ Axiom mident : Type.
 Parameter mident_WhyType : WhyType mident.
 Existing Instance mident_WhyType.
 
+Axiom mident_decide : forall (m1:mident) (m2:mident), (m1 = m2) \/
+  ~ (m1 = m2).
+
 (* Why3 assumption *)
 Inductive ident  :=
   | mk_ident : Z -> ident .

examples/hoare_logic/blocking_semantics3/blocking_semantics3_ImpExpr_eval_msubst_term_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require int.Int.
+Require int.MinMax.
+
+(* Why3 assumption *)
+Inductive list (a:Type) {a_WT:WhyType a} :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
+Existing Instance list_WhyType.
+Implicit Arguments Nil [[a] [a_WT]].
+Implicit Arguments Cons [[a] [a_WT]].
+
+Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type.
+Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
+  (b:Type) {b_WT:WhyType b}, WhyType (map a b).
+Existing Instance map_WhyType.
+
+Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
+  (map a b) -> a -> b.
+
+Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
+  (map a b) -> a -> b -> (map a b).
+
+Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
+  forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
+  ((get (set m a1 b1) a2) = b1).
+
+Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
+  {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
+  forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
+
+Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
+  b -> (map a b).
+
+Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
+  forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
+
+(* Why3 assumption *)
+Inductive datatype  :=
+  | TYunit : datatype 
+  | TYint : datatype 
+  | TYbool : datatype .
+Axiom datatype_WhyType : WhyType datatype.
+Existing Instance datatype_WhyType.
+
+(* Why3 assumption *)
+Inductive value  :=
+  | Vvoid : value 
+  | Vint : Z -> value 
+  | Vbool : bool -> value .
+Axiom value_WhyType : WhyType value.
+Existing Instance value_WhyType.
+
+(* Why3 assumption *)
+Inductive operator  :=
+  | Oplus : operator 
+  | Ominus : operator 
+  | Omult : operator 
+  | Ole : operator .
+Axiom operator_WhyType : WhyType operator.
+Existing Instance operator_WhyType.
+
+Axiom mident : Type.
+Parameter mident_WhyType : WhyType mident.
+Existing Instance mident_WhyType.
+
+Axiom mident_decide : forall (m1:mident) (m2:mident), (m1 = m2) \/
+  ~ (m1 = m2).
+
+(* Why3 assumption *)
+Inductive ident  :=
+  | mk_ident : Z -> ident .
+Axiom ident_WhyType : WhyType ident.
+Existing Instance ident_WhyType.
+
+(* Why3 assumption *)
+Definition ident_index(v:ident): Z := match v with
+  | (mk_ident x) => x
+  end.
+
+(* Why3 assumption *)
+Inductive term_node  :=
+  | Tvalue : value -> term_node 
+  | Tvar : ident -> term_node 
+  | Tderef : mident -> term_node 
+  | Tbin : term -> operator -> term -> term_node 
+  with term  :=
+  | mk_term : term_node -> Z -> term .
+Axiom term_WhyType : WhyType term.
+Existing Instance term_WhyType.
+
+Axiom term_node_WhyType : WhyType term_node.
+Existing Instance term_node_WhyType.
+
+(* Why3 assumption *)
+Definition term_maxvar(v:term): Z := match v with
+  | (mk_term x x1) => x1
+  end.
+
+(* Why3 assumption *)
+Definition term_node1(v:term): term_node :=
+  match v with
+  | (mk_term x x1) => x
+  end.
+
+(* Why3 assumption *)
+Fixpoint var_occurs_in_term(x:ident) (t:term) {struct t}: Prop :=
+  match t with
+  | (mk_term (Tvalue _) _) => False
+  | (mk_term (Tvar i) _) => (x = i)
+  | (mk_term (Tderef _) _) => False
+  | (mk_term (Tbin t1 _ t2) _) => (var_occurs_in_term x t1) \/
+      (var_occurs_in_term x t2)
+  end.
+
+(* Why3 assumption *)
+Definition term_inv(t:term): Prop := forall (x:ident), (var_occurs_in_term x
+  t) -> ((ident_index x) <= (term_maxvar t))%Z.
+
+(* Why3 assumption *)
+Definition mk_tvalue(v:value): term := (mk_term (Tvalue v) (-1%Z)%Z).
+
+Axiom mk_tvalue_inv : forall (v:value), (term_inv (mk_tvalue v)).
+
+(* Why3 assumption *)
+Definition mk_tvar(i:ident): term := (mk_term (Tvar i) (ident_index i)).
+
+Axiom mk_tvar_inv : forall (i:ident), (term_inv (mk_tvar i)).
+
+(* Why3 assumption *)
+Definition mk_tderef(r:mident): term := (mk_term (Tderef r) (-1%Z)%Z).
+
+Axiom mk_tderef_inv : forall (r:mident), (term_inv (mk_tderef r)).
+
+(* Why3 assumption *)
+Definition mk_tbin(t1:term) (o:operator) (t2:term): term := (mk_term (Tbin t1
+  o t2) (Zmax (term_maxvar t1) (term_maxvar t2))).
+
+Axiom mk_tbin_inv : forall (t1:term) (t2:term) (o:operator),
+  ((term_inv t1) /\ (term_inv t2)) -> (term_inv (mk_tbin t1 o t2)).
+
+(* Why3 assumption *)
+Inductive fmla  :=
+  | Fterm : term -> fmla 
+  | Fand : fmla -> fmla -> fmla 
+  | Fnot : fmla -> fmla 
+  | Fimplies : fmla -> fmla -> fmla 
+  | Flet : ident -> term -> fmla -> fmla 
+  | Fforall : ident -> datatype -> fmla -> fmla .
+Axiom fmla_WhyType : WhyType fmla.
+Existing Instance fmla_WhyType.
+
+(* Why3 assumption *)
+Inductive stmt  :=
+  | Sskip : stmt 
+  | Sassign : mident -> term -> stmt 
+  | Sseq : stmt -> stmt -> stmt 
+  | Sif : term -> stmt -> stmt -> stmt 
+  | Sassert : fmla -> stmt 
+  | Swhile : term -> fmla -> stmt -> stmt .
+Axiom stmt_WhyType : WhyType stmt.
+Existing Instance stmt_WhyType.
+
+Axiom decide_is_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
+
+(* Why3 assumption *)
+Definition type_value(v:value): datatype :=
+  match v with
+  | Vvoid => TYunit
+  | (Vint int) => TYint
+  | (Vbool bool1) => TYbool
+  end.
+
+(* Why3 assumption *)
+Inductive type_operator : operator -> datatype -> datatype
+  -> datatype -> Prop :=
+  | Type_plus : (type_operator Oplus TYint TYint TYint)
+  | Type_minus : (type_operator Ominus TYint TYint TYint)
+  | Type_mult : (type_operator Omult TYint TYint TYint)
+  | Type_le : (type_operator Ole TYint TYint TYbool).
+
+(* Why3 assumption *)
+Definition type_stack  := (list (ident* datatype)%type).
+
+Parameter get_vartype: ident -> (list (ident* datatype)%type) -> datatype.
+
+Axiom get_vartype_def : forall (i:ident) (pi:(list (ident* datatype)%type)),
+  match pi with
+  | Nil => ((get_vartype i pi) = TYunit)
+  | (Cons (x, ty) r) => ((x = i) -> ((get_vartype i pi) = ty)) /\
+      ((~ (x = i)) -> ((get_vartype i pi) = (get_vartype i r)))
+  end.
+
+(* Why3 assumption *)
+Definition type_env  := (map mident datatype).
+
+(* Why3 assumption *)
+Inductive type_term : (map mident datatype) -> (list (ident* datatype)%type)
+  -> term -> datatype -> Prop :=
+  | Type_value : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)) (v:value) (m:Z), (type_term sigma pi
+      (mk_term (Tvalue v) m) (type_value v))
+  | Type_var : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)) (v:ident) (m:Z) (ty:datatype), ((get_vartype v
+      pi) = ty) -> (type_term sigma pi (mk_term (Tvar v) m) ty)
+  | Type_deref : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)) (v:mident) (m:Z) (ty:datatype), ((get sigma
+      v) = ty) -> (type_term sigma pi (mk_term (Tderef v) m) ty)
+  | Type_bin : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)) (t1:term) (t2:term) (op:operator) (m:Z) (ty1:datatype)
+      (ty2:datatype) (ty:datatype), (type_term sigma pi t1 ty1) ->
+      ((type_term sigma pi t2 ty2) -> ((type_operator op ty1 ty2 ty) ->
+      (type_term sigma pi (mk_term (Tbin t1 op t2) m) ty))).
+
+(* Why3 assumption *)
+Inductive type_fmla : (map mident datatype) -> (list (ident* datatype)%type)
+  -> fmla -> Prop :=
+  | Type_term : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)) (t:term), (type_term sigma pi t TYbool) ->
+      (type_fmla sigma pi (Fterm t))
+  | Type_conj : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)) (f1:fmla) (f2:fmla), (type_fmla sigma pi f1) ->
+      ((type_fmla sigma pi f2) -> (type_fmla sigma pi (Fand f1 f2)))
+  | Type_neg : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)) (f:fmla), (type_fmla sigma pi f) -> (type_fmla sigma
+      pi (Fnot f))
+  | Type_implies : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)) (f1:fmla) (f2:fmla), (type_fmla sigma pi f1) ->
+      ((type_fmla sigma pi f2) -> (type_fmla sigma pi (Fimplies f1 f2)))
+  | Type_let : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)) (x:ident) (t:term) (f:fmla) (ty:datatype),
+      (type_term sigma pi t ty) -> ((type_fmla sigma (Cons (x, ty) pi) f) ->
+      (type_fmla sigma pi (Flet x t f)))
+  | Type_forall1 : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)) (x:ident) (f:fmla), (type_fmla sigma (Cons (x, TYint)
+      pi) f) -> (type_fmla sigma pi (Fforall x TYint f))
+  | Type_forall2 : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)) (x:ident) (f:fmla), (type_fmla sigma (Cons (x, TYbool)
+      pi) f) -> (type_fmla sigma pi (Fforall x TYbool f))
+  | Type_forall3 : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)) (x:ident) (f:fmla), (type_fmla sigma (Cons (x, TYunit)
+      pi) f) -> (type_fmla sigma pi (Fforall x TYunit f)).
+
+(* Why3 assumption *)
+Inductive type_stmt : (map mident datatype) -> (list (ident* datatype)%type)
+  -> stmt -> Prop :=
+  | Type_skip : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)), (type_stmt sigma pi Sskip)
+  | Type_seq : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)) (s1:stmt) (s2:stmt), (type_stmt sigma pi s1) ->
+      ((type_stmt sigma pi s2) -> (type_stmt sigma pi (Sseq s1 s2)))
+  | Type_assigns : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)) (x:mident) (t:term) (ty:datatype), ((get sigma
+      x) = ty) -> ((type_term sigma pi t ty) -> (type_stmt sigma pi
+      (Sassign x t)))
+  | Type_if : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)) (t:term) (s1:stmt) (s2:stmt), (type_term sigma pi t
+      TYbool) -> ((type_stmt sigma pi s1) -> ((type_stmt sigma pi s2) ->
+      (type_stmt sigma pi (Sif t s1 s2))))
+  | Type_assert : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)) (p:fmla), (type_fmla sigma pi p) -> (type_stmt sigma
+      pi (Sassert p))
+  | Type_while : forall (sigma:(map mident datatype)) (pi:(list (ident*
+      datatype)%type)) (guard:term) (body:stmt) (inv:fmla), (type_fmla sigma
+      pi inv) -> ((type_term sigma pi guard TYbool) -> ((type_stmt sigma pi
+      body) -> (type_stmt sigma pi (Swhile guard inv body)))).
+
+(* Why3 assumption *)
+Definition env  := (map mident value).
+
+(* Why3 assumption *)
+Definition stack  := (list (ident* value)%type).
+
+Parameter get_stack: ident -> (list (ident* value)%type) -> value.
+
+Axiom get_stack_def : forall (i:ident) (pi:(list (ident* value)%type)),
+  match pi with
+  | Nil => ((get_stack i pi) = Vvoid)
+  | (Cons (x, v) r) => ((x = i) -> ((get_stack i pi) = v)) /\ ((~ (x = i)) ->
+      ((get_stack i pi) = (get_stack i r)))
+  end.
+
+Axiom get_stack_eq : forall (x:ident) (v:value) (r:(list (ident*
+  value)%type)), ((get_stack x (Cons (x, v) r)) = v).
+
+Axiom get_stack_neq : forall (x:ident) (i:ident) (v:value) (r:(list (ident*
+  value)%type)), (~ (x = i)) -> ((get_stack i (Cons (x, v) r)) = (get_stack i
+  r)).
+
+Parameter eval_bin: value -> operator -> value -> value.
+
+Axiom eval_bin_def : forall (x:value) (op:operator) (y:value), match (x,
+  y) with
+  | ((Vint x1), (Vint y1)) =>
+      match op with
+      | Oplus => ((eval_bin x op y) = (Vint (x1 + y1)%Z))
+      | Ominus => ((eval_bin x op y) = (Vint (x1 - y1)%Z))
+      | Omult => ((eval_bin x op y) = (Vint (x1 * y1)%Z))
+      | Ole => ((x1 <= y1)%Z -> ((eval_bin x op y) = (Vbool true))) /\
+          ((~ (x1 <= y1)%Z) -> ((eval_bin x op y) = (Vbool false)))
+      end
+  | (_, _) => ((eval_bin x op y) = Vvoid)
+  end.
+
+(* Why3 assumption *)
+Fixpoint eval_term(sigma:(map mident value)) (pi:(list (ident* value)%type))
+  (t:term) {struct t}: value :=
+  match t with
+  | (mk_term (Tvalue v) _) => v
+  | (mk_term (Tvar id) _) => (get_stack id pi)
+  | (mk_term (Tderef id) _) => (get sigma id)
+  | (mk_term (Tbin t1 op t2) _) => (eval_bin (eval_term sigma pi t1) op
+      (eval_term sigma pi t2))
+  end.
+
+Axiom eval_bool_term : forall (sigma:(map mident value)) (pi:(list (ident*
+  value)%type)) (sigmat:(map mident datatype)) (pit:(list (ident*
+  datatype)%type)) (t:term), (type_term sigmat pit t TYbool) ->
+  exists b:bool, ((eval_term sigma pi t) = (Vbool b)).
+
+(* Why3 assumption *)
+Fixpoint eval_fmla(sigma:(map mident value)) (pi:(list (ident* value)%type))
+  (f:fmla) {struct f}: Prop :=
+  match f with
+  | (Fterm t) => ((eval_term sigma pi t) = (Vbool true))
+  | (Fand f1 f2) => (eval_fmla sigma pi f1) /\ (eval_fmla sigma pi f2)
+  | (Fnot f1) => ~ (eval_fmla sigma pi f1)
+  | (Fimplies f1 f2) => (eval_fmla sigma pi f1) -> (eval_fmla sigma pi f2)
+  | (Flet x t f1) => (eval_fmla sigma (Cons (x, (eval_term sigma pi t)) pi)
+      f1)
+  | (Fforall x TYint f1) => forall (n:Z), (eval_fmla sigma (Cons (x,
+      (Vint n)) pi) f1)
+  | (Fforall x TYbool f1) => forall (b:bool), (eval_fmla sigma (Cons (x,
+      (Vbool b)) pi) f1)
+  | (Fforall x TYunit f1) => (eval_fmla sigma (Cons (x, Vvoid) pi) f1)
+  end.
+
+Parameter msubst_term: term -> mident -> ident -> term.
+
+Axiom msubst_term_def : forall (t:term) (r:mident) (v:ident),
+  match t with
+  | (mk_term ((Tvalue _)|(Tvar _)) _) => ((msubst_term t r v) = t)
+  | (mk_term (Tderef x) _) => ((r = x) -> ((msubst_term t r
+      v) = (mk_tvar v))) /\ ((~ (r = x)) -> ((msubst_term t r v) = t))
+  | (mk_term (Tbin t1 op t2) _) => ((msubst_term t r
+      v) = (mk_tbin (msubst_term t1 r v) op (msubst_term t2 r v)))
+  end.
+
+Parameter subst_term: term -> ident -> ident -> term.
+
+Axiom subst_term_def : forall (t:term) (r:ident) (v:ident),
+  match t with
+  | (mk_term ((Tvalue _)|(Tderef _)) _) => ((subst_term t r v) = t)
+  | (mk_term (Tvar x) _) => ((r = x) -> ((subst_term t r
+      v) = (mk_tvar v))) /\ ((~ (r = x)) -> ((subst_term t r v) = t))
+  | (mk_term (Tbin t1 op t2) _) => ((subst_term t r
+      v) = (mk_tbin (subst_term t1 r v) op (subst_term t2 r v)))
+  end.
+
+(* Why3 assumption *)
+Definition fresh_in_term(id:ident) (t:term): Prop :=
+  ((term_maxvar t) < (ident_index id))%Z.
+
+Require Import Why3.
+
+Ltac ae := why3 "alt-ergo" timelimit 3.
+
+(* Why3 goal *)
+Theorem eval_msubst_term : forall (e:term) (sigma:(map mident value))
+  (pi:(list (ident* value)%type)) (x:mident) (v:ident), (fresh_in_term v
+  e) -> ((eval_term sigma pi (msubst_term e x v)) = (eval_term (set sigma x
+  (get_stack v pi)) pi e)).
+induction e.
+destruct t.
+(* Value *)
+ae.
+(* Var *)
+intros sigma pi x v H.
+simpl.
+rewrite (msubst_term_def (mk_term (Tvar i) z)).
+easy.
+(* Ref *)
+intros sigma pi x v H.
+simpl.
+destruct (mident_decide m x).
+(* m = x*)
+ae.
+(* m <> x*)
+ae.
+(* Bin *)
+(*Il manque le bon schema d'induction*)
+Qed.
+
+

examples/hoare_logic/blocking_semantics3/blocking_semantics3_WP_monotonicity_5.v

@@ -717,7 +717,17 @@ pose (id1 := fresh_from p (Sassign m t)).
 fold id1 in H.
 pose (id2 := fresh_from q (Sassign m t)).
 fold id2.
-
+rewrite eval_msubst.
+rewrite get_stack_eq.
+rewrite eval_change_free.
+apply H2.
+rewrite eval_msubst in H.
+rewrite get_stack_eq in H.
+rewrite eval_change_free in H; auto.
+apply fresh_from_fmla; auto.
+apply fresh_from_fmla; auto.
+apply fresh_from_fmla; auto.
+apply fresh_from_fmla; auto.
 Qed.
 
 

examples/hoare_logic/blocking_semantics3/blocking_semantics3_WP_progress_1.v

@@ -162,6 +162,8 @@ Inductive stmt  :=
 Axiom stmt_WhyType : WhyType stmt.
 Existing Instance stmt_WhyType.
 
+Axiom decide_is_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
+
 (* Why3 assumption *)
 Definition type_value(v:value): datatype :=
   match v with
@@ -312,6 +314,11 @@ Fixpoint eval_term(sigma:(map mident value)) (pi:(list (ident* value)%type))
       (eval_term sigma pi t2))
   end.
 
+Axiom eval_bool_term : forall (sigma:(map mident value)) (pi:(list (ident*
+  value)%type)) (sigmat:(map mident datatype)) (pit:(list (ident*
+  datatype)%type)) (t:term), (type_term sigmat pit t TYbool) ->
+  exists b:bool, ((eval_term sigma pi t) = (Vbool b)).
+
 (* Why3 assumption *)
 Fixpoint eval_fmla(sigma:(map mident value)) (pi:(list (ident* value)%type))
   (f:fmla) {struct f}: Prop :=
@@ -438,6 +445,11 @@ Axiom eval_change_free : forall (f:fmla) (sigma:(map mident value)) (pi:(list
 Definition valid_fmla(p:fmla): Prop := forall (sigma:(map mident value))
   (pi:(list (ident* value)%type)), (eval_fmla sigma pi p).
 
+Axiom msubst_implies : forall (p:fmla) (q:fmla), (valid_fmla (Fimplies p
+  q)) -> forall (sigma:(map mident value)) (pi:(list (ident* value)%type))
+  (x:mident) (id:ident), (fresh_in_fmla id (Fand p q)) -> (eval_fmla sigma
+  (Cons (id, (get sigma x)) pi) (Fimplies (msubst p x id) (msubst q x id))).
+
 Axiom let_equiv : forall (id:ident) (id':ident) (t:term) (f:fmla),
   forall (sigma:(map mident value)) (pi:(list (ident* value)%type)),
   (fresh_in_fmla id' f) -> ((eval_fmla sigma pi (Flet id' t (subst f id
@@ -492,7 +504,7 @@ Inductive one_step : (map mident value) -> (list (ident* value)%type) -> stmt
       value)%type)) (cond:term) (inv:fmla) (body:stmt), (eval_fmla sigma pi
       inv) -> (((eval_term sigma pi cond) = (Vbool true)) -> (one_step sigma
       pi (Swhile cond inv body) sigma pi (Sseq body (Swhile cond inv body))))
-  | one_step_while_falsee : forall (sigma:(map mident value)) (pi:(list
+  | one_step_while_false : forall (sigma:(map mident value)) (pi:(list
       (ident* value)%type)) (cond:term) (inv:fmla) (body:stmt),
       (eval_fmla sigma pi inv) -> (((eval_term sigma pi
       cond) = (Vbool false)) -> (one_step sigma pi (Swhile cond inv body)
@@ -658,6 +670,15 @@ Axiom fresh_from_stmt : forall (s:stmt) (f:fmla),
 
 Parameter abstract_effects: stmt -> fmla -> fmla.
 
+Axiom abstract_effects_generalize : forall (sigma:(map mident value))
+  (pi:(list (ident* value)%type)) (s:stmt) (f:fmla), (eval_fmla sigma pi
+  (abstract_effects s f)) -> (eval_fmla sigma pi f).
+
+Axiom abstract_effects_monotonic : forall (s:stmt) (f:fmla),