# HG changeset patch # User Shinji KONO # Date 1705991598 -32400 # Node ID 82029d2a897048f39b4c61b5c449c81626754290 # Parent 8dbddf72211e79388d8e426506984896978ad9f0 ... diff -r 8dbddf72211e -r 82029d2a8970 hoareBinaryTree1.agda --- a/hoareBinaryTree1.agda Mon Jan 22 18:51:56 2024 +0900 +++ b/hoareBinaryTree1.agda Tue Jan 23 15:33:18 2024 +0900 @@ -582,34 +582,34 @@ → 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-unit : {t : bt A} → rotatedTree t t - rtt-node : {left left' right right' : bt A} → {ke : ℕ} {ve : A} → - rotatedTree left left' → rotatedTree right right' → rotatedTree (node ke ve left right) (node ke ve left' right') - -- 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)) - +-- data rotatedTree {n : Level} {A : Set n} : (before after : bt A) → Set n where +-- rtt-unit : {t : bt A} → rotatedTree t t +-- rtt-node : {left left' right right' : bt A} → {ke : ℕ} {ve : A} → +-- rotatedTree left left' → rotatedTree right right' → rotatedTree (node ke ve left right) (node ke ve left' right') +-- -- 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)) +-- RightDown : {n : Level} {A : Set n} → bt (Color ∧ A) → bt (Color ∧ A) RightDown leaf = leaf RightDown (node key ⟪ c , value ⟫ t1 t2) = t2 @@ -651,6 +651,14 @@ RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = tir RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = tir +-- +-- findRBT exit with replaced node +-- case-eq node value is replaced, just do replacedTree and rebuild rb-invariant +-- case-leaf insert new single node +-- case1 if parent node is black, just do replacedTree and rebuild rb-invariant +-- case2 if parent node is red, increase blackdepth, do rotatation +-- + findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A))) → RBtreeInvariant tree ∧ stackInvariant key tree tree0 stack @@ -701,14 +709,15 @@ findRBTreeTest = findTest 14 testRBTree0 testRBI0 $ λ tr s P O → (record {tree = tr ; stack = s ; ti = (proj1 P) ; si = (proj2 P)}) --- we can re use replacedTree --- data replacedRBTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt (Color ∧ A) ) → Set n where --- rbr-leaf : {ca cb : Color} → replacedTree key value leaf (node key ⟪ cb , value ⟫ leaf leaf) --- rbr-node : {value₁ : A} → {ca cb : Color } → {t t₁ : bt (Color ∧ A)} → replacedTree 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 → replacedTree key value t2 t → replacedTree 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)} --- → key < k → replacedTree key value t1 t → replacedTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2) -- k < key → key < k +-- create replaceRBTree with rotate + +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)} + → key < k → replacedRBTree key value t1 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2) -- k < key → key < k 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 } @@ -727,17 +736,25 @@ 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 : ℕ) : (tree repl : bt (Color ∧ A) ) → Set n where + rebuild : {tree repl : bt (Color ∧ A) } → black-depth repl ≡ black-depth (child-replaced key tree) → RBI-state key tree repl + rotate : {tree repl : bt (Color ∧ A) } → color repl ≡ Red → black-depth repl ≡ suc (black-depth (child-replaced key tree)) → RBI-state key tree repl + record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) : Set n where field - tree rot : bt (Color ∧ A) + tree : bt (Color ∧ A) origti : treeInvariant orig origrb : RBtreeInvariant orig treerb : RBtreeInvariant tree -- tree node te be replaced replrb : RBtreeInvariant repl si : stackInvariant key tree orig stack - rotated : rotatedTree tree rot - ri : replacedTree key ⟪ Red , value ⟫ (child-replaced key rot ) repl - ∨ replacedTree key ⟪ Black , value ⟫ (child-replaced key rot ) repl + rotated : replacedRBTree key value tree repl + state : RBI-state key tree repl stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A ) → (stack : List (bt A)) → stackInvariant key tree orig stack @@ -854,7 +871,25 @@ -- = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) --- if we have replacedNode on RBTree, we have RBtreeInvariant +-- +-- replaced node increase blackdepth, so we need tree rotate +-- +-- case2 tree is Red +-- +-- go upward until +-- +-- if root +-- insert top +-- if unkle is leaf or Black +-- go insertCase5/6 +-- +-- make color tree ≡ Black , color unkle ≡ Black, color grand ≡ Red +-- loop with grand as repl +-- +-- case5/case6 rotation +-- +-- rotate and rebuild replaceTree and rb-invariant + replaceRBP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) @@ -942,23 +977,20 @@ -- insertCase13 : (v : Color ∧ A ) → v ≡ value₁ → t insertCase13 ⟪ Black , value₄ ⟫ refl = exit (node key₁ ⟪ Black , value₄ ⟫ left repl) (orig ∷ []) refl record { - tree = orig ; rot = node key₁ value₁ left (RBI.rot r) + tree = orig ; origti = RBI.origti r ; origrb = RBI.origrb r ; treerb = RBI.origrb r - ; replrb = proj1 (rb05 (RBI.ri r)) + ; replrb = ? ; si = s-nil - ; rotated = subst (λ k → rotatedTree k (node key₁ value₁ left (RBI.rot r))) ( - trans (cong (λ k → node key₁ value₁ left k) (sym (rb04 si eq refl))) refl) (rtt-node rtt-unit (RBI.rotated r)) - ; ri = proj2 (rb05 (RBI.ri r)) + ; rotated = ? + ; ri = ? + ; state = ? } where rb09 : {n : Level} {A : Set n} → {key key1 key2 : ℕ} {value value1 : A} {t1 t2 : bt (Color ∧ A)} → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key1 ⟪ Black , value1 ⟫ t1 t2)) → key < key1 rb09 (rb-right-red x x0 x2) = x - rb08 : replacedTree key ⟪ Red , value ⟫ (child-replaced key (RBI.rot r)) repl - ∨ replacedTree key ⟪ Black , value ⟫ (child-replaced key (RBI.rot r)) repl - rb08 = RBI.ri r -- rb05 should more general tkey : {n : Level} {A : Set n } → (rbt : bt (Color ∧ A)) → ℕ tkey (node key value t t2) = key @@ -967,21 +999,6 @@ rb051 = {!!} rb052 : {key key₁ : ℕ} → stackInvariant key (RBI.tree r) orig stack → key < key₁ rb052 = {!!} - rb05 : ( replacedTree key ⟪ Red , value ⟫ (child-replaced key (RBI.rot r)) repl - ∨ replacedTree key ⟪ Black , value ⟫ (child-replaced key (RBI.rot r)) repl ) - → RBtreeInvariant (node key₁ ⟪ Black , value₄ ⟫ left repl) - ∧ ( replacedTree key ⟪ Red , value ⟫ - (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r)) ) - (node key₁ ⟪ Black , value₄ ⟫ left repl) - ∨ - replacedTree key ⟪ Black , value ⟫ - (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r)) ) - (node key₁ ⟪ Black , value₄ ⟫ left repl) ) - rb05 (case1 ri) with <-cmp key key₁ - ... | tri< a ¬b ¬c = ⊥-elim ( ¬c c) - ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c c) - ... | tri> ¬a ¬b c = ⟪ ? , case1 ? ⟫ - rb05 (case2 ri) = ⟪ ? , ? ⟫ insertCase13 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r) ... | Black = exit {!!} {!!} {!!} {!!} ... | Red = exit {!!} {!!} {!!} {!!}