Mercurial > hg > Gears > GearsAgda

changeset 921:46ec01e94947

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 Wed, 05 Jun 2024 14:42:54 +0900
parents 368b9be0b312
children 5fb90d662aa4
files hoareBinaryTree1.agda
diffstat 1 files changed, 89 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Wed Jun 05 09:54:19 2024 +0900
+++ b/hoareBinaryTree1.agda	Wed Jun 05 14:42:54 2024 +0900
@@ -1744,9 +1744,13 @@
    rp01 : t
    rp01 with PG.pg pg
    ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ with <-cmp key kp | proj1 vp in pcolor 
-   ... | tri< a ¬b ¬c | Red = rotateCase1 where
-       rotateCase1 : t
-       rotateCase1 = exit (PG.grand pg ∷ PG.rest pg) record {
+   ... | tri< a ¬b ¬c | Red = buildCase1 tree refl P where
+       rb04 : proj1 vp ≡ Red → ⟪ Red , proj2 vp ⟫ ≡ vp
+       rb04 refl = refl
+       rb07 : key < kp
+       rb07 = a
+       buildCase1 : (tree1 : bt (Color ∧ A)) → tree1 ≡ tree → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) → t
+       buildCase1 leaf refl (case1 refl) = exit (PG.grand pg ∷ PG.rest pg) record {
              tree = PG.grand pg
            ; repl = to-red ( node kg vg (to-black (node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1)) n2 )
            ; origti = ti
@@ -1755,30 +1759,44 @@
            ; replrb = rb-red _ ? ? ? ? ? ? 
            ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
            ; state = rotate ? ? ? ? }
-   ... | tri< a ¬b ¬c | Black = buildCase1 where
-       rb01 : bt (Color ∧ A)
-       rb01 = node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1
-       rb03 : ? -- 1 ≡ black-depth n1
-       rb03 = ? -- RBtreeEQ (subst (λ k → RBtreeInvariant k) x treerb)
-       rb02 : RBtreeInvariant (node kp ⟪ Black , proj2 vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) n1)
-       rb02 = rb-black kp (proj2 vp) rb03 (rb-red _ _ refl refl refl rb-leaf rb-leaf) (RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x treerb))
+       buildCase1 (node key₁ ⟪ c₁ , value₁ ⟫ left right) refl (case2 refl) = exit (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
+             tree = PG.parent pg
+           ; repl = rb01
+           ; origti = ti
+           ; origrb = rbi
+           ; treerb = PGtoRBinvariant1 _ orig rbi _ (popStackInvariant _ _ _ _ _ rb00)
+           ; replrb = subst (λ k → RBtreeInvariant k) (cong (λ k → node kp k _ n1) (rb04 pcolor)) rb11
+           ; si = popStackInvariant _ _ _ _ _ rb00
+           ; state = rebuild  (cong color x) rb06 (subst (λ k → replacedRBTree key value k _) (sym x) (rbr-left refl rb07 rbr-node )) } where
+              rb01 : bt (Color ∧ A)
+              rb01 = node kp vp (node key ⟪ c₁ , value ⟫ left right) n1
+              rb08 : black-depth (node key₁ ⟪ c₁ , value₁ ⟫ left right) ≡ black-depth n1
+              rb08 = RBtreeEQ (subst (λ k → RBtreeInvariant k) x treerb)
+              rb09 : (c₁ : Color ) → black-depth (node key₁ ⟪ c₁ , value ⟫ left right) ≡ black-depth (node key₁ ⟪ c₁ , value₁ ⟫ left right) 
+              rb09 Red = refl
+              rb09 Black = refl
+              rb03 : black-depth (node key₁ ⟪ c₁ , value ⟫ left right) ≡ black-depth n1
+              rb03 = trans (rb09 c₁) rb08
+              rb05 : RBtreeInvariant (node key ⟪ c₁ , value ⟫ left right) 
+              rb05 with RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x treerb)  
+              ... | rb-red _ _ x₁ x₂ x₃ t t₁ = rb-red _ value x₁ x₂ x₃ t t₁
+              ... | rb-black _ _ x₁ t t₁ = rb-black _ value x₁ t t₁
+              rb10 : (vp :  Color ∧ A) → black-depth (node kp vp (node key₁ ⟪ c₁ , value  ⟫ left right) n1) 
+                                       ≡ black-depth (node kp vp (node key₁ ⟪ c₁ , value₁ ⟫ left right) n1)
+              rb10 ⟪ Red , _ ⟫ = cong (λ k → k ⊔ black-depth n1 ) (rb09 c₁)
+              rb10 ⟪ Black , _ ⟫ = cong (λ k → suc (k ⊔ black-depth n1 )) (rb09 c₁)
+              rb06 : black-depth rb01 ≡ black-depth (PG.parent pg)
+              rb06 = trans (rb10 vp) (cong black-depth (sym x)) 
+              rb11 : RBtreeInvariant (node kp ⟪ Red , proj2 vp ⟫ (node key₁ ⟪ c₁ , value ⟫ left right) n1)
+              rb11 with subst (λ k → RBtreeInvariant k) x treerb
+              ... | rb-red .kp value₂ x x₁ x₂ t t₁ = rb-red kp value₂ x x₁ rb03 rb05 t₁
+   ... | tri< a ¬b ¬c | Black = buildCase1 tree refl P where
        rb04 : proj1 vp ≡ Black → ⟪ Black , proj2 vp ⟫ ≡ vp
        rb04 refl = refl
