Zulip Chat Archive

Stream: general

Topic: option troubles


view this post on Zulip Johan Commelin (Oct 09 2018 at 18:14):

I have x : option X, and h : x ≠ none. How do I turn this into a y : X such that x = some y? I want to use option.get and option.is_some. But I can't figure out how to use h.

view this post on Zulip Johan Commelin (Oct 09 2018 at 18:15):

example {X : Type} (x : option X) (h : x  none) : X := sorry

view this post on Zulip Johan Commelin (Oct 09 2018 at 18:16):

Or something like that. I should probably not just return an y : X, but also the proof that x = some y.

view this post on Zulip Chris Hughes (Oct 09 2018 at 18:22):

example {α : Sort*} (x : option α) : x  none  {y // x = some y} :=
option.rec_on x (absurd rfl) (λ y _, y, rfl)

There should be a lemma that says is_some_iff_ne_none, but it seems to be missing.

view this post on Zulip Reid Barton (Oct 09 2018 at 18:23):

Depending on the use, it might be more convenient to just do the cases, absurd at the usage site

view this post on Zulip Johan Commelin (Oct 09 2018 at 18:28):

Thanks @Chris Hughes and @Reid Barton !

view this post on Zulip Patrick Massot (Oct 09 2018 at 18:28):

as in

example {X : Type} (x : option X) (h : x  none) : {y // x = some y} :=
begin
  cases x with a,
  exact absurd (by simpa [h]) not_false,
  exact a, rfl
end

view this post on Zulip Mario Carneiro (Oct 09 2018 at 18:38):

there is is_none_iff_eq_none, but nothing connecting is_some and is_none. I guess we need a few more variants

view this post on Zulip Mario Carneiro (Oct 09 2018 at 18:38):

but the basic story is option.get is supposed to do this


Last updated: May 08 2021 at 04:14 UTC