!4#4891 FieldTheory.SplittingField

Stream: mathlib4

[Riccardo Brasca]

In !4#4339 a lot of definitions (for example addition on splitting fields) are defined using Nat.recOn. in mathlib, Lean is able to guess the motive and the definitions are quite pleasant. Now, it seems we have to explicitly tell Lean what the motive is.

Is this a known problem? Is there something we can do?

CC @Ruben Van de Velde @Eric Rodriguez

[Kevin Buzzard]

Yeah lean 4 has got a lot worse at this. And I bet your motives are not good...

[Kevin Buzzard]

(you can at least write (motive := ...) instead of the @ approach

[Riccardo Brasca]

Yes, that's what we're doing

[Jeremy Tan]

I believe this is a file that will immediately compel us to improve core just so we can port it, like OperatorNorm

[Chris Hughes]

Is it just missing an elab_as_eliminator attribute or something similar?

[Riccardo Brasca]

@Chris Hughes I don't know. But if you want to give a try you're more than welcome...

[Damiano Testa]

I'm looking at the file now. Changing

theorem X_sub_C_mul_removeFactor (f : K[X]) (hf : f.natDegree ≠ 0) :
    (X - C (AdjoinRoot.root f.factor)) * f.removeFactor = map (AdjoinRoot.of f.factor) f :=
  let ⟨g, hg⟩ := factor_dvd_of_natDegree_ne_zero hf
  mul_divByMonic_eq_iff_isRoot.2 <| by
  rw [IsRoot.def, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, MulZeroClass.zero_mul]

to

theorem X_sub_C_mul_removeFactor (f : K[X]) (hf : f.natDegree ≠ 0) :
    (X - C (AdjoinRoot.root f.factor)) * f.removeFactor = map (AdjoinRoot.of f.factor) f := by
  let ⟨g, hg⟩ := factor_dvd_of_natDegree_ne_zero hf
  apply (mul_divByMonic_eq_iff_isRoot (R := AdjoinRoot f.factor) (a := AdjoinRoot.root f.factor)).mpr
  rw [IsRoot.def, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, MulZeroClass.zero_mul]

makes the elaboration time go from over 50s to <16s. I have already seen elsewhere that apply is sometimes much faster than refine/exact or term-mode. In this case, not providing explicitly the implicit arguments R and a doubles the elaboration time to ~34s.

[Damiano Testa]

I guess that similar hacks could be done systematically, but it also does not seem the right solution to the problem...

[Eric Wieser]

Does adjusting to use Nat.rec instead of Nat.rec_on help?

[Eric Wieser]

In lean3 I think rec was harder to use in this file so we used rec_on instead

[Eric Wieser]

Switching to using the equation compiler might also be fine, though in Lean3 I think it generated brec recursion which was annoying

[Damiano Testa]

I'm trying, but I'm failing to write the correct Nat.rec application.

[Damiano Testa]

Also, I keep thinking that it seems that we are constantly fighting with the implementation of a splitting field, whereas I suspect that a better approach would be to abstract the characterising properties of "a field in which something splits".

[Damiano Testa]

(I'm not proposing this change during the port, but in the long run I suspect that it will be beneficial)

[Ruben Van de Velde]

Like IsSplittingField in that file? :)

[Damiano Testa]

Yes, although I would use it much earlier and probably do a similar thing first for AdjoinRoot.

[Damiano Testa]

Anyway, I have not actually tried, so there may very well be traps lying around...

[Ruben Van de Velde]

I had a look but it doesn't seem like splitting (hah) SplittingField out would unblock too much. There's a use in field_theory.normal that might be avoidable (in the base case of normal.of_is_splitting_field), but seemingly more substantial uses in field_theory.is_alg_closed.algebraic_closure and field_theory.primitive_element

[Damiano Testa]

What I think is that a lot of the awkwardness about SplittingFieldAux and the issues with definitional equalities to get the instances to work may be mitigated by abstracting over what an AdjoinRoot is.

[Eric Rodriguez]

I'm still sad that unification seems far weaker in Lean4. I've made an example for congrArg, I'm gonna try to minimise this nat.rec stuff too.

[Damiano Testa]

I do not know if it is weaker: the versions of the lemmas in Lean 3 grew alongside modifications to Lean to improve these specific proofs. This happened over several years. Right now, with the port, these files are simply shoved down Lean 4's throat, with as little modification as possible.

[Damiano Testa]

Maybe a better way of saying this is that Lean 4 has not evolved around these proofs.

[Eric Rodriguez]

This nat.recOn application is very simple, the expected type is given in its fullest extent and there's no magic elaboration magic that needs to be done (except identifying splitting_field_aux 0 with K). It's not the first time people have had problems with induction in lean4, and I think it'd be good to improve it

[Mario Carneiro]

lmk when you have a MWE

[Mario Carneiro]

I have definitely observed elab_as_elim not being as powerful as lean 3 elab_as_eliminator, but I thought the main bugs were fixed

[Jeremy Tan]

Eric Rodriguez said:

I've made an example for congrArg

Can you share this example now so that we can all minimise it?

[Damiano Testa]

Sadly, this PR is blocking all files on the path to quadratic reciprocity.

[Damiano Testa]

This is especially surprising, given the incredible number of different proofs of quadratic reciprocity that Gauss famously gave...

[Patrick Massot]

You should port measure theory and integration instead then!

[Damiano Testa]

It feels like working for the competition, though...

[Eric Rodriguez]

It's an open issue on lean4 repo somewhere, I don't know what the number is but it's my only open issue there (I'm on mobile, sorry)

[Riccardo Brasca]

This one

[Kevin Buzzard]

Damiano Testa said:

This is especially surprising, given the incredible number of different proofs of quadratic reciprocity that Gauss famously gave...

I'm pretty sure that mathlib's original proof by Chris Hughes didn't use splitting fields :-) (indeed it was there well before splitting fields). But I really like Michael's refactor, it's much better to have a more conceptual proof. I'm always confused about why splitting fields are so hard in Lean.

[Thomas Browning]

Would it be simpler to define splitting fields in terms of the algebraic closure, rather than vice versa?

[Riccardo Brasca]

I think we should wait and do such a refactor in Lean4 after the port, unless it's really hard to port the actual strategy. But still, we should understand why.

[Eric Rodriguez]

There's always @Junyan Xu's approach, which is different and maybe better for lean4. I don't rmemebrr what was different about it.

[Thomas Browning]

Yes, I think after the port it is definitely worth considering using Junyan's algebraic closure, and then defining splitting field in terms of that.
Here's Junyan's algebraic closure for reference: https://gist.github.com/alreadydone/daa9760056383d31669755bbb41e2695

[Riccardo Brasca]

@Ruben Van de Velde do you agree that the problems started with AdjoinRoot and they just got worst here?

[Riccardo Brasca]

I mean, it can be easier to understand what's happening looking at AdjoinRoot rather than SplittingField

[Ruben Van de Velde]

AR was already quite terrible, yeah

[Anne Baanen]

We've been looking at AdjoinRoot together in person, and it seems some of the reason is that Polynomial.semiring K on a field K going via DivisionSemiring has to be unified with Polynomial.CommRing going via EuclideanDomain. But I don't know how to avoid that/make that faster.

[Riccardo Brasca]

I am trying to minimize the problem, and already

example [Fact (Irreducible f)] : Div.div (f.map (of f)) (X - C (root f)) = 0 := by
  sorry

takes more than 2 seconds to be stated. I will try to have a look at the trace.

[Anne Baanen]

Here f : K[X] with K a field.

[Damiano Testa]

I think that I observed something similar: when Lean goes from K to AdjoinRoot f it is always very slow... This is the issue, right?

[Damiano Testa]

In the example above, passing explicitly the implicit arguments (R := AdjoinRoot f.factor) (a := AdjoinRoot.root f.factor) makes the elaboration time go from ~35 to ~16 seconds.

[Riccardo Brasca]

In my example (the sorried one) you mean?

[Damiano Testa]

I meant this one.

[Damiano Testa]

On my computer, these are the timings:

--  ~8.5s
example [Fact (Irreducible f)] : Div.div (f.map (of f)) (X - C (root f)) = 0 := by
  sorry

--  ~2.5s
example [Fact (Irreducible f)] : Div.div (α := (AdjoinRoot f)[X]) (f.map (of f)) (X - C (root f)) = 0 := by
  sorry

[Damiano Testa]

From this, I deduce that your computer is about 4x more powerful than mine...

[Riccardo Brasca]

It's new indeed... I'm any case this looks like a reasonably small example to study

[Riccardo Brasca]

Note that it has to some work to do realize that AdjoinRoot f is still a field

[Damiano Testa]

I still think that abstracting AdjoinRoot to basically "K-algebra with a root of f" might make proofs easier and faster. I am still hoping that this refactor can be done after the port, but I am less and less optimistic about this.

[Damiano Testa]

(adding, where appropriate, assumptions that the algebra map is injective, that the image is generated by the root,...)

