Zulip Chat Archive

Stream: Is there code for X?

Topic: bnot (a && b) = (bnot a) || (bnot b)


view this post on Zulip Kevin Buzzard (Apr 25 2020 at 17:27):

Do we have a tactic which solves

example (a b : bool) : bnot (a && b) = (bnot a) || (bnot b) := sorry

? I tried finish, tauto, tauto!, cc, simp and exact dec_trivial but none work. I know I can prove it by casing on a and b, but in my use case a and b are unwieldy and if I have a tactic it will save me the work of generalizeing.

view this post on Zulip Johan Commelin (Apr 25 2020 at 17:28):

revert a b, exact dec_trivial ??

view this post on Zulip Kevin Buzzard (Apr 25 2020 at 17:29):

This does work, but in my use case it will be revert [some unholy mess]. I was surprised that this wasn't in logic.basic -- I should say library_search also seems to fail (unless I've not got the right imports?)

view this post on Zulip Johan Commelin (Apr 25 2020 at 17:29):

Or otherwise

example (a b : bool) : bnot (a && b) = (bnot a) || (bnot b) :=
by cases a; cases b; refl

view this post on Zulip Kevin Buzzard (Apr 25 2020 at 17:29):

What if a and b are 100 ASCII characters long?

view this post on Zulip Johan Commelin (Apr 25 2020 at 17:29):

Then first prove this lemma

view this post on Zulip Kevin Buzzard (Apr 25 2020 at 17:30):

rofl

view this post on Zulip Johan Commelin (Apr 25 2020 at 17:30):

And apply it

view this post on Zulip Kenny Lau (Apr 25 2020 at 17:30):

cases_matching

view this post on Zulip Kenny Lau (Apr 25 2020 at 17:30):

maybe not

view this post on Zulip Johan Commelin (Apr 25 2020 at 17:30):

You can do it locally:

have : \forall (a b : bool) : bnot (a && b) = (bnot a) || (bnot b), from dec_trivial,
apply this,

view this post on Zulip Kevin Buzzard (Apr 25 2020 at 17:30):

Right.

view this post on Zulip Kevin Buzzard (Apr 25 2020 at 17:30):

Does our esteemed mathematics library not contain this result??

view this post on Zulip Kenny Lau (Apr 25 2020 at 17:31):

PR

view this post on Zulip Kevin Buzzard (Apr 25 2020 at 17:31):

Where does it go?

view this post on Zulip Kevin Buzzard (Apr 25 2020 at 17:31):

data.codewars

view this post on Zulip Kevin Buzzard (Apr 25 2020 at 17:31):

together with def lt_abs (x y : ℝ) : x < abs y ↔ x < y ∨ x < -y := lt_max_iff

view this post on Zulip Kenny Lau (Apr 25 2020 at 17:31):

data.bool

view this post on Zulip Kevin Buzzard (Apr 25 2020 at 17:32):

and theorem modeq_iff_dvd' {n : ℕ} {a b : ℕ} (h : a ≤ b) : a ≡ b [MOD n] ↔ n ∣ b - a

view this post on Zulip Kevin Buzzard (Apr 25 2020 at 17:34):

^^ spoiler alerts

view this post on Zulip Patrick Massot (Apr 25 2020 at 17:48):

Why are you suddenly using bool?

view this post on Zulip Kevin Buzzard (Apr 25 2020 at 17:59):

#2523

view this post on Zulip Kevin Buzzard (Apr 25 2020 at 17:59):

Patrick Massot said:

Why are you suddenly using bool?

bloody codewars

view this post on Zulip Kevin Buzzard (Apr 25 2020 at 17:59):

It's Saturday night

view this post on Zulip Mario Carneiro (Apr 25 2020 at 19:27):

This should be in data.bool

view this post on Zulip Kevin Buzzard (Apr 25 2020 at 19:38):

Kevin Buzzard said:

#2523

view this post on Zulip Mario Carneiro (Apr 25 2020 at 19:48):

I read my messages in temporal order, so sometimes my responses come from the past :)


Last updated: May 07 2021 at 23:11 UTC