# HG changeset patch
# User ryokka
# Date 1576232595 -32400
# Node ID 7c739972cd262114aa3d55b50fefa764ce0688fb
# Parent  9caff4e4a402e704ecf533bce337588edd8c6a76
add loopProof

diff -r 9caff4e4a402 -r 7c739972cd26 whileTestGears.agda
--- a/whileTestGears.agda	Thu Dec 12 18:26:39 2019 +0900
+++ b/whileTestGears.agda	Fri Dec 13 19:23:15 2019 +0900
@@ -123,16 +123,14 @@
 
 
 {-# TERMINATING #-}
-whileLoopStep : {l : Level} {t : Set l} → Env → (Code : (e : Env ) → 0 < varn e → t) (Code : (e : Env) → 0 ≡ varn e  → t) → t
+whileLoopStep : {l : Level} {t : Set l} → Env → (Code : (e : Env ) → 1 ≤ varn e → t) (Code : (e : Env) → 0 ≡ varn e  → t) → t
 whileLoopStep env next exit with <-cmp 0 (varn env)
 whileLoopStep env next exit | tri≈ _ eq _ = exit env eq
-whileLoopStep env next exit | tri< gt _ _  =
-    next (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) (lem env gt)
+whileLoopStep env next exit | tri< gt _ _  = {!!}
       where
         lem : (env : Env) → (1 ≤ varn env) → 1 ≤ (varn env - 1)
-        lem record { varn = (suc na) ; vari = vari } (s≤s gt) with na ≟ 0
-        lem record { varn = (suc na) ; vari = vari } (s≤s gt) | does₁ because proof₁ = {!!}
-        -- n が 0 の時正しくない
+        lem env 1<varn = {!!}
+        -- n が 0 の時 は正しい、　n が1の時正しくない
 
 whileLoopStep env next exit | tri> _ _ c  = ⊥-elim (m<n⇒n≢0 {varn env} {0} c refl) -- can't happen
 
@@ -177,9 +175,23 @@
 loop : {l : Level} {t : Set l} → Context → (exit : Context → t) → t
 loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit ) exit
 
+
+
+loopProof : {l : Level} {t : Set l} {P Pre Post Inv : Context → Set } → (c : Context) → (d : Dec (P c))
+          → Pre c → (Context → (continue : (c1 : Context) → ¬ (P c1) → Inv c1 → t)
+          → (exit : (c2 : Context) → (P c2) → Post c2  → t) → t)  → t
+loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt (false because proof₁) f =
+          loopProof {!!} {!!} {!!}
+loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt (true because proof₁) f = {!!}
+
+
 proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error })
     $ λ cxt → whileConvProof cxt 
     $ λ cxt → loop cxt 
     $ λ cxt → vari (whileDG cxt) ≡ c10 cxt
 proofWhileGear c cxt = {!!}
 
+
+CodeGear : {l : Level} {t : Set l} → (cont : Set → t) → (exit : Set → t) → t
+CodeGear = {!!}
+