induction vs induction' with vanilla lean4+mathlib

Stream: new members

[rzeta0]

I've learned about simple induction in the MoP course. I really like how its custom simple_induction tactic creates two new goals and an inductive hypothesis.

But I want to learn to do this in vanilla lean. As has been discussed several times, (1) there seem to be no existing beginner-friendly guides, and (2) the use of an apostrophe for induction' suggests we should be using induction which has different syntax.

So I started playing around:

import Mathlib.Tactic

example {n : ℕ }: 0 * n = 0 := by
  induction' n with k hk
  · -- base case 0 * 0 = 0
    norm_num
  · -- inductive step 0 * (k + 1) = 0
    norm_num

This seems to do what beginner-brained people like me think should happen:

• creates two new goals, the base case and the inductive step
• creates an inductive hypotheses hk : 0 * k = 0 as expected

Question: what does this proof look like using the official induction tactic? I'd welcome a code snippet and an explanation if possible so I can relate it back to the above conceptual model.

My apologies, I'm not familiar with the vertical bar | notation and the right arrows => I've seen in some online resources.

[Julian Berman]

(You say "vanilla lean" but then you're importing Mathlib, so I assume you must not really mean vanilla lean? The answer below continues to assume you're OK using Mathlib).

Type:

import Mathlib.Tactic

example {n : ℕ}: 0 * n = 0 := by
  induction n

and then invoke your editor's code action functionality. In VSCode this is a yellow light bulb that will show up at the bottom line of your proof, and will say "Generate an explicit pattern match for 'induction'". Click that, and you get:

import Mathlib.Tactic

example {n : ℕ}: 0 * n = 0 := by
  induction n with
  | zero => sorry
  | succ n _ => sorry

which is saying for the induction principle you're using (the basic default one for natural numbers) the base case is called "zero" and the inductive step is called "succ" (the names happen to come from the names of the two corresponding constructors of Nat, but if you don't yet know what that is, it's irrelevant, it's just the two steps you are learning).

Now you can fill in the sorries, changing them to norm_num will give you the exact same proof you have there.

[rzeta0]

Thanks I'll have a play with that.

(and yes, the distinction between Mathlib and lean is as clear to me as the difference between lemmas and theorems in mathlib!)

[Julian Berman]

Mathlib is simply a (big, important) library developed by a large group of other people separate -- but with small overlap -- from the ones developing Lean the language, which is what I think "vanilla lean" or "core Lean" normally would connote. It's the same as most any programming language, there's a standard library and then there's other external libraries, and you either mean to use just what's part of the language itself or else you mean to use some of the third party libraries, here Mathlib.

[rzeta0]

I've had a play and am wondering how to use use new syntax if the sub-proofs require more than one line?

example {n : ℕ}: 0 * n = 0 := by
  induction n with
  | zero =>
    -- have
    -- by calc?
  | succ n _ =>
    -- have
    -- by calc?

I can't seem to add a := or a by calc in those commented sections.

Also, what do | and => actually mean?

[Julian Berman]

Maybe you're getting the indentation wrong? Doing so definitely can produce strange error messages.

import Mathlib.Tactic
example {n : ℕ}: 0 * n = 0 := by
  induction n with
  | zero =>
    have : 37 = 37 := rfl
    norm_num
  | succ n _ =>
    have : 73 = 73 := rfl
    norm_num

[Michael Stoll]

(Note that when you want to use the inductive hypothesis in the second branch, you should give it a name by writing | succ n ih => (say) instead of | succ n _ =>.)

[Julian Berman]

Also, what do | and => actually mean?

They're just pieces of syntax of the induction tactic (though of course some other Lean concepts use similar syntax, like the one for defining an inductive type, or a def using the equation compiler, say, neither of which you have likely seen yet). You could perhaps read them as | means "I'm starting to talk about a new constructor in what I'm matching or inducting on" and => is "here's the body of my proof for this constructor", just like := in a theorem, or with a bit of nuance, to \mapsto in a function.

[rzeta0]

Michael Stoll said:

(Note that when you want to use the inductive hypothesis in the second branch, you should give it a name by writing | succ n ih => (say) instead of | succ n _ =>.)

I was just about to ask how to access an inductive hypothesis and you explained it!

[Henrik Böving]

rzeta0 said:

(and yes, the distinction between Mathlib and lean is as clear to me as the difference between lemmas and theorems in mathlib!)

What do you mean by that?