API building helper

Stream: mathlib4

[Rémy Degenne]

I have a preliminary idea for a simple tool that would help building API for a definition, and I would like to hear other's opinions about whether it would be useful and how best to do it.

Example of the issue I want to solve

Let say that I defined def foo (a : A) (b : B) where A and B are types with some typeclasses on them. For example A is defined in a variable line and has [AddCommMonoid A] and B is Measure X for some other type X. Then I add several lemmas. At the time of adding the definition, I have in mind applications in which a changes, but b is a given measure. I think about adding foo_add for foo (a + a') b, and foo_zero_left, perhaps foo_zero_right about b=0. But since I don't think about changing b, which is not something I do in my application, I don't think about adding any lemma about the addition, the order or the lattice structure of Measure X. I also don't think about those because those typeclasses are not readily apparent when I look at the context of my definition: I only see Measure X.
Then a few months later someone wants to use foo for another application, and they find holes in the API: they would like foo_mono_right stating that foo is monotone for the order on measures.
That scenario with measures happened to me recently with Measure.withDensity.

Idea for a solution

Could we help the person writing the definition by providing suggestions for the API? I am thinking of a command #suggest_api foo that would provide a list of lemma statements with proof sorry.

• If there is a zero in A, it adds lemma foo_zero_left (b : B) : foo (0 : A) b = sorry := sorry
• If there is an addition, it adds lemma foo_add_left (a a' : A) (b : B) : foo (a + a') b = sorry := sorry. Similarly for multiplication.
• It also creates default lemmas for any detected order, or for sup and inf for a lattice. Possibly for more typeclasses as well.
• Do that for all explicit arguments, and ignore implicit arguments?
• If the definition is foo (a a' : A), we could add a lemma for the case a = a'.

We could consider going further and if for example there is an order on A and on the type of foo a b, suppose that foo is monotone and create a lemma for that. Suppose that the value at 0 or 1 is 0 or 1 (if those exist), etc.

The result of the command is a big block of code with many statements, that can be inserted at the point where the command is written.

It is likely that many of those lemmas are not interesting: perhaps foo does not interact well with addition, or has no special value at 0. But then the user can very simply delete those and keep only the relevant entries.
The idea is to create many plausible statements to help the definition creator think about all the API lemmas needed, even if most are not useful: deleting is cheap.

There is an issue with automatic naming. _left and _right are fine in the example above because there is only two arguments, but that does not work if there are 3. I think getting the names right matters, since newer contributors will tend to think that the auto-generated names follow the naming convention.

I would like to know if that seems useful. Also I don't currently have the Lean programming knowledge to create that command myself, and I don't think that I will find a time to learn that soon. So this post is also a call to anybody interested: if it looks useful to you, feel free to implement that yourself!
Even a very simple implementation that does not try to be smart about the lemmas created would already bring most of the benefits.

[Daniel Weber]

A small negative of this is that it could waste effort on API nobody will ever use. I don't know how that compares to the inconvenience of missing API

[Rémy Degenne]

Yes it could waste some effort. But it would not force you to prove any of the suggestions, it would just hint that those might be lemmas you want. If you don't want to spend time on them, you remove them. In my mind, the majority of the suggestions will be simply deleted.

I just feel like I often have to PR an obvious lemma foo_zero to some definition just because someone (often me) forgot to include it earlier.