Commit e8632072 authored by MARCHE Claude's avatar MARCHE Claude

rename axiom

parent c5cd8e68
......@@ -759,7 +759,7 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
valid_fmla p -> valid_fmla (abstract_effects s p)
*)
axiom abstract_effects_monotonic_2 :
axiom abstract_effects_monotonic :
forall s:stmt, p q:fmla.
valid_fmla (Fimplies p q) ->
forall sigma:env, pi:stack.
......
......@@ -693,10 +693,7 @@ 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) (p:fmla),
(valid_fmla p) -> (valid_fmla (abstract_effects s p)).
Axiom abstract_effects_monotonic_2 : forall (s:stmt) (p:fmla) (q:fmla),
Axiom abstract_effects_monotonic : forall (s:stmt) (p:fmla) (q:fmla),
(valid_fmla (Fimplies p q)) -> forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)), (eval_fmla sigma pi (abstract_effects s p)) ->
(eval_fmla sigma pi (abstract_effects s q)).
......@@ -754,14 +751,11 @@ intros H sigma pi p q (H0 & H1).
destruct H0.
destruct H1; clear H1.
split; auto.
apply abstract_effects_monotonic_2 with (p:=
apply abstract_effects_monotonic with (p:=
(Fand (Fand (Fimplies (Fand (Fterm t) f) (wp s f))
(Fimplies (Fand (Fnot (Fterm t)) f) p))
(Fand (Fimplies (Fand (Fterm t) f) (wp s f))
(Fimplies (Fand (Fnot (Fterm t)) f) q))))
.
(Fimplies (Fand (Fnot (Fterm t)) f) q)))).
unfold valid_fmla; simpl.
intuition.
apply abstract_effects_distrib_conj; auto.
......
......@@ -693,14 +693,17 @@ 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) (p:fmla),
(valid_fmla p) -> (valid_fmla (abstract_effects s p)).
Axiom abstract_effects_monotonic_2 : forall (s:stmt) (p:fmla) (q:fmla),
Axiom abstract_effects_monotonic : forall (s:stmt) (p:fmla) (q:fmla),
(valid_fmla (Fimplies p q)) -> forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)), (eval_fmla sigma pi (abstract_effects s p)) ->
(eval_fmla sigma pi (abstract_effects s q)).
Axiom abstract_effects_distrib_conj : forall (s:stmt) (p:fmla) (q:fmla)
(sigma:(map mident value)) (pi:(list (ident* value)%type)),
((eval_fmla sigma pi (abstract_effects s p)) /\ (eval_fmla sigma pi
(abstract_effects s q))) -> (eval_fmla sigma pi (abstract_effects s (Fand p
q))).
(* Why3 assumption *)
Fixpoint wp(s:stmt) (q:fmla) {struct s}: fmla :=
match s with
......@@ -741,7 +744,7 @@ unfold valid_fmla.
simpl.
intros H1 p q H2.
intuition.
apply abstract_effects_monotonic_2 with (2:=H3).
apply abstract_effects_monotonic with (2:=H3).
unfold valid_fmla; simpl.
intuition.
Qed.
......
......@@ -693,10 +693,7 @@ 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) (p:fmla),
(valid_fmla p) -> (valid_fmla (abstract_effects s p)).
Axiom abstract_effects_monotonic_2 : forall (s:stmt) (p:fmla) (q:fmla),
Axiom abstract_effects_monotonic : forall (s:stmt) (p:fmla) (q:fmla),
(valid_fmla (Fimplies p q)) -> forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)), (eval_fmla sigma pi (abstract_effects s p)) ->
(eval_fmla sigma pi (abstract_effects s q)).
......@@ -734,7 +731,7 @@ Axiom distrib_conj : forall (s:stmt) (sigma:(map mident value)) (pi:(list
(eval_fmla sigma pi (wp s q))) -> (eval_fmla sigma pi (wp s (Fand p q))).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 2.
Ltac ae := why3 "alt-ergo" timelimit 5.
(* Why3 goal *)
Theorem wp_reduction : forall (sigma:(map mident value)) (sigma':(map mident
......@@ -753,7 +750,9 @@ Theorem wp_reduction : forall (sigma:(map mident value)) (sigma':(map mident
q)) -> (eval_fmla sigma' pi' (wp s' q))
end.
destruct s; auto.
intros _ s' H1 q (_ & H3).
intros _ s' H1 q.
simpl.
intros (_ & H3).
generalize H3.
intro H4.
apply abstract_effects_generalize in H4; simpl in H4.
......
......@@ -575,7 +575,7 @@
edited="blocking_semantics5_TypingAndSemantics_eval_type_term_1.v"
obsolete="false"
archived="false">
<result status="valid" time="4.08"/>
<result status="valid" time="4.01"/>
</proof>
</goal>
</transf>
......@@ -597,7 +597,7 @@
edited="blocking_semantics5_TypingAndSemantics_type_preservation_1.v"
obsolete="false"
archived="false">
<result status="valid" time="7.94"/>
<result status="valid" time="7.92"/>
</proof>
</goal>
</theory>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment