Mercurial > hg > Gears > GearsAgda
changeset 926:9936101bc974
child-replaced on grand parent is no good
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 08 Jun 2024 08:52:35 +0900 |
| parents | 9a67eb8e71ac |
| children | 455981850269 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 9 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Sat Jun 08 07:46:23 2024 +0900 +++ b/hoareBinaryTree1.agda Sat Jun 08 08:52:35 2024 +0900 @@ -950,9 +950,10 @@ → ¬ ( tree ≡ leaf) → (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 tree - → (rotated : replacedRBTree key value tree repl) - → RBI-state key value tree repl stack -- two stages up + rotate : (tree : bt (Color ∧ A)) → {child repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → color repl ≡ Red + → child ≡ child-replaced key tree + → (rotated : replacedRBTree key value child repl) + → RBI-state key value child repl stack -- two stages up top-black : {tree repl : bt (Color ∧ A) } → {stack : List (bt (Color ∧ A))} → stack ≡ tree ∷ [] → (rotated : replacedRBTree key value tree repl ∨ replacedRBTree key value (to-black tree) repl) → RBI-state key value tree repl stack @@ -1753,7 +1754,7 @@ ; treerb = rb-leaf ; replrb = rb-red key value refl refl refl rb-leaf rb-leaf ; si = subst (λ k → stackInvariant key k leaf _ ) crbt01 si - ; state = rotate refl refl rbr-leaf + ; state = rotate leaf refl refl rbr-leaf } where crbt01 : tree ≡ leaf crbt01 with si-property-last _ _ _ _ si | si-property1 si @@ -1792,7 +1793,7 @@ ; treerb = rb-leaf ; replrb = rb-red key value refl refl refl rb-leaf rb-leaf ; si = si - ; state = rotate refl refl rbr-leaf + ; state = rotate leaf refl refl rbr-leaf } crbt00 (node key₁ value₁ left right ) (case1 eq) refl = ⊥-elim (bt-ne (sym eq)) crbt00 (node key₁ value₁ left right ) (case2 eq) refl with si-property-last _ _ _ _ si | si-property1 si @@ -2124,7 +2125,7 @@ rb00 : RBI.tree r ≡ orig rb00 with si-property-last _ _ _ _ (subst (λ k → stackInvariant key (RBI.tree r) orig k) (eq) (RBI.si r)) ... | refl = refl - ... | rotate repl-red pdepth-eq rot with stackToPG (RBI.tree r) orig stack (RBI.si r) + ... | rotate _ repl-red childeq rot with stackToPG (RBI.tree r) orig stack (RBI.si r) ... | case1 eq = exit stack eq r -- no stack, replace top node ... | case2 (case1 eq) = insertCase4 orig refl eq rot (case1 repl-red) (RBI.si r) -- one level stack, orig is parent of repl ... | case2 (case2 pg) with color (PG.parent pg) in pcolor @@ -2167,7 +2168,7 @@ where open ≡-Reasoning rb05 : proj1 vp ≡ Black → black-depth rb01 ≡ black-depth (PG.parent pg) rb05 refl = begin - suc (black-depth repl ⊔ black-depth n1) ≡⟨ cong suc (cong (λ k → k ⊔ black-depth n1) pdepth-eq) ⟩ + suc (black-depth repl ⊔ black-depth n1) ≡⟨ cong suc (cong (λ k → k ⊔ black-depth n1) (sym (RB-repl→eq _ _ (RBI.treerb r) rot))) ⟩ suc (black-depth (RBI.tree r) ⊔ black-depth n1) ≡⟨ refl ⟩ black-depth (node kp vp (RBI.tree r) n1) ≡⟨ cong black-depth (sym x) ⟩ black-depth (PG.parent pg) ∎ @@ -2196,7 +2197,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 rb17 (subst₂ (λ j k → replacedRBTree key value j k ) (sym rb09) refl (rbr-flip-ll repl-red (rb05 refl uneq) rb06 rot)) + ; state = rotate ? refl ? (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)