Zulip Chat Archive

Stream: new members

Topic: defining a list merge function


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Dec 28 2020 at 19:23):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Dec 28 2020 at 19:26):

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

view this post on Zulip Mario Carneiro (Dec 28 2020 at 19:27):

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

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 19:27):

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

view this post on Zulip Mario Carneiro (Dec 28 2020 at 19:27):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 28 2020 at 19:32):

but

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

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 19:34):

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

view this post on Zulip Mario Carneiro (Dec 28 2020 at 19:34):

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

view this post on Zulip 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.

view this post on Zulip 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