RingCon extends

Stream: mathlib4

[Matthew Ballard]

While poking around slow instances, I found a note about making docs#RingCon extend docs#AddCon and docs#Con instead of extending Add and Mul with some fields.

Performance-wise, it doesn't make much difference. Is there an argument against this change?

[Eric Wieser]

Was docs3#con a new-style structure?

[Eric Wieser]

Yes, it was. The port was catching up in Lean3 and I didn't want to have to go back and make setoid an old-style structure

[Matthew Ballard]

So you are saying you have none now?

[Matthew Ballard]

There is #6722 which I can clean up unless people object

[Eric Wieser]

The only counterargument I have is a general distaste for nested inheritance and the asymmetry it forces

[Eric Wieser]

Wrong issue number?

[Damiano Testa]

I do not know if this helps, but I always had in the back of my mind this relationship between Con and Covariants:

import Mathlib.GroupTheory.Congruence

open Function Setoid
variable (M : Type*) [Setoid M] [Mul M]

@[to_additive]
theorem Con.of_covariants [CovariantClass M M (· * ·) r] [CovariantClass M M (swap (· * ·)) r] :
    Con M where
  mul' {w x y z} wx yz :=
    have left  : r (w * y) (x * y) := CovariantClass.elim (μ := swap (· * ·)) y wx
    have right : r (x * y) (x * z) := CovariantClass.elim (μ := (· * ·)) x yz
    Setoid.iseqv.trans left right

I do not know if this is useful to break some proofs up...

[Damiano Testa]

Matthew Ballard said:

There is #6722 which I can clean up unless people object

#6772?

[Matthew Ballard]

Apologies! Semester is starting :brain: :cooking:

[Matthew Ballard]

Eric suggested switching the parent order and now mathlib natively compiles 13% faster (somewhat skeptical).

Marked as awaiting-review

[Sebastian Ullrich]

If you click on the metric to get to its graph, you can see that it has quite a bit of variance, especially now that Mario has significantly decreased its total time http://speed.lean-fro.org/mathlib4/repo-detail/e7b27246-a3e6-496a-b552-ff4b45c7236e?zoomXStart=1692568800000&zoomXEnd=1693346400000&dimensions=build%3Anative%20compilation&dayEquidistant=true

[Sebastian Ullrich]

We don't have a good means of taking that variance into account when reporting yet but I can exclude the metric from significance reporting manually if desired

[Matthew Ballard]

I don’t think it needs to be excluded. That drop is crazy though.

[Eric Wieser]

Eric Wieser said:

The only counterargument I have is a general distaste for nested inheritance and the asymmetry it forces

I'm exploring restoring this symmetry in #6791

[Matthew Ballard]

I can also believe the drop here though since I can imagine compilation of algebraic quotient types is more intense but I don’t really know.