RFC: `List.take_drop` and `List.drop_take`

Stream: batteries

[François G. Dorais]

This theorem just landed in Std from std4#272, upstreaming a variety of useful List theorems from Mathlib. I just noticed this theorem:

theorem drop_take : ∀ (m n : Nat) (l : List α), drop m (take (m + n) l) = take n (drop m l)

It seems to me this theorem (which is not a simp) is much more useful as a rewrite rule in the other direction:

theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l)

The reason is that the lhs catches all take-drop combinations. For the drop-take combination, this lemma seems more useful for the same reason.

theorem drop_take : ∀ (m n : Nat) (l : List α), drop n (take m l) = take (m - n) (drop n l)

With omega in core, we don't need to worry as much about adding Nat operations on the rhs. So I think the two proposed alternatives are objectively better.

I'm asking before doing a PR because the original theorem came from Mathlib and the proposed changes might be disruptive downstream.

[Joachim Breitner]

If you have both yourtake_drop and drop_take (which I agree seem plausible), won't that loop? It seems we have to pick one order as the normal form and only rewrite the other

[Joachim Breitner]

Or are you only proposing them as rw rules to be used manually? Then this isn't a concern of course.

[Eric Wieser]

Isn't the usual rule to put the simpler term on the RHS?

[Eric Wieser]

It sounds like you're claiming the opposite rule of "put the more syntactically general term on the LHS"

[Joachim Breitner]

Yes, that is one good general rule, but not the only one, and sometimes it's not clear what's best.
I'm generally wairy of non-linear LHSs (those where one variable occurs multiple times), they are very brittle and often get in the way of confluence. I experimented a bit with checking local confluence of simp lemmas in https://github.com/nomeata/lean-simplc and non-linearity was one main cause for non-confluence.

I think I'd prefer the drop_take rule shown last; it applies generally, and m - n is in some sense simpler, because smaller than m + n. And take of drop seems to be the natural order, first removing unwanted elements, and then selecting those to keep.

But that's just gut feeling; the interplay between the full set of simp rules matter.

[François G. Dorais]

Neither is intended as a simp, the original form is also not simp. My question is why not use the direction that makes more sense for rewrites. I think these (together with take_take and drop_drop) are meant to allow sequences of drops and takes to be reorganized into a single drop-take or take-drop.

I can't see an objective reason to prefer drop-take or take-drop, but we could just pick one as a normal form and use that as guidance. @Joachim Breitner seems to prefer take-drop. In that case, it makes sense to replace the current drop_take with

theorem drop_take : ∀ (m n : Nat) (l : List α), drop n (take m l) = take (m - n) (drop n l)

I wouldn't mark it simp but it would make sense for users to manually add it when needed.

[François G. Dorais]

(deleted)

[Eric Wieser]

My question is why not use the direction that makes more sense for rewrites.

Perhaps a natural conclusion of this is that _maybe_ it's desirable to be able to name a lemma in one direction, but mark it as simp in the other (in cases where it makes sense to be a simp lemma in the first)

[François G. Dorais]

Yes, maybe. But I think the situation is more complex.

My original point is that we can sometimes disregard adding arithmetical complexity because they can be postponed and resolved easily using awesome tools like omega.

Joachim brought up an excellent point where the proposed drop_take lemma is actually simplifying. If we count list operations, assuming the "generic" case where n ≤ m and m + n ≤ l.length, the lhs takes m + n ops whereas the rhs takes (m - n) + n = m ops. Of course, one needs to take into account calculating m - n. This does take the missing n ops using basic successor arithmetic, but in reality it takes O(log(m+n)) ops which is dwarfed by the list operations.

Anyway, it seems there could be a greater discussion about the general issue here, but probably in another thread with broader audience.

[Mario Carneiro]

I think it would be best to just not try to normalize these

[François G. Dorais]

I think that matches the thumbed up proposal above to change the lemma so it is more applicable but not mark it as simp.

