# Proving Equivalence

Programs that have been rewritten to use tail recursion and an accumulator can look quite different from the original program. The original recursive function is often much easier to understand, but it runs the risk of exhausting the stack at run time. After testing both versions of the program on examples to rule out simple bugs, proofs can be used to show once and for all that the programs are equivalent.

## Proving `sum`

Equal

To prove that both versions of `sum`

are equal, begin by writing the theorem statement with a stub proof:

```
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
skip
```

As expected, Lean describes an unsolved goal:

```
unsolved goals
⊢ NonTail.sum = Tail.sum
```

The `rfl`

tactic cannot be applied here, because `NonTail.sum`

and `Tail.sum`

are not definitionally equal.
Functions can be equal in more ways than just definitional equality, however.
It is also possible to prove that two functions are equal by proving that they produce equal outputs for the same input.
In other words, \( f = g \) can be proved by proving that \( f(x) = g(x) \) for all possible inputs \( x \).
This principle is called *function extensionality*.
Function extensionality is exactly the reason why `NonTail.sum`

equals `Tail.sum`

: they both sum lists of numbers.

In Lean's tactic language, function extensionality is invoked using `funext`

, followed by a name to be used for the arbitrary argument.
The arbitrary argument is added as an assumption to the context, and the goal changes to require a proof that the functions applied to this argument are equal:

```
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
funext xs
```

```
unsolved goals
case h
xs : List Nat
⊢ NonTail.sum xs = Tail.sum xs
```

This goal can be proved by induction on the argument `xs`

.
Both `sum`

functions return `0`

when applied to the empty list, which serves as a base case.
Adding a number to the beginning of the input list causes both functions to add that number to the result, which serves as an induction step.
Invoking the `induction`

tactic results in two goals:

```
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
funext xs
induction xs with
| nil => skip
| cons y ys ih => skip
```

```
unsolved goals
case h.nil
⊢ NonTail.sum [] = Tail.sum []
```

```
unsolved goals
case h.cons
y : Nat
ys : List Nat
ih : NonTail.sum ys = Tail.sum ys
⊢ NonTail.sum (y :: ys) = Tail.sum (y :: ys)
```

The base case for `nil`

can be solved using `rfl`

, because both functions return `0`

when passed the empty list:

```
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
funext xs
induction xs with
| nil => rfl
| cons y ys ih => skip
```

The first step in solving the induction step is to simplify the goal, asking `simp`

to unfold `NonTail.sum`

and `Tail.sum`

:

```
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
funext xs
induction xs with
| nil => rfl
| cons y ys ih =>
simp [NonTail.sum, Tail.sum]
```

```
unsolved goals
case h.cons
y : Nat
ys : List Nat
ih : NonTail.sum ys = Tail.sum ys
⊢ y + NonTail.sum ys = Tail.sumHelper 0 (y :: ys)
```

Unfolding `Tail.sum`

revealed that it immediately delegates to `Tail.sumHelper`

, which should also be simplified:

```
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
funext xs
induction xs with
| nil => rfl
| cons y ys ih =>
simp [NonTail.sum, Tail.sum, Tail.sumHelper]
```

In the resulting goal, `sumHelper`

has taken a step of computation and added `y`

to the accumulator:

```
unsolved goals
case h.cons
y : Nat
ys : List Nat
ih : NonTail.sum ys = Tail.sum ys
⊢ y + NonTail.sum ys = Tail.sumHelper y ys
```

Rewriting with the induction hypothesis removes all mentions of `NonTail.sum`

from the goal:

```
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
funext xs
induction xs with
| nil => rfl
| cons y ys ih =>
simp [NonTail.sum, Tail.sum, Tail.sumHelper]
rw [ih]
```

```
unsolved goals
case h.cons
y : Nat
ys : List Nat
ih : NonTail.sum ys = Tail.sum ys
⊢ y + Tail.sum ys = Tail.sumHelper y ys
```

This new goal states that adding some number to the sum of a list is the same as using that number as the initial accumulator in `sumHelper`

.
For the sake of clarity, this new goal can be proved as a separate theorem:

