Noob Question about `induction` Tactic

Stream: new members

[Husnain Raza]

Hello - after doing some of the Natural Number Game, I thought that I would install Lean locally and try to work through some of the exercises locally. However the following proof gives me an error for using an unknown tactic - what am I doing wrong here? Any advice would be appreciated :smile:

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic

def even (n: ℕ) : Prop := (∃ k : ℕ, 2 * k = n)
def odd (n: ℕ) : Prop := ¬(∃ k: ℕ, 2 * k = n)

example : (odd 3) := by
  rw [odd]
  refine not_exists.mpr ?_
  intro x
  induction x with h ih
  sorry

[Kyle Miller]

It's induction' instead of induction if you want that with clause. (NNG uses its own versions of tactics)

[Husnain Raza]

Thanks! Been trying to migrate from lean3 to lean4 so having to relearn things is fun haha

[Kyle Miller]

If you do induction x by itself, then in VS Code the code action lightbulb pops up

image.png

Clicking it, you can select "generate an explicit pattern match for 'induction'" and then it creates a skeleton for a structured proof.

image.png

Each sub-proof can then be indented:

example : (odd 3) := by
  rw [odd]
  refine not_exists.mpr ?_
  intro x
  induction x with
  | zero =>
    sorry
  | succ n ih =>
    sorry

[Kyle Miller]

For induction, the with clause is for all the pattern matches, which is why you were getting an error in your original version. The induction' tactic is the "Lean 3 compatibility mode" tactic.

[Husnain Raza]

  induction x with
  | zero => sorry
  | succ n ih => sorry

Would this be the correct syntax for Lean4 then?

[Kevin Buzzard]

Yeah that's right. But I don't think that the Lean 4 game engine supports fancy syntax like that (at least in the default mode where the user types in one line per tactic) so we just decided to hack the induction tactic so that it worked in the same way as lean 3. Other hacks: NNG4 cases is Lean 4 cases', NNG4 rw is weaker than Lean 4 rw because Lean 4 rw tries rfl after the rewrite, so closes goals unexpectedly.