Examples of programs and in Lean

We see our first examples of programs and proofs in Lean. A major goal is to illustrate functional programming, where we use recursions for loops and avoid mutable variables.

We define recursively summing to n and prove a theorem about it.

def sumToN (n : ℕ) : ℕ

The function sumToN computes the sum of the first n natural numbers.

Equations

• sumToN 0 = 0
• sumToN m.succ = sumToN m + (m + 1)

theorem sumToN_eq (n : ℕ) : 2 * sumToN n = n * (n + 1)

The theorem sumToN_eq states that the sum of the first n natural numbers is n * (n + 1) / 2.

@[irreducible]

def sumToN' (n : ℕ) : ℕ

Equations

• sumToN' n = if n = 0 then 0 else sumToN' (n - 1) + n

Lean allows imperative programming, but it is not recommended. Here is an example of a program that uses a mutable variable.

def sumToNImperative (n : ℕ) : ℕ

Equations

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