CODEWITHSUNDEEP
algorithmmergesortlean
Kjell
Kjell

Reputation: 432

Lean Mergesort using increasing well founded relation

I am trying to create the mergesort definition in Lean and have created the following code:

def mergesort (a: ℕ): list ℕ → list ℕ     
    | [] := []    
    | [a] := [a]  
    | (x::xs) :=  merge (mergesort (fhalf xs)) (mergesort (sndhalf xs))

With the merge definition

def merge : list ℕ → list ℕ → list ℕ    
    | xs [] := xs    
    | [] ys := ys
    | (x :: xs) (y :: ys) := if x < y then x :: (merge xs ( y :: ys)) 
                                      else y :: (merge (x :: xs) ys)

And fhalf / sndhalf definitions:

 def fhalf {α: Type} (xs: list α): list α := 
    list.take (list.length xs/2) xs

def sndhalf {α: Type} (xs: list α): list α :=
    list.drop (list.length xs/2) xs

However, I get the following error message:

failed to prove recursive application is decreasing, well founded relation 

@has_well_founded.r (list ℕ)
(@has_well_founded_of_has_sizeof (list ℕ) (@list.has_sizeof ℕ nat.has_sizeof))

Possible solutions:

  • Use using_well_founded keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.

  • The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions. The nested exception contains the failure state for the decreasing tactic.

Can anyone help me to prove that the mergesort is decreasing?

Upvotes: 3

Views: 478

Answers (1)

user7396200
user7396200

Reputation: 561

First, notice that there are multiple problems with your definition of mergesort. One, the parameter a is unnecessary and never used. (The a that you match in the second line is fresh.) Two, in the x::xs case, you forget about x entirely. To see what your function is actually doing, you can add the keyword meta, as in meta def mergesort. This disables termination checking, so then you can #eval mergesort 2 [1, 3, 2] and see that you do not get what you want. I'll continue to answer this as you've written it.

There is a default well-founded relation, and the default method for proving it is to look for proofs in the local context. You can see what proofs Lean is expecting by looking at the error messages in your definition: it wants proofs of list.sizeof (fhalf xs) < x + (1 + list.sizeof xs) and list.sizeof (sndhalf xs) < x + (1 + list.sizeof xs). So by adding lines

def mergesort (a : ℕ): list ℕ → list ℕ     
| [] := []    
| [a] := [a]  
| (x::xs) := 
  have list.sizeof (fhalf xs) < x + (1 + list.sizeof xs), from sorry,
  have list.sizeof (sndhalf xs) < x + (1 + list.sizeof xs), from sorry,
  merge (mergesort (fhalf xs)) (mergesort (sndhalf xs))

this strategy will succeed. You need to fill in those sorrys.

Using the linarith tactic available in mathlib (via import tactic.linarith) you can skip some arithmetic:

def mergesort (a : ℕ): list ℕ → list ℕ     
| [] := []    
| [a] := [a]  
| (x::xs) := 
  have list.sizeof (fhalf xs) ≤ list.sizeof xs, from sorry,
  have list.sizeof (sndhalf xs) ≤ list.sizeof xs, from sorry,
  have list.sizeof (fhalf xs) < x + (1 + list.sizeof xs), by linarith,
  have list.sizeof (sndhalf xs) < x + (1 + list.sizeof xs), by linarith,
  merge (mergesort (fhalf xs)) (mergesort (sndhalf xs))

So replace those sorrys with proofs, and you're good to go. You probably want to prove something like

lemma sizeof_take_le {α} [h : has_sizeof α] : ∀ n (xs : list α), 
  list.sizeof (list.take n xs) ≤ list.sizeof xs

The details will change a little when you correct your definition of mergesort.

An alternative approach is to change the well founded relation and decision tactic, as is done in the mathlib definition: https://github.com/leanprover/mathlib/blob/master/data/list/sort.lean#L174 Unfortunately, the interface for doing this is rather low-level and I don't know if or where it's documented.

To change the relation without using_well_founded, you could add a local instance that says to use list.length instead of list.sizeof:

def new_list_sizeof : has_sizeof (list ℕ) := ⟨list.length⟩
local attribute [instance, priority 100000] new_list_sizeof

The goals that this produces will be easier for you to prove than those using sizeof.

Upvotes: 4

Related Questions