Modify notation, state theorem 2.3

wp.v

@@ -147,9 +147,77 @@ Notation "'exists_m' x" := (existsMemForall x)
 
 Definition substAssert : Assert -> Var -> Z -> Assert :=
     fun asser ident val mem => asser (mem [ident <- val]).
-Notation "a < x <- z >" := (substAssert a x z)
+Notation "a [[ x <- z ]]" := (substAssert a x z)
     (at level 50, left associativity).
 Definition substAssertExpr : Assert -> Var -> Expr -> Assert :=
     fun asser ident expr mem => asser (mem [ident <- (expr mem)]).
-Notation "a < x <- 'expr' z >" := (substAssertExpr a x z)
+Notation "a [[ x <- 'expr' z ]]" := (substAssertExpr a x z)
     (at level 50, left associativity).
+
+Definition assertOfExpr : Expr -> Assert :=
+    fun expr mem => expr mem <> 0%Z.
+
+Definition assertImplLogical : Assert -> Assert -> Prop :=
+    fun a1 a2 => forall (m : Mem), (a1 m) -> (a2 m).
+
+
+(***** Hoare provability *****************************************************)
+
+Parameter  hoare_provability : Assert -> Instr -> Assert -> Prop.
+Notation "|- [| pre  |] instr  [| post |]" :=
+        (hoare_provability pre instr post) (at level 30): assert.
+
+Axiom h_skip: forall (asser: Assert), ( |- [|asser|] skip [|asser|]) % assert.
+Axiom h_abort: forall (a1:Assert), forall (a2: Assert),
+    (|- [|a1|] abort [|a2|]) % assert.
+Axiom h_assign: forall (asser: Assert), forall (x: Var), forall (e: Expr),
+    (|- [| asser [[ x <- expr e ]] |] (assign x e) [|asser|]) % assert.
+Axiom h_conseq:
+    forall (a1: Assert), forall (a1': Assert),
+    forall (a2: Assert), forall (a2': Assert),
+    forall (s: Instr),
+    (|- [| a1' |] s [| a2' |]) % assert ->
+            (assertImplLogical a1 a1') ->
+            (assertImplLogical a2' a2) ->
+            (|- [| a1 |] s [| a2 |]) % assert.
+Axiom h_seq:
+    forall (a1: Assert), forall (a2: Assert), forall (a3: Assert),
+    forall (s1: Instr), forall (s2: Instr),
+    (|- [|a1|] s1 [|a2|]) % assert -> (|- [|a2|] s2 [|a3|]) % assert ->
+            (|- [|a1|] (seq s1 s2) [|a3|]) % assert.
+Axiom h_if:
+    forall (a1: Assert), forall (a2: Assert),
+    forall (e: Expr),
+    forall (s1: Instr), forall (s2: Instr),
+    (|- [| a1 /\ (assertOfExpr e) |] s1 [| a2 |]) % assert ->
+        (|- [| a1 /\ ~ (assertOfExpr e) |] s2 [| a2 |]) % assert ->
+        (|- [| a1 |] (ifelse e s1 s2) [| a2 |]) % assert.
+Axiom h_while:
+    forall (inv: Assert),
+    forall (e: Expr),
+    forall (s: Instr),
+    (|- [| inv /\ (assertOfExpr e) |] s [| inv |]) % assert ->
+        (|- [| inv |] (while e s) [| inv /\ ~ (assertOfExpr e) |]) % assert.
+
+(***** Hoare: provability implies consequence ********************************)
+
+Definition conseq_or_bottom (y: Assert) (m: MemCpo) :=
+    match m with
+    | CpoError _ => True
+    | CpoElem _ m0 => y m0
+    end.
+
+Definition hoare_consequence (pre: Assert) (instr: Instr) (post: Assert) :=
+    forall mem: Mem,
+    (pre mem) -> (conseq_or_bottom post (interp instr (MemElem mem))).
+
+Notation "|= [| pre  |] instr  [| post |]" :=
+        (hoare_consequence pre instr post) (at level 30): assert.
+
+Theorem hoare_provability_implies_consequence :
+    forall (pre: Assert), forall (s: Instr), forall (post: Assert),
+    ( |- [| pre |] s [| post |] ) % assert
+            -> ( |= [| pre |] s [| post |] ) % assert.
+Proof.
+    (* TODO *)
+Admitted.