Lean for All

Day 12: Using other theorems🔗

Follow proofs that use library theorems with exact and apply, and that record facts with have.

Lean comes with a library of proved theorems. You can use one like a tool. Nat.le_of_lt says:

Nat.le_of_lt {n m : Nat} : n < m → n ≤ m#check Nat.le_of_lt 
Nat.le_of_lt {n m : Nat} : n < m → n ≤ m

Lean answers Nat.le_of_lt {n m : Nat} : n < m → n ≤ m: if n < m, then n ≤ m. Given a proof h : a < b, writing Nat.le_of_lt h gives a proof of a ≤ b:

theorem weaken (a b : Nat) (h : a < b) : a ≤ b := a:Natb:Nath:a < b⊢ a ≤ b All goals completed! 🐙

A hypothesis hpq : P → Q works the same way: hpq hp is a proof of Q.

apply uses a theorem backwards. The goal is a ≤ b, and Nat.le_of_lt ends in ≤, so:

theorem weaken' (a b : Nat) (h : a < b) : a ≤ b := a:Natb:Nath:a < b⊢ a ≤ b a:Natb:Nath:a < b⊢ a < b All goals completed! 🐙 
a b : Nat
h : a < b
⊢ a ≤ b

becomes

a b : Nat
h : a < b
⊢ a < b

Read apply as: “to prove a ≤ b, it is enough to prove a < b”. The goal becomes the theorem’s if-part.

Some theorems need two facts. Nat.lt_trans says n < m → m < k → n < k: if n < m and m < k, then n < k. The facts go in that order:

theorem chain (x y z : Nat) (h1 : x < y) (h2 : y < z) : x < z := x:Naty:Natz:Nath1:x < yh2:y < z⊢ x < z All goals completed! 🐙

h1 fills the first if-part (x < y), h2 the second (y < z).

have records an intermediate fact, with its proof, so later steps can use it:

theorem two_steps (a b c : Nat) (h1 : a < b) (h2 : b < c) : a ≤ c := a:Natb:Natc:Nath1:a < bh2:b < c⊢ a ≤ c a:Natb:Natc:Nath1:a < bh2:b < ch3:a < c⊢ a ≤ c All goals completed! 🐙

After the have line, the display gains h3 : a < c above the ⊢, and the goal a ≤ c is unchanged.

For an auditor: unlike a hypothesis, a have comes with its own proof, which Lean checks. A proof read as a story is often a chain of have lines: each is a step of the argument.

Check yourself🔗