Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 75:d45e98211d7d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author ryokka
date Thu, 26 Dec 2019 18:34:27 +0900
parents 6f26de2fb7fe
children cf00bc7af369
comparison
equal deleted inserted replaced
74:6f26de2fb7fe 75:d45e98211d7d
224 loopPP n input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input 224 loopPP n input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input
225 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) 225 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)
226 226
227 loopPPSem : {l : Level} {t : Set l} → (input output : Envc ) → output ≡ loopPP (varn input) input refl 227 loopPPSem : {l : Level} {t : Set l} → (input output : Envc ) → output ≡ loopPP (varn input) input refl
228 → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) 228 → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)
229 loopPPSem {l} {t} input output refl s2p = loopPPSemInduct (varn input) input refl s2p (proof (λ x → {!!})) 229 loopPPSem {l} {t} input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p
230 where 230 where
231 -- lem1 : (ncurrent : Envc) → suc (varn ncurrent) + vari ncurrent ≡ c10 ncurrent → varn ncurrent + suc (vari ncurrent) ≡ c10 ncurrent 231 loopPPSemInduct : (n : ℕ) → (current : Envc) → varn current ≡ n → output ≡ loopPP n current {!!}
232 -- lem1 current eq = {!!} 232 → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
233 loopPPSemInduct : (n : ℕ) → (current : Envc) → varn current ≡ n → (whileTestStateP s2 current ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → (whileTestStateP s2 current ) implies (whileTestStateP sf output) 233 loopPPSemInduct zero current refl eq refl with loopPP (varn current) current refl -- = proof λ x → {!!}
234 loopPPSemInduct zero current refl refl imp with loopPP (varn current) current refl -- = proof λ x → {!!} 234 loopPPSemInduct zero record { c10 = _ ; varn = _ ; vari = _ } refl eq refl | record { c10 = c10 ; varn = varn ; vari = vari } = proof (λ x → {!!})
235 loopPPSemInduct zero record { c10 = _ ; varn = _ ; vari = _ } refl refl imp | record { c10 = c10 ; varn = varn ; vari = vari } = proof {!!} 235 loopPPSemInduct (suc n) current refl eq s2p with <-cmp 0 (suc n) | whileLoopPSem current s2p (λ output x → proof {!!}) λ output x → proof λ x₁ → {!!}
236 loopPPSemInduct (suc n) current refl s2p imp with <-cmp 0 (suc n) | whileLoopPSem current s2p (λ output x → proof {!!}) λ output x → proof λ x₁ → {!!} 236 loopPPSemInduct (suc n) record { c10 = _ ; varn = .(suc n) ; vari = _ } refl eq s2p | tri< a ¬b ¬c | proof x = {!!}
237 loopPPSemInduct (suc n) record { c10 = _ ; varn = .(suc n) ; vari = _ } refl s2p imp | tri< a ¬b ¬c | proof x = {!!}
238 237
239 238
240 239
241 lpc : (input : Envc ) → Envc 240 lpc : (input : Envc ) → Envc
242 lpc input@(record { c10 = c10 ; varn = zero ; vari = vari }) = input 241 lpc input@(record { c10 = c10 ; varn = zero ; vari = vari }) = input