How to get the name of the inductive hypothesis

Stream: general

[Bolton Bailey]

After mathport, my lemma looks like this, and shows an error.

theorem MvPolynomial.mul_x_pow_eq_zero {σ R : Type _} [CommSemiring R] {s : σ} (d : ℕ)
    (p : MvPolynomial σ R) (h : MvPolynomial.X s ^ d * p = 0) : p = 0 :=
  by
  induction d
  · simp at h
    exact h
  · apply d_ih -- unknown identifier 'd_ih'
    rw [pow_succ] at h
    apply MvPolynomial.mul_x_eq_zero s
    rw [← mul_assoc]
    exact h

When I mouse over induction I get a docstring saying "You can use with to provide the variables names for each constructor." But how do I do this?

theorem MvPolynomial.mul_x_pow_eq_zero {σ R : Type _} [CommSemiring R] {s : σ} (d : ℕ)
    (p : MvPolynomial σ R) (h : MvPolynomial.X s ^ d * p = 0) : p = 0 :=
  by
  induction d with d d_ih -- unknown tactic
  · simp at h
    exact h
  · apply d_ih
    rw [pow_succ] at h
    apply MvPolynomial.mul_x_eq_zero s
    rw [← mul_assoc]
    exact h

[Bolton Bailey]

Seems like the right way is

theorem MvPolynomial.mul_x_pow_eq_zero {σ R : Type _} [CommSemiring R] {s : σ} (d : ℕ)
    (p : MvPolynomial σ R) (h : MvPolynomial.X s ^ d * p = 0) : p = 0 :=
  by
  induction d with
  | zero =>
    simp at h
    exact h
  | succ x' d_ih =>
    apply d_ih
    rw [pow_succ] at h
    apply MvPolynomial.mul_x_eq_zero s
    rw [← mul_assoc]
    exact h

[Bolton Bailey]

I was very confused by the docstring, in the last bullet point it seems like it's saying I can only use one tactic to close my goal for each case.

[Bolton Bailey]

I'm not actually sure where that docstring lives, I can't find it in either of the lean4 or mathlib4 repos.

[Damiano Testa]

This is not exactly an answer to your question, but, if you leave the cursor at the end of the "inducted" variable, you should get a code-action.
image.png

If you click on the lightbulb and then on Generate... you will get a template that you can fill in. This is what the template looks like:

example (d : Nat) : d = 0 := by
  induction d with
  | zero => sorry
  | succ n ih => sorry

[Bolton Bailey]

I almost never use this feature, so it is not very helpful to me.

I want to point out that cases also has the same problem. I would really like to make a PR to whatever thing provides the text for these tooltips but I can't find it.

[Bolton Bailey]

Also now that I try it, this lightbulb is destroying the line of code after where it inserts the example.

[Henrik Böving]

Damiano Testa said:

This is not exactly an answer to your question, but, if you leave the cursor at the end of the "inducted" variable, you should get a code-action.
image.png

If you click on the lightbulb and then on Generate... you will get a template that you can fill in. This is what the template looks like:

example (d : Nat) : d = 0 := by
  induction d with
  | zero => sorry
  | succ n ih => sorry

Are these code actions defined by std, mathlib or built-in?

[Patrick Massot]

std

[Henrik Böving]

Do we have plans to upstream this eventually?

[Patrick Massot]

You'll need to ask Mario.

[Henrik Böving]

@Mario Carneiro bonk

[Patrick Massot]

More specific answer to "where is it?" is here

[Mario Carneiro]

what's the question?

[Patrick Massot]

Henrik Böving said:

Do we have plans to upstream this eventually?

[Mario Carneiro]

to core? no

[Mario Carneiro]

this seems like an example of something that is suitable for std long-term: it's not necessary for the compiler but is a clear value add on the language

[Mario Carneiro]

I mean, it would be nice to have it in core development but only insofar as anything in std is a nice to have. I would rather solve that by putting std in the bootstrap and that's a far future thing

[Bolton Bailey]

When I use the tooltip doing induction on a list, I get

  induction l generalizing n with
  | α => sorry
  | nil => sorry
  | cons head tail ih => sorry

What is this | α => sorry part? Evidently I don't need it, because I can delete it and prove the other ones normally.

[Eric Wieser]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Nonsense.20autocomplete.20of.20.60cases.20with.60/near/391116492

[Kevin Buzzard]

Is there an open issue for this? Where does it go, if not?

[Bolton Bailey]

Well according to Patrick's comment, this lives in std4.

[Bolton Bailey]

I'm not sure if this is separate from or related to the tooltip eating my code. Maybe there need to be two issues?

[Kevin Buzzard]

std4#270 , hopefully this is useful and in the right place.

[Patrick Massot]

You wrote "tooltip" where you meant "code action".

[Kevin Buzzard]

oh jeez I just copied from someone else. What do these mean, and which is which?

[Kevin Buzzard]

Hopefully I fixed it. So a code action is a lightbulb and a tooltip is...not sure.

[Patrick Massot]

Tooltip is whatever you see when you let your mouse pointer over something and a little piece of information shows up.