feat: Bool.and, Bool.or, and Bool.not propagation in grind (#…

…6861)

This PR adds propagation rules for `Bool.and`, `Bool.or`, and `Bool.not`
to the `grind` tactic.

src/Init/Grind/Lemmas.lean

@@ -69,6 +69,37 @@ theorem eq_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a = b) = a := by s
 theorem eq_congr  {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = a₂) (h₂ : b₁ = b₂) : (a₁ = b₁) = (a₂ = b₂) := by simp [*]
 theorem eq_congr' {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = b₂) (h₂ : b₁ = a₂) : (a₁ = b₁) = (a₂ = b₂) := by rw [h₁, h₂, Eq.comm (a := a₂)]
 
+/-! Bool.and -/
+
+theorem Bool.and_eq_of_eq_true_left {a b : Bool} (h : a = true) : (a && b) = b := by simp [h]
+theorem Bool.and_eq_of_eq_true_right {a b : Bool} (h : b = true) : (a && b) = a := by simp [h]
+theorem Bool.and_eq_of_eq_false_left {a b : Bool} (h : a = false) : (a && b) = false := by simp [h]
+theorem Bool.and_eq_of_eq_false_right {a b : Bool} (h : b = false) : (a && b) = false := by simp [h]
+
+theorem Bool.eq_true_of_and_eq_true_left {a b : Bool} (h : (a && b) = true) : a = true := by simp_all
+theorem Bool.eq_true_of_and_eq_true_right {a b : Bool} (h : (a && b) = true) : b = true := by simp_all
+
+/-! Bool.or -/
+
+theorem Bool.or_eq_of_eq_true_left {a b : Bool} (h : a = true) : (a || b) = true := by simp [h]
+theorem Bool.or_eq_of_eq_true_right {a b : Bool} (h : b = true) : (a || b) = true := by simp [h]
+theorem Bool.or_eq_of_eq_false_left {a b : Bool} (h : a = false) : (a || b) = b := by simp [h]
+theorem Bool.or_eq_of_eq_false_right {a b : Bool} (h : b = false) : (a || b) = a := by simp [h]
+theorem Bool.eq_false_of_or_eq_false_left {a b : Bool} (h : (a || b) = false) : a = false := by
+  cases a <;> simp_all
+theorem Bool.eq_false_of_or_eq_false_right {a b : Bool} (h : (a || b) = false) : b = false := by
+  cases a <;> simp_all
+
+/-! Bool.not -/
+
+theorem Bool.not_eq_of_eq_true {a : Bool} (h : a = true) : (!a) = false := by simp [h]
+theorem Bool.not_eq_of_eq_false {a : Bool} (h : a = false) : (!a) = true := by simp [h]
+theorem Bool.eq_false_of_not_eq_true {a : Bool} (h : (!a) = true) : a = false := by simp_all
+theorem Bool.eq_true_of_not_eq_false {a : Bool} (h : (!a) = false) : a = true := by simp_all
+
+theorem Bool.false_of_not_eq_self {a : Bool} (h : (!a) = a) : False := by
+  by_cases a <;> simp_all
+
 /- The following two helper theorems are used to case-split `a = b` representing `iff`. -/
 theorem of_eq_eq_true {a b : Prop} (h : (a = b) = True) : (¬a ∨ b) ∧ (¬b ∨ a) := by
   by_cases a <;> by_cases b <;> simp_all

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

@@ -27,16 +27,16 @@ builtin_grind_propagator propagateAndUp ↑And := fun e => do
   let_expr And a b := e | return ()
   if (← isEqTrue a) then
     -- a = True → (a ∧ b) = b
-    pushEq e b <| mkApp3 (mkConst ``Lean.Grind.and_eq_of_eq_true_left) a b (← mkEqTrueProof a)
+    pushEq e b <| mkApp3 (mkConst ``Grind.and_eq_of_eq_true_left) a b (← mkEqTrueProof a)
   else if (← isEqTrue b) then
     -- b = True → (a ∧ b) = a
-    pushEq e a <| mkApp3 (mkConst ``Lean.Grind.and_eq_of_eq_true_right) a b (← mkEqTrueProof b)
+    pushEq e a <| mkApp3 (mkConst ``Grind.and_eq_of_eq_true_right) a b (← mkEqTrueProof b)
   else if (← isEqFalse a) then
     -- a = False → (a ∧ b) = False
-    pushEqFalse e <| mkApp3 (mkConst ``Lean.Grind.and_eq_of_eq_false_left) a b (← mkEqFalseProof a)
+    pushEqFalse e <| mkApp3 (mkConst ``Grind.and_eq_of_eq_false_left) a b (← mkEqFalseProof a)
   else if (← isEqFalse b) then
     -- b = False → (a ∧ b) = False
-    pushEqFalse e <| mkApp3 (mkConst ``Lean.Grind.and_eq_of_eq_false_right) a b (← mkEqFalseProof b)
+    pushEqFalse e <| mkApp3 (mkConst ``Grind.and_eq_of_eq_false_right) a b (← mkEqFalseProof b)
 
 /--
 Propagates truth values downwards for a conjunction `a ∧ b` when the
@@ -46,8 +46,8 @@ builtin_grind_propagator propagateAndDown ↓And := fun e => do
   if (← isEqTrue e) then
     let_expr And a b := e | return ()
     let h ← mkEqTrueProof e
-    pushEqTrue a <| mkApp3 (mkConst ``Lean.Grind.eq_true_of_and_eq_true_left) a b h
-    pushEqTrue b <| mkApp3 (mkConst ``Lean.Grind.eq_true_of_and_eq_true_right) a b h
+    pushEqTrue a <| mkApp3 (mkConst ``Grind.eq_true_of_and_eq_true_left) a b h
+    pushEqTrue b <| mkApp3 (mkConst ``Grind.eq_true_of_and_eq_true_right) a b h
 
 /--
 Propagates equalities for a disjunction `a ∨ b` based on the truth values
@@ -63,16 +63,16 @@ builtin_grind_propagator propagateOrUp ↑Or := fun e => do
   let_expr Or a b := e | return ()
   if (← isEqFalse a) then
     -- a = False → (a ∨ b) = b
-    pushEq e b <| mkApp3 (mkConst ``Lean.Grind.or_eq_of_eq_false_left) a b (← mkEqFalseProof a)
+    pushEq e b <| mkApp3 (mkConst ``Grind.or_eq_of_eq_false_left) a b (← mkEqFalseProof a)
   else if (← isEqFalse b) then
     -- b = False → (a ∨ b) = a
-    pushEq e a <| mkApp3 (mkConst ``Lean.Grind.or_eq_of_eq_false_right) a b (← mkEqFalseProof b)
+    pushEq e a <| mkApp3 (mkConst ``Grind.or_eq_of_eq_false_right) a b (← mkEqFalseProof b)
   else if (← isEqTrue a) then
     -- a = True → (a ∨ b) = True
-    pushEqTrue e <| mkApp3 (mkConst ``Lean.Grind.or_eq_of_eq_true_left) a b (← mkEqTrueProof a)
+    pushEqTrue e <| mkApp3 (mkConst ``Grind.or_eq_of_eq_true_left) a b (← mkEqTrueProof a)
   else if (← isEqTrue b) then
     -- b = True → (a ∧ b) = True
-    pushEqTrue e <| mkApp3 (mkConst ``Lean.Grind.or_eq_of_eq_true_right) a b (← mkEqTrueProof b)
+    pushEqTrue e <| mkApp3 (mkConst ``Grind.or_eq_of_eq_true_right) a b (← mkEqTrueProof b)
 
 /--
 Propagates truth values downwards for a disjuction `a ∨ b` when the
@@ -82,8 +82,8 @@ builtin_grind_propagator propagateOrDown ↓Or := fun e => do
   if (← isEqFalse e) then
     let_expr Or a b := e | return ()
     let h ← mkEqFalseProof e
