# HG changeset patch # User Shinji KONO # Date 1706212557 -32400 # Node ID aeb14a056896e751b35e95fa006d88ded565c76d # Parent 317539bdba034528418ab297d71dd1ccaddf4cc9 ... diff -r 317539bdba03 -r aeb14a056896 hoareBinaryTree1.agda --- a/hoareBinaryTree1.agda Thu Jan 25 20:37:25 2024 +0900 +++ b/hoareBinaryTree1.agda Fri Jan 26 04:55:57 2024 +0900 @@ -727,12 +727,54 @@ -- 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 + 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)} + → 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)} + → 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 + + rbr-black-right : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} + → color t₂ ≡ Red → 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 → replacedRBTree key value t₁ t₂ + → replacedRBTree key value (node key₁ ⟪ Black , value₁ ⟫ t₁ t) (node key₁ ⟪ Black , value₁ ⟫ t₂ t) + + rbr-flip-ll : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} + → color t₂ ≡ Red → 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 → 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 → 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 → 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-rotate-ll : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} - case6 + → color t₂ ≡ Red → 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} - case6 + → color t₂ ≡ Red → 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₂ ) + rbr-rotate-lr : {t t₁ t₂ t₃ uncle : bt (Color ∧ A)} {kg kp kn : ℕ} {vg vp vn : A} - case56 + → 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₁ t₂ t₃ uncle : bt (Color ∧ A)} {kg kp kn : ℕ} {vg vp vn : A - case56 + → 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 ⟫ t₁ uncle) (node kp ⟪ Red , vp ⟫ t₂ t₃)) + 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 } @@ -757,8 +799,10 @@ -- 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 ≡ black-depth (child-replaced key tree) → RBI-state key tree repl + rebuild : {tree repl : bt (Color ∧ A) } → black-depth repl ≡ black-depth (child-replaced key tree) + → RBI-state key tree repl -- one stage up + rotate : {tree repl : bt (Color ∧ A) } → color repl ≡ Red → black-depth repl ≡ black-depth (child-replaced key tree) + → RBI-state key tree repl -- two stages up record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) : Set n where field