Mercurial > hg > Gears > GearsAgda

changeset 795:e9ba6a5bc64b

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, 24 Oct 2023 10:33:48 +0900
parents 2a07b50f4bc0
children e1737f00a7aa
files hoareBinaryTree1.agda
diffstat 1 files changed, 9 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Oct 23 19:29:43 2023 +0900
+++ b/hoareBinaryTree1.agda	Tue Oct 24 10:33:48 2023 +0900
@@ -946,7 +946,7 @@
            → stackInvariant key (RBI.tree r) orig stack
            → t
         insertCase12 leaf eq1 si = ? -- can't happen
-        insertCase12  tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ | child-replaced key (node key₁ value₁ left (RBI.rot r)) in eqcd
+        insertCase12  tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ | child-replaced key (node key₁ value₁ left (RBI.rot r)) in eqcr
         ... | tri< a ¬b ¬c | cr = ?
         ... | tri≈ ¬a b ¬c | cr = ? -- can't happen
         ... | tri> ¬a ¬b c | cr = insertCase13 value₁ refl where
@@ -968,7 +968,7 @@
            rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x si) refl refl with si-property1 si
            ... | refl = ⊥-elim ( nat-<> x c  )
            insertCase13 : (v : Color ∧ A ) → v ≡ value₁ → t
-           insertCase13 ⟪ Black , value₄ ⟫ refl = exit (node key₁ value₁ left repl) (orig ∷ [])  refl record {
+           insertCase13 ⟪ Black , value₄ ⟫ refl = exit (node key₁ ⟪ Red , value₄ ⟫ left repl) (orig ∷ [])  refl record {
              tree = orig ; rot = node key₁ value₁ left (RBI.rot r) 
              ; origti = RBI.origti r
              ; origrb = RBI.origrb r
@@ -978,11 +978,14 @@
              ; rotated = subst (λ k → rotatedTree k (node key₁ value₁ left (RBI.rot r))) (
                 trans (cong (λ k → node key₁ value₁ left k) (sym (rb04 si eq refl))) refl) (rtt-node rtt-unit (RBI.rotated r))
              ; ri = proj2 rb05
-             ; repl-red = ?
-             ; repl-eq = ?
+             ; repl-red = refl
+             ; repl-eq = rb07
              } where
-               rb05 : RBtreeInvariant (node key₁ value₁ left repl) ∧  replacedRBTree key value
-                    (child-replaced key (node key₁ value₁ left (RBI.rot r))) (node key₁ value₁ left repl)
+               rb07 :  black-depth (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) ≡ black-depth left ⊔ black-depth repl
+               rb07 = ?
+               -- rb05 should more general     
+               rb05 : RBtreeInvariant (node key₁ ⟪ Red , value₄ ⟫ left repl) ∧  replacedRBTree key value
+                    (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) (node key₁ ⟪ Red , value₄ ⟫ left repl)
                rb05 with RBI.origrb r | rb04 si eq refl | RBI.replrb r in eqrepl
                ... | rb-single key₂ value₂ | refl | rb-single key value = ?
                ... | rb-single key₂ value₂ | refl | rb-right-red x x₁ rb = ?