Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 74:6f26de2fb7fe

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