### changeset 49:91d6d8097a39

...
author Shinji KONO Wed, 18 Dec 2019 19:26:24 +0900 cc8de8bdbf7e 2edb44c5bf52 whileTestGears.agda 1 files changed, 35 insertions(+), 38 deletions(-) [+]
line wrap: on
line diff
```--- a/whileTestGears.agda	Mon Dec 16 16:22:52 2019 +0900
+++ b/whileTestGears.agda	Wed Dec 18 19:26:24 2019 +0900
@@ -94,8 +94,8 @@
proofGears : {c10 :  ℕ } → Set
proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 ))))

-proofGearsMeta : {c10 :  ℕ } →  proofGears {c10}
-proofGearsMeta {c10} = {!!} -- net yet done
+-- proofGearsMeta : {c10 :  ℕ } →  proofGears {c10}
+-- proofGearsMeta {c10} = {!!} -- net yet done

--
--      openended Env c  <=>  Context
@@ -104,57 +104,54 @@
open import Relation.Nullary
open import Relation.Binary

+whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t
+whileTestP c10 next = next (record {varn = c10 ; vari = 0 } )
+
+whileLoopP : {l : Level} {t : Set l} → Env → (next : Env → t) → (exit : Env → t) → t
+whileLoopP env next exit with <-cmp 0 (varn env)
+whileLoopP env next exit | tri≈ ¬a b ¬c = exit env
+whileLoopP env next exit | tri< a ¬b ¬c =
+     next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 })
+
+{-# TERMINATING #-}
+loopP : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+loopP env exit = whileLoopP env (λ env → loopP env exit ) exit
+
+whileTestPCall : {c10 :  ℕ } → Set
+whileTestPCall {c10} = whileTestP {_} {_} c10 (λ env → loopP env (λ env →  ( vari env ≡ c10 )))
+
data whileTestStateP (c10 i n : ℕ ) : Set where
pstate1 : (i ≡ 0) /\ (n ≡ c10) → whileTestStateP c10 i n    -- n ≡ c10
-  pstate2 : (n + i ≡ c10)        → whileTestStateP c10 i n    -- 0 < n < c10
-  pfinstate : (i ≡ c10 )         → whileTestStateP c10 i n    -- n ≡ 0
+  pstate2 : (0 < n) → (n < c10) → (n + i ≡ c10)        → whileTestStateP c10 i n    -- 0 < n < c10
+  pfinstate : (n ≡ 0 ) → (i ≡ c10 )         → whileTestStateP c10 i n    -- n ≡ 0

record EnvP : Set (succ Zero) where
field
-    pvarn : ℕ
-    pvari : ℕ
-    c10 : ℕ
-    cx : whileTestStateP c10 pvarn pvari
+     env : Env
+     c10 : ℕ
+     cx :  whileTestStateP c10 (vari env) (varn env)
+
open EnvP

-whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : EnvP → t) → t
-whileTestP c10 next = next (record {pvarn = c10 ; pvari = 0 ; c10 = c10 ; cx = pstate1 record { pi1 = {!!} ; pi2 = {!!} }  } )
-
-whileLoopP : {l : Level} {t : Set l} → EnvP → (next : EnvP → t) → (exit : EnvP → t) → t
-whileLoopP env next exit with lt 0 (pvarn env)
-whileLoopP env next exit | false = exit record env { cx = {!!} }
-whileLoopP env next exit | true =
-    next (record env {pvarn = (pvarn env) - 1 ; pvari = (pvari env) + 1 ; cx = {!!} })
+whileTestPwithProof : {l : Level} {t : Set l} → (c10 : ℕ ) → (next : (e : EnvP ) → t) → t
+whileTestPwithProof {l} {t} c10 next = next record { env = env1 ; c10 = c10 ; cx = cx1 } where
+    env1 : Env
+    env1 = whileTestP c10 ( λ e → e )
+    cx1 : whileTestStateP c10 (vari env1) (varn env1)
+    cx1 = pstate1 record { pi1 = refl ; pi2 = refl }

{-# TERMINATING #-}
-loopP : {l : Level} {t : Set l} → EnvP → (exit : EnvP → t) → t
-loopP env exit = whileLoopP env (λ env → loopP env exit ) exit
-
-whileTestPCall : {c10 :  ℕ } → Set
-whileTestPCall {c10} = whileTestP {_} {_} c10 (λ env → loopP env (λ env →  ( pvari env ≡ c10 )))
-
-whileTestPwithProof : {l : Level} {t : Set l} → (c10 : ℕ ) → (next : (e : EnvP ) → cx e ≡ pstate1 {!!} → t) → t
-whileTestPwithProof {l} {t} c10 next = next env lemma where
-    env : EnvP
-    env = record { pvarn = {!!} ; pvari = {!!} ; c10 = {!!} ; cx = {!!} }
-    lemma : cx env ≡ pstate1 {!!}
+loopPwithProof : {l : Level} {t : Set l} → (e : EnvP ) → (exit : (e : EnvP ) → t ) → t
+loopPwithProof e exit = whileLoopP (env e) (λ e1 → loopPwithProof record e { env = e1 ; cx = {!!} } exit ) (λ env → exit {!!} ) where
+    lemma :  {!!}
lemma = {!!}

-{-# TERMINATING #-}
-loopPwithProof : {l : Level} {t : Set l} → (e : EnvP ) → (exit : (e : EnvP ) →  cx e ≡ pstate2 {!!} → t) →  cx e ≡ pstate2 {!!} → t
-loopPwithProof env exit eq = whileLoopP env (λ env → loopPwithProof env exit {!!} ) (λ env → exit env {!!} ) where
-    lemma :  cx {!!} ≡ pstate2 {!!}
-    lemma = {!!}
-
-ConvP : (e : EnvP) → cx e ≡ pstate1 {!!} →  cx e ≡ pstate2 {!!}
+ConvP : (e : EnvP) → EnvP
ConvP = {!!}

-finalProof : {l : Level} {t : Set l} → (e : EnvP ) →  cx e ≡ pstate2 {!!} →  pvari e ≡ c10 e
-finalProof env exit = {!!}
-
whileTestPProof : {c :  ℕ } → Set
whileTestPProof {c} = whileTestPwithProof  c
-    \$ λ env eq → loopPwithProof env (λ env eq → {!!} ) (ConvP env eq )
+    \$ λ e → loopPwithProof e (λ e eq → vari (env e) ≡ c10 e ) (ConvP e )

whileTestPProofMeta : {c10 :  ℕ } →  whileTestPProof {c10}
whileTestPProofMeta {c10} = {!!}```