# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1635505759 -32400
# Node ID 908ed82e33c61975e55d10c503297b3674fef34a
# Parent  dc667b21c1b0426461537cd91888b48ec3de0cd9
termination

diff -r dc667b21c1b0 -r 908ed82e33c6 whileTestGears1.agda
--- a/whileTestGears1.agda	Fri Oct 29 13:03:52 2021 +0900
+++ b/whileTestGears1.agda	Fri Oct 29 20:09:19 2021 +0900
@@ -16,18 +16,18 @@
     vari : ℕ
 open Env
 
-whileTestS : { m : Level}  -> (c10 : ℕ) → (Code : Env -> Set m) -> Set m
+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 : {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 : {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 =
@@ -41,7 +41,7 @@
 proof1 = refl
 
 --                                                                              ↓PostCondition
-whileTest' : {l : Level} {t : Set l}  -> {c10 :  ℕ } → (Code : (env : Env)  -> ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -> t) -> t
+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
@@ -52,53 +52,48 @@
 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' : {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
+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 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
+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
           ∎
 
-open import Data.Unit
+open import Data.Unit hiding ( _≟_ ;  _≤?_ ; _≤_)
 
 whileTestSpec1 : (c10 : ℕ) →  (e1 : Env ) → vari e1 ≡ c10 → ⊤
 whileTestSpec1 _ _ x = tt
@@ -106,10 +101,38 @@
 proofGears : {c10 :  ℕ } → ⊤
 proofGears {c10} = whileTest' {_} {_}  {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 p3 → whileTestSpec1 c10 n2 p3 ))) 
 
-{-# TERMINATING #-}
-whileLoop0 : {l : Level} {t m : Set l} -> m -> Env -> (Code : m -> Env -> t) -> t
-whileLoop0 m env next with lt 0 (varn env)
-whileLoop0 m env next | false = next m env
-whileLoop0 m env next | true =
-    whileLoop0 m (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
+--                                                                      ↓PreCondition(Invaliant)
+whileLoopSeg : {l : Level} {t : Set l} → {c10 :  ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10)
+   → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → 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 ) 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
+          ∎
 
+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 {_} {_} {c10} zero env refl p exit = 
+     exit env p
+TerminatingLoop {_} {_} {c10} (suc i) env eq p exit = 
+     whileLoopSeg {_} {_} {c10} env p (λ e1 p1 → TerminatingLoop {_} {_} {c10} i e1 (lemma2 e1 p1 eq) p1 exit) exit where
+         lemma2 :  (e1 : Env) → varn e1 + vari e1 ≡ c10 →  suc i ≡ varn env → i ≡ varn e1
+         lemma2 = {!!}