defining a list merge function

Stream: new members

[Scott Kovach]

hi everyone, new Lean user here! I have some questions about this example:

def merge {α : Type} [linear_order α] : list α → list α → list α
| [] ys := ys
| xs [] := xs
| (x::xs) (y::ys) := if x ≤ y then x :: merge xs (y::ys) else y :: merge (x::xs) ys

--#reduce merge [1,3] [2]

example {α : Type} [linear_order α] (l₂ : list α) : l₂ = merge list.nil l₂ :=
begin cases l₂, refl, simp [merge],
end
example {α : Type} (l₂ : list α) : l₂ = append list.nil l₂ := begin refl end

1: is there something wrong with the way I've defined merge? the reduce command times out, although #eval works
2: I had the mental model that definitions would be normalized away inside proofs, so I was expecting refl to prove the first example. is there a way for me to see why it works for append but simp is required for merge? why does that proof require an initial case split?

[Yakov Pechersky]

For me, in an empty file with your first defn, #reduce does not time out for me.

[Scott Kovach]

oops, I agree. it seems that adding import data.list.perm causes the timeout (I haven't intentionally used anything from this module, but I was planning to)

[Kevin Buzzard]

#print prefix merge shows you what is really going on. The four equations e.g. merge.equations._eqn_3 show you the things which are true, but Lean will not guarantee that they're true by definition.

[Mario Carneiro]

It's not possible for all three equations in merge to be defeqs

[Mario Carneiro]

because you have to case on one of the arguments first; if you case on xs then merge xs [] = xs will not be defeq

[Mario Carneiro]

incidentally, lean has a slightly stupid case tree generator so it manages to break both of the first two defeqs

[Kevin Buzzard]

But there is another issue here:

def merge {α : Type} [linear_order α] : list α → list α → list α
| []      []      := []
| []      (y::ys) := y::ys
| (x::xs) []      := x::xs
| (x::xs) (y::ys) := if x ≤ y then x :: merge xs (y::ys) else y :: merge (x::xs) ys

does not make example {α : Type} [linear_order α] (x : α) (xs : list α) : merge (x :: xs) [] = x :: xs := rfl work.

[Mario Carneiro]

oh, right, this function also has a weird recursion structure

[Mario Carneiro]

it's probably being compiled with well founded recursion which breaks all the defeqs

[Kevin Buzzard]

example {α : Type} [linear_order α] : merge ([] : list α) [] = [] := rfl works!

[Mario Carneiro]

It's possible to compile this one to satisfy the four equations you wrote

[Mario Carneiro]

def merge {α : Type} [linear_order α] : list α → list α → list α :=
λ xs, list.rec_on xs (λ ys, ys) $ λ x xs IH ys,
list.rec_on ys (x::xs) $ λ y ys ih,
if x ≤ y then x :: IH (y::ys) else y :: ih

variables {α : Type} [linear_order α] (x y : α) (xs ys : list α)
example : merge [] ys = ys := rfl
example : merge (x::xs) [] = x::xs := rfl
example : merge (x::xs) (y::ys) =
  if x ≤ y then x :: merge xs (y::ys) else y :: merge (x::xs) ys := rfl

[Mario Carneiro]

but

example : merge xs [] = xs := rfl -- fails

[Kevin Buzzard]

This is about the best one can expect, I guess.

[Mario Carneiro]

right, the different cases that you get defeqs for have to be disjoint

[Kevin Buzzard]

People like me who take definitional equality less seriously just need to know the trick that simp [merge] will solve these lemmas. In a typical Lean formalisation one would in fact take these four "definitional" lemmas and restate them (with any notation which one wants to use), prove them (with rfl or not depending on what works) and then tag the lemmas with simp and let the simplifier do the rewriting for you.

[Scott Kovach]

thanks Kevin and Mario! i'll carry on with propositional equalities for now