Mercurial > hg > Gears > GearsAgda

changeset 783:dca93aef5e36

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix findRBT
author Mori
date Mon, 21 Aug 2023 19:01:36 +0900
parents 0b791ae19543
children 2955d5b7debd
files .git/COMMIT_EDITMSG .git/index work.agda work.agdai
diffstat 4 files changed, 13 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/.git/COMMIT_EDITMSG	Mon Jul 10 20:19:13 2023 +0900
+++ b/.git/COMMIT_EDITMSG	Mon Aug 21 19:01:36 2023 +0900
@@ -1,1 +1,1 @@
-7/7
+8/17
Binary file .git/index has changed
--- a/work.agda	Mon Jul 10 20:19:13 2023 +0900
+++ b/work.agda	Mon Aug 21 19:01:36 2023 +0900
@@ -88,7 +88,7 @@
 data replacedTree {n : Level } {A : Set n} (key : ℕ) (value : A) : (before after : bt A) → Set n where
   r-leaf : replacedTree key value leaf (node key value leaf leaf)
   
-  r-node : {value1 : A} → {left right : bt A} → replacedTree key value (node key value left right) (node key value1 left right)
+  r-node : {value₁ : A} → {left right : bt A} → replacedTree key value (node key value₁ left right) (node key value left right)
   
   -- key is the repl's key , so need comp key and key1
   r-left : {key1 : ℕ} {value1 : A }→ {left right repl : bt A} → key < key1
@@ -97,12 +97,7 @@
   r-right : {key1 : ℕ } {value1 : A} → {left right repl : bt A} → key1 < key
    → replacedTree key value right repl → replacedTree key value (node key1 value1 left right) (node key1 value1 left repl)
 
-{-
-RTtoTI0 : {n : Level} {A : Set n } → (key : ℕ ) → (value : A) → (tree repl : bt A)
- → treeInvariant tree → replacedTree key value tree repl → treeInvariant repl
-RTtoTI0 key value leaf (node key value leaf leaf) tr r-leaf = t-single key value 
-RTtoTI0 key value (node key₁ value₁ tree tree₁) (node key₂ value₂ repl repl₁) (t-node x x₁ s s₁) r-node = t-node x x₁ s s₁
--}
+
 depth-1< : {i j : ℕ} → suc i ≤ suc (i Data.Nat.⊔ j )
 depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
 depth-2< : {i j : ℕ} →   suc i ≤ suc (j Data.Nat.⊔ i )
@@ -329,17 +324,14 @@
        ri : replacedRBTree key value (child-replaced key rot ) repl
 
 
-{-
 rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) ) 
            → RBtreeInvariant parent 
            → RBtreeInvariant repl 
            → {left right : bt (Color ∧ A)} → parent ≡ node key ⟪ Black , value ⟫ left right
            →    (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl  ) )
              ∧  (color left  ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) )
-rbi-case1 {n} {A} {key} (node key1 ⟪ Black , value1 ⟫ l r) leaf rbip rbir left right x = {!!}
-rbi-case1 {n} {A} {key} parent (node key₁ value₁ tree1 tree2) rbi rb2 x = {!!}
+rbi-case1 {n} {A} {key} parent repl rbtip rbtir x = ⟪ {!!} , {!!} ⟫
 
--}
 blackdepth≡ : {n : Level } {A : Set n} → {C : Color} {key : ℕ} {value : A} → (tree1 tree2 : bt (Color ∧ A))
   → RBtreeInvariant tree1
   → RBtreeInvariant tree2
@@ -351,15 +343,14 @@
 blackdepth≡ (node key value t1 t3) leaf ri1 ri2 rip = {!!}
 blackdepth≡ (node key value t1 t3) (node key₁ value₁ t2 t4) ri1 ri2 rip = {!!}
 
-rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) )                                             
-           → RBtreeInvariant parent                                                                                                        
-           → RBtreeInvariant repl                                                                                                           
-           → (left right : bt (Color ∧ A)) → parent ≡ node key ⟪ Black , value ⟫ left right
+
+{-
+rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) )                        
+           → RBtreeInvariant parent                    
+           → RBtreeInvariant repl                                                                                                 → (left right : bt (Color ∧ A)) → parent ≡ node key ⟪ Black , value ⟫ left right
            → RBtreeInvariant left
            → RBtreeInvariant right
-           →    (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl  ) )                                                          ∧  (color left  ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) )    
-rbi-case1 {n} {A} {key} (node key1 ⟪ Black , value1 ⟫ l r) leaf rbip rbir (node key3 ⟪ Red , val3 ⟫ la ra) (node key4 ⟪ Red , val4 ⟫ lb rb) pa li ri
- = ⟪ {!!} rb-left-black {!!} {!!} li , (λ x → rb-right-black {!!} {!!} ri) ⟫
-
---⟪ rb-left-black {!!} {!!} (RBtreeLeftDown left  right rbip ) , {!!} ⟫
---rbi-case1 {n} {A} {key} parent (node key₁ value₁ tree1 tree2) rbi rb2 x = {!!}
+           →    (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl  ) )                                                          ∧  (color left  ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) )
+           
+rbi-case1 {n} {A} {key} (node key1 ⟪ Black , value1 ⟫ l r) leaf rbip rbir (node key3 ⟪ Red , val3 ⟫ la ra) (node key4-- ⟪ Red , val4 ⟫ lb rb) pa li ri = {!!}
+-}
Binary file work.agdai has changed