Mercurial > hg > Papers > 2020 > ryokka-master

comparison paper/src/stackTest.agda @ 2:c7acb9211784

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add code, figure. and paper fix content
author ryokka
date Mon, 27 Jan 2020 20:41:36 +0900
parents
children
comparison
equal deleted inserted replaced
1:ee44dbda6bd3 2:c7acb9211784
1 open import Level renaming (suc to succ ; zero to Zero )
2 module stackTest where
3
4 open import stack
5
6 open import Relation.Binary.PropositionalEquality
7 open import Relation.Binary.Core
8 open import Data.Nat
9 open import Function
10
11
12 open SingleLinkedStack
13 open Stack
14
15 ----
16 --
17 -- proof of properties ( concrete cases )
18 --
19
20 test01 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Maybe a -> Bool {n}
21 test01 stack _ with (top stack)
22 ... | (Just _) = True
23 ... | Nothing = False
24
25
26 test02 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Bool
27 test02 stack = popSingleLinkedStack stack test01
28
29 test03 : {n : Level } {a : Set n} -> a -> Bool
30 test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02
31
32 -- after a push and a pop, the stack is empty
33 lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False
34 lemma = refl
35
36 testStack01 : {n m : Level } {a : Set n} -> a -> Bool {m}
37 testStack01 v = pushStack createSingleLinkedStack v (
38 \s -> popStack s (\s1 d1 -> True))
39
40 -- after push 1 and 2, pop2 get 1 and 2
41
42 testStack02 : {m : Level } -> ( Stack ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m}
43 testStack02 cs = pushStack createSingleLinkedStack 1 (
44 \s -> pushStack s 2 cs)
45
46
47 testStack031 : (d1 d2 : ℕ ) -> Bool {Zero}
48 testStack031 2 1 = True
49 testStack031 _ _ = False
50
51 testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero}
52 testStack032 (Just d1) (Just d2) = testStack031 d1 d2
53 testStack032 _ _ = False
54
55 testStack03 : {m : Level } -> Stack ℕ (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m}
56 testStack03 s cs = pop2Stack s (
57 \s d1 d2 -> cs d1 d2 )
58
59 testStack04 : Bool
60 testStack04 = testStack02 (\s -> testStack03 s testStack032)
61
62 testStack05 : testStack04 ≡ True
63 testStack05 = refl
64
65 testStack06 : {m : Level } -> Maybe (Element ℕ)
66 testStack06 = pushStack createSingleLinkedStack 1 (
67 \s -> pushStack s 2 (\s -> top (stack s)))
68
69 testStack07 : {m : Level } -> Maybe (Element ℕ)
70 testStack07 = pushSingleLinkedStack emptySingleLinkedStack 1 (
71 \s -> pushSingleLinkedStack s 2 (\s -> top s))
72
73 testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1
74 $ \s -> pushSingleLinkedStack s 2
75 $ \s -> pushSingleLinkedStack s 3
76 $ \s -> pushSingleLinkedStack s 4
77 $ \s -> pushSingleLinkedStack s 5
78 $ \s -> top s
79
80 ------
81 --
82 -- proof of properties with indefinite state of stack
83 --
84 -- this should be proved by properties of the stack inteface, not only by the implementation,
85 -- and the implementation have to provides the properties.
86 --
87 -- we cannot write "s ≡ s3", since level of the Set does not fit , but use stack s ≡ stack s3 is ok.
88 -- anyway some implementations may result s != s3
89 --
90
91 stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t} ( SingleLinkedStack D )
92 stackInSomeState s = record { stack = s ; stackMethods = singleLinkedStackSpec }
93
94 push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
95 pushStack ( stackInSomeState s ) x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
96 push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
97
98
99 -- id : {n : Level} {A : Set n} -> A -> A
100 -- id a = a
101
102 -- push a, n times
103
104 n-push : {n : Level} {A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
105 n-push zero s = s
106 n-push {l} {A} {a} (suc n) s = pushSingleLinkedStack (n-push {l} {A} {a} n s) a (\s -> s )
107
108 n-pop : {n : Level}{A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
109 n-pop zero s = s
110 n-pop {_} {A} {a} (suc n) s = popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s )
111
112 open ≡-Reasoning
113
114 push-pop-equiv : {n : Level} {A : Set n} {a : A} (s : SingleLinkedStack A) -> (popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ) ≡ s
115 push-pop-equiv s = refl
116
117 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
118 push-and-n-pop zero s = refl
119 push-and-n-pop {_} {A} {a} (suc n) s = begin
120 n-pop {_} {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id)
121 ≡⟨ refl ⟩
122 popSingleLinkedStack (n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s)
123 ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s )) (push-and-n-pop n s) ⟩
124 popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s)
125 ≡⟨ refl ⟩
126 n-pop {_} {A} {a} (suc n) s
127 ∎
128
129
130 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
131 n-push-pop-equiv zero s = refl
132 n-push-pop-equiv {_} {A} {a} (suc n) s = begin
133 n-pop {_} {A} {a} (suc n) (n-push (suc n) s)
134 ≡⟨ refl ⟩
135 n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s))
136 ≡⟨ push-and-n-pop n (n-push n s) ⟩
137 n-pop {_} {A} {a} n (n-push n s)
138 ≡⟨ n-push-pop-equiv n s ⟩
139 s
140 ∎
141
142
143 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
144 n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack