Mercurial > hg > Gears > GearsAgda

changeset 848:ad97032da3c8

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 Thu, 28 Mar 2024 09:28:57 +0900
parents 045dd0e43c56
children 71d06dae15a4
files hoareBinaryTree1.agda
diffstat 1 files changed, 3 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Wed Mar 27 23:30:49 2024 +0900
+++ b/hoareBinaryTree1.agda	Thu Mar 28 09:28:57 2024 +0900
@@ -785,7 +785,6 @@
     -- 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-to-black : {value₁ : A} → {t t₁ : bt (Color ∧ A)} → replacedRBTree key value (node key ⟪ Red , value₁ ⟫ t t₁) (node key ⟪ Black , 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)}
@@ -892,7 +891,6 @@
      → replacedRBTree key value tree repl → key₁ < key → tr> key₁ tree → tr> key₁ repl
 RB-repl→ti> .leaf .(node key ⟪ Red , value ⟫ leaf leaf) key key₁ value rbr-leaf lt tr = ⟪ lt , ⟪ tt , tt ⟫ ⟫
 RB-repl→ti> .(node key ⟪ _ , _ ⟫ _ _) .(node key ⟪ _ , value ⟫ _ _) key key₁ value rbr-node lt tr = tr
-RB-repl→ti> .(node key ⟪ _ , _ ⟫ _ _) .(node key ⟪ _ , value ⟫ _ _) key key₁ value rbr-to-black lt tr = tr
 RB-repl→ti> .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-right x rbt) lt tr
    = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti> _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫
 RB-repl→ti> .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-left x rbt) lt tr
@@ -931,7 +929,6 @@
      → replacedRBTree key value tree repl → key < key₁ → tr< key₁ tree → tr< key₁ repl
 RB-repl→ti< .leaf .(node key ⟪ Red , value ⟫ leaf leaf) key key₁ value rbr-leaf lt tr = ⟪ lt , ⟪ tt , tt ⟫ ⟫
 RB-repl→ti< .(node key ⟪ _ , _ ⟫ _ _) .(node key ⟪ _ , value ⟫ _ _) key key₁ value rbr-node lt tr = tr
-RB-repl→ti< .(node key ⟪ _ , _ ⟫ _ _) .(node key ⟪ _ , value ⟫ _ _) key key₁ value rbr-to-black lt tr = tr
 RB-repl→ti< .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-right x rbt) lt tr
    = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti< _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫
 RB-repl→ti< .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-left x rbt) lt tr
@@ -1042,13 +1039,11 @@
      (t-node key₁ .key₂ key₃ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (rbr-black-left x x₇ trb) = t-node _ _ _ (proj1 rr00) x₂ (proj1 (proj2 rr00)) (proj2 (proj2 rr00)) x₅ x₆ (RB-repl→ti _ _ _ _ ti trb) ti₁ where
         rr00 : (key₄ < key₂) ∧ tr< key₂ t ∧ tr< key₂ t₁
         rr00 = RB-repl→ti< _ _ _ _ _ trb x₇ ⟪ x₁ , ⟪ x₃ , x₄ ⟫ ⟫
-RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ t₁) leaf) (node key₂ ⟪ Red , value₁ ⟫ (node key₁ ⟪ Black , _ ⟫ t t₁) .(to-black leaf)) key value 
-      (t-left _ .key₂ x₁ x₂ x₃ ti) (rbr-flip-ll x trb) = t-left _ _ x₁ rr00 x₃ ? where
+RB-repl→ti .(node key₂ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ t₁) leaf) (node key₂ ⟪ Red , value₁ ⟫ (node key₁ ⟪ Black , value₂ ⟫ t t₁) .(to-black leaf)) key value 
+      (t-left _ .key₂ x₁ x₂ x₃ ti) (rbr-flip-ll x trb) = t-left _ _ x₁ rr00 x₃ (RTtoTI0 _ _ _ _ rr02 r-node ) where
         rr00 : tr< key₂ t 
         rr00 = RB-repl→ti< _ _ _ _ _ trb ? x₂
-        rr01 : replacedRBTree ? ? (node key₁ ⟪ Red , ? ⟫ ? t₁) (node key₁ ⟪ Black , ? ⟫ t t₁)
-        rr01 = ?
-        rr02 : treeInvariant (node key₁ ⟪ Red , ?  ⟫ t t₁)
+        rr02 : treeInvariant (node key₁ ⟪ Red , value₂  ⟫ t t₁)
         rr02 = RB-repl→ti _ _ _ _ ti (rbr-left ? 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 trb) = ?
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key value ti (rbr-flip-lr x trb) = ?
@@ -1058,7 +1053,6 @@
 RB-repl→ti .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key value ti (rbr-rotate-rr x trb) = ?
 RB-repl→ti .(node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) .(node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₂) (node kg ⟪ Red , _ ⟫ t₃ _)) key value ti (rbr-rotate-lr t₂ t₃ kg kp kn trb) = ?
 RB-repl→ti .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ t₃ _)) key value ti (rbr-rotate-rl t₂ t₃ kg kp kn trb) = ?
-RB-repl→ti .(node key ⟪ Red , _ ⟫ _ _) .(node key ⟪ Black , value ⟫ _ _) key value ti rbr-to-black = ?
 
 --
 -- if we consider tree invariant, this may be much simpler and faster