chore: fix tests

This is a major refactor of the Bool/Prop simp tester to support other
theories and support non-linear test cases.  As part of this, additional
lemmas were added to improve confluence.

doc/examples/bintree.lean

@@ -277,14 +277,13 @@ theorem BinTree.find_insert (b : BinTree β) (k : Nat) (v : β)
     . by_cases' key < k
       cases h; apply ihr; assumption
 
-theorem BinTree.find_insert_of_ne (b : BinTree β) (h : k ≠ k') (v : β)
+theorem BinTree.find_insert_of_ne (b : BinTree β) (ne : k ≠ k') (v : β)
         : (b.insert k v).find? k' = b.find? k' := by
   let ⟨t, h⟩ := b; simp
   induction t with simp
   | leaf =>
-    intros
-    have_eq k k'
-    contradiction
+    intros le
+    exact Nat.lt_of_le_of_ne le ne
   | node left key value right ihl ihr =>
     let .node hl hr bl br := h
     specialize ihl bl

src/Init/ByCases.lean

@@ -37,15 +37,6 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
     f (ite P x y) = ite P (f x) (f y) :=
   apply_dite f P (fun _ => x) (fun _ => y)
 
-/-- Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches. -/
-@[simp] theorem dite_not (P : Prop) {_ : Decidable P}  (x : ¬P → α) (y : ¬¬P → α) :
-    dite (¬P) x y = dite P (fun h => y (not_not_intro h)) x := by
-  by_cases h : P <;> simp [h]
-
-/-- Negation of the condition `P : Prop` in a `ite` is the same as swapping the branches. -/
-@[simp] theorem ite_not (P : Prop) {_ : Decidable P} (x y : α) : ite (¬P) x y = ite P y x :=
-  dite_not P (fun _ => x) (fun _ => y)
-
 @[simp] theorem dite_eq_left_iff {P : Prop} [Decidable P] {B : ¬ P → α} :
     dite P (fun _ => a) B = a ↔ ∀ h, B h = a := by
   by_cases P <;> simp [*, forall_prop_of_true, forall_prop_of_false]

src/Init/Classical.lean

@@ -125,16 +125,15 @@ theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
 /-- The Double Negation Theorem: `¬¬P` is equivalent to `P`.
 The left-to-right direction, double negation elimination (DNE),
 is classically true but not constructively. -/
-@[scoped simp] theorem not_not : ¬¬a ↔ a := Decidable.not_not
+@[simp] theorem not_not : ¬¬a ↔ a := Decidable.not_not
 
-@[simp] theorem not_forall {p : α → Prop} : (¬∀ x, p x) ↔ ∃ x, ¬p x := Decidable.not_forall
+@[simp low] theorem not_forall {p : α → Prop} : (¬∀ x, p x) ↔ ∃ x, ¬p x := Decidable.not_forall
 
 theorem not_forall_not {p : α → Prop} : (¬∀ x, ¬p x) ↔ ∃ x, p x := Decidable.not_forall_not
 theorem not_exists_not {p : α → Prop} : (¬∃ x, ¬p x) ↔ ∀ x, p x := Decidable.not_exists_not
 
 theorem forall_or_exists_not (P : α → Prop) : (∀ a, P a) ∨ ∃ a, ¬ P a := by
   rw [← not_forall]; exact em _
-
 theorem exists_or_forall_not (P : α → Prop) : (∃ a, P a) ∨ ∀ a, ¬ P a := by
   rw [← not_exists]; exact em _
 
@@ -147,8 +146,22 @@ theorem not_and_iff_or_not_not : ¬(a ∧ b) ↔ ¬a ∨ ¬b := Decidable.not_an
 
 theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) := Decidable.not_iff
 
+@[simp] theorem imp_iff_left_iff  : (b ↔ a → b) ↔ a ∨ b := Decidable.imp_iff_left_iff
+@[simp] theorem imp_iff_right_iff : (a → b ↔ b) ↔ a ∨ b := Decidable.imp_iff_right_iff
+
+@[simp] theorem and_or_imp : a ∧ b ∨ (a → c) ↔ a → b ∨ c := Decidable.and_or_imp
+
+@[simp] theorem not_imp : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff_and_not
+
+@[simp] theorem imp_and_neg_imp_iff (p q : Prop) : (p → q) ∧ (¬p → q) ↔ q :=
+  Iff.intro (fun (a : _ ∧ _) => (Classical.em p).rec a.left a.right)
+            (fun a => And.intro (fun _ => a) (fun _ => a))
+
 end Classical
 
+/- Export for Mathlib compat. -/
+export Classical (imp_iff_right_iff imp_and_neg_imp_iff and_or_imp not_imp)
+
 /-- Extract an element from a existential statement, using `Classical.choose`. -/
 -- This enables projection notation.
 @[reducible] noncomputable def Exists.choose {p : α → Prop} (P : ∃ a, p a) : α := Classical.choose P

src/Init/Core.lean

@@ -677,7 +677,7 @@ You can prove theorems about the resulting element by induction on `h`, since
 theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h₂ : p a) : p b :=
   h₁ ▸ h₂
 
-theorem cast_eq {α : Sort u} (h : α = α) (a : α) : cast h a = a :=
+@[simp] theorem cast_eq {α : Sort u} (h : α = α) (a : α) : cast h a = a :=
   rfl
 
 /--
@@ -1403,9 +1403,9 @@ theorem false_imp_iff (a : Prop) : (False → a) ↔ True := iff_true_intro Fals
 
 theorem true_imp_iff (α : Prop) : (True → α) ↔ α := imp_iff_right True.intro
 
-@[simp] theorem imp_self : (a → a) ↔ True := iff_true_intro id
+@[simp high] theorem imp_self : (a → a) ↔ True := iff_true_intro id
 
-theorem imp_false : (a → False) ↔ ¬a := Iff.rfl
+@[simp] theorem imp_false : (a → False) ↔ ¬a := Iff.rfl
 
 theorem imp.swap : (a → b → c) ↔ (b → a → c) := Iff.intro flip flip
 

src/Init/Data/Bool.lean

@@ -29,6 +29,8 @@ instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∃ x, p x) :
   | _, isTrue hf => isTrue ⟨_, hf⟩
   | isFalse ht, isFalse hf => isFalse fun | ⟨true, h⟩ => absurd h ht | ⟨false, h⟩ => absurd h hf
 
+@[simp] theorem default_bool : default = false := rfl
+
 instance : LE Bool := ⟨(. → .)⟩
 instance : LT Bool := ⟨(!. && .)⟩
 
@@ -48,85 +50,202 @@ theorem ne_false_iff : {b : Bool} → b ≠ false ↔ b = true := by decide
 
 theorem eq_iff_iff {a b : Bool} : a = b ↔ (a ↔ b) := by cases b <;> simp
 
-@[simp] theorem decide_eq_true {b : Bool} : decide (b = true) = b := by cases b <;> simp
-@[simp] theorem decide_eq_false {b : Bool} : decide (b = false) = !b := by cases b <;> simp
-@[simp] theorem decide_true_eq {b : Bool} : decide (true = b) = b := by cases b <;> simp
-@[simp] theorem decide_false_eq {b : Bool} : decide (false = b) = !b := by cases b <;> simp
+@[simp] theorem decide_eq_true  {b : Bool} [Decidable (b = true)]  : decide (b = true)  =  b := by cases b <;> simp
+@[simp] theorem decide_eq_false {b : Bool} [Decidable (b = false)] : decide (b = false) = !b := by cases b <;> simp
+@[simp] theorem decide_true_eq  {b : Bool} [Decidable (true = b)]  : decide (true  = b) =  b := by cases b <;> simp
+@[simp] theorem decide_false_eq {b : Bool} [Decidable (false = b)] : decide (false = b) = !b := by cases b <;> simp
 
 /-! ### and -/
 
-@[simp] theorem not_and_self : ∀ (x : Bool), (!x && x) = false := by decide
+@[simp] theorem and_self_left  : ∀(a b : Bool), (a && (a && b)) = (a && b) := by decide
+@[simp] theorem and_self_right : ∀(a b : Bool), ((a && b) && b) = (a && b) := by decide
 
+@[simp] theorem not_and_self : ∀ (x : Bool), (!x && x) = false := by decide
 @[simp] theorem and_not_self : ∀ (x : Bool), (x && !x) = false := by decide
 
+/-
+Added for confluence with `not_and_self` `and_not_self` on term
+`(b && !b) = true` due to reductions:
+
+1. `(b = true ∨ !b = true)` via `Bool.and_eq_true`
+2. `false = true` via `Bool.and_not_self`
+-/
+@[simp] theorem eq_true_and_eq_false_self : ∀(b : Bool), (b = true ∧ b = false) ↔ False := by decide
+@[simp] theorem eq_false_and_eq_true_self : ∀(b : Bool), (b = false ∧ b = true) ↔ False := by decide
+
 theorem and_comm : ∀ (x y : Bool), (x && y) = (y && x) := by decide
 
 theorem and_left_comm : ∀ (x y z : Bool), (x && (y && z)) = (y && (x && z)) := by decide
-
 theorem and_right_comm : ∀ (x y z : Bool), ((x && y) && z) = ((x && z) && y) := by decide
 
