grind and ordered ring

Stream: lean4

[Alex Meiburg]

I've been playing with grind, and in particular I'm very impressed with its ability to do all sorts of thing with equalities over the reals. I did notice that it was "incomplete", though, in the sense that there were true equalities that were consequences of the given ones, that it wasn't proving. After playing around for a while I've determined this was because it can't make full use of the fact that the reals are an ordered ring. (So, maybe, it's complete for field arithmetic + equalities over the complex numbers...?)

Anyway, I made a file of some work where I was playing around with adding @[grind] to different facts and seeing what it and couldn't prove. Certainly, in some of the cases, adding some basic facts to grind made it go :rocket: and it could combine them nicely. But in some other cases, it was unable to use them, and I don't understand why. (And I'd like to.)

I'm also curious if some of these facts (in an appropriately general form) could be tagged @grind in future versions of Lean, or if they wouldn't for issues of being too slow / explosive. In fact towards the end of the file I noticed that grind was entering a loop of generating progressively more complicated expressions, so definitely some combination of the facts that I had were "badly behaved".

live.lean-lang.org

Any feedback + help appreciated!

[Riccardo Brasca]

I don't know if it is related, but I had a similar experience (not for ordered stuff), and I noticed that adding the instance in #27005 made grind smarter.

[Riccardo Brasca]

See the discussion here

[Henrik Böving]

Do keep in mind that grind only supports linear arithmetic and in particular as noted at the end:

Planned future features :

• Better communication between the ring and linarith solvers. There is currently very little communication between these two solvers.
• Non-linear arithmetic over ordered rings.

[Alex Meiburg]

Well, I was referring to the "Algebraic Solver", which is distinctly nonlinear, no?

[Henrik Böving]

Yes but the algebraic solver (which is referred to as ring above) doesn't to business with ordering relations, it only operates on equalities.

[Alex Meiburg]

I see, makes sense. Would it be fair game to include facts like x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 as @[grind], then? Would ring be able to use this effectively?

[Alex Meiburg]

Like, there is a meaningful sense in which the theory of equalities over the reals is equivalent to the theory of inequalities over reals, since 0 <= a iff \exists b, a = b^2. And I'm curious how much this could be boostrapped on top of ring

[Alex Meiburg]

If I add some instances, it helps a bit:

instance Preorder.toGrindPreorder {α} [Preorder α] : Lean.Grind.Preorder α where
  le_refl := le_refl
  le_trans := _root_.le_trans
  lt_iff_le_not_le := _root_.lt_iff_le_not_ge

instance IsOrderedCancelAddMonoid.toOrderedAdd {α} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] :
    Lean.Grind.OrderedAdd α where
  add_le_left_iff c :=
    ⟨(IsOrderedAddMonoid.add_le_add_right _ _ · c),
      IsOrderedCancelAddMonoid.le_of_add_le_add_right c _ _⟩

instance IsStrictOrderedRing.toGrindOrderedRing {α} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] :
    Lean.Grind.OrderedRing α where
  zero_lt_one := zero_lt_one
  mul_lt_mul_of_pos_left := mul_lt_mul_of_pos_left
  mul_lt_mul_of_pos_right := mul_lt_mul_of_pos_right

Will PR.

[Alex Meiburg]

It's just a bit, though, it gets me

theorem ne_of_lt' (a b : ℝ) (h : a < b) : a ≠ b := by
  grind

and none of the other examples in that file.

[Henrik Böving]

Alex Meiburg said:

If I add some instances, it helps a bit:

instance Preorder.toGrindPreorder {α} [Preorder α] : Lean.Grind.Preorder α where
  le_refl := le_refl
  le_trans := _root_.le_trans
  lt_iff_le_not_le := _root_.lt_iff_le_not_ge

instance IsOrderedCancelAddMonoid.toOrderedAdd {α} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] :
    Lean.Grind.OrderedAdd α where
  add_le_left_iff c :=
    ⟨(IsOrderedAddMonoid.add_le_add_right _ _ · c),
      IsOrderedCancelAddMonoid.le_of_add_le_add_right c _ _⟩

