chore: fix tests

src/Init/Grind/Lemmas.lean

@@ -49,6 +49,8 @@ theorem eq_false_of_or_eq_false_right {a b : Prop} (h : (a ∨ b) = False) : b =
 theorem imp_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a → b) = True := by simp [h]
 theorem imp_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a → b) = True := by simp [h]
 theorem imp_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a → b) = b := by simp [h]
+theorem eq_false_of_imp_eq_true {a b : Prop} (h₁ : (a → b) = True) (h₂ : b = False) : a = False := by
+  simp at *; intro h; exact h₂ (h₁ h)
 
 theorem eq_true_of_imp_eq_false {a b : Prop} (h : (a → b) = False) : a = True := by simp_all
 theorem eq_false_of_imp_eq_false {a b : Prop} (h : (a → b) = False) : b = False := by simp_all

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

@@ -46,6 +46,9 @@ where
     else if (← isEqTrue b) then
       -- b = True → (a → b) = True
       pushEqTrue e <| mkApp3 (mkConst ``Grind.imp_eq_of_eq_true_right) a b (← mkEqTrueProof b)
+    else if (← isEqFalse b <&&> isEqTrue e <&&> isProp a) then
+      -- (a → b) = True → b = False → a = False
+      pushEqFalse a <| mkApp4 (mkConst ``Grind.eq_false_of_imp_eq_true) a b (← mkEqTrueProof e) (← mkEqFalseProof b)
 
 private def isEqTrueHyp? (proof : Expr) : Option FVarId := Id.run do
   let_expr eq_true _ p := proof | return none
@@ -105,5 +108,10 @@ def propagateForallPropDown (e : Expr) : GoalM Unit := do
     else
       if b.hasLooseBVars then
         addLocalEMatchTheorems e
+      else
+        unless (← alreadyInternalized b) do return ()
+        if (← isEqFalse b <&&> isProp a) then
+        -- (a → b) = True → b = False → a = False
+        pushEqFalse a <| mkApp4 (mkConst ``Grind.eq_false_of_imp_eq_true) a b (← mkEqTrueProof e) (← mkEqFalseProof b)
 
 end Lean.Meta.Grind

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

@@ -84,9 +84,12 @@ private def isCongrToPrevSplit (c : Expr) : GoalM Bool := do
 
 private def checkForallStatus (e : Expr) : GoalM CaseSplitStatus := do
   if (← isEqTrue e) then
-    let .forallE _ p _ _ := e | return .resolved
+    let .forallE _ p q _ := e | return .resolved
     if (← isEqTrue p <||> isEqFalse p) then
       return .resolved
+    unless q.hasLooseBVars do
+      if (← isEqTrue q <||> isEqFalse q) then
+        return .resolved
     return .ready 2
   else if (← isEqFalse e) then
     return .resolved

tests/lean/run/grind_ctor_ematch.lean

@@ -35,6 +35,11 @@ h : ¬Even 16
     [prop] Even 6 → Even 8
   [eqc] False propositions
     [prop] Even 16
+    [prop] Even 14
+    [prop] Even 12
+    [prop] Even 10
+    [prop] Even 8
+    [prop] Even 6
   [ematch] E-matching patterns
     [thm] Even.plus_two: [Even (#1 + 2)]
     [thm] Even.zero: [Even `[0]]

tests/lean/run/grind_implies.lean

@@ -20,8 +20,8 @@ info: [grind.internalize] p → q
 [grind.internalize] q
 [grind.eqc] (p → q) = True
 [grind.eqc] q = False
+[grind.eqc] p = False
 [grind.eqc] p = True
-[grind.eqc] (p → q) = q
 -/
 #guard_msgs (info) in
 example (p q : Prop) : (p → q) → ¬q → ¬p := by
@@ -73,8 +73,8 @@ info: [grind.internalize] (p → q) = r
 [grind.eqc] (p → q) = r
 [grind.eqc] q = False
 [grind.eqc] r = True
+[grind.eqc] p = False
 [grind.eqc] p = True
-[grind.eqc] (p → q) = q
 -/
 #guard_msgs (info) in
 example (p q : Prop) : (p → q) = r → ¬q → r → ¬p := by

tests/lean/run/grind_split_arith_imp.lean

@@ -6,4 +6,8 @@ example (hi : i < n) (hj : j < i) (hk : k < j) (as : Vector α n) (p : α → Pr
     p (as.swap i j)[k] := by
   grind
 
-example (p : Nat → Prop) (h : p j) (h' : ∀ i, i < j → p i) : ∀ i, i < j + 1 → p i := by grind
+example (p : Nat → Prop) (h : p j) (h' : ∀ i, i < j → p i) : ∀ i, i < j + 1 → p i := by
+  grind
+
+example (p : Nat → Prop) (h : p j) (h' : ∀ i, i < j → p i) : ∀ i, i < j + 1 → p i := by
+  grind (splits := 0)