fix

src/Init/Grind/Lemmas.lean

@@ -66,12 +66,6 @@ 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₂)]
 
-/- 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
-theorem of_eq_eq_false {a b : Prop} (h : (a = b) = False) : (¬a ∨ ¬b) ∧ (b ∨ a) := by
-  by_cases a <;> by_cases b <;> simp_all
-
 /-! Forall -/
 
 theorem forall_propagator (p : Prop) (q : p → Prop) (q' : Prop) (h₁ : p = True) (h₂ : q (of_eq_true h₁) = q') : (∀ hp : p, q hp) = q' := by

src/Init/Grind/Norm.lean

@@ -46,12 +46,6 @@ attribute [grind_norm] not_false_eq_true
 theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
   by_cases p <;> by_cases q <;> simp [*]
 
-@[grind_norm] theorem true_imp_eq (p : Prop) : (True → p) = p := by simp
-@[grind_norm] theorem false_imp_eq (p : Prop) : (False → p) = True := by simp
-@[grind_norm] theorem imp_true_eq (p : Prop) : (p → True) = True := by simp
-@[grind_norm] theorem imp_false_eq (p : Prop) : (p → False) = ¬p := by simp
-@[grind_norm] theorem imp_self_eq (p : Prop) : (p → p) = True := by simp
-
 -- And
 @[grind_norm↓] theorem not_and (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q) := by
   by_cases p <;> by_cases q <;> simp [*]

src/Init/Grind/Tactics.lean

