Mercurial > hg > Gears > GearsAgda
changeset 927:455981850269
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 08 Jun 2024 15:55:03 +0900 |
| parents | 9936101bc974 |
| children | 79d7e2a87f08 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 110 insertions(+), 63 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Sat Jun 08 08:52:35 2024 +0900 +++ b/hoareBinaryTree1.agda Sat Jun 08 15:55:03 2024 +0900 @@ -923,20 +923,20 @@ -- should we require stack-invariant? -- -data ParentGrand {n : Level} {A : Set n} (self : bt A) : (parent uncle grand : bt A) → Set n where +data ParentGrand {n : Level} {A : Set n} (key : ℕ) (self : bt A) : (parent uncle grand : bt A) → Set n where s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } - → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand + → key < kp → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand key self parent n2 grand s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } - → parent ≡ node kp vp n1 self → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand + → kp < key → parent ≡ node kp vp n1 self → grand ≡ node kg vg parent n2 → ParentGrand key self parent n2 grand s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } - → parent ≡ node kp vp self n1 → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand + → key < kp → parent ≡ node kp vp self n1 → grand ≡ node kg vg n2 parent → ParentGrand key self parent n2 grand s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } - → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand + → kp < key → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand key self parent n2 grand -record PG {n : Level } (A : Set n) (self : bt A) (stack : List (bt A)) : Set n where +record PG {n : Level } (A : Set n) (key : ℕ) (self : bt A) (stack : List (bt A)) : Set n where field parent grand uncle : bt A - pg : ParentGrand self parent uncle grand + pg : ParentGrand key self parent uncle grand rest : List (bt A) stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest ) @@ -950,10 +950,14 @@ → ¬ ( tree ≡ leaf) → (rotated : replacedRBTree key value tree repl) → RBI-state key value tree repl stack -- one stage 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 + rotate-leaf : (tree repl : bt (Color ∧ A)) → {stack : List (bt (Color ∧ A))} → color repl ≡ Red + → node-key repl ≡ just key + → (rotated : replacedRBTree key value leaf repl) + → RBI-state key value leaf repl stack -- two stages up + rotate : (tree : bt (Color ∧ A)) → {repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → color repl ≡ Red + → ¬ ( tree ≡ leaf) + → (rotated : replacedRBTree key value tree repl) + → RBI-state key value tree 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 @@ -1016,6 +1020,23 @@ ⊔-succ : {m n : ℕ} → suc (m ⊔ n) ≡ suc m ⊔ suc n ⊔-succ {m} {n} = refl +RB-repl-node : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A)) → {key : ℕ} → {value : A} + → replacedRBTree key value tree repl → ¬ ( repl ≡ leaf) +RB-repl-node {n} {A} .leaf .(node _ ⟪ Red , _ ⟫ leaf leaf) rbr-leaf () +RB-repl-node {n} {A} .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) rbr-node () +RB-repl-node {n} {A} .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) (rbr-right x x₁ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) (rbr-left x x₁ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) (rbr-black-right x x₁ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) (rbr-black-left x x₁ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) (rbr-flip-ll x x₁ x₂ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) (rbr-flip-lr x x₁ x₂ x₃ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rbr-flip-rl x x₁ x₂ x₃ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rbr-flip-rr x x₁ x₂ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) (rbr-rotate-ll x x₁ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) (rbr-rotate-rr x x₁ rpl) () +RB-repl-node {n} {A} .(node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) .(node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₂) (node kg ⟪ Red , _ ⟫ t₃ _)) (rbr-rotate-lr t₂ t₃ kg kp kn x x₁ x₂ rpl) () +RB-repl-node {n} {A} .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ t₃ _)) (rbr-rotate-rl t₂ t₃ kg kp kn x x₁ x₂ rpl) () + RB-repl→eq : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A)) → {key : ℕ} → {value : A} → RBtreeInvariant tree → replacedRBTree key value tree repl → black-depth tree ≡ black-depth repl @@ -1618,48 +1639,48 @@ -- stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A ) → (stack : List (bt A)) → stackInvariant key tree orig stack - → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A tree stack + → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A key tree stack stackToPG {n} {A} {key} tree .tree .(tree ∷ []) s-nil = case1 refl stackToPG {n} {A} {key} tree .(node _ _ _ tree) .(tree ∷ node _ _ _ tree ∷ []) (s-right _ _ _ x s-nil) = case2 (case1 refl) stackToPG {n} {A} {key} tree .(node k2 v2 t5 (node k1 v1 t2 tree)) (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ [])) (s-right tree (node k2 v2 t5 (node k1 v1 t2 tree)) t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) (node k2 v2 t5 (node k1 v1 t2 tree)) t5 {k2} {v2} x₁ s-nil)) = case2 (case2 - record { parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p refl refl ; rest = _ ; stack=gp = refl } ) + record { parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p x refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right tree orig t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) orig t5 {k2} {v2} x₁ (s-right _ _ _ x₂ si))) = case2 (case2 - record { parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p refl refl ; rest = _ ; stack=gp = refl } ) + record { parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p x refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right tree orig t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) orig t5 {k2} {v2} x₁ (s-left _ _ _ x₂ si))) = case2 (case2 - record { parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p refl refl ; rest = _ ; stack=gp = refl } ) + record { parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p x refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree .(node k2 v2 (node k1 v1 t1 tree) t2) .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ []) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ s-nil)) = case2 (case2 - record { parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } ) + record { parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 x refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ (s-right _ _ _ x₂ si))) = case2 (case2 - record { parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } ) + record { parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 x refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ (s-left _ _ _ x₂ si))) = case2 (case2 - record { parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } ) + record { parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 x refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree .(node _ _ tree _) .(tree ∷ node _ _ tree _ ∷ []) (s-left _ _ t1 {k1} {v1} x s-nil) = case2 (case1 refl) stackToPG {n} {A} {key} tree .(node _ _ _ (node k1 v1 tree t1)) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ []) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ s-nil)) = case2 (case2 - record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p refl refl ; rest = _ ; stack=gp = refl } ) + record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p x refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ (s-right _ _ _ x₂ si))) = case2 (case2 - record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p refl refl ; rest = _ ; stack=gp = refl } ) + record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p x refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ (s-left _ _ _ x₂ si))) = case2 (case2 - record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p refl refl ; rest = _ ; stack=gp = refl } ) + record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p x refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree .(node _ _ (node k1 v1 tree t1) _) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ []) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ s-nil)) = case2 (case2 - record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } ) + record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 x refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ (s-right _ _ _ x₂ si))) = case2 (case2 - record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } ) + record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 x refl refl ; rest = _ ; stack=gp = refl } ) stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ (s-left _ _ _ x₂ si))) = case2 (case2 - record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } ) + record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 x refl refl ; rest = _ ; stack=gp = refl } ) stackCase1 : {n : Level} {A : Set n} → {key : ℕ } → {tree orig : bt A } → {stack : List (bt A)} → stackInvariant key tree orig stack → stack ≡ orig ∷ [] → tree ≡ orig stackCase1 s-nil refl = refl -pg-prop-1 : {n : Level} (A : Set n) → (tree orig : bt A ) - → (stack : List (bt A)) → (pg : PG A tree stack) +pg-prop-1 : {n : Level} (A : Set n) → (key : ℕ) → (tree orig : bt A ) + → (stack : List (bt A)) → (pg : PG A key tree stack) → (¬ PG.grand pg ≡ leaf ) ∧ (¬ PG.parent pg ≡ leaf) -pg-prop-1 {_} A tree orig stack pg with PG.pg pg -... | s2-s1p2 refl refl = ⟪ (λ () ) , ( λ () ) ⟫ -... | s2-1sp2 refl refl = ⟪ (λ () ) , ( λ () ) ⟫ -... | s2-s12p refl refl = ⟪ (λ () ) , ( λ () ) ⟫ -... | s2-1s2p refl refl = ⟪ (λ () ) , ( λ () ) ⟫ +pg-prop-1 {_} A _ tree orig stack pg with PG.pg pg +... | s2-s1p2 _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ +... | s2-1sp2 _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ +... | s2-s12p _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ +... | s2-1s2p _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ popStackInvariant : {n : Level} {A : Set n} → (rest : List ( bt (Color ∧ A))) → ( tree parent orig : bt (Color ∧ A)) → (key : ℕ) @@ -1754,7 +1775,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 leaf refl refl rbr-leaf + ; state = rotate-leaf leaf _ refl refl rbr-leaf } where crbt01 : tree ≡ leaf crbt01 with si-property-last _ _ _ _ si | si-property1 si @@ -1793,7 +1814,7 @@ ; treerb = rb-leaf ; replrb = rb-red key value refl refl refl rb-leaf rb-leaf ; si = si - ; state = rotate leaf refl refl rbr-leaf + ; state = rotate-leaf 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 @@ -1947,15 +1968,15 @@ rb00 refl = si-property1 (RBI.si r) ... | case2 (case1 x) = insertCase4 orig refl x rot (case2 ceq) (RBI.si r) -- one level stack, orig is parent of repl ... | case2 (case2 pg) = rebuildCase1 pg where - rb00 : (pg : PG (Color ∧ A) (RBI.tree r) stack) → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) + rb00 : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) rb00 pg = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r) - treerb : (pg : PG (Color ∧ A) (RBI.tree r) stack) → RBtreeInvariant (PG.parent pg) + treerb : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → RBtreeInvariant (PG.parent pg) treerb pg = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (rb00 pg)) - rb08 : (pg : PG (Color ∧ A) (RBI.tree r) stack) → treeInvariant (PG.parent pg) + rb08 : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → treeInvariant (PG.parent pg) rb08 pg = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (rb00 pg)) - rebuildCase1 : (PG (Color ∧ A) (RBI.tree r) stack) → t + rebuildCase1 : (PG (Color ∧ A) key (RBI.tree r) stack) → t rebuildCase1 pg with PG.pg pg - ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = rebuildCase2 where + ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = rebuildCase2 where rebuildCase2 : t rebuildCase2 = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record { tree = PG.parent pg @@ -1984,9 +2005,9 @@ rb07 : (vp : Color ∧ A) → black-depth (node kp vp n1 repl) ≡ black-depth (node kp vp n1 (RBI.tree r)) rb07 ⟪ Black , proj4 ⟫ = cong (λ k → suc (black-depth n1 ⊔ k)) bdepth-eq rb07 ⟪ Red , proj4 ⟫ = cong (λ k → (black-depth n1 ⊔ k)) bdepth-eq - ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? - ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? - ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = rebuildCase2 where + ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? + ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? + ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = rebuildCase2 where rebuildCase2 : t rebuildCase2 = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record { tree = PG.parent pg @@ -2019,7 +2040,7 @@ -- both parent and uncle are Red, rotate then goto rebuild -- insertCase5 : (repl1 : bt (Color ∧ A)) → repl1 ≡ repl - → (pg : PG (Color ∧ A) (RBI.tree r) stack) + → (pg : PG (Color ∧ A) key (RBI.tree r) stack) → (rot : replacedRBTree key value (RBI.tree r) repl) → 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 @@ -2044,7 +2065,7 @@ insertCase51 : t insertCase51 with PG.pg pg - ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = insertCase52 where + ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase52 where insertCase52 : t insertCase52 with <-cmp key kp ... | tri< a ¬b ¬c = next (PG.grand pg ∷ PG.rest pg) record { @@ -2114,10 +2135,9 @@ black-depth (PG.grand pg) ∎ where open ≡-Reasoning ... | tri≈ ¬a b ¬c = ⊥-elim ( si-property-pne _ _ stack (trans (PG.stack=gp pg) (cong (λ k → _ ∷ k ∷ _) x) ) (RBI.si r) b ) -- can't happen ... | tri> ¬a ¬b c = ? - ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? - ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? - ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? - + ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? + ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? + ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? replaceRBP1 : t replaceRBP1 with RBI.state r ... | rebuild ceq bdepth-eq ¬leaf rot = rebuildCase ceq bdepth-eq ¬leaf rot @@ -2125,22 +2145,50 @@ 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 childeq rot with stackToPG (RBI.tree r) orig stack (RBI.si r) + ... | rotate-leaf tree repl repl-red keyeq rot = insertCase0 where + insertCase0 : t + insertCase0 with stackToPG (RBI.tree r) orig stack (RBI.si r) + ... | case1 eq = exit stack eq r + ... | case2 (case1 eq1) = insertCase4 orig refl eq1 rot (case1 repl-red) (RBI.si r) + ... | case2 (case2 pg) with color (PG.parent pg) in pcolor + ... | Black = insertCase1 where + rb00 : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) + rb00 pg = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r) + treerb : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → RBtreeInvariant (PG.parent pg) + treerb pg = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (rb00 pg)) + rb08 : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → treeInvariant (PG.parent pg) + rb08 pg = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (rb00 pg)) + insertCase1 : t + insertCase1 with PG.pg pg + ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record { + tree = PG.parent pg + ; repl = ? + ; origti = RBI.origti r + ; origrb = RBI.origrb r + ; treerb = treerb pg + ; replrb = ? + ; si = popStackInvariant _ _ _ _ _ (rb00 pg) + ; state = rebuild (cong color x) ? ? ? + } ? + insertCase1 | s2-1sp2 lt x x₁ = ? + insertCase1 | s2-s12p lt x x₁ = ? + insertCase1 | s2-1s2p lt x x₁ = ? + ... | Red = ? + ... | rotate _ repl-red ¬leaf 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 ... | Black = insertCase1 where -- Parent is Black, make color repl ≡ color tree then goto rebuildCase - rb00 : (pg : PG (Color ∧ A) (RBI.tree r) stack) → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) + rb00 : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) rb00 pg = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r) - treerb : (pg : PG (Color ∧ A) (RBI.tree r) stack) → RBtreeInvariant (PG.parent pg) + treerb : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → RBtreeInvariant (PG.parent pg) treerb pg = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (rb00 pg)) - rb08 : (pg : PG (Color ∧ A) (RBI.tree r) stack) → treeInvariant (PG.parent pg) + rb08 : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → treeInvariant (PG.parent pg) rb08 pg = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (rb00 pg)) insertCase1 : t insertCase1 with PG.pg pg - ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ with <-cmp key kp - ... | tri< a ¬b ¬c = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record { + ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record { tree = PG.parent pg ; repl = rb01 ; origti = RBI.origti r @@ -2154,7 +2202,8 @@ rb01 : bt (Color ∧ A) rb01 = node kp vp repl n1 rb03 : key < kp - rb03 = a + rb03 = si-property-< ¬leaf (subst (λ k → treeInvariant k) x (rb08 pg)) + (subst (λ k → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x (rb00 pg)) rb04 : ⟪ Black , proj2 vp ⟫ ≡ vp rb04 with subst (λ k → color k ≡ Black) x pcolor ... | refl = refl @@ -2176,16 +2225,14 @@ rb06 : RBtreeInvariant rb01 rb06 = subst (λ k → RBtreeInvariant (node kp k repl n1)) rb04 ( rb-black _ _ rb07 (RBI.replrb r) (RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x (treerb pg)))) - ... | tri≈ ¬a b ¬c = ⊥-elim ( si-property-pne _ _ stack (trans (PG.stack=gp pg) (cong (λ k → _ ∷ k ∷ _) x) ) (RBI.si r) b ) -- can't happen - ... | tri> ¬a ¬b c = ? - insertCase1 | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? - insertCase1 | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? - insertCase1 | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? + insertCase1 | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? + insertCase1 | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? + insertCase1 | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? ... | Red with PG.uncle pg in uneq ... | leaf = insertCase5 repl refl pg rot repl-red (cong color uneq) pcolor ... | node key₁ ⟪ Black , value₁ ⟫ t₁ t₂ = insertCase5 repl refl pg rot repl-red (cong color uneq) pcolor ... | node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ with PG.pg pg -- insertCase2 : uncle and parent are Red, flip color and go up by two level - ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = insertCase2 where + ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase2 where insertCase2 : t insertCase2 with <-cmp key kp ... | tri< a ¬b ¬c = next (PG.grand pg ∷ (PG.rest pg)) @@ -2262,7 +2309,7 @@ where open ≤-Reasoning ... | tri≈ ¬a b ¬c = ⊥-elim ( si-property-pne _ _ stack (trans (PG.stack=gp pg) (cong (λ k → _ ∷ k ∷ _) x) ) (RBI.si r) b ) -- can't happen ... | tri> ¬a ¬b c = ? - ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!} - ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!} - ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!} + ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = {!!} + ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = {!!} + ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = {!!}