# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1706093532 -32400
# Node ID dfa764ddced2c3068980398148e46ab65501d1cf
# Parent  a16f0b2ce509f4911b72de674212d39c2692afd9
reached to insertCase5

diff -r a16f0b2ce509 -r dfa764ddced2 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Wed Jan 24 12:35:05 2024 +0900
+++ b/hoareBinaryTree1.agda	Wed Jan 24 19:52:12 2024 +0900
@@ -750,7 +750,7 @@
 
 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
+   rotate  : {tree repl : bt (Color ∧ A) } → color repl ≡ Red → black-depth repl ≡ 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
@@ -945,38 +945,11 @@
 ... | rotate repl-red pbdeth< with stackToPG (RBI.tree r) orig stack (RBI.si r)
 ... | case1 eq  = exit repl stack eq r     -- no stack, replace top node
 ... | case2 (case1 eq) = insertCase12 orig refl (RBI.si r)  where
-    insertCase2 : (tree parent uncle grand : bt (Color ∧ A))
-      → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack )
-      → (pg : ParentGrand tree parent uncle grand ) → t
-    insertCase2 tree leaf uncle grand stack si (s2-s1p2 () x₁)
-    insertCase2 tree leaf uncle grand stack si (s2-1sp2 () x₁)
-    insertCase2 tree leaf uncle grand stack si (s2-s12p () x₁)
-    insertCase2 tree leaf uncle grand stack si (s2-1s2p () x₁)
-    insertCase2 tree parent@(node kp ⟪ Red , _ ⟫ _ _) uncle grand stack si pg = {!!} -- next {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
-    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) leaf grand stack si pg = {!!}
-    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Red , _ ⟫ _ _ ) grand stack si pg = {!!} -- next {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
-    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s1p2 x x₁) = {!!}
-          -- insertCase5 key value orig tree {!!} rbio {!!} {!!} stack si {!!} ri {!!} {!!} next exit
-      -- tree is left of parent, parent is left of grand
-      --  node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp tree n1
-      --  grand ≡ node kg vg (node kp ⟪ Black , proj3 ⟫ left right) (node ku ⟪ Black , proj4 ⟫ left₁ right₁)
-    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1sp2 x x₁) = {!!}
-          -- rotateLeft key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!}
-          --   (λ a b c d e f h i j k l m  → insertCase5 key value a b c d {!!} {!!} h i j k l {!!} {!!} next exit ) exit
-      -- tree is right of parent, parent is left of grand  rotateLeft
-      --  node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree
-      --  grand ≡ node kg vg (node kp ⟪ Black , proj3 ⟫ left right) (node ku ⟪ Black , proj4 ⟫ left₁ right₁)
-    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s12p x x₁) = {!!}
-          -- rotateRight key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!}
-          --    (λ a b c d e f h i j k l m  → insertCase5 key value a b c d {!!} {!!} h i j k l {!!} {!!} next exit ) exit
-      -- tree is left of parent, parent is right of grand, rotateRight
-      -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp tree n1
-      --  grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
-    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1s2p x x₁) = {!!}
-          -- insertCase5 key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} next exit
-      -- tree is right of parent, parent is right of grand
-      -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree
-      -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
+    --
+    -- we have no grand parent
+    -- eq : stack₁ ≡ RBI.tree r ∷ orig ∷ []
+    -- change parent color ≡ Black and exit 
+    -- 
     -- one level stack, orig is parent of repl
     rb01 : stackInvariant key (RBI.tree r) orig stack
     rb01 = RBI.si r
@@ -994,20 +967,7 @@
        rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl with si-property1 si
        ... | refl = ⊥-elim ( nat-<> x a  )
     ... | tri≈ ¬a b ¬c = {!!} -- can't happen
-    ... | tri> ¬a ¬b c = insertCase13 value₁ refl where
-       --
-       --    orig B
-       --    /  \
-       -- left   tree → rot → repl R
-       --
-       --     B  =>   B             B      =>         B
-       --    / \     / \           / \    rotate L   / \
-       --   L   L1  L   R3        L   R  -- bad     B   B
-       --              / \           / \               / \      1 : child-replace
-       ---            L   L2        L   B             L   L     2:  child-replace ( unbalanced )
-       --                              / \                      3:  child-replace ( rotated / balanced )
-       --                             L   L  
-       -- 
+    ... | tri> ¬a ¬b c = insertCase13 value₁ refl pbdeth< where
        rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → right ≡ RBI.tree r
        rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl = refl
        rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x si) refl refl with si-property1 si
@@ -1015,8 +975,11 @@
        --
        --  RBI key value (node key₁ ⟪ Black , value₄ ⟫ left right) repl stack
        --
-       insertCase13 : (v : Color ∧ A ) → v ≡ value₁ → t
-       insertCase13 ⟪ Black , value₄ ⟫ refl = exit (node key₁ ⟪ Black , value₄ ⟫ left repl) (orig ∷ [])  refl record {
+       insertCase13 : (v : Color ∧ A ) → v ≡ value₁ → black-depth repl ≡ black-depth (child-replaced key (RBI.tree r)) → t
+       insertCase13 ⟪ Black , value₄ ⟫ refl beq with <-cmp key key₁ | child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left right) in creq
+       ... | tri< a ¬b ¬c | cr = ⊥-elim (¬c c)
+       ... | tri≈ ¬a b ¬c | cr = ⊥-elim (¬c c)
+       ... | tri> ¬a ¬b c | cr = exit (node key₁ ⟪ Black , value₄ ⟫ left repl) (orig ∷ [])  refl record {
          tree = orig 
          ; origti = RBI.origti r
          ; origrb = RBI.origrb r
@@ -1025,7 +988,7 @@
          ; si = s-nil
          ; rotated = ?
          ; ri = ?
-         ; state = ?
+         ; state = rebuild ? 
          } 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))
@@ -1035,17 +998,11 @@
            tkey : {n : Level} {A : Set n } → (rbt : bt (Color ∧ A)) → ℕ
            tkey (node key value t t2) = key
            tkey leaf = {!!} -- key is none
-           rb051 : {n : Level} {A : Set n} {key key1 : ℕ } {value : A} {t t1 t2 : bt (Color ∧ A)} {c : Color} → replacedTree key ⟪ ? , value ⟫ (node key1 ⟪ c , value ⟫ t1 t2) (node key1 ⟪ c , value ⟫ t1 t) → key1 < key
-           rb051 = {!!}
-           rb052 : {key key₁ : ℕ} → stackInvariant key (RBI.tree r) orig stack → key < key₁
-           rb052 = {!!}
-       insertCase13 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r)
-       ... | Black = exit {!!} {!!} {!!} {!!} 
-       ... | Red = exit {!!} {!!} {!!} {!!}
-       --       r = orig                            RBI.tree b
-       --      / \                       =>         /    \
-       --     b   b → r RBI.tree r             r = orig   o (r/b)
-... | case2 (case2 pg) = {!!} -- insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)
+       insertCase13 ⟪ Red , value₄ ⟫ eq beq = ? -- can't happen
+... | case2 (case2 pg) with PG.uncle pg
+... | leaf = ? -- insertCase5 
+... | node key₁ ⟪ Black , value₁ ⟫ t₁ t₂ = ? -- insertCase5
+... | node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ = next ? ? ? ?   -- going to two level up