Algebra.id for IntermediateField

Stream: mathlib4

[Xavier Roblot]

The following snippet times out:

import Mathlib.FieldTheory.IntermediateField

variable {A E : Type*} [Field A] [Field E] [Algebra E A] (F : IntermediateField E A)

#synth Algebra F F

Looking at the trace, it seems that Lean decides at some point that its best bet is to prove Algebra A F which leads it to try to prove Algebra A E and from there it gets nowhere.
Rising synthInstance.maxHeartbeats to 150000 or providing a little hint such as

attribute [local instance 1001] Algebra.id

does help it synthesize the instance though.

[Eric Wieser]

attribute [-instance] IsDomain.toCancelCommMonoidWithZero IsDomain.toCancelMonoidWithZero makes it fast

[Eric Wieser]

I think these instances are forming loops somehow

[Kevin Buzzard]

What's wrong with making Algebra.id super-high priority? Whenever it applies it's going to be exactly what we're looking for, right?

[Kevin Buzzard]

#9887 to see what happens

[Kevin Buzzard]

ha ha apparently CI disagrees with this "it can't go wrong" argument :-)

[Xavier Roblot]

I find it very surprising that this change is causing trouble with linarith...

Error: ./././Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean:223:61: error: linarith failed to find a contradiction

[Matthew Ballard]

One problem with docs#Algebra.id is that docs#RingHom.id is not reducible. So when trying unification at reducible or instance transparency Lean won’t unfold it.

[Kevin Buzzard]

yeah mathlib is breaking at completely random places. See the current state of #9887, but it's still not compiling and I'm going to give up.

[Kevin Buzzard]

@Xavier Roblot the issue with linarith is that for some reason which I don't understand at all, (1 + t) / 2 is being replaced with Div.div (1 + t) 2 and this is not in the form which linarith understands (it's definitionally equal but not syntactically equal). Quite why my change caused this, I have no idea.

[Xavier Roblot]

I see. Anyway, thanks for the effort. I'll use one of the above tricks to fix the problem.

[Matthew Ballard]

Aside: #8386 gets pretty close to pushing it under the default limit. You need 35000.

[Eric Wieser]

Matthew Ballard said:

One problem with docs#Algebra.id is that docs#RingHom.id is not reducible. So when trying unification at reducible or instance transparency Lean won’t unfold it.

It sounds like using toRingHom in algebra instances (without overriding toFun) is an anti pattern then?

[Matthew Ballard]

Rewriting some instances like this sounds like a good experiment

[María Inés de Frutos Fernández]

I am having similar problems with IntermediateField. All of the following instances were found by infer_instance in Lean 3, but in Lean 4 I have to provide their proofs explicitly:

import Mathlib.FieldTheory.IntermediateField
import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
import Mathlib.FieldTheory.NormalClosure

noncomputable section

variable {K L : Type _} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L)

-- inferInstance does not find this
instance : Algebra E E := Algebra.id E

-- inferInstance does not find this
instance : SMul E E := Mul.toSMul E

-- inferInstance does not find this
instance aux : IsScalarTower K E E := IsScalarTower.right

-- inferInstance does not find this
instance : Module E E := Algebra.toModule

--ERROR: failed to synthesize SMul L ↥E (?)
instance : SMul E (AlgebraicClosure E) := sorry
-- @AlgebraicClosure.instSMulAlgebraicClosure E _ E _ _

instance aux' : IsScalarTower K L (AlgebraicClosure L) :=  inferInstance

-- inferInstance does not find this
instance : Algebra E ↥(normalClosure K E (AlgebraicClosure E)) :=
  normalClosure.algebra K E (AlgebraicClosure E)

-- inferInstance does not find this
instance :  SMul ↥E ↥(normalClosure K (↥E) (AlgebraicClosure ↥E)) := Algebra.toSMul

