norm_num extensions for factorials

Extensions for norm_num that compute Nat.factorial, Nat.ascFactorial and Nat.descFactorial.

This is done by reducing each of these to ascFactorial, which is computed using a divide and conquer strategy that improves performance and avoids exceeding the recursion depth.

theorem Mathlib.Meta.NormNum.asc_factorial_aux (n l m a b : ℕ) (h₁ : n.ascFactorial l = a) (h₂ : (n + l).ascFactorial m = b) : n.ascFactorial (l + m) = a * b

partial def Mathlib.Meta.NormNum.proveAscFactorial (n l : ℕ) (en el : Q(ℕ)) : ℕ × (eresult : Q(ℕ)) × Q(«$en».ascFactorial «$el» = «$eresult»)

Calculate n.ascFactorial l and return this value along with a proof of the result.

theorem Mathlib.Meta.NormNum.isNat_factorial {n x : ℕ} (h₁ : IsNat n x) (a : ℕ) (h₂ : Nat.ascFactorial 1 x = a) : IsNat n.factorial a

def Mathlib.Meta.NormNum.evalNatFactorial : NormNumExt

Evaluates the Nat.factorial function.

Equations

• One or more equations did not get rendered due to their size.

theorem Mathlib.Meta.NormNum.isNat_ascFactorial {n x l y : ℕ} (h₁ : IsNat n x) (h₂ : IsNat l y) (a : ℕ) (p : x.ascFactorial y = a) : IsNat (n.ascFactorial l) a

def Mathlib.Meta.NormNum.evalNatAscFactorial : NormNumExt

Evaluates the Nat.ascFactorial function.

Equations

• One or more equations did not get rendered due to their size.

theorem Mathlib.Meta.NormNum.isNat_descFactorial {n x l y : ℕ} (z : ℕ) (h₁ : IsNat n x) (h₂ : IsNat l y) (h₃ : x = z + y) (a : ℕ) (p : (z + 1).ascFactorial y = a) : IsNat (n.descFactorial l) a

theorem Mathlib.Meta.NormNum.isNat_descFactorial_zero {n x l y : ℕ} (z : ℕ) (h₁ : IsNat n x) (h₂ : IsNat l y) (h₃ : y = z + x + 1) : IsNat (n.descFactorial l) 0

def Mathlib.Meta.NormNum.evalNatDescFactorial : NormNumExt

Evaluates the Nat.descFactorial function.

Equations

• One or more equations did not get rendered due to their size.