!4#5256 RingTheory.Trace

Stream: mathlib4

[Riccardo Brasca]

In !4#5256 the following is taking forever

set_option maxHeartbeats 1200000 in
theorem Algebra.isIntegral_trace [FiniteDimensional L F] {x : F} (hx : IsIntegral R x) :
    IsIntegral R (Algebra.trace L F x) := by

Note that already in !4#5074 the slowest declarations are related to IsIntegral or to eval. Should we try to investigate this more closely?

[Riccardo Brasca]

@Xavier Roblot I am afraid you will face the same problem in !4#5262

[Xavier Roblot]

Thanks for the warning. I am not quite there but getting close

[Riccardo Brasca]

Here is something interesting: if I use set_option maxHeartbeats 1100000 in (instead of 1200000), after the last convert the goal is

(↑(aeval y) (minpoly R x) = 0) = (↑(aeval y) (minpoly R x) = 0)

Let me see what happens with set_option pp.all true.

[Eric Wieser]

maxHeartbeats changes the behavior of convert!?

[Riccardo Brasca]

It seems so... maybe because the LHS and the RHS are defeq, but with a small maxHeartbeats Lean gives up?

[Eric Wieser]

Is it not possible to distinguish "not defeq" from "could not determine if defeq within the time limit"?

[Eric Wieser]

This strikes me as a bug

[Riccardo Brasca]

Well, of course the output is huge... 24464 lines

[Riccardo Brasca]

The goals starts at line 8754

[Riccardo Brasca]

If I replace convert by exact I get a timeout (with both limits)

[Riccardo Brasca]

Using set_option pp.explicit true the output is much shorter

