Mercurial > hg > Gears > GearsAgda

changeset 850:8647f4c5797c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 29 Mar 2024 16:14:32 +0900
parents 71d06dae15a4
children ea0f5b8a3567
files hoareBinaryTree1.agda
diffstat 1 files changed, 27 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Thu Mar 28 09:44:27 2024 +0900
+++ b/hoareBinaryTree1.agda	Fri Mar 29 16:14:32 2024 +0900
@@ -803,15 +803,15 @@
          → 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 →  key < kp → replacedRBTree key value t₁ t₂
+         → color t₂ ≡ Red →  kp < key → key < kg   → 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 → kp < key → replacedRBTree key value t₁ t₂
+         → color t₂ ≡ Red → kg < key → key < kp  → 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 → kp < key   → replacedRBTree key value t₁ t₂
+         → color t₂ ≡ Red → kg < key   → 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₂))
 
@@ -824,7 +824,7 @@
          → 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₂ )
-    -- case56 the node is inner, make it router and rotate grand
+    -- case56 the node is inner, make it outer and rotate grand
     rbr-rotate-lr : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A}
          → replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃)
          → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁)     uncle)
@@ -903,9 +903,9 @@
    = ⟪ proj1 tr , ⟪ ⟪ proj1 (proj1 (proj2 tr))  , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt (proj1 (proj2 (proj1 (proj2 tr))))
        , proj2 (proj2 (proj1 (proj2 tr))) ⟫ ⟫  , tr>-to-black (proj2 (proj2 tr)) ⟫ ⟫
 RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value
-   (rbr-flip-lr x _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫  , tr>-to-black tr5 ⟫ ⟫
+   (rbr-flip-lr x _ _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫  , tr>-to-black tr5 ⟫ ⟫
 RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value
-   (rbr-flip-rl x _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫  ⟫ ⟫ = ⟪ tr3 , ⟪ tr>-to-black tr5 , ⟪ tr4 , ⟪  RB-repl→ti> _ _ _ _ _ rbt lt tr6 , tr7 ⟫ ⟫   ⟫ ⟫
+   (rbr-flip-rl x _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫  ⟫ ⟫ = ⟪ tr3 , ⟪ tr>-to-black tr5 , ⟪ tr4 , ⟪  RB-repl→ti> _ _ _ _ _ rbt lt tr6 , tr7 ⟫ ⟫   ⟫ ⟫
 RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value
    (rbr-flip-rr x _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr>-to-black tr5 , ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫   ⟫ ⟫
 RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value
@@ -941,9 +941,9 @@
    = ⟪ proj1 tr , ⟪ ⟪ proj1 (proj1 (proj2 tr))  , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt (proj1 (proj2 (proj1 (proj2 tr))))
        , proj2 (proj2 (proj1 (proj2 tr))) ⟫ ⟫  , tr<-to-black (proj2 (proj2 tr)) ⟫ ⟫
 RB-repl→ti< .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value
-   (rbr-flip-lr x _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫  , tr<-to-black tr5 ⟫ ⟫
+   (rbr-flip-lr x _ _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫  , tr<-to-black tr5 ⟫ ⟫
 RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value
-   (rbr-flip-rl x _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫  ⟫ ⟫ = ⟪ tr3 , ⟪ tr<-to-black tr5 , ⟪ tr4 , ⟪  RB-repl→ti< _ _ _ _ _ rbt lt tr6 , tr7 ⟫ ⟫   ⟫ ⟫
+   (rbr-flip-rl x _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫  ⟫ ⟫ = ⟪ tr3 , ⟪ tr<-to-black tr5 , ⟪ tr4 , ⟪  RB-repl→ti< _ _ _ _ _ rbt lt tr6 , tr7 ⟫ ⟫   ⟫ ⟫
 RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value
    (rbr-flip-rr x _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr<-to-black tr5 , ⟪ tr4 , ⟪ tr6 ,  RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫   ⟫ ⟫
 RB-repl→ti< .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value
@@ -1045,9 +1045,25 @@
         rr00 = RB-repl→ti< _ _ _ _ _ trb (<-trans lt x₁) x₂
         rr02 : treeInvariant (node key₁ ⟪ Red , value₂  ⟫ t t₁)
         rr02 = RB-repl→ti _ _ _ _ ti (rbr-left lt trb)
-RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ t₁) (node key₃ _ _ _)) (node key₂ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ t t₁) .(to-black (node key₃ _ _ _))) key value (t-node _ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-ll x lt trb) = ?
-RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key value ti (rbr-flip-lr x lt trb) = ?
-RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key value ti (rbr-flip-rl x lt trb) = ?
+RB-repl→ti (node key₂ ⟪ Black , _ ⟫ (node key₁ ⟪ Red , _ ⟫ t₀ t₁) (node key₃ ⟪ c1 , v1 ⟫  left right)) (node key₂ ⟪ Red , value₁ ⟫ (node _ ⟪ Black , value₂ ⟫ t t₁) (node key₃ ⟪ Black , v1 ⟫  left  right)) key value 
+       (t-node _ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-ll x lt trb) = t-node _ _ _ x₁ x₂ rr00 x₄ x₅ x₆ (RTtoTI0 _ _ _ _ rr02 r-node ) (RTtoTI0 _ _ _ _ ti₁ r-node ) where
+        rr00 : tr< key₂ t
+        rr00 = RB-repl→ti< _ _ _ _ _ trb (<-trans lt x₁)  x₃
+        rr02 : treeInvariant (node key₁ ⟪ Red , value₂ ⟫ t t₁)
+        rr02  = RB-repl→ti _ _ _ _ ti (rbr-left lt trb)
+RB-repl→ti (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ left right) leaf) (node key₂ ⟪ Red , v1 ⟫ (node key₃ ⟪ Black , v2 ⟫ left right₁) leaf) key value 
+      (t-left _ _ x₁ x₂ x₃ ti) (rbr-flip-lr x lt lt2 trb) = t-left _ _ x₁ x₂ rr00 (RTtoTI0 _ _ _ _ rr02 r-node ) where
+        rr00 : tr< key₂ right₁
+        rr00 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃
+        rr02 : treeInvariant (node key₃ ⟪ Red , v2 ⟫ left right₁ )
+        rr02 = RB-repl→ti _ _ _ _ ti (rbr-right lt trb)
+RB-repl→ti (node key₁ ⟪ Black , v1 ⟫ (node key₂ ⟪ Red , v2 ⟫ t t₁) (node key₃ ⟪ c3 , v3 ⟫ t₂ t₃)) (node key₁ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ t t₄) .(to-black (node key₃ ⟪ c3 , _ ⟫ _ _))) key value 
+      (t-node _ _ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-flip-lr x lt lt2 trb) = t-node _ _ _ x₁ x₂ x₄ rr00 x₅ x₆ (RTtoTI0 _ _ _ _ rr02 r-node ) (RTtoTI0 _ _ _ _ ti₁ r-node ) where
+        rr00 : tr< key₁ t₄
+        rr00 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃
+        rr02 : treeInvariant (node key₂ ⟪ Red , v2 ⟫ t t₄)
+        rr02 = RB-repl→ti _ _ _ _ ti (rbr-right lt trb)
+RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key value ti (rbr-flip-rl x lt lt2 trb) = ?
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key value ti (rbr-flip-rr x lt trb) = ?
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) key value ti (rbr-rotate-ll x trb) = ?
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key value ti (rbr-rotate-rr x trb) = ?