feat: improve Bool normalization in grind (#7862)

This PR improves the normalization of `Bool` terms in `grind`. Recall
that `grind` currently does not case split on Boolean terms to reduce
the size of the search space.

src/Init/Grind/Norm.lean

@@ -71,6 +71,9 @@ theorem beq_eq_decide_eq {_ : BEq α} [LawfulBEq α] [DecidableEq α] (a b : α)
 theorem bne_eq_decide_not_eq {_ : BEq α} [LawfulBEq α] [DecidableEq α] (a b : α) : (a != b) = (decide (¬ a = b)) := by
   by_cases a = b <;> simp [*]
 
+theorem xor_eq (a b : Bool) : (a ^^ b) = (a != b) := by
+  rfl
+
 theorem natCast_div (a b : Nat) : (↑(a / b) : Int) = ↑a / ↑b := by
   rfl
 
@@ -86,6 +89,14 @@ theorem Int.pow_one (a : Int) : a ^ 1 = a := by
 theorem forall_true (p : True → Prop) : (∀ h : True, p h) = p True.intro :=
   propext <| Iff.intro (fun h => h True.intro) (fun h _ => h)
 
+-- Helper theorem used by the simproc `simpBoolEq`
+theorem flip_bool_eq (a b : Bool) : (a = b) = (b = a) := by
+  rw [@Eq.comm _ a b]
+
+-- Helper theorem used by the simproc `simpBoolEq`
+theorem bool_eq_to_prop (a b : Bool) : (a = b) = ((a = true) = (b = true)) := by
+  simp
+
 init_grind_norm
   /- Pre theorems -/
   not_and not_or not_ite not_forall not_exists
@@ -122,6 +133,8 @@ init_grind_norm
   Bool.and_false Bool.and_true Bool.false_and Bool.true_and Bool.and_eq_true Bool.and_assoc
   -- Bool not
   Bool.not_not
+  -- Bool xor
+  xor_eq
   -- beq
   beq_iff_eq beq_eq_decide_eq beq_self_eq_true
   -- bne

src/Lean/Meta/Tactic/Grind/SimpUtil.lean

@@ -23,6 +23,30 @@ def registerNormTheorems (preDeclNames : Array Name) (postDeclNames : Array Name
   for declName in postDeclNames do
     addSimpTheorem normExt declName (post := true) (inv := false) .global (eval_prio default)
 
+-- TODO: should we make this extensible?
+private def isBoolEqTarget (declName : Name) : Bool :=
+  declName == ``Bool.and ||
+  declName == ``Bool.or  ||
+  declName == ``Bool.not ||
+  declName == ``BEq.beq  ||
+  declName == ``decide
+
+builtin_simproc_decl simpBoolEq (@Eq Bool _ _) := fun e => do
+  let_expr f@Eq bool lhs rhs ← e | return .continue
+  let .const rhsName _ := rhs.getAppFn | return .continue
+  if rhsName == ``true || rhsName == ``false then return .continue
+  let .const lhsName _ := lhs.getAppFn | return .continue
+  if lhsName == ``true || lhsName == ``false then
+    -- Just apply comm
+    let e' := mkApp3 f bool rhs lhs
+    return .visit { expr := e', proof? := mkApp2 (mkConst ``Grind.flip_bool_eq) lhs rhs }
+  if isBoolEqTarget lhsName || isBoolEqTarget rhsName then
+    -- Convert into `(lhs = true) = (rhs = true)`
+    let tr := mkConst ``true
+    let e' ← mkEq (mkApp3 f bool lhs tr) (mkApp3 f bool rhs tr)
+    return .visit { expr := e', proof? := mkApp2 (mkConst ``Grind.bool_eq_to_prop) lhs rhs }
+  return .continue
+
 /-- Returns the array of simprocs used by `grind`. -/
 protected def getSimprocs : MetaM (Array Simprocs) := do
   let s ← Simp.getSEvalSimprocs
@@ -42,6 +66,7 @@ protected def getSimprocs : MetaM (Array Simprocs) := do
   let s := s.erase ``List.reduceReplicate
   let s ← addSimpMatchDiscrsOnly s
   let s ← addPreMatchCondSimproc s
+  let s ← s.add ``simpBoolEq (post := false)
   return #[s]
 
 /-- Returns the simplification context used by `grind`. -/

tests/lean/grind/bool.lean

@@ -1,8 +0,0 @@
-reset_grind_attrs%
-
-example [BEq α] (a b : α) : (a == b && a == b) = (a == b) := by
-  rw [Bool.eq_iff_iff]
-  grind -- succeeds
-
-example [BEq α] (a b : α) : (a == b && a == b) = (a == b) := by
-  grind -- fails

tests/lean/grind/decide.lean

@@ -1,21 +0,0 @@
----
-
-example {P Q : Prop} [Decidable P] [Decidable Q] : (decide P || decide Q) = decide (P ∨ Q) := by grind
-
----
-
-@[grind] theorem eq_head_or_mem_tail_of_mem_cons {a b : α} {l : List α} :
-    a ∈ b :: l → a = b ∨ a ∈ l := List.mem_cons.mp
-
-attribute [grind] List.mem_cons_self, List.mem_cons_of_mem
-
--- This succeeds:
-example [DecidableEq α] {l : List α} :
-    (y ∈ a :: l) = (y = a) ∨ y ∈ l := by
-  grind
-
-
--- but inserting some `decide`s fails:
-example [BEq α] [LawfulBEq α] {l : List α} :
-    decide (y ∈ a :: l) = (y == a || decide (y ∈ l)) := by
-  grind

tests/lean/run/grind_decide_bool_issues.lean

@@ -0,0 +1,31 @@
+reset_grind_attrs%
+
+example {P Q : Prop} [Decidable P] [Decidable Q] : (decide P || decide Q) = decide (P ∨ Q) := by grind
+
+@[grind] theorem eq_head_or_mem_tail_of_mem_cons {a b : α} {l : List α} :
+    a ∈ b :: l → a = b ∨ a ∈ l := List.mem_cons.mp
+
+attribute [grind] List.mem_cons_self List.mem_cons_of_mem
+
+example [DecidableEq α] {l : List α} :
+    (y ∈ a :: l) = (y = a) ∨ y ∈ l := by -- This one is not `(y ∈ a :: l) = (y = a ∨ y ∈ l)`
+  grind
+
+example [DecidableEq α] {l : List α} :
+    (y ∈ a :: l) = (y = a ∨ y ∈ l) := by
+  grind
+
+-- but inserting some `decide`s fails:
+example [BEq α] [LawfulBEq α] {l : List α} :
+    decide (y ∈ a :: l) = (y == a || decide (y ∈ l)) := by
+  grind
+
+example [BEq α] (a b : α) : (a == b && a == b) = (a == b) := by
+  rw [Bool.eq_iff_iff]
+  grind
+
+example [BEq α] (a b : α) : (a == b && a == b) = (a == b) := by
+  grind
+
+example (a b : List Nat) : (a == b && b == a) = (a == b) := by
+  grind