Mercurial > hg > Gears > GearsAgda

changeset 900:2fea300378ca

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 Thu, 30 May 2024 18:15:36 +0900
parents 58954abea83e
children e70abd8f17a9
files hoareBinaryTree1.agda
diffstat 1 files changed, 69 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Thu May 30 08:06:22 2024 +0900
+++ b/hoareBinaryTree1.agda	Thu May 30 18:15:36 2024 +0900
@@ -147,30 +147,33 @@
 si-property2 (.leaf ∷ []) (s-left _ _ tree₁ x ()) refl
 si-property2 (x₁ ∷ x₂ ∷ stack) (s-left _ _ tree₁ x si) eq = si-property2 (x₂ ∷ stack) si eq
 
-si-property-< :  {n : Level} {A : Set n} {key key₁ kp : ℕ} {value₁ value₂ : A} {tree orig tree₁ tree₂ tree₃ : bt A} → {stack  : List (bt A)}
-   → tree ≡ node key₁ value₁ tree₁ tree₂
+si-property-< :  {n : Level} {A : Set n} {key kp : ℕ} {value₂ : A} {tree orig tree₃ : bt A} → {stack  : List (bt A)}
+   → ¬ ( tree ≡ leaf )
    → treeInvariant (node kp value₂ tree  tree₃ )
    → stackInvariant key tree orig (tree ∷ node kp value₂ tree  tree₃ ∷ stack)
    → key < kp
-si-property-< refl (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x s-nil) = ⊥-elim (nat-<> x₁ x₂)
-si-property-< refl (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x (s-right .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree₁ x₇ si)) = ⊥-elim (nat-<> x₁ x₂)
-si-property-< refl (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x (s-left .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree x₇ si)) = ⊥-elim (nat-<> x₁ x₂)
-si-property-< refl (t-left _ _ x₁ x₂ x₃ ti) (s-left .(node _ _ _ _) _ .leaf x s-nil) = x
-si-property-< refl (t-node _ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-left .(node _ _ _ _) _ .(node key₂ _ _ _) x s-nil) = x
-si-property-< refl ti (s-left .(node _ _ _ _) _ tree x (s-right .(node _ _ (node _ _ _ _) tree) _ tree₁ x₁ si)) = x
-si-property-< refl ti (s-left .(node _ _ _ _) _ tree x (s-left .(node _ _ (node _ _ _ _) tree) _ tree₁ x₁ si)) = x
+si-property-< ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x s-nil) = ⊥-elim (nat-<> x₁ x₂)
+si-property-< ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x (s-right .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree₁ x₇ si)) = ⊥-elim (nat-<> x₁ x₂)
+si-property-< ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x (s-left .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree x₇ si)) = ⊥-elim (nat-<> x₁ x₂)
+si-property-< ne ti (s-left _ _ _ x (s-right .(node _ _ _ _) _ tree₁ x₁ si)) = x
+si-property-< ne ti (s-left _ _ _ x (s-left .(node _ _ _ _) _ tree₁ x₁ si)) = x
+si-property-< ne ti (s-left _ _ _ x s-nil) = x
+si-property-< ne (t-single _ _) (s-right _ _ tree₁ x si) = ⊥-elim ( ne refl )
 
-si-property-> :  {n : Level} {A : Set n} {key key₁ kp : ℕ} {value₁ value₂ : A} {tree orig tree₁ tree₂ tree₃ : bt A} → {stack  : List (bt A)}
-   → tree ≡ node key₁ value₁ tree₁ tree₂
+si-property-> :  {n : Level} {A : Set n} {key kp : ℕ} {value₂ : A} {tree orig tree₃ : bt A} → {stack  : List (bt A)}
+   → ¬ ( tree ≡ leaf )
    → treeInvariant (node kp value₂ tree₃  tree )
    → stackInvariant key tree orig (tree ∷ node kp value₂ tree₃  tree ∷ stack)
    → kp < key