[Damiano Testa]

Something along these lnes:

import Mathlib.RingTheory.Adjoin.Field

open Polynomial AdjoinRoot

structure splex (K) (L) [Field K] [Field L] (f : K[X]) where
  (hom : K →+* L)
  (root : ∃ r : L,  eval₂ hom r f = 0)

variable [Field K] [Field L] (f : K[X])

noncomputable
def d [Field K] (f : K[X]) [Fact (Irreducible f)] : splex K (AdjoinRoot f) f :=
⟨of f, root f, eval₂_root f⟩

The definition is still slow, but I am hopeful that working with splex instead of d would be better.

[Eric Rodriguez]

It'll be funny if my diamond stuff has to get overwritten so fast

[Eric Rodriguez]

On the one hand I would like all lean3 code to work in lean4 but if refactoring all 'bad' code leads to a much faster mathlib4 in the future... Maybe it's the right price to pay

[Damiano Testa]

These files are already slow in mathlib3, just not as much as in Lean4. It was not pleasant to work with them even before the port. At least for me...

[Riccardo Brasca]

We cannot refactor mathlib4 without doing it in mathlib3 (mathport would produce broken code). In my opinion we should consider this as a last resort

[Kevin Buzzard]

Here's some relevant parts of the typeclass trace for Div.div (f.map (of f)) (X - C (root f)) = 0:

[Meta.isDefEq] [1.969095s] ✅ CommSemiring.toSemiring =?= DivisionSemiring.toSemiring ▼
  [] [1.968134s] ✅ CommSemiring.toSemiring =?= CommSemiring.toSemiring ▼
    [] [1.968080s] ✅ CommRing.toCommSemiring.1 =?= Semifield.toCommSemiring.1 ▼
      [] [1.968001s] ✅ Ring.toSemiring =?= Ring.toSemiring ▼
        [] [1.967957s] ✅ CommRing.toRing.1 =?= CommRing.toRing.1 ▼
          [] [1.967225s] ✅ Ring.toSemiring =?= Ring.toSemiring ▼
            [] [1.966967s] ✅ (Function.Surjective.ring Quotient.mk'' (_ : Function.Surjective Quotient.mk'')
                    (_ : Quotient.mk'' 0 = Quotient.mk'' 0) (_ : Quotient.mk'' 1 = Quotient.mk'' 1)
                    (_ : ∀ (x x_1 : K[X]), Quotient.mk'' (x + x_1) = Quotient.mk'' (x + x_1))
                    (_ : ∀ (x x_1 : K[X]), Quotient.mk'' (x * x_1) = Quotient.mk'' (x * x_1))
                    (_ : ∀ (x : K[X]), Quotient.mk'' (-x) = Quotient.mk'' (-x))
                    (_ : ∀ (x x_1 : K[X]), Quotient.mk'' (x - x_1) = Quotient.mk'' (x - x_1))
                    (_ : ∀ (x : K[X]) (x_1 : ℕ), Quotient.mk'' (x_1 • x) = Quotient.mk'' (x_1 • x))
                    (_ : ∀ (x : K[X]) (x_1 : ℤ), Quotient.mk'' (x_1 • x) = Quotient.mk'' (x_1 • x))
                    (_ : ∀ (x : K[X]) (x_1 : ℕ), Quotient.mk'' (x ^ x_1) = Quotient.mk'' (x ^ x_1))
                    (_ : ∀ (x : ℕ), Quotient.mk'' ↑x = Quotient.mk'' ↑x)
                    (_ :
                      ∀ (x : ℤ),
                        Quotient.mk'' ↑x =
                          Quotient.mk''
                            ↑x)).1 =?= (Function.Surjective.ring Quotient.mk'' (_ : Function.Surjective Quotient.mk'')
                    (_ : Quotient.mk'' 0 = Quotient.mk'' 0) (_ : Quotient.mk'' 1 = Quotient.mk'' 1)
                    (_ : ∀ (x x_1 : K[X]), Quotient.mk'' (x + x_1) = Quotient.mk'' (x + x_1))
                    (_ : ∀ (x x_1 : K[X]), Quotient.mk'' (x * x_1) = Quotient.mk'' (x * x_1))
                    (_ : ∀ (x : K[X]), Quotient.mk'' (-x) = Quotient.mk'' (-x))
                    (_ : ∀ (x x_1 : K[X]), Quotient.mk'' (x - x_1) = Quotient.mk'' (x - x_1))
                    (_ : ∀ (x : K[X]) (x_1 : ℕ), Quotient.mk'' (x_1 • x) = Quotient.mk'' (x_1 • x))
                    (_ : ∀ (x : K[X]) (x_1 : ℤ), Quotient.mk'' (x_1 • x) = Quotient.mk'' (x_1 • x))
                    (_ : ∀ (x : K[X]) (x_1 : ℕ), Quotient.mk'' (x ^ x_1) = Quotient.mk'' (x ^ x_1))
                    (_ : ∀ (x : ℕ), Quotient.mk'' ↑x = Quotient.mk'' ↑x)
                    (_ : ∀ (x : ℤ), Quotient.mk'' ↑x = Quotient.mk'' ↑x)).1 ▶

Two seconds to decide if Ring.toSemiring =?= Ring.toSemiring. The next step is a baad way to do this and it has further ramifications. One of the two seconds is spent solving this:

                    [] [1.005322s] ✅ AddCommMonoid.mk
                          (_ :
                            ∀ (a b : RingCon.Quotient (Ideal.Quotient.ringCon (Ideal.span {f}))),
                              a + b =
                                b +
                                  a) =?= AddCommMonoid.mk
                          (_ : ∀ (a b : RingCon.Quotient (Ideal.Quotient.ringCon (Ideal.span {f}))), a + b = b + a)

[Kevin Buzzard]

You might have several problems, but I suspect that one of them is this:

import Mathlib.RingTheory.Adjoin.Field

open Polynomial AdjoinRoot

variable [Field K] (f : K[X])

set_option profiler true in
variable [Fact (Irreducible f)] in
example : (DivisionSemiring.toSemiring : Semiring (AdjoinRoot f))
  = (@CommSemiring.toSemiring (AdjoinRoot f) CommRing.toCommSemiring : Semiring (AdjoinRoot f)) := by
  rfl
-- tactic execution of Lean.Parser.Tactic.refl took 820ms
-- `congr` takes a similar amount of time.

If f is irreducible then the adjoin-root ring will be a field, and hence a semiring via DivisionSemiring. But it's a semiring for any f (e.g. via CommSemiring). But typeclass inference isn't very good at proofs -- basically the only tactic it learnt was rfl, and rfltakes over 3/4 of a second to prove that this isn't a diamond.

[Riccardo Brasca]

Yep I agree. I am trying with (on the bus to the airport, not ideal...)

attribute [-instance] Field.toSemifield
attribute [-instance] Field.toDivisionRing

and it indeed it's faster, but still slow. Thinking about it.

[Jeremy Tan]

Kevin Buzzard said:

Two seconds to decide if Ring.toSemiring =?= Ring.toSemiring. The next step is a baad way to do this and it has further ramifications.

That's it, we're going to have to change core again (most likely)

[Damiano Testa]

By the way, on my computer it seems that adding variable {K : Type u} speeds up the computations (whether or not you have universe u before).

However, variable {K : Type _}, with no mention of an explicit/autoImplicit universe, goes back to being about the same timing as not putting the variable {K} at all.

Do you get the same behaviour?

[Riccardo Brasca]

I am pretty sure this is not the only problem, but changing the instance of Field (AdjoinRoot f) from

