diff --git a/doc/examples/bintree.lean b/doc/examples/bintree.lean
index c1cb158bc3..1b2de5f1b6 100644
--- a/doc/examples/bintree.lean
+++ b/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
diff --git a/src/Init/ByCases.lean b/src/Init/ByCases.lean
index cf886e0ff7..75836cbaee 100644
--- a/src/Init/ByCases.lean
+++ b/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]
diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean
index ae2c589a33..0d52a62e2e 100644
--- a/src/Init/Classical.lean
+++ b/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
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 3b921fc126..d27d909ac8 100644
--- a/src/Init/Core.lean
+++ b/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
 
diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean
index be1e924300..96f0489d95 100644
--- a/src/Init/Data/Bool.lean
+++ b/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
diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean
index df3b4646ac..f97aaa9930 100644
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/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) =
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index bd1ad69203..ec5e2f8bb0 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/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]
diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 2085a2fec0..d7f7232100 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/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]
diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean
index fe5db407a8..2a7a55aa70 100644
--- a/src/Init/PropLemmas.lean
+++ b/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])
diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean
index e822093420..852bfb7a09 100644
--- a/src/Init/SimpLemmas.lean
+++ b/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) :=
diff --git a/src/Lean/Elab/CheckTactic.lean b/src/Lean/Elab/CheckTactic.lean
index 1f3b554c4e..0fc3faeb49 100644
--- a/src/Lean/Elab/CheckTactic.lean
+++ b/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
 
