### changeset 38:7049fbaf5e18

fix
author ryokka Fri, 13 Dec 2019 20:33:52 +0900 2db6120a02e6 2eb30c8e5a20 whileTestGears.agda 1 files changed, 11 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Fri Dec 13 19:54:28 2019 +0900
+++ b/whileTestGears.agda	Fri Dec 13 20:33:52 2019 +0900
@@ -116,7 +116,10 @@
whileLoopContext cxt next with lt 0 (varn (whileDG cxt) )
whileLoopContext cxt next | false = next cxt
whileLoopContext cxt next | true =
-    whileLoopContext (record cxt { whileDG = record {varn = (varn (whileDG cxt)) - 1 ; vari = (vari (whileDG cxt)) + 1} ; whileCond = {!!} } )  next
+    whileLoopContext (record cxt { whileDG = record {varn = (varn (whileDG cxt)) - 1 ; vari = (vari (whileDG cxt)) + 1} ; whileCond = state2 (proof cxt) } )  next
+      where
+        proof : (cxt : Context) → (varn (whileDG cxt) - 1) + (vari (whileDG cxt) + 1) ≡ c10 cxt
+        proof cxt = {!!}

open import Relation.Nullary
open import Relation.Binary
@@ -126,10 +129,12 @@
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 _ _  = {!!}
+whileLoopStep env next exit | tri< gt ¬eq _  = {!!}
where
lem : (env : Env) → (1 ≤ varn env) → 1 ≤ (varn env - 1)
-        lem env 1<varn = {!!}
+        lem env (s≤s 1<varn) with 1 ≤? varn env
+        lem env (s≤s 1<varn) | no ¬p = {!!}
+        lem env (s≤s 1<varn) | yes p = ⊥-elim (¬eq ({!!}))
-- n が 0 の時 は正しい、　n が1の時正しくない

whileLoopStep env next exit | tri> _ _ c  = ⊥-elim (m<n⇒n≢0 {varn env} {0} c refl) -- can't happen
@@ -179,13 +184,13 @@
{-# TERMINATING #-}
loopProof : {l : Level} {t : Set l} {P Inv : Context → Set } → (c : Context) → (if : (c : Context) → Dec (P c))
→ Inv c → (exit : (c2 : Context) → (P c2) → Inv c2  → t)
-          (f : Context → (exit : (c2 : Context) → (P c2) → Inv c2  → t) → t) → t
+          (f : Context → (exitn : (c2 : Context) → (P c2) → Inv c2  → t) → t) → t
loopProof {l} {t} {P} {Inv} cxt if inv exit f = lem cxt inv
where
lem : (c : Context) → Inv c → t
lem c inv with if c
-    lem c inv | no ¬p = f c (λ c1 inv1 inv2 → lem c1 {!!} )
-    lem c inv | yes p = exit {!!} {!!} {!!}
+    lem c inv | no ¬p = f c (λ c1 inv1 exit1 → lem c1 exit1 )
+    lem c inv | yes p = exit c p inv

@@ -194,8 +199,3 @@
\$ λ 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 = {!!}
-