# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1576418228 -32400
# Node ID 8bf82026e4fe071252a05963fa7ff2825b1182f3
# Parent  52523a6ee221e328a849f25be70940baff9a6f7d
simplified env with state condition

diff -r 52523a6ee221 -r 8bf82026e4fe whileTestGears.agda
--- a/whileTestGears.agda	Sun Dec 15 19:22:21 2019 +0900
+++ b/whileTestGears.agda	Sun Dec 15 22:57:08 2019 +0900
@@ -14,11 +14,10 @@
   field
     varn : ℕ
     vari : ℕ
-    cx : Set
 open Env 
 
-whileTest : {l : Level} {t : Set l} (c : Set ) → (c10 : ℕ) → (Code : Env → t) → t
-whileTest c c10 next = next (record {varn = c10 ; vari = 0 ; cx = c} )
+whileTest : {l : Level} {t : Set l}  → (c10 : ℕ) → (Code : Env → t) → t
+whileTest c10 next = next (record {varn = c10 ; vari = 0 } )
 
 {-# TERMINATING #-}
 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
@@ -27,19 +26,19 @@
 whileLoop env next | true =
     whileLoop (record env {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
 
-test1 : (c : Set ) → Env 
-test1 c = whileTest c 10 (λ env → whileLoop env (λ env1 → env1 ))
+test1 : Env 
+test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 ))
 
 
-proof1 : (c : Set ) → whileTest c 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
-proof1 c = refl
+proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
+proof1 = refl
 
 --                                                                              ↓PostCondition
-whileTest' : {l : Level} {t : Set l}  →  {c : Set} → {c10 :  ℕ } → (Code : (env : Env )  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
-whileTest' {_} {_} {c} {c10} next = next env proof2
+whileTest' : {l : Level} {t : Set l}  →  {c10 :  ℕ } → (Code : (env : Env )  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
+whileTest' {_} {_}  {c10} next = next env proof2
   where
     env : Env 
-    env = record {vari = 0 ; varn = c10 ; cx = c }
+    env = record {vari = 0 ; varn = c10 }
     proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition
     proof2 = record {pi1 = refl ; pi2 = refl}
 
@@ -75,7 +74,7 @@
       --        c10
       --     ∎
 
--- Condition to Invaliant
+-- Condition to Invariant
 conversion1 : {l : Level} {t : Set l } → (env : Env ) → {c10 :  ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
                → (Code : (env1 : Env ) → (varn env1 + vari env1 ≡ c10) → t) → t
 conversion1 env {c10} p1 next = next env proof4
@@ -93,146 +92,62 @@
           ∎
 
 
-proofGears : {c10 :  ℕ } → Set → Set
-proofGears {c10} c = whileTest' {_} {_} {c} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
+proofGears : {c10 :  ℕ } → Set
+proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
 
-data whileTestState (c10 : ℕ ) (env : Env ) : Set where
---   error : whileTestState c10 env
-  state1 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestState c10 env
-  state2 : (varn env + vari env ≡ c10) → whileTestState c10 env
-  finstate : ((vari env) ≡ c10 ) → whileTestState c10 env
-
-transition : (c10 : ℕ ) (env0 : Env) → (Env → Env) → Set
-transition c10 env0 prog  = whileTestState c10 env0 → whileTestState c10 (prog env0)
-
-whileTrans : (c10 : ℕ ) (env0 : Env) → transition c10 env0 {!!}
-whileTrans c10 env0 st = {!!}
+proofGearsMeta : {c10 :  ℕ } →  proofGears {c10}
+proofGearsMeta {c10} = {!!} -- net yet done
 
 --
 --      openended Env c  <=>  Context
 --
 
-record Context : Set (succ Zero) where
-   field 
-     c10 : ℕ
-     whileDG : Env
-     whileCond : whileTestState c10 whileDG
-
-open Context
-
-
-
-
 open import Relation.Nullary
 open import Relation.Binary
 
---
--- transparency of condition
---
-
-whileCondP : Env → Set
-whileCondP env = (varn env > 0) /\  (vari 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 = {!!} } )
+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
 
-{-# TERMINATING #-}
-whileLoopContext : {l : Level} {t : Set l} → Context → (Code : Context → t) → t
-whileLoopContext cxt next with lt 0 (varn (whileDG cxt) )
-whileLoopContext cxt next | false = next cxt
-whileLoopContext cxt next | true =
-    whileLoopContext (record cxt { whileDG = record (whileDG cxt) {varn = (varn (whileDG cxt)) - 1 ; vari = (vari (whileDG cxt)) + 1} ; whileCond = state2 (proof3 cxt) } )  next
-      where
-        proof3 : (cxt : Context) → (varn (whileDG cxt) - 1) + (vari (whileDG cxt) + 1) ≡ c10 cxt
-        proof3 cxt = {!!} 
+record EnvP : Set (succ Zero) where
+  field
+    pvarn : ℕ
+    pvari : ℕ
+    c10 : ℕ
+    cx : whileTestStateP c10 pvarn pvari
+open EnvP
 
-{-# TERMINATING #-}
-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 
-whileLoopStep env next exit | tri< gt ¬eq _  = next record env {varn = (varn env) - 1 ; vari = (vari env) + 1} 
-whileLoopStep env next exit | tri> _ _ c  = ⊥-elim (m<n⇒n≢0 {varn env} {0} c refl) 
+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 = {!!} }  } )
 
