Annotate while with invariants in the language

wp.v

@@ -11,13 +11,26 @@ Definition Var := nat.
 Definition Mem := Var -> Z.
 Definition Expr:= Mem -> Z.
 
+Inductive SynAssert : Type:=
+| ATop: SynAssert
+| ABot: SynAssert
+| ANeg: SynAssert -> SynAssert
+| AAnd: SynAssert -> SynAssert -> SynAssert
+| AOr: SynAssert -> SynAssert -> SynAssert
+| AImplies: SynAssert -> SynAssert -> SynAssert
+| AExpr: Expr -> SynAssert
+| AForall: Var -> SynAssert -> SynAssert
+| AExists: Var -> SynAssert -> SynAssert
+| ASubstZ: Var -> Z -> SynAssert -> SynAssert
+| ASubstE: Var -> Expr -> SynAssert -> SynAssert.
+
 Inductive Instr : Type :=
 | skip: Instr
 | abort: Instr
 | assign: Var -> Expr -> Instr
 | seq: Instr -> Instr -> Instr
 | ifelse: Expr -> Instr -> Instr -> Instr
-| while: Expr -> Instr -> Instr.
+| while: SynAssert -> Expr -> Instr -> Instr.
 
 Definition ifonly (exp: Expr) (inst: Instr) : Instr :=
   ifelse exp inst skip.
@@ -87,7 +100,7 @@ Fixpoint interp (inst: Instr) (mem: MemCpo) : MemCpo :=
       if ((guard mem0) =? 0) % Z
         then interp instrElse mem
         else interp instrIf mem
-    | while guard body =>
+    | while _ guard body =>
       let fix while_chain (mem: MemCpo) (n: nat): MemCpo :=
         match n with
         | 0 => mem
@@ -129,16 +142,16 @@ Definition expr_neg (expr: Expr) : Expr :=
   | _ => 0%Z
   end.
 
-Lemma certain_termination_exists body guard mem :
+Lemma certain_termination_exists assert body guard mem :
-  interp (while guard body) mem <> MemError ->
+  interp (while assert guard body) mem <> MemError ->
     exists n: nat,
       interp (nth_iterate (ifonly guard body) n) mem |=e expr_neg guard.
 Proof.
   intros noError.
 Admitted.
 
-Lemma certain_termination_exists_minimal body guard mem :
+Lemma certain_termination_exists_minimal assert body guard mem :
-  interp (while guard body) mem <> MemError ->
+  interp (while assert guard body) mem <> MemError ->
     exists n: nat,
       (forall p: nat, p < n ->
         interp (nth_iterate (ifonly guard body) p) mem |=e guard)
@@ -147,15 +160,15 @@ Proof.
   intros not_error.
 Admitted.
 
-Lemma certain_termination body guard mem :
+Lemma certain_termination assert body guard mem :
-  interp (while guard body) mem <> MemError ->
+  interp (while assert guard body) mem <> MemError ->
     exists n: nat,
       (interp (nth_iterate body n) mem) |=e (expr_neg guard)
      /\ (forall p, p < n -> (interp (nth_iterate body p) mem) |=e guard)
-     /\ interp (while guard body) mem = interp (nth_iterate body n) mem.
+     /\ interp (while assert guard body) mem = interp (nth_iterate body n) mem.
 Proof.
   intros notError.
-  elim (certain_termination_exists_minimal body guard mem).
+  elim (certain_termination_exists_minimal assert body guard mem).
   intros n. intros [notBeforeN atN]. exists n.
   split.
 Admitted.
@@ -240,9 +253,9 @@ Inductive hoare_provability : Assert -> Instr -> Assert -> Prop :=
       (|- [| pre /\ ~(assertOfExpr expr) |] sElse [| post |]) % assert ->
       (|- [| pre |] (ifelse expr sIf sElse) [| post |]) % assert
   | H_while:
-    forall inv, forall expr, forall sBody,
+    forall inv assert expr sBody,
     (|- [| inv /\ (assertOfExpr expr) |] sBody [| inv |]) % assert ->