-       rb05 : black-depth rb01 ≡ black-depth (PG.parent pg)
-       rb05 = begin 
-           black-depth (node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1) ≡⟨ cong (λ k → black-depth (node kp k _ n1)) (sym (rb04 pcolor)) ⟩
-           black-depth (node kp ⟪ Black , proj2 vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) n1) ≡⟨ refl  ⟩
-           black-depth (node kp ⟪ Black , proj2 vp ⟫  leaf n1 )  ≡⟨ cong (λ k → black-depth (node kp k leaf n1)) (rb04 pcolor) ⟩
-           black-depth (node kp vp leaf n1)  ≡⟨ ? ⟩
-           black-depth (PG.parent pg) ∎ where 
-              open ≡-Reasoning
        rb07 : key < kp
-       rb07 = si-property-<  ? (subst (λ k → treeInvariant k) x pti) (subst₂ (λ j k → stackInvariant key j orig k) refl (trans (PG.stack=gp pg) ? ) si)
-       rb06 : replacedRBTree key value (PG.parent pg) (node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1)
-       rb06 = ? -- subst₂ (λ j k → replacedRBTree key value k  (node kp j (node key ⟪ Red , value ⟫ leaf leaf) n1)) (rb04 pcolor) 
-           -- (trans (cong (λ k → node kp k leaf n1) (rb04 pcolor)) (sym x)) ( rbr-black-left refl rb07 rbr-leaf )
-       buildCase1 : t
-       buildCase1 = exit (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
+       rb07 = a
+       buildCase1 : (tree1 : bt (Color ∧ A)) → tree1 ≡ tree → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) → t
+       buildCase1 leaf refl (case1 refl) = exit (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
              tree = PG.parent pg
            ; repl = rb01
            ; origti = ti
@@ -1786,7 +1804,53 @@
            ; treerb = PGtoRBinvariant1 _ orig rbi _ (popStackInvariant _ _ _ _ _ rb00)
            ; replrb = subst (λ k → RBtreeInvariant k) (cong (λ k → node kp k (node key ⟪ Red , value ⟫ leaf leaf) n1) (rb04 pcolor))  rb02
            ; si = popStackInvariant _ _ _ _ _ rb00
-           ; state = rebuild  (cong color x) rb05 rb06 } 
+           ; state = rebuild  (cong color x) rb05 rb06 } where
+           rb01 : bt (Color ∧ A)
+           rb01 = node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1
+           rb03 : 1 ≡ black-depth n1
+           rb03 = RBtreeEQ (subst (λ k → RBtreeInvariant k) x treerb)
+           rb02 : RBtreeInvariant (node kp ⟪ Black , proj2 vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) n1)
+           rb02 = rb-black kp (proj2 vp) rb03 (rb-red _ _ refl refl refl rb-leaf rb-leaf) (RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x treerb))
+           rb06 : replacedRBTree key value (PG.parent pg) (node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1)
+           rb06 = subst₂ (λ j k → replacedRBTree key value k  (node kp j (node key ⟪ Red , value ⟫ leaf leaf) n1)) (rb04 pcolor) 
+               (trans (cong (λ k → node kp k leaf n1) (rb04 pcolor)) (sym x)) ( rbr-black-left refl rb07 rbr-leaf )
+           rb05 : black-depth rb01 ≡ black-depth (PG.parent pg)
+           rb05 = begin 
+               black-depth (node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1) ≡⟨ cong (λ k → black-depth (node kp k _ n1)) (sym (rb04 pcolor)) ⟩
+               black-depth (node kp ⟪ Black , proj2 vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) n1) ≡⟨ refl  ⟩
+               black-depth (node kp ⟪ Black , proj2 vp ⟫  leaf n1 )  ≡⟨ cong (λ k → black-depth (node kp k leaf n1)) (rb04 pcolor) ⟩
+               black-depth (node kp vp leaf n1)  ≡⟨ cong black-depth (sym x) ⟩
+               black-depth (PG.parent pg) ∎ where 
+                  open ≡-Reasoning
+       buildCase1 (node key₁ ⟪ c₁ , value₁ ⟫ left right) refl (case2 refl) = exit (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
+             tree = PG.parent pg
+           ; repl = rb01
+           ; origti = ti
+           ; origrb = rbi
+           ; treerb = PGtoRBinvariant1 _ orig rbi _ (popStackInvariant _ _ _ _ _ rb00)
+           ; replrb = subst (λ k → RBtreeInvariant k) (cong (λ k → node kp k _ n1) (rb04 pcolor)) (rb-black _ _ rb03
+              rb05 (RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x treerb)))
+           ; si = popStackInvariant _ _ _ _ _ rb00
+           ; state = rebuild  (cong color x) rb06 (subst (λ k → replacedRBTree key value k _) (sym x) (rbr-left refl rb07 rbr-node )) } where
+              rb01 : bt (Color ∧ A)
+              rb01 = node kp vp (node key ⟪ c₁ , value ⟫ left right) n1
+              rb08 : black-depth (node key₁ ⟪ c₁ , value₁ ⟫ left right) ≡ black-depth n1
+              rb08 = RBtreeEQ (subst (λ k → RBtreeInvariant k) x treerb)
+              rb09 : (c₁ : Color ) → black-depth (node key₁ ⟪ c₁ , value ⟫ left right) ≡ black-depth (node key₁ ⟪ c₁ , value₁ ⟫ left right) 
+              rb09 Red = refl
+              rb09 Black = refl
+              rb03 : black-depth (node key₁ ⟪ c₁ , value ⟫ left right) ≡ black-depth n1
+              rb03 = trans (rb09 c₁) rb08
+              rb05 : RBtreeInvariant (node key ⟪ c₁ , value ⟫ left right) 
+              rb05 with RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x treerb)  
+              ... | rb-red _ _ x₁ x₂ x₃ t t₁ = rb-red _ value x₁ x₂ x₃ t t₁
+              ... | rb-black _ _ x₁ t t₁ = rb-black _ value x₁ t t₁
+              rb06 : black-depth rb01 ≡ black-depth (PG.parent pg)
+              rb06 = trans (rb10 vp) (cong black-depth (sym x)) where
+                  rb10 : (vp :  Color ∧ A) → black-depth (node kp vp (node key₁ ⟪ c₁ , value  ⟫ left right) n1) 
+                                           ≡ black-depth (node kp vp (node key₁ ⟪ c₁ , value₁ ⟫ left right) n1)
+                  rb10 ⟪ Red , _ ⟫ = cong (λ k → k ⊔ black-depth n1 ) (rb09 c₁)
+                  rb10 ⟪ Black , _ ⟫ = cong (λ k → suc (k ⊔ black-depth n1 )) (rb09 c₁)
    ... | tri≈ ¬a b ¬c | t = ⊥-elim ( si-property-pne _ _ stack (trans (PG.stack=gp pg) (cong (λ k → tree ∷ k ∷ _) x) ) si b )
    ... | tri> ¬a ¬b c | t = ?
    rp01 | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}