Mercurial > hg > Gears > GearsAgda

changeset 813:8dbddf72211e

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, 22 Jan 2024 18:51:56 +0900
parents b8fb1e0755d0
children 82029d2a8970
files hoareBinaryTree1.agda
diffstat 1 files changed, 32 insertions(+), 43 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon Jan 22 11:15:38 2024 +0900
+++ b/hoareBinaryTree1.agda	Mon Jan 22 18:51:56 2024 +0900
@@ -738,8 +738,6 @@
        rotated : rotatedTree tree rot
        ri : replacedTree key ⟪ Red   , value ⟫ (child-replaced key rot ) repl
          ∨  replacedTree key ⟪ Black , value ⟫ (child-replaced key rot ) repl
-       repl-red : color repl ≡ Red
-       repl-eq : black-depth (child-replaced key rot ) ≡ black-depth repl
 
 stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A )
            →  (stack : List (bt A)) → stackInvariant key tree orig stack
@@ -914,10 +912,14 @@
            → 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 eqcr
-        ... | tri< a ¬b ¬c | cr = {!!}
-        ... | tri≈ ¬a b ¬c | cr = {!!} -- can't happen
-        ... | tri> ¬a ¬b c | cr = insertCase13 value₁ refl where
+        insertCase12  tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ 
+        ... | tri< a ¬b ¬c = {!!} where 
+           rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → left ≡ RBI.tree r
+           rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x s-nil) refl refl = refl
+           rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl with si-property1 si
+           ... | refl = ⊥-elim ( nat-<> x a  )
+        ... | tri≈ ¬a b ¬c = {!!} -- can't happen
+        ... | tri> ¬a ¬b c = insertCase13 value₁ refl where
            --
            --    orig B
            --    /  \
@@ -935,35 +937,28 @@
            rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl = refl
            rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x si) refl refl with si-property1 si
            ... | refl = ⊥-elim ( nat-<> x c  )
+           --
+           --  RBI key value (node key₁ ⟪ Black , value₄ ⟫ left right) repl stack
+           --
            insertCase13 : (v : Color ∧ A ) → v ≡ value₁ → t
-           insertCase13 ⟪ Black , value₄ ⟫ refl = exit (node key₁ ⟪ Red , value₄ ⟫ left repl) (orig ∷ [])  refl record {
+           insertCase13 ⟪ Black , value₄ ⟫ refl = exit (node key₁ ⟪ Black , value₄ ⟫ left repl) (orig ∷ [])  refl record {
              tree = orig ; rot = node key₁ value₁ left (RBI.rot r) 
              ; origti = RBI.origti r
              ; origrb = RBI.origrb r
              ; treerb = RBI.origrb r
-             ; replrb = proj1 rb05
+             ; replrb = proj1 (rb05 (RBI.ri r))
              ; si = s-nil
              ; 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 = refl
-             ; repl-eq = rb07
+             ; ri = proj2 (rb05 (RBI.ri r))
              } where
-               rb07 :  black-depth (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) ≡ black-depth left ⊔ black-depth repl
-               rb07 with <-cmp key key₁
-               ... | tri< a ¬b ¬c = rb08 where   -- r : RBI key value (node key₁ ⟪ Black , value₄ ⟫ left right) repl stack
-                   rb08 : black-depth left ≡ black-depth left ⊔ black-depth repl
-                   rb08 = ?
-               ... | tri≈ ¬a b ¬c = ? where
-                   rb08 : suc (black-depth left ⊔ black-depth (RBI.rot r)) ≡ black-depth left ⊔ black-depth repl
-                   rb08 = ?
-               ... | tri> ¬a ¬b c = ? where
-                   rb08 : black-depth (RBI.rot r) ≡ black-depth left ⊔ black-depth repl
-                   rb08 = ?
                rb09 : {n : Level} {A : Set n} →  {key key1 key2 : ℕ}  {value value1  : A} {t1 t2  : bt (Color ∧ A)}
                 → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key1 ⟪ Black , value1 ⟫ t1 t2))
                 → key < key1 
                rb09 (rb-right-red x x0 x2) = x
