Subalgebra/Submodule rewrite failure

Stream: mathlib4

[Junyan Xu]

The following code compiles but fails with the error tactic 'rewrite' failed, motive is not type correct at the first line when the whole Mathlib is imported:

import Mathlib.LinearAlgebra.FreeAlgebra

open Cardinal

theorem Algebra.rank_adjoin_le {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S]
    (s : Set S) : Module.rank R (adjoin R s) ≤ max #s ℵ₀ := by
  rw [adjoin_eq_range_freeAlgebra_lift]
  cases subsingleton_or_nontrivial R
  · rw [rank_subsingleton]; exact one_le_aleph0.trans (le_max_right _ _)
  change Module.rank R (LinearMap.range (FreeAlgebra.lift R Subtype.val).toLinearMap) ≤ _
  rw [← lift_le.{max u v}]
  refine (lift_rank_range_le _).trans ?_
  rw [FreeAlgebra.rank_eq, lift_id'.{v,u}, lift_umax.{v,u}, lift_le, max_comm]
  exact mk_list_le_max _

Not sure what's causing the problem. cc @Eric Wieser

[Eric Wieser]

I think unfortunately the game is now to prune the imports until you find the one that matters

[Matthew Ballard]

I vote category theory :)

[Riccardo Brasca]

You can try importing a very deep file in category theory and see if the error is still there.

[Kevin Buzzard]

import Mathlib.Algebra.DirectSum.Internal breaks it, but

import Mathlib.Algebra.Algebra.Operations
import Mathlib.Algebra.Algebra.Subalgebra.Basic
import Mathlib.Algebra.DirectSum.Algebra

(its imports) doesn't

[Junyan Xu]

I was expecting #synth can tell the difference, but no matter I import Mathlib or just the FreeAlgebra file, #synth is showing that both instances come from docs#Subalgebra.instModuleSubtypeMem

