From 365b2ee5fe488d4c523965ec3634b6aa87ef1d3d Mon Sep 17 00:00:00 2001 From: Ryan Greenblatt Date: Tue, 28 Jun 2022 00:04:54 +0000 Subject: [PATCH] feat(data/bool): bnot_ne (#10562) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Eric Wieser Co-authored-by: Yaël Dillies --- src/data/bool/basic.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/data/bool/basic.lean b/src/data/bool/basic.lean index 981b3d57606f0..3bf145abd8895 100644 --- a/src/data/bool/basic.lean +++ b/src/data/bool/basic.lean @@ -132,6 +132,12 @@ theorem band_elim_right : ∀ {a b : bool}, a && b → b := dec_trivial @[simp] theorem bnot_true : bnot tt = ff := rfl +@[simp] lemma not_eq_bnot : ∀ {a b : bool}, ¬a = !b ↔ a = b := dec_trivial +@[simp] lemma bnot_not_eq : ∀ {a b : bool}, ¬!a = b ↔ a = b := dec_trivial + +lemma ne_bnot {a b : bool} : a ≠ !b ↔ a = b := not_eq_bnot +lemma bnot_ne {a b : bool} : !a ≠ b ↔ a = b := bnot_not_eq + @[simp] theorem bnot_iff_not : ∀ {b : bool}, !b ↔ ¬b := dec_trivial theorem eq_tt_of_bnot_eq_ff : ∀ {a : bool}, bnot a = ff → a = tt := dec_trivial