Docs for `induction` and `cases`

Stream: general

[Filippo A. E. Nuccio]

When doing

#help tactic induction

a long message presenting the different options is displayed, and one can read "You can use with to provide the variables names for each constructor." This is false, this only works with induction', that is also somewhat mentioned but with the doc " The induction' tactic is similar to the induction tactic in Lean 4 core, but with slightly different syntax (such as, no requirement to name the constructors)." That sounds a bit cryptic, to me: I would say that one advantage of induction' is that you can name them!

Similarly, the doc for cases contains "You can use with to provide the variables names for each constructor." that is false, but becomes true for cases' and once more the small doc about cases' has no reference to the fact that it is a good variation to name the constructors. It is also a pity that rcases is not mentioned in the cases docs.

I wanted to open a PR to modify these docs, but I cannot find where they are. The def evalCases contained in Lean/Elab/Tactic/Induction.lean contains no doc (AFAICT), so I do not know where to look.

[Adam Topaz]

I think this refers to the following?

import Mathlib.Tactic

open Nat

example (n : ℕ) : 0 < factorial n := by
  induction n with
  | zero =>
    rw [factorial_zero]
    simp
  | succ n ih =>
    rw [factorial_succ]
    apply mul_pos (succ_pos n) ih

[Adam Topaz]

(similarly for cases)

[Filippo A. E. Nuccio]

Ah, I see, true. But you also agree that one could read it as induction n with m hm works (and it does not).

[Adam Topaz]

But I do agree that the documentation should be improved. For example, the one for induction mentions two examples at the bottom, but not one with the above variant.

[Filippo A. E. Nuccio]

And I'd be happy to help in doing so, but do you know how?

[Adam Topaz]

Yes, if you only read that line without the following three four bulletpoints, you could get that impression

[Adam Topaz]

I think a better wording would be approx "You can use with to provide the variables names for each constructor with one of the following variants:" or something like that.

[Filippo A. E. Nuccio]

Yes

[Adam Topaz]

Hmmm... it is a bit hard to find where the documentation is written!

[Adam Topaz]

I found the one for induction', it's in Mathlib/Tactic/Cases

[Filippo A. E. Nuccio]

Yes, that one I found as well, but not the one for induction.

[Adam Topaz]

https://github.com/leanprover/lean4/blob/4f5f39294d8ccc65e50939270a230899d1d0294c/src/Init/Tactics.lean#L818

[Filippo A. E. Nuccio]

Thanks!

[Adam Topaz]

I had to copy-paste a snippet of text from the doc that #help found, and search through the sourcecode on github in the Lean4 repo :rofl:

[Filippo A. E. Nuccio]

Smart! Did not cross my mind... :cross_mark:

[Adam Topaz]

FWIW I think the #help tactic foo command does roughly the following: it looks for all tactics in the imports that have foo somewhere in the name, and displays their documentation. By "tactic" here it's really looking at the syntax itself, which is why the documentation for induction is attached to where the syntax is defined.

[Filippo A. E. Nuccio]

I think it searches for tactics whose name starts with foo, no?

[Adam Topaz]

yes, you're probably right.

[Adam Topaz]

I guess I can try #help tactic uction :)

[Filippo A. E. Nuccio]

...and?

[Adam Topaz]

nada! you're right :)

[Adam Topaz]

no tactic declarations start with uction

[Filippo A. E. Nuccio]

eheh, which is a pity, otherwise help tactic cases would find rcases.

[Filippo A. E. Nuccio]

(it would admittedly also find briefcases, the day we create it :briefcase: )

[Mario Carneiro]

Adam Topaz said:

I had to copy-paste a snippet of text from the doc that #help found, and search through the sourcecode on github in the Lean4 repo :rofl:

You should be able to ctrl-click something in the #help output

[Filippo A. E. Nuccio]

This works for tactics in mathlib, but not for very basic ones like induction (at least for me).

[Mario Carneiro]

did you import Lean?

[Filippo A. E. Nuccio]

I was in a random file in mathlib, so I do not remember. But I guess that the answer is then

• Sure, I was in mathlib
• Surely not, I was in mathlib
  ...

[Filippo A. E. Nuccio]

I can check

[Filippo A. E. Nuccio]

(in 10 mins...)

[Adam Topaz]

@Mario Carneiro how do you do this in neovim?

[Adam Topaz]

my usual LSP go-to-definition hotkey doesn't do it.

[Mario Carneiro]

The bracketed thing after each entry produced by #help is a MessageData.expr, which means you can ctrl-click on it in vscode

