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!