Instance priorities for quotients of MvPolynomial

Stream: mathlib4

[Antoine Chambert-Loir]

With @María Inés de Frutos Fernández , we bumped onto strange time out issues when defining a commutative algebra by generators and relations, as a quotient of some MvPolynomial R M by a relation r : (MvPolynomial M R) → (MvPolynomial M R) → Prop.
We took inspiration from the definition of docs#TensorAlgebra, except that our variables commute hence we started from MvPolynomial. It appeared that without tweaking with priorities of some instances, Lean cannot prove that this algebra has quotients by ideals.
Here is a MWE that shows some of the problems (but even with the priorities indicated there, further steps do not work).

import Mathlib.Algebra.RingQuot
import Mathlib.RingTheory.Ideal.QuotientOperations
import Mathlib.Data.MvPolynomial.CommRing


noncomputable section

open Finset MvPolynomial Ideal.Quotient Ideal RingQuot

-- Defining an algebra as a quotient of polynomials
-- Experiments

variable (R : Type u) [CommSemiring R] (M : Type v)

-- A trivial relation is enough to show problems
inductive r : (MvPolynomial M R) → (MvPolynomial M R) → Prop

set_option trace.profiler true

def Quot_r := RingQuot (r R M)

instance (priority := 999) :
    Semiring (Quot_r R M) :=
  RingQuot.instSemiring _

/- We have to make the priority of CommSemiring very low,
  or else the `HasQuotient` instance below takes about 3s. -/
instance (priority := 10) :
    CommSemiring (Quot_r R M) := RingQuot.instCommSemiring _

count_heartbeats in
set_option synthInstance.maxHeartbeats 100000 in
set_option trace.profiler true in
set_option pp.proofs.withType false in
instance {S : Type w} [CommRing S] : CommRing (Quot_r S M) :=
  RingQuot.instCommRingRingQuotToSemiringToCommSemiring _

instance instAlgebra
    {R A M} [CommSemiring R] [CommRing A] [Algebra R A] :
    Algebra R (Quot_r A M) :=
  RingQuot.instAlgebraRingQuotInstSemiring _

-- verify there is no diamond
example (R : Type u) [CommRing R] :
    (algebraNat : Algebra ℕ (Quot_r R M)) = instAlgebra :=
  rfl

instance {R S A M} [CommRing R] [CommRing S] [CommRing A]
    [Algebra R A] [Algebra S A] [SMulCommClass R S A] :
    SMulCommClass R S (Quot_r A M)  :=
  RingQuot.instSMulCommClassRingQuotInstSMulRingQuotInstSMulRingQuot _

instance {R S A M} [CommRing R] [CommRing S] [CommRing A]
    [SMul R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] :
    IsScalarTower R S  (Quot_r A M) :=
  RingQuot.instIsScalarTowerRingQuotInstSMulRingQuotInstSMulRingQuot _

instance (R : Type u) [CommRing R] (M : Type v) :
    HasQuotient (Quot_r R M) (Ideal (Quot_r R M)) :=
  Submodule.hasQuotient

example (R : Type u) [CommRing R] (M : Type v) (I : Ideal (Quot_r R M)) :
    CommRing ((Quot_r R M) ⧸ I) :=
  Quotient.commRing I

count_heartbeats in
set_option synthInstance.maxHeartbeats 100000 in
set_option trace.profiler true in
set_option pp.proofs.withType false in
-- This one is still too slow
instance instAlgebra' (
    R M : Type _) [CommRing R] (I : Ideal (Quot_r R M)) :
    Algebra R ((Quot_r R M) ⧸ I) :=
Quotient.algebra R

[Eric Wieser]

Does making Quot_r reducible make things better or worse?

[Kevin Buzzard]

@Antoine Chambert-Loir I don't know which version of mathlib you're on, but on current master

count_heartbeats in
instance {S : Type w} [CommRing S] : CommRing (Quot_r S M) :=
  RingQuot.instCommRingRingQuotToSemiringToCommSemiring _

works fine with no heartbeat bumps, and takes 933 heartbeats (not 100000). A lot has happened in the last week or two.

[Kevin Buzzard]

One of the things which seems to have changed is the naming convention for instance names(?), so your code doesn't compile for me on current master.

