# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1717489773 -32400
# Node ID 4d379ebc53c8148006ca37ac341d82d26446ca3c
# Parent  1d34a752add0c3f079c29cbbf2b72eccba45fe43
...

diff -r 1d34a752add0 -r 4d379ebc53c8 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Tue Jun 04 11:30:20 2024 +0900
+++ b/hoareBinaryTree1.agda	Tue Jun 04 17:29:33 2024 +0900
@@ -1731,30 +1731,67 @@
  → (stack : List (bt (Color ∧ A)))
  → stackInvariant key tree1 tree0 stack
  → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) 
- → (exit : (r : RBI key value tree0 stack ) → t ) → t
+ → (exit : (stack : List ( bt (Color ∧ A))) (r : RBI key value tree0 stack ) → t ) → t
 replaceRBTNode {n} {m} {A}  {t} key value orig rbi ti leaf stack si (case1 refl) exit with stackToPG leaf orig stack si
 ... | case1 x = ?
 ... | case2 (case1 x) = ?
 ... | case2 (case2 pg) = rp00 where
-   buildCase : t
-   buildCase = ?
-   rotateCase : t
-   rotateCase = exit record {
-         tree = ?
-       ; repl = ?
-       ; origti = ti
-       ; origrb = rbi
-       ; treerb = ?
-       ; replrb = ?
-       ; si = ?
-       ; state = rotate ? ? ? ? }
+   rb00 : stackInvariant key leaf orig (leaf ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
+   rb00 = subst (λ k → stackInvariant key leaf orig k) (PG.stack=gp pg) si
+   treerb :  RBtreeInvariant (PG.parent pg)
+   treerb = PGtoRBinvariant1 _ orig rbi _ (popStackInvariant _ _ _ _ _ rb00)
+   pti : treeInvariant (PG.parent pg)
+   pti = siToTreeinvariant _ _ _ _ ti (popStackInvariant _ _ _ _ _ rb00)
    rp00 : t
    rp00 with PG.pg pg
-   ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ?
-   ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
-   ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
-   ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
-replaceRBTNode {n} {m} {A}  key value orig rbi ti tree@(node key₁ value₁ left right) stack si (case2 P) exit = exit record {
+   ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ with proj1 vp in pcolor
+   ... | Red = rotateCase1 where
+       rotateCase1 : t
+       rotateCase1 = exit (PG.grand pg ∷ PG.rest pg) record {
+             tree = PG.grand pg
+           ; repl = to-red ( node kg vg (to-black (node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1)) n2 )
+           ; origti = ti
+           ; origrb = rbi
+           ; treerb = PGtoRBinvariant1 _ orig rbi _ (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))
+           ; replrb = rb-red _ ? ? ? ? ? ? 
+           ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
+           ; state = rotate ? ? ? ? }
+   ... | Black = buildCase1 where
+       rb01 : bt (Color ∧ A)
+       rb01 = node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1
+       rb03 : 1 ≡ black-depth n1
+       rb03 = RBtreeEQ (subst (λ k → RBtreeInvariant k) x treerb)
+       rb02 : RBtreeInvariant (node kp ⟪ Black , proj2 vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) n1)
+       rb02 = rb-black kp (proj2 vp) rb03 (rb-red _ _ refl refl refl rb-leaf rb-leaf) (RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x treerb))
+       rb04 : proj1 vp ≡ Black → ⟪ Black , proj2 vp ⟫ ≡ vp
+       rb04 refl = refl
+       rb05 : black-depth rb01 ≡ black-depth (PG.parent pg)
+       rb05 = begin 
+           black-depth (node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1) ≡⟨ cong (λ k → black-depth (node kp k _ n1)) (sym (rb04 pcolor)) ⟩
+           black-depth (node kp ⟪ Black , proj2 vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) n1) ≡⟨ refl  ⟩
+           black-depth (node kp ⟪ Black , proj2 vp ⟫  leaf n1 )  ≡⟨ cong (λ k → black-depth (node kp k leaf n1)) (rb04 pcolor) ⟩
+           black-depth (node kp vp leaf n1)  ≡⟨ cong black-depth (sym x)  ⟩
+           black-depth (PG.parent pg) ∎ where 
+              open ≡-Reasoning
+       rb07 : key < kp
+       rb07 = si-property-<  ? (subst (λ k → treeInvariant k) x pti) (subst₂ (λ j k → stackInvariant key j orig k) refl (trans (PG.stack=gp pg) ? ) si)
+       rb06 : replacedRBTree key value (PG.parent pg) (node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1)
+       rb06 = subst₂ (λ j k → replacedRBTree key value k  (node kp j (node key ⟪ Red , value ⟫ leaf leaf) n1)) (rb04 pcolor) 
+           (trans (cong (λ k → node kp k leaf n1) (rb04 pcolor)) (sym x)) ( rbr-black-left refl rb07 rbr-leaf )
+       buildCase1 : t
+       buildCase1 = exit (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
+             tree = PG.parent pg
+           ; repl = rb01
+           ; origti = ti
+           ; origrb = rbi
+           ; treerb = PGtoRBinvariant1 _ orig rbi _ (popStackInvariant _ _ _ _ _ rb00)
+           ; replrb = subst (λ k → RBtreeInvariant k) (cong (λ k → node kp k (node key ⟪ Red , value ⟫ leaf leaf) n1) (rb04 pcolor))  rb02
+           ; si = popStackInvariant _ _ _ _ _ rb00
+           ; state = rebuild  (cong color x) rb05 rb06 } 
+   rp00 | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
+   rp00 | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
+   rp00 | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
+replaceRBTNode {n} {m} {A}  key value orig rbi ti tree@(node key₁ value₁ left right) stack si (case2 P) exit = exit ? record {
      tree = tree
    ; repl = node key₁ ⟪ proj1 value₁ , value ⟫ left right
    ; origti = ti