Simple proof to show Lean tactics ((n+1)! - n! = n(n!))

Stream: new members

[Isak Colboubrani]

I am attempting to construct a simple proof to illustrate for absolute beginners (fellow undergraduates) that one can choose between using Lean tactics and performing manual step-by-step rewriting.

import Mathlib

-- Prove the identity: (n+1)! - n! = n(n!)
-- More verbose method
example (n : ℕ) : Nat.factorial (n + 1) - Nat.factorial n = n * (Nat.factorial n) := by
  rw [Nat.factorial_succ]
  rw [add_mul]
  rw [one_mul]
  rw [add_tsub_cancel_right]

-- Prove the identity: (n+1)! - n! = n(n!)
-- Less verbose method
example (n : ℕ) : Nat.factorial (n + 1) - Nat.factorial n = n * (Nat.factorial n) := by
  rw [Nat.factorial_succ]
  ring_nf
  simp

Are the examples idiomatic? How can they be improved? Can the less verbose version be shortened further?

[Kevin Buzzard]

open scoped Nat gives you notation:

example (n : ℕ) : (n + 1)! - n ! = n * n ! := by

Factorial notation is a bit hairy though, because n! doesn't work.

I would not have chosen this example for beginners though because it involves natural subtraction, which is why tactics are struggling.

[Kevin Buzzard]

Here's a toy example for beginners:

import Mathlib

open Finset

example (n : ℕ) : ∑ i in range n, (2 * i + 1) = n^2 := by
  induction n with
  | zero =>
    simp
  | succ n IH =>
    rw [sum_range_succ, IH]
    ring

If you remove the natural subtraction from your original question by moving the n! onto the other side, it becomes easier:

import Mathlib

open Nat

example (n : ℕ) : (n + 1)! = n ! + n * n ! := by
  rw [factorial_succ]
  ring

[Isak Colboubrani]

That is a great example for beginners. Thanks!

Yes, the ! notation is a bit hard to explain to beginners.

I might convince someone that n! is written as n !, but after doing so I have the problem of describing why (n + 1)! cannot be written as (n + 1) ! (in all contexts).

What is the best way to explain that in a way that makes sense for a mathematics undergraduate?

We have | and \mid: could something similar be introduced to separate ! and say \fact?

[Mario Carneiro]

Isak Colboubrani said:

I might convince someone that n! is written as n !, but after doing so I have the problem of describing why (n + 1)! cannot be written as (n + 1) !.

Is that so? These should both work

[Ruben Van de Velde]

Yeah, either is possible if there's a parenthesis, but not if it's just an identifier

[Isak Colboubrani]

In this context:

import Mathlib

open scoped Nat

-- Works.
example (n : ℕ) : (n + 1)! - (n !) = n * (n !) := by
  rw [Nat.factorial_succ]
  ring_nf
  simp

-- Does not work.
example (n : ℕ) : (n + 1) ! - (n !) = n * (n !) := by
  rw [Nat.factorial_succ]
  ring_nf
  simp

-- Works.
example (n : ℕ) : ((n + 1) !) - (n !) = n * (n !) := by
  rw [Nat.factorial_succ]
  ring_nf
  simp

[Ruben Van de Velde]

Wait what-

example (n : ℕ) : ((n + 1) !) - (n !) = n * (n !) := by

also works. Is the ! interfering with the -? Or is it reading - (n !) as (- (n !))?

[Mario Carneiro]

this is because of the funky parsing of prefix ! (boolean not)

[Mario Carneiro]

I think that should be fixed

[Mario Carneiro]

(n + 1) ! - (n !) gets parsed as (n + 1) (! (- (n !)))

[Mario Carneiro]

By the way, if you want to make this look more regular, be aware that an alternative to n ! is (n)!

[Mario Carneiro]

I would really like to implement a parser for n! which does the right thing, but this will require changes to lean core, so maybe I can interest @Kyle Miller ? The idea is to make it so that in an expression like foo! or (e).foo!, if foo! does not resolve as an identifier (there is no declaration with this name, in the namespace of e's type in the latter case), and there is a syntax term "!" : term syntax rule, then split the identifier as "foo" + "!" and try again. Ditto for ? suffixes.

[Yaël Dillies]

That sounds like a great solution from the usability POV, I must say!

[Mario Carneiro]

(lean already has to do something similar for foo.bar which can be either a namespaced name or (foo).bar)

[Kyle Miller]

You mean a parser like this @Mario Carneiro?

[Kyle Miller]

In another direction, lean4#5824 and lean4#5826 were experiments in modifying the ! bool negation notation. I think both of these would fix the "does not work" example in #new members > Simple proof to show Lean tactics ((n+1)! - n! = n(n!)) @ 💬

[Mario Carneiro]

yes exactly. I have reasons to believe that that elaborator is insufficient because identifiers can be used in more ways than just in elabIdent, plus it's probably a performance issue to implement in that way

[Isak Colboubrani]

Are lean4#5824 and lean4#5826 the right places to follow the progress on this suggested change?

[Kyle Miller]

Yes @Isak Colboubrani, for now this Zulip thread and those two PRs are the current state of looking into the issue.