-    pushEqFalse a <| mkApp3 (mkConst ``Lean.Grind.eq_false_of_or_eq_false_left) a b h
-    pushEqFalse b <| mkApp3 (mkConst ``Lean.Grind.eq_false_of_or_eq_false_right) a b h
+    pushEqFalse a <| mkApp3 (mkConst ``Grind.eq_false_of_or_eq_false_left) a b h
+    pushEqFalse b <| mkApp3 (mkConst ``Grind.eq_false_of_or_eq_false_right) a b h
 
 /--
 Propagates equalities for a negation `Not a` based on the truth value of `a`.
@@ -96,12 +96,12 @@ builtin_grind_propagator propagateNotUp ↑Not := fun e => do
   let_expr Not a := e | return ()
   if (← isEqFalse a) then
     -- a = False → (Not a) = True
-    pushEqTrue e <| mkApp2 (mkConst ``Lean.Grind.not_eq_of_eq_false) a (← mkEqFalseProof a)
+    pushEqTrue e <| mkApp2 (mkConst ``Grind.not_eq_of_eq_false) a (← mkEqFalseProof a)
   else if (← isEqTrue a) then
     -- a = True → (Not a) = False
-    pushEqFalse e <| mkApp2 (mkConst ``Lean.Grind.not_eq_of_eq_true) a (← mkEqTrueProof a)
+    pushEqFalse e <| mkApp2 (mkConst ``Grind.not_eq_of_eq_true) a (← mkEqTrueProof a)
   else if (← isEqv e a) then
-    closeGoal <| mkApp2 (mkConst ``Lean.Grind.false_of_not_eq_self) a (← mkEqProof e a)
+    closeGoal <| mkApp2 (mkConst ``Grind.false_of_not_eq_self) a (← mkEqProof e a)
 
 /--
 Propagates truth values downwards for a negation expression `Not a` based on the truth value of `Not a`.
@@ -113,19 +113,19 @@ This function performs the following:
 builtin_grind_propagator propagateNotDown ↓Not := fun e => do
   let_expr Not a := e | return ()
   if (← isEqFalse e) then
-    pushEqTrue a <| mkApp2 (mkConst ``Lean.Grind.eq_true_of_not_eq_false) a (← mkEqFalseProof e)
+    pushEqTrue a <| mkApp2 (mkConst ``Grind.eq_true_of_not_eq_false) a (← mkEqFalseProof e)
   else if (← isEqTrue e) then
-    pushEqFalse a <| mkApp2 (mkConst ``Lean.Grind.eq_false_of_not_eq_true) a (← mkEqTrueProof e)
+    pushEqFalse a <| mkApp2 (mkConst ``Grind.eq_false_of_not_eq_true) a (← mkEqTrueProof e)
   else if (← isEqv e a) then
-    closeGoal <| mkApp2 (mkConst ``Lean.Grind.false_of_not_eq_self) a (← mkEqProof e a)
+    closeGoal <| mkApp2 (mkConst ``Grind.false_of_not_eq_self) a (← mkEqProof e a)
 
 /-- Propagates `Eq` upwards -/
 builtin_grind_propagator propagateEqUp ↑Eq := fun e => do
   let_expr Eq _ a b := e | return ()
   if (← isEqTrue a) then
-    pushEq e b <| mkApp3 (mkConst ``Lean.Grind.eq_eq_of_eq_true_left) a b (← mkEqTrueProof a)
+    pushEq e b <| mkApp3 (mkConst ``Grind.eq_eq_of_eq_true_left) a b (← mkEqTrueProof a)
   else if (← isEqTrue b) then
-    pushEq e a <| mkApp3 (mkConst ``Lean.Grind.eq_eq_of_eq_true_right) a b (← mkEqTrueProof b)
+    pushEq e a <| mkApp3 (mkConst ``Grind.eq_eq_of_eq_true_right) a b (← mkEqTrueProof b)
   else if (← isEqv a b) then
     pushEqTrue e <| mkEqTrueCore e (← mkEqProof a b)
   let aRoot ← getRootENode a
@@ -223,4 +223,64 @@ builtin_grind_propagator propagateDecideUp ↑decide := fun e => do
   else if (← isEqFalse p) then
     pushEq e (← getBoolFalseExpr) <| mkApp3 (mkConst ``Grind.decide_eq_false) p h (← mkEqFalseProof p)
 
+/-- `Bool` version of `propagateAndUp` -/
+builtin_grind_propagator propagateBoolAndUp ↑Bool.and := fun e => do
+  let_expr Bool.and a b := e | return ()
+  if (← isEqBoolTrue a) then
+    pushEq e b <| mkApp3 (mkConst ``Grind.Bool.and_eq_of_eq_true_left) a b (← mkEqBoolTrueProof a)
+  else if (← isEqBoolTrue b) then
+    pushEq e a <| mkApp3 (mkConst ``Grind.Bool.and_eq_of_eq_true_right) a b (← mkEqBoolTrueProof b)
+  else if (← isEqBoolFalse a) then
+    pushEqBoolFalse e <| mkApp3 (mkConst ``Grind.Bool.and_eq_of_eq_false_left) a b (← mkEqBoolFalseProof a)
+  else if (← isEqBoolFalse b) then
+    pushEqBoolFalse e <| mkApp3 (mkConst ``Grind.Bool.and_eq_of_eq_false_right) a b (← mkEqBoolFalseProof b)
+
+/-- `Bool` version of `propagateAndDown` -/
+builtin_grind_propagator propagateBoolAndDown ↓Bool.and := fun e => do
+  if (← isEqBoolTrue e) then
+    let_expr Bool.and a b := e | return ()
+    let h ← mkEqBoolTrueProof e
+    pushEqBoolTrue a <| mkApp3 (mkConst ``Grind.Bool.eq_true_of_and_eq_true_left) a b h
+    pushEqBoolTrue b <| mkApp3 (mkConst ``Grind.Bool.eq_true_of_and_eq_true_right) a b h
+
+/-- `Bool` version of `propagateOrUp` -/
+builtin_grind_propagator propagateBoolOrUp ↑Bool.or := fun e => do
+  let_expr Bool.or a b := e | return ()
+  if (← isEqBoolFalse a) then
+    pushEq e b <| mkApp3 (mkConst ``Grind.Bool.or_eq_of_eq_false_left) a b (← mkEqBoolFalseProof a)
+  else if (← isEqBoolFalse b) then
+    pushEq e a <| mkApp3 (mkConst ``Grind.Bool.or_eq_of_eq_false_right) a b (← mkEqBoolFalseProof b)
+  else if (← isEqBoolTrue a) then
+    pushEqBoolTrue e <| mkApp3 (mkConst ``Grind.Bool.or_eq_of_eq_true_left) a b (← mkEqBoolTrueProof a)
+  else if (← isEqBoolTrue b) then
+    pushEqBoolTrue e <| mkApp3 (mkConst ``Grind.Bool.or_eq_of_eq_true_right) a b (← mkEqBoolTrueProof b)
+
+/-- `Bool` version of `propagateOrDown` -/
+builtin_grind_propagator propagateBoolOrDown ↓Bool.or := fun e => do
+  if (← isEqBoolFalse e) then
+    let_expr Bool.or a b := e | return ()
+    let h ← mkEqBoolFalseProof e
+    pushEqBoolFalse a <| mkApp3 (mkConst ``Grind.Bool.eq_false_of_or_eq_false_left) a b h
+    pushEqBoolFalse b <| mkApp3 (mkConst ``Grind.Bool.eq_false_of_or_eq_false_right) a b h
+
+/-- `Bool` version of `propagateNotUp` -/
+builtin_grind_propagator propagateBoolNotUp ↑Bool.not := fun e => do
+  let_expr Bool.not a := e | return ()
+  if (← isEqBoolFalse a) then
+    pushEqBoolTrue e <| mkApp2 (mkConst ``Grind.Bool.not_eq_of_eq_false) a (← mkEqBoolFalseProof a)
+  else if (← isEqBoolTrue a) then
+    pushEqBoolFalse e <| mkApp2 (mkConst ``Grind.Bool.not_eq_of_eq_true) a (← mkEqBoolTrueProof a)
+  else if (← isEqv e a) then
+    closeGoal <| mkApp2 (mkConst ``Grind.Bool.false_of_not_eq_self) a (← mkEqProof e a)
+
+/-- `Bool` version of `propagateNotDown` -/
+builtin_grind_propagator propagateBoolNotDown ↓Bool.not := fun e => do
+  let_expr Bool.not a := e | return ()
+  if (← isEqBoolFalse e) then
+    pushEqBoolTrue a <| mkApp2 (mkConst ``Grind.Bool.eq_true_of_not_eq_false) a (← mkEqBoolFalseProof e)
+  else if (← isEqBoolTrue e) then
+    pushEqBoolFalse a <| mkApp2 (mkConst ``Grind.Bool.eq_false_of_not_eq_true) a (← mkEqBoolTrueProof e)
+  else if (← isEqv e a) then
+    closeGoal <| mkApp2 (mkConst ``Grind.Bool.false_of_not_eq_self) a (← mkEqProof e a)
+
 end Lean.Meta.Grind

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

