Mercurial > hg > Gears > GearsAgda

changeset 773:d6d442196c87

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, 09 May 2023 19:48:59 +0900
parents a8af918e7fd9
children ebd8a73543dd
files hoareBinaryTree1.agda
diffstat 1 files changed, 48 insertions(+), 44 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon May 08 18:49:57 2023 +0900
+++ b/hoareBinaryTree1.agda	Tue May 09 19:48:59 2023 +0900
@@ -533,40 +533,28 @@
 data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → (bd : ℕ) → Set n where
     rb-leaf     : RBtreeInvariant leaf 0
     rb-single : (key : ℕ) → (value : A) →  RBtreeInvariant (node key ⟪ Black , value ⟫ leaf leaf) 1
-    rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ 
+    rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} 
        → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) 1
        → RBtreeInvariant (node key  ⟪ Red ,   value  ⟫ leaf (node key₁ ⟪ Black , value₁ ⟫ t t₁)) 1
-    rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ →  {c : Color}
+    rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → {c : Color}
        → RBtreeInvariant (node key₁ ⟪ c     , value₁ ⟫ t t₁) 1
        → RBtreeInvariant (node key  ⟪ Black , value  ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁)) 1
-    rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ 
+    rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} 
        → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) 1
        → RBtreeInvariant (node key₁  ⟪ Red ,   value  ⟫ (node key ⟪ Black , value₁ ⟫ t t₁) leaf ) 1
-    rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ →  {c : Color}
+    rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → {c : Color}
        → RBtreeInvariant (node key₁ ⟪ c     , value₁ ⟫ t t₁) 1
        → RBtreeInvariant (node key₁  ⟪ Black , value  ⟫ (node key ⟪ c , value₁ ⟫ t t₁) leaf) 1
-    rb-node-red  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → (d : ℕ)
+    rb-node-red  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → (d : ℕ)
        → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ t₂) d
        → RBtreeInvariant (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄) d
        → RBtreeInvariant (node key₁ ⟪ Red , value₁ ⟫ (node key ⟪ Black , value ⟫ t₁ t₂) (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)) d
-    rb-node-black  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → (d : ℕ)
+    rb-node-black  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → (d : ℕ)
        → {c c₁ : Color}
        → RBtreeInvariant (node key  ⟪ c  , value  ⟫ t₁ t₂) d
        → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) d
        → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)) (suc d)
 
--- RBttreeInvariant tree bd → treeInvariant is easy
-
-RBti→ti : {n : Level} {A : Set n}  (tree : bt (Color ∧ A)) {bd : ℕ} → RBtreeInvariant tree bd → treeInvariant tree
-RBti→ti {n} {A} .leaf rb-leaf = t-leaf
-RBti→ti {n} {A} .(node key ⟪ Black , value ⟫ leaf leaf) (rb-single key value) = t-single ? ?
-RBti→ti {n} {A} .(node _ ⟪ Red , _ ⟫ leaf (node _ ⟪ Black , _ ⟫ _ _)) (rb-right-red x bd) = ?
-RBti→ti {n} {A} .(node _ ⟪ Black , _ ⟫ leaf (node _ ⟪ _ , _ ⟫ _ _)) (rb-right-black x bd) = ?
-RBti→ti {n} {A} .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) leaf) (rb-left-red x bd) = ?
-RBti→ti {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ _ , _ ⟫ _ _) leaf) (rb-left-black x bd) = ?
-RBti→ti {n} {A} .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (node _ ⟪ Black , _ ⟫ _ _)) (rb-node-red x x₁ _ bd bd₁) = ?
-RBti→ti {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ _ , _ ⟫ _ _) (node _ ⟪ _ , _ ⟫ _ _)) (rb-node-black x x₁ d bd bd₁) = ?
-
 tesr-rb-0 : RBtreeInvariant {_} {ℕ} leaf 0
 tesr-rb-0 = rb-leaf
 
@@ -574,15 +562,11 @@
 tesr-rb-1 = rb-single 10 10
 
 tesr-rb-2 : RBtreeInvariant {_} {ℕ} (node 10 ⟪ Red , 10 ⟫ (node 5 ⟪ Black , 5 ⟫ leaf leaf)  leaf) 1
-tesr-rb-2 = rb-left-red (add< _) ( rb-single 10 5)
+tesr-rb-2 = rb-left-red  ( rb-single 10 5)
 
--- This one can be very difficult
--- data replacedRBTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt (Color ∧ A) ) → Set n where
---    rb-leaf : replacedRBTree key value leaf (node key ⟪ Black , value ⟫ leaf leaf)
-
-color : {n : Level} (A : Set n)  → (rb : bt (Color ∧ A)) → Color
-color {n} A leaf = Red
-color {n} A (node key ⟪ c , v ⟫ rb rb₁) = c
+color : {n : Level} {A : Set n}  → (rb : bt (Color ∧ A)) → Color
+color leaf = Red
+color (node key ⟪ c , v ⟫ rb rb₁) = c
 
 RB→bt : {n : Level} (A : Set n)  → (rb : bt (Color ∧ A)) → bt A
 RB→bt {n} A leaf = leaf
@@ -635,30 +619,50 @@
    field
        od d rd : ℕ
        tree rot repl : bt (Color ∧ A)