-- inferInstance does not find this
instance : Field ↥(normalClosure K E (AlgebraicClosure E)) :=
  SubfieldClass.toField (IntermediateField K (AlgebraicClosure E))
    (normalClosure K E (AlgebraicClosure E))

-- inferInstance does not find this
instance : IsScalarTower K E (normalClosure K (↥E) (AlgebraicClosure ↥E)) := by
  exact normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldInstMembershipInstSetLikeIntermediateFieldNormalClosureToSMulToCommSemiringToSemifieldToSemiringToDivisionSemiringToSemifieldToSMulToCommSemiringToSemiringToSemiringToDivisionSemiringToSemifieldToSubalgebraAlgebraToSMulAlgebra
    K (↥E) (AlgebraicClosure ↥E)

Moreover, in the SMul E (AlgebraicClosure E) instance, when I try to provide the proof explicitly I get ERROR: failed to synthesize SMul L ↥E.

[Kevin Buzzard]

Does Eric's fix above, removing some troublesome instances, work?

[María Inés de Frutos Fernández]

If I add attribute [local instance 1001] Algebra.id as Eric suggested, then the first instance is found. So I can similarly add Mul.toSMul, IsScalarTower.right, etc to get the others.
I tried adding the line attribute [-instance] IsDomain.toCancelCommMonoidWithZero IsDomain.toCancelMonoidWithZero as well, but this made no difference for me.
The sorryd instance still gives an error.

[Matthew Ballard]

Does the following work on master? (my cache is misbehaving)

import Mathlib.FieldTheory.IntermediateField
import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
import Mathlib.FieldTheory.NormalClosure

noncomputable section

variable {K L : Type _} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L)

attribute [-instance] IntermediateField.algebra' Subalgebra.algebra' Subalgebra.instSMulSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebra Subsemiring.smul Submonoid.smul IntermediateField.module' Subalgebra.instDistribMulActionSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebraToMonoidToMonoidToMonoidWithZeroToSubmonoidToNonAssocSemiringToSubsemiring Subsemiring.distribMulAction Submonoid.distribMulAction Subalgebra.isScalarTower_left Subsemiring.isScalarTower Submonoid.isScalarTower Subalgebra.isScalarTower_mid

instance : Algebra E E := inferInstance

instance : SMul E E := inferInstance

instance aux : IsScalarTower K E E := inferInstance

instance : Module E E := inferInstance

instance : SMul E (AlgebraicClosure E) :=  inferInstance

instance aux' : IsScalarTower K L (AlgebraicClosure L) :=  inferInstance

instance : Algebra E ↥(normalClosure K E (AlgebraicClosure E)) := inferInstance

instance :  SMul ↥E ↥(normalClosure K (↥E) (AlgebraicClosure ↥E)) := inferInstance

instance : Field ↥(normalClosure K E (AlgebraicClosure E)) := inferInstance

instance : IsScalarTower K E (normalClosure K (↥E) (AlgebraicClosure ↥E)) := inferInstance

[Kevin Buzzard]

All but two work very quickly on master: Algebra E ↥(normalClosure K E (AlgebraicClosure E)) and IsScalarTower K E (normalClosure K (↥E) (AlgebraicClosure ↥E)) time out.

[Matthew Ballard]

Two possibilities:

1. I did this on my working copy of #8386 so that might be it
2. I copied wrong

[Matthew Ballard]

The instances above open up a hole to SMul L E which takes forever to fail (or take forever with unification checks)

[Matthew Ballard]

I didn’t copy wrong

[Matthew Ballard]

This is similar to #mathlib4 > Timeout in Submodule (𝓞 K) (𝓞 K) in that the instances are not under-specified overall but the complement of the expensive-to-resolve classes is under-specified. So to fail we need to go through expensive checks

[Kevin Buzzard]

So this is holding up Maria-Ines' work, which in turn holds up Amelia's work, which in turn holds up my work, so I am super-motivated to try and understand and help fix what's going on here.

