# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1635728383 -32400
# Node ID a7263ecf8671c3db0af0d201d5488949ca634aff
# Parent  9c91d23c2836546c89374c1bee75c497de7b34d9
fix

diff -r 9c91d23c2836 -r a7263ecf8671 whileTestGears.agda
--- a/whileTestGears.agda	Mon Nov 01 08:34:07 2021 +0900
+++ b/whileTestGears.agda	Mon Nov 01 09:59:43 2021 +0900
@@ -1,298 +1,188 @@
 module whileTestGears where
 
 open import Function
-open import Data.Nat
-open import Data.Bool hiding ( _≟_ ; _≤?_ ; _≤_ ; _<_)
-open import Data.Product
+open import Data.Nat renaming ( _∸_ to _-_)
+open import Data.Bool hiding ( _≟_ ;  _≤?_ ; _≤_ ; _<_ )
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Binary.PropositionalEquality
-open import Agda.Builtin.Unit
 
 open import utilities
 open  _/\_
 
--- original codeGear (with non terminatinng )
-
-record Env : Set (succ Zero) where
+record Env  : Set where
   field
     varn : ℕ
     vari : ℕ
 open Env
 
-whileTest : {l : Level} {t : Set l}  → (c10 : ℕ) → (Code : Env → t) → t
-whileTest c10 next = next (record {varn = c10 ; vari = 0 } )
+whileTestS : { m : Level}  → (c10 : ℕ) → (Code : Env → Set m) → Set m
+whileTestS c10 next = next (record {varn = c10 ; vari = 0} )
+
+whileTestS1 :  (c10 : ℕ) →  whileTestS c10 (λ e → ((varn e ≡ c10) /\ (vari e ≡ 0 )) )
+whileTestS1 c10 = record { pi1 = refl ; pi2 = refl }
+
+
+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
 whileLoop env next with lt 0 (varn env)
 whileLoop env next | false = next env
 whileLoop env next | true =
-    whileLoop (record env {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
+    whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
 
 test1 : Env
 test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 ))
 
+
 proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
 proof1 = refl
 
--- codeGear with pre-condtion and post-condition
---
 --                                                                              ↓PostCondition
-whileTest' : {l : Level} {t : Set l}  →  {c10 :  ℕ } → (Code : (env : Env )  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
-whileTest' {_} {_}  {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 }
+    env = record {vari = 0 ; varn = c10}
     proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition
     proof2 = record {pi1 = refl ; pi2 = refl}
 
 open import Data.Empty
 open import Data.Nat.Properties
 
+lemma1 : {i : ℕ} →  ¬ 1 ≤ i → i ≡ 0
+lemma1 {zero} not = refl
+lemma1 {suc i} not = ⊥-elim ( not (s≤s z≤n) )
 
 {-# TERMINATING #-} --                                                  ↓PreCondition(Invaliant)
-whileLoop' : {l : Level} {t : Set l} → (env : Env ) → {c10 :  ℕ } → ((varn env) + (vari env) ≡ c10) → (Code : Env  → t) → t
+whileLoop' : {l : Level} {t : Set l} → (env : Env) → {c10 :  ℕ } → ((varn env) + (vari env) ≡ c10)
+   → (Code : (e1 : Env )→ vari e1 ≡ c10 → t) → t
 whileLoop' env proof next with  ( suc zero  ≤? (varn  env) )
-whileLoop' env proof next | no p = next env
-whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next
-    where
-      env1 = record env {varn = (varn  env) - 1 ; vari = (vari env) + 1}
+whileLoop' env {c10} proof next | no p = next env ( begin
+       vari env            ≡⟨ refl ⟩
+       0 + vari env        ≡⟨ cong (λ k → k + vari env) (sym (lemma1 p )) ⟩
+       varn env + vari env ≡⟨ proof ⟩
+       c10 ∎ ) where open ≡-Reasoning  
+whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next where
+      env1 = record {varn = (varn  env) - 1 ; vari = (vari env) + 1}
       1<0 : 1 ≤ zero → ⊥
       1<0 ()
       proof3 : (suc zero  ≤ (varn  env))  → varn env1 + vari env1 ≡ c10
       proof3 (s≤s lt) with varn  env
       proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p)
