Simple Termination Argument for Quicksort?

Stream: new members

[Agnishom Chattopadhyay]

I am trying to learn Lean4's functional programming capabilities by writing some simple programs.

How do I complete this definition for Quicksort?

-- write a simple quicksort function
def quicksort : List Nat → List Nat
  | [] => []
  | x :: xs =>
      quicksort (xs.filter (· < x))
      ++ [x] ++
      quicksort (xs.filter (· ≥ x))
  termination_by
    quicksort xs => xs.length
  decreasing_by
    sorry

#eval quicksort [3, 4, 2, 1]
-- prints [1, 2, 3, 4]

[Martin Dvořák]

import Mathlib.Data.List.Basic

def quicksort : List Nat → List Nat
  | [] => []
  | x :: xs =>
      quicksort (xs.filter (· < x))
      ++ [x] ++
      quicksort (xs.filter (· ≥ x))
  termination_by
    quicksort xs => xs.length
  decreasing_by
    simp_wf
    rw [Nat.lt_succ]
    apply List.length_filter_le

[Agnishom Chattopadhyay]

Thanks! I have some follow up questions.

• When I put my cursor after the decreasing_by, I do not see any goals. Why is that?
• After I write simp_wf, I see two goals. Which goal do the subsequent tactics apply to?
• Why doesn't writing apply? or exact? after simp_wf give me any helpful suggestions?

[Martin Dvořák]

I had similar questions recently:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unfocus.20goal.20after.60decreasing_by.60

[Agnishom Chattopadhyay]

Oh, interesting. Thanks!

Now, I have

def quicksort : List Nat → List Nat
  | [] => []
  | x :: xs =>
      (
      have : List.length (xs.filter (· < x)) < List.length (x :: xs) := by {
        simp [List.length]
        apply Nat.lt_succ_of_le
        apply List.length_filter_le
      }
      quicksort (xs.filter (· < x))
      )
      ++ [x] ++
      (
      have : List.length (xs.filter (· ≥ x)) < List.length (x :: xs) := by {
        simp [List.length]
        apply Nat.lt_succ_of_le
        apply List.length_filter_le
      }
      quicksort (xs.filter (· ≥ x))
      )
  termination_by
    quicksort xs => xs.length
  decreasing_by
    simp_wf
    simp_all

But I have no idea what is happening here.

• Why can't I see the goals that are created by decreasing_by?
• Does decreasing_by have to be followed by simp_wf? Is simp_wf a tactic?
• How do I select the individual goals after simp_wf?
• What is the meaning of the term (have : ... := ...; x)? Is it the same thing as x? What type does it have?

[Alex J. Best]

simp_wf is a tactic, you should be able to right click it and jump to its definition to see what its implementation is (its not that complicated iirc, just simp with some extra lemmas thrown in that make it useful for well foundedness proofs).

[Alex J. Best]

You don't have to use simp_wf after decreasing by, but probably 90% of the time it does something useful.

[Alex J. Best]

#check (have a : True := trivial; 1) shows you what the have statement elaborates to. It should be definitionally equal to just x in your example but it is not literally x.

[Alex J. Best]

If I put my cursor on the simp_wf in your big example I can see two goals, so I don't understand your first question

[Martin Dvořák]

Alex J. Best said:

#check (have a : True := trivial; 1) shows you what the have statement elaborates to. It should be definitionally equal to just x in your example but it is not literally x.

I think the problem is, if instead of have you want to prove termination after the decreasing_by keyword, both goals are focused. And I don't know how to focus only one of them. As a result, many tools don't work for me the way they should.

[Alex J. Best]

Yeah as you may have noticed that thing isn't really a normal goal state with a by block, whatever tactic you add there is used to fill all decreasing proofs and the state for all needed proofs is displayed in that one spot.
So you probably have to use things like first | tac1 | tac2 to be more flexible if the proofs are complicated

[Alex J. Best]

Thats why most of the time its better to put the proofs as have statements in the term

[Agnishom Chattopadhyay]

Alex J. Best said:

If I put my cursor on the simp_wf in your big example I can see two goals, so I don't understand your first question

Yes, but the goals are only seen _after_ running simp_wf. How do I know what the goal was _before_ running simp_wf?

[Agnishom Chattopadhyay]

Alex J. Best said:

#check (have a : True := trivial; 1) shows you what the have statement elaborates to. It should be definitionally equal to just x in your example but it is not literally x.

That's interesting. I saw that have a : x = y; bis syntactic sugar for (fun a => b) y. I am not really sure how this lets you feed in y into the proofs later though

[Agnishom Chattopadhyay]

Martin Dvořák said:

I think the problem is, if instead of have you want to prove termination after the decreasing_by keyword, both goals are focused. And I don't know how to focus only one of them. As a result, many tools don't work for me the way they should.

Yes, exactly. I do not really understand how to focus on individual goals in this situation. With Coq, I would have used - or { but I do not know what is the analogue for that in Lean

[Alex J. Best]

For normal proofs you can use . or \. to focus a goal, but a decreasing_by block is unfortunately not really a normal proof. I'd recommend proving as much as possible inline in the description of the algorithm, using List.length (xs.filter (· ≥ x)) < List.length (x :: xs) etc where you can use focussing like normal

[Alex J. Best]

Agnishom Chattopadhyay said:

Alex J. Best said:

If I put my cursor on the simp_wf in your big example I can see two goals, so I don't understand your first question

Yes, but the goals are only seen _after_ running simp_wf. How do I know what the goal was _before_ running simp_wf?

If I put my cursor before the s in simp_nf I see the goal before, if I put it after I see the goal after, there is even red/green highlighting to show what changed, in this case basically the whole goal

[Agnishom Chattopadhyay]

Thanks, the goal before the simp_wf now seems to be visible

[Agnishom Chattopadhyay]

How do I complete this argument?

def gcd : Nat → Nat → Nat
  | 0, y => y
  | x, 0 => x
  | x, y =>
    if x > y
    then (have : x - y < x := by {
      sorry -- can't see the hypotheses x > y and x ≠ 0
      } ;
      gcd (x - y) y)
    else (have : y - x < y := sorry; gcd x (y - x))
  termination_by
    gcd x y => x + y
  decreasing_by
    simp_wf
    simp_all

The hypotheses x > y and x <> 0 seem to be missing from the context

[Alex J. Best]

You can do if h : x > y. In this case x > y is enough to prove x \ne 0 also so that shouldn't be needed

[Agnishom Chattopadhyay]

Seems like linarith is not able to resolve this goal

| x, y =>
    if h : x > y
    then (have : x - y < x := by {
      linarith
      } ;
      gcd (x - y) y)
    else (have : y - x < y := sorry; gcd x (y - x))

[Alex J. Best]

If its an inequality about nats, then you probably need to be more careful with subtraction.
try zify [h] as a first step maybe

[Agnishom Chattopadhyay]

I think we need the hypothesis y <> 0. If y = 0, then we would have x - y = x

[Alex J. Best]

Probably the simplest solution is to write it as | (x + 1), (y+ 1) => ... then