grind needs `sub_eq_zero`

Stream: lean4

[Jovan Gerbscheid]

My understanding was that we shouldn't pass algebraic lemmas to grind because it has algebraic solvers that should be able to do this already. But here is a mwe where this doesn't work. We need to pass sub_eq_zero explicitly to grind, or rewrite with it ourselves beforehand.

import Mathlib

variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]

lemma ortho_ne_zero_of_norm_eq_one_of_not_collinear {x : V} {a : ℝ} (hx : ‖x‖ = 1)
    (ha : a ≠ 1) (ha' : a ≠ -1) :
    ¬x - a • x = 0 := by
  rw [sub_eq_zero]
  grind [abs, norm_smul, Real.norm_eq_abs]

[Henrik Böving]

grind does not have a solver for group theory related things at the moment so this is to be expected I would say.

[Jovan Gerbscheid]

But it successfully synthesizes

#synth Lean.Grind.IntModule V

Is this type class currently unused?

[Kim Morrison]

The problem (still present on latest nightly) is indicated by expanding the "Issues" item in the grind failure diagnostics:

[grind] Issues ▼
  [issue] `grind linarith` term with unexpected instance
        a • x

I suspect this is a bug, I will try to minimize a bit!

[Kim Morrison]

I think this is just out of scope at present. It might well find IntModule V, and then the relevant module finds x = a • x, but this doesn't get propagated back to the main grind state.

[Kim Morrison]

Here's a Mathlib free version:

example {W : Type} [Lean.Grind.IntModule W] (f : W → Nat)
    (_ : ∀ (a : Int) (x : W), f (a • x) = a.natAbs * f x)
    (_ : a ≠ 1) (_ : a ≠ -1) (x : W) (_ : f x = 1) :
    ¬ x - a • x = 0 := by
  fail_if_success grind
  rw [Lean.Grind.AddCommGroup.sub_eq_zero_iff]
  grind

[Michael Stoll]

There was a situation where grind needed docs#mul_one to be provided explicitly (I think it came up in a PR I reviewed recently), which I found strange because grind is supposed to do ring...

[Johan Commelin]

@Michael Stoll Was it a 1 in a ring? Or in some other multiplicative structure (like a group)?

[Michael Stoll]

I'm pretty sure it was in a ring. (Is there an easy way to find the PRs from the last few weeks I have commented on? Then I could try to see if I can find the precise situation.) @Johan Commelin

[Johan Commelin]

$ gh pr list --search "commenter:@me updated:>2025-12-01" --state all --repo leanprover-community/mathlib4

[Bryan Gin-ge Chen]

Note that the commenter:@me updated:>2025-12-01 string also works in the PR search form: https://github.com/leanprover-community/mathlib4/pulls?q=is%3Apr+commenter%3A%40me+updated%3A%3E2025-12-01

[Michael Stoll]

It was here: #general > "Missing Tactics" list @ 💬 (not in a PR, after all).
Minimized a bit (without the casts):

import Mathlib

example (ε : ℝ) (hε : 0 < ε) (N : ℝ) (hN : 1 / ε < N) (n : ℝ) (hn : N ≤ n) : 1 / n < ε := by
  try grind [inv_lt_of_inv_lt₀] -- fails
  grind [inv_lt_of_inv_lt₀, one_mul] -- succeeds

[Kim Morrison]

Michael Stoll said:

It was here: #general > "Missing Tactics" list @ 💬 (not in a PR, after all).
Minimized a bit (without the casts):

import Mathlib

example (ε : ℝ) (hε : 0 < ε) (N : ℝ) (hN : 1 / ε < N) (n : ℝ) (hn : N ≤ n) : 1 / n < ε := by
  try grind [inv_lt_of_inv_lt₀] -- fails
  grind [inv_lt_of_inv_lt₀, one_mul] -- succeeds

This one is a bit complicated. We'll work on it. :-) Curiously grind doesn't actually use one_mul at all in the final proof!

Here's a Mathlib-free version:

theorem inv_lt_of_inv_lt₀ {a b : Rat} : 0 < a → a⁻¹ < b → b⁻¹ < a := sorry

example (ε : Rat) (hε : 0 < ε) (N : Rat) (hN : 1 / ε < N) (n : Rat) (hn : N ≤ n) : 1 / n < ε := by
  grind [inv_lt_of_inv_lt₀] -- fails

theorem B (ε : Rat) (hε : 0 < ε) (N : Rat) (hN : 1 / ε < N) (n : Rat) (hn : N ≤ n) : 1 / n < ε := by
  grind [inv_lt_of_inv_lt₀, Lean.Grind.Semiring.one_mul] -- succeeds

[Kim Morrison]

It's pretty strange that this one works at all right now. The order module is getting lucky! It's important to remember that the order/linarith/ring modules have limited communication: they don't just propagate all equalities to each other (they might discover many, indeed infinitely many). So in this case the fact that the ring module understands one_mul isn't helping the order module notice that, and it needs some help from the main ematch/cc loop.

We're going to work more on non-linear inequalities in grind next quarter.

[Michael Stoll]

Kim Morrison said:

We're going to work more on non-linear inequalities in grind next quarter.

Looking forward to that!