[Antoine Chambert-Loir]

Thanks a lot. I just dit lake update, and here is an updated version.
If I don't change the priorities (they are commented in the example below), the final example instAlgebra' does not compile, Lean cannot synthesize Semiring ((Quot_r S M) ⧸ I) while it was just shown to be a CommRing in the example just above.

import Mathlib.Algebra.RingQuot
import Mathlib.RingTheory.Ideal.QuotientOperations
import Mathlib.Data.MvPolynomial.CommRing

noncomputable section

open Finset MvPolynomial Ideal.Quotient Ideal RingQuot

-- Defining an algebra as a quotient of polynomials
-- Experiments

variable (R : Type u) [CommSemiring R] (M : Type v)

-- A trivial relation is enough to show problems
inductive r : (MvPolynomial M R) → (MvPolynomial M R) → Prop

set_option trace.profiler true

def Quot_r := RingQuot (r R M)

instance : -- (priority := 999) :
    Semiring (Quot_r R M) :=
  RingQuot.instSemiring _

/- We have to make the priority of CommSemiring very low,
  or else the `HasQuotient` instance below takes about 3s. -/
instance : -- (priority := 10) :
    CommSemiring (Quot_r R M) := RingQuot.instCommSemiring _

instance {S : Type w} [CommRing S] : CommRing (Quot_r S M) :=
  RingQuot.instCommRingRingQuotToSemiringToCommSemiring _

instance instAlgebra
    {R A M} [CommSemiring R] [CommRing A] [Algebra R A] :
    Algebra R (Quot_r A M) :=
  RingQuot.instAlgebraRingQuot _

-- verify there is no diamond
example (R : Type u) [CommRing R] :
    (algebraNat : Algebra ℕ (Quot_r R M)) = instAlgebra :=
  rfl

instance {R S A M} [CommRing R] [CommRing S] [CommRing A]
    [Algebra R A] [Algebra S A] [SMulCommClass R S A] :
    SMulCommClass R S (Quot_r A M)  :=
  RingQuot.instSMulCommClassRingQuot _

instance {R S A M} [CommRing R] [CommRing S] [CommRing A]
    [SMul R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] :
    IsScalarTower R S  (Quot_r A M) :=
  RingQuot.instIsScalarTowerRingQuot _

instance (R : Type u) [CommRing R] (M : Type v) :
    HasQuotient (Quot_r R M) (Ideal (Quot_r R M)) :=
  Submodule.hasQuotient

example (R : Type u) [CommRing R] (M : Type v) (I : Ideal (Quot_r R M)) :
    CommRing ((Quot_r R M) ⧸ I) :=
  Quotient.commRing I

count_heartbeats in
set_option synthInstance.maxHeartbeats 100000 in
set_option trace.profiler true in
set_option pp.proofs.withType false in
-- This one is still too slow
instance instAlgebra' (
    R M : Type _) [CommRing R] (I : Ideal (Quot_r R M)) :
    Algebra R ((Quot_r R M) ⧸ I) :=
Quotient.algebra R

[Eric Wieser]

Eric Wieser said:

Does making Quot_r reducible make things better or worse?

This is slow but within the main heartbeat limit:

import Mathlib.Algebra.RingQuot
import Mathlib.RingTheory.Ideal.QuotientOperations
import Mathlib.Data.MvPolynomial.CommRing

noncomputable section

open Finset MvPolynomial Ideal.Quotient Ideal RingQuot

variable (R : Type u) [CommSemiring R] (M : Type v)

-- A trivial relation is enough to show problems
inductive r : (MvPolynomial M R) → (MvPolynomial M R) → Prop

abbrev Quot_r := RingQuot (r R M)

set_option synthInstance.maxHeartbeats 40000 in
example (R M : Type _) [CommRing R] (I : Ideal (Quot_r R M)) :
    Algebra R ((Quot_r R M) ⧸ I) :=
  inferInstance

[Eric Wieser]

As a bonus it takes far less code

[Antoine Chambert-Loir]

Eric Wieser said:

Does making Quot_r reducible make things better or worse?

