English
Factorial can be defined by binary splitting: factorialBinarySplitting(n) is 1 if n=0, else the product of numbers 1..n computed by recursively splitting the range.
Русский
Факториал может быть определён через бинарное разбиение: factorialBinarySplitting(n) равно 1 при n=0, иначе произведение 1⋯n вычисляется рекурсивно через разбиение диапазона.
LaTeX
$$factorialBinarySplitting(n) = 1 if n = 0, otherwise prodRange 1 (n+1)$$
Lean4
/-- Factorial implemented using binary splitting.
While this still performs the same number of multiplications,
the big-integer operands to each are much smaller. -/
def factorialBinarySplitting (n : Nat) : Nat :=
if _ : n = 0 then 1 else prodRange 1 (n + 1)
where/-- `prodRange lo hi` is the product of the range `lo` to `hi` (exclusive),
computed by binary splitting.
-/
prodRange (lo hi : Nat) (h : lo < hi := by grind) : Nat :=
if _ : hi = lo + 1 then lo
else
let mid := (lo + hi) / 2
prodRange lo mid * prodRange mid hi
