Mercurial > hg > Members > Moririn

changeset 746:4edec19e8356

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, 25 Apr 2023 08:16:02 +0900
parents 9b7d706e7d0f
children 70ed4cbeaafb
files hoareBinaryTree1.agda
diffstat 1 files changed, 44 insertions(+), 54 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Apr 24 18:42:31 2023 +0900
+++ b/hoareBinaryTree1.agda	Tue Apr 25 08:16:02 2023 +0900
@@ -544,17 +544,35 @@
     Red : Color
     Black : Color
 
-data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where
-    rb-leaf     : RBtreeInvariant leaf
-    rb-single : (key : ℕ) → (value : A) → (c : Color) →  RBtreeInvariant (node key ⟪ c , value ⟫ leaf leaf) 
+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) → (c : Color) →  RBtreeInvariant (node key ⟪ c , value ⟫ leaf leaf) 1
+    rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {d : ℕ }
+       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) d
+       → RBtreeInvariant (node key  ⟪ Red ,   value  ⟫ leaf (node key₁ ⟪ Black , value₁ ⟫ t t₁)) d
+    rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {d : ℕ } {c : Color}
+       → RBtreeInvariant (node key₁ ⟪ c     , value₁ ⟫ t t₁) d
+       → RBtreeInvariant (node key  ⟪ Black , value  ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁)) (suc d)
+    rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {d : ℕ }
+       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) d
+       → RBtreeInvariant (node key₁  ⟪ Red ,   value  ⟫ (node key ⟪ Black , value₁ ⟫ t t₁) leaf ) d
+    rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {d : ℕ } {c : Color}
+       → RBtreeInvariant (node key₁ ⟪ c     , value₁ ⟫ t t₁) d
+       → RBtreeInvariant (node key₁  ⟪ Black , value  ⟫ (node key ⟪ c , value₁ ⟫ t t₁) leaf) (suc d)
+    rb-node-red  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → {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 : ℕ}
+       → {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)
 
-data replacedRBTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt (Color ∧ A) ) → Set n where
-    r-leaf : replacedRBTree key ⟪ ? , value ⟫ leaf (node key ⟪ ? , value ⟫ leaf leaf)
-    r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁) 
-    r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
-          → k < key →  replacedTree key value t2 t →  replacedTree key value (node k v1 t1 t2) (node k v1 t1 t) 
-    r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
-          → key < k →  replacedTree key value t1 t →  replacedTree key value (node k v1 t1 t2) (node k v1 t t2) 
+
+-- 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)
 
 data RBTree {n : Level} (A : Set n) : (key : ℕ) → Color → (b-depth : ℕ) → Set n where
     rb-leaf     : (key : ℕ) → RBTree A key Black 0
@@ -575,41 +593,12 @@
        → RBTree A key₂ c1 d
        → RBTree A key₁ Black (suc d)
 
-color : {n : Level} (A : Set n) {key d : ℕ} {c : Color } → (rb : RBTree A key c d ) → Color
-color {n} A {k} {d} {c} rb = c
-
-rb-key : {n : Level} (A : Set n) {key d : ℕ} {c : Color } → (rb : RBTree A key c d ) → ℕ
-rb-key {n} A {k} {d} {c} rb = k
-
-RB→bt : {n : Level} (A : Set n) {key d : ℕ} {c : Color } → (rb : RBTree A key c d ) → bt A
-RB→bt {n} A (rb-leaf _) = leaf
-RB→bt {n} A (rb-single key value _) = node key value leaf leaf
-RB→bt {n} A (t-right-red key value x rb) = node key value leaf (RB→bt A rb)
-RB→bt {n} A (t-right-black key value x rb) = node key value leaf (RB→bt A rb)
-RB→bt {n} A (t-left-red key value x rb) = node key value (RB→bt A rb) leaf
-RB→bt {n} A (t-left-black key value x rb) = node key value (RB→bt A rb) leaf
-RB→bt {n} A (t-node-red key value x x₁ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁) 
-RB→bt {n} A (t-node-black key value x x₁ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁) 
+color : {n : Level} (A : Set n)  → (rb : bt (A ∧ Color)) → Color
+color {n} A {k} {d} {c} rb = ?
 
-rbt-depth : {n : Level} (A : Set n) {key : ℕ} {c : Color} {d : ℕ} → RBTree A key c d → ℕ
-rbt-depth A (rb-leaf _) = zero
-rbt-depth A (rb-single _ value _) = 1
-rbt-depth A (t-right-red _ value x ab) = suc ( rbt-depth A ab)
-rbt-depth A (t-right-black _ value x ab) = suc ( rbt-depth A ab)
-rbt-depth A (t-left-red _ value x ab) = suc ( rbt-depth A ab)
-rbt-depth A (t-left-black _ value x ab) = suc ( rbt-depth A ab)
-rbt-depth A (t-node-red _ value x x₁ ab ab₁) = suc (Data.Nat._⊔_ (rbt-depth A ab ) (rbt-depth A ab₁ )) 
-rbt-depth A (t-node-black _ value x x₁ ab ab₁) = suc (Data.Nat._⊔_ (rbt-depth A ab ) (rbt-depth A ab₁ )) 
-
-rbt-key : {n : Level} (A : Set n) {key : ℕ} {c : Color} {d : ℕ} → RBTree A key c d → Maybe ℕ
-rbt-key {n} A (rb-leaf _) = nothing
-rbt-key {n} A (rb-single key value _) = just key
-rbt-key {n} A (t-right-red key value x rb) = just key
-rbt-key {n} A (t-right-black key value x rb) = just key
-rbt-key {n} A (t-left-red key value x rb) = just key
-rbt-key {n} A (t-left-black key value x rb) = just key
-rbt-key {n} A (t-node-red key value x x₁ rb rb₁) = just key
-rbt-key {n} A (t-node-black key value x x₁ rb rb₁) = just key
+RB→bt : {n : Level} (A : Set n)  → (rb : bt (A ∧ Color)) → bt A
+RB→bt {n} A leaf = leaf
+RB→bt {n} A (node key ⟪ c , value ⟫ x x₁ rb rb₁) = node key value (RB→bt A rb) (RB→bt A rb₁) 
 
 data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent grand : bt A) → Set n where
     s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 
@@ -621,22 +610,23 @@
     s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } 
         → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand self parent grand 
 
+-- with color
 data rotatedTree  {n : Level} {A : Set n}  : (before after : bt A ) → Set n where
     rr-node : {t : bt A} → rotatedTree t t
-    --     a                  b 
-    --    b  c              d   a
-    --  d                         c
-    rr-right : {ka kb : ℕ } {va vb : A} → {ta tb tc ta1 tb1 tc1 : bt A}
+    --      a                 b 
+    --    b   c             d   a
+    --  d   e                 e   c
+    rr-right : {ka kb : ℕ } {va vb : A} → {c c₁ d d₁ e e₁ : bt A}
           → ka < kb
-          → rotatedTree ta ta1 → rotatedTree tb tb1 → rotatedTree tc tc1
-          → rotatedTree (node ka va (node kb vb ta tb)  tc) (node kb vb ta1 (node ka va tb1 tc1) ) 
+          → rotatedTree d d₁ → rotatedTree e e₁ → rotatedTree c c₁
+          → rotatedTree (node ka va (node kb vb d e)  tc) (node kb vb d₁ (node ka va e₁ c₁) ) 
     --     b                  a 
     --   d   a              b   c
-    --         c          d 
-    rr-left : {ka kb : ℕ } {va vb : A} → {ta tb tc ta1 tb1 tc1 : bt A}
+    --     e   c          d   e
+    rr-left : {ka kb : ℕ } {va vb : A} → {c c₁ d d₁ e e₁ : bt A}
           → ka < kb
-          → rotatedTree ta ta1 → rotatedTree tb tb1 → rotatedTree tc tc1
-          → rotatedTree (node kb vb ta (node ka va tb tc) ) (node ka va (node kb vb ta1 tb1)  tc1) 
+          → rotatedTree d d₁ → rotatedTree e e₁ → rotatedTree c c₁
+          → rotatedTree (node kb vb d (node ka va e c) ) (node ka va (node kb vb d₁ e₁)  c₁) 
 
 record PG {n : Level } (A : Set n) (stack : List (bt A)) : Set n where
     field