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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
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
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
10 open import subtype Context as N
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
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
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
35 plus5AndPushWithPlus3 : {mc : Meta} {{_ : N.DataSegment Num}}
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
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
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
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
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
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
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
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
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
78 pushNum : N.CodeSegment Context Context
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
79 pushNum = N.cs pn
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
80 where
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
81 pn : Context -> Context
62
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
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
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
84
62
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
85 pushOnce : Meta -> Meta
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
86 pushOnce m = M.exec pushSingleLinkedStackCS m
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
87
62
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
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
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
91
63
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
92 popOnce : Meta -> Meta
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
93 popOnce m = M.exec popSingleLinkedStackCS m
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
94
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
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
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
97 n-pop {m} {{mm}} (suc n) = M.csComp {m} {{mm}} {{mm}} {{mm}} {{mm}} (n-pop {m} {{mm}} n) (M.cs {{mm}} {{mm}} popOnce)
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
98
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
99
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
100
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
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
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
104 ; stack = emptySingleLinkedStack
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
105 ; nextCS = code
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
106 }
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
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
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
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
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
111
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
112
62
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
113 n-push-cs-exec-equiv : n-push-cs-exec ≡ record { nextCS = pushNum
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
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
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
116 n-push-cs-exec-equiv = refl
62
29b069a0c409 Define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 61
diff changeset
117
63
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
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
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
120 where
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
121 meta = record { nextCS = N.cs id
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
122 ; context = record { n = 0 ; element = nothing}
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
123 ; stack = record {top = just (cons 9 (just (cons 8 (just (cons 7 (just (cons 6 (just (cons 5 nothing)))))))))}
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
124 }
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
125
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
126 n-pop-cs-exec-equiv : n-pop-cs-exec ≡ record { nextCS = N.cs id
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
127 ; context = record { n = 0 ; element = just 6}
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
128 ; stack = record { top = just (cons 5 nothing)}
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
129 }
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
130
c3afde46a41d Define n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 62
diff changeset
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 -}