[Mario Carneiro]

I don't know if this works in neovim, are you able to ctrl-click things in the goal view normally?

[Adam Topaz]

Oh, I guess not. @Julian Berman could probably help!

[Adam Topaz]

Scratch that, yes, it does work in the infoview in goals etc.

[Mario Carneiro]

well @Julian Berman can probably still help if this is due to goals being implemented in a different way

[Julian Berman]

I'm mostly offline till Monday, but it should work "the same". Is this what you're trying @Adam Topaz ? I'm hitting gd here inside the infoview:

output.mp4

Note two things:

1) it only works between the brackets (this is the same as VSCode AFAICT)
2) make sure you don't accidentally override the gd mapping in the infoview (which I show at the end there, hit :map gd to check). The reason is that this behavior is "fake" -- it doesn't really come from the language server's usual textDocument/definition, so "normal" go to definition isn't what's being used there, we've reimplemented it for this case where it's an interactive diagnostic message. Again AFAIK that's the same as in VSCode.

[Julian Berman]

It's a bit ugly looking, we should do some syntax highlighting there I guess, but I see VSCode doesn't do any either.

[Mario Carneiro]

yeah this behavior seems to be about the same as vscode

[Adam Topaz]

I see, yes it does indeed work with the cursor between the brackets! Thanks @Julian Berman !

[Adam Topaz]

I wish there was some (even slight) colour variation between what's in the bracket and the rest of the text by default, at least to have a visual cue that this is something to try.

[Mario Carneiro]

I would have preferred to just link the syntax line itself, but messageData is limited in the things that get clicky stuff

[Mario Carneiro]

especially because the names of the constants can be quite unsightly

[Jeremy Avigad]

While we are on the topic of induction and cases, I'll share a thought. I am currently teaching an undergraduate course on interactive theorem proving based on MIL (as well as material I will work into a new MIL chapter soon). The last week or so covered induction on the natural numbers, as well as structural induction on things like lists and trees.

MIL has normalized on rcases and obtain for destructing data and we have a pretty good story for using cases with structured proofs for structural induction. We also normalize on induction' for ordinary proof by induction on the natural numbers. The one thing that annoys me is having the prime in the name of the tactic that we pitching as the canonical one for many use cases. Does that annoy anyone else? How about renaming it induct so we can write induct n with n ih rather than induction' n with n ih?

[Patrick Massot]

Why don’t you want to use induction instead? Is it because the code action is not good enough?

[Filippo A. E. Nuccio]

You cannot write induction n with m hm, no?

[Filippo A. E. Nuccio]

You need a prime for it to accept the explicit naming of the new variable and new assumption.

[Ruben Van de Velde]

The alternative is induction ... with | ...

[Ruben Van de Velde]

induction' is not so bad for natural numbers, but much less fun when you have multiple cases where you need to name multiple new variables in each

[Filippo A. E. Nuccio]

This is even less documented.

[Mario Carneiro]

is it? It should be right there in the docstring

[Mario Carneiro]

...well there is a lot of stuff there and no example. There should be an example

[Filippo A. E. Nuccio]

let me check

[Adam Topaz]

It is there, but it would be better to have an example (like at the top of the thread)

[Mario Carneiro]

it would also be nice if induction n with n ih parsed and gave an error with a try this

[Mario Carneiro]

unfortunately, the position after with in induction is already taken, it's a tactic which runs before each match arm

[Filippo A. E. Nuccio]

Well, but there are two points here. One is whether it is possible or not to change the behaviour (probably hard), the other is whether we can at least document well what this behaviour is and provide good information to users.

[Jeremy Avigad]

induction is more verbose. It's usually nicer to write

induction' n with n ih
· [base case]
[induction step]

than

induction n with
| zero => [base case]
| succ n ih =>
  [induction step]

At least, that's what we favor in MIL.

[Jeremy Avigad]

(Sorry, I was responding to Patrick before I saw the other comments.)

[Jeremy Avigad]

I agree that, for many purposes, structured proofs with induction are better. But it's hard to beat induction' for induction on the natural numbers.

[Mario Carneiro]

what would be your opinion on an rcases-like syntax for induction'? It's a bit more verbose, but not multiline

rinduction 0 with _ | ⟨n, ih⟩
· [base case]
[induction step]

[Jeremy Avigad]

I thought about that. IIRC, the SSReflect case (which was similar to rcases could handle recursive eliminators and let you name the inductive hypothesis). But I don't think rinduction would be a big win. I agree with Filippo that when you are doing computer-sciency things with multiple constructors, induction is nicer. induction' is good for simple structures like the natural numbers and lists, when e.g. there is one trivial base case and one constructor. In that case, the syntax of induction' is optimal.

