Mercurial > hg > Gears > GearsAgda

changeset 814:82029d2a8970

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 Tue, 23 Jan 2024 15:33:18 +0900
parents 8dbddf72211e
children e22ebb0f00a3
files hoareBinaryTree1.agda
diffstat 1 files changed, 81 insertions(+), 64 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Jan 22 18:51:56 2024 +0900
+++ b/hoareBinaryTree1.agda	Tue Jan 23 15:33:18 2024 +0900
@@ -582,34 +582,34 @@
        → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)
        → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄))
 
-data rotatedTree {n : Level} {A : Set n} : (before after : bt A) → Set n where
-  rtt-unit : {t : bt A} → rotatedTree t t
-  rtt-node : {left left' right right' : bt A} → {ke : ℕ} {ve : A} → 
-      rotatedTree left left' → rotatedTree right right' → rotatedTree (node ke ve left right) (node ke ve left' right')
-  --     a              b
-  --   b   c          d   a
-  -- d   e              e   c
-  --
-  rtt-right : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A}
-    --kd < kb < ke < ka< kc
-   → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A}
-   → kd < kb → kb < ke → ke < ka → ka < kc
-   → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1)
-   → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1)
-   → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
-   → rotatedTree (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
-    (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
-
-  rtt-left : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A}
-    --kd < kb < ke < ka< kc
-   → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A} -- after child
-   → kd < kb → kb < ke → ke < ka → ka < kc
-   → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1)
-   → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1)
-   → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
-   → rotatedTree  (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
-   (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
-   
+-- data rotatedTree {n : Level} {A : Set n} : (before after : bt A) → Set n where
+--  rtt-unit : {t : bt A} → rotatedTree t t
+--  rtt-node : {left left' right right' : bt A} → {ke : ℕ} {ve : A} → 
+--      rotatedTree left left' → rotatedTree right right' → rotatedTree (node ke ve left right) (node ke ve left' right')
+--  --     a              b
+--  --   b   c          d   a
+--  -- d   e              e   c
+--  --
+--  rtt-right : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A}
+--    --kd < kb < ke < ka< kc
+--   → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A}
+--   → kd < kb → kb < ke → ke < ka → ka < kc
+--   → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1)
+--   → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1)
+--   → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
+--   → rotatedTree (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
+--    (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
+-- 
+--  rtt-left : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A}
+--    --kd < kb < ke < ka< kc
+--   → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A} -- after child
+--   → kd < kb → kb < ke → ke < ka → ka < kc
+--   → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1)
+--   → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1)
+--   → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1)
+--   → rotatedTree  (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1)))
+--   (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr))
+--   
 RightDown : {n : Level} {A : Set n} → bt (Color ∧ A) → bt (Color ∧ A)
 RightDown leaf = leaf
 RightDown (node key ⟪ c , value ⟫ t1 t2) = t2
@@ -651,6 +651,14 @@
 RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = tir
 RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til tir) = tir
 
+--
+--  findRBT exit with replaced node
+--     case-eq        node value is replaced,  just do replacedTree and rebuild rb-invariant
+--     case-leaf      insert new single node
+--        case1       if parent node is black, just do replacedTree and rebuild rb-invariant
+--        case2       if parent node is red,   increase blackdepth, do rotatation
+--
+
 findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) )
            → (stack : List (bt (Color ∧ A)))
            → RBtreeInvariant tree ∧  stackInvariant key tree tree0 stack
@@ -701,14 +709,15 @@
 findRBTreeTest = findTest 14 testRBTree0 testRBI0
        $ λ tr s P O → (record {tree = tr ; stack = s ; ti = (proj1 P) ; si = (proj2 P)})
 
--- we can re use replacedTree
--- data replacedRBTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt (Color ∧ A) ) → Set n where
---     rbr-leaf : {ca cb : Color} → replacedTree key value leaf (node key ⟪ cb , value ⟫ leaf leaf)
---     rbr-node : {value₁ : A} → {ca cb : Color } → {t t₁ : bt (Color ∧ A)} → replacedTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ cb , value ⟫ t t₁)
---     rbr-right : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
---           → k < key →  replacedTree key value t2 t →  replacedTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t1 t)
---     rbr-left : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)}
---           → key < k →  replacedTree key value t1 t →  replacedTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2) -- k < key → key < k 
+-- create replaceRBTree with rotate
+
+data replacedRBTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt (Color ∧ A) ) → Set n where
+    rbr-leaf : {ca cb : Color} → replacedRBTree key value leaf (node key ⟪ cb , value ⟫ leaf leaf)
+    rbr-node : {value₁ : A} → {ca cb : Color } → {t t₁ : bt (Color ∧ A)} → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ cb , value ⟫ t t₁)
+    rbr-right : {k : ℕ } {v1 : A} → {ca cb : 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 ⟪ cb , v1 ⟫ t1 t)
+    rbr-left : {k : ℕ } {v1 : A} → {ca cb : 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 ⟪ cb , v1 ⟫ t t2) -- k < key → key < k 
 
 data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent uncle grand : bt A) → Set n where
     s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A }
@@ -727,17 +736,25 @@
        rest : List (bt A)
        stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest )
 