-      proof3 (s≤s (z≤n {n'}) ) | suc n =  let open ≡-Reasoning  in
-          begin
-             n' + (vari env + 1)
-          ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
-             n' + (1 + vari env )
-          ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
-             (n' + 1) + vari env
-          ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
-             (suc n' ) + vari env
-          ≡⟨⟩
-             varn env + vari env
-          ≡⟨ proof  ⟩
+      proof3 (s≤s (z≤n {n'}) ) | suc n =  let open ≡-Reasoning  in begin
+             n' + (vari env + 1)  ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
+             n' + (1 + vari env ) ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
+             (n' + 1) + vari env  ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
+             (suc n' ) + vari env ≡⟨⟩
+             varn env + vari env  ≡⟨ proof  ⟩
              c10
           ∎
 
--- 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
-   where
+-- Condition to Invaliant
+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 where
       proof4 : varn env + vari env ≡ c10
-      proof4 = let open ≡-Reasoning  in
-          begin
-            varn env + vari env
-          ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
-            c10 + vari env
-          ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩
-            c10 + 0
-          ≡⟨ +-sym {c10} {0} ⟩
+      proof4 = let open ≡-Reasoning  in begin
+            varn env + vari env ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
+            c10 + vari env      ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩
+            c10 + 0             ≡⟨ +-sym {c10} {0} ⟩
             c10
           ∎
 
--- all proofs are connected
-proofGears : {c10 :  ℕ } → Set
-proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 ))))
-
--- but we cannot prove the soundness of the last condition
---
--- proofGearsMeta : {c10 :  ℕ } →  proofGears {c10}
--- proofGearsMeta {c10} = {!!} -- net yet done
+open import Data.Unit hiding ( _≟_ ;  _≤?_ ; _≤_)
 
---
--- codeGear with loop step and closed environment
---
-
-open import Relation.Binary
+whileTestSpec1 : (c10 : ℕ) →  (e1 : Env ) → vari e1 ≡ c10 → ⊤
+whileTestSpec1 _ _ x = tt
 
-record Envc : Set (succ Zero) where
-  field
-    c10 : ℕ
-    varn : ℕ
-    vari : ℕ
-open Envc
+proofGears : {c10 :  ℕ } → ⊤
+proofGears {c10} = whileTest' {_} {_}  {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 p3 → whileTestSpec1 c10 n2 p3 ))) 
 
-whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Envc → t) → t
-whileTestP c10 next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )
-
-whileLoopP : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → 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 })
+--                                                                      ↓PreCondition(Invaliant)
+whileLoopSeg : {l : Level} {t : Set l} → {c10 :  ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10)
+   → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) 
+   → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t
+whileLoopSeg env proof next exit with  ( suc zero  ≤? (varn  env) )
+whileLoopSeg {_} {_} {c10} env proof next exit | no p = exit env ( begin
+       vari env            ≡⟨ refl ⟩
+       0 + vari env        ≡⟨ cong (λ k → k + vari env) (sym (lemma1 p )) ⟩
+       varn env + vari env ≡⟨ proof ⟩
+       c10 ∎ ) where open ≡-Reasoning  
+whileLoopSeg {_} {_} {c10} env proof next exit | yes p = next env1 (proof3 p ) (proof4 (varn env) p) where
+      env1 = record {varn = (varn  env) - 1 ; vari = (vari env) + 1}
+      1<0 : 1 ≤ zero → ⊥
+      1<0 ()
+      proof4 : (i : ℕ) → 1 ≤ i  → i - 1 < i
+      proof4 zero ()
+      proof4 (suc i) lt = begin
+          suc (suc i - 1 ) ≤⟨ ≤-refl ⟩
+          suc i ∎ where open ≤-Reasoning 
+      proof3 : (suc zero  ≤ (varn  env))  → varn env1 + vari env1 ≡ c10
+      proof3 (s≤s lt) with varn  env
+      proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p)
+      proof3 (s≤s (z≤n {n'}) ) | suc n =  let open ≡-Reasoning  in begin
+             n' + (vari env + 1)  ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
+             n' + (1 + vari env ) ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
+             (n' + 1) + vari env  ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
+             (suc n' ) + vari env ≡⟨⟩
+             varn env + vari env  ≡⟨ proof  ⟩
+             c10
+          ∎
 
--- equivalent of whileLoopP but it looks like an induction on varn
-whileLoopP' : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → t) → t
-whileLoopP' env@record { c10 = c10 ; varn = zero ; vari = vari } _ exit = exit env
-whileLoopP' record { c10 = c10 ; varn = suc varn1 ; vari = vari } next _ = next (record {c10 = c10 ; varn = varn1 ; vari = suc vari })
-
--- normal loop without termination
-{-# TERMINATING #-}
-loopP : {l : Level} {t : Set l} → Envc → (exit : Envc → t) → t
-loopP env exit = whileLoopP env (λ env → loopP env exit ) exit
-
-whileTestPCall : (c10 :  ℕ ) → Envc
-whileTestPCall c10 = whileTestP {_} {_} c10 (λ env → loopP env (λ env →  env))
+open import Relation.Binary.Definitions
 
---
--- codeGears with states of condition
---
-data whileTestState  : Set where
-  s1 : whileTestState
-  s2 : whileTestState
-  sf : whileTestState
+nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
+nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
+lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥
+lemma3 refl ()
+lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
+lemma5 (s≤s z≤n) ()
 
-whileTestStateP : whileTestState → Envc →  Set
-whileTestStateP s1 env = (vari env ≡ 0) /\ (varn env ≡ c10 env)
-whileTestStateP s2 env = (varn env + vari env ≡ c10 env)
-whileTestStateP sf env = (vari env ≡ c10 env)
-
-whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t
-whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
-   env : Envc
-   env = whileTestP c10 ( λ env → env )
+TerminatingLoop : {l : Level} {t : Set l} {c10 :  ℕ } → (i : ℕ) → (env : Env) → i ≡ varn env
+   →  varn env + vari env ≡ c10 
+   →  (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t
+TerminatingLoop {_} {t} {c10} i env refl p exit with <-cmp 0 i
+... | tri≈ ¬a b ¬c = whileLoopSeg {_} {t} {c10} env p (λ e1 eq lt → ⊥-elim (lemma3 b lt) ) exit 
+... | tri< a ¬b ¬c = whileLoopSeg {_} {t} {c10} env p (λ e1 p1 lt1 → TerminatingLoop1 i env e1 (≤-step lt1) p1 lt1 ) exit where --  varn e1 < suc (varn env)
+    TerminatingLoop1 : (j : ℕ) → (env e1 : Env) → varn e1 < suc j  → varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t
+    TerminatingLoop1 zero env e1 n≤j eq lt = whileLoopSeg {_} {t} {c10} e1 eq (λ e2 eq lt1 → ⊥-elim (lemma5 n≤j lt1)) exit  
+    TerminatingLoop1 (suc j) env e1 n≤j eq lt with <-cmp (varn e1) (suc j)
+    ... | tri< a ¬b ¬c = TerminatingLoop1 j env e1 a eq lt 
+    ... | tri≈ ¬a refl ¬c = whileLoopSeg {_} {t} {c10} e1 eq lemma4 exit where
+       lemma4 : (e2 : Env) → varn e2 + vari e2 ≡ c10 → varn e2 < varn e1 → t
+       lemma4 e2 eq lt1 = TerminatingLoop1 j e1 e2 lt1 eq lt1 
+    ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )   
 
-whileLoopPwP : {l : Level} {t : Set l}   → (env : Envc ) → whileTestStateP s2 env
-    → (next : (env : Envc ) → whileTestStateP s2 env  → t)
-    → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
-whileLoopPwP env s next exit with <-cmp 0 (varn env)
-whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env (lem (sym b) s)
-  where
-    lem : (varn env ≡ 0) → (varn env + vari env ≡ c10 env) → vari env ≡ c10 env
-    lem refl refl = refl
-whileLoopPwP env s next exit | tri< a ¬b ¬c  = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a)
-  where
-    1<0 : 1 ≤ zero → ⊥
-    1<0 ()
-    proof5 : (suc zero  ≤ (varn  env))  → (varn env - 1) + (vari env + 1) ≡ c10 env
-    proof5 (s≤s lt) with varn  env
-    proof5 (s≤s z≤n) | zero = ⊥-elim (1<0 a)
-    proof5 (s≤s (z≤n {n'}) ) | suc n = let open ≡-Reasoning in
-      begin
-        n' + (vari env + 1)
-      ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
-        n' + (1 + vari env )
-      ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
-        (n' + 1) + vari env
-      ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
-        (suc n' ) + vari env
-      ≡⟨⟩
-        varn env + vari env
-      ≡⟨ s  ⟩
-         c10 env
-      ∎
+proofGearsTerm : {c10 :  ℕ } → ⊤
+proofGearsTerm {c10} = whileTest' {_} {_}  {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → TerminatingLoop (varn n1) n1 refl p2 (λ n2 p3 → whileTestSpec1 c10 n2 p3 ))) 
 
+TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → (Invraiant : Index → Set ) → (ExitCond : Index → Set) → ( reduce : Index → ℕ)
+   → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)  → Invraiant r1 → reduce r1 < reduce r  → t ) → (exit : (re : Index) → ExitCond re → t) → t)
+   → (r : Index) → (p : Invraiant r)  → (exit : (re : Index) → ExitCond re → t)  → t 
+TerminatingLoopS {_} {t} Index Invraiant ExitCond reduce loop  r p exit with <-cmp 0 (reduce r)
+... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) exit 
+... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) exit where 
+    TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j  → Invraiant r1 →  reduce r1 < reduce r → t
+    TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) exit  
+    TerminatingLoop1 (suc j) r r1  n≤j p1 lt with <-cmp (reduce r1) (suc j)
+    ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt 
+    ... | tri≈ ¬a b ¬c = loop r1 p1 lemma4 exit where
+       lemma4 : (r2 : Index) → Invraiant r2 → reduce r2 < reduce r1  → t
+       lemma4 r2 p2 lt1 = TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1  
+    ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )   
 
-whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env
-  → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env  → t)
-  → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
-whileLoopPwP' zero env refl refl next exit = exit env refl
-whileLoopPwP' (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env))
+proofGearsTermS : {c10 :  ℕ } → ⊤
+proofGearsTermS {c10} = whileTest' {_} {_}  {c10} (λ n p →  conversion1 n p (λ n1 p1 →
+    TerminatingLoopS Env (λ env → varn env + vari env ≡ c10) (λ e1 → vari e1 ≡ c10) (λ env → varn env)
+        (λ n2 p2 loop exit → whileLoopSeg {_} {_} {c10} n2 p2 loop exit) n1 p1 (λ ne pe → whileTestSpec1 c10 ne pe))) 
 
 
-{-# TERMINATING #-}
-loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
-loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit
 
 
-loopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
-loopPwP' zero env refl refl exit = exit env refl
-loopPwP' (suc n) env refl refl exit  = whileLoopPwP' (suc n) env refl refl (λ env x y → loopPwP' n env x y exit) exit
-
-
-loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) → (seq : whileTestStateP s2 env) → loopPwP' n env (sym eq) seq λ env₁ x → (vari env₁ ≡ c10 env₁)
-loopHelper zero env eq refl rewrite eq = refl
-loopHelper (suc n) env eq refl rewrite eq = loopHelper n (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env))
-
-
---  all codtions are correctly connected and required condtion is proved in the continuation
---      use required condition as t in (env → t) → t
---
-whileTestPCallwP : (c :  ℕ ) → Set
-whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c10 env )  ) where
-   conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
-   conv e record { pi1 = refl ; pi2 = refl } = +zero
-
 
