factorial is primrec

Stream: mathlib4

[Alex Meiburg]

This was a fact I wanted recently for something else, and I would like to make (as a very very short) PR to Mathlib, but I don't have a good idea of where to put it.

/-- The factorial function is primitive recursive. -/
theorem Primrec.factorial : Primrec Nat.factorial := by
  convert list_foldl (σ := ℕ) (h := fun n ⟨p, k⟩ ↦ p * (k + 1)) list_range (const 1) ?_
  · rw [← Finset.prod_range_add_one_eq_factorial, ← List.foldl_map, ← List.prod_eq_foldl]
    rw [← List.prod_toFinset _ List.nodup_range, ← List.toFinset_range]
  · refine comp₂ ?_ .right
    exact nat_mul.comp₂ .left (succ.comp₂ .right)

There's no file that imports both Nat.factorial and Primrec, as far as I can tell. It would feel silly for the file on factorial to import Primrec to have this fact, as would the other way. It would feel even sillier to add a new file just for this one fact.

I thought I'd ask a maintainer which of those three silly things would be best. (Or maybe something else)

[Bhavik Mehta]

I think putting it in primrec is reasonable (or rather, least unreasonable)

[Ruben Van de Velde]

A new file would be fine too

[Violeta Hernández]

The primrec file is already huge. Let's maybe try not to add to it even further.

[Bolton Bailey]

In fact it's so huge, it triggers the file size linter. We should split it regardless of whether we want to add to it.

[Bolton Bailey]

Here is a candidate PR #33835

[Alex Meiburg]

I added this fact and several other nat functions in this PR: #33864

[Alex Meiburg]

oh wow, I didn't realize it was literally the largest file in Mathlib right now. Ha

[Bolton Bailey]

My PR was merged, so you might have to fix a conflict, sorry!

[Alex Meiburg]

should be okay now. (And thanks, Bolton!)