## Stream: Is there code for X?

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

#### 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.

#### Johan Commelin (Apr 25 2020 at 17:28):

revert a b, exact dec_trivial ??

#### 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?)

#### 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


#### Kevin Buzzard (Apr 25 2020 at 17:29):

What if a and b are 100 ASCII characters long?

#### Johan Commelin (Apr 25 2020 at 17:29):

Then first prove this lemma

rofl

And apply it

#### Kenny Lau (Apr 25 2020 at 17:30):

cases_matching

maybe not

#### 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,


Right.

#### Kevin Buzzard (Apr 25 2020 at 17:30):

Does our esteemed mathematics library not contain this result??

PR

#### Kevin Buzzard (Apr 25 2020 at 17:31):

Where does it go?

#### Kevin Buzzard (Apr 25 2020 at 17:31):

data.codewars

#### 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

#### Kenny Lau (Apr 25 2020 at 17:31):

data.bool

#### 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

#### Patrick Massot (Apr 25 2020 at 17:48):

Why are you suddenly using bool?

#2523

#### Kevin Buzzard (Apr 25 2020 at 17:59):

Patrick Massot said:

Why are you suddenly using bool?

bloody codewars

#### Kevin Buzzard (Apr 25 2020 at 17:59):

It's Saturday night

#### Mario Carneiro (Apr 25 2020 at 19:27):

This should be in data.bool

#### Kevin Buzzard (Apr 25 2020 at 19:38):

Kevin Buzzard said:

#2523

#### 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