diff --git a/src/Lean/Meta.lean b/src/Lean/Meta.lean
index 12a09c44c7..02c39e2de6 100644
--- a/src/Lean/Meta.lean
+++ b/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
diff --git a/src/Lean/Meta/CheckTactic.lean b/src/Lean/Meta/CheckTactic.lean
new file mode 100644
index 0000000000..d346ec3508
--- /dev/null
+++ b/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
diff --git a/tests/lean/1079.lean.expected.out b/tests/lean/1079.lean.expected.out
index f40dfe5257..2ae8133d49 100644
--- a/tests/lean/1079.lean.expected.out
+++ b/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
diff --git a/tests/lean/bool_simp.lean b/tests/lean/bool_simp.lean
new file mode 100644
index 0000000000..c9ac09b34b
--- /dev/null
+++ b/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 !~>
diff --git a/tests/lean/bool_simp.lean.expected.out b/tests/lean/bool_simp.lean.expected.out
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/tests/playground/bool_exhaust_test.lean b/tests/playground/bool_exhaust_test.lean
new file mode 100644
index 0000000000..181fb965ee
--- /dev/null
+++ b/tests/playground/bool_exhaust_test.lean
@@ -0,0 +1,1100 @@
+import Lean.Elab.Command
+import Lean.Elab.Tactic.ElabTerm
+import Lean.Elab.Tactic.Meta
+import Lean.Meta.CheckTactic
+import Lean.Parser.Term
+
+open Lean Lean.Meta Lean.Elab Lean.Elab.Term Lean.Elab.Command
+open Lean.Meta.CheckTactic
+
+
+-- | A `Op` is a first order operation for generating values with a given type.
+structure Op (tp : Type) (val : Type) where
+  args : Array tp
+  result : tp
+  apply : Array val → val
+ deriving Inhabited
+
+def mkOp (args : List tp) (result : tp) (apply : Array val → val) : Op tp val :=
+  { apply := apply, args := args.toArray, result }
+
+def Op.map (op : Op x val) (f : x → y) : Op y val :=
+  { apply := op.apply, args := op.args.map f, result := f op.result }
+
+class HasType (val : Type) (type : outParam Type) where
+  typeOf : val → type
+
+class Value (val : Type) where
+  render : val → TermElabM Term
+
+/--
+Contextual information needed to generate terms.
+-/
+structure GenCtx (val : Type) where
+  -- Maps type indices to operator for corresponding type.
+  -- Types use type indices.
+  ops : Array (Array (Op Nat val))
+  /- Operators to use for patterns at top of terms -/
+  topOps : Array (Op Nat val)
+  /-- Maximum term size -/
+  maxTermSize : Nat
+  /-- Maximum depth of terms -/
+  maxDepth : Nat
+  /-- Maximum number of variables -/
+  maxVarCount : Nat
+  /- Local context variables defined in -/
+  lctx : LocalContext
+  /- Local instances for variables -/
+  linst : LocalInstances
+  /-- Maps type indices to variables for that type. -/
+  vars : Array (Array val)
+
+namespace GenCtx
+
+/-- `var ctx tp idx` returns a term denoting `i`th variable with type `tp`. -/
+def var (ctx : GenCtx val) (tp : Nat) (idx : Nat) : Option val :=
+  if g : tp < ctx.vars.size then
+    let a := ctx.vars[tp]'g
+    if h : idx < a.size then
+      some (a[idx]'h)
+    else
+      none
+  else
+    none
+
+end GenCtx
+
+/-- An operator together with a set of terms to apply to it. -/
+structure PartialApp (term : Type) where
+  /-- Operator to generate -/
+  op : Op Nat term
+  /-- Terms constructed so far -/
+  terms : Array term
+
+namespace PartialApp
+
+def fromOp (op : Op Nat term) : PartialApp term :=
+  { op, terms := .mkEmpty op.args.size }
+
+end PartialApp
+
+/--
+A partial term contains the initial part of a term as constructed from a
+left-to-right preorder traversal.
+
+It stores additional information needed to ensure the ultimate term satisfies
+the generation constraints on term size and number of variables.
+
+The operations for constructing this ensures the term is well-formed
+with respect to the signature and is not a complete term.
+-/
+structure PartialTerm (term : Type) where
+  /-- Stack of partially built term (must be non-empty) -/
+  termStack : Array (PartialApp term)
+  /-- Maximum number of additional operations that may be added. -/
+  remTermSize : Nat
+  /-- Variables used with type index. -/
+  usedVars : Array Nat
+  deriving Inhabited
+
+namespace PartialTerm
+
+/--
+Create an initial partial term from an operator.
+
+If the operator is a constant, then this just returns a complete terms.
+-/
+def init (maxTermSize : Nat) (maxDepth : Nat) (op : Op Nat term) : term ⊕ PartialTerm term :=
+  if op.args.isEmpty then
+    .inl (op.apply #[])
+  else
+    .inr {
+      termStack := #[PartialApp.fromOp op],
+      remTermSize := maxTermSize - (1 + op.args.size),
+      usedVars := #[]
+    }
+
+partial def push (p : PartialTerm term) (t : term) : term ⊕ PartialTerm term :=
+  match p.termStack.back? with
+  | none => .inl t
+  | some { op, terms } =>
+    let p := { p with termStack := p.termStack.pop }
+    let terms := terms.push t
+    if terms.size = op.args.size then
+      let v := op.apply terms
+      push p v
+    else
+      .inr { p with termStack := p.termStack.push { op, terms } }
+
+/-- Push an operator to the stack -/
+def pushOp (p : PartialTerm term) (op : Op Nat term) : PartialTerm term :=
+  { termStack   := p.termStack.push (.fromOp op)
+    remTermSize := p.remTermSize - op.args.size,
+    usedVars := p.usedVars
+  }
+
+end PartialTerm
+
+/--
+Term generator
+-/
+structure Gen (term : Type) where
+  sofar : Array term := #[]
+  pending : Array (PartialTerm term) := #[]
+  deriving Inhabited
+
+namespace Gen
+
+/-- Return true if generator will return no more terms. -/
+def isEmpty (s: Gen term) : Bool := s.sofar.isEmpty && s.pending.isEmpty
+
+def pop (s : Gen term) : Option (Nat × PartialTerm term × Gen term) :=
+  if s.pending.isEmpty then
+    .none
+  else
+    let { sofar, pending } := s
+    let next := pending.back
+    let pending := pending.pop
+    match next.termStack.back? with
+    | none =>
+      panic! "Term stack empty"
+    | some app =>
+      let tp := app.op.args[app.terms.size]!
+      some (tp, next, { sofar, pending })
+
+/- `push s next v` adds the result of `next.push v` to the state. -/
+def push (s : Gen term) (next : PartialTerm term) (v : term) : Gen term :=
+  let { sofar, pending } := s
+  match next.push v with
+  | .inl v => { sofar := sofar.push v, pending }
+  | .inr next => { sofar, pending := pending.push next }
+
+def pushOp (s : Gen term) (ctx : GenCtx term) (next : PartialTerm term) (op : Op Nat term) :=
+  if op.args.isEmpty then
+    s.push next (op.apply #[])
+  else if op.args.size ≤ next.remTermSize ∧ next.termStack.size + 1 < ctx.maxDepth then
+    { s with pending := s.pending.push (next.pushOp op) }
+  else
+    s
+
+def add (s : Gen term) (val : term ⊕ PartialTerm term) : Gen term :=
+  let { sofar, pending } := s
+  match val with
+  | .inl v => { sofar := sofar.push v, pending }
+  | .inr p => { sofar, pending := pending.push p }
+
+/-- Create state that will explore all terms in context -/
+def addOpInstances (s : Gen term) (ctx : GenCtx term) (op : Op Nat term) : Gen term :=
+  s.add (PartialTerm.init ctx.maxTermSize ctx.maxDepth op)
+
+/-- Create state that will explore all terms in context -/
+def init (ctx : GenCtx term) : Gen term :=
+  ctx.topOps.foldl (init := {}) (·.addOpInstances ctx ·)
+
+end Gen
+
+/--
+Generate terms until we reach the limit.
+-/
+partial
+def generateTerms
+    (ctx : GenCtx term)
+    (s : Gen term)
+    (limit : Nat := 0) :
+    Array term × Gen term :=
+  if limit > 0 ∧ s.sofar.size ≥ limit then
+    (s.sofar, { s with sofar := #[] })
+  else
+    match s.pop with
+    | none => (s.sofar, { s with sofar := #[] })
+    | some (tp, next, s) =>
+      let addVar (next : PartialTerm term) (i : Nat) (s : Gen term) : Gen term :=
+            if next.usedVars[i]! = tp then
+              match ctx.var tp i with
+              | some v => s.push next v
+              | none => s
+            else
+              s
+      let s := next.usedVars.size.fold (init := s) (addVar next)
+      let s :=
+        let var := next.usedVars.size
+        if var < ctx.maxVarCount then
+          let next := { next with usedVars := next.usedVars.push tp }
+          addVar next var s
+        else
+          s
+      generateTerms ctx (ctx.ops[tp]!.foldl (init := s) (·.pushOp ctx next ·))
+
+/-
+`addScopeVariables` extends the local context and instances with a copy of the
+variables in the scope (which must be non-empty).
+-/
+def addScopeVariables (lctx : LocalContext) (linst : LocalInstances) (scope : Scope) (idx : Nat) :
+    CoreM (LocalContext × LocalInstances × Ident) := do
+  let act := Term.elabBindersEx scope.varDecls fun vars => do pure (vars, ← (read : MetaM Meta.Context))
+  let mctx := { lctx := lctx, localInstances := linst }
+  let (((vars, mctx), _tstate), _mstate) ← act |>.run |>.run mctx
+  if vars.isEmpty then
+    throwError "No variables declared"
+  let fv := vars[0]!.snd |>.fvarId!
+  let rec drop (nm : Name) :=
+        match nm with
+        | .str .anonymous s => pure (.str .anonymous s!"{s}{idx}")
+        | .str nm _ => drop nm
+        | .num nm _ => drop nm
+        | .anonymous => throwError "Anonymous variable declared."
+  let nm ← drop (mctx.lctx.get! fv |>.userName)
+  let lctx := mctx.lctx.setUserName fv nm
+  pure (lctx, mctx.localInstances, mkIdent nm)
+
+def addVariables (cmdCtx : Command.Context) (cmdState : Command.State) (lctx : LocalContext) (linst : LocalInstances) (n : Nat) (cmd : Command) :
+    CoreM (LocalContext × LocalInstances × Array Ident) := do
+  let (_, s) ←  elabCommand cmd.raw |>.run cmdCtx |>.run cmdState
+  let scope := s.scopes.head!
+  Nat.foldM (n := n) (init := (lctx, linst, .mkEmpty n)) fun i (lctx, linst, a) => do
+    let (lctx, linst, ident) ← addScopeVariables lctx linst scope i
+    pure (lctx, linst, a.push ident)
+
+structure VarDecl (tp : Type) where
+  idx : Nat
+  ident : TSyntax `ident
+  type : tp
+  deriving Inhabited, Repr
+
+instance : BEq (VarDecl tp) where
+  beq x y := x.idx == y.idx
+
+instance : Hashable (VarDecl tp) where
+  hash v := hash v.idx
+
+structure GenStats where
+  maxTermSize : Nat := 9
+  maxDepth : Nat := 3
+  maxVarCount : Nat := 3
+
+def mkCtx [BEq tp] [Hashable tp]
+    (types : Array tp)
+    (ops : List (Op tp val))
+    (varGen : List (tp × CoreM Command))
+    (mkVar : VarDecl tp → val)
+    (stats : GenStats)
+    (topOps : List (Op tp val) := ops) : CommandElabM (GenCtx val) := do
+  let typeMap : HashMap tp Nat := Nat.fold (n := types.size) (init := {}) fun i s =>
+        if p : i < types.size then
+          s.insert types[i] i
+        else
+          s
+  let typeFn (t : tp) := typeMap.findD t 0
+  let addOp (a : Array (Array (Op Nat val))) (op : Op tp val) :=
+        let op := op.map typeFn
+        a.modify op.result (·.push op)
+  let init := Array.ofFn (n := types.size) (fun _ => #[])
+  let ops := ops.foldl (init := init) addOp
+  let ops := ops.map (·.reverse)
+  let topOps := topOps.toArray.map (·.map typeFn)
+  let (lctx, linst, vars) ← liftCoreM do
+    let coreCtx ← read
+    let coreState ← get
+    let fileName := coreCtx.fileName
+    let fileMap  := coreCtx.fileMap
+    let env := coreState.env
+    let maxRecDepth := coreCtx.maxRecDepth
+    let cmdCtx : Command.Context := { fileName, fileMap, tacticCache? := none }
+    let cmdState : Command.State := { env, maxRecDepth }
+    let addVars (p : LocalContext × LocalInstances × Array (Array val))
+                (q : tp × CoreM Command) :
+                CoreM (LocalContext × LocalInstances × _) := do
+          let (lctx, linst, a) := p
+          let (type, gen) := q
+          let cmd ← gen
+          let (lctx, linst, vars) ← addVariables cmdCtx cmdState lctx linst stats.maxVarCount cmd
+          let vars := Array.ofFn (n := vars.size) fun j => mkVar { idx := j.val, ident := vars[j], type }
+          let type := typeFn type
+          pure (lctx, linst, a.modify type (fun _ => vars))
+    let vars := Array.ofFn (n := types.size) fun _ => #[]
+    varGen.foldlM (init := ({}, {}, vars)) addVars
+  let maxTermSize : Nat := stats.maxTermSize
+  let maxDepth : Nat := stats.maxDepth
+  let maxVarCount : Nat := stats.maxVarCount
+  pure { ops, topOps, maxTermSize, maxDepth, maxVarCount, lctx, linst, vars }
+
+def runTests [BEq tp] [HasType val tp] [Value val] (stx : Syntax) (simp : val → val)(tac : Syntax.Tactic) (terms : Array val)
+      : TermElabM Unit := do
+  for tm in terms do
+    if ← IO.checkCanceled then
+      -- should never be visible to users!
+      throw <| Exception.error .missing "Testing interrupted"
+    let res := simp tm
+    let t ← Value.render tm
+    if HasType.typeOf tm != HasType.typeOf res then
+      throwErrorAt stx m!"simp spec for {t} did not preserve type."
+    withoutModifyingEnv $ do
+      let exp ← Value.render res
+      let u ← Lean.Elab.Term.elabTerm t none
+      let type ← inferType u
+      let checkGoalType ← mkCheckGoalType u type
+      let expTerm ← Lean.Elab.Term.elabTerm exp (some type)
+      let mvar ← mkFreshExprMVar (.some checkGoalType)
+      let (goals, _) ← Lean.Elab.runTactic mvar.mvarId! tac.raw
+      match goals with
+      | [next] => do
+        let (val, _, _) ← matchCheckGoalType stx (←next.getType)
+        if !(← Meta.withReducible <| isDefEq val expTerm) then
+          logErrorAt stx
+            m!"{indentExpr u} reduces to{indentExpr val}\nbut is expected to reduce to {indentExpr expTerm}"
+      | [] =>
+        logErrorAt stx
+          m!"{tac} closed goal, but is expected to reduce to {indentExpr expTerm}."
+      | _ => do
+        logErrorAt stx
+          m!"{tac} produced multiple goals, but is expected to reduce to {indentExpr expTerm}."
+
+private def mkCoreContext (ctx : Command.Context) (options : Options) (maxRecDepth : Nat) (initHeartbeats : Nat) : Core.Context :=
+  { fileName       := ctx.fileName
+    fileMap        := ctx.fileMap
+    options,
+    currRecDepth   := ctx.currRecDepth
+    maxRecDepth,
+    ref            := ctx.ref
+    initHeartbeats,
+    currMacroScope := ctx.currMacroScope }
+
+/-- Runs term elaborator in base context. -/
+def runTermElabM (cctx : Core.Context) (cstate : Core.State) (mctx : Meta.Context) (act : TermElabM Unit)
+    : BaseIO (Except Exception MessageLog) := do
+  let r ← act.run |>.run mctx |>.run cctx cstate |>.toBaseIO
+  match r with
+  | .error e =>
+    pure (.error e)
+  | .ok ((((), _termS), _metaS), coreS) =>
+    pure (.ok coreS.messages)
+
+partial
+def runGen [BEq tp] [Hashable tp] [HasType term tp] [Value term]
+
+      (stx : Syntax) (simp : term → term)
+      (varGen : List (tp × CoreM Command))
+      (mkVar : VarDecl tp → term)
+      (stats : GenStats)
+      (types : Array tp)
+      (ops : List (Op tp term))
+      (tac : Syntax.Tactic)
+      (topOps : List (Op tp term) := ops)
+      (concurrent : Bool := true) : CommandElabM Unit := do
+
+  let ctx ← mkCtx (types := types) (ops := ops) (topOps := topOps) (varGen := varGen) (mkVar := mkVar) (stats := stats)
+
+  let lctx := ctx.lctx
+  let linst := ctx.linst
+
+  let cmdCtx : Command.Context ← read
+  let s ← get
+  let ngen := s.ngen
+  let env := s.env
+  let maxRecDepth := s.maxRecDepth
+  let heartbeats ← IO.getNumHeartbeats
+  let options ← getOptions
+  let cctx := mkCoreContext cmdCtx options maxRecDepth heartbeats
+  let cstate : Core.State := { env := env, ngen := ngen, infoState.enabled := false }
+  let mctx : Meta.Context := { lctx := lctx, localInstances := linst }
+  let gen := Gen.init ctx
+  if concurrent then
+    let limit := 400
+    let rec loop (gen : Gen term) (tasks : Array (Task (Except Exception MessageLog))) := do
+      if gen.isEmpty then
+        return tasks
+      else
+        IO.println s!"Writing task"
+        let (terms, gen) := generateTerms ctx gen (limit := limit)
+        let t ← runTests stx simp tac terms |> runTermElabM cctx cstate mctx |>.asTask
+        loop gen (tasks.push t)
+    let tasks ←
+      profileitM Exception "simptest.launch" ({} : Options) (decl := .anonymous) do
+        loop gen #[]
+
+    profileitM Exception "simptest.execute" {} do
+      for i in [0:tasks.size] do
+        if ← IO.checkCanceled then
+          break
+        let act := tasks[i]!
+        match act.get with
+        | .error e =>
+          -- Cancel all tasks after this one
+          (tasks |>.toSubarray (start := i+1) |>.forM IO.cancel : BaseIO Unit)
+          throw e
+        | .ok m =>
+          modify fun s => { s with messages := s.messages ++ m }
+  else
+    let r ← runTermElabM cctx cstate mctx <|
+      let (terms, _) := generateTerms ctx gen
+      runTests stx simp tac terms
+    match r with
+    | .error e => throw e
+    | .ok m => modify fun s => { s with messages := s.messages ++ m }
+
+/-
+
+This file runs many tests on simp and other operations on Boolean/Prop
+values.
+
+It is intended to systematically evaluate simp strategies on different
+operators.
+
+Note. These tests use the simp tactic not necessarily because simp is
+the best strategy for these particular examples, but rather simp may
+wind up needing to discharge conditions during rewriting, and we need
+tests showing that is has generally effective and predictable --
+behavior.
+
+General goals for simp are that the normal forms are sensible to a wide
+range of users and that it performs well.  We also strive for Mathlib
+compatiblity.
+-/
+
+inductive BoolType where
+  | prop
+  | bool
+  deriving BEq, DecidableEq, Hashable, Inhabited, Repr
+
+inductive EqOp where
+  | eqProp
+  | eqBool
+  | iffProp
+  | beqBool
+  deriving BEq, Repr
+
+def EqOp.argType (op : EqOp) : BoolType :=
+  match op with
+  | .eqProp  | .iffProp => .prop
+  | .beqBool | .eqBool => .bool
+
+def EqOp.resultType (op : EqOp) : BoolType :=
+  match op with
+  | .eqProp | .eqBool | .iffProp => .prop
+  | .beqBool => .bool
+
+inductive NeOp where
+  | neProp
+  | neBool
+  | bneBool
+  deriving BEq, Repr
+
+def NeOp.argType (op : NeOp) : BoolType :=
+  match op with
+  | .neProp  => .prop
+  | .neBool | .bneBool => .bool
+
+def NeOp.resultType (op : NeOp) : BoolType :=
+  match op with
+  | .neProp | .neBool  => .prop
+  | .bneBool => .bool
+
+inductive IteOp where
+  | iteProp
+  | iteBool
+  | diteProp
+  | diteBool
+  | condBool
+  deriving BEq, Repr
+
+def IteOp.condType (op : IteOp) : BoolType :=
+  match op with
+  | .iteProp | .diteProp | .iteBool | .diteBool => .prop
+  | .condBool => .bool
+
+def IteOp.resultType (op : IteOp) : BoolType :=
+  match op with
+  | .iteProp | .diteProp => .prop
+  | .iteBool | .diteBool | .condBool => .bool
+
+/--
+A first order term representing a `Bool` or `Prop` Lean expression
+constructed from the operators described in the module header.
+
+This groups operations that perform the same semantic function into the
+same constructor while providing an operator type that identifies the
+particular form of it.
+-/
+inductive BoolVal where
+  | trueVal (tp : BoolType)
+  | falseVal (tp : BoolType)
+  | var (d : VarDecl BoolType)
+    /--
+    `(t : Prop)` when `t` is a `Bool`.
+
+    Equivalent to `t = true`.
+    -/
+  | boolToProp (t : BoolVal)
+    /-- `decide t` is the same as `p : Bool` -/
+  | decide (t : BoolVal)
+  | not (x   : BoolVal) (tp : BoolType)
+  | and (x y : BoolVal) (tp : BoolType)
+  | or  (x y : BoolVal) (tp : BoolType)
+  | implies (x y : BoolVal)
+  | eq (x y : BoolVal) (op : EqOp)
+  | ne (x y : BoolVal) (op : NeOp)
+  | ite (c t f : BoolVal) (op : IteOp)
+  deriving BEq, Inhabited, Repr
+
+namespace BoolVal
+
+def typeOf (v : BoolVal) : BoolType :=
+  match v with
+  | .trueVal tp => tp
+  | .falseVal tp => tp
+  | .var d => d.type
+  | .decide _ => .bool
+  | .boolToProp _ => .prop
+  | .not _ tp => tp
+  | .and _ _ tp => tp
+  | .or  _ _ tp => tp
+  | .implies _ _ => .prop
+  | .eq _ _ op => op.resultType
+  | .ne _ _ op => op.resultType
+  | .ite _ _ _ op => op.resultType
+
+def render [Monad M] [MonadQuotation M] (v : BoolVal) : M Term :=
+  match v with
+  | .var d => do pure d.ident
+  | .trueVal .bool  => `(true)
+  | .trueVal .prop  => `(True)
+  | .falseVal .bool => `(false)
+  | .falseVal .prop => `(False)
+  | .boolToProp t => do `(term| ($(←t.render) : Prop))
+  | .decide t => do `(term| ($(←t.render) : Bool))
+  | .not x .bool => do `(term| !$(←x.render))
+  | .not x .prop => do `(term| ¬$(←x.render))
+  | .and x y .bool => do `(term| $(←x.render) && $(←y.render))
+  | .and x y .prop => do `(term| $(←x.render) ∧  $(←y.render))
+  | .or  x y .bool => do `(term| $(←x.render) || $(←y.render))
+  | .or  x y .prop => do `(term| $(←x.render) ∨  $(←y.render))
+  | .implies x y => do `(term| $(←x.render) → $(←y.render))
+  | .eq x y .eqProp | .eq x y .eqBool => do `(term| $(←x.render) = $(←y.render))
+  | .eq x y .iffProp => do `(term| $(←x.render) ↔ $(←y.render))
+  | .eq x y .beqBool => do `(term| $(←x.render) == $(←y.render))
+  | .ne x y .neProp | .ne x y .neBool => do `(term| $(←x.render) ≠ $(←y.render))
+  | .ne x y .bneBool => do `(term| $(←x.render) != $(←y.render))
+  | .ite c t f op =>
+    match op with
+    | .iteProp | .iteBool => do
+    `(term| if $(←c.render) then $(←t.render) else $(←f.render))
+    | .diteProp | .diteBool => do
+    `(term| if h : $(←c.render) then $(←t.render) else $(←f.render))
+    | .condBool => do
+      `(term| bif $(←c.render) then $(←t.render) else $(←f.render))
+
+def map (f : BoolVal -> BoolVal) (v : BoolVal) : BoolVal :=
+  match v with
+  | .trueVal _ | .falseVal _ | .var _ => v
+  | .boolToProp t => .boolToProp (f t)
+  | .decide t => .decide (f t)
+  | .not x tp   => .not (f x) tp
+  | .and x y tp   => .and (f x) (f y) tp
+  | .or  x y tp   => .or  (f x) (f y) tp
+  | .implies x y => .implies (f x) (f y)
+  | .eq x y op => .eq (f x) (f y) op
+  | .ne x y op => .ne (f x) (f y) op
+  | .ite c x y op => .ite (f c) (f x) (f y) op
+
+
+def trueProp  : BoolVal := .trueVal .prop
+def falseProp : BoolVal := .falseVal .prop
+def trueBool  : BoolVal := .trueVal .bool
+def falseBool : BoolVal := .falseVal .bool
+
+local prefix:75 "~ " => fun t => BoolVal.not t (BoolVal.typeOf t)
+local infix:40 "=v " => fun (x y : BoolVal) =>
+  BoolVal.eq x y (match BoolVal.typeOf x with
+            | .prop => EqOp.eqProp
+            | .bool => EqOp.eqBool)
+instance : AndOp BoolVal where
+  and x y := BoolVal.and x y (BoolVal.typeOf x)
+instance : OrOp BoolVal where
+  or x y  := BoolVal.or x y (BoolVal.typeOf x)
+
+section
+
+@[match_pattern]
+def iff (x y : BoolVal) : BoolVal := .eq x y .iffProp
+
+@[match_pattern]
+def eq_true (x : BoolVal) : BoolVal := .eq x (.trueVal .bool) .eqBool
+
+@[match_pattern]
+def eq_false (x : BoolVal) : BoolVal := .eq x (.falseVal .bool) .eqBool
+
+def toBool (v : BoolVal) : BoolVal :=
+  match v.typeOf with
+  | .prop => .decide v
+  | .bool => v
+
+def toProp (v : BoolVal) : BoolVal :=
+  match v.typeOf with
+  | .prop => v
+  | .bool => eq_true v
+
+def coerceType (v : BoolVal) (type : BoolType) : BoolVal :=
+  match v.typeOf, type with
+  | .prop, .bool => .decide v
+  | .bool, .prop => eq_true v
+  | _, _ => v
+
+
+/--
+Returns true if we should consider `x` a complement of `y`.
+
+Symmetric so also holds if `y` is a complement of `x`.
+-/
+def isComplement (x y : BoolVal) : Bool :=
+  match x, y with
+  | .not x _, y => x == y
+  | x, .not y _ => x == y
+  | .eq a b _, .ne c d _ => a.typeOf == c.typeOf && a == b && c == d
+  | .ne a b _, .eq c d _ => a.typeOf == c.typeOf && a == b && c == d
+  | eq_true x, eq_false y => x == y
+  | eq_false x, eq_true y => x == y
+  | _, _ => false
+
+
+def resolveEq (thunks : List (term → term → Option term)) (x y : term) : Option term :=
+  match thunks with
+  | [] => none
+  | fn :: thunks =>
+    match fn x y with
+    | none => resolveEq thunks x y
+    | some r => some r
+
+/--
+Returns true if we should consider `x` a complement of `y`.
+
+Symmetric so also holds if `y` is a complement of `x`.
+-/
+def isOrComplement (x y : BoolVal) (tp : BoolType) : Bool :=
+  match x, y, tp with
+  | .not x _, y, .bool => x == y
+  | x, .not y _, .bool => x == y
+  | .eq a b _, .ne c d _, _ => a.typeOf == c.typeOf && a == b && c == d
+  | .ne a b _, .eq c d _, _ => a.typeOf == c.typeOf && a == b && c == d
+  | eq_true x, eq_false y, _ => x == y
+  | eq_false x, eq_true y, _ => x == y
+  | _, _, _ => false
+
+partial def simp (v : BoolVal) : BoolVal :=
+  let v := map simp v
+  match v with
+  | .boolToProp b => simp <| eq_true b
+  | .decide p =>
+      match p with
+      | .trueVal  _ => .trueVal  .bool
+      | .falseVal _ => .falseVal .bool
+      | .var _ => v
+      | .boolToProp _ => panic! "Expected boolToProp to simplify away"
+      | .not x _   => simp <| ~(.decide x)
+      | .and x y _ => simp <| (.decide x) &&& (.decide y)
+      | .or x y _  => simp <| (.decide x) ||| (.decide y)
+      | .implies p q => simp <| ~(.decide p) ||| (.decide q)
+      | .eq x y .eqBool =>
+        match y with
+        | .trueVal _ => x
+        | .falseVal _ => simp (~ x)
+        | _ => v
+      | .eq x y .eqProp | iff x y =>
+        simp <| .eq (.decide x) (.decide y) .beqBool
+      | .ne _ _ op =>
+        match op with
+        | .neProp | .neBool => panic! "Expected ne to be reduced to not eq"
+        | .bneBool => panic! "Unexpected bool"
+      | .ite c t f op =>
+        match op with
+        | .iteProp => simp <| .ite c (.decide t) (.decide f) .iteBool
+        | _ => v
+      | .decide _ | .eq _ _ _ =>
+        panic! s!"Unexpected prop {repr p} when bool expected."
+  | .not t _ =>
+    match t with
+    | .trueVal tp => .falseVal tp
+    | .falseVal tp => .trueVal tp
+    | .not t _ => t
+    | .and x y .prop => simp <| .implies x (.not y .prop)
+    | .and x y .bool => simp <| .or (.not x .bool) (.not y .bool) .bool
+    | .or x y  tp    => simp <| .and (.not x tp) (.not y tp) tp
+    | .implies x y => simp <| .and x (.not y .prop) .prop
+    | .eq b (.trueVal  .bool) .eqBool => .eq b (.falseVal .bool) .eqBool
+    | .eq b (.falseVal .bool) .eqBool => .eq b (.trueVal  .bool) .eqBool
+    | .eq b (.not c .bool) .eqBool => simp <| .eq b c .eqBool
+    | .eq (.not b .bool) c .eqBool => simp <| .eq b c .eqBool
+    | .ne b c .neBool  => .eq b c .eqBool
+    | .ite c t f .iteProp =>
+        match t, f with
+        | eq_true  t, eq_true  f => .ite c (eq_false t) (eq_false f) .iteProp
+        | eq_true  t, eq_false f => .ite c (eq_false t) (eq_true  f) .iteProp
+        | eq_false t, eq_true  f => .ite c (eq_true t)  (eq_false f) .iteProp
+        | eq_false t, eq_false f => .ite c (eq_true t)  (eq_true  f) .iteProp
+        | _, _ => v
+    | _ => v
+  | .and x y tp => Id.run do
+      if let .trueVal _ := x then
+        return y
+      if let .falseVal _ := x then
+        return x
+      if let .trueVal _ := y then
+        return x
+      if let .falseVal _ := y then
+        return y
+      if let .and _xl xr _ := x then
+        if xr == y then return x
+      if let .and yl _yr _ := y then
+        if x == yl then return y
+      if x == y then
+        return x
+      else if isComplement x y then
+        return .falseVal tp
+      else
+        return v
+  | .or x y tp => Id.run do
+      -- Hardcoded for and-or-imp special case
+      if let .and x1 x2 .prop := x then
+        if let .implies y1 y2 := y then
+          if x1 == y1 then
+            return (simp <| .implies x1 (.or x2 y2 .prop))
+      if let .falseVal _ := x then
+        return y
+      if let .trueVal _ := x then
+        return x
+      if let .falseVal _ := y then
+        return x
+      if let .trueVal _ := y then
+        return y
+      if let .or _xl xr _ := x then
+        if xr == y then return x
+      if let .or yl _yr _ := y then
+        if x == yl then return y
+      if x == y then
+        return x
+      if isOrComplement x y tp then
+          return .trueVal tp
+      pure v
+  | .implies x y =>
+    match x, y with
+    | .trueVal _, y => y
+    | .falseVal _, _ => .trueVal .prop
+    | _, .trueVal _ => y
+    | _, .falseVal _ => simp <| .not x .prop
+    | .and a b _, y => simp <| .implies a (.implies b y)
+    | x, y => Id.run <| do
+      if x == y then
+        return (.trueVal .prop)
+      if let eq_true b := x then
+        if let eq_false c := y then
+          if b == c then
+            return y
+      if let eq_false b := x then
+        if let eq_true c := y then
+          if b == c then
+            return y
+      if let .not x _ := x then
+        if x == y then
+          return x
+      if let .not yn _ := y then
+        if x == yn then
+          return y
+
+      return v
+  | .eq (.trueVal _) y op =>
+    match y with
+    | .falseVal _ => .falseVal op.resultType
+    | .trueVal _ => .trueVal op.resultType
+    | _ =>
+      match op with
+      | .eqBool => simp <| .eq y (.trueVal .bool) .eqBool
+      | .eqProp | .iffProp | .beqBool => y
+  | .eq (.falseVal tp) y op =>
+    match y with
+    | .trueVal  _ => .falseVal op.resultType
+    | .falseVal _ => .trueVal  op.resultType
+    | _ =>
+      match op with
+      | .eqBool =>
+        simp <| eq_false y
+      | _ =>
+        simp <| .not y tp
+  | .eq x (.trueVal .bool) .eqBool =>
+    (match x with
+    | .trueVal _ | .falseVal _ | .implies _ _ | .boolToProp _ =>
+      panic! "Unexpected term."
+    | .var _ => v
+    | .decide t => t
+    | .not x _   => simp <| eq_false x
+    | .and x y _  => simp <| eq_true x &&& eq_true y
+    | .or x y _   => simp <| eq_true x ||| eq_true y
+    | .eq x y .beqBool => simp <| .eq x y .eqBool
+    | .ne x y .bneBool => simp <| .ne x y .neBool
+    | .ite c t f op =>
+      (match op with
+      | .iteBool | .condBool =>
+        simp <| .ite (coerceType c .prop) (eq_true t) (eq_true f) .iteProp
+      | .diteBool => panic! "expected dite to simplify away."
+      | _ => panic! "Unexpected prop when bool expected.")
+    | .eq _ _ _ | .ne _ _ _ =>
+        panic! "Unexpected prop when bool expected.")
+  | .eq x (.trueVal _) _op => x
+  | .eq x (.falseVal _) .eqBool  =>
+    match x with
+    | .trueVal _ | .falseVal _ | .implies _ _ | .boolToProp _ =>
+      panic! "Unexpected term."
+    | .var _ => v
+    | .decide t =>
+      simp <| .not t .prop
+    | .not x _   =>
+      simp <| .eq x (.trueVal .bool) .eqBool
+    | .and x y _ => simp <| .implies (eq_true x) (eq_false y)
+    | .or  x y _ => simp <| .and (eq_false x) (eq_false y) .prop
+    | .eq x y .beqBool => simp <| .not (.eq x y .eqBool) .prop
+    | .ne x y .bneBool => simp <| .eq x y .eqBool
+    | .ite c t f _ =>
+      simp <| .ite (coerceType c .prop) (eq_false t) (eq_false f) .iteProp
+    | .eq _ _ _ | .ne _ _ _ =>
+        panic! "Unexpected prop when bool expected."
+   -- N.B. bool ops other than .eqBool do not change type.
+  | .eq x y op => Id.run do
+    if let .falseVal tp := y then
+      return simp (.not x tp)
+    if x == y then
+      return (.trueVal op.resultType)
+    if isComplement x y then
+      return (.falseVal op.resultType)
+    if let .beqBool := op then
+      if let .eq x1 x2 .beqBool := x then
+        if x2 == y then
+          return x1
+      if let .eq y1 y2 .beqBool := y then
+        if x == y1 then
+          return y2
+    match op with
+    | .eqProp | .iffProp | .eqBool =>
+      let checks : List (BoolVal → BoolVal → Option BoolVal) := [
+        fun x y =>
+          if let .and x1 x2 _ := x then
+            if x1 == y then
+              some <| .implies (toProp y) (toProp x2)
+            else if x2 == y then
+              some <| .implies (toProp y) (toProp x1)
+            else none
+          else none,
+        fun x y =>
+          if let .and y1 y2 _ := y then
+            if x == y1 then
+              some <| .implies (toProp x) (toProp y2)
+            else if x == y2 then
+              some <| .implies (toProp x) (toProp y1)
+            else none
+          else none,
+        fun x y =>
+          if let .or x1 x2 _ := x then
+            if x1 == y then
+              some <| .implies (toProp x2) (toProp y)
+            else if x2 == y then
+              some <| .implies (toProp x1) (toProp y)
+            else none
+          else none,
+        fun x y =>
+          if let .or y1 y2 _ := y then
+            if x == y1 then
+              some <| .implies (toProp y2) (toProp x)
+            else if x == y2 then
+              some <| .implies (toProp y1) (toProp x)
+            else none
+          else none,
+        fun x y =>
+          if let .or x1 x2 _ := x then
+            if x1 == y then
+              some <| .implies (toProp x2) (toProp y)
+            else if x2 == y then
+              some <| .implies (toProp x1) (toProp y)
+            else none
+          else none,
+        fun x y =>
+          if let .implies x1 x2 := x then
+            if x2 == y then
+              pure <| .or x1 y .prop
+            else none
+          else none,
+        fun x y =>
+          if let .implies y1 y2 := y then
+            if x == y2 then
+              pure <| .or y1 x .prop
+            else none
+          else none
+      ]
+      match resolveEq checks x y with
+      | some r => return (simp r)
+      | none => pure ()
+    | _ =>
+      pure ()
+    match op with
+    | .eqProp | .iffProp =>
+      match x, y with
+      -- The cases below simplify the bool to prop normal forms (b = true, b = false) while
+      -- avoiding distributing not over the normal form.
+      | eq_true  x, eq_true  y => simp <| .eq x y .eqBool
+      | eq_false x, eq_false y => simp <| .eq (~ x) (~ y) .eqBool
+      | eq_true  x, eq_false y => simp <| .eq x (~ y) .eqBool
+      | eq_false x, eq_true  y => simp <| .eq (~ x) y .eqBool
+      | _, _ => iff x y
+    | .eqBool =>
+      match x, y with
+      | .decide x, .decide y => iff x y
+      | _, _ => v
+    | .beqBool => v
+  | .ne x y op => Id.run do
+    if let .neBool := op then
+      return simp (.not (.eq x y .eqBool) .prop)
+    if let .neProp := op then
+      return simp (.not (.eq x y .eqProp) .prop)
+    if let .trueVal _ := x then
+      return simp (~y)
+    if let .falseVal _ := x then
+      return y
+    if let .trueVal _ := y then
+      return simp (~x)
+    if let .falseVal _ := y then
+      return x
+    if x == y then
+      return .falseVal .bool
+    if isComplement x y then
+      return .trueVal .bool
+    if let .ne y1 y2 .bneBool := y then
+      if x == y1 then
+        return y2
+    pure <|
+      match x, y with
+      | .ne a b .bneBool, c => simp <| .ne a (.ne b c .bneBool) .bneBool
+      | .not x _, .not y _ =>  simp <| .ne x y .bneBool
+      | _, _ => v
+  | .ite c t f op => Id.run do
+    if let .trueVal _ := c then
+      return t
+    if let .falseVal _ := c then
+      return f
+    if let .not c _ := c then
+      return simp <| .ite c f t op
+    if let .falseVal tp := t then
+      return simp <| (~(coerceType c tp)) &&& f
+    if let .falseVal tp := f then
+      return simp <| (coerceType c tp) &&& t
+    -- NB. The patterns where a branch is true are
+    -- intentionally after branches with a
+    -- false because we prefer to introduce conjunction
+    -- over disjunction/implies when overlapping.
+    if let .trueVal _ := t then
+      let r :=
+        match op with
+        | .iteBool => simp <| toBool c ||| f
+        | .iteProp => simp <| .implies (~c) f
+        | .condBool => simp <|  c ||| f
+        | _ => v
+      return r
+    if let .trueVal _ := f then
+      let r :=
+        match op with
+        | .iteBool  => simp <| ~(toBool c) ||| t
+        | .iteProp  => simp <| .implies c t
+        | .condBool => simp <| ~c ||| t
+        | _ => v
+      return r
+    if t == f then
+      return t
+    let matchProp c x :=
+          match op with
+          | .iteBool =>
+              if let .decide x := x then
+                if c == x then
+                  some (toBool c)
+                else
+                  none
+              else
+                none
+          | .iteProp | .condBool => if c == x then some c else none
+          | _ => none
+    if let some c := matchProp c t then
+      let r :=
+        match f.typeOf with
+        | .bool => simp <| c ||| f
+        | .prop => simp <| .implies (.not c .prop) f
+      return r
+    if let some c := matchProp c f then
+      return simp <| c &&& t
+    let op := match op with
+              | .diteProp => .iteProp
+              | .diteBool => .iteBool
+              | _ => op
+    .ite c t f op
+  | .trueVal _ | .falseVal _ | .var _ => v
+end
+set_option profiler false
+
+end BoolVal
+
+instance : HasType BoolVal BoolType where
+  typeOf val := val.typeOf
+
+instance : Value BoolVal where
+  render val := val.render
+
+section
+open BoolVal BoolType
+
+def trueOp  (tp : BoolType) := mkOp [] tp fun _ => trueVal  tp
+def falseOp (tp : BoolType) := mkOp [] tp fun _ => falseVal tp
+def boolToPropOp := mkOp [.bool] prop fun a => boolToProp (a[0]!)
+def propToBoolOp := mkOp [prop] bool fun a => BoolVal.decide (a[0]!)
+
+def notOp (tp : BoolType) := mkOp [tp] tp fun a => not (a[0]!) tp
+def andOp (tp : BoolType) := mkOp [tp, tp] tp fun a => and (a[0]!) (a[1]!) tp
+def orOp  (tp : BoolType) := mkOp [tp, tp] tp fun a => or  (a[0]!) (a[1]!) tp
+def impliesOp := mkOp [.prop, .prop] prop fun a => implies  (a[0]!) (a[1]!)
+def eqOp  (op : EqOp)  :=
+  mkOp [op.argType, op.argType] op.resultType fun a => eq (a[0]!) (a[1]!) op
+def neOp  (op : NeOp)  :=
+  mkOp [op.argType, op.argType] op.resultType fun a => ne (a[0]!) (a[1]!) op
+def iteOp (op : IteOp) :=
+  let rtp := op.resultType
+  mkOp [op.condType, rtp, rtp] rtp fun a => ite (a[0]!) (a[1]!) (a[2]!) op
+
+end
+
+def mkBoolDecl : CoreM Command := `(variable (b : Bool))
+def mkDecidablePropDecl : CoreM Command := `(variable (p : Prop) [Decidable p])
+
+syntax:lead (name := boolTestElab) "#boolTest" : command
+
+@[command_elab boolTestElab]
+def elabGenTest : CommandElab := fun stx => do
+  let baseOps := [
+      trueOp  .bool,  trueOp .prop,
+      falseOp .bool, falseOp .prop,
+      boolToPropOp, propToBoolOp,
+      notOp .bool, notOp .prop,
+      andOp .bool, andOp .prop,
+      orOp .bool,  orOp .prop,
+      impliesOp
+  ]
+  let eqOps := [ eqOp .eqProp, eqOp .eqBool, eqOp .iffProp, eqOp .beqBool ]
+  let neOps := [ neOp .neProp, neOp .neBool, neOp .bneBool ]
+  let iteOps := [
+    iteOp .iteProp, iteOp .iteBool,
+    --iteOp .diteProp,  iteOp .diteBool,
+    iteOp .condBool
+  ]
+  let types := #[.prop, .bool]
+  let ops := baseOps ++ eqOps ++ neOps ++ iteOps
+  let varGen : List (BoolType × CoreM Command) := [
+      (.bool, mkBoolDecl),
+      (.prop, mkDecidablePropDecl)
+  ]
+  let stats : GenStats := { maxTermSize := 7, maxDepth := 3, maxVarCount := 2 }
+  let tac : Syntax.Tactic ← `(tactic|try simp)
+  runGen stx BoolVal.simp varGen BoolVal.var stats types ops (topOps := ops) tac
+
+set_option maxHeartbeats 10000000
+#boolTest