@@ -570,13 +570,19 @@ def getGeneration (e : Expr) : GoalM Nat := do
 
 /-- Returns `true` if `e` is in the equivalence class of `True`. -/
 def isEqTrue (e : Expr) : GoalM Bool := do
-  let n ← getENode e
-  return isSameExpr n.root (← getTrueExpr)
+  return isSameExpr (← getENode e).root (← getTrueExpr)
 
 /-- Returns `true` if `e` is in the equivalence class of `False`. -/
 def isEqFalse (e : Expr) : GoalM Bool := do
-  let n ← getENode e
-  return isSameExpr n.root (← getFalseExpr)
+  return isSameExpr (← getENode e).root (← getFalseExpr)
+
+/-- Returns `true` if `e` is in the equivalence class of `Bool.true`. -/
+def isEqBoolTrue (e : Expr) : GoalM Bool := do
+  return isSameExpr (← getENode e).root (← getBoolTrueExpr)
+
+/-- Returns `true` if `e` is in the equivalence class of `Bool.false`. -/
+def isEqBoolFalse (e : Expr) : GoalM Bool := do
+  return isSameExpr (← getENode e).root (← getBoolFalseExpr)
 
 /-- Returns `true` if `a` and `b` are in the same equivalence class. -/
 def isEqv (a b : Expr) : GoalM Bool := do
@@ -678,6 +684,14 @@ def pushEqTrue (a proof : Expr) : GoalM Unit := do
 def pushEqFalse (a proof : Expr) : GoalM Unit := do
   pushEq a (← getFalseExpr) proof
 
+/-- Pushes `a = Bool.true` with `proof` to `newEqs`. -/
+def pushEqBoolTrue (a proof : Expr) : GoalM Unit := do
+  pushEq a (← getBoolTrueExpr) proof
+
+/-- Pushes `a = Bool.false` with `proof` to `newEqs`. -/
+def pushEqBoolFalse (a proof : Expr) : GoalM Unit := do
+  pushEq a (← getBoolFalseExpr) proof
+
 /--
 Records that `parent` is a parent of `child`. This function actually stores the
 information in the root (aka canonical representative) of `child`.
@@ -837,6 +851,20 @@ It assumes `a` and `False` are in the same equivalence class.
 def mkEqFalseProof (a : Expr) : GoalM Expr := do
   mkEqProof a (← getFalseExpr)
 
+/--
+Returns a proof that `a = Bool.true`.
+It assumes `a` and `Bool.true` are in the same equivalence class.
+-/
+def mkEqBoolTrueProof (a : Expr) : GoalM Expr := do
+  mkEqProof a (← getBoolTrueExpr)
+
+/--
+Returns a proof that `a = Bool.false`.
+It assumes `a` and `Bool.false` are in the same equivalence class.
+-/
+def mkEqBoolFalseProof (a : Expr) : GoalM Expr := do
+  mkEqProof a (← getBoolFalseExpr)
+
 /-- Marks current goal as inconsistent without assigning `mvarId`. -/
 def markAsInconsistent : GoalM Unit := do
   unless (← get).inconsistent do

