Mercurial > hg > Members > ryokka > HoareLogic
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 #-}