recommend intro to induction in vanilla lean4

Stream: maths

[rzeta0]

I've started the MoP's chapter on induction - but that course uses MoP specific tactics for simple induction.

Looking through the comments in this site and also stackexchange suggests the Natural Number Game also has specific tactics for induction.

I can't seem find a short guide online about simple induction with vanilla Lean 4?

This link which top several search engines seems to be about "inductive types", probably an advanced topic about types and not about the proof method.

Question: Can you recommend a short intro / guide to simple induction in vanilla lean4?

---

What I like about the MoP simple_induction is that it creates two new sub-goals and an inductive hypothesis, one for the base case and one for the inductive case. This seems like the right conceptual thing to do for many simple proofs.

The following is an example from MoP:

example (n : ℕ) : 2 ^ n ≥ n + 1 := by
  simple_induction n with k IH
  · -- base case
    numbers
  · -- inductive step
    calc 2 ^ (k + 1) = 2 * 2 ^ k := by ring
      _ ≥ 2 * (k + 1) := by rel [IH]
      _ = (k + 1 + 1) + k := by ring
      _ ≥ k + 1 + 1 := by extra

[Adam Topaz]

There is also mathematics in lean. See section 5.2 here: https://leanprover-community.github.io/mathematics_in_lean/C05_Elementary_Number_Theory.html

This mentions induction' which is not vanilla lean4, but vanilla mathlib. If you want pure vanilla lean4 then the theorem proving in lean link you already mentioned is the best reference I know of

[rzeta0]

Thanks - yes I did mean mathlib too.

That site uses induction' with an apostrophe. Does that mean it is using older "lean3" syntax? Is there a newer syntax in lean4?

[Kevin Buzzard]

Here's the same proof but without Heather's MIL-only tactics numbers and extra, and with Lean 4's induction syntax:

import Mathlib

example (n : ℕ) : 2 ^ n ≥ n + 1 := by
  induction n with
  | zero => norm_num
  | succ k IH => calc
      2 ^ (k + 1) = 2 * 2 ^ k := by ring
      _ ≥ 2 * (k + 1) := by rel [IH]
      _ = (k + 1 + 1) + k := by ring
      _ ≥ k + 1 + 1 := by linarith

[Adam Topaz]

The new lean4 syntax should be mentioned in theorem proving in lean. Do you know about #help tactic induction?

[rzeta0]

I was hoping to avoid learning this new vertical bar syntax but I guess I can't avoid it.

For clarity, are the apostrophe versions of tactics and lemmas an indication their use is discouraged, that they are on the path to being deprecated?

[rzeta0]

I don't know about #help but I'll check it out.

[Soundwave]

Lean docs make a strong implication that induction is so bare bones because term mode works well enough. Some examples if you run into issues with induction in a proof.

import Mathlib

-- At top level
example (n : ℕ) : 2 ^ n ≥ n + 1 := elim n
  where
  elim n : 2 ^ n ≥ n + 1 := by
    cases n with
    | zero => norm_num
    | succ k => calc
      2 ^ (k + 1) = 2 * 2 ^ k := by ring
      _ ≥ 2 * (k + 1) := by rel [elim k]
      _ = (k + 1 + 1) + k := by ring
      _ ≥ k + 1 + 1 := by linarith

-- In a proof
example (n : ℕ) : 2 ^ n ≥ n + 1 := by
  let rec elim n : 2 ^ n ≥ n + 1 := by
    cases n with
    | zero => norm_num
    | succ k => calc
      2 ^ (k + 1) = 2 * 2 ^ k := by ring
      _ ≥ 2 * (k + 1) := by rel [elim k]
      _ = (k + 1 + 1) + k := by ring
      _ ≥ k + 1 + 1 := by linarith

  exact elim n

