Mercurial > hg > Gears > GearsAgda

changeset 745:9b7d706e7d0f

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 Mon, 24 Apr 2023 18:42:31 +0900
parents fbe7c5f09ef0
children 4edec19e8356
files hoareBinaryTree1.agda
diffstat 1 files changed, 22 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Apr 24 16:02:38 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Apr 24 18:42:31 2023 +0900
@@ -44,17 +44,17 @@
 data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where
     t-leaf : treeInvariant leaf 
     t-single : (key : ℕ) → (value : A) →  treeInvariant (node key value leaf leaf) 
-    t-right : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) → treeInvariant (node key₁ value₁ t₁ t₂)
+    t-right : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁ → treeInvariant (node key₁ value₁ t₁ t₂)
        → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂)) 
-    t-left  : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → (key < key₁) → treeInvariant (node key value t₁ t₂)
+    t-left  : {key key₁ : ℕ} → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁ → treeInvariant (node key value t₁ t₂)
        → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf ) 
-    t-node  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → (key < key₁) → (key₁ < key₂)
+    t-node  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → key < key₁ → key₁ < key₂
        → treeInvariant (node key value t₁ t₂) 
        → treeInvariant (node key₂ value₂ t₃ t₄)
        → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) 
 
 --
---  stack always contains original top at end
+--  stack always contains original top at end (path of the tree)
 --
 data stackInvariant {n : Level} {A : Set n}  (key : ℕ) : (top orig : bt A) → (stack  : List (bt A)) → Set n where
     s-nil :  {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [])
@@ -544,6 +544,18 @@
     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 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) 
+
 data RBTree {n : Level} (A : Set n) : (key : ℕ) → Color → (b-depth : ℕ) → Set n where
     rb-leaf     : (key : ℕ) → RBTree A key Black 0
     rb-single   : (key : ℕ) → (value : A) → (c : Color) →  RBTree A key c 1
@@ -611,10 +623,16 @@
 
 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}
           → 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) ) 
+    --     b                  a 
+    --   d   a              b   c
+    --         c          d 
     rr-left : {ka kb : ℕ } {va vb : A} → {ta tb tc ta1 tb1 tc1 : bt A}
           → ka < kb
           → rotatedTree ta ta1 → rotatedTree tb tb1 → rotatedTree tc tc1