Mercurial > hg > Members > atton > agda-proofs
annotate cbc/stack-subtype-sample.agda @ 66:211fde284b7e
Trying prove n-push/n-pop
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 15 Jan 2017 02:33:47 +0000 |
parents | c87e85ffde9a |
children | ee2659635734 |
rev | line source |
---|---|
56
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 module stack-subtype-sample where |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 |
64
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
3 open import Level renaming (suc to S ; zero to O) |
61 | 4 open import Function |
56
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import Data.Nat |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import Data.Maybe |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import Relation.Binary.PropositionalEquality |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 |
64
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
9 open import stack-subtype ℕ |
61 | 10 open import subtype Context as N |
11 open import subtype Meta as M | |
56
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 record Num : Set where |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 field |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 num : ℕ |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 instance |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 NumIsNormalDataSegment : N.DataSegment Num |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 NumIsNormalDataSegment = record { get = (\c -> record { num = Context.n c}) |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 ; set = (\c n -> record c {n = Num.num n})} |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 NumIsMetaDataSegment : M.DataSegment Num |
60
bd428bd6b394
Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
56
diff
changeset
|
23 NumIsMetaDataSegment = record { get = (\m -> record {num = Context.n (Meta.context m)}) |
bd428bd6b394
Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
56
diff
changeset
|
24 ; set = (\m n -> record m {context = record (Meta.context m) {n = Num.num n}})} |
56
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 plus3 : Num -> Num |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 plus3 record { num = n } = record {num = n + 3} |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 plus3CS : N.CodeSegment Num Num |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 plus3CS = N.cs plus3 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 |
61 | 35 plus5AndPushWithPlus3 : {mc : Meta} {{_ : N.DataSegment Num}} |
36 -> M.CodeSegment Num (Meta) | |
56
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 plus5AndPushWithPlus3 {mc} {{nn}} = M.cs (\n -> record {context = con n ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} ) |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 where |
60
bd428bd6b394
Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
56
diff
changeset
|
39 co = Meta.context mc |
56
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 con : Num -> Context |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 con record { num = num } = N.DataSegment.set nn co record {num = num + 5} |
60
bd428bd6b394
Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
56
diff
changeset
|
42 st = Meta.stack mc |
56
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 |
61 | 47 push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta |
56
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 push-sample {{nd}} {{md}} = M.exec {{md}} (plus5AndPushWithPlus3 {mc} {{nd}}) mc |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 where |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 con = record { n = 4 ; element = just 0} |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 code = N.cs (\c -> c) |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code} |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 push-sample-equiv : push-sample ≡ record { nextCS = liftContext plus3CS |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 ; stack = record { top = nothing} |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 ; context = record { n = 9} } |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 push-sample-equiv = refl |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
59 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 |
61 | 61 pushed-sample : {m : Meta} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta |
56
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
62 pushed-sample {m} {{nd}} {{md}} = M.exec {{md}} (M.csComp {m} {{md}} pushSingleLinkedStackCS (plus5AndPushWithPlus3 {mc} {{nd}})) mc |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 where |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 con = record { n = 4 ; element = just 0} |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
65 code = N.cs (\c -> c) |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code} |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
68 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
69 |
61 | 70 pushed-sample-equiv : {m : Meta} -> |
60
bd428bd6b394
Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
56
diff
changeset
|
71 pushed-sample {m} ≡ record { nextCS = liftContext plus3CS |
bd428bd6b394
Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
56
diff
changeset
|
72 ; stack = record { top = just (cons 0 nothing) } |
bd428bd6b394
Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
56
diff
changeset
|
73 ; context = record { n = 12} } |
56
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
74 pushed-sample-equiv = refl |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
75 |
ddcd652969e0
Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
76 |
60
bd428bd6b394
Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
56
diff
changeset
|
77 |
61 | 78 pushNum : N.CodeSegment Context Context |
79 pushNum = N.cs pn | |
80 where | |
81 pn : Context -> Context | |
62 | 82 pn record { n = n } = record { n = pred n ; element = just n} |
60
bd428bd6b394
Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
56
diff
changeset
|
83 |
61 | 84 |
62 | 85 pushOnce : Meta -> Meta |
86 pushOnce m = M.exec pushSingleLinkedStackCS m | |
61 | 87 |
62 | 88 n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta |
64
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
89 n-push {{mm}} (zero) = M.cs {{mm}} {{mm}} id |
66
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
90 n-push {m} {{mm}} (suc n) = M.csComp {m} {{mm}} {{mm}} {{mm}} {{mm}} (n-push {m} {{mm}} n) (M.cs {{mm}} {{mm}} pushOnce) |
62 | 91 |
63 | 92 popOnce : Meta -> Meta |
93 popOnce m = M.exec popSingleLinkedStackCS m | |
94 | |
95 n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta | |
64
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
96 n-pop {{mm}} (zero) = M.cs {{mm}} {{mm}} id |
63 | 97 n-pop {m} {{mm}} (suc n) = M.csComp {m} {{mm}} {{mm}} {{mm}} {{mm}} (n-pop {m} {{mm}} n) (M.cs {{mm}} {{mm}} popOnce) |
98 | |
99 | |
61 | 100 |
101 | |
64
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
102 initMeta : ℕ -> Maybe ℕ -> N.CodeSegment Context Context -> Meta |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
103 initMeta n mn code = record { context = record { n = n ; element = mn} |
61 | 104 ; stack = emptySingleLinkedStack |
105 ; nextCS = code | |
106 } | |
107 | |
64
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
108 n-push-cs-exec = M.exec (n-push {meta} 3) meta |
62 | 109 where |
64
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
110 meta = (initMeta 5 (just 9) pushNum) |
61 | 111 |
112 | |
62 | 113 n-push-cs-exec-equiv : n-push-cs-exec ≡ record { nextCS = pushNum |
114 ; context = record {n = 2 ; element = just 3} | |
64
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
115 ; stack = record {top = just (cons 4 (just (cons 5 (just (cons 9 nothing)))))}} |
61 | 116 n-push-cs-exec-equiv = refl |
62 | 117 |
63 | 118 |
64
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
119 n-pop-cs-exec = M.exec (n-pop {meta} 4) meta |
63 | 120 where |
121 meta = record { nextCS = N.cs id | |
122 ; context = record { n = 0 ; element = nothing} | |
123 ; stack = record {top = just (cons 9 (just (cons 8 (just (cons 7 (just (cons 6 (just (cons 5 nothing)))))))))} | |
124 } | |
125 | |
126 n-pop-cs-exec-equiv : n-pop-cs-exec ≡ record { nextCS = N.cs id | |
127 ; context = record { n = 0 ; element = just 6} | |
128 ; stack = record { top = just (cons 5 nothing)} | |
129 } | |
130 | |
131 n-pop-cs-exec-equiv = refl | |
64
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
132 |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
133 |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
134 open ≡-Reasoning |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
135 |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
136 {- |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
137 comp-id-type : {m : Meta} {{mm : M.DataSegment Meta}} (f : M.CodeSegment Meta Meta) -> Set₁ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
138 comp-id-type {m} {{mm}} f = M.csComp {m} {{mm}} {{mm}} {{mm}} {{mm}} f (M.cs {S O} {S O} {Meta} {Meta} {{mm}}{{mm}} id) ≡ f |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
139 |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
140 comp-id : {m : Meta} (f : M.CodeSegment Meta Meta) -> comp-id-type {m} f |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
141 comp-id (M.cs f) = refl |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
142 |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
143 n-pop-pop-once-n-push :(n : ℕ) (m : Meta) -> |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
144 M.exec (M.csComp {m} (M.csComp {m} (n-pop {m} n) (M.cs popOnce)) (n-push {m} (suc n))) m |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
145 ≡ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
146 M.exec (M.csComp {m} (n-pop {m} n) (n-push {m} n)) m |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
147 n-pop-pop-once-n-push zero m = begin |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
148 M.exec (M.csComp {m} (M.csComp {m} (n-pop {m} zero) (M.cs popOnce)) (n-push {m} (suc zero))) m |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
149 ≡⟨ refl ⟩ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
150 M.exec (M.csComp {m} (M.csComp {m} (M.cs {S O} {S O} {Meta} {Meta} id) (M.cs popOnce)) (n-push {m} (suc zero))) m |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
151 ≡⟨ {!!} ⟩ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
152 M.exec (M.csComp {m} (M.cs popOnce) (n-push {m} (suc zero))) m |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
153 ≡⟨ {!!} ⟩ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
154 M.exec (M.csComp {m} (n-pop {m} zero) (n-push {m} zero)) m |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
155 ∎ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
156 n-pop-pop-once-n-push (suc n) m = {!!} |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
157 -} |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
158 |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
159 |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
160 |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
161 |
66
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
162 id-meta : ℕ -> ℕ -> SingleLinkedStack ℕ -> Meta |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
163 id-meta n e s = record { context = record {n = n ; element = just e} |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
164 ; nextCS = (N.cs id) ; stack = s} |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
165 |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
166 exec-comp : (f g : M.CodeSegment Meta Meta) (m : Meta) -> M.exec (M.csComp {m} f g) m ≡ M.exec f (M.exec g m) |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
167 exec-comp (M.cs x) (M.cs _) m = refl |
64
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
168 |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
169 |
66
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
170 push-pop-type : ℕ -> ℕ -> ℕ -> Element ℕ -> Set₁ |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
171 push-pop-type n e x s = M.exec (M.csComp {meta} (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
172 where |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
173 meta = id-meta n e record {top = just (cons x (just s))} |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
174 |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
175 push-pop : (n e x : ℕ) -> (s : Element ℕ) -> push-pop-type n e x s |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
176 push-pop n e x s = refl |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
177 |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
178 |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
179 |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
180 {- |
64
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
181 {- |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
182 n-pop-pop-once-n-push : (n : ℕ) (c : Context) -> |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
183 M.exec (M.csComp {id-meta c} (M.csComp {id-meta c} (n-pop {id-meta c} n) (M.cs popOnce)) (n-push {id-meta c} (suc n))) (id-meta c) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
184 ≡ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
185 M.exec (M.csComp {id-meta c} (n-pop {id-meta c} n) (n-push {id-meta c} n)) (id-meta c) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
186 n-pop-pop-once-n-push zero c = begin |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
187 M.exec (M.csComp {id-meta c} (M.csComp {id-meta c}(n-pop {id-meta c} zero) (M.cs popOnce)) (n-push {id-meta c} (suc zero))) (id-meta c) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
188 ≡⟨ refl ⟩ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
189 M.exec (M.csComp {id-meta c} (M.csComp {id-meta c} (M.cs {S O} {S O} {Meta} {Meta} id) (M.cs popOnce)) (n-push {id-meta c} (suc zero))) (id-meta c) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
190 ≡⟨ refl ⟩ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
191 M.exec (M.csComp {id-meta c} (M.cs popOnce) (n-push {id-meta c} (suc zero))) (id-meta c) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
192 ≡⟨ refl ⟩ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
193 M.exec (M.csComp {id-meta c} (M.cs popOnce) (M.cs pushOnce)) (id-meta c) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
194 ≡⟨ push-pop c ⟩ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
195 id-meta c |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
196 ≡⟨ refl ⟩ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
197 M.exec (M.csComp {id-meta c} (n-pop {id-meta c} zero) (n-push {id-meta c} zero)) (id-meta c) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
198 ∎ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
199 n-pop-pop-once-n-push (suc n) c = begin |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
200 M.exec (M.csComp (M.csComp (n-pop (suc n)) (M.cs popOnce)) (n-push (suc (suc n)))) (id-meta c) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
201 ≡⟨ cong (\f -> M.exec f (id-meta c)) (sym (M.comp-associative (n-push (suc (suc n))) (M.cs popOnce) (n-pop (suc n)))) ⟩ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
202 M.exec (M.csComp (n-pop (suc n)) (M.csComp (M.cs popOnce) (n-push (suc (suc n))))) (id-meta c) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
203 ≡⟨ {!!} ⟩ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
204 M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta c) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
205 ∎ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
206 -} |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
207 |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
208 |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
209 |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
210 |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
211 n-push-pop : (n : ℕ) (c : Context) -> |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
212 (M.exec (M.csComp {id-meta c} (M.cs popOnce) (n-push {id-meta c} (suc n))) (id-meta c)) ≡ M.exec (n-push {id-meta c} n) (id-meta c) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
213 n-push-pop zero c = push-pop c |
66
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
214 n-push-pop (suc n) c = {!!} |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
215 -} |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
216 |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
217 pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
218 pop-n-push-type n cn ce s = M.exec (M.csComp {meta} (M.cs popOnce) (n-push {meta} (suc n))) meta |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
219 ≡ M.exec (n-push {meta} n) meta |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
220 where |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
221 meta = id-meta cn ce s |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
222 |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
223 pop-n-push : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> pop-n-push-type n cn ce s |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
224 pop-n-push zero cn ce s = refl |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
225 pop-n-push (suc n) cn ce s = begin |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
226 M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta cn ce s) |
64
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
227 ≡⟨ refl ⟩ |
66
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
228 M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta cn ce s) |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
229 ≡⟨ exec-comp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s) ⟩ |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
230 M.exec (M.cs popOnce) (M.exec (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s)) |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
231 ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩ |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
232 M.exec (M.cs popOnce) (M.exec (n-push (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s))) |
64
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
233 ≡⟨ refl ⟩ |
66
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
234 M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (record { nextCS = (N.cs id) ; |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
235 context = record {n = cn ; element = just ce} ; |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
236 stack = record {top = just (cons ce (SingleLinkedStack.top s)) } |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
237 })) |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
238 ≡⟨ {!!} ⟩ |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
239 M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) ? |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
240 ≡⟨ {!!} ⟩ |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
241 M.exec (n-push n) (record { nextCS = (N.cs id) ; context = record {n = cn ; element = just ce} ; |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
242 stack = record {top = just (cons ce (SingleLinkedStack.top s))}}) |
65
c87e85ffde9a
Trying define n-push/n-pop equiv...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
64
diff
changeset
|
243 ≡⟨ refl ⟩ |
66
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
244 M.exec (n-push n) (pushOnce (id-meta cn ce s)) |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
245 ≡⟨ refl ⟩ |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
246 M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s)) |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
247 ≡⟨ sym (exec-comp (n-push n) (M.cs pushOnce) (id-meta cn ce s)) ⟩ |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
248 M.exec (M.csComp (n-push n) (M.cs pushOnce)) (id-meta cn ce s) |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
249 ≡⟨ refl ⟩ |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
250 M.exec (n-push (suc n)) (id-meta cn ce s) |
64
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
251 ∎ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
252 |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
253 |
66
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
254 n-push-pop-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
255 n-push-pop-type n cn ce st = M.exec (M.csComp {meta} (n-pop {meta} n) (n-push {meta} n)) meta ≡ meta |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
256 where |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
257 meta = id-meta cn ce st |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
258 |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
259 n-push-pop : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> n-push-pop-type n cn ce s |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
260 n-push-pop zero cn ce s = refl |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
261 n-push-pop (suc n) cn ce s = begin |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
262 M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta cn ce s) |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
263 ≡⟨ refl ⟩ |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
264 M.exec (M.csComp (M.csComp (n-pop n) (M.cs popOnce)) (n-push (suc n))) (id-meta cn ce s) |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
265 ≡⟨ cong (\f -> M.exec f (id-meta cn ce s)) (sym (M.comp-associative (n-push (suc n)) (M.cs popOnce) (n-pop n))) ⟩ |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
266 M.exec (M.csComp (n-pop n) (M.csComp (M.cs popOnce) (n-push (suc n)))) (id-meta cn ce s) |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
267 ≡⟨ exec-comp (n-pop n) (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce s) ⟩ |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
268 M.exec (n-pop n) (M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce s)) |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
269 ≡⟨ cong (\x -> M.exec (n-pop n) x) (pop-n-push n cn ce s) ⟩ |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
270 M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s)) |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
271 ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) ⟩ |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
272 M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s) |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
273 ≡⟨ n-push-pop n cn ce s ⟩ |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
274 id-meta cn ce s |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
275 ∎ |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
276 |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
277 {- |
64
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
278 n-push-pop-equiv : {c : Context} -> (n : ℕ ) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
279 -> M.exec (M.csComp {id-meta c} (n-pop {id-meta c} n) (n-push {id-meta c} n)) (id-meta c) ≡ (id-meta c) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
280 n-push-pop-equiv zero = refl |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
281 n-push-pop-equiv {c} (suc n) = begin |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
282 M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta c) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
283 ≡⟨ refl ⟩ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
284 M.exec (M.csComp (M.csComp (n-pop n) (M.cs popOnce)) (n-push (suc n))) (id-meta c) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
285 ≡⟨ cong (\f -> M.exec f (id-meta c)) (sym (M.comp-associative (n-push (suc n)) (M.cs popOnce) (n-pop n))) ⟩ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
286 M.exec (M.csComp (n-pop n) (M.csComp (M.cs popOnce) (n-push (suc n)))) (id-meta c) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
287 ≡⟨ exec-comp (n-pop n) (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta c) ⟩ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
288 M.exec (n-pop n) (M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta c)) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
289 ≡⟨ cong (\x -> M.exec (n-pop n) x) (n-push-pop n c ) ⟩ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
290 M.exec (n-pop n) (M.exec (n-push {id-meta c} n) (id-meta c)) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
291 ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta c)) ⟩ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
292 M.exec (M.csComp (n-pop n) (n-push n)) (id-meta c) |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
293 ≡⟨ n-push-pop-equiv n ⟩ |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
294 id-meta c |
44d448a978d3
Trying define n-push/n-pop equiv
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
63
diff
changeset
|
295 ∎ |
66
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
296 |
211fde284b7e
Trying prove n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
297 -} |