noncomputable instance field [Fact (Irreducible f)] : Field (AdjoinRoot f) :=
  { AdjoinRoot.instCommRing f,
    Ideal.Quotient.field
      (span {f} : Ideal K[X]) with
    ratCast := fun a => of f (a : K)
    ratCast_mk := fun a b h1 h2 => by
      letI : GroupWithZero (AdjoinRoot f) := Ideal.Quotient.groupWithZero _
      -- porting note: was
      -- `rw [Rat.cast_mk' (K := ℚ), _root_.map_mul, _root_.map_intCast, map_inv₀, map_natCast]`
      convert_to ((Rat.mk' a b h1 h2 : K) : AdjoinRoot f) = ((↑a * (↑b)⁻¹ : K) : AdjoinRoot f)
      . simp only [_root_.map_mul, map_intCast, map_inv₀, map_natCast]
      . simp only [Rat.cast_mk', _root_.map_mul, map_intCast, map_inv₀, map_natCast]
    qsmul := (· • ·)
    qsmul_eq_mul' := fun a x =>
      -- porting note: I gave the explicit motive and changed `rw` to `simp`.
      AdjoinRoot.induction_on (C := fun y => a • y = (of f) a * y) x fun p => by
        simp only [smul_mk, of, RingHom.comp_apply, ← (mk f).map_mul, Polynomial.rat_smul_eq_C_mul]
  }

to

noncomputable instance field [Fact (Irreducible f)] : Field (AdjoinRoot f) :=
  { AdjoinRoot.instCommRing f,
    Quotient.groupWithZero (span {f} : Ideal K[X]) with
    --Ideal.Quotient.field
    --  (span {f} : Ideal K[X]) with
    ratCast := fun a => of f (a : K)
    ratCast_mk := fun a b h1 h2 => by
      letI : GroupWithZero (AdjoinRoot f) := Ideal.Quotient.groupWithZero _
      -- porting note: was
      -- `rw [Rat.cast_mk' (K := ℚ), _root_.map_mul, _root_.map_intCast, map_inv₀, map_natCast]`
      convert_to ((Rat.mk' a b h1 h2 : K) : AdjoinRoot f) = ((↑a * (↑b)⁻¹ : K) : AdjoinRoot f)
      . simp only [_root_.map_mul, map_intCast, map_inv₀, map_natCast]
      . simp only [Rat.cast_mk', _root_.map_mul, map_intCast, map_inv₀, map_natCast]
    qsmul := (· • ·)
    qsmul_eq_mul' := fun a x =>
      -- porting note: I gave the explicit motive and changed `rw` to `simp`.
      AdjoinRoot.induction_on (C := fun y => a • y = (of f) a * y) x fun p => by
        simp only [smul_mk, of, RingHom.comp_apply, ← (mk f).map_mul, Polynomial.rat_smul_eq_C_mul]
  }

makes mul_div_root_cancel quite faster: from 6.2 seconds to 0.4 seconds (and / instead of Div.div works!).

[Damiano Testa]

Do you think that the speed up is due to having fewer overlaps between the fields of the parents? Is this a general heuristic?

Maybe someone else has already observed this.

[Riccardo Brasca]

I don't know

[Riccardo Brasca]

But I've the impression it really helps, it solves Kevin's problem above

[Damiano Testa]

Just to make sure that I am following: you told lean to copy the fields of GroupWithZero, instead of the ones of Field and things are faster, right?

[Damiano Testa]

I wonder if this means that we should try to create typeclasses that are as disjoint as possible.

[Damiano Testa]

(or whether this is something that could be done semi-automatically)

[Riccardo Brasca]

Yes, I (randomly) copied the proof that the quotient by a maximal ideal is a field instead of using the theorem itself

[Riccardo Brasca]

At least the field providing the group with zero structure

[Riccardo Brasca]

I am wondering what happens if we make AdjoinRoot a notation or something similar

[Chris Hughes]

There was talk about having Group (G : Type) [Mul G] [One G] [Inv G] eventually in Lean 4. That would solve a lot of these problems I think.

[Damiano Testa]

Chris, is the issue then mostly with overlapping fields that have data? Or simply avoiding overlaps, whether or not they carry data?

[Damiano Testa]

I am saying this, since for Group you gave exactly the data fields...

[Damiano Testa]

This does not seem too wild: having typeclasses for each data field and then mix-and-match...

[Eric Wieser]

Chris Hughes said:

There was talk about having Group (G : Type) [Mul G] [One G] [Inv G] eventually in Lean 4. That would solve a lot of these problems I think.

It's hard to know whether this will cause other problem elsewhere without doing it, and that's a herculean effort...

[Damiano Testa]

There is something that looks a little funny when you #print the two instances, the one going via field (AdjoinRoot.field) and the one going via GroupWithZero (AdjoinRoot.pield):

def AdjoinRoot.field.{w} : {K : Type w} →
  [inst : Field K] → {f : K[X]} → [inst_1 : Fact (Irreducible f)] → Field (AdjoinRoot f) :=
fun {K} [Field K] {f} [Fact (Irreducible f)] ↦
  let src := instCommRing f;              -- <--- both called `src`
  let src := Quotient.field (span {f});   -- <--- both called `src`
  Field.mk Field.zpow (_ : ∀ (a : K[X] ⧸ span {f}), a ≠ 0 → a * a⁻¹ = 1) (_ : 0⁻¹ = 0) fun x x_1 ↦ x • x_1

def AdjoinRoot.pield.{w} : {K : Type w} →
  [inst : Field K] → {f : K[X]} → [inst_1 : Fact (Irreducible f)] → Field (AdjoinRoot f) :=
fun {K} [Field K] {f} [Fact (Irreducible f)] ↦
  let src := instCommRing f;                       -- <--- one called src
  let src_1 := Quotient.groupWithZero (span {f});  -- <--- the other called src_1
  Field.mk GroupWithZero.zpow (_ : ∀ (a : K[X] ⧸ span {f}), a ≠ 0 → a * a⁻¹ = 1) (_ : 0⁻¹ = 0) fun x x_1 ↦ x • x_1

[Mario Carneiro]

there shouldn't be any lets in instances in the first place, you should be using letI

[Damiano Testa]

I haven't, this is the whole parent, fields setup.

[Damiano Testa]

The instances are the ones above

[Damiano Testa]

Oh, I see a letI!!!

[Damiano Testa]

The instances above now look so contrived: you get the ratCast fields by getting the GroupWithZero instance.

[Damiano Testa]

EricMario, I think that you have spotted something very interesting, but I suspect that the let shown in the print are not the letI, right?

[Riccardo Brasca]

Using my second approach what happens if we remove the letI? (I'm on mobile)

[Damiano Testa]

It works...

[Riccardo Brasca]

Asking since I give it by hand

[Riccardo Brasca]

In any case I think we should understand why the rest of the file is still slow. This is one issue for sure, but not the only one

[Damiano Testa]

Ok, I'll replace the current instance with your version, Riccardo and remove the letI.

[Damiano Testa]

Ah, this is a change to an already ported file: should I open a new PR or should I add the change to the SplittingField PR?

[Damiano Testa]

@Mario Carneiro, first, sorry that I mistook you for Eric!

Second, I think that the lets are introduced by the

instance : ... := { parent, field }

syntax, right? I find this syntax very hard to use, so I may have some completely wrong ideas...

[Riccardo Brasca]

Mmm, rather than opening a PR maybe it's better to try to fix the rest of the problem

[Eric Wieser]

Mario Carneiro said:

there shouldn't be any lets in instances in the first place, you should be using letI

Doesnt { (some foo expr) with bar := .. } generate a let?

[Riccardo Brasca]

In any case @Eric Rodriguez should check that we are not reintroducing the diamond

[Damiano Testa]

Eric, that is what I also think...

[Damiano Testa]

Riccardo, I am going to try to make this change on a new branch of mathlib3 and see if it breaks anything.

[Mario Carneiro]

Eric Wieser said:

Mario Carneiro said:

there shouldn't be any lets in instances in the first place, you should be using letI

Doesnt { (some foo expr) with bar := .. } generate a let?

Perhaps it does. Lean generates a lot of lets for this kind of thing, letI isn't in core

[Eric Wieser]

Does the __ := some foo expr syntax generate letI?

[Eric Wieser]

Damiano Testa said:

Riccardo, I am going to try to make this change on a new branch of mathlib3 and see if it breaks anything.

Just to check, you're not describing a let/letI change, right? The meanings are different in lean 3...

[Damiano Testa]

No, the observation is that in the Lean4 proof, the letI inside the ratCast_mk field is superfluous. Moreover, you can get away with only copying the fields of GroupWithZero, instead of all the ones from Field. I am implementing changes analogous to these in Lean3, if I can, to see if something breaks there.

[Damiano Testa]

I guess that the worry is that these changes in Lean4 might break something down the line that is not yet ported, so this is some form of test that maybe they won't.

[Riccardo Brasca]

Sure, testing that this doesn't break mathlib3 is necessary. But there must be something more fundamental that is wrong about AdjoinRoot, there are other slow declarations, slower than in mathlib3 I think

[Eric Rodriguez]

There is some examples in the file that guarantee the diamond won't break

[Eric Rodriguez]

So as long as those aren't removed

[Damiano Testa]

I have not removed the letI from mathlib3, but going via group_with_zero does not break the splitting_field file.

[Damiano Testa]

(I found 6 examples there, there are comments about the diamond about them and they still work.

[Damiano Testa]

CI confirms that in Lean3, using the fields of group_with_zero does not break proofs further down the line

[Eric Wieser]

Fwiw, the closest thing to Lean4 letI in mathlib3 is tactic-mode haveI

[Eric Wieser]

Damiano Testa said:

CI confirms that in Lean3, using the fields of group_with_zero does not break proofs further down the line

The relevant diff is here

[Riccardo Brasca]

I am analyzing the trace of

def modByMonicHom (hg : g.Monic) : AdjoinRoot g →ₗ[R] R[X] :=
  (Submodule.liftQ _ (Polynomial.modByMonicHom g)
        fun f (hf : f ∈ (Ideal.span {g}).restrictScalars R) =>
        (mem_ker_mod_by_monic hg).mpr (Ideal.mem_span_singleton.mp hf)).comp <|
    (Submodule.Quotient.restrictScalarsEquiv R (Ideal.span {g} : Ideal R[X])).symm.toLinearMap

that takes almost 2 seconds on my laptop. I think the relevant part is

[] [0.197048s] ✅ Algebra.toModule =?= Submodule.Quotient.module' (Ideal.span {g})

Where Lean compares two Module R-structure on AdjoinRoot g (here g : K[X], and K is a field): the first one is via the fact that AdjoinRoot gis a K-algebra, and the second one via Submodule.Quotient.module'. I've tried to modify the definition of Algebra K (AdjoinRoot g), but I didn't succed. On the other hand if I add by hand

instance [CommSemiring S] [Algebra S R] : Module S (AdjoinRoot g) :=
  Submodule.Quotient.module' (span {g} : Ideal R[X])

the declaration is 25% faster... but I have to stop now.

[Damiano Testa]

Thanks Riccardo!

[Damiano Testa]

In the meantime, removing the letI from the mathlib3 proof of rat_cast_mk is giving me a hard time!

[Riccardo Brasca]

Is it something we really want?

[Damiano Testa]

Maybe not, I simply thought that it would be straightforward, but it is actually a mess of coercions.

[Eric Rodriguez]

Damiano Testa said:

In the meantime, removing the letI from the mathlib3 proof of rat_cast_mk is giving me a hard time!

this was a recent change to the proof, let me try dig up the old proof

[Eric Rodriguez]

https://github.com/leanprover-community/mathlib/pull/18857/commits/726384b71f83edc50b7dc1f0d1a23458ed43dc53

[Eric Rodriguez]

this is a relevant commit

[Damiano Testa]

Thanks Eric!

[Damiano Testa]

I guess that this might be one of these situations where the new way of dealing with coercions pays off: in the mathlib4 version, there is no longer the need to use group_with_zero, it "just works".

[Scott Morrison]

Does defining the Field instances in stages help?

[Scott Morrison]

e.g. define the AddCommMonoid (SplittingFieldAux n f) first.

[Riccardo Brasca]

@Damiano Testa Have you opened a mathlib3 PR? If it really works and makes things faster I don't see any reason to wait (especially now that in mathlib4 is almost a leaf file)

[Riccardo Brasca]

I am talking about adjoin_root

[Damiano Testa]

I did not open the PR, but the mathlib3 branch passed CI. I do not know whether it really helps with the SplittingField issue, but I imagine that it cannot make matters worse...

[Damiano Testa]

What is the procedure, make a simultaneous PR in mathlib3 and mathlib4 with the "same" changes?

[Damiano Testa]

This is the branch

[Damiano Testa]

However, the supermarket closes in 20 mins and I do not have food for today! I'll be back soon!

[Riccardo Brasca]

It doesn't solve the problem, but it helps: for example it makes docs4#AdjoinRoot.mul_div_root_cancel much faster (and / instead of Div.div) works. As I sais above I AdjoinRoot has surely other problems, we should fix them before working on SplittingField.

[Riccardo Brasca]

Damiano Testa said:

However, the supermarket closes in 20 mins and I do not have food for today! I'll be back soon!

Eating is still more important than fixing mathlib :D

[Damiano Testa]

Well, it turns out that the supermarket closed 30 mins before I thought it did: might as well fix mathlib! :upside_down:

[Damiano Testa]

Is there a place where I can find out how to make the two PR, in congruent mathlib3 and mathlib4?

[Damiano Testa]

Found it

[Damiano Testa]

#19119 this is the mathlib3 PR switching ..field to ..group_with_zero.

[Damiano Testa]

Eric, thanks for approving the PR!

[Damiano Testa]

Now, I could wait for the mathport output, but in this case, the code that we are going to use is the one above anyway: should I still wait for mathport, or can I go ahead and produce the mathlib4 PR?

[Riccardo Brasca]

You need anyway to wait for the mathlib3 PR to be merged (otherwise the SHA will not be the good one).

[Damiano Testa]

@Eric Wieser did you mean to bors r+ or bors d+? The PR passed CI and I have nothing else to add, so a bors d+ is equivalent to a bors r+, as far as I am concerned!

[Eric Wieser]

Oops!

[Damiano Testa]

The change in syntax from bors3 to bors4 can be confusing... :stuck_out_tongue_closed_eyes:

[Damiano Testa]

The change is now in mathlib3! How do I find out when mathport picks it up?

[Eric Wieser]

You don't need to wait for mathport here

[Damiano Testa]

Ok, so I simply make a normal PR to mathlib4, mirroring the mathlib3 one, right?

[Damiano Testa]

I went ahead and made the PR: !4#4456. Should the commit hash of the corresponding mathlib3 version be updated? Manually by me? With some tool?

[Eric Wieser]

Yes, please manually update the commit hash

[Eric Wieser]

CI will tell you if the hash you pasted doesn't exist

[Damiano Testa]

Done.

I also noticed that I had not removed a LibrarySearch import, so I removed this as well. The whole PR consists of

• the change to the commit hash
• the removal of the LibrarySearch import
• using groupWithZero instead of field.

[Eric Wieser]

That second item should be in the PR description!

[Scott Morrison]

@Riccardo Brasca, have you tried breaking the giant : Field declaration into smaller pieces? We have certainly had to do this elsewhere in the library, and we know there is a blow-up as proofs of earlier fields are copied into later fields when you define everything at once.

I wouldn't be worrying about timeouts until after having made this change.

[Damiano Testa]

Eric Wieser said:

That second item should be in the PR description!

Done!

[Riccardo Brasca]

Scott Morrison said:

Riccardo Brasca, have you tried breaking the giant : Field declaration into smaller pieces? We have certainly had to do this elsewhere in the library, and we know there is a blow-up as proofs of earlier fields are copied into later fields when you define everything at once.

I wouldn't be worrying about timeouts until after having made this change.

Not really, but quite a lot of timeouts happen in declarations without Irreducible f, so there is definitely something else going on. The next step in my opinion is to make docs4#AdjoinRoot.mul_div_root_cancel faster. I will not have time for a couple of days unfortunately (too much grading :unamused: )

[Chris Hughes]

Thomas Browning said:

Yes, I think after the port it is definitely worth considering using Junyan's algebraic closure, and then defining splitting field in terms of that.
Here's Junyan's algebraic closure for reference: https://gist.github.com/alreadydone/daa9760056383d31669755bbb41e2695

Is it sensible to do this before the port given the amount of effort splitting fields take? We can use Junyan's algebraic closure, or even prove span_eval_ne_top in the current algebraic_closure file withouut using splitting fields, which looks like it must be possible. For fun, I proved a category theoretic zorn's lemma which could also be used to define algebraic closure. Maybe the splitting hell is providing motivation to improve things like adjoin_root so it's worth the effort.

[Eric Wieser]

It's not clear to me whether Junyan's approach inherits scalar action structures in a useful way; it's not clear to me that actions on K transfer to the extension of K as they do with splitting_field

[Chris Hughes]

Is there a type-class diamond that has to commute here?

[Chris Hughes]

I guess the usual Z-algebra diamond is an example. It is very yucky that we have to think about this for algebraic closures and splitting fields.

[Eric Wieser]

I think the Z and N instances are ok because Junyan's construction carries around the field structure

[Chris Hughes]

I doubt it. The field structure in the end in Junyan's construction just comes from the axiom of choice. Using zorn's lemma you show there is a maximal alg_extension and this is the algebraic closure, but it's not defined to be anything really.

[Chris Hughes]

You can get the instances to commute on alg_closure by using the current definition adjoin_monic as the definition of algebraic_closure. This field is algebraically closed, but the definition is currently more complicated than that because it's a little bit tricky to prove adjoin_monic is alg closed so Kenny kept on adjoining more roots of polynomials. Then splitting field would work as a subset of this.

[Eric Rodriguez]

the Q-diamond is the most important in practice regardless

[Damiano Testa]

One thing that I find (mathematically) disturbing is that the ℚ-diamond is there for every field, not just fields of characteristic zero.

I understand how it is implemented, but it always gives me an uncomfortable feeling.

[Eric Wieser]

It's not a diamond in other fields

[Damiano Testa]

I meant that there is a map of ℚ to every field, regardless of whether it creates diamonds or not.

[Eric Rodriguez]

it's interesting that our choices about junk values allow us to do it in a semi-consistent way that allows docs#distrib_smul

[Damiano Testa]

Yes, I think that this is one of those situations in which I trust that the conventions work out, mostly because it is formally verified.

[Damiano Testa]

In informal maths, I would never put myself in a situation where I have to rely on these "coincidences".

[Damiano Testa]

In fact, anything that depends on writing a rational number as a ratio of relatively prime integers, makes me already nervous.

[Kevin Buzzard]

The entire porting meeting today was devoted to a discussion of this issue. Perhaps @Eric Wieser or @Mario Carneiro could summarise it?

[Eric Wieser]

The summary was that

noncomputable instance field [Fact (Irreducible f)] : Field (AdjoinRoot f) :=
  { AdjoinRoot.instCommRing f,
    Ideal.Quotient.field (span {f} : Ideal K[X]) with
    /- etc -/ }

generates a term that ignores AdjoinRoot.instCommRing f entirely,

noncomputable instance field [Fact (Irreducible f)] : Field (AdjoinRoot f) :=
  { AdjoinRoot.instCommRing f,
    Quotient.group_with_zero(span {f} : Ideal K[X]) with
    /- etc -/ }

generates a bad version that eta-expands AdjoinRoot.instCommRing

noncomputable instance field [Fact (Irreducible f)] : Field (AdjoinRoot f) :=
  { Ideal.Quotient.field (span {f} : Ideal K[X]) with
    toCommRing := AdjoinRoot.instCommRing f,
    /- etc -/ }

generates a much smaller one that actually just uses the existing commRing structure

[Eric Wieser]

I consider eta-expanding bad here because the original claim for why we wanted new style structures in the first place is that you can efficiently build structures from their parents; but it seems the with clause is choosing an inefficient arrangement that is probably no better than the one flat structures gave us; but with extra indirection

[Riccardo Brasca]

Kevin Buzzard said:

The entire porting meeting today was devoted to a discussion of this issue. Perhaps Eric Wieser or Mario Carneiro could summarise it?

I am sorry to have missed that! Is next meeting on next Monday ?

[Kevin Buzzard]

Note that with the last version both the Div.div problem and the earlier splex example much quicker.

[Kevin Buzzard]

Damiano Testa said:

There is something that looks a little funny when you #print the two instances, the one going via field (AdjoinRoot.field) and the one going via GroupWithZero (AdjoinRoot.pield):

def AdjoinRoot.field.{w} : {K : Type w} →
  [inst : Field K] → {f : K[X]} → [inst_1 : Fact (Irreducible f)] → Field (AdjoinRoot f) :=
fun {K} [Field K] {f} [Fact (Irreducible f)] ↦
  let src := instCommRing f;              -- <--- both called `src`
  let src := Quotient.field (span {f});   -- <--- both called `src`
  Field.mk Field.zpow (_ : ∀ (a : K[X] ⧸ span {f}), a ≠ 0 → a * a⁻¹ = 1) (_ : 0⁻¹ = 0) fun x x_1 ↦ x • x_1

def AdjoinRoot.pield.{w} : {K : Type w} →
  [inst : Field K] → {f : K[X]} → [inst_1 : Fact (Irreducible f)] → Field (AdjoinRoot f) :=
fun {K} [Field K] {f} [Fact (Irreducible f)] ↦
  let src := instCommRing f;                       -- <--- one called src
  let src_1 := Quotient.groupWithZero (span {f});  -- <--- the other called src_1
  Field.mk GroupWithZero.zpow (_ : ∀ (a : K[X] ⧸ span {f}), a ≠ 0 → a * a⁻¹ = 1) (_ : 0⁻¹ = 0) fun x x_1 ↦ x • x_1

This was diagnosed as: "rather surprisingly, if you write it this way in the first example theninstCommRing f isn't used in the actual definition at all, and so Lean is happy to just ignore its name and call the second one src too"

[Damiano Testa]

Oh, I wish I had taken part to the meeting!

I am going to bed now, but this looks all very interesting!

[Damiano Testa]

I will also take me some time to get up to speed with new/flat style.

[Damiano Testa]

Anyway, thank you very much for looking into this and for the report! I may have more questions tomorrow.

[Damiano Testa]

So, is it fair to summarize that, when building instances on top of others, you should only have at most one and then all the remaining ones go inside the with?

[Damiano Testa]

I'm sure that there will be exceptions, but is this a good rule of thumb?

[Eric Wieser]

I think more accurate summary would be "if you can use a toFoo instead of the with, do"

[Eric Wieser]

It's very rare to be in a situation where there is more that one non-trivial to field; only the bottom of the hierarchy has this luxury. But in those cases, it's probably best to provide each of them

[Damiano Testa]

Also, is the order in which you provide the fields/instance of any relevance, for considerations of time outs?

[Damiano Testa]

I tried simple-mindedly using

noncomputable instance field [Fact (Irreducible f)] : Field (AdjoinRoot f) :=
  { Ideal.Quotient.field (span {f} : Ideal K[X]) with
    toCommRing := AdjoinRoot.instCommRing f,
    /- etc -/ }

in AdjoinRoot, but SplittingField still times out. I need to investigate this further.

[Notification Bot]

Riccardo Brasca has marked this topic as resolved.

[Notification Bot]

Riccardo Brasca has marked this topic as unresolved.

[Riccardo Brasca]

Sorry for the noise, I just wanted to change the title (there is a new PR)

[Riccardo Brasca]

tagging @Eric Rodriguez since there is a new proposed approach to SplittingField

[Eric Wieser]

Should we be making these refactors in mathlib3 first?

[Riccardo Brasca]

I agree, we don't want to discover that this creates problems somewhere else...

[Eric Wieser]

From the description alone, I think the design is a good one

[Chris Hughes]

I've mostly done this PR. The only things left are proving that something isomorphic to a field is a field and proving surjectivity of some map

[Scott Morrison]

I did most of the field construction, but seem to be missing something at qsmul_eq_mul'.

[Riccardo Brasca]

I have time to take care of it now, but I still wonder if we want this in mathlib3 before having it in mathlib4

[Eric Rodriguez]

I'll have a look and try to backport :). Will justify me being late on the blogpost!

[Riccardo Brasca]

All the tests to check the diamond is solved are in that file, right?

[Eric Rodriguez]

Yes!

[Chris Hughes]

Riccardo Brasca said:

I have time to take care of it now, but I still wonder if we want this in mathlib3 before having it in mathlib4

I kind of doubt it's worth the effort and we should just risk it. I can't see how it would make anything worse.

[Eric Wieser]

Refactoring mathlib4 before the port is done creates work for porting downstream projects, because then there is no mathlib4 version corresponding to the mathlib 3 version

[Mauricio Collares]

Backporting can be done in parallel (without blocking the mathlib4 PR), though

[Eric Wieser]

Sure; though we have tools to help with forward-porting, but not with backporting

[Mauricio Collares]

That is fair, and the tools are great! This file is a bit of a special case, though, since it is at the very top of all.pdf and the port is close enough to being complete.

[Eric Rodriguez]

I don't think there is that much of a risk, if I'm honest. As long as the API is identical, I don't think anyone outside of splitting_field.lean would be insane enough to try use any weird defeqs to do with it (and the ones we do we are careful to assert as examples in the file, and are just the algebra stuffs). On the other hand, I do agree that it's probably good practice to backport, because I would be very sad if flt_regular ends up being very hard to port because of this - we are lucky that unlike lean-liquid, we have managed to keep it pegged to mathlib3 pretty closely.

[Riccardo Brasca]

I agree the risk is very low, but this would creates a precedent, so we should probably think carefully about it. In any case the backport seems doable in a couple of hours, doesn't it?

[Riccardo Brasca]

I mean, if it creates problems in other files (in mathlib3) then it is going to creates problems with the port

[Riccardo Brasca]

#19178 for the backport (currently only waiting for cache)

[Riccardo Brasca]

Wait to celebrate, I essentially only opened the PR :)

[Kevin Buzzard]

So this doesn't touch AdjoinRoot?

I spent a lot of time last week just staring at traces in AdjoinRoot stuff, and completely failing to figure out how to make things faster.

[Chris Hughes]

It doesn't touch AdjoinRoot

[Chris Hughes]

That problem still needs to be fixed

[Riccardo Brasca]

I have to teach now, if someone wants to write

def splitting_field_aux_aux (n : ℕ) : Π {K : Type u} [field K], by exactI Π (f : K[X]),
  Σ (L : Type u) (inst : field L), by exactI algebra K L :=
nat.rec_on n (λ K inst f, ⟨K, inst, infer_instance⟩) (λ m ih K inst f,
begin
  rcases ih (@remove_factor K inst f) with ⟨L, fL, alg⟩,
  exactI ⟨L, fL, (ring_hom.comp (algebra_map _ _) (adjoin_root.of f.factor)).to_algebra⟩,
end)

in tactic mode please go ahead. Or at least convince Lean that

theorem succ (n : ℕ) (f : K[X]) :
  splitting_field_aux (n+1) f = splitting_field_aux n f.remove_factor := rfl

should work.

[Chris Hughes]

Is this just a case of Lean3 not having eta. So we have to get rid of the rcases and write let L := ih (@remove_factor K inst f); letI := L.2.1; letI := L.2.2; exact ⟨L.1, L.2.1, (ring_hom.comp (algebra_map _ _) (adjoin_root.of f.factor)).to_algebra⟩

[Eric Wieser]

#19179 backports the root_set change (WIP)

[Eric Wieser]

Do you mind finishing off the downstream breakages once CI is done, @Chris Hughes?

[Riccardo Brasca]

#19178 is more or less done (there is still one sorry, the same as in mathlib4). I've incorporated the modifications done in #19179.

[Riccardo Brasca]

Let's see what CI thinks

[Riccardo Brasca]

Eric Wieser said:

Do you mind finishing off the downstream breakages once CI is done, Chris Hughes?

#19179 is green. Is there anything else that should be done in this PR?

[Riccardo Brasca]

I propose to merge it quickly since it's helping the port.

[Eric Wieser]

I think it's ready to go, assuming there's consensus that it's a good change

[Riccardo Brasca]

Something is happening in #19178: there is deterministic timeout in field_theory.finite.galois_field. So maybe changing the definition of splitting_field has some consequence...

[Riccardo Brasca]

The timeout is in

def equiv_zmod_p : galois_field p 1 ≃ₐ[zmod p] (zmod p) :=
have h : (X ^ p ^ 1 : (zmod p)[X]) = X ^ (fintype.card (zmod p)),
  by rw [pow_one, zmod.card p],
have inst : is_splitting_field (zmod p) (zmod p) (X ^ p ^ 1 - X),
  by { rw h, apply_instance },
by exactI (is_splitting_field.alg_equiv (zmod p) (X ^ (p ^ 1) - X : (zmod p)[X])).symm

and it is there even if the proof is sorry. Any ideas?

instance aaa : algebra (zmod p) (galois_field p 1) := infer_instance

works without problems.

[Riccardo Brasca]

The red squiggle in under ≃ₐ but I don't know if this means anything.

[Riccardo Brasca]

Even

def equiv_zmod_p : galois_field p 1 →+ (zmod p) := sorry

gives a timeout.

[Riccardo Brasca]

Ah it seems to be something related to computability.

[Eric Wieser]

Is it possible we've somehow made things worse because lean now has to unify the quotient relation in some way?

[Riccardo Brasca]

Hmm, so adding noncomputable! allows to do the proof. I am seeing what happens in tactic mode:

noncomputable! def equiv_zmod_p : galois_field p 1 ≃ₐ[zmod p] (zmod p) :=
begin
  have h : (X ^ p ^ 1 : (zmod p)[X]) = X ^ (fintype.card (zmod p)),
    by rw [pow_one, zmod.card p],
  haveI inst : is_splitting_field (zmod p) (zmod p) (X ^ p ^ 1 - X),
    by { rw h, apply_instance },
  delta galois_field,
  let φ := is_splitting_field.alg_equiv (zmod p) (X ^ (p ^ 1) - X : (zmod p)[X]),
--No problems until the previous line, `φ` has type `zmod p ≃ₐ[zmod p] (X ^ p ^ 1 - X).splitting_field` as expected.
-- Its inverse should give what we want
let Ψ := φ.symm, --this line gives an error
-- synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
--  splitting_field.algebra' (X ^ p ^ 1 - X)
-- inferred
--  splitting_field.algebra' (X ^ p ^ 1 - X)
  --exactI (is_splitting_field.alg_equiv (zmod p) (X ^ (p ^ 1) - X : (zmod p)[X])).symm,
end

[Eric Wieser]

That looks pretty damning

[Eric Wieser]

(also, #19179 is now in master)

[Chris Hughes]

I remember that zmod p algebra diamonds were basically an unsolved problem last time I checked a couple of years ago. Has this now changed?

[Riccardo Brasca]

It seems that

local attribute [-instance] splitting_field.algebra'

helps a lot. Now we to wait again since I merged master, but I am optimistic.

[Riccardo Brasca]

The instances are

instance algebra : algebra K (splitting_field f) :=
ideal.quotient.algebra _

instance algebra' {R : Type*} [comm_semiring R] [algebra R K] : algebra R (splitting_field f) :=
ideal.quotient.algebra _

and I don't see anything wrong with them.

[Riccardo Brasca]

Oh, I completely forgot the porting meeting! Have you spoken about this issue?

[Kevin Buzzard]

We decided that thinking about splitting fields could wait!

[Riccardo Brasca]

What is the standard solution to

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  λ (a b : p.splitting_field), quotient.decidable_eq a b
inferred
  λ (a b : p.splitting_field), classical.prop_decidable (a = b)

?
It appears now in field_theory.polynomial_galois_group. I guess that removing open locale classical and using [decidable blah] everywhere will work, but there is maybe a quicker solution.

[Riccardo Brasca]

OK, I can use @ and classical.dec_eq

[Kevin Buzzard]

I think that removing open_locale classical is often a good idea especially if you're seeing errors like that!

[Eric Rodriguez]

Riccardo Brasca said:

It seems that

local attribute [-instance] splitting_field.algebra'

helps a lot. Now we to wait again since I merged master, but I am optimistic.

I really don't want to re-fix this for the sake of "port port port"

[Eric Rodriguez]

we really want to have this instance!

[Riccardo Brasca]

Yes, I agree. At the moment it is needed in only one file. I am finishing to fix all the rest, then we can decide. In any case there is still a (Prop-valued) sorry to finish in the construction of the splitting field.

[Riccardo Brasca]

There is now a new strange problem: another timeout it

@[nolint has_nonempty_instance] -- can't prove that they always exist
structure primitive_add_char (R : Type u) [comm_ring R] [fintype R] (R' : Type v) [field R'] :=
(n : ℕ+)
(char : add_char R (cyclotomic_field n R'))
(prim : is_primitive char)

(in src/number_theory/legendre_symbol/add_character.lean). The problem seems to be related to the n: if I replace it with 3 it works, and also if I do something like

@[nolint has_nonempty_instance] -- can't prove that they always exist
structure primitive_add_char (R : Type u) [comm_ring R] [fintype R] (R' : Type v) [field R']
  (n : ℕ+) :=
(char : add_char R (cyclotomic_field n R'))
(prim : is_primitive char)

:thinking:

[Riccardo Brasca]

Time to go to sleep for me, but if someone wants to think about it here is a minimized version.

import field_theory.splitting_field.construction

structure test (K : Type) [inst : field K] :=
(n : ℕ)
(x : @polynomial.splitting_field K inst (n : polynomial K))

fails with deterministic timeout. I've added a test file to the PR to play with.

[Eric Wieser]

Kevin Buzzard said:

I think that removing open_locale classical is often a good idea especially if you're seeing errors like that!

#19182

[Eric Wieser]

Annoying this probably came up during the port, so now the mathlib4 file probably contains a half-hearted attempt at the same cleanup

[Scott Morrison]

I merged that, despite any #outofsync limits, as getting this straightened out is on the critical path!

[Riccardo Brasca]

One last remark before really going to sleep: the timeout is already there without splitting_field!

import data.mv_polynomial.basic
import data.polynomial.ring_division

structure test (K : Type) [inst : field K] := -- deterministic timeout
(n : ℕ)
(x : mv_polynomial ((n : polynomial K).root_set K) K)

Am I too sleepy to miss something trivial?

[Eric Wieser]

Scott Morrison said:

I merged that, despite any #outofsync limits, as getting this straightened out is on the critical path!

CI isn't quite happy with it yet. I'm happy for someone else to take over the issues in downstream files if you want it done in the next 18 hours

[Notification Bot]

21 messages were moved from this topic to #mathlib4 > mysterious finsupp related timeout by Johan Commelin.

[Johan Commelin]

I moved a whole bunch of messages, because after minimizing the problem wasn't specific to splitting fields anymore.

[Johan Commelin]

Returning to the topic of this thread, the PR !4#4891 now passes CI. But I understand that the backport is still blocked on the timeout problem.

[Eric Wieser]

We also need to forward-port the bit of the backport that _did_ go through

[Johan Commelin]

which bit exactly?

[Eric Wieser]

I imagine we can just cherry-pick from !4#4891, and then double check the output against #port-dashboard

[Eric Wieser]

The rootSet change

[Eric Wieser]

Which was orthogonal to the redesign anyway

[Johan Commelin]

Ooh, I forward-ported that already

[Johan Commelin]

But as part of !4#4891

[Eric Wieser]

We should split it out so that it actually gets reviewed as a forward-port

[Eric Wieser]

I imagine the rest of splitting_field is going to need a few more days to settle anyway, so we may as well shrink the diff in the meantime

[Riccardo Brasca]

As a workaround I propose to modify (in mathlib3)

structure primitive_add_char (R : Type u) [comm_ring R] [fintype R] (R' : Type v) [field R']  :=
(n : ℕ+)
(char : add_char R (cyclotomic_field n R'))
(prim : is_primitive char)

into

def primitive_add_char (R : Type u) [comm_ring R] [fintype R] (R' : Type v) [field R'] :=
Σ (n : ℕ+), (Σ' (char : add_char R (cyclotomic_field n R')), is_primitive char)

noncomputable! def primitive_add_char.n {R : Type u} [comm_ring R] [fintype R] {R' : Type v}
  [field R'] : primitive_add_char R R' → ℕ+ := λ χ, χ.1

noncomputable! def primitive_add_char.char {R : Type u} [comm_ring R] [fintype R] {R' : Type v}
  [field R'] : Π (χ : primitive_add_char R R'), add_char R (cyclotomic_field χ.n R') :=
  λ χ, χ.2.1

noncomputable! def primitive_add_char.prim {R : Type u} [comm_ring R] [fintype R] {R' : Type v}
  [field R'] : Π (χ : primitive_add_char R R'), is_primitive χ.char :=
  λ χ, χ.2.2

To construct a primitive character one cannot use {n = ...} anymore, but ⟨_, _, _⟩ works fine, and χ.n, χ.char and χ.prim should be the same as before.

[Eric Wieser]

Instead of falling all the way back to sigma, can we define some simpler structure that at least has nice names?

[Riccardo Brasca]

I don't know how to do it, but I am open to any suggestion :)
Also, I don't understand why but I have to mark the three definition as noncomputable!, otherwise there is again a timeout.

[Riccardo Brasca]

#19178 should now compile.

[Anne Baanen]

Chris Hughes said:

I remember that zmod p algebra diamonds were basically an unsolved problem last time I checked a couple of years ago. Has this now changed?

It seems the wisdom is nowadays that the instance going from CharP to Algebra ZMod should be avoided because it creates data "out of nothing", and instead you should take an instance of [Algebra (ZMod p) R] if you want to get this map. Did we consider adding (in mathlib4?) an instance going the other way?

[Chris Hughes]

Anne Baanen said:

Chris Hughes said:

I remember that zmod p algebra diamonds were basically an unsolved problem last time I checked a couple of years ago. Has this now changed?

It seems the wisdom is nowadays that the instance going from CharP to Algebra ZMod should be avoided because it creates data "out of nothing", and instead you should take an instance of [Algebra (ZMod p) R] if you want to get this map. Did we consider adding (in mathlib4?) an instance going the other way?

The other way to do this is somewhat similar to the Rat smul instance. We can define smul zmod n for every ring, R as a bub x = a.val bub x and then it only has nice properties when char R divides n.

[Eric Wieser]

That definition doesn't work for n = 0

[Chris Hughes]

a.toInt or something then.

[Chris Hughes]

I do wonder if all these things making the definition of a Field really complicated is a good idea or might cause big performance problems.

[Johan Commelin]

Yeah, I'm not a big fan of including these structure maps. Already for Rat it's extremely dubious.
But I understand it solves some problems that we were having.

[Kevin Buzzard]

yeah, it's now got to the point where mathematically it already looks like we're cranks, so I no longer have any intuition about these questions. I look forward to the day where we have inbuilt maps both from zmod n and fin n to every ring :-/

[Michael Stoll]

Riccardo Brasca said:

As a workaround I propose to modify (in mathlib3)

structure primitive_add_char (R : Type u) [comm_ring R] [fintype R] (R' : Type v) [field R']
  (n : ℕ+) :=
(char : add_char R (cyclotomic_field n R'))
(prim : is_primitive char)

into

def primitive_add_char (R : Type u) [comm_ring R] [fintype R] (R' : Type v) [field R'] :=
Σ (n : ℕ+), (Σ' (char : add_char R (cyclotomic_field n R')), is_primitive char)

noncomputable! def primitive_add_char.n {R : Type u} [comm_ring R] [fintype R] {R' : Type v}
  [field R'] : primitive_add_char R R' → ℕ+ := λ χ, χ.1

noncomputable! def primitive_add_char.char {R : Type u} [comm_ring R] [fintype R] {R' : Type v}
  [field R'] : Π (χ : primitive_add_char R R'), add_char R (cyclotomic_field χ.n R') :=
  λ χ, χ.2.1

noncomputable! def primitive_add_char.prim {R : Type u} [comm_ring R] [fintype R] {R' : Type v}
  [field R'] : Π (χ : primitive_add_char R R'), is_primitive χ.char :=
  λ χ, χ.2.2

To construct a primitive character one cannot use {n = ...} anymore, but ⟨_, _, _⟩ works fine, and χ.n, χ.char and χ.prim should be the same as before.

It would be sad if we could not write definitions like this in the natural way.

Am I correct in thinking that the problem is not really the definition of primitive_add_char, but something more fundamental? (I have to admit that I did not follow the discussion in great detail...)

[Riccardo Brasca]

Yes, it's not at all related to your definition.

[Eric Rodriguez]

It's to do with a lean issue, currently in lean3 and 4, about generating some lemmata

[Eric Rodriguez]

Eric (other) is fixing this bug in lean3, I assume lean4 will get a fix soon

[Eric Wieser]

Already fixed in lean3, just needs a review (and for mathlib to survive the change)

[Scott Morrison]

@Eric Wieser, were you planning on compiling mathlib against this change to lean3 before or after we merge it?

[Scott Morrison]

Can we merge #19178 yet? It's unclear to me if there is a still a blocker there.

[Johan Commelin]

I would also like to merge it.
But there are 3 occasions where the instance splitting_field.algebra' is locally disabled...

[Johan Commelin]

I think this shouldn't be a blocker though.

[Scott Morrison]

Yes, I agree. This is still the longest path to completing the port, so I'd prefer that we enable people to start working on further steps concurrently with sorting out the fine details of the backport.

[Eric Wieser]

I would argue against merging it yet. I'd prefer to wait till @Eric Rodriguez is happy, c.f.

Eric Rodriguez said:

Riccardo Brasca said:

It seems that

local attribute [-instance] splitting_field.algebra'

helps a lot. Now we to wait again since I merged master, but I am optimistic.

I really don't want to re-fix this for the sake of "port port port"

[Eric Wieser]

This may still be the longest path to finishing the port, but IMO the graph of unported files is plenty wide enough that we shouldn't just rush through workarounds to satisfy some arbitrary metric

[Eric Wieser]

I would also like to have seen lean#812 merged before this PR

[Riccardo Brasca]

I see that at the end you merged it :D. Concerning

local attribute [-instance] splitting_field.algebra'

I have time now to try to understand why it is needed.

[Eric Wieser]

I share @Eric Rodriguez's concern that that attribute is a very bad sign

[Eric Wieser]

Scott Morrison said:

Eric Wieser, were you planning on compiling mathlib against this change to lean3 before or after we merge it?

After, unless someone can remind me how to do it before.

[Riccardo Brasca]

First good news: there are only two local attribute [-instance] splitting_field.algebra', and one of them (in number_theory.cyclotomic.basic) is useless (I probably forgot it when fixing something, sorry). I am working on the other one.

[Scott Morrison]

Eric Wieser said:

Scott Morrison said:

Eric Wieser, were you planning on compiling mathlib against this change to lean3 before or after we merge it?

After, unless someone can remind me how to do it before.

I'm compiling mathlib against it locally now.

[Riccardo Brasca]

The problem comes from docs#zmod.algebra. Indeed local attribute [-instance] zmod.algebra works too. The point is that

example : splitting_field.algebra (X : (zmod p)[X]) =
  @splitting_field.algebra' (zmod p) _ (X : (zmod p)[X]) (zmod p) _ (zmod.algebra _ p) := rfl --error

fails.

[Eric Wieser]

Did that fail before the refactor?

[Riccardo Brasca]

More fundamentally,

example : algebra.id (zmod p) =
  (zmod.algebra (zmod p) p) := rfl --error

fails

[Eric Wieser]

That one is well known

[Riccardo Brasca]

Eric Wieser said:

Did that fail before the refactor?

This works on yesterday's mathlib :(

[Riccardo Brasca]

But to be honest it doesn't seem a problem in splitting_field. I mean, the two algebra structure on zmod p are not definitionally equal, it looks like a fluke that using one or the other we get definitionally equal algebra structure on splitting_field. Should we set a priority on docs#zmod.algebra to make sure that docs#algebra.id is used whenever possible?

[Eric Wieser]

Priorities are a lousy solution to solving diamond problem, as the wrong instance can still be introduced by using lemmas where only that instance applies

[Riccardo Brasca]

This

variables (p : ℕ) [fact p.prime] (ι : Type) (I : ideal (mv_polynomial ι (zmod p)))

example : @ideal.quotient.algebra (zmod p) (mv_polynomial ι (zmod p)) _ _
  (@mv_polynomial.algebra (zmod p) (zmod p) ι _ _ (algebra.id (zmod p))) I =
  @ideal.quotient.algebra (zmod p) (mv_polynomial ι (zmod p)) _ _
  (@mv_polynomial.algebra (zmod p) (zmod p) ι _ _ (zmod.algebra (zmod p) p)) I := rfl --fails

fails and it is the reason why the same fails for splitting_field. With the old definition no mv_polynomial was involved and this was avoided.

[Riccardo Brasca]

Let me see if it also fails for polynomials in one variable.

[Riccardo Brasca]

example : @polynomial.algebra_of_algebra (zmod p) (zmod p) _ _ (algebra.id (zmod p)) =
  @polynomial.algebra_of_algebra (zmod p) (zmod p) _ _ (zmod.algebra (zmod p) p) := rfl

fails

[Riccardo Brasca]

(#19191 for the other one)

[Anne Baanen]

Riccardo Brasca said:

Indeed local attribute [-instance] zmod.algebra works too.

Does this fix this diamond issue in all 3 occasions? Since zmod.algebra is known to cause diamonds all by itself, I think the conclusion is safe to draw that demoting zmod.algebra is better than splitting_field.algebra'. I'd even argue to do this globally, turning it into a localized instance, or just an outright def.

[Ruben Van de Velde]

I regret to say FieldTheory.IsAlgClosed.AlgebraicClosure (!4#5074) is also full of timeouts

[Riccardo Brasca]

I am puzzled that this does not show up more frequently. When we build an algebraic gadget foo R, we often add the instance algebra R (foo R), and also algebra A (foo R), where R is an A-algebra. Now, for A = R = zmod p this can cause a diamond, since Lean can choose to use two (non-definitionally equal) way of getting algebra (zmod p) (zmod p). Of course this depend on the actual foo, but the problem is more fundamental.

[Riccardo Brasca]

Anne Baanen said:

Riccardo Brasca said:

Indeed local attribute [-instance] zmod.algebra works too.

Does this fix this diamond issue in all 3 occasions? Since zmod.algebra is known to cause diamonds all by itself, I think the conclusion is safe to draw that demoting zmod.algebra is better than splitting_field.algebra'. I'd even argue to do this globally, turning it into a localized instance, or just an outright def.

I've added this to #19191. Let's see what CI thinks.

[Eric Wieser]

Note that !4#5069 is already out of sync; we lose a lot of the benefit of a mathlib3 refactor if we then port the versions of downstream files that don't actually contain the changes from that refactor

[Eric Wieser]

Which is to say; I think it would be bet to refrain from porting a pile of downstream files until we actually have mathport output

[Anne Baanen]

Riccardo Brasca said:

I've added this to #19191. Let's see what CI thinks.

The build passed :tada: so a :peace_sign: from me on the new version.

[Riccardo Brasca]

I agree there is no need to rush here. I think we should first of all fix the various #outofsync and then maybe double checking that the actual FieldTheory.SplittingField.Construction (in mathlib4) is coherent with the mathport output.

[Riccardo Brasca]

We can simply take the mathport output tomorrow and using the fixes already existing, it should be very easy.

[Eric Wieser]

Are you suggesting we port things using the old mathport output then copy over the changes tomorrow, or refrain from porting until tomorrow?

[Ruben Van de Velde]

The three direct dependents are already PRd, fwiw

[Riccardo Brasca]

I am suggesting to wait, but in #19178 no direct dependents has been modified, so it shouldn't make a huge difference.

[Eric Wieser]

We should perhaps refrain from merging any of those dependents

[Eric Wieser]

Or alternative, add a #port-comments to all the files in #19178 saying "please wait till 2023-06-16T04:00:00+01:00 "

[Eric Wieser]

Riccardo Brasca said:

I think we should first of all fix the various #outofsync

!4#5070 is now green

[Eric Wieser]

As is !4#5024

[Riccardo Brasca]

I will review after lunch

[Eric Rodriguez]

do we need the definitional aspects of def equiv_zmod_p : galois_field p 1 ≃ₐ[zmod p] (zmod p) or just the fact it exists? Maybe the correct way to fix this is to make a private version (like this) and then make it polymorphic over all zmod p algebras

[Riccardo Brasca]

Is it reasonable to run mathport locally to have the new version of splitting_field.construction? I followed the instruction doing

./build/bin/mathport config.json Mathbin::field_theory.splitting_field.construction

but where is the output?

[Scott Morrison]

Outputs/src/mathbin

[Anne Baanen]

I have pulled !4#5071 off the queue because it depends on SplittingField.Construction and this thread advocated waiting.

[Riccardo Brasca]

Ah, I used download-release, so I am getting yesterday's version. Let me see how long it takes to make predata

[Scott Morrison]

@Eric Rodriguez, re: your question about whether lean#812 fixes the timeout issue. I'm running out of time tonight, but if you can point me to a mathlib3 commit I can pull that and compile.

[Anne Baanen]

Anne Baanen said:

I have pulled !4#5071 off the queue because it depends on SplittingField.Construction and this thread advocated waiting.

What precise condition is needed for !4#5071 to be ready to merge?

[Scott Morrison]

If there were some PR to mathlib3 that touched the file, that might be a reason not to merge it. But I don't think there is such a PR?

[Riccardo Brasca]

The story is the following:

• @Chris Hughes opened the first mathlib4 PR and realized that porting the file seemed very problematic.
• he then changed the definition of SplittingField, directly in the PR (so in mathlib4)
• I backported the new definition to mathlib3. This PR of myself got merged a couple of hours ago.
• The mathlib4 PR got merged just after

[Riccardo Brasca]

So the current version is not the one produced by mathport, but rather the opposite, the mathlib3 file is the manually backported version of mathlib4.

[Ruben Van de Velde]

!4#5069 is ready for review otherwise

[Riccardo Brasca]

I suggest to modify the mathlib4 using the output of mathport (and the fixes already existing of course). We cannot do it right now since mathport has not yet run again the mathlib3 version.

[Riccardo Brasca]

It seems unlike that this will cause problems in directly dependents file, but it also seemed unlike that backporting the new def would have caused problems, and it did...

[Riccardo Brasca]

I've mathport locally. Here !4#5087 is the result.

[Riccardo Brasca]

@Eric Wieser can you check the this will not confuse any script?

[Scott Morrison]

Is there any reason to wait any longer on !4#5069 and !4#5071?

[Riccardo Brasca]

let's just merge master on them when !4#5087 is merged (half an hour?)

[Riccardo Brasca]

I will do it

[Eric Wieser]

To be extra safe we could wait for the next mathport output for any downstream files

[Riccardo Brasca]

yes, it is in a couple of hours, right?

[Riccardo Brasca]

no, the new output just landed

[Riccardo Brasca]

!4#5069 are !4#5071 are both ready to go (I am just waiting for CI), both the current mathport and the version used to open the PR are built against df76f43357840485b9d04ed5dee5ab115d420e87.

[Eric Rodriguez]

Eric Rodriguez said:

do we need the definitional aspects of def equiv_zmod_p : galois_field p 1 ≃ₐ[zmod p] (zmod p) or just the fact it exists? Maybe the correct way to fix this is to make a private version (like this) and then make it polymorphic over all zmod p algebras

im just going to bump this to ask if it's a good idea

[Riccardo Brasca]

Well, mathematically there is one and only one iso, so we cannot really need anything specific about it.

[Riccardo Brasca]

But I really like @Anne Baanen 's suggestion to turn docs#zmod.algebra into a def, or a local instance. I will try tomorrow, but the diamond is really there, and it has nothing to to with splitting_field or galois_field.

[Johan Commelin]

In that case, I suggest that we go ahead and merge the open porting PRs using splitting fields that are ready to go

[Scott Morrison]

(That had already happened. Although maybe there are again more by now!)

[Johan Commelin]

Yeah my open github page showed me an old cache when I was looking at the PRs this morning.

[Riccardo Brasca]

Anne Baanen said:

Riccardo Brasca said:

Indeed local attribute [-instance] zmod.algebra works too.

Does this fix this diamond issue in all 3 occasions? Since zmod.algebra is known to cause diamonds all by itself, I think the conclusion is safe to draw that demoting zmod.algebra is better than splitting_field.algebra'. I'd even argue to do this globally, turning it into a localized instance, or just an outright def.

#19197

[Johan Commelin]

Should !4#5139 wait for this?

[Xavier Roblot]

I think it should wait. I'll add a note on the PR.

[Sebastien Gouezel]

In any case, this doesn't explain the original issue that declaring variables before a definition or inside the definition makes a difference in the chosen instance path. This feels like a weird bug.

[Eric Wieser]

Do we have a mwe for that?

[Xavier Roblot]

import Mathlib.FieldTheory.SplittingField.Construction
import Mathlib.Data.ZMod.Algebra

open Polynomial

section

def GaloisField0 (p : ℕ) [Fact p.Prime] (n : ℕ) :=
  SplittingField (X ^ p ^ n - X : (ZMod p)[X])

noncomputable instance (p : ℕ) [Fact p.Prime] (n : ℕ) : Field (GaloisField0 p n) := by
  dsimp only [GaloisField0]; infer_instance

end

section

variable (p : ℕ) [Fact p.Prime] (n : ℕ)

def GaloisField1 := SplittingField (X ^ p ^ n - X : (ZMod p)[X])

noncomputable instance (p : ℕ) [Fact p.Prime] (n : ℕ) : Field (GaloisField1 p n) := by
  dsimp only [GaloisField1]; infer_instance

end

example (p : ℕ) [Fact p.Prime] (n : ℕ) : GaloisField0 p n ≃+* GaloisField1 p n := by
  dsimp only [GaloisField0, GaloisField1]
  exact RingEquiv.refl _ -- fails

[Xavier Roblot]

I guess it could be reduced more