-whileTestProof : {l : Level} {t : Set l} → Context → (Code : (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt) ) → t) → t
-whileTestProof cxt next = next record cxt { whileDG = out ; whileCond = init } i!=n where
-    out : Env 
-    out =  whileTest {!!} (c10 cxt) ( λ e → e ) 
-    init : whileTestState (c10 cxt) out
-    init = state1 record { pi1 = refl ; pi2 = refl }
-    i!=n : ¬ vari out ≡ varn out
-    i!=n eq = {!!}
+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 = {!!} }) 
 
 {-# TERMINATING #-}
-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 → next record cxt { whileDG = env ; whileCond = (state2 (proof4 env {!!})) } {!!} ) 
-    ( λ 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
-        proof4 : (e : Env ) → (vari e ≡ 0) /\ (varn e ≡ c10 cxt)  → varn e + vari e ≡ c10 cxt
-        proof4 e p1 = let open ≡-Reasoning  in
-          begin
-            varn e + vari e
-          ≡⟨ cong ( λ n → n + vari e ) (pi2 p1 ) ⟩
-            (c10 cxt) + vari e
-          ≡⟨ cong ( λ n → (c10 cxt) + n ) (pi1 p1 ) ⟩
-            (c10 cxt) + 0
-          ≡⟨ +-sym {c10 cxt} {0} ⟩
-            c10 cxt
-          ∎
-        
-        exitCond : (e : Env ) → 0 ≡ varn e → whileTestState (c10 cxt) e
-        exitCond nenv eq1 with whileCond cxt | inspect whileDG cxt
-        ... | state2 cond | record { eq = eq2 } = finstate ( proof5 nenv {!!} eq1 )
-        ... | _ | _ = {!!} -- error
+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 )))
+
+wTlemma1 : {l : Level} {t : Set l} → (e : EnvP ) → 0 < pvarn e  → cx e ≡ pstate1 {!!}  → (exit : EnvP → t) → t
+wTlemma1 e lt prev exit = exit record e { cx = pstate2 {!!} }
 
-whileConvProof : {l : Level} {t : Set l} → (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt))
-    → ((cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt)) → t) → t
-whileConvProof cxt i!=n next = next record cxt { whileCond = postCond } i!=n where
-    proof4 : (e : Env ) → (vari e ≡ 0) /\ (varn e ≡ c10 cxt)  → varn e + vari e ≡ c10 cxt
-    proof4 env p1 = let open ≡-Reasoning  in
-          begin
-            varn env + vari env
-          ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
-            c10 cxt + vari env
-          ≡⟨ cong ( λ n → c10 cxt + n ) (pi1 p1 ) ⟩
-            c10 cxt + 0
-          ≡⟨ +-sym {c10 cxt} {0} ⟩
-            c10 cxt 
-          ∎
-    postCond : whileTestState (c10 cxt) (whileDG cxt)
-    postCond with whileCond cxt
-    ... | state1 cond = state2 (proof4 (whileDG cxt) cond )
-    ... | _ = {!!} -- error
+wTlemma2 : {l : Level} {t : Set l} → (e : EnvP ) → 0 ≡ pvarn e  →  cx e ≡ pstate2 {!!} → (exit : EnvP → t) → t
+wTlemma2 e eq prev exit = exit record e { cx = pfinstate {!!} }
 
-{-# 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 ) {!!}
+whileTestPProof : {c10 :  ℕ } → Set
+whileTestPProof {c10} = whileTestP {_} {_} c10 
+    $ λ env → wTlemma1 env {!!} {!!}
+    $ λ env → loopP env 
+    $ λ env → wTlemma2 env {!!} {!!} 
+    $ λ env →  ( pvari env ≡ c10 )
+
+whileTestPProofMeta : {c10 :  ℕ } →  whileTestPProof {c10}
+whileTestPProofMeta {c10} = {!!} 
 
 
-
-{-# TERMINATING #-}
-loopProof : {l : Level} {t : Set l} {P Inv : Context → Set } → (c : Context) → (if : (c : Context) → Dec (P c))
-          → ( (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) → 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 i!=n
-    $ λ cxt i+n=c10 → loopProof cxt whileDec {!!} -- whileLoopProof'
-    $ λ cxt _ → {!!} 
-proofWhileGear c cxt = {!!}