```
theorem helper_add_sum_accum (xs : List Nat) (n : Nat) :
n + Tail.sum xs = Tail.sumHelper n xs := by
skip
```

```
unsolved goals
xs : List Nat
n : Nat
⊢ n + Tail.sum xs = Tail.sumHelper n xs
```

Once again, this is a proof by induction where the base case uses `rfl`

:

```
theorem helper_add_sum_accum (xs : List Nat) (n : Nat) :
n + Tail.sum xs = Tail.sumHelper n xs := by
induction xs with
| nil => rfl
| cons y ys ih => skip
```

```
unsolved goals
case cons
n y : Nat
ys : List Nat
ih : n + Tail.sum ys = Tail.sumHelper n ys
⊢ n + Tail.sum (y :: ys) = Tail.sumHelper n (y :: ys)
```

Because this is an inductive step, the goal should be simplified until it matches the induction hypothesis `ih`

.
Simplifying, using the definitions of `Tail.sum`

and `Tail.sumHelper`

, results in the following:

```
theorem helper_add_sum_accum (xs : List Nat) (n : Nat) :
n + Tail.sum xs = Tail.sumHelper n xs := by
induction xs with
| nil => rfl
| cons y ys ih =>
simp [Tail.sum, Tail.sumHelper]
```

```
unsolved goals
case cons
n y : Nat
ys : List Nat
ih : n + Tail.sum ys = Tail.sumHelper n ys
⊢ n + Tail.sumHelper y ys = Tail.sumHelper (y + n) ys
```

Ideally, the induction hypothesis could be used to replace `Tail.sumHelper (y + n) ys`

, but they don't match.
The induction hypothesis can be used for `Tail.sumHelper n ys`

, not `Tail.sumHelper (y + n) ys`

.
In other words, this proof is stuck.

## A Second Attempt

Rather than attempting to muddle through the proof, it's time to take a step back and think.
Why is it that the tail-recursive version of the function is equal to the non-tail-recursive version?
Fundamentally speaking, at each entry in the list, the accumulator grows by the same amount as would be added to the result of the recursion.
This insight can be used to write an elegant proof.
Crucially, the proof by induction must be set up such that the induction hypothesis can be applied to *any* accumulator value.

Discarding the prior attempt, the insight can be encoded as the following statement:

```
theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
(n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
skip
```

In this statement, it's very important that `n`

is part of the type that's after the colon.
The resulting goal begins with `∀ (n : Nat)`

, which is short for "For all `n`

":

```
unsolved goals
xs : List Nat
⊢ ∀ (n : Nat), n + NonTail.sum xs = Tail.sumHelper n xs
```

Using the induction tactic results in goals that include this "for all" statement:

```
theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
(n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
induction xs with
| nil => skip
| cons y ys ih => skip
```

In the `nil`

case, the goal is:

```
unsolved goals
case nil
⊢ ∀ (n : Nat), n + NonTail.sum [] = Tail.sumHelper n []
```

For the induction step for `cons`

, both the induction hypothesis and the specific goal contain the "for all `n`

":

```
unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
⊢ ∀ (n : Nat), n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)
```

In other words, the goal has become more challenging to prove, but the induction hypothesis is correspondingly more useful.

A mathematical proof for a statement that beings with "for all \( x \)" should assume some arbitrary \( x \), and prove the statement.
"Arbitrary" means that no additional properties of \( x \) are assumed, so the resulting statement will work for *any* \( x \).
In Lean, a "for all" statement is a dependent function: no matter which specific value it is applied to, it will return evidence of the proposition.
Similarly, the process of picking an arbitrary \( x \) is the same as using `fun x => ...`

.
In the tactic language, this process of selecting an arbitrary \( x \) is performed using the `intro`

tactic, which produces the function behind the scenes when the tactic script has completed.
The `intro`

tactic should be provided with the name to be used for this arbitrary value.

Using the `intro`

tactic in the `nil`

case removes the `∀ (n : Nat),`

from the goal, and adds an assumption `n : Nat`

:

```
theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
(n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
induction xs with
| nil => intro n
| cons y ys ih => skip
```

