Mercurial > hg > Gears > GearsAgda

changeset 833:9ec2b7f8e5a7

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 Sat, 16 Mar 2024 17:33:57 +0900
parents 01658441313e
children 195281ff1354
files hoareBinaryTree1.agda
diffstat 1 files changed, 39 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Thu Mar 14 18:14:41 2024 +0900
+++ b/hoareBinaryTree1.agda	Sat Mar 16 17:33:57 2024 +0900
@@ -144,6 +144,7 @@
 si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ _ _ _ si ) with  si-property1  si
 ... | refl = si-property-last key x t0 (x ∷ st)   si
 
+
 -- Diffkey : {n : Level} (A : Set n) (tree0 : bt A) → (key : ℕ) →  (tree : bt A) → (stack  : List (bt A)) → (si : stackInvariant key tree tree0 stack) → Set
 -- Diffkey A leaf key .leaf .(leaf ∷ []) s-nil = ?
 -- Diffkey A (node key₁ value tree0 tree1) key .(node key₁ value tree0 tree1) .(node key₁ value tree0 tree1 ∷ []) s-nil = ?
@@ -874,6 +875,44 @@
        rotated : replacedRBTree key value tree repl
        state : RBI-state key tree repl
 
+tr>-to-black : {n : Level} {A : Set n} {key : ℕ} {tree : bt (Color ∧ A)} → tr> key tree → tr> key (to-black tree)
+tr>-to-black {n} {A} {key} {leaf} tr = tt
+tr>-to-black {n} {A} {key} {node key₁ value tree tree₁} tr = tr
+
+RB-repl→ti>  : {n : Level} {A : Set n}  → (tree repl : bt (Color ∧ A)) → (key key₁ : ℕ) → (value : A) 
+     → 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 _ ⟪ _ , _ ⟫ _ _) .(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 
+   = ⟪ proj1 tr , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫
+RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-right x rbt) lt tr 
+   = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti> _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫
+RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-left x rbt) lt tr 
+   = ⟪ proj1 tr , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫
+RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value (rbr-flip-ll x rbt) lt tr 
+   = ⟪ 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 ⟫ ⟫
+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 ⟫ ⟫   ⟫ ⟫
+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 
+   (rbr-rotate-ll x rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5  ⟫ ⟫  = ⟪ tr4 , ⟪  RB-repl→ti> _ _ _ _ _ rbt lt tr6 , ⟪ tr3 , ⟪ tr7 , tr5 ⟫ ⟫ ⟫ ⟫
+RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key key₁ value 
+   (rbr-rotate-rr x rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫  ⟫ ⟫  = ⟪ tr4 , ⟪ ⟪ tr3 , ⟪ tr5 , tr6 ⟫ ⟫ , RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫
+RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value 
+   (rbr-rotate-lr rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5  ⟫ ⟫  = ⟪ ? , ⟪ ? , ⟪ tr3 , ⟪ ? , tr5 ⟫ ⟫ ⟫ ⟫
+RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value 
+   (rbr-rotate-rl rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫  ⟫ ⟫  = ⟪ ? , ⟪  ? , ⟪ ? , ⟪ ? , ? ⟫ ⟫ ⟫ ⟫
+
+RB-repl→ti : {n : Level} {A : Set n} → {key : ℕ } → {value : A} → {tree repl : bt (Color ∧ A) } 
+     → treeInvariant tree → replacedRBTree key value tree repl → treeInvariant repl
+RB-repl→ti = ?
+
 --
 -- if we consider tree invariant, this may be much simpler and faster
 --