Mercurial > hg > Papers > 2018 > ryokka-thesis
comparison final_pre/src/AgdaNPushNPopProof.agda @ 7:28f900230c26
add final_pre
author | ryokka |
---|---|
date | Mon, 19 Feb 2018 23:32:24 +0900 |
parents | |
children |
comparison
equal
deleted
inserted
replaced
6:d927f6b3d2b3 | 7:28f900230c26 |
---|---|
1 pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ | |
2 pop-n-push-type n cn ce s = M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) meta | |
3 ≡ M.exec (n-push n) meta | |
4 where | |
5 meta = id-meta cn ce s | |
6 | |
7 pop-n-push : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> pop-n-push-type n cn ce s | |
8 pop-n-push zero cn ce s = refl | |
9 pop-n-push (suc n) cn ce s = begin | |
10 M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta cn ce s) | |
11 ≡⟨ refl ⟩ | |
12 M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta cn ce s) | |
13 ≡⟨ exec-comp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s) ⟩ | |
14 M.exec (M.cs popOnce) (M.exec (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s)) | |
15 ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩ | |
16 M.exec (M.cs popOnce) (M.exec (n-push (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s))) | |
17 ≡⟨ refl ⟩ | |
18 M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) | |
19 ≡⟨ sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) ⟩ | |
20 M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) | |
21 ≡⟨ pop-n-push n cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) ⟩ | |
22 M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})) | |
23 ≡⟨ refl ⟩ | |
24 M.exec (n-push n) (pushOnce (id-meta cn ce s)) | |
25 ≡⟨ refl ⟩ | |
26 M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s)) | |
27 ≡⟨ refl ⟩ | |
28 M.exec (n-push (suc n)) (id-meta cn ce s) | |
29 ∎ | |
30 | |
31 | |
32 | |
33 n-push-pop-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ | |
34 n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop n) (n-push n)) meta ≡ meta | |
35 where | |
36 meta = id-meta cn ce st | |
37 | |
38 n-push-pop : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> n-push-pop-type n cn ce s | |
39 n-push-pop zero cn ce s = refl | |
40 n-push-pop (suc n) cn ce s = begin | |
41 M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta cn ce s) | |
42 ≡⟨ refl ⟩ | |
43 M.exec (M.csComp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push (suc n))) (id-meta cn ce s) | |
44 ≡⟨ exec-comp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push (suc n)) (id-meta cn ce s) ⟩ | |
45 M.exec (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (M.exec (n-push (suc n)) (id-meta cn ce s)) | |
46 ≡⟨ refl ⟩ | |
47 M.exec (n-pop n) (popOnce (M.exec (n-push (suc n)) (id-meta cn ce s))) | |
48 ≡⟨ refl ⟩ | |
49 M.exec (n-pop n) (M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce s))) | |
50 ≡⟨ cong (\x -> M.exec (n-pop n) x) (sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce s))) ⟩ | |
51 M.exec (n-pop n) (M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce s)) | |
52 ≡⟨ cong (\x -> M.exec (n-pop n) x) (pop-n-push n cn ce s) ⟩ | |
53 M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s)) | |
54 ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) ⟩ | |
55 M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s) | |
56 ≡⟨ n-push-pop n cn ce s ⟩ | |
57 id-meta cn ce s | |
58 ∎ |