changeset 73:52acd110df18

fix
author ryokka
date Thu, 26 Dec 2019 17:39:56 +0900
parents 66ba3b1eec0a
children 6f26de2fb7fe
files whileTestGears.agda
diffstat 1 files changed, 15 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Wed Dec 25 17:15:17 2019 +0900
+++ b/whileTestGears.agda	Thu Dec 26 17:39:56 2019 +0900
@@ -211,11 +211,6 @@
 whileLoopPSem env s next exit | tri≈ ¬a b ¬c rewrite (sym b) = exit env (proof (λ z → z))
 whileLoopPSem env s next exit | tri< a ¬b ¬c  = next env (proof (λ z → z))
 
-{-# TERMINATING #-}
-loopPP : (input : Envc ) → Envc
-loopPP input with <-cmp 0 (varn input)
-loopPP input | tri≈ ¬a b ¬c = input
-loopPP input | tri< a ¬b ¬c = loopPP (whileLoopP input (λ next → loopPP next) (λ output → output))
 
 
 whileLoopPSem' : {l : Level} {t : Set l}   → (input : Envc ) → whileTestStateP s2 input
@@ -225,21 +220,23 @@
 whileLoopPSem' env@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) s next exit = next env (proof (λ z → z))
 
 
-loopPP' : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
-loopPP' n input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input
+loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
+loopPP n input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input
+loopPP n input@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) refl = whileLoopP (record { c10 = c10 ; varn = (varn₁) ; vari = vari }) (λ x → loopPP (n - 1)  (record { c10 = c10 ; varn = (varn₁) ; vari = vari }) refl) (λ output → output)
 
--- Maybe "Z-Conbinater"
--- Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))
+loopPPSem : {l : Level} {t : Set l} → (input output : Envc ) → loopPP (varn input)  input refl ≡  output
+  → (whileTestStateP s2 input ) implies (whileTestStateP sf output)
+loopPPSem {l} {t} input output refl = loopPPSemInduct (varn input) input refl
+  where
+    loopPPSemInduct : (n : ℕ) → (current : Envc) → varn current ≡ n  → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
+    loopPPSemInduct zero current refl = proof λ x → {!!}
+    loopPPSemInduct (suc n) current refl with whileLoopPSem current {!!} {!!} {!!}
+    ... | aa = {!!}
 
-loopPP' n input@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) refl = whileLoopP (record { c10 = c10 ; varn = (varn₁) ; vari = vari }) (λ x → loopPP' (n - 1)  (record { c10 = c10 ; varn = (varn₁) ; vari = vari }) refl) (λ output → output)
 
 
 lpc : (input : Envc ) → Envc
 lpc input@(record { c10 = c10 ; varn = zero ; vari = vari }) = input
-
--- Maybe "Z-Conbinater"
--- Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))
-
 lpc input@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) = whileLoopP (record { c10 = c10 ; varn = (varn₁) ; vari = vari }) (λ x → lpc record { c10 = c10 ; varn = (varn₁) ; vari = vari }) (λ output → output)
 
 
@@ -255,10 +252,11 @@
 whileLoopPSemSound : (input output : Envc )
    → whileTestStateP s2 input
    →  output ≡ lpc input
-   -- (whileLoopP input (λ tt → whileLoopP tt {!!} {!!}) {!!}) ← y-conbinater
    → (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
-whileLoopPSemSound input output pre refl with (lpc input)
-whileLoopPSemSound record { c10 = c11 ; varn = varn₁ ; vari = vari₁ } .(lpc (record { c10 = c11 ; varn = varn₁ ; vari = vari₁ })) pre refl | record { c10 = c10 ; varn = varn ; vari = vari } = proof λ x → {!!}
+whileLoopPSemSound input output pre eq = {!!}
+
+-- with (lpc input)
+-- record { c10 = c11 ; varn = varn₁ ; vari = vari₁ } .(lpc (record { c10 = c11 ; varn = varn₁ ; vari = vari₁ })) pre refl | record { c10 = c10 ; varn = varn ; vari = vari } = proof λ x → {!!}
   -- where
   --   lem : (whileTestStateP s2 input ) → (varn input + vari input ≡ c10 input)
   --     implies (vari output ≡ c10 output)