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:
- The Hitchhiker’s Guide to Logical Verification