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

Stream: Is there code for X?

[Kevin Buzzard]

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]

revert a b, exact dec_trivial ??

[Kevin Buzzard]

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]

Or otherwise

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

[Kevin Buzzard]

What if a and b are 100 ASCII characters long?

[Johan Commelin]

Then first prove this lemma

[Kevin Buzzard]

rofl

[Johan Commelin]

And apply it

[Kenny Lau]

cases_matching

[Kenny Lau]

maybe not

[Johan Commelin]

You can do it locally:

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

[Kevin Buzzard]

Right.

[Kevin Buzzard]

Does our esteemed mathematics library not contain this result??

[Kenny Lau]

PR

[Kevin Buzzard]

Where does it go?

[Kevin Buzzard]

data.codewars

[Kevin Buzzard]

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

[Kenny Lau]

data.bool

[Kevin Buzzard]

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

[Kevin Buzzard]

^^ spoiler alerts

[Patrick Massot]

Why are you suddenly using bool?

[Kevin Buzzard]

#2523

[Kevin Buzzard]

Patrick Massot said:

Why are you suddenly using bool?

bloody codewars

[Kevin Buzzard]

It's Saturday night

[Mario Carneiro]

This should be in data.bool

[Kevin Buzzard]

Kevin Buzzard said:

#2523

[Mario Carneiro]

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