I thought a lot about these slow typeclass issues in algebra over the summer (when I had time to think) and saw lots of examples of slowness caused by typeclass goals of the form CommRing.ToCommSemiring R =?= CommRing.ToCommSemiring R which were taking forever to succeed, because one side would explode. We narrowed it down to certain instances being defined in the form A,B,C with and having lets in. I tried to remove a bunch of lets and had partial success. Since then I've become mired in 6 months of teaching (I finish late March) and Matt has taken over the reins, and Eric understands what's happening, but I've lost track. Now my understanding is that the main sin is not the let and that we now have a better understanding of the underlying problem, which is something to do with eta expansion, a concept which I am at worst hazy about.

This code here

import Mathlib.FieldTheory.IntermediateField
import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
import Mathlib.FieldTheory.NormalClosure

noncomputable section

variable {K L : Type _} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L)

set_option trace.profiler true
set_option synthInstance.maxHeartbeats 0
set_option maxHeartbeats 0
instance : Algebra E E := inferInstance

takes 21 seconds to succeed on my fast machine. If I plough through the instance trace I see that a big part of the problem is

[tryResolve] [17.066374s] ✅ IsDomain ↥E ≟ IsDomain ↥E

which is precisely one of these things which I was seeing all summer when I last thought a lot about these problems. This bifurcates into two problems, one of which is

                [delta] [8.548725s] ✅ Ring.toSemiring =?= Ring.toSemiring ▼
                  [] [8.548709s] ✅ CommRing.toRing =?= SubringClass.toRing E ▼
                    [] [8.548614s] ✅ CommRing.toRing =?= Function.Injective.ring Subtype.val _ _ _ _ _ _ _ _ _ _ _ _ ▼
                      [] [8.548491s] ✅ CommRing.toRing =?= let src := Function.Injective.mulZeroClass Subtype.val _ _ _;
                          let src_1 := Function.Injective.addGroupWithOne Subtype.val _ _ _ _ _ _ _ _ _ _;
                          let src_2 := Function.Injective.addCommGroup Subtype.val _ _ _ _ _ _ _;
                          let src_3 := Function.Injective.monoid Subtype.val _ _ _ _;
                          let src_4 := Function.Injective.distrib Subtype.val _ _ _;
                          Ring.mk AddGroupWithOne.zsmul _ ▶

and this is exactly the phenomenon which I was seeing all summer: Lean is finding two defeq semiring instances on E and then spending forever checking that they're defeq. I was blaming this on the lets but my understanding is that this is not the issue, and there are people out there who understand the actual issue but I'm not one of them.

The explosion here is caused by docs#Function.Injective.ring , whose definition is very withy:

