--- a/whileTestPrim.agda	Sat Dec 15 11:57:18 2018 +0900
+++ b/whileTestPrim.agda	Sat Dec 15 16:59:52 2018 +0900
@@ -7,6 +7,7 @@
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Binary.PropositionalEquality
 
+open import utilities
 
 record Env : Set where
   field
@@ -28,86 +29,6 @@
   If    : Cond -> Comm -> Comm -> Comm
   While : Cond -> Comm -> Comm
 
-_-_ : ℕ -> ℕ -> ℕ
-x - zero  = x
-zero - _  = zero
-(suc x) - (suc y)  = x - y
-
-lt : ℕ -> ℕ -> Bool
-lt x y with suc x  ≤? y
-lt x y | yes p = true
-lt x y | no ¬p = false
-
-Equal : ℕ -> ℕ -> Bool
-Equal x y with x ≟ y
-Equal x y | yes p = true
-Equal x y | no ¬p = false
-
----------------------------
-
-implies : Bool → Bool → Bool
-implies false _ = true
-implies true true = true
-implies true false = false
-
-impl-1 : {x : Bool} → implies x true  ≡ true
-impl-1 {x} with x
-impl-1 {x} | false = refl
-impl-1 {x} | true = refl
-
-impl-2 : {x : Bool} → implies false x  ≡ true
-impl-2 {x} with x
-impl-2 {x} | false = refl
-impl-2 {x} | true = refl
-
-and-lemma-1 : { x y : Bool } → x  ∧  y  ≡ true  → x  ≡ true
-and-lemma-1 {x} {y} eq with x | y | eq
-and-lemma-1 {x} {y} eq | false | b | ()
-and-lemma-1 {x} {y} eq | true | false | ()
-and-lemma-1 {x} {y} eq | true | true | refl = refl
-
-and-lemma-2 : { x y : Bool } →  x  ∧  y  ≡ true  → y  ≡ true
-and-lemma-2 {x} {y} eq with x | y | eq
-and-lemma-2 {x} {y} eq | false | b | ()
-and-lemma-2 {x} {y} eq | true | false | ()
-and-lemma-2 {x} {y} eq | true | true | refl = refl
-
-bool-case : ( x : Bool ) { p : Set } → ( x ≡ true  → p ) → ( x ≡ false  → p ) → p
-bool-case x T F with x
-bool-case x T F | false = F refl
-bool-case x T F | true = T refl
-
-impl :  {x y : Bool} → (x  ≡ true → y  ≡ true ) → implies x y  ≡ true
-impl {x} {y} p = bool-case x (λ x=t →   let open ≡-Reasoning  in
-          begin
-            implies x y
-          ≡⟨  cong ( \ z -> implies x z ) (p x=t ) ⟩
-            implies x true
-          ≡⟨ impl-1 ⟩
-            true
-          ∎
-    ) ( λ x=f →  let open ≡-Reasoning  in
-          begin
-            implies x y
-          ≡⟨  cong ( \ z -> implies z y ) x=f ⟩
-            true
-          ∎
-  )
- 
-eqlemma : { x y : ℕ } →  Equal x y ≡ true → x ≡ y
-eqlemma {x} {y} eq with x ≟ y
-eqlemma {x} {y} refl | yes refl = refl
-eqlemma {x} {y} () | no ¬p 
-
-eqlemma1 : { x y : ℕ } →  Equal x y ≡ Equal (suc x) (suc y)
-eqlemma1 {x} {y} with  x ≟ y
-eqlemma1 {x} {.x} | yes refl = refl
-eqlemma1 {x} {y} | no ¬p = refl
-
-add-lemma1 : { x : ℕ } → x + 1 ≡ suc x
-add-lemma1 {zero} = refl
-add-lemma1 {suc x} = cong ( \ z -> suc z ) ( add-lemma1 {x} )
-
 ---------------------------
 
 program : Comm
@@ -151,13 +72,13 @@
 
 
 Axiom : Cond -> PrimComm -> Cond -> Set
-Axiom pre comm post = ∀ (env : Env) →  implies (pre env) ( post (comm env)) ≡ true
+Axiom pre comm post = ∀ (env : Env) →  (pre env) ⇒ ( post (comm env)) ≡ true
 
 Tautology : Cond -> Cond -> Set