-      (|- [| inv |] (while expr sBody)
+      (|- [| inv |] (while assert expr sBody)
           [| inv /\ ~ (assertOfExpr expr) |]) % assert
 where "|- [| pre  |] instr  [| post |]" :=
     (hoare_provability pre instr post) : assert.
@@ -390,9 +403,9 @@ Proof.
       + assumption.
       + rewrite <- Z.eqb_eq. congruence.
   - unfold conseq_or_bottom.
-    destruct (interp (while expr sBody) (MemElem mem)) eqn:interpRel.
+    destruct (interp (while assert expr sBody) (MemElem mem)) eqn:interpRel.
     * trivial.
-    * elim (certain_termination sBody expr (MemElem mem)).
+    * elim (certain_termination assert sBody expr (MemElem mem)).
       intros n [lastIter [notLastIter isWhile] ].
       rewrite isWhile in interpRel.
       destruct n.
@@ -440,6 +453,23 @@ Proof.
       + rewrite interpRel; unfold MemError; congruence.
 Qed.
 
+(***** Syntactic assertion interpretation ************************************)
+
+Fixpoint aInterp (src: SynAssert): Assert :=
+  fun (mem: Mem) => match src with
+  | ATop => True
+  | ABot => False
+  | ANeg x => ~ (aInterp x mem)
+  | AAnd x y => (aInterp x mem) /\ (aInterp y mem)
+  | AOr x y => (aInterp x mem) \/ (aInterp y mem)
+  | AImplies x y => (~ (aInterp x mem)) \/ (aInterp y mem)
+  | AExpr exp => exp mem <> 0%Z
+  | AForall v x => forall (z: Z), aInterp x (mem [v <- z])
+  | AExists v x => exists (z: Z), aInterp x (mem [v <- z])
+  | ASubstZ v z x => aInterp x (mem [v <- z])
+  | ASubstE v e x => aInterp x (mem [v <- (e mem)])
+  end.
+
 (***** Weakest precondition **************************************************)
 
 Fixpoint wp (instr: Instr) (cond: Assert) : Assert := match instr with
@@ -450,7 +480,7 @@ Fixpoint wp (instr: Instr) (cond: Assert) : Assert := match instr with
 | ifelse guard sIf sElse =>
     ((assertOfExpr guard -> wp sIf cond)
      /\ (~ (assertOfExpr guard) -> wp sElse cond)) % assert
-| while guard body => assertBot
+| while assert guard body => assertBot
 end.
 
 Lemma assertImplElim {a b: Assert} :
@@ -527,7 +557,7 @@ Proof.
   * apply (H_conseq
       assertBot post
       assertBot (assertBot /\ ~ (assertOfExpr e))%assert).
-    - apply (H_while assertBot e instr).
+    - apply (H_while assertBot s e instr).
       apply (H_conseq
         (assertBot /\ assertOfExpr e)%assert assertBot
         assertBot assertBot).
@@ -585,35 +615,7 @@ Proof.
   apply wp_correctness_provable.
 Qed.
 
-(***** Assertions syntaxiques******** ****************************************)
+(***** Assertions syntaxiques -- proprietes **********************************)
-
-Inductive SynAssert : Type:=
-| ATop: SynAssert
-| ABot: SynAssert
-| ANeg: SynAssert -> SynAssert
-| AAnd: SynAssert -> SynAssert -> SynAssert
-| AOr: SynAssert -> SynAssert -> SynAssert
-| AImplies: SynAssert -> SynAssert -> SynAssert
-| AExpr: Expr -> SynAssert
-| AForall: Var -> SynAssert -> SynAssert
-| AExists: Var -> SynAssert -> SynAssert
-| ASubstZ: Var -> Z -> SynAssert -> SynAssert
-| ASubstE: Var -> Expr -> SynAssert -> SynAssert.
-
-Fixpoint aInterp (src: SynAssert): Assert :=
-  fun (mem: Mem) => match src with
-  | ATop => True
-  | ABot => False
-  | ANeg x => ~ (aInterp x mem)
-  | AAnd x y => (aInterp x mem) /\ (aInterp y mem)
-  | AOr x y => (aInterp x mem) \/ (aInterp y mem)
-  | AImplies x y => (~ (aInterp x mem)) \/ (aInterp y mem)
-  | AExpr exp => exp mem <> 0%Z
-  | AForall v x => forall (z: Z), aInterp x (mem [v <- z])
-  | AExists v x => exists (z: Z), aInterp x (mem [v <- z])
-  | ASubstZ v z x => aInterp x (mem [v <- z])
-  | ASubstE v e x => aInterp x (mem [v <- (e mem)])
-  end.
 
 Fixpoint wps (instr: Instr) (asser: SynAssert) : SynAssert := match instr with
 | skip => asser
@@ -624,7 +626,7 @@ Fixpoint wps (instr: Instr) (asser: SynAssert) : SynAssert := match instr with
     AAnd
       (AImplies (AExpr guard) (wps sIf asser))
       (AImplies (ANeg (AExpr guard)) (wps sElse asser))
-| while guard body => ABot
+| while assert guard body => ABot
 end.
 
 Lemma aInterpConsistent (instr: Instr):