more results on hoare logic example

0241585e · MARCHE Claude · 9ebc9463 · 0241585e · 0241585e · 0241585e
Commit 0241585e authored Oct 03, 2011 by MARCHE Claude
--- a/examples/hoare_logic/imp.why
+++ b/examples/hoare_logic/imp.why
@@ -130,6 +130,15 @@ inductive one_step state stmt state stmt =
       many_steps s2 i2 s3 i3 ->
       many_steps s1 i1 s3 i3

+lemma many_steps_seq:
+  forall s1 s3:state, i1 i2:stmt.
+    many_steps s1 (Sseq i1 i2) s3 Sskip ->
+    exists s2:state.
+      many_steps s1 i1 s2 Sskip /\ many_steps s2 i2 s3 Sskip
+
+
+(* formulas *)
+
 type fmla =
  | Fterm expr

@@ -138,15 +147,7 @@ predicate eval_fmla (s:state) (f:fmla) =
  | Fterm e -> eval_expr s e <> 0
  end

-type triple = T fmla stmt fmla
-
-predicate valid_triple (t:triple) =
-  match t with
-  | T p i q ->
-    forall s:state. eval_fmla s p ->
-      forall s':state. many_steps s i s' Sskip ->
-        eval_fmla s' q
-  end
+(* substitution *) 

 function subst_expr (e:expr) (x:ident) (t:expr) : expr =
  match e with
@@ -155,6 +156,11 @@ function subst_expr (e:expr) (x:ident) (t:expr) : expr =
  | Ebin e1 op e2 -> Ebin (subst_expr e1 x t) op (subst_expr e2 x t)
  end

+lemma eval_subst_expr:
+  forall s:state, e:expr, x:ident, t:expr.
+    eval_expr s (subst_expr e x t) =
+      eval_expr (IdMap.set s x (eval_expr s t)) e
+
 function subst (f:fmla) (x:ident) (t:expr) : fmla =
  match f with
  | Fterm e -> Fterm (subst_expr e x t)
@@ -164,12 +170,30 @@ lemma eval_subst:
  forall s:state, f:fmla, x:ident, t:expr.
    eval_fmla s (subst f x t) -> eval_fmla (IdMap.set s x (eval_expr s t)) f

+(* Hoare triples *)
+
+type triple = T fmla stmt fmla
+
+predicate valid_triple (t:triple) =
+  match t with
+  | T p i q ->
+    forall s:state. eval_fmla s p ->
+      forall s':state. many_steps s i s' Sskip ->
+        eval_fmla s' q
+  end
+
+
 (* Hoare logic rules *)

 lemma assign_rule:
  forall q:fmla, x:ident, e:expr.
  valid_triple (T (subst q x e) (Sassign x e) q)

+lemma seq_rule:
+  forall p q r:fmla, i1 i2:stmt.
+  valid_triple (T p i1 r) /\ valid_triple (T r i2 q) ->
+  valid_triple (T p (Sseq i1 i2) q)
+
 end


--- a/examples/hoare_logic/imp/imp_Imp_assign_rule_1.v
+++ b/examples/hoare_logic/imp/imp_Imp_assign_rule_1.v
@@ -135,6 +135,9 @@ Definition subst(f:fmla) (x:ident) (t:expr): fmla :=
  | (Fterm e) => (Fterm (subst_expr e x t))
  end.

+Axiom eval_subst : forall (s:(map ident Z)) (f:fmla) (x:ident) (t:expr),
+  (eval_fmla s (subst f x t)) -> (eval_fmla (set s x (eval_expr s t)) f).
+
 (* YOU MAY EDIT THE CONTEXT BELOW *)

 (* DO NOT EDIT BELOW *)
@@ -150,7 +153,7 @@ inversion H; subst.
 inversion H0; subst.
 (* normal case *)
 clear H Hred H0.
-apply subst_lemma.
+apply eval_subst; auto.

 (* absurd case *)
 inversion H1.

--- a/examples/hoare_logic/imp/why3session.xml
+++ b/examples/hoare_logic/imp/why3session.xml
@@ -10,6 +10,10 @@
  id="coq"
  name="Coq"
  version="8.2pl1"/>
+ <prover
+  id="coq-realize"
+  name="Coq Realize"
+  version="8.2pl1"/>
 <prover
  id="cvc3"
  name="CVC3"
@@ -58,7 +62,7 @@
    name="check_skip"
    sum="6e45bbe5f29a8cfd919ae1f08a1020e2"
    proved="true"
-    expanded="true"
+    expanded="false"
    shape="ainfix =V0aSskipNOainfix =V0aSskipF">
    <proof
     prover="cvc3"
@@ -79,7 +83,7 @@
    name="Test13"
    sum="e12eecbdd96b2281610235f2fcc63751"
    proved="true"
-    expanded="true"
+    expanded="false"
    shape="Laconstc0ainfix =aeval_exprV0aEconstc13c13">
    <proof
     prover="cvc3"
@@ -121,7 +125,7 @@
    name="Test42"
    sum="f8558a13a875934483ed332056b4cbbe"
    proved="true"
