Grind failure for CommSemiring, not Semiring

Stream: lean4

[Bolton Bailey]

Here is an MWE, thanks Riccardo Brasca for noting this in #25925.

I figured that grind would have all the same tools available for CommSemiring as Semiring, so I don't know why this fails, does anyone have an explanation or guidance to what I could change to fix this?

import Mathlib

example {R : Type*} [Semiring R] (f r : R) (hg : f * r ≠ 0) :
    f ≠ 0 := by
  intro hf
  grind -- success

example {R : Type*} [CommSemiring R] (f r : R) (hg : f * r ≠ 0) :
    f ≠ 0 := by
  intro hf
  grind -- failed

[Riccardo Brasca]

Mathlib free

example {R : Type} [Lean.Grind.Semiring R] (f r : R) (hg : f * r ≠ 0) :
    f ≠ 0 := by
  grind -- success

example {R : Type} [Lean.Grind.CommSemiring R] (f r : R) (hg : f * r ≠ 0) :
    f ≠ 0 := by
  grind -- failed

[Notification Bot]

This topic was moved here from #mathlib4 > Grind failure for CommSemiring, not Semiring by Riccardo Brasca.

[Riccardo Brasca]

Since it's not mathlib related I am moving the discussion here.

[Riccardo Brasca]

cc @Kim Morrison

[Kim Morrison]

I've opened a fix: https://github.com/leanprover/lean4/pull/11881

The issue was that propagateMul (which handles 0 * a = 0 and a * 0 = 0) was only firing for "unsupported" semirings. CommSemiring was considered "supported" because it uses a ring envelope for normalization, but that approach doesn't propagate these equalities back to original terms.