# HG changeset patch # User Shinji KONO # Date 1705917116 -32400 # Node ID 8dbddf72211e79388d8e426506984896978ad9f0 # Parent b8fb1e0755d0a7b63d97494390e41d0245faff8e ... diff -r b8fb1e0755d0 -r 8dbddf72211e hoareBinaryTree1.agda --- a/hoareBinaryTree1.agda Mon Jan 22 11:15:38 2024 +0900 +++ b/hoareBinaryTree1.agda Mon Jan 22 18:51:56 2024 +0900 @@ -738,8 +738,6 @@ rotated : rotatedTree tree rot ri : replacedTree key ⟪ Red , value ⟫ (child-replaced key rot ) repl ∨ replacedTree key ⟪ Black , value ⟫ (child-replaced key rot ) repl - repl-red : color repl ≡ Red - repl-eq : black-depth (child-replaced key rot ) ≡ black-depth repl stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A ) → (stack : List (bt A)) → stackInvariant key tree orig stack @@ -914,10 +912,14 @@ → stackInvariant key (RBI.tree r) orig stack → t insertCase12 leaf eq1 si = {!!} -- can't happen - insertCase12 tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ | child-replaced key (node key₁ value₁ left (RBI.rot r)) in eqcr - ... | tri< a ¬b ¬c | cr = {!!} - ... | tri≈ ¬a b ¬c | cr = {!!} -- can't happen - ... | tri> ¬a ¬b c | cr = insertCase13 value₁ refl where + insertCase12 tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ + ... | tri< a ¬b ¬c = {!!} 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) refl refl = refl + rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl with si-property1 si + ... | refl = ⊥-elim ( nat-<> x a ) + ... | tri≈ ¬a b ¬c = {!!} -- can't happen + ... | tri> ¬a ¬b c = insertCase13 value₁ refl where -- -- orig B -- / \ @@ -935,35 +937,28 @@ 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 ) + -- + -- RBI key value (node key₁ ⟪ Black , value₄ ⟫ left right) repl stack + -- insertCase13 : (v : Color ∧ A ) → v ≡ value₁ → t - insertCase13 ⟪ Black , value₄ ⟫ refl = exit (node key₁ ⟪ Red , value₄ ⟫ left repl) (orig ∷ []) refl record { + insertCase13 ⟪ Black , value₄ ⟫ refl = exit (node key₁ ⟪ Black , value₄ ⟫ left repl) (orig ∷ []) refl record { tree = orig ; rot = node key₁ value₁ left (RBI.rot r) ; origti = RBI.origti r ; origrb = RBI.origrb r ; treerb = RBI.origrb r - ; replrb = proj1 rb05 + ; replrb = proj1 (rb05 (RBI.ri r)) ; si = s-nil ; rotated = subst (λ k → rotatedTree k (node key₁ value₁ left (RBI.rot r))) ( trans (cong (λ k → node key₁ value₁ left k) (sym (rb04 si eq refl))) refl) (rtt-node rtt-unit (RBI.rotated r)) - ; ri = ? -- proj2 rb05 - ; repl-red = refl - ; repl-eq = rb07 + ; ri = proj2 (rb05 (RBI.ri r)) } where - rb07 : black-depth (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) ≡ black-depth left ⊔ black-depth repl - rb07 with <-cmp key key₁ - ... | tri< a ¬b ¬c = rb08 where -- r : RBI key value (node key₁ ⟪ Black , value₄ ⟫ left right) repl stack - rb08 : black-depth left ≡ black-depth left ⊔ black-depth repl - rb08 = ? - ... | tri≈ ¬a b ¬c = ? where - rb08 : suc (black-depth left ⊔ black-depth (RBI.rot r)) ≡ black-depth left ⊔ black-depth repl - rb08 = ? - ... | tri> ¬a ¬b c = ? where - rb08 : black-depth (RBI.rot r) ≡ black-depth left ⊔ black-depth repl - rb08 = ? rb09 : {n : Level} {A : Set n} → {key key1 key2 : ℕ} {value value1 : A} {t1 t2 : bt (Color ∧ A)} → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key1 ⟪ Black , value1 ⟫ t1 t2)) → key < key1 rb09 (rb-right-red x x0 x2) = x + rb08 : replacedTree key ⟪ Red , value ⟫ (child-replaced key (RBI.rot r)) repl + ∨ replacedTree key ⟪ Black , value ⟫ (child-replaced key (RBI.rot r)) repl + rb08 = RBI.ri r -- rb05 should more general tkey : {n : Level} {A : Set n } → (rbt : bt (Color ∧ A)) → ℕ tkey (node key value t t2) = key @@ -972,27 +967,21 @@ rb051 = {!!} rb052 : {key key₁ : ℕ} → stackInvariant key (RBI.tree r) orig stack → key < key₁ rb052 = {!!} - rb05 : RBtreeInvariant (node key₁ ⟪ Red , value₄ ⟫ left repl) ∧ replacedTree key ⟪ ? , value ⟫ - (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) (node key₁ ⟪ Red , value₄ ⟫ left repl) - rb05 with RBI.origrb r | rb04 si eq refl | RBI.replrb r in eqrepl | <-cmp key₁ (tkey repl) -- si and ri have key's relation - ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri< a ¬b ¬c = {!!} -- need paternmatch with c - ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri≈ ¬a b ¬c = {!!} -- key is unique ? - ... | rb-single key₂ value₂ | refl | rb-single key₃ value | tri> ¬a ¬b c = ⊥-elim (nat-<> {!!} {!!}) --⊥-elim (¬a (rb052 {!!})) - ... | rb-single key₂ value₂ | refl | rb-right-red x x₁ rb | t = {!!} -- cant happen ? red - red - ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri< a ¬b ¬c = ⟪ rb-right-red a ? (RBI.replrb r) , {!!} ⟫ -- t₁ t₂ = leaf , c₁ = Red - ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri≈ ¬a b ¬c = {!!} --rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} - ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb | tri> ¬a ¬b c = ⊥-elim ({!!} ) - ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb | t = {!!} --red -red - ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri< a ¬b ¬c = ⟪ rb-right-red a ? (RBI.replrb r) , {!!} ⟫ - ... | rb-single key₁ value₂ | refl | rb-left-black x x₁ rb | tri≈ ¬a b ¬c = ⊥-elim (¬c {!!} ) --(rb09 (RBI.origrb r))) - ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb | tri> ¬a ¬b c = {!!} - ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb rb₁ | t = {!!}　-- red-red - ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb rb₁ | tri< a ¬b ¬c = {!!} - ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb rb₁ | tri≈ ¬a b ¬c = {!!} - ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb rb₁ | tri> ¬a ¬b c = ⊥-elim {!!} - --... | rb-right-black x x₁ t | refl | rb | t = ? --⟪ proj1 {!!} , {!!} ⟫ - --... | rb-left-black x x₁ t | refl | rb | t = {!!} --⟪ rb-node-red ? ? ? ? ? ? , ? ⟫ - --... | rb-node-black x x₁ x₂ t x₃ t₁ | refl | rb | t = {!!} + rb05 : ( replacedTree key ⟪ Red , value ⟫ (child-replaced key (RBI.rot r)) repl + ∨ replacedTree key ⟪ Black , value ⟫ (child-replaced key (RBI.rot r)) repl ) + → RBtreeInvariant (node key₁ ⟪ Black , value₄ ⟫ left repl) + ∧ ( replacedTree key ⟪ Red , value ⟫ + (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r)) ) + (node key₁ ⟪ Black , value₄ ⟫ left repl) + ∨ + replacedTree key ⟪ Black , value ⟫ + (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r)) ) + (node key₁ ⟪ Black , value₄ ⟫ left repl) ) + rb05 (case1 ri) with <-cmp key key₁ + ... | tri< a ¬b ¬c = ⊥-elim ( ¬c c) + ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c c) + ... | tri> ¬a ¬b c = ⟪ ? , case1 ? ⟫ + rb05 (case2 ri) = ⟪ ? , ? ⟫ insertCase13 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r) ... | Black = exit {!!} {!!} {!!} {!!} ... | Red = exit {!!} {!!} {!!} {!!}