Add properties that characterize Data.Tree.AVL.Indexed.delete.

[mikedelorimier]

These are properties for the core delete on AVL trees and are similar to the preexisting 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 Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties, 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]

Fantastic work. But a few things may need tweaked.

[JacquesCarette]

since you uniformly do with on both compare and p, I recommend that you do both of them at once.

[jamesmckinna]

And, again arguably, p could be handled by 'ordinary' pattern matching clauses, with the with compare... analysis subsidiary to that? Anything to help manage the readability problem!

[JacquesCarette]

irrefutable with ?

[jamesmckinna]

or even let bind the result? alternatively, use using syntax

[JacquesCarette]

For further clarify, don't bother naming all the things you don't use in the rhs.

[JacquesCarette]

Same comment throughout this file: don't name unused arguments.

[JacquesCarette]

This sub-function is used twice -- name it?

[JacquesCarette]

Do these 2 cases need to be separate?

[JacquesCarette]

same question here: merge those 2 cases?

[JacquesCarette]

in the next two functions, should some of the arguments be implicit?

[jamesmckinna]

Not only that, but why is V a parameter to the anonymous module, whereas all the other arguments are local to the functions being defined, when those functions share the same telescope of hypotheses?

The private declaration of Val can be inlined as a telescope-level let binding, I think, or even, if shared, simply really inlined?

[jamesmckinna]

This looks impressive, but reading this PR was heavy going, to say the least. FWIW, I might have preferred this PR in two stages:

• code motion of the existing proofs under Any.Properties, which could be easily merged without having to think too hard
• a separate follow-up PR which isolates what is new, both for the Join* properties, and then also those for Delete and the ancillary stuff

As for your own proofs, the original code in Indexed seems to have been written to rely a bit too heavily on with, as a consequence of which your own code has to do elaborate gymnastics in order to cope downstream.

Suggested simplifications strip out some, but not yet all, of such things, and hopefully provide a model for subsequent refactoring/simplification...

A subsequent refactoring might wish to reconsider the basics under Indexed, with 'with sometimes considered harmful' borne in mind... cf #2123 / #2369

[jamesmckinna]

This can be drastically simplified as follows

Suggested change

	headTail-head⁻ (node {hˡ = suc _} _ t₁₂ _ _) p
	with headTail t₁₂
	headTail-head⁻ (node {hˡ = suc _} _ t₁₂@(node _ _ _ _) _ _) p
	| k₁ , l<k₁ , t₂ = left (headTail-head⁻ t₁₂ p)
	headTail-head⁻ {P = P} (node _ t₁₂@(node _ _ _ _) _ _) p = left (headTail-head⁻ {P = P} t₁₂ p)

where, unfortunately, the threading of {P = P} from LHS to RHS seems necessary, unless the same let-binding trick is used to obtain as a wholesale rewrite

headTail-head⁻ : ∀ {l u h} → (t : Tree V l u (suc h)) →
                 let k , _ = headTail t in
                 P k → Any P t
headTail-head⁻ (node _ (leaf _) _ ∼+) p = here p
headTail-head⁻ (node _ (leaf _) _ ∼0) p = here p
headTail-head⁻ (node _ t₁₂@(node _ _ _ _) _ _) p = left (headTail-head⁻ t₁₂ p)

[jamesmckinna]

Eg as a specimen refactoring, the first two clauses could be simplified if the original defn of headTail were modified as follows:

In Height, add the lemma

0∼ : ∀ {i m} → 0 ∼ i ⊔ m → i ≡ m
0∼ ∼+ = refl
0∼ ∼0 = refl

and then in Indexed, change the definition of headTail instead to read

 headTail : ∀ {l u h} → Tree V l u (1 + h) →
             ∃ λ (k : K& V) → l <⁺ [ k .key ] ×
                            ∃ λ i → Tree V [ k .key ] u (i ⊕ h)
  headTail (node k₁ (leaf l<k₁) t₂ bal) with refl ← 0∼ bal = k₁ , l<k₁ , 0# , t₂
  headTail (node k₃ t₁₂@(node _ _ _ _) t₄ bal)
    using (k₁ , l<k₁ , t₂) ← headTail t₁₂ = k₁ , l<k₁ , joinˡ⁻ _ k₃ t₂ t₄ bal