-theorem and_or_distrib_left : ∀ (x y z : Bool), (x && (y || z)) = ((x && y) || (x && z)) := by
-  decide
+/-
+Bool version `and_iff_left_iff_imp`.
 
-theorem and_or_distrib_right : ∀ (x y z : Bool), ((x || y) && z) = ((x && z) || (y && z)) := by
-  decide
-
-theorem and_xor_distrib_left : ∀ (x y z : Bool), (x && xor y z) = xor (x && y) (x && z) := by decide
-
-theorem and_xor_distrib_right : ∀ (x y z : Bool), (xor x y && z) = xor (x && z) (y && z) := by
-  decide
-
-/-- De Morgan's law for boolean and -/
-theorem not_and : ∀ (x y : Bool), (!(x && y)) = (!x || !y) := by decide
-
-theorem and_eq_true_iff : ∀ (x y : Bool), (x && y) = true ↔ x = true ∧ y = true := by decide
-
-theorem and_eq_false_iff : ∀ (x y : Bool), (x && y) = false ↔ x = false ∨ y = false := by decide
+Needed for confluence of term `(a && b) ↔ a` which reduces to `(a && b) = a` via
+`Bool.coe_iff_coe` and `a → b` via `Bool.and_eq_true` and
+`and_iff_left_iff_imp`.
+-/
+@[simp] theorem and_iff_left_iff_imp  : ∀(a b : Bool), ((a && b) = a) ↔ (a → b) := by decide
+@[simp] theorem and_iff_right_iff_imp : ∀(a b : Bool), ((a && b) = b) ↔ (b → a) := by decide
+@[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
 
 /-! ### or -/
 
-@[simp] theorem not_or_self : ∀ (x : Bool), (!x || x) = true := by decide
+@[simp] theorem or_self_left  : ∀(a b : Bool), (a || (a || b)) = (a || b) := by decide
+@[simp] theorem or_self_right : ∀(a b : Bool), ((a || b) || b) = (a || b) := by decide
 
+@[simp] theorem not_or_self : ∀ (x : Bool), (!x || x) = true := by decide
 @[simp] theorem or_not_self : ∀ (x : Bool), (x || !x) = true := by decide
 
+/-
+Added for confluence with `not_or_self` `or_not_self` on term
+`(b || !b) = true` due to reductions:
+1. `(b = true ∨ !b = true)` via `Bool.or_eq_true`
+2. `true = true` via `Bool.or_not_self`
+-/
+@[simp] theorem eq_true_or_eq_false_self : ∀(b : Bool), (b = true ∨ b = false) ↔ True := by decide
+@[simp] theorem eq_false_or_eq_true_self : ∀(b : Bool), (b = false ∨ b = true) ↔ True := by decide
+
+/-
+Bool version `or_iff_left_iff_imp`.
+
+Needed for confluence of term `(a || b) ↔ a` which reduces to `(a || b) = a` via
+`Bool.coe_iff_coe` and `a → b` via `Bool.or_eq_true` and
+`and_iff_left_iff_imp`.
+-/
+@[simp] theorem or_iff_left_iff_imp  : ∀(a b : Bool), ((a || b) = a) ↔ (b → a) := by decide
+@[simp] theorem or_iff_right_iff_imp : ∀(a b : Bool), ((a || b) = b) ↔ (a → b) := by decide
+@[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
+
 theorem or_comm : ∀ (x y : Bool), (x || y) = (y || x) := by decide
 
 theorem or_left_comm : ∀ (x y z : Bool), (x || (y || z)) = (y || (x || z)) := by decide
-
 theorem or_right_comm : ∀ (x y z : Bool), ((x || y) || z) = ((x || z) || y) := by decide
 
-theorem or_and_distrib_left : ∀ (x y z : Bool), (x || (y && z)) = ((x || y) && (x || z)) := by
-  decide
+/-! ### distributivity -/
 
-theorem or_and_distrib_right : ∀ (x y z : Bool), ((x && y) || z) = ((x || z) && (y || z)) := by
-  decide
+theorem and_or_distrib_left  : ∀ (x y z : Bool), (x && (y || z)) = (x && y || x && z) := by decide
+theorem and_or_distrib_right : ∀ (x y z : Bool), ((x || y) && z) = (x && z || y && z) := by decide
+
+theorem or_and_distrib_left  : ∀ (x y z : Bool), (x || y && z) = ((x || y) && (x || z)) := by decide
+theorem or_and_distrib_right : ∀ (x y z : Bool), (x && y || z) = ((x || z) && (y || z)) := by decide
+
+/-- De Morgan's law for boolean and -/
+@[simp] theorem not_and : ∀ (x y : Bool), (!(x && y)) = (!x || !y) := by decide
 
 /-- De Morgan's law for boolean or -/
-theorem not_or : ∀ (x y : Bool), (!(x || y)) = (!x && !y) := by decide
+@[simp] theorem not_or : ∀ (x y : Bool), (!(x || y)) = (!x && !y) := by decide
 
-theorem or_eq_true_iff : ∀ (x y : Bool), (x || y) = true ↔ x = true ∨ y = true := by decide
+theorem and_eq_true_iff (x y : Bool) : (x && y) = true ↔ x = true ∧ y = true :=
+  Iff.of_eq (and_eq_true x y)
 
-theorem or_eq_false_iff : ∀ (x y : Bool), (x || y) = false ↔ x = false ∧ y = false := by decide
+theorem and_eq_false_iff : ∀ (x y : Bool), (x && y) = false ↔ x = false ∨ y = false := by decide
+
+/-
+New simp rule that replaces `Bool.and_eq_false_eq_eq_false_or_eq_false` in
+Mathlib due to confluence:
+
+Consider the term: `¬((b && c) = true)`:
+
+1. Reduces to `((b && c) = false)` via `Bool.not_eq_true`
+2. Reduces to `¬(b = true ∧ c = true)` via `Bool.and_eq_true`.
+
+
+1. Further reduces to `b = false ∨ c = false` via `Bool.and_eq_false_eq_eq_false_or_eq_false`.
+2. Further reduces to `b = true → c = false` via `not_and` and `Bool.not_eq_true`.
+-/
+@[simp] theorem and_eq_false_imp : ∀ (x y : Bool), (x && y) = false ↔ (x = true → y = false) := by decide
+
+@[simp] theorem or_eq_true_iff : ∀ (x y : Bool), (x || y) = true ↔ x = true ∨ y = true := by decide
+
+@[simp] theorem or_eq_false_iff : ∀ (x y : Bool), (x || y) = false ↔ x = false ∧ y = false := by decide
+
+/-! ### eq/beq/bne -/
+
+/--
+These two rules follow trivially by simp, but are needed to avoid non-termination
+in false_eq and true_eq.
+-/
+@[simp] theorem false_eq_true : (false = true) = False := by simp
+@[simp] theorem true_eq_false : (true = false) = False := by simp
+
+-- The two lemmas below normalize terms with a constant to the
+-- right-hand side but risk non-termination if `false_eq_true` and
+-- `true_eq_false` are disabled.
+@[simp low] theorem false_eq (b : Bool) : (false = b) = (b = false) := by
+  cases b <;> simp
+
+@[simp low] theorem true_eq (b : Bool) : (true = b) = (b = true) := by
+  cases b <;> simp
+
+@[simp] theorem true_beq  : ∀b, (true  == b) =  b := by decide
+@[simp] theorem false_beq : ∀b, (false == b) = !b := by decide
+@[simp] theorem beq_true  : ∀b, (b == true)  =  b := by decide
+@[simp] theorem beq_false : ∀b, (b == false) = !b := by decide
+
+@[simp] theorem true_bne  : ∀(b : Bool), (true  != b) = !b := by decide
+@[simp] theorem false_bne : ∀(b : Bool), (false != b) =  b := by decide
+@[simp] theorem bne_true  : ∀(b : Bool), (b != true)  = !b := by decide
+@[simp] theorem bne_false : ∀(b : Bool), (b != false) =  b := by decide
+
+@[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
+
+/-
+Added for equivalence with `Bool.not_beq_self` and needed for confluence
+due to `beq_iff_eq`.
+-/
+@[simp] theorem not_eq_self : ∀(b : Bool), ((!b) = b) ↔ False := by decide
+@[simp] theorem eq_not_self : ∀(b : Bool), (b = (!b)) ↔ False := by decide
+
+@[simp] theorem beq_self_left  : ∀(a b : Bool), (a == (a == b)) = b := by decide
+@[simp] theorem beq_self_right : ∀(a b : Bool), ((a == b) == b) = a := by decide
+@[simp] theorem bne_self_left  : ∀(a b : Bool), (a != (a != b)) = b := by decide
+@[simp] theorem bne_self_right : ∀(a b : Bool), ((a != b) != b) = a := by decide
+
+@[simp] theorem not_bne_not : ∀ (x y : Bool), ((!x) != (!y)) = (x != y) := by decide
+
+@[simp] theorem bne_assoc : ∀ (x y z : Bool), ((x != y) != z) = (x != (y != z)) := by decide
+
+@[simp] theorem bne_left_inj  : ∀ (x y z : Bool), (x != y) = (x != z) ↔ y = z := by decide
+@[simp] theorem bne_right_inj : ∀ (x y z : Bool), (x != z) = (y != z) ↔ x = y := by decide
+
+/-! ### coercision related normal forms -/
+
+@[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
+
+@[simp] theorem coe_true_iff_false  : ∀(a b : Bool), (a ↔ b = false) ↔ a = (!b) := by decide
+@[simp] theorem coe_false_iff_true  : ∀(a b : Bool), (a = false ↔ b) ↔ (!a) = b := by decide
+@[simp] theorem coe_false_iff_false : ∀(a b : Bool), (a = false ↔ b = false) ↔ (!a) = (!b) := by decide
 
 /-! ### xor -/
 
-@[simp] theorem false_xor : ∀ (x : Bool), xor false x = x := by decide
+theorem false_xor : ∀ (x : Bool), xor false x = x := false_bne
 
-@[simp] theorem xor_false : ∀ (x : Bool), xor x false = x := by decide
+theorem xor_false : ∀ (x : Bool), xor x false = x := bne_false
 
-@[simp] theorem true_xor : ∀ (x : Bool), xor true x = !x := by decide
+theorem true_xor : ∀ (x : Bool), xor true x = !x := true_bne
 
-@[simp] theorem xor_true : ∀ (x : Bool), xor x true = !x := by decide
+theorem xor_true : ∀ (x : Bool), xor x true = !x := bne_true
 
-@[simp] theorem not_xor_self : ∀ (x : Bool), xor (!x) x = true := by decide
+theorem not_xor_self : ∀ (x : Bool), xor (!x) x = true := not_bne_self
 
-@[simp] theorem xor_not_self : ∀ (x : Bool), xor x (!x) = true := by decide
+theorem xor_not_self : ∀ (x : Bool), xor x (!x) = true := bne_not_self
 
 theorem not_xor : ∀ (x y : Bool), xor (!x) y = !(xor x y) := by decide
 
 theorem xor_not : ∀ (x y : Bool), xor x (!y) = !(xor x y) := by decide
 
-@[simp] theorem not_xor_not : ∀ (x y : Bool), xor (!x) (!y) = (xor x y) := by decide
+theorem not_xor_not : ∀ (x y : Bool), xor (!x) (!y) = (xor x y) := not_bne_not
 
 theorem xor_self : ∀ (x : Bool), xor x x = false := by decide
 
@@ -136,13 +255,11 @@ theorem xor_left_comm : ∀ (x y z : Bool), xor x (xor y z) = xor y (xor x z) :=
 
 theorem xor_right_comm : ∀ (x y z : Bool), xor (xor x y) z = xor (xor x z) y := by decide
 
-theorem xor_assoc : ∀ (x y z : Bool), xor (xor x y) z = xor x (xor y z) := by decide
+theorem xor_assoc : ∀ (x y z : Bool), xor (xor x y) z = xor x (xor y z) := bne_assoc
 
-@[simp]
-theorem xor_left_inj : ∀ (x y z : Bool), xor x y = xor x z ↔ y = z := by decide
+theorem xor_left_inj : ∀ (x y z : Bool), xor x y = xor x z ↔ y = z := bne_left_inj
 
-@[simp]
-theorem xor_right_inj : ∀ (x y z : Bool), xor x z = xor y z ↔ x = y := by decide
+theorem xor_right_inj : ∀ (x y z : Bool), xor x z = xor y z ↔ x = y := bne_right_inj
 
 /-! ### le/lt -/
 
@@ -227,16 +344,147 @@ theorem toNat_lt (b : Bool) : b.toNat < 2 :=
 
 @[simp] theorem toNat_eq_zero (b : Bool) : b.toNat = 0 ↔ b = false := by
   cases b <;> simp
-@[simp] theorem toNat_eq_one (b : Bool) : b.toNat = 1 ↔ b = true := by
+@[simp] theorem toNat_eq_one  (b : Bool) : b.toNat = 1 ↔ b = true := by
   cases b <;> simp
 
-end Bool
+/-! ### ite -/
+
+@[simp] theorem if_true_left  (p : Prop) [h : Decidable p] (f : Bool) :
+    (ite p true f) = (p || f) := by cases h with | _ p => simp [p]
+
+@[simp] theorem if_false_left  (p : Prop) [h : Decidable p] (f : Bool) :
+    (ite p false f) = (!p && f) := by cases h with | _ p => simp [p]
+
+@[simp] theorem if_true_right  (p : Prop) [h : Decidable p] (t : Bool) :
+    (ite p t true) = (!(p : Bool) || t) := by cases h with | _ p => simp [p]
+
+@[simp] theorem if_false_right  (p : Prop) [h : Decidable p] (t : Bool) :
+    (ite p t false) = (p && t) := by cases h with | _ p => simp [p]
+
+@[simp] theorem ite_eq_true_distrib (p : Prop) [h : Decidable p] (t f : Bool) :
+    (ite p t f = true) = ite p (t = true) (f = true) := by
+  cases h with | _ p => simp [p]
+
+@[simp] theorem ite_eq_false_distrib (p : Prop) [h : Decidable p] (t f : Bool) :
+    (ite p t f = false) = ite p (t = false) (f = false) := by
+  cases h with | _ p => simp [p]
+
+/-
+`not_ite_eq_true_eq_true` and related theorems below are added for
+non-confluence.  A motivating example is
+`¬((if u then b else c) = true)`.
+
+This reduces to:
+1. `¬((if u then (b = true) else (c = true))` via `ite_eq_true_distrib`
+2. `(if u then b c) = false)` via `Bool.not_eq_true`.
+
+Similar logic holds for `¬((if u then b else c) = false)` and related
+lemmas.
+-/
+
+@[simp]
+theorem not_ite_eq_true_eq_true (p : Prop) [h : Decidable p] (b c : Bool) :
+  ¬(ite p (b = true) (c = true)) ↔ (ite p (b = false) (c = false)) := by
+  cases h with | _ p => simp [p]
+
+@[simp]
+theorem not_ite_eq_false_eq_false (p : Prop) [h : Decidable p] (b c : Bool) :
+  ¬(ite p (b = false) (c = false)) ↔ (ite p (b = true) (c = true)) := by
+  cases h with | _ p => simp [p]
+
+@[simp]
+theorem not_ite_eq_true_eq_false (p : Prop) [h : Decidable p] (b c : Bool) :
+  ¬(ite p (b = true) (c = false)) ↔ (ite p (b = false) (c = true)) := by
+  cases h with | _ p => simp [p]
+
+@[simp]
+theorem not_ite_eq_false_eq_true (p : Prop) [h : Decidable p] (b c : Bool) :
+  ¬(ite p (b = false) (c = true)) ↔ (ite p (b = true) (c = false)) := by
+  cases h with | _ p => simp [p]
+
+/-
+Added for confluence between `if_true_left` and `ite_false_same` on
+`if b = true then True else b = true`
+-/
+@[simp] theorem eq_false_imp_eq_true : ∀(b:Bool), (b = false → b = true) ↔ (b = true) := by decide
+
+/-
+Added for confluence between `if_true_left` and `ite_false_same` on
+`if b = false then True else b = false`
+-/
+@[simp] theorem eq_true_imp_eq_false : ∀(b:Bool), (b = true → b = false) ↔ (b = false) := by decide
+
 
 /-! ### cond -/
 
-theorem cond_eq_if : (bif b then x else y) = (if b then x else y) := by
+theorem cond_eq_ite {α} (b : Bool) (t e : α) : cond b t e = if b then t else e := by
   cases b <;> simp
 
+theorem cond_eq_if : (bif b then x else y) = (if b then x else y) := cond_eq_ite b x y
+
+@[simp] theorem cond_not (b : Bool) (t e : α) : cond (!b) t e = cond b e t := by
+  cases b <;> rfl
+
+@[simp] theorem cond_self (c : Bool) (t : α) : cond c t t = t := by cases c <;> rfl
+
+/-
+This is a simp rule in Mathlib, but results in non-confluence that is
+difficult to fix as decide distributes over propositions.
+
+A possible fix would be to completely simplify away `cond`, but that
+is not taken since it could result in major rewriting of code that is
+otherwise purely about `Bool`.
+-/
+theorem cond_decide {α} (p : Prop) [Decidable p] (t e : α) :
+    cond (decide p) t e = if p then t else e := by
+  simp [cond_eq_ite]
+
+@[simp] theorem cond_eq_ite_iff (a : Bool) (p : Prop) [h : Decidable p] (x y u v : α) :
+  (cond a x y = ite p u v) ↔ ite a x y = ite p u v := by
+  simp [Bool.cond_eq_ite]
+
+@[simp] theorem ite_eq_cond_iff (p : Prop) [h : Decidable p] (a : Bool) (x y u v : α) :
+  (ite p x y = cond a u v) ↔ ite p x y = ite a u v := by
+  simp [Bool.cond_eq_ite]
+
+@[simp] theorem cond_eq_true_distrib : ∀(c t f : Bool),
+    (cond c t f = true) = ite (c = true) (t = true) (f = true) := by
+  decide
+
+@[simp] theorem cond_eq_false_distrib : ∀(c t f : Bool),
+    (cond c t f = false) = ite (c = true) (t = false) (f = false) := by decide
+
+protected theorem cond_true  {α : Type u} {a b : α} : cond true  a b = a := cond_true  a b
+protected theorem cond_false {α : Type u} {a b : α} : cond false a b = b := cond_false a b
+
+@[simp] theorem cond_true_left   : ∀(c f : Bool), cond c true f  = ( c || f) := by decide
+@[simp] theorem cond_false_left  : ∀(c f : Bool), cond c false f = (!c && f) := by decide
+@[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
+
+@[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
+
+/-# decidability -/
+
+protected theorem decide_coe (b : Bool) [Decidable (b = true)] : decide (b = true) = b := decide_eq_true
+
+@[simp] theorem decide_and (p q : Prop) [dpq : Decidable (p ∧ q)] [dp : Decidable p] [dq : Decidable q] :
+    decide (p ∧ q) = (p && q) := by
+  cases dp with | _ p => simp [p]
+
+@[simp] theorem decide_or (p q : Prop) [dpq : Decidable (p ∨ q)] [dp : Decidable p] [dq : Decidable q] :
+    decide (p ∨ q) = (p || q) := by
+  cases dp with | _ p => simp [p]
+
+@[simp] theorem decide_iff_dist (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidable p] [dq : Decidable q] :
+    decide (p ↔ q) = (decide p == decide q) := by
+  cases dp with | _ p => simp [p]
+
+end Bool
+
+export Bool (cond_eq_if)
+
 /-! ### decide -/
 
 @[simp] theorem false_eq_decide_iff {p : Prop} [h : Decidable p] : false = decide p ↔ ¬p := by

src/Init/Data/Fin/Lemmas.lean

@@ -687,7 +687,7 @@ decreasing_by decreasing_with
 
 @[simp] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :
     (reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero := by
-  rw [reverseInduction]; simp; rfl
+  rw [reverseInduction]; simp
 
 @[simp] theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
     (i : Fin n) : reverseInduction (motive := motive) zero succ (castSucc i) =

src/Init/Data/List/Lemmas.lean

@@ -69,7 +69,7 @@ theorem mem_cons_self (a : α) (l : List α) : a ∈ a :: l := .head ..
 theorem mem_cons_of_mem (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l := .tail _
 
 theorem eq_nil_iff_forall_not_mem {l : List α} : l = [] ↔ ∀ a, a ∉ l := by
-  cases l <;> simp
+  cases l <;> simp [-not_or]
 
 /-! ### append -/
 
@@ -451,9 +451,9 @@ theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
   induction as with
   | nil => simp [filter]
   | cons a as ih =>
-    by_cases h : p a <;> simp [*, or_and_right]
-    · exact or_congr_left (and_iff_left_of_imp fun | rfl => h).symm
-    · exact (or_iff_right fun ⟨rfl, h'⟩ => h h').symm
+    by_cases h : p a
+    · simp_all [or_and_left]
+    · simp_all [or_and_right]
 
 theorem filter_eq_nil {l} : filter p l = [] ↔ ∀ a, a ∈ l → ¬p a := by
   simp only [eq_nil_iff_forall_not_mem, mem_filter, not_and]

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -256,25 +256,24 @@ theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
 
 theorem testBit_one_zero : testBit 1 0 = true := by trivial
 
+theorem not_decide_mod_two_eq_one (x : Nat)
+    : (!decide (x % 2 = 1)) = decide (x % 2 = 0) := by
+  cases Nat.mod_two_eq_zero_or_one x <;> (rename_i p; simp [p])
+
 theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
     testBit (2^n - (x + 1)) i = (decide (i < n) && ! testBit x i) := by
   induction i generalizing n x with
   | zero =>
-    simp only [testBit_zero, zero_eq, Bool.and_eq_true, decide_eq_true_eq,
-      Bool.not_eq_true']
     match n with
     | 0 => simp
     | n+1 =>
-      -- just logic + omega:
-      simp only [zero_lt_succ, decide_True, Bool.true_and]
-      rw [← decide_not, decide_eq_decide]
+      simp [not_decide_mod_two_eq_one]
       omega
   | succ i ih =>
     simp only [testBit_succ]
     match n with
     | 0 =>
-      simp only [Nat.pow_zero, succ_sub_succ_eq_sub, Nat.zero_sub, Nat.zero_div, zero_testBit]
-      rw [decide_eq_false] <;> simp
+      simp [decide_eq_false]
     | n+1 =>
       rw [Nat.two_pow_succ_sub_succ_div_two, ih]
       · simp [Nat.succ_lt_succ_iff]

src/Init/PropLemmas.lean

@@ -11,6 +11,18 @@ import Init.Core
 import Init.NotationExtra
 set_option linter.missingDocs true -- keep it documented
 
+/-! ## cast and equality -/
+
+@[simp] theorem eq_mp_eq_cast  (h : α = β) : Eq.mp  h = cast h := rfl
+@[simp] theorem eq_mpr_eq_cast (h : α = β) : Eq.mpr h = cast h.symm := rfl
+
+@[simp] theorem cast_cast : ∀ (ha : α = β) (hb : β = γ) (a : α),
+    cast hb (cast ha a) = cast (ha.trans hb) a
+  | rfl, rfl, _ => rfl
+
+@[simp] theorem eq_true_eq_id : Eq True = id := by
+  funext _; simp only [true_iff, id.def, eq_iff_iff]
+
 /-! ## not -/
 
 theorem not_not_em (a : Prop) : ¬¬(a ∨ ¬a) := fun h => h (.inr (h ∘ .inl))
@@ -104,10 +116,62 @@ theorem and_or_right : (a ∧ b) ∨ c ↔ (a ∨ c) ∧ (b ∨ c) := by rw [@or
 
 theorem or_imp : (a ∨ b → c) ↔ (a → c) ∧ (b → c) :=
   Iff.intro (fun h => ⟨h ∘ .inl, h ∘ .inr⟩) (fun ⟨ha, hb⟩ => Or.rec ha hb)
-theorem not_or : ¬(p ∨ q) ↔ ¬p ∧ ¬q := or_imp
+
+/-
+`not_or` is made simp for confluence with `¬((b || c) = true)`:
+
+Critical pair:
+1. `¬(b = true ∨ c = true)` via `Bool.or_eq_true`.
+2. `(b || c = false)` via `Bool.not_eq_true` which then
+   reduces to `b = false ∧ c = false` via Mathlib simp lemma
+   `Bool.or_eq_false_eq_eq_false_and_eq_false`.
+
+Both reduce to `b = false ∧ c = false` via `not_or`.
+-/
+@[simp] theorem not_or : ¬(p ∨ q) ↔ ¬p ∧ ¬q := or_imp
 
 theorem not_and_of_not_or_not (h : ¬a ∨ ¬b) : ¬(a ∧ b) := h.elim (mt (·.1)) (mt (·.2))
 
+
+/-! ## Ite -/
+
+@[simp]
+theorem if_false_left [h : Decidable p] :
+    ite p False q ↔ ¬p ∧ q := by cases h <;> (rename_i g; simp [g])
+
+@[simp]
+theorem if_false_right [h : Decidable p] :
+    ite p q False ↔ p ∧ q := by cases h <;> (rename_i g; simp [g])
+
+/-
+`if_true_left` and `if_true_right` are lower priority because
+they introduce disjunctions and we prefer `if_false_left` and
+`if_false_right` if they overlap.
+-/
+
+@[simp low]
+theorem if_true_left [h : Decidable p] :
+    ite p True q ↔ ¬p → q := by cases h <;> (rename_i g; simp [g])
+
+@[simp low]
+theorem if_true_right [h : Decidable p] :
+    ite p q True ↔ p → q := by cases h <;> (rename_i g; simp [g])
+
+/-- Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches. -/
+@[simp] theorem dite_not [hn : Decidable (¬p)] [h : Decidable p]  (x : ¬p → α) (y : ¬¬p → α) :
+    dite (¬p) x y = dite p (fun h => y (not_not_intro h)) x := by
+  cases h <;> (rename_i g; simp [g])
+
+/-- Negation of the condition `P : Prop` in a `ite` is the same as swapping the branches. -/
+@[simp] theorem ite_not (p : Prop) [Decidable p] (x y : α) : ite (¬p) x y = ite p y x :=
+  dite_not (fun _ => x) (fun _ => y)
+
+@[simp] theorem ite_true_same (p q : Prop) [h : Decidable p] : (if p then p else q) = (¬p → q) := by
+  cases h <;> (rename_i g; simp [g])
+
+@[simp] theorem ite_false_same (p q : Prop) [h : Decidable p] : (if p then q else p) = (p ∧ q) := by
+  cases h <;> (rename_i g; simp [g])
+
 /-! ## exists and forall -/
 
 section quantifiers
@@ -268,7 +332,14 @@ end quantifiers
 
 /-! ## decidable -/
 
-theorem Decidable.not_not [Decidable p] : ¬¬p ↔ p := ⟨of_not_not, not_not_intro⟩
+@[simp] theorem Decidable.not_not [Decidable p] : ¬¬p ↔ p := ⟨of_not_not, not_not_intro⟩
+
+/-- Excluded middle.  Added as alias for Decidable.em -/
+abbrev Decidable.or_not_self := em
+
+/-- Excluded middle commuted.  Added as alias for Decidable.em -/
+theorem Decidable.not_or_self (p : Prop) [h : Decidable p] : ¬p ∨ p := by
+  cases h <;> simp [*]
 
 theorem Decidable.by_contra [Decidable p] : (¬p → False) → p := of_not_not
 
@@ -310,7 +381,7 @@ theorem Decidable.not_imp_symm [Decidable a] (h : ¬a → b) (hb : ¬b) : a :=
 theorem Decidable.not_imp_comm [Decidable a] [Decidable b] : (¬a → b) ↔ (¬b → a) :=
   ⟨not_imp_symm, not_imp_symm⟩
 
-theorem Decidable.not_imp_self [Decidable a] : (¬a → a) ↔ a := by
+@[simp] theorem Decidable.not_imp_self [Decidable a] : (¬a → a) ↔ a := by
   have := @imp_not_self (¬a); rwa [not_not] at this
 
 theorem Decidable.or_iff_not_imp_left [Decidable a] : a ∨ b ↔ (¬a → b) :=
@@ -389,8 +460,12 @@ theorem Decidable.and_iff_not_or_not [Decidable a] [Decidable b] : a ∧ b ↔
   rw [← not_and_iff_or_not_not, not_not]
 
 theorem Decidable.imp_iff_right_iff [Decidable a] : (a → b ↔ b) ↔ a ∨ b :=
-  ⟨fun H => (Decidable.em a).imp_right fun ha' => H.1 fun ha => (ha' ha).elim,
-   fun H => H.elim imp_iff_right fun hb => iff_of_true (fun _ => hb) hb⟩
+  Iff.intro
+    (fun h => (Decidable.em a).imp_right fun ha' => h.mp fun ha => (ha' ha).elim)
+    (fun ab => ab.elim imp_iff_right fun hb => iff_of_true (fun _ => hb) hb)
+
+theorem Decidable.imp_iff_left_iff  [Decidable a] : (b ↔ a → b) ↔ a ∨ b :=
+  propext (@Iff.comm (a → b) b) ▸ (@Decidable.imp_iff_right_iff a b _)
 
 theorem Decidable.and_or_imp [Decidable a] : a ∧ b ∨ (a → c) ↔ a → b ∨ c :=
   if ha : a then by simp only [ha, true_and, true_imp_iff]
@@ -435,3 +510,53 @@ protected theorem Decidable.not_forall_not {p : α → Prop} [Decidable (∃ x,
 protected theorem Decidable.not_exists_not {p : α → Prop} [∀ x, Decidable (p x)] :
     (¬∃ x, ¬p x) ↔ ∀ x, p x := by
   simp only [not_exists, Decidable.not_not]
+
+export Decidable (not_imp_self)
+
+/-
+`decide_implies` simp justification.
+
+We have a critical pair from `decide (¬(p ∧ q))`:
+
+ 1. `decide (p → ¬q)` via `not_and`
+ 2. `!decide (p ∧ q)` via `decide_not` This further refines to
+    `!(decide p) || !(decide q)` via `Bool.decide_and` (in Mathlib) and
+    `Bool.not_and` (made simp in Mathlib).
+
+We introduce `decide_implies` below and then both normalize to
+`!(decide p) || !(decide q)`.
+-/
+@[simp]
+theorem decide_implies (u v : Prop)
+    [duv : Decidable (u → v)] [du : Decidable u] {dv : u → Decidable v}
+  : decide (u → v) = dite u (fun h => @decide v (dv h)) (fun _ => true) :=
+  if h : u then by
+    simp [h]
+  else by
+    simp [h]
+
+/-
+`decide_ite` is needed to resolve critical pair with
+
+We have a critical pair from `decide (ite p b c = true)`:
+
+ 1. `ite p b c` via `decide_coe`
+ 2. `decide (ite p (b = true) (c = true))` via `Bool.ite_eq_true_distrib`.
+
+We introduce `decide_ite` so both normalize to `ite p b c`.
+-/
+@[simp]
+theorem decide_ite (u : Prop) [du : Decidable u] (p q : Prop)
+      [dpq : Decidable (ite u p q)] [dp : Decidable p] [dq : Decidable q] :
+    decide (ite u p q) = ite u (decide p) (decide q) := by
+  cases du <;> simp [*]
+
+/- Confluence for `ite_true_same` and `decide_ite`. -/
+@[simp] theorem ite_true_decide_same (p : Prop) [h : Decidable p] (b : Bool) :
+  (if p then decide p else b) = (decide p || b) := by
+  cases h <;> (rename_i pt; simp [pt])
+
+/- Confluence for `ite_false_same` and `decide_ite`. -/
+@[simp] theorem ite_false_decide_same (p : Prop) [h : Decidable p] (b : Bool) :
+  (if p then b else decide p) = (decide p && b) := by
+  cases h <;> (rename_i pt; simp [pt])

src/Init/SimpLemmas.lean

@@ -15,12 +15,15 @@ theorem of_eq_false (h : p = False) : ¬ p := fun hp => False.elim (h.mp hp)
 theorem eq_true (h : p) : p = True :=
   propext ⟨fun _ => trivial, fun _ => h⟩
 
+-- Adding this attribute needs `eq_true`.
+attribute [simp] cast_heq
+
 theorem eq_false (h : ¬ p) : p = False :=
   propext ⟨fun h' => absurd h' h, fun h' => False.elim h'⟩
 
 theorem eq_false' (h : p → False) : p = False := eq_false h
 
-theorem eq_true_of_decide {p : Prop} {_ : Decidable p} (h : decide p = true) : p = True :=
+theorem eq_true_of_decide {p : Prop} [Decidable p] (h : decide p = true) : p = True :=
   eq_true (of_decide_eq_true h)
 
 theorem eq_false_of_decide {p : Prop} {_ : Decidable p} (h : decide p = false) : p = False :=
@@ -124,6 +127,7 @@ end SimprocHelperLemmas
 @[simp] theorem not_true_eq_false : (¬ True) = False := by decide
 
 @[simp] theorem not_iff_self : ¬(¬a ↔ a) | H => iff_not_self H.symm
+attribute [simp] iff_not_self
 
 /-! ## and -/
 
@@ -173,6 +177,11 @@ theorem or_iff_left_of_imp  (hb : b → a) : (a ∨ b) ↔ a  := Iff.intro (Or.r
 @[simp] theorem or_iff_left_iff_imp  : (a ∨ b ↔ a) ↔ (b → a) := Iff.intro (·.mp ∘ Or.inr) or_iff_left_of_imp
 @[simp] theorem or_iff_right_iff_imp : (a ∨ b ↔ b) ↔ (a → b) := by rw [or_comm, or_iff_left_iff_imp]
 
+@[simp] theorem iff_self_or (a b : Prop) : (a ↔ a ∨ b) ↔ (b → a) :=
+  propext (@Iff.comm _ a) ▸ @or_iff_left_iff_imp a b
+@[simp] theorem iff_or_self (a b : Prop) : (b ↔ a ∨ b) ↔ (a → b) :=
+  propext (@Iff.comm _ b) ▸ @or_iff_right_iff_imp a b
+
 /-# Bool -/
 
 @[simp] theorem Bool.or_false (b : Bool) : (b || false) = b  := by cases b <;> rfl
@@ -199,9 +208,9 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
 @[simp] theorem Bool.not_not (b : Bool) : (!!b) = b := by cases b <;> rfl
 @[simp] theorem Bool.not_true  : (!true) = false := by decide
 @[simp] theorem Bool.not_false : (!false) = true := by decide
-@[simp] theorem Bool.not_beq_true (b : Bool) : (!(b == true)) = (b == false) := by cases b <;> rfl
+@[simp] theorem Bool.not_beq_true  (b : Bool) : (!(b == true)) = (b == false) := by cases b <;> rfl
 @[simp] theorem Bool.not_beq_false (b : Bool) : (!(b == false)) = (b == true) := by cases b <;> rfl
-@[simp] theorem Bool.not_eq_true' (b : Bool) : ((!b) = true) = (b = false) := by cases b <;> simp
+@[simp] theorem Bool.not_eq_true'  (b : Bool) : ((!b) = true) = (b = false) := by cases b <;> simp
 @[simp] theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true) := by cases b <;> simp
 
 @[simp] theorem Bool.beq_to_eq (a b : Bool) :
@@ -212,11 +221,14 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
 @[simp] theorem Bool.not_eq_true (b : Bool) : (¬(b = true)) = (b = false) := by cases b <;> decide
 @[simp] theorem Bool.not_eq_false (b : Bool) : (¬(b = false)) = (b = true) := by cases b <;> decide
 
-@[simp] theorem decide_eq_true_eq {_ : Decidable p} : (decide p = true) = p := propext <| Iff.intro of_decide_eq_true decide_eq_true
-@[simp] theorem decide_not {h : Decidable p} : decide (¬ p) = !decide p := by cases h <;> rfl
-@[simp] theorem not_decide_eq_true {h : Decidable p} : ((!decide p) = true) = ¬ p := by cases h <;> simp [decide, *]
+@[simp] theorem decide_eq_true_eq [Decidable p] : (decide p = true) = p :=
+  propext <| Iff.intro of_decide_eq_true decide_eq_true
+@[simp] theorem decide_not [g : Decidable p] [h : Decidable (Not p)] : decide (Not p) = !(decide p) := by
+  cases g <;> (rename_i gp; simp [gp]; rfl)
+@[simp] theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by
+  cases h <;> (rename_i hp; simp [decide, hp])
 
-@[simp] theorem heq_eq_eq {α : Sort u} (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq
+@[simp] theorem heq_eq_eq (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq
 
 @[simp] theorem cond_true (a b : α) : cond true a b = a := rfl
 @[simp] theorem cond_false (a b : α) : cond false a b = b := rfl
@@ -228,11 +240,29 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
 @[simp] theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by simp [bne]
 
 @[simp] theorem decide_False : decide False = false := rfl
-@[simp] theorem decide_True : decide True = true := rfl
+@[simp] theorem decide_True  : decide True  = true := rfl
 
 @[simp] theorem bne_iff_ne [BEq α] [LawfulBEq α] (a b : α) : a != b ↔ a ≠ b := by
   simp [bne]; rw [← beq_iff_eq a b]; simp [-beq_iff_eq]
 
+/-
+Added for critical pair for `¬((a != b) = true)`
+
+1. `(a != b) = false` via `Bool.not_eq_true`
+2. `¬(a ≠ b)` via `bne_iff_ne`
+
+These will both normalize to `a = b` with the first via `bne_eq_false_iff_eq`.
+-/
+@[simp] theorem beq_eq_false_iff_ne [BEq α] [LawfulBEq α]
+    (a b : α) : (a == b) = false ↔ a ≠ b := by
+  rw [ne_eq, ← beq_iff_eq a b]
+  cases a == b <;> decide
+
+@[simp] theorem bne_eq_false_iff_eq [BEq α] [LawfulBEq α] (a b : α) :
+    (a != b) = false ↔ a = b := by
+  rw [bne, ← beq_iff_eq a b]
+  cases a == b <;> decide
+
 /-# Nat -/
 
 @[simp] theorem Nat.le_zero_eq (a : Nat) : (a ≤ 0) = (a = 0) :=

src/Lean/Elab/CheckTactic.lean

@@ -7,6 +7,7 @@ prelude
 import Lean.Elab.Tactic.ElabTerm
 import Lean.Elab.Command
 import Lean.Elab.Tactic.Meta
+import Lean.Meta.CheckTactic
 
 /-!
 Commands to validate tactic results.
@@ -18,15 +19,6 @@ open Lean.Meta CheckTactic
 open Lean.Elab.Tactic
 open Lean.Elab.Command
 
-private def matchCheckGoalType (stx : Syntax) (goalType : Expr) : MetaM (Expr × Expr × Level) := do
-  let u ← mkFreshLevelMVar
-  let type ← mkFreshExprMVar (some (.sort u))
-  let val  ← mkFreshExprMVar (some type)
-  let extType := mkAppN (.const ``CheckGoalType [u]) #[type, val]
-  if !(← isDefEq goalType extType) then
-    throwErrorAt stx "Goal{indentExpr goalType}\nis expected to match {indentExpr extType}"
-  pure (val, type, u)
-
 @[builtin_command_elab Lean.Parser.checkTactic]
 def elabCheckTactic : CommandElab := fun stx => do
   let `(#check_tactic $t ~> $result by $tac) := stx | throwUnsupportedSyntax
@@ -34,11 +26,10 @@ def elabCheckTactic : CommandElab := fun stx => do
     runTermElabM $ fun _vars => do
       let u ← Lean.Elab.Term.elabTerm t none
       let type ← inferType u
-      let lvl ← mkFreshLevelMVar
-      let checkGoalType : Expr := mkApp2 (mkConst ``CheckGoalType [lvl]) type u
+      let checkGoalType ← mkCheckGoalType u type
       let mvar ← mkFreshExprMVar (.some checkGoalType)
-      let (goals, _) ← Lean.Elab.runTactic mvar.mvarId! tac.raw
       let expTerm ← Lean.Elab.Term.elabTerm result (.some type)
+      let (goals, _) ← Lean.Elab.runTactic mvar.mvarId! tac.raw
       match goals with
       | [] =>
         throwErrorAt stx
@@ -51,7 +42,6 @@ def elabCheckTactic : CommandElab := fun stx => do
       | _ => do
         throwErrorAt stx
           m!"{tac} produced multiple goals, but is expected to reduce to {indentExpr expTerm}."
-      pure ()
 
 @[builtin_command_elab Lean.Parser.checkTacticFailure]
 def elabCheckTacticFailure : CommandElab := fun stx => do
@@ -60,8 +50,7 @@ def elabCheckTacticFailure : CommandElab := fun stx => do
     runTermElabM $ fun _vars => do
       let val ← Lean.Elab.Term.elabTerm t none
       let type ← inferType val
-      let lvl ← mkFreshLevelMVar
-      let checkGoalType : Expr := mkApp2 (mkConst ``CheckGoalType [lvl]) type val
+      let checkGoalType ← mkCheckGoalType val type
       let mvar ← mkFreshExprMVar (.some checkGoalType)
       let act := Lean.Elab.runTactic mvar.mvarId! tactic.raw
       match ← try (Term.withoutErrToSorry (some <$> act)) catch _ => pure none with
@@ -73,12 +62,12 @@ def elabCheckTacticFailure : CommandElab := fun stx => do
                 pure m!"{indentExpr val}"
           let msg ←
             match gls with
-              | [] => pure m!"{tactic} expected to fail on {val}, but closed goal."
+              | [] => pure m!"{tactic} expected to fail on {t}, but closed goal."
               | [g] =>
-                pure <| m!"{tactic} expected to fail on {val}, but returned: {←ppGoal g}"
+                pure <| m!"{tactic} expected to fail on {t}, but returned: {←ppGoal g}"
               | gls =>
                 let app m g := do pure <| m ++ (←ppGoal g)
-                let init := m!"{tactic} expected to fail on {val}, but returned goals:"
+                let init := m!"{tactic} expected to fail on {t}, but returned goals:"
                 gls.foldlM (init := init) app
           throwErrorAt stx msg
 

src/Lean/Meta.lean

@@ -47,3 +47,4 @@ import Lean.Meta.CoeAttr
 import Lean.Meta.Iterator
 import Lean.Meta.LazyDiscrTree
 import Lean.Meta.LitValues
+import Lean.Meta.CheckTactic

src/Lean/Meta/CheckTactic.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix
+-/
+prelude
+import Lean.Meta.Basic
+
+namespace Lean.Meta.CheckTactic
+
+def mkCheckGoalType (val type : Expr) : MetaM Expr := do
+  let lvl ← mkFreshLevelMVar
+  pure <| mkApp2 (mkConst ``CheckGoalType [lvl]) type val
+
+def matchCheckGoalType (stx : Syntax) (goalType : Expr) : MetaM (Expr × Expr × Level) := do
+  let u ← mkFreshLevelMVar
+  let type ← mkFreshExprMVar (some (.sort u))
+  let val  ← mkFreshExprMVar (some type)
+  let extType := mkAppN (.const ``CheckGoalType [u]) #[type, val]
+  if !(← isDefEq goalType extType) then
+    throwErrorAt stx "Goal{indentExpr goalType}\nis expected to match {indentExpr extType}"
+  pure (val, type, u)
+
+end Lean.Meta.CheckTactic

tests/lean/1079.lean.expected.out

@@ -5,32 +5,4 @@
       ?a = ?a
     with
       Ordering.eq = Ordering.lt
-[Meta.Tactic.simp.unify] @forall_exists_index:1000, failed to unify
-      ∀ (h : ∃ x, ?p x), ?q h
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_eq:1000, failed to unify
-      ∀ (a : ?α), a = ?a' → ?p a
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_eq':1000, failed to unify
-      ∀ (a : ?α), ?a' = a → ?p a
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_eq_or_imp:1000, failed to unify
-      ∀ (a : ?α), a = ?a' ∨ ?q a → ?p a
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_apply_eq_imp_iff:1000, failed to unify
-      ∀ (b : ?β) (a : ?α), ?f a = b → ?p b
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_eq_apply_imp_iff:1000, failed to unify
-      ∀ (b : ?β) (a : ?α), b = ?f a → ?p b
-    with
-      False → False
-[Meta.Tactic.simp.unify] @forall_apply_eq_imp_iff₂:1000, failed to unify
-      ∀ (b : ?β) (a : ?α), ?p a → ?f a = b → ?q b
-    with
-      False → False
-[Meta.Tactic.simp.rewrite] @imp_self:1000, False → False ==> True
+[Meta.Tactic.simp.rewrite] @imp_self:10000, False → False ==> True

tests/lean/bool_simp.lean

@@ -0,0 +1,389 @@
+variable (p q : Prop)
+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 ¬(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
+#check_simp decide (ite u b c = true) ~> ite u b c
+#check_simp true ≠ (b || c) ~> b = false ∧ c = false
+#check_simp ¬((!b = false) ∧ (c = false)) ~> b = true → c = true
+#check_simp (((!b) && c) ≠ false) ~> b = false ∧ c = true
+#check_simp (cond b false c ≠ false) ~> b = false ∧ c
+#check_simp (b && c) = false ~> b → c = false
+#check_simp (b && c) ≠   false ~> b ∧ c
+#check_simp decide (u → False) ~> !decide u
+#check_simp decide (¬u) ~> !decide u
+#check_simp (b = true) ≠ (c = false) ~> b = c
+#check_simp (b != c) != (false != d) ~> b != (c != d)
+#check_simp (b == false) ≠ (c != d) ~> b = (c != d)
+#check_simp (b = true) ≠ (c = false) ~> b = c
+#check_simp ¬b = !c ~> b = c
+#check_simp (b == c) = false ~> ¬(b = c)
+#check_simp (true ≠ if u then b else c) ~> (if u then b = false else c = false)
+#check_simp (u ∧ v → False) ~> u → v → False
+#check_simp (u = (v ≠ w)) ~> (u ↔ ¬(v ↔ w))
+#check_simp ((b = false) = (c = false)) ~> (!b) = (!c)
+#check_simp True ≠ (c = false) ~> c = true
+#check_simp u ∧ u ∧ v ~> u ∧ v
+#check_simp b || (b || c) ~> b || c
+#check_simp ((b ≠ c) : Bool) ~> !(decide (b = c))
+#check_simp ((u ≠ v) : Bool) ~> !((u : Bool) == (v : Bool))
+#check_simp decide (u → False) ~> !(decide u)
+#check_simp decide (¬u) ~> !u
+-- Specific regressions done
+
+-- Round trip isomorphisms
+#check_simp (decide (b : Prop)) ~> b
+#check_simp ((u : Bool) : Prop) ~> u
+
+/- # not -/
+
+variable [Decidable u]
+
+-- Ground
+#check_simp (¬True) ~> False
+#check_simp (¬true) ~> False
+#check_simp (!True) ~> false
+#check_simp (!true) ~> false
+
+#check_simp (¬False) ~> True
+#check_simp (!False) ~> true
+#check_simp (¬false) ~> True
+#check_simp (!false) ~> true
+
+/- # Coercions and not -/
+
+#check_simp ¬p !~>
+#check_simp !b !~>
+
+#check_simp (¬u : Prop) !~>
+#check_simp (¬u : Bool) ~> !u
+#check_simp (!u : Prop) ~> ¬u
+#check_simp (!u : Bool) !~>
+#check_simp (¬b : Prop) ~> b = false
+#check_simp (¬b : Bool) ~> !b
+#check_simp (!b : Prop) ~> b = false
+#check_simp (!b : Bool) !~>
+
+#check_simp (¬¬u) ~> u
+
+/- # and -/
+
+-- Validate coercions
+#check_simp (u ∧  v : Prop) !~>
+#check_simp (u ∧  v : Bool) ~> u && v
+#check_simp (u && v : Prop) ~> u ∧  v
+#check_simp (u && v : Bool) !~>
+#check_simp (b ∧  c : Prop) !~>
+#check_simp (b ∧  c : Bool) ~> b && c
+#check_simp (b && c : Prop) ~> b ∧  c
+#check_simp (b && c : Bool) !~>
+
+-- Partial evaluation
+#check_simp (True ∧  v : Prop) ~> v
+#check_simp (True ∧  v : Bool) ~> (v : Bool)
+#check_simp (True && v : Prop) ~> v
+#check_simp (True && v : Bool) ~> (v : Bool)
+#check_simp (true ∧  c : Prop) ~> (c : Prop)
+#check_simp (true ∧  c : Bool) ~> c
+#check_simp (true && c : Prop) ~> (c : Prop)
+#check_simp (true && c : Bool) ~> c
+
+#check_simp (u ∧  True : Prop) ~> u
+#check_simp (u ∧  True : Bool) ~> (u : Bool)
+#check_simp (u && True : Prop) ~> u
+#check_simp (u && True : Bool) ~> (u : Bool)
+#check_simp (b ∧  true : Prop) ~> (b : Prop)
+#check_simp (b ∧  true : Bool) ~> b
+#check_simp (b && true : Prop) ~> (b : Prop)
+#check_simp (b && true : Bool) ~> b
+
+#check_simp (False ∧  v : Prop) ~> False
+#check_simp (False ∧  v : Bool) ~> false
+#check_simp (False && v : Prop) ~> False
+#check_simp (False && v : Bool) ~> false
+#check_simp (false ∧  c : Prop) ~> False
+#check_simp (false ∧  c : Bool) ~> false
+#check_simp (false && c : Prop) ~> False
+#check_simp (false && c : Bool) ~> false
+
+#check_simp (u ∧  False : Prop) ~> False
+#check_simp (u ∧  False : Bool) ~> false
+#check_simp (u && False : Prop) ~> False
+#check_simp (u && False : Bool) ~> false
+#check_simp (b ∧  false : Prop) ~> False
+#check_simp (b ∧  false : Bool) ~> false
+#check_simp (b && false : Prop) ~> False
+#check_simp (b && false : Bool) ~> false
+
+-- Idempotence
+#check_simp (u ∧  u) ~> u
+#check_simp (u && u) ~> (u : Bool)
+#check_simp (b ∧  b) ~> (b : Prop)
+#check_simp (b && b) ~> b
+
+-- Cancelation
+#check_simp (u ∧ ¬u)  ~> False
+#check_simp (¬u ∧ u)  ~> False
+#check_simp (b && ¬b) ~> false
+#check_simp (¬b && b) ~> false
+
+-- Check we swap operators, but do apply deMorgan etc
+#check_simp ¬(u ∧ v)  ~> u → ¬v
+#check_simp decide (¬(u ∧ v))  ~> !u || !v
+#check_simp !(u ∧ v)  ~> !u || !v
+#check_simp ¬(b ∧ c)  ~> b → c = false
+#check_simp !(b ∧ c)  ~> !b || !c
+#check_simp ¬(u && v) ~> u → ¬ v
+#check_simp ¬(b && c) ~> b = true → c = false
+#check_simp !(u && v) ~> !u || !v
+#check_simp !(b && c) ~> !b || !c
+#check_simp ¬u ∧  ¬v !~>
+#check_simp ¬b ∧  ¬c  ~> ((b = false) ∧ (c = false))
+#check_simp ¬u && ¬v  ~> (!u && !v)
+#check_simp ¬b && ¬c  ~> (!b && !c)
+
+-- Some ternary test cases
+#check_simp (u ∧ (v ∧ w) : Prop) !~>
+#check_simp (u ∧ (v ∧ w) : Bool) ~> (u && (v && w))
+#check_simp ((u ∧ v) ∧ w : Prop) !~>
+#check_simp ((u ∧ v) ∧ w : Bool)  ~> ((u && v) && w)
+#check_simp (b && (c && d) : Prop) ~> (b ∧ c ∧ d)
+#check_simp (b && (c && d) : Bool) !~>
+#check_simp ((b && c) && d : Prop)  ~> ((b ∧ c) ∧ d)
+#check_simp ((b && c) && d : Bool) !~>
+
+/- # or -/
+
+-- Validate coercions
+#check_simp p ∨ q !~>
+#check_simp q ∨ p !~>
+#check_simp (u ∨ v : Prop) !~>
+#check_simp (u ∨ v : Bool)  ~> u || v
+#check_simp (u || v : Prop) ~> u ∨  v
+#check_simp (u || v : Bool) !~>
+#check_simp (b ∨ c : Prop)  !~>
+#check_simp (b ∨ c : Bool)  ~> b || c
+#check_simp (b || c : Prop) ~> b ∨  c
+#check_simp (b || c : Bool) !~>
+
+-- Partial evaluation
+#check_simp (True ∨ v : Prop)  ~> True
+#check_simp (True ∨ v : Bool)  ~> true
+#check_simp (True || v : Prop) ~> True
+#check_simp (True || v : Bool) ~> true
+#check_simp (true ∨  c : Prop) ~> True
+#check_simp (true ∨  c : Bool) ~> true
+#check_simp (true || c : Prop) ~> True
+#check_simp (true || c : Bool) ~> true
+
+#check_simp (u ∨  True : Prop) ~> True
+#check_simp (u ∨  True : Bool) ~> true
+#check_simp (u || True : Prop) ~> True
+#check_simp (u || True : Bool) ~> true
+#check_simp (b ∨  true : Prop) ~> True
+#check_simp (b ∨  true : Bool) ~> true
+#check_simp (b || true : Prop) ~> True
+#check_simp (b || true : Bool) ~> true
+
+#check_simp (False ∨ v : Prop)  ~> v
+#check_simp (False ∨ v : Bool)  ~> (v : Bool)
+#check_simp (False || v : Prop) ~> v
+#check_simp (False || v : Bool) ~> (v : Bool)
+#check_simp (false ∨ c : Prop)  ~> (c : Prop)
+#check_simp (false ∨ c : Bool)  ~> c
+#check_simp (false || c : Prop) ~> (c : Prop)
+#check_simp (false || c : Bool) ~> c
+
+#check_simp (u ∨ False : Prop)  ~> u
+#check_simp (u ∨ False : Bool)  ~> (u : Bool)
+#check_simp (u || False : Prop) ~> u
+#check_simp (u || False : Bool) ~> (u : Bool)
+#check_simp (b ∨ false : Prop)  ~> (b : Prop)
+#check_simp (b ∨ false : Bool)  ~> b
+#check_simp (b || false : Prop) ~> (b : Prop)
+#check_simp (b || false : Bool) ~> b
+
+-- Idempotence
+#check_simp (u ∨ u)  ~> u
+#check_simp (u || u) ~> (u : Bool)
+#check_simp (b ∨  b) ~> (b : Prop)
+#check_simp (b || b) ~> b
+
+-- Complement
+-- Note. We may want to revisit this.
+--   Decidable excluded middle currently does not simplify.
+#check_simp ( u ∨  ¬u) !~>
+#check_simp (¬u ∨   u) !~>
+#check_simp ( b || ¬b)  ~> true
+#check_simp (¬b ||  b)  ~> true
+
+-- Check we swap operators, but do apply deMorgan etc
+#check_simp ¬(u ∨ v)  ~> ¬u ∧ ¬v
+#check_simp !(u ∨ v)  ~> !u && !v
+#check_simp ¬(b ∨ c)  ~> b = false ∧ c =false
+#check_simp !(b ∨ c)  ~> !b && !c
+#check_simp ¬(u || v) ~> ¬u ∧ ¬v
+#check_simp ¬(b || c) ~> b = false ∧ c = false
+#check_simp !(u || v) ~> !u && !v
+#check_simp !(b || c) ~> !b && !c
+#check_simp ¬u ∨  ¬v !~>
+#check_simp (¬b) ∨ (¬c)  ~> b = false ∨ c = false
+#check_simp ¬u || ¬v  ~> (!u || !v)
+#check_simp ¬b || ¬c  ~> (!b || !c)
+
+-- Some ternary test cases
+#check_simp (u ∨ (v ∨ w) : Prop) !~>
+#check_simp (u ∨ (v ∨ w) : Bool)   ~> (u || (v || w))
+#check_simp ((u ∨ v) ∨ w : Prop) !~>
+#check_simp ((u ∨ v) ∨ w : Bool)   ~> ((u || v) || w)
+#check_simp (b || (c || d) : Prop) ~> (b ∨ c ∨ d)
+#check_simp (b || (c || d) : Bool) !~>
+#check_simp ((b || c) || d : Prop) ~> ((b ∨ c) ∨ d)
+#check_simp ((b || c) || d : Bool) !~>
+
+/- # and/or -/
+
+-- We don't currently do automatic simplification across and/or/not
+-- This tests for non-unexpected reductions.
+
+#check_simp p ∧ (p ∨ q) !~>
+#check_simp (p ∨ q) ∧ p !~>
+
+#check_simp u ∧ (v ∨ w) !~>
+#check_simp u ∨ (v ∧ w) !~>
+#check_simp (v ∨ w) ∧ u !~>
+#check_simp (v ∧ w) ∨ u !~>
+#check_simp b && (c || d) !~>
+#check_simp b || (c && d) !~>
+#check_simp (c || d) && b !~>
+#check_simp (c && d) || b !~>
+
+/- # implication -/
+
+#check_simp (b → c) !~>
+#check_simp (u → v) !~>
+#check_simp p → q !~>
+#check_simp decide (u → ¬v)  ~> !u || !v
+
+/- # iff -/
+
+#check_simp (u = v : Prop) ~> u ↔ v
+#check_simp (u = v : Bool) ~> u == v
+#check_simp (u ↔ v : Prop) !~>
+#check_simp (u ↔ v : Bool) ~> u == v
+#check_simp (u == v : Prop) ~> u ↔ v
+#check_simp (u == v : Bool) !~>
+
+#check_simp (b = c : Prop) !~>
+#check_simp (b = c : Bool) !~>
+#check_simp (b ↔ c : Prop) ~> b = c
+#check_simp (b ↔ c : Bool) ~> decide (b = c)
+#check_simp (b == c : Prop) ~> b = c
+#check_simp (b == c : Bool) !~>
+
+-- Partial evaluation
+#check_simp (True = v : Prop)  ~> v
+#check_simp (True = v : Bool)  ~> (v : Bool)
+#check_simp (True ↔ v : Prop)  ~> v
+#check_simp (True ↔ v : Bool)  ~> (v : Bool)
+#check_simp (True == v : Prop) ~> v
+#check_simp (True == v : Bool) ~> (v : Bool)
+#check_simp (true =  c : Prop) ~> c = true
+#check_simp (true =  c : Bool) ~> c
+#check_simp (true ↔  c : Prop) ~> c = true
+#check_simp (true ↔  c : Bool) ~> c
+#check_simp (true == c : Prop) ~> (c : Prop)
+#check_simp (true == c : Bool) ~> c
+
+#check_simp (v = True : Prop)  ~> v
+#check_simp (v = True : Bool)  ~> (v : Bool)
+#check_simp (v ↔ True : Prop)  ~> v
+#check_simp (v ↔ True : Bool)  ~> (v : Bool)
+#check_simp (v == True : Prop) ~> v
+#check_simp (v == True : Bool) ~> (v : Bool)
+#check_simp (c = true : Prop) !~>
+#check_simp (c = true : Bool) ~> c
+#check_simp (c ↔ true : Prop) ~> c = true
+#check_simp (c ↔ true : Bool) ~> c
+#check_simp (c == true : Prop) ~> c = true
+#check_simp (c == true : Bool) ~> c
+
+#check_simp (True = v : Prop)  ~> v
+#check_simp (True = v : Bool)  ~> (v : Bool)
+#check_simp (True ↔ v : Prop)  ~> v
+#check_simp (True ↔ v : Bool)  ~> (v : Bool)
+#check_simp (True == v : Prop) ~> v
+#check_simp (True == v : Bool) ~> (v : Bool)
+#check_simp (true =  c : Prop) ~> c = true
+#check_simp (true =  c : Bool) ~> c
+#check_simp (true ↔  c : Prop) ~> c = true
+#check_simp (true ↔  c : Bool) ~> c
+#check_simp (true == c : Prop) ~> (c : Prop)
+#check_simp (true == c : Bool) ~> c
+
+#check_simp (v = False : Prop)  ~> ¬v
+#check_simp (v = False : Bool)  ~> !v
+#check_simp (v ↔ False : Prop)  ~> ¬v
+#check_simp (v ↔ False : Bool)  ~> !v
+#check_simp (v == False : Prop) ~> ¬v
+#check_simp (v == False : Bool) ~> !v
+#check_simp (c = false : Prop) !~>
+#check_simp (c = false : Bool) ~> !c
+#check_simp (c ↔ false : Prop) ~> c = false
+#check_simp (c ↔ false : Bool) ~> !c
+#check_simp (c == false : Prop) ~> c = false
+#check_simp (c == false : Bool) ~> !c
+
+#check_simp (False = v : Prop)  ~> ¬v
+#check_simp (False = v : Bool)  ~> !v
+#check_simp (False ↔ v : Prop)  ~> ¬v
+#check_simp (False ↔ v : Bool)  ~> !v
+#check_simp (False == v : Prop) ~> ¬v
+#check_simp (False == v : Bool) ~> !v
+#check_simp (false =  c : Prop) ~> c = false
+#check_simp (false =  c : Bool) ~> !c
+#check_simp (false ↔  c : Prop) ~> c = false
+#check_simp (false ↔  c : Bool) ~> !c
+#check_simp (false == c : Prop) ~> c = false
+#check_simp (false == c : Bool) ~> !c
+
+-- Ternary (expand these)
+
+#check_simp (u == (v =  w)) ~> u == (v == w)
+#check_simp (u == (v == w)) !~>
+
+/- # bne -/
+
+#check_simp p ≠ q ~> ¬(p ↔ q)
+#check_simp (b != c : Bool) !~>
+#check_simp ¬(p = q) ~> ¬(p ↔ q)
+#check_simp b ≠ c    ~> b ≠ c
+#check_simp ¬(b = c) !~>
+#check_simp ¬(b ↔ c) ~> ¬(b = c)
+#check_simp (b != c : Prop) ~> b ≠ c
+#check_simp u ≠ v    ~> ¬(u ↔ v)
+#check_simp ¬(u = v) ~> ¬(u ↔ v)
+#check_simp ¬(u ↔ v) !~>
+#check_simp ((u:Bool) != v : Bool) !~>
+#check_simp ((u:Bool) != v : Prop) ~> ¬(u ↔ v)
+
+/- # equality and and/or interactions -/
+
+#check_simp (u == (v ∨ w)) ~>  u == (v || w)
+#check_simp (u == (v || w)) !~>
+#check_simp ((u ∧ v) == w) ~> (u && v) == w
+
+/- # ite/cond -/
+
+#check_simp if b then c else d !~>
+#check_simp if b then p else q !~>
+#check_simp if u then p else q !~>
+#check_simp if u then b else c !~>
+#check_simp if u then u else q ~> ¬u → q
+#check_simp if u then q else u ~> u ∧ q
+#check_simp if u then q else q  ~> q
+#check_simp cond b c d !~>