Termination of bubble sort

Stream: lean4

[Tomas Skrivan]

The thread on ackermann got me thinking how do I show termination of bubble sort?

Here is my unfinished attempt:

variable {α} [LT α] [∀ x y : α, Decidable (x < y)]

def List.sort : List α → List α
| [] => []
| x :: xs =>
  match (sort xs) with
  | [] => [x]
  | y :: ys =>
    if y < x then
      y :: sort (x :: ys)
    else
      x :: y :: ys
termination_by'
{
  rel := λ a b =>
    match Classical.propDecidable (a.1 = b.1) with
    | isTrue h => @List.lt _ a.2.1 a.2.2.2 (h ▸ b.2.2.2)  -- I need graded lexicographical ordering
    | isFalse h => False
  wf := sorry
}

I think the default inequality on List is not sufficient, as the bubble sort is decreasing first in length and then in lexicographical order. By default [5] < [1,2] is false but I need it to be true.

Also, what I'm confused about is that termination_by wants a relation between lists with different types and a ordering. Is it ok to declare Lists with different types or ordering as incomparable? How do I define such relation? I invoked classical reasoning, but I'm expecting that is not necessary as I'm eliminating to Prop.

[Gabriel Ebner]

I don't think lexicographic ordering will save you here, you know nothing about the ys returned by the recursive sort-call.

[Gabriel Ebner]

The easiest way is probably to bundle the invariant into a subtype:

def bubblesort (xs : List α) : { ys : List α // ys.length = xs.length } :=
  match xs with
  ...
termination_by => xs.size

(all of the recursive calls are on lists of smaller length)

[Gabriel Ebner]

With the new termination_by (new syntax as of today) you only need to specify a decreasing value (in some type that has WellFoundedRelation instance). No need to construct a well-founded relation explicitly, or to unbundle the function arguments.

[Tomas Skrivan]

So this should work with tomorrow nightly build?

def List.bubblesort (l : List α) : {l' : List α // l.length = l'.length} :=
match l with
| [] => ⟨[], rfl⟩
| x :: xs =>
  match (bubblesort xs) with
  | ⟨[], h⟩ => ⟨[x], by simp; rw[h]; simp done⟩
  | ⟨y :: ys, h⟩ =>
    if y < x then
      ⟨y :: (bubblesort (x :: ys)).1,
       by simp; rw[h]; simp;
          rw[← (bubblesort (x :: ys)).2]; simp; done⟩
    else
      ⟨x :: y :: ys, by simp; rw[h]; simp done⟩
termination_by => l.length

[Leonardo de Moura]

https://github.com/leanprover/lean4/commit/1620987b6ce40c98aaca78393e1ef15b261e6400