[Merged by Bors] - perf(NumberTheory.NumberField.Basic): make RingOfIntegers a Type.

[riccardobrasca]

We make 𝓞 K a type rather then a Subalgebra to speed up instances search.

Co-authored-by: Anne Baanen <Vierkantor>
Co-authored-by: Yaël Dillies <YaelDillies>
Co-authored-by: Matthew Ballard <mattrobball>

---

[riccardobrasca]

!bench

[leanprover-bot]

Here are the benchmark results for commit 2ce7ff8.
There were significant changes against commit 90e480d:

  Benchmark                                                         Metric         Change
  =======================================================================================
+ ~Mathlib.NumberTheory.Cyclotomic.Rat                              instructions   -29.1%
+ ~Mathlib.NumberTheory.NumberField.Basic                           instructions   -33.6%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic        instructions   -39.0%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody   instructions   -27.7%
+ ~Mathlib.NumberTheory.NumberField.ClassNumber                     instructions   -48.1%
+ ~Mathlib.NumberTheory.NumberField.Discriminant                    instructions   -26.0%
+ ~Mathlib.NumberTheory.NumberField.FractionalIdeal                 instructions   -61.1%
+ ~Mathlib.NumberTheory.NumberField.Norm                            instructions   -30.6%
+ ~Mathlib.NumberTheory.NumberField.Units                           instructions   -21.2%

[Vierkantor]

I will try to address the review comments I made in the next hours.

[Vierkantor]

We should figure out why simp dislikes these lemmas.

[Vierkantor]

I tried for a bit and can't figure it out. If I write mk_add_mk _ then simp can use it (e.g. in restrict_addMonoidHom), but mk_add_mk is too hard.

[riccardobrasca]

Weird

[mattrobball]

If it works with _ and not without it, then there are some instance implicit arguments that cannot be found (or unified correctly) with typeclass synthesis. The underscore bypasses typeclass search for all arguments (if I remember correctly).

[Ruben-VandeVelde]

It's not because of the ⟨x, hx⟩ syntax?

[Vierkantor]

If it works with _ and not without it, then there are some instance implicit arguments that cannot be found (or unified correctly) with typeclass synthesis. The underscore bypasses typeclass search for all arguments (if I remember correctly).

I forgot to give more details but they seem not to even be considered according to the set_option trace output. So it doesn't even appear to arrive at the instance synth step. But afaict the terms match perfectly syntactically: the discrimination tree should just find the simp lemmas.

[riccardobrasca]

!bench

[leanprover-bot]

Here are the benchmark results for commit 19ed662.
There were significant changes against commit d96c1e7:

  Benchmark                                                         Metric         Change
  =======================================================================================
+ ~Mathlib.NumberTheory.Cyclotomic.Rat                              instructions   -35.4%
+ ~Mathlib.NumberTheory.NumberField.Basic                           instructions   -32.0%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic        instructions   -42.8%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody   instructions   -28.9%
+ ~Mathlib.NumberTheory.NumberField.ClassNumber                     instructions   -66.6%
+ ~Mathlib.NumberTheory.NumberField.Discriminant                    instructions   -26.1%
+ ~Mathlib.NumberTheory.NumberField.FractionalIdeal                 instructions   -71.9%
+ ~Mathlib.NumberTheory.NumberField.Norm                            instructions   -30.6%
+ ~Mathlib.NumberTheory.NumberField.Units                           instructions   -30.5%

[kbuzzard]

This is a very cool PR! It is kind of annoying that Lean 4's typeclass inference search is forcing us to do this, but on the other hand I don't really see any reason why we shouldn't do it anyway. IIRC we were already having problems with O_K as a subring being slow in Lean 3.

I have been thinking about the problem of how to set up this sort of problem on and off for years now, although as a non-specialist in type theory I have not really had good answers. In the Coq odd order proof they made all finite groups equal to subgroups of a large ambient group (so, in particular, terms). But this is not possible in ring theory because given two rings there might be no large ambient ring containing both as subrings (subrings must share a 1 with the ambient ring), so we are forced to reject this approach. IsScalarTower was our solution to making all rings equal to types, and for rings of integers of number fields we tried a different hybrid approach with the fields being types and the integer rings being terms, but the evidence we now have is that this is not as good a design pattern as just making everything a type anyway. I have had generations of students finding this part of the library painful to use; thanks a lot for making these changes!

[kbuzzard]