⊢ @Eq Prop
    (@Eq
      ((fun x ↦ @AlgebraicClosure F inst✝⁵)
        (↑(@trace L F (@EuclideanDomain.toCommRing L (@Field.toEuclideanDomain L inst✝⁸))
              (@EuclideanDomain.toCommRing F (@Field.toEuclideanDomain F inst✝⁵)) inst✝³)
          x))
      (↑(@aeval R
            ((fun x ↦ @AlgebraicClosure F inst✝⁵)
              (↑(@trace L F (@EuclideanDomain.toCommRing L (@Field.toEuclideanDomain L inst✝⁸))
                    (@EuclideanDomain.toCommRing F (@Field.toEuclideanDomain F inst✝⁵)) inst✝³)
                x))
            (@CommRing.toCommSemiring R inst✝¹⁴)
            (@Ring.toSemiring
              ((fun x ↦ @AlgebraicClosure F inst✝⁵)
                (↑(@trace L F (@EuclideanDomain.toCommRing L (@Field.toEuclideanDomain L inst✝⁸))
                      (@EuclideanDomain.toCommRing F (@Field.toEuclideanDomain F inst✝⁵)) inst✝³)
                  x))
              (@CommRing.toRing
                ((fun x ↦ @AlgebraicClosure F inst✝⁵)
                  (↑(@trace L F (@EuclideanDomain.toCommRing L (@Field.toEuclideanDomain L inst✝⁸))
                        (@EuclideanDomain.toCommRing F (@Field.toEuclideanDomain F inst✝⁵)) inst✝³)
                    x))
                (@EuclideanDomain.toCommRing
                  ((fun x ↦ @AlgebraicClosure F inst✝⁵)
                    (↑(@trace L F (@EuclideanDomain.toCommRing L (@Field.toEuclideanDomain L inst✝⁸))
                          (@EuclideanDomain.toCommRing F (@Field.toEuclideanDomain F inst✝⁵)) inst✝³)
                      x))
                  (@Field.toEuclideanDomain
                    ((fun x ↦ @AlgebraicClosure F inst✝⁵)
                      (↑(@trace L F (@EuclideanDomain.toCommRing L (@Field.toEuclideanDomain L inst✝⁸))
                            (@EuclideanDomain.toCommRing F (@Field.toEuclideanDomain F inst✝⁵)) inst✝³)
                        x))
                    (@AlgebraicClosure.instFieldAlgebraicClosure F inst✝⁵)))))
            this✝ y)
        (@minpoly R F inst✝¹⁴ (@DivisionRing.toRing F (@Field.toDivisionRing F inst✝⁵)) inst✝² x))
      0)
    (@Eq
      ((fun x_1 ↦
          (fun x ↦ @AlgebraicClosure F inst✝⁵)
            (↑(@trace L F (@EuclideanDomain.toCommRing L (@Field.toEuclideanDomain L inst✝⁸))
                  (@EuclideanDomain.toCommRing F (@Field.toEuclideanDomain F inst✝⁵)) inst✝³)
              x))
        (@minpoly R F inst✝¹⁴ (@CommRing.toRing F (@EuclideanDomain.toCommRing F (@Field.toEuclideanDomain F inst✝⁵)))
          inst✝² x))
      (↑(@aeval R
            ((fun x ↦ @AlgebraicClosure F inst✝⁵)
              (↑(@trace L F (@EuclideanDomain.toCommRing L (@Field.toEuclideanDomain L inst✝⁸))
                    (@EuclideanDomain.toCommRing F (@Field.toEuclideanDomain F inst✝⁵)) inst✝³)
                x))
            (@CommRing.toCommSemiring R inst✝¹⁴)
            (@CommSemiring.toSemiring
              ((fun x ↦ @AlgebraicClosure F inst✝⁵)
                (↑(@trace L F (@EuclideanDomain.toCommRing L (@Field.toEuclideanDomain L inst✝⁸))
                      (@EuclideanDomain.toCommRing F (@Field.toEuclideanDomain F inst✝⁵)) inst✝³)
                  x))
              (@Semifield.toCommSemiring
                ((fun x ↦ @AlgebraicClosure F inst✝⁵)
                  (↑(@trace L F (@EuclideanDomain.toCommRing L (@Field.toEuclideanDomain L inst✝⁸))
                        (@EuclideanDomain.toCommRing F (@Field.toEuclideanDomain F inst✝⁵)) inst✝³)
                    x))
                (@Field.toSemifield
                  ((fun x ↦ @AlgebraicClosure F inst✝⁵)
                    (↑(@trace L F (@EuclideanDomain.toCommRing L (@Field.toEuclideanDomain L inst✝⁸))
                          (@EuclideanDomain.toCommRing F (@Field.toEuclideanDomain F inst✝⁵)) inst✝³)
                      x))
                  (@AlgebraicClosure.instFieldAlgebraicClosure F inst✝⁵))))
            this✝ y)
        (@minpoly R F inst✝¹⁴ (@CommRing.toRing F (@EuclideanDomain.toCommRing F (@Field.toEuclideanDomain F inst✝⁵)))
          inst✝² x))
      0)

[Riccardo Brasca]

From 1200000 to 240000!

