Mercurial > hg > Gears > GearsAgda
annotate stack.agda @ 523:8fbc3ef749b6
separate Agda
| author | ryokka |
|---|---|
| date | Fri, 05 Jan 2018 16:39:43 +0900 |
| parents | src/parallel_execution/stack.agda@54ff7a97aec1 |
| children | f6060e1bf900 |
| rev | line source |
|---|---|
| 499 | 1 open import Level renaming (suc to succ ; zero to Zero ) |
| 496 | 2 module stack where |
| 154 | 3 |
| 161 | 4 open import Relation.Binary.PropositionalEquality |
| 477 | 5 open import Relation.Binary.Core |
| 484 | 6 open import Data.Nat |
| 478 | 7 |
| 484 | 8 ex : 1 + 2 ≡ 3 |
| 9 ex = refl | |
| 179 | 10 |
| 501 | 11 data Bool {n : Level } : Set n where |
| 161 | 12 True : Bool |
| 13 False : Bool | |
| 164 | 14 |
| 501 | 15 record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where |
| 485 | 16 field |
| 17 pi1 : a | |
| 18 pi2 : b | |
| 477 | 19 |
| 496 | 20 data Maybe {n : Level } (a : Set n) : Set n where |
| 161 | 21 Nothing : Maybe a |
| 22 Just : a -> Maybe a | |
| 23 | |
| 515 | 24 record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where |
| 161 | 25 field |
| 26 push : stackImpl -> a -> (stackImpl -> t) -> t | |
| 27 pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t | |
| 484 | 28 pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t |
|
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
29 get : stackImpl -> (stackImpl -> Maybe a -> t) -> t |
| 484 | 30 get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t |
|
503
413ce51da50b
separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
502
diff
changeset
|
31 open StackMethods |
| 427 | 32 |
| 515 | 33 record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where |
|
503
413ce51da50b
separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
502
diff
changeset
|
34 field |
|
413ce51da50b
separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
502
diff
changeset
|
35 stack : si |
| 515 | 36 stackMethods : StackMethods {n} {m} a {t} si |
| 37 pushStack : a -> (Stack a si -> t) -> t | |
|
503
413ce51da50b
separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
502
diff
changeset
|
38 pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } )) |
| 515 | 39 popStack : (Stack a si -> Maybe a -> t) -> t |
|
503
413ce51da50b
separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
502
diff
changeset
|
40 popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) |
| 515 | 41 pop2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t |
|
503
413ce51da50b
separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
502
diff
changeset
|
42 pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) |
| 515 | 43 getStack : (Stack a si -> Maybe a -> t) -> t |
|
503
413ce51da50b
separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
502
diff
changeset
|
44 getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) |
| 515 | 45 get2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t |
|
503
413ce51da50b
separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
502
diff
changeset
|
46 get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) |
| 484 | 47 |
|
503
413ce51da50b
separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
502
diff
changeset
|
48 open Stack |
| 427 | 49 |
| 496 | 50 data Element {n : Level } (a : Set n) : Set n where |
| 161 | 51 cons : a -> Maybe (Element a) -> Element a |
| 52 | |
| 496 | 53 datum : {n : Level } {a : Set n} -> Element a -> a |
| 161 | 54 datum (cons a _) = a |
| 55 | |
| 496 | 56 next : {n : Level } {a : Set n} -> Element a -> Maybe (Element a) |
| 161 | 57 next (cons _ n) = n |
| 58 | |
| 59 | |
| 164 | 60 {- |
| 61 -- cannot define recrusive record definition. so use linked list with maybe. | |
| 496 | 62 record Element {l : Level} (a : Set n l) : Set n (suc l) where |
| 161 | 63 field |
| 164 | 64 datum : a -- `data` is reserved by Agda. |
| 161 | 65 next : Maybe (Element a) |
| 66 -} | |
| 155 | 67 |
| 68 | |
| 164 | 69 |
| 496 | 70 record SingleLinkedStack {n : Level } (a : Set n) : Set n where |
| 161 | 71 field |
| 72 top : Maybe (Element a) | |
| 73 open SingleLinkedStack | |
| 155 | 74 |
| 499 | 75 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t |
| 161 | 76 pushSingleLinkedStack stack datum next = next stack1 |
| 77 where | |
| 78 element = cons datum (top stack) | |
| 164 | 79 stack1 = record {top = Just element} |
| 161 | 80 |
| 155 | 81 |
| 499 | 82 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t |
| 161 | 83 popSingleLinkedStack stack cs with (top stack) |
| 84 ... | Nothing = cs stack Nothing | |
| 85 ... | Just d = cs stack1 (Just data1) | |
| 154 | 86 where |
| 161 | 87 data1 = datum d |
| 88 stack1 = record { top = (next d) } | |
| 154 | 89 |
| 499 | 90 pop2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t |
| 91 pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack) | |
| 484 | 92 ... | Nothing = cs stack Nothing Nothing |
| 499 | 93 ... | Just d = pop2SingleLinkedStack' {n} {m} stack cs |
| 484 | 94 where |
| 499 | 95 pop2SingleLinkedStack' : {n m : Level } {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t |
| 484 | 96 pop2SingleLinkedStack' stack cs with (next d) |
| 97 ... | Nothing = cs stack Nothing Nothing | |
| 511 | 98 ... | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1)) |
| 484 | 99 |
| 100 | |
| 499 | 101 getSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t |
|
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
102 getSingleLinkedStack stack cs with (top stack) |
|
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
103 ... | Nothing = cs stack Nothing |
|
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
104 ... | Just d = cs stack (Just data1) |
|
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
105 where |
|
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
106 data1 = datum d |
|
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
107 |
| 499 | 108 get2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t |
| 109 get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack) | |
|
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
110 ... | Nothing = cs stack Nothing Nothing |
| 499 | 111 ... | Just d = get2SingleLinkedStack' {n} {m} stack cs |
|
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
112 where |
| 499 | 113 get2SingleLinkedStack' : {n m : Level} {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t |
| 484 | 114 get2SingleLinkedStack' stack cs with (next d) |
| 115 ... | Nothing = cs stack Nothing Nothing | |
| 116 ... | Just d1 = cs stack (Just (datum d)) (Just (datum d1)) | |
| 117 | |
|
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
118 |
|
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
119 |
| 496 | 120 emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a |
| 161 | 121 emptySingleLinkedStack = record {top = Nothing} |
| 122 | |
|
509
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
123 ----- |
|
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
124 -- Basic stack implementations are specifications of a Stack |
|
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
125 -- |
| 515 | 126 singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a) |
|
509
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
127 singleLinkedStackSpec = record { |
|
503
413ce51da50b
separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
502
diff
changeset
|
128 push = pushSingleLinkedStack |
| 161 | 129 ; pop = popSingleLinkedStack |
| 484 | 130 ; pop2 = pop2SingleLinkedStack |
|
483
9098ec0a9e6b
add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents:
478
diff
changeset
|
131 ; get = getSingleLinkedStack |
| 484 | 132 ; get2 = get2SingleLinkedStack |
|
503
413ce51da50b
separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
502
diff
changeset
|
133 } |
| 161 | 134 |
| 515 | 135 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a) |
|
509
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
136 createSingleLinkedStack = record { |
|
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
137 stack = emptySingleLinkedStack ; |
|
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
138 stackMethods = singleLinkedStackSpec |
|
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
139 } |
|
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
140 |
|
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
141 ---- |
|
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
142 -- |
|
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
143 -- proof of properties ( concrete cases ) |
|
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
144 -- |
| 156 | 145 |
| 499 | 146 test01 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Maybe a -> Bool {n} |
| 161 | 147 test01 stack _ with (top stack) |
| 148 ... | (Just _) = True | |
| 149 ... | Nothing = False | |
| 150 | |
| 156 | 151 |
| 496 | 152 test02 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Bool |
| 153 test02 stack = popSingleLinkedStack stack test01 | |
| 156 | 154 |
| 496 | 155 test03 : {n : Level } {a : Set n} -> a -> Bool |
| 165 | 156 test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02 |
| 156 | 157 |
| 499 | 158 -- after a push and a pop, the stack is empty |
| 159 lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False | |
| 160 lemma = refl | |
| 161 | |
| 501 | 162 testStack01 : {n m : Level } {a : Set n} -> a -> Bool {m} |
| 477 | 163 testStack01 v = pushStack createSingleLinkedStack v ( |
| 164 \s -> popStack s (\s1 d1 -> True)) | |
| 165 | |
| 500 | 166 -- after push 1 and 2, pop2 get 1 and 2 |
| 167 | |
| 515 | 168 testStack02 : {m : Level } -> ( Stack ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m} |
| 484 | 169 testStack02 cs = pushStack createSingleLinkedStack 1 ( |
| 170 \s -> pushStack s 2 cs) | |
| 477 | 171 |
| 485 | 172 |
| 499 | 173 testStack031 : (d1 d2 : ℕ ) -> Bool {Zero} |
| 500 | 174 testStack031 2 1 = True |
| 485 | 175 testStack031 _ _ = False |
| 176 | |
| 499 | 177 testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero} |
| 485 | 178 testStack032 (Just d1) (Just d2) = testStack031 d1 d2 |
| 179 testStack032 _ _ = False | |
| 484 | 180 |
| 515 | 181 testStack03 : {m : Level } -> Stack ℕ (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m} |
| 485 | 182 testStack03 s cs = pop2Stack s ( |
| 183 \s d1 d2 -> cs d1 d2 ) | |
| 484 | 184 |
| 485 | 185 testStack04 : Bool |
| 186 testStack04 = testStack02 (\s -> testStack03 s testStack032) | |
| 187 | |
| 500 | 188 testStack05 : testStack04 ≡ True |
| 189 testStack05 = refl | |
| 179 | 190 |
| 501 | 191 ------ |
|
503
413ce51da50b
separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
502
diff
changeset
|
192 -- |
|
509
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
193 -- proof of properties with indefinite state of stack |
|
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
194 -- |
|
503
413ce51da50b
separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
502
diff
changeset
|
195 -- this should be proved by properties of the stack inteface, not only by the implementation, |
|
413ce51da50b
separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
502
diff
changeset
|
196 -- and the implementation have to provides the properties. |
|
413ce51da50b
separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
502
diff
changeset
|
197 -- |
|
509
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
198 -- we cannot write "s ≡ s3", since level of the Set does not fit , but use stack s ≡ stack s3 is ok. |
|
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
199 -- anyway some implementations may result s != s3 |
| 504 | 200 -- |
|
509
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
201 |
| 515 | 202 stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t} ( SingleLinkedStack D ) |
|
509
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
203 stackInSomeState s = record { stack = s ; stackMethods = singleLinkedStackSpec } |
|
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
204 |
|
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
205 push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) -> |
|
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
206 pushStack ( stackInSomeState s ) x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) )) |
|
51f0d5e5d1e5
stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
504
diff
changeset
|
207 push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl } |
| 501 | 208 |
| 209 | |
| 496 | 210 id : {n : Level} {A : Set n} -> A -> A |
| 179 | 211 id a = a |
| 212 | |
| 499 | 213 -- push a, n times |
| 179 | 214 |
| 496 | 215 n-push : {n : Level} {A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A |
| 179 | 216 n-push zero s = s |
| 499 | 217 n-push {l} {A} {a} (suc n) s = pushSingleLinkedStack (n-push {l} {A} {a} n s) a (\s -> s ) |
| 179 | 218 |
| 499 | 219 n-pop : {n : Level}{A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A |
| 179 | 220 n-pop zero s = s |
| 499 | 221 n-pop {_} {A} {a} (suc n) s = popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s ) |
| 179 | 222 |
| 223 open ≡-Reasoning | |
| 224 | |
| 499 | 225 push-pop-equiv : {n : Level} {A : Set n} {a : A} (s : SingleLinkedStack A) -> (popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ) ≡ s |
| 179 | 226 push-pop-equiv s = refl |
| 227 | |
| 499 | 228 push-and-n-pop : {n : Level} {A : Set n} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ n-pop {_} {A} {a} n s |
| 179 | 229 push-and-n-pop zero s = refl |
| 496 | 230 push-and-n-pop {_} {A} {a} (suc n) s = begin |
| 499 | 231 n-pop {_} {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id) |
| 179 | 232 ≡⟨ refl ⟩ |
| 499 | 233 popSingleLinkedStack (n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s) |
| 234 ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s )) (push-and-n-pop n s) ⟩ | |
| 235 popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s) | |
| 179 | 236 ≡⟨ refl ⟩ |
| 499 | 237 n-pop {_} {A} {a} (suc n) s |
| 179 | 238 ∎ |
| 239 | |
| 240 | |
| 499 | 241 n-push-pop-equiv : {n : Level} {A : Set n} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> (n-pop {_} {A} {a} n (n-push {_} {A} {a} n s)) ≡ s |
| 179 | 242 n-push-pop-equiv zero s = refl |
| 499 | 243 n-push-pop-equiv {_} {A} {a} (suc n) s = begin |
| 244 n-pop {_} {A} {a} (suc n) (n-push (suc n) s) | |
| 179 | 245 ≡⟨ refl ⟩ |
| 499 | 246 n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s)) |
| 179 | 247 ≡⟨ push-and-n-pop n (n-push n s) ⟩ |
| 499 | 248 n-pop {_} {A} {a} n (n-push n s) |
| 180 | 249 ≡⟨ n-push-pop-equiv n s ⟩ |
| 499 | 250 s |
| 179 | 251 ∎ |
| 181 | 252 |
| 253 | |
| 496 | 254 n-push-pop-equiv-empty : {n : Level} {A : Set n} {a : A} -> (n : ℕ) -> n-pop {_} {A} {a} n (n-push {_} {A} {a} n emptySingleLinkedStack) ≡ emptySingleLinkedStack |
| 181 | 255 n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack |