Add properties that characterize Data.Tree.AVL.Indexed.delete.#2961
Open
mikedelorimier wants to merge 1 commit intoagda:masterfrom
Open
Add properties that characterize Data.Tree.AVL.Indexed.delete.#2961mikedelorimier wants to merge 1 commit intoagda:masterfrom
Data.Tree.AVL.Indexed.delete.#2961mikedelorimier wants to merge 1 commit intoagda:masterfrom
Conversation
These are properties for the core delete on AVL trees and similar to the prexisting properties of `insert`. Lemmas added for `delete` are `delete⁺`, `delete-tree⁻`, `delete-key-∈⁻` and `delete-key⁻`. Together these can be used to prove `(k′ ∈ delete k t) ⇔ (k′ ≉ k × k′ ∈ t)`, which fully characterizes `delete`. `delete⁺`, `delete-tree⁻`, and `delete-key⁻` correspond to Coq.FSets.FSetInterface's `remove_2`, `remove_3`, and `remove_1`, respectively. Just like other lemmas in this file, `delete⁺`, `delete-tree⁻`, `delete-key⁻` generalize `k′ ∈ t` to `Any P t`. `delete-key-∈⁻` is essentally a helper for `delete-key⁻`, which would be difficult to prove directly. Many more lemmas were added for AVL functions that `delete` depends on. These additional lemmas characterize the functions `castʳ`, `joinˡ⁺`, `joinʳ⁺`, `joinˡ⁻`, `joinʳ⁻`, `headTail`, and `join`. Adding all this code to Properties.agda caused `make test` to overflow past the 4096 MB default heap size. This was solved by breaking Properties.agda into multiple files, with roughly one file for each AVL function. Added proofs are a similar style the preexisting proofs in Properties.agda.
JacquesCarette
requested changes
Mar 15, 2026
Collaborator
JacquesCarette
left a comment
JacquesCarette
left a comment
There was a problem hiding this comment.
Fantastic work. But a few things may need tweaked.
|
|
||
| castʳ⁻ : ∀ {l m u h} {lm : Tree V l m h} {m<u : m <⁺ u} → | ||
| Any P (castʳ lm m<u) → Any P lm | ||
| castʳ⁻ {lm = node _ _ _ _} (here p) = here p |
Collaborator
There was a problem hiding this comment.
Do you really need to 'force' ln to a node for this to work?
| (p : Any P t) → lookupKey p ≉ k → | ||
| Any P (proj₂ (delete k t seg)) | ||
| delete⁺ (leaf _) _ p _ = p | ||
| delete⁺ (node (k′ , v) lk′ k′u bal) (l<k , k<u) p p≉k |
Collaborator
There was a problem hiding this comment.
since you uniformly do with on both compare and p, I recommend that you do both of them at once.
| Any P t₁ → Any P (proj₂ (join t₁ t₂ bal)) | ||
| join-left⁺ _ (leaf _) ∼- p = castʳ⁺ p | ||
| join-left⁺ {hʳ = suc _} t₁ t₂₃@(node _ _ _ _) bal p | ||
| with headTail t₂₃ |
Collaborator
There was a problem hiding this comment.
irrefutable with ?
| (r : Tree V [ kv .key ] u hʳ) → | ||
| (bal : hˡ ∼ hʳ ⊔ h) → | ||
| P kv → Any P (proj₂ (joinˡ⁺ kv l r bal)) | ||
| joinˡ⁺-here⁺ k₂ (0# , t₁) t₃ bal p = here p |
Collaborator
There was a problem hiding this comment.
For further clarify, don't bother naming all the things you don't use in the rhs.
| joinˡ⁺-here⁺ k₄ (1# , node k₂ t₁ t₃ ∼0) t₅ ∼- p = right (here p) | ||
| joinˡ⁺-here⁺ k₆ (1# , node⁺ k₂ t₁ k₄ t₃ t₅ bal) t₇ ∼- p = right (here p) | ||
|
|
||
| joinˡ⁺-left⁺ : ∀ {l u hˡ hʳ h} → |
Collaborator
There was a problem hiding this comment.
Same comment throughout this file: don't name unused arguments.
| joinˡ⁺⁻ k₂ (0# , t₁) t₃ ba = Any.toSum | ||
| joinˡ⁺⁻ k₂ (1# , t₁) t₃ ∼0 = Any.toSum | ||
| joinˡ⁺⁻ k₂ (1# , t₁) t₃ ∼+ = Any.toSum | ||
| joinˡ⁺⁻ k₄ (1# , node k₂ t₁ t₃ ∼-) t₅ ∼- = λ where |
Collaborator
There was a problem hiding this comment.
This sub-function is used twice -- name it?
| joinʳ⁺-here⁺ k₂ t₁ (0# , t₃) bal p = here p | ||
| joinʳ⁺-here⁺ k₂ t₁ (1# , t₃) ∼0 p = here p | ||
| joinʳ⁺-here⁺ k₂ t₁ (1# , t₃) ∼- p = here p | ||
| joinʳ⁺-here⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+) ∼+ p = left (here p) |
Collaborator
There was a problem hiding this comment.
Do these 2 cases need to be separate?
| joinʳ⁺-left⁺ k₂ t₁ (0# , t₃) bal p = left p | ||
| joinʳ⁺-left⁺ k₂ t₁ (1# , t₃) ∼0 p = left p | ||
| joinʳ⁺-left⁺ k₂ t₁ (1# , t₃) ∼- p = left p | ||
| joinʳ⁺-left⁺ k₂ t₁ (1# , node k₄ t₃ t₅ ∼+) ∼+ p = left (left p) |
Collaborator
There was a problem hiding this comment.
same question here: merge those 2 cases?
| private | ||
| Val = Value.family V | ||
|
|
||
| singleton⁺ : {P : Pred (K& V) p} → |
Collaborator
There was a problem hiding this comment.
in the next two functions, should some of the arguments be implicit?
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
These are properties for the core delete on AVL trees and are similar to the preexisting properties of
insert.Lemmas added for
deletearedelete⁺,delete-tree⁻,delete-key-∈⁻anddelete-key⁻. Together these can be used to prove(k′ ∈ delete k t) ⇔ (k′ ≉ k × k′ ∈ t), which fully characterizesdelete.delete⁺,delete-tree⁻, anddelete-key⁻correspond to Coq.FSets.FSetInterface'sremove_2,remove_3, andremove_1, respectively.Just like other lemmas in Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties,
delete⁺,delete-tree⁻,delete-key⁻generalizek′ ∈ ttoAny P t.delete-key-∈⁻is essentally a helper fordelete-key⁻, which would be difficult to prove directly.Many more lemmas were added for AVL functions that
deletedepends on. These additional lemmas characterize the functionscastʳ,joinˡ⁺,joinʳ⁺,joinˡ⁻,joinʳ⁻,headTail, andjoin. Adding all this code to Properties.agda causedmake testto overflow past the 4096 MB default heap size. This was solved by breaking Properties.agda into multiple files, with roughly one file for each AVL function.Added proofs are a similar style the preexisting proofs in Properties.agda.