Mercurial > hg > Members > Moririn
diff work.agda @ 779:68904fdaab71
te
| author | Moririn < Moririn@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 10 Jul 2023 19:59:14 +0900 |
| parents | |
| children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/work.agda Mon Jul 10 19:59:14 2023 +0900 @@ -0,0 +1,365 @@ +module work where +open import Level hiding (suc ; zero ; _⊔_ ) + +open import Data.Nat hiding (compare) +open import Data.Nat.Properties as NatProp +open import Data.Maybe +-- open import Data.Maybe.Properties +open import Data.Empty +open import Data.List +open import Data.Product + +open import Function as F hiding (const) + +open import Relation.Binary +open import Relation.Binary.PropositionalEquality +open import Relation.Nullary +open import logic + +data bt {n : Level} (A : Set n) : Set n where + leaf : bt A + node : (key : ℕ) → (value : A) → (left : bt A) → (right : bt A) → bt A + +node-key : {n : Level}{A : Set n} → bt A → Maybe ℕ +node-key leaf = nothing +node-key (node key value tree tree₁) = just key + +node-value : {n : Level} {A : Set n} → bt A → Maybe A +node-value leaf = nothing +node-value (node key value tree tree₁) = just value + +bt-depth : {n : Level} {A : Set n} → (tree : bt A) → ℕ +bt-depth leaf = 0 +bt-depth (node key value tree tree₁) = suc (bt-depth tree ⊔ bt-depth tree₁) +--一番下のleaf =0から戻るたびにsucをしていく +treeTest1 : bt ℕ +treeTest1 = node 0 0 leaf (node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf)) + +-- 0 0 +-- / \ +-- leaf 3 1 +-- / \ +-- 2 5 2 +-- / \ +-- 1 leaf 3 +-- / \ +-- leaf leaf 4 + +treeTest2 : bt ℕ +treeTest2 = node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf) + +testdb : ℕ +testdb = bt-depth treeTest1 -- 4 + +import Data.Unit hiding ( _≟_ ; _≤?_ ; _≤_) + +data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where + t-leaf : treeInvariant leaf + + t-single : (key : ℕ) → (value : A) → treeInvariant (node key value leaf leaf) + + t-left : {key key1 : ℕ} → {value value1 : A} → {t1 t2 : bt A} → key < key1 + → treeInvariant (node key value t1 t2) + → treeInvariant (node key1 value1 (node key value t1 t2) leaf) + + t-right : {key key1 : ℕ} → {value value1 : A} → {t1 t2 : bt A} → key < key1 + → treeInvariant (node key1 value1 t1 t2) + → treeInvariant (node key value leaf (node key1 value1 t1 t2)) + + t-node : {key key1 key2 : ℕ}→ {value value1 value2 : A} → {t1 t2 t3 t4 : bt A} → key1 < key → key < key2 + → treeInvariant (node key1 value1 t1 t2) + → treeInvariant (node key2 value2 t3 t4) + → treeInvariant (node key value (node key1 value1 t1 t2) (node key2 value2 t3 t4)) + +data stackInvariant {n : Level} {A : Set n} (key : ℕ ) : (top orig : bt A) + → (stack : List (bt A)) → Set n where + s-nil : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [] ) + + s-right : {key1 : ℕ } → {value : A } → {tree0 t1 t2 : bt A } → {st : List (bt A)} + → key1 < key + → stackInvariant key (node key1 value t1 t2) tree0 st + → stackInvariant key t2 tree0 (t2 ∷ st) + + s-left : {key1 : ℕ } → {value : A } → {tree0 t1 t2 : bt A } → {st : List (bt A)} + → key < key1 + → stackInvariant key (node key1 value t1 t2) tree0 st + → stackInvariant key t1 tree0 (t1 ∷ st) + +data replacedTree {n : Level } {A : Set n} (key : ℕ) (value : A) : (before after : bt A) → Set n where + r-leaf : replacedTree key value leaf (node key value leaf leaf) + + r-node : {value1 : A} → {left right : bt A} → replacedTree key value (node key value left right) (node key value1 left right) + + -- key is the repl's key , so need comp key and key1 + r-left : {key1 : ℕ} {value1 : A }→ {left right repl : bt A} → key < key1 + → replacedTree key value left repl → replacedTree key value (node key1 value1 left right) (node key1 value1 repl right) + + r-right : {key1 : ℕ } {value1 : A} → {left right repl : bt A} → key1 < key + → replacedTree key value right repl → replacedTree key value (node key1 value1 left right) (node key1 value1 left repl) + +{- +RTtoTI0 : {n : Level} {A : Set n } → (key : ℕ ) → (value : A) → (tree repl : bt A) + → treeInvariant tree → replacedTree key value tree repl → treeInvariant repl +RTtoTI0 key value leaf (node key value leaf leaf) tr r-leaf = t-single key value +RTtoTI0 key value (node key₁ value₁ tree tree₁) (node key₂ value₂ repl repl₁) (t-node x x₁ s s₁) r-node = t-node x x₁ s s₁ +-} +depth-1< : {i j : ℕ} → suc i ≤ suc (i Data.Nat.⊔ j ) +depth-1< {i} {j} = s≤s (m≤m⊔n _ j) +depth-2< : {i j : ℕ} → suc i ≤ suc (j Data.Nat.⊔ i ) +depth-2< {i} {j} = s≤s (m≤n⊔m j i) +depth-3< : {i : ℕ } → suc i ≤ suc (suc i) +depth-3< {zero} = s≤s ( z≤n ) +depth-3< {suc i} = s≤s (depth-3< {i} ) + +treeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} → (tleft tright : bt A) + → treeInvariant (node key value tleft tright) + → treeInvariant tleft +treeLeftDown leaf leaf (t-single key value) = t-leaf +treeLeftDown leaf (node key value t1 t2) (t-right x ti) = t-leaf +treeLeftDown (node key value t t₁) leaf (t-left x ti) = ti +treeLeftDown (node key value t t₁) (node key₁ value₁ t1 t2) (t-node x x1 ti ti2 ) = ti + +treeRightDown : {n : Level} {A : Set n} {key : ℕ} {value : A} → (tleft tright : bt A) + → treeInvariant (node key value tleft tright) + → treeInvariant tright +treeRightDown leaf leaf (t-single key value) = t-leaf +treeRightDown leaf (node key value t1 t2) (t-right x ti) = ti + +treeRightDown (node key value t t₁) leaf (t-left x ti) = t-leaf +treeRightDown (node key value t t₁) (node key₁ value₁ t1 t2) (t-node x x1 ti ti2 ) = ti2 + + +findP : {n m : Level} {A : Set n} {t : Set n} → (tkey : ℕ) → (top orig : bt A) → (st : List (bt A)) + → (treeInvariant top) + → stackInvariant tkey top orig st + → (next : (newtop : bt A) → (stack : List (bt A)) + → (treeInvariant newtop) + → (stackInvariant tkey newtop orig stack) + → bt-depth newtop < bt-depth top → t) + → (exit : (newtop : bt A) → (stack : List (bt A)) + → (treeInvariant newtop) + → (stackInvariant tkey newtop orig stack) --need new stack ? + → (newtop ≡ leaf) ∨ (node-key newtop ≡ just tkey) → t) + → t +findP tkey leaf orig st ti si next exit = exit leaf st ti si (case1 refl) +findP tkey (node key value tl tr) orig st ti si next exit with <-cmp tkey key +findP tkey top orig st ti si next exit | tri≈ ¬a refl ¬c = exit top st ti si (case2 refl) +findP tkey (node key value tl tr) orig st ti si next exit | tri< a ¬b ¬c = next tl (tl ∷ st) (treeLeftDown tl tr ti) (s-left a si) (s≤s (m≤m⊔n (bt-depth tl) (bt-depth tr))) + +findP tkey (node key value tl tr) orig st ti si next exit | tri> ¬a ¬b c = next tr (tr ∷ st) (treeRightDown tl tr ti) (s-right c si) (s≤s (m≤n⊔m (bt-depth tl) (bt-depth tr))) + + +--RBT +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 + +black-depth : {n : Level} {A : Set n} → (tree : bt (Color ∧ A) ) → ℕ +black-depth leaf = 0 +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₁ ) + +data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where + rb-leaf : RBtreeInvariant leaf + rb-single : (key : ℕ) → (value : A) → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf leaf) + rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ + → black-depth t ≡ black-depth t₁ + → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) + → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key₁ ⟪ Black , value₁ ⟫ t t₁)) + rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {c : Color} + → black-depth t ≡ black-depth t₁ + → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁) + → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁)) + rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ + → black-depth t ≡ black-depth t₁ + → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) + → RBtreeInvariant (node key ⟪ Red , value ⟫ (node key₁ ⟪ Black , value₁ ⟫ t t₁) leaf ) + rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {c : Color} + → black-depth t ≡ black-depth t₁ + → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁) + → RBtreeInvariant (node key ⟪ Black , value ⟫ (node key₁ ⟪ c , value₁ ⟫ t t₁) leaf) + rb-node-red : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ + → black-depth t₁ ≡ black-depth t₂ + → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ t₂) + → black-depth t₃ ≡ black-depth t₄ + → RBtreeInvariant (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄) + → RBtreeInvariant (node key₁ ⟪ Red , value₁ ⟫ (node key ⟪ Black , value ⟫ t₁ t₂) (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)) + rb-node-black : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ + → {c c₁ : Color} + → black-depth t₁ ≡ black-depth t₂ + → RBtreeInvariant (node key ⟪ c , value ⟫ t₁ t₂) + → black-depth t₃ ≡ black-depth t₄ + → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) + → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)) + + +data rotatedTree {n : Level} {A : Set n} : (before after : bt A) → Set n where + rtt-node : {t : bt A } → rotatedTree t t + -- a b + -- b c d a + -- d e e c + -- + rtt-right : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A} + --kd < kb < ke < ka< kc + → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A} + → kd < kb → kb < ke → ke < ka → ka < kc + → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1) + → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1) + → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1) + → rotatedTree (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr)) + (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1))) + + rtt-left : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A} + --kd < kb < ke < ka< kc + → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A} -- after child + → kd < kb → kb < ke → ke < ka → ka < kc + → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1) + → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1) + → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1) + → rotatedTree (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1))) + (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr)) + +RBtreeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color} + → (tleft tright : bt (Color ∧ A)) + → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright) + → RBtreeInvariant tleft +RBtreeLeftDown leaf leaf (rb-single k1 v) = rb-leaf +RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rb-leaf +RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rb-leaf +RBtreeLeftDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rb-leaf +RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti +RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti)= ti +RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti +RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til +RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til bde2 tir) = til +RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til +RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til +RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til + +RBtreeRightDown : {n : Level} {A : Set n} { key : ℕ} {value : A} {c : Color} + → (tleft tright : bt (Color ∧ A)) + → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright) + → RBtreeInvariant tright +RBtreeRightDown leaf leaf (rb-single k1 v1 ) = rb-leaf +RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rbti +RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rbti +RBtreeRightDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rbti +RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf +RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti) = rb-leaf +RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf +RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir +RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til bde2 tir) = tir +RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir +RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir +RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir + +findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) ) + → (stack : List (bt (Color ∧ A))) + → treeInvariant tree ∧ stackInvariant key tree tree0 stack + → RBtreeInvariant tree + → (next : (tree1 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A))) + → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack + → RBtreeInvariant tree1 + → bt-depth tree1 < bt-depth tree → t ) + → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) + → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack + → RBtreeInvariant tree1 + → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t +findRBT key leaf tree0 stack ti rb0 next exit = exit leaf stack ti rb0 (case1 refl) +findRBT key n@(node key₁ value left right) tree0 stack ti rb0 next exit with <-cmp key key₁ +findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri< a ¬b ¬c + = next left (left ∷ stack) ⟪ treeLeftDown left right (_∧_.proj1 ti) , s-left a (_∧_.proj2 ti) ⟫ (RBtreeLeftDown left right rb0) depth-1< +findRBT key n tree0 stack ti rb0 _ exit | tri≈ ¬a refl ¬c = exit n stack ti rb0 (case2 refl) +findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri> ¬a ¬b c + = next right (right ∷ stack) ⟪ treeRightDown left right (_∧_.proj1 ti), s-right c (_∧_.proj2 ti) ⟫ (RBtreeRightDown left right rb0) depth-2< + +child-replaced : {n : Level} {A : Set n} (key : ℕ) (tree : bt A) → bt A +child-replaced key leaf = leaf +child-replaced key (node key₁ value left right) with <-cmp key key₁ +... | tri< a ¬b ¬c = left +... | tri≈ ¬a b ¬c = node key₁ value left right +... | tri> ¬a ¬b c = right + + +data replacedRBTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt (Color ∧ A) ) → Set n where + rbr-leaf : {ca cb : Color} → replacedRBTree key value leaf (node key ⟪ cb , value ⟫ leaf leaf) + rbr-node : {value₁ : A} → {ca cb : Color } → {t t₁ : bt (Color ∧ A)} + → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ cb , value ⟫ t t₁) + rbr-right : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)} + → k < key → replacedRBTree key value t2 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t1 t) + rbr-left : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)} + → k < key → replacedRBTree key value t1 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2) + +data ParentGrand {n : Level} {A : Set n} (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 } + → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand + s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } + → parent ≡ node kp vp n1 self → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand + s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } + → parent ≡ node kp vp self n1 → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand + s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } + → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand + +record PG {n : Level } (A : Set n) (self : bt A) (stack : List (bt A)) : Set n where + field + parent grand uncle : bt A + pg : ParentGrand self parent uncle grand + rest : List (bt A) + stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest ) + +record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) : Set n where + field + od d rd : ℕ + tree rot : bt (Color ∧ A) + origti : treeInvariant orig + origrb : RBtreeInvariant orig + treerb : RBtreeInvariant tree + replrb : RBtreeInvariant repl + d=rd : ( d ≡ rd ) ∨ ((suc d ≡ rd ) ∧ (color tree ≡ Red)) + si : stackInvariant key tree orig stack + rotated : rotatedTree tree rot + ri : replacedRBTree key value (child-replaced key rot ) repl + + +{- +rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) ) + → RBtreeInvariant parent + → RBtreeInvariant repl + → {left right : bt (Color ∧ A)} → parent ≡ node key ⟪ Black , value ⟫ left right + → (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl ) ) + ∧ (color left ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) ) +rbi-case1 {n} {A} {key} (node key1 ⟪ Black , value1 ⟫ l r) leaf rbip rbir left right x = {!!} +rbi-case1 {n} {A} {key} parent (node key₁ value₁ tree1 tree2) rbi rb2 x = {!!} + +-} +blackdepth≡ : {n : Level } {A : Set n} → {C : Color} {key : ℕ} {value : A} → (tree1 tree2 : bt (Color ∧ A)) + → RBtreeInvariant tree1 + → RBtreeInvariant tree2 + → RBtreeInvariant (node key ⟪ C , value ⟫ tree1 tree2) + → black-depth tree1 ≡ black-depth tree2 + +blackdepth≡ leaf leaf ri1 ri2 rip = refl +blackdepth≡ leaf (node key value t2 t3) ri1 ri2 rip = {!!} --rip kara mitibiki daseru RBinvariant kara toreruka +blackdepth≡ (node key value t1 t3) leaf ri1 ri2 rip = {!!} +blackdepth≡ (node key value t1 t3) (node key₁ value₁ t2 t4) ri1 ri2 rip = {!!} + +rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) ) + → RBtreeInvariant parent + → RBtreeInvariant repl + → (left right : bt (Color ∧ A)) → parent ≡ node key ⟪ Black , value ⟫ left right + → RBtreeInvariant left + → RBtreeInvariant right + → (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl ) ) ∧ (color left ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) ) +rbi-case1 {n} {A} {key} (node key1 ⟪ Black , value1 ⟫ l r) leaf rbip rbir (node key3 ⟪ Red , val3 ⟫ la ra) (node key4 ⟪ Red , val4 ⟫ lb rb) pa li ri + = ⟪ {!!} rb-left-black {!!} {!!} li , (λ x → rb-right-black {!!} {!!} ri) ⟫ + +--⟪ rb-left-black {!!} {!!} (RBtreeLeftDown left right rbip ) , {!!} ⟫ +--rbi-case1 {n} {A} {key} parent (node key₁ value₁ tree1 tree2) rbi rb2 x = {!!}