grind failures

Stream: general

[Michael Stoll]

(Maybe it is useful to have a thread that collects (perceived) failures of grind.)

I'm surprised that grind does not do the following :

import Mathlib

example {ε : ℝ} (hε : 0 < ε) : 0 < ε / 2 := by
  try grind -- fails
  linarith -- works
  --  exact half_pos hε -- also works

(Even grind [half_pos] fails here.)

Here are some variants.

import Mathlib.Algebra.Order.Field.Basic

variable {R : Type} [Field R] [LinearOrder R] [IsStrictOrderedRing R]

lemma foo {ε : R} (hε : 0 < ε) : 0 < ε / 2 := by
  try grind [half_pos] -- fails
  exact half_pos hε

example {ε : R} (hε : 0 < ε) : 0 < 2 * ε := by
  grind -- works

example {ε : R} (hε : 0 < ε) : 0 < 2⁻¹ * ε := by
  try grind -- fails
  grind [Left.mul_pos] -- succeeds

example : (0 : R) < 2⁻¹ := by
  grind -- works

[Michael Stoll]

Another example showing that grind has problems with halves:

import Mathlib

example {a b x : ℝ} (ha : a < x / 2) (hb : b < x / 2) : a + b < x := by
  grind -- fails

[Ilmārs Cīrulis]

This works:

import Mathlib

example {a b x : ℝ} (ha : a < x / 2) (hb : b < x / 2) : a + b < x := by
  have h := add_halves x
  grind [add_lt_add]

But this doesn't:

import Mathlib

example {a b x : ℝ} (ha : a < x / 2) (hb : b < x / 2) : a + b < x := by
  grind [add_lt_add, add_halves]

[Ilmārs Cīrulis]

Not saying this is failure, more like a curiosity (for me).

[Moritz Doll]

Michael Stoll said:

(Maybe it is useful to have a thread that collects (perceived) failures of grind.)

I'm surprised that grind does not do the following :

import Mathlib

example {ε : ℝ} (hε : 0 < ε) : 0 < ε / 2 := by
  try grind -- fails
  linarith -- works
  --  exact half_pos hε -- also works

(Even grind [half_pos] fails here.)

Here are some variants.

import Mathlib.Algebra.Order.Field.Basic

variable {R : Type} [Field R] [LinearOrder R] [IsStrictOrderedRing R]

lemma foo {ε : R} (hε : 0 < ε) : 0 < ε / 2 := by
  try grind [half_pos] -- fails
  exact half_pos hε

example {ε : R} (hε : 0 < ε) : 0 < 2 * ε := by
  grind -- works

example {ε : R} (hε : 0 < ε) : 0 < 2⁻¹ * ε := by
  try grind -- fails
  grind [Left.mul_pos] -- succeeds

example : (0 : R) < 2⁻¹ := by
  grind -- works

all of these can be solved by positivity (at least when you important enough of mathlib), so I don't know whether it is bad that grind fails

[Kim Morrison]

I think essentially all of these were fixed a few days ago. Can you try them again on nightly-testing-green and report which, if any, still fail?

[Michael Stoll]

Kim Morrison said:

Can you try them again on nightly-testing-green

On live.lean-lang.org with "Lean Nightly":

example {ε : Rat} (hε : 0 < ε) : 0 < ε / 2 := by grind

example {ε : Rat} (hε : 0 < ε) : 0 < 2⁻¹ * ε := by grind

example {a b x : Rat} (ha : a < x / 2) (hb : b < x / 2) : a + b < x := by grind

all work (but with "Latest Mathlib", they fail).

[Kim Morrison]

Great! These features won't be available with "Latest Mathlib" until mid-December.

[Michael Stoll]

Here is another example that I expected grind to solve.

import Mathlib

open Real

example {t : ℝ} (ht : 0 < t) : -2 * t < 0 := by
  grind -- works

example {t : ℝ} (ht : 0 < t) : -2 * π * t < 0 := by
  grind -- does not work

example {t : ℝ} (ht : 0 < t) : -2 * π * t < 0 := by
  grind [Real.pi_pos] -- does not work

example {t : ℝ} (ht : 0 < t) : -2 * π * t < 0 := by
  have := pi_pos
  grind -- does not work

-- the original problem
example {h t : ℝ} (hh : 0 < h) (ht : 0 < t) : -2 * π * t / h < 0 := by
  grind -- does not work

