# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1715605158 -32400
# Node ID 5b6225b81409e1602d25bee03e83ba419d27452e
# Parent  e92daa8d617b47bdb293a8f24a69ce391c1d2b69
...

diff -r e92daa8d617b -r 5b6225b81409 hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Mon May 13 10:59:03 2024 +0900
+++ b/hoareBinaryTree1.agda	Mon May 13 21:59:18 2024 +0900
@@ -179,6 +179,13 @@
 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
 nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
 
+nat-<≡ : { x : ℕ } → x < x → ⊥
+nat-<≡  (s≤s lt) = nat-<≡ lt
+
+nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
+nat-≡< refl lt = nat-<≡ lt
+
+
 open _∧_
 
 
@@ -791,11 +798,11 @@
 data replacedRBTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt (Color ∧ A) ) → Set n where
     -- no rotation case
     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-node : {value₁ : A} → {ca ca1 : Color } → {t t₁ : bt (Color ∧ A)} → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ ca1 , value ⟫ t t₁)
+    rbr-right : {k : ℕ } {v1 : A} → {ca ca1 : 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 ⟪ ca1 , v1 ⟫ t1 t)
+    rbr-left  : {k : ℕ } {v1 : A} → {ca ca1 : 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 ⟪ ca1 , v1 ⟫ t t2) -- k < key → key < k
     -- case1 parent is black
     rbr-black-right : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ}
          → color t₂ ≡ Red → key₁ < key  → replacedRBTree key value t₁ t₂
@@ -982,7 +989,7 @@
    (t-left key₁ .key x x₁ x₂ ti) rbr-node = t-left key₁ key x x₁ x₂ ti
 RB-repl→ti .(node key ⟪ _ , _ ⟫ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key ⟪ _ , value ⟫ (node key₁ _ _ _) (node key₂ _ _ _)) key value 
    (t-node key₁ .key key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) rbr-node = t-node key₁ key key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁
-RB-repl→ti (node key₁ ⟪ ca , v1 ⟫ leaf leaf) (node key₁ ⟪ ca , v1 ⟫ leaf tree@(node key₂ value₁ t t₁)) key value 
+RB-repl→ti (node key₁ ⟪ ca , v1 ⟫ leaf leaf) (node key₁ ⟪ ca1 , v1 ⟫ leaf tree@(node key₂ value₁ t t₁)) key value 
    (t-single key₁ ⟪ ca , v1 ⟫) (rbr-right x trb) = t-right _ _  (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ t-leaf trb) where
         rr00 : (key₁ < key₂ ) ∧ tr> key₁ t ∧ tr> key₁ t₁
         rr00 = RB-repl→ti> _ _ _ _ _ trb x tt
@@ -990,11 +997,11 @@
    (t-right _ key₁ x₁ x₂ x₃ ti) (rbr-right x trb) = t-right _ _ (proj1 rr00) (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) (RB-repl→ti _ _ _ _ ti trb) where
         rr00 : (key₂ < key₃) ∧ tr> key₂ t ∧ tr> key₂ t₁ 
         rr00 = RB-repl→ti> _ _ _ _ _ trb x ⟪ x₁ , ⟪ x₂ , x₃ ⟫ ⟫
-RB-repl→ti .(node key₂ ⟪ ca , v1 ⟫ (node key₁ value₁ t t₁) leaf) (node key₂ ⟪ ca , v1 ⟫ (node key₁ value₁ t t₁) (node key₃ value₂ t₂ t₃)) key value 
+RB-repl→ti (node key₂ ⟪ ca , v1 ⟫ (node key₁ value₁ t t₁) leaf) (node key₂ ⟪ ca1 , v1 ⟫ (node key₁ value₁ t t₁) (node key₃ value₂ t₂ t₃)) key value 
    (t-left key₁ _ x₁ x₂ x₃ ti) (rbr-right x trb) = t-node _ _ _ x₁ (proj1 rr00) x₂ x₃ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ti (RB-repl→ti _ _ _ _ t-leaf trb) where
         rr00 : (key₂ < key₃) ∧ tr> key₂ t₂ ∧ tr> key₂ t₃
         rr00 = RB-repl→ti> _ _ _ _ _ trb x tt
