Mercurial > hg > Members > atton > agda-proofs
annotate cbc/stack-product.agda @ 54:fa95e3070138
Define SingleLinkedStack using subtype
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 11 Jan 2017 10:56:13 +0000 |
parents | b8e606ab3a0b |
children | bd428bd6b394 |
rev | line source |
---|---|
27
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 module stack-product where |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open import product |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 open import Data.Product |
29 | 5 open import Data.Nat |
28
67978ba63a6f
Rewrite cs composition style
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
6 open import Function using (id) |
27
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import Relation.Binary.PropositionalEquality |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 -- definition based from Gears(209:5708390a9d88) src/parallel_execution |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 goto = executeCS |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 data Bool : Set where |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 True : Bool |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 False : Bool |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 data Maybe (a : Set) : Set where |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 Nothing : Maybe a |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 Just : a -> Maybe a |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 record Stack {a t : Set} (stackImpl : Set) : Set where |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 field |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 stack : stackImpl |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 push : CodeSegment (stackImpl × a × (CodeSegment stackImpl t)) t |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 pop : CodeSegment (stackImpl × (CodeSegment (stackImpl × Maybe a) t)) t |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 data Element (a : Set) : Set where |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 cons : a -> Maybe (Element a) -> Element a |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 datum : {a : Set} -> Element a -> a |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 datum (cons a _) = a |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 next : {a : Set} -> Element a -> Maybe (Element a) |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 next (cons _ n) = n |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 record SingleLinkedStack (a : Set) : Set where |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 field |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 top : Maybe (Element a) |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 open SingleLinkedStack |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 emptySingleLinkedStack = record {top = Nothing} |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 pushSingleLinkedStack : {a t : Set} -> CodeSegment ((SingleLinkedStack a) × a × (CodeSegment (SingleLinkedStack a) t)) t |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 pushSingleLinkedStack = cs push |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 where |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 push : {a t : Set} -> ((SingleLinkedStack a) × a × (CodeSegment (SingleLinkedStack a) t)) -> t |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 push (stack , datum , next) = goto next stack1 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 where |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 element = cons datum (top stack) |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 stack1 = record {top = Just element} |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 popSingleLinkedStack : {a t : Set} -> CodeSegment (SingleLinkedStack a × (CodeSegment (SingleLinkedStack a × Maybe a) t)) t |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 popSingleLinkedStack = cs pop |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
59 where |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 pop : {a t : Set} -> (SingleLinkedStack a × (CodeSegment (SingleLinkedStack a × Maybe a) t)) -> t |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 pop (record { top = Nothing } , nextCS) = goto nextCS (emptySingleLinkedStack , Nothing) |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
62 pop (record { top = Just x } , nextCS) = goto nextCS (stack1 , (Just datum1)) |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 where |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 datum1 = datum x |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
65 stack1 = record { top = (next x) } |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
68 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
69 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
70 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
71 createSingleLinkedStack : {a b : Set} -> Stack {a} {b} (SingleLinkedStack a) |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
72 createSingleLinkedStack = record { stack = emptySingleLinkedStack |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
73 ; push = pushSingleLinkedStack |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
74 ; pop = popSingleLinkedStack |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
75 } |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
76 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
77 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
78 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
79 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
80 test01 : {a : Set} -> CodeSegment (SingleLinkedStack a × Maybe a) Bool |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
81 test01 = cs test01' |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
82 where |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
83 test01' : {a : Set} -> (SingleLinkedStack a × Maybe a) -> Bool |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
84 test01' (record { top = Nothing } , _) = False |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
85 test01' (record { top = Just x } , _) = True |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
86 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
87 |
28
67978ba63a6f
Rewrite cs composition style
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
88 test02 : {a : Set} -> CodeSegment (SingleLinkedStack a) (SingleLinkedStack a × Maybe a) |
27
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
89 test02 = cs test02' |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
90 where |
28
67978ba63a6f
Rewrite cs composition style
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
91 test02' : {a : Set} -> SingleLinkedStack a -> (SingleLinkedStack a × Maybe a) |
67978ba63a6f
Rewrite cs composition style
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
92 test02' stack = goto popSingleLinkedStack (stack , (cs id)) |
27
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
93 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
94 |
28
67978ba63a6f
Rewrite cs composition style
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
95 test03 : {a : Set} -> CodeSegment a (SingleLinkedStack a) |
27
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
96 test03 = cs test03' |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
97 where |
28
67978ba63a6f
Rewrite cs composition style
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
98 test03' : {a : Set} -> a -> SingleLinkedStack a |
67978ba63a6f
Rewrite cs composition style
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
99 test03' a = goto pushSingleLinkedStack (emptySingleLinkedStack , a , (cs id)) |
27
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
100 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
101 |
28
67978ba63a6f
Rewrite cs composition style
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
102 lemma : {A : Set} {a : A} -> goto (test03 ◎ test02 ◎ test01) a ≡ False |
27
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
103 lemma = refl |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
104 |
28
67978ba63a6f
Rewrite cs composition style
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
105 |
29 | 106 n-push : {A : Set} {a : A} -> CodeSegment (ℕ × SingleLinkedStack A) (ℕ × SingleLinkedStack A) |
107 n-push {A} {a} = cs (push {A} {a}) | |
108 where | |
109 push : {A : Set} {a : A} -> (ℕ × SingleLinkedStack A) -> (ℕ × SingleLinkedStack A) | |
110 push {A} {a} (zero , s) = (zero , s) | |
54
fa95e3070138
Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
29
diff
changeset
|
111 push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , ? {- n-push -}) -- needs subtype |
27
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
112 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
113 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
114 {- |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
115 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
116 n-push : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
117 n-push zero s = s |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
118 n-push {A} {a} (suc n) s = pushSingleLinkedStack (n-push {A} {a} n s) a (\s -> s) |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
119 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
120 n-pop : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
121 n-pop zero s = s |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
122 n-pop {A} {a} (suc n) s = popSingleLinkedStack (n-pop {A} {a} n s) (\s _ -> s) |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
123 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
124 open ≡-Reasoning |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
125 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
126 push-pop-equiv : {A : Set} {a : A} (s : SingleLinkedStack A) -> popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ≡ s |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
127 push-pop-equiv s = refl |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
128 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
129 push-and-n-pop : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> n-pop {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ n-pop {A} {a} n s |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
130 push-and-n-pop zero s = refl |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
131 push-and-n-pop {A} {a} (suc n) s = begin |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
132 n-pop (suc (suc n)) (pushSingleLinkedStack s a id) |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
133 ≡⟨ refl ⟩ |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
134 popSingleLinkedStack (n-pop (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s) |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
135 ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s)) (push-and-n-pop n s) ⟩ |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
136 popSingleLinkedStack (n-pop n s) (\s _ -> s) |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
137 ≡⟨ refl ⟩ |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
138 n-pop (suc n) s |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
139 ∎ |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
140 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
141 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
142 n-push-pop-equiv : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> (n-pop {A} {a} n (n-push {A} {a} n s)) ≡ s |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
143 n-push-pop-equiv zero s = refl |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
144 n-push-pop-equiv {A} {a} (suc n) s = begin |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
145 n-pop (suc n) (n-push (suc n) s) |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
146 ≡⟨ refl ⟩ |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
147 n-pop (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s)) |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
148 ≡⟨ push-and-n-pop n (n-push n s) ⟩ |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
149 n-pop n (n-push n s) |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
150 ≡⟨ n-push-pop-equiv n s ⟩ |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
151 s |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
152 ∎ |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
153 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
154 |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
155 n-push-pop-equiv-empty : {A : Set} {a : A} -> (n : Nat) -> n-pop {A} {a} n (n-push {A} {a} n emptySingleLinkedStack) ≡ emptySingleLinkedStack |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
156 n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
157 -} |
892f8b3aa57e
ReWrite stack.agda using product type definition
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
158 |