Mercurial > hg > Gears > GearsAgda

changeset 942:49ac34a645ef

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 19:56:16 +0900
parents aa28dc870715
children 03857be39158
files hoareBinaryTree2.agda
diffstat 1 files changed, 16 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree2.agda	Sat Jun 15 18:28:43 2024 +0900
+++ b/hoareBinaryTree2.agda	Sat Jun 15 19:56:16 2024 +0900
@@ -1714,9 +1714,9 @@
             ; origti = RBI.origti r
             ; origrb = RBI.origrb r
             ; treerb = rb02
-            ; replrb = ?
+            ; replrb = rb10
             ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
-            ; state = rebuild rb33 ? (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) ?
+            ; state = rebuild rb33 rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) rb11
            } rb15 where
                 -- inner case, repl  is decomposed
                 -- lt          : key < kp
@@ -1748,11 +1748,14 @@
             rb20 = proj2 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r) ) (cong proj1 rb23))
             rb03 : replacedRBTree key value (node kg _ (PG.uncle pg) (node kp _ (RBI.tree r) n1 ))
                (node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left ) (node kp ⟪ Red , proj2 vp ⟫  rp-right n1 ))
-            rb03 = rbr-rotate-rl rp-left rp-right kg kp rkey rb20 ? ?
+            rb03 = rbr-rotate-rl rp-left rp-right kg kp rkey rb20 rb21 rb04
                 (subst (λ k → replacedRBTree key value (RBI.tree r) k) (trans (sym eq) (cong (λ k → node rkey k rp-left rp-right) rb23 )) rot )
-            rb24 : ? -- node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r)) (PG.uncle pg) ≡ PG.grand pg
-            rb24 = ? -- trans (trans (cong₂ (λ j k → node kg j (node kp k n1 (RBI.tree r)) (PG.uncle pg)) rb14 rb13 ) (cong (λ k → node kg vg k (PG.uncle pg)) (sym x))) (sym x₁)
-            rb25 : ? -- node rkey ⟪ Black , proj2 vr ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg)) ≡ rb01
+            rb24 : node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) ≡ PG.grand pg
+            rb24 = ?
+             -- node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r)) (PG.uncle pg) ≡ PG.grand pg
+            -- rb24 = ? -- trans (trans (cong₂ (λ j k → node kg j (node kp k n1 (RBI.tree r)) (PG.uncle pg)) rb14 rb13 ) (cong (λ k → node kg vg k (PG.uncle pg)) (sym x))) (sym x₁)
+            rb25 : node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left) (node kp ⟪ Red , proj2 vp ⟫ rp-right n1) ≡ rb01
+                   -- node rkey ⟪ Black , proj2 vr ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg)) ≡ rb01
             rb25 = ? -- begin 
                 -- node rkey ⟪ Black , proj2 vr ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg)) 
                 --      ≡⟨ cong (λ k → node _ _ (node kp k  n1 rp-left) _ ) rb13 ⟩
@@ -1770,14 +1773,17 @@
             rb28 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r))
             rb31 : RBtreeInvariant (node rkey vr rp-left rp-right )
             rb31 = subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)
-            rb18 : black-depth rp-right ≡ black-depth (PG.uncle pg)
-            rb18 = begin
+            rb18 : black-depth (PG.uncle pg) ≡ black-depth rp-left
+            rb18 = ?
+            rb18' : black-depth rp-right ≡ black-depth (PG.uncle pg)
+            rb18' = begin
                 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 (proj1 (red-children-eq1 x pcolor rb09) ) ⟩
                 black-depth (PG.parent pg) ≡⟨ sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) x₁ rb02 )) ⟩
                 black-depth (PG.uncle pg) ∎ where open ≡-Reasoning
-            rb27 : ? -- black-depth n1 ≡ black-depth rp-left
+            rb27 : black-depth rp-right ≡ black-depth n1
+             -- 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 ⟩
@@ -1805,7 +1811,7 @@
             -- rb10 : RBtreeInvariant (node rkey ⟪ Black , proj2 vr ⟫ (node kp vp n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg)))
             -- rb10 = rb-black _ _ rb19 (rbi-from-red-black _ _ kp vp rb06 rb26 rb27 rb29 rb30 rb13) (rb-red _ _ rb20 uncle-black rb18 rb28 rb05)
             rb10 : RBtreeInvariant (node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left ) (node kp vp rp-right n1) )
-            rb10 = rb-black _ _ rb19 (rb-red _ _ uncle-black rb30 ? ? ? ) (rbi-from-red-black _ _ _ _ ? ? ? ? ? ? )
+            rb10 = rb-black _ _ rb19 (rb-red _ _ uncle-black rb30 rb18 rb05 rb26 ) (rbi-from-red-black _ _ _ _ rb28 rb06 rb27 rb20 rb16 rb13 )
             rb17 : suc (black-depth (PG.uncle pg) ⊔ black-depth rp-left ⊔ black-depth (node kp vp rp-right n1)) ≡ black-depth (PG.grand pg)
     -- rb17 : ? -- suc (black-depth (node kp vp n1 rp-left) ⊔ (black-depth rp-right ⊔ black-depth (PG.uncle pg))) ≡ black-depth (PG.grand pg)
             rb17 = ? -- begin