-    expanded="true"
+    expanded="false"
    shape="Lamk_identc0Lasetaconstc0V0c42ainfix =aeval_exprV1aEvarV0c42">
    <proof
     prover="cvc3"
@@ -163,7 +167,7 @@
    name="Test55"
    sum="dd37008f932e3fc376d52c430886f5b5"
    proved="true"
-    expanded="true"
+    expanded="false"
    shape="Lamk_identc0Lasetaconstc0V0c42ainfix =aeval_exprV1aEbinaEvarV0aOplusaEconstc13c55">
    <proof
     prover="cvc3"
@@ -184,7 +188,7 @@
    name="Ass42"
    sum="8042f4b04d21f83c438b7f3fa5ffefc2"
    proved="true"
-    expanded="true"
+    expanded="false"
    shape="Lamk_identc0Laconstc0ainfix =agetV2V0c42Iaone_stepV1aSassignV0aEconstc42V2aSskipF">
    <proof
     prover="cvc3"
@@ -205,7 +209,7 @@
    name="If42"
    sum="5d1dcda6f7eb3a2c6571b851ec21e278"
    proved="true"
-    expanded="true"
+    expanded="false"
    shape="Lamk_identc0Laconstc0ainfix =agetV3V0c42Iaone_stepV2V4V3aSskipIaone_stepV1aSifaEvarV0aSassignV0aEconstc13aSassignV0aEconstc42V2V4F">
    <proof
     prover="cvc3"
@@ -226,7 +230,7 @@
    name="progress"
    sum="edc177614e801c2dfa962191c2a4e85b"
    proved="true"
-    expanded="true"
+    expanded="false"
    shape="aone_stepV0V1V2V3EIainfix =V1aSskipNF">
    <proof
     prover="coq"
@@ -237,45 +241,73 @@
    </proof>
   </goal>
   <goal
-    name="assign_rule"
-    sum="2be3942838f1e6d9c24da52b80f6a313"
+    name="many_steps_seq"
+    sum="dae00dd4ef3b6c0bd2bac324a43f8912"
    proved="false"
    expanded="true"
-    shape="avalid_tripleaTasubstV0V1V2aSassignV1V2V0F">
+    shape="amany_stepsV4V3V1aSskipAamany_stepsV0V2V4aSskipEIamany_stepsV0aSseqV2V3V1aSskipF">
    <proof
     prover="coq"
     timelimit="5"
-     edited="imp_Imp_assign_rule_1.v"
-     obsolete="true">
-     <result status="unknown" time="0.47"/>
+     edited="imp_Imp_many_steps_seq_1.v"
+     obsolete="false">
+     <result status="unknown" time="0.46"/>
    </proof>
+   </goal>
+   <goal
+    name="eval_subst_expr"
+    sum="14cc95a56d17cee5b1dc5efb931894d4"
+    proved="false"
+    expanded="true"
+    shape="ainfix =aeval_exprV0asubst_exprV1V2V3aeval_exprasetV0V2aeval_exprV0V3V1F">
    <proof
-     prover="cvc3"
+     prover="coq"
     timelimit="5"
-     edited=""
+     edited="imp_Imp_eval_subst_expr_1.v"
     obsolete="false">
-     <result status="timeout" time="5.10"/>
+     <result status="unknown" time="0.43"/>
    </proof>
+   </goal>
+   <goal
+    name="eval_subst"
+    sum="de5b9237db9ed93a3dc89a621ff33ac1"
+    proved="true"
+    expanded="false"
+    shape="aeval_fmlaasetV0V2aeval_exprV0V3V1Iaeval_fmlaV0asubstV1V2V3F">
    <proof
-     prover="alt-ergo"
+     prover="coq"
     timelimit="5"
-     edited=""
+     edited="imp_Imp_eval_subst_2.v"
     obsolete="false">
-     <result status="timeout" time="5.03"/>
+     <result status="valid" time="0.43"/>
    </proof>
+   </goal>
+   <goal
+    name="assign_rule"
+    sum="41acd7707b568b56dbfbf43c39dc9142"
+    proved="true"
+    expanded="false"
+    shape="avalid_tripleaTasubstV0V1V2aSassignV1V2V0F">
    <proof
-     prover="z3"
+     prover="coq"
     timelimit="5"
-     edited=""
+     edited="imp_Imp_assign_rule_1.v"
     obsolete="false">
-     <result status="timeout" time="5.09"/>
+     <result status="valid" time="0.55"/>
    </proof>
+   </goal>
+   <goal
+    name="seq_rule"
+    sum="509f2baa69407fb64a13daf344618b5a"
+    proved="true"
+    expanded="false"
+    shape="avalid_tripleaTV0aSseqV3V4V1Iavalid_tripleaTV2V4V1Aavalid_tripleaTV0V3V2F">
    <proof
-     prover="vampire"
+     prover="z3"
     timelimit="5"
     edited=""
     obsolete="false">
-     <result status="timeout" time="5.08"/>
+     <result status="valid" time="0.17"/>
    </proof>
   </goal>
  </theory>