Mercurial > hg > Gears > GearsAgda
changeset 796:e1737f00a7aa
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 26 Oct 2023 18:11:17 +0900 |
| parents | e9ba6a5bc64b |
| children | 03831d974342 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 1 insertions(+), 62 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Tue Oct 24 10:33:48 2023 +0900 +++ b/hoareBinaryTree1.agda Thu Oct 26 18:11:17 2023 +0900 @@ -700,67 +700,6 @@ repl-red : color repl ≡ Red repl-eq : black-depth (child-replaced key rot ) ≡ black-depth repl --- r (b , b) inserting a node into black node does not change the black depth, but color may change --- → b (b , r ) ∨ b (r , b) --- b (b , b) --- → b (b , r ) ∨ b (r , b) --- b (r , b) inserting to right → b (r , r ) --- b (r , b) inserting to left may increse black depth, need rotation --- find b in left and move the b to the right (one down or two down) --- -rbi-case1 : {n : Level} {A : Set n} → {key d : ℕ} → {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} = {!!} - -rbi-case31 : {n : Level} {A : Set n} → {kg kp d dp : ℕ} → {vg vp : A} → {cg : Color} → (tree grand parent repl : bt (Color ∧ A) ) - → RBtreeInvariant grand - → RBtreeInvariant repl - → {uncle left right : bt (Color ∧ A) } - → grand ≡ node kg ⟪ cg , vg ⟫ uncle parent - → parent ≡ node kp ⟪ Red , vp ⟫ left right - → color uncle ≡ Red - → (color left ≡ Red → RBtreeInvariant (node kg ⟪ Red , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ repl right )) ) - ∧ (color right ≡ Red → RBtreeInvariant (node kg ⟪ Red , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ left repl )) ) -rbi-case31 {n} {A} {key} = {!!} - --- --- case4 increase the black depth --- -rbi-case41 : {n : Level} {A : Set n} → {kg kp d dp : ℕ} → {vg vp : A} → {cg : Color} → (tree grand parent repl : bt (Color ∧ A) ) - → RBtreeInvariant grand - → RBtreeInvariant repl - → {uncle left right : bt (Color ∧ A) } - → grand ≡ node kg ⟪ cg , vg ⟫ uncle parent - → parent ≡ node kp ⟪ Red , vp ⟫ left right - → color uncle ≡ Black - → (color left ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ repl right )) ) - ∧ (color right ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ left repl )) ) -rbi-case41 {n} {A} {key} = {!!} - -rbi-case51 : {n : Level} {A : Set n} → {kg kp d dp : ℕ} → {vg vp : A} → {cg : Color} → (tree grand parent repl : bt (Color ∧ A) ) - → RBtreeInvariant grand - → RBtreeInvariant repl - → {uncle left right : bt (Color ∧ A) } - → grand ≡ node kg ⟪ cg , vg ⟫ uncle parent - → parent ≡ node kp ⟪ Red , vp ⟫ left right - → color uncle ≡ Black - → (color left ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ repl right )) ) - ∧ (color right ≡ Red → RBtreeInvariant (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ left repl )) ) -rbi-case51 {n} {A} {key} = {!!} - ---... | Black = record { --- d = ? ; od = RBI.od rbi ; rd = ? --- ; tree = ? ; rot = ? ; repl = ? --- ; treerb = ? ; replrb = ? --- ; d=rd = ? ; si = ? ; rotated = ? ; ri = ? --- ; origti = RBI.origti rbi ; origrb = RBI.origrb rbi --- } ---... | Red = ? - stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A ) → (stack : List (bt A)) → stackInvariant key tree orig stack → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A tree stack @@ -959,7 +898,7 @@ -- / \ / \ / \ rotate L / \ -- L L1 L R3 L R -- bad B B -- / \ / \ / \ 1 : child-replace - --- L L2 L B L L 2: child-replace ( unbrance ) + --- L L2 L B L L 2: child-replace ( unbalanced ) -- / \ 3: child-replace ( rotated / balanced ) -- L L --