-Tautology pre post = ∀ (env : Env) →  implies (pre env) (post env) ≡ true
+Tautology pre post = ∀ (env : Env) →  (pre env)  ⇒ (post env) ≡ true
 
-_/\_ :  Cond -> Cond -> Cond
-x /\ y =  λ env → x env ∧ y env 
+_and_ :  Cond -> Cond -> Cond
+x and y =  λ env → x env ∧ y env 
 
 neg :  Cond -> Cond 
 neg x  =  λ env → not ( x env )
@@ -183,12 +104,12 @@
   IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
            {bPre : Cond} -> {bPost : Cond} ->
            {b : Cond} ->
-           HTProof (bPre /\ b) cmThen bPost ->
-           HTProof (bPre /\ neg b) cmElse bPost ->
+           HTProof (bPre and b) cmThen bPost ->
+           HTProof (bPre and neg b) cmElse bPost ->
            HTProof bPre (If b cmThen cmElse) bPost
   WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
-              HTProof (bInv /\ b) cm bInv ->
-              HTProof bInv (While b cm) (bInv /\ neg b)
+              HTProof (bInv and b) cm bInv ->
+              HTProof bInv (While b cm) (bInv and neg b)
 
 initCond : Cond
 initCond env = true
@@ -203,7 +124,7 @@
 whileInv env = Equal ((varn env) + (vari env)) 10
 
 whileInv' : Cond
-whileInv' env = Equal ((varn env) + (vari env)) 11
+whileInv' env = Equal ((varn env) + (vari env)) 11 ∧ lt zero (varn env)
 
 termCond : Cond
 termCond env = Equal (vari env) 10
@@ -236,9 +157,9 @@
      lemma1 env | false = refl
      lemma1 env | true = refl
      lemma21 : {env : Env } → stmt2Cond env ≡ true → varn env ≡ 10
-     lemma21 eq = eqlemma (and-lemma-1 eq)
+     lemma21 eq = Equal→≡ (∧-pi1 eq)
      lemma22 : {env : Env } → stmt2Cond env ≡ true → vari env ≡ 0
-     lemma22 eq = eqlemma (and-lemma-2 eq)
+     lemma22 eq = Equal→≡ (∧-pi2 eq)
      lemma23 :  {env : Env } → stmt2Cond env ≡ true → varn env + vari env ≡ 10
      lemma23 {env} eq = let open ≡-Reasoning  in
           begin
@@ -252,44 +173,93 @@
      lemma2 env = bool-case (stmt2Cond env) (
         λ eq → let open ≡-Reasoning  in
           begin
-            implies (stmt2Cond env) (whileInv env)
+            (stmt2Cond env)  ⇒  (whileInv env)
           ≡⟨⟩
-            implies (stmt2Cond env) ( Equal (varn env + vari env) 10 )
-          ≡⟨  cong ( \ x -> implies (stmt2Cond env) ( Equal x 10 ) ) ( lemma23 {env} eq ) ⟩
-            implies (stmt2Cond env) (Equal 10 10)
+            (stmt2Cond env)  ⇒ ( Equal (varn env + vari env) 10 )
+          ≡⟨  cong ( \ x -> (stmt2Cond env)  ⇒ ( Equal x 10 ) ) ( lemma23 {env} eq ) ⟩
+            (stmt2Cond env)  ⇒ (Equal 10 10)
           ≡⟨⟩
-            implies (stmt2Cond env) true
-          ≡⟨ impl-1 ⟩
+            (stmt2Cond env)  ⇒  true
+          ≡⟨ ⇒t ⟩
             true
           ∎
         ) (
          λ ne → let open ≡-Reasoning  in
           begin
-            implies (stmt2Cond env) (whileInv env)
-          ≡⟨ cong ( \ x -> implies x (whileInv env) ) ne ⟩
-             implies false (whileInv env)
-          ≡⟨ impl-2 {whileInv env} ⟩
+            (stmt2Cond env)  ⇒  (whileInv env)
+          ≡⟨ cong ( \ x -> x  ⇒  (whileInv env) ) ne ⟩
+             false  ⇒  (whileInv env)
+          ≡⟨ f⇒ {whileInv env} ⟩
             true
           ∎
         ) 
      lemma3 :   Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv'
