feat: add lemma code-action

[adomani]

The 'lemma' command elaborates as 'theorem' but gives warning + codeaction to use 'theorem' instead.

I am picking up @jcommelin's PR #413, but I did not know how to modify the old one, so I am opening a new one.

[adomani]

awaiting-review

[fgdorais]

While lemma shouldn't be used in Std (for legitimate reasons). I think it's inappropriate to force that idea on downstream projects. Certainly, downstream projects should not be advised to use Mathlib just to avoid this minor issue.

I would prefer that Std.Tactic.Lemmas exists and introduces the lemma command without any apologies, restrictions, nor alternate recommendations. That lemma shouldn't be used in Std itself is best handled by a linter.

[digama0]

Certainly, downstream projects should not be advised to use Mathlib just to avoid this minor issue.

Downstream projects don't have to use mathlib, you can declare the lemma command in one line given the implementation here. It could even be an option. But recommending to import mathlib is useful in case this was a typo - this is in fact the whole point of adding the lemma keyword to std, to improve the error message you get when using lemma when the relevant file isn't imported.

[adomani]

I view it as follows. Std does not impose lemma on downstream projects, but offers it with minimal effort. If a user of a downstream project writes lemma, they probably expect it to work. The code action gives a no-effort change that works. With minimal effort, they can "turn lemmas on". Moreover, since lemma is not a Std thing, the suggestion to think about Mathlib seems helpful, rather than intrusive.

[fgdorais]

When you say it's easy to turn on lemmas, you're only measuring the number of lines of code needed. But it is not discoverable and nothing else works that way. At least, the error message should say how to turn on lemmas.

I still don't understand the utility of throwing a special error message if lemma is not implemented. The main effect I see are users asking "why is theorem better than lemma?" or "how do I turn on corollaries?" on Zulip. Why shouldn't Std just provide the lemma command and let users decide whether to use it or not?

[adomani]

I think that the argument against Std introducing lemma is to avoid it straying from the core syntax: there is no interest in introducing lemma into core.

I am happy to add a line to the error mentioning how to turn on lemmas.

This is the most common use-case of the error, for me. Some mathematician who has no idea of what a programming language is, finds a tutorial with lemma in, pastes it into "lean" and gets confused by the error message. I am sure that someone with any computer science knowledge will not think that trying random words hoping that they match the syntax of the language should be supported -- these people will likely not even reach the stage of seeing the error message above.

[digama0]

I still don't understand the utility of throwing a special error message if lemma is not implemented.

I think this sets a bad precedent, if we are not allowed to implement error messages for things that are not in the grammar but are known to be common misspellings. These are essentially independent design questions (or at least they should be independent):

1. Should lemma be part of the grammar?
2. For code which is syntactically incorrect (like a use of lemma assuming "no" to 1), should we give a better error message?

I don't like the implication that an attempt to implement 2 requires us to implement 1 as well, or contrapositively, if we say "no" to 1 then we cannot do anything to improve 2.

[digama0]

Honestly, I think it would be great if one could paste well formed Coq code using Theorem, Corollary etc, and get an error message saying that you meant to use theorem instead, with a code action that performs the replacement. This is not at all to say that I want Theorem to be valid lean syntax.

[fgdorais]

Honestly, I think it would be great if one could paste well formed Coq code using Theorem, Corollary etc, and get an error message saying that you meant to use theorem instead, with a code action that performs the replacement. This is not at all to say that I want Theorem to be valid lean syntax.

So lemma is a red herring... That makes sense! I couldn't understand the fixation on lemma. I can definitely get behind a solution that catches common misspellings and such, proposes alternatives and a code action to boot!

I'm still perplexed by the implementation of the current (partial) solution. We actually are providing an implementation for lemma as a synonym for theorem, then we hide it behind a switch. That's unusual but worse is that keeping the switch off has no real benefit for users.

[digama0]

I'm still perplexed by the implementation of the current (partial) solution. We actually are providing an implementation for lemma as a synonym for theorem, then we hide it behind a switch. That's unusual but worse is that keeping the switch off has no real benefit for users.

The reason is because we know that, in the contexts where it works, lemma is supposed to be followed by the same syntax as theorem, and it does the same thing. So if we go ahead with that interpretation (after logging the error using logError, not throwError) then there will be less breakage downstream of this error: not only will we not complain that the following token is not a command, we can even understand uses of the declared lemma in the next def/theorem. (The analogue with Theorem is that we would expect valid Coq syntax to follow it, and we would translate that syntax into lean syntax to interpret it and for the code action.)

In other words, good recovery from lemma involves actually knowing what it does and how it works, which is why it's already 90% of the work of an actual implementation! So in that light it's natural to just give people a flag to turn off the error if they want to enable the lemma statement itself, since it would just duplicate this logic. If people wanted lemma with a different behavior, they would just ignore this code and write their own lemma parser.

[fgdorais]

That makes sense. I still think just enabling lemma is a better experience than this for users but I understand that it shouldn't be part of the grammar. I'm happy to move on to more practical matters.

Let's talk about that switch though. It's unique in design and not easily discoverable. How about making it an option that could be controlled locally using set_option and globally by setting it in the lakefile (or even the command line)?

• This uses well known command set_option that is normally used for turning features on and off. Adding a line or two to the lakefile is something that users can grok easily.
• It's clear that this is an extension of the language, especially if the option is called std.lang.lemma_extension, for example.
• There is no "precedent issue". Lean's syntax is extensible by design, it expected for Std to provide some such extensions but not all of them, and there is no doubt lemma is a desirable such extension.
• Mathlib users wouldn't have to worry about including Mathlib.Tactic.Lemma since the option would be set in the lakefile. (They would still need to include Std but it's hard for a Mathlib user not to do that.)

I don't see disadvantages of using that mechanism.

[fgdorais]

I just edited to use the option lang.lemmaCmd to control whether lemma is allowed or not. Feel free to revert if the old switch mechanism was preferable.

[adomani]

I personally do not have a preference between the initial version and the new set_option switch: I'm happy to go with either.

I suspect that most people who will try to use lemma will do so while looking at someMathlib-based tutorial. Thus, I find that a reference to Mathlib would be more useful than simply mentioning how to switch on lemma "in isolation". However, I am also happy to wait and see whether the Mathlib-agnostic error sparks comments on Zulip before reassessing, if needed.

[fgdorais]

Bummer. Looks like options that aren't declared in core (or plugins?) can't be set in the lakefile/command line. Using option won't work well for Mathlib unless that changes: set_option would have to be used in each file that uses lemma rather than being set globally in the lakefile. I think this is a bug with the option mechanism or a bug in my understanding how it should work.

Reverting to the old switch is probably best for now but let's see what @joehendrix and @digama0 have to say.

PS: It looks like putting this in a plugin could work but I'm not sure.

[digama0]

Bummer. Looks like options that aren't declared in core (or plugins?) can't be set in the lakefile/command line.

I've been planning to write a fix for that for some time. Please report it as an issue so we can track it; I'm pretty sure that we can get consensus that this is undesirable, it's just a matter of designing a better solution. The reason this is the case is that lean needs to know the type of each option to typecheck the inputs for it, but maybe we can delay the typechecking for unknown options until after imports have been processed.

[fgdorais]

Issue filed at lean4#3403.

[fgdorais]

Lean core PR #4741 may finally enable this to work!

[fgdorais]

lean4#4741 has landed in v4.11.0-rc1. This PR is now ready for a final review and hopefully a quick merge!