Mercurial > hg > Members > Moririn

changeset 748:1d7803a2c4c0

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 16:50:12 +0900
parents 70ed4cbeaafb
children 923f72af015c
files hoareBinaryTree1.agda
diffstat 1 files changed, 14 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Tue Apr 25 09:05:03 2023 +0900
+++ b/hoareBinaryTree1.agda	Tue Apr 25 16:50:12 2023 +0900
@@ -115,28 +115,6 @@
 si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ si ) with  si-property1  si
 ... | refl = si-property-last key x t0 (x ∷ st)   si
 
-ti-right : {n  : Level} {A : Set n} {tree₁ repl : bt A} → {key₁ : ℕ} → {v1 : A} →  treeInvariant  (node key₁ v1 tree₁ repl) → treeInvariant repl
-ti-right {_} {_} {.leaf} {_} {key₁} {v1} (t-single .key₁ .v1) = t-leaf
-ti-right {_} {_} {.leaf} {_} {key₁} {v1} (t-right x ti) = ti
-ti-right {_} {_} {.(node _ _ _ _)} {_} {key₁} {v1} (t-left x ti) = t-leaf
-ti-right {_} {_} {.(node _ _ _ _)} {_} {key₁} {v1} (t-node x x₁ ti ti₁) = ti₁
-
-ti-left : {n  : Level} {A : Set n} {tree₁ repl : bt A} → {key₁ : ℕ} → {v1 : A} →  treeInvariant  (node key₁ v1 repl tree₁ ) → treeInvariant repl
-ti-left {_} {_} {.leaf} {_} {key₁} {v1} (t-single .key₁ .v1) = t-leaf
-ti-left {_} {_} {_} {_} {key₁} {v1} (t-right x ti) = t-leaf
-ti-left {_} {_} {_} {_} {key₁} {v1} (t-left x ti) = ti
-ti-left {_} {_} {.(node _ _ _ _)} {_} {key₁} {v1} (t-node x x₁ ti ti₁) = ti
-
-stackTreeInvariant : {n  : Level} {A : Set n} (key : ℕ) (sub tree : bt A) → (stack : List (bt A))
-   →  treeInvariant tree → stackInvariant key sub tree stack  → treeInvariant sub
-stackTreeInvariant {_} {A} key sub tree (sub ∷ []) ti (s-nil  ) = ti
-stackTreeInvariant {_} {A} key sub tree (sub ∷ st) ti (s-right _ si ) = ti-right (si1 si) where
-   si1 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} →  stackInvariant key (node key₁ v1 tree₁ sub ) tree st → treeInvariant  (node key₁ v1 tree₁ sub )
-   si1 {tree₁ }  {key₁ }  {v1 }  si = stackTreeInvariant  key (node key₁ v1 tree₁ sub ) tree st ti si
-stackTreeInvariant {_} {A} key sub tree (sub ∷ st) ti (s-left _ si ) = ti-left ( si2 si) where
-   si2 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} →  stackInvariant key (node key₁ v1 sub tree₁ ) tree st → treeInvariant  (node key₁ v1 sub tree₁ )
-   si2 {tree₁ }  {key₁ }  {v1 }  si = stackTreeInvariant  key (node key₁ v1 sub tree₁ ) tree st ti si
-
 rt-property1 :  {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
 rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf ()
 rt-property1 {n} {A} key value .(node key _ _ _) .(node key value _ _) r-node ()
@@ -652,12 +630,13 @@
      → ParentGrand 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 ) (orig : RBTree A key1 c1 d1 ) 
---           →  (stack : List (bt A)) → stackInvariant key (RB→bt A tree) (RB→bt A orig) stack
---           → (next : {key0 d0 : ℕ} {c0 : Color} → (tree1 : RBTree A key0 c0 d0 ) → (stack : List (bt A)) → stackInvariant key (RB→bt A tree1) (RB→bt A orig) stack  → rbt-depth A tree1 < rbt-depth A tree   → t )
---           → (exit : {key0 d0 : ℕ} {c0 : Color} → (tree1 : RBTree A key0 c0 d0 ) → (stack : List (bt A)) → stackInvariant key (RB→bt A tree1) (RB→bt A orig) stack 
---                 → (rbt-depth A tree1 ≡ 0 ) ∨ ( rbt-key A tree1 ≡ just key )  → t ) → t
---findRBP {n} {m} {A} {t} key {key1} tree orig st si next exit = ?
+findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A))) → {d d0 : ℕ}
+           →  RBtreeInvariant tree0 d0 
+           →  RBtreeInvariant tree d ∧ stackInvariant key tree tree0 stack  
+           → (next : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → {d1 : ℕ} → RBtreeInvariant tree1 d1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree   → t )
+           → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → {d1 : ℕ} → RBtreeInvariant tree1 d1 ∧ stackInvariant key tree1 tree0 stack
+                 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
+findRBT = ?
 
 rotateRight : ?
 rotateRight = ?
@@ -683,14 +662,18 @@
 
 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → {key0 key1 d0 d1 : ℕ} {c0 c1 : Color}  
-     → (orig tree : bt (Color ∧ A)) 
-     → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
+     → (orig tree : bt (Color ∧ A)) {d0 : ℕ}
+     →  RBtreeInvariant orig d0 
+     →  {d : ℕ} → RBtreeInvariant tree d → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
      → (next : {key2 d2 : ℕ} {c2 : Color}  
         → (to tr : bt (Color ∧ A)) 
+        →  RBtreeInvariant orig d0 
+        →  {d : ℕ} → RBtreeInvariant tree d 
         → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 
         → length stack1 < length stack  → t )
      → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
-         → (ri : rotatedTree (RB→bt A orig) (RB→bt A rot) ) → replacedTree key value (RB→bt A rot) (RB→bt A repl) → t ) → t
+        →  {d : ℕ} → RBtreeInvariant repl d 
+        → (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
 replaceRBP {n} {m} {A} {t} key value {_} {key1} orig tree stack si next exit = ? where
     insertCase2 : {k0 k1 d0 d1 d2 : ℕ} {c0 c1 c2 : Color} → (tree parent grand : bt (Color ∧ A)) 
       → (stack : List (bt (Color ∧ A))) → (tr to : bt (Color ∧ A)) → (si : stackInvariant key tr to stack )