Over the past few articles we’ve talked about inductive types, dependent functions, propositions as types, type classes, etc.
While this machinery is not strictly needed to start writing simple proofs (as witnessed by the amazing Natural Numbers Game), it certainly is when one is ready to move beyond carefully crafted pedagogical examples.
Today we’re finally in a position to discuss in much more detail how to create proofs in Lean; in particular we’ll analyze examples introduced previously.
Latest revision: Sep 4, 2022
1. Two styles of proofs
1.1 Forward Proofs
A “forward” or “functional” proof is just a regular function that uses standard functional programming constructs such as function application, pattern matching, variable assignment, etc. to construct a value of a given type.
1.1.1 Example 1
As a first example let’s analyze the following statement:
Let be two arbitrary propositions.
( is the logical
This can be written in Lean as
def and_is_comm (p q: Prop) (h: p ∧ q): q ∧ p := sorry
∧ is entered with
This function takes 3 arguments:
- Two propositions
- A value
p ∧ q. In other words,
his a proof of the proposition
p ∧ q.
The function itself corresponds to a logical implication; in order to prove it we have to create a value of type
q ∧ p.
Looking at the definition of the
And combinator we notice it is a structure with one constructor:
structure And (a b: Prop): Prop := intro :: (left: a) (right: b)
Note on syntax:
intro ::changes the default constructor’s name (
mk), so that values can be created with
And.intro a b
This means that we can use
And.intro to introduce (i.e. create) conjunctions, and we can use
And.right to eliminate (i.e. consume, or extract components of) conjunctions.
The unicode symbol
∧ is just an infix alias for the type
and, declared like so:
infixr:35 " ∧ " => And
With this information let’s finish the proof of
theorem and_is_comm (p q: Prop) (h: p ∧ q): q ∧ p := And.intro h.right h.left
1.2 Backward Proofs
A second way to build proofs is using tactics. Tactics are meta programs that provide a layer of automation on top of the normal “forward” style. In many cases they are more convenient for interactive use:
theorem and_is_comm' (p q: Prop) (h: p ∧ q): q ∧ p := by apply And.intro exact h.right exact h.left
Tactics can only be used in tactic mode, which can be entered with the keywords
Before describing each tactic we need to talk about the local context and the proof goal.
The local context can be seen in VSCode’s Lean Infoview. If you place the cursor in the
by line above you should see this:
pq: Prop h: p ∧ q ⊢ q ∧ p
⊢ (turnstile) is used in logic to indicate that the right-hand side (
q ∧ p) can be proved, or follows logically from the left-hand side.
The general form is:
Context ⊢ Goal
- The context is a series of statements describing terms of specific types.
- The goal is a type; in many cases a proposition
It is common to use the letter Gamma to represent the context:
Γ ⊢ Goal
When proving things in Lean our objective is to create a term of the type specified by the goal; or alternatively simplify the goal into something that is logically equivalent.
Returning to our proof:
apply And.introuses the constructor
And.introto generate two (sub) goals:
pq: Prop h: p ∧ q ⊢ q pq: Prop h: p ∧ q ⊢ p
Intuitively, in order to prove
q ∧ p it suffices to prove
p separately, since we can use
exact h.rightuses the function
and.rightto select the
h, and tries to close the subgoal
exact h.leftdoes the same for the second subgoal
After this there are no more goals left so this concludes the proof.
Notice how the context is just the scope of the function that represents the proof.
2. Induction and Natural Numbers
2.1 Example 2
Let’s start with this proposition:
Addition of natural numbers is defined in Lean like so:
def add: Nat -> Nat -> Nat | a, 0 => a | a, b + 1 => (add a b) + 1
and so the proposition is true basically “by definition” (it is the first case
|a, 0 => a above)
theorem add_zero' (n: Nat): n + 0 = n := by rfl
this theorem is available in the stdlib as
2.2 Example 3
On the other hand:
needs to be proved.
We’ll use mathematical induction over the input argument
theorem zero_add (n: Nat): 0 + n = n := by induction n with | zero => -- base case: sorry | succ d hd => -- inductive step: sorry
induction tactic operates on the goal, which has to be a proposition that depends on a given variable
n: Nat, whereas
hd are (arbitrary) variable names.
induction creates two subgoals, the base case and the inductive step:
case zero ⊢ 0 + Nat.zero = Nat.zero case succ d: Nat hd: 0 + d = d ⊢ 0 + Nat.succ d = Nat.succ d
The first subgoal can be completed with
theorem zero_add (n: Nat): 0 + n = n := by induction n with | zero => rfl | succ d hd => -- inductive step: sorry
For the second subgoal we’ll use the tactic
rw to rewrite it towards something that can be proved by
The rewrite tactic
rwtakes a value
a = band uses it to replace all occurrences of
bin the goal.
We’re going to use the std library function
Nat.add_succ : ∀ (n m : Nat), n + Nat.succ m = Nat.succ (n + m)
#check Nat.add_succ 0 -- Nat.add_succ 0 : ∀ (m : Nat), 0 + Nat.succ m = Nat.succ (0 + m)
rw [Nat.add_succ 0 d]
⊢ 0 + Nat.succ d = Nat.succ d
⊢ Nat.succ (0 + d) = Nat.succ d
rw [hd] will replace
0 + d by
Putting all the pieces together:
theorem zero_add (n: Nat): 0 + n = n := by induction n with | zero => rfl | succ d hd => rw [Nat.add_succ 0 d] rw [hd] -- Goals accomplished 🎉
rw [Nat.add_succ 0 d] can be also written as
rw [Nat.add_succ], as Lean can infer the arguments
Before moving on let’s show a different approach that can produce more compact proofs:
theorem zero_add': ∀ (n: Nat), 0 + n = n | 0 => rfl | d + 1 => by rw [Nat.add_succ, zero_add' d]
We are pattern matching on the structure of
n: Nat and returning two proofs, and Lean is using them to assemble the full inductive proof.
rwlines can be collapsed into a single
- within the inductive step
(d + 1)Lean adds the inductive hypothesis as
zero_add': ∀ (n : Nat), 0 + n = n
3. Structural Induction
Induction over the natural numbers (mathematical induction) is a special case of Structural Induction, which can be used in Lean to prove properties of inductively defined data types.
3.1 Example 4
Let’s analyze the
map_length example we mentioned back in the first part of this series.
Given the following definitions of
map on Lists:
def length: List A -> Nat |  => 0 | _ :: t => 1 + length t def map (f: A -> B): List A -> List B |  =>  | h :: t => f h :: map f t
we’ll prove that applying
map doesn’t change the length of the resulting List.
length (map f l) = length l
The idea is the same as in induction over the natural numbers: we consider all constructors for the given data type and provide proofs of all cases. Lean will assemble all the pieces into a proof that is valid for all inhabitants of the given type:
theorem map_length (f: A -> B): ∀ (l: List A), length (map f l) = length l |  => by rfl | h :: t => by rw [length, map, length, map_length f t]
The base case is trivially true (provable by
rfl) so let’s focus on the inductive step.
This is the initial proof state:
A B: Type f: A → B map_length: ∀ (l : List A), length (map f l) = length l h: A t: List A ⊢ length (map f (h :: t)) = length (h :: t)
we’re going to manipulate the goal until we get something “obvious” that can be proved by
In this case we’ve used
rw with a function as an argument (instead of an equation);
rw will “unfold” the function definition, one step at a time.
The last step has the form
a = a, and
rw [map_length] will apply
rfl automatically for us, thus closing the goal.
This is a good moment to mention the tactic
simp [h₁ h₂ ... hₙ]uses the provided expressions and other theorems tagged with the attribute
[simp]to simplify the main goal.
We could have proved the inductive step like this:
| h :: t => by simp [length, map, map_length]
3.2 A very low level proof
As a comparison here’s a different proof (in functional style), showing all the gory details:
theorem map_length' (f: A -> B): ∀ (l: List A), length (map f l) = length l |  => rfl | h :: t => -- show that: length (map f (h :: t)) = length (h :: t) let l1: length (map f t) = length t := map_length' f t -- by induction hypothesis let l2: 1 + length (map f t) = 1 + length t := congrArg _ l1 -- adding 1 in both sides let d1: 1 + length (map f t) = length (f h :: map f t) := rfl -- by definition of length let d2: f h :: map f t = map f (h :: t) := rfl -- by definition of map let l3: 1 + length t = length (f h :: map f t) := l2 ▸ d1 -- substitution (l2 in d1) let l4: 1 + length t = length (map f (h :: t)) := d2 ▸ l3 -- substitution (d2 in l3) let d3: 1 + length t = length (h :: t) := rfl -- by definition of length again let goal: length (map f (h :: t)) = length (h :: t) := l4 ▸ d3 -- substitution (l4 in d3) goal
(a = b) ▸ ereplaces all occurrences of
e. It servers the same purpose as
rwin tactic mode.
If you look carefully at lines 9 and 12:
let d2: f h :: map f t = map f (h :: t) := rfl let d3: 1 + length t = length (h :: t) := rfl
you’ll notice that we’re creating proofs of something that is not literally of the form
a = a.
d2 follows from the defintion of
d3 from the definition of
This shows that we can use
by rfl) to prove that two things are identical or equal “by definition”.
Tactic-mode proofs are very handy for interactive use, since it’s easy to inspect the state of the proof. On the other hand the state itself is not captured in the source code, which can make the proof harder to read.
It is good to remember that tactic mode and regular mode can be mixed as needed.
- Theorem Proving in Lean:
- The Hitchhiker’s Guide to Logical Verification