grind regression: fails on goals that previously worked

[kim-em]

The grind tactic has regressed in nightly-2025-11-02, failing on goals that previously worked in v4.24.0 and nightly-2025-11-01.

Bisect Result

We bisected the regression to PR #11047 (commit faed852) - "feat: equality propagation in grind order".

Example 1

This Mathlib-free example now requires simp and norm_cast preprocessing:

example {n a b : Nat}
  (this : (b : Int) ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b) ≤
          (↑b + (↑a - ↑b)) ^ (n + 1)) :
    (n + 1) * a * b ^ n ≤ a ^ (n + 1) + n * b * b ^ n := by
  -- This used to work in v4.24.0 and nightly-2025-11-01
  grind  -- now fails

  -- Workaround:
  simp [Int.mul_sub, ← Int.add_sub_assoc] at this
  norm_cast at this
  grind

Example 2

A simpler example where a superfluous hypothesis trips up grind:

example (a b : Nat) (f g : Nat → Nat)
    (hf : (∀ i ≤ a, f i ≤ f (i + 1)) ∧ f 0 = 0)
    (hg : (∀ i ≤ b, g i ≤ g (i + 1)) ∧ g 0 = 0 ∧ g b = 0) :
    g (a + b - a) = 0 := by
  -- This used to work in v4.24.0 and nightly-2025-11-01
  grind  -- now fails

  -- Workaround:
  simp_all

Context

These examples come from https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60simp.20only.60.20.2B.20.60grind.60.20failure/near/560621777

The regression appears to be caused by the new equality propagation in grind order reasoning, which may be creating unhelpful case splits or reaching the case-split limit prematurely.

🤖 Created by Claude Code

[kim-em]

Looking at #11047, here's what it changed and why it causes this regression:

What PR #11047 Changed

The PR implements equality propagation from grind's order reasoning component back to the main grind core. Specifically:

1. It internalizes nested arithmetic terms (not just constraints) into the order graph
2. For each term normalized as a + k, it creates bidirectional edges in the order graph
3. It propagates equalities discovered by the order component back to grind's main state

Why This Causes the Regression

The failing examples have many nested arithmetic terms:

• Example 1: (b : Int) ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b)
• Example 3: g (a + b - a)

With PR #11047, grind now internalizes all these nested HAdd, HSub, and OfNat applications into the order graph. Each creates bidirectional edges, leading to a combinatorial explosion of case splits.

From the diagnostic output when grind fails, we can see it's making unhelpful equality case splits like:

• case inl / case inr branches based on n + 1 = 1
• Similar splits on various nested arithmetic terms

The problem is that grind hits its case-split limit (default: 9) before finding the actual proof, because it's exploring too many irrelevant arithmetic equalities.

Why the Workarounds Work

Both simp (example 1) and simp_all (example 3) work because they simplify the nested arithmetic terms before grind sees them:

• simp [Int.mul_sub, ← Int.add_sub_assoc] reduces the complex expression
• simp_all simplifies a + b - a to just b

With fewer nested terms, grind doesn't generate as many case splits and can find the proof.

🤖 Analysis by Claude Code