Does that make sense to you @Mario Carneiro and @Eric Wieser?

[Mario Carneiro]

I would not replace the original, both variants look useful

[François G. Dorais]

For the sake of avoiding primes or other meaningless annotations, do you think it makes sense to reword the original drop_take as mentioned above:

theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l)

Of course, neither this nor the proposed drop_take would be maked as simp lemmas.

[Joe Hendrix]

One challenge with these lemmas is that there are many List (and other data structures) is that there are many operations and so even the pairwise combination is quite large. I think for List, ensuring there are good simp rules for (op ..).get? and then relying on List.ext is a good option for expressions involving take/drop/append.

I'm not sure what's best to do for operations such as List.filter, and longer term we likely will want something with better automation.

[Timo Carlin-Burns]

Another possibility would be to reduce the number of distinct list operations by grouping them based on their effect on the "shape" of the list. For example, take, drop, dropFirst, dropLast, and eraseIdx all have the effect of removing a contiguous range of indices from the list. If we had eraseRange, we could define all of the above as abbrevs in terms of eraseRange. If we did this for all of the List methods, we would drastically reduce the number of simp lemmas we need

[Joachim Breitner]

That is an option - at the expense that running simp will turn simple functions the user likes to see into a something more complicated that they didn't write.
I'm wondering if having the n² lemmas is really so bad, if each of these lemmas is quickly written. This means more work in the libraries, but good simp behavior for the users.

[James Gallicchio]

my gut is telling me that List.take and List.drop are best characterized in terms of prefixes/suffixes, not List.get. But I have not yet tried incorporating them into LeanColls.

[James Gallicchio]

List.take n L = L' \iff L'.length = min(n, L.length) \and L' <+: L or something

[James Gallicchio]

not very simp-friendly though

[Kim Morrison]

It's good to have characteristic lemmas, but they are not a replacement for the n^2 "successive operations" or n*m "operation then observation" lemmas. More of a backup!

[James Gallicchio]

if we could get automation to do

generalize hLtake : List.take n L = Ltake at *
rw [List.take_char] at hLtake

whenever it sees List.take n L, I would give it a try :P

[Kim Morrison]

@James Gallicchio, I don't understand why we would want that. Can you give more context?

[James Gallicchio]

I don't really have a context in mind for it. But I've been experimenting with reasoning about collections generically, and remember this pattern coming up. Let me look for an example.

[François G. Dorais]

Belated announcement... the PR exists std4#710

Right now it only deletes the old drop_take and replaces it by two theorems:

theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l) := ...

theorem drop_take : ∀ (m n : Nat) (l : List α), drop n (take m l) = take (m - n) (drop n l) := ...

Note that neither is simp and the old drop_take is now Eq.symm (take_drop ...).

I'm glad this discussion is happening and I'm happy to make changes accordingly. Also feel free to comment on the PR itself.

[Timo Carlin-Burns]

Joachim Breitner said:

That is an option - at the expense that running simp will turn simple functions the user likes to see into a something more complicated that they didn't write.

Is there a way, maybe with delaborators, to make sure that operations which are expressible as one of the specialized functions are pretty printed that way? I think you could get the best of both worlds of nice shorthands and streamlined reasoning

[Joachim Breitner]

Hmm, that’s a dangerous amount of magic, I fear…

The GHC simplifier has phases, so it would rewrite .drop to eraseRange, then do the main work, and at the end rewrite eraseRange back to dropif it fits. This would indeed reduce the number of lemmas needed while keeping the proof goals simple, at the expense that simp will do “something” even if it doesn’t do anything useful and ends up returning the same goal.

And then there are more general approaches (match up to equivalences and whatnot) that may also help here, maybe we’ll get them eventually.

Until then, just writing many theorems isn’t so bad, and thanks to the discrimination trees, at least it’s not going to slow down simp to have them.

[Joe Hendrix]

