|
781
|
1 module work where
|
|
|
2 open import Level hiding (suc ; zero ; _⊔_ )
|
|
|
3
|
|
|
4 open import Data.Nat hiding (compare)
|
|
|
5 open import Data.Nat.Properties as NatProp
|
|
|
6 open import Data.Maybe
|
|
|
7 -- open import Data.Maybe.Properties
|
|
|
8 open import Data.Empty
|
|
|
9 open import Data.List
|
|
|
10 open import Data.Product
|
|
|
11
|
|
|
12 open import Function as F hiding (const)
|
|
|
13
|
|
|
14 open import Relation.Binary
|
|
|
15 open import Relation.Binary.PropositionalEquality
|
|
|
16 open import Relation.Nullary
|
|
|
17 open import logic
|
|
|
18
|
|
802
|
19 zero≢suc : { m : ℕ } → zero ≡ suc m → ⊥
|
|
|
20 zero≢suc ()
|
|
|
21 suc≢zero : {m : ℕ } → suc m ≡ zero → ⊥
|
|
|
22 suc≢zero ()
|
|
|
23 {-# TERMINATING #-}
|
|
|
24 DepthCal : ( l m n : ℕ ) → l ≡ m ⊔ n
|
|
|
25 DepthCal zero zero zero = refl
|
|
|
26 DepthCal zero zero (suc n) = ⊥-elim (zero≢suc (DepthCal zero zero (suc n)))
|
|
|
27 DepthCal zero (suc m) zero = ⊥-elim (zero≢suc (DepthCal zero (suc m) zero))
|
|
|
28 DepthCal zero (suc m) (suc n) = ⊥-elim (zero≢suc (DepthCal zero (suc m) (suc n)))
|
|
|
29 DepthCal (suc l) zero zero = ⊥-elim (suc≢zero (DepthCal (suc l) zero zero ))
|
|
|
30 DepthCal (suc l) zero (suc n) with <-cmp (suc l) (suc n)
|
|
|
31 ... | tri< a ¬b ¬c = ⊥-elim (¬b (DepthCal (suc l) zero (suc n) ))
|
|
|
32 ... | tri≈ ¬a b ¬c = cong suc (suc-injective b)
|
|
|
33 ... | tri> ¬a ¬b c = ⊥-elim (¬b (DepthCal (suc l) zero (suc n) ))
|
|
|
34 DepthCal (suc l) (suc m) zero with <-cmp (suc l) (suc m)
|
|
|
35 ... | tri< a ¬b ¬c = ⊥-elim (¬b (DepthCal (suc l) (suc m) zero ))
|
|
|
36 ... | tri≈ ¬a b ¬c = cong suc (suc-injective b)
|
|
|
37 ... | tri> ¬a ¬b c = ⊥-elim (¬b (DepthCal (suc l) (suc m) zero ))
|
|
|
38 DepthCal (suc l) (suc m) (suc n) = cong suc (DepthCal l m n )
|
|
|
39
|
|
|
40
|
|
781
|
41 data bt {n : Level} (A : Set n) : Set n where
|
|
|
42 leaf : bt A
|
|
|
43 node : (key : ℕ) → (value : A) → (left : bt A) → (right : bt A) → bt A
|
|
|
44
|
|
|
45 node-key : {n : Level}{A : Set n} → bt A → Maybe ℕ
|
|
|
46 node-key leaf = nothing
|
|
|
47 node-key (node key value tree tree₁) = just key
|
|
|
48
|
|
|
49 node-value : {n : Level} {A : Set n} → bt A → Maybe A
|
|
|
50 node-value leaf = nothing
|
|
|
51 node-value (node key value tree tree₁) = just value
|
|
|
52
|
|
|
53 bt-depth : {n : Level} {A : Set n} → (tree : bt A) → ℕ
|
|
|
54 bt-depth leaf = 0
|
|
|
55 bt-depth (node key value tree tree₁) = suc (bt-depth tree ⊔ bt-depth tree₁)
|
|
|
56 --一番下のleaf =0から戻るたびにsucをしていく
|
|
|
57 treeTest1 : bt ℕ
|
|
|
58 treeTest1 = node 0 0 leaf (node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf))
|
|
|
59
|
|
|
60 -- 0 0
|
|
|
61 -- / \
|
|
|
62 -- leaf 3 1
|
|
|
63 -- / \
|
|
|
64 -- 2 5 2
|
|
|
65 -- / \
|
|
|
66 -- 1 leaf 3
|
|
|
67 -- / \
|
|
|
68 -- leaf leaf 4
|
|
|
69
|
|
|
70 treeTest2 : bt ℕ
|
|
|
71 treeTest2 = node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf)
|
|
|
72
|
|
|
73 testdb : ℕ
|
|
|
74 testdb = bt-depth treeTest1 -- 4
|
|
|
75
|
|
802
|
76 import Data.Unit --hiding ( _≟_ ; _≤?_ ; _≤_)
|
|
781
|
77
|
|
|
78 data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
|
|
|
79 t-leaf : treeInvariant leaf
|
|
|
80
|
|
|
81 t-single : (key : ℕ) → (value : A) → treeInvariant (node key value leaf leaf)
|
|
|
82
|
|
|
83 t-left : {key key1 : ℕ} → {value value1 : A} → {t1 t2 : bt A} → key < key1
|
|
|
84 → treeInvariant (node key value t1 t2)
|
|
|
85 → treeInvariant (node key1 value1 (node key value t1 t2) leaf)
|
|
|
86
|
|
|
87 t-right : {key key1 : ℕ} → {value value1 : A} → {t1 t2 : bt A} → key < key1
|
|
|
88 → treeInvariant (node key1 value1 t1 t2)
|
|
|
89 → treeInvariant (node key value leaf (node key1 value1 t1 t2))
|
|
|
90
|
|
|
91 t-node : {key key1 key2 : ℕ}→ {value value1 value2 : A} → {t1 t2 t3 t4 : bt A} → key1 < key → key < key2
|
|
|
92 → treeInvariant (node key1 value1 t1 t2)
|
|
|
93 → treeInvariant (node key2 value2 t3 t4)
|
|
|
94 → treeInvariant (node key value (node key1 value1 t1 t2) (node key2 value2 t3 t4))
|
|
|
95
|
|
802
|
96 {-
|
|
|
97 treekey : {n : Level} {A : Set n} → {key key1 : ℕ} {value value1 : A} {t1 t2 : bt A} → treeInvariant (node key value (node key1 value1 t1 t2) leaf) → key1 < key
|
|
|
98 treekey (t-left x x₁) = x -- normal level
|
|
|
99 --treekey t-single key value = {!!}
|
|
|
100 -}
|
|
|
101
|
|
781
|
102 data stackInvariant {n : Level} {A : Set n} (key : ℕ ) : (top orig : bt A)
|
|
|
103 → (stack : List (bt A)) → Set n where
|
|
|
104 s-nil : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [] )
|
|
|
105
|
|
|
106 s-right : {key1 : ℕ } → {value : A } → {tree0 t1 t2 : bt A } → {st : List (bt A)}
|
|
|
107 → key1 < key
|
|
|
108 → stackInvariant key (node key1 value t1 t2) tree0 st
|
|
|
109 → stackInvariant key t2 tree0 (t2 ∷ st)
|
|
|
110
|
|
|
111 s-left : {key1 : ℕ } → {value : A } → {tree0 t1 t2 : bt A } → {st : List (bt A)}
|
|
|
112 → key < key1
|
|
|
113 → stackInvariant key (node key1 value t1 t2) tree0 st
|
|
|
114 → stackInvariant key t1 tree0 (t1 ∷ st)
|
|
|
115
|
|
|
116 data replacedTree {n : Level } {A : Set n} (key : ℕ) (value : A) : (before after : bt A) → Set n where
|
|
|
117 r-leaf : replacedTree key value leaf (node key value leaf leaf)
|
|
|
118
|
|
783
|
119 r-node : {value₁ : A} → {left right : bt A} → replacedTree key value (node key value₁ left right) (node key value left right)
|
|
781
|
120
|
|
|
121 -- key is the repl's key , so need comp key and key1
|
|
|
122 r-left : {key1 : ℕ} {value1 : A }→ {left right repl : bt A} → key < key1
|
|
|
123 → replacedTree key value left repl → replacedTree key value (node key1 value1 left right) (node key1 value1 repl right)
|
|
|
124
|
|
|
125 r-right : {key1 : ℕ } {value1 : A} → {left right repl : bt A} → key1 < key
|
|
|
126 → replacedTree key value right repl → replacedTree key value (node key1 value1 left right) (node key1 value1 left repl)
|
|
|
127
|
|
783
|
128
|
|
781
|
129 depth-1< : {i j : ℕ} → suc i ≤ suc (i Data.Nat.⊔ j )
|
|
|
130 depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
|
|
|
131 depth-2< : {i j : ℕ} → suc i ≤ suc (j Data.Nat.⊔ i )
|
|
|
132 depth-2< {i} {j} = s≤s (m≤n⊔m j i)
|
|
|
133 depth-3< : {i : ℕ } → suc i ≤ suc (suc i)
|
|
|
134 depth-3< {zero} = s≤s ( z≤n )
|
|
|
135 depth-3< {suc i} = s≤s (depth-3< {i} )
|
|
|
136
|
|
|
137 treeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} → (tleft tright : bt A)
|
|
|
138 → treeInvariant (node key value tleft tright)
|
|
|
139 → treeInvariant tleft
|
|
|
140 treeLeftDown leaf leaf (t-single key value) = t-leaf
|
|
|
141 treeLeftDown leaf (node key value t1 t2) (t-right x ti) = t-leaf
|
|
|
142 treeLeftDown (node key value t t₁) leaf (t-left x ti) = ti
|
|
|
143 treeLeftDown (node key value t t₁) (node key₁ value₁ t1 t2) (t-node x x1 ti ti2 ) = ti
|
|
|
144
|
|
|
145 treeRightDown : {n : Level} {A : Set n} {key : ℕ} {value : A} → (tleft tright : bt A)
|
|
|
146 → treeInvariant (node key value tleft tright)
|
|
|
147 → treeInvariant tright
|
|
|
148 treeRightDown leaf leaf (t-single key value) = t-leaf
|
|
|
149 treeRightDown leaf (node key value t1 t2) (t-right x ti) = ti
|
|
|
150
|
|
|
151 treeRightDown (node key value t t₁) leaf (t-left x ti) = t-leaf
|
|
|
152 treeRightDown (node key value t t₁) (node key₁ value₁ t1 t2) (t-node x x1 ti ti2 ) = ti2
|
|
|
153
|
|
|
154
|
|
|
155 findP : {n m : Level} {A : Set n} {t : Set n} → (tkey : ℕ) → (top orig : bt A) → (st : List (bt A))
|
|
|
156 → (treeInvariant top)
|
|
|
157 → stackInvariant tkey top orig st
|
|
|
158 → (next : (newtop : bt A) → (stack : List (bt A))
|
|
|
159 → (treeInvariant newtop)
|
|
|
160 → (stackInvariant tkey newtop orig stack)
|
|
|
161 → bt-depth newtop < bt-depth top → t)
|
|
|
162 → (exit : (newtop : bt A) → (stack : List (bt A))
|
|
|
163 → (treeInvariant newtop)
|
|
|
164 → (stackInvariant tkey newtop orig stack) --need new stack ?
|
|
|
165 → (newtop ≡ leaf) ∨ (node-key newtop ≡ just tkey) → t)
|
|
|
166 → t
|
|
|
167 findP tkey leaf orig st ti si next exit = exit leaf st ti si (case1 refl)
|
|
|
168 findP tkey (node key value tl tr) orig st ti si next exit with <-cmp tkey key
|
|
|
169 findP tkey top orig st ti si next exit | tri≈ ¬a refl ¬c = exit top st ti si (case2 refl)
|
|
|
170 findP tkey (node key value tl tr) orig st ti si next exit | tri< a ¬b ¬c = next tl (tl ∷ st) (treeLeftDown tl tr ti) (s-left a si) (s≤s (m≤m⊔n (bt-depth tl) (bt-depth tr)))
|
|
|
171
|
|
|
172 findP tkey (node key value tl tr) orig st ti si next exit | tri> ¬a ¬b c = next tr (tr ∷ st) (treeRightDown tl tr ti) (s-right c si) (s≤s (m≤n⊔m (bt-depth tl) (bt-depth tr)))
|
|
|
173
|
|
|
174
|
|
|
175 --RBT
|
|
|
176 data Color : Set where
|
|
|
177 Red : Color
|
|
|
178 Black : Color
|
|
|
179
|
|
|
180 RB→bt : {n : Level} (A : Set n) → (bt (Color ∧ A)) → bt A
|
|
|
181 RB→bt {n} A leaf = leaf
|
|
|
182 RB→bt {n} A (node key ⟪ C , value ⟫ tr t1) = (node key value (RB→bt A tr) (RB→bt A t1))
|
|
|
183
|
|
|
184 color : {n : Level} {A : Set n} → (bt (Color ∧ A)) → Color
|
|
|
185 color leaf = Black
|
|
|
186 color (node key ⟪ C , value ⟫ rb rb₁) = C
|
|
|
187
|
|
|
188 black-depth : {n : Level} {A : Set n} → (tree : bt (Color ∧ A) ) → ℕ
|
|
|
189 black-depth leaf = 0
|
|
|
190 black-depth (node key ⟪ Red , value ⟫ t t₁) = black-depth t ⊔ black-depth t₁
|
|
|
191 black-depth (node key ⟪ Black , value ⟫ t t₁) = suc (black-depth t ⊔ black-depth t₁ )
|
|
|
192
|
|
802
|
193
|
|
|
194
|
|
781
|
195 data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where
|
|
786
|
196 rb-leaf : RBtreeInvariant leaf
|
|
781
|
197 rb-single : (key : ℕ) → (value : A) → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf leaf)
|
|
|
198 rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁
|
|
|
199 → black-depth t ≡ black-depth t₁
|
|
|
200 → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁)
|
|
|
201 → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key₁ ⟪ Black , value₁ ⟫ t t₁))
|
|
|
202 rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {c : Color}
|
|
|
203 → black-depth t ≡ black-depth t₁
|
|
|
204 → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁)
|
|
|
205 → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁))
|
|
|
206 rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁
|
|
|
207 → black-depth t ≡ black-depth t₁
|
|
|
208 → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁)
|
|
|
209 → RBtreeInvariant (node key ⟪ Red , value ⟫ (node key₁ ⟪ Black , value₁ ⟫ t t₁) leaf )
|
|
|
210 rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {c : Color}
|
|
|
211 → black-depth t ≡ black-depth t₁
|
|
|
212 → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁)
|
|
|
213 → RBtreeInvariant (node key ⟪ Black , value ⟫ (node key₁ ⟪ c , value₁ ⟫ t t₁) leaf)
|
|
|
214 rb-node-red : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂
|
|
|
215 → black-depth t₁ ≡ black-depth t₂
|
|
|
216 → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ t₂)
|
|
|
217 → black-depth t₃ ≡ black-depth t₄
|
|
|
218 → RBtreeInvariant (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)
|
|
|
219 → RBtreeInvariant (node key₁ ⟪ Red , value₁ ⟫ (node key ⟪ Black , value ⟫ t₁ t₂) (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄))
|
|
|
220 rb-node-black : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂
|
|
|
221 → {c c₁ : Color}
|
|
|
222 → black-depth t₁ ≡ black-depth t₂
|
|
|
223 → RBtreeInvariant (node key ⟪ c , value ⟫ t₁ t₂)
|
|
|
224 → black-depth t₃ ≡ black-depth t₄
|
|
|
225 → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)
|
|
|
226 → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄))
|
|
|
227
|
|
|
228
|
|
|
229 data rotatedTree {n : Level} {A : Set n} : (before after : bt A) → Set n where
|
|
|
230 rtt-node : {t : bt A } → rotatedTree t t
|
|
|
231 -- a b
|
|
|
232 -- b c d a
|
|
|
233 -- d e e c
|
|
|
234 --
|
|
|
235 rtt-right : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A}
|
|
|
236 --kd < kb < ke < ka< kc
|
|
|
237 → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A}
|
|
|
238 → kd < kb → kb < ke → ke < ka → ka < kc
|
|
|
239 → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1)
|
|
|
240 → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1)
|
|
|
241 → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
|
|
|
242 → rotatedTree (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
|
|
|
243 (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
|
|
|
244
|
|
|
245 rtt-left : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A}
|
|
|
246 --kd < kb < ke < ka< kc
|
|
|
247 → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A} -- after child
|
|
|
248 → kd < kb → kb < ke → ke < ka → ka < kc
|
|
|
249 → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1)
|
|
|
250 → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1)
|
|
|
251 → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
|
|
|
252 → rotatedTree (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
|
|
|
253 (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
|
|
|
254
|
|
|
255 RBtreeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color}
|
|
|
256 → (tleft tright : bt (Color ∧ A))
|
|
|
257 → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright)
|
|
|
258 → RBtreeInvariant tleft
|
|
|
259 RBtreeLeftDown leaf leaf (rb-single k1 v) = rb-leaf
|
|
|
260 RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rb-leaf
|
|
|
261 RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rb-leaf
|
|
|
262 RBtreeLeftDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rb-leaf
|
|
|
263 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti
|
|
|
264 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti)= ti
|
|
|
265 RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti
|
|
|
266 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til
|
|
|
267 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til bde2 tir) = til
|
|
|
268 RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til
|
|
|
269 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til
|
|
|
270 RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til
|
|
|
271
|
|
|
272 RBtreeRightDown : {n : Level} {A : Set n} { key : ℕ} {value : A} {c : Color}
|
|
|
273 → (tleft tright : bt (Color ∧ A))
|
|
|
274 → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright)
|
|
|
275 → RBtreeInvariant tright
|
|
|
276 RBtreeRightDown leaf leaf (rb-single k1 v1 ) = rb-leaf
|
|
|
277 RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rbti
|
|
|
278 RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rbti
|
|
|
279 RBtreeRightDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rbti
|
|
|
280 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf
|
|
|
281 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti) = rb-leaf
|
|
|
282 RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf
|
|
|
283 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir
|
|
|
284 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til bde2 tir) = tir
|
|
|
285 RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir
|
|
|
286 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir
|
|
|
287 RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir
|
|
|
288
|
|
|
289 findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) )
|
|
|
290 → (stack : List (bt (Color ∧ A)))
|
|
|
291 → treeInvariant tree ∧ stackInvariant key tree tree0 stack
|
|
|
292 → RBtreeInvariant tree
|
|
|
293 → (next : (tree1 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A)))
|
|
|
294 → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
|
|
|
295 → RBtreeInvariant tree1
|
|
|
296 → bt-depth tree1 < bt-depth tree → t )
|
|
|
297 → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A)))
|
|
|
298 → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
|
|
|
299 → RBtreeInvariant tree1
|
|
|
300 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t
|
|
|
301 findRBT key leaf tree0 stack ti rb0 next exit = exit leaf stack ti rb0 (case1 refl)
|
|
|
302 findRBT key n@(node key₁ value left right) tree0 stack ti rb0 next exit with <-cmp key key₁
|
|
|
303 findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri< a ¬b ¬c
|
|
|
304 = next left (left ∷ stack) ⟪ treeLeftDown left right (_∧_.proj1 ti) , s-left a (_∧_.proj2 ti) ⟫ (RBtreeLeftDown left right rb0) depth-1<
|
|
|
305 findRBT key n tree0 stack ti rb0 _ exit | tri≈ ¬a refl ¬c = exit n stack ti rb0 (case2 refl)
|
|
|
306 findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri> ¬a ¬b c
|
|
|
307 = next right (right ∷ stack) ⟪ treeRightDown left right (_∧_.proj1 ti), s-right c (_∧_.proj2 ti) ⟫ (RBtreeRightDown left right rb0) depth-2<
|
|
|
308
|
|
|
309 child-replaced : {n : Level} {A : Set n} (key : ℕ) (tree : bt A) → bt A
|
|
|
310 child-replaced key leaf = leaf
|
|
|
311 child-replaced key (node key₁ value left right) with <-cmp key key₁
|
|
|
312 ... | tri< a ¬b ¬c = left
|
|
|
313 ... | tri≈ ¬a b ¬c = node key₁ value left right
|
|
|
314 ... | tri> ¬a ¬b c = right
|
|
|
315
|
|
|
316
|
|
|
317 data replacedRBTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt (Color ∧ A) ) → Set n where
|
|
|
318 rbr-leaf : {ca cb : Color} → replacedRBTree key value leaf (node key ⟪ cb , value ⟫ leaf leaf)
|
|
|
319 rbr-node : {value₁ : A} → {ca cb : Color } → {t t₁ : bt (Color ∧ A)}
|
|
|
320 → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ cb , value ⟫ t t₁)
|
|
|
321 rbr-right : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
|
|
|
322 → k < key → replacedRBTree key value t2 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t1 t)
|
|
|
323 rbr-left : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
|
|
|
324 → k < key → replacedRBTree key value t1 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2)
|
|
|
325
|
|
|
326 data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent uncle grand : bt A) → Set n where
|
|
|
327 s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
328 → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand
|
|
|
329 s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
330 → parent ≡ node kp vp n1 self → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand
|
|
|
331 s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
332 → parent ≡ node kp vp self n1 → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand
|
|
|
333 s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
334 → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand
|
|
|
335
|
|
|
336 record PG {n : Level } (A : Set n) (self : bt A) (stack : List (bt A)) : Set n where
|
|
|
337 field
|
|
|
338 parent grand uncle : bt A
|
|
|
339 pg : ParentGrand self parent uncle grand
|
|
|
340 rest : List (bt A)
|
|
|
341 stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest )
|
|
|
342
|
|
|
343 record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) : Set n where
|
|
|
344 field
|
|
|
345 od d rd : ℕ
|
|
|
346 tree rot : bt (Color ∧ A)
|
|
|
347 origti : treeInvariant orig
|
|
|
348 origrb : RBtreeInvariant orig
|
|
|
349 treerb : RBtreeInvariant tree
|
|
|
350 replrb : RBtreeInvariant repl
|
|
|
351 d=rd : ( d ≡ rd ) ∨ ((suc d ≡ rd ) ∧ (color tree ≡ Red))
|
|
|
352 si : stackInvariant key tree orig stack
|
|
|
353 rotated : rotatedTree tree rot
|
|
|
354 ri : replacedRBTree key value (child-replaced key rot ) repl
|
|
|
355
|
|
|
356
|
|
|
357 rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) )
|
|
|
358 → RBtreeInvariant parent
|
|
|
359 → RBtreeInvariant repl
|
|
|
360 → {left right : bt (Color ∧ A)} → parent ≡ node key ⟪ Black , value ⟫ left right
|
|
|
361 → (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl ) )
|
|
|
362 ∧ (color left ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) )
|
|
783
|
363 rbi-case1 {n} {A} {key} parent repl rbtip rbtir x = ⟪ {!!} , {!!} ⟫
|
|
781
|
364
|
|
802
|
365 blackdepth≡ : {n : Level } {A : Set n} → {C : Color} {key key1 : ℕ} {value value1 : A} → (tree1 tree2 : bt (Color ∧ A))
|
|
781
|
366 → RBtreeInvariant tree1
|
|
|
367 → RBtreeInvariant tree2
|
|
|
368 → RBtreeInvariant (node key ⟪ C , value ⟫ tree1 tree2)
|
|
|
369 → black-depth tree1 ≡ black-depth tree2
|
|
802
|
370 blackdepth≡ leaf leaf ri1 ri2 rip = refl
|
|
|
371 blackdepth≡ {n} {A} leaf (node key .(⟪ Black , _ ⟫) t2 t3) ri1 ri2 (rb-right-red x x₁ rip) = DepthCal (black-depth {n} {A} leaf) (black-depth (node key ⟪ Black , _ ⟫ t2 t3)) 0
|
|
|
372 blackdepth≡ {n} {A} leaf (node key .(⟪ _ , _ ⟫) t2 t3) ri1 ri2 (rb-right-black x x₁ rip) = DepthCal (black-depth {n} {A} leaf) (black-depth (node key ⟪ _ , _ ⟫ t2 t3) ) (black-depth (node key ⟪ _ , _ ⟫ t2 t3) )
|
|
|
373 blackdepth≡ {n} {A} (node key .(⟪ Black , _ ⟫) t1 t3) leaf ri1 ri2 (rb-left-red x x₁ rip) = DepthCal (black-depth (node key ⟪ Black , _ ⟫ t1 t3)) (black-depth {n} {A} leaf) 0
|
|
|
374 blackdepth≡ {n} {A} (node key .(⟪ _ , _ ⟫) t1 t3) leaf ri1 ri2 (rb-left-black x x₁ rip) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) (black-depth {n} {A} leaf) 0
|
|
|
375 blackdepth≡ (node key .(⟪ Black , _ ⟫) t1 t3) (node key₁ .(⟪ Black , _ ⟫) t2 t4) ri1 ri2 (rb-node-red x x₁ x₂ rip x₃ rip₁) = DepthCal (black-depth (node key ⟪ Black , _ ⟫ t1 t3)) (black-depth (node key₁ ⟪ Black , _ ⟫ t2 t4)) 0
|
|
|
376 blackdepth≡ (node key .(⟪ _ , _ ⟫) t1 t3) (node key₁ .(⟪ _ , _ ⟫) t2 t4) ri1 ri2 (rb-node-black x x₁ x₂ rip x₃ rip₁) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) ( black-depth (node key₁ ⟪ _ , _ ⟫ t2 t4)) (black-depth (node key₁ (⟪ _ , _ ⟫) t2 t4))
|
|
803
|
377
|
|
802
|
378 rb08 : {n : Level } {A : Set n}{key key1 : ℕ} {value value1 : A} {c c1 : Color} {t₁ t₂ t₃ t₄ : bt (Color ∧ A)}
|
|
|
379 → black-depth (node key ⟪ c , value ⟫ t₁ t₂) ≡ black-depth (node key1 ⟪ c1 , value1 ⟫ t₃ t₄)
|
|
|
380 rb08 = {!!}
|
|
783
|
381
|
|
|
382 {-
|
|
|
383 rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) )
|
|
|
384 → RBtreeInvariant parent
|
|
|
385 → RBtreeInvariant repl → (left right : bt (Color ∧ A)) → parent ≡ node key ⟪ Black , value ⟫ left right
|
|
781
|
386 → RBtreeInvariant left
|
|
|
387 → RBtreeInvariant right
|
|
783
|
388 → (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl ) ) ∧ (color left ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) )
|
|
|
389
|
|
|
390 rbi-case1 {n} {A} {key} (node key1 ⟪ Black , value1 ⟫ l r) leaf rbip rbir (node key3 ⟪ Red , val3 ⟫ la ra) (node key4-- ⟪ Red , val4 ⟫ lb rb) pa li ri = {!!}
|
|
|
391 -}
|