instance IsStrictOrderedRing.toGrindOrderedRing {α} [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] :
    Lean.Grind.OrderedRing α where
  zero_lt_one := zero_lt_one
  mul_lt_mul_of_pos_left := mul_lt_mul_of_pos_left
  mul_lt_mul_of_pos_right := mul_lt_mul_of_pos_right

Will PR.

This seems reasonable yes, in general it would be good to focus on how mathlib can connect their hierarchies to grind's and then see what still doesn't work afterwards.

Alex Meiburg said:

I see, makes sense. Would it be fair game to include facts like x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 as @[grind], then? Would ring be able to use this effectively?

I'm not sure about this unfortunately.

[Heather Macbeth]

I noticed that grind seems to slow down on ring problems when a lot is imported. For example,

variable {K : Type*} [Field K] {x y z : K}

#time
example : x ^ 3 * x ^ 42 = x ^ 45 := by grind

With import Mathlib.Algebra.Field.Rat it takes 66 ms, with import Mathlib it takes 1091 ms. (On the web editor.). Is this to be expected?

[Heather Macbeth]

(Note that ring doesn't seem to have this problem.)

[Henrik Böving]

This is because inferring Lean.Grind.NoNatZeroDivisors is slow, presumably because Mathlib as a whole has some instance that makes this go horribly wrong.

[Henrik Böving]

Hm, looking at trace.profiler there seem to be about 30 applicable instances that sum to 600ms of latency and the lower you set the profiler threshold the more instances with very low latency pop up. So the issue is seemingly just that there is a million ways to get to NoNatZeroDivisors and all are tried.

[Heather Macbeth]

Pretty weird because that instance is not actually needed for the problem.

[Henrik Böving]

Ah, this could be because grind precomputes these instances as to avoid synthesizing them repeatedly by in subterms and putting pressure on caches. Maybe thunking these computations could be of interest then. I'll open an issue about it.

[Heather Macbeth]

Thanks!

[Floris van Doorn]

I think on the Mathlib side we can also do a (much) better job managing instances, which I wrote about yesterday here: #mathlib4 > bug with quotient of Z

[Mauricio Barba da Costa]

I saw this thread and was moved to be more selective about the imports I was making in a file that uses grind. However, when I import just the files that cause the red squiggles to go away, grind isn't able to prove my theorem. I supposed this is because there are some grind instances that are needed but are not being imported. Is there a way to get the minimal imports needed to get a grind to work? I've tried grind? but the infoview just suggests trying grind only. I've attached a mwe of my code below.

import Mathlib

theorem statement (A B C D : ℂ)
  (h1 : (A - 0) * (B - 1) - (C - 1) * (D - 0) = 0)
  (h2 : (A - 0) * (D - 0) + (C - 0) * (B - 1) = 0)
  (h5 : (0 - 0) * (B - 0) - (1 - 0) * (D - 0) ≠ 0) :
  4 * (2⁻¹ * ((0 - 0) * (B - 0) - (1 - 0) * (D - 0)))^2 =
    ((0 - D)^2 + (1 - B)^2) * ((0 - A)^2 + (0 - C)^2)
    := by grind
-- This works

import Mathlib.Data.Complex.Basic

theorem statement (A B C D : ℂ)
  (h1 : (A - 0) * (B - 1) - (C - 1) * (D - 0) = 0)
  (h2 : (A - 0) * (D - 0) + (C - 0) * (B - 1) = 0)
  (h5 : (0 - 0) * (B - 0) - (1 - 0) * (D - 0) ≠ 0) :
  4 * (2⁻¹ * ((0 - 0) * (B - 0) - (1 - 0) * (D - 0)))^2 =
    ((0 - D)^2 + (1 - B)^2) * ((0 - A)^2 + (0 - C)^2)
    := by grind
-- This does not work

[Robin Arnez]

#min_imports?

[Mauricio Barba da Costa]

That did it. Thanks!