Lean for All

Day 16: Definitions by cases and recursion🔗

Read definitions written case by case or in terms of themselves, by computing small cases, and read the goals that induction produces.

Some definitions treat inputs case by case. This one gives the number before n:

def before : Nat → Nat | 0 => 0 | n + 1 => n 4#eval before 5 0#eval before 0 
4
0

Nat → Nat means “takes a natural number, gives a natural number”. Each line starting with | is a case: a pattern on the left of =>, the result on the right. The pattern n + 1 matches every number that is one more than some n (so every number except 0), and calls that smaller number n.

Notice before 0 = 0. No natural number comes before 0, so the writer had to pick something. Every case must give some value.

The same idea is often written with match:

def isZero (n : Nat) : Bool := match n with | 0 => true | _ => false true#eval isZero 0 false#eval isZero 7 
true
false

match n with means “look at n and pick the first case that fits”. Lean tries the cases from top to bottom. The pattern _ matches anything, so it catches every n that is not 0.

Bool is the type with the two values true and false, which a program can compute. It is different from Prop, the type of statements, which need proofs.

A definition can use itself on a smaller input. This is recursion:

def fact : Nat → Nat | 0 => 1 | n + 1 => (n + 1) * fact n 24#eval fact 4 
24

To read it, compute small cases by hand, from the bottom up:

  • fact 0 = 1

  • fact 1 = 1 * fact 0 = 1

  • fact 2 = 2 * fact 1 = 2

  • fact 3 = 3 * fact 2 = 6

So fact n is 1 × 2 × … × n, the factorial of n. Each step uses a smaller number, so the computation always reaches 0 and stops.

Small cases are the fastest way to catch a wrong definition. This one is meant to add up 0 + 1 + … + n:

def sumTo : Nat → Nat | 0 => 0 | n + 1 => n + sumTo n 3#eval sumTo 3 
3

Lean shows 3, but 0 + 1 + 2 + 3 = 6. The second case should add n + 1, not n. Every theorem about this sumTo is about the wrong function.

Small cases can show that a definition is wrong. They cannot show that it is right for every n: that needs a proof.

Proofs about recursive definitions usually use induction. You only need to read the goals it produces:

def fact : Nat → Nat | 0 => 1 | n + 1 => (n + 1) * fact n theorem fact_pos (n : Nat) : fact n > 0 := n:Nat⊢ fact n > 0 induction n with ⊢ fact 0 > 0 All goals completed! 🐙 n:Natih:fact n > 0⊢ fact (n + 1) > 0 All goals completed! 🐙

induction n splits the goal in two:

case zero
⊢ fact 0 > 0

case succ
n : Nat
ih : fact n > 0
⊢ fact (n + 1) > 0

First prove it for 0. Then prove it for n + 1, assuming it for n. That assumption, ih, is the induction hypothesis. Together the two cases cover 0, 1, 2, … like a row of falling dominoes.

Check yourself🔗