Is there any documentation of the induction tactic syntax?

Stream: mathlib4

[Geoffrey Irving]

I am a bit dismayed that now I am forced to rewrite all of my uses of induction' (primed) to the new unprimed syntax throughout various repos, though I understand the motivation for cleaning it up.

But, at least: is there a page documenting the syntax? The Mathlib4 source doesn't seem to do this (typically, Mathlib doesn't contained documentation for Mathlib tactics), but also the Lean 4 manual doesn't seem to do it either.

[Geoffrey Irving]

If a page documenting the syntax did exist, it would be wonderful to link to it from

1. https://leanprover-community.github.io/mathlib4_docs/Init/Tactics.html#Lean.Parser.Tactic.induction
2. Some of the error messages in https://github.com/leanprover-community/mathlib4/commit/5e8936e560f53cd39eb49ed22e93662a0f0a1928 (this I guess is obsolete, not that the tactic is just gone)

[Julian Berman]

I think #general > Discussion thread for Lean Language Reference @ 💬 is a related message from David with his thoughts at least at that moment.

[Geoffrey Irving]

I should clarify that I am less concerned about abstract thoughts than I am about actually knowing how to use the tactic. I don't know how to use induction. I can piece it together with a bunch of grepping through mathlib, but usually when I do things that way I miss some of the flavour and different modes of how to use things. My impression is that induction is a commonly used tactic, and I would like to understand it well.

[Geoffrey Irving]

Ah, I think you interpreted "documenting the syntax" as "provide a formal grammar". I meant a normal page with any kind of documentation at all!

[Julian Berman]

Indeed I did -- the latter seems lots more likely to already exist but I don't know of where specifically it might be, I see #mil still uses induction' at least.

[Geoffrey Irving]

This is generally where my frustration is coming from: banning a core tactic I've used for years without documenting the replacement is not an amazing user experience.

[Etienne Marion]

Isn’t the syntax documented in https://leanprover-community.github.io/mathlib4_docs/Init/Tactics.html#Lean.Parser.Tactic.induction?

[Aaron Liu]

Is the stuff at docs#Lean.Parser.Tactic.induction not enough? Can you spell out what you might be looking for from a documentation page that's not present there?

[Michael Rothgang]

Does https://leanprover-community.github.io/mathlib-manual/html-multi//Tactics/All-tactics/#induction-next answer your question?

[Michael Rothgang]

That's the tactic doc-string, I believe. (In general, if that "all tactics" page in the mathlib manual fails to mention at tactic, that's a bug.)

[Geoffrey Irving]

Examples are things that are not mentioned:

1. What is the newline structure if you don't have a one line use? That page gives exactly one example of the syntax showing where the child tactics go, but it's a one-liner. This is the most confusing thing to start.
2. Making explicit that one has to use the names of the arguments in the induction principle? I think? Maybe one doesn't have do that, or could use n + 1? There's no discussion of why you can do n+1 for match and not here, or whether they are in fact different.

[Michael Rothgang]

New tactics have to be added manually at the moment, so it's possible this is lagging behind. The field tactic is missing, for example.

[Geoffrey Irving]

Michael Rothgang said:

That's the tactic doc-string, I believe. (In general, if that "all tactics" page in the mathlib manual fails to mention at tactic, that's a bug.)

This is the same as the thing which I think is insufficient. I should say that you're catching me in a very narrow window of still being confused about things like newline syntax, flexibility, etc. Soon I am going to forget about this as learn the tactic and settle into the long, slow process of manually fixing my code to be more verbose than it used to be. (Cursor seems quite unreliable at doing this translation, but maybe it'll improve for longer files with more context.)

[Michael Rothgang]

I agree, the tactic docstring is not comprehensive enough. Sorry for that!

[Geoffrey Irving]

No worries! I do appreciate that once I do the translation I'll have all the benefits of the more verbose syntax.

[Michael Rothgang]

Let me also add: induction' is deprecated within mathlib --- you can still use it in your projects. (Yes, it can be nice to migrate. But waiting for good migration guides is a valid reason to wait, and you point out that some things are indeed missing.)

[Geoffrey Irving]

Aha! I may hold off on the translation as yet, then. And I imagine I can avoid deprecation warnings too?

[Michael Rothgang]

You can turn off the deprecation linter using set_option. (The linter even tells you how.) If you add this to your lakefile, the warning is off project-wide.