[Jeremy Avigad]

It's hard to beat induction' xs with x xs ih for induction on lists.

[Mario Carneiro]

I'm not sure it's optimal, even if we restrict to the simple case. For example, you could just name the variable the same as the original induction variable and call the inductive hypothesis ih always, and then there is nothing to name

[Mario Carneiro]

if we focus in on just nat / list I think optimal means no names

[Mario Carneiro]

(or optional but frequently omitted names)

[Filippo A. E. Nuccio]

Observe also that if you do not know exactly what the names of constructors are, induction'inserts it for you, but induction does not. For instance, when proving

example (n : ℕ) : 0 ≤ n := by
  induction n with
  |

you see 0 ≤ 0 but you need to write zero to enter a nice goal state; on the other hand, after

example (n : ℕ) : 0 ≤ n := by
  induction' n with m hm
  ·

you are ready to go.

[Jeremy Avigad]

I don't have strong opinions about that. But I don't mind writing induction' n with n ih; it seems to be good hygiene to name the things that are being introduced. (And I'd prefer induct n with n ih.) Having to write the underscore and the angle brackets is a much bigger imposition.

[Mario Carneiro]

if you write induction n you can see the names of the constructors

[Jeremy Avigad]

(Again, my response was to Mario.)

[Mario Carneiro]

What do other systems do?

[Filippo A. E. Nuccio]

Mario Carneiro said:

if you write induction n you can see the names of the constructors

For Nat, you see 0 but you need to type zero. If you start off with

| 0 => simp

you get problems, but what you see is a 0.
What you might do is to use the bulb to have VSCode create the pattern-matching for you, but this also is not written in the doc.

[Jeremy Avigad]

https://coq.inria.fr/doc/V8.18.0/refman/proofs/writing-proofs/reasoning-inductives.html#coq:tacn.induction

[Mario Carneiro]