-RB-repl→ti .(node key₃ ⟪ ca , v1 ⟫ (node key₁ v2 t₁ t₂) (node key₂ _ _ _)) (node key₃ ⟪ ca , v1 ⟫ (node key₁ v2 t₁ t₂) (node key₄ value₁ t₃ t₄)) key value 
+RB-repl→ti (node key₃ ⟪ ca , v1 ⟫ (node key₁ v2 t₁ t₂) (node key₂ _ _ _)) (node key₃ ⟪ ca1 , v1 ⟫ (node key₁ v2 t₁ t₂) (node key₄ value₁ t₃ t₄)) key value 
    (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-right x trb) = t-node _ _ _ x₁ 
      (proj1 rr00) x₃ x₄ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) ti (RB-repl→ti _ _ _ _ ti₁ trb) where
         rr00 : (key₃ < key₄) ∧ tr> key₃ t₃ ∧ tr> key₃ t₄
@@ -1201,7 +1208,7 @@
 RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ leaf leaf) .leaf) (node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ leaf) (node kg ⟪ Red , _ ⟫ leaf _)) .kn _ (t-left .kp .kg x x₁ x₂ ti) (rbr-rotate-lr .leaf .leaf kg kp kn lt1 lt2 rbr-leaf) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _)
 RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ (node key₁ value₁ t t₁) leaf) .leaf) (node kn ⟪ Black , v3 ⟫ (node kp ⟪ Red , _ ⟫ _ leaf) (node kg ⟪ Red , _ ⟫ leaf _)) .kn .v3 (t-left .kp .kg x x₁ x₂ (t-left .key₁ .kp x₃ x₄ x₅ ti)) (rbr-rotate-lr .leaf .leaf kg kp kn lt1 lt2 rbr-leaf) = 
     t-node _ _ _ lt1 lt2 ⟪ <-trans x₃ lt1  , ⟪ >-tr< x₄ lt1  , >-tr< x₅ lt1 ⟫ ⟫  tt tt tt (t-left _ _ x₃ x₄ x₅ ti) (t-single _ _) 
-RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .leaf (node key₁ .(⟪ Red , _ ⟫) .leaf .leaf)) .leaf) (node .key₁ ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ leaf) (node kg ⟪ Red , _ ⟫ leaf _)) .key₁ _ (t-left .kp .kg x x₁ x₂ (t-right .kp .key₁ x₃ x₄ x₅ ti)) (rbr-rotate-lr .leaf .leaf kg kp .key₁ lt1 lt2 rbr-node) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _) 
+RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .leaf (node key₁ (⟪ Red , _ ⟫) leaf leaf)) leaf) (node .key₁ ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ leaf) (node kg ⟪ Red , _ ⟫ leaf _)) .key₁ _ (t-left .kp .kg x x₁ x₂ (t-right .kp .key₁ x₃ x₄ x₅ ti)) (rbr-rotate-lr .leaf .leaf kg kp .key₁ lt1 lt2 rbr-node) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _) 
 RB-repl→ti (node kg ⟪ Black , v1 ⟫ (node kp ⟪ Red , v2 ⟫ .leaf (node key₁ value₁ t₁ t₂)) .leaf) (node kn ⟪ Black , value₃ ⟫ (node kp ⟪ Red , _ ⟫ _ leaf) (node kg ⟪ Red , _ ⟫ (node key₂ value₂ t₄ t₅) t₆)) key value (t-left .kp .kg x x₁ x₂ (t-right .kp .key₁ x₃ x₄ x₅ ti)) (rbr-rotate-lr .leaf .(node key₂ value₂ t₄ t₅) kg kp kn lt1 lt2 trb) = 
    t-node _ _ _ (proj1 rr00) (proj1 rr01) tt tt rr03 tt (t-single _ _) (t-left _ _ (proj1 rr02) (proj1 (proj2 rr02)) (proj2 (proj2 rr02)) (treeRightDown _ _ ( RB-repl→ti _ _ _ _ ti trb))) where
         rr00 : (kp < kn) ∧ ⊤ ∧ ((kp < key₂) ∧ tr> kp t₄ ∧ tr> kp t₅ )
@@ -1313,7 +1320,7 @@
         rr03 = proj1 (proj2 rr01)
         rr04 = proj2 (proj2 rr01)
 RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .leaf leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) .kn .vn (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 rbr-leaf) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _)
-RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node kn ⟪ Red , _ ⟫ leaf leaf) leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) .kn .vn (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 rbr-node) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _) 
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ (node kn ⟪ Red , _ ⟫ leaf leaf) leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) .kn .vn (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 rbr-node) = t-node _ _ _ lt1 lt2 tt tt tt tt (t-single _ _) (t-single _ _) 
 RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .leaf (node key₁ value₁ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) .kn .vn (t-right .kg .kp x x₁ x₂ (t-right .kp .key₁ x₃ x₄ x₅ ti)) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 rbr-leaf) = t-node _ _ _ lt1 lt2 tt tt tt ⟪ <-trans lt2 x₃ , ⟪ <-tr> x₄ lt2 , <-tr> x₅ lt2 ⟫ ⟫  (t-single _ _) (t-right _ _ x₃ x₄ x₅ ti) 
 RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ .(node key₂ _ _ _) (node key₁ value₁ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-right .kg .kp x x₁ x₂ (t-node key₂ .kp .key₁ x₃ x₄ x₅ x₆ x₇ x₈ ti ti₁)) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 trb) = t-node _ _ _ (proj1 rr00) (proj1 rr01) tt tt tt ⟪ <-trans (proj1 rr01) x₄ , ⟪ <-tr> x₇ (proj1 rr01) , <-tr> x₈ (proj1 rr01) ⟫ ⟫  (t-single _ _) (t-right _ _ x₄ x₇ x₈ ti₁) where
         rr00 : (kg < kn) ∧ ⊤ ∧ ⊤
@@ -1614,19 +1621,34 @@
        rb04 : {stack : List ( bt ( Color ∧ A))} → stack ≡ RBI.tree r ∷ orig ∷ [] → leaf ≡ orig → stackInvariant key (RBI.tree r) orig stack →   ⊥
        rb04  refl refl (s-right tree leaf tree₁ x si) = si-property2 _ (s-right tree leaf tree₁ x si) refl
        rb04  refl refl (s-left tree₁ leaf tree x si) = si-property2 _  (s-left tree₁ leaf tree x si) refl
-    insertCase12  tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁
-    ... | tri< a ¬b ¬c = {!!} where
+    insertCase12  tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ | child-replaced key (node key₁ value₁ left right) in creq
+    ... | tri< a ¬b ¬c | cr = exit (node key₁ ⟪ Black ,  proj2 value₁  ⟫ left right) (orig ∷ []) refl record {
+         tree = orig
+         ; origti = RBI.origti r
+         ; origrb = RBI.origrb r
+         ; treerb = RBI.origrb r
+         ; replrb = ?
+         ; si = s-nil
+         ; rotated = ?
+         ; state = rebuild ?
+         } where
        rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → left ≡ RBI.tree r
        rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x s-nil) refl refl = refl
        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 pbdeth< where
+    ... | tri≈ ¬a b ¬c | cr = ⊥-elim ( rb06 _ eq (RBI.si r) b ) where -- can't happen
+       rb06 : (stack    : List (bt (Color ∧ A))) → stack ≡ RBI.tree r ∷ node key₁ value₁ left right ∷ [] 
+         →  stackInvariant key (RBI.tree r) (node key₁ value₁ left right) stack
+         → key ≡ key₁
+         → ⊥
+       rb06 (.right ∷ node key₁ value₁ left right ∷ []) refl (s-right .right .(node key₁ value₁ left right) .left x s-nil) eq = ⊥-elim ( nat-≡< (sym eq) x)
+       rb06 (.left ∷ node key₁ value₁ left right ∷ []) refl (s-left .left .(node key₁ value₁ left right) .right x s-nil) eq = ⊥-elim ( nat-≡< eq x)
+    ... | tri> ¬a ¬b c | cr = 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
        ... | refl = ⊥-elim ( nat-<> x c  )
-       --
+       -- 
        --  RBI key value (node key₁ ⟪ Black , value₄ ⟫ left right) repl stack
        --
        insertCase13 : (v : Color ∧ A ) → v ≡ value₁ → black-depth repl ≡ black-depth (child-replaced key (RBI.tree r)) → t