|
948
|
1 module RBTree0 where
|
|
|
2
|
|
|
3 open import Level hiding (suc ; zero ; _⊔_ )
|
|
|
4
|
|
|
5 open import Data.Nat hiding (compare)
|
|
|
6 open import Data.Nat.Properties as NatProp
|
|
|
7 open import Data.Maybe
|
|
|
8 -- open import Data.Maybe.Properties
|
|
|
9 open import Data.Empty
|
|
|
10 open import Data.List
|
|
|
11 open import Data.Product
|
|
|
12
|
|
|
13 open import Function as F hiding (const)
|
|
|
14
|
|
|
15 open import Relation.Binary
|
|
|
16 open import Relation.Binary.PropositionalEquality
|
|
|
17 open import Relation.Nullary
|
|
|
18 open import logic
|
|
|
19
|
|
|
20
|
|
|
21 --
|
|
|
22 --
|
|
|
23 -- no children , having left node , having right node , having both
|
|
|
24 --
|
|
|
25 data bt {n : Level} (A : Set n) : Set n where
|
|
|
26 leaf : bt A
|
|
|
27 node : (key : ℕ) → (value : A) →
|
|
|
28 (left : bt A ) → (right : bt A ) → bt A
|
|
|
29
|
|
|
30 node-key : {n : Level} {A : Set n} → bt A → Maybe ℕ
|
|
|
31 node-key (node key _ _ _) = just key
|
|
|
32 node-key _ = nothing
|
|
|
33
|
|
|
34 node-value : {n : Level} {A : Set n} → bt A → Maybe A
|
|
|
35 node-value (node _ value _ _) = just value
|
|
|
36 node-value _ = nothing
|
|
|
37
|
|
|
38 bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ
|
|
|
39 bt-depth leaf = 0
|
|
|
40 bt-depth (node key value t t₁) = suc (bt-depth t ⊔ bt-depth t₁ )
|
|
|
41
|
|
|
42 bt-ne : {n : Level} {A : Set n} {key : ℕ} {value : A} {t t₁ : bt A} → ¬ ( leaf ≡ node key value t t₁ )
|
|
|
43 bt-ne {n} {A} {key} {value} {t} {t₁} ()
|
|
|
44
|
|
|
45 open import Data.Unit hiding ( _≟_ ) -- ; _≤?_ ; _≤_)
|
|
|
46
|
|
|
47 tr< : {n : Level} {A : Set n} → (key : ℕ) → bt A → Set
|
|
|
48 tr< {_} {A} key leaf = ⊤
|
|
|
49 tr< {_} {A} key (node key₁ value tr tr₁) = (key₁ < key ) ∧ tr< key tr ∧ tr< key tr₁
|
|
|
50
|
|
|
51 tr> : {n : Level} {A : Set n} → (key : ℕ) → bt A → Set
|
|
|
52 tr> {_} {A} key leaf = ⊤
|
|
|
53 tr> {_} {A} key (node key₁ value tr tr₁) = (key < key₁ ) ∧ tr> key tr ∧ tr> key tr₁
|
|
|
54
|
|
|
55 --
|
|
|
56 --
|
|
|
57 data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
|
|
|
58 t-leaf : treeInvariant leaf
|
|
|
59 t-single : (key : ℕ) → (value : A) → treeInvariant (node key value leaf leaf)
|
|
|
60 t-right : (key key₁ : ℕ) → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁
|
|
|
61 → tr> key t₁
|
|
|
62 → tr> key t₂
|
|
|
63 → treeInvariant (node key₁ value₁ t₁ t₂)
|
|
|
64 → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂))
|
|
|
65 t-left : (key key₁ : ℕ) → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁
|
|
|
66 → tr< key₁ t₁
|
|
|
67 → tr< key₁ t₂
|
|
|
68 → treeInvariant (node key value t₁ t₂)
|
|
|
69 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf )
|
|
|
70 t-node : (key key₁ key₂ : ℕ) → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → key < key₁ → key₁ < key₂
|
|
|
71 → tr< key₁ t₁
|
|
|
72 → tr< key₁ t₂
|
|
|
73 → tr> key₁ t₃
|
|
|
74 → tr> key₁ t₄
|
|
|
75 → treeInvariant (node key value t₁ t₂)
|
|
|
76 → treeInvariant (node key₂ value₂ t₃ t₄)
|
|
|
77 → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄))
|
|
|
78
|
|
|
79 --
|
|
|
80 -- stack always contains original top at end (path of the tree)
|
|
|
81 --
|
|
|
82 data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (top orig : bt A) → (stack : List (bt A)) → Set n where
|
|
|
83 s-nil : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [])
|
|
|
84 s-right : (tree tree0 tree₁ : bt A) → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
|
|
|
85 → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
|
|
|
86 s-left : (tree₁ tree0 tree : bt A) → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)}
|
|
|
87 → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree₁ tree0 (tree₁ ∷ st)
|
|
|
88
|
|
|
89 add< : { i : ℕ } (j : ℕ ) → i < suc i + j
|
|
|
90 add< {i} j = begin
|
|
|
91 suc i ≤⟨ m≤m+n (suc i) j ⟩
|
|
|
92 suc i + j ∎ where open ≤-Reasoning
|
|
|
93
|
|
|
94 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
|
|
|
95 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
|
|
|
96 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
|
|
|
97 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
|
|
|
98
|
|
|
99 nat-<≡ : { x : ℕ } → x < x → ⊥
|
|
|
100 nat-<≡ (s≤s lt) = nat-<≡ lt
|
|
|
101
|
|
|
102 nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
|
|
|
103 nat-≡< refl lt = nat-<≡ lt
|
|
|
104
|
|
|
105 treeTest1 : bt ℕ
|
|
|
106 treeTest1 = node 0 0 leaf (node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf))
|
|
|
107 treeTest2 : bt ℕ
|
|
|
108 treeTest2 = node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf)
|
|
|
109
|
|
|
110 treeInvariantTest1 : treeInvariant treeTest1
|
|
|
111 treeInvariantTest1 = t-right _ _ (m≤m+n _ 2)
|
|
|
112 ⟪ add< _ , ⟪ ⟪ add< _ , _ ⟫ , _ ⟫ ⟫
|
|
|
113 ⟪ add< _ , ⟪ _ , _ ⟫ ⟫ (t-node _ _ _ (add< 0) (add< 1) ⟪ add< _ , ⟪ _ , _ ⟫ ⟫ _ _ _ (t-left _ _ (add< 0) _ _ (t-single 1 7)) (t-single 5 5) )
|
|
|
114
|
|
|
115 stack-top : {n : Level} {A : Set n} (stack : List (bt A)) → Maybe (bt A)
|
|
|
116 stack-top [] = nothing
|
|
|
117 stack-top (x ∷ s) = just x
|
|
|
118
|
|
|
119 stack-last : {n : Level} {A : Set n} (stack : List (bt A)) → Maybe (bt A)
|
|
|
120 stack-last [] = nothing
|
|
|
121 stack-last (x ∷ []) = just x
|
|
|
122 stack-last (x ∷ s) = stack-last s
|
|
|
123
|
|
|
124 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
|
|
|
125 stackInvariantTest1 = s-right _ _ _ (add< 3) (s-nil )
|
|
|
126
|
|
|
127 si-property0 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → {stack : List (bt A)} → stackInvariant key tree tree0 stack → ¬ ( stack ≡ [] )
|
|
|
128 si-property0 (s-nil ) ()
|
|
|
129 si-property0 (s-right _ _ _ x si) ()
|
|
|
130 si-property0 (s-left _ _ _ x si) ()
|
|
|
131
|
|
|
132 si-property1 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 tree1 : bt A} → {stack : List (bt A)} → stackInvariant key tree tree0 (tree1 ∷ stack)
|
|
|
133 → tree1 ≡ tree
|
|
|
134 si-property1 (s-nil ) = refl
|
|
|
135 si-property1 (s-right _ _ _ _ si) = refl
|
|
|
136 si-property1 (s-left _ _ _ _ si) = refl
|
|
|
137
|
|
|
138 si-property2 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 tree1 : bt A} → (stack : List (bt A)) → stackInvariant key tree tree0 (tree1 ∷ stack)
|
|
|
139 → ¬ ( just leaf ≡ stack-last stack )
|
|
|
140 si-property2 (.leaf ∷ []) (s-right _ _ tree₁ x ()) refl
|
|
|
141 si-property2 (x₁ ∷ x₂ ∷ stack) (s-right _ _ tree₁ x si) eq = si-property2 (x₂ ∷ stack) si eq
|
|
|
142 si-property2 (.leaf ∷ []) (s-left _ _ tree₁ x ()) refl
|
|
|
143 si-property2 (x₁ ∷ x₂ ∷ stack) (s-left _ _ tree₁ x si) eq = si-property2 (x₂ ∷ stack) si eq
|
|
|
144
|
|
|
145 si-property-< : {n : Level} {A : Set n} {key kp : ℕ} {value₂ : A} {tree orig tree₃ : bt A} → {stack : List (bt A)}
|
|
|
146 → ¬ ( tree ≡ leaf )
|
|
|
147 → treeInvariant (node kp value₂ tree tree₃ )
|
|
|
148 → stackInvariant key tree orig (tree ∷ node kp value₂ tree tree₃ ∷ stack)
|
|
|
149 → key < kp
|
|
|
150 si-property-< ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x s-nil) = ⊥-elim (nat-<> x₁ x₂)
|
|
|
151 si-property-< ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x (s-right .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree₁ x₇ si)) = ⊥-elim (nat-<> x₁ x₂)
|
|
|
152 si-property-< ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x (s-left .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree x₇ si)) = ⊥-elim (nat-<> x₁ x₂)
|
|
|
153 si-property-< ne ti (s-left _ _ _ x (s-right .(node _ _ _ _) _ tree₁ x₁ si)) = x
|
|
|
154 si-property-< ne ti (s-left _ _ _ x (s-left .(node _ _ _ _) _ tree₁ x₁ si)) = x
|
|
|
155 si-property-< ne ti (s-left _ _ _ x s-nil) = x
|
|
|
156 si-property-< ne (t-single _ _) (s-right _ _ tree₁ x si) = ⊥-elim ( ne refl )
|
|
|
157
|
|
|
158 si-property-> : {n : Level} {A : Set n} {key kp : ℕ} {value₂ : A} {tree orig tree₃ : bt A} → {stack : List (bt A)}
|
|
|
159 → ¬ ( tree ≡ leaf )
|
|
|
160 → treeInvariant (node kp value₂ tree₃ tree )
|
|
|
161 → stackInvariant key tree orig (tree ∷ node kp value₂ tree₃ tree ∷ stack)
|
|
|
162 → kp < key
|
|
|
163 si-property-> ne ti (s-right _ _ tree₁ x s-nil) = x
|
|
|
164 si-property-> ne ti (s-right _ _ tree₁ x (s-right .(node _ _ tree₁ _) _ tree₂ x₁ si)) = x
|
|
|
165 si-property-> ne ti (s-right _ _ tree₁ x (s-left .(node _ _ tree₁ _) _ tree x₁ si)) = x
|
|
|
166 si-property-> ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-left _ _ _ x s-nil) = ⊥-elim (nat-<> x₁ x₂)
|
|
|
167 si-property-> ne (t-node _ _ _ x₂ x₃ x₄ x₅ x₆ x₇ ti ti₁) (s-left _ _ _ x (s-right .(node _ _ _ _) _ tree₁ x₁ si)) = ⊥-elim (nat-<> x₂ x₃)
|
|
|
168 si-property-> ne (t-node _ _ _ x₂ x₃ x₄ x₅ x₆ x₇ ti ti₁) (s-left _ _ _ x (s-left .(node _ _ _ _) _ tree x₁ si)) = ⊥-elim (nat-<> x₂ x₃)
|
|
|
169 si-property-> ne (t-single _ _) (s-left _ _ _ x s-nil) = ⊥-elim ( ne refl )
|
|
|
170 si-property-> ne (t-single _ _) (s-left _ _ _ x (s-right .(node _ _ leaf leaf) _ tree₁ x₁ si)) = ⊥-elim ( ne refl )
|
|
|
171 si-property-> ne (t-single _ _) (s-left _ _ _ x (s-left .(node _ _ leaf leaf) _ tree x₁ si)) = ⊥-elim ( ne refl )
|
|
|
172
|
|
|
173 si-property-last : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → stackInvariant key tree tree0 stack
|
|
|
174 → stack-last stack ≡ just tree0
|
|
|
175 si-property-last key t t0 (t ∷ []) (s-nil ) = refl
|
|
|
176 si-property-last key t t0 (.t ∷ x ∷ st) (s-right _ _ _ _ si ) with si-property1 si
|
|
|
177 ... | refl = si-property-last key x t0 (x ∷ st) si
|
|
|
178 si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ _ _ _ si ) with si-property1 si
|
|
|
179 ... | refl = si-property-last key x t0 (x ∷ st) si
|
|
|
180
|
|
|
181 si-property-pne : {n : Level} {A : Set n} {key key₁ : ℕ} {value₁ : A} (tree orig : bt A) → {left right x : bt A} → (stack : List (bt A)) {rest : List (bt A)}
|
|
|
182 → stack ≡ x ∷ node key₁ value₁ left right ∷ rest
|
|
|
183 → stackInvariant key tree orig stack
|
|
|
184 → ¬ ( key ≡ key₁ )
|
|
|
185 si-property-pne tree orig .(tree ∷ node _ _ _ _ ∷ _) refl (s-right .tree .orig tree₁ x si) eq with si-property1 si
|
|
|
186 ... | refl = ⊥-elim ( nat-≡< (sym eq) x)
|
|
|
187 si-property-pne tree orig .(tree ∷ node _ _ _ _ ∷ _) refl (s-left .tree .orig tree₁ x si) eq with si-property1 si
|
|
|
188 ... | refl = ⊥-elim ( nat-≡< eq x)
|
|
|
189
|
|
|
190 si-property-parent-node : {n : Level} {A : Set n} {key : ℕ} (tree orig : bt A) {x : bt A}
|
|
|
191 → (stack : List (bt A)) {rest : List (bt A)}
|
|
|
192 → stackInvariant key tree orig stack
|
|
|
193 → ¬ ( stack ≡ x ∷ leaf ∷ rest )
|
|
|
194 si-property-parent-node {n} {A} tree orig .(tree ∷ leaf ∷ _) (s-right .tree .orig tree₁ x si) refl with si-property1 si
|
|
|
195 ... | ()
|
|
|
196 si-property-parent-node {n} {A} tree orig .(tree ∷ leaf ∷ _) (s-left .tree .orig tree₁ x si) refl with si-property1 si
|
|
|
197 ... | ()
|
|
|
198
|
|
|
199
|
|
|
200
|
|
|
201 open _∧_
|
|
|
202
|
|
|
203
|
|
|
204 depth-1< : {i j : ℕ} → suc i ≤ suc (i Data.Nat.⊔ j )
|
|
|
205 depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
|
|
|
206
|
|
|
207 depth-2< : {i j : ℕ} → suc i ≤ suc (j Data.Nat.⊔ i )
|
|
|
208 depth-2< {i} {j} = s≤s (m≤n⊔m j i)
|
|
|
209
|
|
|
210 depth-3< : {i : ℕ } → suc i ≤ suc (suc i)
|
|
|
211 depth-3< {zero} = s≤s ( z≤n )
|
|
|
212 depth-3< {suc i} = s≤s (depth-3< {i} )
|
|
|
213
|
|
|
214
|
|
|
215 treeLeftDown : {n : Level} {A : Set n} {k : ℕ} {v1 : A} → (tree tree₁ : bt A )
|
|
|
216 → treeInvariant (node k v1 tree tree₁)
|
|
|
217 → treeInvariant tree
|
|
|
218 treeLeftDown {n} {A} {_} {v1} leaf leaf (t-single k1 v1) = t-leaf
|
|
|
219 treeLeftDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right _ _ x _ _ ti) = t-leaf
|
|
|
220 treeLeftDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left _ _ x _ _ ti) = ti
|
|
|
221 treeLeftDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node _ _ _ x x₁ _ _ _ _ ti ti₁) = ti
|
|
|
222
|
|
|
223 treeRightDown : {n : Level} {A : Set n} {k : ℕ} {v1 : A} → (tree tree₁ : bt A )
|
|
|
224 → treeInvariant (node k v1 tree tree₁)
|
|
|
225 → treeInvariant tree₁
|
|
|
226 treeRightDown {n} {A} {_} {v1} .leaf .leaf (t-single _ .v1) = t-leaf
|
|
|
227 treeRightDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right _ _ x _ _ ti) = ti
|
|
|
228 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left _ _ x _ _ ti) = t-leaf
|
|
|
229 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node _ _ _ x x₁ _ _ _ _ ti ti₁) = ti₁
|
|
|
230
|
|
|
231 ti-property1 : {n : Level} {A : Set n} {key₁ : ℕ} {value₂ : A} {left right : bt A} → treeInvariant (node key₁ value₂ left right ) → tr< key₁ left ∧ tr> key₁ right
|
|
|
232 ti-property1 {n} {A} {key₁} {value₂} {.leaf} {.leaf} (t-single .key₁ .value₂) = ⟪ tt , tt ⟫
|
|
|
233 ti-property1 {n} {A} {key₁} {value₂} {.leaf} {.(node key₂ _ _ _)} (t-right .key₁ key₂ x x₁ x₂ t) = ⟪ tt , ⟪ x , ⟪ x₁ , x₂ ⟫ ⟫ ⟫
|
|
|
234 ti-property1 {n} {A} {key₁} {value₂} {.(node key _ _ _)} {.leaf} (t-left key .key₁ x x₁ x₂ t) = ⟪ ⟪ x , ⟪ x₁ , x₂ ⟫ ⟫ , tt ⟫
|
|
|
235 ti-property1 {n} {A} {key₁} {value₂} {.(node key _ _ _)} {.(node key₂ _ _ _)} (t-node key .key₁ key₂ x x₁ x₂ x₃ x₄ x₅ t t₁)
|
|
|
236 = ⟪ ⟪ x , ⟪ x₂ , x₃ ⟫ ⟫ , ⟪ x₁ , ⟪ x₄ , x₅ ⟫ ⟫ ⟫
|
|
|
237
|
|
|
238
|
|
|
239 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
|
|
|
240 → treeInvariant tree ∧ stackInvariant key tree tree0 stack
|
|
|
241 → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t )
|
|
|
242 → (exit : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
|
|
|
243 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t
|
|
|
244 findP key leaf tree0 st Pre _ exit = exit leaf st Pre (case1 refl)
|
|
|
245 findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁
|
|
|
246 findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl)
|
|
|
247 findP {n} {_} {A} key (node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree (tree ∷ st)
|
|
|
248 ⟪ treeLeftDown tree tree₁ (proj1 Pre) , findP1 a st (proj2 Pre) ⟫ depth-1< where
|
|
|
249 findP1 : key < key₁ → (st : List (bt A)) → stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
|
|
|
250 findP1 a (x ∷ st) si = s-left _ _ _ a si
|
|
|
251 findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right _ _ _ c (proj2 Pre) ⟫ depth-2<
|
|
|
252
|
|
|
253 replaceTree1 : {n : Level} {A : Set n} {t t₁ : bt A } → ( k : ℕ ) → (v1 value : A ) → treeInvariant (node k v1 t t₁) → treeInvariant (node k value t t₁)
|
|
|
254 replaceTree1 k v1 value (t-single .k .v1) = t-single k value
|
|
|
255 replaceTree1 k v1 value (t-right _ _ x a b t) = t-right _ _ x a b t
|
|
|
256 replaceTree1 k v1 value (t-left _ _ x a b t) = t-left _ _ x a b t
|
|
|
257 replaceTree1 k v1 value (t-node _ _ _ x x₁ a b c d t t₁) = t-node _ _ _ x x₁ a b c d t t₁
|
|
|
258
|
|
|
259 open import Relation.Binary.Definitions
|
|
|
260
|
|
|
261 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥
|
|
|
262 lemma3 refl ()
|
|
|
263 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
|
|
|
264 lemma5 (s≤s z≤n) ()
|
|
|
265 ¬x<x : {x : ℕ} → ¬ (x < x)
|
|
|
266 ¬x<x (s≤s lt) = ¬x<x lt
|
|
|
267
|
|
|
268 child-replaced : {n : Level} {A : Set n} (key : ℕ) (tree : bt A) → bt A
|
|
|
269 child-replaced key leaf = leaf
|
|
|
270 child-replaced key (node key₁ value left right) with <-cmp key key₁
|
|
|
271 ... | tri< a ¬b ¬c = left
|
|
|
272 ... | tri≈ ¬a b ¬c = node key₁ value left right
|
|
|
273 ... | tri> ¬a ¬b c = right
|
|
|
274
|
|
|
275 child-replaced-left : {n : Level} {A : Set n} {key key₁ : ℕ} {value : A} {left right : bt A}
|
|
|
276 → key < key₁
|
|
|
277 → child-replaced key (node key₁ value left right) ≡ left
|
|
|
278 child-replaced-left {n} {A} {key} {key₁} {value} {left} {right} lt = ch00 (node key₁ value left right) refl lt where
|
|
|
279 ch00 : (tree : bt A) → tree ≡ node key₁ value left right → key < key₁ → child-replaced key tree ≡ left
|
|
|
280 ch00 (node key₁ value tree tree₁) refl lt1 with <-cmp key key₁
|
|
|
281 ... | tri< a ¬b ¬c = refl
|
|
|
282 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a lt1)
|
|
|
283 ... | tri> ¬a ¬b c = ⊥-elim (¬a lt1)
|
|
|
284
|
|
|
285 child-replaced-right : {n : Level} {A : Set n} {key key₁ : ℕ} {value : A} {left right : bt A}
|
|
|
286 → key₁ < key
|
|
|
287 → child-replaced key (node key₁ value left right) ≡ right
|
|
|
288 child-replaced-right {n} {A} {key} {key₁} {value} {left} {right} lt = ch00 (node key₁ value left right) refl lt where
|
|
|
289 ch00 : (tree : bt A) → tree ≡ node key₁ value left right → key₁ < key → child-replaced key tree ≡ right
|
|
|
290 ch00 (node key₁ value tree tree₁) refl lt1 with <-cmp key key₁
|
|
|
291 ... | tri< a ¬b ¬c = ⊥-elim (¬c lt1)
|
|
|
292 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c lt1)
|
|
|
293 ... | tri> ¬a ¬b c = refl
|
|
|
294
|
|
|
295 child-replaced-eq : {n : Level} {A : Set n} {key key₁ : ℕ} {value : A} {left right : bt A}
|
|
|
296 → key₁ ≡ key
|
|
|
297 → child-replaced key (node key₁ value left right) ≡ node key₁ value left right
|
|
|
298 child-replaced-eq {n} {A} {key} {key₁} {value} {left} {right} lt = ch00 (node key₁ value left right) refl lt where
|
|
|
299 ch00 : (tree : bt A) → tree ≡ node key₁ value left right → key₁ ≡ key → child-replaced key tree ≡ node key₁ value left right
|
|
|
300 ch00 (node key₁ value tree tree₁) refl lt1 with <-cmp key key₁
|
|
|
301 ... | tri< a ¬b ¬c = ⊥-elim (¬b (sym lt1))
|
|
|
302 ... | tri≈ ¬a b ¬c = refl
|
|
|
303 ... | tri> ¬a ¬b c = ⊥-elim (¬b (sym lt1))
|
|
|
304
|
|
|
305 record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where
|
|
|
306 field
|
|
|
307 tree0 : bt A
|
|
|
308 ti : treeInvariant tree0
|
|
|
309 si : stackInvariant key tree tree0 stack
|
|
|
310 ci : C tree repl stack -- data continuation
|
|
|
311
|
|
|
312 record replacePR' {n : Level} {A : Set n} (key : ℕ) (value : A) (orig : bt A ) (stack : List (bt A)) : Set n where
|
|
|
313 field
|
|
|
314 tree repl : bt A
|
|
|
315 ti : treeInvariant orig
|
|
|
316 si : stackInvariant key tree orig stack
|
|
|
317 -- treeInvariant of tree and repl is inferred from ti, si and ri.
|
|
|
318
|
|
|
319 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
|
|
|
320 → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key )
|
|
|
321 → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → t) → t
|
|
|
322 replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 )
|
|
|
323 replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P) where
|
|
|
324 repl00 : node k value t t₁ ≡ child-replaced k (node k value t t₁)
|
|
|
325 repl00 with <-cmp k k
|
|
|
326 ... | tri< a ¬b ¬c = ⊥-elim (¬b refl)
|
|
|
327 ... | tri≈ ¬a b ¬c = refl
|
|
|
328 ... | tri> ¬a ¬b c = ⊥-elim (¬b refl)
|
|
|
329
|
|
|
330 replaceP : {n m : Level} {A : Set n} {t : Set m}
|
|
|
331 → (key : ℕ) → (value : A) → {tree : bt A} ( repl : bt A)
|
|
|
332 → (stack : List (bt A)) → replacePR key value tree repl stack (λ _ _ _ → Lift n ⊤)
|
|
|
333 → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A))
|
|
|
334 → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t)
|
|
|
335 → (exit : (tree1 repl : bt A) → t) → t
|
|
|
336 replaceP key value {tree} repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen
|
|
|
337 replaceP key value {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ (replacePR.si Pre)-- tree0 ≡ leaf
|
|
|
338 ... | refl = exit (replacePR.tree0 Pre) (node key value leaf leaf)
|
|
|
339 replaceP key value {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁
|
|
|
340 ... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) (node key₁ value₁ repl right )
|
|
|
341 ... | tri≈ ¬a b ¬c = exit (replacePR.tree0 Pre) repl
|
|
|
342 ... | tri> ¬a ¬b c = exit (replacePR.tree0 Pre) (node key₁ value₁ left repl )
|
|
|
343 replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(tree1 ∷ st1)) Pre next exit = next key value repl st Post ≤-refl where
|
|
|
344 Post : replacePR key value tree1 repl (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤)
|
|
|
345 Post with replacePR.si Pre
|
|
|
346 ... | s-right _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ci = lift tt } where
|
|
|
347 repl09 : tree1 ≡ node key₂ v1 tree₁ leaf
|
|
|
348 repl09 = si-property1 si
|
|
|
349 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
|
|
|
350 repl10 with si-property1 si
|
|
|
351 ... | refl = si
|
|
|
352 repl07 : child-replaced key (node key₂ v1 tree₁ leaf) ≡ leaf
|
|
|
353 repl07 with <-cmp key key₂
|
|
|
354 ... | tri< a ¬b ¬c = ⊥-elim (¬c x)
|
|
|
355 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x)
|
|
|
356 ... | tri> ¬a ¬b c = refl
|
|
|
357 ... | s-left _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ci = lift tt } where
|
|
|
358 repl09 : tree1 ≡ node key₂ v1 leaf tree₁
|
|
|
359 repl09 = si-property1 si
|
|
|
360 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
|
|
|
361 repl10 with si-property1 si
|
|
|
362 ... | refl = si
|
|
|
363 repl07 : child-replaced key (node key₂ v1 leaf tree₁ ) ≡ leaf
|
|
|
364 repl07 with <-cmp key key₂
|
|
|
365 ... | tri< a ¬b ¬c = refl
|
|
|
366 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a x)
|
|
|
367 ... | tri> ¬a ¬b c = ⊥-elim (¬a x)
|
|
|
368 replaceP {n} {_} {A} key value {tree} repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁
|
|
|
369 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st Post ≤-refl where
|
|
|
370 Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤)
|
|
|
371 Post with replacePR.si Pre
|
|
|
372 ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ci = lift tt } where
|
|
|
373 repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right)
|
|
|
374 repl09 = si-property1 si
|
|
|
375 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
|
|
|
376 repl10 with si-property1 si
|
|
|
377 ... | refl = si
|
|
|
378 repl03 : child-replaced key (node key₁ value₁ left right) ≡ left
|
|
|
379 repl03 with <-cmp key key₁
|
|
|
380 ... | tri< a1 ¬b ¬c = refl
|
|
|
381 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a)
|
|
|
382 ... | tri> ¬a ¬b c = ⊥-elim (¬a a)
|
|
|
383 repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right
|
|
|
384 repl02 with repl09 | <-cmp key key₂
|
|
|
385 ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt)
|
|
|
386 ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt)
|
|
|
387 ... | refl | tri> ¬a ¬b c = refl
|
|
|
388 repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1
|
|
|
389 repl04 = begin
|
|
|
390 node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03 ⟩
|
|
|
391 node key₁ value₁ left right ≡⟨ sym repl02 ⟩
|
|
|
392 child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
|
|
|
393 child-replaced key tree1 ∎ where open ≡-Reasoning
|
|
|
394 ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ci = lift tt } where
|
|
|
395 repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁
|
|
|
396 repl09 = si-property1 si
|
|
|
397 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
|
|
|
398 repl10 with si-property1 si
|
|
|
399 ... | refl = si
|
|
|
400 repl03 : child-replaced key (node key₁ value₁ left right) ≡ left
|
|
|
401 repl03 with <-cmp key key₁
|
|
|
402 ... | tri< a1 ¬b ¬c = refl
|
|
|
403 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a)
|
|
|
404 ... | tri> ¬a ¬b c = ⊥-elim (¬a a)
|
|
|
405 repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right
|
|
|
406 repl02 with repl09 | <-cmp key key₂
|
|
|
407 ... | refl | tri< a ¬b ¬c = refl
|
|
|
408 ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt)
|
|
|
409 ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt)
|
|
|
410 repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1
|
|
|
411 repl04 = begin
|
|
|
412 node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03 ⟩
|
|
|
413 node key₁ value₁ left right ≡⟨ sym repl02 ⟩
|
|
|
414 child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
|
|
|
415 child-replaced key tree1 ∎ where open ≡-Reasoning
|
|
|
416 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st Post ≤-refl where
|
|
|
417 Post : replacePR key value tree1 (node key₁ value left right ) (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤)
|
|
|
418 Post with replacePR.si Pre
|
|
|
419 ... | s-right _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ci = lift tt } where
|
|
|
420 repl09 : tree1 ≡ node key₂ v1 tree₁ tree -- (node key₁ value₁ left right)
|
|
|
421 repl09 = si-property1 si
|
|
|
422 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
|
|
|
423 repl10 with si-property1 si
|
|
|
424 ... | refl = si
|
|
|
425 repl07 : child-replaced key (node key₂ v1 tree₁ tree) ≡ tree
|
|
|
426 repl07 with <-cmp key key₂
|
|
|
427 ... | tri< a ¬b ¬c = ⊥-elim (¬c x)
|
|
|
428 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x)
|
|
|
429 ... | tri> ¬a ¬b c = refl
|
|
|
430 ... | s-left _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ci = lift tt } where
|
|
|
431 repl09 : tree1 ≡ node key₂ v1 tree tree₁
|
|
|
432 repl09 = si-property1 si
|
|
|
433 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
|
|
|
434 repl10 with si-property1 si
|
|
|
435 ... | refl = si
|
|
|
436 repl07 : child-replaced key (node key₂ v1 tree tree₁ ) ≡ tree
|
|
|
437 repl07 with <-cmp key key₂
|
|
|
438 ... | tri< a ¬b ¬c = refl
|
|
|
439 ... | tri≈ ¬a b ¬c = ⊥-elim (¬a x)
|
|
|
440 ... | tri> ¬a ¬b c = ⊥-elim (¬a x)
|
|
|
441 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st Post ≤-refl where
|
|
|
442 Post : replacePR key value tree1 (node key₁ value₁ left repl ) st (λ _ _ _ → Lift n ⊤)
|
|
|
443 Post with replacePR.si Pre
|
|
|
444 ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ci = lift tt } where
|
|
|
445 repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right)
|
|
|
446 repl09 = si-property1 si
|
|
|
447 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
|
|
|
448 repl10 with si-property1 si
|
|
|
449 ... | refl = si
|
|
|
450 repl03 : child-replaced key (node key₁ value₁ left right) ≡ right
|
|
|
451 repl03 with <-cmp key key₁
|
|
|
452 ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c)
|
|
|
453 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c)
|
|
|
454 ... | tri> ¬a ¬b c = refl
|
|
|
455 repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right
|
|
|
456 repl02 with repl09 | <-cmp key key₂
|
|
|
457 ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt)
|
|
|
458 ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt)
|
|
|
459 ... | refl | tri> ¬a ¬b c = refl
|
|
|
460 repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1
|
|
|
461 repl04 = begin
|
|
|
462 node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩
|
|
|
463 node key₁ value₁ left right ≡⟨ sym repl02 ⟩
|
|
|
464 child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
|
|
|
465 child-replaced key tree1 ∎ where open ≡-Reasoning
|
|
|
466 ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ci = lift tt } where
|
|
|
467 repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁
|
|
|
468 repl09 = si-property1 si
|
|
|
469 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
|
|
|
470 repl10 with si-property1 si
|
|
|
471 ... | refl = si
|
|
|
472 repl03 : child-replaced key (node key₁ value₁ left right) ≡ right
|
|
|
473 repl03 with <-cmp key key₁
|
|
|
474 ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c)
|
|
|
475 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c)
|
|
|
476 ... | tri> ¬a ¬b c = refl
|
|
|
477 repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right
|
|
|
478 repl02 with repl09 | <-cmp key key₂
|
|
|
479 ... | refl | tri< a ¬b ¬c = refl
|
|
|
480 ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt)
|
|
|
481 ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt)
|
|
|
482 repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1
|
|
|
483 repl04 = begin
|
|
|
484 node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩
|
|
|
485 node key₁ value₁ left right ≡⟨ sym repl02 ⟩
|
|
|
486 child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
|
|
|
487 child-replaced key tree1 ∎ where open ≡-Reasoning
|
|
|
488
|
|
|
489 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
|
|
|
490 → (r : Index) → (p : Invraiant r)
|
|
|
491 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t
|
|
|
492 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r)
|
|
|
493 ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) )
|
|
|
494 ... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (m≤n⇒m≤1+n lt1) p1 lt1 ) where
|
|
|
495 TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t
|
|
|
496 TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1))
|
|
|
497 TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j)
|
|
|
498 ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt
|
|
|
499 ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 )
|
|
|
500 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j )
|
|
|
501
|
|
|
502 open _∧_
|
|
|
503
|
|
|
504
|
|
|
505 insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree
|
|
|
506 → (exit : (tree repl : bt A) → treeInvariant repl → t ) → t
|
|
|
507 insertTreeP {n} {m} {A} {t} tree key value ti exit = ?
|
|
|
508 -- TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , tree ∷ [] ⟫ ⟪ ? , s-nil ⟫
|
|
|
509 -- $ λ p P loop → findP key (proj1 p) tree (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )
|
|
|
510 -- $ λ t s P C → replaceNodeP key value t C (proj1 P)
|
|
|
511 -- $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ bt A ∧ bt A )
|
|
|
512 -- {λ p → replacePR key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) (λ _ _ _ → Lift n ⊤ ) }
|
|
|
513 -- (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = ? ; si = proj2 P ; ri = R ; ci = lift tt }
|
|
|
514 -- $ λ p P1 loop → replaceP key value (proj2 (proj2 p)) (proj1 p) P1
|
|
|
515 -- (λ key value {tree1} repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ P2 lt )
|
|
|
516 -- $ λ tree repl P → exit tree repl ?
|
|
|
517 --
|
|
|
518 insertTestP1 = insertTreeP leaf 1 1 t-leaf
|
|
|
519 $ λ _ x0 P0 → insertTreeP x0 2 1 ?
|
|
|
520 $ λ _ x1 P1 → insertTreeP x1 3 2 ?
|
|
|
521 $ λ _ x2 P2 → insertTreeP x2 2 2 ? (λ _ x P → x )
|
|
|
522
|
|
|
523 top-value : {n : Level} {A : Set n} → (tree : bt A) → Maybe A
|
|
|
524 top-value leaf = nothing
|
|
|
525 top-value (node key value tree tree₁) = just value
|
|
|
526
|
|
|
527 -- is realy inserted?
|
|
|
528
|
|
|
529 -- other element is preserved?
|
|
|
530
|
|
|
531 -- deletion?
|
|
|
532
|
|
|
533
|
|
|
534 data Color : Set where
|
|
|
535 Red : Color
|
|
|
536 Black : Color
|
|
|
537
|
|
|
538 RB→bt : {n : Level} (A : Set n) → (bt (Color ∧ A)) → bt A
|
|
|
539 RB→bt {n} A leaf = leaf
|
|
|
540 RB→bt {n} A (node key ⟪ C , value ⟫ tr t1) = (node key value (RB→bt A tr) (RB→bt A t1))
|
|
|
541
|
|
|
542 color : {n : Level} {A : Set n} → (bt (Color ∧ A)) → Color
|
|
|
543 color leaf = Black
|
|
|
544 color (node key ⟪ C , value ⟫ rb rb₁) = C
|
|
|
545
|
|
|
546 to-red : {n : Level} {A : Set n} → (tree : bt (Color ∧ A)) → bt (Color ∧ A)
|
|
|
547 to-red leaf = leaf
|
|
|
548 to-red (node key ⟪ _ , value ⟫ t t₁) = (node key ⟪ Red , value ⟫ t t₁)
|
|
|
549
|
|
|
550 to-black : {n : Level} {A : Set n} → (tree : bt (Color ∧ A)) → bt (Color ∧ A)
|
|
|
551 to-black leaf = leaf
|
|
|
552 to-black (node key ⟪ _ , value ⟫ t t₁) = (node key ⟪ Black , value ⟫ t t₁)
|
|
|
553
|
|
|
554 black-depth : {n : Level} {A : Set n} → (tree : bt (Color ∧ A) ) → ℕ
|
|
|
555 black-depth leaf = 1
|
|
|
556 black-depth (node key ⟪ Red , value ⟫ t t₁) = black-depth t ⊔ black-depth t₁
|
|
|
557 black-depth (node key ⟪ Black , value ⟫ t t₁) = suc (black-depth t ⊔ black-depth t₁ )
|
|
|
558
|
|
|
559 zero≢suc : { m : ℕ } → zero ≡ suc m → ⊥
|
|
|
560 zero≢suc ()
|
|
|
561 suc≢zero : {m : ℕ } → suc m ≡ zero → ⊥
|
|
|
562 suc≢zero ()
|
|
|
563
|
|
|
564 data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where
|
|
|
565 rb-leaf : RBtreeInvariant leaf
|
|
|
566 rb-red : (key : ℕ) → (value : A) → {left right : bt (Color ∧ A)}
|
|
|
567 → color left ≡ Black → color right ≡ Black
|
|
|
568 → black-depth left ≡ black-depth right
|
|
|
569 → RBtreeInvariant left → RBtreeInvariant right
|
|
|
570 → RBtreeInvariant (node key ⟪ Red , value ⟫ left right)
|
|
|
571 rb-black : (key : ℕ) → (value : A) → {left right : bt (Color ∧ A)}
|
|
|
572 → black-depth left ≡ black-depth right
|
|
|
573 → RBtreeInvariant left → RBtreeInvariant right
|
|
|
574 → RBtreeInvariant (node key ⟪ Black , value ⟫ left right)
|
|
|
575
|
|
|
576 RightDown : {n : Level} {A : Set n} → bt (Color ∧ A) → bt (Color ∧ A)
|
|
|
577 RightDown leaf = leaf
|
|
|
578 RightDown (node key ⟪ c , value ⟫ t1 t2) = t2
|
|
|
579 LeftDown : {n : Level} {A : Set n} → bt (Color ∧ A) → bt (Color ∧ A)
|
|
|
580 LeftDown leaf = leaf
|
|
|
581 LeftDown (node key ⟪ c , value ⟫ t1 t2 ) = t1
|
|
|
582
|
|
|
583 RBtreeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color}
|
|
|
584 → (left right : bt (Color ∧ A))
|
|
|
585 → RBtreeInvariant (node key ⟪ c , value ⟫ left right)
|
|
|
586 → RBtreeInvariant left
|
|
|
587 RBtreeLeftDown left right (rb-red _ _ x x₁ x₂ rb rb₁) = rb
|
|
|
588 RBtreeLeftDown left right (rb-black _ _ x rb rb₁) = rb
|
|
|
589
|
|
|
590
|
|
|
591 RBtreeRightDown : {n : Level} {A : Set n} { key : ℕ} {value : A} {c : Color}
|
|
|
592 → (left right : bt (Color ∧ A))
|
|
|
593 → RBtreeInvariant (node key ⟪ c , value ⟫ left right)
|
|
|
594 → RBtreeInvariant right
|
|
|
595 RBtreeRightDown left right (rb-red _ _ x x₁ x₂ rb rb₁) = rb₁
|
|
|
596 RBtreeRightDown left right (rb-black _ _ x rb rb₁) = rb₁
|
|
|
597
|
|
|
598 RBtreeEQ : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color}
|
|
|
599 → {left right : bt (Color ∧ A)}
|
|
|
600 → RBtreeInvariant (node key ⟪ c , value ⟫ left right)
|
|
|
601 → black-depth left ≡ black-depth right
|
|
|
602 RBtreeEQ (rb-red _ _ x x₁ x₂ rb rb₁) = x₂
|
|
|
603 RBtreeEQ (rb-black _ _ x rb rb₁) = x
|
|
|
604
|
|
|
605 RBtreeToBlack : {n : Level} {A : Set n}
|
|
|
606 → (tree : bt (Color ∧ A))
|
|
|
607 → RBtreeInvariant tree
|
|
|
608 → RBtreeInvariant (to-black tree)
|
|
|
609 RBtreeToBlack leaf rb-leaf = rb-leaf
|
|
|
610 RBtreeToBlack (node key ⟪ Red , value ⟫ left right) (rb-red _ _ x x₁ x₂ rb rb₁) = rb-black key value x₂ rb rb₁
|
|
|
611 RBtreeToBlack (node key ⟪ Black , value ⟫ left right) (rb-black _ _ x rb rb₁) = rb-black key value x rb rb₁
|
|
|
612
|
|
|
613 RBtreeToBlackColor : {n : Level} {A : Set n}
|
|
|
614 → (tree : bt (Color ∧ A))
|
|
|
615 → RBtreeInvariant tree
|
|
|
616 → color (to-black tree) ≡ Black
|
|
|
617 RBtreeToBlackColor leaf rb-leaf = refl
|
|
|
618 RBtreeToBlackColor (node key ⟪ Red , value ⟫ left right) (rb-red _ _ x x₁ x₂ rb rb₁) = refl
|
|
|
619 RBtreeToBlackColor (node key ⟪ Black , value ⟫ left right) (rb-black _ _ x rb rb₁) = refl
|
|
|
620
|
|
|
621 RBtreeParentColorBlack : {n : Level} {A : Set n} → (left right : bt (Color ∧ A)) { value : A} {key : ℕ} { c : Color}
|
|
|
622 → RBtreeInvariant (node key ⟪ c , value ⟫ left right)
|
|
|
623 → (color left ≡ Red) ∨ (color right ≡ Red)
|
|
|
624 → c ≡ Black
|
|
|
625 RBtreeParentColorBlack leaf leaf (rb-red _ _ x₁ x₂ x₃ x₄ x₅) (case1 ())
|
|
|
626 RBtreeParentColorBlack leaf leaf (rb-red _ _ x₁ x₂ x₃ x₄ x₅) (case2 ())
|
|
|
627 RBtreeParentColorBlack (node key ⟪ Red , proj4 ⟫ left left₁) right (rb-red _ _ () x₁ x₂ rb rb₁) (case1 x₃)
|
|
|
628 RBtreeParentColorBlack (node key ⟪ Black , proj4 ⟫ left left₁) right (rb-red _ _ x x₁ x₂ rb rb₁) (case1 ())
|
|
|
629 RBtreeParentColorBlack left (node key ⟪ Red , proj4 ⟫ right right₁) (rb-red _ _ x () x₂ rb rb₁) (case2 x₃)
|
|
|
630 RBtreeParentColorBlack left (node key ⟪ Black , proj4 ⟫ right right₁) (rb-red _ _ x x₁ x₂ rb rb₁) (case2 ())
|
|
|
631 RBtreeParentColorBlack left right (rb-black _ _ x rb rb₁) x₃ = refl
|
|
|
632
|
|
|
633 RBtreeChildrenColorBlack : {n : Level} {A : Set n} → (left right : bt (Color ∧ A)) { value : Color ∧ A} {key : ℕ}
|
|
|
634 → RBtreeInvariant (node key value left right)
|
|
|
635 → proj1 value ≡ Red
|
|
|
636 → (color left ≡ Black) ∧ (color right ≡ Black)
|
|
|
637 RBtreeChildrenColorBlack left right (rb-red _ _ x x₁ x₂ rbi rbi₁) refl = ⟪ x , x₁ ⟫
|
|
|
638
|
|
|
639 --
|
|
|
640 -- findRBT exit with replaced node
|
|
|
641 -- case-eq node value is replaced, just do replacedTree and rebuild rb-invariant
|
|
|
642 -- case-leaf insert new single node
|
|
|
643 -- case1 if parent node is black, just do replacedTree and rebuild rb-invariant
|
|
|
644 -- case2 if parent node is red, increase blackdepth, do rotatation
|
|
|
645 --
|
|
|
646
|
|
|
647 findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) )
|
|
|
648 → (stack : List (bt (Color ∧ A)))
|
|
|
649 → RBtreeInvariant tree ∧ stackInvariant key tree tree0 stack
|
|
|
650 → (next : (tree1 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A)))
|
|
|
651 → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
|
|
|
652 → bt-depth tree1 < bt-depth tree → t )
|
|
|
653 → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A)))
|
|
|
654 → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
|
|
|
655 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t
|
|
|
656 findRBT key leaf tree0 stack rb0 next exit = exit leaf stack rb0 (case1 refl)
|
|
|
657 findRBT key (node key₁ value left right) tree0 stack rb0 next exit with <-cmp key key₁
|
|
|
658 findRBT key (node key₁ value left right) tree0 stack rb0 next exit | tri< a ¬b ¬c
|
|
|
659 = next left (left ∷ stack) ⟪ RBtreeLeftDown left right (_∧_.proj1 rb0) , s-left _ _ _ a (_∧_.proj2 rb0) ⟫ depth-1<
|
|
|
660 findRBT key n tree0 stack rb0 _ exit | tri≈ ¬a refl ¬c = exit n stack rb0 (case2 refl)
|
|
|
661 findRBT key (node key₁ value left right) tree0 stack rb0 next exit | tri> ¬a ¬b c
|
|
|
662 = next right (right ∷ stack) ⟪ RBtreeRightDown left right (_∧_.proj1 rb0), s-right _ _ _ c (_∧_.proj2 rb0) ⟫ depth-2<
|
|
|
663
|
|
|
664
|
|
|
665
|
|
|
666 findTest : {n m : Level} {A : Set n } {t : Set m }
|
|
|
667 → (key : ℕ)
|
|
|
668 → (tree0 : bt (Color ∧ A))
|
|
|
669 → RBtreeInvariant tree0
|
|
|
670 → (exit : (tree1 : bt (Color ∧ A))
|
|
|
671 → (stack : List (bt (Color ∧ A)))
|
|
|
672 → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
|
|
|
673 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t
|
|
|
674 findTest {n} {m} {A} {t} k tr0 rb0 exit = TerminatingLoopS (bt (Color ∧ A) ∧ List (bt (Color ∧ A)))
|
|
|
675 {λ p → RBtreeInvariant (proj1 p) ∧ stackInvariant k (proj1 p) tr0 (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tr0 , tr0 ∷ [] ⟫ ⟪ rb0 , s-nil ⟫
|
|
|
676 $ λ p RBP loop → findRBT k (proj1 p) tr0 (proj2 p) RBP (λ t1 s1 P2 lt1 → loop ⟪ t1 , s1 ⟫ P2 lt1 )
|
|
|
677 $ λ tr1 st P2 O → exit tr1 st P2 O
|
|
|
678
|
|
|
679
|
|
|
680 testRBTree0 : bt (Color ∧ ℕ)
|
|
|
681 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))
|
|
|
682
|
|
|
683 -- testRBI0 : RBtreeInvariant testRBTree0
|
|
|
684 -- 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) ))
|
|
|
685
|
|
|
686 -- findRBTreeTest : result
|
|
|
687 -- findRBTreeTest = findTest 14 testRBTree0 testRBI0
|
|
|
688 -- $ λ tr s P O → (record {tree = tr ; stack = s ; ti = (proj1 P) ; si = (proj2 P)})
|
|
|
689
|
|
|
690 -- create replaceRBTree with rotate
|
|
|
691
|
|
|
692
|
|
|
693 --
|
|
|
694 -- Parent Grand Relation
|
|
|
695 -- should we require stack-invariant?
|
|
|
696 --
|
|
|
697
|
|
|
698 data ParentGrand {n : Level} {A : Set n} (key : ℕ) (self : bt A) : (parent uncle grand : bt A) → Set n where
|
|
|
699 s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
700 → key < kp → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand key self parent n2 grand
|
|
|
701 s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
702 → kp < key → parent ≡ node kp vp n1 self → grand ≡ node kg vg parent n2 → ParentGrand key self parent n2 grand
|
|
|
703 s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
704 → key < kp → parent ≡ node kp vp self n1 → grand ≡ node kg vg n2 parent → ParentGrand key self parent n2 grand
|
|
|
705 s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
|
|
|
706 → kp < key → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand key self parent n2 grand
|
|
|
707
|
|
|
708 record PG {n : Level } (A : Set n) (key : ℕ) (self : bt A) (stack : List (bt A)) : Set n where
|
|
|
709 field
|
|
|
710 parent grand uncle : bt A
|
|
|
711 pg : ParentGrand key self parent uncle grand
|
|
|
712 rest : List (bt A)
|
|
|
713 stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest )
|
|
|
714
|
|
|
715 --
|
|
|
716 -- RBI : Invariant on InsertCase2
|
|
|
717 -- color repl ≡ Red ∧ black-depth repl ≡ suc (black-depth tree)
|
|
|
718 --
|
|
|
719
|
|
|
720 data RBI-state {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree repl : bt (Color ∧ A) ) → (stak : List (bt (Color ∧ A))) → Set n where
|
|
|
721 rebuild : {tree repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → color tree ≡ color repl → black-depth repl ≡ black-depth tree
|
|
|
722 → ¬ ( tree ≡ leaf)
|
|
|
723 → RBI-state key value tree repl stack -- one stage up
|
|
|
724 rotate : (tree : bt (Color ∧ A)) → {repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → color repl ≡ Red
|
|
|
725 → RBI-state key value tree repl stack -- two stages up
|
|
|
726 top-black : {tree repl : bt (Color ∧ A) } → {stack : List (bt (Color ∧ A))} → stack ≡ tree ∷ []
|
|
|
727 → RBI-state key value tree repl stack
|
|
|
728
|
|
|
729 record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) : Set n where
|
|
|
730 field
|
|
|
731 tree repl : bt (Color ∧ A)
|
|
|
732 origti : treeInvariant orig
|
|
|
733 origrb : RBtreeInvariant orig
|
|
|
734 treerb : RBtreeInvariant tree -- tree node te be replaced
|
|
|
735 replrb : RBtreeInvariant repl
|
|
|
736 si : stackInvariant key tree orig stack
|
|
|
737 state : RBI-state key value tree repl stack
|
|
|
738
|
|
|
739 tr>-to-black : {n : Level} {A : Set n} {key : ℕ} {tree : bt (Color ∧ A)} → tr> key tree → tr> key (to-black tree)
|
|
|
740 tr>-to-black {n} {A} {key} {leaf} tr = tt
|
|
|
741 tr>-to-black {n} {A} {key} {node key₁ value tree tree₁} tr = tr
|
|
|
742
|
|
|
743 tr<-to-black : {n : Level} {A : Set n} {key : ℕ} {tree : bt (Color ∧ A)} → tr< key tree → tr< key (to-black tree)
|
|
|
744 tr<-to-black {n} {A} {key} {leaf} tr = tt
|
|
|
745 tr<-to-black {n} {A} {key} {node key₁ value tree tree₁} tr = tr
|
|
|
746
|
|
|
747 to-black-eq : {n : Level} {A : Set n} (tree : bt (Color ∧ A)) → color tree ≡ Red → suc (black-depth tree) ≡ black-depth (to-black tree)
|
|
|
748 to-black-eq {n} {A} (leaf) ()
|
|
|
749 to-black-eq {n} {A} (node key₁ ⟪ Red , proj4 ⟫ tree tree₁) eq = refl
|
|
|
750 to-black-eq {n} {A} (node key₁ ⟪ Black , proj4 ⟫ tree tree₁) ()
|
|
|
751
|
|
|
752 red-children-eq : {n : Level} {A : Set n} {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color}
|
|
|
753 → tree ≡ node key ⟪ c , value ⟫ left right
|
|
|
754 → c ≡ Red
|
|
|
755 → RBtreeInvariant tree
|
|
|
756 → (black-depth tree ≡ black-depth left ) ∧ (black-depth tree ≡ black-depth right)
|
|
|
757 red-children-eq {n} {A} {.(node key₁ ⟪ Red , value₁ ⟫ left right)} {left} {right} {.key₁} {.value₁} {Red} refl eq₁ rb2@(rb-red key₁ value₁ x x₁ x₂ rb rb₁) =
|
|
|
758 ⟪ ( begin
|
|
|
759 black-depth left ⊔ black-depth right ≡⟨ cong (λ k → black-depth left ⊔ k) (sym (RBtreeEQ rb2)) ⟩
|
|
|
760 black-depth left ⊔ black-depth left ≡⟨ ⊔-idem _ ⟩
|
|
|
761 black-depth left ∎ ) , (
|
|
|
762 begin
|
|
|
763 black-depth left ⊔ black-depth right ≡⟨ cong (λ k → k ⊔ black-depth right ) (RBtreeEQ rb2) ⟩
|
|
|
764 black-depth right ⊔ black-depth right ≡⟨ ⊔-idem _ ⟩
|
|
|
765 black-depth right ∎ ) ⟫ where open ≡-Reasoning
|
|
|
766 red-children-eq {n} {A} {tree} {left} {right} {key} {value} {Black} eq () rb
|
|
|
767
|
|
|
768 black-children-eq : {n : Level} {A : Set n} {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color}
|
|
|
769 → tree ≡ node key ⟪ c , value ⟫ left right
|
|
|
770 → c ≡ Black
|
|
|
771 → RBtreeInvariant tree
|
|
|
772 → (black-depth tree ≡ suc (black-depth left) ) ∧ (black-depth tree ≡ suc (black-depth right))
|
|
|
773 black-children-eq {n} {A} {.(node key₁ ⟪ Black , value₁ ⟫ left right)} {left} {right} {.key₁} {.value₁} {Black} refl eq₁ rb2@(rb-black key₁ value₁ x rb rb₁) =
|
|
|
774 ⟪ ( begin
|
|
|
775 suc (black-depth left ⊔ black-depth right) ≡⟨ cong (λ k → suc (black-depth left ⊔ k)) (sym (RBtreeEQ rb2)) ⟩
|
|
|
776 suc (black-depth left ⊔ black-depth left) ≡⟨ ⊔-idem _ ⟩
|
|
|
777 suc (black-depth left) ∎ ) , (
|
|
|
778 begin
|
|
|
779 suc (black-depth left ⊔ black-depth right) ≡⟨ cong (λ k → suc (k ⊔ black-depth right)) (RBtreeEQ rb2) ⟩
|
|
|
780 suc (black-depth right ⊔ black-depth right) ≡⟨ ⊔-idem _ ⟩
|
|
|
781 suc (black-depth right) ∎ ) ⟫ where open ≡-Reasoning
|
|
|
782 black-children-eq {n} {A} {tree} {left} {right} {key} {value} {Red} eq () rb
|
|
|
783
|
|
|
784 black-depth-cong : {n : Level} (A : Set n) {tree tree₁ : bt (Color ∧ A)}
|
|
|
785 → tree ≡ tree₁ → black-depth tree ≡ black-depth tree₁
|
|
|
786 black-depth-cong {n} A {leaf} {leaf} refl = refl
|
|
|
787 black-depth-cong {n} A {node key ⟪ Red , value ⟫ left right} {node .key ⟪ Red , .value ⟫ .left .right} refl
|
|
|
788 = cong₂ (λ j k → j ⊔ k ) (black-depth-cong A {left} {left} refl) (black-depth-cong A {right} {right} refl)
|
|
|
789 black-depth-cong {n} A {node key ⟪ Black , value ⟫ left right} {node .key ⟪ Black , .value ⟫ .left .right} refl
|
|
|
790 = cong₂ (λ j k → suc (j ⊔ k) ) (black-depth-cong A {left} {left} refl) (black-depth-cong A {right} {right} refl)
|
|
|
791
|
|
|
792 black-depth-resp : {n : Level} (A : Set n) (tree tree₁ : bt (Color ∧ A)) → {c1 c2 : Color} { l1 l2 r1 r2 : bt (Color ∧ A)} {key1 key2 : ℕ} {value1 value2 : A}
|
|
|
793 → tree ≡ node key1 ⟪ c1 , value1 ⟫ l1 r1 → tree₁ ≡ node key2 ⟪ c2 , value2 ⟫ l2 r2
|
|
|
794 → color tree ≡ color tree₁
|
|
|
795 → black-depth l1 ≡ black-depth l2 → black-depth r1 ≡ black-depth r2
|
|
|
796 → black-depth tree ≡ black-depth tree₁
|
|
|
797 black-depth-resp A _ _ {Black} {Black} refl refl refl eql eqr = cong₂ (λ j k → suc (j ⊔ k) ) eql eqr
|
|
|
798 black-depth-resp A _ _ {Red} {Red} refl refl refl eql eqr = cong₂ (λ j k → j ⊔ k ) eql eqr
|
|
|
799
|
|
|
800 red-children-eq1 : {n : Level} {A : Set n} {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color}
|
|
|
801 → tree ≡ node key ⟪ c , value ⟫ left right
|
|
|
802 → color tree ≡ Red
|
|
|
803 → RBtreeInvariant tree
|
|
|
804 → (black-depth tree ≡ black-depth left ) ∧ (black-depth tree ≡ black-depth right)
|
|
|
805 red-children-eq1 {n} {A} {.(node key₁ ⟪ Red , value₁ ⟫ left right)} {left} {right} {.key₁} {.value₁} {Red} refl eq₁ rb2@(rb-red key₁ value₁ x x₁ x₂ rb rb₁) =
|
|
|
806 ⟪ ( begin
|
|
|
807 black-depth left ⊔ black-depth right ≡⟨ cong (λ k → black-depth left ⊔ k) (sym (RBtreeEQ rb2)) ⟩
|
|
|
808 black-depth left ⊔ black-depth left ≡⟨ ⊔-idem _ ⟩
|
|
|
809 black-depth left ∎ ) , (
|
|
|
810 begin
|
|
|
811 black-depth left ⊔ black-depth right ≡⟨ cong (λ k → k ⊔ black-depth right ) (RBtreeEQ rb2) ⟩
|
|
|
812 black-depth right ⊔ black-depth right ≡⟨ ⊔-idem _ ⟩
|
|
|
813 black-depth right ∎ ) ⟫ where open ≡-Reasoning
|
|
|
814 red-children-eq1 {n} {A} {.(node key ⟪ Black , value ⟫ left right)} {left} {right} {key} {value} {Black} refl () rb
|
|
|
815
|
|
|
816 black-children-eq1 : {n : Level} {A : Set n} {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color}
|
|
|
817 → tree ≡ node key ⟪ c , value ⟫ left right
|
|
|
818 → color tree ≡ Black
|
|
|
819 → RBtreeInvariant tree
|
|
|
820 → (black-depth tree ≡ suc (black-depth left) ) ∧ (black-depth tree ≡ suc (black-depth right))
|
|
|
821 black-children-eq1 {n} {A} {.(node key₁ ⟪ Black , value₁ ⟫ left right)} {left} {right} {.key₁} {.value₁} {Black} refl eq₁ rb2@(rb-black key₁ value₁ x rb rb₁) =
|
|
|
822 ⟪ ( begin
|
|
|
823 suc (black-depth left ⊔ black-depth right) ≡⟨ cong (λ k → suc (black-depth left ⊔ k)) (sym (RBtreeEQ rb2)) ⟩
|
|
|
824 suc (black-depth left ⊔ black-depth left) ≡⟨ ⊔-idem _ ⟩
|
|
|
825 suc (black-depth left) ∎ ) , (
|
|
|
826 begin
|
|
|
827 suc (black-depth left ⊔ black-depth right) ≡⟨ cong (λ k → suc (k ⊔ black-depth right)) (RBtreeEQ rb2) ⟩
|
|
|
828 suc (black-depth right ⊔ black-depth right) ≡⟨ ⊔-idem _ ⟩
|
|
|
829 suc (black-depth right) ∎ ) ⟫ where open ≡-Reasoning
|
|
|
830 black-children-eq1 {n} {A} {.(node key ⟪ Red , value ⟫ left right)} {left} {right} {key} {value} {Red} refl () rb
|
|
|
831
|
|
|
832
|
|
|
833 rbi-from-red-black : {n : Level } {A : Set n} → (n1 rp-left : bt (Color ∧ A)) → (kp : ℕ) → (vp : Color ∧ A)
|
|
|
834 → RBtreeInvariant n1 → RBtreeInvariant rp-left
|
|
|
835 → black-depth n1 ≡ black-depth rp-left
|
|
|
836 → color n1 ≡ Black → color rp-left ≡ Black → ⟪ Red , proj2 vp ⟫ ≡ vp
|
|
|
837 → RBtreeInvariant (node kp vp n1 rp-left)
|
|
|
838 rbi-from-red-black leaf leaf kp vp rb1 rbp deq ceq1 ceq2 ceq3
|
|
|
839 = subst (λ k → RBtreeInvariant (node kp k leaf leaf)) ceq3 (rb-red kp (proj2 vp) refl refl refl rb-leaf rb-leaf)
|
|
|
840 rbi-from-red-black leaf (node key ⟪ .Black , proj3 ⟫ trpl trpl₁) kp vp rb1 rbp deq ceq1 refl ceq3
|
|
|
841 = subst (λ k → RBtreeInvariant (node kp k _ _)) ceq3 (rb-red kp (proj2 vp) refl refl deq rb1 rbp)
|
|
|
842 rbi-from-red-black (node key ⟪ .Black , proj3 ⟫ tn1 tn2) leaf kp vp rb1 rbp deq refl ceq2 ceq3
|
|
|
843 = subst (λ k → RBtreeInvariant (node kp k _ _)) ceq3 (rb-red kp (proj2 vp) refl refl deq rb1 rbp)
|
|
|
844 rbi-from-red-black (node key ⟪ .Black , proj3 ⟫ tn1 tn2) (node key₁ ⟪ .Black , proj4 ⟫ trpl trpl₁) kp vp rb1 rbp deq refl refl ceq3
|
|
|
845 = subst (λ k → RBtreeInvariant (node kp k _ _)) ceq3 (rb-red kp (proj2 vp) refl refl deq rb1 rbp )
|
|
|
846
|
|
|
847 ⊔-succ : {m n : ℕ} → suc (m ⊔ n) ≡ suc m ⊔ suc n
|
|
|
848 ⊔-succ {m} {n} = refl
|
|
|
849
|
|
|
850
|
|
|
851 --
|
|
|
852 -- if we consider tree invariant, this may be much simpler and faster
|
|
|
853 --
|
|
|
854 stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A )
|
|
|
855 → (stack : List (bt A)) → stackInvariant key tree orig stack
|
|
|
856 → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A key tree stack
|
|
|
857 stackToPG {n} {A} {key} tree .tree .(tree ∷ []) s-nil = case1 refl
|
|
|
858 stackToPG {n} {A} {key} tree .(node _ _ _ tree) .(tree ∷ node _ _ _ tree ∷ []) (s-right _ _ _ x s-nil) = case2 (case1 refl)
|
|
|
859 stackToPG {n} {A} {key} tree .(node k2 v2 t5 (node k1 v1 t2 tree)) (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ [])) (s-right tree (node k2 v2 t5 (node k1 v1 t2 tree)) t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) (node k2 v2 t5 (node k1 v1 t2 tree)) t5 {k2} {v2} x₁ s-nil)) = case2 (case2
|
|
|
860 record { parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p x refl refl ; rest = _ ; stack=gp = refl } )
|
|
|
861 stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right tree orig t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) orig t5 {k2} {v2} x₁ (s-right _ _ _ x₂ si))) = case2 (case2
|
|
|
862 record { parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p x refl refl ; rest = _ ; stack=gp = refl } )
|
|
|
863 stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right tree orig t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) orig t5 {k2} {v2} x₁ (s-left _ _ _ x₂ si))) = case2 (case2
|
|
|
864 record { parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p x refl refl ; rest = _ ; stack=gp = refl } )
|
|
|
865 stackToPG {n} {A} {key} tree .(node k2 v2 (node k1 v1 t1 tree) t2) .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ []) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ s-nil)) = case2 (case2
|
|
|
866 record { parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 x refl refl ; rest = _ ; stack=gp = refl } )
|
|
|
867 stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ (s-right _ _ _ x₂ si))) = case2 (case2
|
|
|
868 record { parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 x refl refl ; rest = _ ; stack=gp = refl } )
|
|
|
869 stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ (s-left _ _ _ x₂ si))) = case2 (case2
|
|
|
870 record { parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 x refl refl ; rest = _ ; stack=gp = refl } )
|
|
|
871 stackToPG {n} {A} {key} tree .(node _ _ tree _) .(tree ∷ node _ _ tree _ ∷ []) (s-left _ _ t1 {k1} {v1} x s-nil) = case2 (case1 refl)
|
|
|
872 stackToPG {n} {A} {key} tree .(node _ _ _ (node k1 v1 tree t1)) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ []) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ s-nil)) = case2 (case2
|
|
|
873 record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p x refl refl ; rest = _ ; stack=gp = refl } )
|
|
|
874 stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ (s-right _ _ _ x₂ si))) = case2 (case2
|
|
|
875 record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p x refl refl ; rest = _ ; stack=gp = refl } )
|
|
|
876 stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ (s-left _ _ _ x₂ si))) = case2 (case2
|
|
|
877 record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p x refl refl ; rest = _ ; stack=gp = refl } )
|
|
|
878 stackToPG {n} {A} {key} tree .(node _ _ (node k1 v1 tree t1) _) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ []) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ s-nil)) = case2 (case2
|
|
|
879 record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 x refl refl ; rest = _ ; stack=gp = refl } )
|
|
|
880 stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ (s-right _ _ _ x₂ si))) = case2 (case2
|
|
|
881 record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 x refl refl ; rest = _ ; stack=gp = refl } )
|
|
|
882 stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ (s-left _ _ _ x₂ si))) = case2 (case2
|
|
|
883 record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 x refl refl ; rest = _ ; stack=gp = refl } )
|
|
|
884
|
|
|
885 stackCase1 : {n : Level} {A : Set n} → {key : ℕ } → {tree orig : bt A }
|
|
|
886 → {stack : List (bt A)} → stackInvariant key tree orig stack
|
|
|
887 → stack ≡ orig ∷ [] → tree ≡ orig
|
|
|
888 stackCase1 s-nil refl = refl
|
|
|
889
|
|
|
890 pg-prop-1 : {n : Level} (A : Set n) → (key : ℕ) → (tree orig : bt A )
|
|
|
891 → (stack : List (bt A)) → (pg : PG A key tree stack)
|
|
|
892 → (¬ PG.grand pg ≡ leaf ) ∧ (¬ PG.parent pg ≡ leaf)
|
|
|
893 pg-prop-1 {_} A _ tree orig stack pg with PG.pg pg
|
|
|
894 ... | s2-s1p2 _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫
|
|
|
895 ... | s2-1sp2 _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫
|
|
|
896 ... | s2-s12p _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫
|
|
|
897 ... | s2-1s2p _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫
|
|
|
898
|
|
|
899 popStackInvariant : {n : Level} {A : Set n} → (rest : List ( bt (Color ∧ A)))
|
|
|
900 → ( tree parent orig : bt (Color ∧ A)) → (key : ℕ)
|
|
|
901 → stackInvariant key tree orig ( tree ∷ parent ∷ rest )
|
|
|
902 → stackInvariant key parent orig (parent ∷ rest )
|
|
|
903 popStackInvariant rest tree parent orig key (s-right .tree .orig tree₁ x si) = sc00 where
|
|
|
904 sc00 : stackInvariant key parent orig (parent ∷ rest )
|
|
|
905 sc00 with si-property1 si
|
|
|
906 ... | refl = si
|
|
|
907 popStackInvariant rest tree parent orig key (s-left .tree .orig tree₁ x si) = sc00 where
|
|
|
908 sc00 : stackInvariant key parent orig (parent ∷ rest )
|
|
|
909 sc00 with si-property1 si
|
|
|
910 ... | refl = si
|
|
|
911
|
|
|
912
|
|
|
913 siToTreeinvariant : {n : Level} {A : Set n} → (rest : List ( bt (Color ∧ A)))
|
|
|
914 → ( tree orig : bt (Color ∧ A)) → (key : ℕ)
|
|
|
915 → treeInvariant orig
|
|
|
916 → stackInvariant key tree orig ( tree ∷ rest )
|
|
|
917 → treeInvariant tree
|
|
|
918 siToTreeinvariant .[] tree .tree key ti s-nil = ti
|
|
|
919 siToTreeinvariant .(node _ _ leaf leaf ∷ []) .leaf .(node _ _ leaf leaf) key (t-single _ _) (s-right .leaf .(node _ _ leaf leaf) .leaf x s-nil) = t-leaf
|
|
|
920 siToTreeinvariant .(node _ _ leaf (node key₁ _ _ _) ∷ []) .(node key₁ _ _ _) .(node _ _ leaf (node key₁ _ _ _)) key (t-right _ key₁ x₁ x₂ x₃ ti) (s-right .(node key₁ _ _ _) .(node _ _ leaf (node key₁ _ _ _)) .leaf x s-nil) = ti
|
|
|
921 siToTreeinvariant .(node _ _ (node key₁ _ _ _) leaf ∷ []) .leaf .(node _ _ (node key₁ _ _ _) leaf) key (t-left key₁ _ x₁ x₂ x₃ ti) (s-right .leaf .(node _ _ (node key₁ _ _ _) leaf) .(node key₁ _ _ _) x s-nil) = t-leaf
|
|
|
922 siToTreeinvariant .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _) ∷ []) .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) key (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key₁ _ _ _) x s-nil) = ti₁
|
|
|
923 siToTreeinvariant .(node _ _ tree₁ tree ∷ _) tree orig key ti (s-right .tree .orig tree₁ x si2@(s-right .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2
|
|
|
924 ... | t-single _ _ = t-leaf
|
|
|
925 ... | t-right _ key₁ x₂ x₃ x₄ ti₁ = ti₁
|
|
|
926 ... | t-left key₁ _ x₂ x₃ x₄ ti₁ = t-leaf
|
|
|
927 ... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ ti₁ ti₂ = ti₂
|
|
|
928 siToTreeinvariant .(node _ _ tree₁ tree ∷ _) tree orig key ti (s-right .tree .orig tree₁ x si2@(s-left .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2
|
|
|
929 ... | t-single _ _ = t-leaf
|
|
|
930 ... | t-right _ key₁ x₂ x₃ x₄ ti₁ = ti₁
|
|
|
931 ... | t-left key₁ _ x₂ x₃ x₄ ti₁ = t-leaf
|
|
|
932 ... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ ti₁ ti₂ = ti₂
|
|
|
933 siToTreeinvariant .(node _ _ leaf leaf ∷ []) .leaf .(node _ _ leaf leaf) key (t-single _ _) (s-left .leaf .(node _ _ leaf leaf) .leaf x s-nil) = t-leaf
|
|
|
934 siToTreeinvariant .(node _ _ leaf (node key₁ _ _ _) ∷ []) .leaf .(node _ _ leaf (node key₁ _ _ _)) key (t-right _ key₁ x₁ x₂ x₃ ti) (s-left .leaf .(node _ _ leaf (node key₁ _ _ _)) .(node key₁ _ _ _) x s-nil) = t-leaf
|
|
|
935 siToTreeinvariant .(node _ _ (node key₁ _ _ _) leaf ∷ []) .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) leaf) key (t-left key₁ _ x₁ x₂ x₃ ti) (s-left .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) leaf) .leaf x s-nil) = ti
|
|
|
936 siToTreeinvariant .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _) ∷ []) .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) key (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-left .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key₂ _ _ _) x s-nil) = ti
|
|
|
937 siToTreeinvariant .(node _ _ tree tree₁ ∷ _) tree orig key ti (s-left .tree .orig tree₁ x si2@(s-right .(node _ _ tree tree₁) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2
|
|
|
938 ... | t-single _ _ = t-leaf
|
|
|
939 ... | t-right _ key₁ x₂ x₃ x₄ t = t-leaf
|
|
|
940 ... | t-left key₁ _ x₂ x₃ x₄ t = t
|
|
|
941 ... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ t t₁ = t
|
|
|
942 siToTreeinvariant .(node _ _ tree tree₁ ∷ _) tree orig key ti (s-left .tree .orig tree₁ x si2@(s-left .(node _ _ tree tree₁) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2
|
|
|
943 ... | t-single _ _ = t-leaf
|
|
|
944 ... | t-right _ key₁ x₂ x₃ x₄ t = t-leaf
|
|
|
945 ... | t-left key₁ _ x₂ x₃ x₄ t = t
|
|
|
946 ... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ t t₁ = t
|
|
|
947
|
|
|
948 PGtoRBinvariant1 : {n : Level} {A : Set n}
|
|
|
949 → (tree orig : bt (Color ∧ A) )
|
|
|
950 → {key : ℕ }
|
|
|
951 → (rb : RBtreeInvariant orig)
|
|
|
952 → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack )
|
|
|
953 → RBtreeInvariant tree
|
|
|
954 PGtoRBinvariant1 tree .tree rb .(tree ∷ []) s-nil = rb
|
|
|
955 PGtoRBinvariant1 tree orig rb (tree ∷ rest) (s-right .tree .orig tree₁ x si) with PGtoRBinvariant1 _ orig rb _ si
|
|
|
956 ... | rb-red _ value x₁ x₂ x₃ t t₁ = t₁
|
|
|
957 ... | rb-black _ value x₁ t t₁ = t₁
|
|
|
958 PGtoRBinvariant1 tree orig rb (tree ∷ rest) (s-left .tree .orig tree₁ x si) with PGtoRBinvariant1 _ orig rb _ si
|
|
|
959 ... | rb-red _ value x₁ x₂ x₃ t t₁ = t
|
|
|
960 ... | rb-black _ value x₁ t t₁ = t
|
|
|
961
|
|
|
962 RBI-child-replaced : {n : Level} {A : Set n} (tr : bt (Color ∧ A)) (key : ℕ) → RBtreeInvariant tr → RBtreeInvariant (child-replaced key tr)
|
|
|
963 RBI-child-replaced {n} {A} leaf key rbi = rbi
|
|
|
964 RBI-child-replaced {n} {A} (node key₁ value tr tr₁) key rbi with <-cmp key key₁
|
|
|
965 ... | tri< a ¬b ¬c = RBtreeLeftDown _ _ rbi
|
|
|
966 ... | tri≈ ¬a b ¬c = rbi
|
|
|
967 ... | tri> ¬a ¬b c = RBtreeRightDown _ _ rbi
|
|
|
968
|
|
|
969 --
|
|
|
970 -- create RBT invariant after findRBT, continue to replaceRBT
|
|
|
971 --
|
|
|
972 createRBT : {n m : Level} {A : Set n } {t : Set m }
|
|
|
973 → (key : ℕ) (value : A)
|
|
|
974 → (tree0 : bt (Color ∧ A))
|
|
|
975 → RBtreeInvariant tree0
|
|
|
976 → treeInvariant tree0
|
|
|
977 → (tree1 : bt (Color ∧ A))
|
|
|
978 → (stack : List (bt (Color ∧ A)))
|
|
|
979 → stackInvariant key tree1 tree0 stack
|
|
|
980 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )
|
|
|
981 → (exit : (stack : List ( bt (Color ∧ A))) (r : RBI key value tree0 stack ) → t ) → t
|
|
|
982 createRBT {n} {m} {A} {t} key value orig rbi ti tree (x ∷ []) si P exit = crbt00 orig P refl where
|
|
|
983 crbt00 : (tree1 : bt (Color ∧ A)) → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) → tree1 ≡ orig → t
|
|
|
984 crbt00 leaf P refl = exit (x ∷ []) record {
|
|
|
985 tree = leaf
|
|
|
986 ; repl = node key ⟪ Red , value ⟫ leaf leaf
|
|
|
987 ; origti = ti
|
|
|
988 ; origrb = rbi
|
|
|
989 ; treerb = rb-leaf
|
|
|
990 ; replrb = rb-red key value refl refl refl rb-leaf rb-leaf
|
|
|
991 ; si = subst (λ k → stackInvariant key k leaf _ ) crbt01 si
|
|
|
992 ; state = rotate leaf refl
|
|
|
993 } where
|
|
|
994 crbt01 : tree ≡ leaf
|
|
|
995 crbt01 with si-property-last _ _ _ _ si | si-property1 si
|
|
|
996 ... | refl | refl = refl
|
|
|
997 crbt00 (node key₁ value₁ left right ) (case1 eq) refl with si-property-last _ _ _ _ si | si-property1 si
|
|
|
998 ... | refl | refl = ⊥-elim (bt-ne (sym eq))
|
|
|
999 crbt00 (node key₁ value₁ left right ) (case2 eq) refl with si-property-last _ _ _ _ si | si-property1 si
|
|
|
1000 ... | refl | refl = exit (x ∷ []) record {
|
|
|
1001 tree = node key₁ value₁ left right
|
|
|
1002 ; repl = node key₁ ⟪ proj1 value₁ , value ⟫ left right
|
|
|
1003 ; origti = ti
|
|
|
1004 ; origrb = rbi
|
|
|
1005 ; treerb = rbi
|
|
|
1006 ; replrb = crbt03 value₁ rbi
|
|
|
1007 ; si = si
|
|
|
1008 ; state = rebuild refl (crbt01 value₁ ) (λ ())
|
|
|
1009 } where
|
|
|
1010 crbt01 : (value₁ : Color ∧ A) → black-depth (node key₁ ⟪ proj1 value₁ , value ⟫ left right) ≡ black-depth (node key₁ value₁ left right)
|
|
|
1011 crbt01 ⟪ Red , proj4 ⟫ = refl
|
|
|
1012 crbt01 ⟪ Black , proj4 ⟫ = refl
|
|
|
1013 crbt03 : (value₁ : Color ∧ A) → RBtreeInvariant (node key₁ value₁ left right) → RBtreeInvariant (node key₁ ⟪ proj1 value₁ , value ⟫ left right)
|
|
|
1014 crbt03 ⟪ Red , proj4 ⟫ (rb-red .key₁ .proj4 x x₁ x₂ rbi rbi₁) = rb-red key₁ _ x x₁ x₂ rbi rbi₁
|
|
|
1015 crbt03 ⟪ Black , proj4 ⟫ (rb-black .key₁ .proj4 x rbi rbi₁) = rb-black key₁ _ x rbi rbi₁
|
|
|
1016 keq : ( just key₁ ≡ just key ) → key₁ ≡ key
|
|
|
1017 keq refl = refl
|
|
|
1018 createRBT {n} {m} {A} {t} key value orig rbi ti tree (x ∷ leaf ∷ stack) si P exit = ⊥-elim (si-property-parent-node _ _ _ si refl)
|
|
|
1019 createRBT {n} {m} {A} {t} key value orig rbi ti tree sp@(x ∷ node kp vp pleft pright ∷ stack) si P exit = crbt00 tree P refl where
|
|
|
1020 crbt00 : (tree1 : bt (Color ∧ A)) → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) → tree1 ≡ tree → t
|
|
|
1021 crbt00 leaf P refl = exit sp record {
|
|
|
1022 tree = leaf
|
|
|
1023 ; repl = node key ⟪ Red , value ⟫ leaf leaf
|
|
|
1024 ; origti = ti
|
|
|
1025 ; origrb = rbi
|
|
|
1026 ; treerb = rb-leaf
|
|
|
1027 ; replrb = rb-red key value refl refl refl rb-leaf rb-leaf
|
|
|
1028 ; si = si
|
|
|
1029 ; state = rotate leaf refl
|
|
|
1030 }
|
|
|
1031 crbt00 (node key₁ value₁ left right ) (case1 eq) refl = ⊥-elim (bt-ne (sym eq))
|
|
|
1032 crbt00 (node key₁ value₁ left right ) (case2 eq) refl with si-property-last _ _ _ _ si | si-property1 si
|
|
|
1033 ... | eq1 | eq2 = exit sp record {
|
|
|
1034 tree = node key₁ value₁ left right
|
|
|
1035 ; repl = node key₁ ⟪ proj1 value₁ , value ⟫ left right
|
|
|
1036 ; origti = ti
|
|
|
1037 ; origrb = rbi
|
|
|
1038 ; treerb = treerb
|
|
|
1039 ; replrb = crbt03 value₁ treerb
|
|
|
1040 ; si = si
|
|
|
1041 ; state = rebuild refl (crbt01 value₁ ) (λ ())
|
|
|
1042 } where
|
|
|
1043 crbt01 : (value₁ : Color ∧ A) → black-depth (node key₁ ⟪ proj1 value₁ , value ⟫ left right) ≡ black-depth (node key₁ value₁ left right)
|
|
|
1044 crbt01 ⟪ Red , proj4 ⟫ = refl
|
|
|
1045 crbt01 ⟪ Black , proj4 ⟫ = refl
|
|
|
1046 crbt03 : (value₁ : Color ∧ A) → RBtreeInvariant (node key₁ value₁ left right) → RBtreeInvariant (node key₁ ⟪ proj1 value₁ , value ⟫ left right)
|
|
|
1047 crbt03 ⟪ Red , proj4 ⟫ (rb-red .key₁ .proj4 x x₁ x₂ rbi rbi₁) = rb-red key₁ _ x x₁ x₂ rbi rbi₁
|
|
|
1048 crbt03 ⟪ Black , proj4 ⟫ (rb-black .key₁ .proj4 x rbi rbi₁) = rb-black key₁ _ x rbi rbi₁
|
|
|
1049 keq : ( just key₁ ≡ just key ) → key₁ ≡ key
|
|
|
1050 keq refl = refl
|
|
|
1051 treerb : RBtreeInvariant (node key₁ value₁ left right)
|
|
|
1052 treerb = PGtoRBinvariant1 _ orig rbi _ si
|
|
|
1053
|
|
|
1054 --
|
|
|
1055 -- rotate and rebuild replaceTree and rb-invariant
|
|
|
1056 --
|
|
|
1057 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
|
|
|
1058 → (key : ℕ) → (value : A)
|
|
|
1059 → (orig : bt (Color ∧ A))
|
|
|
1060 → (stack : List (bt (Color ∧ A)))
|
|
|
1061 → (r : RBI key value orig stack )
|
|
|
1062 → (next : (stack1 : List (bt (Color ∧ A)))
|
|
|
1063 → (r : RBI key value orig stack1 )
|
|
|
1064 → length stack1 < length stack → t )
|
|
|
1065 → (exit : (stack1 : List (bt (Color ∧ A)))
|
|
|
1066 → stack1 ≡ (orig ∷ [])
|
|
|
1067 → RBI key value orig stack1
|
|
|
1068 → t ) → t
|
|
|
1069 replaceRBP {n} {m} {A} {t} key value orig stack r next exit = replaceRBP1 where
|
|
|
1070 -- we have no grand parent
|
|
|
1071 -- eq : stack₁ ≡ RBI.tree r ∷ orig ∷ []
|
|
|
1072 -- change parent color ≡ Black and exit
|
|
|
1073 -- one level stack, orig is parent of repl
|
|
|
1074 repl = RBI.repl r
|
|
|
1075 insertCase4 : (tr0 : bt (Color ∧ A)) → tr0 ≡ orig
|
|
|
1076 → (eq : stack ≡ RBI.tree r ∷ orig ∷ [])
|
|
|
1077 → ( color repl ≡ Red ) ∨ (color (RBI.tree r) ≡ color repl)
|
|
|
1078 → stackInvariant key (RBI.tree r) orig stack
|
|
|
1079 → t
|
|
|
1080 insertCase4 leaf eq1 eq col si = ⊥-elim (rb04 eq eq1 si) where -- can't happen
|
|
|
1081 rb04 : {stack : List ( bt ( Color ∧ A))} → stack ≡ RBI.tree r ∷ orig ∷ [] → leaf ≡ orig → stackInvariant key (RBI.tree r) orig stack → ⊥
|
|
|
1082 rb04 refl refl (s-right tree leaf tree₁ x si) = si-property2 _ (s-right tree leaf tree₁ x si) refl
|
|
|
1083 rb04 refl refl (s-left tree₁ leaf tree x si) = si-property2 _ (s-left tree₁ leaf tree x si) refl
|
|
|
1084 insertCase4 tr0@(node key₁ value₁ left right) refl eq col si with <-cmp key key₁
|
|
|
1085 ... | tri< a ¬b ¬c = rb07 col where
|
|
|
1086 rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → left ≡ RBI.tree r
|
|
|
1087 rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x s-nil) refl refl = refl
|
|
|
1088 rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl with si-property1 si
|
|
|
1089 ... | refl = ⊥-elim ( nat-<> x a )
|
|
|
1090 rb06 : black-depth repl ≡ black-depth right
|
|
|
1091 rb06 = ?
|
|
|
1092 rb08 : (color (RBI.tree r) ≡ color repl) → RBtreeInvariant (node key₁ value₁ repl right)
|
|
|
1093 rb08 ceq with proj1 value₁ in coeq
|
|
|
1094 ... | Red = subst (λ k → RBtreeInvariant (node key₁ k repl right)) (cong (λ k → ⟪ k , _ ⟫) (sym coeq) )
|
|
|
1095 (rb-red _ (proj2 value₁) rb09 (proj2 (RBtreeChildrenColorBlack _ _ (RBI.origrb r) coeq)) rb06 (RBI.replrb r)
|
|
|
1096 (RBtreeRightDown _ _ (RBI.origrb r))) where
|
|
|
1097 rb09 : color repl ≡ Black
|
|
|
1098 rb09 = trans (trans (sym ceq) (sym (cong color (rb04 si eq refl) ))) (proj1 (RBtreeChildrenColorBlack _ _ (RBI.origrb r) coeq))
|
|
|
1099 ... | Black = subst (λ k → RBtreeInvariant (node key₁ k repl right)) (cong (λ k → ⟪ k , _ ⟫) (sym coeq) )
|
|
|
1100 (rb-black _ (proj2 value₁) rb06 (RBI.replrb r) (RBtreeRightDown _ _ (RBI.origrb r)))
|
|
|
1101 rb07 : ( color repl ≡ Red ) ∨ (color (RBI.tree r) ≡ color repl) → t
|
|
|
1102 rb07 (case2 cc ) = exit (orig ∷ []) refl record {
|
|
|
1103 tree = orig
|
|
|
1104 ; repl = node key₁ value₁ repl right
|
|
|
1105 ; origti = RBI.origti r
|
|
|
1106 ; origrb = RBI.origrb r
|
|
|
1107 ; treerb = RBI.origrb r
|
|
|
1108 ; replrb = rb08 cc
|
|
|
1109 ; si = s-nil
|
|
|
1110 ; state = top-black refl
|
|
|
1111 }
|
|
|
1112 rb07 (case1 repl-red) = exit (orig ∷ []) refl record {
|
|
|
1113 tree = orig
|
|
|
1114 ; repl = to-black (node key₁ value₁ repl right)
|
|
|
1115 ; origti = RBI.origti r
|
|
|
1116 ; origrb = RBI.origrb r
|
|
|
1117 ; treerb = RBI.origrb r
|
|
|
1118 ; replrb = rb-black _ _ rb06 (RBI.replrb r) (RBtreeRightDown _ _ (RBI.origrb r))
|
|
|
1119 ; si = s-nil
|
|
|
1120 ; state = top-black refl
|
|
|
1121 }
|
|
|
1122 ... | tri≈ ¬a b ¬c = ⊥-elim ( si-property-pne _ _ stack eq si b ) -- can't happen
|
|
|
1123 ... | tri> ¬a ¬b c = rb07 col where
|
|
|
1124 rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → right ≡ RBI.tree r
|
|
|
1125 rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl = refl
|
|
|
1126 rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x si) refl refl with si-property1 si
|
|
|
1127 ... | refl = ⊥-elim ( nat-<> x c )
|
|
|
1128 rb06 : black-depth repl ≡ black-depth left
|
|
|
1129 rb06 = ?
|
|
|
1130 rb08 : (color (RBI.tree r) ≡ color repl) → RBtreeInvariant (node key₁ value₁ left repl )
|
|
|
1131 rb08 ceq with proj1 value₁ in coeq
|
|
|
1132 ... | Red = subst (λ k → RBtreeInvariant (node key₁ k left repl )) (cong (λ k → ⟪ k , _ ⟫) (sym coeq) )
|
|
|
1133 (rb-red _ (proj2 value₁) (proj1 (RBtreeChildrenColorBlack _ _ (RBI.origrb r) coeq)) rb09 (sym rb06)
|
|
|
1134 (RBtreeLeftDown _ _ (RBI.origrb r))(RBI.replrb r)) where
|
|
|
1135 rb09 : color repl ≡ Black
|
|
|
1136 rb09 = trans (trans (sym ceq) (sym (cong color (rb04 si eq refl) ))) (proj2 (RBtreeChildrenColorBlack _ _ (RBI.origrb r) coeq))
|
|
|
1137 ... | Black = subst (λ k → RBtreeInvariant (node key₁ k left repl )) (cong (λ k → ⟪ k , _ ⟫) (sym coeq) )
|
|
|
1138 (rb-black _ (proj2 value₁) (sym rb06) (RBtreeLeftDown _ _ (RBI.origrb r)) (RBI.replrb r))
|
|
|
1139 rb07 : ( color repl ≡ Red ) ∨ (color (RBI.tree r) ≡ color repl) → t
|
|
|
1140 rb07 (case2 cc ) = exit (orig ∷ []) refl record {
|
|
|
1141 tree = orig
|
|
|
1142 ; repl = node key₁ value₁ left repl
|
|
|
1143 ; origti = RBI.origti r
|
|
|
1144 ; origrb = RBI.origrb r
|
|
|
1145 ; treerb = RBI.origrb r
|
|
|
1146 ; replrb = rb08 cc
|
|
|
1147 ; si = s-nil
|
|
|
1148 ; state = top-black refl
|
|
|
1149 }
|
|
|
1150 rb07 (case1 repl-red ) = exit (orig ∷ []) refl record {
|
|
|
1151 tree = orig
|
|
|
1152 ; repl = to-black (node key₁ value₁ left repl)
|
|
|
1153 ; origti = RBI.origti r
|
|
|
1154 ; origrb = RBI.origrb r
|
|
|
1155 ; treerb = RBI.origrb r
|
|
|
1156 ; replrb = rb-black _ _ (sym rb06) (RBtreeLeftDown _ _ (RBI.origrb r)) (RBI.replrb r)
|
|
|
1157 ; si = s-nil
|
|
|
1158 ; state = top-black refl
|
|
|
1159 }
|
|
|
1160 rebuildCase : (ceq : color (RBI.tree r) ≡ color repl)
|
|
|
1161 → (bdepth-eq : black-depth repl ≡ black-depth (RBI.tree r))
|
|
|
1162 → (¬ RBI.tree r ≡ leaf) → t
|
|
|
1163 rebuildCase ceq bdepth-eq ¬leaf with stackToPG (RBI.tree r) orig stack (RBI.si r)
|
|
|
1164 ... | case1 x = exit stack x r where -- single node case
|
|
|
1165 rb00 : stack ≡ orig ∷ [] → orig ≡ RBI.tree r
|
|
|
1166 rb00 refl = si-property1 (RBI.si r)
|
|
|
1167 ... | case2 (case1 x) = insertCase4 orig refl x (case2 ceq) (RBI.si r) -- one level stack, orig is parent of repl
|
|
|
1168 ... | case2 (case2 pg) = rebuildCase1 pg where
|
|
|
1169 rb00 : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
|
|
|
1170 rb00 pg = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r)
|
|
|
1171 treerb : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → RBtreeInvariant (PG.parent pg)
|
|
|
1172 treerb pg = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (rb00 pg))
|
|
|
1173 rb08 : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → treeInvariant (PG.parent pg)
|
|
|
1174 rb08 pg = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (rb00 pg))
|
|
|
1175 rebuildCase1 : (PG (Color ∧ A) key (RBI.tree r) stack) → t
|
|
|
1176 rebuildCase1 pg with PG.pg pg
|
|
|
1177 ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = rebuildCase2 where
|
|
|
1178 rebuildCase2 : t
|
|
|
1179 rebuildCase2 = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
|
|
|
1180 tree = PG.parent pg
|
|
|
1181 ; repl = rb01
|
|
|
1182 ; origti = RBI.origti r
|
|
|
1183 ; origrb = RBI.origrb r
|
|
|
1184 ; treerb = treerb pg
|
|
|
1185 ; replrb = rb02
|
|
|
1186 ; si = popStackInvariant _ _ _ _ _ (rb00 pg)
|
|
|
1187 ; state = rebuild (cong color x) rb06 (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ()))
|
|
|
1188 } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where
|
|
|
1189 rb01 : bt (Color ∧ A)
|
|
|
1190 rb01 = node kp vp repl n1
|
|
|
1191 rb03 : black-depth n1 ≡ black-depth repl
|
|
|
1192 rb03 = ?
|
|
|
1193 rb02 : RBtreeInvariant rb01
|
|
|
1194 rb02 with subst (λ k → RBtreeInvariant k) x (treerb pg)
|
|
|
1195 ... | rb-red .kp value cx cx₁ ex₂ t t₁ = rb-red kp value (trans (sym ceq) cx) cx₁ (sym rb03) (RBI.replrb r) t₁
|
|
|
1196 ... | rb-black .kp value ex t t₁ = rb-black kp value (sym rb03) (RBI.replrb r) t₁
|
|
|
1197 rb05 : treeInvariant (node kp vp (RBI.tree r) n1 )
|
|
|
1198 rb05 = subst (λ k → treeInvariant k) x (rb08 pg)
|
|
|
1199 rb04 : key < kp
|
|
|
1200 rb04 = lt
|
|
|
1201 rb06 : black-depth rb01 ≡ black-depth (PG.parent pg)
|
|
|
1202 rb06 = trans (rb07 vp) ( cong black-depth (sym x) ) where
|
|
|
1203 rb07 : (vp : Color ∧ A) → black-depth (node kp vp repl n1) ≡ black-depth (node kp vp (RBI.tree r) n1 )
|
|
|
1204 rb07 ⟪ Black , proj4 ⟫ = cong (λ k → suc (k ⊔ black-depth n1 )) bdepth-eq
|
|
|
1205 rb07 ⟪ Red , proj4 ⟫ = cong (λ k → (k ⊔ black-depth n1 )) bdepth-eq
|
|
|
1206 ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = rebuildCase2 where
|
|
|
1207 rebuildCase2 : t
|
|
|
1208 rebuildCase2 = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
|
|
|
1209 tree = PG.parent pg
|
|
|
1210 ; repl = rb01
|
|
|
1211 ; origti = RBI.origti r
|
|
|
1212 ; origrb = RBI.origrb r
|
|
|
1213 ; treerb = treerb pg
|
|
|
1214 ; replrb = rb02
|
|
|
1215 ; si = popStackInvariant _ _ _ _ _ (rb00 pg)
|
|
|
1216 ; state = rebuild (cong color x) rb06 (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ()))
|
|
|
1217 } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where
|
|
|
1218 rb01 : bt (Color ∧ A)
|
|
|
1219 rb01 = node kp vp n1 repl
|
|
|
1220 rb03 : black-depth n1 ≡ black-depth repl
|
|
|
1221 rb03 = ?
|
|
|
1222 rb02 : RBtreeInvariant rb01
|
|
|
1223 rb02 with subst (λ k → RBtreeInvariant k) x (treerb pg)
|
|
|
1224 ... | rb-red .kp value cx cx₁ ex₂ t t₁ = rb-red kp value cx (trans (sym ceq) cx₁) rb03 t (RBI.replrb r)
|
|
|
1225 ... | rb-black .kp value ex t t₁ = rb-black kp value rb03 t (RBI.replrb r)
|
|
|
1226 rb05 : treeInvariant (node kp vp n1 (RBI.tree r) )
|
|
|
1227 rb05 = subst (λ k → treeInvariant k) x (rb08 pg)
|
|
|
1228 rb04 : kp < key
|
|
|
1229 rb04 = lt
|
|
|
1230 rb06 : black-depth rb01 ≡ black-depth (PG.parent pg)
|
|
|
1231 rb06 = trans (rb07 vp) ( cong black-depth (sym x) ) where
|
|
|
1232 rb07 : (vp : Color ∧ A) → black-depth (node kp vp n1 repl) ≡ black-depth (node kp vp n1 (RBI.tree r))
|
|
|
1233 rb07 ⟪ Black , proj4 ⟫ = cong (λ k → suc (black-depth n1 ⊔ k)) bdepth-eq
|
|
|
1234 rb07 ⟪ Red , proj4 ⟫ = cong (λ k → (black-depth n1 ⊔ k)) bdepth-eq
|
|
|
1235 ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = rebuildCase2 where
|
|
|
1236 rebuildCase2 : t
|
|
|
1237 rebuildCase2 = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
|
|
|
1238 tree = PG.parent pg
|
|
|
1239 ; repl = rb01
|
|
|
1240 ; origti = RBI.origti r
|
|
|
1241 ; origrb = RBI.origrb r
|
|
|
1242 ; treerb = treerb pg
|
|
|
1243 ; replrb = rb02
|
|
|
1244 ; si = popStackInvariant _ _ _ _ _ (rb00 pg)
|
|
|
1245 ; state = rebuild (cong color x) rb06 (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ()))
|
|
|
1246 } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where
|
|
|
1247 rb01 : bt (Color ∧ A)
|
|
|
1248 rb01 = node kp vp repl n1
|
|
|
1249 rb03 : black-depth n1 ≡ black-depth repl
|
|
|
1250 rb03 = ?
|
|
|
1251 rb02 : RBtreeInvariant rb01
|
|
|
1252 rb02 with subst (λ k → RBtreeInvariant k) x (treerb pg)
|
|
|
1253 ... | rb-red .kp value cx cx₁ ex₂ t t₁ = rb-red kp value (trans (sym ceq) cx) cx₁ (sym rb03) (RBI.replrb r) t₁
|
|
|
1254 ... | rb-black .kp value ex t t₁ = rb-black kp value (sym rb03) (RBI.replrb r) t₁
|
|
|
1255 rb05 : treeInvariant (node kp vp (RBI.tree r) n1)
|
|
|
1256 rb05 = subst (λ k → treeInvariant k) x (rb08 pg)
|
|
|
1257 rb04 : key < kp
|
|
|
1258 rb04 = lt
|
|
|
1259 rb06 : black-depth rb01 ≡ black-depth (PG.parent pg)
|
|
|
1260 rb06 = trans (rb07 vp) ( cong black-depth (sym x) ) where
|
|
|
1261 rb07 : (vp : Color ∧ A) → black-depth (node kp vp repl n1) ≡ black-depth (node kp vp (RBI.tree r) n1)
|
|
|
1262 rb07 ⟪ Black , proj4 ⟫ = cong (λ k → suc (k ⊔ black-depth n1 )) bdepth-eq
|
|
|
1263 rb07 ⟪ Red , proj4 ⟫ = cong (λ k → (k ⊔ black-depth n1 )) bdepth-eq
|
|
|
1264 ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = rebuildCase2 where
|
|
|
1265 rebuildCase2 : t
|
|
|
1266 rebuildCase2 = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
|
|
|
1267 tree = PG.parent pg
|
|
|
1268 ; repl = rb01
|
|
|
1269 ; origti = RBI.origti r
|
|
|
1270 ; origrb = RBI.origrb r
|
|
|
1271 ; treerb = treerb pg
|
|
|
1272 ; replrb = rb02
|
|
|
1273 ; si = popStackInvariant _ _ _ _ _ (rb00 pg)
|
|
|
1274 ; state = rebuild (cong color x) rb06 (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ()))
|
|
|
1275 } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where
|
|
|
1276 rb01 : bt (Color ∧ A)
|
|
|
1277 rb01 = node kp vp n1 repl
|
|
|
1278 rb03 : black-depth n1 ≡ black-depth repl
|
|
|
1279 rb03 = ?
|
|
|
1280 rb02 : RBtreeInvariant rb01
|
|
|
1281 rb02 with subst (λ k → RBtreeInvariant k) x (treerb pg)
|
|
|
1282 ... | rb-red .kp value cx cx₁ ex₂ t t₁ = rb-red kp value cx (trans (sym ceq) cx₁) rb03 t (RBI.replrb r)
|
|
|
1283 ... | rb-black .kp value ex t t₁ = rb-black kp value rb03 t (RBI.replrb r)
|
|
|
1284 rb05 : treeInvariant (node kp vp n1 (RBI.tree r))
|
|
|
1285 rb05 = subst (λ k → treeInvariant k) x (rb08 pg)
|
|
|
1286 rb04 : kp < key
|
|
|
1287 rb04 = si-property-> ¬leaf rb05 (subst (λ k → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x (rb00 pg))
|
|
|
1288 rb06 : black-depth rb01 ≡ black-depth (PG.parent pg)
|
|
|
1289 rb06 = trans (rb07 vp) ( cong black-depth (sym x) ) where
|
|
|
1290 rb07 : (vp : Color ∧ A) → black-depth (node kp vp n1 repl) ≡ black-depth (node kp vp n1 (RBI.tree r))
|
|
|
1291 rb07 ⟪ Black , proj4 ⟫ = cong (λ k → suc (black-depth n1 ⊔ k)) bdepth-eq
|
|
|
1292 rb07 ⟪ Red , proj4 ⟫ = cong (λ k → (black-depth n1 ⊔ k)) bdepth-eq
|
|
|
1293 --
|
|
|
1294 -- both parent and uncle are Red, rotate then goto rebuild
|
|
|
1295 --
|
|
|
1296 insertCase5 : (repl1 : bt (Color ∧ A)) → repl1 ≡ repl
|
|
|
1297 → (pg : PG (Color ∧ A) key (RBI.tree r) stack)
|
|
|
1298 → color repl ≡ Red → color (PG.uncle pg) ≡ Black → color (PG.parent pg) ≡ Red → t
|
|
|
1299 insertCase5 leaf eq pg repl-red uncle-black pcolor = ⊥-elim ( rb00 repl repl-red (cong color (sym eq))) where
|
|
|
1300 rb00 : (repl : bt (Color ∧ A)) → color repl ≡ Red → color repl ≡ Black → ⊥
|
|
|
1301 rb00 (node key ⟪ Black , proj4 ⟫ repl repl₁) () eq1
|
|
|
1302 rb00 (node key ⟪ Red , proj4 ⟫ repl repl₁) eq ()
|
|
|
1303 insertCase5 (node rkey vr rp-left rp-right) eq pg repl-red uncle-black pcolor = insertCase51 where
|
|
|
1304 rb00 : stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
|
|
|
1305 rb00 = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r)
|
|
|
1306 rb15 : suc (length (PG.rest pg)) < length stack
|
|
|
1307 rb15 = begin
|
|
|
1308 suc (suc (length (PG.rest pg))) ≤⟨ <-trans (n<1+n _) (n<1+n _) ⟩
|
|
|
1309 length (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) ≡⟨ cong length (sym (PG.stack=gp pg)) ⟩
|
|
|
1310 length stack ∎
|
|
|
1311 where open ≤-Reasoning
|
|
|
1312 rb02 : RBtreeInvariant (PG.grand pg)
|
|
|
1313 rb02 = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))
|
|
|
1314 rb09 : RBtreeInvariant (PG.parent pg)
|
|
|
1315 rb09 = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ rb00)
|
|
|
1316 rb08 : treeInvariant (PG.parent pg)
|
|
|
1317 rb08 = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00)
|
|
|
1318
|
|
|
1319 insertCase51 : t
|
|
|
1320 insertCase51 with PG.pg pg
|
|
|
1321 ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase52 where
|
|
|
1322 insertCase52 : t
|
|
|
1323 insertCase52 = next (PG.grand pg ∷ PG.rest pg) record {
|
|
|
1324 tree = PG.grand pg
|
|
|
1325 ; repl = rb01
|
|
|
1326 ; origti = RBI.origti r
|
|
|
1327 ; origrb = RBI.origrb r
|
|
|
1328 ; treerb = rb02
|
|
|
1329 ; replrb = subst (λ k → RBtreeInvariant k) rb10 (rb-black _ _ rb18 (RBI.replrb r) (rb-red _ _ rb16 uncle-black rb19 rb06 rb05))
|
|
|
1330 ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
|
|
|
1331 ; state = rebuild (trans (cong color x₁) (cong proj1 (sym rb14))) rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ()))
|
|
|
1332 } rb15 where
|
|
|
1333 rb01 : bt (Color ∧ A)
|
|
|
1334 rb01 = to-black (node kp vp (node rkey vr rp-left rp-right) (to-red (node kg vg n1 (PG.uncle pg))))
|
|
|
1335 rb04 : key < kp
|
|
|
1336 rb04 = lt
|
|
|
1337 rb16 : color n1 ≡ Black
|
|
|
1338 rb16 = proj2 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) x rb09) (trans (cong color (sym x)) pcolor))
|
|
|
1339 rb13 : ⟪ Red , proj2 vp ⟫ ≡ vp
|
|
|
1340 rb13 with subst (λ k → color k ≡ Red ) x pcolor
|
|
|
1341 ... | refl = refl
|
|
|
1342 rb14 : ⟪ Black , proj2 vg ⟫ ≡ vg
|
|
|
1343 rb14 with RBtreeParentColorBlack _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02) (case1 pcolor)
|
|
|
1344 ... | refl = refl
|
|
|
1345 rb10 : node kp ⟪ Black , proj2 vp ⟫ repl (node kg ⟪ Red , proj2 vg ⟫ n1 (PG.uncle pg)) ≡ rb01
|
|
|
1346 rb10 = begin
|
|
|
1347 to-black (node kp vp repl (to-red (node kg vg n1 (PG.uncle pg)))) ≡⟨ cong (λ k → node _ _ k _) (sym eq) ⟩
|
|
|
1348 rb01 ∎ where open ≡-Reasoning
|
|
|
1349 rb12 : node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) (PG.uncle pg) ≡ PG.grand pg
|
|
|
1350 rb12 = begin
|
|
|
1351 node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) (PG.uncle pg)
|
|
|
1352 ≡⟨ cong₂ (λ j k → node kg j (node kp k (RBI.tree r) n1) (PG.uncle pg) ) rb14 rb13 ⟩
|
|
|
1353 node kg vg _ (PG.uncle pg) ≡⟨ cong (λ k → node _ _ k _) (sym x) ⟩
|
|
|
1354 node kg vg (PG.parent pg) (PG.uncle pg) ≡⟨ sym x₁ ⟩
|
|
|
1355 PG.grand pg ∎ where open ≡-Reasoning
|
|
|
1356 rb05 : RBtreeInvariant (PG.uncle pg)
|
|
|
1357 rb05 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02)
|
|
|
1358 rb06 : RBtreeInvariant n1
|
|
|
1359 rb06 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x rb09)
|
|
|
1360 rb19 : black-depth n1 ≡ black-depth (PG.uncle pg)
|
|
|
1361 rb19 = trans (sym ( proj2 (red-children-eq x (sym (cong proj1 rb13)) rb09) )) (RBtreeEQ (subst (λ k → RBtreeInvariant k) x₁ rb02))
|
|
|
1362 rb18 : black-depth repl ≡ black-depth n1 ⊔ black-depth (PG.uncle pg)
|
|
|
1363 rb18 = ?
|
|
|
1364 rb17 : suc (black-depth (node rkey vr rp-left rp-right) ⊔ (black-depth n1 ⊔ black-depth (PG.uncle pg))) ≡ black-depth (PG.grand pg)
|
|
|
1365 rb17 = ?
|
|
|
1366 ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase52 where
|
|
|
1367 insertCase52 : t
|
|
|
1368 insertCase52 = next (PG.grand pg ∷ PG.rest pg) record {
|
|
|
1369 tree = PG.grand pg
|
|
|
1370 ; repl = rb01
|
|
|
1371 ; origti = RBI.origti r
|
|
|
1372 ; origrb = RBI.origrb r
|
|
|
1373 ; treerb = rb02
|
|
|
1374 ; replrb = rb10
|
|
|
1375 ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
|
|
|
1376 ; state = rebuild rb33 rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ()))
|
|
|
1377 } rb15 where
|
|
|
1378 -- inner case, repl is decomposed
|
|
|
1379 -- lt : kp < key
|
|
|
1380 -- x : PG.parent pg ≡ node kp vp n1 (RBI.tree r)
|
|
|
1381 -- x₁ : PG.grand pg ≡ node kg vg (PG.parent pg) (PG.uncle pg)
|
|
|
1382 -- eq : node rkey vr rp-left rp-right ≡ RBI.repl r
|
|
|
1383 rb01 : bt (Color ∧ A)
|
|
|
1384 rb01 = to-black (node rkey vr (node kp vp n1 rp-left) (to-red (node kg vg rp-right (PG.uncle pg))))
|
|
|
1385 rb04 : kp < key
|
|
|
1386 rb04 = lt
|
|
|
1387 rb21 : key < kg -- this can be a part of ParentGand relation
|
|
|
1388 rb21 = si-property-< (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) (subst (λ k → treeInvariant k ) x₁ (siToTreeinvariant _ _ _ _ (RBI.origti r)
|
|
|
1389 (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))))
|
|
|
1390 (subst (λ k → stackInvariant key _ orig (PG.parent pg ∷ k ∷ PG.rest pg)) x₁ (popStackInvariant _ _ _ _ _ rb00))
|
|
|
1391 rb16 : color n1 ≡ Black
|
|
|
1392 rb16 = proj1 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) x rb09) (trans (cong color (sym x)) pcolor))
|
|
|
1393 rb13 : ⟪ Red , proj2 vp ⟫ ≡ vp
|
|
|
1394 rb13 with subst (λ k → color k ≡ Red ) x pcolor
|
|
|
1395 ... | refl = refl
|
|
|
1396 rb14 : ⟪ Black , proj2 vg ⟫ ≡ vg
|
|
|
1397 rb14 with RBtreeParentColorBlack _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02) (case1 pcolor)
|
|
|
1398 ... | refl = refl
|
|
|
1399 rb33 : color (PG.grand pg) ≡ Black
|
|
|
1400 rb33 = subst (λ k → color k ≡ Black ) (sym x₁) (sym (cong proj1 rb14))
|
|
|
1401 rb23 : vr ≡ ⟪ Red , proj2 vr ⟫
|
|
|
1402 rb23 with subst (λ k → color k ≡ Red ) (sym eq) repl-red
|
|
|
1403 ... | refl = refl
|
|
|
1404 rb20 : color rp-right ≡ Black
|
|
|
1405 rb20 = proj2 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r) ) (cong proj1 rb23))
|
|
|
1406 rb24 : node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r)) (PG.uncle pg) ≡ PG.grand pg
|
|
|
1407 rb24 = trans (trans (cong₂ (λ j k → node kg j (node kp k n1 (RBI.tree r)) (PG.uncle pg)) rb14 rb13 ) (cong (λ k → node kg vg k (PG.uncle pg)) (sym x))) (sym x₁)
|
|
|
1408 rb25 : node rkey ⟪ Black , proj2 vr ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg)) ≡ rb01
|
|
|
1409 rb25 = begin
|
|
|
1410 node rkey ⟪ Black , proj2 vr ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg))
|
|
|
1411 ≡⟨ cong (λ k → node _ _ (node kp k n1 rp-left) _ ) rb13 ⟩
|
|
|
1412 node rkey ⟪ Black , proj2 vr ⟫ (node kp vp n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg)) ≡⟨ refl ⟩
|
|
|
1413 rb01 ∎ where open ≡-Reasoning
|
|
|
1414 rb05 : RBtreeInvariant (PG.uncle pg)
|
|
|
1415 rb05 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02)
|
|
|
1416 rb06 : RBtreeInvariant n1
|
|
|
1417 rb06 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x rb09)
|
|
|
1418 rb26 : RBtreeInvariant rp-left
|
|
|
1419 rb26 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r))
|
|
|
1420 rb28 : RBtreeInvariant rp-right
|
|
|
1421 rb28 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r))
|
|
|
1422 rb31 : RBtreeInvariant (node rkey vr rp-left rp-right )
|
|
|
1423 rb31 = subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)
|
|
|
1424 rb18 : black-depth rp-right ≡ black-depth (PG.uncle pg)
|
|
|
1425 rb18 = ?
|
|
|
1426 rb27 : black-depth n1 ≡ black-depth rp-left
|
|
|
1427 rb27 = ?
|
|
|
1428 rb19 : black-depth (node kp vp n1 rp-left) ≡ black-depth rp-right ⊔ black-depth (PG.uncle pg)
|
|
|
1429 rb19 = begin
|
|
|
1430 black-depth (node kp vp n1 rp-left) ≡⟨ black-depth-resp A (node kp vp n1 rp-left) (node kp vp rp-left rp-left) refl refl refl rb27 refl ⟩
|
|
|
1431 black-depth (node kp vp rp-left rp-left) ≡⟨ black-depth-resp A (node kp vp rp-left rp-left) (node rkey vr rp-left rp-right)
|
|
|
1432 refl refl (trans (sym (cong proj1 rb13)) (sym (cong proj1 rb23))) refl (RBtreeEQ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r))) ⟩
|
|
|
1433 black-depth (node rkey vr rp-left rp-right) ≡⟨ black-depth-cong A eq ⟩
|
|
|
1434 black-depth (RBI.repl r) ≡⟨ proj2 (red-children-eq1 (sym eq) repl-red (RBI.replrb r)) ⟩
|
|
|
1435 black-depth rp-right ≡⟨ sym ( ⊔-idem _ ) ⟩
|
|
|
1436 black-depth rp-right ⊔ black-depth rp-right ≡⟨ cong (λ k → black-depth rp-right ⊔ k) rb18 ⟩
|
|
|
1437 black-depth rp-right ⊔ black-depth (PG.uncle pg) ∎
|
|
|
1438 where open ≡-Reasoning
|
|
|
1439 rb29 : color n1 ≡ Black
|
|
|
1440 rb29 = proj1 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) x rb09) (sym (cong proj1 rb13)) )
|
|
|
1441 rb30 : color rp-left ≡ Black
|
|
|
1442 rb30 = proj1 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)) (cong proj1 rb23))
|
|
|
1443 rb32 : suc (black-depth (PG.uncle pg)) ≡ black-depth (PG.grand pg)
|
|
|
1444 rb32 = sym (proj2 ( black-children-eq1 x₁ rb33 rb02 ))
|
|
|
1445 rb10 : RBtreeInvariant (node rkey ⟪ Black , proj2 vr ⟫ (node kp vp n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg)))
|
|
|
1446 rb10 = rb-black _ _ rb19 (rbi-from-red-black _ _ kp vp rb06 rb26 rb27 rb29 rb30 rb13) (rb-red _ _ rb20 uncle-black rb18 rb28 rb05)
|
|
|
1447 rb17 : suc (black-depth (node kp vp n1 rp-left) ⊔ (black-depth rp-right ⊔ black-depth (PG.uncle pg))) ≡ black-depth (PG.grand pg)
|
|
|
1448 rb17 = begin
|
|
|
1449 suc (black-depth (node kp vp n1 rp-left) ⊔ (black-depth rp-right ⊔ black-depth (PG.uncle pg))) ≡⟨ cong (λ k → suc (k ⊔ _)) rb19 ⟩
|
|
|
1450 suc ((black-depth rp-right ⊔ black-depth (PG.uncle pg)) ⊔ (black-depth rp-right ⊔ black-depth (PG.uncle pg))) ≡⟨ cong suc ( ⊔-idem _) ⟩
|
|
|
1451 suc (black-depth rp-right ⊔ black-depth (PG.uncle pg)) ≡⟨ cong (λ k → suc (k ⊔ _)) rb18 ⟩
|
|
|
1452 suc (black-depth (PG.uncle pg) ⊔ black-depth (PG.uncle pg)) ≡⟨ cong suc (⊔-idem _) ⟩
|
|
|
1453 suc (black-depth (PG.uncle pg)) ≡⟨ rb32 ⟩
|
|
|
1454 black-depth (PG.grand pg) ∎
|
|
|
1455 where open ≡-Reasoning
|
|
|
1456 ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase52 where
|
|
|
1457 insertCase52 : t
|
|
|
1458 insertCase52 = next (PG.grand pg ∷ PG.rest pg) record {
|
|
|
1459 tree = PG.grand pg
|
|
|
1460 ; repl = rb01
|
|
|
1461 ; origti = RBI.origti r
|
|
|
1462 ; origrb = RBI.origrb r
|
|
|
1463 ; treerb = rb02
|
|
|
1464 ; replrb = rb10
|
|
|
1465 ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
|
|
|
1466 ; state = rebuild rb33 rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ()))
|
|
|
1467 } rb15 where
|
|
|
1468 -- inner case, repl is decomposed
|
|
|
1469 -- lt : key < kp
|
|
|
1470 -- x : PG.parent pg ≡ node kp vp (RBI.tree r) n1
|
|
|
1471 -- x₁ : PG.grand pg ≡ node kg vg (PG.uncle pg) (PG.parent pg)
|
|
|
1472 -- eq : node rkey vr rp-left rp-right ≡ RBI.repl r
|
|
|
1473 rb01 : bt (Color ∧ A)
|
|
|
1474 rb01 = to-black (node rkey vr (to-red (node kg vg (PG.uncle pg) rp-left )) (node kp vp rp-right n1))
|
|
|
1475 rb04 : key < kp
|
|
|
1476 rb04 = lt
|
|
|
1477 rb21 : kg < key -- this can be a part of ParentGand relation
|
|
|
1478 rb21 = si-property-> (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) (subst (λ k → treeInvariant k ) x₁ (siToTreeinvariant _ _ _ _ (RBI.origti r)
|
|
|
1479 (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))))
|
|
|
1480 (subst (λ k → stackInvariant key _ orig (PG.parent pg ∷ k ∷ PG.rest pg)) x₁ (popStackInvariant _ _ _ _ _ rb00))
|
|
|
1481 rb16 : color n1 ≡ Black
|
|
|
1482 rb16 = proj2 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) x rb09) (trans (cong color (sym x)) pcolor))
|
|
|
1483 rb13 : ⟪ Red , proj2 vp ⟫ ≡ vp
|
|
|
1484 rb13 with subst (λ k → color k ≡ Red ) x pcolor
|
|
|
1485 ... | refl = refl
|
|
|
1486 rb14 : ⟪ Black , proj2 vg ⟫ ≡ vg
|
|
|
1487 rb14 with RBtreeParentColorBlack _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02) (case2 pcolor)
|
|
|
1488 ... | refl = refl
|
|
|
1489 rb33 : color (PG.grand pg) ≡ Black
|
|
|
1490 rb33 = subst (λ k → color k ≡ Black ) (sym x₁) (sym (cong proj1 rb14))
|
|
|
1491 rb23 : vr ≡ ⟪ Red , proj2 vr ⟫
|
|
|
1492 rb23 with subst (λ k → color k ≡ Red ) (sym eq) repl-red
|
|
|
1493 ... | refl = refl
|
|
|
1494 rb20 : color rp-right ≡ Black
|
|
|
1495 rb20 = proj2 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r) ) (cong proj1 rb23))
|
|
|
1496 rb24 : node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) ≡ PG.grand pg
|
|
|
1497 rb24 = begin
|
|
|
1498 node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1)
|
|
|
1499 ≡⟨ cong₂ (λ j k → node kg j (PG.uncle pg) (node kp k (RBI.tree r) n1) ) rb14 rb13 ⟩
|
|
|
1500 node kg vg (PG.uncle pg) (node kp vp (RBI.tree r) n1) ≡⟨ cong (λ k → node kg vg (PG.uncle pg) k ) (sym x) ⟩
|
|
|
1501 node kg vg (PG.uncle pg) (PG.parent pg) ≡⟨ sym x₁ ⟩
|
|
|
1502 PG.grand pg ∎ where open ≡-Reasoning
|
|
|
1503 rb25 : node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left) (node kp ⟪ Red , proj2 vp ⟫ rp-right n1) ≡ rb01
|
|
|
1504 rb25 = begin
|
|
|
1505 node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left) (node kp ⟪ Red , proj2 vp ⟫ rp-right n1)
|
|
|
1506 ≡⟨ cong (λ k → node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left) (node kp k rp-right n1)) rb13 ⟩
|
|
|
1507 node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left) (node kp vp rp-right n1) ≡⟨ refl ⟩
|
|
|
1508 rb01 ∎ where open ≡-Reasoning
|
|
|
1509 rb05 : RBtreeInvariant (PG.uncle pg)
|
|
|
1510 rb05 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02)
|
|
|
1511 rb06 : RBtreeInvariant n1
|
|
|
1512 rb06 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x rb09)
|
|
|
1513 rb26 : RBtreeInvariant rp-left
|
|
|
1514 rb26 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r))
|
|
|
1515 rb28 : RBtreeInvariant rp-right
|
|
|
1516 rb28 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r))
|
|
|
1517 rb31 : RBtreeInvariant (node rkey vr rp-left rp-right )
|
|
|
1518 rb31 = subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)
|
|
|
1519 rb18 : black-depth (PG.uncle pg) ≡ black-depth rp-left
|
|
|
1520 rb18 = ?
|
|
|
1521 rb27 : black-depth rp-right ≡ black-depth n1
|
|
|
1522 rb27 = ?
|
|
|
1523 rb19 : black-depth (PG.uncle pg) ⊔ black-depth rp-left ≡ black-depth (node kp vp rp-right n1)
|
|
|
1524 rb19 = sym ( begin
|
|
|
1525 black-depth (node kp vp rp-right n1) ≡⟨ black-depth-resp A (node kp vp rp-right n1) (node kp vp rp-right rp-right) refl refl refl refl (sym rb27) ⟩
|
|
|
1526 black-depth (node kp vp rp-right rp-right) ≡⟨ black-depth-resp A (node kp vp rp-right rp-right) (node rkey vr rp-left rp-right)
|
|
|
1527 refl refl (trans (sym (cong proj1 rb13)) (sym (cong proj1 rb23))) (sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)))) refl ⟩
|
|
|
1528 black-depth (node rkey vr rp-left rp-right) ≡⟨ black-depth-cong A eq ⟩
|
|
|
1529 black-depth (RBI.repl r) ≡⟨ proj1 (red-children-eq1 (sym eq) repl-red (RBI.replrb r)) ⟩
|
|
|
1530 black-depth rp-left ≡⟨ sym ( ⊔-idem _ ) ⟩
|
|
|
1531 black-depth rp-left ⊔ black-depth rp-left ≡⟨ cong (λ k → k ⊔ black-depth rp-left ) (sym rb18) ⟩
|
|
|
1532 black-depth (PG.uncle pg) ⊔ black-depth rp-left ∎ )
|
|
|
1533 where open ≡-Reasoning
|
|
|
1534 rb29 : color n1 ≡ Black
|
|
|
1535 rb29 = proj2 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) x rb09) (sym (cong proj1 rb13)) )
|
|
|
1536 rb30 : color rp-left ≡ Black
|
|
|
1537 rb30 = proj1 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)) (cong proj1 rb23))
|
|
|
1538 rb32 : suc (black-depth (PG.uncle pg)) ≡ black-depth (PG.grand pg)
|
|
|
1539 rb32 = sym (proj1 ( black-children-eq1 x₁ rb33 rb02 ))
|
|
|
1540 rb10 : RBtreeInvariant (node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left ) (node kp vp rp-right n1) )
|
|
|
1541 rb10 = rb-black _ _ rb19 (rb-red _ _ uncle-black rb30 rb18 rb05 rb26 ) (rbi-from-red-black _ _ _ _ rb28 rb06 rb27 rb20 rb16 rb13 )
|
|
|
1542 rb17 : suc (black-depth (PG.uncle pg) ⊔ black-depth rp-left ⊔ black-depth (node kp vp rp-right n1)) ≡ black-depth (PG.grand pg)
|
|
|
1543 rb17 = begin
|
|
|
1544 suc (black-depth (PG.uncle pg) ⊔ black-depth rp-left ⊔ black-depth (node kp vp rp-right n1)) ≡⟨ cong (λ k → suc (_ ⊔ k)) (sym rb19) ⟩
|
|
|
1545 suc (black-depth (PG.uncle pg) ⊔ black-depth rp-left ⊔ (black-depth (PG.uncle pg) ⊔ black-depth rp-left)) ≡⟨ cong suc ( ⊔-idem _) ⟩
|
|
|
1546 suc (black-depth (PG.uncle pg) ⊔ black-depth rp-left ) ≡⟨ cong (λ k → suc (_ ⊔ k)) (sym rb18) ⟩
|
|
|
1547 suc (black-depth (PG.uncle pg) ⊔ black-depth (PG.uncle pg)) ≡⟨ cong suc (⊔-idem _) ⟩
|
|
|
1548 suc (black-depth (PG.uncle pg)) ≡⟨ rb32 ⟩
|
|
|
1549 black-depth (PG.grand pg) ∎
|
|
|
1550 where open ≡-Reasoning
|
|
|
1551 ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase52 where
|
|
|
1552 insertCase52 : t
|
|
|
1553 insertCase52 = next (PG.grand pg ∷ PG.rest pg) record {
|
|
|
1554 tree = PG.grand pg
|
|
|
1555 ; repl = rb01
|
|
|
1556 ; origti = RBI.origti r
|
|
|
1557 ; origrb = RBI.origrb r
|
|
|
1558 ; treerb = rb02
|
|
|
1559 ; replrb = subst (λ k → RBtreeInvariant k) rb10 (rb-black _ _ rb18 (rb-red _ _ uncle-black rb16 rb19 rb05 rb06) (RBI.replrb r) )
|
|
|
1560 ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
|
|
|
1561 ; state = rebuild rb33 rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ()))
|
|
|
1562 } rb15 where
|
|
|
1563 -- outer case, repl is not decomposed
|
|
|
1564 -- lt : kp < key
|
|
|
1565 -- x : PG.parent pg ≡ node kp vp n1 (RBI.tree r)
|
|
|
1566 -- x₁ : PG.grand pg ≡ node kg vg (PG.uncle pg) (PG.parent pg)
|
|
|
1567 rb01 : bt (Color ∧ A)
|
|
|
1568 rb01 = to-black (node kp vp (to-red (node kg vg (PG.uncle pg) n1) )(node rkey vr rp-left rp-right))
|
|
|
1569 rb04 : kp < key
|
|
|
1570 rb04 = lt
|
|
|
1571 rb16 : color n1 ≡ Black
|
|
|
1572 rb16 = proj1 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) x rb09) (trans (cong color (sym x)) pcolor))
|
|
|
1573 rb13 : ⟪ Red , proj2 vp ⟫ ≡ vp
|
|
|
1574 rb13 with subst (λ k → color k ≡ Red ) x pcolor
|
|
|
1575 ... | refl = refl
|
|
|
1576 rb14 : ⟪ Black , proj2 vg ⟫ ≡ vg
|
|
|
1577 rb14 with RBtreeParentColorBlack _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02) (case2 pcolor)
|
|
|
1578 ... | refl = refl
|
|
|
1579 rb33 : color (PG.grand pg) ≡ Black
|
|
|
1580 rb33 = subst (λ k → color k ≡ Black ) (sym x₁) (sym (cong proj1 rb14))
|
|
|
1581 rb10 : node kp ⟪ Black , proj2 vp ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) n1 ) repl ≡ rb01
|
|
|
1582 rb10 = cong (λ k → node _ _ _ k ) (sym eq)
|
|
|
1583 rb12 : node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r)) ≡ PG.grand pg
|
|
|
1584 rb12 = begin
|
|
|
1585 node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r))
|
|
|
1586 ≡⟨ cong₂ (λ j k → node kg j (PG.uncle pg) (node kp k n1 (RBI.tree r) ) ) rb14 rb13 ⟩
|
|
|
1587 node kg vg (PG.uncle pg) _ ≡⟨ cong (λ k → node _ _ _ k) (sym x) ⟩
|
|
|
1588 node kg vg (PG.uncle pg) (PG.parent pg) ≡⟨ sym x₁ ⟩
|
|
|
1589 PG.grand pg ∎ where open ≡-Reasoning
|
|
|
1590 rb05 : RBtreeInvariant (PG.uncle pg)
|
|
|
1591 rb05 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02)
|
|
|
1592 rb06 : RBtreeInvariant n1
|
|
|
1593 rb06 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x rb09)
|
|
|
1594 rb19 : black-depth (PG.uncle pg) ≡ black-depth n1
|
|
|
1595 rb19 = sym (trans (sym ( proj1 (red-children-eq x (sym (cong proj1 rb13)) rb09) )) (sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) x₁ rb02))))
|
|
|
1596 rb18 : black-depth (PG.uncle pg) ⊔ black-depth n1 ≡ black-depth repl
|
|
|
1597 rb18 = ?
|
|
|
1598 rb17 : suc (black-depth (PG.uncle pg) ⊔ black-depth n1 ⊔ black-depth (node rkey vr rp-left rp-right)) ≡ black-depth (PG.grand pg)
|
|
|
1599 rb17 = ?
|
|
|
1600 replaceRBP1 : t
|
|
|
1601 replaceRBP1 with RBI.state r
|
|
|
1602 ... | rebuild ceq bdepth-eq ¬leaf = rebuildCase ceq bdepth-eq ¬leaf
|
|
|
1603 ... | top-black eq = exit stack (trans eq (cong (λ k → k ∷ []) rb00)) r where
|
|
|
1604 rb00 : RBI.tree r ≡ orig
|
|
|
1605 rb00 with si-property-last _ _ _ _ (subst (λ k → stackInvariant key (RBI.tree r) orig k) (eq) (RBI.si r))
|
|
|
1606 ... | refl = refl
|
|
|
1607 ... | rotate _ repl-red with stackToPG (RBI.tree r) orig stack (RBI.si r)
|
|
|
1608 ... | case1 eq = exit stack eq r -- no stack, replace top node
|
|
|
1609 ... | case2 (case1 eq) = insertCase4 orig refl eq (case1 repl-red) (RBI.si r) -- one level stack, orig is parent of repl
|
|
|
1610 ... | case2 (case2 pg) with color (PG.parent pg) in pcolor
|
|
|
1611 ... | Black = insertCase1 where
|
|
|
1612 -- Parent is Black, make color repl ≡ color tree then goto rebuildCase
|
|
|
1613 rb00 : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
|
|
|
1614 rb00 pg = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r)
|
|
|
1615 treerb : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → RBtreeInvariant (PG.parent pg)
|
|
|
1616 treerb pg = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (rb00 pg))
|
|
|
1617 rb08 : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → treeInvariant (PG.parent pg)
|
|
|
1618 rb08 pg = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (rb00 pg))
|
|
|
1619 insertCase1 : t
|
|
|
1620 insertCase1 with PG.pg pg
|
|
|
1621 ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
|
|
|
1622 tree = PG.parent pg
|
|
|
1623 ; repl = rb01
|
|
|
1624 ; origti = RBI.origti r
|
|
|
1625 ; origrb = RBI.origrb r
|
|
|
1626 ; treerb = treerb pg
|
|
|
1627 ; replrb = rb06
|
|
|
1628 ; si = popStackInvariant _ _ _ _ _ (rb00 pg)
|
|
|
1629 ; state = rebuild (cong color x) (rb05 (trans (sym (cong color x)) pcolor)) (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ()))
|
|
|
1630 } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where
|
|
|
1631 rb01 : bt (Color ∧ A)
|
|
|
1632 rb01 = node kp vp repl n1
|
|
|
1633 rb03 : key < kp
|
|
|
1634 rb03 = lt
|
|
|
1635 rb04 : ⟪ Black , proj2 vp ⟫ ≡ vp
|
|
|
1636 rb04 with subst (λ k → color k ≡ Black) x pcolor
|
|
|
1637 ... | refl = refl
|
|
|
1638 rb07 : black-depth repl ≡ black-depth n1
|
|
|
1639 rb07 = ?
|
|
|
1640 rb05 : proj1 vp ≡ Black → black-depth rb01 ≡ black-depth (PG.parent pg)
|
|
|
1641 rb05 refl = ?
|
|
|
1642 rb06 : RBtreeInvariant rb01
|
|
|
1643 rb06 = subst (λ k → RBtreeInvariant (node kp k repl n1)) rb04
|
|
|
1644 ( rb-black _ _ rb07 (RBI.replrb r) (RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x (treerb pg))))
|
|
|
1645 ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
|
|
|
1646 tree = PG.parent pg
|
|
|
1647 ; repl = rb01
|
|
|
1648 ; origti = RBI.origti r
|
|
|
1649 ; origrb = RBI.origrb r
|
|
|
1650 ; treerb = treerb pg
|
|
|
1651 ; replrb = rb06
|
|
|
1652 ; si = popStackInvariant _ _ _ _ _ (rb00 pg)
|
|
|
1653 ; state = rebuild (cong color x) (rb05 (trans (sym (cong color x)) pcolor)) (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ()))
|
|
|
1654
|
|
|
1655 } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where
|
|
|
1656 --- x : PG.parent pg ≡ node kp vp n1 (RBI.tree r)
|
|
|
1657 --- x₁ : PG.grand pg ≡ node kg vg (PG.parent pg) (PG.uncle pg)
|
|
|
1658 rb01 : bt (Color ∧ A)
|
|
|
1659 rb01 = node kp vp n1 repl
|
|
|
1660 rb03 : kp < key
|
|
|
1661 rb03 = lt
|
|
|
1662 rb04 : ⟪ Black , proj2 vp ⟫ ≡ vp
|
|
|
1663 rb04 with subst (λ k → color k ≡ Black) x pcolor
|
|
|
1664 ... | refl = refl
|
|
|
1665 rb07 : black-depth repl ≡ black-depth n1
|
|
|
1666 rb07 = ?
|
|
|
1667 rb05 : proj1 vp ≡ Black → black-depth rb01 ≡ black-depth (PG.parent pg)
|
|
|
1668 rb05 refl = ?
|
|
|
1669 rb06 : RBtreeInvariant rb01
|
|
|
1670 rb06 = subst (λ k → RBtreeInvariant (node kp k n1 repl )) rb04
|
|
|
1671 ( rb-black _ _ (sym rb07) (RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x (treerb pg))) (RBI.replrb r) )
|
|
|
1672 insertCase1 | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
|
|
|
1673 tree = PG.parent pg
|
|
|
1674 ; repl = rb01
|
|
|
1675 ; origti = RBI.origti r
|
|
|
1676 ; origrb = RBI.origrb r
|
|
|
1677 ; treerb = treerb pg
|
|
|
1678 ; replrb = rb06
|
|
|
1679 ; si = popStackInvariant _ _ _ _ _ (rb00 pg)
|
|
|
1680 ; state = rebuild (cong color x) (rb05 (trans (sym (cong color x)) pcolor)) (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ()))
|
|
|
1681 } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where
|
|
|
1682 rb01 : bt (Color ∧ A)
|
|
|
1683 rb01 = node kp vp repl n1
|
|
|
1684 rb03 : key < kp
|
|
|
1685 rb03 = lt
|
|
|
1686 rb04 : ⟪ Black , proj2 vp ⟫ ≡ vp
|
|
|
1687 rb04 with subst (λ k → color k ≡ Black) x pcolor
|
|
|
1688 ... | refl = refl
|
|
|
1689 rb07 : black-depth repl ≡ black-depth n1
|
|
|
1690 rb07 = ?
|
|
|
1691 rb05 : proj1 vp ≡ Black → black-depth rb01 ≡ black-depth (PG.parent pg)
|
|
|
1692 rb05 refl = ?
|
|
|
1693 rb06 : RBtreeInvariant rb01
|
|
|
1694 rb06 = subst (λ k → RBtreeInvariant (node kp k repl n1)) rb04
|
|
|
1695 ( rb-black _ _ rb07 (RBI.replrb r) (RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x (treerb pg))))
|
|
|
1696 insertCase1 | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
|
|
|
1697 tree = PG.parent pg
|
|
|
1698 ; repl = rb01
|
|
|
1699 ; origti = RBI.origti r
|
|
|
1700 ; origrb = RBI.origrb r
|
|
|
1701 ; treerb = treerb pg
|
|
|
1702 ; replrb = rb06
|
|
|
1703 ; si = popStackInvariant _ _ _ _ _ (rb00 pg)
|
|
|
1704 ; state = rebuild (cong color x) (rb05 (trans (sym (cong color x)) pcolor)) (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ()))
|
|
|
1705 } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where
|
|
|
1706 -- x : PG.parent pg ≡ node kp vp (RBI.tree r) n1
|
|
|
1707 -- x₁ : PG.grand pg ≡ node kg vg (PG.uncle pg) (PG.parent pg)
|
|
|
1708 rb01 : bt (Color ∧ A)
|
|
|
1709 rb01 = node kp vp n1 repl
|
|
|
1710 rb03 : kp < key
|
|
|
1711 rb03 = lt
|
|
|
1712 rb04 : ⟪ Black , proj2 vp ⟫ ≡ vp
|
|
|
1713 rb04 with subst (λ k → color k ≡ Black) x pcolor
|
|
|
1714 ... | refl = refl
|
|
|
1715 rb07 : black-depth repl ≡ black-depth n1
|
|
|
1716 rb07 = ?
|
|
|
1717 rb05 : proj1 vp ≡ Black → black-depth rb01 ≡ black-depth (PG.parent pg)
|
|
|
1718 rb05 refl = ?
|
|
|
1719 rb06 : RBtreeInvariant rb01
|
|
|
1720 rb06 = subst (λ k → RBtreeInvariant (node kp k n1 repl )) rb04
|
|
|
1721 ( rb-black _ _ (sym rb07) (RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x (treerb pg))) (RBI.replrb r) )
|
|
|
1722 ... | Red with PG.uncle pg in uneq
|
|
|
1723 ... | leaf = insertCase5 repl refl pg repl-red (cong color uneq) pcolor
|
|
|
1724 ... | node key₁ ⟪ Black , value₁ ⟫ t₁ t₂ = insertCase5 repl refl pg repl-red (cong color uneq) pcolor
|
|
|
1725 ... | node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ with PG.pg pg -- insertCase2 : uncle and parent are Red, flip color and go up by two level
|
|
|
1726 ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase2 where
|
|
|
1727 insertCase2 : t
|
|
|
1728 insertCase2 = next (PG.grand pg ∷ (PG.rest pg))
|
|
|
1729 record {
|
|
|
1730 tree = PG.grand pg
|
|
|
1731 ; repl = to-red (node kg vg (to-black (node kp vp repl n1)) (to-black (PG.uncle pg)))
|
|
|
1732 ; origti = RBI.origti r
|
|
|
1733 ; origrb = RBI.origrb r
|
|
|
1734 ; treerb = rb01
|
|
|
1735 ; replrb = rb-red _ _ refl (RBtreeToBlackColor _ rb02) rb12 (rb-black _ _ rb13 (RBI.replrb r) rb04) (RBtreeToBlack _ rb02)
|
|
|
1736 ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
|
|
|
1737 ; state = rotate _ refl
|
|
|
1738 } rb15 where
|
|
|
1739 rb00 : stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
|
|
|
1740 rb00 = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r)
|
|
|
1741 rb01 : RBtreeInvariant (PG.grand pg)
|
|
|
1742 rb01 = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))
|
|
|
1743 rb02 : RBtreeInvariant (PG.uncle pg)
|
|
|
1744 rb02 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01)
|
|
|
1745 rb03 : RBtreeInvariant (PG.parent pg)
|
|
|
1746 rb03 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01)
|
|
|
1747 rb04 : RBtreeInvariant n1
|
|
|
1748 rb04 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x rb03)
|
|
|
1749 rb05 : { tree : bt (Color ∧ A) } → tree ≡ PG.uncle pg → tree ≡ node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ → color (PG.uncle pg) ≡ Red
|
|
|
1750 rb05 refl refl = refl
|
|
|
1751 rb08 : treeInvariant (PG.parent pg)
|
|
|
1752 rb08 = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00)
|
|
|
1753 rb07 : treeInvariant (node kp vp (RBI.tree r) n1)
|
|
|
1754 rb07 = subst (λ k → treeInvariant k) x (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00))
|
|
|
1755 rb06 : key < kp
|
|
|
1756 rb06 = lt
|
|
|
1757 rb10 : vg ≡ ⟪ Black , proj2 vg ⟫
|
|
|
1758 rb10 with RBtreeParentColorBlack _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) (case1 pcolor)
|
|
|
1759 ... | refl = refl
|
|
|
1760 rb11 : vp ≡ ⟪ Red , proj2 vp ⟫
|
|
|
1761 rb11 with subst (λ k → color k ≡ Red) x pcolor
|
|
|
1762 ... | refl = refl
|
|
|
1763 rb09 : PG.grand pg ≡ node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) (PG.uncle pg)
|
|
|
1764 rb09 = begin
|
|
|
1765 PG.grand pg ≡⟨ x₁ ⟩
|
|
|
1766 node kg vg (PG.parent pg) (PG.uncle pg) ≡⟨ cong (λ k → node kg vg k (PG.uncle pg)) x ⟩
|
|
|
1767 node kg vg (node kp vp (RBI.tree r) n1) (PG.uncle pg) ≡⟨ cong₂ (λ j k → node kg j (node kp k (RBI.tree r) n1) (PG.uncle pg)) rb10 rb11 ⟩
|
|
|
1768 node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) (PG.uncle pg) ∎
|
|
|
1769 where open ≡-Reasoning
|
|
|
1770 rb13 : black-depth repl ≡ black-depth n1
|
|
|
1771 rb13 = ?
|
|
|
1772 rb12 : suc (black-depth repl ⊔ black-depth n1) ≡ black-depth (to-black (PG.uncle pg))
|
|
|
1773 rb12 = ?
|
|
|
1774 rb15 : suc (length (PG.rest pg)) < length stack
|
|
|
1775 rb15 = begin
|
|
|
1776 suc (suc (length (PG.rest pg))) ≤⟨ <-trans (n<1+n _) (n<1+n _) ⟩
|
|
|
1777 length (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) ≡⟨ cong length (sym (PG.stack=gp pg)) ⟩
|
|
|
1778 length stack ∎
|
|
|
1779 where open ≤-Reasoning
|
|
|
1780 ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase2 where
|
|
|
1781 insertCase2 : t
|
|
|
1782 insertCase2 = next (PG.grand pg ∷ (PG.rest pg))
|
|
|
1783 record {
|
|
|
1784 tree = PG.grand pg
|
|
|
1785 ; repl = to-red (node kg vg (to-black (node kp vp n1 repl)) (to-black (PG.uncle pg)) )
|
|
|
1786 ; origti = RBI.origti r
|
|
|
1787 ; origrb = RBI.origrb r
|
|
|
1788 ; treerb = rb01
|
|
|
1789 ; replrb = rb-red _ _ refl (RBtreeToBlackColor _ rb02) rb12 (rb-black _ _ (sym rb13) rb04 (RBI.replrb r)) (RBtreeToBlack _ rb02)
|
|
|
1790 ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
|
|
|
1791 ; state = rotate _ refl
|
|
|
1792 } rb15 where
|
|
|
1793 --
|
|
|
1794 -- lt : kp < key
|
|
|
1795 -- x : PG.parent pg ≡ node kp vp n1 (RBI.tree r)
|
|
|
1796 --- x₁ : PG.grand pg ≡ node kg vg (PG.parent pg) (PG.uncle pg)
|
|
|
1797 --
|
|
|
1798 rb00 : stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
|
|
|
1799 rb00 = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r)
|
|
|
1800 rb01 : RBtreeInvariant (PG.grand pg)
|
|
|
1801 rb01 = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))
|
|
|
1802 rb02 : RBtreeInvariant (PG.uncle pg)
|
|
|
1803 rb02 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01)
|
|
|
1804 rb03 : RBtreeInvariant (PG.parent pg)
|
|
|
1805 rb03 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01)
|
|
|
1806 rb04 : RBtreeInvariant n1
|
|
|
1807 rb04 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x rb03)
|
|
|
1808 rb05 : { tree : bt (Color ∧ A) } → tree ≡ PG.uncle pg → tree ≡ node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ → color (PG.uncle pg) ≡ Red
|
|
|
1809 rb05 refl refl = refl
|
|
|
1810 rb08 : treeInvariant (PG.parent pg)
|
|
|
1811 rb08 = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00)
|
|
|
1812 rb07 : treeInvariant (node kp vp n1 (RBI.tree r) )
|
|
|
1813 rb07 = subst (λ k → treeInvariant k) x (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00))
|
|
|
1814 rb06 : kp < key
|
|
|
1815 rb06 = lt
|
|
|
1816 rb21 : key < kg -- this can be a part of ParentGand relation
|
|
|
1817 rb21 = si-property-< (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) (subst (λ k → treeInvariant k ) x₁ (siToTreeinvariant _ _ _ _ (RBI.origti r)
|
|
|
1818 (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))))
|
|
|
1819 (subst (λ k → stackInvariant key _ orig (PG.parent pg ∷ k ∷ PG.rest pg)) x₁ (popStackInvariant _ _ _ _ _ rb00))
|
|
|
1820 rb10 : vg ≡ ⟪ Black , proj2 vg ⟫
|
|
|
1821 rb10 with RBtreeParentColorBlack _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) (case1 pcolor)
|
|
|
1822 ... | refl = refl
|
|
|
1823 rb11 : vp ≡ ⟪ Red , proj2 vp ⟫
|
|
|
1824 rb11 with subst (λ k → color k ≡ Red) x pcolor
|
|
|
1825 ... | refl = refl
|
|
|
1826 rb09 : node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r) ) (PG.uncle pg) ≡ PG.grand pg
|
|
|
1827 rb09 = sym ( begin
|
|
|
1828 PG.grand pg ≡⟨ x₁ ⟩
|
|
|
1829 node kg vg (PG.parent pg) (PG.uncle pg) ≡⟨ cong (λ k → node kg vg k (PG.uncle pg)) x ⟩
|
|
|
1830 node kg vg (node kp vp n1 (RBI.tree r) ) (PG.uncle pg) ≡⟨ cong₂ (λ j k → node kg j (node kp k n1 (RBI.tree r) ) (PG.uncle pg) ) rb10 rb11 ⟩
|
|
|
1831 node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r) ) (PG.uncle pg) ∎ )
|
|
|
1832 where open ≡-Reasoning
|
|
|
1833 rb13 : black-depth repl ≡ black-depth n1
|
|
|
1834 rb13 = ?
|
|
|
1835 rb12 : suc (black-depth n1 ⊔ black-depth repl) ≡ black-depth (to-black (PG.uncle pg))
|
|
|
1836 rb12 = ?
|
|
|
1837 rb15 : suc (length (PG.rest pg)) < length stack
|
|
|
1838 rb15 = begin
|
|
|
1839 suc (suc (length (PG.rest pg))) ≤⟨ <-trans (n<1+n _) (n<1+n _) ⟩
|
|
|
1840 length (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) ≡⟨ cong length (sym (PG.stack=gp pg)) ⟩
|
|
|
1841 length stack ∎
|
|
|
1842 where open ≤-Reasoning
|
|
|
1843 ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase2 where
|
|
|
1844 insertCase2 : t
|
|
|
1845 insertCase2 = next (PG.grand pg ∷ (PG.rest pg))
|
|
|
1846 record {
|
|
|
1847 tree = PG.grand pg
|
|
|
1848 ; repl = to-red (node kg vg (to-black (PG.uncle pg)) (to-black (node kp vp repl n1)) )
|
|
|
1849 ; origti = RBI.origti r
|
|
|
1850 ; origrb = RBI.origrb r
|
|
|
1851 ; treerb = rb01
|
|
|
1852 ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
|
|
|
1853 ; replrb = rb-red _ _ (RBtreeToBlackColor _ rb02) refl rb12 (RBtreeToBlack _ rb02) (rb-black _ _ rb13 (RBI.replrb r) rb04)
|
|
|
1854 ; state = rotate _ refl
|
|
|
1855 } rb15 where
|
|
|
1856 -- x : PG.parent pg ≡ node kp vp (RBI.tree r) n1
|
|
|
1857 -- x₁ : PG.grand pg ≡ node kg vg (PG.uncle pg) (PG.parent pg)
|
|
|
1858 rb00 : stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
|
|
|
1859 rb00 = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r)
|
|
|
1860 rb01 : RBtreeInvariant (PG.grand pg)
|
|
|
1861 rb01 = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))
|
|
|
1862 rb02 : RBtreeInvariant (PG.uncle pg)
|
|
|
1863 rb02 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01)
|
|
|
1864 rb03 : RBtreeInvariant (PG.parent pg)
|
|
|
1865 rb03 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01)
|
|
|
1866 rb04 : RBtreeInvariant n1
|
|
|
1867 rb04 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x rb03)
|
|
|
1868 rb05 : { tree : bt (Color ∧ A) } → tree ≡ PG.uncle pg → tree ≡ node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ → color (PG.uncle pg) ≡ Red
|
|
|
1869 rb05 refl refl = refl
|
|
|
1870 rb08 : treeInvariant (PG.parent pg)
|
|
|
1871 rb08 = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00)
|
|
|
1872 rb07 : treeInvariant (node kp vp (RBI.tree r) n1)
|
|
|
1873 rb07 = subst (λ k → treeInvariant k) x (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00))
|
|
|
1874 rb06 : key < kp
|
|
|
1875 rb06 = lt
|
|
|
1876 rb21 : kg < key -- this can be a part of ParentGand relation
|
|
|
1877 rb21 = si-property-> (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) (subst (λ k → treeInvariant k ) x₁ (siToTreeinvariant _ _ _ _ (RBI.origti r)
|
|
|
1878 (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))))
|
|
|
1879 (subst (λ k → stackInvariant key _ orig (PG.parent pg ∷ k ∷ PG.rest pg)) x₁ (popStackInvariant _ _ _ _ _ rb00))
|
|
|
1880 rb10 : vg ≡ ⟪ Black , proj2 vg ⟫
|
|
|
1881 rb10 with RBtreeParentColorBlack _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) (case2 pcolor)
|
|
|
1882 ... | refl = refl
|
|
|
1883 rb11 : vp ≡ ⟪ Red , proj2 vp ⟫
|
|
|
1884 rb11 with subst (λ k → color k ≡ Red) x pcolor
|
|
|
1885 ... | refl = refl
|
|
|
1886 rb09 : node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) ≡ PG.grand pg
|
|
|
1887 rb09 = sym ( begin
|
|
|
1888 PG.grand pg ≡⟨ x₁ ⟩
|
|
|
1889 node kg vg (PG.uncle pg) (PG.parent pg) ≡⟨ cong (λ k → node kg vg (PG.uncle pg) k) x ⟩
|
|
|
1890 node kg vg (PG.uncle pg) (node kp vp (RBI.tree r) n1) ≡⟨ cong₂ (λ j k → node kg j (PG.uncle pg) (node kp k (RBI.tree r) n1) ) rb10 rb11 ⟩
|
|
|
1891 node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) ∎ )
|
|
|
1892 where open ≡-Reasoning
|
|
|
1893 rb13 : black-depth repl ≡ black-depth n1
|
|
|
1894 rb13 = ?
|
|
|
1895 rb12 : black-depth (to-black (PG.uncle pg)) ≡ suc (black-depth repl ⊔ black-depth n1)
|
|
|
1896 rb12 = ?
|
|
|
1897 rb17 : suc (black-depth repl ⊔ black-depth n1) ⊔ black-depth (to-black (PG.uncle pg)) ≡ black-depth (PG.grand pg)
|
|
|
1898 rb17 = begin
|
|
|
1899 suc (black-depth repl ⊔ black-depth n1) ⊔ black-depth (to-black (PG.uncle pg)) ≡⟨ cong (λ k → k ⊔ black-depth (to-black (PG.uncle pg))) (sym rb12) ⟩
|
|
|
1900 black-depth (to-black (PG.uncle pg)) ⊔ black-depth (to-black (PG.uncle pg)) ≡⟨ ⊔-idem _ ⟩
|
|
|
1901 black-depth (to-black (PG.uncle pg)) ≡⟨ sym (to-black-eq (PG.uncle pg) (cong color uneq )) ⟩
|
|
|
1902 suc (black-depth (PG.uncle pg)) ≡⟨ sym ( proj1 (black-children-eq x₁ (cong proj1 rb10) rb01 )) ⟩
|
|
|
1903 black-depth (PG.grand pg) ∎
|
|
|
1904 where open ≡-Reasoning
|
|
|
1905 rb15 : suc (length (PG.rest pg)) < length stack
|
|
|
1906 rb15 = begin
|
|
|
1907 suc (suc (length (PG.rest pg))) ≤⟨ <-trans (n<1+n _) (n<1+n _) ⟩
|
|
|
1908 length (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) ≡⟨ cong length (sym (PG.stack=gp pg)) ⟩
|
|
|
1909 length stack ∎
|
|
|
1910 where open ≤-Reasoning
|
|
|
1911 ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase2 where
|
|
|
1912 --- lt : kp < key
|
|
|
1913 --- x : PG.parent pg ≡ node kp vp n1 (RBI.tree r)
|
|
|
1914 --- x₁ : PG.grand pg ≡ node kg vg (PG.uncle pg) (PG.parent pg)
|
|
|
1915 insertCase2 : t
|
|
|
1916 insertCase2 = next (PG.grand pg ∷ (PG.rest pg))
|
|
|
1917 record {
|
|
|
1918 tree = PG.grand pg
|
|
|
1919 ; repl = to-red (node kg vg (to-black (PG.uncle pg)) (to-black (node kp vp n1 repl )) )
|
|
|
1920 ; origti = RBI.origti r
|
|
|
1921 ; origrb = RBI.origrb r
|
|
|
1922 ; treerb = rb01
|
|
|
1923 ; replrb = rb-red _ _ (RBtreeToBlackColor _ rb02) refl rb12 (RBtreeToBlack _ rb02) (rb-black _ _ (sym rb13) rb04 (RBI.replrb r) )
|
|
|
1924 ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
|
|
|
1925 ; state = rotate _ refl
|
|
|
1926 } rb15 where
|
|
|
1927 rb00 : stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
|
|
|
1928 rb00 = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r)
|
|
|
1929 rb01 : RBtreeInvariant (PG.grand pg)
|
|
|
1930 rb01 = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))
|
|
|
1931 rb02 : RBtreeInvariant (PG.uncle pg)
|
|
|
1932 rb02 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01)
|
|
|
1933 rb03 : RBtreeInvariant (PG.parent pg)
|
|
|
1934 rb03 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01)
|
|
|
1935 rb04 : RBtreeInvariant n1
|
|
|
1936 rb04 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x rb03)
|
|
|
1937 rb05 : { tree : bt (Color ∧ A) } → tree ≡ PG.uncle pg → tree ≡ node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ → color (PG.uncle pg) ≡ Red
|
|
|
1938 rb05 refl refl = refl
|
|
|
1939 rb08 : treeInvariant (PG.parent pg)
|
|
|
1940 rb08 = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00)
|
|
|
1941 rb07 : treeInvariant (node kp vp n1 (RBI.tree r) )
|
|
|
1942 rb07 = subst (λ k → treeInvariant k) x (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00))
|
|
|
1943 rb06 : kp < key
|
|
|
1944 rb06 = lt
|
|
|
1945 rb10 : vg ≡ ⟪ Black , proj2 vg ⟫
|
|
|
1946 rb10 with RBtreeParentColorBlack _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) (case2 pcolor)
|
|
|
1947 ... | refl = refl
|
|
|
1948 rb11 : vp ≡ ⟪ Red , proj2 vp ⟫
|
|
|
1949 rb11 with subst (λ k → color k ≡ Red) x pcolor
|
|
|
1950 ... | refl = refl
|
|
|
1951 rb09 : PG.grand pg ≡ node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r) )
|
|
|
1952 rb09 = begin
|
|
|
1953 PG.grand pg ≡⟨ x₁ ⟩
|
|
|
1954 node kg vg (PG.uncle pg) (PG.parent pg) ≡⟨ cong (λ k → node kg vg (PG.uncle pg) k) x ⟩
|
|
|
1955 node kg vg (PG.uncle pg) (node kp vp n1 (RBI.tree r) ) ≡⟨ cong₂ (λ j k → node kg j (PG.uncle pg) (node kp k n1 (RBI.tree r) ) ) rb10 rb11 ⟩
|
|
|
1956 node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r) ) ∎
|
|
|
1957 where open ≡-Reasoning
|
|
|
1958 rb13 : black-depth repl ≡ black-depth n1
|
|
|
1959 rb13 = ?
|
|
|
1960 rb12 : black-depth (to-black (PG.uncle pg)) ≡ suc (black-depth n1 ⊔ black-depth repl)
|
|
|
1961 rb12 = ?
|
|
|
1962 rb15 : suc (length (PG.rest pg)) < length stack
|
|
|
1963 rb15 = begin
|
|
|
1964 suc (suc (length (PG.rest pg))) ≤⟨ <-trans (n<1+n _) (n<1+n _) ⟩
|
|
|
1965 length (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) ≡⟨ cong length (sym (PG.stack=gp pg)) ⟩
|
|
|
1966 length stack ∎
|
|
|
1967 where open ≤-Reasoning
|
|
|
1968
|
|
|
1969
|
|
|
1970 insertRBTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt (Color ∧ A)) → (key : ℕ) → (value : A)
|
|
|
1971 → treeInvariant tree → RBtreeInvariant tree
|
|
|
1972 → (exit : (stack : List (bt (Color ∧ A))) → stack ≡ (tree ∷ []) → RBI key value tree stack → t ) → t
|
|
|
1973 insertRBTreeP {n} {m} {A} {t} orig key value ti rbi exit = TerminatingLoopS (bt (Color ∧ A) ∧ List (bt (Color ∧ A)))
|
|
|
1974 {λ p → RBtreeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) orig (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ orig , orig ∷ [] ⟫ ⟪ rbi , s-nil ⟫
|
|
|
1975 $ λ p RBP findLoop → findRBT key (proj1 p) orig (proj2 p) RBP (λ t1 s1 P2 lt1 → findLoop ⟪ t1 , s1 ⟫ P2 lt1 )
|
|
|
1976 $ λ tr1 st P2 O → createRBT key value orig rbi ti tr1 st (proj2 P2) O
|
|
|
1977 $ λ st rbi → TerminatingLoopS (List (bt (Color ∧ A))) {λ stack → RBI key value orig stack }
|
|
|
1978 (λ stack → length stack ) st rbi
|
|
|
1979 $ λ stack rbi replaceLoop → replaceRBP key value orig stack rbi (λ stack1 rbi1 lt → replaceLoop stack1 rbi1 lt )
|
|
|
1980 $ λ stack eq r → exit stack eq r
|
|
|
1981
|
