# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1576664784 -32400
# Node ID 91d6d8097a39a8bdf2b5dac7838695392782c8a2
# Parent  cc8de8bdbf7e1a34630cec6462425acc26505716
...

diff -r cc8de8bdbf7e -r 91d6d8097a39 whileTestGears.agda
--- 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} = {!!}