# HG changeset patch
# User ryokka
# Date 1576910850 -32400
# Node ID 34601fe34b713d3c2861c9f43ab4a4d98eaeec31
# Parent  1be7bb658cf0eafb2594bb52238dda150f0d2698
fix

diff -r 1be7bb658cf0 -r 34601fe34b71 whileTestGears.agda
--- a/whileTestGears.agda	Fri Dec 20 17:45:56 2019 +0900
+++ b/whileTestGears.agda	Sat Dec 21 15:47:30 2019 +0900
@@ -143,7 +143,7 @@
    env : Envc
    env = whileTestP c10 ( λ env → env )
 
-whileLoopPwP : {l : Level} {t : Set l}   → (env : Envc ) → whileTestStateP s2 env 
+whileLoopPwP : {l : Level} {t : Set l}   → (env : Envc ) → whileTestStateP s2 env
     → (next : (env : Envc ) → whileTestStateP s2 env  → t)
     → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
 whileLoopPwP env s next exit with <-cmp 0 (varn env)
@@ -152,8 +152,27 @@
     lem : (varn env ≡ 0) → (varn env + vari env ≡ c10 env) → vari env ≡ c10 env
     lem p1 p2 rewrite p1 = p2
 
-whileLoopPwP env s next exit | tri< a ¬b ¬c =
-     next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) {!!}
+whileLoopPwP env s next exit | tri< a ¬b ¬c  = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a)
+  where
+    1<0 : 1 ≤ zero → ⊥
+    1<0 ()
+    proof5 : (suc zero  ≤ (varn  env))  → (varn env - 1) + (vari env + 1) ≡ c10 env
+    proof5 (s≤s lt) with varn  env
+    proof5 (s≤s z≤n) | zero = ⊥-elim (1<0 a)
+    proof5 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in
+      begin
+        n' + (vari env + 1)
+      ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
+        n' + (1 + vari env )
+      ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
+        (n' + 1) + vari env
+      ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
+        (suc n' ) + vari env
+      ≡⟨⟩
+        varn env + vari env
+      ≡⟨ s  ⟩
+         c10 env
+      ∎
 
 {-# TERMINATING #-}
 loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
@@ -165,11 +184,11 @@
     conv e record { pi1 = refl ; pi2 = refl } = +zero
 
 Proof : (c :  ℕ ) → whileTestPCallwP c
-Proof c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → {!!} ) ) where
+Proof zero = whileTestPwP {_} {_} zero (λ env s → loopPwP env (conv env s) (λ env s → refl))
+  where
     conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
     conv e record { pi1 = refl ; pi2 = refl } = +zero
-
-
-
-
-
+Proof (suc c) = whileTestPwP {_} {_} zero (λ env s → loopPwP env (conv env s) (λ env s → {!!})) -- Proof c したいが with <-cmp 0 c とか with 0 ≤ c とかするとAgda の check が終わらない
+  where
+    conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
+    conv e record { pi1 = refl ; pi2 = refl } = +zero