-whileTestPCallwP' : (c :  ℕ ) → Set
-whileTestPCallwP' c = whileTestPwP {_} {_} c (λ env s → loopPwP' (varn env) env refl (conv env s) ( λ env s → vari env ≡ c10 env )  ) where
-  conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
-  conv e record { pi1 = refl ; pi2 = refl } = +zero
-
-helperCallwP : (c : ℕ) → whileTestPCallwP' c
-helperCallwP c = whileTestPwP {_} {_} c (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero)
-
---
--- Using imply relation to make soundness explicit
--- termination is shown by induction on varn
---
-
-data _implies_  (A B : Set ) : Set (succ Zero) where
-    proof : ( A → B ) → A implies B
-
-implies2p : {A B : Set } → A implies B  → A → B
-implies2p (proof x) = x
-
-bwhileTestPSem :  (c : ℕ) → whileTestP c ( λ env → ⊤ implies (whileTestStateP s1 env) )
-whileTestPSem c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } )
-
-SemGears : (f : {l : Level } {t : Set l } → (e0 : Envc ) → ((e : Envc) → t)  → t ) → Set (succ Zero)
-SemGears f = Envc → Envc → Set
-
-GearsUnitSound : (e0 e1 : Envc) {pre : Envc → Set} {post : Envc → Set}
-   → (f : {l : Level } {t : Set l } → (e0 : Envc ) → (Envc → t)  → t )
-   → (fsem : (e0 : Envc ) → f e0 ( λ e1 → (pre e0) implies (post e1)))
-   → f e0 (λ e1 → pre e0 implies post e1)
-GearsUnitSound e0 e1 f fsem = fsem e0
-
-whileTestPSemSound : (c : ℕ ) (output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c))
-whileTestPSemSound c output refl = whileTestPSem c
 
 
-whileConvPSemSound : {l : Level} → (input : Envc) → (whileTestStateP s1 input ) implies (whileTestStateP s2 input)
-whileConvPSemSound input = proof λ x → (conv input x) where
-  conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
-  conv e record { pi1 = refl ; pi2 = refl } = +zero
 
-loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
-loopPP zero input refl = input
-loopPP (suc n) input refl =
-    loopPP n (record input { varn = pred (varn input) ; vari = suc (vari input)}) refl
-
-whileLoopPSem : {l : Level} {t : Set l}   → (input : Envc ) → whileTestStateP s2 input
-  → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output)  → t)
-  → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)  → t) → t
-whileLoopPSem env s next exit with varn env | s
-... | zero | _ = exit env (proof (λ z → z))
-... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } ) (proof λ x → +-suc varn (vari env) )
-
-loopPPSem : (input output : Envc ) →  output ≡ loopPP (varn input)  input refl
-  → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)
-loopPPSem input output refl s2p = loopPPSemInduct (varn input) input  refl refl s2p
-  where
-    lem : (n : ℕ) → (env : Envc) → n + suc (vari env) ≡ suc (n + vari env)
-    lem n env = +-suc (n) (vari env)
-    loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) →  (loopeq : output ≡ loopPP n current eq)
-      → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
-    loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl)
-    loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) =
-        whileLoopPSem current refl
-            (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
-            (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
-
-whileLoopPSemSound : {l : Level} → (input output : Envc )
-   → whileTestStateP s2 input
-   →  output ≡ loopPP (varn input) input refl
-   → (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
-whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre
-
-
--- whileTestSound : {l : Level} (c : ℕ) → (output : Envc) → ⊤ →  whileTestStateP sf output
--- whileTestSound {l} c record { c10 = c10 ; varn = varn ; vari = vari } top =
---    implies2p (whileLoopPSemSound {l} (record { c10 = c ; varn = c ; vari = zero }) (record { c10 = c10 ; varn = c ; vari = vari}) (+zero) {!!})
---    (implies2p (whileConvPSemSound {l} (record { c10 = c ; varn = c ; vari = zero })) (implies2p (whileTestPSemSound c (whileTestP c (λ e → e)) refl) top))
diff -r 9c91d23c2836 -r a7263ecf8671 whileTestGears1.agda
--- a/whileTestGears1.agda	Mon Nov 01 08:34:07 2021 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,188 +0,0 @@
-module whileTestGears1 where
-
-open import Function
-open import Data.Nat renaming ( _∸_ to _-_)
-open import Data.Bool hiding ( _≟_ ;  _≤?_ ; _≤_ ; _<_ )
-open import Level renaming ( suc to succ ; zero to Zero )
-open import Relation.Nullary using (¬_; Dec; yes; no)
-open import Relation.Binary.PropositionalEquality
-
-open import utilities
-open  _/\_
-
-record Env  : Set where
-  field
-    varn : ℕ
-    vari : ℕ
-open Env
-
-whileTestS : { m : Level}  → (c10 : ℕ) → (Code : Env → Set m) → Set m
-whileTestS c10 next = next (record {varn = c10 ; vari = 0} )
-
-whileTestS1 :  (c10 : ℕ) →  whileTestS c10 (λ e → ((varn e ≡ c10) /\ (vari e ≡ 0 )) )
-whileTestS1 c10 = record { pi1 = refl ; pi2 = refl }
-
-
-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
-whileLoop env next with lt 0 (varn env)
-whileLoop env next | false = next env
-whileLoop env next | true =
-    whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
-
-test1 : Env
-test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 ))
-
-
-proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
-proof1 = refl
-
---                                                                              ↓PostCondition
-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}
-    proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition
-    proof2 = record {pi1 = refl ; pi2 = refl}
-
-open import Data.Empty
-open import Data.Nat.Properties
-
-lemma1 : {i : ℕ} →  ¬ 1 ≤ i → i ≡ 0
-lemma1 {zero} not = refl
-lemma1 {suc i} not = ⊥-elim ( not (s≤s z≤n) )
-
-{-# TERMINATING #-} --                                                  ↓PreCondition(Invaliant)
-whileLoop' : {l : Level} {t : Set l} → (env : Env) → {c10 :  ℕ } → ((varn env) + (vari env) ≡ c10)
-   → (Code : (e1 : Env )→ vari e1 ≡ c10 → t) → t
-whileLoop' env proof next with  ( suc zero  ≤? (varn  env) )
-whileLoop' env {c10} proof next | no p = next env ( begin
-       vari env            ≡⟨ refl ⟩
-       0 + vari env        ≡⟨ cong (λ k → k + vari env) (sym (lemma1 p )) ⟩
-       varn env + vari env ≡⟨ proof ⟩
-       c10 ∎ ) where open ≡-Reasoning  
-whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next where
-      env1 = record {varn = (varn  env) - 1 ; vari = (vari env) + 1}
-      1<0 : 1 ≤ zero → ⊥
-      1<0 ()
-      proof3 : (suc zero  ≤ (varn  env))  → varn env1 + vari env1 ≡ c10
-      proof3 (s≤s lt) with varn  env
-      proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p)
-      proof3 (s≤s (z≤n {n'}) ) | suc n =  let open ≡-Reasoning  in begin
-             n' + (vari env + 1)  ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
-             n' + (1 + vari env ) ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
-             (n' + 1) + vari env  ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
-             (suc n' ) + vari env ≡⟨⟩
-             varn env + vari env  ≡⟨ proof  ⟩
-             c10
-          ∎
-
--- Condition to Invaliant
-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 where
-      proof4 : varn env + vari env ≡ c10
-      proof4 = let open ≡-Reasoning  in begin
-            varn env + vari env ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
-            c10 + vari env      ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩
-            c10 + 0             ≡⟨ +-sym {c10} {0} ⟩
-            c10
-          ∎
-
-open import Data.Unit hiding ( _≟_ ;  _≤?_ ; _≤_)
-
-whileTestSpec1 : (c10 : ℕ) →  (e1 : Env ) → vari e1 ≡ c10 → ⊤
-whileTestSpec1 _ _ x = tt
-
-proofGears : {c10 :  ℕ } → ⊤
-proofGears {c10} = whileTest' {_} {_}  {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 p3 → whileTestSpec1 c10 n2 p3 ))) 
-
---                                                                      ↓PreCondition(Invaliant)
-whileLoopSeg : {l : Level} {t : Set l} → {c10 :  ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10)
-   → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t) 
-   → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t
-whileLoopSeg env proof next exit with  ( suc zero  ≤? (varn  env) )
-whileLoopSeg {_} {_} {c10} env proof next exit | no p = exit env ( begin
-       vari env            ≡⟨ refl ⟩
-       0 + vari env        ≡⟨ cong (λ k → k + vari env) (sym (lemma1 p )) ⟩
-       varn env + vari env ≡⟨ proof ⟩
-       c10 ∎ ) where open ≡-Reasoning  
-whileLoopSeg {_} {_} {c10} env proof next exit | yes p = next env1 (proof3 p ) (proof4 (varn env) p) where
-      env1 = record {varn = (varn  env) - 1 ; vari = (vari env) + 1}
-      1<0 : 1 ≤ zero → ⊥
-      1<0 ()
-      proof4 : (i : ℕ) → 1 ≤ i  → i - 1 < i
-      proof4 zero ()
-      proof4 (suc i) lt = begin
-          suc (suc i - 1 ) ≤⟨ ≤-refl ⟩
-          suc i ∎ where open ≤-Reasoning 
-      proof3 : (suc zero  ≤ (varn  env))  → varn env1 + vari env1 ≡ c10
-      proof3 (s≤s lt) with varn  env
-      proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p)
-      proof3 (s≤s (z≤n {n'}) ) | suc n =  let open ≡-Reasoning  in begin
-             n' + (vari env + 1)  ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
-             n' + (1 + vari env ) ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
-             (n' + 1) + vari env  ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
-             (suc n' ) + vari env ≡⟨⟩
-             varn env + vari env  ≡⟨ proof  ⟩
-             c10
-          ∎
-
-open import Relation.Binary.Definitions
-
-nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
-nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
-lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥
-lemma3 refl ()
-lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
-lemma5 (s≤s z≤n) ()
-
-TerminatingLoop : {l : Level} {t : Set l} {c10 :  ℕ } → (i : ℕ) → (env : Env) → i ≡ varn env
-   →  varn env + vari env ≡ c10 
-   →  (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t
-TerminatingLoop {_} {t} {c10} i env refl p exit with <-cmp 0 i
-... | tri≈ ¬a b ¬c = whileLoopSeg {_} {t} {c10} env p (λ e1 eq lt → ⊥-elim (lemma3 b lt) ) exit 
-... | tri< a ¬b ¬c = whileLoopSeg {_} {t} {c10} env p (λ e1 p1 lt1 → TerminatingLoop1 i env e1 (≤-step lt1) p1 lt1 ) exit where --  varn e1 < suc (varn env)
-    TerminatingLoop1 : (j : ℕ) → (env e1 : Env) → varn e1 < suc j  → varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t
-    TerminatingLoop1 zero env e1 n≤j eq lt = whileLoopSeg {_} {t} {c10} e1 eq (λ e2 eq lt1 → ⊥-elim (lemma5 n≤j lt1)) exit  
-    TerminatingLoop1 (suc j) env e1 n≤j eq lt with <-cmp (varn e1) (suc j)
-    ... | tri< a ¬b ¬c = TerminatingLoop1 j env e1 a eq lt 
-    ... | tri≈ ¬a refl ¬c = whileLoopSeg {_} {t} {c10} e1 eq lemma4 exit where
-       lemma4 : (e2 : Env) → varn e2 + vari e2 ≡ c10 → varn e2 < varn e1 → t
-       lemma4 e2 eq lt1 = TerminatingLoop1 j e1 e2 lt1 eq lt1 
-    ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )   
-
-proofGearsTerm : {c10 :  ℕ } → ⊤
-proofGearsTerm {c10} = whileTest' {_} {_}  {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → TerminatingLoop (varn n1) n1 refl p2 (λ n2 p3 → whileTestSpec1 c10 n2 p3 ))) 
-
-TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → (Invraiant : Index → Set ) → (ExitCond : Index → Set) → ( reduce : Index → ℕ)
-   → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)  → Invraiant r1 → reduce r1 < reduce r  → t ) → (exit : (re : Index) → ExitCond re → t) → t)
-   → (i : ℕ) → (r : Index) → reduce r ≡ i  → (p : Invraiant r)  → (exit : (re : Index) → ExitCond re → t)  → t 
-TerminatingLoopS {_} {t} Index Invraiant ExitCond reduce loop  i r refl p exit with <-cmp 0 i
-... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) exit 
-... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 i r r1 (≤-step lt1) p1 lt1 ) exit where 
-    TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j  → Invraiant r1 →  reduce r1 < reduce r → t
-    TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) exit  
-    TerminatingLoop1 (suc j) r r1  n≤j p1 lt with <-cmp (reduce r1) (suc j)
-    ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt 
-    ... | tri≈ ¬a b ¬c = loop r1 p1 lemma4 exit where
-       lemma4 : (r2 : Index) → Invraiant r2 → reduce r2 < reduce r1  → t
-       lemma4 r2 p2 lt1 = TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1  
-    ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )   
-
-proofGearsTermS : {c10 :  ℕ } → ⊤
-proofGearsTermS {c10} = whileTest' {_} {_}  {c10} (λ n p →  conversion1 n p (λ n1 p1 →
-    TerminatingLoopS Env (λ env → varn env + vari env ≡ c10) (λ e1 → vari e1 ≡ c10) (λ env → varn env)
-        (λ n2 p2 loop exit → whileLoopSeg {_} {_} {c10} n2 p2 loop exit) (varn n1) n1 refl p1 (λ ne pe → whileTestSpec1 c10 ne pe))) 
-
-
-
-
-
-
-
-
diff -r 9c91d23c2836 -r a7263ecf8671 whileTestPrim.agda
--- a/whileTestPrim.agda	Mon Nov 01 08:34:07 2021 +0900
+++ b/whileTestPrim.agda	Mon Nov 01 09:59:43 2021 +0900
@@ -1,7 +1,7 @@
 module whileTestPrim where
 
 open import Function
-open import Data.Nat
+open import Data.Nat renaming ( _∸_ to _-_)
 open import Data.Bool hiding ( _≟_ )
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Relation.Nullary using (¬_; Dec; yes; no)
diff -r 9c91d23c2836 -r a7263ecf8671 whileTestPrimProof.agda
--- a/whileTestPrimProof.agda	Mon Nov 01 08:34:07 2021 +0900
+++ b/whileTestPrimProof.agda	Mon Nov 01 09:59:43 2021 +0900
@@ -1,7 +1,7 @@
 module whileTestPrimProof where
 
 open import Function
-open import Data.Nat
+open import Data.Nat renaming  ( _∸_ to _-_)
 open import Data.Bool hiding ( _≟_ )
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Relation.Nullary using (¬_; Dec; yes; no)