Mercurial > hg > Gears > GearsAgda
diff RBTree.agda @ 954:08281092430b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 06 Oct 2024 17:59:51 +0900 |
| parents | 24255e0dd027 |
| children | 415915a840fe |
line wrap: on
line diff
--- a/RBTree.agda Fri Sep 13 13:25:17 2024 +0900 +++ b/RBTree.agda Sun Oct 06 17:59:51 2024 +0900 @@ -23,137 +23,11 @@ open import nat open import BTree +open import RBTreeBase +open import RBTree1 open _∧_ -data Color : Set where - Red : Color - Black : Color - -RB→bt : {n : Level} (A : Set n) → (bt (Color ∧ A)) → bt A -RB→bt {n} A leaf = leaf -RB→bt {n} A (node key ⟪ C , value ⟫ tr t1) = (node key value (RB→bt A tr) (RB→bt A t1)) - -color : {n : Level} {A : Set n} → (bt (Color ∧ A)) → Color -color leaf = Black -color (node key ⟪ C , value ⟫ rb rb₁) = C - -to-red : {n : Level} {A : Set n} → (tree : bt (Color ∧ A)) → bt (Color ∧ A) -to-red leaf = leaf -to-red (node key ⟪ _ , value ⟫ t t₁) = (node key ⟪ Red , value ⟫ t t₁) - -to-black : {n : Level} {A : Set n} → (tree : bt (Color ∧ A)) → bt (Color ∧ A) -to-black leaf = leaf -to-black (node key ⟪ _ , value ⟫ t t₁) = (node key ⟪ Black , value ⟫ t t₁) - -black-depth : {n : Level} {A : Set n} → (tree : bt (Color ∧ A) ) → ℕ -black-depth leaf = 1 -black-depth (node key ⟪ Red , value ⟫ t t₁) = black-depth t ⊔ black-depth t₁ -black-depth (node key ⟪ Black , value ⟫ t t₁) = suc (black-depth t ⊔ black-depth t₁ ) - -zero≢suc : { m : ℕ } → zero ≡ suc m → ⊥ -zero≢suc () -suc≢zero : {m : ℕ } → suc m ≡ zero → ⊥ -suc≢zero () - -data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where - rb-leaf : RBtreeInvariant leaf - rb-red : (key : ℕ) → (value : A) → {left right : bt (Color ∧ A)} - → color left ≡ Black → color right ≡ Black - → black-depth left ≡ black-depth right - → RBtreeInvariant left → RBtreeInvariant right - → RBtreeInvariant (node key ⟪ Red , value ⟫ left right) - rb-black : (key : ℕ) → (value : A) → {left right : bt (Color ∧ A)} - → black-depth left ≡ black-depth right - → RBtreeInvariant left → RBtreeInvariant right - → RBtreeInvariant (node key ⟪ Black , value ⟫ left right) - -RightDown : {n : Level} {A : Set n} → bt (Color ∧ A) → bt (Color ∧ A) -RightDown leaf = leaf -RightDown (node key ⟪ c , value ⟫ t1 t2) = t2 -LeftDown : {n : Level} {A : Set n} → bt (Color ∧ A) → bt (Color ∧ A) -LeftDown leaf = leaf -LeftDown (node key ⟪ c , value ⟫ t1 t2 ) = t1 - -RBtreeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color} - → (left right : bt (Color ∧ A)) - → RBtreeInvariant (node key ⟪ c , value ⟫ left right) - → RBtreeInvariant left -RBtreeLeftDown {n} {A} {key} {value} {c} left right rb = lem00 _ rb refl where - lem00 : (tree : bt (Color ∧ A) ) → ( rb : RBtreeInvariant tree ) → tree ≡ node key ⟪ c , value ⟫ left right → RBtreeInvariant left - lem00 _ rb-leaf () - lem00 (node key ⟪ c , value ⟫ _ _) (rb-red key value x x₁ x₂ rb rb₁) eq = subst (λ k → RBtreeInvariant k) (just-injective (cong node-left eq)) rb - lem00 (node key ⟪ c , value ⟫ _ _) (rb-black key value x rb rb₁) eq = subst (λ k → RBtreeInvariant k) (just-injective (cong node-left eq)) rb - - -RBtreeRightDown : {n : Level} {A : Set n} { key : ℕ} {value : A} {c : Color} - → (left right : bt (Color ∧ A)) - → RBtreeInvariant (node key ⟪ c , value ⟫ left right) - → RBtreeInvariant right -RBtreeRightDown {n} {A} {key} {value} {c} left right rb = lem00 _ rb refl where - lem00 : (tree : bt (Color ∧ A) ) → ( rb : RBtreeInvariant tree ) → tree ≡ node key ⟪ c , value ⟫ left right → RBtreeInvariant right - lem00 _ rb-leaf () - lem00 (node key ⟪ c , value ⟫ _ _) (rb-red key value x x₁ x₂ rb rb₁) eq = subst (λ k → RBtreeInvariant k) (just-injective (cong node-right eq)) rb₁ - lem00 (node key ⟪ c , value ⟫ _ _) (rb-black key value x rb rb₁) eq = subst (λ k → RBtreeInvariant k) (just-injective (cong node-right eq)) rb₁ - -RBtreeEQ : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color} - → {left right : bt (Color ∧ A)} - → RBtreeInvariant (node key ⟪ c , value ⟫ left right) - → black-depth left ≡ black-depth right -RBtreeEQ {n} {A} {key} {value} {c} {left} {right} rb = lem00 _ rb refl where - lem00 : (tree : bt (Color ∧ A) ) → ( rb : RBtreeInvariant tree ) → tree ≡ node key ⟪ c , value ⟫ left right → black-depth left ≡ black-depth right - lem00 _ rb-leaf () - lem00 (node key ⟪ c , value ⟫ _ _) (rb-red key value x x₁ x₂ rb rb₁) eq - = subst₂ (λ k l → black-depth k ≡ black-depth l) (just-injective (cong node-left eq)) (just-injective (cong node-right eq)) x₂ - lem00 (node key ⟪ c , value ⟫ _ _) (rb-black key value x rb rb₁) eq - = subst₂ (λ k l → black-depth k ≡ black-depth l) (just-injective (cong node-left eq)) (just-injective (cong node-right eq)) x - -RBtreeToBlack : {n : Level} {A : Set n} - → (tree : bt (Color ∧ A)) - → RBtreeInvariant tree - → RBtreeInvariant (to-black tree) -RBtreeToBlack {n} {A} tree rb = lem00 _ rb where - lem00 : (tree : bt (Color ∧ A) ) → ( rb : RBtreeInvariant tree ) → RBtreeInvariant (to-black tree) - lem00 _ rb-leaf = rb-leaf - lem00 (node key ⟪ c , value ⟫ left right) (rb-red key value x x₁ x₂ rb rb₁) = rb-black key value x₂ rb rb₁ - lem00 (node key ⟪ c , value ⟫ left right) (rb-black key value x rb rb₁) = rb-black key value x rb rb₁ - -RBtreeToBlackColor : {n : Level} {A : Set n} - → (tree : bt (Color ∧ A)) - → RBtreeInvariant tree - → color (to-black tree) ≡ Black -RBtreeToBlackColor {n} {A} _ rb-leaf = refl -RBtreeToBlackColor {n} {A} (node key ⟪ c , value ⟫ left right) (rb-red key value x x₁ x₂ rb rb₁) = refl -RBtreeToBlackColor {n} {A} (node key ⟪ c , value ⟫ left right) (rb-black key value x rb rb₁) = refl - -⊥-color : ( Black ≡ Red ) → ⊥ -⊥-color () - -RBtreeParentColorBlack : {n : Level} {A : Set n} → (left right : bt (Color ∧ A)) { value : A} {key : ℕ} { c : Color} - → RBtreeInvariant (node key ⟪ c , value ⟫ left right) - → (color left ≡ Red) ∨ (color right ≡ Red) - → c ≡ Black -RBtreeParentColorBlack {n} {A} left right {value} {key} {c} rb = lem00 _ rb refl where - lem00 : (tree : bt (Color ∧ A) ) → {c1 : Color } → ( rb : RBtreeInvariant tree ) - → (node key ⟪ c1 , value ⟫ left right ≡ tree) → (color left ≡ Red) ∨ (color right ≡ Red) → c1 ≡ Black - lem00 _ rb-leaf () - lem00 (node key ⟪ .Red , value ⟫ _ _) (rb-red key value x x₁ x₂ rb rb₁) eq (case1 left-red) - = ⊥-elim (⊥-color (sym (trans (trans (sym left-red) (cong color (just-injective (cong node-left eq)))) x))) - lem00 (node key ⟪ .Red , value ⟫ _ _) (rb-red key value x x₁ x₂ rb rb₁) eq (case2 right-red) - = ⊥-elim (⊥-color (sym (trans (trans (sym right-red) (cong color (just-injective (cong node-right eq)))) x₁ ))) - lem00 (node key ⟪ c , value ⟫ _ _) (rb-black key value x rb rb₁) eq p = cong color eq - -RBtreeChildrenColorBlack : {n : Level} {A : Set n} → (left right : bt (Color ∧ A)) { value : Color ∧ A} {key : ℕ} - → RBtreeInvariant (node key value left right) - → proj1 value ≡ Red - → (color left ≡ Black) ∧ (color right ≡ Black) -RBtreeChildrenColorBlack {n} {A} left right {value} {key} br pv=r = lem00 _ br refl where - lem00 : (tree : bt (Color ∧ A) ) → ( rb : RBtreeInvariant tree ) → tree ≡ node key value left right → (color left ≡ Black) ∧ (color right ≡ Black) - lem00 _ rb-leaf () - lem00 (node key value _ _) (rb-red key value₁ x x₁ x₂ rb rb₁) eq = ⟪ trans (sym (cong color (just-injective (cong node-left eq)))) x - , trans (sym (cong color (just-injective (cong node-right eq)))) x₁ ⟫ - lem00 (node key value _ _) (rb-black key value₁ x rb rb₁) eq = ⊥-elim ( ⊥-color (sym (trans (sym pv=r) (cong proj1 (sym (just-injective (cong node-value eq))))))) - -- -- findRBT exit with replaced node -- case-eq node value is replaced, just do replacedTree and rebuild rb-invariant @@ -205,955 +79,6 @@ -- findRBTreeTest = findTest 14 testRBTree0 testRBI0 -- $ λ tr s P O → (record {tree = tr ; stack = s ; ti = (proj1 P) ; si = (proj2 P)}) --- create replaceRBTree with rotate - -data replacedRBTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt (Color ∧ A) ) → Set n where - -- no rotation case - rbr-leaf : replacedRBTree key value leaf (node key ⟪ Red , value ⟫ leaf leaf) - rbr-node : {value₁ : A} → {ca : Color } → {t t₁ : bt (Color ∧ A)} - → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ ca , value ⟫ t t₁) - rbr-right : {k : ℕ } {v1 : A} → {ca : Color} → {t t1 t2 : bt (Color ∧ A)} - → color t2 ≡ color t - → k < key → replacedRBTree key value t2 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ ca , v1 ⟫ t1 t) - rbr-left : {k : ℕ } {v1 : A} → {ca : Color} → {t t1 t2 : bt (Color ∧ A)} - → color t1 ≡ color t - → key < k → replacedRBTree key value t1 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ ca , v1 ⟫ t t2) -- k < key → key < k - -- in all other case, color of replaced node is changed from Black to Red - -- case1 parent is black - rbr-black-right : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} - → color t₂ ≡ Red → key₁ < key → replacedRBTree key value t₁ t₂ - → replacedRBTree key value (node key₁ ⟪ Black , value₁ ⟫ t t₁) (node key₁ ⟪ Black , value₁ ⟫ t t₂) - rbr-black-left : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} - → color t₂ ≡ Red → key < key₁ → replacedRBTree key value t₁ t₂ - → replacedRBTree key value (node key₁ ⟪ Black , value₁ ⟫ t₁ t) (node key₁ ⟪ Black , value₁ ⟫ t₂ t) - - -- case2 both parent and uncle are red (should we check uncle color?), flip color and up - rbr-flip-ll : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - → color t₂ ≡ Red → color uncle ≡ Red → key < kp → replacedRBTree key value t₁ t₂ - → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t) uncle) - (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t₂ t) (to-black uncle)) - rbr-flip-lr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - → color t₂ ≡ Red → color uncle ≡ Red → kp < key → key < kg → replacedRBTree key value t₁ t₂ - → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) - (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t t₂) (to-black uncle)) - rbr-flip-rl : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - → color t₂ ≡ Red → color uncle ≡ Red → kg < key → key < kp → replacedRBTree key value t₁ t₂ - → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t)) - (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t₂ t)) - rbr-flip-rr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - → color t₂ ≡ Red → color uncle ≡ Red → kp < key → replacedRBTree key value t₁ t₂ - → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t t₁)) - (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t t₂)) - - -- case6 the node is outer, rotate grand - rbr-rotate-ll : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - → color t₂ ≡ Red → key < kp → replacedRBTree key value t₁ t₂ - → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t) uncle) - (node kp ⟪ Black , vp ⟫ t₂ (node kg ⟪ Red , vg ⟫ t uncle)) - rbr-rotate-rr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - → color t₂ ≡ Red → kp < key → replacedRBTree key value t₁ t₂ - → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t t₁)) - (node kp ⟪ Black , vp ⟫ (node kg ⟪ Red , vg ⟫ uncle t) t₂ ) - -- case56 the node is inner, make it outer and rotate grand - rbr-rotate-lr : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} - → color t₃ ≡ Black → kp < key → key < kg - → replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃) - → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) - (node kn ⟪ Black , vn ⟫ (node kp ⟪ Red , vp ⟫ t t₂) (node kg ⟪ Red , vg ⟫ t₃ uncle)) - rbr-rotate-rl : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} - → color t₃ ≡ Black → kg < key → key < kp - → replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃) - → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t)) - (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , vg ⟫ uncle t₂) (node kp ⟪ Red , vp ⟫ t₃ t)) - - --- --- Parent Grand Relation --- should we require stack-invariant? --- - -data ParentGrand {n : Level} {A : Set n} (key : ℕ) (self : bt A) : (parent uncle grand : bt A) → Set n where - s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } - → key < kp → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand key self parent n2 grand - s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } - → kp < key → parent ≡ node kp vp n1 self → grand ≡ node kg vg parent n2 → ParentGrand key self parent n2 grand - s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } - → key < kp → parent ≡ node kp vp self n1 → grand ≡ node kg vg n2 parent → ParentGrand key self parent n2 grand - s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } - → kp < key → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand key self parent n2 grand - -record PG {n : Level } (A : Set n) (key : ℕ) (self : bt A) (stack : List (bt A)) : Set n where - field - parent grand uncle : bt A - pg : ParentGrand key self parent uncle grand - rest : List (bt A) - stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest ) - --- --- RBI : Invariant on InsertCase2 --- color repl ≡ Red ∧ black-depth repl ≡ suc (black-depth tree) --- - -data RBI-state {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree repl : bt (Color ∧ A) ) → (stak : List (bt (Color ∧ A))) → Set n where - rebuild : {tree repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → color tree ≡ color repl → black-depth repl ≡ black-depth tree - → ¬ ( tree ≡ leaf) - → (rotated : replacedRBTree key value tree repl) - → RBI-state key value tree repl stack -- one stage up - rotate : (tree : bt (Color ∧ A)) → {repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → color repl ≡ Red - → (rotated : replacedRBTree key value tree repl) - → RBI-state key value tree repl stack -- two stages up - top-black : {tree repl : bt (Color ∧ A) } → {stack : List (bt (Color ∧ A))} → stack ≡ tree ∷ [] - → (rotated : replacedRBTree key value tree repl ∨ replacedRBTree key value (to-black tree) repl) - → RBI-state key value tree repl stack - -record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) : Set n where - field - tree repl : bt (Color ∧ A) - origti : treeInvariant orig - origrb : RBtreeInvariant orig - treerb : RBtreeInvariant tree -- tree node te be replaced - replrb : RBtreeInvariant repl - replti : treeInvariant repl - si : stackInvariant key tree orig stack - state : RBI-state key value tree repl stack - -tr>-to-black : {n : Level} {A : Set n} {key : ℕ} {tree : bt (Color ∧ A)} → tr> key tree → tr> key (to-black tree) -tr>-to-black {n} {A} {key} {leaf} tr = tt -tr>-to-black {n} {A} {key} {node key₁ value tree tree₁} tr = tr - - -tr<-to-black : {n : Level} {A : Set n} {key : ℕ} {tree : bt (Color ∧ A)} → tr< key tree → tr< key (to-black tree) -tr<-to-black {n} {A} {key} {leaf} tr = tt -tr<-to-black {n} {A} {key} {node key₁ value tree tree₁} tr = tr - -to-black-eq : {n : Level} {A : Set n} (tree : bt (Color ∧ A)) → color tree ≡ Red → suc (black-depth tree) ≡ black-depth (to-black tree) -to-black-eq {n} {A} (leaf) () -to-black-eq {n} {A} (node key₁ ⟪ Red , proj4 ⟫ tree tree₁) eq = refl -to-black-eq {n} {A} (node key₁ ⟪ Black , proj4 ⟫ tree tree₁) () - -red-children-eq : {n : Level} {A : Set n} {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color} - → tree ≡ node key ⟪ c , value ⟫ left right - → c ≡ Red - → RBtreeInvariant tree - → (black-depth tree ≡ black-depth left ) ∧ (black-depth tree ≡ black-depth right) -red-children-eq {n} {A} {_} {left} {right} {key} {value} {c} () ceq rb-leaf -red-children-eq {n} {A} {(node key₁ ⟪ Red , value₁ ⟫ left₁ right₁)} {left} {right} {key} {value} {c} teq ceq (rb-red key₁ value₁ x x₁ x₂ rb rb₁) - = ⟪ begin - black-depth left₁ ⊔ black-depth right₁ ≡⟨ cong (λ k → black-depth left₁ ⊔ k) (sym x₂) ⟩ - black-depth left₁ ⊔ black-depth left₁ ≡⟨ ⊔-idem _ ⟩ - black-depth left₁ ≡⟨ cong black-depth (just-injective (cong node-left teq )) ⟩ - black-depth left ∎ - , begin - black-depth left₁ ⊔ black-depth right₁ ≡⟨ cong (λ k → k ⊔ black-depth right₁) x₂ ⟩ - black-depth right₁ ⊔ black-depth right₁ ≡⟨ ⊔-idem _ ⟩ - black-depth right₁ ≡⟨ cong black-depth (just-injective (cong node-right teq )) ⟩ - black-depth right ∎ ⟫ - where open ≡-Reasoning -red-children-eq {n} {A} {node key₁ ⟪ Black , value₁ ⟫ left₁ right₁} {left} {right} {key} {value} {c} teq ceq (rb-black key₁ value₁ x rb rb₁) - = ⊥-elim ( ⊥-color (trans (cong color teq) ceq)) - -black-children-eq : {n : Level} {A : Set n} {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color} - → tree ≡ node key ⟪ c , value ⟫ left right - → c ≡ Black - → RBtreeInvariant tree - → (black-depth tree ≡ suc (black-depth left) ) ∧ (black-depth tree ≡ suc (black-depth right)) -black-children-eq {n} {A} {_} {left} {right} {key} {value} {c} () ceq rb-leaf -black-children-eq {n} {A} {.(node key₁ ⟪ Red , value₁ ⟫ _ _)} {left} {right} {key} {value} {c} teq ceq (rb-red key₁ value₁ x x₁ x₂ rb rb₁) - = ⊥-elim ( ⊥-color (sym (trans (cong color teq) ceq))) -black-children-eq {n} {A} {(node key₁ ⟪ Black , value₁ ⟫ left₁ right₁)} {left} {right} {key} {value} {c} teq ceq rb2@(rb-black key₁ value₁ x rb rb₁) = - ⟪ ( begin - suc (black-depth left₁ ⊔ black-depth right₁) ≡⟨ cong (λ k → suc (black-depth left₁ ⊔ k)) (sym (RBtreeEQ rb2)) ⟩ - suc (black-depth left₁ ⊔ black-depth left₁) ≡⟨ cong (λ k → suc (black-depth k ⊔ black-depth k)) (just-injective (cong node-left teq )) ⟩ - suc (black-depth left ⊔ black-depth left) ≡⟨ ⊔-idem _ ⟩ - suc (black-depth left) ∎ ) , ( - begin - suc (black-depth left₁ ⊔ black-depth right₁) ≡⟨ cong (λ k → suc (k ⊔ black-depth right₁)) (RBtreeEQ rb2) ⟩ - suc (black-depth right₁ ⊔ black-depth right₁) ≡⟨ cong (λ k → suc (black-depth k ⊔ black-depth k)) (just-injective (cong node-right teq )) ⟩ - suc (black-depth right ⊔ black-depth right) ≡⟨ ⊔-idem _ ⟩ - suc (black-depth right) ∎ ) ⟫ where open ≡-Reasoning - -black-depth-cong : {n : Level} (A : Set n) {tree tree₁ : bt (Color ∧ A)} - → tree ≡ tree₁ → black-depth tree ≡ black-depth tree₁ -black-depth-cong {n} A {leaf} {leaf} eq = refl -black-depth-cong {n} A {leaf} {node _ _ _ _} () -black-depth-cong {n} A {node key value tree tree₂} {leaf} () -black-depth-cong {n} A {node key ⟪ Red , v0 ⟫ tree tree₂} {node key₁ ⟪ Red , v1 ⟫ tree₁ tree₃} eq - = cong₂ _⊔_ (black-depth-cong A (just-injective (cong node-left eq ))) (black-depth-cong A (just-injective (cong node-right eq ))) -black-depth-cong {n} A {node key ⟪ Red , v0 ⟫ tree tree₂} {node key₁ ⟪ Black , v1 ⟫ tree₁ tree₃} () -black-depth-cong {n} A {node key ⟪ Black , v0 ⟫ tree tree₂} {node key₁ ⟪ Red , v1 ⟫ tree₁ tree₃} () -black-depth-cong {n} A {node key ⟪ Black , v0 ⟫ tree tree₂} {node key₁ ⟪ Black , v1 ⟫ tree₁ tree₃} eq - = cong₂ (λ j k → suc j ⊔ suc k) (black-depth-cong A (just-injective (cong node-left eq ))) (black-depth-cong A (just-injective (cong node-right eq ))) - - -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} - → tree ≡ node key1 ⟪ c1 , value1 ⟫ l1 r1 → tree₁ ≡ node key2 ⟪ c2 , value2 ⟫ l2 r2 - → color tree ≡ color tree₁ - → black-depth l1 ≡ black-depth l2 → black-depth r1 ≡ black-depth r2 - → black-depth tree ≡ black-depth tree₁ -black-depth-resp A leaf tree₁ {c1} {c2} {l1} {l2} {r1} {r2} {key1} {key2} {value1} {value2} () eq₁ ceq bd1 bd2 -black-depth-resp A (node key value tree tree₂) leaf eq () ceq bd1 bd2 -black-depth-resp A (node key ⟪ Red , value ⟫ tree tree₂) (node key₁ ⟪ Red , value₁ ⟫ tree₁ tree₃) {c1} {c2} {l1} {l2} {r1} {r2} eq eq₁ ceq bd1 bd2 = begin - black-depth tree ⊔ black-depth tree₂ ≡⟨ cong₂ (λ j k → black-depth j ⊔ black-depth k) (just-injective (cong node-left eq )) (just-injective (cong node-right eq )) ⟩ - black-depth l1 ⊔ black-depth r1 ≡⟨ cong₂ _⊔_ bd1 bd2 ⟩ - black-depth l2 ⊔ black-depth r2 ≡⟨ cong₂ (λ j k → black-depth j ⊔ black-depth k) (just-injective (cong node-left (sym eq₁) )) (just-injective (cong node-right (sym eq₁) )) ⟩ - black-depth tree₁ ⊔ black-depth tree₃ - ∎ where open ≡-Reasoning -black-depth-resp A (node key ⟪ Red , value ⟫ tree tree₂) (node key₁ ⟪ Black , value₁ ⟫ tree₁ tree₃) eq eq₁ ceq bd1 bd2 = ⊥-elim ( ⊥-color (sym ceq )) -black-depth-resp A (node key ⟪ Black , value ⟫ tree tree₂) (node key₁ ⟪ Red , proj4 ⟫ tree₁ tree₃) eq eq₁ ceq bd1 bd2 = ⊥-elim ( ⊥-color ceq) -black-depth-resp A (node key ⟪ Black , value ⟫ tree tree₂) (node key₁ ⟪ Black , proj4 ⟫ tree₁ tree₃) {c1} {c2} {l1} {l2} {r1} {r2} eq eq₁ ceq bd1 bd2 = begin - suc (black-depth tree ⊔ black-depth tree₂) ≡⟨ cong₂ (λ j k → suc (black-depth j ⊔ black-depth k)) (just-injective (cong node-left eq )) (just-injective (cong node-right eq )) ⟩ - suc (black-depth l1 ⊔ black-depth r1) ≡⟨ cong suc ( cong₂ _⊔_ bd1 bd2) ⟩ - suc (black-depth l2 ⊔ black-depth r2) ≡⟨ cong₂ (λ j k → suc (black-depth j ⊔ black-depth k)) (just-injective (cong node-left (sym eq₁) )) (just-injective (cong node-right (sym eq₁) )) ⟩ - suc (black-depth tree₁ ⊔ black-depth tree₃) ∎ where open ≡-Reasoning - -red-children-eq1 : {n : Level} {A : Set n} {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color} - → tree ≡ node key ⟪ c , value ⟫ left right - → color tree ≡ Red - → RBtreeInvariant tree - → (black-depth tree ≡ black-depth left ) ∧ (black-depth tree ≡ black-depth right) -red-children-eq1 {n} {A} {tree} {left} {right} {key} {value} {c} eq ceq rb = red-children-eq eq ((trans (sym (cong color eq) ) ceq )) rb - -black-children-eq1 : {n : Level} {A : Set n} {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color} - → tree ≡ node key ⟪ c , value ⟫ left right - → color tree ≡ Black - → RBtreeInvariant tree - → (black-depth tree ≡ suc (black-depth left) ) ∧ (black-depth tree ≡ suc (black-depth right)) -black-children-eq1 {n} {A} {tree} {left} {right} {key} {value} {c} eq ceq rb = black-children-eq eq ((trans (sym (cong color eq) ) ceq )) rb - - -rbi-from-red-black : {n : Level } {A : Set n} → (n1 rp-left : bt (Color ∧ A)) → (kp : ℕ) → (vp : Color ∧ A) - → RBtreeInvariant n1 → RBtreeInvariant rp-left - → black-depth n1 ≡ black-depth rp-left - → color n1 ≡ Black → color rp-left ≡ Black → ⟪ Red , proj2 vp ⟫ ≡ vp - → RBtreeInvariant (node kp vp n1 rp-left) -rbi-from-red-black leaf leaf kp vp rb1 rbp deq ceq1 ceq2 ceq3 - = subst (λ k → RBtreeInvariant (node kp k leaf leaf)) ceq3 (rb-red kp (proj2 vp) refl refl refl rb-leaf rb-leaf) -rbi-from-red-black leaf (node key ⟪ .Black , proj3 ⟫ trpl trpl₁) kp vp rb1 rbp deq ceq1 refl ceq3 - = subst (λ k → RBtreeInvariant (node kp k _ _)) ceq3 (rb-red kp (proj2 vp) refl refl deq rb1 rbp) -rbi-from-red-black (node key ⟪ .Black , proj3 ⟫ tn1 tn2) leaf kp vp rb1 rbp deq refl ceq2 ceq3 - = subst (λ k → RBtreeInvariant (node kp k _ _)) ceq3 (rb-red kp (proj2 vp) refl refl deq rb1 rbp) -rbi-from-red-black (node key ⟪ .Black , proj3 ⟫ tn1 tn2) (node key₁ ⟪ .Black , proj4 ⟫ trpl trpl₁) kp vp rb1 rbp deq refl refl ceq3 - = subst (λ k → RBtreeInvariant (node kp k _ _)) ceq3 (rb-red kp (proj2 vp) refl refl deq rb1 rbp ) - -⊔-succ : {m n : ℕ} → suc (m ⊔ n) ≡ suc m ⊔ suc n -⊔-succ {m} {n} = refl - -RB-repl-node : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A)) → {key : ℕ} → {value : A} - → replacedRBTree key value tree repl → ¬ ( repl ≡ leaf) -RB-repl-node {n} {A} .leaf .(node _ ⟪ Red , _ ⟫ leaf leaf) rbr-leaf () -RB-repl-node {n} {A} .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) rbr-node () -RB-repl-node {n} {A} .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) (rbr-right x x₁ rpl) () -RB-repl-node {n} {A} .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) (rbr-left x x₁ rpl) () -RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) (rbr-black-right x x₁ rpl) () -RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) (rbr-black-left x x₁ rpl) () -RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) (rbr-flip-ll x x₁ x₂ x₃) () -RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) (rbr-flip-lr x x₁ x₂ x₃ x₄) () -RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rbr-flip-rl x x₁ x₂ x₃ x₄) () -RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rbr-flip-rr x₁ x₂ x₃ x₄) () -RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) (rbr-rotate-ll x x₁ x₂) () -RB-repl-node {n} {A} .(node x₂ ⟪ Black , _ ⟫ (node x₃ ⟪ Red , _ ⟫ _ _) _) .(node x₄ ⟪ Black , _ ⟫ (node x₃ ⟪ Red , _ ⟫ _ x) (node x₂ ⟪ Red , _ ⟫ x₁ _)) (rbr-rotate-lr x x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈) () -RB-repl-node {n} {A} .(node x₂ ⟪ Black , _ ⟫ _ (node x₃ ⟪ Red , _ ⟫ _ _)) .(node x₄ ⟪ Black , _ ⟫ (node x₂ ⟪ Red , _ ⟫ _ x) (node x₃ ⟪ Red , _ ⟫ x₁ _)) (rbr-rotate-rl x x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈) () -RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) (rbr-rotate-rr x x₁ x₂) () - -RBTPred : {n : Level} (A : Set n) (m : Level) → Set (n Level.⊔ Level.suc m) -RBTPred {n} A m = (key : ℕ) → (value : A) → (before after : bt (Color ∧ A)) → replacedRBTree key value before after → Set m - -RBTI-induction : {n m : Level} (A : Set n) → (tree tree1 repl : bt (Color ∧ A)) → (key : ℕ) → (value : A) → tree ≡ tree1 → (rbt : replacedRBTree key value tree repl ) - → {P : RBTPred A m } - → ( P key value leaf (node key ⟪ Red , value ⟫ leaf leaf) rbr-leaf - ∧ ( (ca : Color ) → (value₂ : A) → (t t₁ : bt (Color ∧ A)) → P key value (node key ⟪ ca , value₂ ⟫ t t₁) (node key ⟪ ca , value ⟫ t t₁) rbr-node ) - ∧ ( {k : ℕ } {v1 : A} → {ca : Color} → {t t1 t2 : bt (Color ∧ A)} → (x : color t2 ≡ color t) ( x₁ : k < key ) → (rbt : replacedRBTree key value t2 t ) - → P key value t2 t rbt → P key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ ca , v1 ⟫ t1 t) (rbr-right x x₁ rbt ) ) - ∧ ( {k : ℕ } {v1 : A} → {ca : Color} → {t t1 t2 : bt (Color ∧ A)} → (x : color t1 ≡ color t) ( x₁ : key < k ) → (rbt : replacedRBTree key value t1 t ) - → P key value t1 t rbt - → P key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ ca , v1 ⟫ t t2) (rbr-left x x₁ rbt)) - ∧ ( {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} → (x : color t₂ ≡ Red) → (x₁ : key₁ < key) → (rbt : replacedRBTree key value t₁ t₂ ) - → P key value t₁ t₂ rbt - → P key value (node key₁ ⟪ Black , value₁ ⟫ t t₁) (node key₁ ⟪ Black , value₁ ⟫ t t₂) (rbr-black-right x x₁ rbt) ) - ∧ ({t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} → (x : color t₂ ≡ Red ) → (x₁ : key < key₁ ) → (rbt : replacedRBTree key value t₁ t₂ ) - → P key value t₁ t₂ rbt - → P key value (node key₁ ⟪ Black , value₁ ⟫ t₁ t) (node key₁ ⟪ Black , value₁ ⟫ t₂ t) (rbr-black-left x x₁ rbt) ) - ∧ ( {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - → (x : color t₂ ≡ Red ) → (x₁ : color uncle ≡ Red ) → (x₂ : key < kp ) → (rbt : replacedRBTree key value t₁ t₂ ) - → P key value t₁ t₂ rbt - → P key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t) uncle) (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t₂ t) (to-black uncle)) - (rbr-flip-ll x x₁ x₂ rbt)) - ∧ ( {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} → (x : color t₂ ≡ Red ) → (x₁ : color uncle ≡ Red ) → (x₂ : kp < key ) → (x₃ : key < kg) - → (rbt : replacedRBTree key value t₁ t₂ ) - → P key value t₁ t₂ rbt - → P key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t t₂) (to-black uncle)) - (rbr-flip-lr x x₁ x₂ x₃ rbt) ) - ∧ ( {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - → (x : color t₂ ≡ Red ) → (x₁ : color uncle ≡ Red ) → (x₂ : kg < key ) → (x₃ : key < kp) → (rbt : replacedRBTree key value t₁ t₂ ) - → P key value t₁ t₂ rbt - → P key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t)) - (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t₂ t)) - (rbr-flip-rl x x₁ x₂ x₃ rbt)) - ∧ ( {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - → (x : color t₂ ≡ Red ) → (x₁ : color uncle ≡ Red ) → (x₂ : kp < key ) → (rbt : replacedRBTree key value t₁ t₂ ) - → P key value t₁ t₂ rbt - → P key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t t₁)) (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t t₂)) - (rbr-flip-rr x x₁ x₂ rbt) ) - ∧ ( {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} → (x : color t₂ ≡ Red) → (x₁ : key < kp ) → (rbt : replacedRBTree key value t₁ t₂ ) - → P key value t₁ t₂ rbt - → P key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t) uncle) (node kp ⟪ Black , vp ⟫ t₂ (node kg ⟪ Red , vg ⟫ t uncle)) (rbr-rotate-ll x x₁ rbt)) - ∧ ({t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - → (x : color t₂ ≡ Red ) → (x₁ : kp < key ) → (rbt : replacedRBTree key value t₁ t₂ ) - → P key value t₁ t₂ rbt - → P key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t t₁)) (node kp ⟪ Black , vp ⟫ (node kg ⟪ Red , vg ⟫ uncle t) t₂) - (rbr-rotate-rr x x₁ rbt) ) - ∧ ({t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} - → (x : color t₃ ≡ Black) → (x₁ : kp < key )→ (x₂ : key < kg ) - → (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) - → P key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃) rbt - → P key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) (node kn ⟪ Black , vn ⟫ (node kp ⟪ Red , vp ⟫ t t₂) (node kg ⟪ Red , vg ⟫ t₃ uncle)) - (rbr-rotate-lr t₂ t₃ kg kp kn x x₁ x₂ rbt) ) - ∧ ( {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} - → (x : color t₃ ≡ Black) → (x₁ : kg < key) → (x₂ : key < kp ) - → (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃) ) - → P key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃) rbt - → P key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , vg ⟫ uncle t₂) (node kp ⟪ Red , vp ⟫ t₃ t)) - (rbr-rotate-rl t₂ t₃ kg kp kn x x₁ x₂ rbt) )) - → P key value tree repl rbt -RBTI-induction {n} {m} A tree leaf repl key value eq rbr-leaf {P} p = proj1 p -RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-node {value₂} {ca} {t} {t1} ) {P} p = proj1 (proj2 p) ca value₂ t t1 -RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-right {k} {v1} {ca} {t} {t1} {t2} x x₁ rbt) {P} p - = proj1 (proj2 (proj2 p)) x x₁ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p) -RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-left x x₁ rbt) {P} p - = proj1 (proj2 (proj2 (proj2 p))) x x₁ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p) -RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-black-right x x₁ rbt) {P} p - = proj1 (proj2 (proj2 (proj2 (proj2 p)))) x x₁ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p) -RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-black-left x x₁ rbt) {P} p - = proj1 (proj2 (proj2 (proj2 (proj2 (proj2 p))))) x x₁ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p) -RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-flip-ll {t} {t₁} {t₂} x x₁ x₂ rbt) {P} p - = proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 p)))))) x x₁ x₂ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p) -RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-flip-lr x x₁ x₂ x₃ rbt) {P} p - = proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 p))))))) x x₁ x₂ x₃ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p) -RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-flip-rl x x₁ x₂ x₃ rbt) {P} p - = proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 p)))))))) x x₁ x₂ x₃ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p) -RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-flip-rr x x₁ x₂ rbt) {P} p - = proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 p))))))))) x x₁ x₂ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p) -RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-rotate-ll x x₁ rbt) {P} p - = proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 p)))))))))) x x₁ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p) -RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-rotate-rr x x₁ rbt) {P} p - = proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 p))))))))))) x x₁ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p) -RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-rotate-lr t₂ t₃ kg kp kn x x₁ x₂ rbt) {P} p - = proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 p)))))))))))) _ _ _ _ _ x x₁ x₂ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p) -RBTI-induction {n} {m} A tree (node key₁ value₁ tree1 tree2) repl key value eq (rbr-rotate-rl t₂ t₃ kg kp kn x x₁ x₂ rbt) {P} p - = proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 p)))))))))))) _ _ _ _ _ x x₁ x₂ rbt (RBTI-induction A _ _ _ key value refl rbt {P} p) - - -RB-repl→eq : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A)) → {key : ℕ} → {value : A} - → RBtreeInvariant tree - → replacedRBTree key value tree repl → black-depth tree ≡ black-depth repl -RB-repl→eq {n} {A} tree repl {key} {value} rbt rbr = RBTI-induction A tree tree repl key value refl rbr {λ key value b a rbt → black-depth b ≡ black-depth a } - ⟪ refl , ⟪ (λ ca _ _ _ → lem00 ca _ _ _ ) , ⟪ - (λ {k} {v1} {ca} {t} {t1} {t2} → lem01 {k} {v1} {ca} {t} {t1} {t2}) , ⟪ (λ {k} {v1} {ca} {t} {t1} {t2} → lem02 {k} {v1} {ca} {t} {t1} {t2}) , ⟪ - (λ {t} {t₁} {t₂} {v1} → lem03 {t} {t₁} {t₂} {v1} ) , ⟪ (λ {t} {t₁} {t₂} {v₁} {k₁} → lem04 {t} {t₁} {t₂} {v₁} {k₁}) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem05 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem06 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem07 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem08 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem09 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem10 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ - (λ {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} → lem11 {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} ) , - (λ {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} → lem12 {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} ) ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ where - lem00 : (ca : Color) → ( value₂ : A) → (t t₁ : bt (Color ∧ A)) → black-depth (node key ⟪ ca , value₂ ⟫ t t₁) ≡ black-depth (node key ⟪ ca , value ⟫ t t₁) - lem00 Black v t t₁ = refl - lem00 Red v t t₁ = refl - lem01 : {k : ℕ} {v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t2 ≡ color t) (x₁ : k < key) - (rbt : replacedRBTree key value t2 t) → black-depth t2 ≡ black-depth t → black-depth (node k ⟪ ca , v1 ⟫ t1 t2) ≡ black-depth (node k ⟪ ca , v1 ⟫ t1 t) - lem01 {k} {v1} {Red} {t} {t1} {t2} ceq x₁ rbt prev = cong ( λ k → black-depth t1 ⊔ k ) prev - lem01 {k} {v1} {Black} {t} {t1} {t2} ceq x₁ rbt prev = cong ( λ k → suc (black-depth t1 ⊔ k) ) prev - lem02 : {k : ℕ} {v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t1 ≡ color t) (x₁ : key < k) - (rbt₁ : replacedRBTree key value t1 t) → black-depth t1 ≡ black-depth t → black-depth (node k ⟪ ca , v1 ⟫ t1 t2) ≡ black-depth (node k ⟪ ca , v1 ⟫ t t2) - lem02 {k} {v1} {Red} {t} {t1} {t2} ceq x₁ rbt prev = cong ( λ k → k ⊔ _ ) prev - lem02 {k} {v1} {Black} {t} {t1} {t2} ceq x₁ rbt prev = cong ( λ k → suc (k ⊔ _) ) prev - lem03 : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} (x : color t₂ ≡ Red) (x₁ : key₁ < key) (rbt₁ : replacedRBTree key value t₁ t₂) → - black-depth t₁ ≡ black-depth t₂ → suc (black-depth t ⊔ black-depth t₁) ≡ suc (black-depth t ⊔ black-depth t₂) - lem03 {t} x x₁ rbt eq = cong (λ k → suc (black-depth t ⊔ k)) eq - lem04 : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} (x : color t₂ ≡ Red) (x₁ : key < key₁) (rbt₁ : replacedRBTree key value t₁ t₂) → - black-depth t₁ ≡ black-depth t₂ → suc (black-depth t₁ ⊔ black-depth t) ≡ suc (black-depth t₂ ⊔ black-depth t) - lem04 {t} {t₁} {t₂} {v₁} x x₁ rbt eq = cong (λ k → suc (k ⊔ black-depth t)) eq - lem05 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : key < kp) (rbt₁ : replacedRBTree key value t₁ t₂) → - black-depth t₁ ≡ black-depth t₂ → suc (black-depth t₁ ⊔ black-depth t ⊔ black-depth uncle) ≡ suc (black-depth t₂ ⊔ black-depth t) ⊔ black-depth (to-black uncle) - lem05 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ rbt eq = begin - suc (black-depth t₁ ⊔ black-depth t ⊔ black-depth uncle) ≡⟨ cong (λ k → suc (k ⊔ _ ⊔ _ )) eq ⟩ - suc (black-depth t₂ ⊔ black-depth t) ⊔ suc (black-depth uncle) ≡⟨ cong (λ k → suc (black-depth t₂ ⊔ black-depth t) ⊔ k) (to-black-eq uncle x₁ ) ⟩ - suc (black-depth t₂ ⊔ black-depth t) ⊔ black-depth (to-black uncle) ∎ where open ≡-Reasoning - lem06 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key) - (x₃ : key < kg) (rbt₁ : replacedRBTree key value t₁ t₂) → - black-depth t₁ ≡ black-depth t₂ → suc (black-depth t ⊔ black-depth t₁ ⊔ black-depth uncle) ≡ suc (black-depth t ⊔ black-depth t₂) ⊔ black-depth (to-black uncle) - lem06 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ x₃ rbt eq = begin - suc (black-depth t ⊔ black-depth t₁ ⊔ black-depth uncle) ≡⟨ cong (λ k → suc (black-depth t ⊔ k ⊔ _ )) eq ⟩ - suc (black-depth t ⊔ black-depth t₂) ⊔ suc (black-depth uncle) ≡⟨ cong (λ k → suc (black-depth t ⊔ black-depth t₂) ⊔ k) (to-black-eq uncle x₁ ) ⟩ - suc (black-depth t ⊔ black-depth t₂) ⊔ black-depth (to-black uncle) ∎ where open ≡-Reasoning - lem07 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kg < key) - (x₃ : key < kp) (rbt₁ : replacedRBTree key value t₁ t₂) → - black-depth t₁ ≡ black-depth t₂ → suc (black-depth uncle ⊔ (black-depth t₁ ⊔ black-depth t)) ≡ black-depth (to-black uncle) ⊔ suc (black-depth t₂ ⊔ black-depth t) - lem07 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ x₃ rbt eq = begin - suc (black-depth uncle ⊔ (black-depth t₁ ⊔ black-depth t)) ≡⟨ cong (λ k → suc (black-depth uncle ⊔ (k ⊔ _))) eq ⟩ - suc (black-depth uncle ⊔ (black-depth t₂ ⊔ black-depth t)) ≡⟨ cong (λ k → k ⊔ _) (to-black-eq uncle x₁) ⟩ - black-depth (to-black uncle) ⊔ suc (black-depth t₂ ⊔ black-depth t) ∎ where open ≡-Reasoning - lem08 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key) (rbt₁ : replacedRBTree key value t₁ t₂) → - black-depth t₁ ≡ black-depth t₂ → suc (black-depth uncle ⊔ (black-depth t ⊔ black-depth t₁)) ≡ black-depth (to-black uncle) ⊔ suc (black-depth t ⊔ black-depth t₂) - lem08 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ rbt eq = begin - suc (black-depth uncle ⊔ (black-depth t ⊔ black-depth t₁)) ≡⟨ cong (λ k → suc (black-depth uncle ⊔ (_ ⊔ k))) eq ⟩ - suc (black-depth uncle ⊔ (black-depth t ⊔ black-depth t₂)) ≡⟨ cong (λ k → k ⊔ _) (to-black-eq uncle x₁) ⟩ - black-depth (to-black uncle) ⊔ suc (black-depth t ⊔ black-depth t₂) ∎ where open ≡-Reasoning - lem09 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : key < kp) (rbt₁ : replacedRBTree key value t₁ t₂) → - black-depth t₁ ≡ black-depth t₂ → suc (black-depth t₁ ⊔ black-depth t ⊔ black-depth uncle) ≡ suc (black-depth t₂ ⊔ (black-depth t ⊔ black-depth uncle)) - lem09 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ rbt eq = begin - suc (black-depth t₁ ⊔ black-depth t ⊔ black-depth uncle) ≡⟨ cong (λ k → suc (k ⊔ _ ⊔ _)) eq ⟩ - suc (black-depth t₂ ⊔ black-depth t ⊔ black-depth uncle) ≡⟨ ⊔-assoc (suc (black-depth t₂)) (suc (black-depth t)) (suc (black-depth uncle)) ⟩ - suc (black-depth t₂ ⊔ (black-depth t ⊔ black-depth uncle)) ∎ where open ≡-Reasoning - lem10 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : kp < key) (rbt₁ : replacedRBTree key value t₁ t₂) → - black-depth t₁ ≡ black-depth t₂ → suc (black-depth uncle ⊔ (black-depth t ⊔ black-depth t₁)) ≡ suc (black-depth uncle ⊔ black-depth t ⊔ black-depth t₂) - lem10 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ rbt eq = begin - suc (black-depth uncle ⊔ (black-depth t ⊔ black-depth t₁)) ≡⟨ cong (λ k → suc (black-depth uncle ⊔ (_ ⊔ k))) eq ⟩ - suc (black-depth uncle ⊔ (black-depth t ⊔ black-depth t₂)) ≡⟨ sym (⊔-assoc (suc (black-depth uncle)) (suc (black-depth t)) (suc (black-depth t₂))) ⟩ - suc (black-depth uncle ⊔ black-depth t ⊔ black-depth t₂) ∎ where open ≡-Reasoning - lem11 : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black) (x₁ : kp < key) (x₂ : key < kg) - (rbt₁ : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) → - black-depth t₁ ≡ black-depth t₂ ⊔ black-depth t₃ → suc (black-depth t ⊔ black-depth t₁ ⊔ black-depth uncle) ≡ suc - (black-depth t ⊔ black-depth t₂ ⊔ (black-depth t₃ ⊔ black-depth uncle)) - lem11 {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} x x₁ x₂ rbt eq = begin - suc (black-depth t ⊔ black-depth t₁ ⊔ black-depth uncle) ≡⟨ cong (λ k → suc (black-depth t ⊔ k ⊔ _)) eq ⟩ - suc ((black-depth t ⊔ (black-depth t₂ ⊔ black-depth t₃ )) ⊔ black-depth uncle) ≡⟨ cong (λ k → suc (k ⊔ black-depth uncle )) (sym ( ⊔-assoc (black-depth t) (black-depth t₂) _ )) ⟩ - suc (((black-depth t ⊔ black-depth t₂) ⊔ black-depth t₃) ⊔ black-depth uncle) ≡⟨ cong suc ( ⊔-assoc _ (black-depth t₃) (black-depth uncle) ) ⟩ - suc ((black-depth t ⊔ black-depth t₂ ) ⊔ (black-depth t₃ ⊔ black-depth uncle)) ∎ where open ≡-Reasoning - lem12 : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black) (x₁ : kg < key) (x₂ : key < kp) - (rbt₁ : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) - → black-depth t₁ ≡ black-depth t₂ ⊔ black-depth t₃ - → suc (black-depth uncle ⊔ (black-depth t₁ ⊔ black-depth t)) ≡ suc (black-depth uncle ⊔ black-depth t₂ ⊔ (black-depth t₃ ⊔ black-depth t)) - lem12 {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} x x₁ x₂ rbt eq = begin - suc (black-depth uncle ⊔ (black-depth t₁ ⊔ black-depth t)) ≡⟨ cong (λ k → suc (black-depth uncle ⊔ (k ⊔ _))) eq ⟩ - suc (black-depth uncle ⊔ ((black-depth t₂ ⊔ black-depth t₃) ⊔ black-depth t)) ≡⟨ cong (λ k → suc (black-depth uncle ⊔ k )) (( ⊔-assoc (black-depth t₂) (black-depth t₃) _ )) ⟩ - suc (black-depth uncle ⊔ (black-depth t₂ ⊔ (black-depth t₃ ⊔ black-depth t))) ≡⟨ cong suc (sym (⊔-assoc (black-depth uncle) (black-depth t₂) (black-depth t₃ ⊔ black-depth t ))) ⟩ - suc (black-depth uncle ⊔ black-depth t₂ ⊔ (black-depth t₃ ⊔ black-depth t)) ∎ where open ≡-Reasoning - - -RB-repl→ti> : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A)) → (key key₁ : ℕ) → (value : A) - → replacedRBTree key value tree repl → key₁ < key → tr> key₁ tree → tr> key₁ repl -RB-repl→ti> {n} {A} tree repl key key₁ value rbr s1 s2 = RBTI-induction A tree tree repl key value refl rbr - {λ key value b a rbt → (key₁ : ℕ) → key₁ < key → tr> key₁ b → tr> key₁ a} - ⟪ (λ _ x _ → ⟪ x , ⟪ tt , tt ⟫ ⟫ ) , ⟪ lem00 , ⟪ (λ {k} {v1} {ca} {t} {t1} {t2} → lem01 {k} {v1} {ca} {t} {t1} {t2} ) , ⟪ - (λ {k} {v1} {ca} {t} {t1} {t2} → lem02 {k} {v1} {ca} {t} {t1} {t2} ) , ⟪ - (λ {t} {t₁} {t₂} {v1} x x₁ rbt prev k3 x₃ x₂ → lem03 {t} {t₁} {t₂} {v1} x x₁ rbt prev k3 x₃ x₂ ) , ⟪ - (λ {t} {t₁} {t₂} {v₁} {key₁} → lem04 {t} {t₁} {t₂} {v₁} {key₁} ) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem05 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem06 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem07 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem08 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem09 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem11 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ) , ⟪ - (λ {t} {t₁} {t₂} → lem12 {t} {t₁} {t₂} ) , (λ {t} {t₁} {t₂} → lem13 {t} {t₁} {t₂} ) ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ key₁ s1 s2 where - lem00 : (ca : Color) (value₂ : A) (t t₁ : bt (Color ∧ A)) (key₂ : ℕ) → key₂ < key → (key₂ < key) ∧ tr> key₂ t ∧ tr> key₂ t₁ → (key₂ < key) ∧ tr> key₂ t ∧ tr> key₂ t₁ - lem00 ca v2 t t₁ k2 x ⟪ x₁ , ⟪ x₂ , x₃ ⟫ ⟫ = ⟪ x , ⟪ x₂ , x₃ ⟫ ⟫ - lem01 : {k : ℕ} {v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t2 ≡ color t) (x₁ : k < key) - (rbt : replacedRBTree key value t2 t) → ((key₂ : ℕ) → key₂ < key → tr> key₂ t2 → tr> key₂ t) → (key₂ : ℕ) → key₂ < key → - (key₂ < k) ∧ tr> key₂ t1 ∧ tr> key₂ t2 → (key₂ < k) ∧ tr> key₂ t1 ∧ tr> key₂ t - lem01 {k} {v1} {ca} {t} {t1} {t2} ceq x₁ rbt prev k2 x x₂ = ⟪ proj1 x₂ , ⟪ proj1 (proj2 x₂) , prev _ x (proj2 (proj2 x₂)) ⟫ ⟫ - lem02 : {k : ℕ} {v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t1 ≡ color t) (x₁ : key < k) (rbt : replacedRBTree key value t1 t) → - ((key₂ : ℕ) → key₂ < key → tr> key₂ t1 → tr> key₂ t) → (key₂ : ℕ) → key₂ < key → (key₂ < k) ∧ tr> key₂ t1 ∧ tr> key₂ t2 → (key₂ < k) ∧ tr> key₂ t ∧ tr> key₂ t2 - lem02 {k} {v1} {ca} {t} {t1} {t2} ceq x₁ rbt prev k2 x x₂ = ⟪ proj1 x₂ , ⟪ prev _ x (proj1 (proj2 x₂)) , proj2 (proj2 x₂) ⟫ ⟫ - lem03 : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ = key₂ : ℕ} (x : color t₂ ≡ Red) (x₁ : key₂ < key) (rbt : replacedRBTree key value t₁ t₂) → - ((key₃ : ℕ) → key₃ < key → tr> key₃ t₁ → tr> key₃ t₂) → (key₃ : ℕ) → key₃ < key → (key₃ < key₂) ∧ tr> key₃ t ∧ tr> key₃ t₁ → (key₃ < key₂) ∧ tr> key₃ t ∧ tr> key₃ t₂ - lem03 {t} x x₁ rbt prev k3 x₃ x₂ = ⟪ proj1 x₂ , ⟪ proj1 (proj2 x₂) , prev _ x₃ (proj2 (proj2 x₂)) ⟫ ⟫ - lem04 : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ = key₂ : ℕ} (x : color t₂ ≡ Red) (x₁ : key < key₂) (rbt : replacedRBTree key value t₁ t₂) → - ((key₃ : ℕ) → key₃ < key → tr> key₃ t₁ → tr> key₃ t₂) → (key₃ : ℕ) → key₃ < key → (key₃ < key₂) ∧ tr> key₃ t₁ ∧ tr> key₃ t → (key₃ < key₂) ∧ tr> key₃ t₂ ∧ tr> key₃ t - lem04 {t} {t₁} {t₂} {v₁} x x₁ rbt prev k3 x₃ x₂ = ⟪ proj1 x₂ , ⟪ prev _ x₃ (proj1 (proj2 x₂)) , proj2 (proj2 x₂) ⟫ ⟫ - lem05 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : key < kp) (rbt : replacedRBTree key value t₁ t₂) → - ((key₂ : ℕ) → key₂ < key → tr> key₂ t₁ → tr> key₂ t₂) → (key₂ : ℕ) → key₂ < key → - (key₂ < kg) ∧ ((key₂ < kp) ∧ tr> key₂ t₁ ∧ tr> key₂ t) ∧ tr> key₂ uncle → (key₂ < kg) ∧ ((key₂ < kp) ∧ tr> key₂ t₂ ∧ tr> key₂ t) ∧ tr> key₂ (to-black uncle) - lem05 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ rbt prev k2 x₄ x₃ = ⟪ proj1 x₃ , - ⟪ ⟪ proj1 lem10 , ⟪ prev _ x₄ (proj1 (proj2 lem10)) , proj2 (proj2 lem10) ⟫ ⟫ , tr>-to-black (proj2 (proj2 x₃)) ⟫ ⟫ where - lem10 = proj1 (proj2 x₃) - lem06 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key) - (x₃ : key < kg) (rbt : replacedRBTree key value t₁ t₂) → ((key₂ : ℕ) → key₂ < key → tr> key₂ t₁ → tr> key₂ t₂) → (key₂ : ℕ) → - key₂ < key → (key₂ < kg) ∧ ((key₂ < kp) ∧ tr> key₂ t ∧ tr> key₂ t₁) ∧ tr> key₂ uncle → - (key₂ < kg) ∧ ((key₂ < kp) ∧ tr> key₂ t ∧ tr> key₂ t₂) ∧ tr> key₂ (to-black uncle) - lem06 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ x₃ rbt prev k2 x₄ x₅ = ⟪ proj1 x₅ , - ⟪ ⟪ proj1 lem10 , ⟪ proj1 (proj2 lem10) , prev _ x₄ (proj2 (proj2 lem10)) ⟫ ⟫ , tr>-to-black (proj2 (proj2 x₅)) ⟫ ⟫ where - lem10 = proj1 (proj2 x₅) - lem07 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kg < key) - (x₃ : key < kp) (rbt : replacedRBTree key value t₁ t₂) → ((key₂ : ℕ) → key₂ < key → tr> key₂ t₁ → tr> key₂ t₂) → - (key₂ : ℕ) → key₂ < key → (key₂ < kg) ∧ tr> key₂ uncle ∧ (key₂ < kp) ∧ tr> key₂ t₁ ∧ tr> key₂ t → (key₂ < kg) ∧ - tr> key₂ (to-black uncle) ∧ (key₂ < kp) ∧ tr> key₂ t₂ ∧ tr> key₂ t - lem07 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ x₃ rbt prev k2 x₄ x₅ = ⟪ proj1 x₅ , ⟪ tr>-to-black (proj1 (proj2 x₅)) , - ⟪ proj1 (proj2 (proj2 x₅)) , ⟪ prev _ x₄ (proj1 (proj2 (proj2 (proj2 x₅)))) , proj2 (proj2 (proj2 (proj2 x₅))) ⟫ ⟫ ⟫ ⟫ - lem08 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key) - (rbt : replacedRBTree key value t₁ t₂) → ((key₂ : ℕ) → key₂ < key → tr> key₂ t₁ → tr> key₂ t₂) → (key₂ : ℕ) → - key₂ < key → (key₂ < kg) ∧ tr> key₂ uncle ∧ (key₂ < kp) ∧ tr> key₂ t ∧ tr> key₂ t₁ → - (key₂ < kg) ∧ tr> key₂ (to-black uncle) ∧ (key₂ < kp) ∧ tr> key₂ t ∧ tr> key₂ t₂ - lem08 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ rbt prev k2 x₄ x₅ = ⟪ proj1 x₅ , ⟪ tr>-to-black (proj1 (proj2 x₅)) , - ⟪ proj1 (proj2 (proj2 x₅)) , ⟪ proj1 (proj2 (proj2 (proj2 x₅))) , prev _ x₄ (proj2 (proj2 (proj2 (proj2 x₅)))) ⟫ ⟫ ⟫ ⟫ - lem09 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : key < kp) (rbt : replacedRBTree key value t₁ t₂) → - ((key₂ : ℕ) → key₂ < key → tr> key₂ t₁ → tr> key₂ t₂) → (key₂ : ℕ) → key₂ < key → - (key₂ < kg) ∧ ((key₂ < kp) ∧ tr> key₂ t₁ ∧ tr> key₂ t) ∧ tr> key₂ uncle → (key₂ < kp) ∧ tr> key₂ t₂ ∧ (key₂ < kg) ∧ tr> key₂ t ∧ tr> key₂ uncle - lem09 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ rbt prev k2 x₄ x₅ = ⟪ proj1 lem10 , - ⟪ prev _ x₄ (proj1 (proj2 lem10)) , ⟪ proj1 x₅ , ⟪ proj2 (proj2 lem10) , proj2 (proj2 x₅) ⟫ ⟫ ⟫ ⟫ where - lem10 = proj1 (proj2 x₅) - lem11 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : kp < key) (rbt : replacedRBTree key value t₁ t₂) → - ((key₂ : ℕ) → key₂ < key → tr> key₂ t₁ → tr> key₂ t₂) → (key₂ : ℕ) → key₂ < key → (key₂ < kg) ∧ - tr> key₂ uncle ∧ (key₂ < kp) ∧ tr> key₂ t ∧ tr> key₂ t₁ → (key₂ < kp) ∧ ((key₂ < kg) ∧ tr> key₂ uncle ∧ tr> key₂ t) ∧ tr> key₂ t₂ - lem11 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ rbt prev k2 x₄ x₅ = ⟪ proj1 (proj2 (proj2 x₅)) , - ⟪ ⟪ proj1 x₅ , ⟪ proj1 (proj2 x₅) , proj1 (proj2 (proj2 (proj2 x₅))) ⟫ ⟫ , prev _ x₄ (proj2 (proj2 (proj2 (proj2 x₅)))) ⟫ ⟫ - lem12 : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black) - (x₁ : kp < key) (x₂ : key < kg) (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) → - ((key₂ : ℕ) → key₂ < key → tr> key₂ t₁ → (key₂ < kn) ∧ tr> key₂ t₂ ∧ tr> key₂ t₃) → (key₂ : ℕ) → key₂ < key → - (key₂ < kg) ∧ ((key₂ < kp) ∧ tr> key₂ t ∧ tr> key₂ t₁) ∧ tr> key₂ uncle → (key₂ < kn) ∧ - ((key₂ < kp) ∧ tr> key₂ t ∧ tr> key₂ t₂) ∧ (key₂ < kg) ∧ tr> key₂ t₃ ∧ tr> key₂ uncle - lem12 {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} x x₁ x₂ rbt prev k2 x₄ x₅ = ⟪ proj1 lem14 , ⟪ ⟪ proj1 lem15 , - ⟪ proj1 (proj2 lem15) , proj1 (proj2 lem14) ⟫ ⟫ , ⟪ proj1 x₅ , ⟪ proj2 (proj2 lem14) , proj2 (proj2 x₅) ⟫ ⟫ ⟫ ⟫ where - lem15 = proj1 (proj2 x₅) - lem14 : (k2 < kn ) ∧ tr> k2 t₂ ∧ tr> k2 t₃ - lem14 = prev _ x₄ (proj2 (proj2 lem15)) - lem13 : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black) (x₁ : kg < key) (x₂ : key < kp) - (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) → ((key₂ : ℕ) → key₂ < key → tr> key₂ t₁ → (key₂ < kn) ∧ tr> key₂ t₂ ∧ tr> key₂ t₃) → - (key₂ : ℕ) → key₂ < key → (key₂ < kg) ∧ tr> key₂ uncle ∧ (key₂ < kp) ∧ tr> key₂ t₁ ∧ tr> key₂ t → - (key₂ < kn) ∧ ((key₂ < kg) ∧ tr> key₂ uncle ∧ tr> key₂ t₂) ∧ (key₂ < kp) ∧ tr> key₂ t₃ ∧ tr> key₂ t - lem13 {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} x x₁ x₂ rbt prev k2 x₄ x₅ = ⟪ proj1 lem14 , ⟪ ⟪ proj1 x₅ , - ⟪ proj1 (proj2 x₅) , proj1 (proj2 lem14) ⟫ ⟫ , ⟪ proj1 (proj2 (proj2 x₅)) , ⟪ proj2 (proj2 lem14) , proj2 (proj2 (proj2 (proj2 x₅))) ⟫ ⟫ ⟫ ⟫ where - lem14 : (k2 < kn ) ∧ tr> k2 t₂ ∧ tr> k2 t₃ - lem14 = prev _ x₄ (proj1 (proj2 (proj2 (proj2 x₅)))) - - - -RB-repl→ti< : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A)) → (key key₁ : ℕ) → (value : A) - → replacedRBTree key value tree repl → key < key₁ → tr< key₁ tree → tr< key₁ repl -RB-repl→ti< {n} {A} tree repl key key₁ value rbr s1 s2 = RBTI-induction A tree tree repl key value refl rbr - {λ key value b a rbt → (key₁ : ℕ) → key < key₁ → tr< key₁ b → tr< key₁ a} - ⟪ (λ _ x _ → ? ) , ⟪ lem00 , ⟪ (λ {k} {v1} {ca} {t} {t1} {t2} → lem01 {k} {v1} {ca} {t} {t1} {t2} ) , ⟪ - (λ {k} {v1} {ca} {t} {t1} {t2} → lem02 {k} {v1} {ca} {t} {t1} {t2} ) , ⟪ - (λ {t} {t₁} {t₂} {v1} → lem03 {t} {t₁} {t₂} {v1} ) , ⟪ - (λ {t} {t₁} {t₂} {v₁} {key₁} → lem04 {t} {t₁} {t₂} {v₁} {key₁} ) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem05 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem06 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem07 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem08 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp}) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem09 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ) , ⟪ - (λ {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} → lem11 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} ) , ⟪ - (λ {t} {t₁} {uncle} → lem12 {t} {t₁} {uncle} ) , - (λ {t} {t₁} {uncle} → lem13 {t} {t₁} {uncle} ) - ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ key₁ s1 s2 where - lem00 : (ca : Color) (value₂ : A) (t t₁ : bt (Color ∧ A)) (key₂ : ℕ) → key < key₂ → (key < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁ → (key < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁ - lem00 ca v2 t t₁ k2 x ⟪ x₁ , ⟪ x₂ , x₃ ⟫ ⟫ = ⟪ x , ⟪ x₂ , x₃ ⟫ ⟫ - lem01 : {k : ℕ} {v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t2 ≡ color t) (x₁ : k < key ) - (rbt : replacedRBTree key value t2 t) → ((key₂ : ℕ) → key < key₂ → tr< key₂ t2 → tr< key₂ t) → (key₂ : ℕ) → key < key₂ → - (k < key₂ ) ∧ tr< key₂ t1 ∧ tr< key₂ t2 → (k < key₂ ) ∧ tr< key₂ t1 ∧ tr< key₂ t - lem01 {k} {v1} {ca} {t} {t1} {t2} ceq x₁ rbt prev k2 x x₂ = ⟪ proj1 x₂ , ⟪ proj1 (proj2 x₂) , prev _ x (proj2 (proj2 x₂)) ⟫ ⟫ - lem02 : {k : ℕ} {v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t1 ≡ color t) (x₁ : key < k) - (rbt : replacedRBTree key value t1 t) → ((key₂ : ℕ) → key < key₂ → tr< key₂ t1 → tr< key₂ t) → - (key₂ : ℕ) → key < key₂ → (k < key₂) ∧ tr< key₂ t1 ∧ tr< key₂ t2 → (k < key₂) ∧ tr< key₂ t ∧ tr< key₂ t2 - lem02 {k} {v1} {ca} {t} {t1} {t2} ceq x₁ rbt prev k2 x x₂ = ⟪ proj1 x₂ , ⟪ prev _ x (proj1 (proj2 x₂)) , proj2 (proj2 x₂) ⟫ ⟫ - lem03 : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ = key₂ : ℕ} (x : color t₂ ≡ Red) (x₁ : key₂ < key) (rbt : replacedRBTree key value t₁ t₂) → - ((key₃ : ℕ) → key < key₃ → tr< key₃ t₁ → tr< key₃ t₂) → (key₃ : ℕ) → key < key₃ → (key₂ < key₃) ∧ tr< key₃ t ∧ tr< key₃ t₁ → (key₂ < key₃) ∧ tr< key₃ t ∧ tr< key₃ t₂ - lem03 {t} x x₁ rbt prev k3 x₃ x₂ = ⟪ proj1 x₂ , ⟪ proj1 (proj2 x₂) , prev _ x₃ (proj2 (proj2 x₂)) ⟫ ⟫ - lem04 : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} (x : color t₂ ≡ Red) (x₁ : key < key₁) (rbt : replacedRBTree key value t₁ t₂) → - ((key₃ : ℕ) → key < key₃ → tr< key₃ t₁ → tr< key₃ t₂) → (key₃ : ℕ) → key < key₃ → (key₁ < key₃) ∧ tr< key₃ t₁ ∧ tr< key₃ t → (key₁ < key₃) ∧ tr< key₃ t₂ ∧ tr< key₃ t - lem04 {t} {t₁} {t₂} {v₁} x x₁ rbt prev k3 x₃ x₂ = ⟪ proj1 x₂ , ⟪ prev _ x₃ (proj1 (proj2 x₂)) , proj2 (proj2 x₂) ⟫ ⟫ - lem05 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : key < kp) (rbt : replacedRBTree key value t₁ t₂) → - ((key₂ : ℕ) → key < key₂ → tr< key₂ t₁ → tr< key₂ t₂) → (key₂ : ℕ) → key < key₂ → (kg < key₂) ∧ - ((kp < key₂) ∧ tr< key₂ t₁ ∧ tr< key₂ t) ∧ tr< key₂ uncle → (kg < key₂) ∧ ((kp < key₂) ∧ tr< key₂ t₂ ∧ tr< key₂ t) ∧ tr< key₂ (to-black uncle) - lem05 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ rbt prev k2 x₄ x₃ = ⟪ proj1 x₃ , - ⟪ ⟪ proj1 lem10 , ⟪ prev _ x₄ (proj1 (proj2 lem10)) , proj2 (proj2 lem10) ⟫ ⟫ , tr<-to-black (proj2 (proj2 x₃)) ⟫ ⟫ where - lem10 = proj1 (proj2 x₃) - lem06 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key) - (x₃ : key < kg) (rbt : replacedRBTree key value t₁ t₂) → ((key₂ : ℕ) → key < key₂ → tr< key₂ t₁ → tr< key₂ t₂) → (key₂ : ℕ) → key < key₂ → - (kg < key₂) ∧ ((kp < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁) ∧ tr< key₂ uncle → (kg < key₂) ∧ ((kp < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₂) ∧ tr< key₂ (to-black uncle) - lem06 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ x₃ rbt prev k2 x₄ x₅ = ⟪ proj1 x₅ , - ⟪ ⟪ proj1 lem10 , ⟪ proj1 (proj2 lem10) , prev _ x₄ (proj2 (proj2 lem10)) ⟫ ⟫ , tr<-to-black (proj2 (proj2 x₅)) ⟫ ⟫ where - lem10 = proj1 (proj2 x₅) - lem07 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kg < key) - (x₃ : key < kp) (rbt : replacedRBTree key value t₁ t₂) → ((key₂ : ℕ) → key < key₂ → tr< key₂ t₁ → tr< key₂ t₂) → - (key₂ : ℕ) → key < key₂ → (kg < key₂) ∧ tr< key₂ uncle ∧ (kp < key₂) ∧ tr< key₂ t₁ ∧ tr< key₂ t → (kg < key₂) ∧ - tr< key₂ (to-black uncle) ∧ (kp < key₂) ∧ tr< key₂ t₂ ∧ tr< key₂ t - lem07 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ x₃ rbt prev k2 x₄ x₅ = ⟪ proj1 x₅ , ⟪ tr<-to-black (proj1 (proj2 x₅)) , - ⟪ proj1 (proj2 (proj2 x₅)) , ⟪ prev _ x₄ (proj1 (proj2 (proj2 (proj2 x₅)))) , proj2 (proj2 (proj2 (proj2 x₅))) ⟫ ⟫ ⟫ ⟫ - lem08 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key) - (rbt : replacedRBTree key value t₁ t₂) → ((key₂ : ℕ) → key < key₂ → tr< key₂ t₁ → tr< key₂ t₂) → - (key₂ : ℕ) → key < key₂ → (kg < key₂) ∧ tr< key₂ uncle ∧ (kp < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁ → - (kg < key₂) ∧ tr< key₂ (to-black uncle) ∧ (kp < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₂ - lem08 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ x₂ rbt prev k2 x₄ x₅ = ⟪ proj1 x₅ , ⟪ tr<-to-black (proj1 (proj2 x₅)) , - ⟪ proj1 (proj2 (proj2 x₅)) , ⟪ proj1 (proj2 (proj2 (proj2 x₅))) , prev _ x₄ (proj2 (proj2 (proj2 (proj2 x₅)))) ⟫ ⟫ ⟫ ⟫ - lem09 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : key < kp) (rbt : replacedRBTree key value t₁ t₂) → - ((key₂ : ℕ) → key < key₂ → tr< key₂ t₁ → tr< key₂ t₂) → (key₂ : ℕ) → key < key₂ → (kg < key₂) ∧ - ((kp < key₂) ∧ tr< key₂ t₁ ∧ tr< key₂ t) ∧ tr< key₂ uncle → (kp < key₂) ∧ tr< key₂ t₂ ∧ (kg < key₂) ∧ tr< key₂ t ∧ tr< key₂ uncle - lem09 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ rbt prev k2 x₄ x₅ = ⟪ proj1 lem10 , - ⟪ prev _ x₄ (proj1 (proj2 lem10)) , ⟪ proj1 x₅ , ⟪ proj2 (proj2 lem10) , proj2 (proj2 x₅) ⟫ ⟫ ⟫ ⟫ where - lem10 = proj1 (proj2 x₅) - lem11 : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) (x₁ : kp < key) (rbt : replacedRBTree key value t₁ t₂) → - ((key₂ : ℕ) → key < key₂ → tr< key₂ t₁ → tr< key₂ t₂) → (key₂ : ℕ) → key < key₂ → (kg < key₂) ∧ - tr< key₂ uncle ∧ (kp < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁ → (kp < key₂) ∧ ((kg < key₂) ∧ tr< key₂ uncle ∧ tr< key₂ t) ∧ tr< key₂ t₂ - lem11 {t} {t₁} {t₂} {uncle} {kg} {kp} {vg} {vp} x x₁ rbt prev k2 x₄ x₅ = ⟪ proj1 (proj2 (proj2 x₅)) , - ⟪ ⟪ proj1 x₅ , ⟪ proj1 (proj2 x₅) , proj1 (proj2 (proj2 (proj2 x₅))) ⟫ ⟫ , prev _ x₄ (proj2 (proj2 (proj2 (proj2 x₅)))) ⟫ ⟫ - lem12 : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black) (x₁ : kp < key) (x₂ : key < kg) - (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) → ((key₂ : ℕ) → key < key₂ → tr< key₂ t₁ → (kn < key₂) ∧ tr< key₂ t₂ ∧ tr< key₂ t₃) → - (key₂ : ℕ) → key < key₂ → (kg < key₂) ∧ ((kp < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁) ∧ tr< key₂ uncle → - (kn < key₂) ∧ ((kp < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₂) ∧ (kg < key₂) ∧ tr< key₂ t₃ ∧ tr< key₂ uncle - lem12 {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} x x₁ x₂ rbt prev k2 x₄ x₅ = ⟪ proj1 lem14 , ⟪ ⟪ proj1 lem15 , - ⟪ proj1 (proj2 lem15) , proj1 (proj2 lem14) ⟫ ⟫ , ⟪ proj1 x₅ , ⟪ proj2 (proj2 lem14) , proj2 (proj2 x₅) ⟫ ⟫ ⟫ ⟫ where - lem15 = proj1 (proj2 x₅) - lem14 : (kn < k2 ) ∧ tr< k2 t₂ ∧ tr< k2 t₃ - lem14 = prev _ x₄ (proj2 (proj2 lem15)) - lem13 : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black) (x₁ : kg < key) (x₂ : key < kp) - (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) → ((key₂ : ℕ) → key < key₂ → tr< key₂ t₁ → (kn < key₂) ∧ tr< key₂ t₂ ∧ tr< key₂ t₃) → (key₂ : ℕ) → - key < key₂ → (kg < key₂) ∧ tr< key₂ uncle ∧ (kp < key₂) ∧ tr< key₂ t₁ ∧ tr< key₂ t → - (kn < key₂) ∧ ((kg < key₂) ∧ tr< key₂ uncle ∧ tr< key₂ t₂) ∧ (kp < key₂) ∧ tr< key₂ t₃ ∧ tr< key₂ t - lem13 {t} {t₁} {uncle} t₂ t₃ kg kp kn {vg} {vp} {vn} x x₁ x₂ rbt prev k2 x₄ x₅ = ⟪ proj1 lem14 , ⟪ ⟪ proj1 x₅ , - ⟪ proj1 (proj2 x₅) , proj1 (proj2 lem14) ⟫ ⟫ , ⟪ proj1 (proj2 (proj2 x₅)) , ⟪ proj2 (proj2 lem14) , proj2 (proj2 (proj2 (proj2 x₅))) ⟫ ⟫ ⟫ ⟫ where - lem14 : (kn < k2 ) ∧ tr< k2 t₂ ∧ tr< k2 t₃ - lem14 = prev _ x₄ (proj1 (proj2 (proj2 (proj2 x₅)))) - -node-cong : {n : Level} {A : Set n} → {key key₁ : ℕ} → {value value₁ : A} → {left right left₁ right₁ : bt A} - → key ≡ key₁ → value ≡ value₁ → left ≡ left₁ → right ≡ right₁ → node key value left right ≡ node key₁ value₁ left₁ right₁ -node-cong {n} {A} refl refl refl refl = refl - -RB-repl→ti-lem03 : {n : Level} {A : Set n} {key k : ℕ} {value v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t1 ≡ color t) (x₁ : key < k) - (rbt : replacedRBTree key value t1 t) → (treeInvariant t1 → treeInvariant t) → treeInvariant (node k ⟪ ca , v1 ⟫ t1 t2) → treeInvariant (node k ⟪ ca , v1 ⟫ t t2) -RB-repl→ti-lem03 {n} {A} {key} {k} {value} {v1} {ca} {t} {t1} {t2} ceq x₁ rbt prev ti = lem21 (node k ⟪ ca , v1 ⟫ t1 t2) ti refl rbt where - lem22 : treeInvariant t - lem22 = prev (treeLeftDown _ _ ti) - lem21 : (tree : bt (Color ∧ A)) → treeInvariant tree → tree ≡ node k ⟪ ca , v1 ⟫ t1 t2 → replacedRBTree key value t1 t → treeInvariant (node k ⟪ ca , v1 ⟫ t t2) - lem21 tree ti eq rbt = ? - -RB-repl→ti-lem04 : {n : Level} {A : Set n} {key : ℕ} {value : A} {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} (x : color t₂ ≡ Red) (x₁ : key₁ < key) - (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) - → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₂) -RB-repl→ti-lem04 = ? - -RB-repl→ti-lem05 : {n : Level} {A : Set n} {key : ℕ} {value : A} {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} (x : color t₂ ≡ Red) (x₁ : key < key₁) - (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t₁ t) - → treeInvariant (node key₁ ⟪ Black , value₁ ⟫ t₂ t) -RB-repl→ti-lem05 = ? - -RB-repl→ti-lem06 : {n : Level} {A : Set n} {key : ℕ} {value : A} {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} (x : color t₂ ≡ Red) - (x₁ : color uncle ≡ Red) (x₂ : key < kp) (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) - → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t) uncle) - → treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t₂ t) (to-black uncle)) -RB-repl→ti-lem06 = ? - -RB-repl→ti-lem07 : {n : Level} {A : Set n} {key : ℕ} {value : A} {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key) (x₃ : key < kg) (rbt : replacedRBTree key value t₁ t₂) → (treeInvariant t₁ → treeInvariant t₂) - → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) - → treeInvariant (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t t₂) (to-black uncle)) -RB-repl→ti-lem07 = ? - -RB-repl→ti-lem08 : {n : Level} {A : Set n} {key : ℕ} {value : A} → {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kg < key) (x₃ : key < kp) (rbt : replacedRBTree key value t₁ t₂) - → (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t)) - → treeInvariant (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t₂ t)) -RB-repl→ti-lem08 = ? - -RB-repl→ti-lem09 : {n : Level} {A : Set n} {key : ℕ} {value : A} → {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - (x : color t₂ ≡ Red) (x₁ : color uncle ≡ Red) (x₂ : kp < key) (rbt : replacedRBTree key value t₁ t₂) → - (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t t₁)) → - treeInvariant (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t t₂)) -RB-repl→ti-lem09 = ? - -RB-repl→ti-lem10 : {n : Level} {A : Set n} {key : ℕ} {value : A} → {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - (x : color t₂ ≡ Red) (x₁ : key < kp) (rbt : replacedRBTree key value t₁ t₂) → - (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t) uncle) → - treeInvariant (node kp ⟪ Black , vp ⟫ t₂ (node kg ⟪ Red , vg ⟫ t uncle)) -RB-repl→ti-lem10 = ? - -RB-repl→ti-lem11 : {n : Level} {A : Set n} {key : ℕ} {value : A} → {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - (x : color t₂ ≡ Red) (x₁ : kp < key) (rbt : replacedRBTree key value t₁ t₂) → - (treeInvariant t₁ → treeInvariant t₂) → treeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t t₁)) → - treeInvariant (node kp ⟪ Black , vp ⟫ (node kg ⟪ Red , vg ⟫ uncle t) t₂) -RB-repl→ti-lem11 = ? - -RB-repl→ti-lem12 : {n : Level} {A : Set n} {key : ℕ} {value : A} → {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black) - (x₁ : kp < key) (x₂ : key < kg) (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) → - (treeInvariant t₁ → treeInvariant (node kn ⟪ Red , vn ⟫ t₂ t₃)) → treeInvariant (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) → - treeInvariant (node kn ⟪ Black , vn ⟫ (node kp ⟪ Red , vp ⟫ t t₂) (node kg ⟪ Red , vg ⟫ t₃ uncle)) -RB-repl→ti-lem12 = ? - -RB-repl→ti-lem13 : {n : Level} {A : Set n} {key : ℕ} {value : A} → {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} (x : color t₃ ≡ Black) - (x₁ : kg < key) (x₂ : key < kp) (rbt : replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)) → - (treeInvariant t₁ → treeInvariant (node kn ⟪ Red , vn ⟫ t₂ t₃)) → treeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t)) → - treeInvariant (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , vg ⟫ uncle t₂) (node kp ⟪ Red , vp ⟫ t₃ t)) -RB-repl→ti-lem13 = ? - -RB-repl→ti : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A) ) → (key : ℕ ) → (value : A) → treeInvariant tree - → replacedRBTree key value tree repl → treeInvariant repl -RB-repl→ti {n} {A} tree repl key value ti rbr = RBTI-induction A tree tree repl key value refl rbr {λ key value b a rbr → treeInvariant b → treeInvariant a } - ⟪ lem00 , ⟪ lem01 , ⟪ lem02 , ⟪ RB-repl→ti-lem03 , ⟪ RB-repl→ti-lem04 , ⟪ RB-repl→ti-lem05 , - ⟪ RB-repl→ti-lem06 , ⟪ RB-repl→ti-lem07 , ⟪ RB-repl→ti-lem08 , ⟪ RB-repl→ti-lem09 , ⟪ RB-repl→ti-lem10 , ⟪ RB-repl→ti-lem11 - , ⟪ RB-repl→ti-lem12 , RB-repl→ti-lem13 ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ⟫ ti where - lem00 : treeInvariant leaf → treeInvariant (node key ⟪ Red , value ⟫ leaf leaf) - lem00 ti = t-single key ⟪ Red , value ⟫ - lem01 : (ca : Color) (value₂ : A) (t t₁ : bt (Color ∧ A)) → treeInvariant (node key ⟪ ca , value₂ ⟫ t t₁) → treeInvariant (node key ⟪ ca , value ⟫ t t₁) - lem01 ca v2 t t₁ ti = lem20 (node key ⟪ ca , v2 ⟫ t t₁) ti refl where - lem20 : (tree : bt (Color ∧ A)) → treeInvariant tree → tree ≡ node key ⟪ ca , v2 ⟫ t t₁ → treeInvariant (node key ⟪ ca , value ⟫ t t₁) - lem20 .leaf t-leaf () - lem20 (node key v3 leaf leaf) (t-single key v3) eq = subst treeInvariant - (node-cong (just-injective (cong node-key eq)) refl (just-injective (cong node-left eq)) (just-injective (cong node-right eq))) (t-single key ⟪ ca , value ⟫) - lem20 (node key _ leaf (node key₁ _ _ _)) (t-right key key₁ x x₁ x₂ ti) eq = subst treeInvariant - (node-cong (just-injective (cong node-key eq)) refl (just-injective (cong node-left eq)) (just-injective (cong node-right eq))) (t-right key key₁ x x₁ x₂ ti) - lem20 (node key₁ _ (node key _ _ _) leaf) (t-left key key₁ x x₁ x₂ ti) eq = subst treeInvariant - (node-cong (just-injective (cong node-key eq)) refl (just-injective (cong node-left eq)) (just-injective (cong node-right eq))) (t-left key key₁ x x₁ x₂ ti) - lem20 (node key₁ _ (node key _ _ _) (node key₂ _ _ _)) (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) eq = subst treeInvariant - (node-cong (just-injective (cong node-key eq)) refl (just-injective (cong node-left eq)) (just-injective (cong node-right eq))) - (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) - lem02 : {k : ℕ} {v1 : A} {ca : Color} {t t1 t2 : bt (Color ∧ A)} (x : color t2 ≡ color t) (x₁ : k < key) - (rbt : replacedRBTree key value t2 t) → (treeInvariant t2 → treeInvariant t) → treeInvariant (node k ⟪ ca , v1 ⟫ t1 t2) → treeInvariant (node k ⟪ ca , v1 ⟫ t1 t) - lem02 {k} {v1} {ca} {t} {t1} {t2} ceq x₁ rbt prev ti = lem21 (node k ⟪ ca , v1 ⟫ t1 t2) ti refl rbt where - lem22 : treeInvariant t - lem22 = prev (treeRightDown _ _ ti) - lem21 : (tree : bt (Color ∧ A)) → treeInvariant tree → tree ≡ node k ⟪ ca , v1 ⟫ t1 t2 → replacedRBTree key value t2 t → treeInvariant (node k ⟪ ca , v1 ⟫ t1 t) - lem21 .leaf t-leaf () - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) eq rbr-leaf = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₁ _ (subst (λ k → k < key) (sym lem23) x₁) tt tt lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () rbr-node - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-right x x₁ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-left x x₁ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-black-right x x₁ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-black-left x x₁ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-flip-ll x x₁ x₂ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-flip-lr x x₁ x₂ x₃ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-flip-rl x x₁ x₂ x₃ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-flip-rr x x₁ x₂ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-rotate-ll x x₁ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-rotate-rr x x₁ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-rotate-lr t₂ t₃ kg kp kn x x₁ x₂ rbt) - lem21 (node k₁ v2 leaf leaf) (t-single k₁ v2) () (rbr-rotate-rl t₂ t₃ kg kp kn x x₁ x₂ rbt) - lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₄ x₂ ti) eq rbr-leaf = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ (subst (λ k → k < key) (sym lem23) x₁) tt tt lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {t₁} {t₂} x x₁₀ x₂ ti) eq (rbr-node {_} {_} {left} {right}) = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-right k₃ _ (subst (λ k → k < key) (sym lem23) x₁) (subst (λ k → tr> k₃ k) lem24 x₁₀) (subst (λ k → tr> k₃ k) lem25 x₂) lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - lem24 : t₁ ≡ left - lem24 = just-injective (cong node-left (just-injective (cong node-right eq))) - lem25 : t₂ ≡ right - lem25 = just-injective (cong node-right (just-injective (cong node-right eq))) - lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {left} {right} x x₁₀ x₂ ti) eq (rbr-right {k₂} {_} {_} {t₁} {t₂} {t₃} x₃ x₄ trb) = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-right k₃ _ (subst (λ k → k₃ < k) lem26 x) (subst (λ k → tr> k₃ k) lem24 x₁₀) rr01 lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - lem26 : k₁ ≡ k₂ - lem26 = just-injective (cong node-key (just-injective (cong node-right eq))) - lem24 : left ≡ t₂ - lem24 = just-injective (cong node-left (just-injective (cong node-right eq))) - rr01 : tr> k₃ t₁ - rr01 = RB-repl→ti> _ _ _ _ _ trb (<-trans (subst (λ k → k₃ < k ) lem26 x ) x₄ ) - (subst (λ j → tr> k₃ j) (just-injective (cong node-right (just-injective (cong node-right eq)))) x₂ ) - lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {left} {right} x x₁₀ x₂ ti) eq (rbr-left {k₂} {_} {_} {t₁} {t₂} {t₃} x₃ x₄ rbt) = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-right k₃ _ (subst (λ k → k₃ < k) lem26 x) rr02 rr01 lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - lem26 : k₁ ≡ k₂ - lem26 = just-injective (cong node-key (just-injective (cong node-right eq))) - rr01 : tr> k₃ t₃ - rr01 = subst (λ k → tr> k₃ k) (just-injective (cong node-right (just-injective (cong node-right eq)))) x₂ - rr02 : tr> k₃ t₁ - rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) - (subst (λ j → tr> k₃ j) (just-injective (cong node-left (just-injective (cong node-right eq)))) x₁₀ ) - lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {left} {right} x x₁₀ x₂ ti) eq (rbr-black-right {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-right k₃ _ (subst (λ k → k₃ < k) lem26 x) rr01 rr02 lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - lem26 : k₁ ≡ k₂ - lem26 = just-injective (cong node-key (just-injective (cong node-right eq))) - rr01 : tr> k₃ t₁ - rr01 = subst (λ k → tr> k₃ k) (just-injective (cong node-left (just-injective (cong node-right eq)))) x₁₀ - rr02 : tr> k₃ t₃ - rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) - (subst (λ k → tr> k₃ k) (just-injective (cong node-right (just-injective (cong node-right eq)))) x₂ ) - lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {left} {right} x x₁₀ x₂ ti) eq (rbr-black-left {t₁} {t₂} {t₃} {_} {k₂} x₃ x₄ rbt) = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ (subst (λ k → k₃ < k) lem26 x) rr02 rr01 lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - lem26 : k₁ ≡ k₂ - lem26 = just-injective (cong node-key (just-injective (cong node-right eq))) - rr01 : tr> k₃ t₁ - rr01 = subst (λ k → tr> k₃ k) (just-injective (cong node-right (just-injective (cong node-right eq)))) x₂ - rr02 : tr> k₃ t₃ - rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) - (subst (λ k → tr> k₃ k) (just-injective (cong node-left (just-injective (cong node-right eq)))) x₁₀ ) - lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti) eq (rbr-flip-ll x₃ x₄ x₅ rbt) = ⊥-elim ( ⊥-color ceq ) - lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti) eq (rbr-flip-lr x₃ x₄ x₅ x₆ rbt) = ⊥-elim ( ⊥-color ceq ) - lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti) eq (rbr-flip-rl x₃ x₄ x₅ x₆ rbt) = ⊥-elim ( ⊥-color ceq ) - lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti) eq (rbr-flip-rr x₃ x₄ x₅ rbt) = ⊥-elim ( ⊥-color ceq ) - lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ {_} {_} {left} {right} x x₁₀ x₂ ti₁) eq (rbr-rotate-ll {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ lem27 rr02 rr01 lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - lem27 : k₃ < kp - lem27 = subst (λ k → k < kp) (sym lem23) (<-trans x₁ x₄) - rr04 : (k₃ < kg) ∧ ((k₃ < kp) ∧ tr> k₃ t₁ ∧ tr> k₃ t) ∧ tr> k₃ uncle - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr01 : (k₃ < kg) ∧ tr> k₃ t ∧ tr> k₃ uncle - rr01 = ⟪ proj1 rr04 , ⟪ proj2 (proj2 (proj1 (proj2 rr04))) , proj2 (proj2 rr04) ⟫ ⟫ - rr02 : tr> k₃ t₂ - rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 (proj1 (proj2 rr04)))) - lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-rr {t} {t₁} {t₂} {uncle} {kg} {kp} x₃ x₄ rbt) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ lem27 rr01 rr02 lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₃ < kg) ∧ tr> k₃ uncle ∧ ((k₃ < kp) ∧ tr> k₃ t ∧ tr> k₃ t₁) - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - lem27 : k₃ < kp - lem27 = proj1 (proj2 (proj2 rr04)) - rr01 : (k₃ < kg) ∧ tr> k₃ uncle ∧ tr> k₃ t - rr01 = ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ - rr02 : tr> k₃ t₂ - rr02 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 (proj2 (proj2 rr04)))) - lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ lem27 rr05 rr06 lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₃ < kg) ∧ ((k₃ < kp) ∧ tr> k₃ t ∧ tr> k₃ t₁) ∧ tr> k₃ uncle - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr01 : (k₃ < kn) ∧ tr> k₃ t₂ ∧ tr> k₃ t₃ - rr01 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 (proj1 (proj2 rr04)))) - lem27 : k₃ < kn - lem27 = proj1 rr01 - rr05 : (k₃ < kp) ∧ tr> k₃ t ∧ tr> k₃ t₂ - rr05 = ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , proj1 (proj2 rr01) ⟫ ⟫ - rr06 : (k₃ < kg) ∧ tr> k₃ t₃ ∧ tr> k₃ uncle - rr06 = ⟪ proj1 rr04 , ⟪ proj2 (proj2 rr01) , proj2 (proj2 rr04) ⟫ ⟫ - lem21 (node k₃ _ leaf (node k₁ _ _ _)) (t-right k₃ k₁ x x₁₀ x₂ ti₁) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) (t-right k₃ _ lem27 rr05 rr06 lem22) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₃ < kg) ∧ tr> k₃ uncle ∧ ( (k₃ < kp) ∧ tr> k₃ t₁ ∧ tr> k₃ t) - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr01 : (k₃ < kn) ∧ tr> k₃ t₂ ∧ tr> k₃ t₃ - rr01 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 (proj2 (proj2 rr04))) ) - lem27 : k₃ < kn - lem27 = proj1 rr01 - rr05 : (k₃ < kg) ∧ tr> k₃ uncle ∧ tr> k₃ t₂ - rr05 = ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 rr01) ⟫ ⟫ - rr06 : (k₃ < kp) ∧ tr> k₃ t₃ ∧ tr> k₃ t - rr06 = ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj2 (proj2 rr01) , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti₁) eq rbr-leaf = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (subst (λ j → j < key) (sym lem23) x₁) x₁₀ x₂ tt tt ti₁ (t-single key ⟪ Red , value ⟫)) where - lem23 : k₃ ≡ k - lem23 = just-injective (cong node-key eq) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () rbr-node - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-right x₃ x₄ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-left x₃ x₄ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-black-right x₃ x₄ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-black-left x₃ x₄ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-flip-ll x₃ x₄ x₅ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-flip-lr x₃ x₄ x₅ x₆ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-flip-rl x₃ x₄ x₅ x₆ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-flip-rr x₃ x₄ x₅ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-rotate-ll x₃ x₄ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-rotate-rr x₃ x₄ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-rotate-lr t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) - lem21 (node k₃ _ (node k₁ _ _ _) leaf) (t-left .k₁ k₃ x x₁₀ x₂ ti) () (rbr-rotate-rl t₂ t₃ kg kp kn x₃ x₄ x₅ rbt) - lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti ti₁) () rbr-leaf - lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ {_} {_} {_} {t} {t₁} {t₂} x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-node {_} {_} {t₃} {t₄}) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (subst (λ j → j < key) (sym lem23) x₁) x₂ x₃ (proj1 (proj2 rr04)) (proj2 (proj2 rr04)) ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < key) ∧ tr> k₁ t₃ ∧ tr> k₁ t₄ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-right {k₃} {_} {_} {t₁} {t₂} {t₃} x₆ x₇ rbt) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (proj1 rr04) x₂ x₃ (proj1 (proj2 rr04)) rr05 ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < k₃) ∧ tr> k₁ t₂ ∧ tr> k₁ t₃ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti)) - rr05 : tr> k₁ t₁ - rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 rr04)) - lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-left {k₃} {_} {_} {t₁} {t₂} {t₃} x₆ x₇ rbt) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (proj1 rr04) x₂ x₃ rr05 (proj2 (proj2 rr04)) ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < k₃) ∧ tr> k₁ t₂ ∧ tr> k₁ t₃ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti )) - rr05 : tr> k₁ t₁ - rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 rr04)) - lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-right {t₁} {t₂} {t₃} {_} {k₃} x₆ x₇ rbt) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (proj1 rr04) x₂ x₃ (proj1 (proj2 rr04)) rr05 ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < k₃) ∧ tr> k₁ t₁ ∧ tr> k₁ t₂ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti )) - rr05 : tr> k₁ t₃ - rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 rr04)) - lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-black-left {t₁} {t₂} {t₃} {_} {k₃} x₆ x₇ rbt) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (proj1 rr04) x₂ x₃ rr05 (proj2 (proj2 rr04)) ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < k₃) ∧ tr> k₁ t₂ ∧ tr> k₁ t₁ - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti )) - rr05 : tr> k₁ t₃ - rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 rr04)) - lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti ti₁) eq (rbr-flip-ll x₆ x₇ x₈ rbt) = ⊥-elim ( ⊥-color ceq ) - lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti ti₁) eq (rbr-flip-lr x₆ x₇ x₈ x₉ rbt) = ⊥-elim ( ⊥-color ceq ) - lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti ti₁) eq (rbr-flip-rl x₆ x₇ x₈ x₉ rbt) = ⊥-elim ( ⊥-color ceq ) - lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti ti₁) eq (rbr-flip-rr x₆ x₇ x₈ rbt) = ⊥-elim ( ⊥-color ceq ) - lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-ll {t₁} {t₂} {t₃} {uncle} {kg} {kp} x₆ x₇ rbt) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (proj1 (proj1 (proj2 rr04))) x₂ x₃ rr05 ⟪ proj1 rr04 , ⟪ proj2 (proj2 (proj1 (proj2 rr04))) , proj2 (proj2 rr04) ⟫ ⟫ ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < kg) ∧ ((k₁ < kp) ∧ tr> k₁ t₂ ∧ tr> k₁ t₁) ∧ tr> k₁ uncle - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti )) - rr05 : tr> k₁ t₃ - rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 (proj1 (proj2 rr04)))) - lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rr {t₁} {t₂} {t₃} {uncle} {kg} {kp} x₆ x₇ rbt) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (proj1 (proj2 (proj2 rr04))) x₂ x₃ ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ rr05 ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < kg) ∧ tr> k₁ uncle ∧ ((k₁ < kp) ∧ tr> k₁ t₁ ∧ tr> k₁ t₂) - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti )) - rr05 : tr> k₁ t₃ - rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 (proj2 (proj2 rr04)))) - lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-lr {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (proj1 rr05) x₂ x₃ ⟪ proj1 (proj1 (proj2 rr04)) , ⟪ proj1 (proj2 (proj1 (proj2 rr04))) , proj1 (proj2 rr05) ⟫ ⟫ - ⟪ proj1 rr04 , ⟪ proj2 (proj2 rr05) , proj2 (proj2 rr04) ⟫ ⟫ ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < kg) ∧ ((k₁ < kp) ∧ tr> k₁ t ∧ tr> k₁ t₁) ∧ tr> k₁ uncle - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti )) - rr05 : (k₁ < kn) ∧ tr> k₁ t₂ ∧ tr> k₁ t₃ - rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj2 (proj2 (proj1 (proj2 rr04)))) - lem21 (node k₁ _ (node k₂ _ _ _) (node k₄ _ _ _)) (t-node k₂ .k₁ k₄ x x₁₀ x₂ x₃ x₄ x₅ ti₁ ti₂) eq (rbr-rotate-rl {t} {t₁} {uncle} t₂ t₃ kg kp kn x₆ x₇ x₈ rbt) - = subst treeInvariant - (node-cong lem23 refl (just-injective (cong node-left eq)) refl) - (t-node _ _ _ x (proj1 rr05) x₂ x₃ ⟪ proj1 rr04 , ⟪ proj1 (proj2 rr04) , proj1 (proj2 rr05) ⟫ ⟫ - ⟪ proj1 (proj2 (proj2 rr04)) , ⟪ proj2 (proj2 rr05) , proj2 (proj2 (proj2 (proj2 rr04))) ⟫ ⟫ ti₁ lem22) where - lem23 : k₁ ≡ k - lem23 = just-injective (cong node-key eq) - rr04 : (k₁ < kg) ∧ tr> k₁ uncle ∧ ((k₁ < kp) ∧ tr> k₁ t₁ ∧ tr> k₁ t) - rr04 = proj2 (ti-property1 (subst (λ k → treeInvariant ( node k _ _ _ )) (sym lem23) ti )) - rr05 : (k₁ < kn) ∧ tr> k₁ t₂ ∧ tr> k₁ t₃ - rr05 = RB-repl→ti> _ _ _ _ _ rbt (subst (λ j → j < key) (sym lem23) x₁) (proj1 (proj2 (proj2 (proj2 rr04)))) PGtoRBinvariant1 : {n : Level} {A : Set n} → (tree orig : bt (Color ∧ A) ) @@ -1164,14 +89,6 @@ PGtoRBinvariant1 tree .tree rb .(tree ∷ []) s-nil = rb PGtoRBinvariant1 tree orig rb = {!!} -RBI-child-replaced : {n : Level} {A : Set n} (tr : bt (Color ∧ A)) (key : ℕ) → RBtreeInvariant tr → RBtreeInvariant (child-replaced key tr) -RBI-child-replaced {n} {A} leaf key rbi = rbi -RBI-child-replaced {n} {A} (node key₁ value tr tr₁) key rbi with <-cmp key key₁ -... | tri< a ¬b ¬c = RBtreeLeftDown _ _ rbi -... | tri≈ ¬a b ¬c = rbi -... | tri> ¬a ¬b c = RBtreeRightDown _ _ rbi - - -- -- if we consider tree invariant, this may be much simpler and faster --