# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1544792784 -32400
# Node ID 28e80739eed6a61738df6bd0ef83fdc3f8be02f5
# Parent  17e4f3b5814881ef9d293dfb8ad78dbe5e8af689
fix whileTestGears

diff -r 17e4f3b58148 -r 28e80739eed6 whileTestGears.agda
--- a/whileTestGears.agda	Fri Dec 14 19:51:54 2018 +0900
+++ b/whileTestGears.agda	Fri Dec 14 22:06:24 2018 +0900
@@ -8,21 +8,54 @@
 open import Relation.Binary.PropositionalEquality
 
 
-record Env  : Set where
+record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
   field
-    varn : ℕ
-    vari : ℕ
-open Env
+    pi1 : a
+    pi2 : b
+
+open  _∧_
 
 _-_ : ℕ -> ℕ -> ℕ 
 x - zero  = x
 zero - _  = zero
 (suc x) - (suc y)  = x - y
 
-record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
-  field
-    pi1 : a
-    pi2 : b
+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
@@ -34,6 +67,12 @@
 Equal x y | yes p = true
 Equal x y | no ¬p = false
 
+record Env  : Set where
+  field
+    varn : ℕ
+    vari : ℕ
+open Env
+
 whileTest : {l : Level} {t : Set l} -> (Code : Env -> t) -> t
 whileTest next = next (record {varn = 10 ; vari = 0} )
 
@@ -52,14 +91,6 @@
 proof1 = refl
 
 
-record EnvWithCond : Set (succ Zero) where
-  field
-    input : Env
-    condition : Set
-    proof : condition
-open EnvWithCond
-
-
 
 -- stmt2Cond : {l : Level} → EnvWithCond {l} → 
 -- stmt2Cond env = (Equal (varn' env) 10) ∧ (Equal (vari' env) 0)
@@ -80,11 +111,32 @@
     where
       env1 = record {varn = (varn  env) - 1 ; vari = (vari env) + 1}
       proof3 : varn env1 + vari env1 ≡ 10
-      proof3 = {!!}
+      proof3 = let open ≡-Reasoning  in
+          begin 
+            varn env1 + vari env1
+          ≡⟨⟩
+            (varn env - 1) + (vari env + 1)
+          ≡⟨ {!!} ⟩
+            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 = {!!}
+conversion1 env p1 next = next env proof4
+   where
+      proof4 : varn env + vari env ≡ 10
+      proof4 = let open ≡-Reasoning  in
+          begin
+            varn env + vari env
+          ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
+            10 + vari env
+          ≡⟨ cong ( λ n → 10 + n ) (pi1 p1 ) ⟩
+            10 + 0
+          ≡⟨⟩
+            10
+          ∎
 
-proofGears : whileTest' (λ n →  conversion1 n {!!} (λ n1 → whileLoop' n1 {!!}  (λ n2 → (vari n2) ≡ 10)))
-proofGears = {!!}
+
+proofGears : Set
+proofGears = whileTest' (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ 10 ))))