Flatten Option

Stream: Is there code for X?

[Marcus Rossel]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I think it's option.join.

[Kevin Buzzard]

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

[Adam Topaz]

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

[Marcus Rossel]

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.

[Adam Topaz]

docs#mjoin

[Adam Topaz]

import control.monad.basic

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

[Yakov Pechersky]

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

[Yakov Pechersky]

Lemmas like join_eq_some and join_eq_some

[Yakov Pechersky]

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.

[Marcus Rossel]

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?

[Mario Carneiro]

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]

[Kevin Buzzard]

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?

[Marcus Rossel]

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

[Yakov Pechersky]

Specifically, docs#option.alternative

[Yakov Pechersky]

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."

[Mario Carneiro]

You can also use option.orelse for the core function

[Marcus Rossel]

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.

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

Which has to do which lemmas about how zip_with works.

[Yakov Pechersky]

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.

[Yakov Pechersky]

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?)