none ≠ some

Stream: new members

[Marcus Rossel]

I have the following goal state and don't know how to continue:

v: value
⊢ ¬none = ↑v

If I understand this correctly, I'm supposed to prove ¬ none = some v. I thought simp would handle that, but it doesn't.
How can I resolve this?

[Johan Commelin]

@Marcus Rossel there should be a lemma option.some_ne_none. Alternatively, you can close this with option.no_confusion.

[Johan Commelin]

Have you tried library_search?

[Marcus Rossel]

Johan Commelin said:

Have you tried library_search?

Yeah, it couldn't come up with anything, which seems odd.

[Eric Wieser]

What if you change the goal to be expressed using some instead of a coercion?

[Marcus Rossel]

Eric Wieser said:

What if you change the goal to be expressed using some instead of a coercion?

The coercion was introduced by Lean itself. The proposition where v comes from explicitly uses some v.

[Kevin Buzzard]

You can use change to change it to some.

[Marcus Rossel]

Kevin Buzzard said:

You can use change to change it to some.

Like this change ↑v with (some v)? Because that just introduces two subgoals for me:

example {value : Type*} (v : value) :
  ¬ (none : (option value)) = ↑v :=
  begin
    change ↑v with (some v),
    -- 1: ⊢ ¬none = ↑v
    -- 2: ⊢ has_lift_t value (option value)
  end

[Johan Commelin]

change \not none = some v

[Johan Commelin]

example {value : Type*} (v : value) :
  ¬ (none : (option value)) = ↑v :=
begin
  apply option.no_confusion
end

[Yakov Pechersky]

Perhaps 'coe_eq_some' should be a simp lemma

[Johan Commelin]

Hmm, shouldn't the other direction be a simp-lemma?

[Eric Wieser]

I think we have a lot of simp lemmas that the linter will complain about if some stopped being simp-normal