The downsides with writing many theorems from my perspective are:

• You probably want consistency across other Array and other sequence types so that increaases workload further.
• Users interested in seeing what they can prove have to look through it all.
• Each theorem may break when upstream changes occur. More lemmas = more chances to break.
• The fragments of logic when working with arrays/lists has many undecidable subproblems (e.g., monoid word problem) so set of "reasonable" lemmas is probably larger than quadratic with respect to number of operations. Practically, users will probably want lemmas involving things like taking apart a list with take/drop and then rebuilding.

If one could write up a crisp characterization of what the proposed "N^2" lemmas are, then I'd feel more confident that was the correct approach.

Longer term, there's also a lot of research in "string" theories in SMT that eventually may help with Lean automation.

[Mario Carneiro]

If one could write up a crisp characterization of what the proposed "N^2" lemmas are, then I'd feel more confident that was the correct approach.

The reference to "N^2" should be fairly clear about this much: it's referring to the pairwise interaction of every two definitions in the API. Obviously this is very oversimplified: many pairs can't be placed close enough together to interact, and some can be placed in multiple ways. But generally speaking I think the bound is approximately correct - there are O(1) ways to combine two constants together, and in any case it is good guidance on the question "how do I make an API that 'feels complete'".

[Mario Carneiro]

The fragments of logic when working with arrays/lists has many undecidable subproblems (e.g., monoid word problem) so set of "reasonable" lemmas is probably larger than quadratic with respect to number of operations.

I think this reasoning is incorrect. The word problem is undecidable, but it is "finitely generated": there are a fixed finite set of lemmas which give you the moves and there is an infinite space of ways you can combine them. We only need to give the generating set, not the full space. Most of the points in the space are not interesting anyway: we do not want a lemma that says x + 0 + 0 + 0 = x because we can obtain it using only lemmas in the "generating set" in a very straightforward way (= "by simp")

[François G. Dorais]

Mario Carneiro said:

The fragments of logic when working with arrays/lists has many undecidable subproblems (e.g., monoid word problem) so set of "reasonable" lemmas is probably larger than quadratic with respect to number of operations.

I think this reasoning is incorrect.

Yes, this is incorrect reasoning: this is the free monoid, which does have decidable equality.

[François G. Dorais]

Mario Carneiro said:

The word problem is undecidable, but it is "finitely generated": there are a fixed finite set of lemmas which give you the moves and there is an infinite space of ways you can combine them. We only need to give the generating set, not the full space. Most of the points in the space are not interesting anyway: we do not want a lemma that says x + 0 + 0 + 0 = x because we can obtain it using only lemmas in the "generating set" in a very straightforward way (= "by simp")

This is right, the word problem is semi-decidable and simp is a semi-decision tool: it's always right but it can fail.

[François G. Dorais]

It's perfectly reasonable to make complete simp rules for the word problem, non-withstanding depth limits and such.

[Joe Hendrix]

I should have not elaborated on the decidability issue; I think that's irrelevant to the current discussion.

Pragmatically, I think the number of lemmas is large and I still haven't a nice writeup of what the strategy beyond all pairwise combination of lemmas for some unspecified set of operations. I think it'd be great to see a nice writeup.

[Kim Morrison]

Just a general remark: the n * m lemmas about the n operations and the m observations are generally higher priority than the n * n lemmas. e.g. for BitVec, the observations are something like .getLsb i, getMsb i, msb, toNat, ...

