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