Porting note: Fixing up `mono`

Stream: mathlib4

[Thomas Murrills]

@Yaël Dillies reminded me of my old porting-era effort to port mono (#2323), which was still an open PR. I'll repeat some of my comment on that PR here:

I believe the consensus from a long-ago porting meeting was that the PR introduced too much infrastructure, that the stopgap behavior (using solve_by_elim) was ok, and that we had another tactic (which I now forget) to handle some specific cases anyway.

However, mono is still just using that stopgap behavior. There's currently no distinction between mono and mono*, and it actually throws errors upon seeing left/right/both, with, and using syntax.

Now that we're post-port, I feel like there's an argument to be made for intentionally abandoning or modifying some of the syntax:

• mono ... with was essentially an artifact of mono's bespoke backtracking procedure.
• using could still be supported in spirit, and perhaps pass lemmas to a solve_by_elim or aesop call.
• left and right could be useful to someone, and it maybe makes sense to have some way to distinguish between different sorts of lemmas based on strictness, but I'm not sure calling them "left" and "right" is really a clear, understandable abstraction. Also, mono left and mono right seem pretty infrequent.

What should we do with mono? Relevant questions include:

• Should we simply jettison all other syntax and make the current behavior the only behavior?
• Should we switch to aesop instead of solve_by_elim?
• Should we make an effort to improve the API and provide something instead of left and right to distinguish between docs#mul_lt_mul and docs#mul_lt_mul'?
• Or should we even still try to port the lean 3 version with some modifications, such as giving mono single-step behavior and preserving left, right, and using behavior?

I feel the best choice to make is the one preferred by users of mono. I'm not a user of mono, so I can't really give an opinion here.

How do people feel?

[Yaël Dillies]

I assume the tactic you're referring to is Heather'sgcongr?

[Thomas Murrills]

Yes, I believe so! Thanks, I couldn't quite remember.

[Ruben Van de Velde]

Removing the unsupported syntax seems like the lowest effort improvement and doesn't prevent us from adding it back if someone needs it

[Thomas Murrills]

We could do that, but would that amount to leaving another porting note? I'm kind of wondering what people think the "final" ported version of mono in lean 4 should be (with respect to how it was in lean 3).

[Kim Morrison]

What problem is mono actually solving at this point? Can we just not have it?

[Thomas Murrills]

Fwiw, I'm not counting many uses: maybe 10-20 if we include porting notes mentioning it? Could be worth just trying to replace those and see what happens (if we want to try removing it).

[Mario Carneiro]

I would be in support of just dropping mono and replacing it with gcongr and similar tactics, and/or redesigning a mono-alike from a clean slate

[Moritz Doll]

I've used mono a bit in the Lean 3 days and gcongr feels so much user-friendlier than mono was.

[Michael Rothgang]

#13881 is a PR replacing most occurrence of mono by gcongr. #13890 is a drive-by clean-up (not strictly required) - to enable using gcongr in one more instance. Review welcome!

[Michael Rothgang]

I would like feedback on 136a9e6: it seems gcongr doesn't pick up local hypothesis by itself? Help welcome how to makes this as nice as the one-line mono was.

[Michael Rothgang]

In two cases, I need help: after gcongr, a goal remains which is not so obvious to me (apparently mono used local hypotheses)

• in ContinuedFractions/Computation/Approximations.lean
• in Dynamics/OmegaLimit.lean

With these fixed, all occurrences of mono can be replaced by gcongr!

[Michael Rothgang]

In the mean-time, some more PRs removed the uses of mono in the above two files. #25698 removes the last use.

[Michael Rothgang]

#25700 (WIP) proposes a syntax lint against the tactic. Are there any reasons not to have this?

[Junyan Xu]

Can we add a deprecated attribute to a tactic and the linter would lint against all deprecated tactics?

[Johan Commelin]

That sounds like a good idea to me.

[Jovan Gerbscheid]

Speaking of deprecating tactics, there is a variant of gcongr called rel, which I don't think many people know about.

gcongr by default uses a basic discharger that attempts things like assumption and symm to close main goals, and otherwise leaves them as side goals. rel on the other hand takes a list of arguments that it uses to discharge the side goals, and throws an error if it can't prove all the goals.

But essentially, rel [a,b,c] can be replaced by gcongr; exacts [a,b,c] which is more robust since it is now clear which subgoal corresponds to which of a,b,c. (or we can use have := a; have := b; have := c; gcongr)

So I propose using the same deprecation attribute for rel. Do people want to be able to pass arguments to gcongr to discharge its main goals?

[Patrick Massot]

rel is explicitly a teaching tactic. It should play no role in mathlib but stay available.

[Michael Rothgang]

Junyan Xu said:

Can we add a deprecated attribute to a tactic and the linter would lint against all deprecated tactics?

Functionally, that is what the deprecated syntax linter does.
Implementation-wise, it does so manually instead of a deprecation attribute on the tactics. This matches its behaviour on cases' and refine', for example. I'm happy about a PR adding a deprecation attribute, but it doesn't feel high priority to me.