# HG changeset patch
# User Moririn
# Date 1702101441 -32400
# Node ID 0eee181bd7155e125fb5904a3aecda611a1fa9bd
# Parent  6f27c2c180356d46cd935a49eb6a45ab1962fdac
...

diff -r 6f27c2c18035 -r 0eee181bd715 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Mon Dec 04 18:05:05 2023 +0900
+++ b/hoareBinaryTree1.agda	Sat Dec 09 14:57:21 2023 +0900
@@ -563,8 +563,7 @@
 ... | tri< a ¬b ¬c = ⊥-elim (¬b (DepthCal (suc l) (suc m) zero ))
 ... | tri≈ ¬a b ¬c = cong suc (suc-injective b)
 ... | tri> ¬a ¬b c = ⊥-elim (¬b (DepthCal (suc l) (suc m) zero ))
-DepthCal (suc l) (suc m) (suc n) = cong suc (DepthCal l m n ) 
-
+DepthCal (suc l) (suc m) (suc n) = cong suc (DepthCal l m n )
 
 data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where
     rb-leaf : RBtreeInvariant leaf
@@ -683,6 +682,19 @@
  = next right (right ∷ stack) ⟪ treeRightDown left right (_∧_.proj1 ti), s-right _ _ _ c (_∧_.proj2 ti) ⟫ (RBtreeRightDown left right rb0) depth-2<
 
 
+blackdepth≡ : {n : Level } {A : Set n} → {C : Color} {key key1 : ℕ} {value value1 : 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≡ {n} {A}  leaf (node key .(⟪ Black , _ ⟫) t2 t3) ri1 ri2 (rb-right-red x x₁ rip) = DepthCal (black-depth {n} {A} leaf) (black-depth (node key ⟪ Black , _ ⟫ t2 t3)) 0
+blackdepth≡ {n} {A} leaf (node key .(⟪ _ , _ ⟫) t2 t3) ri1 ri2 (rb-right-black x x₁ rip) = DepthCal (black-depth {n} {A} leaf) (black-depth (node key ⟪ _ , _ ⟫ t2 t3) ) (black-depth (node key ⟪ _ , _ ⟫ t2 t3))
+blackdepth≡ {n} {A} (node key .(⟪ Black , _ ⟫) t1 t3) leaf ri1 ri2 (rb-left-red x x₁ rip) = DepthCal (black-depth (node key ⟪ Black , _ ⟫ t1 t3))  (black-depth {n} {A} leaf)  0
+blackdepth≡ {n} {A} (node key .(⟪ _ , _ ⟫) t1 t3) leaf ri1 ri2 (rb-left-black x x₁ rip) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) (black-depth {n} {A} leaf) 0
+blackdepth≡ (node key .(⟪ Black , _ ⟫) t1 t3) (node key₁ .(⟪ Black , _ ⟫) t2 t4) ri1 ri2 (rb-node-red x x₁ x₂ rip x₃ rip₁) = DepthCal (black-depth  (node key ⟪ Black , _ ⟫ t1 t3)) (black-depth (node key₁ ⟪ Black , _ ⟫ t2 t4)) 0
+blackdepth≡ (node key .(⟪ _ , _ ⟫) t1 t3) (node key₁ .(⟪ _ , _ ⟫) t2 t4) ri1 ri2 (rb-node-black x x₁ x₂ rip x₃ rip₁) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) ( black-depth (node key₁ ⟪ _ , _ ⟫ t2 t4))  (black-depth (node key₁ (⟪ _ , _ ⟫) t2 t4))
+
 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₁)
@@ -952,20 +964,24 @@
                 → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key1 ⟪ Black , value1 ⟫ t1 t2))
                 → key < key1 
                rb09 (rb-right-red x x1 x2) = x
-               -- rb05 should more general     
+               -- rb05 should more general
+               inkey : {n : Level} {A : Set n } → (rbt : bt (Color ∧ A)) → ℕ
+               inkey (node key value t t2) = key  
                rb05 : RBtreeInvariant (node key₁ ⟪ Red , value₄ ⟫ left repl) ∧  replacedRBTree key value
                     (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) (node key₁ ⟪ Red , value₄ ⟫ left repl)