How about adding a coercion from O_K to K? I remember @Vierkantor once explaining to me why it was not possible to make algebraMap a coercion (something to do with head symbols, but I have forgotten the details, probably this means I didn't understand them properly). But is it possible here?

[Vierkantor]

I didn't define the coercion because I thought it would require a lot more work to set up the API: that it preserves the ring operations etc. With algebraMap we get that for free, in exchange for a lot more writing.

The reason we can't say instance : CoeHead (𝓞 K) K := ⟨algebraMap _ _⟩ is that all the metaprogramming needs a @[coe] attribute on the expression to identify a coercion. Specifically on the head symbol. In this case, because algebraMap is a bundled function, the head symbol is different from algebraMap in this case. We'd need to define a synonym for this map that is not bundled and we can give that the @[coe] attribute.

Following what @erdOne suggests, the coercion be defined something as:

@[coe]
abbrev val (x : 𝓞 K) : K := algebraMap _ _ x

/-- This instance has to be `CoeHead` because we only want to apply it from `𝓞 K` to `K`. -/
instance : CoeHead (𝓞 K) K := ⟨val⟩

Although I can't say for sure if making val an abbrev would work, perhaps it has to be a def.

[kbuzzard]

So you want the units to coerce to K, but not the integers?

[riccardobrasca]

We have flt-regular as a stress test for this, where we use units a lot. If bumping mathlib is a lot of trouble I will be back to this.

[Vierkantor]

I thought the same at the start of the refactor, now I'm slightly in favour of adding `.val` as a cast because it really is less cumbersome notation.

…

On 29 April 2024 11.50.36 CEST, Riccardo Brasca ***@***.***> wrote: @riccardobrasca commented on this pull request. > + +instance : CommRing (𝓞 K) := + inferInstanceAs (CommRing (integralClosure _ _)) +instance : IsDomain (𝓞 K) := + inferInstanceAs (IsDomain (integralClosure _ _)) +instance : CharZero (𝓞 K) := + inferInstanceAs (CharZero (integralClosure _ _)) +instance : Algebra (𝓞 K) K := + inferInstanceAs (Algebra (integralClosure _ _) _) +instance : NoZeroSMulDivisors (𝓞 K) K := + inferInstanceAs (NoZeroSMulDivisors (integralClosure _ _) _) +instance : Nontrivial (𝓞 K) := + inferInstanceAs (Nontrivial (integralClosure _ _)) + +variable {K} + Anyway do we really want this? It seems to me that this can just be confusing, while using `algebraMap` seems a rather natural way of doing this. -- Reply to this email directly or view it on GitHub: #12386 (comment) You are receiving this because you were mentioned. Message ID: ***@***.***>

[riccardobrasca]

I thought the same at the start of the refactor, now I'm slightly in favour of adding .val as a cast because it really is less cumbersome notation.
…
On 29 April 2024 11.50.36 CEST, Riccardo Brasca @.> wrote: @riccardobrasca commented on this pull request. > + +instance : CommRing (𝓞 K) := + inferInstanceAs (CommRing (integralClosure _ _)) +instance : IsDomain (𝓞 K) := + inferInstanceAs (IsDomain (integralClosure _ _)) +instance : CharZero (𝓞 K) := + inferInstanceAs (CharZero (integralClosure _ _)) +instance : Algebra (𝓞 K) K := + inferInstanceAs (Algebra (integralClosure _ _) _) +instance : NoZeroSMulDivisors (𝓞 K) K := + inferInstanceAs (NoZeroSMulDivisors (integralClosure _ _) _) +instance : Nontrivial (𝓞 K) := + inferInstanceAs (Nontrivial (integralClosure _ _)) + +variable {K} + Anyway do we really want this? It seems to me that this can just be confusing, while using algebraMap seems a rather natural way of doing this. -- Reply to this email directly or view it on GitHub: #12386 (comment) You are receiving this because you were mentioned. Message ID: @.>

I am not really against it. Do you mean adding it as a coercion or just the notation?

[Vierkantor]

Do you mean adding it as a coercion or just the notation?

As a coercion. I don't think that simply defining .val is enough to improve the situation.

[riccardobrasca]

Do you mean adding it as a coercion or just the notation?

As a coercion. I don't think that simply defining .val is enough to improve the situation.

OK, I am having a look.

[mathlib-bors]

Build failed:

• Build

[riccardobrasca]

!bench

[leanprover-bot]

Here are the benchmark results for commit 7b28e54.
There were significant changes against commit 4e159e0:

  Benchmark                                                         Metric         Change
  =======================================================================================
+ ~Mathlib.NumberTheory.Cyclotomic.Rat                              instructions   -41.0%
+ ~Mathlib.NumberTheory.NumberField.Basic                           instructions   -48.0%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic        instructions   -36.9%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody   instructions   -27.6%
+ ~Mathlib.NumberTheory.NumberField.ClassNumber                     instructions   -80.0%
+ ~Mathlib.NumberTheory.NumberField.Discriminant                    instructions   -28.8%
+ ~Mathlib.NumberTheory.NumberField.FractionalIdeal                 instructions   -76.3%
+ ~Mathlib.NumberTheory.NumberField.Norm                            instructions   -28.5%
+ ~Mathlib.NumberTheory.NumberField.Units.DirichletTheorem          instructions   -30.8%

[mattrobball]

Given it has already been blessed (and I barely touched it).

bors merge

[mathlib-bors]

Build failed:

• Build

[Vierkantor]

This looks more like a temporary build failure, so I'm going to retry:

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style