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

[Michael Stoll]

Would it be reasonable to make docs#zero_le_one a grind lemma?
I noticed this gap in a context like this:

import Mathlib

example {ι M : Type*} [DecidableEq ι] [Zero M] [One M] [LinearOrder M] [ZeroLEOneClass M] (i j : ι) {x : M} (h : 0 ≤ x) :
    0 ≤ if i = j then x else 1 := by
  -- grind -- fails
  grind [zero_le_one]

[Jovan Gerbscheid]

The following works if you use Fin n instead of Fin (n + 1):

example (a b n : Nat) (ha : a < n + 1) (hb : b < n + 1) :
    (⟨a, ha⟩ : Fin (n + 1)) < ⟨b, hb⟩ ↔ a < b := by
  grind

[Michael Stoll]

Is this supposed to answer my question?

[Jovan Gerbscheid]

No, sorry, just another grind failure (you reminded me that I wanted to post this one)

[Jovan Gerbscheid]

Michael Stoll said:

Would it be reasonable to make docs#zero_le_one a grind lemma?

grind knows this as long as it can find a Lean.Grind.OrderedRing instance. Are there other cases where we want grind to know this?

[Michael Stoll]

See the example above. I was trying to make a lemma as general as possible (which was originally stated for real numbers), which made grind fail at some place in the proof, where it was working before.

[Jovan Gerbscheid]

But how do you plan to make it work with transitivity? This doesn't seem to work:

