Commit 91cd433e authored by MARCHE Claude's avatar MARCHE Claude

petites ameliorations

parent 81343923
......@@ -313,18 +313,10 @@ inductive type_fmla type_env type_stack fmla =
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)
| Type_forall :
forall sigma: type_env, pi:type_stack, x:ident, f:fmla, ty:datatype.
type_fmla sigma (Cons (x,ty) pi) f ->
type_fmla sigma pi (Fforall x ty f)
inductive type_stmt type_env type_stack stmt =
| Type_skip :
......@@ -351,11 +343,11 @@ inductive type_stmt type_env type_stack stmt =
type_fmla sigma pi p ->
type_stmt sigma pi (Sassert p)
| Type_while :
forall sigma: type_env, pi:type_stack, guard:term, body:stmt, inv:fmla.
forall sigma: type_env, pi:type_stack, cond:term, body:stmt, inv:fmla.
type_fmla sigma pi inv ->
type_term sigma pi guard TYbool ->
type_term sigma pi cond TYbool ->
type_stmt sigma pi body ->
type_stmt sigma pi (Swhile guard inv body)
type_stmt sigma pi (Swhile cond inv body)
end
......@@ -379,6 +371,10 @@ inductive compatible datatype value =
*)
predicate compatible_env (sigma:env) (sigmat:type_env) (pi:stack) (pit: type_stack) =
(forall id: mident. type_value (IdMap.get sigma id) = get_reftype id sigmat) /\
(forall id: ident. type_value (get_stack id pi) = get_vartype id pit)
lemma type_inversion : forall v:value.
match (type_value v) with
| TYbool -> exists b: bool. v = Vbool b
......@@ -386,10 +382,6 @@ lemma type_inversion : forall v:value.
| TYunit -> v = Vvoid
end
predicate compatible_env (sigma:env) (sigmat:type_env) (pi:stack) (pit: type_stack) =
(forall id: mident. type_value (IdMap.get sigma id) = get_reftype id sigmat) /\
(forall id: ident. type_value (get_stack id pi) = get_vartype id pit)
lemma eval_type_term:
forall t:term, sigma:env, pi:stack, sigmat:type_env, pit:type_stack, ty:datatype.
compatible_env sigma sigmat pi pit ->
......@@ -416,33 +408,6 @@ theory FreshVariables
use import SemOp
use import list.Append
(** [fresh_in_term id t] is true when [id] does not occur in [t] *)
predicate fresh_in_term (x:ident) (t:term) =
match t with
| Tvalue _ -> true
| Tvar i -> x <> i
| Tderef _ -> true
| Tbin t1 _ t2 -> fresh_in_term x t1 /\ fresh_in_term x t2
end
(*
lemma fresh_in_binop:
forall t t':term, op:operator, v:ident.
fresh_in_term v (Tbin t op t') ->
fresh_in_term v t /\ fresh_in_term v t'
*)
predicate fresh_in_fmla (id:ident) (f:fmla) =
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 f -> fresh_in_fmla id f
| Flet y t f -> id <> y /\ fresh_in_term id t /\ fresh_in_fmla id f
| Fforall y ty f -> id <> y /\ fresh_in_fmla id f
end
(** substitution of a reference [r] by a logic variable [v]
warning: proper behavior only guaranted if [v] is fresh *)
......@@ -465,6 +430,28 @@ function msubst (f:fmla) (x:mident) (v:ident) : fmla =
end
(** [fresh_in_term id t] is true when [id] does not occur in [t] *)
predicate fresh_in_term (x:ident) (t:term) =
match t with
| Tvalue _ -> true
| Tvar i -> x <> i
| Tderef _ -> true
| Tbin t1 _ t2 -> fresh_in_term x t1 /\ fresh_in_term x t2
end
predicate fresh_in_fmla (id:ident) (f:fmla) =
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 f -> fresh_in_fmla id f
| Flet y t f -> id <> y /\ fresh_in_term id t /\ fresh_in_fmla id f
| Fforall y ty f -> id <> y /\ fresh_in_fmla id f
end
(* Needed for monotonicity and wp_reduction *)
lemma eval_msubst_term:
forall e:term, sigma:env, pi:stack, x:mident, v:ident.
......@@ -497,9 +484,8 @@ lemma eval_term_change_free :
(* Need it for monotonicity*)
lemma eval_change_free :
forall f:fmla, id:ident, v:value.
forall f:fmla, sigma:env, pi:stack, id:ident, v:value.
fresh_in_fmla id f ->
forall sigma:env, pi:stack.
(eval_fmla sigma (Cons (id,v) pi) f <-> eval_fmla sigma pi f)
......
......@@ -202,14 +202,14 @@ Inductive one_step : (map mident value) -> (list (ident* value)%type) -> stmt
value)%type)) (f:fmla), (eval_fmla sigma pi f) -> (one_step sigma pi
(Sassert f) sigma pi Sskip)
| one_step_while_true : 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 true)) -> (one_step sigma
pi (Swhile cond inv body) sigma pi (Sseq body (Swhile cond inv body))))
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_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)
sigma pi Sskip)).
((eval_fmla sigma pi inv) /\ ((eval_term sigma pi
cond) = (Vbool false))) -> (one_step sigma pi (Swhile cond inv body)
sigma pi Sskip).
(* Why3 assumption *)
Inductive many_steps : (map mident value) -> (list (ident* value)%type)
......@@ -230,7 +230,7 @@ Axiom steps_non_neg : forall (sigma1:(map mident value)) (sigma2:(map mident
(0%Z <= n)%Z.
(* Why3 assumption *)
Definition reducible(sigma:(map mident value)) (pi:(list (ident*
Definition reductible(sigma:(map mident value)) (pi:(list (ident*
value)%type)) (s:stmt): Prop := exists sigma':(map mident value),
exists pi':(list (ident* value)%type), exists s':stmt, (one_step sigma pi s
sigma' pi' s').
......@@ -282,27 +282,6 @@ Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
a)), (mem x l) -> exists l1:(list a), exists l2:(list a),
(l = (infix_plpl l1 (Cons x l2))).
(* Why3 assumption *)
Fixpoint fresh_in_term(x:ident) (t:term) {struct t}: Prop :=
match t with
| (Tvalue _) => True
| (Tvar i) => ~ (x = i)
| (Tderef _) => True
| (Tbin t1 _ t2) => (fresh_in_term x t1) /\ (fresh_in_term x t2)
end.
(* Why3 assumption *)
Fixpoint fresh_in_fmla(id:ident) (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.
Parameter msubst_term: term -> mident -> ident -> term.
Axiom msubst_term_def : forall (t:term) (r:mident) (v:ident),
......@@ -325,6 +304,27 @@ Fixpoint msubst(f:fmla) (x:mident) (v:ident) {struct f}: fmla :=
| (Fforall y ty f1) => (Fforall y ty (msubst f1 x v))
end.
(* Why3 assumption *)
Fixpoint fresh_in_term(x:ident) (t:term) {struct t}: Prop :=
match t with
| (Tvalue _) => True
| (Tvar i) => ~ (x = i)
| (Tderef _) => True
| (Tbin t1 _ t2) => (fresh_in_term x t1) /\ (fresh_in_term x t2)
end.
(* Why3 assumption *)
Fixpoint fresh_in_fmla(id:ident) (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.
Axiom 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
......@@ -361,26 +361,25 @@ Theorem eval_change_free : forall (f:fmla),
| (Fand f1 f2) => True
| (Fnot f1) => True
| (Fimplies f1 f2) => True
| (Flet i t f1) => (forall (id:ident) (v:value), (fresh_in_fmla id f1) ->
forall (sigma:(map mident value)) (pi:(list (ident* value)%type)),
(eval_fmla sigma (Cons (id, v) pi) f1) <-> (eval_fmla sigma pi f1)) ->
forall (id:ident) (v:value), (fresh_in_fmla id f) -> forall (sigma:(map
mident value)) (pi:(list (ident* value)%type)), (eval_fmla sigma
(Cons (id, v) pi) f) -> (eval_fmla sigma pi f)
| (Flet i t f1) => (forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)) (id:ident) (v:value), (fresh_in_fmla id f1) ->
((eval_fmla sigma (Cons (id, v) pi) f1) <-> (eval_fmla sigma pi
f1))) -> forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)) (id:ident) (v:value), (fresh_in_fmla id f) ->
((eval_fmla sigma pi f) -> (eval_fmla sigma (Cons (id, v) pi) f))
| (Fforall i d f1) => True
end.
destruct f; auto.
simpl.
intros.
destruct H0 as (h1 & h2 & h3).
rewrite eval_term_change_free in H1; auto.
simpl; intros H sigma pi id v (h1 & h2 & h3).
rewrite eval_term_change_free; auto.
assert (eval_fmla sigma (infix_plpl (Nil : (list (ident*value)))
(Cons (i, eval_term sigma pi t) (Cons (id, v) pi))) f =
eval_fmla sigma
(Cons (i, eval_term sigma pi t) (Cons (id, v) pi)) f);
auto.
rewrite <- H0 in H1; clear H0.
apply eval_swap in H1; auto.
apply H in H1; auto.
rewrite <- H0; clear H0.
rewrite eval_swap; auto.
apply H; auto.
Qed.
......@@ -202,14 +202,14 @@ Inductive one_step : (map mident value) -> (list (ident* value)%type) -> stmt
value)%type)) (f:fmla), (eval_fmla sigma pi f) -> (one_step sigma pi
(Sassert f) sigma pi Sskip)
| one_step_while_true : 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 true)) -> (one_step sigma
pi (Swhile cond inv body) sigma pi (Sseq body (Swhile cond inv body))))
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_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)
sigma pi Sskip)).
((eval_fmla sigma pi inv) /\ ((eval_term sigma pi
cond) = (Vbool false))) -> (one_step sigma pi (Swhile cond inv body)
sigma pi Sskip).
(* Why3 assumption *)
Inductive many_steps : (map mident value) -> (list (ident* value)%type)
......@@ -230,7 +230,7 @@ Axiom steps_non_neg : forall (sigma1:(map mident value)) (sigma2:(map mident
(0%Z <= n)%Z.
(* Why3 assumption *)
Definition reducible(sigma:(map mident value)) (pi:(list (ident*
Definition reductible(sigma:(map mident value)) (pi:(list (ident*
value)%type)) (s:stmt): Prop := exists sigma':(map mident value),
exists pi':(list (ident* value)%type), exists s':stmt, (one_step sigma pi s
sigma' pi' s').
......@@ -282,27 +282,6 @@ Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
a)), (mem x l) -> exists l1:(list a), exists l2:(list a),
(l = (infix_plpl l1 (Cons x l2))).
(* Why3 assumption *)
Fixpoint fresh_in_term(x:ident) (t:term) {struct t}: Prop :=
match t with
| (Tvalue _) => True
| (Tvar i) => ~ (x = i)
| (Tderef _) => True
| (Tbin t1 _ t2) => (fresh_in_term x t1) /\ (fresh_in_term x t2)
end.
(* Why3 assumption *)
Fixpoint fresh_in_fmla(id:ident) (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.
Parameter msubst_term: term -> mident -> ident -> term.
Axiom msubst_term_def : forall (t:term) (r:mident) (v:ident),
......@@ -325,6 +304,27 @@ Fixpoint msubst(f:fmla) (x:mident) (v:ident) {struct f}: fmla :=
| (Fforall y ty f1) => (Fforall y ty (msubst f1 x v))
end.
(* Why3 assumption *)
Fixpoint fresh_in_term(x:ident) (t:term) {struct t}: Prop :=
match t with
| (Tvalue _) => True
| (Tvar i) => ~ (x = i)
| (Tderef _) => True
| (Tbin t1 _ t2) => (fresh_in_term x t1) /\ (fresh_in_term x t2)
end.
(* Why3 assumption *)
Fixpoint fresh_in_fmla(id:ident) (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.
Axiom 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
......@@ -358,26 +358,24 @@ Theorem eval_change_free : forall (f:fmla),
| (Fand f1 f2) => True
| (Fnot f1) => True
| (Fimplies f1 f2) => True
| (Flet i t f1) => (forall (id:ident) (v:value), (fresh_in_fmla id f1) ->
forall (sigma:(map mident value)) (pi:(list (ident* value)%type)),
(eval_fmla sigma (Cons (id, v) pi) f1) <-> (eval_fmla sigma pi f1)) ->
forall (id:ident) (v:value), (fresh_in_fmla id f) -> forall (sigma:(map
mident value)) (pi:(list (ident* value)%type)), (eval_fmla sigma pi
f) -> (eval_fmla sigma (Cons (id, v) pi) f)
| (Flet i t f1) => (forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)) (id:ident) (v:value), (fresh_in_fmla id f1) ->
((eval_fmla sigma (Cons (id, v) pi) f1) <-> (eval_fmla sigma pi
f1))) -> forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)) (id:ident) (v:value), (fresh_in_fmla id f) ->
((eval_fmla sigma (Cons (id, v) pi) f) -> (eval_fmla sigma pi f))
| (Fforall i d f1) => True
end.
destruct f; auto.
simpl.
intros.
destruct H0 as (h1 & h2 & h3).
simpl; intros H sigma pi id v (h1 & h2 & h3).
rewrite eval_term_change_free; auto.
assert (eval_fmla sigma (infix_plpl (Nil : (list (ident*value)))
assert (h : eval_fmla sigma (infix_plpl (Nil : (list (ident*value)))
(Cons (i, eval_term sigma pi t) (Cons (id, v) pi))) f =
eval_fmla sigma
(Cons (i, eval_term sigma pi t) (Cons (id, v) pi)) f);
auto.
rewrite <- H0; clear H0.
apply eval_swap; auto.
rewrite <- h.
rewrite eval_swap; auto.
apply H; auto.
Qed.
......
......@@ -202,14 +202,14 @@ Inductive one_step : (map mident value) -> (list (ident* value)%type) -> stmt
value)%type)) (f:fmla), (eval_fmla sigma pi f) -> (one_step sigma pi
(Sassert f) sigma pi Sskip)
| one_step_while_true : 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 true)) -> (one_step sigma
pi (Swhile cond inv body) sigma pi (Sseq body (Swhile cond inv body))))
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_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)
sigma pi Sskip)).
((eval_fmla sigma pi inv) /\ ((eval_term sigma pi
cond) = (Vbool false))) -> (one_step sigma pi (Swhile cond inv body)
sigma pi Sskip).
(* Why3 assumption *)
Inductive many_steps : (map mident value) -> (list (ident* value)%type)
......@@ -230,7 +230,7 @@ Axiom steps_non_neg : forall (sigma1:(map mident value)) (sigma2:(map mident
(0%Z <= n)%Z.
(* Why3 assumption *)
Definition reducible(sigma:(map mident value)) (pi:(list (ident*
Definition reductible(sigma:(map mident value)) (pi:(list (ident*
value)%type)) (s:stmt): Prop := exists sigma':(map mident value),
exists pi':(list (ident* value)%type), exists s':stmt, (one_step sigma pi s
sigma' pi' s').
......@@ -282,27 +282,6 @@ Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
a)), (mem x l) -> exists l1:(list a), exists l2:(list a),
(l = (infix_plpl l1 (Cons x l2))).
(* Why3 assumption *)
Fixpoint fresh_in_term(x:ident) (t:term) {struct t}: Prop :=
match t with
| (Tvalue _) => True
| (Tvar i) => ~ (x = i)
| (Tderef _) => True
| (Tbin t1 _ t2) => (fresh_in_term x t1) /\ (fresh_in_term x t2)
end.
(* Why3 assumption *)
Fixpoint fresh_in_fmla(id:ident) (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.
Parameter msubst_term: term -> mident -> ident -> term.
Axiom msubst_term_def : forall (t:term) (r:mident) (v:ident),
......@@ -325,6 +304,27 @@ Fixpoint msubst(f:fmla) (x:mident) (v:ident) {struct f}: fmla :=
| (Fforall y ty f1) => (Fforall y ty (msubst f1 x v))
end.
(* Why3 assumption *)
Fixpoint fresh_in_term(x:ident) (t:term) {struct t}: Prop :=
match t with
| (Tvalue _) => True
| (Tvar i) => ~ (x = i)
| (Tderef _) => True
| (Tbin t1 _ t2) => (fresh_in_term x t1) /\ (fresh_in_term x t2)
end.
(* Why3 assumption *)
Fixpoint fresh_in_fmla(id:ident) (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.
Axiom 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
......@@ -359,17 +359,16 @@ Theorem eval_change_free : forall (f:fmla),
| (Fnot f1) => True
| (Fimplies f1 f2) => True
| (Flet i t f1) => True
| (Fforall i d f1) => (forall (id:ident) (v:value), (fresh_in_fmla id
f1) -> forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)), (eval_fmla sigma (Cons (id, v) pi) f1) <->
(eval_fmla sigma pi f1)) -> forall (id:ident) (v:value),
(fresh_in_fmla id f) -> forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)), (eval_fmla sigma (Cons (id, v) pi) f) ->
(eval_fmla sigma pi f)
| (Fforall i d f1) => (forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)) (id:ident) (v:value), (fresh_in_fmla id f1) ->
((eval_fmla sigma (Cons (id, v) pi) f1) <-> (eval_fmla sigma pi
f1))) -> forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)) (id:ident) (v:value), (fresh_in_fmla id f) ->
((eval_fmla sigma pi f) -> (eval_fmla sigma (Cons (id, v) pi) f))
end.
destruct f; auto.
simpl.
intros H id v (H1 & H2) sigma pi H3.
intros H sigma pi id v (H1 & H2) H3.
destruct d.
(* TYunit*)
......@@ -377,9 +376,9 @@ assert
(eval_fmla sigma (infix_plpl (Nil : (list (ident*value)))
(Cons (i, Vvoid) (Cons (id, v) pi))) f =
eval_fmla sigma (Cons (i, Vvoid) (Cons (id, v) pi)) f); auto.
rewrite <- H0 in H3.
rewrite eval_swap in H3; auto.
apply H in H3; auto.
rewrite <- H0.
rewrite eval_swap; auto.
simpl; apply H; auto.
(* TYint*)
intro n.
......@@ -388,22 +387,20 @@ assert
(eval_fmla sigma (infix_plpl (Nil : (list (ident*value)))
(Cons (i, Vint n) (Cons (id, v) pi))) f =
eval_fmla sigma (Cons (i, Vint n) (Cons (id, v) pi)) f); auto.
rewrite <- H0 in h.
clear H3.
rewrite eval_swap in h; auto.
apply H in h; auto.
rewrite <- H0.
rewrite eval_swap; auto.
simpl; apply H; auto.
(* TYbool*)
intro.
intro b.
assert (h: eval_fmla sigma (Cons (i, Vbool b) (Cons (id, v) pi)) f); auto.
assert
(eval_fmla sigma (infix_plpl (Nil : (list (ident*value)))
(Cons (i, Vbool b) (Cons (id, v) pi))) f =
eval_fmla sigma (Cons (i, Vbool b) (Cons (id, v) pi)) f); auto.
clear H3.
rewrite <- H0 in h.
rewrite eval_swap in h; auto.
apply H in h; auto.
rewrite <- H0.
rewrite eval_swap; auto.
simpl; apply H; auto.
Qed.
......@@ -202,14 +202,14 @@ Inductive one_step : (map mident value) -> (list (ident* value)%type) -> stmt
value)%type)) (f:fmla), (eval_fmla sigma pi f) -> (one_step sigma pi
(Sassert f) sigma pi Sskip)
| one_step_while_true : 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 true)) -> (one_step sigma