+               rb08 : replacedTree key ⟪ Red   , value ⟫ (child-replaced key (RBI.rot r)) repl
+                   ∨  replacedTree key ⟪ Black , value ⟫ (child-replaced key (RBI.rot r)) repl
+               rb08 = RBI.ri r
                -- rb05 should more general
                tkey : {n : Level} {A : Set n } → (rbt : bt (Color ∧ A)) → ℕ
                tkey (node key value t t2) = key
@@ -972,27 +967,21 @@
                rb051 = {!!}
                rb052 : {key key₁ : ℕ} → stackInvariant key (RBI.tree r) orig stack → key < key₁
                rb052 = {!!}
-               rb05 : RBtreeInvariant (node key₁ ⟪ Red , value₄ ⟫ left repl) ∧  replacedTree 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 | <-cmp  key₁ (tkey repl) -- si and ri have key's relation 
-               ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri< a ¬b ¬c = {!!} -- need paternmatch with c 
-               ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri≈ ¬a b ¬c = {!!} -- key is unique ? 
-               ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri> ¬a ¬b c = ⊥-elim (nat-<> {!!} {!!}) --⊥-elim (¬a (rb052 {!!}))
-               ... | rb-single key₂ value₂ | refl | rb-right-red x x₁ rb | t = {!!} -- cant happen ? red - red
-               ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri< a ¬b ¬c = ⟪ rb-right-red a ? (RBI.replrb r) , {!!} ⟫ -- t₁ t₂ = leaf , c₁ = Red 
-               ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri≈ ¬a b ¬c = {!!} --rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
-               ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri> ¬a ¬b c = ⊥-elim ({!!} )
-               ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb | t = {!!} --red -red
-               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri< a ¬b ¬c = ⟪ rb-right-red a ? (RBI.replrb r) , {!!} ⟫
-               ... | rb-single key₁ value₂ | refl | rb-left-black x x₁ rb | tri≈ ¬a b ¬c = ⊥-elim (¬c {!!} ) --(rb09 (RBI.origrb r)))
-               ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri> ¬a ¬b c = {!!}
-               ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb rb₁ | t = {!!}　-- red-red
-               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb rb₁ | tri< a ¬b ¬c = {!!}
-               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb rb₁ | tri≈ ¬a b ¬c = {!!}
-               ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb rb₁ | tri> ¬a ¬b c = ⊥-elim {!!}
-               --... | rb-right-black x x₁ t | refl | rb | t = ? --⟪ proj1 {!!} , {!!} ⟫
-               --... | rb-left-black x x₁ t | refl | rb | t = {!!} --⟪ rb-node-red ? ? ? ? ? ? , ? ⟫
-               --... | rb-node-black x x₁ x₂ t x₃ t₁ | refl | rb | t = {!!}
+               rb05 : ( replacedTree key ⟪ Red   , value ⟫ (child-replaced key (RBI.rot r)) repl
+                   ∨  replacedTree key ⟪ Black , value ⟫ (child-replaced key (RBI.rot r)) repl ) 
+                   → RBtreeInvariant (node key₁ ⟪ Black , value₄ ⟫ left repl) 
+                      ∧  ( replacedTree key ⟪ Red , value ⟫
+                        (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r)) )
+                        (node key₁ ⟪ Black , value₄ ⟫ left repl)
+                        ∨
+                        replacedTree key ⟪ Black , value ⟫
+                        (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r)) )
+                        (node key₁ ⟪ Black , value₄ ⟫ left repl) )
+               rb05 (case1 ri) with <-cmp key key₁
+               ... | tri< a ¬b ¬c = ⊥-elim ( ¬c c)
+               ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c c)
+               ... | tri> ¬a ¬b c = ⟪  ? , case1 ? ⟫
+               rb05 (case2 ri) = ⟪ ? , ? ⟫
            insertCase13 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r)
            ... | Black = exit {!!} {!!} {!!} {!!} 
            ... | Red = exit {!!} {!!} {!!} {!!}