@@ -25,7 +25,7 @@ Passed to `grind` using, for example, the `grind (config := { matchEqs := true }
 -/
 structure Config where
   /-- Maximum number of case-splits in a proof search branch. It does not include splits performed during normalization. -/
-  splits : Nat := 8
+  splits : Nat := 5
   /-- Maximum number of E-matching (aka heuristic theorem instantiation) rounds before each case split. -/
   ematch : Nat := 5
   /--

src/Lean/Meta/Basic.lean

@@ -1964,22 +1964,15 @@ def sortFVarIds (fvarIds : Array FVarId) : MetaM (Array FVarId) := do
 
 end Methods
 
-/--
-Return `some info` if `declName` is an inductive predicate where `info : InductiveVal`.
-That is, `inductive` type in `Prop`.
--/
-def isInductivePredicate? (declName : Name) : MetaM (Option InductiveVal) := do
-  match (← getEnv).find? declName with
-  | some (.inductInfo info) =>
-    forallTelescopeReducing info.type fun _ type => do
-      match (← whnfD type) with
-      | .sort u .. => if u == levelZero then return some info else return none
-      | _ => return none
-  | _ => return none
-
 /-- Return `true` if `declName` is an inductive predicate. That is, `inductive` type in `Prop`. -/
 def isInductivePredicate (declName : Name) : MetaM Bool := do
-  return (← isInductivePredicate? declName).isSome
+  match (← getEnv).find? declName with
+  | some (.inductInfo { type := type, ..}) =>
+    forallTelescopeReducing type fun _ type => do
+      match (← whnfD type) with
+      | .sort u .. => return u == levelZero
+      | _ => return false
+  | _ => return false
 
 def isListLevelDefEqAux : List Level → List Level → MetaM Bool
   | [],    []    => return true

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

@@ -141,7 +141,6 @@ where
     updateRoots lhs rhsNode.root
     trace_goal[grind.debug] "{← ppENodeRef lhs} new root {← ppENodeRef rhsNode.root}, {← ppENodeRef (← getRoot lhs)}"
     reinsertParents parents
-    propagateEqcDown lhs
     setENode lhsNode.root { (← getENode lhsRoot.self) with -- We must retrieve `lhsRoot` since it was updated.
       next := rhsRoot.next
     }
@@ -159,13 +158,14 @@ where
       updateMT rhsRoot.self
 
   updateRoots (lhs : Expr) (rootNew : Expr) : GoalM Unit := do
-    traverseEqc lhs fun n =>
-      setENode n.self { n with root := rootNew }
-
-  propagateEqcDown (lhs : Expr) : GoalM Unit := do
-    traverseEqc lhs fun n =>
+    let rec loop (e : Expr) : GoalM Unit := do
+      let n ← getENode e
+      setENode e { n with root := rootNew }
       unless (← isInconsistent) do
-        propagateDown n.self
+        propagateDown e
+      if isSameExpr lhs n.next then return ()
+      loop n.next
+    loop lhs
 
 /-- Ensures collection of equations to be processed is empty. -/
 private def resetNewEqs : GoalM Unit :=
@@ -217,22 +217,14 @@ def add (fact : Expr) (proof : Expr) (generation := 0) : GoalM Unit := do
 where
   go (p : Expr) (isNeg : Bool) : GoalM Unit := do
     match_expr p with
-    | Eq α lhs rhs =>
-      if α.isProp then
-        -- It is morally an iff.
-        -- We do not use the `goEq` optimization because we want to register `p` as a case-split
-        goFact p isNeg
-      else
-        goEq p lhs rhs isNeg false
+    | Eq _ lhs rhs => goEq p lhs rhs isNeg false
     | HEq _ lhs _ rhs => goEq p lhs rhs isNeg true
-    | _ => goFact p isNeg
-
-  goFact (p : Expr) (isNeg : Bool) : GoalM Unit := do
-    internalize p generation
-    if isNeg then
-      addEq p (← getFalseExpr) (← mkEqFalse proof)
-    else
-      addEq p (← getTrueExpr) (← mkEqTrue proof)
+    | _ =>
+      internalize p generation
+      if isNeg then
+        addEq p (← getFalseExpr) (← mkEqFalse proof)
+      else
+        addEq p (← getTrueExpr) (← mkEqTrue proof)
 
   goEq (p : Expr) (lhs rhs : Expr) (isNeg : Bool) (isHEq : Bool) : GoalM Unit := do
     if isNeg then

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

@@ -170,43 +170,11 @@ private builtin_initialize ematchTheoremsExt : SimpleScopedEnvExtension EMatchTh
     initial  := {}
   }
 
-/--
-Symbols with built-in support in `grind` are unsuitable as pattern candidates for E-matching.
-This is because `grind` performs normalization operations and uses specialized data structures
-to implement these symbols, which may interfere with E-matching behavior.
--/
 -- TODO: create attribute?
 private def forbiddenDeclNames := #[``Eq, ``HEq, ``Iff, ``And, ``Or, ``Not]
 
 private def isForbidden (declName : Name) := forbiddenDeclNames.contains declName
 
-/--
-Auxiliary function to expand a pattern containing forbidden application symbols
-into a multi-pattern.
-
-This function enhances the usability of the `[grind =]` attribute by automatically handling
-forbidden pattern symbols. For example, consider the following theorem tagged with this attribute:
-```
-getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔ ∃ ys, xs = ys ++ [a]
-```
-Here, the selected pattern is `xs.getLast? = some a`, but `Eq` is a forbidden pattern symbol.
-Instead of producing an error, this function converts the pattern into a multi-pattern,
-allowing the attribute to be used conveniently.
-
-The function recursively expands patterns with forbidden symbols by splitting them
-into their sub-components. If the pattern does not contain forbidden symbols,
-it is returned as-is.
--/
-partial def splitWhileForbidden (pat : Expr) : List Expr :=
-  match_expr pat with
-  | Not p => splitWhileForbidden p
-  | And p₁ p₂ => splitWhileForbidden p₁ ++ splitWhileForbidden p₂
-  | Or p₁ p₂ => splitWhileForbidden p₁ ++ splitWhileForbidden p₂
-  | Eq _ lhs rhs => splitWhileForbidden lhs ++ splitWhileForbidden rhs
-  | Iff lhs rhs => splitWhileForbidden lhs ++ splitWhileForbidden rhs
-  | HEq _ lhs _ rhs => splitWhileForbidden lhs ++ splitWhileForbidden rhs
-  | _ => [pat]
-
 private def dontCare := mkConst (Name.mkSimple "[grind_dontcare]")
 
 def mkGroundPattern (e : Expr) : Expr :=
@@ -500,8 +468,7 @@ def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof :
       | _ => throwError "invalid E-matching equality theorem, conclusion must be an equality{indentExpr type}"
     let pat := if useLhs then lhs else rhs
     let pat ← preprocessPattern pat normalizePattern
-    let pats := splitWhileForbidden (pat.abstract xs)
-    return (xs.size, pats)
+    return (xs.size, [pat.abstract xs])
   mkEMatchTheoremCore origin levelParams numParams proof patterns
 
 /--

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

@@ -53,20 +53,12 @@ private def addSplitCandidate (e : Expr) : GoalM Unit := do
 -- TODO: add attribute to make this extensible
 private def forbiddenSplitTypes := [``Eq, ``HEq, ``True, ``False]
 
-/-- Returns `true` if `e` is of the form `@Eq Prop a b` -/
-def isMorallyIff (e : Expr) : Bool :=
-  let_expr Eq α _ _ := e | false
-  α.isProp
-
 /-- Inserts `e` into the list of case-split candidates if applicable. -/
 private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
   unless e.isApp do return ()
   if (← getConfig).splitIte && (e.isIte || e.isDIte) then
     addSplitCandidate e
     return ()
-  if isMorallyIff e then
-    addSplitCandidate e
-    return ()
   if (← getConfig).splitMatch then
     if (← isMatcherApp e) then
       if let .reduced _ ← reduceMatcher? e then

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

@@ -58,12 +58,9 @@ private def checkParents (e : Expr) : GoalM Unit := do
           found := true
           break
       -- Recall that we have support for `Expr.forallE` propagation. See `ForallProp.lean`.
-      if let .forallE _ d b _ := parent then
+      if let .forallE _ d _ _ := parent then
         if (← checkChild d) then
           found := true
-        unless b.hasLooseBVars do
-          if (← checkChild b) then
-            found := true
       unless found do
         assert! (← checkChild parent.getAppFn)
   else

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

@@ -14,123 +14,77 @@ namespace Lean.Meta.Grind
 inductive CaseSplitStatus where
   | resolved
   | notReady
-  | ready (numCases : Nat) (isRec := false)
+  | ready
   deriving Inhabited, BEq
 
-/-- Given `c`, the condition of an `if-then-else`, check whether we need to case-split on the `if-then-else` or not -/
-private def checkIteCondStatus (c : Expr) : GoalM CaseSplitStatus := do
-  if (← isEqTrue c <||> isEqFalse c) then
-    return .resolved
-  else
-    return .ready 2
-
-/--
-Given `e` of the form `a ∨ b`, check whether we are ready to case-split on `e`.
-That is, `e` is `True`, but neither `a` nor `b` is `True`."
--/
-private def checkDisjunctStatus (e a b : Expr) : GoalM CaseSplitStatus := do
-  if (← isEqTrue e) then
-    if (← isEqTrue a <||> isEqTrue b) then
-      return .resolved
-    else
-      return .ready 2
-  else if (← isEqFalse e) then
-    return .resolved
-  else
-    return .notReady
-
-/--
-Given `e` of the form `a ∧ b`, check whether we are ready to case-split on `e`.
-That is, `e` is `False`, but neither `a` nor `b` is `False`.
- -/
-private def checkConjunctStatus (e a b : Expr) : GoalM CaseSplitStatus := do
-  if (← isEqTrue e) then
-    return .resolved
-  else if (← isEqFalse e) then
-    if (← isEqFalse a <||> isEqFalse b) then
-      return .resolved
-    else
-      return .ready 2
-  else
-    return .notReady
-
-/--
-Given `e` of the form `@Eq Prop a b`, check whether we are ready to case-split on `e`.
-There are two cases:
-1- `e` is `True`, but neither both `a` and `b` are `True`, nor both `a` and `b` are `False`.
-2- `e` is `False`, but neither `a` is `True` and `b` is `False`, nor `a` is `False` and `b` is `True`.
--/
-private def checkIffStatus (e a b : Expr) : GoalM CaseSplitStatus := do
-  if (← isEqTrue e) then
-    if (← (isEqTrue a <&&> isEqTrue b) <||> (isEqFalse a <&&> isEqFalse b)) then
-      return .resolved
-    else
-      return .ready 2
-  else if (← isEqFalse e) then
-    if (← (isEqTrue a <&&> isEqFalse b) <||> (isEqFalse a <&&> isEqTrue b)) then
-      return .resolved
-    else
-      return .ready 2
-  else
-    return .notReady
-
 private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do
   match_expr e with
-  | Or a b => checkDisjunctStatus e a b
-  | And a b => checkConjunctStatus e a b
-  | Eq _ a b => checkIffStatus e a b
-  | ite _ c _ _ _ => checkIteCondStatus c
-  | dite _ c _ _ _ => checkIteCondStatus c
+  | Or a b =>
+    if (← isEqTrue e) then
+      if (← isEqTrue a <||> isEqTrue b) then
+        return .resolved
+      else
+        return .ready
+    else if (← isEqFalse e) then
+      return .resolved
+    else
+      return .notReady
+  | And a b =>
+    if (← isEqTrue e) then
+      return .resolved
+    else if (← isEqFalse e) then
+      if (← isEqFalse a <||> isEqFalse b) then
+        return .resolved
+      else
+        return .ready
+    else
+      return .notReady
+  | ite _ c _ _ _ =>
+    if (← isEqTrue c <||> isEqFalse c) then
+      return .resolved
+    else
+      return .ready
+  | dite _ c _ _ _ =>
+    if (← isEqTrue c <||> isEqFalse c) then
+      return .resolved
+    else
+      return .ready
   | _ =>
     if (← isResolvedCaseSplit e) then
       trace[grind.debug.split] "split resolved: {e}"
       return .resolved
-    if let some info := isMatcherAppCore? (← getEnv) e then
-      return .ready info.numAlts
+    if (← isMatcherApp e) then
+      return .ready
     let .const declName .. := e.getAppFn | unreachable!
-    if let some info ← isInductivePredicate? declName then
-      if (← isEqTrue e) then
-        return .ready info.ctors.length info.isRec
+    if (← isInductivePredicate declName <&&> isEqTrue e) then
+      return .ready
     return .notReady
 
-private inductive SplitCandidate where
-  | none
-  | some (c : Expr) (numCases : Nat) (isRec : Bool)
-
 /-- Returns the next case-split to be performed. It uses a very simple heuristic. -/
-private def selectNextSplit? : GoalM SplitCandidate := do
-  if (← isInconsistent) then return .none
-  if (← checkMaxCaseSplit) then return .none
-  go (← get).splitCandidates .none []
+private def selectNextSplit? : GoalM (Option Expr) := do
+  if (← isInconsistent) then return none
+  if (← checkMaxCaseSplit) then return none
+  go (← get).splitCandidates none []
 where
-  go (cs : List Expr) (c? : SplitCandidate) (cs' : List Expr) : GoalM SplitCandidate := do
+  go (cs : List Expr) (c? : Option Expr) (cs' : List Expr) : GoalM (Option Expr) := do
     match cs with
     | [] =>
       modify fun s => { s with splitCandidates := cs'.reverse }
-      if let .some _ numCases isRec := c? then
-        let numSplits := (← get).numSplits
-        -- We only increase the number of splits if there is more than one case or it is recursive.
-        let numSplits := if numCases > 1 || isRec then numSplits + 1 else numSplits
+      if c?.isSome then
         -- Remark: we reset `numEmatch` after each case split.
         -- We should consider other strategies in the future.
-        modify fun s => { s with numSplits, numEmatch := 0 }
+        modify fun s => { s with numSplits := s.numSplits + 1, numEmatch := 0 }
       return c?
     | c::cs =>
     match (← checkCaseSplitStatus c) with
     | .notReady => go cs c? (c::cs')
     | .resolved => go cs c? cs'
-    | .ready numCases isRec =>
+    | .ready =>
     match c? with
-    | .none => go cs (.some c numCases isRec) cs'
-    | .some c' numCases' _ =>
-     let isBetter : GoalM Bool := do
-       if numCases == 1 && !isRec && numCases' > 1 then
-         return true
-       if (← getGeneration c) < (← getGeneration c') then
-         return true
-       return numCases < numCases'
-     if (← isBetter) then
-        go cs (.some c numCases isRec) (c'::cs')
+    | none => go cs (some c) cs'
+    | some c' =>
+      if (← getGeneration c) < (← getGeneration c') then
+        go cs (some c) (c'::cs')
       else
         go cs c? (c::cs')
 
@@ -140,11 +94,6 @@ private def mkCasesMajor (c : Expr) : GoalM Expr := do
   | And a b => return mkApp3 (mkConst ``Grind.or_of_and_eq_false) a b (← mkEqFalseProof c)
   | ite _ c _ _ _ => return mkEM c
   | dite _ c _ _ _ => return mkEM c
-  | Eq _ a b =>
-    if (← isEqTrue c) then
-      return mkApp3 (mkConst ``Grind.of_eq_eq_true) a b (← mkEqTrueProof c)
-    else
-      return mkApp3 (mkConst ``Grind.of_eq_eq_false) a b (← mkEqFalseProof c)
   | _ => return mkApp2 (mkConst ``of_eq_true) c (← mkEqTrueProof c)
 
 /-- Introduces new hypotheses in each goal. -/
@@ -159,10 +108,9 @@ and returns a new list of goals if successful.
 -/
 def splitNext : GrindTactic := fun goal => do
   let (goals?, _) ← GoalM.run goal do
-    let .some c numCases isRec ← selectNextSplit?
+    let some c ← selectNextSplit?
       | return none
     let gen ← getGeneration c
-    let genNew := if numCases > 1 || isRec then gen+1 else gen
     trace_goal[grind.split] "{c}, generation: {gen}"
     let mvarIds ← if (← isMatcherApp c) then
       casesMatch (← get).mvarId c
@@ -171,7 +119,7 @@ def splitNext : GrindTactic := fun goal => do
       cases (← get).mvarId major
     let goal ← get
     let goals := mvarIds.map fun mvarId => { goal with mvarId }
-    let goals ← introNewHyp goals [] genNew
+    let goals ← introNewHyp goals [] (gen+1)
     return some goals
   return goals?
 

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

@@ -702,15 +702,6 @@ def getENodes : GoalM (Array ENode) := do
   let nodes := (← get).enodes.toArray.map (·.2)
   return nodes.qsort fun a b => a.idx < b.idx
 
-/-- Executes `f` to each term in the equivalence class containing `e` -/
-@[inline] def traverseEqc (e : Expr) (f : ENode → GoalM Unit) : GoalM Unit := do
-  let mut curr := e
-  repeat
-    let n ← getENode curr
-    f n
-    if isSameExpr n.next e then return ()
-    curr := n.next
-
 def forEachENode (f : ENode → GoalM Unit) : GoalM Unit := do
   let nodes ← getENodes
   for n in nodes do
@@ -723,7 +714,7 @@ def filterENodes (p : ENode → GoalM Bool) : GoalM (Array ENode) := do
       ref.modify (·.push n)
   ref.get
 
-def forEachEqcRoot (f : ENode → GoalM Unit) : GoalM Unit := do
+def forEachEqc (f : ENode → GoalM Unit) : GoalM Unit := do
   let nodes ← getENodes
   for n in nodes do
     if isSameExpr n.self n.root then

src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean

@@ -50,24 +50,18 @@ def simpCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   if let some arg := e.not? then
     let mut eNew?   := none
     let mut thmName := Name.anonymous
-    match_expr arg with
-    | LE.le α _ _ _ =>
-      if α.isConstOf ``Nat then
-        eNew?   := some (← mkLE (← mkAdd (arg.getArg! 3) (mkNatLit 1)) (arg.getArg! 2))
-        thmName := ``Nat.not_le_eq
-    | GE.ge α _ _ _ =>
-      if α.isConstOf ``Nat then
-        eNew?   := some (← mkLE (← mkAdd (arg.getArg! 2) (mkNatLit 1)) (arg.getArg! 3))
-        thmName := ``Nat.not_ge_eq
-    | LT.lt α _ _ _ =>
-      if α.isConstOf ``Nat then
-        eNew?   := some (← mkLE (arg.getArg! 3) (arg.getArg! 2))
-        thmName := ``Nat.not_lt_eq
-    | GT.gt α _ _ _ =>
-      if α.isConstOf ``Nat then
-        eNew?   := some (← mkLE (arg.getArg! 2) (arg.getArg! 3))
-        thmName := ``Nat.not_gt_eq
-    | _ => pure ()
+    if arg.isAppOfArity ``LE.le 4 then
+      eNew?   := some (← mkLE (← mkAdd (arg.getArg! 3) (mkNatLit 1)) (arg.getArg! 2))
+      thmName := ``Nat.not_le_eq
+    else if arg.isAppOfArity ``GE.ge 4 then
+      eNew?   := some (← mkLE (← mkAdd (arg.getArg! 2) (mkNatLit 1)) (arg.getArg! 3))
+      thmName := ``Nat.not_ge_eq
+    else if arg.isAppOfArity ``LT.lt 4 then
+      eNew?   := some (← mkLE (arg.getArg! 3) (arg.getArg! 2))
+      thmName := ``Nat.not_lt_eq
+    else if arg.isAppOfArity ``GT.gt 4 then
+      eNew?   := some (← mkLE (arg.getArg! 2) (arg.getArg! 3))
+      thmName := ``Nat.not_gt_eq
     if let some eNew := eNew? then
       let h₁ := mkApp2 (mkConst thmName) (arg.getArg! 2) (arg.getArg! 3)
       if let some (eNew', h₂) ← simpCnstrPos? eNew then

tests/lean/run/grind_eq_pattern.lean

@@ -1,22 +0,0 @@
-attribute [grind] List.append_ne_nil_of_left_ne_nil
-attribute [grind] List.append_ne_nil_of_right_ne_nil
-/--
-info: [grind.ematch.pattern] List.getLast?_eq_some_iff: [@List.getLast? #2 #1, @some ? #0]
--/
-#guard_msgs (info) in
-set_option trace.grind.ematch.pattern true in
-attribute [grind =] List.getLast?_eq_some_iff
-
-/--
-info: [grind.assert] xs.getLast? = b?
-[grind.assert] b? = some 10
-[grind.assert] xs = []
-[grind.assert] (xs.getLast? = some 10) = ∃ ys, xs = ys ++ [10]
-[grind.assert] xs = w ++ [10]
-[grind.assert] ¬w = [] → ¬w ++ [10] = []
-[grind.assert] ¬w ++ [10] = []
--/
-#guard_msgs (info) in
-set_option trace.grind.assert true in
-example (xs : List Nat) : xs.getLast? = b? → b? = some 10 → xs ≠ [] := by
-  grind

tests/lean/run/grind_implies.lean

@@ -28,13 +28,10 @@ example (p q : Prop) : (p → q) → ¬q → ¬p := by
   grind
 
 /--
-info: [grind.internalize] (p → q) = r
-[grind.internalize] Prop
-[grind.internalize] p → q
+info: [grind.internalize] p → q
 [grind.internalize] p
 [grind.internalize] q
 [grind.internalize] r
-[grind.eqc] ((p → q) = r) = True
 [grind.eqc] (p → q) = r
 [grind.eqc] p = False
 [grind.eqc] (p → q) = True
@@ -46,13 +43,10 @@ example (p q : Prop) : (p → q) = r → ¬p → r := by
 
 
 /--
-info: [grind.internalize] (p → q) = r
-[grind.internalize] Prop
-[grind.internalize] p → q
+info: [grind.internalize] p → q
 [grind.internalize] p
 [grind.internalize] q
 [grind.internalize] r
-[grind.eqc] ((p → q) = r) = True
 [grind.eqc] (p → q) = r
 [grind.eqc] q = True
 [grind.eqc] (p → q) = True
@@ -63,13 +57,10 @@ example (p q : Prop) : (p → q) = r → q → r := by
   grind
 
 /--
-info: [grind.internalize] (p → q) = r
-[grind.internalize] Prop
-[grind.internalize] p → q
+info: [grind.internalize] p → q
 [grind.internalize] p
 [grind.internalize] q
 [grind.internalize] r
-[grind.eqc] ((p → q) = r) = True
 [grind.eqc] (p → q) = r
 [grind.eqc] q = False
 [grind.eqc] r = True
@@ -81,13 +72,10 @@ example (p q : Prop) : (p → q) = r → ¬q → r → ¬p := by
   grind
 
 /--
-info: [grind.internalize] (p → q) = r
-[grind.internalize] Prop
-[grind.internalize] p → q
+info: [grind.internalize] p → q
 [grind.internalize] p
 [grind.internalize] q
 [grind.internalize] r
-[grind.eqc] ((p → q) = r) = True
 [grind.eqc] (p → q) = r
 [grind.eqc] q = False
 [grind.eqc] r = False

tests/lean/run/grind_pre.lean

@@ -86,28 +86,13 @@ example (p : Prop) (a b c : Nat) : p → a = 0 → a = b → h a = h c → a = c
 set_option trace.grind.debug.proof true
 /--
 error: `grind` failed
-case grind.1
+case grind
 α : Type
 a : α
 p q r : Prop
 h₁ : HEq p a
 h₂ : HEq q a
 h₃ : p = r
-left : ¬p ∨ r
-right : ¬r ∨ p
-h : ¬r
-⊢ False
-
-case grind.2
-α : Type
-a : α
-p q r : Prop
-h₁ : HEq p a
-h₂ : HEq q a
-h₃ : p = r
-left : ¬p ∨ r
-right : ¬r ∨ p
-h : p
 ⊢ False
 -/
 #guard_msgs (error) in

tests/lean/run/grind_propagate_connectives.lean

@@ -6,7 +6,7 @@ def fallback : Fallback := do
   let falseExprs := (← filterENodes fun e => return e.self.isFVar && (← isEqFalse e.self)).toList.map (·.self)
   logInfo m!"true:  {trueExprs}"
   logInfo m!"false: {falseExprs}"
-  forEachEqcRoot fun n => do
+  forEachEqc fun n => do
     unless (← isProp n.self) || (← isType n.self) || n.size == 1 do
       let eqc ← getEqc n.self
       logInfo eqc

tests/lean/run/grind_t1.lean

@@ -213,53 +213,3 @@ example (P Q R : α → Prop) (h₁ : ∀ x, Q x → P x) (h₂ : ∀ x, R x →
 
 example (w : Nat → Type) (h : ∀ n, Subsingleton (w n)) : True := by
   grind
-
-example {P1 P2 : Prop} : (P1 ∧ P2) ↔ (P2 ∧ P1) := by
-  grind
-
-example {P U V W : Prop} (h : P ↔ (V ↔ W)) (w : ¬ U ↔ V) : ¬ P ↔ (U ↔ W) := by
-  grind
-
-example {P Q : Prop} (q : Q) (w : P = (P = ¬ Q)) : False := by
-  grind
-
-example (P Q : Prop) : (¬P → ¬Q) ↔ (Q → P) := by
-  grind
-
-example {α} (a b c : α) [LE α] :
-  ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b := by
-  simp_arith -- should not fail
-  sorry
-
-example {α} (a b c : α) [LE α] :
-  ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b := by
-  grind
-
-example (x y : Bool) : ¬(x = true ↔ y = true) ↔ (¬(x = true) ↔ y = true) := by
-  grind
-
-/--
-error: `grind` failed
-case grind
-p q : Prop
-a✝¹ : p = q
-a✝ : p
-⊢ False
--/
-#guard_msgs (error) in
-set_option trace.grind.split true in
-example (p q : Prop) : (p ↔ q) → p → False := by
-  grind -- should not split on (p ↔ q)
-
-/--
-error: `grind` failed
-case grind
-p q : Prop
-a✝¹ : p = ¬q
-a✝ : p
-⊢ False
--/
-#guard_msgs (error) in
-set_option trace.grind.split true in
-example (p q : Prop) : ¬(p ↔ q) → p → False := by
-  grind -- should not split on (p ↔ q)