Mercurial > hg > Gears > GearsAgda
changeset 956:bfc7007177d0 default tip
safe and cubical compatible with no warning done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 19 Oct 2024 09:48:48 +0900 |
| parents | 415915a840fe |
| children | |
| files | BTree.agda RBTree.agda |
| diffstat | 2 files changed, 227 insertions(+), 39 deletions(-) [+] |
line wrap: on
line diff
--- a/BTree.agda Fri Oct 18 21:03:55 2024 +0900 +++ b/BTree.agda Sat Oct 19 09:48:48 2024 +0900 @@ -344,11 +344,21 @@ si-property-pne {_} {_} {key} {key₁} {value₁} tree .tree {left} {right} .(tree ∷ []) () s-nil eq --- si-property-parent-node : {n : Level} {A : Set n} {key : ℕ} (tree orig : bt A) {x : bt A} --- → (stack : List (bt A)) {rest : List (bt A)} --- → stackInvariant key tree orig stack --- → ¬ ( stack ≡ x ∷ leaf ∷ rest ) --- si-property-parent-node {n} {A} tree orig = ? +si-property-parent-node : {n : Level} {A : Set n} {key : ℕ} (tree orig : bt A) {x : bt A} + → (stack : List (bt A)) {rest : List (bt A)} + → stackInvariant key tree orig stack + → ¬ ( stack ≡ x ∷ leaf ∷ rest ) +si-property-parent-node {n} {A} tree .tree .(tree ∷ []) s-nil () +si-property-parent-node {n} {A} tree .(node _ _ tree₁ tree) .(tree ∷ node _ _ tree₁ tree ∷ []) (s-right .tree .(node _ _ tree₁ tree) tree₁ x s-nil) () +si-property-parent-node {n} {A} tree orig .(tree ∷ node _ _ tree₁ tree ∷ _) (s-right .tree .orig tree₁ x (s-right .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) eq + = ⊥-elim ( bt-ne (sym (∷-injectiveˡ (∷-injectiveʳ eq)) )) +si-property-parent-node {n} {A} tree orig .(tree ∷ node _ _ tree₁ tree ∷ _) (s-right .tree .orig tree₁ x (s-left .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) eq + = ⊥-elim ( bt-ne (sym (∷-injectiveˡ (∷-injectiveʳ eq)) )) +si-property-parent-node {n} {A} tree .(node _ _ tree tree₁) .(tree ∷ node _ _ tree tree₁ ∷ []) (s-left .tree .(node _ _ tree tree₁) tree₁ x s-nil) () +si-property-parent-node {n} {A} tree orig .(tree ∷ node _ _ tree tree₁ ∷ _) (s-left .tree .orig tree₁ x (s-right .(node _ _ tree tree₁) .orig tree₂ x₁ si)) eq + = ⊥-elim ( bt-ne (sym (∷-injectiveˡ (∷-injectiveʳ eq)) )) +si-property-parent-node {n} {A} tree orig .(tree ∷ node _ _ tree tree₁ ∷ _) (s-left .tree .orig tree₁ x (s-left .(node _ _ tree tree₁) .orig tree₂ x₁ si)) eq + = ⊥-elim ( bt-ne (sym (∷-injectiveˡ (∷-injectiveʳ eq)) )) rt-property1 : {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
--- a/RBTree.agda Fri Oct 18 21:03:55 2024 +0900 +++ b/RBTree.agda Sat Oct 19 09:48:48 2024 +0900 @@ -92,7 +92,100 @@ → stackInvariant key tree1 tree0 stack → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → (exit : (stack : List ( bt (Color ∧ A))) (r : RBI key value tree0 stack ) → t ) → t -createRBT {n} {m} {A} {t} key value orig rbi ti tree = ? +createRBT {n} {m} {A} {t} key value orig rbi ti tree [] si P exit = ⊥-elim (si-property0 si refl ) +createRBT {n} {m} {A} {t} key value orig rbi ti tree (x ∷ []) si P exit = crbt00 orig P refl where + crbt00 : (tree1 : bt (Color ∧ A)) → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) → tree1 ≡ orig → t + crbt00 leaf P eq = exit (x ∷ []) record { + tree = leaf + ; repl = node key ⟪ Red , value ⟫ leaf leaf + ; origti = ti + ; origrb = rbi + ; treerb = rb-leaf + ; replrb = rb-red key value refl refl refl rb-leaf rb-leaf + ; replti = t-single key _ + ; si = subst (λ k → stackInvariant key k orig _) crbt01 si + ; state = rotate leaf refl rbr-leaf + } where + crbt01 : tree ≡ leaf + crbt01 with si-property-last _ _ _ _ si | si-property1 si + ... | eq3 | eq4 = trans (sym eq4) (trans (just-injective eq3) (sym eq)) + crbt00 (node key₁ value₁ left right ) (case1 eq) eq1 with si-property-last _ _ _ _ si | si-property1 si + ... | eq2 | eq3 = ⊥-elim (bt-ne (trans (sym eq) (trans (trans (sym eq3) (just-injective eq2) ) (sym eq1) ))) + crbt00 (node key₁ value₁ left right ) (case2 eq) eq1 with si-property-last _ _ _ _ si | si-property1 si + ... | eq2 | eq3 = exit (x ∷ []) record { + tree = node key₁ value₁ left right + ; repl = node key₁ ⟪ proj1 value₁ , value ⟫ left right + ; origti = ti + ; origrb = rbi + ; treerb = subst (λ k → RBtreeInvariant k) (sym eq1) rbi + ; replrb = crbt03 value₁ refl (subst (λ k → RBtreeInvariant k) (sym eq1) rbi) + ; replti = replaceTree1 _ _ _ (subst (λ k → treeInvariant k) (sym eq1) ti) + ; si = subst (λ k → stackInvariant key k orig _) (trans (trans (sym eq3) (just-injective eq2)) (sym eq1)) si + ; state = rebuild refl (crbt01 value₁ ) (λ ()) crbt04 + } where + crbt01 : (value₁ : Color ∧ A) → black-depth (node key₁ ⟪ proj1 value₁ , value ⟫ left right) ≡ black-depth (node key₁ value₁ left right) + crbt01 ⟪ Red , proj4 ⟫ = refl + crbt01 ⟪ Black , proj4 ⟫ = refl + crbt03 : {tree : bt (Color ∧ A)} → (value₁ : Color ∧ A) → tree ≡ (node key₁ value₁ left right) → RBtreeInvariant tree + → RBtreeInvariant (node key₁ ⟪ proj1 value₁ , value ⟫ left right) + crbt03 v1 () rb-leaf + crbt03 v1 eq (rb-red key₂ value₂ x x₁ x₂ rbi rbi₁) = subst (λ k → RBtreeInvariant k) (node-cong refl (cong (λ k → ⟪ k , _ ⟫ ) + (cong proj1 (just-injective (cong node-value eq))) ) + (just-injective (cong node-left eq)) (just-injective (cong node-right eq)) ) ( rb-red key₁ value x x₁ x₂ rbi rbi₁ ) + crbt03 v1 eq (rb-black key value x rbi rbi₁) = subst (λ k → RBtreeInvariant k) (node-cong refl (cong (λ k → ⟪ k , _ ⟫ ) + (cong proj1 (just-injective (cong node-value eq))) ) + (just-injective (cong node-left eq)) (just-injective (cong node-right eq)) ) ( rb-black key₁ _ x rbi rbi₁ ) + crbt04 : replacedRBTree key value (node key₁ value₁ left right) (node key₁ ⟪ proj1 value₁ , value ⟫ left right) + crbt04 = subst (λ k → replacedRBTree k value (node key₁ value₁ left right) (node key₁ ⟪ proj1 value₁ , value ⟫ left right)) + (just-injective (trans (cong node-key (trans eq1 (sym (trans (sym eq3) (just-injective eq2))))) eq) ) rbr-node +createRBT {n} {m} {A} {t} key value orig rbi ti tree (x ∷ leaf ∷ stack) si P exit = ⊥-elim (si-property-parent-node _ _ _ si refl) +createRBT {n} {m} {A} {t} key value orig rbi ti tree sp@(x ∷ node kp vp pleft pright ∷ stack) si P exit = crbt00 tree P refl where + crbt00 : (tree1 : bt (Color ∧ A)) → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) → tree1 ≡ tree → t + crbt00 leaf P eq = exit sp record { + tree = leaf + ; repl = node key ⟪ Red , value ⟫ leaf leaf + ; origti = ti + ; origrb = rbi + ; treerb = rb-leaf + ; replrb = rb-red key value refl refl refl rb-leaf rb-leaf + ; si = subst (λ k → stackInvariant key k orig _) (sym eq) si + ; replti = t-single key ⟪ Red , value ⟫ + ; state = rotate leaf refl rbr-leaf + } + crbt00 (node key₁ value₁ left right ) (case1 eq) eq1 = ⊥-elim (bt-ne (sym (trans eq1 eq) )) + crbt00 (node key₁ value₁ left right ) (case2 eq) eq1 with si-property-last _ _ _ _ si | si-property1 si + ... | eq2 | eq3 = exit sp record { + tree = node key₁ value₁ left right + ; repl = node key₁ ⟪ proj1 value₁ , value ⟫ left right + ; origti = ti + ; origrb = rbi + ; treerb = treerb + ; replrb = crbt03 value₁ refl treerb + ; si = subst (λ k → stackInvariant key k orig _) (sym eq1) si + ; replti = replaceTree1 _ _ _ (siToTreeinvariant _ _ _ _ ti (subst₂ (λ j k → stackInvariant key j orig k) (sym eq1) (cong (λ k → k ∷ _) + (trans eq3 (sym eq1))) si) ) + ; state = rebuild refl (crbt01 value₁ ) (λ ()) crbt04 + } where + crbt01 : (value₁ : Color ∧ A) → black-depth (node key₁ ⟪ proj1 value₁ , value ⟫ left right) ≡ black-depth (node key₁ value₁ left right) + crbt01 ⟪ Red , proj4 ⟫ = refl + crbt01 ⟪ Black , proj4 ⟫ = refl + crbt03 : {tree : bt (Color ∧ A) } (value₁ : Color ∧ A) → tree ≡ node key₁ value₁ left right → RBtreeInvariant tree + → RBtreeInvariant (node key₁ ⟪ proj1 value₁ , value ⟫ left right) + crbt03 _ () rb-leaf + crbt03 ⟪ Red , proj4 ⟫ teq (rb-red key₂ proj5 x x₁ x₂ rbi rbi₁) = subst (λ k → RBtreeInvariant k) (node-cong refl (cong (λ k → ⟪ k , value ⟫ ) + (cong proj1 (just-injective (cong node-value teq))) ) + (just-injective (cong node-left teq)) (just-injective (cong node-right teq)) ) ( rb-red key₁ value x x₁ x₂ rbi rbi₁ ) + crbt03 ⟪ Black , proj4 ⟫ () (rb-red key₁ proj5 x x₁ x₂ rbi rbi₁) + crbt03 ⟪ Black , proj4 ⟫ teq (rb-black key₂ proj5 x rbi rbi₁) = subst (λ k → RBtreeInvariant k) (node-cong refl (cong (λ k → ⟪ k , value ⟫ ) + (cong proj1 (just-injective (cong node-value teq))) ) + (just-injective (cong node-left teq)) (just-injective (cong node-right teq)) ) ( rb-black key₁ _ x rbi rbi₁ ) + crbt03 ⟪ Red , proj4 ⟫ () (rb-black key₁ proj5 x rbi rbi₁) + keq : key₁ ≡ key + keq = just-injective (trans (cong node-key eq1) eq) + crbt04 : replacedRBTree key value (node key₁ value₁ left right) (node key₁ ⟪ proj1 value₁ , value ⟫ left right) + crbt04 = subst (λ k → replacedRBTree k value (node key₁ value₁ left right) (node key₁ ⟪ proj1 value₁ , value ⟫ left right)) keq rbr-node + treerb : RBtreeInvariant (node key₁ value₁ left right) + treerb = PGtoRBinvariant1 _ orig rbi _ (subst (λ k → stackInvariant key k orig _) (sym eq1) si) ti-to-black : {n : Level} {A : Set n} → {tree : bt (Color ∧ A)} → treeInvariant tree → treeInvariant (to-black tree) @@ -131,12 +224,27 @@ → t insertCase4 leaf eq1 eq rot col si = ⊥-elim (rb04 eq eq1 si) where -- can't happen rb04 : {stack : List ( bt ( Color ∧ A))} → stack ≡ RBI.tree r ∷ orig ∷ [] → leaf ≡ orig → stackInvariant key (RBI.tree r) orig stack → ⊥ - rb04 = ? + rb04 () eq1 s-nil + rb04 eq eq1 (s-right .(RBI.tree r) .orig tree₁ x si) = si-property2 _ (s-right _ _ tree₁ x si) (trans (cong just eq1) + (sym (cong stack-last (∷-injectiveʳ eq)))) + rb04 eq eq1 (s-left .(RBI.tree r) .orig tree x si) = si-property2 _ (s-left _ _ tree x si) (trans (cong just eq1) + (sym (cong stack-last (∷-injectiveʳ eq)))) insertCase4 tr0@(node key₁ value₁ left right) refl eq rot col si with <-cmp key key₁ ... | tri< a ¬b ¬c = rb07 col where rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → left ≡ RBI.tree r - rb04 = ? -- (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x s-nil) eq eq1 = ? - -- rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) eq eq1 = ? + rb04 s-nil () eq1 + rb04 (s-right tree .(node key₁ value₁ left right) tree₁ {key₂} {v1} {st} x si₁) eq eq1 = + ⊥-elim ( nat-<> x (subst (λ k → key < k) (rb10 (subst (λ k → stackInvariant _ _ _ k ) rb11 si₁)) a )) where + rb11 : st ≡ node key₁ value₁ left right ∷ [] + rb11 = ∷-injectiveʳ eq + rb10 : stackInvariant key (node key₂ v1 tree₁ tree) (node key₁ value₁ left right) (node key₁ value₁ left right ∷ []) → key₁ ≡ key₂ + rb10 si₁ = just-injective (cong node-key (si-property1 si₁)) + rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} {v1} {st} x si₁) eq eq1 = + rb10 (subst (λ k → stackInvariant _ _ _ k ) rb11 si₁) where + rb11 : st ≡ node key₁ value₁ left right ∷ [] + rb11 = ∷-injectiveʳ eq + rb10 : stackInvariant key (node key₂ v1 tree₁ tree) (node key₁ value₁ left right) (node key₁ value₁ left right ∷ []) → left ≡ tree₁ + rb10 si₁ = just-injective (cong node-left (si-property1 si₁)) rb06 : black-depth repl ≡ black-depth right rb06 = begin black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ @@ -180,13 +288,22 @@ } where rb10 : replacedRBTree key value (node key₁ ⟪ Black , proj2 value₁ ⟫ left right) (node key₁ ⟪ Black , proj2 value₁ ⟫ repl right) rb10 = rbr-black-left repl-red a (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot) - - ... | tri≈ ¬a b ¬c = ? -- ⊥-elim ( si-property-pne _ _ stack eq si b ) -- can't happen + ... | tri≈ ¬a b ¬c = ⊥-elim ( si-property-pne _ _ stack eq si b ) -- can't happen ... | tri> ¬a ¬b c = rb07 col where rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → right ≡ RBI.tree r - rb04 = ? -- (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl = refl - -- rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x si) refl refl with si-property1 si - -- ... | refl = ⊥-elim ( nat-<> x c ) + rb04 s-nil () eq1 + rb04 (s-left tree .(node key₁ value₁ left right) tree₁ {key₂} {v1} {st} x si₁) eq eq1 = + ⊥-elim ( nat-<> x (subst (λ k → k < key ) (rb10 (subst (λ k → stackInvariant _ _ _ k ) rb11 si₁)) c )) where + rb11 : st ≡ node key₁ value₁ left right ∷ [] + rb11 = ∷-injectiveʳ eq + rb10 : stackInvariant key (node key₂ v1 tree tree₁) (node key₁ value₁ left right) (node key₁ value₁ left right ∷ []) → key₁ ≡ key₂ + rb10 si₁ = just-injective (cong node-key (si-property1 si₁)) + rb04 (s-right tree₁ .(node key₁ value₁ left right) tree {key₂} {v1} {st} x si₁) eq eq1 = + rb10 (subst (λ k → stackInvariant _ _ _ k ) rb11 si₁) where + rb11 : st ≡ node key₁ value₁ left right ∷ [] + rb11 = ∷-injectiveʳ eq + rb10 : stackInvariant key (node key₂ v1 tree tree₁) (node key₁ value₁ left right) (node key₁ value₁ left right ∷ []) → right ≡ tree₁ + rb10 si₁ = just-injective (cong node-right (si-property1 si₁)) rb06 : black-depth repl ≡ black-depth left rb06 = begin black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ @@ -254,7 +371,7 @@ ; origti = RBI.origti r ; origrb = RBI.origrb r ; treerb = treerb pg - ; replrb = rb02 + ; replrb = rb02 (PG.parent pg) x (treerb pg) ; replti = RB-repl→ti _ _ _ _ (rb08 pg) (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-left ceq rb04 rot)) ; si = popStackInvariant _ _ _ _ _ (rb00 pg) ; state = rebuild (cong color x) rb06 (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-left ceq rb04 rot)) @@ -263,11 +380,26 @@ rb01 = node kp vp repl n1 rb03 : black-depth n1 ≡ black-depth repl rb03 = trans (sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) x (treerb pg)))) (RB-repl→eq _ _ (RBI.treerb r) rot) - rb02 : RBtreeInvariant rb01 - rb02 = ? - -- with subst (λ k → RBtreeInvariant k) x (treerb pg) - -- ... | rb-red .kp value cx cx₁ ex₂ t t₁ = rb-red kp value (trans (sym ceq) cx) cx₁ (sym rb03) (RBI.replrb r) t₁ - -- ... | rb-black .kp value ex t t₁ = rb-black kp value (sym rb03) (RBI.replrb r) t₁ + rb02 : (tree : bt (Color ∧ A)) → tree ≡ node kp vp (RBI.tree r) n1 → RBtreeInvariant tree → RBtreeInvariant rb01 + rb02 .leaf eq rb-leaf = ⊥-elim ( bt-ne eq ) + rb02 (node key ⟪ Red , value ⟫ left right) eq (rb-red key value cx cx₁ x₂ rbi rbi₁) = + subst (λ k → RBtreeInvariant k) (node-cong refl rb11 refl rb12) (rb-red kp value (trans (sym ceq) rb13) cx₁ rb14 (RBI.replrb r) rbi₁) where + rb11 : ⟪ Red , value ⟫ ≡ vp + rb11 = just-injective (cong node-value eq) + rb12 : right ≡ n1 + rb12 = just-injective (cong node-right eq) + rb13 : color (RBI.tree r) ≡ Black + rb13 = trans (sym (cong color ( just-injective (cong node-left eq) ))) cx + rb14 : black-depth repl ≡ black-depth right + rb14 = trans (sym rb03) (cong black-depth (sym (just-injective (cong node-right eq)))) + rb02 (node key ⟪ Black , value ⟫ left right) eq (rb-black key value cx rbi rbi₁) = + subst (λ k → RBtreeInvariant k) (node-cong refl rb11 refl rb12) (rb-black kp value rb14 (RBI.replrb r) rbi₁) where + rb11 : ⟪ Black , value ⟫ ≡ vp + rb11 = just-injective (cong node-value eq) + rb12 : right ≡ n1 + rb12 = just-injective (cong node-right eq) + rb14 : black-depth repl ≡ black-depth right + rb14 = trans (sym rb03) (cong black-depth (sym (just-injective (cong node-right eq)))) rb05 : treeInvariant (node kp vp (RBI.tree r) n1 ) rb05 = subst (λ k → treeInvariant k) x (rb08 pg) rb04 : key < kp @@ -285,7 +417,7 @@ ; origti = RBI.origti r ; origrb = RBI.origrb r ; treerb = treerb pg - ; replrb = rb02 + ; replrb = rb02 (PG.parent pg) x (treerb pg) ; replti = RB-repl→ti _ _ _ _ (rb08 pg) (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-right ceq rb04 rot)) ; si = popStackInvariant _ _ _ _ _ (rb00 pg) ; state = rebuild (cong color x) rb06 (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-right ceq rb04 rot)) @@ -294,10 +426,26 @@ rb01 = node kp vp n1 repl rb03 : black-depth n1 ≡ black-depth repl rb03 = trans (RBtreeEQ (subst (λ k → RBtreeInvariant k) x (treerb pg))) ((RB-repl→eq _ _ (RBI.treerb r) rot)) - rb02 : RBtreeInvariant rb01 - rb02 = ? -- with subst (λ k → RBtreeInvariant k) x (treerb pg) - -- ... | rb-red .kp value cx cx₁ ex₂ t t₁ = rb-red kp value cx (trans (sym ceq) cx₁) rb03 t (RBI.replrb r) - -- ... | rb-black .kp value ex t t₁ = rb-black kp value rb03 t (RBI.replrb r) + rb02 : (tree : bt (Color ∧ A)) → tree ≡ node kp vp n1 (RBI.tree r) → RBtreeInvariant tree → RBtreeInvariant rb01 + rb02 .leaf eq rb-leaf = ⊥-elim ( bt-ne eq ) + rb02 (node key ⟪ Red , value ⟫ left right) eq (rb-red key value cx cx₁ x₂ rbi rbi₁) = + subst (λ k → RBtreeInvariant k) (node-cong refl rb11 rb12 refl) (rb-red kp value cx (trans (sym ceq) rb13) (sym rb14) rbi (RBI.replrb r)) where + rb11 : ⟪ Red , value ⟫ ≡ vp + rb11 = just-injective (cong node-value eq) + rb12 : left ≡ n1 + rb12 = just-injective (cong node-left eq) + rb13 : color (RBI.tree r) ≡ Black + rb13 = trans (sym (cong color ( just-injective (cong node-right eq) ))) cx₁ + rb14 : black-depth repl ≡ black-depth left + rb14 = trans (sym rb03) (cong black-depth (sym (just-injective (cong node-left eq)))) + rb02 (node key ⟪ Black , value ⟫ left right) eq (rb-black key value cx rbi rbi₁) = + subst (λ k → RBtreeInvariant k) (node-cong refl rb11 rb12 refl) (rb-black kp value (sym rb14) rbi (RBI.replrb r)) where + rb11 : ⟪ Black , value ⟫ ≡ vp + rb11 = just-injective (cong node-value eq) + rb12 : left ≡ n1 + rb12 = just-injective (cong node-left eq) + rb14 : black-depth repl ≡ black-depth left + rb14 = trans (sym rb03) (cong black-depth (sym (just-injective (cong node-left eq)))) rb05 : treeInvariant (node kp vp n1 (RBI.tree r) ) rb05 = subst (λ k → treeInvariant k) x (rb08 pg) rb04 : kp < key @@ -315,7 +463,7 @@ ; origti = RBI.origti r ; origrb = RBI.origrb r ; treerb = treerb pg - ; replrb = rb02 + ; replrb = rb02 (PG.parent pg) x (treerb pg) ; replti = RB-repl→ti _ _ _ _ (rb08 pg) (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-left ceq rb04 rot)) ; si = popStackInvariant _ _ _ _ _ (rb00 pg) ; state = rebuild (cong color x) rb06 (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-left ceq rb04 rot)) @@ -324,10 +472,26 @@ rb01 = node kp vp repl n1 rb03 : black-depth n1 ≡ black-depth repl rb03 = trans (sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) x (treerb pg)))) ((RB-repl→eq _ _ (RBI.treerb r) rot)) - rb02 : RBtreeInvariant rb01 - rb02 = ? -- with subst (λ k → RBtreeInvariant k) x (treerb pg) - -- ... | rb-red .kp value cx cx₁ ex₂ t t₁ = rb-red kp value (trans (sym ceq) cx) cx₁ (sym rb03) (RBI.replrb r) t₁ - -- ... | rb-black .kp value ex t t₁ = rb-black kp value (sym rb03) (RBI.replrb r) t₁ + rb02 : (tree : bt (Color ∧ A)) → tree ≡ node kp vp (RBI.tree r) n1 → RBtreeInvariant tree → RBtreeInvariant rb01 + rb02 .leaf eq rb-leaf = ⊥-elim ( bt-ne eq ) + rb02 (node key ⟪ Red , value ⟫ left right) eq (rb-red key value cx cx₁ x₂ rbi rbi₁) = + subst (λ k → RBtreeInvariant k) (node-cong refl rb11 refl rb12) (rb-red kp value (trans (sym ceq) rb13) cx₁ rb14 (RBI.replrb r) rbi₁) where + rb11 : ⟪ Red , value ⟫ ≡ vp + rb11 = just-injective (cong node-value eq) + rb12 : right ≡ n1 + rb12 = just-injective (cong node-right eq) + rb13 : color (RBI.tree r) ≡ Black + rb13 = trans (sym (cong color ( just-injective (cong node-left eq) ))) cx + rb14 : black-depth repl ≡ black-depth right + rb14 = trans (sym rb03) (cong black-depth (sym (just-injective (cong node-right eq)))) + rb02 (node key ⟪ Black , value ⟫ left right) eq (rb-black key value cx rbi rbi₁) = + subst (λ k → RBtreeInvariant k) (node-cong refl rb11 refl rb12) (rb-black kp value rb14 (RBI.replrb r) rbi₁) where + rb11 : ⟪ Black , value ⟫ ≡ vp + rb11 = just-injective (cong node-value eq) + rb12 : right ≡ n1 + rb12 = just-injective (cong node-right eq) + rb14 : black-depth repl ≡ black-depth right + rb14 = trans (sym rb03) (cong black-depth (sym (just-injective (cong node-right eq)))) rb05 : treeInvariant (node kp vp (RBI.tree r) n1) rb05 = subst (λ k → treeInvariant k) x (rb08 pg) rb04 : key < kp @@ -345,7 +509,7 @@ ; origti = RBI.origti r ; origrb = RBI.origrb r ; treerb = treerb pg - ; replrb = rb02 + ; replrb = rb02 (PG.parent pg) x (treerb pg) ; replti = RB-repl→ti _ _ _ _ (rb08 pg) (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-right ceq rb04 rot)) ; si = popStackInvariant _ _ _ _ _ (rb00 pg) ; state = rebuild (cong color x) rb06 (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-right ceq rb04 rot)) @@ -354,10 +518,26 @@ rb01 = node kp vp n1 repl rb03 : black-depth n1 ≡ black-depth repl rb03 = trans (RBtreeEQ (subst (λ k → RBtreeInvariant k) x (treerb pg))) ((RB-repl→eq _ _ (RBI.treerb r) rot)) - rb02 : RBtreeInvariant rb01 - rb02 = ? -- with subst (λ k → RBtreeInvariant k) x (treerb pg) - -- ... | rb-red .kp value cx cx₁ ex₂ t t₁ = rb-red kp value cx (trans (sym ceq) cx₁) rb03 t (RBI.replrb r) - -- ... | rb-black .kp value ex t t₁ = rb-black kp value rb03 t (RBI.replrb r) + rb02 : (tree : bt (Color ∧ A)) → tree ≡ node kp vp n1 (RBI.tree r) → RBtreeInvariant tree → RBtreeInvariant rb01 + rb02 .leaf eq rb-leaf = ⊥-elim ( bt-ne eq ) + rb02 (node key ⟪ Red , value ⟫ left right) eq (rb-red key value cx cx₁ x₂ rbi rbi₁) = + subst (λ k → RBtreeInvariant k) (node-cong refl rb11 rb12 refl) (rb-red kp value cx (trans (sym ceq) rb13) (sym rb14) rbi (RBI.replrb r)) where + rb11 : ⟪ Red , value ⟫ ≡ vp + rb11 = just-injective (cong node-value eq) + rb12 : left ≡ n1 + rb12 = just-injective (cong node-left eq) + rb13 : color (RBI.tree r) ≡ Black + rb13 = trans (sym (cong color ( just-injective (cong node-right eq) ))) cx₁ + rb14 : black-depth repl ≡ black-depth left + rb14 = trans (sym rb03) (cong black-depth (sym (just-injective (cong node-left eq)))) + rb02 (node key ⟪ Black , value ⟫ left right) eq (rb-black key value cx rbi rbi₁) = + subst (λ k → RBtreeInvariant k) (node-cong refl rb11 rb12 refl) (rb-black kp value (sym rb14) rbi (RBI.replrb r)) where + rb11 : ⟪ Black , value ⟫ ≡ vp + rb11 = just-injective (cong node-value eq) + rb12 : left ≡ n1 + rb12 = just-injective (cong node-left eq) + rb14 : black-depth repl ≡ black-depth left + rb14 = trans (sym rb03) (cong black-depth (sym (just-injective (cong node-left eq)))) rb05 : treeInvariant (node kp vp n1 (RBI.tree r)) rb05 = subst (λ k → treeInvariant k) x (rb08 pg) rb04 : kp < key @@ -376,8 +556,7 @@ → color repl ≡ Red → color (PG.uncle pg) ≡ Black → color (PG.parent pg) ≡ Red → t insertCase5 leaf eq pg rot repl-red uncle-black pcolor = ⊥-elim ( rb00 repl repl-red (cong color (sym eq))) where rb00 : (repl : bt (Color ∧ A)) → color repl ≡ Red → color repl ≡ Black → ⊥ - rb00 = ? -- (node key ⟪ Black , proj4 ⟫ repl repl₁) () eq1 - -- rb00 (node key ⟪ Red , proj4 ⟫ repl repl₁) eq () + rb00 repl eq eq₁ = ⊥-elim ( ⊥-color (trans (sym eq₁) eq )) insertCase5 (node rkey vr rp-left rp-right) eq pg rot repl-red uncle-black pcolor = insertCase51 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) @@ -758,8 +937,7 @@ ... | rebuild ceq bdepth-eq ¬leaf rot = rebuildCase ceq bdepth-eq ¬leaf rot ... | top-black eq rot = exit stack (trans eq (cong (λ k → k ∷ []) rb00)) r where 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 + rb00 = just-injective (si-property-last _ _ _ _ (subst (λ k → stackInvariant key (RBI.tree r) orig k) (eq) (RBI.si r))) ... | rotate _ repl-red 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