feat: Bool lemmas improving confluence (leanprover#5155)

src/Init/Data/Bool.lean

@@ -55,6 +55,12 @@ theorem eq_iff_iff {a b : Bool} : a = b ↔ (a ↔ b) := by cases b <;> simp
 theorem decide_true_eq  {b : Bool} [Decidable (true = b)]  : decide (true  = b) =  b := by cases b <;> simp
 theorem decide_false_eq {b : Bool} [Decidable (false = b)] : decide (false = b) = !b := by cases b <;> simp
 
+-- These lemmas assist with confluence.
+@[simp] theorem eq_false_imp_eq_true_iff :
+    ∀(a b : Bool), ((a = false → b = true) ↔ (b = false → a = true)) = True := by decide
+@[simp] theorem eq_true_imp_eq_false_iff :
+    ∀(a b : Bool), ((a = true → b = false) ↔ (b = true → a = false)) = True := by decide
+
 /-! ### and -/
 
 @[simp] theorem and_self_left  : ∀(a b : Bool), (a && (a && b)) = (a && b) := by decide
@@ -91,6 +97,11 @@ Needed for confluence of term `(a && b) ↔ a` which reduces to `(a && b) = a` v
 @[simp] theorem iff_self_and : ∀(a b : Bool), (a = (a && b)) ↔ (a → b) := by decide
 @[simp] theorem iff_and_self : ∀(a b : Bool), (b = (a && b)) ↔ (b → a) := by decide
 
+@[simp] theorem not_and_iff_left_iff_imp  : ∀ (a b : Bool), ((!a && b) = a) ↔ !a ∧ !b := by decide
+@[simp] theorem and_not_iff_right_iff_imp : ∀ (a b : Bool), ((a && !b) = b) ↔ !a ∧ !b := by decide
+@[simp] theorem iff_not_self_and : ∀ (a b : Bool), (a = (!a && b)) ↔ !a ∧ !b := by decide
+@[simp] theorem iff_and_not_self : ∀ (a b : Bool), (b = (a && !b)) ↔ !a ∧ !b := by decide
+
 /-! ### or -/
 
 @[simp] theorem or_self_left  : ∀(a b : Bool), (a || (a || b)) = (a || b) := by decide
@@ -120,6 +131,11 @@ Needed for confluence of term `(a || b) ↔ a` which reduces to `(a || b) = a` v
 @[simp] theorem iff_self_or : ∀(a b : Bool), (a = (a || b)) ↔ (b → a) := by decide
 @[simp] theorem iff_or_self : ∀(a b : Bool), (b = (a || b)) ↔ (a → b) := by decide
 
+@[simp] theorem not_or_iff_left_iff_imp  : ∀ (a b : Bool), ((!a || b) = a) ↔ a ∧ b := by decide
+@[simp] theorem or_not_iff_right_iff_imp : ∀ (a b : Bool), ((a || !b) = b) ↔ a ∧ b := by decide
+@[simp] theorem iff_not_self_or : ∀ (a b : Bool), (a = (!a || b)) ↔ a ∧ b := by decide
+@[simp] theorem iff_or_not_self : ∀ (a b : Bool), (b = (a || !b)) ↔ a ∧ b := by decide
+
 theorem or_comm : ∀ (x y : Bool), (x || y) = (y || x) := by decide
 instance : Std.Commutative (· || ·) := ⟨or_comm⟩
 
@@ -202,8 +218,11 @@ instance : Std.LawfulIdentity (· != ·) false where
 @[simp] theorem not_beq_self : ∀ (x : Bool), ((!x) == x) = false := by decide
 @[simp] theorem beq_not_self : ∀ (x : Bool), (x   == !x) = false := by decide
 
-@[simp] theorem not_bne_self : ∀ (x : Bool), ((!x) != x) = true := by decide
-@[simp] theorem bne_not_self : ∀ (x : Bool), (x   != !x) = true := by decide
+@[simp] theorem not_bne : ∀ (a b : Bool), ((!a) != b) = !(a != b) := by decide
+@[simp] theorem bne_not : ∀ (a b : Bool), (a != !b) = !(a != b) := by decide
+
+theorem not_bne_self : ∀ (x : Bool), ((!x) != x) = true := by decide
+theorem bne_not_self : ∀ (x : Bool), (x   != !x) = true := by decide
 
 /-
 Added for equivalence with `Bool.not_beq_self` and needed for confluence
@@ -235,8 +254,10 @@ theorem beq_eq_decide_eq [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) :
   · simp [ne_of_beq_false h]
   · simp [eq_of_beq h]
 
-@[simp] theorem not_eq_not : ∀ {a b : Bool}, ¬a = !b ↔ a = b := by decide
+theorem eq_not : ∀ (a b : Bool), (a = (!b)) ↔ (a ≠ b) := by decide
+theorem not_eq : ∀ (a b : Bool), ((!a) = b) ↔ (a ≠ b) := by decide
 
+@[simp] theorem not_eq_not : ∀ {a b : Bool}, ¬a = !b ↔ a = b := by decide
 @[simp] theorem not_not_eq : ∀ {a b : Bool}, ¬(!a) = b ↔ a = b := by decide
 
 @[simp] theorem coe_iff_coe : ∀(a b : Bool), (a ↔ b) ↔ a = b := by decide
@@ -509,6 +530,10 @@ protected theorem cond_false {α : Type u} {a b : α} : cond false a b = b := co
 @[simp] theorem cond_true_right  : ∀(c t : Bool), cond c t true  = (!c || t) := by decide
 @[simp] theorem cond_false_right : ∀(c t : Bool), cond c t false = ( c && t) := by decide
 
+-- These restore confluence between the above lemmas and `cond_not`.
+@[simp] theorem cond_true_not_same  : ∀ (c b : Bool), cond c (!c) b = (!c && b) := by decide
+@[simp] theorem cond_false_not_same : ∀ (c b : Bool), cond c b (!c) = (!c || b) := by decide
+
 @[simp] theorem cond_true_same  : ∀(c b : Bool), cond c c b = (c || b) := by decide
 @[simp] theorem cond_false_same : ∀(c b : Bool), cond c b c = (c && b) := by decide
 

tests/lean/bool_simp.lean

@@ -3,7 +3,7 @@ variable (b c d : Bool)
 variable (u v w : Prop) [Decidable u] [Decidable v] [Decidable w]
 
 -- Specific regressions found when introducing Boolean normalization
-#check_simp (b != !c) = false ~> b = !c
+#check_simp (b != !c) = false ~> b ≠ c
 #check_simp ¬(u → v ∨ w) ~> u ∧ ¬v ∧ ¬w
 #check_simp decide (u ∧ (v → False)) ~> decide u && !decide v
 #check_simp decide (cond true b c = true) ~> b