Zulip Chat Archive

Stream: lean4

Topic: Termination of bubble sort


Tomas Skrivan (Jan 13 2022 at 09:55):

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 (Jan 13 2022 at 10:34):

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

Gabriel Ebner (Jan 13 2022 at 10:36):

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 (Jan 13 2022 at 10:38):

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 (Jan 13 2022 at 11:25):

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 (Jan 13 2022 at 17:59):

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


Last updated: Dec 20 2023 at 11:08 UTC