Merge sort termination

Stream: general

[Mukesh Tiwari]

Hi everyone,

I am wondering how can I show the termination of mergeList function. (I understand that I need to turn 1 + sizeOf (xhs ++ yh :: yhs) into 2 + sizeOf (xhs ++ yhs) but I am lacking the knowledge of syntax and the required lemmas)

import Init.Data.List


section MergeSort
  universe u
  variable
    {A : Type u}
    (f : A -> A -> Bool)


  def splitList : Nat -> List A -> List A × List A :=
    fun n xs => (List.take n xs, List.drop n xs)

  def split : List A -> List A × List A :=
    fun xs => splitList (Nat.div (xs.length) 2) xs


  def mergeList : List A  -> List A -> List A
  | [], ys => ys
  | xs, [] => xs
  | (xh :: xhs), (yh :: yhs) =>
    match f xh yh with
    | true => xh :: mergeList xhs (yh :: yhs)
    | false => yh :: mergeList (xh :: xhs) yhs
  termination_by mergeList xs ys => xs ++ ys
  have
  /-
    How to show
    A : Type u
    xh : A
    xhs : List A
    yh : A
    yhs : List A
    ⊢ 1 + sizeOf (xhs ++ yhs) < 1 + sizeOf (xhs ++ yh :: yhs)

  -/

end MergeSort

[Mario Carneiro]

you want to use xs.length + ys.length as the termination measure, not xs ++ ys

[Mukesh Tiwari]

@Mario Carneiro Thanks! Given that the goal is provable, I am still curious about the proof using have or decreasing_by syntax.

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
A : Type u
xh : A
xhs : List A
yh : A
yhs : List A
⊢ 1 + sizeOf (xhs ++ yhs) < 1 + sizeOf (xhs ++ yh :: yhs)

[Mario Carneiro]

The goal there is more annoying because it relies on the sizeOf function for lists, which does not have many lemmas about it (because if the automatic proof method doesn't work then you should use something with more sensible proof principles like length instead)

[Mario Carneiro]

  theorem foo (xs ys : List A) : sizeOf (xs ++ a :: ys) = 1 + sizeOf a + sizeOf (xs ++ ys) := by
    induction xs <;> simp [*]

  def mergeList : List A  -> List A -> List A
  | [], ys => ys
  | xs, [] => xs
  | (xh :: xhs), (yh :: yhs) =>
    match f xh yh with
    | true => xh :: mergeList xhs (yh :: yhs)
    | false =>
      have : 1 + sizeOf (xhs ++ yhs) < 1 + sizeOf (xhs ++ yh :: yhs) := by
        simp [foo]; decreasing_trivial
      yh :: mergeList (xh :: xhs) yhs
  termination_by mergeList xs ys => xs ++ ys

[Mario Carneiro]

another termination metric which works here is lexicographic order:

  def mergeList : List A  -> List A -> List A
  | [], ys => ys
  | xs, [] => xs
  | (xh :: xhs), (yh :: yhs) =>
    match f xh yh with
    | true => xh :: mergeList xhs (yh :: yhs)
    | false => yh :: mergeList (xh :: xhs) yhs
  termination_by mergeList xs ys => (xs, ys)