(I was thinking of languages other than coq, since lean's tactics are mostly borrowed from coq to begin with)

[Jeremy Avigad]

https://isabelle.in.tum.de/Isar/Isar-induct.pdf

[Mario Carneiro]

the isar syntax looks more heavyweight and similar to lean 4 induction

[Jeremy Avigad]

It's similar to induction.

[Mario Carneiro]

Here's a HOL4 proof:

(* Theorem: x IN G /\ y IN G /\ x * y = y * x ==> (x ** n) * (y ** m) = (y ** m) * (x ** n) *)
(* Proof:
   By inducton on m.
   Base case: x ** n * y ** 0 = y ** 0 * x ** n
   LHS = x ** n * y ** 0
       = x ** n * #e         by monoid_exp_0
       = x ** n              by monoid_rid
       = #e * x ** n         by monoid_lid
       = y ** 0 * x ** n     by monoid_exp_0
       = RHS
   Step case: x ** n * y ** m = y ** m * x ** n ==> x ** n * y ** SUC m = y ** SUC m * x ** n
   LHS = x ** n * y ** SUC m
       = x ** n * (y * y ** m)    by monoid_exp_SUC
       = (x ** n * y) * y ** m    by monoid_assoc
       = (y * x ** n) * y ** m    by monoid_comm_exp (with single y)
       = y * (x ** n * y ** m)    by monoid_assoc
       = y * (y ** m * x ** n)    by induction hypothesis
       = (y * y ** m) * x ** n    by monoid_assoc
       = y ** SUC m  * x ** n     by monoid_exp_SUC
       = RHS
*)
val monoid_comm_exp_exp = store_thm(
  "monoid_comm_exp_exp",
  ``!g:'a monoid. Monoid g ==> !x y. x IN G /\ y IN G /\ (x * y = y * x) ==>
   !n m. x ** n * y ** m = y ** m * x ** n``,
  rpt strip_tac >>
  Induct_on `m` >-
  rw[] >>
  `x ** n * y ** SUC m = x ** n * (y * y ** m)` by rw[] >>
  `_ = (x ** n * y) * y ** m` by rw[monoid_assoc] >>
  `_ = (y * x ** n) * y ** m` by metis_tac[monoid_comm_exp] >>
  `_ = y * (x ** n * y ** m)` by rw[monoid_assoc] >>
  `_ = y * (y ** m * x ** n)` by metis_tac[] >>
  rw[monoid_assoc]);

[Mario Carneiro]

which I think means that the inductive hypothesis is in scope but basically unnamed, and the variable name has been reused

[Jeremy Avigad]

In the HOL family, assumptions in the context (like the ih) aren't named, right?

[Jeremy Avigad]

We're writing at the same time.

[Mario Carneiro]

usually you pick out hypotheses by giving patterns describing their type

[Mario Carneiro]

like the \f<> syntax

[Mario Carneiro]

(or you just call hammers all the time like in this example)

[Jeremy Avigad]

In Isabelle tactic proofs, it was more common just to call hammers or use tactics that take the first assumption that matches.

[Jeremy Avigad]

Anyhow, I think induction' is close to optimal. Maybe there is a way to choose sensible defaults when the with is omitted, but that seems to be a minor issue. I am more bothered by the aesthetics of having the prime in the name.

[François G. Dorais]

I don't have any interesting facts to add to this discussion other than I'm a fan of induction the way it is now and I think of induction' as legacy Lean 3 code. That said, I'm noticing I appear to be in the minority.

I especially like you can use the place afterwith to deal with trivial cases and focus on important ones. This is from Batteries.Data.Array code I played with this morning:

theorem size_shrink_loop (a : Array α) (n) : (shrink.loop n a).size = a.size - n := by
  induction n generalizing a with simp [shrink.loop, *]
  | succ => omega

This one is pretty slick (and didn't make it to the PR because of the non-terminal simp). I find this format especially clear and useful when there's a lot of cases and only one or two are nontrivial.

[Mario Carneiro]

I think Jeremy has a valid argument here that while the syntax of induction' doesn't scale well, it does handle the simple (and common!) cases better than most alternatives, and the challenge is how to have the best of both worlds

[Mario Carneiro]

In particular, we should stop thinking of induction' as legacy lean 3 code, there are reasons to use it which have nothing to do with historical usage patterns

[Jeremy Avigad]

Note that we have a similar duality with rcases and structured case syntax. Sometimes rcases is more convenient, and sometimes it is better to use a more verbose but structured proof with cases. I like the fact that Lean offers both options and they are both first-class citizens. Similarly, I like the fact that we can choose between induction' and induction. I only dislike the fact that the prime makes induction' feel like a second-class citizen.

[Mario Carneiro]

another thing I was thinking of would be to make with a tactic, which just acts like map_tacs [rename_i ..., rename_i ...]. So then you could write induction x; with | n ih which is pretty compact and also generalizes to any tactic that does both multiple subgoals and intros

[François G. Dorais]

Mario Carneiro said:

I think Jeremy has a valid argument here that while the syntax of induction' doesn't scale well, it does handle the simple (and common!) cases better than most alternatives, and the challenge is how to have the best of both worlds

In particular, we should stop thinking of induction' as legacy lean 3 code, there are reasons to use it which have nothing to do with historical usage patterns

I agree with that. I certainly did not mean to imply that everyone should think of induction' as legacy Lean 3 code! I barely use it now but I do use it occasionally, I think. I certainly have used it in the past. Maybe my brain rewired itself to use the new induction over time but I'm definitely not against occasionally using induction'.

[Mario Carneiro]

maybe a minimalistic change to induction' which is backward compatible is to allow adding | between the variables to separate the cases

[François G. Dorais]

Mario Carneiro said:

another thing I was thinking of would be to make with a tactic, which just acts like map_tacs [rename_i ..., rename_i ...]. So then you could write induction x; with | n ih which is pretty compact and also generalizes to any tactic that does both multiple subgoals and intros

This is pretty similar to induction x; next => ...; next n ih => ... (Admittedly, I never thought next was an obvious name for what it does.)

[Mario Carneiro]

the difference is that all the names come at the beginning instead of before the case

[François G. Dorais]

Mario Carneiro said:

maybe a minimalistic change to induction' which is backward compatible is to allow adding | between the variables to separate the cases

That's pretty much like Coq, right?

[Mario Carneiro]

yeah, the idea is to make it closer to rcases patterns which are also similar to ssreflect intro patterns

[Mario Carneiro]

there isn't a whole lot to work with in the syntax there because there are no delimiters at all

[François G. Dorais]

Sounds good. Like you suggested elsewhere a while ago, we ultimately would like to have some form of "Coq compatibility mode" be able to copy paste a Coq proof in Lean. That task is easier if Lean has some syntax options that are mostly compatible with Coq's syntax.

[Mario Carneiro]

Stay tuned, I'll be talking to Assia next week and we'll be thinking about this general area

[Mario Carneiro]

but I think it's more likely to go in the direction of syntax translation, which means the main concern is ensuring that equivalent semantics exist, even if the concrete syntax differs in trivial ways

[Ruben Van de Velde]

One thing we might consider: if induction' didn't exist and we were all used to the (admittedly fairly verbose) induction syntax - would we add it?

[François G. Dorais]

Mario Carneiro said:

but I think it's more likely to go in the direction of syntax translation, which means the main concern is ensuring that equivalent semantics exist, even if the concrete syntax differs in trivial ways

Indeed, let's get v1.0 working and then add copy-paste functionality in v2.0.

[Eric Wieser]

Patrick Massot said:

Is it because the code action is not good enough?

I always struggle with the code action. I think my issue is that I write induction n with, and then it's too late for the action to run?

[Eric Wieser]

But also, I don't think the action supports induction using, so then you play this stupid game where you only get an error message telling you what the missing cases are after your first correct guess

[Mario Carneiro]

an enumeration of failing examples (and expected results if it's not obvious) would help

[Kevin Buzzard]

Three worked examples in the induction tactic docstring would help.

[Floris van Doorn]

I like induction as well. It's a bit verbose, but since I don't have to type it myself, I don't mind.

[Jireh Loreaux]

Eric Wieser said:

But also, I don't think the action supports induction using, so then you play this stupid game where you only get an error message telling you what the missing cases are after your first correct guess

While it's true that the action doesn't support using, you don't have to get a correct guess first. If you put your cursor on | in the example below, you'll see in the infoview the arm named in the infoview: case ind, which tells you how to name the arms.

universe u
example {motive : Nat → Sort u} (t : Nat) (zero : motive Nat.zero)
    (succ : (n : ℕ) → motive n → motive n.succ) :
    motive t := by
  induction t using Nat.strongRecOn with
  |

[Jireh Loreaux]

@Mario Carneiro do you need failing examples of where the code action doesn't work for induction ... using ... with _?

[Jireh Loreaux]

The thing about induction that annoys me is that the hypotheses in each arm are introduced by default (and inaccessible if unnamed). This wouldn't be so bad, except I don't think there's anyway to disable the introduction.

I just learned about the @ syntax for induction arms (this is not included in the documentation, and I only found out about it by stumbling on the docstring for docs#Lean.Parser.Tactic.inductionAltLHS), which allows you to name implicit arguments, but unfortunately | @succ => sorry still introduces the inaccessible variables :sad:. See also this thread

[Mario Carneiro]

Jireh Loreaux said:

Mario Carneiro do you need failing examples of where the code action doesn't work for induction ... using ... with _?

I want examples where it doesn't work and you think it should

[Mario Carneiro]

Jireh Loreaux said:

The thing about induction that annoys me is that the hypotheses in each arm are introduced by default (and inaccessible if unnamed). This wouldn't be so bad, except I don't think there's anyway to disable the introduction.

Yeah, I don't think you should think of it as doing an introduction, it's part of the tactic operation itself (and it has to do some other stuff afterwards) so it's not really an option to not do it - you can name the variables or revert them if you don't want them intro'd. (Or just use apply with the recursor in this case)

[Jireh Loreaux]

@Mario Carneiro here is an example of the code action working (without using) and failing (with using). I have never seen the code action available for using; I thought it just wasn't implemented.

example {motive : Nat → Sort _} (t : Nat) : motive t := by
  induction t with _ -- cursor on `_` gives an :idea: bubble, which generates:
  -- | zero => sorry
  -- | succ n ih => sorry

example {motive : Nat → Sort _} (t : Nat) : motive t := by
  induction t using Nat.strongRecOn with _ -- no :idea: bubble

[Floris van Doorn]

(@Jireh Loreaux: not directly related, but note that induction t already gives a code action, no need to type with _)

[Floris van Doorn]

But I indeed also have no code action for (variations of) the second example.

[Mario Carneiro]

I wasn't saying it is implemented, I was requesting scenarios where the code action does not work, including also incomplete inputs that the code action did not anticipate

[Mario Carneiro]

another case I'm aware of is match e with | ... or induction e with | ... where the arms are present but not exhaustive (e.g. there is a missing variant)

[Patrick Massot]

@Mario Carneiro Is there any news about having a code action for induction … using …?

[Mario Carneiro]

batteries#1030

[Patrick Massot]

Great, thank you so much!

[Julian Berman]

How much pushing of luck is it to ask the same question about the match arm generation code action (which it looks like was last discussed here: https://leanprover.zulipchat.com/#narrow/channel/455414-Infinity-Cosmos/topic/the.20coherent.20isomorphism/near/471050444 )?