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:

1. If one of the input lists is empty, then the result is the other list.
2. 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 \)