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 $p, q$ be two arbitrary propositions.

Then

$$p \land q \implies q \land p$$

($\land$ is the logical And combinator)

This can be written in Lean as

def and_is_comm (p q: Prop) (h: p ∧ q): q ∧ p := 
	sorry

(∧ is entered with \and; ∨ with \or)

This function takes 3 arguments:

• Two propositions p , q
• A value h of type p ∧ q. In other words, h is 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.left and 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 and_is_comm:

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 by.

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

The symbol ⊢ (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.intro uses the constructor And.intro to 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 q and p separately, since we can use And.intro afterwards.

• exact h.right uses the function and.right to select the q component of h, and tries to close the subgoal q with it.
• exact h.left does 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 Nat.add_zero

2.2 Example 3

On the other hand:

needs to be proved.

We'll use mathematical induction over the input argument n:

theorem zero_add (n: Nat): 0 + n = n := by
  induction n with
  | zero =>
    -- base case:
    sorry
    
  | succ d hd =>
    -- inductive step:
    sorry

The induction tactic operates on the goal, which has to be a proposition that depends on a given variable n: Nat, whereas d and 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 rfl

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 rfl:

The rewrite tactic rw takes a value h of type a = b and uses it to replace all occurrences of a by b in the goal.

We're going to use the std library function Nat.add_succ:

Nat.add_succ : ∀ (n m : Nat), n + Nat.succ m = Nat.succ (n + m)

in particular

#check Nat.add_succ 0

-- Nat.add_succ 0 : ∀ (m : Nat), 0 + Nat.succ m = Nat.succ (0 + m)

so that

rw [Nat.add_succ 0 d]

will transform

⊢ 0 + Nat.succ d = Nat.succ d

into

⊢ Nat.succ (0 + d) = Nat.succ d

Similarly, rw [hd] will replace 0 + d by d.

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 🎉

The line rw [Nat.add_succ 0 d] can be also written as rw [Nat.add_succ], as Lean can infer the arguments 0 and d.

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.

• consecutive rw lines can be collapsed into a single rw [...]
• 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 length and 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 rfl:

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

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) ▸ e replaces all occurrences of a for b in e. It servers the same purpose as rw in 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 map and d3 from the definition of length.

This shows that we can use rfl (or 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.

Resources

• Theorem Proving in Lean:
  • Tactics
  • Induction and Recursion
• The Hitchhiker’s Guide to Logical Verification