example {M : Type*} [Zero M] [One M] [LinearOrder M] [ZeroLEOneClass M] {x y : M} (h : 1 ≤ x) (h' : y ≤ 0) :
    y ≤ x := by
  -- grind -- fails
  grind [zero_le_one]

[Michael Stoll]

This works:

import Mathlib

example {M : Type*} [Zero M] [One M] [LinearOrder M] [ZeroLEOneClass M] {x y : M} (h : 1 ≤ x) (h' : y ≤ 0) :
    y ≤ x := by
  grind [zero_le_one' M]

(but not as grind [zero_le_one'] without instantiating the type :frown:)

[Bhavik Mehta]

Jovan Gerbscheid said:

The following works if you use Fin n instead of Fin (n + 1):

example (a b n : Nat) (ha : a < n + 1) (hb : b < n + 1) :
    (⟨a, ha⟩ : Fin (n + 1)) < ⟨b, hb⟩ ↔ a < b := by
  grind

lean4#12245

[Kim Morrison]

Michael Stoll said:

Would it be reasonable to make docs#zero_le_one a grind lemma?
I noticed this gap in a context like this:

import Mathlib

example {ι M : Type*} [DecidableEq ι] [Zero M] [One M] [LinearOrder M] [ZeroLEOneClass M] (i j : ι) {x : M} (h : 0 ≤ x) :
    0 ≤ if i = j then x else 1 := by
  -- grind -- fails
  grind [zero_le_one]

grind isn't really intended to do algebra outside of the situations where it can do it properly. So no, we generally don't want to tag lemmas that enable grind to "brute force" algebra/inequality proofs that it could otherwise do with "reasonable" typeclass hypotheses. If you want to do this, use local/scoped/namespaces attributes, or just pass the lemmas to grind at the call site.

[Andrew Yang]

I am really surprised that grind cannot do this. Am I missing something?

import Mathlib

/-- failed -/
#guard_msgs (substring := true) in
example (n m : ℕ) (hn : 0 < n) : m < (m + 2) * n := by grind

[Snir Broshi]

I guess that multiplication by a variable isn't linear so lia can't work it out without cases n first

[Snir Broshi]

I tried to trigger grinds case-splitting but ended up finding a bug:

/-- error: unknown metavariable `?_uniq.893` -/
#guard_msgs in
example (n m : Nat) (hn : n ≠ 0) (h : match n with | .zero | .succ _ => 1 = 1) : m ≤ m * n := by
  grind

[Pim Otte]

I'm not entirely sure if this is in scope for grind, but it would be really nice to be able to do this kind of stuff:

Demathlibified:

theorem test {f : R → R} {P : R → Prop} {LE' : R → R → Prop}:
  (∀ ib, ∃ ia, ∀ x, LE' x ia → P x → LE' (f x) ib) ↔ ∀ M, ∃ z, ∀ x, P x → LE' x z → LE' (f x) M := by
  grind

Closer to my actual usecase:

import Mathlib

theorem test {f : ℝ → ℝ} {D : Set ℝ} :
  (∀ (ib : ℝ), ∃ ia, ∀ x ≤ ia, x ∈ D → f x ≤ ib) ↔ ∀ (M : ℝ), ∃ z, ∀ x ∈ D, x ≤ z → f x ≤ M := by
  grind

[Kim Morrison]

Andrew Yang said:

I am really surprised that grind cannot do this. Am I missing something?

import Mathlib

/-- failed -/
#guard_msgs (substring := true) in
example (n m : ℕ) (hn : 0 < n) : m < (m + 2) * n := by grind

grind doesn't do any non-linear inequalities (yet)

[Kim Morrison]

Pim Otte said:

I'm not entirely sure if this is in scope for grind, but it would be really nice to be able to do this kind of stuff:

Demathlibified:

theorem test {f : R → R} {P : R → Prop} {LE' : R → R → Prop}:
  (∀ ib, ∃ ia, ∀ x, LE' x ia → P x → LE' (f x) ib) ↔ ∀ M, ∃ z, ∀ x, P x → LE' x z → LE' (f x) M := by
  grind

Closer to my actual usecase:

import Mathlib

theorem test {f : ℝ → ℝ} {D : Set ℝ} :
  (∀ (ib : ℝ), ∃ ia, ∀ x ≤ ia, x ∈ D → f x ≤ ib) ↔ ∀ (M : ℝ), ∃ z, ∀ x ∈ D, x ≤ z → f x ≤ M := by
  grind

grind typically won't solve problems that require picking witnesses for existentials.

[Jovan Gerbscheid]

I was very surprised to see grind succeed on this:

import Mathlib

lemma LT.lt.exists_disjoint_Iio_Ioi' [LinearOrder α] (a b : α) (h : a < b) :
    ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y := by
  grind only

How does this work?

[Pim Otte]

Kim Morrison said:

...

grind typically won't solve problems that require picking witnesses for existentials.

Just to double-check, the thing with this example is that it doesn't require picking a witness (since "the same choice" works). The following does work:

import Mathlib

theorem test {f : ℝ → ℝ} {D : Set ℝ} :
  (∀ (ib : ℝ), ∃ ia, ∀ x ≤ ia, x ∈ D → f x ≤ ib) ↔ ∀ (M : ℝ), ∃ z, ∀ x ∈ D, x ≤ z → f x ≤ M := by
  refine forall_congr' fun M ↦ ?_
  refine exists_congr ?_
  grind

(Still totally understand if this is out-of-scope for grind, I can imagine this is an edge case)

[Michael Stoll]

Perhaps it would make sense to add these two points (that seem to come up fairly regularly here) to the documentation of grind?

[Violeta Hernández]

Jovan Gerbscheid ha dicho:

How does this work?

My guess is that it's reproducing this proof:

lemma LT.lt.exists_disjoint_Iio_Ioi' {α} [LinearOrder α] (a b : α) (h : a < b) :
    ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y := by
  by_contra! H
  obtain ⟨c, hc, d, hd, hdc⟩ := H b h a h
  obtain ⟨e, he, f, hf, hef⟩ := H d hd c hc
  order

[Violeta Hernández]

If you do want to prove this manually, a less mystical proof might be to case on whether Ioo a b is empty. If a < x < b for some x then a' = b' = x satisfies the property. Otherwise, b' = a and a' = b does.

[Jovan Gerbscheid]

Yes, that's the proof I imagined as well.

[Jovan Gerbscheid]

I encountered the following in #35563

variable {α : Type} [Lean.Grind.IntModule α] [LE α] [LT α] [Std.IsPreorder α] [Std.LawfulOrderLT α]

example (a : α) : 0 < a → a ≠ 0 := by
  grind -- `grind linarith` internal error, structure is not a preorder

[Jovan Gerbscheid]

In the same PR, I encountered a panic (an assertion violation) in grind (https://github.com/leanprover-community/mathlib4/pull/35563#issuecomment-3935035240). I'm not sure how to go about debugging this because the panic only happened once, in CI, and after re-running, CI is happy now. It's also not clear wether this panic actually has anything to do with the changes of this PR.

I remember in the early days of grind there were problems with grind being inconsisted due to the use of pointer cache. Could it be that this problem still hasn't fully been resolved?

[Chris Henson]

This same error appears sporadically in a particular module of CSLib, which at least suggests to me that certain kinds of proofs trigger this panic. I first reported this at #lean4 > PANIC at _private.Lean.Meta.Tactic.Grind.Proof, which links to some earlier occurrences.