@[reducible]
protected def Function.Injective.ring [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul ℕ β]
    [SMul ℤ β] [Pow β ℕ] [NatCast β] [IntCast β] (f : β → α) (hf : Injective f) (zero : f 0 = 0)
    (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
    (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
    (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ (x) (n : ℤ), f (n • x) = n • f x)
    (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (nat_cast : ∀ n : ℕ, f n = n)
    (int_cast : ∀ n : ℤ, f n = n) : Ring β :=
  { hf.mulZeroClass f zero mul, -- porting note: had to add this explicitly?
    hf.addGroupWithOne f zero one add neg sub nsmul zsmul nat_cast int_cast,
    hf.addCommGroup f zero add neg sub nsmul zsmul,
    hf.monoid f one mul npow,
    hf.distrib f add mul with }

and which expands to

fun {α} {β} [Ring α] [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul ℕ β] [SMul ℤ β] [Pow β ℕ] [NatCast β]
    [IntCast β] f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast ↦
  let src := Injective.mulZeroClass f hf zero mul;
  let src_1 := Injective.addGroupWithOne f hf zero one add neg sub nsmul zsmul nat_cast int_cast;
  let src_2 := Injective.addCommGroup f hf zero add neg sub nsmul zsmul;
  let src_3 := Injective.monoid f hf one mul npow;
  let src_4 := Injective.distrib f hf add mul;
  Ring.mk AddGroupWithOne.zsmul _

It's at this point in the conversation when people now pop in and start talking about eta and I get lost. Have I isolated at least one of the problems here, and how does one go about fixing it?

[Matthew Ballard]

I think the problem with Function.Injective.ring is that it has unify data over and over again. Once for itself and then for each of the supplied instances

[Kevin Buzzard]

Right: the next bi(multi)furcation is

                                [] [8.604870s] ✅ Ring.mk Ring.zsmul _ =?= Ring.mk AddGroupWithOne.zsmul _ ▼
                                  [] [1.236130s] ✅ Ring.zsmul =?= AddGroupWithOne.zsmul ▶
                                  [] [3.741473s] ✅ Ring.toSemiring =?= Semiring.mk _ _ Monoid.npow ▶
                                  [] [1.204535s] ✅ Ring.toNeg =?= AddGroupWithOne.toNeg ▶
                                  [] [1.197401s] ✅ Ring.toSub =?= AddGroupWithOne.toSub ▶
                                  [] [1.224481s] ✅ Ring.toIntCast =?= AddGroupWithOne.toIntCast ▶

and expanding one of these at random (I choose Neg) the next bifurcation is

                                    [] [1.204373s] ✅ AddGroupWithOne.toNeg =?= AddGroupWithOne.toNeg ▼
                                      [delta] [1.204269s] ✅ AddGroupWithOne.toNeg =?= AddGroupWithOne.toNeg ▼
                                        [] [1.203737s] ✅ Function.Injective.addGroupWithOne Subtype.val _ _ _ _ _ _ _ _ _
                                              _ =?= Function.Injective.addGroupWithOne Subtype.val _ _ _ _ _ _ _ _ _ _ ▼
                                          [delta] [1.203617s] ✅ Function.Injective.addGroupWithOne Subtype.val _ _ _ _ _ _ _ _ _
                                                _ =?= Function.Injective.addGroupWithOne Subtype.val _ _ _ _ _ _ _ _ _ _ ▼
                                            [] [0.662417s] ✅ Distrib.toAdd =?= Distrib.toAdd ▶
                                            [] [0.527991s] ✅ Semiring.toNatCast =?= Semiring.toNatCast ▶

and these bifurcations just occur again and again (for example the Distrib.toAdd one bifurcates to

                                                                [] [0.661214s] ✅ NonUnitalNonAssocSemiring.mk _ _ _ _ =?= NonUnitalNonAssocSemiring.mk _ _ _ _ ▼
                                                                  [] [0.306879s] ✅ AddCommMonoid.mk _ =?= NonUnitalNonAssocSemiring.toAddCommMonoid ▶
                                                                  [] [0.353811s] ✅ NonUnitalNonAssocRing.toMul =?= NonUnitalNonAssocSemiring.toMul ▶

(so to answer a question about Neg we seem to be now answering a question about Mul, which to me is very weird)

[Matthew Ballard]

I think writing versions of Function.Injective.*/Function.Surjective.* only for Subtype.coe/Quotient.mk using less data might help

[Matthew Ballard]

I am not sure if there is a fix for the pattern occurring in the all the disabled instances above other than not making them instances. @Anne Baanen might have more ideas

[Kevin Buzzard]

I was hoping you were going to say "my work here will sort all of this out, don't worry".

[Matthew Ballard]

No

[Matthew Ballard]

Should help sure but there are other problems

[Kevin Buzzard]

I don't understand that work properly, you see, so I always feel a bit like I'm floundering around.

[Kevin Buzzard]

I would like to contribute but I need supervision.

[Matthew Ballard]

I don’t think the eta reductions can be pushed any further but writing versions of these instance transport defs which only apply to Subtype.coe/Quotient.mk is still untouched

[Matthew Ballard]

There was a (some?) thread(s) about this a while back. I will search when I get to a more conducive machine

[Sébastien Gouëzel]

Not directly related, but it made a big difference in the Lean 3 days: we had a linter to check the priority of instances, with the rule that instances that always apply (i.e., they involve a generic type, instead of a type constructed in a specific way) should have priority < 1000. The day this was implemented (by @Floris van Doorn I think?) and enforced throughout the library, all of a sudden things got much better for many searches.

I don't think we have this in Lean 4. For a long time it was blocked by the fact that priorities could not be changed after the fact, but I don't think it's the case any more so if someone with meta skills wanted to have a look it could be a big gain for a minor(?) investment. (More precisely, I'd be willing to spend a lot of time fixing the library if someone writes the linter for me :-)

For instance, for now, if one is looking for a monoid structure on A x B, I think there's no reason that Monoid.Prod (or whatever it's named) would be tried before Group.toMonoid, while obviously the former is the thing to do.

[Matthew Ballard]

Yeah, I think a lot more care with priorities would be great

[Eric Rodriguez]

Would it not be nice for this to be enforced directly by Lean itself? On the other hand that does require a core change...

[Ruben Van de Velde]

I don't understand much either, but I do recall Function.injective.foo coming up as a red flag a number of times

[Matthew Ballard]

Matthew Ballard said:

There was a (some?) thread(s) about this a while back. I will search when I get to a more conducive machine

This is a version where the data is replaced by proofs

Matthew Ballard said:

I think the best way forward is to make things passing through RingCon faster overall by going from

variable [CommRing α]

@[reducible]
protected def Function.Injective.commRing [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β]
    [SMul ℕ β] [SMul ℤ β] [Pow β ℕ] [NatCast β] [IntCast β] (f : β → α) (hf : Injective f)
    (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x)
    (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x)
    (zsmul : ∀ (x) (n : ℤ), f (n • x) = n • f x) (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n)
    (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) : CommRing β := ...

to

variable [CommRing α]

@[reducible]
protected def Function.Injective.commRing' (f : β → α) (hf : Injective f)
    (zero : 0 ∈ Set.range f) (one : 1 ∈ Set.range f) (add : ∀ x y, f x + f y ∈ Set.range f)
    (mul : ∀ x y, f x * f y ∈ Set.range f) (neg : ∀ x, -f x ∈ Set.range f)
    (sub : ∀ x y, f x - f y ∈ Set.range f) (nsmul : ∀ (x) (n : ℕ), n • f x ∈ Set.range f)
    (zsmul : ∀ (x) (n : ℤ), n • f x ∈ Set.range f) (npow : ∀ (x) (n : ℕ), f x ^ n ∈ Set.range f)
    (nat_cast : ∀ n : ℕ, (n : α) ∈ Set.range f) (int_cast : ∀ n : ℤ, (n : α) ∈ Set.range f) : CommRing β := ...

in some spots and for Function.Surjective similarly.

Or maybe just for Subtype.coe and Quotient.mk alone.

[Matthew Ballard]

It may have been refined more elsewhere

[Matthew Ballard]

Kevin Buzzard said:

All but two work very quickly on master: Algebra E ↥(normalClosure K E (AlgebraicClosure E)) and IsScalarTower K E (normalClosure K (↥E) (AlgebraicClosure ↥E)) time out.

No quick fix here that I see other than #8386

[Matthew Ballard]

Removing aux and aux’ makes those also timeout on #8386

[Yaël Dillies]

Kevin Buzzard said:

Right: the next bi(multi)furcation is [...}

I can't help but thinking this means this happens because we're not respecting the preferred parent of Ring

[Anne Baanen]

Kevin Buzzard said:

If I plough through the instance trace I see that a big part of the problem is

[tryResolve] [17.066374s] ✅ IsDomain ↥E ≟ IsDomain ↥E

Certainly we should fix the slow Function.Injective unification issues, but why is IsDomain even needed here? Presumably by tweaking priorities/modifying instances we can avoid hitting the real slow path.

[Yaël Dillies]

This is all coming from instances declared via extends having normal priority (instead of 100), right?

[Anne Baanen]

Yes, that will be a big part of it.

[Yaël Dillies]

Okay here I notice that Function.Injective.semiring is not even used in the definition of Function.Injective.ring. This seems very very wrong.

[Yaël Dillies]

I'm gonna open a PR using preferred parents and we can benchmark it.

[Anne Baanen]

Looks like this is the path onto IsDomain:

      [] ✅ apply @IntermediateField.algebra' to Algebra ↥E ↥E ▼
        [tryResolve] ✅ Algebra ↥E ↥E ≟ Algebra ↥E ↥E
        [] new goal SMul (↥E) K ▶
      [] ✅ apply @SMulZeroClass.toSMul to SMul (↥E) K ▶
      [] ✅ apply @SMulWithZero.toSMulZeroClass to SMulZeroClass (↥E) K ▼
        [tryResolve] ✅ SMulZeroClass (↥E) K ≟ SMulZeroClass (↥E) K
        [] new goal Zero ↥E ▶
      [] ✅ apply @CommMonoidWithZero.toZero to Zero ↥E ▶
      [] ✅ apply @CancelCommMonoidWithZero.toCommMonoidWithZero to CommMonoidWithZero ↥E ▶
      [] ✅ apply @IsDomain.toCancelCommMonoidWithZero to CancelCommMonoidWithZero ↥E ▶

[Yaël Dillies]

Weird. docs#IsDomain.toCancelCommMonoidWithZero has priority 100

[Anne Baanen]

Yeah, but IntermediateField.algebra' probably should have low priority (like we recently changed for Subalgebra.module').

[Anne Baanen]

Indeed, lowering the priority makes this a lot faster:

attribute [instance 100] IntermediateField.algebra' Subalgebra.algebra'

set_option trace.profiler true
count_heartbeats in
instance : Algebra E E := inferInstance
/-
▶ 12:1-13:1: information:
Used 9186 heartbeats, which is less than the current maximum of 200000.

▶ 12:1-13:1: information:
[Elab.command] [0.589160s] count_heartbeats
      in instance : Algebra E E :=
        inferInstance ▶
-/

(My system is about twice as slow as Kevin's, according to our profiler outputs.)

[Anne Baanen]

#9936

[Yaël Dillies]

Priority 100 is for instances that always apply, right? This is not the case here, so maybe you should choose 900 or something? Smaller than default, but greater than 100.

[Matthew Ballard]

Yaël Dillies said:

I'm gonna open a PR using preferred parents and we can benchmark it.

I think was tried before to mixed results. Maybe intervening changes will help though

[Anne Baanen]

Yaël Dillies said:

Priority 100 is for instances that always apply, right? This is not the case here, so maybe you should choose 900 or something? Smaller than default, but greater than 100.

I went with (priority := low) like what we have for docs#Subalgebra.module' now. I suppose it's slightly more selective than the blanket instance so indeed it deserves a higher number. I don't actually know what the Lean 4 constants are, though!

[Yaël Dillies]

I was working under the assumption that preferred parents were set first, so if nothing else making sure they actually are will help me better understand the situation! (plus, it's good to have a consistent style for those declarations)

[Yaël Dillies]

#9938 for the switch to preferred parents

[Matthew Ballard]

Eric Wieser said:

Matthew Ballard said:

One problem with docs#Algebra.id is that docs#RingHom.id is not reducible. So when trying unification at reducible or instance transparency Lean won’t unfold it.

It sounds like using toRingHom in algebra instances (without overriding toFun) is an anti pattern then?

And smul. Experiment at #9949 with Algebra.id to check performance impact

[Eric Wieser]

I worry that Module.compHom has a problem here too

[Eric Wieser]

Maybe this is an argument that we need unbundled IsRingHom predicates, even if most of the time we keep usingRingHom

[Eric Wieser]

Maybe instance reducibility is just a weird concept?

[Matthew Ballard]

Oliver Nash said:

I'm quite surprised by a failure illustrated in Example 2 below. It has the characteristics that:

1. simp only [Pi.smul_apply] fails but both simp only [Pi.smul_apply _] and rw [Pi.smul_apply] work,
2. the failure is triggered by adding let statement to the context which does not change the goal.

Here are the examples:

import Mathlib.Data.Pi.Algebra
import Mathlib.Algebra.Algebra.Basic

-- Example 1: succeeds
example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  simp only [Pi.smul_apply] -- succeeds

-- Example 2: fails!
example {α R : Type*} [CommRing R] (f : α → R) (r : R) (a : α) :
    (r • f) a = r • (f a) := by
  let bar : SMul R R := SMulZeroClass.toSMul
  simp only [Pi.smul_apply] -- Fails!

These work now. :)

[Matthew Ballard]

Matthew Ballard said:

So in well-studied example of Pi.smul_apply #lean4 > simp [X] fails, rw [X] works we have three options to have simp work "as expected":

1. Make the instance implicit just implicit #9020
2. Make RingHom.id (and intermediate defs reducible) #9025
3. Use simp [Pi.smul_apply _].

Option 2 follows the general principles for handling this situation but the (mind-numbed) implementation is horrifically slower overall. Option 3 muddles us along.

This gives Option 4 which follows existing best practices.

[Kevin Buzzard]

Here's some code from that IntermediateField file:

/- More general form of `IntermediateField.algebra`.

This instance should have low priority since it is slow to fail:
before failing, it will cause a search through all `SMul K' K` instances,
which can quickly get expensive.
-/
instance (priority := 500) algebra' {K'} [CommSemiring K'] [SMul K' K] [Algebra K' L]
    [IsScalarTower K' K L] :
    Algebra K' S :=
  S.toSubalgebra.algebra'

That instance can be discovered by inferInstance -- it's not necessary. What are the consequences of making a low priority shortcut instance?

[Kevin Buzzard]

@María Inés de Frutos Fernández here's a workaround using #10116 :

import Mathlib.FieldTheory.IntermediateField
import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
import Mathlib.FieldTheory.NormalClosure

noncomputable section

variable {K L : Type _} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L)

instance : Algebra E E := inferInstance

attribute [-instance]
  Subalgebra.instSMulSubtypeMemSubalgebraInstMembershipInstSetLikeSubalgebra
  Subsemiring.smul
  Submonoid.smul
  IntermediateField.module'
  Subalgebra.isScalarTower_left
  Subsemiring.isScalarTower
  Submonoid.isScalarTower

instance : SMul E E := inferInstance

instance aux : IsScalarTower K E E := inferInstance

instance : Module E E := inferInstance

instance : SMul E (AlgebraicClosure E) := inferInstance

instance aux' : IsScalarTower K L (AlgebraicClosure L) :=  inferInstance

set_option synthInstance.maxHeartbeats 400000
instance : Algebra E ↥(normalClosure K E (AlgebraicClosure E)) :=
inferInstance

instance :  SMul ↥E ↥(normalClosure K (↥E) (AlgebraicClosure ↥E)) := inferInstance

instance : Field ↥(normalClosure K E (AlgebraicClosure E)) := inferInstance

instance : IsScalarTower K E (normalClosure K (↥E) (AlgebraicClosure ↥E)) := inferInstance

[Kevin Buzzard]

Oh in fact this works fine on master.

[Kevin Buzzard]

Inspired by docs#Algebra -- do we have this:

class foo (R : Type u) (A : Type v) [CommMonoid R] [Monoid A] extends SMul R A,
  R →* A where
  commutes' : ∀ r x, toMonoidHom r * x = x * toMonoidHom r
  smul_def' : ∀ r x, r • x = toMonoidHom r * x

?

[Kevin Buzzard]

Should we (a) have it (b) make it a coercion (c) let Algebra extend it?

There are a lot of fields going on in Maria Ines' example. We have L/K a field extension (so types), E an intermediate field (so a term), but then immediately promoted to a type (so \u E is now a K-algebra) and then AlgebraicClosure E is a new type, and in my head I have a picture of all the fields and their inclusions, commonly represented on a whiteboard by a graph with smaller fields under bigger ones, and I can see it's blatantly obvious that K acts on AlgebraicClosure E because of the picture, but typeclass inference has a real problem with this. For example

instance foo (A B C : Type*) [CommSemiring A] [CommSemiring B] [Semiring C]
  [Algebra A B] [Algebra B C] : Algebra A C := by sorry

fails some linting test because B isn't mentioned in the output, so transitivity of Algebra (part of the geometry of the diagram) is not understood by the typeclass inference system. This is why you get it floundering around asking for Algebra E K (i.e. the other way around from what it shoeld be, clearly should be rejected as nonsense or at the worst unlikely but the system takes a long time to fail with this stuff

[María Inés de Frutos Fernández]

If I am not mistaken, this foo class is the lift_monoid_hom proposed in @Anne Baanen 's thesis, and I agree that it would be very convenient if this could be made into a coercion and extended by Algebra, but Anne said this is not compatible with the current Lean 4 coercion mechanism.

[Anne Baanen]

Indeed! The specific issue that I see is that coercions are now expanded: where the term in Lean 3 looked like @coe A B { coe := foo } x, in Lean 4 the term looks like foo x. So we'd have to teach tactics like the simplifier that when they see foo (a * b) then they can apply coe_mul. It's possible but not so easy.

[Anne Baanen]

I feel like we're running into the limits of what a single Algebra class can do. Just like for coercions we have Coe, CoeHead, CoeOut and so on, I think we also need to make the construction of the transitive closure explicit here. That would look like instances having type Algebra and theorems assuming AlgebraT (and in between these two there is "hidden" machinery for making id and transitivity work, that mathematicians can hopefully just ignore).

[Anne Baanen]

Kevin Buzzard said:

Should we (a) have it (b) make it a coercion (c) let Algebra extend it?

I would like it! The drawback is that this is going to cause quite some redundancy with the heavy Algebra machinery I propose. So that was why I proposed in Lean 3 to reuse the coercion mechanism.

[Anne Baanen]

There is a way to redo the Lean 3 design, although it's not quite optimal:

• Introduce a new operation, let's say lift, which comes from class LiftT (A B : Type*) := (lift : A → B). Make instances so LiftT is the reflexive transitive closure of Lift, analogous to LiftT and CoeT.
• Optional: declare lift to be a coercion and add the corresponding CoeT instance.
• Create classes saying "this LiftT is a monoid/ring/etc hom":

class MonoidLift (A B : Type*) [LiftT A B] [Monoid A] [Monoid B] :=
  (lift_one : lift (1 : A) = (1 : B))
  (lift_mul : ∀ x y : A, (lift (x * y) : B) = lift x * lift y)

• Replace (most of) our Algebra hierarchy with Lift, LiftOut, ... and RingLift instances.

[Anne Baanen]

The advantage is that we can redo the Algebra hierarchy with a more principled / effective search mechanism, and that the same will work for monoids, etc.

[Anne Baanen]

Some drawbacks:

• Existing maps such as Nat.cast are coercions, not lifts, so tactics still won't recognize that RingLift applies here.
• By writing every map as lift and only distinguishing which lift we mean by instances, we lose most advantages of the discrimination tree: simp might get somewhat slower.
• Unlike algebraMap, lift is a plain function: we'd have to bundle it explicitly to get a RingHom.