From 55eef82c54cc196fce759963693b5679bf946c06 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Wed, 6 Dec 2017 01:15:10 +0100
Subject: [PATCH] Th2.3: prove If rule

---
 wp.v | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/wp.v b/wp.v
index f7b4834..2913853 100644
--- a/wp.v
+++ b/wp.v
@@ -83,8 +83,8 @@ Fixpoint interp (inst: Instr) (mem: MemCpo) : MemCpo :=
         | seq instr1 instr2 => interp instr2 (interp instr1 (MemElem mem0))
         | ifelse guard instrIf instrElse =>
             if ((guard mem0) =? 0) % Z
-                then interp instrIf mem
-                else interp instrElse mem
+                then interp instrElse mem
+                else interp instrIf mem
         | while guard body =>
             let fix while_chain (mem: MemCpo) (n: nat): MemCpo :=
                 match n with
@@ -155,7 +155,7 @@ 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.
+    fun expr mem => (expr mem <> 0)%Z.
 
 Definition assertImplLogical (a1 a2: Assert): Prop :=
     forall (m: Mem), (a1 m) -> (a2 m).
@@ -240,4 +240,12 @@ Proof.
         apply (IHdeduction2 m). unfold hoare_consequence in IHdeduction1.
         specialize IHdeduction1 with mem as IH1_mem.
         rewrite mRel in IH1_mem. apply IH1_mem. assumption.
-    - 
+    - destruct (expr mem =? 0)%Z eqn:branchEqn.
+        * apply (IHdeduction2 mem). unfold assertOfExpr.
+          unfold assertAnd. split.
+            + assumption.
+            + unfold assertNot. rewrite <- Z.eqb_eq. congruence.
+        * apply (IHdeduction1 mem). unfold assertOfExpr.
+          unfold assertAnd. split.
+            + assumption.
+            + rewrite <- Z.eqb_eq. congruence.