From 01104cc81e81cbbdabd9c860c72506654fd801c2 Mon Sep 17 00:00:00 2001
From: Joe Hendrix <joe@lean-fro.org>
Date: Mon, 4 Mar 2024 15:56:30 -0800
Subject: [PATCH] chore: bool and prop lemmas for Mathlib compatibility and
 improved confluence (#3508)

This adds a number of lemmas for simplification of `Bool` and `Prop`
terms. It pulls lemmas from Mathlib and adds additional lemmas where
confluence or consistency suggested they are needed.

It has been tested against Mathlib using some automated test
infrastructure.

That testing module is not yet included in this PR, but will be included
as part of this.

Note. There are currently some comments saying the origin of the simp
rule. These will be removed prior to merging, but are added to clarify
where the rule came from during review.

---------

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
---
 doc/examples/bintree.lean               |    7 +-
 src/Init/ByCases.lean                   |    9 -
 src/Init/Classical.lean                 |   19 +-
 src/Init/Core.lean                      |    6 +-
 src/Init/Data/Bool.lean                 |  340 ++++++-
 src/Init/Data/Fin/Lemmas.lean           |    2 +-
 src/Init/Data/List/Lemmas.lean          |    8 +-
 src/Init/Data/Nat/Bitwise/Lemmas.lean   |   13 +-
 src/Init/PropLemmas.lean                |  135 ++-
 src/Init/SimpLemmas.lean                |   46 +-
 src/Lean/Elab/CheckTactic.lean          |   25 +-
 src/Lean/Meta.lean                      |    1 +
 src/Lean/Meta/CheckTactic.lean          |   24 +
 tests/lean/1079.lean.expected.out       |   30 +-
 tests/lean/bool_simp.lean               |  389 ++++++++
 tests/lean/bool_simp.lean.expected.out  |    0
 tests/playground/bool_exhaust_test.lean | 1100 +++++++++++++++++++++++
 17 files changed, 2017 insertions(+), 137 deletions(-)
 create mode 100644 src/Lean/Meta/CheckTactic.lean
 create mode 100644 tests/lean/bool_simp.lean
 create mode 100644 tests/lean/bool_simp.lean.expected.out
 create mode 100644 tests/playground/bool_exhaust_test.lean

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