Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 72:66ba3b1eec0a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author ryokka
date Wed, 25 Dec 2019 17:15:17 +0900
parents 57d5a3884898
children 52acd110df18
comparison
equal deleted inserted replaced
71:57d5a3884898 72:66ba3b1eec0a
121 whileLoopP env next exit | tri≈ ¬a b ¬c = exit env 121 whileLoopP env next exit | tri≈ ¬a b ¬c = exit env
122 whileLoopP env next exit | tri< a ¬b ¬c = 122 whileLoopP env next exit | tri< a ¬b ¬c =
123 next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) 123 next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 })
124 124
125 whileLoopP' : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → t) → t 125 whileLoopP' : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → t) → t
126 whileLoopP' env@record { c10 = c10 ; varn = varn ; vari = zero } next exit = exit env 126 whileLoopP' env@record { c10 = c10 ; varn = zero ; vari = vari } next exit = exit env
127 whileLoopP' env@record { c10 = c10 ; varn = varn ; vari = (suc vari₁) } next exit = next (record env {varn = varn - 1 ; vari = (suc vari₁) + 1 }) 127 whileLoopP' env@record { c10 = c10 ; varn = (suc varn1) ; vari = vari } next exit = next (record env {varn = varn1 ; vari = vari + 1 })
128 128
129 -- whileLoopP env next exit | tri≈ ¬a b ¬c = exit env 129 -- whileLoopP env next exit | tri≈ ¬a b ¬c = exit env
130 -- whileLoopP env next exit | tri< a ¬b ¬c = 130 -- whileLoopP env next exit | tri< a ¬b ¬c =
131 -- next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) 131 -- next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 })
132 132
216 loopPP input with <-cmp 0 (varn input) 216 loopPP input with <-cmp 0 (varn input)
217 loopPP input | tri≈ ¬a b ¬c = input 217 loopPP input | tri≈ ¬a b ¬c = input
218 loopPP input | tri< a ¬b ¬c = loopPP (whileLoopP input (λ next → loopPP next) (λ output → output)) 218 loopPP input | tri< a ¬b ¬c = loopPP (whileLoopP input (λ next → loopPP next) (λ output → output))
219 219
220 220
221 whileLoopPSem' : {l : Level} {t : Set l} → (input : Envc ) → whileTestStateP s2 input
222 → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → t)
223 → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) → t) → t
224 whileLoopPSem' env@(record { c10 = c10 ; varn = zero ; vari = vari }) s next exit = exit env (proof (λ z → z))
225 whileLoopPSem' env@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) s next exit = next env (proof (λ z → z))
226
227
228 loopPP' : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
229 loopPP' n input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input
230
231 -- Maybe "Z-Conbinater"
232 -- Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))
233
234 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)
235
236
237 lpc : (input : Envc ) → Envc
238 lpc input@(record { c10 = c10 ; varn = zero ; vari = vari }) = input
239
240 -- Maybe "Z-Conbinater"
241 -- Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))
242
243 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)
244
245
246
247
248 -- loopPP' input | tri≈ ¬a b ¬c = input
249 -- loopPP' input | tri< a ¬b ¬c = whileLoopP input (λ enext → loopPP' enext) (λ eout → eout)
250 -- loopPP' (whileLoopP input (λ next → loopPP' next) (λ output → output))
251
252
221 -- = whileLoopP input (λ next → loopPP next ) (λ output → output ) 253 -- = whileLoopP input (λ next → loopPP next ) (λ output → output )
222 254
223 whileLoopPSemSound : (input output : Envc ) 255 whileLoopPSemSound : (input output : Envc )
224 → whileTestStateP s2 input 256 → whileTestStateP s2 input
225 → output ≡ loopPP input 257 → output ≡ lpc input
226 -- (whileLoopP input (λ tt → whileLoopP tt {!!} {!!}) {!!}) ← y-conbinater 258 -- (whileLoopP input (λ tt → whileLoopP tt {!!} {!!}) {!!}) ← y-conbinater
227 → (whileTestStateP s2 input ) implies ( whileTestStateP sf output ) 259 → (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
228 whileLoopPSemSound input output pre eq = whileLoopPSem input pre {!!} {!!} -- proof (whileLoopPwP input pre (λ e p1 p11 → {!!}) (λ e2 p2 p22 → {!!}) ) 260 whileLoopPSemSound input output pre refl with (lpc input)
261 whileLoopPSemSound 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 → {!!}
262 -- where
263 -- lem : (whileTestStateP s2 input ) → (varn input + vari input ≡ c10 input)
264 -- implies (vari output ≡ c10 output)
265 -- lem refl = proof λ x → {!!}
266
267
268 -- whileLoopPSem' input pre (λ output1 x → proof (λ x₁ → ?)) (λ output₁ x → proof (λ x₁ → ?))))
269 -- proof (whileLoopPwP input pre (λ e p1 p11 → {!!}) (λ e2 p2 p22 → {!!}) )
229 -- with <-cmp 0 (varn input ) 270 -- with <-cmp 0 (varn input )
230 -- ... | ttt = {!!} 271 -- ... | ttt = {!!}
231 272
232 -- induction にする 273 -- induction にする
233 {-# TERMINATING #-} 274 {-# TERMINATING #-}