variable {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (s : Set S)
#synth Module R (Algebra.adjoin R s)
#synth Module R ((FreeAlgebra.lift R) ((↑) : s → S)).range

[Kevin Buzzard]

instance AddCommMonoid.ofSubmonoidOnSemiring [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R]
    (A : ι → σ) : ∀ i, AddCommMonoid (A i) := fun i => by infer_instance

seems to be the culprit

[Matthew Ballard]

Can that be deleted?

[Kevin Buzzard]

import Mathlib.LinearAlgebra.FreeAlgebra

section from_Mathlib.Algebra.DirectSum.Internal

variable {ι : Type*} {σ S R : Type*}

--uncomment to break
-- instance AddCommMonoid.ofSubmonoidOnSemiring [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R]
--     (A : ι → σ) : ∀ i, AddCommMonoid (A i) := fun i => by infer_instance

end from_Mathlib.Algebra.DirectSum.Internal

universe u v

open Cardinal

theorem Algebra.rank_adjoin_le {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S]
    (s : Set S) : Module.rank R (adjoin R s) ≤ max #s ℵ₀ := by
  rw [adjoin_eq_range_freeAlgebra_lift]
  cases subsingleton_or_nontrivial R
  · rw [rank_subsingleton]; exact one_le_aleph0.trans (le_max_right _ _)
  change Module.rank R (LinearMap.range (FreeAlgebra.lift R Subtype.val).toLinearMap) ≤ _
  rw [← lift_le.{max u v}]
  refine (lift_rank_range_le _).trans ?_
  rw [FreeAlgebra.rank_eq, lift_id'.{v,u}, lift_umax.{v,u}, lift_le, max_comm]
  exact mk_list_le_max _

[Junyan Xu]

This is very weird. AddCommMonoid.ofSubmonoidOnSemiring is only a shortcut instance, so the root cause lies deeper.

[Junyan Xu]

Is it suggesting the problem is with Add not SMul? But the underlying instance docs#AddSubmonoidClass.toAddCommMonoid definitely looks very innocent. And my example has nothing to do with Pi types. How does the shortcut instance affect the synthesis path?

[Junyan Xu]

It looks like it might be Add's problem. When importing Mathlib both instances are given by docs#AddCommGroup.ofSubgroupOnRing, while when importing FreeAlgebra both are given by docs#Ring.toAddCommGroup

variable {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] (s : Set S)
#synth AddCommGroup (Algebra.adjoin R s)
#synth AddCommGroup (FreeAlgebra.lift R ((↑) : s → S)).range

For the AddCommMonoid instances (required by Module), the instances are given by docs#AddCommMonoid.ofSubmonoidOnSemiring (the one Kevin found) and docs#NonUnitalNonAssocSemiring.toAddCommMonoid respectively.

[Junyan Xu]

The synthesis results are very interesting! I never expected it splits Algebra.adjoin R s as a function application, and the AlgHom.range _ as well!

AddCommMonoid.ofSubmonoidOnSemiring (Algebra.adjoin R) s
AddCommMonoid.ofSubmonoidOnSemiring AlgHom.range ((FreeAlgebra.lift R) Subtype.val)

But there's nothing fishy going on here. Still haven't found the root cause ...

[Eric Wieser]

I would guess that AddCommMonoid.ofSubmonoidOnSemiring causes it to capture terms of an arbitrary type ι under binders, which then gets in the way of rewrites: so this isn't a diamond, but it's an unwanted eta expansion

[Eric Wieser]

Matthew Ballard said:

Can that be deleted?

Did someone try? This might be left from Lean 3

[Eric Wieser]

This works fine:

import Mathlib

open Cardinal

theorem Algebra.rank_adjoin_le {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S]
    (s : Set S) : Module.rank R (adjoin R s) ≤ max #s ℵ₀ := by
  unfold AddCommMonoid.ofSubmonoidOnSemiring  -- added
  rw [adjoin_eq_range_freeAlgebra_lift]
  cases subsingleton_or_nontrivial R
  · rw [rank_subsingleton]; exact one_le_aleph0.trans (le_max_right _ _)
  change Module.rank R (LinearMap.range (FreeAlgebra.lift R Subtype.val).toLinearMap) ≤ _
  rw [← lift_le.{max u v}]
  refine (lift_rank_range_le _).trans ?_
  rw [FreeAlgebra.rank_eq, lift_id'.{v,u}, lift_umax.{v,u}, lift_le, max_comm]
  exact mk_list_le_max _

[Eric Wieser]

maybe making AddCommMonoid.ofSubmonoidOnSemiring an abbrev is also enough

[Kevin Buzzard]

Eric Wieser said:

Matthew Ballard said:

Can that be deleted?

Did someone try? This might be left from Lean 3

What are your feelings on the next line,

instance AddCommGroup.ofSubgroupOnRing [Ring R] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ) :
    ∀ i, AddCommGroup (A i) := fun i => by infer_instance

?

[Eric Wieser]

Probably also harmful

[Eric Wieser]

I think I added these because I had no choice, not because I wanted them

[Junyan Xu]

Eric Wieser said:

I would guess that AddCommMonoid.ofSubmonoidOnSemiring causes it to capture terms of an arbitrary type ι under binders, which then gets in the way of rewrites: so this isn't a diamond, but it's an unwanted eta expansion

Yeah, I can see the difference between Set S and FreeAlgebra R { x // x ∈ s } →ₐ[R] S probably caused the trouble.

@AddCommMonoid.ofSubmonoidOnSemiring (Set S) (Subalgebra R S) S Ring.toSemiring Subalgebra.instSetLike ⋯
  (Algebra.adjoin R) s : AddCommMonoid ↥(Algebra.adjoin R s)

@AddCommMonoid.ofSubmonoidOnSemiring (FreeAlgebra R { x // x ∈ s } →ₐ[R] S) (Subalgebra R S) S Ring.toSemiring
  Subalgebra.instSetLike ⋯ AlgHom.range ((FreeAlgebra.lift R) Subtype.val) : AddCommMonoid ↥((FreeAlgebra.lift R) Subtype.val).range

[Kevin Buzzard]

In Lean 4 the Internal file compiles without the instances. #18149

[Eric Wieser]

Did abbrev also fix the issue?

[Eric Wieser]

Not because I think it's a better solution, but to help understand the problem better

[Junyan Xu]

Eric Wieser said:

Did abbrev also fix the issue?

Yeah, changing instance to abbrev in Kevin's code doesn't break the proof. (I mean, the proof is then no longer broken.)

[Eric Wieser]

The proof in this thread or the proof in that file?

[Eric Wieser]

Sorry, that was a stupid suggestion

[Eric Wieser]

@[reducible] instance is what I meant

[Eric Wieser]

Or @[instance] abbrev

[Junyan Xu]

Both would still break my proof

[Eric Wieser]

Is there a Module version of this instance in a later file that we should also remove?

[Kevin Buzzard]

mathlib compiles with the removal of the ∀ i, AddCommMonoid (A i) and ∀ i, AddCommGroup (A i) instances, but I can't see any module instances, although we do have Semiring (A 0), CommSemiring (A 0) etc instances.

[Floris van Doorn]

docs#AddCommMonoid.ofSubmonoidOnSemiring seems like a bad instance. What is even the reason of stating it as
(A : ι → σ) (i : ι) : AddCommMonoid ↥(A i) instead of (A : σ) : AddCommMonoid ↥A? (sorry if this was mentioned before, I didn't read everything here.)

[Floris van Doorn]

Oh, is it precisely because type-class inference struggles with these dependent types (or did so in Lean 3)?

[Matthew Ballard]

Benchmarking indicates they seem to help a bit locally but overall effect is negligible

[Eric Wieser]

Kevin Buzzard said:

although we do have Semiring (A 0), CommSemiring (A 0) etc instances.

These are surely bad enough to be scoped, but I never go around to it since they didn't cause any visible trouble

[Floris van Doorn]

I think removing all the instances like this we don't need anymore in Lean 4 and scoping the remainder would be very good.

[Matthew Ballard]

Any objections to #18149 before it boards the merge train? (Fixed: thanks Floris)

[Floris van Doorn]

#18149

[Eric Wieser]

The A 0 instances were never a Lean 3 hack, but rather a questionable feature of my own making

[Kevin Buzzard]

Yes, my students needed them a few months ago, they're much newer

[Eric Wieser]

Maybe some of them are, but I wrote many of them at the same time as the ones we're deleting, I thought

[Matthew Ballard]

I remember them being stress-tested in a past PR

[Eric Wieser]

They exist because there is no way to say "Let $A_i$ be a collection of additive monoids where $A_0$ is also a semi ring"

[Junyan Xu]

Side story: I discovered this issue because nowadays I usually write little lemmas in the web editor importing Mathlib, and later use #find_home to put them into appropriate files. (Maybe a healthy habit to promote!) I had to use docs#Subalgebra.rank_toSubmodule (a rfl lemma) due to this failure, and since LinearAlgebra.FreeAlgebra is only imported by a leaf file, #find_home suggested Mathlib itself, so I ended up importing LinearAlgebra.Dimension.Constructions into LinearAlgebra.FreeAlgebra, causing a large-import alert. I decided to use change rather than the rfl lemma and remove the import, but was surprised to find the rewrite simply works in LinearAlgebra.FreeAlgebra. I went back to recheck this doesn't work with import Mathlib and opened this topic.

I think many people (including myself) encountered such rewrite failures many times before, but in the case of myself, I just wasn't sufficiently convinced that such failures are something that shouldn't happen to report them.