UPDATED: now part of #2968

[mikedelorimier]

For changes in this PR that depend on #2968, is it best to I wait for #2968 to merge, or to stack on jamesmckinna:refactor-AVL?

[jamesmckinna]

Use of with considered (sometimes) harmful... Instead, can simplify as follows

Suggested change

	headTail⁺ : ∀ {l u h} (t : Tree V l u (1 + h)) →
	Any P t →
	P (proj₁ (headTail t))
	⊎ Any P (proj₂ (proj₂ (proj₂ (headTail t))))
	headTail⁺ (node _ (leaf _) _ ∼+) (here p) = inj₁ p
	headTail⁺ (node _ (leaf _) _ ∼+) (right p) = inj₂ p
	headTail⁺ (node _ (leaf _) _ ∼0) (here p) = inj₁ p
	headTail⁺ (node {hˡ = suc _} k₃ t₁₂@(node _ _ _ _) t₄ bal) (here p)
	with headTail t₁₂
	... | k₁ , l<k₁ , t₂ = inj₂ (joinˡ⁻-here⁺ k₃ t₂ t₄ bal p)
	headTail⁺ (node {hˡ = suc _} k₃ t₁₂@(node _ _ _ _) t₄ bal) (left p)
	with headTail t₁₂ | headTail⁺ t₁₂ p
	... | k₁ , l<k₁ , t₂ | inj₁ ph = inj₁ ph
	... | k₁ , l<k₁ , t₂ | inj₂ pt = inj₂ (joinˡ⁻-left⁺ k₃ t₂ t₄ bal pt)
	headTail⁺ (node {hˡ = suc _} k₃ t₁₂@(node _ _ _ _) t₄ bal) (right p)
	with headTail t₁₂
	... | k₁ , l<k₁ , t₂ = inj₂ (joinˡ⁻-right⁺ k₃ t₂ t₄ bal p)
	headTail⁺ : ∀ {l u h} (t : Tree V l u (suc h)) →
	Any P t → let k , l<k , i , t⁻ = headTail t in
	P k ⊎ Any P t⁻
	headTail⁺ (node _ (leaf _) _ ∼+) (here p) = inj₁ p
	headTail⁺ (node _ (leaf _) _ ∼+) (right p) = inj₂ p
	headTail⁺ (node _ (leaf _) _ ∼0) (here p) = inj₁ p
	headTail⁺ (node k₃ t₁₂@(node _ _ _ _) t₄ bal) (here p)
	= let _ , _ , t⁻ = headTail t₁₂ in inj₂ (joinˡ⁻-here⁺ k₃ t⁻ t₄ bal p)
	headTail⁺ (node k₃ t₁₂@(node _ _ _ _) t₄ bal) (left p)
	= let _ , _ , t⁻ = headTail t₁₂ in Sum.map id (joinˡ⁻-left⁺ k₃ t⁻ t₄ bal) (headTail⁺ t₁₂ p)

UPDATED to remove the implicit pattern binding of {hˡ = suc _}

[jamesmckinna]

Granted that the case analysis on bal appears to be necessary for the sake of the termination checker, this can however be made a bit less indigestible as follows:

