## Stream: new members

### Topic: defining a list merge function

#### Scott Kovach (Dec 28 2020 at 19:04):

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] 

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 (Dec 28 2020 at 19:07):

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

#### Scott Kovach (Dec 28 2020 at 19:22):

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 (Dec 28 2020 at 19:22):

#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 (Dec 28 2020 at 19:23):

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

#### Mario Carneiro (Dec 28 2020 at 19:24):

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 (Dec 28 2020 at 19:25):

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

#### Kevin Buzzard (Dec 28 2020 at 19:25):

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 (Dec 28 2020 at 19:26):

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

#### Mario Carneiro (Dec 28 2020 at 19:27):

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

#### Kevin Buzzard (Dec 28 2020 at 19:27):

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

#### Mario Carneiro (Dec 28 2020 at 19:27):

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

#### Mario Carneiro (Dec 28 2020 at 19:31):

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 (Dec 28 2020 at 19:32):

but

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


#### Kevin Buzzard (Dec 28 2020 at 19:34):

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

#### Mario Carneiro (Dec 28 2020 at 19:34):

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

#### Kevin Buzzard (Dec 28 2020 at 19:36):

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 (Dec 28 2020 at 19:47):

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

Last updated: May 13 2021 at 18:26 UTC