WP for while, partial proof

examples/hoare_logic/wp2.mlw

@@ -398,7 +398,7 @@ module WP
     { forall sigma pi sigma' pi':env, w:Set.set ident .
         eval_fmla sigma pi f /\ stmt_writes i w /\
         assigns sigma w sigma' ->
-        eval_fmla sigma' pi' f
+        eval_fmla sigma' pi' result
      }
 
   let rec wp (i:stmt) (q:fmla) =

examples/hoare_logic/wp2/why3session.xml

@@ -901,10 +901,10 @@
     locfile="wp2/../wp2.mlw"
     loclnum="404" loccnumb="10" loccnume="12"
     expl="parameter wp"
-    sum="dcafb8261f30f6ebb50461a7f178823e"
+    sum="6016991fbe22c1568eb59dfa2d21135c"
     proved="false"
     expanded="true"
-    shape="CV0aSskipavalid_tripleV1V0V1aSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVavalid_tripleaFletV8V7asubstV1V6V8V0V1Iafresh_in_fmlaV8V1FaSifVVVavalid_tripleaFandaFimpliesaFtermV9V12aFimpliesaFnotaFtermV9V13V0V1Iavalid_tripleV13V11V1FIavalid_tripleV12V10V1FaSassertVavalid_tripleaFimpliesV14V1V0V1aSwhileVVVavalid_tripleaFandV16V19V0V1Iaeval_fmlaV22V23aFandaFimpliesaFandaFtermV15V16V18aFimpliesaFandaFnotaFtermV15V16V1IaassignsV20V24V22Aastmt_writesV17V24Aaeval_fmlaV20V21aFandaFimpliesaFandaFtermV15V16V18aFimpliesaFandaFnotaFtermV15V16V1FFIavalid_tripleV18V17V16FFF">
+    shape="CV0aSskipavalid_tripleV1V0V1aSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVavalid_tripleaFletV8V7asubstV1V6V8V0V1Iafresh_in_fmlaV8V1FaSifVVVavalid_tripleaFandaFimpliesaFtermV9V12aFimpliesaFnotaFtermV9V13V0V1Iavalid_tripleV13V11V1FIavalid_tripleV12V10V1FaSassertVavalid_tripleaFimpliesV14V1V0V1aSwhileVVVavalid_tripleaFandV16V19V0V1Iaeval_fmlaV22V23V19IaassignsV20V24V22Aastmt_writesV17V24Aaeval_fmlaV20V21aFandaFimpliesaFandaFtermV15V16V18aFimpliesaFandaFnotaFtermV15V16V1FFIavalid_tripleV18V17V16FFF">
     <label
      name="expl:parameter wp">
      </label>
@@ -1130,10 +1130,10 @@
       locfile="wp2/../wp2.mlw"
       loclnum="404" loccnumb="10" loccnume="12"
       expl="parameter wp"
-      sum="99d3b823822394e2f7ed9d01bb5f5c5e"
+      sum="266ccf12817473194352d201a62731c0"
       proved="false"
       expanded="true"
-      shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVavalid_tripleaFandV11V14V0V1Iaeval_fmlaV17V18aFandaFimpliesaFandaFtermV10V11V13aFimpliesaFandaFnotaFtermV10V11V1IaassignsV15V19V17Aastmt_writesV12V19Aaeval_fmlaV15V16aFandaFimpliesaFandaFtermV10V11V13aFimpliesaFandaFnotaFtermV10V11V1FFIavalid_tripleV13V12V11FFF">
+      shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVavalid_tripleaFandV11V14V0V1Iaeval_fmlaV17V18V14IaassignsV15V19V17Aastmt_writesV12V19Aaeval_fmlaV15V16aFandaFimpliesaFandaFtermV10V11V13aFimpliesaFandaFnotaFtermV10V11V1FFIavalid_tripleV13V12V11FFF">
       <label
        name="expl:parameter wp">
        </label>

examples/hoare_logic/wp2/wp2_WP_WP_WP_parameter_wp_2.v

@@ -183,7 +183,7 @@ Fixpoint subst(f:fmla) (x:Z) (v:Z) {struct f}: fmla :=
   | (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 t (subst f1 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.
@@ -427,11 +427,33 @@ Theorem WP_parameter_wp : forall (i:stmt), forall (q:fmla),
       value)) (sigmaqt:(map Z value)) (piqt:(map Z value)) (w:(set1 Z)),
       ((eval_fmla sigma pi (Fand (Fimplies (Fand (Fterm e) inv) result)
       (Fimplies (Fand (Fnot (Fterm e)) inv) q))) /\ ((stmt_writes i1 w) /\
-      (assigns sigma w sigmaqt))) -> (eval_fmla sigmaqt piqt
-      (Fand (Fimplies (Fand (Fterm e) inv) result)
-      (Fimplies (Fand (Fnot (Fterm e)) inv) q)))) -> (valid_triple (Fand inv
-      result1) i q)
+      (assigns sigma w sigmaqt))) -> (eval_fmla sigmaqt piqt result1)) ->
+      (valid_triple (Fand inv result1) i q)
   end.
+destruct i; trivial.
+rename t into cond.
+rename f into inv.
+rename i into body.
+intros Post WP_body H_WP_body.
+intros abstracted_fmla H_abstracted.
+red.
+intros s1 p1 H1 s2 p2 n Hsteps.
+generalize (steps_non_neg _ _ _ _ _ _ _ Hsteps).
+intro H_n_pos.
+generalize s1 p1 H1 Hsteps; clear s1 p1 H1 Hsteps.
+apply Z_lt_induction with (P := 
+  fun n => forall s1 p1 : map Z value,
+    eval_fmla s1 p1 (Fand inv abstracted_fmla) ->
+    many_steps s1 p1 (Swhile cond inv body) s2 p2 Sskip n ->
+    eval_fmla s2 p2 Post); auto.
+intros.
+inversion H1; subst; clear H1.
+inversion H2; subst; clear H2.
+generalize (many_steps_seq _ _ _ _ _ _ _ H3); clear H3.
+intros (s3 & p3 & n1 & n2 & First_iter & Next_iter & Hn1n2).
+generalize (steps_non_neg _ _ _ _ _ _ _ First_iter); intro Hn1_pos.
+generalize (steps_non_neg _ _ _ _ _ _ _ Next_iter); intro Hn2_pos.
+apply H with (3:=Next_iter); auto with zarith.
 
 Qed.