-     lemma3 env = impl ( λ cond →  let open ≡-Reasoning  in
+     lemma3 env = impl⇒ ( λ cond →  let open ≡-Reasoning  in
           begin
             whileInv' (record { varn = varn env ; vari = vari env + 1 }) 
           ≡⟨⟩
+             Equal (varn env + (vari env + 1)) 11 ∧ (lt 0 (varn env) )
+          ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) 11 ∧ z ) (∧-pi2 cond )  ⟩
+             Equal (varn env + (vari env + 1)) 11 ∧ true
+          ≡⟨ ∧true ⟩
             Equal (varn env + (vari env + 1)) 11
           ≡⟨ cong ( \ x -> Equal x 11 ) (sym (+-assoc (varn env) (vari env) 1)) ⟩
             Equal ((varn env + vari env) + 1) 11
-          ≡⟨ cong ( \ x -> Equal x 11 ) add-lemma1 ⟩
+          ≡⟨ cong ( \ x -> Equal x 11 ) +1≡suc ⟩
             Equal (suc (varn env + vari env)) 11
-          ≡⟨ sym eqlemma1 ⟩
+          ≡⟨ sym Equal+1 ⟩
             Equal ((varn env + vari env) ) 10
-          ≡⟨ and-lemma-1 cond ⟩
+          ≡⟨ ∧-pi1  cond ⟩
             true
           ∎ )
+     lemma41 : (env : Env ) → (varn env + vari env) ≡ 11 → lt 0 (varn env) ≡ true  → Equal ((varn env - 1) + vari env) 10 ≡ true
+     lemma41 env c1 c2 =  let open ≡-Reasoning  in
+          begin
+            Equal ((varn env - 1) + vari env) 10
+          ≡⟨ cong ( λ z → Equal ((z - 1 ) +  vari env ) 10 ) (sym (suc-predℕ=n c2) )  ⟩
+            Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) 10
+          ≡⟨⟩
+            Equal ((predℕ {varn env} c2 ) + vari env) 10
+          ≡⟨  Equal+1 ⟩
+            Equal ((suc (predℕ {varn env} c2 )) + vari env) 11
+          ≡⟨ cong ( λ z → Equal (z  +  vari env ) 11 ) (suc-predℕ=n c2 )  ⟩
+            Equal (varn env + vari env) 11
+          ≡⟨ cong ( λ z → (Equal z 11 )) c1 ⟩
+            Equal 11 11
+          ≡⟨⟩
+            true
+          ∎
      lemma4 :  Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
-     lemma4 env = {!!}
-     lemma5 :  Tautology ((λ e → Equal (varn e + vari e) 10) /\ neg (λ z → lt zero (varn z))) termCond
-     lemma5 env = {!!}
+     lemma4 env = impl⇒ ( λ cond → let open ≡-Reasoning  in
+          begin
+            whileInv (record { varn = varn env - 1 ; vari = vari env })
+          ≡⟨⟩
+            Equal ((varn env - 1) + vari env) 10
+          ≡⟨ lemma41 env (Equal→≡ (∧-pi1  cond)) (∧-pi2  cond) ⟩
+            true
+          ∎
+        )
+     lemma51 : (z : Env ) → neg (λ z → lt zero (varn z)) z ≡ true → varn z ≡ zero
+     lemma51 z cond with lt zero (varn z) | (suc zero) ≤? (varn z)
+     lemma51 z () | false | yes p
+     lemma51 z () | true | yes p
+     lemma51 z refl | _ | no ¬p with varn z
+     lemma51 z refl | _ | no ¬p | zero = refl
+     lemma51 z refl | _ | no ¬p | suc x = ⊥-elim ( ¬p (s≤s z≤n ) )
+     lemma5 :  Tautology ((λ e → Equal (varn e + vari e) 10) and (neg (λ z → lt zero (varn z)))) termCond
+     lemma5 env = impl⇒ ( λ cond → let open ≡-Reasoning  in
+         begin
+            termCond env
+          ≡⟨⟩
+             Equal (vari env) 10 
+          ≡⟨⟩
+             Equal (zero + vari env) 10 
+          ≡⟨ cong ( λ z →  Equal (z + vari env) 10 )  (sym ( lemma51 env ( ∧-pi2  cond ) )) ⟩
+             Equal (varn env + vari env) 10 
+          ≡⟨ ∧-pi1  cond  ⟩
+             true
+          ∎
+        )
 
 
+