-si-property-> refl ti (s-right .(node _ _ _ _) _ tree₁ x s-nil) = x
-si-property-> refl ti (s-right .(node _ _ _ _) _ tree₁ x (s-right .(node _ _ tree₁ (node _ _ _ _)) _ tree₂ x₁ si)) = x
-si-property-> refl ti (s-right .(node _ _ _ _) _ tree₁ x (s-left .(node _ _ tree₁ (node _ _ _ _)) _ tree x₁ si)) = x
-si-property-> refl (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-left .(node _ _ _ _) _ .(node _ _ _ _) x s-nil) = ⊥-elim (nat-<> x₁ x₂)
-si-property-> refl (t-node _ _ _ x₂ x₃ x₄ x₅ x₆ x₇ ti ti₁) (s-left .(node _ _ _ _) _ .(node _ _ _ _) x (s-right .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree₁ x₁ si)) = ⊥-elim (nat-<> x₂ x₃)
-si-property-> refl (t-node _ _ _ x₂ x₃ x₄ x₅ x₆ x₇ ti ti₁) (s-left .(node _ _ _ _) _ .(node _ _ _ _) x (s-left .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree x₁ si)) = ⊥-elim (nat-<> x₂ x₃)
+si-property-> ne ti (s-right _ _ tree₁ x s-nil) = x
+si-property-> ne ti (s-right _ _ tree₁ x (s-right .(node _ _ tree₁ _) _ tree₂ x₁ si)) = x
+si-property-> ne ti (s-right _ _ tree₁ x (s-left .(node _ _ tree₁ _) _ tree x₁ si)) = x
+si-property-> ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-left _ _ _ x s-nil) = ⊥-elim (nat-<> x₁ x₂)
+si-property-> ne (t-node _ _ _ x₂ x₃ x₄ x₅ x₆ x₇ ti ti₁) (s-left _ _ _ x (s-right .(node _ _ _ _) _ tree₁ x₁ si)) = ⊥-elim (nat-<> x₂ x₃)
+si-property-> ne (t-node _ _ _ x₂ x₃ x₄ x₅ x₆ x₇ ti ti₁) (s-left _ _ _ x (s-left .(node _ _ _ _) _ tree x₁ si)) = ⊥-elim (nat-<> x₂ x₃)
+si-property-> ne (t-single _ _) (s-left _ _ _ x s-nil) = ⊥-elim ( ne refl )
+si-property-> ne (t-single _ _) (s-left _ _ _ x (s-right .(node _ _ leaf leaf) _ tree₁ x₁ si)) = ⊥-elim ( ne refl )
+si-property-> ne (t-single _ _) (s-left _ _ _ x (s-left .(node _ _ leaf leaf) _ tree x₁ si)) = ⊥-elim ( ne refl )
 
 si-property-last :  {n : Level} {A : Set n}  (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) →  stackInvariant key tree tree0 stack
    → stack-last stack ≡ just tree0
@@ -744,6 +747,18 @@
 RBtreeToBlackColor (node key ⟪ Red , value ⟫ left right) (rb-red _ _ x x₁ x₂ rb rb₁) = refl
 RBtreeToBlackColor (node key ⟪ Black , value ⟫ left right) (rb-black _ _ x rb rb₁) = refl
 
+RBtreeParentColorBlack : {n : Level} {A : Set n} → (left right  : bt (Color ∧ A)) { value : A} {key : ℕ} { c : Color}
+ → RBtreeInvariant (node key ⟪ c , value ⟫ left right)
+ → (color left ≡ Red) ∨ (color right ≡ Red) 
+ → c ≡ Black
+RBtreeParentColorBlack leaf leaf (rb-red _ _ x₁ x₂ x₃ x₄ x₅) (case1 ())
+RBtreeParentColorBlack leaf leaf (rb-red _ _ x₁ x₂ x₃ x₄ x₅) (case2 ())
+RBtreeParentColorBlack (node key ⟪ Red , proj4 ⟫ left left₁) right (rb-red _ _ () x₁ x₂ rb rb₁) (case1 x₃)
+RBtreeParentColorBlack (node key ⟪ Black , proj4 ⟫ left left₁) right (rb-red _ _ x x₁ x₂ rb rb₁) (case1 ())
+RBtreeParentColorBlack left (node key ⟪ Red , proj4 ⟫ right right₁) (rb-red _ _ x () x₂ rb rb₁) (case2 x₃)
+RBtreeParentColorBlack left (node key ⟪ Black , proj4 ⟫ right right₁) (rb-red _ _ x x₁ x₂ rb rb₁) (case2 ())
+RBtreeParentColorBlack left right (rb-black _ _ x rb rb₁) x₃ = refl
+
 --
 --  findRBT exit with replaced node
 --     case-eq        node value is replaced,  just do replacedTree and rebuild rb-invariant
@@ -898,6 +913,7 @@
 record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A)))  : Set n where
    field
        tree : bt (Color ∧ A)
+       ¬leaf : ¬ ( tree ≡ leaf )
        origti : treeInvariant orig
        origrb : RBtreeInvariant orig
        treerb : RBtreeInvariant tree     -- tree node te be replaced
