Zulip Chat Archive

Stream: new members

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


Jiekai (Jul 14 2021 at 05:04):

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 (Jul 14 2021 at 05:11):

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

Mario Carneiro (Jul 14 2021 at 05:11):

it just knows that different constructors are different

Mario Carneiro (Jul 14 2021 at 05:12):

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

Marcus Rossel (Jul 14 2021 at 05:14):

@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 (Jul 14 2021 at 05:14):

Yes, simp? or squeeze_simp

Mario Carneiro (Jul 14 2021 at 05:14):

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

Marcus Rossel (Jul 14 2021 at 05:15):

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 (Jul 14 2021 at 05:22):

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 (Jul 14 2021 at 05:32):

Don't forget this proof:

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

Last updated: Dec 20 2023 at 11:08 UTC