Mercurial > hg > Gears > GearsAgda

annotate src/parallel_execution/stack.agda @ 504:0bec9490c199

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
stack.agda comment
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 01 Jan 2018 19:17:01 +0900
parents 413ce51da50b
children 51f0d5e5d1e5
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
1 open import Level renaming (suc to succ ; zero to Zero )
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
2 module stack where
154
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
3
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
4 open import Relation.Binary.PropositionalEquality
477
c3202635c20a fix Stack.agda
ryokka
parents: 427
diff changeset
5 open import Relation.Binary.Core
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
6 open import Data.Nat
478
0223c07c3946 fix stack.agda
ryokka
parents: 477
diff changeset
7
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
8 ex : 1 + 2 ≡ 3
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
9 ex = refl
179
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
10
501
55077dd40a51 stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
11 data Bool {n : Level } : Set n where
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
12 True : Bool
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
13 False : Bool
164
b0c6e0392b00 Add comment to stack.agda
atton
parents: 161
diff changeset
14
501
55077dd40a51 stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
15 record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
485
a7548f01f013 proof pop2 function in agda
ryokka
parents: 484
diff changeset
16 field
a7548f01f013 proof pop2 function in agda
ryokka
parents: 484
diff changeset
17 pi1 : a
a7548f01f013 proof pop2 function in agda
ryokka
parents: 484
diff changeset
18 pi2 : b
477
c3202635c20a fix Stack.agda
ryokka
parents: 427
diff changeset
19
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
20 data Maybe {n : Level } (a : Set n) : Set n where
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
21 Nothing : Maybe a
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
22 Just : a -> Maybe a
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
23
503
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
24 record StackMethods {n m : Level } {a : Set n } {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
25 field
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
26 push : stackImpl -> a -> (stackImpl -> t) -> t
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
27 pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
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
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
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
07ccd411ad70 fix interface in agda
ryokka
parents: 181
diff changeset
32
503
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
33 record Stack {n m : Level } {a : Set n } {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
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
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
36 stackMethods : StackMethods {n} {m} {a} {t} si
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
37 pushStack : a -> (Stack si -> t) -> t
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 } ))
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
39 popStack : (Stack si -> Maybe a -> t) -> t
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 )
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
41 pop2Stack : (Stack si -> Maybe a -> Maybe a -> t) -> t
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)
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
43 getStack : (Stack si -> Maybe a -> t) -> t
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 )
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
45 get2Stack : (Stack si -> Maybe a -> Maybe a -> t) -> t
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
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
47
503
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
48 open Stack
427
07ccd411ad70 fix interface in agda
ryokka
parents: 181
diff changeset
49
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
50 data Element {n : Level } (a : Set n) : Set n where
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
51 cons : a -> Maybe (Element a) -> Element a
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
52
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
53 datum : {n : Level } {a : Set n} -> Element a -> a
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
54 datum (cons a _) = a
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
55
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
56 next : {n : Level } {a : Set n} -> Element a -> Maybe (Element a)
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
57 next (cons _ n) = n
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
58
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
59
164
b0c6e0392b00 Add comment to stack.agda
atton
parents: 161
diff changeset
60 {-
b0c6e0392b00 Add comment to stack.agda
atton
parents: 161
diff changeset
61 -- cannot define recrusive record definition. so use linked list with maybe.
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
62 record Element {l : Level} (a : Set n l) : Set n (suc l) where
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
63 field
164
b0c6e0392b00 Add comment to stack.agda
atton
parents: 161
diff changeset
64 datum : a -- `data` is reserved by Agda.
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
65 next : Maybe (Element a)
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
66 -}
155
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
67
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
68
164
b0c6e0392b00 Add comment to stack.agda
atton
parents: 161
diff changeset
69
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
70 record SingleLinkedStack {n : Level } (a : Set n) : Set n where
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
71 field
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
72 top : Maybe (Element a)
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
73 open SingleLinkedStack
155
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
74
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
75 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
76 pushSingleLinkedStack stack datum next = next stack1
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
77 where
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
78 element = cons datum (top stack)
164
b0c6e0392b00 Add comment to stack.agda
atton
parents: 161
diff changeset
79 stack1 = record {top = Just element}
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
80
155
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
81
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
82 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
83 popSingleLinkedStack stack cs with (top stack)
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
84 ... | Nothing = cs stack Nothing
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
85 ... | Just d = cs stack1 (Just data1)
154
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
86 where
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
87 data1 = datum d
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
88 stack1 = record { top = (next d) }
154
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
89
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
90 pop2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
91 pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
92 ... | Nothing = cs stack Nothing Nothing
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
93 ... | Just d = pop2SingleLinkedStack' {n} {m} stack cs
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
94 where
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
95 pop2SingleLinkedStack' : {n m : Level } {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
96 pop2SingleLinkedStack' stack cs with (next d)
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
97 ... | Nothing = cs stack Nothing Nothing
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
98 ... | Just d1 = cs (record {top = (next d)}) (Just (datum d)) (Just (datum d1))
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
99
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
100
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
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
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
108 get2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
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
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
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
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
113 get2SingleLinkedStack' : {n m : Level} {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
114 get2SingleLinkedStack' stack cs with (next d)
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
115 ... | Nothing = cs stack Nothing Nothing
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
116 ... | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
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
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
120 emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
121 emptySingleLinkedStack = record {top = Nothing}
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
122
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
123 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} {a} {t} (SingleLinkedStack a)
503
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
124 createSingleLinkedStack = record {
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
125 stack = emptySingleLinkedStack ;
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
126 stackMethods = record {
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
127 push = pushSingleLinkedStack
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
128 ; pop = popSingleLinkedStack
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
129 ; pop2 = pop2SingleLinkedStack
483
9098ec0a9e6b add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents: 478
diff changeset
130 ; get = getSingleLinkedStack
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
131 ; get2 = get2SingleLinkedStack
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
132 }
503
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
133 }
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
134
156
0aa2265660a0 Add stack lemma
atton
parents: 155
diff changeset
135
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
136 test01 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Maybe a -> Bool {n}
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
137 test01 stack _ with (top stack)
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
138 ... | (Just _) = True
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
139 ... | Nothing = False
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
140
156
0aa2265660a0 Add stack lemma
atton
parents: 155
diff changeset
141
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
142 test02 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Bool
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
143 test02 stack = popSingleLinkedStack stack test01
156
0aa2265660a0 Add stack lemma
atton
parents: 155
diff changeset
144
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
145 test03 : {n : Level } {a : Set n} -> a -> Bool
165
bf26f1105862 Generalize lemma
atton
parents: 164
diff changeset
146 test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02
156
0aa2265660a0 Add stack lemma
atton
parents: 155
diff changeset
147
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
148 -- after a push and a pop, the stack is empty
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
149 lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
150 lemma = refl
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
151
501
55077dd40a51 stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
152 testStack01 : {n m : Level } {a : Set n} -> a -> Bool {m}
477
c3202635c20a fix Stack.agda
ryokka
parents: 427
diff changeset
153 testStack01 v = pushStack createSingleLinkedStack v (
c3202635c20a fix Stack.agda
ryokka
parents: 427
diff changeset
154 \s -> popStack s (\s1 d1 -> True))
c3202635c20a fix Stack.agda
ryokka
parents: 427
diff changeset
155
500
6d984ea42fd2 fix proof
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
156 -- after push 1 and 2, pop2 get 1 and 2
6d984ea42fd2 fix proof
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
157
501
55077dd40a51 stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
158 testStack02 : {m : Level } -> ( Stack (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m}
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
159 testStack02 cs = pushStack createSingleLinkedStack 1 (
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
160 \s -> pushStack s 2 cs)
477
c3202635c20a fix Stack.agda
ryokka
parents: 427
diff changeset
161
485
a7548f01f013 proof pop2 function in agda
ryokka
parents: 484
diff changeset
162
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
163 testStack031 : (d1 d2 : ℕ ) -> Bool {Zero}
500
6d984ea42fd2 fix proof
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
164 testStack031 2 1 = True
485
a7548f01f013 proof pop2 function in agda
ryokka
parents: 484
diff changeset
165 testStack031 _ _ = False
a7548f01f013 proof pop2 function in agda
ryokka
parents: 484
diff changeset
166
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
167 testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero}
485
a7548f01f013 proof pop2 function in agda
ryokka
parents: 484
diff changeset
168 testStack032 (Just d1) (Just d2) = testStack031 d1 d2
a7548f01f013 proof pop2 function in agda
ryokka
parents: 484
diff changeset
169 testStack032 _ _ = False
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
170
501
55077dd40a51 stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
171 testStack03 : {m : Level } -> Stack (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m}
485
a7548f01f013 proof pop2 function in agda
ryokka
parents: 484
diff changeset
172 testStack03 s cs = pop2Stack s (
a7548f01f013 proof pop2 function in agda
ryokka
parents: 484
diff changeset
173 \s d1 d2 -> cs d1 d2 )
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
174
485
a7548f01f013 proof pop2 function in agda
ryokka
parents: 484
diff changeset
175 testStack04 : Bool
a7548f01f013 proof pop2 function in agda
ryokka
parents: 484
diff changeset
176 testStack04 = testStack02 (\s -> testStack03 s testStack032)
a7548f01f013 proof pop2 function in agda
ryokka
parents: 484
diff changeset
177
500
6d984ea42fd2 fix proof
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
178 testStack05 : testStack04 ≡ True
6d984ea42fd2 fix proof
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 499
diff changeset
179 testStack05 = refl
179
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
180
501
55077dd40a51 stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
181 ------
503
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
182 --
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
183 -- 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
184 -- 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
185 --
504
0bec9490c199 stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 503
diff changeset
186 -- we cannot write "s ≡ s3", since level of the Set does not fit , but we cant use stack s ≡ stack s3
0bec9490c199 stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 503
diff changeset
187 --
501
55077dd40a51 stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
188 -- push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : Stack (SingleLinkedStack D) ) ->
502
8d997f0c9b2c stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
189 -- pushStack s x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> ((stack s ≡ stack s3 ) ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))))
501
55077dd40a51 stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
190 -- push->push->pop2 {l} {D} x y s = {!!}
502
8d997f0c9b2c stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
191 -- where
8d997f0c9b2c stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
192 -- t0 : (s3 : Stack {_} {succ l} {D} {Set l} (SingleLinkedStack D)) (x1 y1 : Maybe D) -> (stack s ≡ stack s3 ) -> (Just x ≡ x1 ) -> (Just y ≡ y1 )
8d997f0c9b2c stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
193 -- -> ((stack s ≡ stack s3 ) ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ))
8d997f0c9b2c stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
194 -- t0 s3 x1 y1 refl refl refl = record { pi1 = refl ; pi2 = record { pi1 = refl ; pi2 = refl } }
8d997f0c9b2c stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
195 -- t1 : (s2 : Stack (SingleLinkedStack D)) -> pop2Stack s2 ( \s3 y1 x1 -> ((stack s ≡ stack s3 ) ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
8d997f0c9b2c stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
196 -- t1 s2 = {!!}
8d997f0c9b2c stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
197 -- t2 : (s1 : Stack (SingleLinkedStack D)) (x1 y1 : Maybe D) ->
8d997f0c9b2c stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
198 -- pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> ((stack s ≡ stack s3 ) ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ) ))
8d997f0c9b2c stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
199 -- t2 s1 = {!!}
501
55077dd40a51 stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
200
55077dd40a51 stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
201
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
202 id : {n : Level} {A : Set n} -> A -> A
179
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
203 id a = a
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
204
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
205 -- push a, n times
179
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
206
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
207 n-push : {n : Level} {A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
179
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
208 n-push zero s = s
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
209 n-push {l} {A} {a} (suc n) s = pushSingleLinkedStack (n-push {l} {A} {a} n s) a (\s -> s )
179
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
210
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
211 n-pop : {n : Level}{A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
179
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
212 n-pop zero s = s
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
213 n-pop {_} {A} {a} (suc n) s = popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s )
179
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
214
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
215 open ≡-Reasoning
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
216
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
217 push-pop-equiv : {n : Level} {A : Set n} {a : A} (s : SingleLinkedStack A) -> (popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ) ≡ s
179
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
218 push-pop-equiv s = refl
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
219
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
220 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
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
221 push-and-n-pop zero s = refl
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
222 push-and-n-pop {_} {A} {a} (suc n) s = begin
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
223 n-pop {_} {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id)
179
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
224 ≡⟨ refl ⟩
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
225 popSingleLinkedStack (n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s)
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
226 ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s )) (push-and-n-pop n s) ⟩
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
227 popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s)
179
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
228 ≡⟨ refl ⟩
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
229 n-pop {_} {A} {a} (suc n) s
179
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
230 ∎
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
231
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
232
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
233 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
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
234 n-push-pop-equiv zero s = refl
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
235 n-push-pop-equiv {_} {A} {a} (suc n) s = begin
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
236 n-pop {_} {A} {a} (suc n) (n-push (suc n) s)
179
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
237 ≡⟨ refl ⟩
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
238 n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s))
179
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
239 ≡⟨ push-and-n-pop n (n-push n s) ⟩
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
240 n-pop {_} {A} {a} n (n-push n s)
180
d8947747ff3b Fix syntax
atton
parents: 179
diff changeset
241 ≡⟨ n-push-pop-equiv n s ⟩
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
242 s
179
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
243 ∎
181
78b28c8ffff2 Prove equivalence n-push/n-pop to empty stack
atton
parents: 180
diff changeset
244
78b28c8ffff2 Prove equivalence n-push/n-pop to empty stack
atton
parents: 180
diff changeset
245
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
246 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
78b28c8ffff2 Prove equivalence n-push/n-pop to empty stack
atton
parents: 180
diff changeset
247 n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack