fix: grind +splitImp, arrow propagator, missing normalization rule (#8158)

This PR fixes the `grind +splitImp` and the arrow propagator. Given `p :
Prop`, the propagator was incorrectly assuming `A` was always a
proposition in an arrow `A -> p`. This PR also adds a missing
normalization rule to `grind`.

Author: leodemoura

src/Init/Grind/Norm.lean

@@ -31,6 +31,11 @@ theorem not_eq_prop (p q : Prop) : (¬(p = q)) = (p = ¬q) := by
 theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
   by_cases p <;> by_cases q <;> simp [*]
 
+-- Unless `+splitImp` is used, `grind` will not be able to do much with this kind of implication.
+-- Thus, this normalization step is enabled by default.
+theorem forall_imp_eq_or {α} (p : α → Prop) (q : Prop) : ((∀ a, p a) → q) = ((∃ a, ¬ p a) ∨ q) := by
+  rw [imp_eq]; simp
+
 theorem true_imp_eq (p : Prop) : (True → p) = p := by simp
 theorem false_imp_eq (p : Prop) : (False → p) = True := by simp
 theorem imp_true_eq (p : Prop) : (p → True) = True := by simp
@@ -125,6 +130,7 @@ init_grind_norm
   dite_eq_ite
   -- Forall
   forall_and forall_false forall_true
+  forall_imp_eq_or
   -- Exists
   exists_const exists_or exists_prop exists_and_left exists_and_right
   -- Bool cond

src/Lean/Expr.lean

@@ -1000,6 +1000,18 @@ def bindingInfo! : Expr → BinderInfo
   | lam _ _ _ bi     => bi
   | _                => panic! "binding expected"
 
+def forallName : (a : Expr) → a.isForall → Name
+  | forallE n _ _ _, _  => n
+
+def forallDomain : (a : Expr) → a.isForall → Expr
+  | forallE _ d _ _, _  => d
+
+def forallBody : (a : Expr) → a.isForall → Expr
+  | forallE _ _ b _, _  => b
+
+def forallInfo : (a : Expr) → a.isForall → BinderInfo
+  | forallE _ _ _ i, _  => i
+
 def letName! : Expr → Name
   | letE n .. => n
   | _         => panic! "let expression expected"

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

@@ -86,7 +86,7 @@ private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
 def propagateForallPropDown (e : Expr) : GoalM Unit := do
   let .forallE n a b bi := e | return ()
   if (← isEqFalse e) then
-    if b.hasLooseBVars then
+    if b.hasLooseBVars || !(← isProp a) then
       let α := a
       let p := b
       -- `e` is of the form `∀ x : α, p x`

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

@@ -59,7 +59,7 @@ def isMorallyIff (e : Expr) : Bool :=
 
 /-- Inserts `e` into the list of case-split candidates if applicable. -/
 private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
-  match e with
+  match h : e with
   | .app .. =>
     if (← getConfig).splitIte && (e.isIte || e.isDIte) then
       addSplitCandidate (.default e)
@@ -91,12 +91,13 @@ private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
       addSplitCandidate (.default e)
   | .forallE _ d _ _ =>
     if (← getConfig).splitImp then
-      addSplitCandidate (.default e)
+      if (← isProp d) then
+        addSplitCandidate (.imp e (h ▸ rfl))
     else if Arith.isRelevantPred d then
       if (← getConfig).lookahead then
-        addLookaheadCandidate (.default e)
+        addLookaheadCandidate (.imp e (h ▸ rfl))
       else
-        addSplitCandidate (.default e)
+        addSplitCandidate (.imp e (h ▸ rfl))
   | _ => pure ()
 
 /--

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

@@ -83,20 +83,6 @@ private def isCongrToPrevSplit (c : Expr) : GoalM Bool := do
     else
       return c'.isApp && isCongruent (← get).enodes c c'
 
-private def checkForallStatus (e : Expr) : GoalM SplitStatus := do
-  if (← isEqTrue e) then
-    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
-  else
-    return .notReady
-
 private def checkDefaultSplitStatus (e : Expr) : GoalM SplitStatus := do
   match_expr e with
   | Or a b => checkDisjunctStatus e a b
@@ -112,10 +98,6 @@ private def checkDefaultSplitStatus (e : Expr) : GoalM SplitStatus := do
     if (← isResolvedCaseSplit e) then
       trace_goal[grind.debug.split] "split resolved: {e}"
       return .resolved
-    if e.isForall then
-      let s ← checkForallStatus e
-      trace_goal[grind.debug.split] "{e}, status: {repr s}"
-      return s
     if (← isCongrToPrevSplit e) then
       return .resolved
     if let some info := isMatcherAppCore? (← getEnv) e then
@@ -156,9 +138,25 @@ def checkSplitInfoArgStatus (a b : Expr) (eq : Expr) : GoalM SplitStatus := do
     it_b := it_b.appFn!
   return .ready 2
 
+private def checkForallStatus (imp : Expr) (h : imp.isForall) : GoalM SplitStatus := do
+  if (← isEqTrue imp) then
+    let p := imp.forallDomain h
+    let q := imp.forallBody h
+    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 imp) then
+    return .resolved
+  else
+    return .notReady
+
 def checkSplitStatus (s : SplitInfo) : GoalM SplitStatus := do
   match s with
   | .default e => checkDefaultSplitStatus e
+  | .imp e h => checkForallStatus e h
   | .arg a b _ eq => checkSplitInfoArgStatus a b eq
 
 private inductive SplitCandidate where
@@ -229,9 +227,7 @@ private def mkCasesMajor (c : Expr) : GoalM Expr := do
       return mkGrindEM c
   | Not e => return mkGrindEM e
   | _ =>
-    if let .forallE _ p _ _ := c then
-      return mkGrindEM p
-    else if (← isEqTrue c) then
+    if (← isEqTrue c) then
       return mkOfEqTrueCore c (← mkEqTrueProof c)
     else
       return c
@@ -242,6 +238,12 @@ private def introNewHyp (goals : List Goal) (acc : List Goal) (generation : Nat)
   | [] => return acc.reverse
   | goal::goals => introNewHyp goals ((← intros generation goal) ++ acc) generation
 
+private def casesWithTrace (major : Expr) : GoalM (List MVarId) := do
+  if (← getConfig).trace then
+    if let .const declName _ := (← whnfD (← inferType major)).getAppFn then
+      saveCases declName false
+  cases (← get).mvarId major
+
 /--
 Selects a case-split from the list of candidates,
 and returns a new list of goals if successful.
@@ -250,22 +252,20 @@ def splitNext : GrindTactic := fun goal => do
   let (goals?, _) ← GoalM.run goal do
     let .some c numCases isRec _ ← selectNextSplit?
       | return none
-    let c := c.getExpr
-    let gen ← getGeneration c
+    let cExpr := c.getExpr
+    let gen ← getGeneration cExpr
     let genNew := if numCases > 1 || isRec then gen+1 else gen
-    markCaseSplitAsResolved c
-    trace_goal[grind.split] "{c}, generation: {gen}"
-    let mvarIds ← if (← isMatcherApp c) then
-      casesMatch (← get).mvarId c
+    markCaseSplitAsResolved cExpr
+    trace_goal[grind.split] "{cExpr}, generation: {gen}"
+    let mvarIds ← if let .imp e h := c then
+      casesWithTrace (mkGrindEM (e.forallDomain h))
+    else if (← isMatcherApp cExpr) then
+      casesMatch (← get).mvarId cExpr
     else
-      let major ← mkCasesMajor c
-      if (← getConfig).trace then
-        if let .const declName _ := (← whnfD (← inferType major)).getAppFn then
-          saveCases declName false
-      cases (← get).mvarId major
+      casesWithTrace (← mkCasesMajor cExpr)
     let goal ← get
     let numSubgoals := mvarIds.length
-    let goals := mvarIds.mapIdx fun i mvarId => { goal with mvarId, split.trace := { expr := c, i, num := numSubgoals } :: goal.split.trace }
+    let goals := mvarIds.mapIdx fun i mvarId => { goal with mvarId, split.trace := { expr := cExpr, i, num := numSubgoals } :: goal.split.trace }
     let goals ← introNewHyp goals [] genNew
     return some goals
   return goals?

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

@@ -496,24 +496,37 @@ inductive SplitInfo where
     Term `e` may be an inductive predicate, `match`-expression, `if`-expression, implication, etc.
     -/
     default (e : Expr)
+  /-- `e` is an implication and we want to split on its antecedent. -/
+  | imp (e : Expr) (h : e.isForall)
   | /--
     Given applications `a` and `b`, case-split on whether the corresponding
     `i`-th arguments are equal or not. The split is only performed if all other
     arguments are already known to be equal or are also tagged as split candidates.
     -/
     arg (a b : Expr) (i : Nat) (eq : Expr)
-  deriving BEq, Hashable, Inhabited
+  deriving Hashable, Inhabited
+
+def SplitInfo.beq : SplitInfo → SplitInfo → Bool
+ | .default e₁, .default e₂ => e₁ == e₂
+ | .imp e₁ _, .imp e₂ _ => e₁ == e₂
+ | .arg a₁ b₁ i₁ eq₁, arg a₂ b₂ i₂ eq₂ => a₁ == a₂ && b₁ == b₂ && i₁ == i₂ && eq₁ == eq₂
+ | _, _ => false
+
+instance : BEq SplitInfo where
+  beq := SplitInfo.beq
 
 def SplitInfo.getExpr : SplitInfo → Expr
-  | .default (.forallE _ d _ _) => d
   | .default e => e
+  | .imp e h => e.forallDomain h
   | .arg _ _ _ eq => eq
 
 def SplitInfo.lt : SplitInfo → SplitInfo → Bool
-  | .default e₁, .default e₂       => e₁.lt e₂
+  | .default e₁, .default e₂     => e₁.lt e₂
+  | .imp e₁ _, .imp e₂ _         => e₁.lt e₂
   | .arg _ _ _ e₁, .arg _ _ _ e₂ => e₁.lt e₂
-  | .default _, .arg ..           => true
-  | .arg .., .default _           => false
+  | .default .., _               => true
+  | .imp .., _                   => true
+  | _, _                         => false
 
 /-- Argument `arg : type` of an application `app` in `SplitInfo`. -/
 structure SplitArg where

tests/lean/grind/countP.lean tests/lean/run/grind_countP.leantests/lean/grind/countP.lean renamed to tests/lean/run/grind_countP.lean

@@ -1,15 +1,13 @@
+set_option grind.warning false
 variable {α : Type u} {l : List α} {P Q : α → Bool}
 
 attribute [grind] List.countP_nil List.countP_cons
 
--- It would be really nice if we didn't need to `specialize` here!
-
 theorem List.countP_le_countP (hpq : ∀ x ∈ l, P x → Q x) :
     l.countP P ≤ l.countP Q := by
   induction l with
   | nil => grind
   | cons x xs ih =>
-    specialize ih (by grind)
     grind
 
 theorem List.countP_lt_countP (hpq : ∀ x ∈ l, P x → Q x) (y:α) (hx: y ∈ l) (hxP : P y = false) (hxQ : Q y) :
@@ -18,5 +16,4 @@ theorem List.countP_lt_countP (hpq : ∀ x ∈ l, P x → Q x) (y:α) (hx: y ∈
   | nil => grind
   | cons x xs ih =>
     have : xs.countP P ≤ xs.countP Q := countP_le_countP (by grind)
-    specialize ih (by grind)
     grind

…lean/grind/eq_false_of_imp_eq_false.lean …/run/grind_eq_false_of_imp_eq_false.leantests/lean/grind/eq_false_of_imp_eq_false.lean renamed to tests/lean/run/grind_eq_false_of_imp_eq_false.lean tests/lean/grind/eq_false_of_imp_eq_false.lean renamed to tests/lean/run/grind_eq_false_of_imp_eq_false.lean

@@ -1,11 +1,11 @@
 reset_grind_attrs%
-
+set_option grind.warning false
 open List
 
 attribute [grind] List.map_nil
 
 theorem map_eq_cons_iff {f : α → β} {l : List α} :
     map f l = b :: l₂ ↔ ∃ a l₁, l = a :: l₁ ∧ f a = b ∧ map f l₁ = l₂ := by
   cases l
-  case nil => grind -- kernel error
+  case nil => grind
   case cons a l => sorry