2
$\begingroup$

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

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.

$\endgroup$

1 Answer 1

2
$\begingroup$

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))
$\endgroup$
6
  • $\begingroup$ Using List.length feels much more natural, thanks! But termination_by l => List.length l produces the error message function 'l' not found in current declaration. I don't know why :-/ And if I try termination_by _ => List.length then, after all_goals simp_wf the goal is changed to False. $\endgroup$ Commented Feb 5 at 7:43
  • $\begingroup$ @Matematiflo I think there is some misunderstanding. I gave you complete code which I tested in Lean. It uses a more idiomatic style IMHO too. Does this code not work in your version of Lean? (Indentation matters here. Lean 4 is white space sensitive like Python.) If so what version is it? Also termination_by should not go inside the decreasing_by proof. $\endgroup$
    – Jason Rute
    Commented Feb 5 at 10:56
  • $\begingroup$ @Matematiflo I think I now understand your confusion. See my edited answer. $\endgroup$
    – Jason Rute
    Commented Feb 5 at 12:29
  • $\begingroup$ Thanks @Jason-Rute. Indeed, there must be a problem with the version of Lean 4 that I am using (leanprover/lean4:v4.5.0 in my lean-toolchain file) because when I type in your code (which indeed works if I test it on live.lean-lang.org), after termination_by L.length, I get unexpected end of input; expected '=>'. I'll investigate further and report back here when I solve the issue or if I end up not being able to. Maybe I just need to use a more recent release of Lean. $\endgroup$ Commented Feb 5 at 14:06
  • 1
    $\begingroup$ @Matematiflo Oh, indeed it looks like termination_by syntax was changed in Lean 4.6 (release notes), which is still a release candidate. I'm going to leave my answer remain since it is going to be the correct answer soon, but if you look at that release note, you can see the 4.5 syntax, which requires one to also supply the function name in termination_by. (In 4.6, each function gets its own termination_by. Previously there was one termination_by for a declaration, like yours which defines 3 functions simultaneously.) $\endgroup$
    – Jason Rute
    Commented Feb 5 at 14:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.