# Zulip Chat Archive

## Stream: new members

### Topic: defining a list merge function

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

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 (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