# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1544860792 -32400
# Node ID bc819bdda3746dd3b015d4e97b68392a2e00890f
# Parent  46b301ad447892b2669d8172e2121a4837f96907
proof completed

diff -r 46b301ad4478 -r bc819bdda374 whileTestGears.agda
--- a/whileTestGears.agda	Sat Dec 15 11:57:18 2018 +0900
+++ b/whileTestGears.agda	Sat Dec 15 16:59:52 2018 +0900
@@ -2,70 +2,13 @@
 
 open import Function
 open import Data.Nat
-open import Data.Bool hiding ( _≟_ ; _∧_)
+open import Data.Bool hiding ( _≟_ )
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Binary.PropositionalEquality
 
-
-record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
-  field
-    pi1 : a
-    pi2 : b
-
-open  _∧_
-
-_-_ : ℕ -> ℕ -> ℕ 
-x - zero  = x
-zero - _  = zero
-(suc x) - (suc y)  = x - y
-
-sym1 : { y : ℕ } -> y + zero  ≡ y
-sym1 {zero} = refl
-sym1 {suc y} = cong ( λ x → suc x ) ( sym1 {y} )
-
-+-sym : { x y : ℕ } -> x + y ≡ y + x
-+-sym {zero} {zero} = refl
-+-sym {zero} {suc y} = let open ≡-Reasoning  in
-          begin
-            zero + suc y 
-          ≡⟨⟩
-            suc y
-          ≡⟨ sym sym1 ⟩
-            suc y + zero
-          ∎
-+-sym {suc x} {zero} =  let open ≡-Reasoning  in
-          begin
-            suc x + zero
-          ≡⟨ sym1  ⟩
-            suc x
-          ≡⟨⟩
-            zero + suc x
-          ∎
-+-sym {suc x} {suc y} = cong ( λ z → suc z ) (  let open ≡-Reasoning  in
-          begin
-            x + suc y
-          ≡⟨ +-sym {x} {suc y} ⟩
-            suc (y + x)
-          ≡⟨ cong ( λ z → suc z )  (+-sym {y} {x}) ⟩
-            suc (x + y)
-          ≡⟨ sym ( +-sym {y} {suc x}) ⟩
-            y + suc x
-          ∎ )
-
-minus-plus : { x y : ℕ } -> (suc x - 1) + (y + 1) ≡ suc x + y
-minus-plus {zero} {y} = +-sym {y} {1}
-minus-plus {suc x} {y} =  cong ( λ z → suc z ) (minus-plus {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
+open import utilities
+open  _/\_
 
 record Env  : Set where
   field
@@ -90,12 +33,12 @@
 proof1 : whileTest (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
 proof1 = refl
 
-whileTest' : {l : Level} {t : Set l}  -> (Code : (env : Env)  -> ((vari env) ≡ 0) ∧ ((varn env) ≡ 10) -> t) -> t
+whileTest' : {l : Level} {t : Set l}  -> (Code : (env : Env)  -> ((vari env) ≡ 0) /\ ((varn env) ≡ 10) -> t) -> t
 whileTest' next = next env proof2
   where
     env : Env
     env = record {vari = 0 ; varn = 10}
-    proof2 : ((vari env) ≡ 0) ∧ ((varn env) ≡ 10)
+    proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ 10)
     proof2 = record {pi1 = refl ; pi2 = refl}
     
 {-# TERMINATING #-}
@@ -111,7 +54,7 @@
       proof3 (s≤s lt) | suc n = {!!}
 
 
-conversion1 : {l : Level} {t : Set l } → (env : Env) -> ((vari env) ≡ 0) ∧ ((varn env) ≡ 10)
+conversion1 : {l : Level} {t : Set l } → (env : Env) -> ((vari env) ≡ 0) /\ ((varn env) ≡ 10)
                -> (Code : (env1 : Env) -> (varn env1 + vari env1 ≡ 10) -> t) -> t
 conversion1 env p1 next = next env proof4
    where
diff -r 46b301ad4478 -r bc819bdda374 whileTestPrim.agda
--- 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
+          ∎
+        )
 
 
+