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