proof by induction

Stream: new members

[JK]

I am getting stuck in the following proof and not sure why:

import Mathlib

def fact : ℕ → ℕ
  | 0 => 1
  | n + 1 => (n+1) * fact n

example (n:ℕ) : 1 ≤ fact n := by
  induction n
  rw [fact]
  rw [fact]
  calc
    1 ≤ fact n := a

(my proof state before invoking calc has a✝ : 1 ≤ fact n✝ in it; I am not sure why the hypothesis was not called ih.) What am I doing wrong here?

[Riccardo Brasca]

Because you didn't tell Lean the name. Do you see the yellow bulb putting the cursor on a new line after induction n?

[Riccardo Brasca]

If you click on it you have something like "generate skeleton for induction", and Lean should automatically structure your proof

[JK]

I don't see any warning/error after the induction n line

[Aaron Liu]

put your cursor on the induction

[Aaron Liu]

and if you're in VSCode then there should be a yellow lightbulb appearing

[Aaron Liu]

apparently you can also use the keyboard shortcut Ctrl+.

[JK]

When I do that I get some text that includes "For example, given n : Nat and a goal with a hypothesis h : P n and target Q n, induction n produces one goal with hypothesis h : P 0 and target Q 0, and one goal with hypotheses h : P (Nat.succ a) and ih₁ : P a → Q a and target Q (Nat.succ a). Here the names a and ih₁ are chosen automatically and are not accessible."

This makes me think that induction n should work(?)

Anyway, I don't care whether the inductive hypothesis is called ih or a if I can proceed with the proof.

[JK]

ah, eventually a yellow bulb did pop up

[Riccardo Brasca]

If you don't specify the name the variable is inaccessible, meaning that you cannot refert to it

[Riccardo Brasca]

Anyway you can of course write everything by hand, the yellow bulb just helps you

[Aaron Liu]

JK said:

This makes me think that induction n should work(?)

it works but you get inaccessible variables which are the same as all the other variables but you can't refer to them by name

[JK]

I now have

example (n:ℕ) : 1 ≤ fact n := by
  induction n with
  | zero => rw [fact]
  | succ n _ =>
    rw [fact]

and my induction hypothesis is still called a

[Aaron Liu]

Now it's called ih

example (n:ℕ) : 1 ≤ fact n := by
  induction n with
  | zero => rw [fact]
  | succ n ih =>
    rw [fact]

[JK]

OK, thanks, the following works:

import Mathlib

def fact : ℕ → ℕ
  | 0 => 1
  | n + 1 => (n+1) * fact n

example (n:ℕ) : 1 ≤ fact n := by
  induction n with
  | zero => rw [fact]
  | succ n ih =>
    rw [fact]
    calc
      1 ≤ (n+1) * 1 := by norm_num
      _ ≤ (n+1) * fact n := by rel [ih]