In the file below (the one adjusted after Kevin's indication that we had an obsolete mathlib), everything is just slightly faster, but not enough to have the last Algebra instance compile.

[Eric Wieser]

Doesn't my message above show that making it reducible and removing all the redundant instances makes things faster?

[Antoine Chambert-Loir]

I had written@[reducible] and switching to abbrev made it faster.
Apparently not enough for what comes later, unless the problem is different: I see Lean struggling with universes, telling me that max u v is not max v u…

[Eric Wieser]

Are you using Type _ or Type*?

[Antoine Chambert-Loir]

Type u, Type v, etc., but let me check that there isn't a hidden Type _ somewhere…

[Antoine Chambert-Loir]

(deleted)

[Antoine Chambert-Loir]

Forget what I said about theses universes, I had written something that couldn't type…
OTOH, it takes 15s to compile the final example, and in a real life application, it ends up being unable to synthesize the instance necessary to have algebraMap R (Quot_r R M ⧸ I)…

[Matthew Ballard]

Someone should double check me but this seems instant on mrb/reduce_eta2

[Junyan Xu]

Maybe related: if you add

instance [CommSemiring R] : AddCommMonoid (symmetricSubalgebra σ R) := inferInstance

after src#MvPolynomial.symmetricSubalgebra, you get a timeout:

failed to synthesize
  AddCommMonoid { x // x ∈ symmetricSubalgebra σ R }
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

(on commit 3d6112b5c7d095d3088b359c611a5a2704c5dbdc)

[Junyan Xu]

Oops, the timeout only appears with import Mathlib.Data.Finsupp.WellFounded which was authored by me ...

[Eric Wieser]

We have problems all over mathlib where we struggle to infer algebraic instances on Subalgebras

[Junyan Xu]

You mean in Lean 4, right?

[Matthew Ballard]

Actually in front of the computer now. Yes, this takes 0.05s for me

instance instAlgebra' (
    R M : Type _) [CommRing R] (I : Ideal (Quot_r R M)) :
    Algebra R ((Quot_r R M) ⧸ I) :=
Quotient.algebra R

[Matthew Ballard]

Eric's shorter one takes ~0.07s (and about half that with Type*).

[Antoine Chambert-Loir]

The same one takes 18s on my computer…

[Antoine Chambert-Loir]

together with a strange error : compiler IR check failed at '_example._rarg', error: unknown declaration 'MvPolynomial.instCommRingMvPolynomial'

[Matthew Ballard]

I am using a toolchain where given

structure A where

structure B extends A where

def  a : A := sorry

def b : B := { a with }

Lean will expand b to

let src := a
{ toA := src }

This presentation of the term seems more suited to unification.

There are some instances (somewhere) that would benefit from going from the {a with} pattern to {toA := a}. This is not very actionable alas.

[Kevin Buzzard]

The IR error just means "write noncomputable"

[Antoine Chambert-Loir]

The IR error was strange because I was already in a noncomputable section. But if I switch the order of open and section, it disappeared.

[Antoine Chambert-Loir]

Well, if I want things to go fast, here is what runs best:

import Mathlib.Algebra.RingQuot
import Mathlib.RingTheory.Ideal.QuotientOperations
import Mathlib.Data.MvPolynomial.CommRing



open Finset MvPolynomial Ideal.Quotient Ideal RingQuot

noncomputable section

set_option trace.profiler true

-- Defining an algebra as a quotient of polynomials
-- Experiments
-- A trivial relation is enough to show problems
inductive r (R : Type u) [CommSemiring R] (M : Type v) : (MvPolynomial M R) → (MvPolynomial M R) → Prop

def Quot_r (R : Type u) [CommSemiring R] (M : Type v) := RingQuot (r R M)

variable (R : Type u) [CommRing R] (M : Type v)

instance instCommRing' : CommRing (Quot_r R M) :=
  instCommRingRingQuotToSemiringToCommSemiring (r R M)

instance instAlgebra' (I : Ideal (Quot_r R M)) :
    Algebra R ((Quot_r R M) ⧸ I) := by
  dsimp [Quot_r]
  exact Ideal.Quotient.algebra R

def bar (I : Ideal (Quot_r R M)) :
    R →+* ((Quot_r R M) ⧸ I) :=
  @algebraMap R ((Quot_r R M) ⧸ I) _ (inferInstance) (instAlgebra' R M I)