Prove Th2.3 up to consequence

wp.v

@@ -157,8 +157,8 @@ Notation "a [[ x <- 'expr' z ]]" := (substAssertExpr a x z)
 Definition assertOfExpr : Expr -> Assert :=
     fun expr mem => expr mem <> 0%Z.
 
-Definition assertImplLogical : Assert -> Assert -> Prop :=
+Definition assertImplLogical (a1 a2: Assert): Prop :=
-    fun a1 a2 => forall (m : Mem), (a1 m) -> (a2 m).
+    forall (m: Mem), (a1 m) -> (a2 m).
 
 
 (***** Hoare provability *****************************************************)
@@ -212,10 +212,32 @@ Definition hoare_consequence (pre: Assert) (instr: Instr) (post: Assert) :=
 Notation "|= [| pre  |] instr  [| post |]" :=
         (hoare_consequence pre instr post) (at level 30): assert.
 
+Lemma weaken_in_conseq:
+    forall a1, forall a2, forall m,
+    assertImplLogical a1 a2 -> conseq_or_bottom a1 m ->
+        conseq_or_bottom a2 m.
+Proof.
+    intros a1 a2 m impl conseq. destruct m.
+    - apply conseq.
+    - simpl. unfold assertImplLogical in impl. apply (impl m). apply conseq.
+Qed.
+
+
 Theorem hoare_provability_implies_consequence :
     forall (pre: Assert), forall (s: Instr), forall (post: Assert),
     ( |- [| pre |] s [| post |] ) % assert
             -> ( |= [| pre |] s [| post |] ) % assert.
 Proof.
-    (* TODO *)
+    intros pre instr post. intros deduction.
-Admitted.
+    induction deduction; intros mem preInMem; simpl.
+    - exact preInMem.
+    - trivial.
+    - exact preInMem.
+    - apply (weaken_in_conseq post' post (interp s (MemElem mem)) H0).
+      apply IHdeduction. apply H. exact preInMem.
+    - destruct (interp s1 (MemElem mem)) eqn:mRel.
+        admit.
+        apply (IHdeduction2 m). unfold hoare_consequence in IHdeduction1.
+        specialize IHdeduction1 with mem as IH1_mem.
+        rewrite mRel in IH1_mem. apply IH1_mem. assumption.
+    -