more proofs in hoare_logic/wp4

examples/hoare_logic/wp4.mlw

@@ -63,6 +63,14 @@ function get_stack (i:ident) (pi:stack) : value =
   | Cons (x,v) r -> if x=i then v else get_stack i r
   end
 
+lemma get_stack_eq:
+  forall x:ident, v:value, r:stack.
+    get_stack x (Cons (x,v) r) = v
+
+lemma get_stack_neq:
+  forall x i:ident, v:value, r:stack.
+    x <> i -> get_stack i (Cons (x,v) r) = get_stack i r 
+
 function eval_term (sigma:env) (pi:stack) (t:term) : value =
   match t with
   | Tvalue v -> v
@@ -228,7 +236,7 @@ inductive one_step env stack expr env stack expr =
 
   | one_step_while:
       forall sigma:env, pi:stack, e:expr, inv:fmla, e':expr.
-        one_step sigma pi (Ewhile e inv e') sigma pi 
+        one_step sigma pi (Ewhile e inv e') sigma pi
         (Eif e (Eseq e' (Ewhile e inv e')) void)
 
 (***
@@ -507,7 +515,7 @@ predicate expr_writes (i:expr) (w:Set.set ident) =
           (abstract_effects i
             (Fand
                 (Fimplies (Fand (Fterm e) inv) (wp i inv))
-                (Fimplies (Fand (Fnot (Fterm e)) inv) q))) 
+                (Fimplies (Fand (Fnot (Fterm e)) inv) q)))
 
     end
     { valid_triple result i q }