Once you have all those lemmas, you can hope that often but not always the proofs of the n^2 lemmas are ext <;> simp (sometimes having to hold ext's hand and tell it which "observation" to use).

[Eric Wieser]

Scott Morrison said:

Just a general remark: the n * m lemmas about the n operations and the m observations are generally higher priority than the n * n lemmas. e.g. for BitVec, the observations are something like .getLsb i, getMsb i, msb, toNat, ...

Is this a good place to draw the core / std or std / mathlib line?

[Mario Carneiro]

Not in my opinion. The line would be more once you get beyond just direct implications of the definitions (the n * n lemmas) and into more sophisticated (and mathematically interesting) properties, but I think it is more difficult to make that precise

[Joachim Breitner]

You probably want consistency across other Array and other sequence types so that increaases workload further.

Right. But part of the (mental) work load is wondering “which lemmas do we need” and “for a given lemma, should it be simp”.

The every-two-function-interaction rule helps deciding that. I imagine it would go together with a documented linear ordering of functions which gives their desired ordering, so that you know which way to go (I’d expect :: to be the outermost because that’s the value normal form, it would probably prefer map (filter …) over filter (map …), because one can rewrite in one direction well but not in the other, maybe a tendency to push unary operations like map and filter into binary ones like ++ … I don’t have a complete set of rules yet, but I hope they can be found). This gives guidance and should also help to keep the simp-set non-looping.

Ideally (maybe I am being too optimistic or spoiled by isabelle), each of these lemmas is a two liner consisting of one extensionality or induction (maybe functional inductinon) tactic and one closing tactic (by induction … <;> simp_all), so the individual workload should be low.

As for multiple types: if you have Arrays and Lists then you probably want, in this maximalists view, every lemma for lists also for arrays, and visa-verse. Plus 2×n lemmas about how toArray and toList interact with each operation. One nice thing is that a local confluence checker would, once you have the toArray lemma for an operation, tell you about all the missing lemmas within that type.

Of course, this desire to have confluence in the simp lemma has implications that need to be weighted. It means that if
you had both docs#List.length_replicate and docs#List.replicate_add as simp lemmas, you also should have docs#Nat.left_distrib (and docs#List.length_append) as a simp lemma. Right now docs#Nat.left_distrib isn’t a simp lemma, and probably for a good reason, and this therefore give guidance that docs#List.replicate_add shouldn’t be a simp lemma either. I find that helpful.

[Jannis Limperg]

Joachim Breitner said:

Ideally (maybe I am being too optimistic or spoiled by isabelle), each of these lemmas is a two liner consisting of one extensionality or induction (maybe functional inductinon) tactic and one closing tactic (by induction … <;> simp_all), so the individual workload should be low.

As one data point, I made a test file for Aesop containing the first 100 lemmas from mathlib3's data.list.basic (this was before Mathlib4 was a thing). With some sensible Aesop rules, ~95% of these lemmas are by aesop or by induction x <;> aesop (and the aesop call often comes down mostly to simp_all).

[Joe Hendrix]

@Jannis Limperg Thanks for sharing. That's good to hear.

Are the comments such as "-- attribute [-simp] subset_def" affecting Aesop by disabling the named lemmas?

[Kim Morrison]

This change has caused a breakage in Mathlib. See #11833. If anyone is able to take a look that would be great. (This will be needed to release v4.8.0-rc1 and get Mathlib on it.)

[Kim Morrison]

The problem is in Mathlib/Combinators/Enumerative/Composition.lean, in get_splitWrtCompositionAux. Perhaps @Sébastien Gouëzel (the author) or @Yaël Dillies is able to take a look?

[Eric Wieser]

(there's probably no point looking for another hour, since there is no cache yet :) )

[Kim Morrison]

Depends on your machine, I guess. :-)

In any case, I just fixed this, sorry for the noise.

[Jannis Limperg]

Joe Hendrix said:

Jannis Limperg Thanks for sharing. That's good to hear.

Are the comments such as "-- attribute [-simp] subset_def" affecting Aesop by disabling the named lemmas?

This test file was originally an evaluation for the Aesop paper. For lemmas that were already ported to Mathlib4 at the time and were tagged @[simp], I removed the simp attribute so that Aesop wouldn't trivially succeed. For lemmas that weren't tagged @[simp], I wrote these comments to indicate that I had checked this. But the comments have no effect on Aesop.