tactics for `¬ option.some m = option.none`

Stream: new members

[Jiekai]

example (m : ℕ) : ¬ option.some m = option.none :=
begin
  sorry
end

simp works. Does simp mainly do rw? If that's true, what should the rw be?

[Mario Carneiro]

This is using the part of simp that isn't rw, namely the constructor_eq setting

[Mario Carneiro]

it just knows that different constructors are different

[Mario Carneiro]

however there might be a rewrite lemma for this, probably called docs#option.some_ne_none

[Marcus Rossel]

@Mario Carneiro Is there a way to get an output of what kind of lemmas simp or finish used though (if they use any)?

[Mario Carneiro]

Yes, simp? or squeeze_simp

[Mario Carneiro]

however in this case I doubt that lemma will show up, because simp only will already perform this reduction

[Marcus Rossel]

Mario Carneiro said:

however in this case I doubt that lemma will show up, because simp only will already perform this reduction

Yeah, it did simp only [not_false_iff].

[Jiekai]

I looked up the mathlib code and found apply option.no_confusion works.
But when I used vscode Go to Definition there is no no_confusion. Then I created my own version of option, and no_confusion still works.

Then I found this xena no-confusion-over-no_confusion :tada:

[Mario Carneiro]

Don't forget this proof:

example (m : ℕ) : ¬ option.some m = option.none.