Basic facts about factorials in Mathlib

Stream: new members

[Isak Colboubrani]

While demonstrating some elementary undergraduate mathematics in Lean to a couple of fellow students, I noticed that I couldn’t construct the concise “one-liner proofs” I had naively expected to achieve using tactics or pre-existing theorems for these three basic results about factorials:

example (n : ℕ) : 1 ≤ (n)! := by sorry
example (n : ℕ) : (n)! ≤ (n + 1)! := by sorry
example (n : ℕ) (h : 0 < n) : (n)! < (n + 1)! := by sorry

I have three main questions:

1.) Was my search inadequate—that is, did I overlook any tactics or known results that would have allowed me to write the type concise “one-liner proof" described above?

2.) What would be the expected names for these theorems if they were in Mathlib?

3.) We explored a few alternative solutions (shown below). What improvements could be made to make these proofs more idiomatic, and/or more in line with Mathlib coding standards?

import Mathlib

open Nat

theorem factorial_le_factorial_succ_a {n : ℕ} : (n)! ≤ (n + 1)! := by
  gcongr
  exact Nat.le_add_right n 1
theorem factorial_le_factorial_succ_b {n : ℕ} : (n)! ≤ (n + 1)! := by
  apply factorial_le
  exact Nat.le_add_right n 1

theorem factorial_lt_factorial_succ_a {n : ℕ} (h : 0 < n) : (n)! < (n + 1)! := by
  gcongr
  exact lt_add_one n
theorem factorial_lt_factorial_succ_b {n : ℕ} (h : 0 < n) : (n)! < (n + 1)! := by
  rw [factorial_succ, succ_mul, Nat.lt_add_left_iff_pos]
  exact Nat.mul_pos h n.factorial_pos

theorem one_le_factorial_a {n : ℕ} : 1 ≤ (n)! := by
  have : n ! ≠ 0 := factorial_ne_zero n
  omega
theorem one_le_factorial_b {n : ℕ} : 1 ≤ (n)! := by
  induction n with
  | zero => rfl
  | succ n h => exact Nat.le_trans h factorial_le_factorial_succ_a

[Aaron Liu]

import Mathlib

open Nat

example (n : ℕ) : 1 ≤ (n)! := monotone_factorial n.zero_le
example (n : ℕ) : (n)! ≤ (n + 1)! := monotone_factorial n.lt_add_one.le
example (n : ℕ) (h : 0 < n) : (n)! < (n + 1)! := factorial_lt_of_lt h n.lt_add_one

[Eric Wieser]

Your gcongr proofs look like the right ones to me; I think show_term will produce pretty much the same proofs that Aaron wrote

[Matt Diamond]

@Isak Colboubrani do you use the Mathlib docs search to find lemmas? I tried typing "factorial lt" into the search box and Nat.factorial_lt_of_lt was the second result in the dropdown

[Matt Diamond]

Loogle and exact? can be helpful but I often find what I need just by typing the relevant terms into the search box

[Eric Wieser]

In this case reaching for gcongr is the better approach than trying to guess the lemma name, especially once you learn about show_term gcongr if you want to discover what it found.

[Isak Colboubrani]

Thanks @Eric Wieser. TIL about show_term. Very handy!

[Isak Colboubrani]

What about the third non-gcongr example?

import Mathlib
theorem one_le_factorial_a {n : ℕ} : 1 ≤ (n)! := by
  have : n ! ≠ 0 := factorial_ne_zero n
  omega
theorem one_le_factorial_b {n : ℕ} : 1 ≤ (n)! := by
  induction n with
  | zero => rfl
  | succ n h => exact Nat.le_trans h factorial_le_factorial_succ_a -- defined above

How could these proofs be improved to be more idiomatic and more aligned with Mathlib coding standards?

[Eric Wieser]

The first proof looks pretty good to me

[Eric Wieser]

You could golf it using Nat.one_le_iff_ne_zero if you wanted, but I think reviewers would only suggest that if they wanted an excuse to play golf.

[Isak Colboubrani]

I often find it challenging to decide when to use the "most specific theorem" available to advance a proof versus when to adopt a broader approach with higher-level tactics (like omega and gcongr in the examples above).

As a beginner, I find the latter tactics-based approach more readable, and also nicer from a workflow perspective. As @Eric Wieser mentioned, I could use show_term tac as a tool to discover the underlying theorems, and then replace the higher level tactics with direct use of the underlying theorem (via exact, apply, etc.).

Is there a good rule of thumb for when to keep the higher-level tactic in the proof, versus replacing it with the "more specific underlying theorem"?

Is this trade-off mainly a matter of readability versus compile-time efficiency, or do other factors come into play?