Evolution of a Lean programmer

Changes

1 changed files (+79/-0)

• Factorial.lean (new)
  • @@ -0,0 +1,79 @@
    + import Mathlib + + /-- + Novice Lean programmer + Hey this is kinda like Python right? + -/ + def fac₁ n := Id.run do + let mut ans := 1 + for i in List.range' 1 n do + ans := ans * i + return ans + + #eval fac₁ 5 + + /-- + Intermediate Lean programmer + Hmmm, just an ordinary functional programming language? + -/ + def fac₂ n := + if n > 1 then n * fac₂ (n - 1) else n + + #eval fac₂ 5 + + /-- + Experienced Lean programmer + It compiles so it's probably correct + -/ + def fac₃ + | 0 => 0 + | n + 1 => (n + 1) * fac₃ n + + #eval fac₃ 5 + + /-- + Lean golfer + It's so short and cute! + -/ + def fac₄ n := + [1:n+1].toList.prod + + #eval fac₄ 5 + + /- + Evil Lean programmer + -/ + namespace evil + instance : Zero ℕ where + zero := 1 + + instance : Add ℕ where + add := Nat.mul + + def fac₅ n := + List.range' 1 n |>.sum + + #eval fac₅ 5 + end evil + + /-- + Secretly a mathematician + -/ + def fac₆ n := + ∏ i ∈ Finset.Ioc 0 n, i + + #eval fac₆ 5 + + /-- + Openly a mathematician + -/ + noncomputable def fac₇ (n : ℕ) : ℂ := + ∫ x in Set.Ioi (0 : ℝ), ↑(-x).exp * ↑x ^ n + + example : fac₇ 5 = 120 := by + rw [fac₇] + suffices Complex.GammaIntegral 6 = 120 by + rw [← this, Complex.GammaIntegral] + norm_cast + rw [← Complex.Gamma_eq_integral (by simp), Complex.Gamma_ofNat_eq_factorial] + simp [Nat.factorial]