How to understand why grind doesn't work?

Stream: general

[Riccardo Brasca]

grind is able to prove the following

example (a b c : Nat) (h : a = b) : a + c = c + b := by
  grind

But not the following

import Mathlib

variable {R : Type*} [CommSemiring R] [IsCancelAdd R]

example (a b c : R) (h : a = b) : a + c = c + b := by
  grind

(it is enough to add rw [add_comm a c] to make it working). How can I understand why it is smarter with ℕ? In particular, how can I make it as smart as for ℕ but for MyNat, my copy of the natural numbers (of course I've defined all the relevant instances, but still grind is better with ℕ)?

[Henrik Böving]

Have people in mathlib already established a connection between IsCancelAdd and grinds internal type classes?

[Junyan Xu]

I don't think IsCancelAdd is needed ...

[Riccardo Brasca]

Oh sorry, of course it's not (I minimized too much my original example where it was needed).

[Riccardo Brasca]

The question makes even more sense, with Nat grind realized that has to use add_comm, but not in general.

[Henrik Böving]

You need another grind typeclass for this to work:

variable {R : Type} [Lean.Grind.CommSemiring R] [Lean.Grind.AddRightCancel R]

example (a b c : R) (h : a = b) : a + c = c + b := by
  grind

so someone needs to build that connection in mathlib

[Riccardo Brasca]

I see. This is still confusing though, why grind needs Lean.Grind.AddRightCancel R? As pointed out this is completely useless for the result at hand.

[Rémy Degenne]

But IsCancelAdd or Lean.Grind.AddRightCancel should not be needed to prove this.

variable {R : Type} [Lean.Grind.CommSemiring R]

example (a b c : R) (h : a = b) : a + c = c + b := by rw [h]; grind --succeeds
example (a b c : R) (h : a = b) : a + c = c + b := by grind -- fails

Is this expected? Shouldn't grind be able to use h? (I know nothing about what grind does)

[Riccardo Brasca]

Well, even the following does not work

variable {A : Type} [Lean.Grind.AddCommMonoid A]

example (a b : A) : a + b = b + a := by
  grind

[Riccardo Brasca]

But I don't know if it is expected or not.

[Henrik Böving]

Riccardo Brasca said:

Well, even the following does not work

variable {A : Type} [Lean.Grind.AddCommMonoid A]

example (a b : A) : a + b = b + a := by
  grind

The algebraic structure section of the manual has information on this. There is no built-in solver provided for monoids but only what is described in the manual.

Note that you can do the following:

variable {A : Type} [Lean.Grind.AddCommMonoid A]

example (a b : A) : a + b = b + a := by
  grind [Lean.Grind.AddCommMonoid.add_comm]

As grind has the capability to instantiate theorems (see the section on e matching), keep in mind that it is not necessarily a good idea to just mark everything grind as grind cannot scale infinitely.

[Riccardo Brasca]

What I still don't get is why it works for Nat. Is it the case that Nat has special support?

[Henrik Böving]

Because Nat has the instance it needs to make the construction mentioned in the reference manual work:

#synth Lean.Grind.AddRightCancel Nat

[Riccardo Brasca]

But this is has to do with cancellativity.

[Jireh Loreaux]

Agreed, this is just congr and commutativity.

[Riccardo Brasca]

Anyway, the question is more generally the following: I have theorem that grind is able to prove immediately for Nat (where the equality is a consequence of a linear combination of the assumptions), but not for a blah semiring, where blah is a class that is enough for the theorem (in practice the goal is a linear combination of the assumptions, and indeed linar_combination does it).

Is there a way to make grind smart enough to prove it for blah semirings?

[Riccardo Brasca]

One example is

example {R : Type*} [CommSemiring R] [IsCancelAdd R] (a b c d e f : R) (h1 : a + d = b + c)
    (h2 : c + f = d + e) : a + f = b + e := by
  linear_combination h1 + h2

[Riccardo Brasca]

OK, I understood what's missing here: there is no instance that relates mathlb with Lean.Grind.AddRightCancel.

[Riccardo Brasca]

We surely want this, right?

[Jireh Loreaux]

But that still doesn't explain the problem in the OP right?

[Riccardo Brasca]

Yes

[Jireh Loreaux]

But yes, we definitely want that. This is what Henrik was suggesting above.

[Riccardo Brasca]

#27005

[Asei Inoue]

I see same issue

open Lean Grind

variable {M : Type} [AddCommMonoid M]

example (l m n : M) : l + m + n = (l + m) + n := by
  -- This can be proven
  grind

set_option warn.sorry false in

example (l m n : M) : l + m = m + l := by
  -- I think `grind` *should* be able to close this goal, but currently it cannot.
  fail_if_success grind
  sorry

[Jovan Gerbscheid]

I was trying out grind, and was surprised it couldn't solve the following:

import Mathlib

example {f : ℝ → ℝ} {a b : ℝ} (h1 : 2 * a + b = 0) (h2 : b = 0) : f a = f 0 := by
  grind

[Jovan Gerbscheid]

In the above example, if I add a completely irrelevant extra variable x and hypothis a = x + 1, then the example does work.

[Jovan Gerbscheid]

So I guess grind needs to be given some sort of hint that a should be normalized using the Gröbner basis

[Damiano Testa]

In fact, it looks like simply adding set c := a also allows grind to solve the goal!

[Robin Carlier]

I have trouble debugging the following grind failure. The example is from mathlib and is not quite minimal. I’ve included all attributes I’ve added when stumbling on this.
aesop_cat solves this with no issues.

From what I see in the diagnostic, it has trouble using once more that (𝟙 _).app _ = 𝟙 _.

import Mathlib.CategoryTheory.Whiskering

namespace CategoryTheory.Functor

universe u₁ v₁ u₂ v₂ u₃ v₃ u₄ v₄

variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] {E : Type u₃}
  [Category.{v₃} E]

attribute [grind =] Category.comp_id Category.id_comp
attribute [grind _=_] Category.assoc

attribute [grind _=_] NatTrans.naturality NatTrans.vcomp_app'
attribute [grind =] NatTrans.id_app

attribute [grind _=_] Functor.map_comp
attribute [grind =] Functor.map_id Functor.comp_obj Functor.comp_map Functor.id_obj Functor.id_map

attribute [grind] whiskerLeft_app

@[simps]
def whiskeringLeft' : (C ⥤ D) ⥤ (D ⥤ E) ⥤ C ⥤ E where
  obj F :=
    { obj G := F ⋙ G
      map := fun α => whiskerLeft F α }
  map τ :=
    { app H :=
        { app x := H.map (τ.app x)
          naturality := by intros; grind }
      naturality := by intros; ext; grind }
  map_id x := by
    ext F t
    grind (gen := 10) (ematch := 20) -- fails

end CategoryTheory.Functor

Is there a magic trick/lemma/pattern that I’m missing?

grind_pattern NatTrans.id_app => (𝟙 F : F ⟶ F).app X does nothing.

[Robin Carlier]

:man_facepalming: [grind _=_] NatTrans.id_app works, I thought I had tried this...