option troubles

Stream: general

[Johan Commelin]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Chris Hughes]

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.

[Reid Barton]

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

[Johan Commelin]

Thanks @Chris Hughes and @Reid Barton !

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

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