Mercurial > hg > Members > Moririn

comparison work.agda @ 779:68904fdaab71

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