-- simplify by removing `π`
example {h t : ℝ} (hh : 0 < h) (ht : 0 < t) : -2 * t / h < 0 := by
  grind -- does not work

example {h t : ℝ} (hh : 0 < h) (ht : 0 < t) : 0 < t / h := by
  grind [div_pos] -- does not work

example {h t : ℝ} (hh : 0 < h) (ht : 0 < t) : 0 < h * t := by
  grind [mul_pos] -- works (but doesn't without `[mul_pos]`)

[Jovan Gerbscheid]

Somehow I expected grind to solve this:

example (f : Prop → Nat) (p q : Prop) : f (p ∧ q) = f (q ∧ p) := by grind

[Snir Broshi]

#new members > Weirdness with cutsat
#lean4 > possible grind regression?
#mathlib4>simp only + grind failure

[Kim Morrison]

Michael Stoll said:

Here is another example that I expected grind to solve.

import Mathlib

open Real

example {t : ℝ} (ht : 0 < t) : -2 * t < 0 := by
  grind -- works

example {t : ℝ} (ht : 0 < t) : -2 * π * t < 0 := by
  grind -- does not work

example {t : ℝ} (ht : 0 < t) : -2 * π * t < 0 := by
  grind [Real.pi_pos] -- does not work

example {t : ℝ} (ht : 0 < t) : -2 * π * t < 0 := by
  have := pi_pos
  grind -- does not work

-- the original problem
example {h t : ℝ} (hh : 0 < h) (ht : 0 < t) : -2 * π * t / h < 0 := by
  grind -- does not work

-- simplify by removing `π`
example {h t : ℝ} (hh : 0 < h) (ht : 0 < t) : -2 * t / h < 0 := by
  grind -- does not work

example {h t : ℝ} (hh : 0 < h) (ht : 0 < t) : 0 < t / h := by
  grind [div_pos] -- does not work

example {h t : ℝ} (hh : 0 < h) (ht : 0 < t) : 0 < h * t := by
  grind [mul_pos] -- works (but doesn't without `[mul_pos]`)

There is no non-linear arithmetic in grind yet.

[Bhavik Mehta]

Should mul_pos become a grind lemma? Should we add annotations to make the penultimate example work too?

[Michael Stoll]

Kim Morrison said:

There is no non-linear arithmetic in grind yet.

Fair enough. But:

example {t : ℝ} (ht : 0 < t) : -2 * π * t < 0 := by
  grind -- does not work

I would consider this a linear problem (π is a constant).

example {h t : ℝ} (hh : 0 < h) (ht : 0 < t) : 0 < t / h := by
  grind [div_pos] -- does not work

example {h t : ℝ} (hh : 0 < h) (ht : 0 < t) : 0 < h * t := by
  grind [mul_pos] -- works

Why does the second work, but the first does not?
I'm willing to help grind along, but right now I find it hard to predict what will work.

In any case, are there plans to extend the scope of grind so that it eventually will be able to solve goals like this? (The word "yet" in your message gives me some hope...)

[Michael Stoll]

On a more positive note, I'm trying to use grind whenever possible to deal with "obvious" stuff, and I find that it already works quite well. E.g., in my formalization of the Conditional Convergence Theorem, it is used 80 times, about once every 8 lines (including documentation and comments).

[Michael Stoll]

Another surprise: #lean4 > grind needs `sub_eq_zero` @ 💬 (where one has to tell grind explicitly to use one_mul).

[Michael Stoll]

import Mathlib

example (n : ℕ) : 0 < 2 ^ n := by grind -- fails

[Bhavik Mehta]

I often add Nat.pow_pos to grind in projects, with a pattern, to help with this last case:

grind_pattern Nat.pow_pos => a ^ n

example (n : Nat) : 0 < 2 ^ n := by grind

[Kim Morrison]

Yes, we should definitely add this with the isValue guard on a.

[Kim Morrison]

I don't think in this case it makes sense to think of π as a constant. :-)

[Kim Morrison]

Yes, working out how to do non-linear arithmetic with grind, through some combination of annotations, internally defined propagators, and perhaps new grind modules, is on the roadmap for next quarter.

[Bhavik Mehta]

Actually, on Lean nightly Michael's last example already succeeds, because there's a pattern for Nat.pow_pos (which is more reasonable than mine) there already