Mercurial > hg > Gears > GearsAgda

changeset 904:e86f6b9545fc

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 Fri, 31 May 2024 14:15:44 +0900
parents d79ffbf8f450
children acee838690c9
files hoareBinaryTree1.agda
diffstat 1 files changed, 28 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Fri May 31 12:25:36 2024 +0900
+++ b/hoareBinaryTree1.agda	Fri May 31 14:15:44 2024 +0900
@@ -933,7 +933,7 @@
    rebuild : {tree repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → black-depth repl ≡ black-depth (child-replaced key tree)
        → (rotated : replacedRBTree key value tree repl)
        → RBI-state key value tree repl stack  -- one stage up
-   rotate  : {tree repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → color repl ≡ Red → black-depth repl ≡ black-depth (child-replaced key tree)
+   rotate  : {tree repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → color repl ≡ Red → black-depth repl ≡ black-depth tree
        → (rotated : replacedRBTree key value tree repl)
        → RBI-state key value tree repl stack  -- two stages up
    top-black : {tree repl : bt (Color ∧ A) } → {stack : List (bt (Color ∧ A))}  → stack ≡ tree ∷ []
@@ -978,8 +978,23 @@
         black-depth left ⊔ black-depth right ≡⟨ cong (λ k → k ⊔ black-depth right ) (RBtreeEQ rb2) ⟩
         black-depth right ⊔ black-depth right ≡⟨ ⊔-idem _ ⟩
         black-depth right ∎ ) ⟫ where open ≡-Reasoning
+red-children-eq {n} {A} {tree} {left} {right} {key} {value} {Black} eq () rb
 
-red-children-eq {n} {A} {tree} {left} {right} {key} {value} {Black} eq () rb
+black-children-eq : {n : Level} {A : Set n}  {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color}
+   → tree ≡ node key ⟪ c , value ⟫ left right
+   → c ≡ Black 
+   → RBtreeInvariant tree
+   → (black-depth tree ≡ suc (black-depth left) ) ∧ (black-depth tree ≡ suc (black-depth right))
+black-children-eq {n} {A} {.(node key₁ ⟪ Black , value₁ ⟫ left right)} {left} {right} {.key₁} {.value₁} {Black} refl eq₁ rb2@(rb-black key₁ value₁ x rb rb₁) = 
+  ⟪ ( begin
+        suc (black-depth left ⊔ black-depth right) ≡⟨ cong (λ k → suc (black-depth left ⊔ k)) (sym (RBtreeEQ rb2)) ⟩
+        suc (black-depth left ⊔ black-depth left) ≡⟨ ⊔-idem _ ⟩
+        suc (black-depth left) ∎  ) ,  (
+     begin
+        suc (black-depth left ⊔ black-depth right) ≡⟨ cong (λ k → suc (k ⊔ black-depth right)) (RBtreeEQ rb2) ⟩
+        suc (black-depth right ⊔ black-depth right) ≡⟨ ⊔-idem _ ⟩ 
+        suc (black-depth right) ∎ ) ⟫ where open ≡-Reasoning
+black-children-eq {n} {A} {tree} {left} {right} {key} {value} {Red} eq () rb
 
 ⊔-succ : {m n : ℕ} → suc (m ⊔ n) ≡ suc m ⊔ suc n
 ⊔-succ {m} {n} = refl
@@ -1898,7 +1913,7 @@
          ; treerb = rb01
          ; replrb = rb-red _ _ refl (RBtreeToBlackColor _ rb02) rb12 (rb-black _ _ rb13 (RBI.replrb r) rb04) (RBtreeToBlack _ rb02)
          ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
-         ; 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))
+         ; state = rotate refl rb17 (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)
@@ -1947,20 +1962,21 @@
           suc (black-depth (PG.uncle pg)) ≡⟨ to-black-eq (PG.uncle pg) (cong color uneq ) ⟩
           black-depth (to-black (PG.uncle pg)) ∎
              where open ≡-Reasoning
-       rb16 : kg < key
-       rb16 = ?
-       rb14 : suc (black-depth repl ⊔ black-depth n1) ⊔ black-depth (to-black (PG.uncle pg)) ≡ black-depth (child-replaced key (PG.grand pg))
-       rb14 = begin
+       rb17 : suc (black-depth repl ⊔ black-depth n1) ⊔ black-depth (to-black (PG.uncle pg)) ≡ black-depth (PG.grand pg)
+       rb17 = begin
           suc (black-depth repl ⊔ black-depth n1) ⊔ black-depth (to-black (PG.uncle pg)) ≡⟨ cong (λ k → k ⊔ black-depth (to-black (PG.uncle pg))) rb12 ⟩
           black-depth (to-black (PG.uncle pg)) ⊔ black-depth (to-black (PG.uncle pg)) ≡⟨ ⊔-idem _ ⟩
           black-depth (to-black (PG.uncle pg)) ≡⟨ sym (to-black-eq (PG.uncle pg) (cong color uneq )) ⟩
-          suc (black-depth (PG.uncle pg)) ≡⟨ sym (cong suc ( cong  black-depth (child-replaced-right rb16 ))) ⟩
-          suc (black-depth (child-replaced key (node kg vg (PG.parent pg) (PG.uncle pg))))  ≡⟨ cong (λ k → suc (black-depth (child-replaced key k))) (sym x₁) ⟩
-          suc (black-depth (child-replaced key (PG.grand pg)))  ≡⟨ ? ⟩
-          black-depth (child-replaced key (PG.grand pg)) ∎
+          suc (black-depth (PG.uncle pg)) ≡⟨ sym ( proj2 (black-children-eq x₁ (cong proj1 rb10) rb01 )) ⟩
+          black-depth (PG.grand pg) ∎
              where open ≡-Reasoning
        rb15 : suc (length (PG.rest pg)) < length stack
-       rb15 = ?
+       rb15 = begin
+          suc (suc (length (PG.rest pg))) ≤⟨ <-trans (n<1+n _) (n<1+n _) ⟩
+          length (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) ≡⟨ cong length (sym (PG.stack=gp pg)) ⟩
+          length stack ∎
+             where open ≤-Reasoning
+