8.4.1. 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. Behind the scenes, Lean uses this fact to prove that it terminates:

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

This splitting function is structurally recursive.

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:

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, and Lean is unable to automatically discover a decreasing measure:

fail to show termination for
  mergeSort
with errors
failed to infer structural recursion:
Not considering parameter α of mergeSort:
  it is unchanged in the recursive calls
Not considering parameter #2 of mergeSort:
  it is unchanged in the recursive calls
Cannot use parameter xs:
  failed to eliminate recursive application
    mergeSort halves.fst


Could not find a decreasing measure.
The basic measures relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
            xs #1
1) 70:11-31  ?  ?
2) 70:34-54  _  _

#1: xs.length

Please use `termination_by` to specify a decreasing measure.

The reason it terminates is that splitList always returns lists that are shorter than its input, at least when applied to lists that contain at least two elements. 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:

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_1xs:List αh:¬xs.length < 2halves:List α × List α := splitList xs⊢ (splitList xs).fst.length < xs.length

8.4.2. 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:

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

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:

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

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

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:

unsolved goals
consα:Type u_1x:αxs:List αih:(splitList xs).fst.length ≤ xs.length ∧ (splitList xs).snd.length ≤ xs.length⊢ (splitList xs).snd.length ≤ xs.length ∧ (splitList xs).fst.length ≤ xs.length + 1

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:

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:

unsolved goals
cons.introα:Type u_1x:αxs:List αleft✝:(splitList xs).fst.length ≤ xs.lengthright✝:(splitList xs).snd.length ≤ xs.length⊢ (splitList xs).snd.length ≤ xs.length ∧ (splitList xs).fst.length ≤ xs.length + 1

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:

unsolved goals
cons.intro.leftα:Type u_1x:αxs:List αleft✝:(splitList xs).fst.length ≤ xs.lengthright✝:(splitList xs).snd.length ≤ xs.length⊢ (splitList xs).snd.length ≤ xs.length

cons.intro.rightα:Type u_1x:αxs:List αleft✝:(splitList xs).fst.length ≤ xs.lengthright✝:(splitList xs).snd.length ≤ xs.length⊢ (splitList xs).fst.length ≤ xs.length + 1

The left goal is identical to the left✝ assumption, so the assumption tactic dispatches it:

unsolved goals
cons.intro.rightα:Type u_1x:αxs:List αleft✝:(splitList xs).fst.length ≤ xs.lengthright✝:(splitList xs).snd.length ≤ xs.length⊢ (splitList xs).fst.length ≤ xs.length + 1

The right goal resembles the right✝ assumption, except the goal adds a + 1 only to the length of the input list. It's time to prove that the inequality holds.

unsolved goals
n m:Nat⊢ n ≤ m → n ≤ m + 1

unsolved goals
n m:Nath:n ≤ m⊢ n ≤ m + 1

unsolved goals
refln m:Nat⊢ n ≤ n + 1

unsolved goals
stepn m m✝:Nata✝:n.le m✝ih:n ≤ m✝ + 1⊢ n ≤ m✝.succ + 1