+       origti : treeInvariant orig 
        origrb : RBtreeInvariant orig od
        treerb : RBtreeInvariant tree d
        replrb : RBtreeInvariant repl rd
-       d=rd : ( d ≡ rd ) ∨ ( suc d ≡ rd )
+       d=rd : ( d ≡ rd ) ∨ ( (suc d ≡ rd ) ∧ (color tree ≡ Red))
        si : stackInvariant key tree orig stack
        rotated : rotatedTree tree rot
        ri : replacedRBTree key value (child-replaced key rot ) repl
-   
-rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (tree orig : bt (Color ∧ A) )
-           →  (stack : List (bt (Color ∧ A))) 
-           →  stack ≡ tree ∷ orig ∷ [] → RBI key value orig stack → RBI key value orig (orig ∷ [])
-rbi-case1 {n} {A} {key} {value} tree₁ .(node k1 ⟪ Red , v1 ⟫ t1 tree₁) (tree₁ ∷ node k1 ⟪ Red , v1 ⟫ t1 tree₁ ∷ []) refl record { od = od ; d = d ; rd = rd ; tree = .tree₁ ; rot = rot ; repl = repl ; origrb = origrb ; treerb = treerb ; replrb = replrb ; d=rd = d=rd ; si = (s-right .tree₁ .(node _ ⟪ Red , v1 ⟫ t1 tree₁) t1 x s-nil) ; rotated = rotated ; ri = ri } = record {
-       od = od ; d = ? ; rd = ?
-     ; tree = node _ ⟪ Red , v1 ⟫ t1 tree₁ ; rot = ? ; repl = node k1 ⟪ Red , v1 ⟫ t1 repl
-     ; origrb = origrb
-     ; treerb = ?
-     ; replrb = ?
-     ; d=rd = ?
-     ; si = s-nil
-     ; rotated = ?
-     ; ri = ?
-   }
-rbi-case1 {n} {A} {key} {value} tree₁ .(node _ ⟪ Black , proj4 ⟫ t1 tree₁) (tree₁ ∷ node _ ⟪ Black , proj4 ⟫ t1 tree₁ ∷ []) refl record { od = od ; d = d ; rd = rd ; tree = .tree₁ ; rot = rot ; repl = repl ; origrb = origrb ; treerb = treerb ; replrb = replrb ; d=rd = d=rd ; si = (s-right .tree₁ .(node _ ⟪ Black , proj4 ⟫ t1 tree₁) t1 x s-nil) ; rotated = rotated ; ri = ri } = ?
-rbi-case1 {n} {A} {key} {value} tree₁ orig (tree₁ ∷ orig ∷ []) refl record { od = od ; d = d ; rd = rd ; tree = .tree₁ ; rot = rot ; repl = repl ; origrb = origrb ; treerb = treerb ; replrb = replrb ; d=rd = d=rd ; si = (s-left _ _ _ x si) ; rotated = rotated ; ri = ri } = ?
+
+--   r (b , b)    inserting a node into black node does not change the black depth, but color may change
+--       → b (b , r ) ∨ b (r , b)
+--   b (b , b)    
+--       → b (b , r ) ∨ b (r , b)
+--   b (r , b)    inserting to right → b (r , r ) 
+--   b (r , b)    inserting to left may increse black depth, need rotation
+--      find b in left and move the b to the right (one down or two down)
+--
+rbi-case1 : {n : Level} {A : Set n} → {key d : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) ) 
+           → RBtreeInvariant parent (suc d)
+           → RBtreeInvariant repl d 
+           → {left right : bt (Color ∧ A) } → parent ≡ node key ⟪ Black , value ⟫ left right
+           →    (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl  ) (suc d))
+             ∧  (color left  ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) (suc d))
+rbi-case1 {n} {A} {key} = ?
+
+rbi-case3 : {n : Level} {A : Set n} → {kg kp d dp : ℕ} → {vg vp : A} → {cg : Color} → (tree grand parent repl : bt (Color ∧ A) ) 
+           → RBtreeInvariant grand dp
+           → RBtreeInvariant repl d 
+           → {uncle left right : bt (Color ∧ A) } 
+           → grand  ≡ node kg ⟪ cg , vg ⟫ uncle parent
+           → parent ≡ node kp ⟪ Red , vp ⟫ left  right
+           → color uncle ≡ Red
+           →     (color left  ≡ Red → RBtreeInvariant (node kg ⟪ Red , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ repl right )) dp) 
+              ∧  (color right ≡ Red → RBtreeInvariant (node kg ⟪ Red , vg ⟫ uncle (node kp ⟪ Black , vp ⟫ left repl  )) dp)
+rbi-case3 {n} {A} {key} = ?
+
+--... | Black = record {
+--             d = ? ; od = RBI.od rbi ; rd = ? 
+--          ;  tree = ? ; rot = ? ; repl = ?
+--          ;  treerb = ? ; replrb = ?
+--          ;  d=rd = ? ; si = ? ; rotated = ? ; ri = ?
+--          ;  origti = RBI.origti rbi ; origrb = RBI.origrb rbi
+--       }
+--... | Red = ?
 
 stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A )
            →  (stack : List (bt A)) → stackInvariant key tree orig stack