```
unsolved goals
case nil
n : Nat
⊢ n + NonTail.sum [] = Tail.sumHelper n []
```

Both sides of this propositional equality are definitionally equal to `n`

, so `rfl`

suffices:

```
theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
(n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
induction xs with
| nil =>
intro n
rfl
| cons y ys ih => skip
```

The `cons`

goal also contains a "for all":

```
unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
⊢ ∀ (n : Nat), n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)
```

This suggests the use of `intro`

.

```
theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
(n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
induction xs with
| nil =>
intro n
rfl
| cons y ys ih =>
intro n
```

```
unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)
```

The proof goal now contains both `NonTail.sum`

and `Tail.sumHelper`

applied to `y :: ys`

.
The simplifier can make the next step more clear:

```
theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
(n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
induction xs with
| nil =>
intro n
rfl
| cons y ys ih =>
intro n
simp [NonTail.sum, Tail.sumHelper]
```

```
unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + (y + NonTail.sum ys) = Tail.sumHelper (y + n) ys
```

This goal is very close to matching the induction hypothesis. There are two ways in which it does not match:

- The left-hand side of the equation is
`n + (y + NonTail.sum ys)`

, but the induction hypothesis needs the left-hand side to be a number added to`NonTail.sum ys`

. In other words, this goal should be rewritten to`(n + y) + NonTail.sum ys`

, which is valid because addition of natural numbers is associative. - When the left side has been rewritten to
`(y + n) + NonTail.sum ys`

, the accumulator argument on the right side should be`n + y`

rather than`y + n`

in order to match. This rewrite is valid because addition is also commutative.

The associativity and commutativity of addition have already been proved in Lean's standard library.
The proof of associativity is named `Nat.add_assoc`

, and its type is `(n m k : Nat) → (n + m) + k = n + (m + k)`

, while the proof of commutativity is called `Nat.add_comm`

and has type `(n m : Nat) → n + m = m + n`

.
Normally, the `rw`

tactic is provided with an expression whose type is an equality.
However, if the argument is instead a dependent function whose return type is an equality, it attempts to find arguments to the function that would allow the equality to match something in the goal.
There is only one opportunity to apply associativity, though the direction of the rewrite must be reversed because the right side of the equality in `Nat.add_assoc`

is the one that matches the proof goal:

```
theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
(n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
induction xs with
| nil =>
intro n
rfl
| cons y ys ih =>
intro n
simp [NonTail.sum, Tail.sumHelper]
rw [←Nat.add_assoc]
```

```
unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + y + NonTail.sum ys = Tail.sumHelper (y + n) ys
```

Rewriting directly with `Nat.add_comm`

, however, leads to the wrong result.
The `rw`

tactic guesses the wrong location for the rewrite, leading to an unintended goal:

```
theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
(n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
induction xs with
| nil =>
intro n
rfl
| cons y ys ih =>
intro n
simp [NonTail.sum, Tail.sumHelper]
rw [←Nat.add_assoc]
rw [Nat.add_comm]
```

```
unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ NonTail.sum ys + (n + y) = Tail.sumHelper (y + n) ys
```

This can be fixed by explicitly providing `y`

and `n`

as arguments to `Nat.add_comm`

:

```
theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
(n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
induction xs with
| nil =>
intro n
rfl
| cons y ys ih =>
intro n
simp [NonTail.sum, Tail.sumHelper]
rw [←Nat.add_assoc]
rw [Nat.add_comm y n]
```

```
unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + y + NonTail.sum ys = Tail.sumHelper (n + y) ys
```

The goal now matches the induction hypothesis.
In particular, the induction hypothesis's type is a dependent function type.
Applying `ih`

to `n + y`

results in exactly the desired type.
The `exact`

tactic completes a proof goal if its argument has exactly the desired type:

```
theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
(n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
induction xs with
| nil => intro n; rfl
| cons y ys ih =>
intro n
simp [NonTail.sum, Tail.sumHelper]
rw [←Nat.add_assoc]
rw [Nat.add_comm y n]
exact ih (n + y)
```

The actual proof requires only a little additional work to get the goal to match the helper's type. The first step is still to invoke function extensionality:

```
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
funext xs
```

```
unsolved goals
case h
xs : List Nat
⊢ NonTail.sum xs = Tail.sum xs
```

The next step is unfold `Tail.sum`

, exposing `Tail.sumHelper`

:

```
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
funext xs
simp [Tail.sum]
```

```
unsolved goals
case h
xs : List Nat
⊢ NonTail.sum xs = Tail.sumHelper 0 xs
```

Having done this, the types almost match.
However, the helper has an additional addend on the left side.
In other words, the proof goal is `NonTail.sum xs = Tail.sumHelper 0 xs`

, but applying `non_tail_sum_eq_helper_accum`

to `xs`

and `0`

yields the type `0 + NonTail.sum xs = Tail.sumHelper 0 xs`

.
Another standard library proof, `Nat.zero_add`

, has type `(n : Nat) → 0 + n = n`

.
Applying this function to `NonTail.sum xs`

results in an expression with type `0 + NonTail.sum xs = NonTail.sum xs`

, so rewriting from right to left results in the desired goal:

```
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
funext xs
simp [Tail.sum]
rw [←Nat.zero_add (NonTail.sum xs)]
```

```
unsolved goals
case h
xs : List Nat
⊢ 0 + NonTail.sum xs = Tail.sumHelper 0 xs
```

Finally, the helper can be used to complete the proof:

```
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
funext xs
simp [Tail.sum]
rw [←Nat.zero_add (NonTail.sum xs)]
exact non_tail_sum_eq_helper_accum xs 0
```

This proof demonstrates a general pattern that can be used when proving that an accumulator-passing tail-recursive function is equal to the non-tail-recursive version.
The first step is to discover the relationship between the starting accumulator argument and the final result.
For instance, beginning `Tail.sumHelper`

with an accumulator of `n`

results in the final sum being added to `n`

, and beginning `Tail.reverseHelper`

with an accumulator of `ys`

results in the final reversed list being prepended to `ys`

.
The second step is to write down this relationship as a theorem statement and prove it by induction.
While the accumulator is always initialized with some neutral value in practice, such as `0`

or `[]`

, this more general statement that allows the starting accumulator to be any value is what's needed to get a strong enough induction hypothesis.
Finally, using this helper theorem with the actual initial accumulator value results in the desired proof.
For example, in `non_tail_sum_eq_tail_sum`

, the accumulator is specified to be `0`

.
This may require rewriting the goal to make the neutral initial accumulator values occur in the right place.

## Exercise

### Warming Up

Write your own proofs for `Nat.zero_add`

, `Nat.add_assoc`

, and `Nat.add_comm`

using the `induction`

tactic.

### More Accumulator Proofs

#### Reversing Lists

Adapt the proof for `sum`

into a proof for `NonTail.reverse`

and `Tail.reverse`

.
The first step is to think about the relationship between the accumulator value being passed to `Tail.reverseHelper`

and the non-tail-recursive reverse.
Just as adding a number to the accumulator in `Tail.sumHelper`

is the same as adding it to the overall sum, using `List.cons`

to add a new entry to the accumulator in `Tail.reverseHelper`

is equivalent to some change to the overall result.
Try three or four different accumulator values with pencil and paper until the relationship becomes clear.
Use this relationship to prove a suitable helper theorem.
Then, write down the overall theorem.
Because `NonTail.reverse`

and `Tail.reverse`

are polymorphic, stating their equality requires the use of `@`

to stop Lean from trying to figure out which type to use for `α`

.
Once `α`

is treated as an ordinary argument, `funext`

should be invoked with both `α`

and `xs`

:

```
theorem non_tail_reverse_eq_tail_reverse : @NonTail.reverse = @Tail.reverse := by
funext α xs
```

This results in a suitable goal:

```
unsolved goals
case h.h
α : Type u_1
xs : List α
⊢ NonTail.reverse xs = Tail.reverse xs
```

#### Factorial

Prove that `NonTail.factorial`

from the exercises in the previous section is equal to your tail-recursive solution by finding the relationship between the accumulator and the result and proving a suitable helper theorem.