changeset 79:52d957db0222

fix
author ryokka
date Mon, 30 Dec 2019 20:53:00 +0900
parents 083a18424f75
children 148feaa1e346
files utilities.agda whileTestGears.agda
diffstat 2 files changed, 32 insertions(+), 45 deletions(-) [+]
line wrap: on
line diff
--- a/utilities.agda	Fri Dec 27 21:10:02 2019 +0900
+++ b/utilities.agda	Mon Dec 30 20:53:00 2019 +0900
@@ -64,6 +64,7 @@
             y + suc x
           ∎ )
 
+
 minus-plus : { x y : ℕ } → (suc x - 1) + (y + 1) ≡ suc x + y
 minus-plus {zero} {y} = +-sym {y} {1}
 minus-plus {suc x} {y} =  cong ( λ z → suc z ) (minus-plus {x} {y})
--- a/whileTestGears.agda	Fri Dec 27 21:10:02 2019 +0900
+++ b/whileTestGears.agda	Mon Dec 30 20:53:00 2019 +0900
@@ -123,12 +123,9 @@
      next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 })
 
 whileLoopP' : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → t) → t
-whileLoopP' env@record { c10 = c10 ; varn = zero ; vari = vari } next exit = exit env
-whileLoopP' env@record { c10 = c10 ; varn = (suc varn1) ; vari = vari } next exit = next (record env {varn = varn1 ; vari = vari + 1 })
+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 })
 
--- 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} → Envc → (exit : Envc → t) → t
@@ -216,65 +213,54 @@
 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@(record { c10 = c10 ; varn = zero ; vari = vari }) s next exit = exit env (proof (λ z → z))
-whileLoopPSem' env@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) s next exit = next env (proof (λ z → {!!}))
+whileLoopPSem' env@(record { c10 = c10 ; varn = zero ; vari = vari }) s _ exit = exit env (proof (λ z → z))
+whileLoopPSem' env@(record { c10 = c10 ; varn = suc varn ; vari = vari }) refl next _ =
+  next (record env {c10 = c10 ; varn = varn ; vari = suc vari }) (proof λ x → +-suc varn vari)
 
 
+{--
+ (((⊤ implies varn ≡ 0 ∧ vari ≡ c10 ) implies (varn + vari ≡ c10)) implies vari ≡ c10)
+
+
+--}
 loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
 loopPP zero input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input
-loopPP (suc n) input@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) refl = whileLoopP' (record { c10 = c10 ; varn = (varn₁) ; vari = vari }) (λ x → loopPP n  (record { c10 = c10 ; varn = (varn₁) ; vari = vari }) refl) (λ output → output)
+loopPP (suc n) input@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) refl = whileLoopP input (λ x → loopPP n (record x { c10 = c10 ; varn = varn₁ ; vari = suc vari }) refl) λ x → x -- ?
 
-loopPPSem : {l : Level} {t : Set l} → (input output : Envc ) →  output ≡ loopPP (varn input)  input refl
+loopPP' : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
+loopPP' zero input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input
+loopPP' (suc n) input@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) refl = loopPP' n (record { c10 = c10 ; varn = varn₁ ; vari = suc vari }) refl -- ?
+
+loopPPSem : (input output : Envc ) →  output ≡ loopPP' (varn input)  input refl
   → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)
-loopPPSem {l} {t} input output refl s2p = loopPPSemInduct (varn input) input  refl refl s2p
+loopPPSem input output refl s2p = loopPPSemInduct (varn input) input  refl refl s2p
   where
     -- lem : (output : Envc) → loopPP (varn input) input refl ≡ output → Envc.vari (loopPP (Envc.varn input) input refl) ≡  Envc.c10 output
     -- lem output eq with <-cmp 0 (Envc.varn input)
-    -- lem output refl | tri< a ¬b ¬c = {!!}
+    -- lem output refl | tri< a ¬b ¬c rewrite s2p = {!!}
     -- lem output refl | tri≈ ¬a refl ¬c = s2p
-    loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) →  output ≡ loopPP n  current eq
+    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 → x) -- proof (λ x → lem {!!} {!!})
-    loopPPSemInduct (suc n) current refl loopeq s2p  with <-cmp 0 (suc n)
-    loopPPSemInduct (suc n) current refl loopeq refl | tri< a ¬b ¬c = {!!}
-    -- loopPPSemInduct (suc n) record { c10 = _ ; varn = .(suc n) ; vari = _ } refl eq s2p | tri< a ¬b ¬c | proof x = proof λ x₁ → {!!}
+    loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl) -- loopeq には output ≡ loopPP zero current (zero = varn current)
 
---    loopPPSemInduct (suc n) record { c10 = _ ; varn = .(suc n) ; vari = _ } refl eq s2p | tri< a ¬b ¬c | aa = {!!}
-
-
+    -- n を減らして loop を回しつつ証明したい
+    loopPPSemInduct (suc n) current refl loopeq refl = whileLoopPSem' current refl (λ output x → loopPPSemInduct (suc n) current {!!} {!!} {!!}) {!!}  -- why we can't write loopPPSemInduct n (record { c10 = suc (n + vari current) ; varn = n ; vari = suc (vari current) }) hogefuga
+    -- loopPPSemInduct zero (record { c10 = vari current ; varn = zero ; vari = vari current }) {!!} {!!} refl) {!!}
 
-lpc : (input : Envc ) → Envc
-lpc input@(record { c10 = c10 ; varn = zero ; vari = vari }) = input
-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)
+    loopPPSemInduct2 : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) →  (loopeq : output ≡ loopPP n  current eq)
+      → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
+    loopPPSemInduct2 .0 record { c10 = .vari₁ ; varn = zero ; vari = vari₁ } refl loopeq refl rewrite loopeq = proof (λ x → refl)
+    loopPPSemInduct2 .(suc varn₁) record { c10 = .(suc (varn₁ + vari₁)) ; varn = (suc varn₁) ; vari = vari₁ } refl loopeq refl rewrite loopeq = whileLoopPSem' (record { c10 = (suc (varn₁ + vari₁)) ; varn = (suc varn₁) ; vari = vari₁ }) refl (λ output x → {!!}) λ exit x → {!!}
 
-
+-- -- whileLoopPSem' current refl (λ output x → loopPPSemInduct2 (n) (current) refl loopeq refl) (λ output x → loopPPSemInduct2 (n) (current) refl loopeq refl)
 
 
--- loopPP' input | tri≈ ¬a b ¬c = input
--- loopPP' input | tri< a ¬b ¬c = whileLoopP input (λ enext → loopPP' enext) (λ eout → eout)
--- loopPP' (whileLoopP input (λ next → loopPP' next) (λ output → output))
-
-
--- = whileLoopP input (λ next → loopPP next ) (λ output → output )
-
-whileLoopPSemSound : (input output : Envc )
+whileLoopPSemSound : {l : Level} → (input output : Envc )
    → whileTestStateP s2 input
-   →  output ≡ lpc input
+   →  output ≡ loopPP' (varn input) input refl
    → (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
-whileLoopPSemSound input output pre eq = {!!}
+whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre
 
--- 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)
-  --   lem refl = proof λ x → {!!}
-
-
--- whileLoopPSem' input pre (λ output1 x → proof (λ x₁ → ?)) (λ output₁ x → proof (λ x₁ → ?))))
--- proof (whileLoopPwP input pre (λ e p1 p11 → {!!}) (λ e2 p2 p22 → {!!}) )
--- with <-cmp 0 (varn input )
--- ... | ttt = {!!}
 
 -- induction にする
 {-# TERMINATING #-}