# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1575939072 -32400
# Node ID bf7c7bd69e358449dc0eafa0383db93223204d02
# Parent  600b4e914071a8e56f01b043a74e218a32680b11
conversion. loop needs cases

diff -r 600b4e914071 -r bf7c7bd69e35 whileTestGears.agda
--- a/whileTestGears.agda	Tue Dec 10 09:19:14 2019 +0900
+++ b/whileTestGears.agda	Tue Dec 10 09:51:12 2019 +0900
@@ -94,25 +94,12 @@
 proofGears : {c10 :  ℕ } → Set
 proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
 
--- proofGearsMeta : {c10 :  ℕ } → whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
--- proofGearsMeta {c10} = {!!}
-
 data whileTestState (c10 : ℕ ) : Set where
   error : whileTestState c10
   state1 : (env : Env)  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestState c10
   state2 : (env : Env) → (varn env + vari env ≡ c10) → whileTestState c10
   finstate : (env : Env)  → ((vari env) ≡ c10 ) → whileTestState c10
 
-whileLoopProof0 : {c10 : ℕ } → Set
-whileLoopProof0 {c10 } = Env /\ whileTestState c10 → whileLoop {!!} ( λ env → vari env ≡ c10 )  
-whileTestProof0 : {c10 : ℕ } → Set
-whileTestProof0 {c10} = Env /\ whileTestState c10 → whileTest c10 (λ env →  {!!} )
-
-proofGearsState : {c10 :  ℕ } → whileTestProof0
-proofGearsState {c10} = {!!}  where 
-  lemma1 : (env : Env ) →  vari env ≡ c10
-  lemma1 = {!!}
-
 record Context : Set where
    field 
      c10 : ℕ
@@ -148,12 +135,8 @@
 {-# TERMINATING #-}
 whileLoopProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) (Code : Context -> t) -> t
 whileLoopProof cxt next exit = whileLoopStep (whileDG cxt)
-    ( λ env → next record cxt { whileDG = env ; whileCond = nextCond env } )  
+    ( λ env → next record cxt { whileDG = env } ) 
     ( λ env → exit record cxt { whileDG = env ; whileCond = exitCond env } )   where
-        nextCond : Env → whileTestState (c10 cxt)
-        nextCond nenv with whileCond cxt
-        ... | state2 e inv = state2 (whileDG cxt) {!!}
-        ... | _ = error
         exitCond : Env → whileTestState (c10 cxt)
         exitCond nenv with whileCond cxt
         ... | state2 e inv = finstate (whileDG cxt) {!!}
@@ -161,9 +144,20 @@
 
 whileConvProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) -> t
 whileConvProof cxt next = next record cxt { whileCond = postCond } where
+    proof4 : (e : Env ) → (vari e ≡ 0) /\ (varn e ≡ c10 cxt)  → varn e + vari e ≡ c10 cxt
+    proof4 env p1 = let open ≡-Reasoning  in
+          begin
+            varn env + vari env
+          ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
+            c10 cxt + vari env
+          ≡⟨ cong ( λ n → c10 cxt + n ) (pi1 p1 ) ⟩
+            c10 cxt + 0
+          ≡⟨ +-sym {c10 cxt} {0} ⟩
+            c10 cxt 
+          ∎
     postCond : whileTestState (c10 cxt)
     postCond with whileCond cxt
-    ... | state1 e inv = state2 (whileDG cxt) {!!}
+    ... | state1 e inv = state2 e (proof4 e inv)
     ... | _ = error
 
 {-# TERMINATING #-}
@@ -174,5 +168,5 @@
     $ λ cxt → whileConvProof cxt 
     $ λ cxt → loop cxt 
     $ λ cxt → vari (whileDG cxt) ≡ c10 cxt
-proofWhileGear cxt = {!!}
+proofWhileGear c cxt = {!!}