attribute [-instance] Field.toEuclideanDomain
set_option maxHeartbeats 240000 in
theorem Algebra.isIntegral_trace [FiniteDimensional L F] {x : F} (hx : IsIntegral R x) :
    IsIntegral R (Algebra.trace L F x) := by
  have hx' : IsIntegral L x := isIntegral_of_isScalarTower hx
  have splits :(minpoly L x).Splits (algebraMap L (AlgebraicClosure F)) := by
    apply IsAlgClosed.splits_codomain
  rw [← isIntegral_algebraMap_iff
    (algebraMap L (AlgebraicClosure F)).injective, trace_eq_sum_roots splits]
  refine' (IsIntegral.multiset_sum _).nsmul _
  intro y hy
  rw [mem_roots_map (minpoly.ne_zero hx')] at hy
  use minpoly R x, minpoly.monic hx
  rw [← aeval_def]
  refine' minpoly.aeval_of_isScalarTower (K := L) R x y _
  rw [aeval_def]
  convert hy

[Riccardo Brasca]

Can docs4#Field.toEuclideanDomain be a big problem? This new proof is much better, it is almost the same as in mathlib3

[Riccardo Brasca]

I am trying to set

attribute [-instance] Field.toEuclideanDomain

also in other slow files to see what happens

[Riccardo Brasca]

Step.isIntegral in FieldTheory.IsAlgClosed.AlgebraicClosure goes from 700000 to 450000 :scream:

[Ruben Van de Velde]

I'm finding it hard to read the zeroes, is that better?

[Riccardo Brasca]

From 700 to 450

[Riccardo Brasca]

Seeing what happens if it is a def everywhere

[Riccardo Brasca]

(I mean, it's not even mathematically clear that a field is a euclidean domain...)

[Sebastien Gouezel]

Do you achieve the same improvement by just lowering its priority?

[Riccardo Brasca]

It's already 100

[Riccardo Brasca]

There is even a comment

-- Porting note: this seems very slow.
-- see Note [lower instance priority]

[Sebastien Gouezel]

You could put it at 10 to see if it makes a difference.

[Riccardo Brasca]

I will play with this after dinner. For the time being !4#5264 and #19205 to see if we use the instance somewhere.

[Sebastien Gouezel]

Using the instance

instance (priority := 100) Field.toEuclideanDomain {K : Type _} [Field K] : EuclideanDomain K :=
{ toCommRing := Field.toCommRing
  quotient := (· / ·), remainder := fun a b => a - a * b / b, quotient_zero := div_zero,
  quotient_mul_add_remainder_eq := fun a b => by
    -- Porting note: was `by_cases h : b = 0 <;> simp [h, mul_div_cancel']`
    by_cases h : b = 0 <;> dsimp only
    · dsimp only
      rw [h, zero_mul, mul_zero, zero_div, zero_add, sub_zero]
    · dsimp only
      rw [mul_div_cancel' _ h]
      simp only [ne_eq, h, not_false_iff, mul_div_cancel, sub_self, add_zero]
  r := fun a b => a = 0 ∧ b ≠ 0,
  r_wellFounded :=
    WellFounded.intro fun a =>
      (Acc.intro _) fun b ⟨hb, _⟩ => (Acc.intro _) fun c ⟨_, hnb⟩ => False.elim <| hnb hb,
  remainder_lt := fun a b hnb => by simp [hnb],
  mul_left_not_lt := fun a b hnb ⟨hab, hna⟩ => Or.casesOn (mul_eq_zero.1 hab) hna hnb }

is probably much better.

[Riccardo Brasca]

Let me try also this

[Sebastien Gouezel]

This better instance also solves the porting note:

instance (priority := 100) Field.toEuclideanDomain {K : Type _} [Field K] : EuclideanDomain K :=
{ toCommRing := Field.toCommRing
  quotient := (· / ·), remainder := fun a b => a - a * b / b, quotient_zero := div_zero,
  quotient_mul_add_remainder_eq := fun a b => by
    by_cases h : b = 0 <;> simp [h, mul_div_cancel']
  r := fun a b => a = 0 ∧ b ≠ 0,
  r_wellFounded :=
    WellFounded.intro fun a =>
      (Acc.intro _) fun b ⟨hb, _⟩ => (Acc.intro _) fun c ⟨_, hnb⟩ => False.elim <| hnb hb,
  remainder_lt := fun a b hnb => by simp [hnb],
  mul_left_not_lt := fun a b hnb ⟨hab, hna⟩ => Or.casesOn (mul_eq_zero.1 hab) hna hnb }

works just fine. With set_option pp.explicit true, the old definition takes 2100 lines in #print Field.toEuclideanDomain, the new one 90.

[Riccardo Brasca]

So, in !4#5264 I've made the instance a def and fixed the two errors. Then I had a look at the files that we ported in the last month and that were slow, reducing the heartbeats to the minimum that works. It's not miraculous, but it's definitely better.

[Riccardo Brasca]

Now I will compare what happens with the new instance.

[Riccardo Brasca]

OK, forget about !4#5264. Indeed the modification proposed in !4#5266 is as good as making the instance a def.

Tagging @Damiano Testa @Eric Wieser @Kevin Buzzard @Ruben Van de Velde @Chris Hughes @Xavier Roblot since they were involved is all these problems with SplittingField and friends.

[Riccardo Brasca]

Note that not all problems are solved, the situation is only slightly better, but maybe we only need to fix some instance.

[Damiano Testa]

Is it a good heuristic to say that we should stay away from with in instances, unless we are really sure about what we are doing?

[Kevin Buzzard]

Removing with does not completely solve the problem. I changed another instance here and it had a similar effect: things got fractionally better but the problems are still there. It's not the with per se, it's the term the with produces.

[Matthew Ballard]

I have more elementary question: what should I expect Lean to be doing when it wants a CommRing and I hand it

 ‹Field K› with
    add := (· + ·), mul := (· * ·), one := 1, zero := 0, neg := Neg.neg,

? It seems crazy over-specified and, during porting, there were other instances (ha) where stripping out things helped behavior.

[Riccardo Brasca]

Kevin Buzzard said:

Removing with does not completely solve the problem. I changed another instance here and it had a similar effect: things got fractionally better but the problems are still there. It's not the with per se, it's the term the with produces.

You also did something very similar in !4#4507 and it also helped. We have to find the other places where this is needed...

[Eric Wieser]

I would imagine we have a very large number of such places

[Eric Wieser]

For instance, all of the docs4#Function.Surjective.ring type instances will have this problem

[Yaël Dillies]

Is there any chance that we can make the with notation smarter rather than working around it?

[Eric Wieser]

I don't think that necessarily helps, sometimes we might not even be handing with an appropriate argument

[Eric Wieser]

Unless you had with! for "i know none of my base classes are really base classes, but I meant it anyway"

[Xavier Roblot]

I have just merged !4#5266 into the port of RingTheory.Norm and the improvement is phenomenal!

[Xavier Roblot]

Everything now works so nicely :smile:

[Riccardo Brasca]

docs4#lift_of_splits is still slow (why in the root namespace?!). It is something related to this message. Maybe docs4#Subalgebra.algebra' is suboptimal, but I am not sure.

[Xavier Roblot]

Well, !4#5262 is ready (but it depends on !4#5266)

[Kevin Buzzard]

            [] [13.358618s] refine' (AdjoinRoot.liftHom (minpoly (Algebra.adjoin F (↑s : Set K)) a) y hy).comp _ ▶
            [] [30.068997s] exact (AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly (Algebra.adjoin F (↑s : Set K)) a).toAlgHom ▶

was why lift_of_splits was slow in master. It will be interesting to see if there are still issues such as

                  [] [9.118708s] ✅ CommSemiring.toSemiring =?= CommSemiring.toSemiring

after !4#5266 .

[Kevin Buzzard]

The issue is that the left hand side is

@AdjoinRoot.instCommRing { x // x ∈ Algebra.adjoin F ↑s } (Subalgebra.toCommRing (Algebra.adjoin F ↑s))
  (minpoly { x // x ∈ Algebra.adjoin F ↑s } a) : CommRing (AdjoinRoot (minpoly { x // x ∈ Algebra.adjoin F ↑s } a))

and the right hand side is

@AdjoinRoot.instCommRing { x // x ∈ Algebra.adjoin F ↑s } EuclideanDomain.toCommRing
  (minpoly { x // x ∈ Algebra.adjoin F ↑s } a) : CommRing (AdjoinRoot (minpoly { x // x ∈ Algebra.adjoin F ↑s } a))

where the Euclidean domain instance is coming from letI := fieldOfFiniteDimensional F (Algebra.adjoin F (↑s : Set K)) (on master)

[Riccardo Brasca]

Now I see

[Meta.synthInstance] [7.769144s] ✅ Algebra { x // x ∈ Algebra.adjoin F ↑s } (AdjoinRoot (minpoly { x // x ∈ Algebra.adjoin F ↑s } a))

and if I click on the arrow the output is huge

[Riccardo Brasca]

It does this

[] [0.720522s] ✅ CommSemiring.toSemiring =?= Ring.toSemiring

several times. The LHS is

@CommSemiring.toSemiring { x // x ∈ Algebra.adjoin F ↑s } (Subalgebra.toCommSemiring (Algebra.adjoin F ↑s)) : Semiring { x // x ∈ Algebra.adjoin F ↑s }

and the RHS is

@Ring.toSemiring { x // x ∈ Algebra.adjoin F ↑s } (SubringClass.toRing (Algebra.adjoin F ↑s)) : Semiring { x // x ∈ Algebra.adjoin F ↑s }

[Kevin Buzzard]

It's much quicker than before though.

[Sebastien Gouezel]

Again, the current form of fieldOfFiniteDimensional is suboptimal. It should probably be changed to

lemma glouk (F : Type _) {K : Type _} [Field F] [Ring K] [IsDomain K]
    [Algebra F K] [FiniteDimensional F K] {x : K} (H : x ≠ 0) : ∃ y, x * y = 1 := by
  have : Function.Surjective (LinearMap.mulLeft F x) :=
    LinearMap.injective_iff_surjective.1 fun y z => ((mul_right_inj' H).1 : x * y = x * z → y = z)
  exact this 1

/-- A domain that is module-finite as an algebra over a field is a division ring. -/
noncomputable def divisionRingOfFiniteDimensional (F K : Type _) [Field F] [h : Ring K] [IsDomain K]
    [Algebra F K] [FiniteDimensional F K] : DivisionRing K :=
  { ‹IsDomain K› with
    toRing := h
    inv := fun x => if H : x = 0 then 0 else Classical.choose <| glouk F H
    mul_inv_cancel := fun x hx =>
      show x * dite _ _ _ = _ by
        rw [dif_neg hx]
        exact (Classical.choose_spec (glouk F hx) :)
    inv_zero := dif_pos rfl }
#align division_ring_of_finite_dimensional divisionRingOfFiniteDimensional

/-- An integral domain that is module-finite as an algebra over a field is a field. -/
noncomputable def fieldOfFiniteDimensional (F K : Type _) [Field F] [h : CommRing K] [IsDomain K]
    [Algebra F K] [FiniteDimensional F K] : Field K :=
  { divisionRingOfFiniteDimensional F K with
    toCommRing := h }
#align field_of_finite_dimensional fieldOfFiniteDimensional

What is going on is that the definition of a Field has a CommRing embedded inside it. The old definition was taking a CommRing instance but did not use it directly to build the CommRing field, instead it broke it into pieces and then reassembled the bits by hand.

Also, having an auxiliary lemma before the first definition that hides away the LinearMap.mulLeft business and the algebra structure makes sure that the definition of linear maps does not show up in the definition of the inverse and makes the corresponding term much shorter.

[Kevin Buzzard]

I tried a version of this two weeks ago but it didn't make any difference to the problem I was trying to solve, namely slowdowns (I failed to get !bench working so I just timed it locally and there was no difference). Perhaps my error was that I didn't also change the DivisionRing instance? I'll try this version now.

[Kevin Buzzard]

If I make the change above and then recompile what needs to be recompiled on master, I get

real    10m35.143s
user    85m38.248s
sys 1m56.750s

If I then revert the change and recompile again, I get

real    10m32.122s
user    85m27.783s
sys 1m58.641s

So, just as my experiment two weeks ago, it might make the terms nicer but it doesn't make mathlib compile any faster.

[Kevin Buzzard]

On the other hand it might make debugging slowdowns easier so it's probably worth making the change anyway.

[Sebastien Gouezel]

Sure, these are not instances, they are defs, so they are only relevant when they are explicitely used, which is not a lot (once for each of them).

[Kevin Buzzard]

Aah I see!

[Kevin Buzzard]

!4#5288