making `op` irreducible

Stream: mathlib4

[Matthew Ballard]

Taking the new diagnostics tool for a ride and this was the biggest offender in the file with the worst regressions with 4.8.

[Matthew Ballard]

The canonical map α → αᵒᵖ.

Sounds kinda evil

[Eric Wieser]

Just to be clear, this is docs#Opposite.op, from category theory?

[Eric Wieser]

(Should we namespace the definition in CategoryTheory?)

[Markus Himmel]

Matthew Ballard said:

Sounds kinda evil

Why is it evil? How else would you go from an object X : C to the corresponding object in the opposite category?

[Matthew Ballard]

However I did it, I wouldn't tell Lean

[Adam Topaz]

Markus Himmel said:

Why is it evil?

It's evil because an object is not an object of C but rather an object in some unspecified category equivalent to C. (sorry...)

[Joël Riou]

Anyway, it is completely unreasonable to make Opposite.op irreducible.

[Matthew Ballard]

In terms of impractical?

[Joël Riou]

Yes.

[Adam Topaz]

I'm not sure it's completely unreasonable, but if we do make it irreducible we would have to be very careful in developing the initial API.

[Matthew Ballard]

I am attempting the experiment now with the new attribute [local semireducible] and trying to quarantine those with irreducible

[Adam Topaz]

It's already a structure, right? Is the main issue with eta-reduction?

[Matthew Ballard]

Opposite is a structure. op is a def

[Adam Topaz]

docs#Opposite.op

[Adam Topaz]

Why aren't we doing:

structure Opposite := op :: unop : α

[Joël Riou]

It this does what I think it does, I would be ok with this.

[Matthew Ballard]

Joël Riou said:

It this does what I think it does, I would be ok with this.

Sorry, I cannot parse "this". Are you referring to Adam's suggestion to use the constructor directly?

[Joël Riou]

Matthew Ballard said:

Joël Riou said:

It this does what I think it does, I would be ok with this.

Sorry, I cannot parse "this". Are you referring to Adam's suggestion to use the constructor directly?

Yes!

[Matthew Ballard]

That does seem more principled

[Joël Riou]

Isn't it mostly like making op reducible?

[Matthew Ballard]

Structure eta?

[Eric Wieser]

Adam Topaz said:

Why aren't we doing:

structure Opposite := op :: unop : α

Independent of the performance discussion in this thread, we should certainly do this

[Matthew Ballard]

Let's see what happens... #12636

[Matthew Ballard]

I got caught in DTH in one proof and didn't have the energy to fight my way out

[Matthew Ballard]

I had to no_index a couple of instances because the discrimination tree was applying structure eta to get the keys making Lean miss the instance

[Matthew Ballard]

AlgebraicGeometry.GammaSpecAdjunction gets sped up by about 10% but is still incredibly slow compared to before v4.8

[Markus Himmel]

Matthew Ballard said:

Let's see what happens... #12636

An unfortunate consequence of this change is that instead of op X the pretty printer now prints { unop := X } everywhere. In lean4#4675 I'm proposing a new attribute @[pp_no_structure_instances] that we can apply to Opposite to fix this.

[Yaël Dillies]

I've offered a different solution which would solve other problems along the way, namely to decouple the default constructor from the \<> notation and instead couple it to mk.

[Markus Himmel]

Ah, thanks for reminding me about that discussion (for reference: this one). That seems like a much larger change to me, and from the discussion so far it also seems not clear whether the issue I'm referring to would be affected by your suggested change at all, since it's about the delaborator producing { field := value } notation rather than \<> notation. So it seems to me that there is value in getting this tiny change to the delaborator merged while your suggestion makes its way through the RFC process.