examples/hoare_logic/wp4/wp4_ImpExpr_eval_change_free_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Require int.Int.
+
+(* Why3 assumption *)
+Definition implb(x:bool) (y:bool): bool := match (x,
+  y) with
+  | (true, false) => false
+  | (_, _) => true
+  end.
+
+(* Why3 assumption *)
+Inductive datatype  :=
+  | TYunit : datatype 
+  | TYint : datatype 
+  | TYbool : datatype .
+
+(* Why3 assumption *)
+Inductive value  :=
+  | Vvoid : value 
+  | Vint : Z -> value 
+  | Vbool : bool -> value .
+
+(* Why3 assumption *)
+Inductive operator  :=
+  | Oplus : operator 
+  | Ominus : operator 
+  | Omult : operator 
+  | Ole : operator .
+
+(* Why3 assumption *)
+Definition ident  := Z.
+
+(* Why3 assumption *)
+Inductive term  :=
+  | Tvalue : value -> term 
+  | Tvar : Z -> term 
+  | Tderef : Z -> term 
+  | Tbin : term -> operator -> term -> term .
+
+(* Why3 assumption *)
+Inductive fmla  :=
+  | Fterm : term -> fmla 
+  | Fand : fmla -> fmla -> fmla 
+  | Fnot : fmla -> fmla 
+  | Fimplies : fmla -> fmla -> fmla 
+  | Flet : Z -> term -> fmla -> fmla 
+  | Fforall : Z -> datatype -> fmla -> fmla .
+
+Parameter map : forall (a:Type) (b:Type), Type.
+
+Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
+Implicit Arguments get.
+
+Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
+Implicit Arguments set.
+
+Axiom Select_eq : forall (a:Type) (b:Type), 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) (b:Type), 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 (b:Type) (a:Type), b -> (map a b).
+Set Contextual Implicit.
+Implicit Arguments const.
+Unset Contextual Implicit.
+
+Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
+  ((get (const b1:(map a b)) a1) = b1).
+
+(* Why3 assumption *)
+Definition env  := (map Z value).
+
+(* Why3 assumption *)
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Set Contextual Implicit.
+Implicit Arguments Nil.
+Unset Contextual Implicit.
+Implicit Arguments Cons.
+
+(* Why3 assumption *)
+Definition stack  := (list (Z* value)%type).
+
+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) = (Vbool false))
+  end.
+
+Parameter get_stack: Z -> (list (Z* value)%type) -> value.
+
+Axiom get_stack_def : forall (i:Z) (pi:(list (Z* 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:Z) (v:value) (r:(list (Z* value)%type)),
+  ((get_stack x (Cons (x, v) r)) = v).
+
+Axiom get_stack_neq : forall (x:Z) (i:Z) (v:value) (r:(list (Z*
+  value)%type)), (~ (x = i)) -> ((get_stack i (Cons (x, v) r)) = (get_stack i
+  r)).
+
+(* Why3 assumption *)
+Set Implicit Arguments.
+Fixpoint eval_term(sigma:(map Z value)) (pi:(list (Z* value)%type))
+  (t:term) {struct t}: value :=
+  match t with
+  | (Tvalue v) => v
+  | (Tvar id) => (get_stack id pi)
+  | (Tderef id) => (get sigma id)
+  | (Tbin t1 op t2) => (eval_bin (eval_term sigma pi t1) op (eval_term sigma
+      pi t2))
+  end.
+Unset Implicit Arguments.
+
+(* Why3 assumption *)
+Set Implicit Arguments.
+Fixpoint eval_fmla(sigma:(map Z value)) (pi:(list (Z* 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.
+Unset Implicit Arguments.
+
+Parameter subst_term: term -> Z -> Z -> term.
+
+Axiom subst_term_def : forall (e:term) (r:Z) (v:Z),
+  match e with
+  | ((Tvalue _)|(Tvar _)) => ((subst_term e r v) = e)
+  | (Tderef x) => ((r = x) -> ((subst_term e r v) = (Tvar v))) /\
+      ((~ (r = x)) -> ((subst_term e r v) = e))
+  | (Tbin e1 op e2) => ((subst_term e r v) = (Tbin (subst_term e1 r v) op
+      (subst_term e2 r v)))
+  end.
+
+(* Why3 assumption *)
+Set Implicit Arguments.
+Fixpoint fresh_in_term(id:Z) (t:term) {struct t}: Prop :=
+  match t with
+  | (Tvalue _) => True
+  | (Tvar v) => ~ (id = v)
+  | (Tderef _) => True
+  | (Tbin t1 _ t2) => (fresh_in_term id t1) /\ (fresh_in_term id t2)
+  end.
+Unset Implicit Arguments.
+
+Axiom eval_subst_term : forall (sigma:(map Z value)) (pi:(list (Z*
+  value)%type)) (e:term) (x:Z) (v:Z), (fresh_in_term v e) ->
+  ((eval_term sigma pi (subst_term e x v)) = (eval_term (set sigma x
+  (get_stack v pi)) pi e)).
+
+Axiom eval_term_change_free : forall (t:term) (sigma:(map Z value)) (pi:(list
+  (Z* value)%type)) (id:Z) (v:value), (fresh_in_term id t) ->
+  ((eval_term sigma (Cons (id, v) pi) t) = (eval_term sigma pi t)).
+
+(* Why3 assumption *)
+Set Implicit Arguments.
+Fixpoint fresh_in_fmla(id:Z) (f:fmla) {struct f}: Prop :=
+  match f with
+  | (Fterm e) => (fresh_in_term id e)
+  | ((Fand f1 f2)|(Fimplies f1 f2)) => (fresh_in_fmla id f1) /\
+      (fresh_in_fmla id f2)
+  | (Fnot f1) => (fresh_in_fmla id f1)
+  | (Flet y t f1) => (~ (id = y)) /\ ((fresh_in_term id t) /\
+      (fresh_in_fmla id f1))
+  | (Fforall y ty f1) => (~ (id = y)) /\ (fresh_in_fmla id f1)
+  end.
+Unset Implicit Arguments.
+
+(* Why3 assumption *)
+Set Implicit Arguments.
+Fixpoint subst(f:fmla) (x:Z) (v:Z) {struct f}: fmla :=
+  match f with
+  | (Fterm e) => (Fterm (subst_term e x v))
+  | (Fand f1 f2) => (Fand (subst f1 x v) (subst f2 x v))
+  | (Fnot f1) => (Fnot (subst f1 x v))
+  | (Fimplies f1 f2) => (Fimplies (subst f1 x v) (subst f2 x v))
+  | (Flet y t f1) => (Flet y (subst_term t x v) (subst f1 x v))
+  | (Fforall y ty f1) => (Fforall y ty (subst f1 x v))
+  end.
+Unset Implicit Arguments.
+
+Axiom eval_subst : forall (f:fmla) (sigma:(map Z value)) (pi:(list (Z*
+  value)%type)) (x:Z) (v:Z), (fresh_in_fmla v f) -> ((eval_fmla sigma pi
+  (subst f x v)) <-> (eval_fmla (set sigma x (get_stack v pi)) pi f)).
+
+Axiom eval_swap : forall (f:fmla) (sigma:(map Z value)) (pi:(list (Z*
+  value)%type)) (id1:Z) (id2:Z) (v1:value) (v2:value), (~ (id1 = id2)) ->
+  ((eval_fmla sigma (Cons (id1, v1) (Cons (id2, v2) pi)) f) <->
+  (eval_fmla sigma (Cons (id2, v2) (Cons (id1, v1) pi)) f)).
+
+Require Import Why3.
+Ltac ae := why3 "alt-ergo" timelimit 2.
+
+(* Why3 goal *)
+Theorem eval_change_free : forall (f:fmla) (sigma:(map Z value)) (pi:(list
+  (Z* value)%type)) (id:Z) (v:value), (fresh_in_fmla id f) ->
+  ((eval_fmla sigma (Cons (id, v) pi) f) <-> (eval_fmla sigma pi f)).
+
+induction f.
+ae.
+ae.
+ae.
+ae.
+ae.
+
+intros sigma pi id v.
+simpl.
+intros (hdiff & h).
+destruct d.
+ae.
+
+split.
+intros h1 n; generalize (h1 n); ae.
+ae.
+
+split.
+intros h1 n; generalize (h1 n); ae.
+ae.
+Qed.
+
+

examples/hoare_logic/wp4/wp4_ImpExpr_eval_subst_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Require int.Int.
+
+(* Why3 assumption *)
+Definition implb(x:bool) (y:bool): bool := match (x,
+  y) with
+  | (true, false) => false
+  | (_, _) => true
+  end.
+
+(* Why3 assumption *)
+Inductive datatype  :=
+  | TYunit : datatype 
+  | TYint : datatype 
+  | TYbool : datatype .
+
+(* Why3 assumption *)
+Inductive value  :=
+  | Vvoid : value 
+  | Vint : Z -> value 
+  | Vbool : bool -> value .
+
+(* Why3 assumption *)
+Inductive operator  :=
+  | Oplus : operator 
+  | Ominus : operator 
+  | Omult : operator 
+  | Ole : operator .
+
+(* Why3 assumption *)
+Definition ident  := Z.
+
+(* Why3 assumption *)
+Inductive term  :=
+  | Tvalue : value -> term 
+  | Tvar : Z -> term 
+  | Tderef : Z -> term 
+  | Tbin : term -> operator -> term -> term .
+
+(* Why3 assumption *)
+Inductive fmla  :=
+  | Fterm : term -> fmla 
+  | Fand : fmla -> fmla -> fmla 
+  | Fnot : fmla -> fmla 
+  | Fimplies : fmla -> fmla -> fmla 
+  | Flet : Z -> term -> fmla -> fmla 
+  | Fforall : Z -> datatype -> fmla -> fmla .
+
+Parameter map : forall (a:Type) (b:Type), Type.
+
+Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
+Implicit Arguments get.
+
+Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
+Implicit Arguments set.
+
+Axiom Select_eq : forall (a:Type) (b:Type), 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) (b:Type), 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 (b:Type) (a:Type), b -> (map a b).
+Set Contextual Implicit.
+Implicit Arguments const.
+Unset Contextual Implicit.
+
+Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
+  ((get (const b1:(map a b)) a1) = b1).
+
+(* Why3 assumption *)
+Definition env  := (map Z value).
+
+(* Why3 assumption *)
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Set Contextual Implicit.
+Implicit Arguments Nil.
+Unset Contextual Implicit.
+Implicit Arguments Cons.
+
+(* Why3 assumption *)
+Definition stack  := (list (Z* value)%type).
+
+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) = (Vbool false))
+  end.
+
+Parameter get_stack: Z -> (list (Z* value)%type) -> value.
+
+Axiom get_stack_def : forall (i:Z) (pi:(list (Z* 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:Z) (v:value) (r:(list (Z* value)%type)),
+  ((get_stack x (Cons (x, v) r)) = v).
+
+Axiom get_stack_neq : forall (x:Z) (i:Z) (v:value) (r:(list (Z*
+  value)%type)), (~ (x = i)) -> ((get_stack i (Cons (x, v) r)) = (get_stack i
+  r)).
+
+(* Why3 assumption *)
+Set Implicit Arguments.
+Fixpoint eval_term(sigma:(map Z value)) (pi:(list (Z* value)%type))
+  (t:term) {struct t}: value :=
+  match t with
+  | (Tvalue v) => v
+  | (Tvar id) => (get_stack id pi)
+  | (Tderef id) => (get sigma id)
+  | (Tbin t1 op t2) => (eval_bin (eval_term sigma pi t1) op (eval_term sigma
+      pi t2))
+  end.
+Unset Implicit Arguments.
+
+(* Why3 assumption *)
+Set Implicit Arguments.
+Fixpoint eval_fmla(sigma:(map Z value)) (pi:(list (Z* 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.
+Unset Implicit Arguments.
+
+Parameter subst_term: term -> Z -> Z -> term.
+
+Axiom subst_term_def : forall (e:term) (r:Z) (v:Z),
+  match e with
+  | ((Tvalue _)|(Tvar _)) => ((subst_term e r v) = e)
+  | (Tderef x) => ((r = x) -> ((subst_term e r v) = (Tvar v))) /\
+      ((~ (r = x)) -> ((subst_term e r v) = e))
+  | (Tbin e1 op e2) => ((subst_term e r v) = (Tbin (subst_term e1 r v) op
+      (subst_term e2 r v)))
+  end.
+
+(* Why3 assumption *)
+Set Implicit Arguments.
+Fixpoint fresh_in_term(id:Z) (t:term) {struct t}: Prop :=
+  match t with
+  | (Tvalue _) => True
+  | (Tvar v) => ~ (id = v)
+  | (Tderef _) => True
+  | (Tbin t1 _ t2) => (fresh_in_term id t1) /\ (fresh_in_term id t2)
+  end.
+Unset Implicit Arguments.
+
+Axiom eval_subst_term : forall (sigma:(map Z value)) (pi:(list (Z*
+  value)%type)) (e:term) (x:Z) (v:Z), (fresh_in_term v e) ->
+  ((eval_term sigma pi (subst_term e x v)) = (eval_term (set sigma x
+  (get_stack v pi)) pi e)).
+
+Axiom eval_term_change_free : forall (t:term) (sigma:(map Z value)) (pi:(list
+  (Z* value)%type)) (id:Z) (v:value), (fresh_in_term id t) ->
+  ((eval_term sigma (Cons (id, v) pi) t) = (eval_term sigma pi t)).
+
+(* Why3 assumption *)
+Set Implicit Arguments.
+Fixpoint fresh_in_fmla(id:Z) (f:fmla) {struct f}: Prop :=
+  match f with
+  | (Fterm e) => (fresh_in_term id e)
+  | ((Fand f1 f2)|(Fimplies f1 f2)) => (fresh_in_fmla id f1) /\
+      (fresh_in_fmla id f2)
+  | (Fnot f1) => (fresh_in_fmla id f1)
+  | (Flet y t f1) => (~ (id = y)) /\ ((fresh_in_term id t) /\
+      (fresh_in_fmla id f1))
+  | (Fforall y ty f1) => (~ (id = y)) /\ (fresh_in_fmla id f1)
+  end.
+Unset Implicit Arguments.
+
+(* Why3 assumption *)
+Set Implicit Arguments.
+Fixpoint subst(f:fmla) (x:Z) (v:Z) {struct f}: fmla :=
+  match f with
+  | (Fterm e) => (Fterm (subst_term e x v))
+  | (Fand f1 f2) => (Fand (subst f1 x v) (subst f2 x v))
+  | (Fnot f1) => (Fnot (subst f1 x v))
+  | (Fimplies f1 f2) => (Fimplies (subst f1 x v) (subst f2 x v))
+  | (Flet y t f1) => (Flet y (subst_term t x v) (subst f1 x v))
+  | (Fforall y ty f1) => (Fforall y ty (subst f1 x v))
+  end.
+Unset Implicit Arguments.
+
+Require Import Why3.
+Ltac ae := why3 "alt-ergo" timelimit 2.
+
+(* Why3 goal *)
+Theorem eval_subst : forall (f:fmla) (sigma:(map Z value)) (pi:(list (Z*
+  value)%type)) (x:Z) (v:Z), (fresh_in_fmla v f) -> ((eval_fmla sigma pi
+  (subst f x v)) <-> (eval_fmla (set sigma x (get_stack v pi)) pi f)).
+induction f.
+ae.
+ae.
+ae.
+ae.
+ae.
+intros sigma pi x v.
+simpl; intros (F1&F2).
+destruct d; ae.
+Qed.
+
+

examples/hoare_logic/wp4/wp4_ImpExpr_eval_subst_term_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Require int.Int.
+
+(* Why3 assumption *)
+Definition implb(x:bool) (y:bool): bool := match (x,
+  y) with
+  | (true, false) => false
+  | (_, _) => true
+  end.
+
+(* Why3 assumption *)
+Inductive datatype  :=
+  | TYunit : datatype 
+  | TYint : datatype 
+  | TYbool : datatype .
+
+(* Why3 assumption *)
+Inductive value  :=
+  | Vvoid : value 
+  | Vint : Z -> value 
+  | Vbool : bool -> value .
+
+(* Why3 assumption *)
+Inductive operator  :=
+  | Oplus : operator 
+  | Ominus : operator 
+  | Omult : operator 
+  | Ole : operator .
+
+(* Why3 assumption *)
+Definition ident  := Z.
+
+(* Why3 assumption *)
+Inductive term  :=
+  | Tvalue : value -> term 
+  | Tvar : Z -> term 
+  | Tderef : Z -> term 
+  | Tbin : term -> operator -> term -> term .
+
+(* Why3 assumption *)
+Inductive fmla  :=
+  | Fterm : term -> fmla 
+  | Fand : fmla -> fmla -> fmla 
+  | Fnot : fmla -> fmla 
+  | Fimplies : fmla -> fmla -> fmla 
+  | Flet : Z -> term -> fmla -> fmla 
+  | Fforall : Z -> datatype -> fmla -> fmla .
+
+Parameter map : forall (a:Type) (b:Type), Type.
+
+Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
+Implicit Arguments get.
+
+Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
+Implicit Arguments set.
+
+Axiom Select_eq : forall (a:Type) (b:Type), 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) (b:Type), 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 (b:Type) (a:Type), b -> (map a b).
+Set Contextual Implicit.
+Implicit Arguments const.
+Unset Contextual Implicit.
+
+Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
+  ((get (const b1:(map a b)) a1) = b1).
+
+(* Why3 assumption *)
+Definition env  := (map Z value).
+
+(* Why3 assumption *)
+Inductive list (a:Type) :=
+  | Nil : list a
+  | Cons : a -> (list a) -> list a.
+Set Contextual Implicit.
+Implicit Arguments Nil.
+Unset Contextual Implicit.
+Implicit Arguments Cons.
+
+(* Why3 assumption *)
+Definition stack  := (list (Z* value)%type).
+
+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) = (Vbool false))
+  end.
+
+Parameter get_stack: Z -> (list (Z* value)%type) -> value.
+
+Axiom get_stack_def : forall (i:Z) (pi:(list (Z* 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.
+
+(* Why3 assumption *)
+Set Implicit Arguments.
+Fixpoint eval_term(sigma:(map Z value)) (pi:(list (Z* value)%type))
+  (t:term) {struct t}: value :=
+  match t with
+  | (Tvalue v) => v
+  | (Tvar id) => (get_stack id pi)
+  | (Tderef id) => (get sigma id)
+  | (Tbin t1 op t2) => (eval_bin (eval_term sigma pi t1) op (eval_term sigma
+      pi t2))
+  end.
+Unset Implicit Arguments.
+
+(* Why3 assumption *)
+Set Implicit Arguments.
+Fixpoint eval_fmla(sigma:(map Z value)) (pi:(list (Z* 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)