Suggested change

	headTail-tail⁻ (node {hˡ = suc _} k₃ t₁₂@(node _ _ _ _) t₄ bal) p
	with k₁ , l<k₁ , t₂ ← headTail t₁₂ in eq
	-- This match on `bal` is so the termination checker sees `h`
	-- decrease.
	| joinˡ⁻⁻ k₃ t₂ t₄ bal p | bal | eq
	... | inj₁ pk | _ | ≡-refl = here pk
	... | inj₂ (inj₁ pl) | ∼+ | ≡-refl = left (headTail-tail⁻ t₁₂ pl)
	... | inj₂ (inj₁ pl) | ∼0 | ≡-refl = left (headTail-tail⁻ t₁₂ pl)
	... | inj₂ (inj₁ pl) | ∼- | ≡-refl = left (headTail-tail⁻ t₁₂ pl)
	... | inj₂ (inj₂ pr) | _ | ≡-refl = right pr
	headTail-tail⁻ (node k₃ t₁₂@(node _ _ _ _) t₄ bal) p
	using k₁ , l<k₁ , t₂ ← headTail t₁₂
	with joinˡ⁻⁻ k₃ t₂ t₄ bal p
	... | inj₁ pk = here pk
	... | inj₂ (inj₂ pr) = right pr
	... | inj₂ (inj₁ pl) using p⁻ ← headTail-tail⁻ t₁₂ pl with bal
	... | ∼+ = left p⁻
	... | ∼0 = left p⁻
	... | ∼- = left p⁻

[jamesmckinna]

For the 'improvement' below, it seems cleaner to follow the let-binding rephrasing, and write instead:

Suggested change

	headTail-tail⁻ : ∀ {l u h} (t : Tree V l u (1 + h)) →
	Any P (proj₂ (proj₂ (proj₂ (headTail t)))) →
	Any P t
	headTail-tail⁻ : ∀ {l u h} (t : Tree V l u (suc h)) →
	let _ , _ , _ , t⁻ = headTail t in
	Any P t⁻ → Any P t

[jamesmckinna]

The repetition between the first and third clauses here can be handled by analysis of the bal constraint , which in fact forces the heights to be equal, and thus these two can be collapsed into one, here and similarly elsewhere throughout the development. In that sense the pattern match on here p is conceptually prior to that of the tree and its balance factor.

UPDATED: see #2968 for this analysis in the definition of headTail...

[jamesmckinna]

Ditto. here as to how to avoid the duplication.

[jamesmckinna]

Is it clearer to handle these subcomputations via a where block, rather than using a let?

[jamesmckinna]

Ditto.

[jamesmckinna]

I think that Agda is smart enough to detect this clause as impossible anyway, so could be deleted.

[jamesmckinna]

No need to match {hʳ = suc _} here?

[jamesmckinna]

Similarly, t₁ must be a leaf _ instance, and the balance factor 0#/1# can be ignored.

[jamesmckinna]

Ditto.

[jamesmckinna]

Similarly, I'd reorder to consider here p clauses before right p clauses, and then collapse the two clauses by ignoring the balance factor and noting that t₁ is in fact a leaf _...

[jamesmckinna]

Ditto.

[jamesmckinna]

Ditto., but now for t₃...

[jamesmckinna]

Similarly: reorder clauses and collapse.

[jamesmckinna]

These cases can be simplified by ignoring the balance factor, and even noting that t₁ must in fact be an instance of leaf _, so a pattern synonym might be useful additional machinery to handle this case.

UPDATED: see #2968 for examples of this.

[jamesmckinna]

Blocks such as this might be better be handled in one go via Any.toSum

[jamesmckinna]

Ditto. Any.toSum (and then you can eta-contract as well ;-))

[jamesmckinna]

Ditto.

[jamesmckinna]

Any.toSum twice.

[jamesmckinna]

Ditto.

[jamesmckinna]

Ditto.

[jamesmckinna]

Suggested change

	join-node⁻ _ lk′ k′u bal p with join⁻ lk′ k′u bal p
	... | inj₁ p₁ = left p₁
	... | inj₂ p₂ = right p₂
	join-node⁻ _ lk′ k′u bal p
	= Sum.[ (λ p → left p) , (λ p → right p) ] (join⁻ lk′ k′u bal p)

[jamesmckinna]

... And this could even be inlined in the single place where join-node⁻ is invoked?

[jamesmckinna]

Indeed, no need to do the case analysis:

