preuves avec typage

examples/hoare_logic/blocking_semantics/blocking_semantics_WP_progress_1.v

@@ -213,9 +213,9 @@ Unset Implicit Arguments.
 Axiom subst_fresh : forall (f:fmla) (x:ident) (v:ident), (fresh_in_fmla x
   f) -> ((subst f x v) = f).
 
-Axiom let_subst : forall (t:term) (f:fmla) (x:ident) (id:ident) (idqt:ident),
-  ((subst (Flet x t f) id idqt) = (Flet x (subst_term t id idqt) (subst f id
-  idqt))).
+Axiom let_subst : forall (t:term) (f:fmla) (x:ident) (id:ident) (id':ident),
+  ((subst (Flet x t f) id id') = (Flet x (subst_term t id id') (subst f id
+  id'))).
 
 Axiom eval_subst : forall (f:fmla) (sigma:(map ident value)) (pi:(list
   (ident* value)%type)) (x:ident) (v:ident), (fresh_in_fmla v f) ->
@@ -235,9 +235,9 @@ Axiom eval_change_free : forall (f:fmla) (sigma:(map ident value)) (pi:(list
 Definition valid_fmla(p:fmla): Prop := forall (sigma:(map ident value))
   (pi:(list (ident* value)%type)), (eval_fmla sigma pi p).
 
-Axiom let_equiv : forall (id:ident) (idqt:ident) (t:term) (f:fmla),
+Axiom let_equiv : forall (id:ident) (id':ident) (t:term) (f:fmla),
   forall (sigma:(map ident value)) (pi:(list (ident* value)%type)),
-  (eval_fmla sigma pi (Flet idqt t (subst f id idqt))) -> (eval_fmla sigma pi
+  (eval_fmla sigma pi (Flet id' t (subst f id id'))) -> (eval_fmla sigma pi
   (Flet id t f)).
 
 (* Why3 assumption *)
@@ -282,50 +282,49 @@ Inductive one_step : (map ident value) -> (list (ident* value)%type) -> expr
   | one_step_deref : forall (sigma:(map ident value)) (pi:(list (ident*
       value)%type)) (v:ident), (one_step sigma pi (Ederef v) sigma pi
       (Evalue (get sigma v)))
-  | one_step_bin_ctxt1 : forall (sigma:(map ident value)) (sigmaqt:(map ident
-      value)) (pi:(list (ident* value)%type)) (piqt:(list (ident*
-      value)%type)) (op:operator) (e1:expr) (e1qt:expr) (e2:expr),
-      (one_step sigma pi e1 sigmaqt piqt e1qt) -> (one_step sigma pi (Ebin e1
-      op e2) sigmaqt piqt (Ebin e1qt op e2))
-  | one_step_bin_ctxt2 : forall (sigma:(map ident value)) (sigmaqt:(map ident
-      value)) (pi:(list (ident* value)%type)) (piqt:(list (ident*
-      value)%type)) (op:operator) (v1:value) (e2:expr) (e2qt:expr),
-      (one_step sigma pi e2 sigmaqt piqt e2qt) -> (one_step sigma pi
-      (Ebin (Evalue v1) op e2) sigmaqt piqt (Ebin (Evalue v1) op e2qt))
-  | one_step_bin_value : forall (sigma:(map ident value)) (sigmaqt:(map ident
-      value)) (pi:(list (ident* value)%type)) (piqt:(list (ident*
+  | one_step_bin_ctxt1 : forall (sigma:(map ident value)) (sigma':(map ident
+      value)) (pi:(list (ident* value)%type)) (pi':(list (ident*
+      value)%type)) (op:operator) (e1:expr) (e1':expr) (e2:expr),
+      (one_step sigma pi e1 sigma' pi' e1') -> (one_step sigma pi (Ebin e1 op
+      e2) sigma' pi' (Ebin e1' op e2))
+  | one_step_bin_ctxt2 : forall (sigma:(map ident value)) (sigma':(map ident
+      value)) (pi:(list (ident* value)%type)) (pi':(list (ident*
+      value)%type)) (op:operator) (v1:value) (e2:expr) (e2':expr),
+      (one_step sigma pi e2 sigma' pi' e2') -> (one_step sigma pi
+      (Ebin (Evalue v1) op e2) sigma' pi' (Ebin (Evalue v1) op e2'))
+  | one_step_bin_value : forall (sigma:(map ident value)) (sigma':(map ident
+      value)) (pi:(list (ident* value)%type)) (pi':(list (ident*
       value)%type)) (op:operator) (v1:value) (v2:value), (one_step sigma pi
-      (Ebin (Evalue v1) op (Evalue v2)) sigmaqt piqt (Evalue (eval_bin v1 op
+      (Ebin (Evalue v1) op (Evalue v2)) sigma' pi' (Evalue (eval_bin v1 op
       v2)))
-  | one_step_assign_ctxt : forall (sigma:(map ident value)) (sigmaqt:(map
-      ident value)) (pi:(list (ident* value)%type)) (piqt:(list (ident*
-      value)%type)) (x:ident) (e:expr) (eqt:expr), (one_step sigma pi e
-      sigmaqt piqt eqt) -> (one_step sigma pi (Eassign x e) sigmaqt piqt
-      (Eassign x eqt))
+  | one_step_assign_ctxt : forall (sigma:(map ident value)) (sigma':(map
+      ident value)) (pi:(list (ident* value)%type)) (pi':(list (ident*
+      value)%type)) (x:ident) (e:expr) (e':expr), (one_step sigma pi e sigma'
+      pi' e') -> (one_step sigma pi (Eassign x e) sigma' pi' (Eassign x e'))
   | one_step_assign_value : forall (sigma:(map ident value)) (pi:(list
       (ident* value)%type)) (x:ident) (v:value), (one_step sigma pi
       (Eassign x (Evalue v)) (set sigma x v) pi (Evalue Vvoid))
-  | one_step_seq_ctxt : forall (sigma:(map ident value)) (sigmaqt:(map ident
-      value)) (pi:(list (ident* value)%type)) (piqt:(list (ident*
-      value)%type)) (e1:expr) (e1qt:expr) (e2:expr), (one_step sigma pi e1
-      sigmaqt piqt e1qt) -> (one_step sigma pi (Eseq e1 e2) sigmaqt piqt
-      (Eseq e1qt e2))
+  | one_step_seq_ctxt : forall (sigma:(map ident value)) (sigma':(map ident
+      value)) (pi:(list (ident* value)%type)) (pi':(list (ident*
+      value)%type)) (e1:expr) (e1':expr) (e2:expr), (one_step sigma pi e1
+      sigma' pi' e1') -> (one_step sigma pi (Eseq e1 e2) sigma' pi' (Eseq e1'
+      e2))
   | one_step_seq_value : forall (sigma:(map ident value)) (pi:(list (ident*
       value)%type)) (e:expr), (one_step sigma pi (Eseq (Evalue Vvoid) e)
       sigma pi e)
-  | one_step_let_ctxt : forall (sigma:(map ident value)) (sigmaqt:(map ident
-      value)) (pi:(list (ident* value)%type)) (piqt:(list (ident*
-      value)%type)) (id:ident) (e1:expr) (e1qt:expr) (e2:expr),
-      (one_step sigma pi e1 sigmaqt piqt e1qt) -> (one_step sigma pi (Elet id
-      e1 e2) sigmaqt piqt (Elet id e1qt e2))
+  | one_step_let_ctxt : forall (sigma:(map ident value)) (sigma':(map ident
+      value)) (pi:(list (ident* value)%type)) (pi':(list (ident*
+      value)%type)) (id:ident) (e1:expr) (e1':expr) (e2:expr),
+      (one_step sigma pi e1 sigma' pi' e1') -> (one_step sigma pi (Elet id e1
+      e2) sigma' pi' (Elet id e1' e2))
   | one_step_let_value : forall (sigma:(map ident value)) (pi:(list (ident*
       value)%type)) (id:ident) (v:value) (e:expr), (one_step sigma pi
       (Elet id (Evalue v) e) sigma (Cons (id, v) pi) e)
-  | one_step_if_ctxt : forall (sigma:(map ident value)) (sigmaqt:(map ident
-      value)) (pi:(list (ident* value)%type)) (piqt:(list (ident*
-      value)%type)) (e1:expr) (e1qt:expr) (e2:expr) (e3:expr),
-      (one_step sigma pi e1 sigmaqt piqt e1qt) -> (one_step sigma pi (Eif e1
-      e2 e3) sigmaqt piqt (Eif e1qt e2 e3))
+  | one_step_if_ctxt : forall (sigma:(map ident value)) (sigma':(map ident
+      value)) (pi:(list (ident* value)%type)) (pi':(list (ident*
+      value)%type)) (e1:expr) (e1':expr) (e2:expr) (e3:expr), (one_step sigma
+      pi e1 sigma' pi' e1') -> (one_step sigma pi (Eif e1 e2 e3) sigma' pi'
+      (Eif e1' e2 e3))
   | one_step_if_true : forall (sigma:(map ident value)) (pi:(list (ident*
       value)%type)) (e1:expr) (e2:expr), (one_step sigma pi
       (Eif (Evalue (Vbool true)) e1 e2) sigma pi e1)
@@ -375,26 +374,25 @@ Axiom many_steps_let : forall (sigma1:(map ident value)) (sigma3:(map ident
   n1) /\ ((many_steps sigma2 (Cons (id, v1) pi2) e2 sigma3 pi3 (Evalue v2)
   n2) /\ (n = ((1%Z + n1)%Z + n2)%Z)).
 
-Axiom one_step_change_free : forall (e:expr) (eqt:expr) (sigma:(map ident
-  value)) (sigmaqt:(map ident value)) (pi:(list (ident* value)%type))
-  (piqt:(list (ident* value)%type)) (id:ident) (v:value), (fresh_in_expr id
-  e) -> ((one_step sigma (Cons (id, v) pi) e sigmaqt piqt eqt) ->
-  (one_step sigma pi e sigmaqt piqt eqt)).
+Axiom one_step_change_free : forall (e:expr) (e':expr) (sigma:(map ident
+  value)) (sigma':(map ident value)) (pi:(list (ident* value)%type))
+  (pi':(list (ident* value)%type)) (id:ident) (v:value), (fresh_in_expr id
+  e) -> ((one_step sigma (Cons (id, v) pi) e sigma' pi' e') ->
+  (one_step sigma pi e sigma' pi' e')).
 
 (* Why3 assumption *)
 Definition valid_triple(p:fmla) (e:expr) (q:fmla): Prop := forall (sigma:(map
   ident value)) (pi:(list (ident* value)%type)), (eval_fmla sigma pi p) ->
-  forall (sigmaqt:(map ident value)) (piqt:(list (ident* value)%type))
-  (v:value) (n:Z), (many_steps sigma pi e sigmaqt piqt (Evalue v) n) ->
-  (eval_fmla sigmaqt (Cons (result, v) piqt) q).
+  forall (sigma':(map ident value)) (pi':(list (ident* value)%type))
+  (v:value) (n:Z), (many_steps sigma pi e sigma' pi' (Evalue v) n) ->
+  (eval_fmla sigma' (Cons (result, v) pi') q).
 
 (* Why3 assumption *)
 Definition total_valid_triple(p:fmla) (e:expr) (q:fmla): Prop :=
   forall (sigma:(map ident value)) (pi:(list (ident* value)%type)),
-  (eval_fmla sigma pi p) -> exists sigmaqt:(map ident value),
-  exists piqt:(list (ident* value)%type), exists v:value, exists n:Z,
-  (many_steps sigma pi e sigmaqt piqt (Evalue v) n) /\ (eval_fmla sigmaqt
-  (Cons (result, v) piqt) q).
+  (eval_fmla sigma pi p) -> exists sigma':(map ident value), exists pi':(list
+  (ident* value)%type), exists v:value, exists n:Z, (many_steps sigma pi e
+  sigma' pi' (Evalue v) n) /\ (eval_fmla sigma' (Cons (result, v) pi') q).
 
 Parameter set1 : forall (a:Type), Type.
 
@@ -478,9 +476,9 @@ Unset Contextual Implicit.
 Axiom all_def : forall (a:Type), forall (x:a), (mem x (all :(set1 a))).
 
 (* Why3 assumption *)
-Definition assigns(sigma:(map ident value)) (a:(set1 ident)) (sigmaqt:(map
+Definition assigns(sigma:(map ident value)) (a:(set1 ident)) (sigma':(map
   ident value)): Prop := forall (i:ident), (~ (mem i a)) -> ((get sigma
-  i) = (get sigmaqt i)).
+  i) = (get sigma' i)).
 
 Axiom assigns_refl : forall (sigma:(map ident value)) (a:(set1 ident)),
   (assigns sigma a sigma).
@@ -489,13 +487,13 @@ Axiom assigns_trans : forall (sigma1:(map ident value)) (sigma2:(map ident
   value)) (sigma3:(map ident value)) (a:(set1 ident)), ((assigns sigma1 a
   sigma2) /\ (assigns sigma2 a sigma3)) -> (assigns sigma1 a sigma3).
 
-Axiom assigns_union_left : forall (sigma:(map ident value)) (sigmaqt:(map
+Axiom assigns_union_left : forall (sigma:(map ident value)) (sigma':(map
   ident value)) (s1:(set1 ident)) (s2:(set1 ident)), (assigns sigma s1
-  sigmaqt) -> (assigns sigma (union s1 s2) sigmaqt).
+  sigma') -> (assigns sigma (union s1 s2) sigma').
 
-Axiom assigns_union_right : forall (sigma:(map ident value)) (sigmaqt:(map
+Axiom assigns_union_right : forall (sigma:(map ident value)) (sigma':(map
   ident value)) (s1:(set1 ident)) (s2:(set1 ident)), (assigns sigma s2
-  sigmaqt) -> (assigns sigma (union s1 s2) sigmaqt).
+  sigma') -> (assigns sigma (union s1 s2) sigma').
 
 (* Why3 assumption *)
 Set Implicit Arguments.
@@ -533,11 +531,11 @@ Fixpoint wp(e:expr) (q:fmla) {struct e}: fmla :=
   | (Eseq e1 e2) => (wp e1 (wp e2 q))
   | (Elet id e1 e2) => (wp e1 (Flet id (Tvar result) (wp e2 q)))
   | (Ebin e1 op e2) => let t1 := (fresh_from q e) in let t2 :=
-      (fresh_from (Fand (Fterm (Tvar t1)) q) e) in let qqt := (Flet result
+      (fresh_from (Fand (Fterm (Tvar t1)) q) e) in let q' := (Flet result
       (Tbin (Tvar t1) op (Tvar t2)) q) in let f := (wp e2 (Flet t2
-      (Tvar result) qqt)) in (wp e1 (Flet t1 (Tvar result) f))
-  | (Eassign x e1) => let id := (fresh_from q e1) in let qqt := (Flet result
-      (Tvalue Vvoid) q) in (wp e1 (Flet id (Tvar result) (subst qqt x id)))
+      (Tvar result) q')) in (wp e1 (Flet t1 (Tvar result) f))
+  | (Eassign x e1) => let id := (fresh_from q e1) in let q' := (Flet result
+      (Tvalue Vvoid) q) in (wp e1 (Flet id (Tvar result) (subst q' x id)))
   | (Eif e1 e2 e3) => let f := (Fand (Fimplies (Fterm (Tvar result)) (wp e2
       q)) (Fimplies (Fnot (Fterm (Tvar result))) (wp e3 q))) in (wp e1 f)
   | (Ewhile cond inv body) => (Fand inv (abstract_effects body (wp cond
@@ -546,9 +544,9 @@ Fixpoint wp(e:expr) (q:fmla) {struct e}: fmla :=
   end.
 Unset Implicit Arguments.
 
-Axiom wp_subst : forall (e:expr) (q:fmla) (id:ident) (idqt:ident),
-  (fresh_in_expr id e) -> ((subst (wp e q) id idqt) = (wp e (subst q id
-  idqt))).
+Axiom wp_subst : forall (e:expr) (q:fmla) (id:ident) (id':ident),
+  (fresh_in_expr id e) -> ((subst (wp e q) id id') = (wp e (subst q id
+  id'))).
 
 Axiom wp_implies : forall (p:fmla) (q:fmla), (forall (sigma:(map ident
   value)) (pi:(list (ident* value)%type)), (eval_fmla sigma pi p) ->
@@ -560,11 +558,10 @@ Axiom wp_conj : forall (sigma:(map ident value)) (pi:(list (ident*
   value)%type)) (e:expr) (p:fmla) (q:fmla), (eval_fmla sigma pi (wp e (Fand p
   q))) <-> ((eval_fmla sigma pi (wp e p)) /\ (eval_fmla sigma pi (wp e q))).
 
-Axiom wp_reduction : forall (sigma:(map ident value)) (sigmaqt:(map ident
-  value)) (pi:(list (ident* value)%type)) (piqt:(list (ident* value)%type))
-  (e:expr) (eqt:expr), (one_step sigma pi e sigmaqt piqt eqt) ->
-  forall (q:fmla), (eval_fmla sigma pi (wp e q)) -> (eval_fmla sigmaqt piqt
-  (wp eqt q)).
+Axiom wp_reduction : forall (sigma:(map ident value)) (sigma':(map ident
+  value)) (pi:(list (ident* value)%type)) (pi':(list (ident* value)%type))
+  (e:expr) (e':expr), (one_step sigma pi e sigma' pi' e') -> forall (q:fmla),
+  (eval_fmla sigma pi (wp e q)) -> (eval_fmla sigma' pi' (wp e' q)).
 
 (* Why3 assumption *)
 Definition not_a_value(e:expr): Prop :=
@@ -579,9 +576,8 @@ Axiom decide_value : forall (e:expr), (not_a_value e) \/ exists v:value,
 (* Why3 goal *)
 Theorem progress : forall (e:expr) (sigma:(map ident value)) (pi:(list
   (ident* value)%type)) (q:fmla), ((eval_fmla sigma pi (wp e q)) /\
-  (not_a_value e)) -> exists sigmaqt:(map ident value), exists piqt:(list
-  (ident* value)%type), exists eqt:expr, (one_step sigma pi e sigmaqt piqt
-  eqt).
+  (not_a_value e)) -> exists sigma':(map ident value), exists pi':(list
+  (ident* value)%type), exists e':expr, (one_step sigma pi e sigma' pi' e').
 
 induction e.
 simpl; tauto.
@@ -748,6 +744,4 @@ eexists.
 eexists.
 eapply one_step_while; auto.
 
-Qed.
-
-
+Qed.
\ No newline at end of file

examples/hoare_logic/blocking_semantics/why3session.xml

@@ -902,7 +902,7 @@
      edited="blocking_semantics_WP_progress_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.74"/>
+     <result status="valid" time="0.76"/>
     </proof>
    </goal>
   </theory>

examples/hoare_logic/blocking_semantics2.mlw

@@ -29,12 +29,14 @@ type ident
 
 constant result : ident
 
+(** Terms *)
 type term =
   | Tvalue value
   | Tvar ident
   | Tderef mident
   | Tbin term operator term
 
+(** Formulas *)
 type fmla =
   | Fterm term
   | Fand fmla fmla
@@ -43,6 +45,19 @@ type fmla =
   | Flet ident term fmla         (* let id = term in fmla *)
   | Fforall ident datatype fmla  (* forall id : ty, fmla *)
 
+(** Expressions *)
+type expr =
+  | Evalue value
+  | Ebin expr operator expr
+  | Evar ident
+  | Ederef mident
+  | Eassign mident expr
+  | Eseq expr expr
+  | Elet ident expr expr
+  | Eif expr expr expr
+  | Eassert fmla
+  | Ewhile expr fmla expr  (* while cond invariant inv body *)
+
 (** Typing *)
 
 function type_value (v:value) : datatype =
@@ -69,15 +84,104 @@ type type_env = IdMap.map mident datatype  (* map global mutable variables to th
 function get_reftype (i:mident) (e:type_env) : datatype = IdMap.get e i
 
 inductive type_term type_env type_stack term datatype =
-  | Type_value : forall sigma: type_env, pi:type_stack, v:value. type_term sigma pi (Tvalue v) (type_value v)
-  | Type_var : forall sigma: type_env, pi:type_stack, v: ident, ty:datatype.
-        (get_vartype v pi = ty) -> type_term sigma pi (Tvar v) (ty)
-  | Type_deref : forall sigma: type_env, pi:type_stack, v: mident, ty:datatype.
-        (get_reftype v sigma = ty) -> type_term sigma pi (Tderef v) (ty)
-  | Type_bin : forall sigma: type_env, pi:type_stack, t1 t2 : term, op:operator, ty1 ty2 ty:datatype.
-        (type_term sigma pi t1 ty1) /\
-	(type_term sigma pi t2 ty2) /\
-	(type_operator op ty1 ty2 ty) -> type_term sigma pi (Tbin t1 op t2) ty
+  | Type_value :
+      forall sigma: type_env, pi:type_stack, v:value.
+	type_term sigma pi (Tvalue v) (type_value v)
+  | Type_var :
+      forall sigma: type_env, pi:type_stack, v: ident, ty:datatype.
+        (get_vartype v pi = ty) -> type_term sigma pi (Tvar v) ty
+  | Type_deref :
+      forall sigma: type_env, pi:type_stack, v: mident, ty:datatype.
+        (get_reftype v sigma = ty) -> type_term sigma pi (Tderef v) ty
+  | Type_bin :
+      forall sigma: type_env, pi:type_stack, t1 t2 : term, op:operator, ty1 ty2 ty:datatype.
+        type_term sigma pi t1 ty1 ->
+	type_term sigma pi t2 ty2 ->
+	type_operator op ty1 ty2 ty -> type_term sigma pi (Tbin t1 op t2) ty
+
+inductive type_fmla type_env type_stack fmla =
+  | Type_term :
+      forall sigma: type_env, pi:type_stack, t:term.
+	type_term sigma pi t TYbool ->
+	type_fmla sigma pi (Fterm t)
+  | Type_conj :
+      forall sigma: type_env, pi:type_stack, f1 f2:fmla.
+	type_fmla sigma pi f1 ->
+        type_fmla sigma pi f2 ->
+        type_fmla sigma pi (Fand f1 f2)
+  | Type_neg :
+      forall sigma: type_env, pi:type_stack, f:fmla.
+	type_fmla sigma pi f ->
+        type_fmla sigma pi (Fnot f)
+  | Type_implies :
+      forall sigma: type_env, pi:type_stack, f1 f2:fmla.
+	type_fmla sigma pi f1 ->
+        type_fmla sigma pi f2 ->
+        type_fmla sigma pi (Fimplies f1 f2)
+  | Type_let :
+      forall sigma: type_env, pi:type_stack, 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: type_env, pi:type_stack, x:ident, f:fmla.
+        type_fmla sigma (Cons (x,TYint) pi) f ->
+  	type_fmla sigma pi (Fforall x TYint f)
+  | Type_forall2 :
+      forall sigma: type_env, pi:type_stack, x:ident, f:fmla.
+        type_fmla sigma (Cons (x,TYbool) pi) f ->
+  	type_fmla sigma pi (Fforall x TYbool f)
+  | Type_forall3:
+      forall sigma: type_env, pi:type_stack, x:ident, f:fmla.
+        type_fmla sigma (Cons (x,TYunit) pi) f ->
+  	type_fmla sigma pi (Fforall x TYunit f)
+
+inductive type_expr type_env type_stack expr datatype =
+  | Type_evalue :
+      forall sigma: type_env, pi:type_stack, v:value.
+	type_expr sigma pi (Evalue v) (type_value v)
+  | Type_evar   :
+      forall sigma: type_env, pi:type_stack, v:ident, ty:datatype.
+        (get_vartype v pi = ty) -> type_expr sigma pi (Evar v) ty
+  | Type_ederef :
+      forall sigma: type_env, pi:type_stack, v:mident, ty:datatype.
+        (get_reftype v sigma = ty) -> type_expr sigma pi (Ederef v) ty
+  | Type_ebin   :
+      forall sigma: type_env, pi:type_stack, e1 e2:expr, op:operator, ty1 ty2 ty:datatype.
+        type_expr sigma pi e1 ty1 ->
+	type_expr sigma pi e2 ty2 ->
+	type_operator op ty1 ty2 ty -> type_expr sigma pi (Ebin e1 op e2) ty
+  | Type_eseq :
+      forall sigma: type_env, pi:type_stack, e1 e2:expr, op:operator, ty:datatype.
+        type_expr sigma pi e1 TYunit ->
+	type_expr sigma pi e2 ty ->
+	type_expr sigma pi (Eseq e1 e2) ty
+  | Type_eassigns :
+      forall sigma: type_env, pi:type_stack, x:mident, e:expr, ty:datatype.
+	(get_reftype x sigma = ty) ->
+        type_expr sigma pi e ty ->
+        type_expr sigma pi (Eassign x e) TYunit
+  | Type_elet :
+      forall sigma: type_env, pi:type_stack, x:ident, e1 e2:expr, ty1 ty2 ty:datatype.
+	type_expr sigma pi e1 ty1 ->
+        type_expr sigma (Cons (x,ty2) pi) e2 ty2 ->
+	type_expr sigma pi (Elet x e1 e2) ty2
+  | Type_eif :
+      forall sigma: type_env, pi:type_stack, e1 e2 e3:expr, ty:datatype.
+	type_expr sigma pi e1 TYbool ->
+	type_expr sigma pi e2 ty ->
+	type_expr sigma pi e3 ty ->
+    	type_expr sigma pi (Eif e1 e2 e3) ty 
+  | Type_eassert :
+      forall sigma: type_env, pi:type_stack, p:fmla, ty:datatype.
+	type_fmla sigma pi p ->
+    	type_expr sigma pi (Eassert p) TYbool
+  | Type_ewhile :
+      forall sigma: type_env, pi:type_stack, guard body:expr, inv:fmla, ty:datatype.
+	type_fmla sigma pi inv ->
+        type_expr sigma pi guard TYbool ->
+        type_expr sigma pi body TYunit ->
+        type_expr sigma pi (Ewhile guard inv body) TYunit
 
 (** Operational semantic *)
 type env = IdMap.map mident value  (* map global mutable variables to their value *)
@@ -216,12 +320,12 @@ lemma subst_fresh :
 
 lemma let_subst:
     forall t:term, f:fmla, x id':ident, id :mident.
-    subst (Flet x t f) id id' = Flet x (subst_term t id id') (subst f id id')
+    msubst (Flet x t f) id id' = Flet x (msubst_term t id id') (msubst f id id')
 
 lemma eval_subst:
   forall f:fmla, sigma:env, pi:stack, x:mident, v:ident.
     fresh_in_fmla v f ->
-    (eval_fmla sigma pi (subst f x v) <->
+    (eval_fmla sigma pi (msubst f x v) <->
      eval_fmla (IdMap.set sigma x (get_stack v pi)) pi f)
 
 lemma eval_swap:
@@ -240,25 +344,11 @@ lemma eval_change_free :
   predicate valid_fmla (p:fmla) = forall sigma:env, pi:stack. eval_fmla sigma pi p
 
 (** 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. *)
-(*       eval_fmla sigma pi (Flet id' t (subst f id id')) *)
-(*       -> eval_fmla sigma pi (Flet id t f) *)
-
-(* expressions *)
-
-type expr =
-  | Evalue value
-  | Ebin expr operator expr
-  | Evar ident
-  | Ederef mident
-  | Eassign mident expr
-  | Eseq expr expr
-  | Elet ident expr expr
-  | Eif expr expr expr
-  | Eassert fmla
-  | Ewhile expr fmla expr  (* while cond invariant inv body *)
+lemma let_equiv :
+  forall id:ident, id':ident, t:term, f:fmla.
+    forall sigma:env, pi:stack.
+      eval_fmla sigma pi (Flet id' t (subst f id id'))
+      -> eval_fmla sigma pi (Flet id t f)
 
 predicate fresh_in_expr (id:ident) (e:expr) =
   match e with
@@ -490,7 +580,7 @@ lemma value_rule:
 
 lemma assign_rule:
   forall p q:fmla, x:mident, e:expr.
-  valid_triple p e (subst q x result) ->
+  valid_triple p e (msubst q x result) ->
   valid_triple p (Eassign x e) q
 
 lemma seq_rule:
@@ -614,7 +704,7 @@ predicate expr_writes (e:expr) (w:Set.set mident) =
     | Eassign x e ->
         let id = fresh_from q e in
         let q' = Flet result (Tvalue Vvoid) q in
-        wp e (Flet id (Tvar result) (subst q' x id))
+        wp e (Flet id (Tvar result) (msubst q' x id))
     | Eif e1 e2 e3 ->
         let f =
           Fand (Fimplies (Fterm (Tvar result)) (wp e2 q))
@@ -669,13 +759,15 @@ predicate expr_writes (e:expr) (w:Set.set mident) =
     forall e:expr. not (is_value e) \/ exists v:value. e = Evalue v
 
   lemma bool_value:
-    forall e:expr. type_expr sigmat pit e TYbool -> is_value e -> 
-          (e = Tvalue True) \/ (e = Tvalue False).
+    forall e:expr, sigmat: type_env, pit:type_stack.  
+      type_expr sigmat pit e TYbool -> is_value e ->
+          (e = Evalue (Vbool Bool.False)) \/ (e = Evalue (Vbool Bool.True))
 
   lemma progress:
     forall e:expr, sigma:env, pi:stack, sigmat: type_env, pit: type_stack, ty: datatype, q:fmla.
-      type_expr sigmat pit e ty -> type_fmla sigmat (Cons(result, ty) pit) q
-    eval_fmla sigma pi (wp e q) -> not_a_value e ->
+      type_expr sigmat pit e ty -> 
+      type_fmla sigmat (Cons(result, ty) pit) q ->
+    eval_fmla sigma pi (wp e q) -> not is_value e ->
     exists sigma':env, pi':stack, e':expr.
       one_step sigma pi e sigma' pi' e'
 
@@ -962,7 +1054,7 @@ end
 
 (***
 Local Variables:
-compile-command: "why3ide blocking_semantics.mlw"
+compile-command: "why3ide blocking_semantics2.mlw"
 End:
 *)