Mercurial > hg > Members > atton > agda-proofs

comparison cbc/stack-subtype-sample.agda @ 68:f3ad255e3b50

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove n-pop/n-push !
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 15 Jan 2017 04:02:23 +0000
parents ee2659635734
children b3b778d828c8
comparison
equal deleted inserted replaced
67:ee2659635734 68:f3ad255e3b50
85 pushOnce : Meta -> Meta 85 pushOnce : Meta -> Meta
86 pushOnce m = M.exec pushSingleLinkedStackCS m 86 pushOnce m = M.exec pushSingleLinkedStackCS m
87 87
88 n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta 88 n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
89 n-push {{mm}} (zero) = M.cs {{mm}} {{mm}} id 89 n-push {{mm}} (zero) = M.cs {{mm}} {{mm}} id
90 n-push {m} {{mm}} (suc n) = M.csComp {m} {{mm}} {{mm}} {{mm}} {{mm}} (n-push {m} {{mm}} n) (M.cs {{mm}} {{mm}} pushOnce) 90 n-push {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-push {m} {{mm}} n) (pushOnce m))
91 91
92 popOnce : Meta -> Meta 92 popOnce : Meta -> Meta
93 popOnce m = M.exec popSingleLinkedStackCS m 93 popOnce m = M.exec popSingleLinkedStackCS m
94 94
95 n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta 95 n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
219 ≡ M.exec (n-push {meta} n) meta 219 ≡ M.exec (n-push {meta} n) meta
220 where 220 where
221 meta = id-meta cn ce s 221 meta = id-meta cn ce s
222 222
223 pop-n-push : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> pop-n-push-type n cn ce s 223 pop-n-push : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> pop-n-push-type n cn ce s
224
224 pop-n-push zero cn ce s = refl 225 pop-n-push zero cn ce s = refl
225 pop-n-push (suc n) cn ce s = begin 226 pop-n-push (suc n) cn ce s = begin
226 M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta cn ce s) 227 M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc (suc n)))) (id-meta cn ce s)
227 ≡⟨ refl ⟩ 228 ≡⟨ refl ⟩
228 M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta cn ce s) 229 M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce))) (id-meta cn ce s)
229 ≡⟨ exec-comp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s) ⟩ 230 ≡⟨ exec-comp (M.cs popOnce) (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce)) (id-meta cn ce s) ⟩
230 M.exec (M.cs popOnce) (M.exec (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s)) 231 M.exec (M.cs popOnce) (M.exec (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce)) (id-meta cn ce s))
231 ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩ 232 ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩
232 M.exec (M.cs popOnce) (M.exec (n-push (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s))) 233 M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s)))
233 ≡⟨ refl ⟩ 234 ≡⟨ refl ⟩
234 M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) 235 M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})))
235 ≡⟨ sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) ⟩ 236 ≡⟨ sym (exec-comp (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) ⟩
236 M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) 237 M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
237 ≡⟨ pop-n-push {!!} cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) ⟩ 238 ≡⟨ pop-n-push n cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) ⟩
238 M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) 239 M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
239 ≡⟨ refl ⟩ 240 ≡⟨ refl ⟩
240 M.exec (n-push n) (pushOnce (id-meta cn ce s)) 241 M.exec (n-push n) (pushOnce (id-meta cn ce s))
241 ≡⟨ refl ⟩ 242 ≡⟨ refl ⟩
242 M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s)) 243 M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s))
243 ≡⟨ sym (exec-comp (n-push n) (M.cs pushOnce) (id-meta cn ce s)) ⟩ 244 ≡⟨ refl ⟩
244 M.exec (M.csComp (n-push n) (M.cs pushOnce)) (id-meta cn ce s) 245 M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s)
245 ≡⟨ refl ⟩ 246 ∎
246 M.exec (n-push (suc n)) (id-meta cn ce s) 247
247 ∎ 248 {-begin
249 {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} M.exec (n-push (suc n)) (id-meta cn ce s)
250 ∎
251 -}
248 252
249 253
250 n-push-pop-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ 254 n-push-pop-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁
251 n-push-pop-type n cn ce st = M.exec (M.csComp {meta} (n-pop {meta} n) (n-push {meta} n)) meta ≡ meta 255 n-push-pop-type n cn ce st = M.exec (M.csComp {meta} (n-pop {meta} n) (n-push {meta} n)) meta ≡ meta
252 where 256 where
253 meta = id-meta cn ce st 257 meta = id-meta cn ce st
254 258
255 n-push-pop : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> n-push-pop-type n cn ce s 259 n-push-pop : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> n-push-pop-type n cn ce s
256 n-push-pop zero cn ce s = refl 260 n-push-pop zero cn ce s = refl
257 n-push-pop (suc n) cn ce s = begin 261 n-push-pop (suc n) cn ce s = begin
258 M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta cn ce s) 262 M.exec (M.csComp (n-pop (suc n)) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s)
259 ≡⟨ refl ⟩ 263 ≡⟨ refl ⟩
260 M.exec (M.csComp (M.csComp (n-pop n) (M.cs popOnce)) (n-push (suc n))) (id-meta cn ce s) 264 M.exec (M.csComp (M.csComp (n-pop n) (M.cs popOnce)) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s)
261 ≡⟨ cong (\f -> M.exec f (id-meta cn ce s)) (sym (M.comp-associative (n-push (suc n)) (M.cs popOnce) (n-pop n))) ⟩ 265 ≡⟨ cong (\f -> M.exec f (id-meta cn ce s)) (sym (M.comp-associative (n-push {id-meta cn ce s} (suc n)) (M.cs popOnce) (n-pop n))) ⟩
262 M.exec (M.csComp (n-pop n) (M.csComp (M.cs popOnce) (n-push (suc n)))) (id-meta cn ce s) 266 M.exec (M.csComp (n-pop n) (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce s} (suc n)))) (id-meta cn ce s)
263 ≡⟨ exec-comp (n-pop n) (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce s) ⟩ 267 ≡⟨ exec-comp (n-pop n) (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s) ⟩
264 M.exec (n-pop n) (M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce s)) 268 M.exec (n-pop n) (M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s))
265 ≡⟨ cong (\x -> M.exec (n-pop n) x) (pop-n-push n cn ce s) ⟩ 269 ≡⟨ cong (\x -> M.exec (n-pop n) x) (pop-n-push n cn ce s) ⟩
266 M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s)) 270 M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s))
267 ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) ⟩ 271 ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) ⟩
268 M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s) 272 M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s)
269 ≡⟨ n-push-pop n cn ce s ⟩ 273 ≡⟨ n-push-pop n cn ce s ⟩