@@ -1763,6 +1779,7 @@
     insertCase12  tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ | child-replaced key (node key₁ value₁ left right) in creq
     ... | tri< a ¬b ¬c | cr = exit (to-black (node key₁ value₁ repl right)) (orig ∷ []) refl record {
          tree = orig
+         ; ¬leaf = ?
          ; origti = RBI.origti r
          ; origrb = RBI.origrb r
          ; treerb = RBI.origrb r
@@ -1795,6 +1812,7 @@
        rb06 (.left ∷ node key₁ value₁ left right ∷ []) refl (s-left .left .(node key₁ value₁ left right) .right x s-nil) eq = ⊥-elim ( nat-≡< eq x)
     ... | tri> ¬a ¬b c | cr = exit (to-black (node key₁ value₁ left repl)) (orig ∷ [])  refl record {
          tree = orig
+         ; ¬leaf = ?
          ; origti = RBI.origti r
          ; origrb = RBI.origrb r
          ; treerb = RBI.origrb r
@@ -1827,13 +1845,14 @@
 ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = next (to-red (node kg vg (to-black (node kp vp repl n1)) (to-black (PG.uncle pg)))) (PG.grand pg ∷ (PG.rest pg))
     record {
          tree = PG.grand pg
+         ; ¬leaf = subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())
          ; origti = RBI.origti r
          ; origrb = RBI.origrb r
          ; treerb = rb01
-         ; replrb = rb-red _ _ refl (RBtreeToBlackColor _ rb02) ? (rb-black _ _ ? (RBI.replrb r) rb04) (RBtreeToBlack _ rb02)
+         ; replrb = rb-red _ _ refl (RBtreeToBlackColor _ rb02) rb12 (rb-black _ _ rb13 (RBI.replrb r) rb04) (RBtreeToBlack _ rb02)
          ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
-         ; state = rotate refl ? (subst₂ (λ j k → replacedRBTree key value j k ) (sym ?) refl  (rbr-flip-ll repl-red (rb05 refl uneq) ? rot))
-     }  ? where
+         ; state = rotate refl rb14 (subst₂ (λ j k → replacedRBTree key value j k ) (sym rb09) refl  (rbr-flip-ll repl-red (rb05 refl uneq) rb06 rot))
+     }  rb15 where
        rb00 : stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
        rb00 = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r)
        rb01 :  RBtreeInvariant (PG.grand pg)
@@ -1849,9 +1868,37 @@
        rb08 : treeInvariant (PG.parent pg)
        rb08 = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00)
        rb07 : treeInvariant (node kp vp (RBI.tree r) n1)
-       rb07 = ?
+       rb07 = subst (λ k → treeInvariant k) x (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00))
        rb06 : key < kp
-       rb06 = si-property-< ? rb07 (subst (λ k → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x rb00)
+       rb06 = si-property-< (RBI.¬leaf r) rb07 (subst (λ k → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x rb00)
+       rb10 : vg ≡ ⟪ Black , proj2 vg ⟫
+       rb10 with RBtreeParentColorBlack _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) (case1 pcolor)
+       ... | refl = refl
+       rb11 : vp ≡ ⟪ Red , proj2 vp ⟫
+       rb11 with subst (λ k → color k ≡ Red) x pcolor
+       ... | refl = refl
+       rb09 : PG.grand pg ≡ node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) (PG.uncle pg)
+       rb09 = begin
+           PG.grand pg ≡⟨ x₁ ⟩
+           node kg vg (PG.parent pg) (PG.uncle pg) ≡⟨ cong (λ k → node kg vg k (PG.uncle pg)) x ⟩
+           node kg vg (node kp vp (RBI.tree r) n1) (PG.uncle pg) ≡⟨ cong₂ (λ j k → node kg j (node kp k (RBI.tree r) n1) (PG.uncle pg)) rb10 rb11  ⟩
+           node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) (PG.uncle pg) ∎
+             where open ≡-Reasoning
+       rb13 : black-depth repl ≡ black-depth n1
+       rb13 = begin
+          black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩
+          black-depth (RBI.tree r) ≡⟨ RBtreeEQ (subst (λ k → RBtreeInvariant k) x rb03) ⟩
+          black-depth n1 ∎
+             where open ≡-Reasoning
+       rb12 : suc (black-depth repl ⊔ black-depth n1) ≡ black-depth (to-black (PG.uncle pg))
+       rb12 = ?
+       rb14 : suc (black-depth repl ⊔ black-depth n1) ⊔ black-depth (to-black (PG.uncle pg)) ≡ black-depth (child-replaced key (PG.grand pg))
+       rb14 = ?
+       rb15 : suc (length (PG.rest pg)) < length stack
+       rb15 = ?
+
+          
+
 ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
 ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
 ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}