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