### changeset 41:107cd3825e61

...
author Shinji KONO Sun, 15 Dec 2019 10:18:26 +0900 a9cac7960e81 8813f26da3b7 whileTestGears.agda 1 files changed, 42 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
```--- a/whileTestGears.agda	Sat Dec 14 21:27:49 2019 +0900
+++ b/whileTestGears.agda	Sun Dec 15 10:18:26 2019 +0900
@@ -100,6 +100,10 @@
state2 : (varn env + vari env ≡ c10) → whileTestState c10 env
finstate : ((vari env) ≡ c10 ) → whileTestState c10 env

+--
+--      openended Env  <=>  Context
+--
+
record Context : Set where
field
c10 : ℕ
@@ -108,6 +112,19 @@

open Context

+open import Relation.Nullary
+open import Relation.Binary
+
+--
+-- transparency of condition
+--
+
+whileCondP : Env → Set
+whileCondP env = varn env > 0
+
+whileDec : (cxt : Context) → Dec (whileCondP (whileDG cxt))
+whileDec cxt = {!!}
+
whileTestContext : {l : Level} {t : Set l} → Context → (Code : Context → t) → t
whileTestContext cxt next = next (record cxt { whileDG = record (whileDG cxt) {varn = c10 cxt ; vari = 0} ; whileCond = {!!} } )

@@ -121,15 +138,11 @@
proof : (cxt : Context) → (varn (whileDG cxt) - 1) + (vari (whileDG cxt) + 1) ≡ c10 cxt
proof cxt = {!!}

-open import Relation.Nullary
-open import Relation.Binary
-
-
{-# TERMINATING #-}
-whileLoopStep : {l : Level} {t : Set l} → Env → (next : (e : Env ) → 1 ≤ varn e → t) (exit : (e : Env) → 0 ≡ varn e  → t) → t
+whileLoopStep : {l : Level} {t : Set l} → Env → (next : (e : Env ) → t) (exit : (e : Env) → 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 ¬eq _  = next env gt
+whileLoopStep env next exit | tri≈ _ eq _ = exit env
+whileLoopStep env next exit | tri< gt ¬eq _  = next record {varn = (varn env) - 1 ; vari = (vari env) + 1}
whileLoopStep env next exit | tri> _ _ c  = ⊥-elim (m<n⇒n≢0 {varn env} {0} c refl)

whileTestProof : {l : Level} {t : Set l} → Context → (Code : (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt) ) → t) → t
@@ -142,11 +155,11 @@
i!=n eq = {!!}

{-# TERMINATING #-}
-whileLoopProof : {l : Level} {t : Set l} → (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt) )
-    → (continue : (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt) )  → t) (exit : Context → (vari (whileDG cxt) ≡ varn (whileDG cxt) )  → t) → t
+whileLoopProof : {l : Level} {t : Set l} → (cxt : Context ) → whileCondP (whileDG cxt)
+    → (continue : (cxt : Context ) → whileCondP (whileDG cxt)  → t) (exit : Context → ¬ whileCondP (whileDG cxt)  → t) → t
whileLoopProof cxt i!=n next exit = whileLoopStep (whileDG cxt)
-    ( λ env lt → next record cxt { whileDG = env ; whileCond = {!!} } {!!} )
-    ( λ env eq → exit record cxt { whileDG = env ; whileCond = exitCond env eq } {!!} )   where
+    ( λ env → next record cxt { whileDG = env ; whileCond = {!!} } {!!} )
+    ( λ env → exit record cxt { whileDG = env ; whileCond = exitCond env {!!} } {!!} )   where
proof5 : (e : Env ) → varn e + vari e ≡ c10 cxt →  0 ≡ varn e → vari e ≡ c10 cxt
proof5 record { varn = .0 ; vari = vari } refl refl = refl
exitCond : (e : Env ) → 0 ≡ varn e → whileTestState (c10 cxt) e
@@ -173,27 +186,29 @@
... | state1 cond = state2 (proof4 (whileDG cxt) cond )
... | _ = error

--- {-# TERMINATING #-}
--- loop : {l : Level} {t : Set l} → (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt) )
---    → (exit : (cxt : Context ) → (vari (whileDG cxt) ≡ varn (whileDG cxt) )  → t) → t
--- loop cxt i!=n exit = whileLoopProof cxt i!=n (λ cxt → loop cxt {!!} {!!} exit ) {!!}
+{-# TERMINATING #-}
+loop : {l : Level} {t : Set l} → (cxt : Context ) → whileCondP (whileDG cxt)
+    → (exit : (cxt : Context ) → ¬ whileCondP (whileDG cxt)  → t) → t
+loop cxt i!=n exit = whileLoopProof cxt i!=n (λ cxt → loop cxt {!!} {!!} exit ) {!!}

{-# 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 → (exitn : (c2 : Context) → (P c2) → Inv c2  → t) → t) → t
-loopProof {l} {t} {P} {Inv} cxt if inv exit f = lem cxt inv
+          → ( (cont : (c2 : Context) → (P c2) → t) → (exit : (c2 : Context) → ¬ (P c2) → t) → t )
+          → t
+loopProof {l} {t} {P} {Inv} cxt if f = {!!}
where
-    lem : (c : Context) → Inv c → t
-    lem c inv with if c
-    lem c inv | no ¬p = f c (λ c1 inv1 exit1 → lem c1 exit1 )
-    lem c inv | yes p = exit c p inv
+    lem : (c : Context) → t
+    lem c with if c
+    lem c | no ¬p = {!!} -- f c (λ c1 _ → lem c1 )
+    lem c | yes p = {!!}

+whileLoopProof' : {l : Level} {t : Set l} → (cxt : Context )
+    → (continue : (cxt : Context ) → whileCondP (whileDG cxt)  → t) (exit : Context → ¬ whileCondP (whileDG cxt)  → t) → t
+whileLoopProof' = ?

-
-proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error }) {!!}
-    \$ λ cxt i!=n → whileConvProof cxt {!!}
-    \$ λ cxt i+n=c10 → loopProof cxt {!!} {!!} ( whileLoopStep (whileDG cxt) {!!} {!!} )
-    \$ λ cxt _ → vari (whileDG cxt) ≡ c10 cxt
+proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error })
+    \$ λ cxt i!=n → whileConvProof cxt i!=n
+    \$ λ cxt i+n=c10 → loopProof cxt whileDec ?
+    \$ λ cxt _ → ?
proofWhileGear c cxt = {!!}```