extend simps

Stream: mathlib4

[Kenny Lau]

#mathlib4 > A quadratic scaling problem @ 💬

@Robin Carlier and others have expressed interest to change @[simps] in some ways, such as adding more projections that aren't a part of the definition; let's discuss it here

[Robin Carlier]

My two "wishes" for [simps] and [simps!] are that

1. The current logging is very painful to navigate. When writing or reviewing code it’s crucial to use @[simps!?] and @[simps?] to check the generated lemmas, and the current system is hard to read. It would be super cool have an output ressembling that of a failing grind call. I have explored this a bit privately but this did not get very far.
2. More importantly, current simps/simps! is very bad with inductive types: it often generates lemmas with match arms in the RHS, and the "correct" lemmas are often obtained by applying a constructor to one of the inputs, in these cases we have to do every lemma manually which is boring, repetitive, takes up code space (e.g here), but can’t really be avoided if one wants good characterizing lemmas (I’ll let you imagine what it would be if the inductive type in this example had 4 constructors instead of 2...). Perhaps this falls under the umbrella of what @Robert Maxton described as "custom projections"?

[Robin Carlier]

Also: this message #general > "Missing Tactics" list @ 💬 is relevant for this discussion.

[Floris van Doorn]

Yeah, simps still has a lot of rough edges, and improvements are welcome (there are also a bunch of open issues in the Mathlib4 issue tracker).

Adding simp-lemmas for definitions where one of the arguments is an inductive type is indeed nice, but it might be nice to think how you want to design that precisely, since it's complicated. For example, if I have two arguments of type Option α, we can potentially generate 9 lemmas:

variable, variable (the only one we can currently generate)
variable, some
variable, none
some, variable
some, some
some, none
none, variable
none, some
none, none

Which ones do we generate by default? How do we specify others we want to generalize?
How does this work if the arguments have type Option ℕ? How does it interact with the codomain having as type a structure that generates 4 simp-lemmas?
Another tricky thing is to compute the "correct" right-hand side of the simp-lemma (though you could just apply simp to compute it after unfolding the definition, and that might be fine).

It is even more complicated if you want to add more custom projections that are not of the form "apply to a constructor (or a definitionally equal variant) of an inductive type" or "apply (definitionally equal variant of) a projection of the return-type". I believe this is what @Robert Maxton was suggesting in the post linked above. In that case I'm not even sure how you'd compute the right-hand-side of the generated lemmas (unless you just unfold the new definition and call simp).

[Kenny Lau]

Floris van Doorn said:

unless you just unfold the new definition and call simp

is there any drawbacks to this?

[Floris van Doorn]

That might be fine. I'm not sure if that is the lemma you actually want in the use cases people care about.
The only drawback I can imagine is that it might be somewhat slow to call simp once for every lemma you generate (but we already do that for @[simps!] IIRC).

[Robin Carlier]

Yes, I agree that one of the main problem with "apply constructor of the inductive" is that we need to be able to surgically specify (and name!) which generated lemmas we want and which ones we don’t. I guess a discussion thread like this is specifically made so that this can be discussed and we can come up with ideas before doing any actual implementations. I do not guarantee that I would have time or skills do to a full implementation anyways, but at least having a focused proposal would be good starting point.

[Robin Carlier]

I think the default behavior with inductive should stay unchanged (so that we don’t suddenly generate a huge amount of lemmas), and then perhaps we could have syntax [simps! +inductive foo] which says that "for every argument of type foo in the generated lemmas, build for their consructor"? This would at least be a start, though it wouldn’t handle well the case you describe where the declaration takes many inductive of the same type as input and we only want to apply constructor to some but not all of them.

[Robin Carlier]

so, only "opt-in" when dealing with inductives.

[Aaron Liu]

Can we have custom simps projections that aren't just wrappers around the default projections

[Robert Maxton]

Floris van Doorn said:

It is even more complicated if you want to add more custom projections that are not of the form "apply to a constructor (or a definitionally equal variant) of an inductive type" or "apply (definitionally equal variant of) a projection of the return-type". I believe this is what @Robert Maxton was suggesting in the post linked above. In that case I'm not even sure how you'd compute the right-hand-side of the generated lemmas (unless you just unfold the new definition and call simp).

Essentially, yes. For some type Foo you'd write down a "computed field" Foo.bar, which is approximately just a definition for which projection notation would be valid, and then every time you make a definition of type Foo simps would attempt to create a lemma of the form x.bar = _.

@Robin Carlier's idea appears to essentially be the dual concept -- writing custom 'coprojections' /possibly-non-canonical constructors such that, whenever simps creates a lemma that accepts a Foo, it should (instead?) create lemmas for each possible constructor, registered noncanonical constructors included. Then we could just use the existing initialize_simps_projections command to say e.g. "please write lemmas that accept variables of Option α and also values of the form some _, but not none" (purely as an example, I'm not sure we'd actually want to register Option this way."