+--
+-- RBI : Invariant on InsertCase2
+--     color repl ≡ Red ∧ black-depth repl ≡ suc (black-depth tree)
+--
+
+data RBI-state  {n : Level} {A : Set n} (key : ℕ) : (tree repl : bt (Color ∧ A) ) → Set n where
+   rebuild : {tree repl : bt (Color ∧ A) } → black-depth repl ≡ black-depth (child-replaced key tree) → RBI-state key tree repl
+   rotate  : {tree repl : bt (Color ∧ A) } → color repl ≡ Red → black-depth repl ≡ suc (black-depth (child-replaced key tree)) → RBI-state key tree repl
+
 record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A)))  : Set n where
    field
-       tree rot : bt (Color ∧ A)
+       tree : bt (Color ∧ A)
        origti : treeInvariant orig
        origrb : RBtreeInvariant orig
        treerb : RBtreeInvariant tree     -- tree node te be replaced
        replrb : RBtreeInvariant repl
        si : stackInvariant key tree orig stack
-       rotated : rotatedTree tree rot
-       ri : replacedTree key ⟪ Red   , value ⟫ (child-replaced key rot ) repl
-         ∨  replacedTree key ⟪ Black , value ⟫ (child-replaced key rot ) repl
+       rotated : replacedRBTree key value tree repl
+       state : RBI-state key tree repl
 
 stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A )
            →  (stack : List (bt A)) → stackInvariant key tree orig stack
@@ -854,7 +871,25 @@
     -- = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)
 
 
--- if we have replacedNode on RBTree, we have RBtreeInvariant
+--
+-- replaced node increase blackdepth, so we need tree rotate
+--
+-- case2 tree is Red         
+--
+--   go upward until
+--
+--   if root           
+--       insert top
+--   if unkle is leaf or Black
+--       go insertCase5/6
+--       
+--   make color tree ≡ Black , color unkle ≡ Black, color grand ≡ Red
+--   loop with grand as repl
+--
+-- case5/case6 rotation
+--
+--   rotate and rebuild replaceTree and rb-invariant
+
 
 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A)
@@ -942,23 +977,20 @@
            --
            insertCase13 : (v : Color ∧ A ) → v ≡ value₁ → t
            insertCase13 ⟪ Black , value₄ ⟫ refl = exit (node key₁ ⟪ Black , value₄ ⟫ left repl) (orig ∷ [])  refl record {
-             tree = orig ; rot = node key₁ value₁ left (RBI.rot r) 
+             tree = orig 
              ; origti = RBI.origti r
              ; origrb = RBI.origrb r
              ; treerb = RBI.origrb r
-             ; replrb = proj1 (rb05 (RBI.ri r))
+             ; replrb = ?
              ; si = s-nil
-             ; rotated = subst (λ k → rotatedTree k (node key₁ value₁ left (RBI.rot r))) (
-                trans (cong (λ k → node key₁ value₁ left k) (sym (rb04 si eq refl))) refl) (rtt-node rtt-unit (RBI.rotated r))
-             ; ri = proj2 (rb05 (RBI.ri r))
+             ; rotated = ?
+             ; ri = ?
+             ; state = ?
              } where
                rb09 : {n : Level} {A : Set n} →  {key key1 key2 : ℕ}  {value value1  : A} {t1 t2  : bt (Color ∧ A)}
                 → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key1 ⟪ Black , value1 ⟫ t1 t2))
                 → key < key1 
                rb09 (rb-right-red x x0 x2) = x
-               rb08 : replacedTree key ⟪ Red   , value ⟫ (child-replaced key (RBI.rot r)) repl
-                   ∨  replacedTree key ⟪ Black , value ⟫ (child-replaced key (RBI.rot r)) repl
-               rb08 = RBI.ri r
                -- rb05 should more general
                tkey : {n : Level} {A : Set n } → (rbt : bt (Color ∧ A)) → ℕ
                tkey (node key value t t2) = key
@@ -967,21 +999,6 @@
                rb051 = {!!}
                rb052 : {key key₁ : ℕ} → stackInvariant key (RBI.tree r) orig stack → key < key₁
                rb052 = {!!}
-               rb05 : ( replacedTree key ⟪ Red   , value ⟫ (child-replaced key (RBI.rot r)) repl
-                   ∨  replacedTree key ⟪ Black , value ⟫ (child-replaced key (RBI.rot r)) repl ) 
-                   → RBtreeInvariant (node key₁ ⟪ Black , value₄ ⟫ left repl) 
-                      ∧  ( replacedTree key ⟪ Red , value ⟫
-                        (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r)) )
-                        (node key₁ ⟪ Black , value₄ ⟫ left repl)
-                        ∨
-                        replacedTree key ⟪ Black , value ⟫
-                        (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r)) )
-                        (node key₁ ⟪ Black , value₄ ⟫ left repl) )
-               rb05 (case1 ri) with <-cmp key key₁
-               ... | tri< a ¬b ¬c = ⊥-elim ( ¬c c)
-               ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c c)
-               ... | tri> ¬a ¬b c = ⟪  ? , case1 ? ⟫
-               rb05 (case2 ri) = ⟪ ? , ? ⟫
            insertCase13 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r)
            ... | Black = exit {!!} {!!} {!!} {!!} 
            ... | Red = exit {!!} {!!} {!!} {!!}