tests/lean/run/grind_bool_prop.lean

@@ -0,0 +1,19 @@
+example (f : Bool → Nat) : f (a && b) = 0 → a = false → f false = 0 := by grind (splits := 0)
+example (f : Bool → Nat) : f (a && b) = 0 → b = false → f false = 0 := by grind (splits := 0)
+example (f : Bool → Nat) : f (a && b) = 0 → a = true → f b = 0 := by grind (splits := 0)
+example (f : Bool → Nat) : f (a && b) = 0 → b = true → f a = 0 := by grind (splits := 0)
+example (f : Bool → Nat) : (a && b) = c → c = true → f a = 0 → f true = 0 := by grind (splits := 0)
+example (f : Bool → Nat) : (a && b) = c → c = true → f b = 0 → f true = 0 := by grind (splits := 0)
+
+example (f : Bool → Nat) : f (a || b) = 0 → a = false → f b = 0 := by grind (splits := 0)
+example (f : Bool → Nat) : f (a || b) = 0 → b = false → f a = 0 := by grind (splits := 0)
+example (f : Bool → Nat) : f (a || b) = 0 → a = true → f true = 0 := by grind (splits := 0)
+example (f : Bool → Nat) : f (a || b) = 0 → b = true → f true = 0 := by grind (splits := 0)
+example (f : Bool → Nat) : (a || b) = c → c = false → f a = 0 → f false = 0 := by grind (splits := 0)
+example (f : Bool → Nat) : (a || b) = c → c = false → f b = 0 → f false = 0 := by grind (splits := 0)
+
+example (f : Bool → Nat) : f (!a) = 0 → a = true → f false = 0 := by grind (splits := 0)
+example (f : Bool → Nat) : f (!a) = 0 → a = false → f true = 0 := by grind (splits := 0)
+example (f : Bool → Nat) : (!a) = c → c = true → f a = 0 → f false = 0 := by grind (splits := 0)
+example (f : Bool → Nat) : (!a) = c → c = false → f a = 0 → f true = 0 := by grind (splits := 0)
+example : (!a) = c → c = a → False := by grind (splits := 0)

tests/lean/run/grind_split_issue.lean

@@ -5,45 +5,26 @@ inductive X : Nat → Prop
 
 /--
 error: `grind` failed
-case grind.1.1
+case grind.1
 c : Nat
 q : X c 0
-s✝ : Nat
-h✝² : 0 = s✝
-h✝¹ : HEq ⋯ ⋯
 s : Nat
-h✝ : c = s
+h✝ : 0 = s
 h : HEq ⋯ ⋯
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts
     [prop] X c 0
-    [prop] X c 0
-    [prop] X c c → X c 0
-    [prop] X c c
-    [prop] 0 = s✝
-    [prop] HEq ⋯ ⋯
-    [prop] c = s
+    [prop] 0 = s
     [prop] HEq ⋯ ⋯
   [eqc] True propositions
     [prop] X c 0
-    [prop] X c c → X c 0
-    [prop] X c c
-    [prop] X c s✝
     [prop] X c s
   [eqc] Equivalence classes
-    [eqc] {c, s}
-    [eqc] {s✝, 0}
-  [ematch] E-matching patterns
-    [thm] X.f: [X #1 #0]
-    [thm] X.g: [X #2 #1]
+    [eqc] {s, 0}
 [grind] Issues
-  [issue] #2 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)`
-[grind] Counters
-  [thm] E-Matching instances
-    [thm] X.f ↦ 2
-    [thm] X.g ↦ 2
+  [issue] #1 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)`
 -/
 #guard_msgs (error) in
 example {c : Nat} (q : X c 0) : False := by
-  grind [X]
+  grind [cases X]