Suggested change

	join-right⁺ {hʳ = suc _} t₁ t₂₃@(node _ _ _ _) bal p
	with headTail t₂₃ | headTail⁺ t₂₃ p
	... | k₂ , m<k₂ , t₃ | inj₁ ph =
	joinʳ⁻-here⁺ k₂ (castʳ t₁ m<k₂) t₃ bal ph
	... | k₂ , m<k₂ , t₃ | inj₂ pt =
	joinʳ⁻-right⁺ k₂ (castʳ t₁ m<k₂) t₃ bal pt
	join-right⁺ t₁ t₂₃@(node _ _ _ _) bal p
	using k₂ , m<k₂ , t₃ ← headTail t₂₃
	= Sum.[ joinʳ⁻-here⁺ k₂ (castʳ t₁ m<k₂) t₃ bal
	, joinʳ⁻-right⁺ k₂ (castʳ t₁ m<k₂) t₃ bal ]′
	(headTail⁺ t₂₃ p)

[jamesmckinna]

Suggested change

	join⁻ {hʳ = suc _} t₁ t₂₃@(node _ _ _ _) bal p
	with (k₂ , m<k₂ , t₃) ← headTail t₂₃ in eq
	| joinʳ⁻⁻ k₂ (castʳ t₁ m<k₂) t₃ bal p | eq
	... | inj₁ pk | ≡-refl = inj₂ (headTail-head⁻ t₂₃ pk)
	... | inj₂ (inj₁ pl) | ≡-refl = inj₁ (castʳ⁻ pl)
	... | inj₂ (inj₂ pr) | ≡-refl = inj₂ (headTail-tail⁻ t₂₃ pr)
	join⁻ t₁ t₂₃@(node _ _ _ _) bal p
	using k₂ , m<k₂ , t₃ ← headTail t₂₃
	with joinʳ⁻⁻ k₂ (castʳ t₁ m<k₂) t₃ bal p
	... | inj₁ pk = inj₂ (headTail-head⁻ t₂₃ pk)
	... | inj₂ (inj₁ pl) = inj₁ (castʳ⁻ pl)
	... | inj₂ (inj₂ pr) = inj₂ (headTail-tail⁻ t₂₃ pr)

[jamesmckinna]

This is an impossible clause (p = ()), so could be deleted.

[jamesmckinna]

A large number of sub-terms are irrelevant to this analysis, as they merely recapitulate the recursion analysis already present in the definition of delete (perhaps one solution is to reconsider the implicit/explicit bindings in the various join lemmas), so this may be considerably streamlined as follows:

Suggested change

	delete-tree⁻ (node (k′ , v) lk′ k′u bal) (l<k , k<u) p
	with compare k′ k
	delete-tree⁻ (node kv@(k′ , v) lk′ k′u bal) (l<k , k<u) p
	| tri< k′<k _ _
	with joinʳ⁻⁻ kv lk′ (delete k k′u ([ k′<k ]ᴿ , k<u)) bal p
	... | inj₁ pk = here pk
	... | inj₂ (inj₁ pl) = left pl
	... | inj₂ (inj₂ pr) = right (delete-tree⁻ k′u ([ k′<k ]ᴿ , k<u) pr)
	delete-tree⁻ (node kv@(k′ , v) lk′ k′u bal) (l<k , k<u) p
	| tri> _ _ k′>k
	with joinˡ⁻⁻ kv (delete k lk′ (l<k , [ k′>k ]ᴿ)) k′u bal p
	... | inj₁ pk = here pk
	... | inj₂ (inj₁ pl) = left (delete-tree⁻ lk′ (l<k , [ k′>k ]ᴿ) pl)
	... | inj₂ (inj₂ pr) = right pr
	delete-tree⁻ (node (k′ , v) lk′ k′u bal) (l<k , k<u) p
	| tri≈ _ _ _ =
	join-node⁻ v lk′ k′u bal p
	delete-tree⁻ (node kv@(k′ , _) l u bal) (l<k , k<u) p with compare k′ k
	delete-tree⁻ (node kv l u bal) (_ , k<u) p
	| tri< k′<k _ _
	using k′<k<u ← [ k′<k ]ᴿ , k<u
	with joinʳ⁻⁻ kv l (delete k u k′<k<u) bal p
	... | inj₁ pk = here pk
	... | inj₂ (inj₁ pl) = left pl
	... | inj₂ (inj₂ pr) = right (delete-tree⁻ u k′<k<u pr)
	delete-tree⁻ (node kv l u bal) (l<k , _) p
	| tri> _ _ k′>k
	using l<k<k′ ← l<k , [ k′>k ]ᴿ
	with joinˡ⁻⁻ kv (delete k l l<k<k′) u bal p
	... | inj₁ pk = here pk
	... | inj₂ (inj₁ pl) = left (delete-tree⁻ l l<k<k′ pl)
	... | inj₂ (inj₂ pr) = right pr
	delete-tree⁻ (node _ l u bal) _ p
	| tri≈ _ _ _ = join-node⁻ _ l u bal p

