Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 80:148feaa1e346

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
write loopPPSemInduct
author ryokka
date Wed, 01 Jan 2020 21:50:38 +0900
parents 52d957db0222
children 0122f980427c
comparison
equal deleted inserted replaced
79:52d957db0222 80:148feaa1e346
212 212
213 whileLoopPSem' : {l : Level} {t : Set l} → (input : Envc ) → whileTestStateP s2 input 213 whileLoopPSem' : {l : Level} {t : Set l} → (input : Envc ) → whileTestStateP s2 input
214 → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → t) 214 → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → t)
215 → (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
216 whileLoopPSem' env@(record { c10 = c10 ; varn = zero ; vari = vari }) s _ exit = exit env (proof (λ z → z)) 216 whileLoopPSem' env@(record { c10 = c10 ; varn = zero ; vari = vari }) s _ exit = exit env (proof (λ z → z))
217 whileLoopPSem' env@(record { c10 = c10 ; varn = suc varn ; vari = vari }) refl next _ = 217 whileLoopPSem' env@(record { c10 = c10 ; varn = suc varn ; vari = vari }) refl next exit =
218 next (record env {c10 = c10 ; varn = varn ; vari = suc vari }) (proof λ x → +-suc varn vari) 218 next (record env {c10 = c10 ; varn = varn ; vari = suc vari }) (proof λ x → +-suc varn vari)
219 219
220 220
221 {-- 221 {--
222 (((⊤ implies varn ≡ 0 ∧ vari ≡ c10 ) implies (varn + vari ≡ c10)) implies vari ≡ c10) 222 (((⊤ implies varn ≡ 0 ∧ vari ≡ c10 ) implies (varn + vari ≡ c10)) implies vari ≡ c10)
226 loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc 226 loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
227 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
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 -- ? 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 -- ?
229 229
230 loopPP' : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc 230 loopPP' : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
231
231 loopPP' zero input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input 232 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 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
234 loopPPSem : (input output : Envc ) → output ≡ loopPP' (varn input) input refl 235 loopPPSem : (input output : Envc ) → output ≡ loopPP' (varn input) input refl
235 → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output) 236 → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)
237 where 238 where
238 -- lem : (output : Envc) → loopPP (varn input) input refl ≡ output → Envc.vari (loopPP (Envc.varn input) input refl) ≡ Envc.c10 output 239 -- lem : (output : Envc) → loopPP (varn input) input refl ≡ output → Envc.vari (loopPP (Envc.varn input) input refl) ≡ Envc.c10 output
239 -- lem output eq with <-cmp 0 (Envc.varn input) 240 -- lem output eq with <-cmp 0 (Envc.varn input)
240 -- lem output refl | tri< a ¬b ¬c rewrite s2p = {!!} 241 -- lem output refl | tri< a ¬b ¬c rewrite s2p = {!!}
241 -- lem output refl | tri≈ ¬a refl ¬c = s2p 242 -- lem output refl | tri≈ ¬a refl ¬c = s2p
243 lem : (n : ℕ) → (env : Envc) → n + suc (vari env) ≡ suc (n + vari env)
244 lem n env = +-suc (n) (vari env)
242 loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) → (loopeq : output ≡ loopPP' n current eq) 245 loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) → (loopeq : output ≡ loopPP' n current eq)
243 → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output) 246 → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
244 loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl) -- loopeq には output ≡ loopPP zero current (zero = varn current) 247 loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl) -- loopeq には output ≡ loopPP zero current (zero = varn current)
245 248
246 -- n を減らして loop を回しつつ証明したい 249 -- n を減らして loop を回しつつ証明したい
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 250 loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) = whileLoopPSem' current refl (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl) (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
248 -- loopPPSemInduct zero (record { c10 = vari current ; varn = zero ; vari = vari current }) {!!} {!!} refl) {!!}
249
250 loopPPSemInduct2 : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) → (loopeq : output ≡ loopPP n current eq)
251 → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
252 loopPPSemInduct2 .0 record { c10 = .vari₁ ; varn = zero ; vari = vari₁ } refl loopeq refl rewrite loopeq = proof (λ x → refl)
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 → {!!}
254 251
255 -- -- whileLoopPSem' current refl (λ output x → loopPPSemInduct2 (n) (current) refl loopeq refl) (λ output x → loopPPSemInduct2 (n) (current) refl loopeq refl) 252 -- -- whileLoopPSem' current refl (λ output x → loopPPSemInduct2 (n) (current) refl loopeq refl) (λ output x → loopPPSemInduct2 (n) (current) refl loopeq refl)
256 253
257 254
258 whileLoopPSemSound : {l : Level} → (input output : Envc ) 255 whileLoopPSemSound : {l : Level} → (input output : Envc )
278 conv1 e record { pi1 = refl ; pi2 = refl } = +zero 275 conv1 e record { pi1 = refl ; pi2 = refl } = +zero
279 276
280 -- = whileTestPwP (suc c) (λ env s → loopPwP env (conv1 env s) (λ env₁ s₁ → {!!})) 277 -- = whileTestPwP (suc c) (λ env s → loopPwP env (conv1 env s) (λ env₁ s₁ → {!!}))
281 278
282 279
283 data GComm : Set (succ Zero) where 280 -- data GComm : Set (succ Zero) where
284 Skip : GComm 281 -- Skip : GComm
285 Abort : GComm 282 -- Abort : GComm
286 PComm : Set → GComm 283 -- PComm : Set → GComm
287 -- Seq : GComm → GComm → GComm 284 -- -- Seq : GComm → GComm → GComm
288 -- If : whileTestState → GComm → GComm → GComm 285 -- -- If : whileTestState → GComm → GComm → GComm
289 while : whileTestState → GComm → GComm 286 -- while : whileTestState → GComm → GComm
290 287
291 gearsSem : {l : Level} {t : Set l} → {c10 : ℕ} → Envc → Envc → (Envc → (Envc → t) → t) → Set 288 -- gearsSem : {l : Level} {t : Set l} → {c10 : ℕ} → Envc → Envc → (Envc → (Envc → t) → t) → Set
292 gearsSem pre post = {!!} 289 -- gearsSem pre post = {!!}
293 290
294 unionInf : ∀ {l} -> (ℕ -> Rel Set l) -> Rel Set l 291 -- unionInf : ∀ {l} -> (ℕ -> Rel Set l) -> Rel Set l
295 unionInf f a b = ∃ (λ (n : ℕ) → f n a b) 292 -- unionInf f a b = ∃ (λ (n : ℕ) → f n a b)
296 293
297 comp : ∀ {l} → Rel Set l → Rel Set l → Rel Set (succ Zero Level.⊔ l) 294 -- comp : ∀ {l} → Rel Set l → Rel Set l → Rel Set (succ Zero Level.⊔ l)
298 comp r1 r2 a b = ∃ (λ (a' : Set) → r1 a a' × r2 a' b) 295 -- comp r1 r2 a b = ∃ (λ (a' : Set) → r1 a a' × r2 a' b)
299 296
300 -- repeat : ℕ -> rel set zero -> rel set zero 297 -- -- repeat : ℕ -> rel set zero -> rel set zero
301 -- repeat ℕ.zero r = λ x x₁ → ⊤ 298 -- -- repeat ℕ.zero r = λ x x₁ → ⊤
302 -- repeat (ℕ.suc m) r = comp (repeat m r) r 299 -- -- repeat (ℕ.suc m) r = comp (repeat m r) r
303 300
304 GSemComm : {l : Level} {t : Set l} → GComm → Rel whileTestState (Zero) 301 -- GSemComm : {l : Level} {t : Set l} → GComm → Rel whileTestState (Zero)
305 GSemComm Skip = λ x x₁ → ⊤ 302 -- GSemComm Skip = λ x x₁ → ⊤
306 GSemComm Abort = λ x x₁ → ⊥ 303 -- GSemComm Abort = λ x x₁ → ⊥
307 GSemComm (PComm x) = λ x₁ x₂ → x 304 -- GSemComm (PComm x) = λ x₁ x₂ → x
308 -- GSemComm (Seq con con₁ con₃) = λ x₁ x₂ → {!!} 305 -- -- GSemComm (Seq con con₁ con₃) = λ x₁ x₂ → {!!}
309 -- GSemComm (If x con con₁) = {!!} 306 -- -- GSemComm (If x con con₁) = {!!}
310 GSemComm (while x con) = λ x₁ x₂ → unionInf {Zero} (λ (n : ℕ) → {!!}) {!!} {!!} 307 -- GSemComm (while x con) = λ x₁ x₂ → unionInf {Zero} (λ (n : ℕ) → {!!}) {!!} {!!}
311 308
312 ProofConnect : {l : Level} {t : Set l} 309 ProofConnect : {l : Level} {t : Set l}
313 → (pr1 : Envc → Set → Set) 310 → (pr1 : Envc → Set → Set)
314 → (Envc → Set → (Envc → Set → t)) 311 → (Envc → Set → (Envc → Set → t))
315 → (Envc → Set → Set) 312 → (Envc → Set → Set)