Mercurial > hg > Members > Moririn

changeset 736:744ead2536a4

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 Fri, 21 Apr 2023 14:44:52 +0900
parents 7901892bb1d8
children 7ae2dea2546b
files hoareBinaryTree1.agda
diffstat 1 files changed, 27 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Fri Apr 21 10:50:10 2023 +0900
+++ b/hoareBinaryTree1.agda	Fri Apr 21 14:44:52 2023 +0900
@@ -593,21 +593,27 @@
 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
 
-data rbstackInvariant2 {n : Level} {A : Set n} (orig : bt A) : (parent grand : bt A) → Set n where
-    s2-left  :  {key : ℕ} {value : A} → (n1 : bt A) → rbstackInvariant2 orig (node key value orig n1) orig
-    s2-right :  {key : ℕ} {value : A} → (n1 : bt A) → rbstackInvariant2 orig (node key value n1 orig) orig
+data rbstackInvariant2 {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 : bt A } → parent ≡ node kp vp self n1 → rbstackInvariant2 self parent (node kg vg parent n2) 
+    s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent : bt A } → parent ≡ node kp vp n1 self → rbstackInvariant2 self parent (node kg vg parent n2) 
+    s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent : bt A } → parent ≡ node kp vp self n1 → rbstackInvariant2 self parent (node kg vg n2 parent) 
+    s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent : bt A } → parent ≡ node kp vp n1 self → rbstackInvariant2 self parent (node kg vg n2 parent) 
 
-data replacedTreeRotate  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt A ) → Set n where
-    rr-leaf : replacedTreeRotate key value leaf (node key value leaf leaf)
-    rr-node : {value₁ : A} → {t t₁ : bt A} → replacedTreeRotate key value (node key value₁ t t₁) (node key value t t₁) 
-    rr-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
-          → k < key →  replacedTreeRotate key value t2 t →  replacedTreeRotate key value (node k v1 t1 t2) (node k v1 t1 t) 
-    rr-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
-          → key < k →  replacedTreeRotate key value t1 t →  replacedTreeRotate key value (node k v1 t1 t2) (node k v1 t t2) 
+data rotatedTree  {n : Level} {A : Set n}  : (before after : bt A ) → Set n where
+    rr-leaf : rotatedTree leaf leaf
+    rr-node : {t : bt A} → rotatedTree t t
+    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) ) 
+    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
+          → rotatedTree (node kb vb ta (node ka va tb tc) ) (node ka va (node kb vb ta1 tb1)  tc1) 
 
-rbsi-len :  {n : Level} {A : Set n}  {key : ℕ} {c : Color} {d : ℕ} (orig : RBTree A key c d ) {key₁ : ℕ } 
-     → rbstackInvariant2 ? ? ? → ℕ
-rbsi-len orig = ?
+rbsi-len :  {n : Level} {A : Set n} {orig parent grand : bt A}
+     → rbstackInvariant2 orig parent grand → ℕ
+rbsi-len {n} {A} {s} {p} {g} st = ?
 
 findRBP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) {key1 d d1 : ℕ} → {c c1 : Color} → (tree : RBTree A key c d ) (tree1 : RBTree A key1 c1 d1 ) 
            →  rbstackInvariant2 ? ? ?
@@ -633,13 +639,13 @@
      → (key : ℕ) → (value : A) → {key0 key1 key2 d0 d1 d2 : ℕ} {c0 c1 c2 : Color}  
      → (orig : RBTree A key1 c1 d1 ) → (tree : RBTree A key1 c1 d1 ) ( repl : RBTree A key2 c2 d2 )
      → (si : rbstackInvariant2 ? ? ?)
-     → (ri : replacedTreeRotate key value (RB→bt A tree) (RB→bt A repl))
+     → (ri : rotatedTree (RB→bt A tree) (RB→bt A repl))
      → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (tree1 : RBTree A k1 c1 d1 ) (repl1 : RBTree A k2 c2 d2 ) 
          → (si1 : rbstackInvariant2 ? ? ?)
-         → (ri : replacedTreeRotate key value (RB→bt A tree1) (RB→bt A repl1))
-         → rbsi-len orig si1 < rbsi-len orig si → t )
+         → (ri : rotatedTree (RB→bt A tree1) (RB→bt A repl1))
+         → rbsi-len si1 < rbsi-len si → t )
      → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 : RBTree A k1 c1 d1 ) → (repl1 : RBTree A k2 c2 d2 ) 
-         → (ri : replacedTreeRotate key value (RB→bt A orig) (RB→bt A repl1))
+         → (ri : rotatedTree (RB→bt A orig) (RB→bt A repl1))
          → t ) → t
 insertCase5 {n} {m} {A} {t} key value orig tree repl si ri next exit = ? where
     insertCase51 : (key1 : ℕ)  (si : rbstackInvariant2 ? ? ? )  → t
@@ -649,13 +655,13 @@
      → (key : ℕ) → (value : A) → {key0 key1 key2 d0 d1 d2 : ℕ} {c0 c1 c2 : Color}  
      → (orig : RBTree A key1 c1 d1 ) → (tree : RBTree A key1 c1 d1 ) ( repl : RBTree A key2 c2 d2 )
      → (si : rbstackInvariant2 ? ? ? )
-     → (ri : replacedTreeRotate key value (RB→bt A tree) (RB→bt A repl))
+     → (ri : rotatedTree (RB→bt A tree) (RB→bt A repl))
      → (next : ℕ → A → {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} → (tree1 : RBTree A k1 c1 d1 ) (repl1 : RBTree A k2 c2 d2 ) 
          → (si1 : rbstackInvariant2 ? ? ? )
-         → (ri : replacedTreeRotate key value (RB→bt A tree1) (RB→bt A repl1))
-         → rbsi-len orig si1 < rbsi-len orig si → t )
+         → (ri : rotatedTree (RB→bt A tree1) (RB→bt A repl1))
+         → rbsi-len si1 < rbsi-len si → t )
      → (exit : {k1 k2 d1 d2 : ℕ} {c1 c2 : Color} (tree1 : RBTree A k1 c1 d1 ) → (repl1 : RBTree A k2 c2 d2 ) 
-         → (ri : replacedTreeRotate key value (RB→bt A orig) (RB→bt A repl1))
+         → (ri : rotatedTree (RB→bt A orig) (RB→bt A repl1))
          → t ) → t
 replaceRBP {n} {m} {A} {t} key value {_} {key2} orig tree repl si ri next exit = insertCase1 key2 si where
     insertCase4 : (key1 : ℕ) → (si : rbstackInvariant2 ? ? ? ) →  {k1 d1 d2 : ℕ} {c1 c2 : Color} → (parent : RBTree A k1 c1 d1) → (grand : RBTree A key1 c2 d2) → t