which shows off the dependencies of the recursive calls on the corresponding appeals to join lemmas...

[mikedelorimier]

Thanks for the detailed review! I'll just start chugging along on your comments...

[jamesmckinna]

Consider also all the various equivalent ways in which the hypothesis 'k is not the key at position p' is expressed in the types of insertWith⁺, insert, and lookup⁺, and then also now your own delete⁺, and perhaps we could refactor to reconcile all the expression of all these equivalent statements...? See the discussion on #2968 ;-)

[jamesmckinna]

Thanks for the detailed review! I'll just start chugging along on your comments...

NB. Some of my suggested refactorings may depend on the modifications to the definitions of eg Indexed.headTail etc. also suggested by me. So it remains to be seen if (some; modest) additional refactoring is required to get things to typecheck!?

UPDATED: see #2968

[jamesmckinna]

Looping back to your original preamble, I haven't seen exactly the same memory issues as you when checking even the new Properties of delete and friends in the one module, so I'd be interested to know if the reorganisation into submodules is really necessary (although as time goes on, we're bound to hit hard memory limits on GitHub eventually)...
... FTR I check things locally on a Gen8 Lenovo X1 Carbon with 16GB of RAM, but agda never occupies even 4GB (top -o %MEM reports max usage as 3.9GB/24.9%... but YMMV)

[mikedelorimier]

Looping back to your original preamble, I haven't seen exactly the same memory issues as you when checking even the new Properties of delete and friends in the one module, so I'd be interested to know if the reorganisation into submodules is really necessary (although as time goes on, we're bound to hit hard memory limits on GitHub eventually)... ... FTR I check things locally on a Gen8 Lenovo X1 Carbon with 16GB of RAM, but agda never occupies even 4GB (top -o %MEM reports max usage as 3.9GB/24.9%... but YMMV)

Yes, it was annoying to split up Properties.agda because this should be a different PR than the delete addition. Unfortunately I didn't keep my old code with all my additions in Properties.agda so it's difficult to reproduce the out-of-memory. I did repeat make clean; make test 4 times and saw that it ran out of mem each time.

Possibly the difference is due to a different ghc or agda versions. I was running with ghc version 9.4.8 and agda version 2.7.0.1. Probably it's not due to different max heap size settings, since my max heap size was 4GB, and you measured a max usage of about 4GB. The difference is also probably not due to my laptop, which has 32GB RAM, is AMD Ryzen 7 7735U, Pangolin 13.

It's counterintuitive to me that checking a large file takes much memory when there are no cyclic dependencies in the file and no holes. Comparing line number counts in the stdlib, Data.Nat.Properties has the max of 2501 and there are only 1074 lines of Data.Tree.AVL.Indexed.Relation.Unary.Any.* (post split). So it's somewhat surprising that the pre-split Properties was the worst in the stdlib.

However, checking the unsplit Properties.agda was very slow, which made me think it was a good idea to split it up at some point, regardless of the memory issue.

[mikedelorimier]

In the updated Singleton it seems arbitrary to me which arguments are in private variable and which are module _ parameters. For example, in Singleton, is there a reason for l u : Key⁺ to be variables rather than module params?