-               rb05 with RBI.origrb r | rb04 si eq refl | RBI.replrb r in eqrepl 
-               ... | rb-single key₂ value₂ | refl | rb-single key value = ⟪ rb-right-red (rb09 (proj1 rb05)) refl (RBI.replrb r) , {!!} ⟫
-               ... | rb-single key₂ value₂ | refl | rb-right-red x x₁ rb = {!!} -- cant happen ? red - red
-               ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb = {!!} --⟪ rb-right-red {!!} {!!} (RBI.replrb r) , {!!}  ⟫ -- if c₁ is Black , Cant happen . Red-leaf-leaf
-               ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb = {!!} --red -red
-               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb = ⟪ rb-right-red (rb09 (proj1 rb05)) {!!} (RBI.replrb r) , {!!} ⟫ -- if c₁ is Black , Cant happen . Red-leaf-leaf
-               ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb x₃ rb₁ = {!!}-- red -red
-               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ = ⟪ rb-right-red (rb09 (proj1 rb05)) {!!} {!!} , {!!} ⟫
-               ... | rb-right-black x x₁ t | refl | rb = ⟪ proj1 {!!} , {!!} ⟫
-               ... | rb-left-black x x₁ t | refl | rb = {!!} --⟪ rb-node-red ? ? ? ? ? ? , ? ⟫
-               ... | rb-node-black x x₁ x₂ t x₃ t₁ | refl | rb = {!!}
+               rb05 with RBI.origrb r | rb04 si eq refl | RBI.replrb r in eqrepl | <-cmp (inkey orig) (inkey repl)
+               ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri< a ¬b ¬c = ⟪ rb-right-red a refl (RBI.replrb r) , {!!} ⟫
+               ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri≈ ¬a b ¬c = {!!} -- key is unique
+               ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri> ¬a ¬b c = ⊥-elim (¬a {!!})
+               ... | rb-single key₂ value₂ | refl | rb-right-red x x₁ rb | t = {!!} -- cant happen ? red - red
+               ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | t = {!!} --⟪ rb-right-red {!!} {!!} (RBI.replrb r) , {!!}  ⟫ -- if c₁ is Black , need rotate . 
+               ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb | t = {!!} --red -red
+               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | t = {!!} --⟪ rb-right-red (rb09 (proj1 rb05)) ({!!}) (RBI.replrb r) , {!!} ⟫ -- if c₁ is Black , need rotate .
+               ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb x₃ rb₁ | t = {!!}-- red -red
+               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ | t = {!!} --⟪ rb-right-red (rb09 (proj1 rb05)) (DepthCal {!!} {!!} {!!}) {!!} , {!!} ⟫
+               --... | rb-right-black x x₁ t | refl | rb | t = ? --⟪ proj1 {!!} , {!!} ⟫
+               --... | rb-left-black x x₁ t | refl | rb | t = {!!} --⟪ rb-node-red ? ? ? ? ? ? , ? ⟫
+               --... | rb-node-black x x₁ x₂ t x₃ t₁ | refl | rb | t = {!!}
            insertCase13 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r)
            ... | Black = exit {!!} {!!} {!!} {!!} 
            ... | Red = exit {!!} {!!} {!!} {!!}
diff -r 6f27c2c18035 -r 0eee181bd715 work.agda
--- a/work.agda	Mon Dec 04 18:05:05 2023 +0900
+++ b/work.agda	Sat Dec 09 14:57:21 2023 +0900
@@ -374,6 +374,7 @@
 blackdepth≡ {n} {A} (node key .(⟪ _ , _ ⟫) t1 t3) leaf ri1 ri2 (rb-left-black x x₁ rip) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) (black-depth {n} {A} leaf) 0
 blackdepth≡ (node key .(⟪ Black , _ ⟫) t1 t3) (node key₁ .(⟪ Black , _ ⟫) t2 t4) ri1 ri2 (rb-node-red x x₁ x₂ rip x₃ rip₁) = DepthCal (black-depth  (node key ⟪ Black , _ ⟫ t1 t3)) (black-depth (node key₁ ⟪ Black , _ ⟫ t2 t4)) 0
 blackdepth≡ (node key .(⟪ _ , _ ⟫) t1 t3) (node key₁ .(⟪ _ , _ ⟫) t2 t4) ri1 ri2 (rb-node-black x x₁ x₂ rip x₃ rip₁) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) ( black-depth (node key₁ ⟪ _ , _ ⟫ t2 t4))  (black-depth (node key₁ (⟪ _ , _ ⟫) t2 t4))
+
 rb08 : {n : Level } {A : Set n}{key key1 : ℕ} {value value1 : A} {c c1 : Color} {t₁ t₂ t₃ t₄ : bt (Color ∧ A)}
  →  black-depth (node key ⟪ c , value ⟫ t₁ t₂) ≡ black-depth (node key1 ⟪ c1 , value1 ⟫ t₃ t₄)
 rb08 = {!!}