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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
b8e606ab3a0b Trying define n-push...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
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
b8e606ab3a0b Trying define n-push...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
106 n-push : {A : Set} {a : A} -> CodeSegment (ℕ × SingleLinkedStack A) (ℕ × SingleLinkedStack A)
b8e606ab3a0b Trying define n-push...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
107 n-push {A} {a} = cs (push {A} {a})
b8e606ab3a0b Trying define n-push...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
108 where
b8e606ab3a0b Trying define n-push...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
109 push : {A : Set} {a : A} -> (ℕ × SingleLinkedStack A) -> (ℕ × SingleLinkedStack A)
b8e606ab3a0b Trying define n-push...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
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