Mercurial > hg > Members > Moririn
annotate redBlackTreeTest.agda @ 563:8634f448e699
minor fix
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 30 Mar 2018 11:09:06 +0900 |
parents | 9df8103bc493 |
children | 40ab3d39e49d |
rev | line source |
---|---|
537 | 1 module redBlackTreeTest where |
2 | |
3 open import RedBlackTree | |
4 open import stack | |
554
988c12d7f887
use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
553
diff
changeset
|
5 open import Level hiding (zero) renaming ( suc to succ ) |
537 | 6 |
553 | 7 open import Data.Empty |
8 | |
537 | 9 open import Data.Nat |
553 | 10 open import Relation.Nullary |
537 | 11 |
12 open Tree | |
13 open Node | |
14 open RedBlackTree.RedBlackTree | |
15 open Stack | |
16 | |
17 -- tests | |
18 | |
562 | 19 putTree1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → k → a → (RedBlackTree {n} {m} {t} a k → t) → t |
543 | 20 putTree1 {n} {m} {a} {k} {t} tree k1 value next with (root tree) |
537 | 21 ... | Nothing = next (record tree {root = Just (leafNode k1 value) }) |
562 | 22 ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (λ s → findNode tree s (leafNode k1 value) n2 (λ tree1 s n1 → replaceNode tree1 s n1 next)) |
537 | 23 |
24 open import Relation.Binary.PropositionalEquality | |
25 open import Relation.Binary.Core | |
26 open import Function | |
27 | |
28 | |
562 | 29 check1 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool {m} |
537 | 30 check1 Nothing _ = False |
31 check1 (Just n) x with Data.Nat.compare (value n) x | |
32 ... | equal _ = True | |
33 ... | _ = False | |
34 | |
562 | 35 check2 : {m : Level } (n : Maybe (Node ℕ ℕ)) → ℕ → Bool {m} |
549 | 36 check2 Nothing _ = False |
37 check2 (Just n) x with compare2 (value n) x | |
38 ... | EQ = True | |
39 ... | _ = False | |
40 | |
562 | 41 test1 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 x 1 ≡ True )) |
537 | 42 test1 = refl |
43 | |
44 test2 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( | |
562 | 45 λ t → putTree1 t 2 2 ( |
46 λ t → getRedBlackTree t 1 ( | |
47 λ t x → check2 x 1 ≡ True ))) | |
537 | 48 test2 = refl |
49 | |
545 | 50 open ≡-Reasoning |
542 | 51 test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 |
562 | 52 $ λ t → putTree1 t 2 2 |
53 $ λ t → putTree1 t 3 3 | |
54 $ λ t → putTree1 t 4 4 | |
55 $ λ t → getRedBlackTree t 1 | |
56 $ λ t x → check2 x 1 ≡ True | |
545 | 57 test3 = begin |
549 | 58 check2 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1 |
545 | 59 ≡⟨ refl ⟩ |
60 True | |
61 ∎ | |
542 | 62 |
63 test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 | |
562 | 64 $ λ t → putTree1 t 2 2 |
65 $ λ t → putTree1 t 3 3 | |
66 $ λ t → putTree1 t 4 4 | |
67 $ λ t → getRedBlackTree t 4 | |
68 $ λ t x → x | |
538
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
69 |
540 | 70 -- test5 : Maybe (Node ℕ ℕ) |
541 | 71 test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4 |
562 | 72 $ λ t → putTree1 t 6 6 |
73 $ λ t0 → clearSingleLinkedStack (nodeStack t0) | |
74 $ λ s → findNode1 t0 s (leafNode 3 3) ( root t0 ) | |
75 $ λ t1 s n1 → replaceNode t1 s n1 | |
76 $ λ t → getRedBlackTree t 3 | |
77 -- $ λ t x → SingleLinkedStack.top (stack s) | |
78 -- $ λ t x → n1 | |
79 $ λ t x → root t | |
540 | 80 where |
562 | 81 findNode1 : {n m : Level } {a k : Set n} {t : Set m} → RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → (Node a k) → (Maybe (Node a k)) → (RedBlackTree {n} {m} {t} a k → SingleLinkedStack (Node a k) → Node a k → t) → t |
540 | 82 findNode1 t s n1 Nothing next = next t s n1 |
83 findNode1 t s n1 ( Just n2 ) next = findNode t s n1 n2 next | |
538
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
84 |
562 | 85 -- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ λ t → |
86 -- putTree1 t 2 2 $ λ t → putTree1 t 3 3 $ λ t → root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} ) | |
538
5c001e8ba0d5
add redBlackTreeTest.agda test5,test51. but not work
ryokka
parents:
537
diff
changeset
|
87 -- test51 = refl |
539 | 88 |
89 test6 : Maybe (Node ℕ ℕ) | |
90 test6 = root (createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}) | |
91 | |
92 | |
93 test7 : Maybe (Node ℕ ℕ) | |
562 | 94 test7 = clearSingleLinkedStack (nodeStack tree2) (λ s → replaceNode tree2 s n2 (λ t → root t)) |
539 | 95 where |
96 tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)} | |
97 k1 = 1 | |
98 n2 = leafNode 0 0 | |
99 value1 = 1 | |
100 | |
101 test8 : Maybe (Node ℕ ℕ) | |
102 test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 | |
562 | 103 $ λ t → putTree1 t 2 2 (λ t → root t) |
544 | 104 |
105 | |
562 | 106 test9 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( λ t → getRedBlackTree t 1 ( λ t x → check2 x 1 ≡ True )) |
544 | 107 test9 = refl |
108 | |
109 test10 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( | |
562 | 110 λ t → putRedBlackTree t 2 2 ( |
111 λ t → getRedBlackTree t 1 ( | |
112 λ t x → check2 x 1 ≡ True ))) | |
544 | 113 test10 = refl |
114 | |
115 test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 | |
562 | 116 $ λ t → putRedBlackTree t 2 2 |
117 $ λ t → putRedBlackTree t 3 3 | |
118 $ λ t → getRedBlackTree t 2 | |
119 $ λ t x → root t | |
545 | 120 |
121 | |
562 | 122 redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} → RedBlackTree {Level.zero} {m} {t} a ℕ |
549 | 123 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 } |
545 | 124 |
562 | 125 -- compare2 : (x y : ℕ ) → CompareResult {Level.zero} |
549 | 126 -- compare2 zero zero = EQ |
127 -- compare2 (suc _) zero = GT | |
128 -- compare2 zero (suc _) = LT | |
129 -- compare2 (suc x) (suc y) = compare2 x y | |
546 | 130 |
562 | 131 contraposition : {m : Level } {A B : Set m} → (B → A) → (¬ A → ¬ B) |
132 contraposition f = λ x y → x (f y) | |
133 | |
134 compareTri1 : (n : ℕ) → zero <′ suc n | |
554
988c12d7f887
use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
553
diff
changeset
|
135 compareTri1 zero = ≤′-refl |
988c12d7f887
use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
553
diff
changeset
|
136 compareTri1 (suc n) = ≤′-step ( compareTri1 n ) |
553 | 137 |
562 | 138 compareTri2 : (n m : ℕ) → n ≤′ m → suc n ≤′ suc m |
554
988c12d7f887
use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
553
diff
changeset
|
139 compareTri2 _ _ ≤′-refl = ≤′-refl |
556 | 140 compareTri2 n (suc m) ( ≤′-step p ) = ≤′-step { suc n } ( compareTri2 n m p ) |
141 | |
558 | 142 <′dec : Set |
143 <′dec = ∀ m n → Dec ( m ≤′ n ) | |
562 | 144 |
145 compareTri6 : ∀ m {n} → ¬ m ≤′ n → ¬ suc m ≤′ suc n | |
146 | |
558 | 147 is≤′ : <′dec |
148 is≤′ zero zero = yes ≤′-refl | |
562 | 149 is≤′ zero (suc n) = yes (lemma n) |
150 where | |
151 lemma : (n : ℕ) → zero ≤′ suc n | |
152 lemma zero = ≤′-step ≤′-refl | |
153 lemma (suc n) = ≤′-step (lemma n) | |
154 is≤′ (suc m) (zero) = no ( λ () ) | |
558 | 155 is≤′ (suc m) (suc n) with is≤′ m n |
562 | 156 ... | yes p = yes ( compareTri2 _ _ p ) |
157 ... | no p = no ( compareTri6 _ p ) | |
557 | 158 |
562 | 159 compareTri20 : {n : ℕ} → ¬ suc n ≤′ zero |
561
1bbbd787472e
trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
560
diff
changeset
|
160 compareTri20 () |
1bbbd787472e
trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
560
diff
changeset
|
161 |
559 | 162 |
562 | 163 compareTri21 : (n m : ℕ) → suc n ≤′ suc m → n ≤′ m |
559 | 164 compareTri21 _ _ ≤′-refl = ≤′-refl |
561
1bbbd787472e
trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
560
diff
changeset
|
165 compareTri21 (suc n) zero ( ≤′-step p ) = compareTri23 (suc n) ( ≤′-step p ) p |
1bbbd787472e
trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
560
diff
changeset
|
166 where |
562 | 167 compareTri23 : (n : ℕ) → suc n ≤′ suc zero → suc n ≤′ zero → n ≤′ zero |
561
1bbbd787472e
trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
560
diff
changeset
|
168 compareTri23 zero ( ≤′-step p ) _ = ≤′-refl |
1bbbd787472e
trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
560
diff
changeset
|
169 compareTri23 zero ≤′-refl _ = ≤′-refl |
1bbbd787472e
trichotomos on ≤′ done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
560
diff
changeset
|
170 compareTri23 (suc n1) ( ≤′-step p ) () |
559 | 171 compareTri21 n (suc m) ( ≤′-step p ) = ≤′-step (compareTri21 _ _ p) |
560 | 172 compareTri21 zero zero ( ≤′-step p ) = ≤′-refl |
173 | |
559 | 174 |
175 compareTri3 : ∀ m {n} → ¬ m ≡ suc (m + n) | |
176 compareTri3 zero () | |
177 compareTri3 (suc m) eq = compareTri3 m (cong pred eq) | |
178 | |
563 | 179 compareTri4' : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m |
180 compareTri4' m {n} with n ≟ m | |
559 | 181 ... | yes refl = λ x y → x refl |
182 ... | no p = λ x y → p ( cong pred y ) | |
183 | |
563 | 184 compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m |
185 compareTri4 m = contraposition ( λ x → cong pred x ) | |
186 | |
562 | 187 -- compareTri6 : ∀ m {n} → ¬ m ≤′ n → ¬ suc m ≤′ suc n |
559 | 188 compareTri6 m {n} = λ x y → x (compareTri21 _ _ y) |
189 | |
560 | 190 compareTri5 : ∀ m {n} → ¬ m <′ n → ¬ suc m <′ suc n |
191 compareTri5 m {n} = compareTri6 (suc m) | |
192 | |
554
988c12d7f887
use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
553
diff
changeset
|
193 compareTri : Trichotomous _≡_ _<′_ |
988c12d7f887
use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
553
diff
changeset
|
194 compareTri zero zero = tri≈ ( λ ()) refl ( λ ()) |
988c12d7f887
use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
553
diff
changeset
|
195 compareTri zero (suc n) = tri< ( compareTri1 n ) ( λ ()) ( λ ()) |
988c12d7f887
use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
553
diff
changeset
|
196 compareTri (suc n) zero = tri> ( λ ()) ( λ ()) ( compareTri1 n ) |
553 | 197 compareTri (suc n) (suc m) with compareTri n m |
556 | 198 ... | tri< p q r = tri< (compareTri2 (suc n) m p ) (compareTri4 _ q) ( compareTri5 _ r ) |
199 ... | tri≈ p refl r = tri≈ (compareTri5 _ p) refl ( compareTri5 _ r ) | |
200 ... | tri> p q r = tri> ( compareTri5 _ p ) (compareTri4 _ q) (compareTri2 (suc m) n r ) | |
553 | 201 |
562 | 202 compareDecTest : (n n1 : Node ℕ ℕ) → ( key n ≡ key n1 ) ∨ ( ¬ key n ≡ key n1 ) |
553 | 203 compareDecTest n n1 with (key n) ≟ (key n1) |
556 | 204 ... | yes p = pi1 p |
554
988c12d7f887
use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
553
diff
changeset
|
205 ... | no ¬p = pi2 ¬p |
553 | 206 |
207 | |
562 | 208 putTest1Lemma2 : (k : ℕ) → compare2 k k ≡ EQ |
548 | 209 putTest1Lemma2 zero = refl |
210 putTest1Lemma2 (suc k) = putTest1Lemma2 k | |
546 | 211 |
562 | 212 putTest1Lemma1 : (x y : ℕ) → compareℕ x y ≡ compare2 x y |
548 | 213 putTest1Lemma1 zero zero = refl |
214 putTest1Lemma1 (suc m) zero = refl | |
215 putTest1Lemma1 zero (suc n) = refl | |
216 putTest1Lemma1 (suc m) (suc n) with Data.Nat.compare m n | |
217 putTest1Lemma1 (suc .m) (suc .(Data.Nat.suc m + k)) | less m k = lemma1 m | |
218 where | |
562 | 219 lemma1 : (m : ℕ) → LT ≡ compare2 m (ℕ.suc (m + k)) |
548 | 220 lemma1 zero = refl |
221 lemma1 (suc y) = lemma1 y | |
222 putTest1Lemma1 (suc .m) (suc .m) | equal m = lemma1 m | |
223 where | |
562 | 224 lemma1 : (m : ℕ) → EQ ≡ compare2 m m |
548 | 225 lemma1 zero = refl |
226 lemma1 (suc y) = lemma1 y | |
227 putTest1Lemma1 (suc .(Data.Nat.suc m + k)) (suc .m) | greater m k = lemma1 m | |
228 where | |
562 | 229 lemma1 : (m : ℕ) → GT ≡ compare2 (ℕ.suc (m + k)) m |
548 | 230 lemma1 zero = refl |
231 lemma1 (suc y) = lemma1 y | |
232 | |
562 | 233 putTest1Lemma3 : (k : ℕ) → compareℕ k k ≡ EQ |
548 | 234 putTest1Lemma3 k = trans (putTest1Lemma1 k k) ( putTest1Lemma2 k ) |
546 | 235 |
562 | 236 compareLemma1 : {x y : ℕ} → compare2 x y ≡ EQ → x ≡ y |
551 | 237 compareLemma1 {zero} {zero} refl = refl |
238 compareLemma1 {zero} {suc _} () | |
239 compareLemma1 {suc _} {zero} () | |
562 | 240 compareLemma1 {suc x} {suc y} eq = cong ( λ z → ℕ.suc z ) ( compareLemma1 ( trans lemma2 eq ) ) |
550
2476f7123dc3
root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
549
diff
changeset
|
241 where |
2476f7123dc3
root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
549
diff
changeset
|
242 lemma2 : compare2 (ℕ.suc x) (ℕ.suc y) ≡ compare2 x y |
2476f7123dc3
root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
549
diff
changeset
|
243 lemma2 = refl |
549 | 244 |
546 | 245 |
545 | 246 putTest1 :{ m : Level } (n : Maybe (Node ℕ ℕ)) |
562 | 247 → (k : ℕ) (x : ℕ) |
248 → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x | |
249 (λ t → getRedBlackTree t k (λ t x1 → check2 x1 x ≡ True)) | |
546 | 250 putTest1 n k x with n |
552 | 251 ... | Just n1 = lemma2 ( record { top = Nothing } ) |
551 | 252 where |
562 | 253 lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t → |
551 | 254 GetRedBlackTree.checkNode t k (λ t₁ x1 → check2 x1 x ≡ True) (root t)) |
552 | 255 lemma2 s with compare2 k (key n1) |
553 | 256 ... | EQ = lemma3 {!!} |
551 | 257 where |
562 | 258 lemma3 : compare2 k (key n1) ≡ EQ → getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { |
551 | 259 key = key n1 ; value = x ; right = right n1 ; left = left n1 ; color = Black |
562 | 260 } ) ; nodeStack = s ; compare = λ x₁ y → compare2 x₁ y } ) k ( λ t x1 → check2 x1 x ≡ True) |
552 | 261 lemma3 eq with compare2 x x | putTest1Lemma2 x |
262 ... | EQ | refl with compare2 k (key n1) | eq | |
263 ... | EQ | refl with compare2 x x | putTest1Lemma2 x | |
264 ... | EQ | refl = refl | |
551 | 265 ... | GT = {!!} |
266 ... | LT = {!!} | |
549 | 267 ... | Nothing = lemma1 |
268 where | |
269 lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record { root = Just ( record { | |
270 key = k ; value = x ; right = Nothing ; left = Nothing ; color = Red | |
271 } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compare2 x₁ y } ) k | |
562 | 272 ( λ t x1 → check2 x1 x ≡ True) |
550
2476f7123dc3
root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
549
diff
changeset
|
273 lemma1 with compare2 k k | putTest1Lemma2 k |
2476f7123dc3
root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
549
diff
changeset
|
274 ... | EQ | refl with compare2 x x | putTest1Lemma2 x |
2476f7123dc3
root = Nothing case passed on putTest1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
549
diff
changeset
|
275 ... | EQ | refl = refl |