Mercurial > hg > Gears > GearsAgda
changeset 952:f913c7b010b5
BTree fixed
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 24 Aug 2024 19:20:47 +0900 |
| parents | ccdcf5572a54 |
| children | 24255e0dd027 |
| files | BTree.agda RBTree.agda |
| diffstat | 2 files changed, 287 insertions(+), 251 deletions(-) [+] |
line wrap: on
line diff
--- a/BTree.agda Sun Aug 18 20:02:03 2024 +0900 +++ b/BTree.agda Sat Aug 24 19:20:47 2024 +0900 @@ -827,21 +827,92 @@ lem11 : tr> k₁ t₃ lem11 = subst₂ (λ j k → tr> j k ) (just-injective (cong node-key eq)) (just-injective (cong node-right ( just-injective (cong node-right eq))) ) x₅ - - +si-property3 : {n : Level} {A : Set n} → (stack rest : List ( bt A)) + → ( tree orig : bt A) → (key : ℕ) + → stack ≡ ( tree ∷ leaf ∷ rest ) + → ¬ stackInvariant key tree orig stack +si-property3 {n} {A} stack rest tree orig key eq si = lem00 stack si eq where + lem00 : (stack : List (bt A)) → stackInvariant key tree orig stack → stack ≡ (tree ∷ leaf ∷ rest ) → ⊥ + lem00 _ s-nil () + lem00 _ (s-right .tree .orig tree₁ x si1) eq with si-property1 (subst₂ (λ j k → stackInvariant key j orig k) refl (∷-injectiveʳ eq) si1) + ... | () + lem00 _ (s-left tree₁ .orig tree x si1) eq with si-property1 (subst₂ (λ j k → stackInvariant key j orig k) refl (∷-injectiveʳ eq) si1) + ... | () popStackInvariant : {n : Level} {A : Set n} → (rest : List ( bt A)) → ( tree parent orig : bt A) → (key : ℕ) → stackInvariant key tree orig ( tree ∷ parent ∷ rest ) → stackInvariant key parent orig (parent ∷ rest ) -popStackInvariant rest tree parent orig key = ? +popStackInvariant {n} {A} rest tree parent orig key si = lem00 _ ( tree ∷ parent ∷ rest ) si refl where + lem00 : (parent : bt A) → (stack : List (bt A)) → stackInvariant key tree orig stack → stack ≡ (tree ∷ parent ∷ rest ) → stackInvariant key parent orig (parent ∷ rest ) + lem00 leaf _ si1 eq = ⊥-elim (si-property3 _ _ _ _ _ eq si1) + lem00 (node pkey pvalue left right) .(tree ∷ _) (s-right .tree .orig tree₁ x si1) eq + = subst₂ (λ j k → stackInvariant key j orig k ) (sym (si-property1 (subst₂ (λ j k → stackInvariant key j orig k) + refl (∷-injectiveʳ eq) si1))) (∷-injectiveʳ eq) si1 + lem00 (node pkey pvalue left right) (tree₁ ∷ _) (s-left .tree₁ .orig tree x si1) eq + = subst₂ (λ j k → stackInvariant key j orig k ) (sym (si-property1 (subst₂ (λ j k → stackInvariant key j orig k) + refl (∷-injectiveʳ eq) si1))) (∷-injectiveʳ eq) si1 siToTreeinvariant : {n : Level} {A : Set n} → (rest : List ( bt A)) → ( tree orig : bt A) → (key : ℕ) → treeInvariant orig → stackInvariant key tree orig ( tree ∷ rest ) → treeInvariant tree -siToTreeinvariant = ? +siToTreeinvariant {n} {A} rest tree orig key ti si = lem00 _ (tree ∷ rest) rest si refl ti where + lem00 : (tree : bt A) → (stack rest : List (bt A)) → stackInvariant key tree orig stack → stack ≡ (tree ∷ rest ) → treeInvariant orig → treeInvariant tree + lem00 _ (tree ∷ []) _ (s-right .tree .orig tree₁ {key₁} {v₁} x si1) eq tio = ⊥-elim (si-property0 si1 refl) + lem00 _ (tree ∷ leaf ∷ st) _ (s-right .tree .orig tree₁ {key₁} {v₁} x si1) eq tio with si-property1 si1 + ... | () + lem00 _ st0@(tree ∷ parent @ (node key₁ value tree₃ tree₁) ∷ st) rest₀ si2@(s-right .tree .orig tree₂ {key₂} {v₁} x si1) eq tio = + treeRightDown _ _ (lem01 _ st0 si2 (cong (λ k → tree ∷ node key₁ value tree₃ k ∷ st) lem02 )) where + lem02 : tree₁ ≡ tree + lem02 = just-injective (cong node-right (si-property1 si1)) + lem01 : (parent : bt A) → (stack : List (bt A)) → stackInvariant key tree orig stack → stack ≡ (tree ∷ parent ∷ st ) → treeInvariant parent + lem01 parent .(orig ∷ []) s-nil () + lem01 parent (tree ∷ []) (s-right .tree .orig tree₁ {key₃} {v₃} x si) () + lem01 parent (tree ∷ parent₁ ∷ st3) (s-right .tree .orig tree₁ {key₃} {v₃} x si) eq3 = subst (λ k → treeInvariant k) lem03 (lem00 _ _ st si lem04 tio) where + lem03 : node key₃ v₃ tree₁ tree ≡ parent + lem03 = trans (sym (si-property1 si)) (∷-injectiveˡ (∷-injectiveʳ eq3)) + lem04 : parent₁ ∷ st3 ≡ node key₃ v₃ tree₁ tree ∷ st + lem04 = cong₂ (λ j k → j ∷ k) (si-property1 si) (∷-injectiveʳ (∷-injectiveʳ eq3)) + lem01 parent (tree ∷ []) (s-left .tree .orig tree₁ {key₃} {v₃} x si) () + lem01 parent (tree ∷ parent₁ ∷ st3) (s-left .tree .orig tree₁ {key₃} {v₃} x si) eq3 = subst (λ k → treeInvariant k) lem03 (lem00 _ _ st si lem04 tio) where + lem03 : node key₃ v₃ tree tree₁ ≡ parent + lem03 = trans (sym (si-property1 si)) (∷-injectiveˡ (∷-injectiveʳ eq3)) + lem04 : parent₁ ∷ st3 ≡ node key₃ v₃ tree tree₁ ∷ st + lem04 = cong₂ (λ j k → j ∷ k) (si-property1 si) (∷-injectiveʳ (∷-injectiveʳ eq3)) + lem00 _ (tree ∷ []) _ (s-left .tree .orig tree₁ {key₁} {v₁} x si1) eq tio = ⊥-elim (si-property0 si1 refl) + lem00 _ (tree ∷ leaf ∷ st) _ (s-left .tree .orig tree₁ {key₁} {v₁} x si1) eq tio with si-property1 si1 + ... | () + lem00 _ st0@(tree ∷ parent @ (node key₁ value tree₃ tree₁) ∷ st) rest₀ si2@(s-left .tree .orig tree₂ {key₂} {v₁} x si1) eq tio = + treeLeftDown _ _ (lem01 _ st0 si2 (cong (λ k → tree ∷ node key₁ value k tree₁ ∷ st) lem02 )) where + lem02 : tree₃ ≡ tree + lem02 = just-injective (cong node-left (si-property1 si1)) + lem01 : (parent : bt A) → (stack : List (bt A)) → stackInvariant key tree orig stack → stack ≡ (tree ∷ parent ∷ st ) → treeInvariant parent + lem01 parent .(orig ∷ []) s-nil () + lem01 parent (tree ∷ []) (s-right .tree .orig tree₁ {key₃} {v₃} x si) () + lem01 parent (tree ∷ parent₁ ∷ st3) (s-right .tree .orig tree₁ {key₃} {v₃} x si) eq3 = subst (λ k → treeInvariant k) lem03 (lem00 _ _ st si lem04 tio) where + lem03 : node key₃ v₃ tree₁ tree ≡ parent + lem03 = trans (sym (si-property1 si)) (∷-injectiveˡ (∷-injectiveʳ eq3)) + lem04 : parent₁ ∷ st3 ≡ node key₃ v₃ tree₁ tree ∷ st + lem04 = cong₂ (λ j k → j ∷ k) (si-property1 si) (∷-injectiveʳ (∷-injectiveʳ eq3)) + lem01 parent (tree ∷ []) (s-left .tree .orig tree₁ {key₃} {v₃} x si) () + lem01 parent (tree ∷ parent₁ ∷ st3) (s-left .tree .orig tree₁ {key₃} {v₃} x si) eq3 = subst (λ k → treeInvariant k) lem03 (lem00 _ _ st si lem04 tio) where + lem03 : node key₃ v₃ tree tree₁ ≡ parent + lem03 = trans (sym (si-property1 si)) (∷-injectiveˡ (∷-injectiveʳ eq3)) + lem04 : parent₁ ∷ st3 ≡ node key₃ v₃ tree tree₁ ∷ st + lem04 = cong₂ (λ j k → j ∷ k) (si-property1 si) (∷-injectiveʳ (∷-injectiveʳ eq3)) + lem00 _ _ _ s-nil eq tio = tio + +child-repaced-ti : {n : Level} {A : Set n} (key : ℕ) (tree : bt A) → treeInvariant tree → treeInvariant (child-replaced key tree) +child-repaced-ti {n} {A} key tree ti = ch00 tree _ ti refl where + ch00 : (tree tree₁ : bt A) → treeInvariant tree → tree₁ ≡ child-replaced key tree → treeInvariant tree₁ + ch00 leaf tree₁ ti eq = subst (λ k → treeInvariant k) (sym eq) t-leaf + ch00 (node key₁ value tree tree₂) tree₁ ti₁ eq with <-cmp key key₁ + ... | tri< a ¬b ¬c = subst (λ k → treeInvariant k) (sym eq) (treeLeftDown _ _ ti₁ ) + ... | tri≈ ¬a b ¬c = subst (λ k → treeInvariant k) (sym eq) ti₁ + ... | tri> ¬a ¬b c = subst (λ k → treeInvariant k) (sym eq) (treeRightDown _ _ ti₁ ) + record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where field @@ -855,16 +926,13 @@ replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value (child-replaced key tree) tree1 → t) → t -replaceNodeP = ? --- replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 ) r-leaf --- replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P) --- (subst (λ j → replacedTree k v1 j (node k v1 t t₁) ) repl00 r-node) where --- repl00 : node k value t t₁ ≡ child-replaced k (node k value t t₁) --- repl00 with <-cmp k k --- ... | tri< a ¬b ¬c = ⊥-elim (¬b refl) --- ... | tri≈ ¬a b ¬c = refl --- ... | tri> ¬a ¬b c = ⊥-elim (¬b refl) --- +replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 ) r-leaf +replaceNodeP k v1 (node k₁ value t t₁) (case1 ()) P next +replaceNodeP k v1 (node k₁ value t t₁) (case2 eq) P next = next (node k v1 t t₁) (replaceTree1 k value v1 (subst (λ k → treeInvariant (node k value t t₁)) repl01 P)) repl00 where + repl01 : k₁ ≡ k + repl01 = just-injective eq + repl00 : replacedTree k v1 (child-replaced k (node k₁ value t t₁)) (node k v1 t t₁) + repl00 = subst (λ j → replacedTree k v1 j (node k v1 t t₁)) (trans (cong (λ k → node k value t t₁) (sym repl01) ) (sym ( child-replaced-eq repl01 )) ) r-node replaceP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → {tree : bt A} ( repl : bt A) @@ -873,258 +941,225 @@ → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t) → (exit : (tree1 repl : bt A) → treeInvariant repl ∧ replacedTree key value tree1 repl → t) → t replaceP key value {tree} repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen -replaceP key value {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ (replacePR.si Pre)-- tree0 ≡ leaf -... | eq = exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ t-single _ _ , ? ⟫ +replaceP key value {tree} repl (leaf ∷ []) Pre next exit = exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ t-single _ _ , repl00 ⟫ where + repl00 : replacedTree key value (replacePR.tree0 Pre) (node key value leaf leaf) + repl00 = subst (λ k → replacedTree key value k (node key value leaf leaf)) (just-injective (si-property-last _ _ _ _ (replacePR.si Pre))) r-leaf replaceP key value {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁ -... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) (node key₁ value₁ repl right ) - ⟪ RTtoTI0 _ _ _ _ (replacePR.ti Pre) repl01 , repl01 ⟫ where - repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ repl right ) - -- repl01 = ? --with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre) - repl01 = ? where - -- | refl | refl = subst (λ k → replacedTree key value (node key₁ value₁ k right ) (node key₁ value₁ repl right )) repl02 (r-left a repl03) where - repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl - repl03 = replacePR.ri ? - repl02 : child-replaced key (node key₁ value₁ left right) ≡ left - repl02 with <-cmp key key₁ - ... | tri< a ¬b ¬c = refl - ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a a) - ... | tri> ¬a ¬b c = ⊥-elim ( ¬a a) -... | tri≈ ¬a b ¬c = exit (replacePR.tree0 Pre) repl ⟪ RTtoTI0 _ _ _ _ (replacePR.ti Pre) repl01 , repl01 ⟫ where - repl01 : replacedTree key value (replacePR.tree0 Pre) repl - --repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre) - repl01 = ? where - --repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl02 (replacePR.ri Pre) where - repl02 : child-replaced key (node key₁ value₁ left right) ≡ node key₁ value₁ left right - repl02 with <-cmp key key₁ - ... | tri< a ¬b ¬c = ⊥-elim ( ¬b b) - ... | tri≈ ¬a b ¬c = refl - ... | tri> ¬a ¬b c = ⊥-elim ( ¬b b) -... | tri> ¬a ¬b c = exit (replacePR.tree0 Pre) (node key₁ value₁ left repl ) ⟪ RTtoTI0 _ _ _ _ (replacePR.ti Pre) repl01 , repl01 ⟫ where - repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ left repl ) - -- repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre) - repl01 = ? where - -- repl01 | refl | refl = subst (λ k → replacedTree key value (node key₁ value₁ left k ) (node key₁ value₁ left repl )) repl02 (r-right c repl03) where - repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl - repl03 = replacePR.ri ? - repl02 : child-replaced key (node key₁ value₁ left right) ≡ right - repl02 with <-cmp key key₁ - ... | tri< a ¬b ¬c = ⊥-elim ( ¬c c) - ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c c) - ... | tri> ¬a ¬b c = refl +... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) (node key₁ value₁ repl right ) ⟪ RTtoTI0 _ _ _ _ (replacePR.ti Pre) repl02 , repl02 ⟫ where + repl03 : node key₁ value₁ (child-replaced key tree) right ≡ replacePR.tree0 Pre + repl03 = begin + node key₁ value₁ (child-replaced key tree) right ≡⟨ cong (λ k → node key₁ value₁ (child-replaced key k) right) (sym (si-property1 (replacePR.si Pre ))) ⟩ + node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right ) (child-replaced-left a ) ⟩ + node key₁ value₁ left right ≡⟨ just-injective (si-property-last _ _ _ _ (replacePR.si Pre)) ⟩ + replacePR.tree0 Pre ∎ where + open ≡-Reasoning + repl02 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ repl right) + repl02 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) repl03 ( r-left a (replacePR.ri Pre)) +... | tri≈ ¬a b ¬c = exit (replacePR.tree0 Pre) repl ⟪ RTtoTI0 _ _ _ _ (replacePR.ti Pre) repl02 , repl02 ⟫ where + repl03 : child-replaced key tree ≡ replacePR.tree0 Pre + repl03 = begin + child-replaced key tree ≡⟨ cong (λ k → child-replaced key k ) (sym (si-property1 (replacePR.si Pre))) ⟩ + child-replaced key (node key₁ value₁ left right) ≡⟨ child-replaced-eq (sym b) ⟩ + node key₁ value₁ left right ≡⟨ just-injective (si-property-last _ _ _ _ (replacePR.si Pre)) ⟩ + replacePR.tree0 Pre ∎ where open ≡-Reasoning + repl02 : replacedTree key value (replacePR.tree0 Pre) repl + repl02 = subst (λ k → replacedTree key value k repl ) repl03 (replacePR.ri Pre) +... | tri> ¬a ¬b c = exit (replacePR.tree0 Pre) (node key₁ value₁ left repl ) ⟪ RTtoTI0 _ _ _ _ (replacePR.ti Pre) repl02 , repl02 ⟫ where + repl03 : node key₁ value₁ left (child-replaced key tree) ≡ replacePR.tree0 Pre + repl03 = begin + node key₁ value₁ left (child-replaced key tree) ≡⟨ cong (λ k → node key₁ value₁ left (child-replaced key k) ) (sym (si-property1 (replacePR.si Pre ))) ⟩ + node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) (child-replaced-right c ) ⟩ + node key₁ value₁ left right ≡⟨ just-injective (si-property-last _ _ _ _ (replacePR.si Pre)) ⟩ + replacePR.tree0 Pre ∎ where + open ≡-Reasoning + repl02 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ left repl ) + repl02 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl ) ) repl03 ( r-right c (replacePR.ri Pre)) replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(tree1 ∷ st1)) Pre next exit = next key value repl st Post ≤-refl where Post : replacePR key value tree1 repl (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤) - Post = ? -- where with replacePR.si Pre --- -- ... | s-right _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; --- rti = replacePR.rti Pre ; ci = lift tt } where --- repl09 : tree1 ≡ node key₂ v1 tree₁ leaf --- repl09 = si-property1 si --- repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) --- repl10 with si-property1 si --- ... | refl = si --- repl07 : child-replaced key (node key₂ v1 tree₁ leaf) ≡ leaf --- repl07 with <-cmp key key₂ --- ... | tri< a ¬b ¬c = ⊥-elim (¬c x) --- ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x) --- ... | tri> ¬a ¬b c = refl --- repl12 : replacedTree key value (child-replaced key tree1 ) repl --- repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07 ) ) (sym (rt-property-leaf (replacePR.ri Pre))) r-leaf --- ... | s-left _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = replacePR.rti Pre ; ri = repl12 ; ci = lift tt } where --- repl09 : tree1 ≡ node key₂ v1 leaf tree₁ --- repl09 = si-property1 si --- repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) --- repl10 with si-property1 si --- ... | refl = si --- repl07 : child-replaced key (node key₂ v1 leaf tree₁ ) ≡ leaf --- repl07 with <-cmp key key₂ --- ... | tri< a ¬b ¬c = refl --- ... | tri≈ ¬a b ¬c = ⊥-elim (¬a x) --- ... | tri> ¬a ¬b c = ⊥-elim (¬a x) --- repl12 : replacedTree key value (child-replaced key tree1 ) repl --- repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07) ) (sym (rt-property-leaf (replacePR.ri Pre ))) r-leaf -replaceP {n} {_} {A} key value {tree} repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁ + Post = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 _ (replacePR.si Pre) refl ; rti = replacePR.rti Pre ; ci = lift tt } where + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 = popStackInvariant _ _ _ _ _ (subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (leaf ∷ tree1 ∷ st1) ) + (sym (si-property1 (replacePR.si Pre))) (replacePR.si Pre) ) + repl12 : (stack : List (bt A)) → stackInvariant key tree (replacePR.tree0 Pre) stack → stack ≡ (leaf ∷ tree1 ∷ st1) + → replacedTree key value (child-replaced key tree1 ) repl + repl12 _ s-nil () + repl12 (node k₁ v₁ left right ∷ st₁) (s-right .(node k₁ v₁ left right) .(replacePR.tree0 Pre) tree₁ x si) () + repl12 (leaf ∷ st₁) (s-right .tree .(replacePR.tree0 Pre) tree₁ {key₁} {v₁} x si) eq = subst₂ (λ j k → replacedTree key value j k ) lem10 lem09 r-leaf where + lem09 : node key value leaf leaf ≡ repl + lem09 = sym (rt-property-leaf (replacePR.ri Pre)) + lem10 : leaf ≡ child-replaced key tree1 + lem10 = begin + leaf ≡⟨ sym (child-replaced-right x ) ⟩ + child-replaced key (node key₁ _ tree₁ leaf) ≡⟨ cong (child-replaced key) (sym repl13) ⟩ + child-replaced key tree1 ∎ where + open ≡-Reasoning + repl13 : tree1 ≡ node key₁ v₁ tree₁ leaf + repl13 = si-property1 (subst (λ k → stackInvariant key (node key₁ v₁ tree₁ leaf) (replacePR.tree0 Pre) k) (∷-injectiveʳ eq) si ) + repl12 (node k₁ v₁ left right ∷ st₁) (s-left .(node k₁ v₁ left right) .(replacePR.tree0 Pre) tree₁ x si) () + repl12 (leaf ∷ st₁) (s-left .tree .(replacePR.tree0 Pre) tree₁ {key₁} {v₁} x si) eq = subst₂ (λ j k → replacedTree key value j k ) lem10 lem09 r-leaf where + lem09 : node key value leaf leaf ≡ repl + lem09 = sym (rt-property-leaf (replacePR.ri Pre)) + lem10 : leaf ≡ child-replaced key tree1 + lem10 = begin + leaf ≡⟨ sym (child-replaced-left x ) ⟩ + child-replaced key (node key₁ _ leaf tree₁ ) ≡⟨ cong (child-replaced key) (sym repl13) ⟩ + child-replaced key tree1 ∎ where + open ≡-Reasoning + repl13 : tree1 ≡ node key₁ v₁ leaf tree₁ + repl13 = si-property1 (subst (λ k → stackInvariant key (node key₁ v₁ leaf tree₁ ) (replacePR.tree0 Pre) k) (∷-injectiveʳ eq) si ) +replaceP {n} {_} {A} key value {tree} repl (nd@( node key₁ value₁ left right) ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁ ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st Post ≤-refl where Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤) - Post = ? -- with replacePR.si Pre --- ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 --- ; rti = repl13 --- ; ri = repl12 ; ci = lift tt } where --- repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right) --- repl09 = si-property1 si --- repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) --- repl10 with si-property1 si --- ... | refl = si --- repl11 : stackInvariant key (node key₂ v1 tree₁ (node key₁ value₁ left right)) (replacePR.tree0 Pre) (node key₂ v1 tree₁ (node key₁ value₁ left right)∷ st1) --- repl11 = subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (k ∷ st1)) repl09 repl10 --- repl03 : child-replaced key (node key₁ value₁ left right) ≡ left --- repl03 with <-cmp key key₁ --- ... | tri< a1 ¬b ¬c = refl --- ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a) --- ... | tri> ¬a ¬b c = ⊥-elim (¬a a) --- repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right --- repl02 with repl09 | <-cmp key key₂ --- ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt) --- ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt) --- ... | refl | tri> ¬a ¬b c = refl --- repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1 --- repl04 = begin --- node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03 ⟩ --- node key₁ value₁ left right ≡⟨ sym repl02 ⟩ --- child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ --- child-replaced key tree1 ∎ where open ≡-Reasoning --- repl05 : node key₁ value₁ left right ≡ child-replaced key tree1 --- repl05 = begin --- node key₁ value₁ left right ≡⟨ sym repl02 ⟩ --- child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ --- child-replaced key tree1 ∎ where open ≡-Reasoning --- repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ repl right) --- repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) repl04 (r-left a (replacePR.ri Pre)) --- repl13 : treeInvariant (node key₁ value₁ repl right) --- repl13 = RTtoTI0 _ _ _ _ (subst (λ k → treeInvariant k) repl05 (treeRightDown _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) repl11 ) )) repl12 --- ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = repl13 ; ri = repl12 ; ci = lift tt } where --- repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁ --- repl09 = si-property1 si --- repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) --- repl10 with si-property1 si --- ... | refl = si --- repl03 : child-replaced key (node key₁ value₁ left right) ≡ left --- repl03 with <-cmp key key₁ --- ... | tri< a1 ¬b ¬c = refl --- ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a) --- ... | tri> ¬a ¬b c = ⊥-elim (¬a a) --- repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right --- repl02 with repl09 | <-cmp key key₂ --- ... | refl | tri< a ¬b ¬c = refl --- ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt) --- ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt) --- repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1 --- repl04 = begin --- node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03 ⟩ --- node key₁ value₁ left right ≡⟨ sym repl02 ⟩ --- child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ --- child-replaced key tree1 ∎ where open ≡-Reasoning --- repl05 : node key₁ value₁ left right ≡ child-replaced key tree1 --- repl05 = begin --- node key₁ value₁ left right ≡⟨ sym repl02 ⟩ --- child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ --- child-replaced key tree1 ∎ where open ≡-Reasoning --- repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ repl right) --- repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) repl04 (r-left a (replacePR.ri Pre)) --- repl11 = subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (k ∷ st1)) repl09 repl10 --- repl13 : treeInvariant (node key₁ value₁ repl right) --- repl13 = RTtoTI0 _ _ _ _ (subst (λ k → treeInvariant k) repl05 (treeLeftDown _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) repl11 ) )) repl12 + Post = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 _ (replacePR.si Pre) refl ; rti = lem14 ; ci = lift tt } where + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 = popStackInvariant _ _ _ _ _ (subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (nd ∷ tree1 ∷ st1) ) + (sym (si-property1 (replacePR.si Pre))) (replacePR.si Pre) ) + repl12 : (stack : List (bt A)) → stackInvariant key tree (replacePR.tree0 Pre) stack → stack ≡ (nd ∷ tree1 ∷ st1) + → replacedTree key value (child-replaced key tree1) (node key₁ value₁ repl right) + repl12 _ s-nil () + repl12 (leaf ∷ st₁) (s-right .leaf .(replacePR.tree0 Pre) tree₁ {key₂} {v₂} x si) () + repl12 (node k₁ v₁ left₂ right₂ ∷ st₁) (s-right .(node k₁ v₁ left₂ right₂) .(replacePR.tree0 Pre) tree₁ {key₂} {v₂} x si) eq = lem13 where + -- si : stackInvariant key (node key₂ v₂ tree₁ (node k₁ v₁ left₂ right₂)) (replacePR.tree0 Pre) st₁ + -- eq : node k₁ v₁ left₂ right₂ ∷ st₁ ≡ node key₁ value₁ left right ∷ tree1 ∷ st1 + lem20 : node k₁ v₁ left₂ right₂ ≡ node key₁ value₁ left right + lem20 = ∷-injectiveˡ eq + lem21 : tree1 ≡ node key₂ v₂ tree₁ (node k₁ v₁ left₂ right₂) + lem21 = (si-property1 (subst₂ (λ j k → stackInvariant key _ j k ) refl (∷-injectiveʳ eq) si )) + lem10 : node key₁ value₁ (child-replaced key (node k₁ v₁ left₂ right₂)) right ≡ child-replaced key tree1 + lem10 = begin + node key₁ value₁ (child-replaced key (node k₁ v₁ left₂ right₂)) right ≡⟨ cong ( λ k → node key₁ value₁ k right ) ( child-replaced-left repl13 ) ⟩ + node key₁ value₁ left₂ right ≡⟨ cong ( λ k → node key₁ value₁ k right ) (just-injective (cong node-left lem20)) ⟩ + node key₁ value₁ left right ≡⟨ sym lem20 ⟩ + node k₁ v₁ left₂ right₂ ≡⟨ sym ( child-replaced-right x) ⟩ + child-replaced key (node key₂ v₂ tree₁ (node k₁ v₁ left₂ right₂)) ≡⟨ sym ( cong (child-replaced key ) lem21 ) ⟩ + child-replaced key tree1 ∎ where + open ≡-Reasoning + repl13 : key < k₁ + repl13 = subst (λ k → key < k) (sym (just-injective (cong node-key lem20))) a + lem13 : replacedTree key value (child-replaced key tree1) (node key₁ value₁ repl right ) + lem13 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) lem10 (r-left a (replacePR.ri Pre)) + repl12 (leaf ∷ st₁) (s-left .tree .(replacePR.tree0 Pre) tree₁ {key₂} {v₂} x si) () + repl12 (node k₁ v₁ left₂ right₂ ∷ st₁) (s-left .(node k₁ v₁ left₂ right₂) .(replacePR.tree0 Pre) tree₁ {key₂} {v₂} x si) eq = lem13 where + lem20 : node k₁ v₁ left₂ right₂ ≡ node key₁ value₁ left right + lem20 = ∷-injectiveˡ eq + lem21 : tree1 ≡ node key₂ v₂ (node k₁ v₁ left₂ right₂) tree₁ + lem21 = (si-property1 (subst₂ (λ j k → stackInvariant key _ j k ) refl (∷-injectiveʳ eq) si )) + lem10 : node key₁ value₁ (child-replaced key (node k₁ v₁ left₂ right₂)) right ≡ child-replaced key tree1 + lem10 = begin + node key₁ value₁ (child-replaced key (node k₁ v₁ left₂ right₂)) right ≡⟨ cong ( λ k → node key₁ value₁ k right ) ( child-replaced-left repl13 ) ⟩ + node key₁ value₁ left₂ right ≡⟨ cong ( λ k → node key₁ value₁ k right ) (just-injective (cong node-left lem20)) ⟩ + node key₁ value₁ left right ≡⟨ sym lem20 ⟩ + node k₁ v₁ left₂ right₂ ≡⟨ sym ( child-replaced-left x) ⟩ + child-replaced key (node key₂ v₂ (node k₁ v₁ left₂ right₂) tree₁ ) ≡⟨ sym ( cong (child-replaced key ) lem21 ) ⟩ + child-replaced key tree1 ∎ where + open ≡-Reasoning + repl13 : key < k₁ + repl13 = subst (λ k → key < k) (sym (just-injective (cong node-key lem20))) a + lem13 : replacedTree key value (child-replaced key tree1) (node key₁ value₁ repl right ) + lem13 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) lem10 (r-left a (replacePR.ri Pre)) + lem14 : treeInvariant (node key₁ value₁ repl right) + lem14 = RTtoTI0 _ _ _ _ (child-repaced-ti key tree1 (siToTreeinvariant _ tree1 _ _ (replacePR.ti Pre) repl10 )) (repl12 _ (replacePR.si Pre) refl) ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st Post ≤-refl where Post : replacePR key value tree1 (node key₁ value left right ) (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤) - Post = ? --- with replacePR.si Pre --- ... | s-right _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = repl13 ; ri = repl12 b ; ci = lift tt } where --- repl09 : tree1 ≡ node key₂ v1 tree₁ tree -- (node key₁ value₁ left right) --- repl09 = si-property1 si --- repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) --- repl10 with si-property1 si --- ... | refl = si --- repl07 : child-replaced key (node key₂ v1 tree₁ tree) ≡ tree --- repl07 with <-cmp key key₂ --- ... | tri< a ¬b ¬c = ⊥-elim (¬c x) --- ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x) --- ... | tri> ¬a ¬b c = refl --- repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key tree1 ) (node key₁ value left right ) --- repl12 refl with repl09 --- ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node --- repl13 : treeInvariant (node key₁ value left right) --- repl13 = RTtoTI0 _ _ _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) (replacePR.si Pre)) r-node --- ... | s-left _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = repl13 ; ri = repl12 b ; ci = lift tt } where --- repl09 : tree1 ≡ node key₂ v1 tree tree₁ --- repl09 = si-property1 si --- repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) --- repl10 with si-property1 si --- ... | refl = si --- repl07 : child-replaced key (node key₂ v1 tree tree₁ ) ≡ tree --- repl07 with <-cmp key key₂ --- ... | tri< a ¬b ¬c = refl --- ... | tri≈ ¬a b ¬c = ⊥-elim (¬a x) --- ... | tri> ¬a ¬b c = ⊥-elim (¬a x) --- repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key tree1 ) (node key₁ value left right ) --- repl12 refl with repl09 --- ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node --- repl13 : treeInvariant (node key₁ value left right) --- repl13 = RTtoTI0 _ _ _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) (replacePR.si Pre)) r-node + Post = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 _ (replacePR.si Pre) refl ; rti = lem14 ; ci = lift tt } where + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 = popStackInvariant _ _ _ _ _ (subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (nd ∷ tree1 ∷ st1) ) + (sym (si-property1 (replacePR.si Pre))) (replacePR.si Pre) ) + repl12 : (stack : List (bt A)) → stackInvariant key tree (replacePR.tree0 Pre) stack → stack ≡ (nd ∷ tree1 ∷ st1) + → replacedTree key value (child-replaced key tree1) (node key₁ value left right) + repl12 _ s-nil () + repl12 (leaf ∷ st₁) (s-right .leaf .(replacePR.tree0 Pre) tree₁ {key₂} {v₂} x si) () + repl12 (node k₁ v₁ left₂ right₂ ∷ st₁) (s-right .(node k₁ v₁ left₂ right₂) .(replacePR.tree0 Pre) tree₁ {key₂} {v₂} x si) eq = lem13 where + lem20 : node k₁ v₁ left₂ right₂ ≡ node key₁ value₁ left right + lem20 = ∷-injectiveˡ eq + lem21 : tree1 ≡ node key₂ v₂ tree₁ (node k₁ v₁ left₂ right₂) + lem21 = (si-property1 (subst₂ (λ j k → stackInvariant key _ j k ) refl (∷-injectiveʳ eq) si )) + lem10 : node key value₁ left right ≡ child-replaced key tree1 + lem10 = begin + node key value₁ left right ≡⟨ cong (λ k → node k value₁ left right ) b ⟩ + node key₁ value₁ left right ≡⟨ sym lem20 ⟩ + node k₁ v₁ left₂ right₂ ≡⟨ sym ( child-replaced-right x) ⟩ + child-replaced key (node key₂ v₂ tree₁ (node k₁ v₁ left₂ right₂)) ≡⟨ cong (child-replaced key) (sym lem21) ⟩ + child-replaced key tree1 ∎ where + open ≡-Reasoning + lem13 : replacedTree key value (child-replaced key tree1) (node key₁ value left right) + lem13 = subst₂ (λ j k → replacedTree key value j (node k value left right) ) lem10 b r-node + repl12 (leaf ∷ st₁) (s-left .tree .(replacePR.tree0 Pre) tree₁ {key₂} {v₂} x si) () + repl12 (node k₁ v₁ left₂ right₂ ∷ st₁) (s-left .(node k₁ v₁ left₂ right₂) .(replacePR.tree0 Pre) tree₁ {key₂} {v₂} x si) eq = lem13 where + lem20 : node k₁ v₁ left₂ right₂ ≡ node key₁ value₁ left right + lem20 = ∷-injectiveˡ eq + lem21 : tree1 ≡ node key₂ v₂ (node k₁ v₁ left₂ right₂) tree₁ + lem21 = (si-property1 (subst₂ (λ j k → stackInvariant key _ j k ) refl (∷-injectiveʳ eq) si )) + lem10 : node key value₁ left right ≡ child-replaced key tree1 + lem10 = begin + node key value₁ left right ≡⟨ cong (λ k → node k value₁ left right ) b ⟩ + node key₁ value₁ left right ≡⟨ sym lem20 ⟩ + node k₁ v₁ left₂ right₂ ≡⟨ sym ( child-replaced-left x) ⟩ + child-replaced key (node key₂ v₂ (node k₁ v₁ left₂ right₂) tree₁ ) ≡⟨ cong (child-replaced key) (sym lem21) ⟩ + child-replaced key tree1 ∎ where + open ≡-Reasoning + lem13 : replacedTree key value (child-replaced key tree1) (node key₁ value left right) + lem13 = subst₂ (λ j k → replacedTree key value j (node k value left right) ) lem10 b r-node + lem14 : treeInvariant (node key₁ value left right) + lem14 = RTtoTI0 _ _ _ _ (child-repaced-ti key tree1 (siToTreeinvariant _ tree1 _ _ (replacePR.ti Pre) repl10 )) (repl12 _ (replacePR.si Pre) refl) ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st Post ≤-refl where Post : replacePR key value tree1 (node key₁ value₁ left repl ) st (λ _ _ _ → Lift n ⊤) - Post = ? - -- with replacePR.si Pre --- ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = repl13 ; ri = repl12 ; ci = lift tt } where --- repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right) --- repl09 = si-property1 si --- repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) --- repl10 with si-property1 si --- ... | refl = si --- repl03 : child-replaced key (node key₁ value₁ left right) ≡ right --- repl03 with <-cmp key key₁ --- ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c) --- ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c) --- ... | tri> ¬a ¬b c = refl --- repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right --- repl02 with repl09 | <-cmp key key₂ --- ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt) --- ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt) --- ... | refl | tri> ¬a ¬b c = refl --- repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1 --- repl04 = begin --- node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩ --- node key₁ value₁ left right ≡⟨ sym repl02 ⟩ --- child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ --- child-replaced key tree1 ∎ where open ≡-Reasoning --- repl05 : node key₁ value₁ left right ≡ child-replaced key tree1 --- repl05 = begin --- node key₁ value₁ left right ≡⟨ sym repl02 ⟩ --- child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ --- child-replaced key tree1 ∎ where open ≡-Reasoning --- repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ left repl) --- repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl) ) repl04 (r-right c (replacePR.ri Pre)) --- repl11 = subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (k ∷ st1)) repl09 repl10 --- repl13 : treeInvariant (node key₁ value₁ left repl) --- repl13 = RTtoTI0 _ _ _ _ (subst (λ k → treeInvariant k) repl05 (treeRightDown _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) repl11 ) )) repl12 --- ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = repl13 ; ri = repl12 ; ci = lift tt } where --- repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁ --- repl09 = si-property1 si --- repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) --- repl10 with si-property1 si --- ... | refl = si --- repl03 : child-replaced key (node key₁ value₁ left right) ≡ right --- repl03 with <-cmp key key₁ --- ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c) --- ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c) --- ... | tri> ¬a ¬b c = refl --- repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right --- repl02 with repl09 | <-cmp key key₂ --- ... | refl | tri< a ¬b ¬c = refl --- ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt) --- ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt) --- repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1 --- repl04 = begin --- node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩ --- node key₁ value₁ left right ≡⟨ sym repl02 ⟩ --- child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ --- child-replaced key tree1 ∎ where open ≡-Reasoning --- repl05 : node key₁ value₁ left right ≡ child-replaced key tree1 --- repl05 = begin --- node key₁ value₁ left right ≡⟨ sym repl02 ⟩ --- child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ --- child-replaced key tree1 ∎ where open ≡-Reasoning --- repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ left repl) --- repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl) ) repl04 (r-right c (replacePR.ri Pre)) --- repl13 : treeInvariant (node key₁ value₁ left repl) --- repl13 = RTtoTI0 _ _ _ _ (subst (λ k → treeInvariant k) repl05 (treeLeftDown _ _ --- (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) (subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (k ∷ st1)) repl09 repl10)) )) repl12 + Post = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 _ (replacePR.si Pre) refl ; rti = lem14 ; ci = lift tt } where + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 = popStackInvariant _ _ _ _ _ (subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (nd ∷ tree1 ∷ st1) ) + (sym (si-property1 (replacePR.si Pre))) (replacePR.si Pre) ) + repl12 : (stack : List (bt A)) → stackInvariant key tree (replacePR.tree0 Pre) stack → stack ≡ (nd ∷ tree1 ∷ st1) + → replacedTree key value (child-replaced key tree1) (node key₁ value₁ left repl ) + repl12 _ s-nil () + repl12 (leaf ∷ st₁) (s-right .leaf .(replacePR.tree0 Pre) tree₁ {key₂} {v₂} x si) () + repl12 (node k₁ v₁ left₂ right₂ ∷ st₁) (s-right .(node k₁ v₁ left₂ right₂) .(replacePR.tree0 Pre) tree₁ {key₂} {v₂} x si) eq = lem13 where + lem20 : node k₁ v₁ left₂ right₂ ≡ node key₁ value₁ left right + lem20 = ∷-injectiveˡ eq + lem21 : tree1 ≡ node key₂ v₂ tree₁ (node k₁ v₁ left₂ right₂) + lem21 = (si-property1 (subst₂ (λ j k → stackInvariant key _ j k ) refl (∷-injectiveʳ eq) si )) + lem10 : node key₁ value₁ left (child-replaced key (node k₁ v₁ left₂ right₂)) ≡ child-replaced key tree1 + lem10 = begin + node key₁ value₁ left (child-replaced key (node k₁ v₁ left₂ right₂)) ≡⟨ cong ( λ k → node key₁ value₁ left k ) ( child-replaced-right repl13 ) ⟩ + node key₁ value₁ left right₂ ≡⟨ cong ( λ k → node key₁ value₁ left k ) (just-injective (cong node-right lem20)) ⟩ + node key₁ value₁ left right ≡⟨ sym lem20 ⟩ + node k₁ v₁ left₂ right₂ ≡⟨ sym ( child-replaced-right x) ⟩ + child-replaced key (node key₂ v₂ tree₁ (node k₁ v₁ left₂ right₂)) ≡⟨ sym ( cong (child-replaced key ) lem21 ) ⟩ + child-replaced key tree1 ∎ where + open ≡-Reasoning + repl13 : k₁ < key + repl13 = subst (λ k → k < key) (sym (just-injective (cong node-key lem20))) c + lem13 : replacedTree key value (child-replaced key tree1) (node key₁ value₁ left repl ) + lem13 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl ) ) lem10 (r-right c (replacePR.ri Pre)) + repl12 (leaf ∷ st₁) (s-left .tree .(replacePR.tree0 Pre) tree₁ {key₂} {v₂} x si) () + repl12 (node k₁ v₁ left₂ right₂ ∷ st₁) (s-left .(node k₁ v₁ left₂ right₂) .(replacePR.tree0 Pre) tree₁ {key₂} {v₂} x si) eq = lem13 where + lem20 : node k₁ v₁ left₂ right₂ ≡ node key₁ value₁ left right + lem20 = ∷-injectiveˡ eq + lem21 : tree1 ≡ node key₂ v₂ (node k₁ v₁ left₂ right₂) tree₁ + lem21 = (si-property1 (subst₂ (λ j k → stackInvariant key _ j k ) refl (∷-injectiveʳ eq) si )) + lem10 : node key₁ value₁ left (child-replaced key (node k₁ v₁ left₂ right₂)) ≡ child-replaced key tree1 + lem10 = begin + node key₁ value₁ left (child-replaced key (node k₁ v₁ left₂ right₂)) ≡⟨ cong ( λ k → node key₁ value₁ left k ) ( child-replaced-right repl13 ) ⟩ + node key₁ value₁ left right₂ ≡⟨ cong ( λ k → node key₁ value₁ left k ) (just-injective (cong node-right lem20)) ⟩ + node key₁ value₁ left right ≡⟨ sym lem20 ⟩ + node k₁ v₁ left₂ right₂ ≡⟨ sym ( child-replaced-left x) ⟩ + child-replaced key (node key₂ v₂ (node k₁ v₁ left₂ right₂) tree₁ ) ≡⟨ sym ( cong (child-replaced key ) lem21 ) ⟩ + child-replaced key tree1 ∎ where + open ≡-Reasoning + repl13 : k₁ < key + repl13 = subst (λ k → k < key) (sym (just-injective (cong node-key lem20))) c + lem13 : replacedTree key value (child-replaced key tree1) (node key₁ value₁ left repl ) + lem13 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl ) ) lem10 (r-right c (replacePR.ri Pre)) + lem14 : treeInvariant (node key₁ value₁ left repl ) + lem14 = RTtoTI0 _ _ _ _ (child-repaced-ti key tree1 (siToTreeinvariant _ tree1 _ _ (replacePR.ti Pre) repl10 )) (repl12 _ (replacePR.si Pre) refl) TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) → (r : Index) → (p : Invraiant r) → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r) -... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim ? ) -- +... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (nat-≡< b (≤-trans (s≤s z≤n) lt ) ) ) ... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (m≤n⇒m≤1+n lt1) p1 lt1 ) where TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t - TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim ?) -- (lemma5 n≤j lt1)) + TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (nat-≤> (≤-trans (s≤s z≤n) lt1) n≤j ) ) TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 ) @@ -1149,6 +1184,7 @@ $ λ _ x1 P1 → insertTreeP x1 3 2 (proj1 P1) $ λ _ x2 P2 → insertTreeP x2 2 2 (proj1 P2) (λ _ x P → x ) + -- is realy inserted? -- other element is preserved?
--- a/RBTree.agda Sun Aug 18 20:02:03 2024 +0900 +++ b/RBTree.agda Sat Aug 24 19:20:47 2024 +0900 @@ -1,5 +1,5 @@ -- {-# OPTIONS --cubical-compatible --safe #-} -{-# OPTIONS --cubical-compatible #-} +{-# OPTIONS --allow-unsolved-metas --cubical-compatible #-} module RBTree where open import Level hiding (suc ; zero ; _⊔_ )