Mercurial > hg > Members > ryokka > HoareLogic
changeset 74:6f26de2fb7fe
...
| author | ryokka |
|---|---|
| date | Thu, 26 Dec 2019 18:16:35 +0900 |
| parents | 52acd110df18 |
| children | d45e98211d7d |
| files | whileTestGears.agda |
| diffstat | 1 files changed, 10 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/whileTestGears.agda Thu Dec 26 17:39:56 2019 +0900 +++ b/whileTestGears.agda Thu Dec 26 18:16:35 2019 +0900 @@ -224,14 +224,17 @@ 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) -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 +loopPPSem : {l : Level} {t : Set l} → (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 s2p (proof (λ x → {!!})) 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 = {!!} + -- lem1 : (ncurrent : Envc) → suc (varn ncurrent) + vari ncurrent ≡ c10 ncurrent → varn ncurrent + suc (vari ncurrent) ≡ c10 ncurrent + -- lem1 current eq = {!!} + loopPPSemInduct : (n : ℕ) → (current : Envc) → varn current ≡ n → (whileTestStateP s2 current ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → (whileTestStateP s2 current ) implies (whileTestStateP sf output) + loopPPSemInduct zero current refl refl imp with loopPP (varn current) current refl -- = proof λ x → {!!} + loopPPSemInduct zero record { c10 = _ ; varn = _ ; vari = _ } refl refl imp | record { c10 = c10 ; varn = varn ; vari = vari } = proof {!!} + loopPPSemInduct (suc n) current refl s2p imp with <-cmp 0 (suc n) | whileLoopPSem current s2p (λ output x → proof {!!}) λ output x → proof λ x₁ → {!!} + loopPPSemInduct (suc n) record { c10 = _ ; varn = .(suc n) ; vari = _ } refl s2p imp | tri< a ¬b ¬c | proof x = {!!}