Issue with irreducible, report

Stream: lean4

[Julien Marquet]

Hello,

I encountered an issue with @[irreducible] where isDefEq tries to unfold an irreducible definition. I don't really know how to write a MWE for this, so I don't hope for any solution, but maybe someone will know what triggers the issue and will be interested.
I tried to get quickly to the point in this message but I know I should really just try to reduce this to a MWE. Unfortunately I can't do that now. I eventually managed to work around this, but maybe this report will be interesting to someone.

Here are the relevant lines in my project, I explain what they mean in the rest of the message.

I defined the tensor product of vector spaces, and I want this equips the category Vect with a monoidal structure. My definition of tensor products involves quotients, which give very long definitions. I marked these definitions irreducible. I also defined some categorical notions, in particular products and functors, and I want to define monoidal structures in terms of functors C ×c C ⟶ C (with the notations I use in my code).
The issue happens when I want to define the associator, which in readable terms gives maps (A ⊗ B) ⊗ C ⟶ A ⊗ (B ⊗ C), but in my framework is typed (full definition here)

((tensor_bifunctor K ×c Category.identity (KVect K)) ≫ tensor_bifunctor K) ⟶
    (Category.Product.assoc _ _ _
      ≫ (Category.identity (KVect K) ×c tensor_bifunctor K)
      ≫ tensor_bifunctor K)

(a natural transformation between the right functors, which is very convoluted, sorry, I wish I knew how to reduce this to a simpler example).
What happens is that I want to define the data of a natural transformation, which is, since I work in Vect, for each object a map

LinearMap (tensor_space (tensor_space U V) W) (tensor_space U (tensor_space V W))

and a function that takes ((U, V), W) ((U', V'), W') ((f, g), h) (two triples of spaces and a triple of maps between them) and gives a proof that the previous maps are natural. This holds by definition, and I was able to make Lean understand that.

I encountered a first issue when defining the maps of my natural transformation: isDefEq would reach the maximum number of heartbeats.
What happened was that the type of the maps involved a tensor_space which is a cokernel, which in turn reduces to a quotient. By making cokernel irreducible I managed to work around the issue.
Now, I want to prove naturality. I start by with intro ((U, V), W) ((U', V'), W') ((f, g), h), which is type correct, but makes isDefEq consume too much resource. What happens is that, even though cokernel is irreducible, isDefEq tries to unfold it (which I found out using set_option trace.Meta.isDefEq true.
This behavior is very surprising to me, as Lean doesn't do this on the line above.

I managed to work around this issue by using opaque :

opaque opaque_id_wrapper {α : Type u} : { f : α → α // f = id } := ⟨ id, rfl ⟩
def opaque_id {α : Type u} : α → α := opaque_id_wrapper.1
theorem opaque_id_eq {α : Type u} : @opaque_id α = id := opaque_id_wrapper.2

If I hide all my definitions behind opaque_id, it works, as isDefEq won't be able to unfold this. Better: with this trick, I can know my definitions are, indeed, type correct and coherent by definitional equality.

[Julien Marquet]

I don't have a specific question although I'd appreciate any comment :) especially on whether this is a known or new issue. Also, maybe I'm just doing things wrong :sweat_smile: please tell me if so :)

[Jeremy Salwen]

Is this section relevant? https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/master/md/main/metam.md#transparency

basically something is using TransparencyMode all?

[Sebastian Ullrich]

This sounds like https://github.com/leanprover/lean4/pull/2162, but it looks like your Lean version is recent enough to contain the fix

[Sebastian Ullrich]

Well, I suppose the match discriminant is trivial anyway in the case of pattern intro

[Julien Marquet]

Jeremy Salwen said:

Is this section relevant? https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/master/md/main/metam.md#transparency

Yes, I also tried to look at the source of Lean, and I went searching here on Zulip, that's how I found about opaque (and constant which seems to be deprecated?)
It seems to me like I'm not the only one who's getting confused with @[irreducible], I found some topics about it (that's where I learned more about how reducibility hints work in Lean 4).

Jeremy Salwen said:

basically something is using TransparencyMode all?

Yes, I guess that's what happens... it's surprising though. I guess there is a difference between the checks that are performed by exact and those that are performed by intro, but I don't know the detail.

[Mario Carneiro]

constant is now spelled axiom

[Mario Carneiro]

although opaque sometimes works in its place (and should be preferred if applicable)

[Mario Carneiro]

by the way, your trick with opaque_id is codified in mathlib as the irreducible_def command

[Julien Marquet]

Sebastian Ullrich said:

This sounds like https://github.com/leanprover/lean4/pull/2162, but it looks like your Lean version is recent enough to contain the fix

My issue looks similar to this, maybe I stumbled on a piece of code that contains a similar misbehavior?

[Mario Carneiro]

can you make a MWE version of the example?

[Julien Marquet]

Mario Carneiro said:

by the way, your trick with opaque_id is codified in mathlib as the irreducible_def command

Yes, I just copied this from a discussion here about this particular command :sweat_smile:
(This still gives rise to issues though, because now I have some rewriting to do, but that's another subject.)

[Julien Marquet]

Mario Carneiro said:

can you make a MWE version of the example?

I'd love to, I'll try later :)