Mechanics of Proof -- Trouble rewriting factorial sometimes?

Stream: maths

[Jonatas Miguel]

Ahoy all!

So, a few exercises and examples in chapter 6, that required providing Lean proofs for, required rewriting recurrence relations and for the most part it worked but, there were a few cases when trying to deal with factorial that it just refused to work for me in a calc block, and I'm not sure what I'm doing wrong. I was hoping someone could provide some insight here?

Here's what example 6.2.6 ended up looking like for me:

example (n : ℕ) : (n + 1)! ≥ 2 ^ n := by
  simple_induction n with k IH
  · rw [factorial, factorial]
    numbers
    -- NOTE: the below should be equivalent but is not working for some reason...
    -- calc
    --   (0 + 1)! = (0 + 1) * 0! := by rw [factorial]
    --   _ = (0 + 1) * 1 := by rw [factorial]
    --   _ ≥ 2^0 := by numbers
  · calc
      (k + 1 + 1)! = (k + 1 + 1) * (k + 1)! := by rw [factorial]
      _ ≥ (k + 1 + 1) * 2^k := by rel [IH]
      _ = 2^(k + 1) + k*2^k := by ring
      _ ≥ 2^(k + 1) := by extra

Similarly, for exercise 6.2.7.7 , my solution ended up resolving the base case without using a calc block:

example {n : ℕ} (hn : 2 ≤ n) : Nat.Even (n !) := by
  induction_from_starting_point n, hn with k hk IH
  · use 1
    rw [factorial]
    rw [factorial]
    rw [factorial]
  · obtain ⟨x, hx⟩ := IH
    use (k + 1) * x
    calc
      (k + 1) ! = (k + 1) * k ! := by rw [factorial]
      _ = (k + 1) * (2 * x) := by rw [hx]
      _ = 2*((k + 1) * x) := by ring

Would anyone know what I'm doing wrong?

cc: @Heather Macbeth

[Kevin Buzzard]

What's the error?

[Jonatas Miguel]

Here's a screenshot of the squiggly and it's hovered suggestion for example 6.2.6

Screenshot-2024-08-12-at-6.58.41AM.png

[Jonatas Miguel]

For reference, here's what works for example 6.2.6:

rw [factorial] -- takes `(0 + 1)! \ge 2^0` to `(0 + 1) * 0! \ge 2^0`
rw [factorial] -- takes `(0 + 1) * 0! \ge 2^0` to `(0 + 1) * 1 \ge 2^0`
numbers -- takes `(0 + 1) * 1 \ge 2^0` to goal

rw [factorial, factorial] -- takes `(0 + 1)! \ge 2^0` to `(0 + 1) * 1 \ge 2^0`
numbers -- takes `(0 + 1) * 1 \ge 2^0` to goal

calc
  (0 + 1)! = (0 + 1) * 1 := by rw [factorial, factorial]
  _ ≥ 2^0 := by numbers

It's just odd that the original formulation that tried to reach the goal more slowly didn't work, and it's not really clear to me why...

[Jonatas Miguel]

I'm starting to wonder if it has something to do with the specific version of Lean v4 that I'm using. The version specified for the codebase seems to be v4.3.0, not sure if this is relevant or not though.

[Kim Morrison]

Sorry, it's very hard to diagnose errors in code when we can't run it ourselves. (See your other thread!)

[Jonatas Miguel]

No worries, I understand. I figured I'd ask just in case other people have run into some of the same issues I've run into. Lemme know if there's anything else I can provide/do to help the process.

[Mario Carneiro]

Jonatas Miguel said:

No worries, I understand. I figured I'd ask just in case other people have run into some of the same issues I've run into. Lemme know if there's anything else I can provide/do to help the process.

#mwe <- this is a link, which gives our standard suggestion for how to make questions that people can answer

[Timo Carlin-Burns]

Here is a #mwe after translating the example to mathlib using the advice in the Transitioning to mainstream Lean appendix

import Mathlib

example (n : ℕ) : (n + 1).factorial ≥ 2 ^ n := by
  induction' n with k IH
  · -- Why does this version error when the commented version works?
    calc Nat.factorial (0 + 1)
      _ = (0 + 1) * (0).factorial := by rw [Nat.factorial] -- Error
      _ = (0 + 1) * 1 := by rw [Nat.factorial]
      _ ≥ 2^0 := by norm_num

    -- (No error)
    -- rw [Nat.factorial, Nat.factorial]
    -- norm_num
  · calc
      (k + 1 + 1).factorial = (k + 1 + 1) * (k + 1).factorial := by rw [Nat.factorial]
      _ ≥ (k + 1 + 1) * 2^k := by rel [IH]
      _ = 2^(k + 1) + k*2^k := by ring
      _ ≥ 2^(k + 1) := le_add_of_nonneg_right (by positivity)

[Timo Carlin-Burns]

Or even more minimal

import Mathlib

-- Why does this version work when the calc-ified version errors?
example : (0 + 1).factorial = (0 + 1) * 1 := by
  rw [Nat.factorial, Nat.factorial]

example : (0 + 1).factorial = (0 + 1) * 1 := by
  calc Nat.factorial (0 + 1)
    _ = (0 + 1) * (0).factorial := by rw [Nat.factorial] -- Error
    _ = (0 + 1) * 1 := by rw [Nat.factorial]

[Timo Carlin-Burns]

The problem is that in the calc version, when you rewrite using Nat.factorial, the goal is (0 + 1).factorial = (0 + 1) * (0).factorial and rw is choosing to unfold (0).factorial = 1 instead of (0 + 1).factorial = .... You can work around this by creating separate theorems for the two equations and specifying which one rw should be using

theorem factorial_zero : (0).factorial = 1 := by
  rw [Nat.factorial]

theorem factorial_succ (n : ℕ) : (n + 1).factorial = (n + 1) * n.factorial := by
  rw [Nat.factorial]

example : (0 + 1).factorial * (0).factorial = (0 + 1) * (0).factorial * (0).factorial := by
  rw [Nat.factorial_succ, Nat.factorial_zero]

example : (0 + 1).factorial = (0 + 1) * 1 := by
  calc Nat.factorial (0 + 1)
    _ = (0 + 1) * (0).factorial := by rw [Nat.factorial_succ]
    _ = (0 + 1) * 1 := by rw [Nat.factorial_zero]

[Timo Carlin-Burns]

Arguably this is a bug/undesirable behavior in rw. I'll make a new thread for that

[Ruben Van de Velde]

I think someone mentioned a similar issue recently

[Timo Carlin-Burns]

Made a thread for the bug. Forgive me if it's a duplicate. https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/nth_rw.20and.20equation.20lemmas/near/462212475

[Jonatas Miguel]

I feel like my original concern is resolved at this point. The other thread that @Timo Carlin-Burns created can be used to discuss this issue amongst people working on Lean itself I think.

Thanks everyone!