|
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
|
|
807
|
73
|
|
|
74
|
|
781
|
75 testdb : ℕ
|
|
|
76 testdb = bt-depth treeTest1 -- 4
|
|
|
77
|
|
802
|
78 import Data.Unit --hiding ( _≟_ ; _≤?_ ; _≤_)
|
|
781
|
79
|
|
|
80 data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
|
|
|
81 t-leaf : treeInvariant leaf
|
|
|
82
|
|
|
83 t-single : (key : ℕ) → (value : A) → treeInvariant (node key value leaf leaf)
|
|
|
84
|
|
|
85 t-left : {key key1 : ℕ} → {value value1 : A} → {t1 t2 : bt A} → key < key1
|
|
|
86 → treeInvariant (node key value t1 t2)
|
|
|
87 → treeInvariant (node key1 value1 (node key value t1 t2) leaf)
|
|
|
88
|
|
|
89 t-right : {key key1 : ℕ} → {value value1 : A} → {t1 t2 : bt A} → key < key1
|
|
|
90 → treeInvariant (node key1 value1 t1 t2)
|
|
|
91 → treeInvariant (node key value leaf (node key1 value1 t1 t2))
|
|
|
92
|
|
|
93 t-node : {key key1 key2 : ℕ}→ {value value1 value2 : A} → {t1 t2 t3 t4 : bt A} → key1 < key → key < key2
|
|
|
94 → treeInvariant (node key1 value1 t1 t2)
|
|
|
95 → treeInvariant (node key2 value2 t3 t4)
|
|
|
96 → treeInvariant (node key value (node key1 value1 t1 t2) (node key2 value2 t3 t4))
|
|
|
97
|
|
802
|
98 {-
|
|
|
99 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
|
|
|
100 treekey (t-left x x₁) = x -- normal level
|
|
|
101 --treekey t-single key value = {!!}
|
|
|
102 -}
|
|
|
103
|
|
781
|
104 data stackInvariant {n : Level} {A : Set n} (key : ℕ ) : (top orig : bt A)
|
|
|
105 → (stack : List (bt A)) → Set n where
|
|
|
106 s-nil : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [] )
|
|
|
107
|
|
|
108 s-right : {key1 : ℕ } → {value : A } → {tree0 t1 t2 : bt A } → {st : List (bt A)}
|
|
|
109 → key1 < key
|
|
|
110 → stackInvariant key (node key1 value t1 t2) tree0 st
|
|
|
111 → stackInvariant key t2 tree0 (t2 ∷ st)
|
|
|
112
|
|
|
113 s-left : {key1 : ℕ } → {value : A } → {tree0 t1 t2 : bt A } → {st : List (bt A)}
|
|
|
114 → key < key1
|
|
|
115 → stackInvariant key (node key1 value t1 t2) tree0 st
|
|
|
116 → stackInvariant key t1 tree0 (t1 ∷ st)
|
|
|
117
|
|
|
118 data replacedTree {n : Level } {A : Set n} (key : ℕ) (value : A) : (before after : bt A) → Set n where
|
|
|
119 r-leaf : replacedTree key value leaf (node key value leaf leaf)
|
|
|
120
|
|
783
|
121 r-node : {value₁ : A} → {left right : bt A} → replacedTree key value (node key value₁ left right) (node key value left right)
|
|
781
|
122
|
|
|
123 -- key is the repl's key , so need comp key and key1
|
|
|
124 r-left : {key1 : ℕ} {value1 : A }→ {left right repl : bt A} → key < key1
|
|
|
125 → replacedTree key value left repl → replacedTree key value (node key1 value1 left right) (node key1 value1 repl right)
|
|
|
126
|
|
|
127 r-right : {key1 : ℕ } {value1 : A} → {left right repl : bt A} → key1 < key
|
|
|
128 → replacedTree key value right repl → replacedTree key value (node key1 value1 left right) (node key1 value1 left repl)
|
|
|
129
|
|
783
|
130
|
|
781
|
131 depth-1< : {i j : ℕ} → suc i ≤ suc (i Data.Nat.⊔ j )
|
|
|
132 depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
|
|
|
133 depth-2< : {i j : ℕ} → suc i ≤ suc (j Data.Nat.⊔ i )
|
|
|
134 depth-2< {i} {j} = s≤s (m≤n⊔m j i)
|
|
|
135 depth-3< : {i : ℕ } → suc i ≤ suc (suc i)
|
|
|
136 depth-3< {zero} = s≤s ( z≤n )
|
|
|
137 depth-3< {suc i} = s≤s (depth-3< {i} )
|
|
|
138
|
|
|
139 treeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} → (tleft tright : bt A)
|
|
|
140 → treeInvariant (node key value tleft tright)
|
|
|
141 → treeInvariant tleft
|
|
|
142 treeLeftDown leaf leaf (t-single key value) = t-leaf
|
|
|
143 treeLeftDown leaf (node key value t1 t2) (t-right x ti) = t-leaf
|
|
|
144 treeLeftDown (node key value t t₁) leaf (t-left x ti) = ti
|
|
|
145 treeLeftDown (node key value t t₁) (node key₁ value₁ t1 t2) (t-node x x1 ti ti2 ) = ti
|
|
|
146
|
|
|
147 treeRightDown : {n : Level} {A : Set n} {key : ℕ} {value : A} → (tleft tright : bt A)
|
|
|
148 → treeInvariant (node key value tleft tright)
|
|
|
149 → treeInvariant tright
|
|
|
150 treeRightDown leaf leaf (t-single key value) = t-leaf
|
|
|
151 treeRightDown leaf (node key value t1 t2) (t-right x ti) = ti
|
|
|
152
|
|
|
153 treeRightDown (node key value t t₁) leaf (t-left x ti) = t-leaf
|
|
|
154 treeRightDown (node key value t t₁) (node key₁ value₁ t1 t2) (t-node x x1 ti ti2 ) = ti2
|
|
|
155
|
|
|
156
|
|
|
157 findP : {n m : Level} {A : Set n} {t : Set n} → (tkey : ℕ) → (top orig : bt A) → (st : List (bt A))
|
|
|
158 → (treeInvariant top)
|
|
|
159 → stackInvariant tkey top orig st
|
|
|
160 → (next : (newtop : bt A) → (stack : List (bt A))
|
|
|
161 → (treeInvariant newtop)
|
|
|
162 → (stackInvariant tkey newtop orig stack)
|
|
|
163 → bt-depth newtop < bt-depth top → t)
|
|
|
164 → (exit : (newtop : bt A) → (stack : List (bt A))
|
|
|
165 → (treeInvariant newtop)
|
|
|
166 → (stackInvariant tkey newtop orig stack) --need new stack ?
|
|
|
167 → (newtop ≡ leaf) ∨ (node-key newtop ≡ just tkey) → t)
|
|
|
168 → t
|
|
|
169 findP tkey leaf orig st ti si next exit = exit leaf st ti si (case1 refl)
|
|
|
170 findP tkey (node key value tl tr) orig st ti si next exit with <-cmp tkey key
|
|
|
171 findP tkey top orig st ti si next exit | tri≈ ¬a refl ¬c = exit top st ti si (case2 refl)
|
|
|
172 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)))
|
|
|
173
|
|
|
174 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)))
|
|
|
175
|
|
|
176
|
|
|
177 --RBT
|
|
|
178 data Color : Set where
|
|
|
179 Red : Color
|
|
|
180 Black : Color
|
|
|
181
|
|
|
182 RB→bt : {n : Level} (A : Set n) → (bt (Color ∧ A)) → bt A
|
|
|
183 RB→bt {n} A leaf = leaf
|
|
|
184 RB→bt {n} A (node key ⟪ C , value ⟫ tr t1) = (node key value (RB→bt A tr) (RB→bt A t1))
|
|
|
185
|
|
807
|
186 RBTreeTest : bt (Color ∧ ℕ)
|
|
|
187 RBTreeTest = node 8 ⟪ Black , 200 ⟫ (node 5 ⟪ Red , 100 ⟫ (_) (_)) (node 10 ⟪ Red , 300 ⟫ (_) (_))
|
|
|
188
|
|
781
|
189 color : {n : Level} {A : Set n} → (bt (Color ∧ A)) → Color
|
|
|
190 color leaf = Black
|
|
|
191 color (node key ⟪ C , value ⟫ rb rb₁) = C
|
|
|
192
|
|
|
193 black-depth : {n : Level} {A : Set n} → (tree : bt (Color ∧ A) ) → ℕ
|
|
|
194 black-depth leaf = 0
|
|
|
195 black-depth (node key ⟪ Red , value ⟫ t t₁) = black-depth t ⊔ black-depth t₁
|
|
|
196 black-depth (node key ⟪ Black , value ⟫ t t₁) = suc (black-depth t ⊔ black-depth t₁ )
|
|
|
197
|
|
802
|
198
|
|
|
199
|
|
781
|
200 data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where
|
|
786
|
201 rb-leaf : RBtreeInvariant leaf
|
|
807
|
202 rb-single : {c : Color} → (key : ℕ) → (value : A) → RBtreeInvariant (node key ⟪ c , value ⟫ leaf leaf)
|
|
781
|
203 rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁
|
|
|
204 → black-depth t ≡ black-depth t₁
|
|
|
205 → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁)
|
|
|
206 → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key₁ ⟪ Black , value₁ ⟫ t t₁))
|
|
|
207 rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {c : Color}
|
|
|
208 → black-depth t ≡ black-depth t₁
|
|
|
209 → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁)
|
|
|
210 → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁))
|
|
807
|
211 rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key₁ < key
|
|
781
|
212 → black-depth t ≡ black-depth t₁
|
|
|
213 → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁)
|
|
|
214 → RBtreeInvariant (node key ⟪ Red , value ⟫ (node key₁ ⟪ Black , value₁ ⟫ t t₁) leaf )
|
|
807
|
215 rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → {c : Color} → key₁ < key
|
|
781
|
216 → black-depth t ≡ black-depth t₁
|
|
|
217 → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁)
|
|
|
218 → RBtreeInvariant (node key ⟪ Black , value ⟫ (node key₁ ⟪ c , value₁ ⟫ t t₁) leaf)
|
|
|
219 rb-node-red : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂
|
|
807
|
220 → black-depth (node key ⟪ Black , value ⟫ t₁ t₂) ≡ black-depth (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)
|
|
781
|
221 → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ t₂)
|
|
|
222 → RBtreeInvariant (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)
|
|
|
223 → RBtreeInvariant (node key₁ ⟪ Red , value₁ ⟫ (node key ⟪ Black , value ⟫ t₁ t₂) (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄))
|
|
|
224 rb-node-black : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂
|
|
|
225 → {c c₁ : Color}
|
|
807
|
226 → black-depth (node key ⟪ c , value ⟫ t₁ t₂) ≡ black-depth (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)
|
|
781
|
227 → RBtreeInvariant (node key ⟪ c , value ⟫ t₁ t₂)
|
|
|
228 → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)
|
|
|
229 → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄))
|
|
|
230
|
|
|
231
|
|
|
232 data rotatedTree {n : Level} {A : Set n} : (before after : bt A) → Set n where
|
|
|
233 rtt-node : {t : bt A } → rotatedTree t t
|
|
|
234 -- a b
|
|
|
235 -- b c d a
|
|
|
236 -- d e e c
|
|
|
237 --
|
|
|
238 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}
|
|
|
239 --kd < kb < ke < ka< kc
|
|
|
240 → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A}
|
|
|
241 → kd < kb → kb < ke → ke < ka → ka < kc
|
|
|
242 → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1)
|
|
|
243 → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1)
|
|
|
244 → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
|
|
|
245 → rotatedTree (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
|
|
|
246 (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
|
|
|
247
|
|
|
248 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}
|
|
|
249 --kd < kb < ke < ka< kc
|
|
|
250 → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A} -- after child
|
|
|
251 → kd < kb → kb < ke → ke < ka → ka < kc
|
|
|
252 → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1)
|
|
|
253 → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1)
|
|
|
254 → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
|
|
|
255 → rotatedTree (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
|
|
|
256 (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
|
|
|
257
|
|
|
258 RBtreeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color}
|
|
|
259 → (tleft tright : bt (Color ∧ A))
|
|
|
260 → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright)
|
|
|
261 → RBtreeInvariant tleft
|
|
|
262 RBtreeLeftDown leaf leaf (rb-single k1 v) = rb-leaf
|
|
|
263 RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rb-leaf
|
|
|
264 RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rb-leaf
|
|
|
265 RBtreeLeftDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rb-leaf
|
|
|
266 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti
|
|
|
267 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti)= ti
|
|
|
268 RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti
|
|
807
|
269 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = til --x x1 bde1 til bde2 tir) = til
|
|
|
270 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til tir) = til
|
|
|
271 RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = til
|
|
|
272 RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = til
|
|
|
273 RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = til
|
|
781
|
274
|
|
|
275 RBtreeRightDown : {n : Level} {A : Set n} { key : ℕ} {value : A} {c : Color}
|
|
|
276 → (tleft tright : bt (Color ∧ A))
|
|
|
277 → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright)
|
|
|
278 → RBtreeInvariant tright
|
|
|
279 RBtreeRightDown leaf leaf (rb-single k1 v1 ) = rb-leaf
|
|
|
280 RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rbti
|
|
|
281 RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rbti
|
|
|
282 RBtreeRightDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rbti
|
|
|
283 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf
|
|
|
284 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti) = rb-leaf
|
|
|
285 RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf
|
|
807
|
286 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir ) = tir --x x1 bde1 til bde2 tir) = tir
|
|
|
287 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde til tir) = tir
|
|
|
288 RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = tir
|
|
|
289 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = tir
|
|
|
290 RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = tir
|
|
|
291
|
|
|
292
|
|
|
293 blackdepth≡ : {n : Level } {A : Set n} → {C : Color} {key key1 : ℕ} {value value1 : A} → (tree1 tree2 : bt (Color ∧ A))
|
|
|
294 → RBtreeInvariant tree1
|
|
|
295 → RBtreeInvariant tree2
|
|
|
296 → RBtreeInvariant (node key ⟪ C , value ⟫ tree1 tree2)
|
|
|
297 → black-depth tree1 ≡ black-depth tree2
|
|
|
298 blackdepth≡ leaf leaf ri1 ri2 rip = refl
|
|
|
299 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
|
|
|
300 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))
|
|
|
301 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
|
|
|
302 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
|
|
|
303 blackdepth≡ (node key .(⟪ Black , _ ⟫) t1 t3) (node key₁ .(⟪ Black , _ ⟫) t2 t4) ri1 ri2 (rb-node-red x x₁ x₂ rip rip₁) = DepthCal (black-depth (node key ⟪ Black , _ ⟫ t1 t3)) (black-depth (node key₁ ⟪ Black , _ ⟫ t2 t4)) 0
|
|
|
304 blackdepth≡ (node key .(⟪ _ , _ ⟫) t1 t3) (node key₁ .(⟪ _ , _ ⟫) t2 t4) ri1 ri2 (rb-node-black x x₁ x₂ rip rip₁) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) ( black-depth (node key₁ ⟪ _ , _ ⟫ t2 t4)) (black-depth (node key₁ (⟪ _ , _ ⟫) t2 t4))
|
|
781
|
305
|
|
|
306 findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) )
|
|
|
307 → (stack : List (bt (Color ∧ A)))
|
|
807
|
308 → RBtreeInvariant tree ∧ stackInvariant key tree tree0 stack
|
|
781
|
309 → (next : (tree1 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A)))
|
|
807
|
310 → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
|
|
781
|
311 → bt-depth tree1 < bt-depth tree → t )
|
|
|
312 → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A)))
|
|
807
|
313 → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
|
|
781
|
314 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t
|
|
807
|
315 findRBT key leaf tree0 stack inv next exit = exit leaf stack inv (case1 refl)
|
|
|
316 findRBT key (node key₁ value left right) tree0 stack inv next exit with <-cmp key key₁
|
|
|
317 findRBT key (node key₁ value left right) tree0 stack inv next exit | tri< a ¬b ¬c
|
|
|
318 = next left (left ∷ stack) ⟪ RBtreeLeftDown left right (_∧_.proj1 inv) , s-left a (_∧_.proj2 inv) ⟫ depth-1<
|
|
|
319 findRBT key n tree0 stack inv _ exit | tri≈ ¬a refl ¬c = exit n stack inv (case2 refl)
|
|
|
320 findRBT key (node key₁ value left right) tree0 stack inv next exit | tri> ¬a ¬b c
|
|
|
321 = next right (right ∷ stack) ⟪ RBtreeRightDown left right (_∧_.proj1 inv) , s-right c (_∧_.proj2 inv) ⟫ depth-2<
|
|
781
|
322
|
|
|
323 child-replaced : {n : Level} {A : Set n} (key : ℕ) (tree : bt A) → bt A
|
|
|
324 child-replaced key leaf = leaf
|
|
|
325 child-replaced key (node key₁ value left right) with <-cmp key key₁
|
|
|
326 ... | tri< a ¬b ¬c = left
|
|
|
327 ... | tri≈ ¬a b ¬c = node key₁ value left right
|
|
|
328 ... | tri> ¬a ¬b c = right
|
|
|
329
|
|
|
330
|
|
807
|
331 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥
|
|
|
332 lemma3 refl ()
|
|
|
333 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
|
|
|
334 lemma5 (s≤s z≤n) ()
|
|
|
335 ¬x<x : {x : ℕ} → ¬ (x < x)
|
|
|
336 ¬x<x (s≤s lt) = ¬x<x lt
|
|
|
337 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
|
|
|
338 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
|
|
|
339 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
|
|
|
340 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
|
|
|
341
|
|
|
342 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
|
|
|
343 → (r : Index) → (p : Invraiant r)
|
|
|
344 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t
|
|
|
345 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r)
|
|
|
346 ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) )
|
|
|
347 ... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (m≤n⇒m≤1+n lt1) p1 lt1 ) where
|
|
|
348 TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t
|
|
|
349 TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1))
|
|
|
350 TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j)
|
|
|
351 ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt
|
|
|
352 ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 )
|
|
|
353 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j )
|
|
|
354 open _∧_
|
|
|
355 --findRBTree : (exit : )
|
|
|
356 add< : { i : ℕ } (j : ℕ ) → i < suc i + j
|
|
|
357 add< {i} j = begin
|
|
|
358 suc i ≤⟨ m≤m+n (suc i) j ⟩
|
|
|
359 suc i + j ∎ where open ≤-Reasoning
|
|
|
360
|
|
|
361 findTest : {n m : Level} {A : Set n } {t : Set m }
|
|
|
362 → (key : ℕ)
|
|
|
363 → (tree0 : bt (Color ∧ A))
|
|
|
364 → RBtreeInvariant tree0
|
|
|
365 → (exit : (tree1 : bt (Color ∧ A))
|
|
|
366 → (stack : List (bt (Color ∧ A)))
|
|
|
367 → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
|
|
|
368 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t
|
|
|
369 findTest {n} {m} {A} {t} k tr0 rb0 exit = TerminatingLoopS (bt (Color ∧ A) ∧ List (bt (Color ∧ A))) {λ p → RBtreeInvariant (proj1 p) ∧ stackInvariant k (proj1 p) tr0 (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tr0 , tr0 ∷ [] ⟫ ⟪ rb0 , s-nil ⟫
|
|
|
370 $ λ p P loop → findRBT k (proj1 p) tr0 (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )
|
|
|
371 $ λ tr1 st P2 O → exit tr1 st P2 O
|
|
|
372
|
|
|
373 testRBTree0 : bt (Color ∧ ℕ)
|
|
|
374 testRBTree0 = node 8 ⟪ Black , 800 ⟫ (node 5 ⟪ Red , 500 ⟫ (node 2 ⟪ Black , 200 ⟫ leaf leaf) (node 6 ⟪ Black , 600 ⟫ leaf leaf)) (node 10 ⟪ Red , 1000 ⟫ (leaf) (node 15 ⟪ Black , 1500 ⟫ (node 14 ⟪ Red , 1400 ⟫ leaf leaf) leaf))
|
|
|
375 testRBTree : bt (Color ∧ ℕ)
|
|
|
376 testRBTree = node 10 ⟪ Red , 1000 ⟫ _ _
|
|
|
377
|
|
|
378 record result {n : Level} {A : Set n} {key : ℕ} {tree0 : bt (Color ∧ A)} : Set n where
|
|
|
379 field
|
|
|
380 tree : bt (Color ∧ A)
|
|
|
381 stack : List (bt (Color ∧ A))
|
|
|
382 ti : RBtreeInvariant tree
|
|
|
383 si : stackInvariant key tree tree0 stack
|
|
|
384
|
|
|
385 testRBI0 : RBtreeInvariant testRBTree0
|
|
|
386 testRBI0 = rb-node-black (add< 2) (add< 1) refl (rb-node-red (add< 2) (add< 0) refl (rb-single 2 200) (rb-single 6 600)) (rb-right-red (add< 4) refl (rb-left-black (add< 0) refl (rb-single 14 1400) ))
|
|
|
387
|
|
|
388 findRBTreeTest : result
|
|
|
389 findRBTreeTest = findTest 14 testRBTree0 testRBI0
|
|
|
390 $ λ tr s P O → (record {tree = tr ; stack = s ; ti = (proj1 P) ; si = (proj2 P)})
|
|
|
391
|
|
|
392
|
|
|
393 {-
|
|
781
|
394 data replacedRBTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt (Color ∧ A) ) → Set n where
|
|
|
395 rbr-leaf : {ca cb : Color} → replacedRBTree key value leaf (node key ⟪ cb , value ⟫ leaf leaf)
|
|
|
396 rbr-node : {value₁ : A} → {ca cb : Color } → {t t₁ : bt (Color ∧ A)}
|
|
|
397 → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ cb , value ⟫ t t₁)
|
|
|
398 rbr-right : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
|
|
|
399 → k < key → replacedRBTree key value t2 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t1 t)
|
|
|
400 rbr-left : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
|
|
|
401 → k < key → replacedRBTree key value t1 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2)
|
|
|
402
|
|
|
403 data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent uncle grand : bt A) → Set n where
|
|
|
404 s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
405 → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand
|
|
|
406 s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
407 → parent ≡ node kp vp n1 self → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand
|
|
|
408 s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
409 → parent ≡ node kp vp self n1 → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand
|
|
|
410 s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
411 → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand
|
|
|
412
|
|
|
413 record PG {n : Level } (A : Set n) (self : bt A) (stack : List (bt A)) : Set n where
|
|
|
414 field
|
|
|
415 parent grand uncle : bt A
|
|
|
416 pg : ParentGrand self parent uncle grand
|
|
|
417 rest : List (bt A)
|
|
|
418 stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest )
|
|
|
419
|
|
|
420 record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) : Set n where
|
|
|
421 field
|
|
|
422 od d rd : ℕ
|
|
|
423 tree rot : bt (Color ∧ A)
|
|
|
424 origti : treeInvariant orig
|
|
|
425 origrb : RBtreeInvariant orig
|
|
|
426 treerb : RBtreeInvariant tree
|
|
|
427 replrb : RBtreeInvariant repl
|
|
|
428 d=rd : ( d ≡ rd ) ∨ ((suc d ≡ rd ) ∧ (color tree ≡ Red))
|
|
|
429 si : stackInvariant key tree orig stack
|
|
|
430 rotated : rotatedTree tree rot
|
|
|
431 ri : replacedRBTree key value (child-replaced key rot ) repl
|
|
|
432
|
|
|
433
|
|
|
434 rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) )
|
|
|
435 → RBtreeInvariant parent
|
|
|
436 → RBtreeInvariant repl
|
|
|
437 → {left right : bt (Color ∧ A)} → parent ≡ node key ⟪ Black , value ⟫ left right
|
|
|
438 → (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl ) )
|
|
|
439 ∧ (color left ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) )
|
|
783
|
440 rbi-case1 {n} {A} {key} parent repl rbtip rbtir x = ⟪ {!!} , {!!} ⟫
|
|
781
|
441
|
|
802
|
442 blackdepth≡ : {n : Level } {A : Set n} → {C : Color} {key key1 : ℕ} {value value1 : A} → (tree1 tree2 : bt (Color ∧ A))
|
|
781
|
443 → RBtreeInvariant tree1
|
|
|
444 → RBtreeInvariant tree2
|
|
|
445 → RBtreeInvariant (node key ⟪ C , value ⟫ tree1 tree2)
|
|
|
446 → black-depth tree1 ≡ black-depth tree2
|
|
802
|
447 blackdepth≡ leaf leaf ri1 ri2 rip = refl
|
|
|
448 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
|
|
|
449 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) )
|
|
|
450 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
|
|
|
451 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
|
|
|
452 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
|
|
|
453 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
|
454
|
|
802
|
455 rb08 : {n : Level } {A : Set n}{key key1 : ℕ} {value value1 : A} {c c1 : Color} {t₁ t₂ t₃ t₄ : bt (Color ∧ A)}
|
|
|
456 → black-depth (node key ⟪ c , value ⟫ t₁ t₂) ≡ black-depth (node key1 ⟪ c1 , value1 ⟫ t₃ t₄)
|
|
|
457 rb08 = {!!}
|
|
783
|
458
|
|
|
459 {-
|
|
|
460 rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) )
|
|
|
461 → RBtreeInvariant parent
|
|
|
462 → RBtreeInvariant repl → (left right : bt (Color ∧ A)) → parent ≡ node key ⟪ Black , value ⟫ left right
|
|
781
|
463 → RBtreeInvariant left
|
|
|
464 → RBtreeInvariant right
|
|
783
|
465 → (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl ) ) ∧ (color left ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) )
|
|
|
466
|
|
|
467 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 = {!!}
|
|
|
468 -}
|
|
807
|
469
|
|
|
470 -}
|
