Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 79:52d957db0222

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author ryokka
date Mon, 30 Dec 2019 20:53:00 +0900
parents 083a18424f75
children 148feaa1e346
comparison
equal deleted inserted replaced
78:083a18424f75 79:52d957db0222
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 = zero ; vari = vari } next exit = exit env 126 whileLoopP' env@record { c10 = c10 ; varn = zero ; vari = vari } _ exit = exit env
127 whileLoopP' env@record { c10 = c10 ; varn = (suc varn1) ; vari = vari } next exit = next (record env {varn = varn1 ; vari = vari + 1 }) 127 whileLoopP' record { c10 = c10 ; varn = suc varn1 ; vari = vari } next _ = next (record {c10 = c10 ; varn = varn1 ; vari = suc vari })
128 128
129 -- whileLoopP env next exit | tri≈ ¬a b ¬c = exit env
130 -- whileLoopP env next exit | tri< a ¬b ¬c =
131 -- next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 })
132 129
133 {-# TERMINATING #-} 130 {-# TERMINATING #-}
134 loopP : {l : Level} {t : Set l} → Envc → (exit : Envc → t) → t 131 loopP : {l : Level} {t : Set l} → Envc → (exit : Envc → t) → t
135 loopP env exit = whileLoopP env (λ env → loopP env exit ) exit 132 loopP env exit = whileLoopP env (λ env → loopP env exit ) exit
136 133
214 211
215 212
216 whileLoopPSem' : {l : Level} {t : Set l} → (input : Envc ) → whileTestStateP s2 input 213 whileLoopPSem' : {l : Level} {t : Set l} → (input : Envc ) → whileTestStateP s2 input
217 → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → t) 214 → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → t)
218 → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) → t) → t 215 → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) → t) → t
219 whileLoopPSem' env@(record { c10 = c10 ; varn = zero ; vari = vari }) s next exit = exit env (proof (λ z → z)) 216 whileLoopPSem' env@(record { c10 = c10 ; varn = zero ; vari = vari }) s _ exit = exit env (proof (λ z → z))
220 whileLoopPSem' env@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) s next exit = next env (proof (λ z → {!!})) 217 whileLoopPSem' env@(record { c10 = c10 ; varn = suc varn ; vari = vari }) refl next _ =
221 218 next (record env {c10 = c10 ; varn = varn ; vari = suc vari }) (proof λ x → +-suc varn vari)
222 219
220
221 {--
222 (((⊤ implies varn ≡ 0 ∧ vari ≡ c10 ) implies (varn + vari ≡ c10)) implies vari ≡ c10)
223
224
225 --}
223 loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc 226 loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
224 loopPP zero input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input 227 loopPP zero input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input
225 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) 228 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 -- ?
226 229
227 loopPPSem : {l : Level} {t : Set l} → (input output : Envc ) → output ≡ loopPP (varn input) input refl 230 loopPP' : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
231 loopPP' zero input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input
232 loopPP' (suc n) input@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) refl = loopPP' n (record { c10 = c10 ; varn = varn₁ ; vari = suc vari }) refl -- ?
233
234 loopPPSem : (input output : Envc ) → output ≡ loopPP' (varn input) input refl
228 → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) 235 → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)
229 loopPPSem {l} {t} input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p 236 loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p
230 where 237 where
231 -- lem : (output : Envc) → loopPP (varn input) input refl ≡ output → Envc.vari (loopPP (Envc.varn input) input refl) ≡ Envc.c10 output 238 -- lem : (output : Envc) → loopPP (varn input) input refl ≡ output → Envc.vari (loopPP (Envc.varn input) input refl) ≡ Envc.c10 output
232 -- lem output eq with <-cmp 0 (Envc.varn input) 239 -- lem output eq with <-cmp 0 (Envc.varn input)
233 -- lem output refl | tri< a ¬b ¬c = {!!} 240 -- lem output refl | tri< a ¬b ¬c rewrite s2p = {!!}
234 -- lem output refl | tri≈ ¬a refl ¬c = s2p 241 -- lem output refl | tri≈ ¬a refl ¬c = s2p
235 loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) → output ≡ loopPP n current eq 242 loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) → (loopeq : output ≡ loopPP' n current eq)
236 → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output) 243 → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
237 loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → x) -- proof (λ x → lem {!!} {!!}) 244 loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl) -- loopeq には output ≡ loopPP zero current (zero = varn current)
238 loopPPSemInduct (suc n) current refl loopeq s2p with <-cmp 0 (suc n) 245
239 loopPPSemInduct (suc n) current refl loopeq refl | tri< a ¬b ¬c = {!!} 246 -- n を減らして loop を回しつつ証明したい
240 -- loopPPSemInduct (suc n) record { c10 = _ ; varn = .(suc n) ; vari = _ } refl eq s2p | tri< a ¬b ¬c | proof x = proof λ x₁ → {!!} 247 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
241 248 -- loopPPSemInduct zero (record { c10 = vari current ; varn = zero ; vari = vari current }) {!!} {!!} refl) {!!}
242 -- loopPPSemInduct (suc n) record { c10 = _ ; varn = .(suc n) ; vari = _ } refl eq s2p | tri< a ¬b ¬c | aa = {!!} 249
243 250 loopPPSemInduct2 : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) → (loopeq : output ≡ loopPP n current eq)
244 251 → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
245 252 loopPPSemInduct2 .0 record { c10 = .vari₁ ; varn = zero ; vari = vari₁ } refl loopeq refl rewrite loopeq = proof (λ x → refl)
246 lpc : (input : Envc ) → Envc 253 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 → {!!}
247 lpc input@(record { c10 = c10 ; varn = zero ; vari = vari }) = input 254
248 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) 255 -- -- whileLoopPSem' current refl (λ output x → loopPPSemInduct2 (n) (current) refl loopeq refl) (λ output x → loopPPSemInduct2 (n) (current) refl loopeq refl)
249 256
250 257
251 258 whileLoopPSemSound : {l : Level} → (input output : Envc )
252
253 -- loopPP' input | tri≈ ¬a b ¬c = input
254 -- loopPP' input | tri< a ¬b ¬c = whileLoopP input (λ enext → loopPP' enext) (λ eout → eout)
255 -- loopPP' (whileLoopP input (λ next → loopPP' next) (λ output → output))
256
257
258 -- = whileLoopP input (λ next → loopPP next ) (λ output → output )
259
260 whileLoopPSemSound : (input output : Envc )
261 → whileTestStateP s2 input 259 → whileTestStateP s2 input
262 → output ≡ lpc input 260 → output ≡ loopPP' (varn input) input refl
263 → (whileTestStateP s2 input ) implies ( whileTestStateP sf output ) 261 → (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
264 whileLoopPSemSound input output pre eq = {!!} 262 whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre
265 263
266 -- with (lpc input)
267 -- 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 → {!!}
268 -- where
269 -- lem : (whileTestStateP s2 input ) → (varn input + vari input ≡ c10 input)
270 -- implies (vari output ≡ c10 output)
271 -- lem refl = proof λ x → {!!}
272
273
274 -- whileLoopPSem' input pre (λ output1 x → proof (λ x₁ → ?)) (λ output₁ x → proof (λ x₁ → ?))))
275 -- proof (whileLoopPwP input pre (λ e p1 p11 → {!!}) (λ e2 p2 p22 → {!!}) )
276 -- with <-cmp 0 (varn input )
277 -- ... | ttt = {!!}
278 264
279 -- induction にする 265 -- induction にする
280 {-# TERMINATING #-} 266 {-# TERMINATING #-}
281 loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t 267 loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
282 loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit 268 loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit