# More Inequalities

Lean's built-in proof automation is sufficient to check that `arrayMapHelper`

and `findHelper`

terminate.
All that was needed was to provide an expression whose value decreases with each recursive call.
However, Lean's built-in automation is not magic, and it often needs some help.

## Merge Sort

One example of a function whose termination proof is non-trivial is merge sort on `List`

.
Merge sort consists of two phases: first, a list is split in half.
Each half is sorted using merge sort, and then the results are merged using a function that combines two sorted lists into a larger sorted list.
The base cases are the empty list and the singleton list, both of which are already considered to be sorted.

To merge two sorted lists, there are two basic cases to consider:

- If one of the input lists is empty, then the result is the other list.
- If both lists are non-empty, then their heads should be compared. The result of the function is the smaller of the two heads, followed by the result of merging the remaining entries of both lists.

This is not structurally recursive on either list.
The recursion terminates because an entry is removed from one of the two lists in each recursive call, but it could be either list.
The `termination_by`

clause uses the sum of the length of both lists as a decreasing value:

```
def merge [Ord α] (xs : List α) (ys : List α) : List α :=
match xs, ys with
| [], _ => ys
| _, [] => xs
| x'::xs', y'::ys' =>
match Ord.compare x' y' with
| .lt | .eq => x' :: merge xs' (y' :: ys')
| .gt => y' :: merge (x'::xs') ys'
termination_by merge xs ys => xs.length + ys.length
```

In addition to using the lengths of the lists, a pair that contains both lists can also be provided:

```
def merge [Ord α] (xs : List α) (ys : List α) : List α :=
match xs, ys with
| [], _ => ys
| _, [] => xs
| x'::xs', y'::ys' =>
match Ord.compare x' y' with
| .lt | .eq => x' :: merge xs' (y' :: ys')
| .gt => y' :: merge (x'::xs') ys'
termination_by merge xs ys => (xs, ys)
```

This works because Lean has a built-in notion of sizes of data, expressed through a type class called `WellFoundedRelation`

.
The instance for pairs automatically considers them to be smaller if either the first or the second item in the pair shrinks.

A simple way to split a list is to add each entry in the input list to two alternating output lists:

```
def splitList (lst : List α) : (List α × List α) :=
match lst with
| [] => ([], [])
| x :: xs =>
let (a, b) := splitList xs
(x :: b, a)
```

Merge sort checks whether a base case has been reached. If so, it returns the input list. If not, it splits the input, and merges the result of sorting each half:

```
def mergeSort [Ord α] (xs : List α) : List α :=
if h : xs.length < 2 then
match xs with
| [] => []
| [x] => [x]
else
let halves := splitList xs
merge (mergeSort halves.fst) (mergeSort halves.snd)
```

Lean's pattern match compiler is able to tell that the assumption `h`

introduced by the `if`

that tests whether `xs.length < 2`

rules out lists longer than one entry, so there is no "missing cases" error.
However, even though this program always terminates, it is not structurally recursive:

```
fail to show termination for
mergeSort
with errors
argument #3 was not used for structural recursion
failed to eliminate recursive application
mergeSort halves.fst
structural recursion cannot be used
failed to prove termination, use `termination_by` to specify a well-founded relation
```

The reason it terminates is that `splitList`

always returns lists that are shorter than its input.
Thus, the length of `halves.fst`

and `halves.snd`

are less than the length of `xs`

.
This can be expressed using a `termination_by`

clause:

```
def mergeSort [Ord α] (xs : List α) : List α :=
if h : xs.length < 2 then
match xs with
| [] => []
| [x] => [x]
else
let halves := splitList xs
merge (mergeSort halves.fst) (mergeSort halves.snd)
termination_by mergeSort xs => xs.length
```

With this clause, the error message changes.
Instead of complaining that the function isn't structurally recursive, Lean instead points out that it was unable to automatically prove that `(splitList xs).fst.length < xs.length`

:

```
failed to prove termination, possible solutions:
- Use `have`-expressions to prove the remaining goals
- Use `termination_by` to specify a different well-founded relation
- Use `decreasing_by` to specify your own tactic for discharging this kind of goal
α : Type u_1
xs : List α
h : ¬List.length xs < 2
halves : List α × List α := splitList xs
⊢ List.length (splitList xs).fst < List.length xs
```

## Splitting a List Makes it Shorter

It will also be necessary to prove that `(splitList xs).snd.length < xs.length`

.
Because `splitList`

alternates between adding entries to the two lists, it is easiest to prove both statements at once, so the structure of the proof can follow the algorithm used to implement `splitList`

.
In other words, it is easiest to prove that `∀(lst : List), (splitList lst).fst.length < lst.length ∧ (splitList lst).snd.length < lst.length`

.

Unfortunately, the statement is false.
In particular, `splitList []`

is `([], [])`

. Both output lists have length `0`

, which is not less than `0`

, the length of the input list.
Similarly, `splitList ["basalt"]`

evaluates to `(["basalt"], [])`

, and `["basalt"]`

is not shorter than `["basalt"]`

.
However, `splitList ["basalt", "granite"]`

evaluates to `(["basalt"], ["granite"])`

, and both of these output lists are shorter than the input list.

It turns out that the lengths of the output lists are always less than or equal to the length of the input list, but they are only strictly shorter when the input list contains at least two entries. It turns out to be easiest to prove the former statement, then extend it to the latter statement. Begin with a theorem statement:

```
theorem splitList_shorter_le (lst : List α) :
(splitList lst).fst.length ≤ lst.length ∧
(splitList lst).snd.length ≤ lst.length := by
skip
```

```
unsolved goals
α : Type u_1
lst : List α
⊢ List.length (splitList lst).fst ≤ List.length lst ∧ List.length (splitList lst).snd ≤ List.length lst
```

Because `splitList`

is structurally recursive on the list, the proof should use induction.
The structural recursion in `splitList`

fits a proof by induction perfectly: the base case of the induction matches the base case of the recursion, and the inductive step matches the recursive call.
The `induction`

tactic gives two goals:

```
theorem splitList_shorter_le (lst : List α) :
(splitList lst).fst.length ≤ lst.length ∧
(splitList lst).snd.length ≤ lst.length := by
induction lst with
| nil => skip
| cons x xs ih => skip
```

```
unsolved goals
case nil
α : Type u_1
⊢ List.length (splitList []).fst ≤ List.length [] ∧ List.length (splitList []).snd ≤ List.length []
```

```
unsolved goals
case cons
α : Type u_1
x : α
xs : List α
ih : List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList (x :: xs)).fst ≤ List.length (x :: xs) ∧
List.length (splitList (x :: xs)).snd ≤ List.length (x :: xs)
```

The goal for the `nil`

case can be proved by invoking the simplifier and instructing it to unfold the definition of `splitList`

, because the length of the empty list is less than or equal to the length of the empty list.
Similarly, simplifying with `splitList`

in the `cons`

case places `Nat.succ`

around the lengths in the goal:

```
theorem splitList_shorter_le (lst : List α) :
(splitList lst).fst.length ≤ lst.length ∧
(splitList lst).snd.length ≤ lst.length := by
induction lst with
| nil => simp [splitList]
| cons x xs ih =>
simp [splitList]
```

```
unsolved goals
case cons
α : Type u_1
x : α
xs : List α
ih : List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs) ∧
List.length (splitList xs).fst ≤ Nat.succ (List.length xs)
```

This is because the call to `List.length`

consumes the head of the list `x :: xs`

, converting it to a `Nat.succ`

, in both the length of the input list and the length of the first output list.

Writing `A ∧ B`

in Lean is short for `And A B`

.
`And`

is a structure type in the `Prop`

universe:

```
structure And (a b : Prop) : Prop where
intro ::
left : a
right : b
```

In other words, a proof of `A ∧ B`

consists of the `And.intro`

constructor applied to a proof of `A`

in the `left`

field and a proof of `B`

in the `right`

field.

The `cases`

tactic allows a proof to consider each constructor of a datatype or each potential proof of a proposition in turn.
It corresponds to a `match`

expression without recursion.
Using `cases`

on a structure results in the structure being broken apart, with an assumption added for each field of the structure, just as a pattern match expression extracts the field of a structure for use in a program.
Because structures have only one constructor, using `cases`

on a structure does not result in additional goals.

Because `ih`

is a proof of `List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs`

, using `cases ih`

results in an assumption that `List.length (splitList xs).fst ≤ List.length xs`

and an assumption that `List.length (splitList xs).snd ≤ List.length xs`

:

```
theorem splitList_shorter_le (lst : List α) :
(splitList lst).fst.length ≤ lst.length ∧
(splitList lst).snd.length ≤ lst.length := by
induction lst with
| nil => simp [splitList]
| cons x xs ih =>
simp [splitList]
cases ih
```

```
unsolved goals
case cons.intro
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs) ∧
List.length (splitList xs).fst ≤ Nat.succ (List.length xs)
```

Because the goal of the proof is also an `And`

, the `constructor`

tactic can be used to apply `And.intro`

, resulting in a goal for each argument:

```
theorem splitList_shorter_le (lst : List α) :
(splitList lst).fst.length ≤ lst.length ∧
(splitList lst).snd.length ≤ lst.length := by
induction lst with
| nil => simp [splitList]
| cons x xs ih =>
simp [splitList]
cases ih
constructor
```

```
unsolved goals
case cons.intro.left
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs)
case cons.intro.right
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ Nat.succ (List.length xs)
```

The `left`

goal is very similar to the `left✝`

assumption, except the goal wraps both sides of the inequality in `Nat.succ`

.
Likewise, the `right`

goal resembles the `right✝`

assumption, except the goal adds a `Nat.succ`

only to the length of the input list.
It's time to prove that these wrappings of `Nat.succ`

preserve the truth of the statement.

### Adding One to Both Sides

For the `left`

goal, the statement to prove is `Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m`

.
In other words, if `n ≤ m`

, then adding one to both sides doesn't change this fact.
Why is this true?
The proof that `n ≤ m`

is a `Nat.le.refl`

constructor with `m - n`

instances of the `Nat.le.step`

constructor wrapped around it.
Adding one to both sides simply means that the `refl`

applies to a number that's one larger than before, with the same number of `step`

constructors.

More formally, the proof is by induction on the evidence that `n ≤ m`

.
If the evidence is `refl`

, then `n = m`

, so `Nat.succ n = Nat.succ m`

and `refl`

can be used again.
If the evidence is `step`

, then the induction hypothesis provides evidence that `Nat.succ n ≤ Nat.succ m`

, and the goal is to show that `Nat.succ n ≤ Nat.succ (Nat.succ m)`

.
This can be done by using `step`

together with the induction hypothesis.

In Lean, the theorem statement is:

```
theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m := by
skip
```

and the error message recapitulates it:

```
unsolved goals
n m : Nat
⊢ n ≤ m → Nat.succ n ≤ Nat.succ m
```

The first step is to use the `intro`

tactic, bringing the hypothesis that `n ≤ m`

into scope and giving it a name:

```
theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m := by
intro h
```

```
unsolved goals
n m : Nat
h : n ≤ m
⊢ Nat.succ n ≤ Nat.succ m
```

Because the proof is by induction on the evidence that `n ≤ m`

, the next tactic is `induction h`

:

```
theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m := by
intro h
induction h
```

This results in two goals, once for each constructor of `Nat.le`

:

```
unsolved goals
case refl
n m : Nat
⊢ Nat.succ n ≤ Nat.succ n
case step
n m m✝ : Nat
a✝ : Nat.le n m✝
a_ih✝ : Nat.succ n ≤ Nat.succ m✝
⊢ Nat.succ n ≤ Nat.succ (Nat.succ m✝)
```

The goal for `refl`

can itself be solved using `refl`

, which the `constructor`

tactic selects.
The goal for `step`

will also require a use of the `step`

constructor:

```
theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m := by
intro h
induction h with
| refl => constructor
| step h' ih => constructor
```

```
unsolved goals
case step.a
n m m✝ : Nat
h' : Nat.le n m✝
ih : Nat.succ n ≤ Nat.succ m✝
⊢ Nat.le (Nat.succ n) (m✝ + 1)
```

The goal is no longer shown using the `≤`

operator, but it is equivalent to the induction hypothesis `ih`

.
The `assumption`

tactic automatically selects an assumption that fulfills the goal, and the proof is complete:

```
theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m := by
intro h
induction h with
| refl => constructor
| step h' ih =>
constructor
assumption
```

Written as a recursive function, the proof is:

```
theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m
| .refl => .refl
| .step h' => .step (Nat.succ_le_succ h')
```

It can be instructional to compare the tactic-based proof by induction with this recursive function. Which proof steps correspond to which parts of the definition?

### Adding One to the Greater Side

The second inequality needed to prove `splitList_shorter_le`

is `∀(n m : Nat), n ≤ m → n ≤ Nat.succ m`

.
This proof is almost identical to `Nat.succ_le_succ`

.
Once again, the incoming assumption that `n ≤ m`

essentially tracks the difference between `n`

and `m`

in the number of `Nat.le.step`

constructors.
Thus, the proof should add an extra `Nat.le.step`

in the base case.
The proof can be written:

```
theorem Nat.le_succ_of_le : n ≤ m → n ≤ Nat.succ m := by
intro h
induction h with
| refl => constructor; constructor
| step => constructor; assumption
```

To reveal what's going on behind the scenes, the `apply`

and `exact`

tactics can be used to indicate exactly which constructor is being applied.
The `apply`

tactic solves the current goal by applying a function or constructor whose return type matches, creating new goals for each argument that was not provided, while `exact`

fails if any new goals would be needed:

```
theorem Nat.le_succ_of_le : n ≤ m → n ≤ Nat.succ m := by
intro h
induction h with
| refl => apply Nat.le.step; exact Nat.le.refl
| step _ ih => apply Nat.le.step; exact ih
```

The proof can be golfed:

```
theorem Nat.le_succ_of_le (h : n ≤ m) : n ≤ Nat.succ m := by
induction h <;> repeat (first | constructor | assumption)
```

In this short tactic script, both goals introduced by `induction`

are addressed using `repeat (first | constructor | assumption)`

.
The tactic `first | T1 | T2 | ... | Tn`

means to use try `T1`

through `Tn`

in order, using the first tactic that succeeds.
In other words, `repeat (first | constructor | assumption)`

applies constructors as long as it can, and then attempts to solve the goal using an assumption.

Finally, the proof can be written as a recursive function:

```
theorem Nat.le_succ_of_le : n ≤ m → n ≤ Nat.succ m
| .refl => .step .refl
| .step h => .step (Nat.le_succ_of_le h)
```

Each style of proof can be appropriate to different circumstances. The detailed proof script is useful in cases where beginners may be reading the code, or where the steps of the proof provide some kind of insight. The short, highly-automated proof script is typically easier to maintain, because automation is frequently both flexible and robust in the face of small changes to definitions and datatypes. The recursive function is typically both harder to understand from the perspective of mathematical proofs and harder to maintain, but it can be a useful bridge for programmers who are beginning to work with interactive theorem proving.

### Finishing the Proof

Now that both helper theorems have been proved, the rest of `splitList_shorter_le`

will be completed quickly.
The current proof state has two goals, for the left and right sides of the `And`

:

```
unsolved goals
case cons.intro.left
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs)
case cons.intro.right
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ Nat.succ (List.length xs)
```

The goals are named for the fields of the `And`

structure. This means that the `case`

tactic (not to be confused with `cases`

) can be used to focus on each of them in turn:

```
theorem splitList_shorter_le (lst : List α) :
(splitList lst).fst.length ≤ lst.length ∧ (splitList lst).snd.length ≤ lst.length := by
induction lst with
| nil => simp [splitList]
| cons x xs ih =>
simp [splitList]
cases ih
constructor
case left => skip
case right => skip
```

Instead of a single error that lists both unsolved goals, there are now two messages, one on each `skip`

.
For the `left`

goal, `Nat.succ_le_succ`

can be used:

```
unsolved goals
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs)
```

In the right goal, `Nat.le_suc_of_le`

fits:

```
unsolved goals
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ Nat.succ (List.length xs)
```

Both theorems include the precondition that `n ≤ m`

.
These can be found as the `left✝`

and `right✝`

assumptions, which means that the `assumption`

tactic takes care of the final goals:

```
theorem splitList_shorter_le (lst : List α) :
(splitList lst).fst.length ≤ lst.length ∧ (splitList lst).snd.length ≤ lst.length := by
induction lst with
| nil => simp [splitList]
| cons x xs ih =>
simp [splitList]
cases ih
constructor
case left => apply Nat.succ_le_succ; assumption
case right => apply Nat.le_succ_of_le; assumption
```

The next step is to return to the actual theorem that is needed to prove that merge sort terminates: that so long as a list has at least two entries, both results of splitting it are strictly shorter.

```
theorem splitList_shorter (lst : List α) (_ : lst.length ≥ 2) :
(splitList lst).fst.length < lst.length ∧
(splitList lst).snd.length < lst.length := by
skip
```

```
unsolved goals
α : Type u_1
lst : List α
x✝ : List.length lst ≥ 2
⊢ List.length (splitList lst).fst < List.length lst ∧ List.length (splitList lst).snd < List.length lst
```

Pattern matching works just as well in tactic scripts as it does in programs.
Because `lst`

has at least two entries, they can be exposed with `match`

, which also refines the type through dependent pattern matching:

```
theorem splitList_shorter (lst : List α) (_ : lst.length ≥ 2) :
(splitList lst).fst.length < lst.length ∧
(splitList lst).snd.length < lst.length := by
match lst with
| x :: y :: xs =>
skip
```

```
unsolved goals
α : Type u_1
lst : List α
x y : α
xs : List α
x✝ : List.length (x :: y :: xs) ≥ 2
⊢ List.length (splitList (x :: y :: xs)).fst < List.length (x :: y :: xs) ∧
List.length (splitList (x :: y :: xs)).snd < List.length (x :: y :: xs)
```

Simplifying using `splitList`

removes `x`

and `y`

, resulting in the computed lengths of lists each gaining a `Nat.succ`

:

```
theorem splitList_shorter (lst : List α) (_ : lst.length ≥ 2) :
(splitList lst).fst.length < lst.length ∧
(splitList lst).snd.length < lst.length := by
match lst with
| x :: y :: xs =>
simp [splitList]
```

```
unsolved goals
α : Type u_1
lst : List α
x y : α
xs : List α
x✝ : List.length (x :: y :: xs) ≥ 2
⊢ Nat.succ (List.length (splitList xs).fst) < Nat.succ (Nat.succ (List.length xs)) ∧
Nat.succ (List.length (splitList xs).snd) < Nat.succ (Nat.succ (List.length xs))
```

Replacing `simp`

with `simp_arith`

removes these `Nat.succ`

constructors, because `simp_arith`

makes use of the fact that `n + 1 < m + 1`

implies `n < m`

:

```
theorem splitList_shorter (lst : List α) (_ : lst.length ≥ 2) :
(splitList lst).fst.length < lst.length ∧
(splitList lst).snd.length < lst.length := by
match lst with
| x :: y :: xs =>
simp_arith [splitList]
```

```
unsolved goals
α : Type u_1
lst : List α
x y : α
xs : List α
x✝ : List.length (x :: y :: xs) ≥ 2
⊢ List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs
```

This goal now matches `splitList_shorter_le`

, which can be used to conclude the proof:

```
theorem splitList_shorter (lst : List α) (_ : lst.length ≥ 2) :
(splitList lst).fst.length < lst.length ∧
(splitList lst).snd.length < lst.length := by
match lst with
| x :: y :: xs =>
simp_arith [splitList]
apply splitList_shorter_le
```

The facts needed to prove that `mergeSort`

terminates can be pulled out of the resulting `And`

:

```
theorem splitList_shorter_fst (lst : List α) (h : lst.length ≥ 2) :
(splitList lst).fst.length < lst.length :=
splitList_shorter lst h |>.left
theorem splitList_shorter_snd (lst : List α) (h : lst.length ≥ 2) :
(splitList lst).snd.length < lst.length :=
splitList_shorter lst h |>.right
```

## Merge Sort Terminates

Merge sort has two recursive calls, one for each sub-list returned by `splitList`

.
Each recursive call will require a proof that the length of the list being passed to it is shorter than the length of the input list.
It's usually convenient to write a termination proof in two steps: first, write down the propositions that will allow Lean to verify termination, and then prove them.
Otherwise, it's possible to put a lot of effort into proving the propositions, only to find out that they aren't quite what's needed to establish that the recursive calls are on smaller inputs.

The `sorry`

tactic can prove any goal, even false ones.
It isn't intended for use in production code or final proofs, but it is a convenient way to "sketch out" a proof or program ahead of time.
Any definitions or theorems that use `sorry`

are annotated with a warning.

The initial sketch of `mergeSort`

's termination argument that uses `sorry`

can be written by copying the goals that Lean couldn't prove into `have`

-expressions.
In Lean, `have`

is similar to `let`

.
When using `have`

, the name is optional.
Typically, `let`

is used to define names that refer to interesting values, while `have`

is used to locally prove propositions that can be found when Lean is searching for evidence that an array lookup is in-bounds or that a function terminates.

```
def mergeSort [Ord α] (xs : List α) : List α :=
if h : xs.length < 2 then
match xs with
| [] => []
| [x] => [x]
else
let halves := splitList xs
have : halves.fst.length < xs.length := by
sorry
have : halves.snd.length < xs.length := by
sorry
merge (mergeSort halves.fst) (mergeSort halves.snd)
termination_by mergeSort xs => xs.length
```

The warning is located on the name `mergeSort`

:

```
declaration uses 'sorry'
```

Because there are no errors, the proposed propositions are enough to establish termination.

The proofs begin by applying the helper theorems:

```
def mergeSort [Ord α] (xs : List α) : List α :=
if h : xs.length < 2 then
match xs with
| [] => []
| [x] => [x]
else
let halves := splitList xs
have : halves.fst.length < xs.length := by
apply splitList_shorter_fst
have : halves.snd.length < xs.length := by
apply splitList_shorter_snd
merge (mergeSort halves.fst) (mergeSort halves.snd)
termination_by mergeSort xs => xs.length
```

Both proofs fail, because `splitList_shorter_fst`

and `splitList_shorter_snd`

both require a proof that `xs.length ≥ 2`

:

```
unsolved goals
case h
α : Type ?u.37732
inst✝ : Ord α
xs : List α
h : ¬List.length xs < 2
halves : List α × List α := splitList xs
⊢ List.length xs ≥ 2
```

To check that this will be enough to complete the proof, add it using `sorry`

and check for errors:

```
def mergeSort [Ord α] (xs : List α) : List α :=
if h : xs.length < 2 then
match xs with
| [] => []
| [x] => [x]
else
let halves := splitList xs
have : xs.length ≥ 2 := by sorry
have : halves.fst.length < xs.length := by
apply splitList_shorter_fst
assumption
have : halves.snd.length < xs.length := by
apply splitList_shorter_snd
assumption
merge (mergeSort halves.fst) (mergeSort halves.snd)
termination_by mergeSort xs => xs.length
```

Once again, there is only a warning.

```
declaration uses 'sorry'
```

There is one promising assumption available: `h : ¬List.length xs < 2`

, which comes from the `if`

.
Clearly, if it is not the case that `xs.length < 2`

, then `xs.length ≥ 2`

.
The Lean library provides this theorem under the name `Nat.ge_of_not_lt`

.
The program is now complete:

```
def mergeSort [Ord α] (xs : List α) : List α :=
if h : xs.length < 2 then
match xs with
| [] => []
| [x] => [x]
else
let halves := splitList xs
have : xs.length ≥ 2 := by
apply Nat.ge_of_not_lt
assumption
have : halves.fst.length < xs.length := by
apply splitList_shorter_fst
assumption
have : halves.snd.length < xs.length := by
apply splitList_shorter_snd
assumption
merge (mergeSort halves.fst) (mergeSort halves.snd)
termination_by mergeSort xs => xs.length
```

The function can be tested on examples:

```
#eval mergeSort ["soapstone", "geode", "mica", "limestone"]
```

```
["geode", "limestone", "mica", "soapstone"]
```

```
#eval mergeSort [5, 3, 22, 15]
```

```
[3, 5, 15, 22]
```

## Division as Iterated Subtraction

Just as multiplication is iterated addition and exponentiation is iterated multiplication, division can be understood as iterated subtraction. The very first description of recursive functions in this book presents a version of division that terminates when the divisor is not zero, but that Lean does not accept. Proving that division terminates requires the use of a fact about inequalities.

The first step is to refine the definition of division so that it requires evidence that the divisor is not zero:

```
def div (n k : Nat) (ok : k > 0) : Nat :=
if n < k then
0
else
1 + div (n - k) k ok
```

The error message is somewhat longer, due to the additional argument, but it contains essentially the same information:

```
fail to show termination for
div
with errors
argument #1 was not used for structural recursion
failed to eliminate recursive application
div (n - k) k ok
argument #2 was not used for structural recursion
failed to eliminate recursive application
div (n - k) k ok
argument #3 was not used for structural recursion
application type mismatch
@Nat.le.brecOn (Nat.succ 0) fun k ok => Nat → Nat
argument
fun k ok => Nat → Nat
has type
(k : Nat) → k > 0 → Type : Type 1
but is expected to have type
(a : Nat) → Nat.le (Nat.succ 0) a → Prop : Type
structural recursion cannot be used
failed to prove termination, use `termination_by` to specify a well-founded relation
```

This definition of `div`

terminates because the first argument `n`

is smaller on each recursive call.
This can be expressed using a `termination_by`

clause:

```
def div (n k : Nat) (ok : k > 0) : Nat :=
if h : n < k then
0
else
1 + div (n - k) k ok
termination_by div n k ok => n
```

Now, the error is confined to the recursive call:

```
failed to prove termination, possible solutions:
- Use `have`-expressions to prove the remaining goals
- Use `termination_by` to specify a different well-founded relation
- Use `decreasing_by` to specify your own tactic for discharging this kind of goal
n k : Nat
ok : k > 0
h : ¬n < k
⊢ n - k < n
```

This can be proved using a theorem from the standard library, `Nat.sub_lt`

.
This theorem states that `∀ {n k : Nat}, 0 < n → 0 < k → n - k < n`

(the curly braces indicate that `n`

and `k`

are implicit arguments).
Using this theorem requires demonstrating that both `n`

and `k`

are greater than zero.
Because `k > 0`

is syntactic sugar for `0 < k`

, the only necessary goal is to show that `0 < n`

.
There are two possibilities: either `n`

is `0`

, or it is `n' + 1`

for some other `Nat`

`n'`

.
But `n`

cannot be `0`

.
The fact that the `if`

selected the second branch means that `¬ n < k`

, but if `n = 0`

and `k > 0`

then `n`

must be less than `k`

, which would be a contradiction.
This, `n = Nat.succ n'`

, and `Nat.succ n'`

is clearly greater than `0`

.

The full definition of `div`

, including the termination proof, is:

```
def div (n k : Nat) (ok : k > 0) : Nat :=
if h : n < k then
0
else
have : 0 < n := by
cases n with
| zero => contradiction
| succ n' => simp_arith
have : n - k < n := by
apply Nat.sub_lt <;> assumption
1 + div (n - k) k ok
termination_by div n k ok => n
```

## Exercises

Prove the following theorems:

- For all natural numbers \( n \), \( 0 < n + 1 \).
- For all natural numbers \( n \), \( 0 \leq n \).
- For all natural numbers \( n \) and \( k \), \( (n + 1) - (k + 1) = n - k \)
- For all natural numbers \( n \) and \( k \), if \( k < n \) then \( n \neq 0 \)
- For all natural numbers \( n \), \( n - n = 0 \)
- For all natural numbers \( n \) and \( k \), if \( n + 1 < k \) then \( n < k \)