Zulip Chat Archive

Stream: Is there code for X?

Topic: Flatten Option


view this post on Zulip Marcus Rossel (Jan 11 2021 at 16:03):

Is there a way to flatten a v : option (option nat)) into a v' : option nat?

view this post on Zulip Kevin Buzzard (Jan 11 2021 at 16:03):

that looks like something a monad does. And option is a monad.

view this post on Zulip Kevin Buzzard (Jan 11 2021 at 16:04):

I think it's option.join.

view this post on Zulip Kevin Buzzard (Jan 11 2021 at 16:05):

lol I found this with library_search and it looks like Yakov put it there last week.

view this post on Zulip Adam Topaz (Jan 11 2021 at 16:06):

The general join for a monad is mjoin. So if you know you have a monad instance, you can just use that.

view this post on Zulip Marcus Rossel (Jan 11 2021 at 16:06):

Kevin Buzzard said:

lol I found this with library_search and it looks like Yakov put it there last week.

How did you find it with library_search? I tried to do it that way too, but it didn't work out.

view this post on Zulip Adam Topaz (Jan 11 2021 at 16:06):

docs#mjoin

view this post on Zulip Adam Topaz (Jan 11 2021 at 16:09):

import control.monad.basic

example {α : Type*} : option (option α)  option α := by library_search
-- try this: option.join

view this post on Zulip Yakov Pechersky (Jan 11 2021 at 16:36):

mjoin and option.join should do the same thing (that's proven), but there will like be more lemmas about how option.join works with option than the general mjoin

view this post on Zulip Yakov Pechersky (Jan 11 2021 at 16:36):

Lemmas like join_eq_some and join_eq_some

view this post on Zulip Yakov Pechersky (Jan 11 2021 at 16:37):

May I ask what the use case is? How will you use the output flattened option? It's likely that you can just bind on the original, and that might be more performant.

view this post on Zulip Marcus Rossel (Jan 11 2021 at 16:45):

Yakov Pechersky said:

May I ask what the use case is? How will you use the output flattened option? It's likely that you can just bind on the original, and that might be more performant.

I'm merging one list onto another:

-- `last` should override those positions in `first` where the value in `last` is not `empty`
def merge {α : Type*} (first last : list (option α)) : list (option α) :=
  last.enum.map (λ i, e⟩, if e  none then e else mjoin (first.nth i))

For some reason option.join is not available to me. Do I need to update my version of mathlib somehow?

view this post on Zulip Mario Carneiro (Jan 11 2021 at 16:52):

def merge {α : Type*} (first last : list (option α)) : list (option α) :=
  last.zip_with (<|>) first

#eval merge [some 1, some 2, none, none] [some 2, none, some 3, none]
-- [some 2, some 2, some 3, none]

view this post on Zulip Kevin Buzzard (Jan 11 2021 at 17:19):

I used today's mathlib. Sure feel free to update. Are you working in mathlib itself or in a project with mathlib as a dependency?

view this post on Zulip Marcus Rossel (Jan 11 2021 at 18:35):

For those as clueless as me, the <|> comes from has_orelse.

view this post on Zulip Yakov Pechersky (Jan 11 2021 at 18:36):

Specifically, docs#option.alternative

view this post on Zulip Yakov Pechersky (Jan 11 2021 at 18:37):

Which defines the alternative instance for option as equivalent to "when given two options, if the first is some then that one, otherwise the second one."

view this post on Zulip Mario Carneiro (Jan 11 2021 at 18:39):

You can also use option.orelse for the core function

view this post on Zulip Marcus Rossel (Jan 11 2021 at 18:58):

Where would I find theorems about option's alternative and or_else. E.g. if I wanted to prove

example (l : list (option α)) : merge l (list.repeat none l.length) = l := sorry

... I would need to show in some way that combining none with some x always yields x.

view this post on Zulip Yakov Pechersky (Jan 11 2021 at 19:05):

You can prove this by induction on l. Sorry, you can prove this by ext too.

view this post on Zulip Yakov Pechersky (Jan 11 2021 at 19:07):

Which goes like, for some x ∈ merge ... it is the same as the x ∈ l

view this post on Zulip Yakov Pechersky (Jan 11 2021 at 19:07):

Which has to do which lemmas about how zip_with works.

view this post on Zulip Yakov Pechersky (Jan 11 2021 at 19:08):

then, use docs#option.none_orelse. Note that it is tagged with simp. I expect that the simplifier would do most of the work for you.

view this post on Zulip Yakov Pechersky (Jan 11 2021 at 19:10):

You'd need to say simp [list.eq_of_mem_repeat], since that's not tagged with simp at the moment (simp experts -- should it be?)


Last updated: May 07 2021 at 19:12 UTC