Mercurial > hg > Gears > GearsAgda

changeset 940:b2537fa14a75

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 Sat, 15 Jun 2024 00:40:16 +0900
parents 3fee93d41dc1
children aa28dc870715
files hoareBinaryTree2.agda
diffstat 1 files changed, 16 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree2.agda	Fri Jun 14 22:59:29 2024 +0900
+++ b/hoareBinaryTree2.agda	Sat Jun 15 00:40:16 2024 +0900
@@ -830,6 +830,14 @@
 black-depth-cong {n} A {node key ⟪ Black , value ⟫ left right} {node .key ⟪ Black , .value ⟫ .left .right} refl 
    = cong₂ (λ j k → suc (j ⊔ k) ) (black-depth-cong A {left} {left} refl) (black-depth-cong A {right} {right} refl)
 
+black-depth-resp  : {n : Level} (A : Set n)   (tree tree₁ : bt (Color ∧ A)) → {c1 c2 : Color}  { l1 l2 r1 r2 : bt (Color ∧ A)} {key1 key2 : ℕ} {value1 value2 : A} 
+   → tree ≡ node key1 ⟪ c1 , value1 ⟫ l1 r1 → tree₁ ≡ node key2 ⟪ c2 , value2 ⟫ l2 r2 
+   → color tree  ≡ color tree₁ 
+   → black-depth l1 ≡ black-depth l2 → black-depth r1 ≡ black-depth r2
+   → black-depth tree ≡ black-depth tree₁
+black-depth-resp  A _ _ {Black} {Black} refl refl refl eql eqr = cong₂ (λ j k → suc (j ⊔ k) ) eql eqr
+black-depth-resp  A _ _ {Red} {Red} refl refl refl eql eqr = cong₂ (λ j k → j ⊔ k ) eql eqr
+
 red-children-eq1 : {n : Level} {A : Set n}  {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color}
    → tree ≡ node key ⟪ c , value ⟫ left right
    → color tree ≡ Red
@@ -1656,33 +1664,25 @@
             rb31 = subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)
             rb18 : black-depth rp-right ≡ black-depth (PG.uncle pg)
             rb18 = begin
-                black-depth rp-right ≡⟨ sym (proj2 (red-children-eq (cong (λ k → node rkey k rp-left rp-right) rb23) refl rb31 )) ⟩
-                black-depth (node rkey vr rp-left rp-right) ≡⟨ cong black-depth eq ⟩
+                black-depth rp-right ≡⟨ sym ( proj2 (red-children-eq1 (sym eq) repl-red (RBI.replrb r) )) ⟩
                 black-depth (RBI.repl r) ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩
-                black-depth (RBI.tree r) ≡⟨ sym (proj2 (red-children-eq refl refl 
-                   (subst (λ k → RBtreeInvariant k) (trans x (cong (λ k → node kp k n1 (RBI.tree r) ) (sym rb13) )) rb09))) ⟩
-                black-depth (node kp ⟪ Red , proj2 vp ⟫  n1 (RBI.tree r)) ≡⟨ black-depth-cong _ (cong (λ k → node kp k n1 (RBI.tree r)) rb13) ⟩
-                black-depth (node kp vp n1 (RBI.tree r)) ≡⟨ black-depth-cong _ (sym x) ⟩
+                black-depth (RBI.tree r) ≡⟨ sym (proj2 (red-children-eq1 x pcolor rb09) ) ⟩
                 black-depth (PG.parent pg) ≡⟨ RBtreeEQ (subst (λ k → RBtreeInvariant k) x₁ rb02 ) ⟩
                 black-depth (PG.uncle pg) ∎ where open ≡-Reasoning
             rb27 : black-depth n1 ≡ black-depth rp-left
             rb27 = begin
                black-depth n1 ≡⟨ RBtreeEQ (subst (λ k → RBtreeInvariant k) x rb09) ⟩
                black-depth (RBI.tree r) ≡⟨ RB-repl→eq _ _ (RBI.treerb r) rot ⟩
-               black-depth (RBI.repl r) ≡⟨ cong black-depth (sym eq) ⟩
-               black-depth (node rkey vr rp-left rp-right) ≡⟨ black-depth-cong _ (cong (λ k → node rkey k rp-left rp-right) rb23) ⟩
-               black-depth (node rkey ⟪ Red , proj2 vr ⟫ rp-left rp-right) ≡⟨⟩
-               black-depth  rp-left ⊔ black-depth rp-right ≡⟨ cong (λ k → black-depth rp-left ⊔ k) (sym (RBtreeEQ rb31)) ⟩
-               black-depth  rp-left ⊔ black-depth rp-left ≡⟨ ⊔-idem _ ⟩ 
+               black-depth (RBI.repl r) ≡⟨ proj1 (red-children-eq1 (sym eq) repl-red (RBI.replrb r)) ⟩
                black-depth rp-left ∎ 
                   where open ≡-Reasoning
             rb19 : black-depth (node kp vp n1 rp-left) ≡ black-depth rp-right ⊔ black-depth (PG.uncle pg)
             rb19 = begin
-                black-depth (node kp vp n1 rp-left) ≡⟨ cong (λ k → black-depth (node kp k n1 _)) (sym rb13) ⟩
-                black-depth (node kp ⟪ Red , proj2 vp ⟫ n1 rp-left) ≡⟨⟩
-                black-depth n1 ⊔ black-depth rp-left ≡⟨ cong (λ k → k ⊔ black-depth rp-left) rb27 ⟩
-                black-depth rp-left  ⊔ black-depth rp-left ≡⟨ ⊔-idem _ ⟩
-                black-depth rp-left ≡⟨ RBtreeEQ rb31 ⟩
+                black-depth (node kp vp n1 rp-left) ≡⟨ black-depth-resp A (node kp vp n1 rp-left) (node kp vp rp-left rp-left)  refl refl refl rb27 refl ⟩
+                black-depth (node kp vp rp-left rp-left) ≡⟨ black-depth-resp A (node kp vp rp-left rp-left) (node rkey vr rp-left rp-right) 
+                     refl refl (trans (sym (cong proj1 rb13)) (sym (cong proj1 rb23))) refl (RBtreeEQ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r))) ⟩
+                black-depth (node rkey vr rp-left rp-right) ≡⟨ black-depth-cong A eq ⟩
+                black-depth (RBI.repl r) ≡⟨ proj2 (red-children-eq1 (sym eq) repl-red (RBI.replrb r)) ⟩
                 black-depth rp-right ≡⟨ sym ( ⊔-idem _ ) ⟩
                 black-depth rp-right ⊔ black-depth rp-right ≡⟨ cong (λ k → black-depth rp-right ⊔ k) rb18 ⟩
                 black-depth rp-right ⊔ black-depth (PG.uncle pg) ∎