Using `decreasing_by` to prove termination in Lean 4

Question

Warning: This was written for Lean v4.5.0. To make the accepted answer work, please use v4.6.0-rc1.

I would like to define an elementary quicksort function for lists in Lean 4. The following declaration can be used in computations but I want to fill the sorry:

def qsort (L : List Int) : List Int :=
  match L with
  | [] => []
  | x :: l => qsort (p1 x l) ++ [x] ++ qsort (p2 x l)
    where
      p1 (x : Int) (l : List Int) : List Int := (l.filter (· ≤ x))
      p2 (x : Int) (l : List Int) : List Int := (l.filter (· > x))
  decreasing_by {sorry}

#eval qsort [1, -3, 4, 5, 2]  -- [-3, 1, 2, 4, 5]

The tactic state that I see in the Lean infoview is the following:

2 goals

x: Int
l: List Int
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (qsort.p1 x l) (x :: l)

x: Int
l: List Int
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (qsort.p2 x l) (x :: l)

I think that, to prove that the recursion terminates, it should be enough to prove the following proposition:

List.length (qsort.p1 x l) < List.length (x::l) : Prop

and similarly for qsort.p2. So I would like the expression

invImage (fun a => sizeOf a) instWellFoundedRelation

that I see in the Lean infoview to be

invImage (List.length : List Int → Nat) Nat.lt_wfRel 

but I have not been able to make this appear in the goal. Indeed, this is a term of type WellFoundedRelation (List Int) whose first projection is the relation r L1 L2 defined by List.length L1 < List.length L2.

If I could make this appear in the goal, then I should to be able to conclude by proving the proposition List.length (qsort.p1 x l) < List.length (x::l).

I have looked at the answers to the following question

• How to prove the termination of Ackermann in Lean?

but I have not been able to use termination_by in my example, so I am trying to use decreasing_by instead, which has the effect of making Lean enter tactic mode and display a goal.

Answer 1

You can follow the examples in TPIL4 Chapter 8. (Edit: This answer is for the new syntax, which changed in Lean 4.6. See the 4.6 release notes for a comparison with the former syntax.) In particular:

• termination_by specifies what the decreasing value is.
  • By default is the built-in value sizeOf.
  • In this case it is better to go with length.
  • If the parameter, is to the right of the colon, then you supply a function—e.g. termination_by l => l.length, termination_by (fun x : List Int => x.length), or termination_by List.length.
  • If the parameter, L in this case, is to the left of the colon, then you just give the value in terms of L, e.g. termination_by L.length.
• decreasing_by is the proof that the value from termination_by is decreasing.
  • Use all_goals simp_wf to get rid of the boilerplate. (all_goals since you have multiple recursive calls).
  • After that, in this case, the proof is mostly just applying the lemma List.length_filter_le (found in Std).
• termination_by and decreasing_by go before where, else Lean applies them to the last auxiliary function p2.

import Std

def qsort : (L : List Int) -> (List Int)
| [] => []
| x :: l => qsort (p1 x l) ++ [x] ++ qsort (p2 x l)
termination_by l => l.length
decreasing_by
  all_goals simp_wf
  /-
  x : Int
  l : List Int
  ⊢ List.length (qsort.p1 x l) < Nat.succ (List.length l)
  
  x : Int
  l : List Int
  ⊢ List.length (qsort.p2 x l) < Nat.succ (List.length l)
  -/
  . calc
      (qsort.p1 x l).length ≤ l.length     := by unfold qsort.p1; simp [List.length_filter_le]
      _                     < l.length + 1 := by simp
  . calc
      (qsort.p2 x l).length ≤ l.length     := by unfold qsort.p2; simp [List.length_filter_le]
      _                     < l.length + 1 := by simp
where
  p1 (x : Int) (l : List Int) : List Int := (l.filter (· ≤ x))
  p2 (x : Int) (l : List Int) : List Int := (l.filter (· > x))

---

The form I wrote the recursive definition is equivalent to yours and probably more idiomatic. But if you go with your version where the parameter L is to the left of the colon, then termination_by would look different, as follows (no =>):

def qsort (L : List Int) : List Int :=
  match L with
  | [] => []
  | x :: l => qsort (p1 x l) ++ [x] ++ qsort (p2 x l)
termination_by L.length
decreasing_by
  all_goals simp_wf
  . sorry
  . sorry
where
  p1 (x : Int) (l : List Int) : List Int := (l.filter (· ≤ x))
  p2 (x : Int) (l : List Int) : List Int := (l.filter (· > x))