-- We need to go deeper
example (n : ℕ) : 2 ^ n ≥ n + 1 :=
  let rec elim n : 2 ^ n ≥ n + 1 := by
    -- Lots of other match features: motives, match hypotheses... Check docs.
    match n with
    | .zero => norm_num
    | .succ k => calc
      2 ^ (k + 1) = 2 * 2 ^ k := by ring
      _ ≥ 2 * (k + 1) := by rel [elim k]
      _ = (k + 1 + 1) + k := by ring
      _ ≥ k + 1 + 1 := by linarith

  elim n

[Dan Velleman]

Induction in Lean is one of my pet peeves. In a course like Heather's, it seems to me induction should be taught as a method of proving a goal of the form ∀ (n : ℕ), P n. That's how it is explained in every "transition to proof" textbook, and it's what any mathematician who doesn't use Lean would say induction is for. But in Lean, induction is set up to prove a goal of the form P n, and if your goal is ∀ (n : ℕ), P n, then you have to do intro n before using the induction tactic.

In How To Prove It With Lean I defined my own induction tactic that expects the goal to have the form ∀ (n : ℕ), P n. An alternative in standard Lean is to use apply Nat.recAux:

example : ∀ (n : ℕ), 2 ^ n ≥ n + 1 := by
  apply Nat.recAux
  · -- base case.  Goal: 2 ^ 0 ≥ 0 + 1
    norm_num
  · -- inductive step.  Goal:  ∀ (n : Nat), 2 ^ n ≥ n + 1 → 2 ^ (n + 1) ≥ n + 1 + 1
    intro n ih
    calc 2 ^ (n + 1)
      _ = 2 * 2 ^ n := by ring
      _ ≥ 2 * (n + 1) := by rel [ih]
      _ ≥ n + 1 + 1 := by linarith
  done

This also works if the goal has the form P n, but surprisingly Lean needs help figuring out the motive in this example:

example (n : ℕ) : 2 ^ n ≥ n + 1 := by
  apply Nat.recAux (motive := fun n => 2 ^ n ≥ n + 1)
  · -- base case.  Goal: 2 ^ 0 ≥ 0 + 1
    norm_num
  · -- inductive step.  Goal:  ∀ (n : ℕ), 2 ^ n ≥ n + 1 → 2 ^ (n + 1) ≥ n + 1 + 1
    intro n ih
    calc 2 ^ (n + 1)
      _ = 2 * 2 ^ n := by ring
      _ ≥ 2 * (n + 1) := by rel [ih]
      _ ≥ n + 1 + 1 := by linarith
  done

[Edward van de Meent]

i suppose that maybe the current tactic should be called induction_on :sweat_smile:

[rzeta0]

Some of the people on this thread are clearly very experienced in both mathematics and lean the language.

Perhaps some of them might create a language enhancement request?

( the core developers won't give a suggestion from me any credence )

[Soundwave]

imo the current features serve well enough for the core.

The only part that really irks me is that the features of the lean3 syntax are just completely gone: you can't name hypotheses without using a structured proof. This seems like an oversight (but maybe this was intentional? I'm not aware of the history)

[Soundwave]

scratch that, I guess the canonical unstructured technique is induction and then rename_i...

I don't love it, but it works.

[Jireh Loreaux]

it's definitely intentional to encourage using structured proofs by not providing the unstructured variants.

[Soundwave]

That's very fair, I just figured it would have been a rather controversial choice: unstructured style is popular.

I mean, I guess that's why the primed mathlib tactics still see use.

[Jireh Loreaux]

The primed tactics only exist because they were semi-necessary for porting, and we haven't yet managed to purge them.

[Soundwave]

Yeah I peeked through some recent commits and didn't see them, I figured they were considered deprecated for mathlib purposes. I've seen them a lot in notes and individual developments though, perhaps out of habit; I didn't work on any larger developments in coq but my impression there was that there was the opposite inclination, to avoid term mode or similar structures.

I've come around to the structured style: deciphering the proof structure in an unstructured proof is a bit of an art.