Zulip Chat Archive

Stream: new members

Topic: none ≠ some


view this post on Zulip Marcus Rossel (Jan 13 2021 at 08:06):

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?

view this post on Zulip Johan Commelin (Jan 13 2021 at 08:20):

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

view this post on Zulip Johan Commelin (Jan 13 2021 at 08:21):

Have you tried library_search?

view this post on Zulip Marcus Rossel (Jan 13 2021 at 08:25):

Johan Commelin said:

Have you tried library_search?

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

view this post on Zulip Eric Wieser (Jan 13 2021 at 08:27):

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

view this post on Zulip Marcus Rossel (Jan 13 2021 at 08:35):

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.

view this post on Zulip Kevin Buzzard (Jan 13 2021 at 08:38):

You can use change to change it to some.

view this post on Zulip Marcus Rossel (Jan 13 2021 at 08:48):

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

view this post on Zulip Johan Commelin (Jan 13 2021 at 08:49):

change \not none = some v

view this post on Zulip Johan Commelin (Jan 13 2021 at 08:51):

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

view this post on Zulip Yakov Pechersky (Jan 13 2021 at 14:52):

Perhaps 'coe_eq_some' should be a simp lemma

view this post on Zulip Johan Commelin (Jan 13 2021 at 14:58):

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

view this post on Zulip Eric Wieser (Jan 13 2021 at 15:32):

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


Last updated: May 08 2021 at 09:11 UTC