unexpanders for functors

Stream: mathlib4

[Adam Topaz]

I'm experimenting with some unexpanders for functors in the category theory library. I can't seem to figure out how to get this to work for docs4#CategoryTheory.Functor specifically the obj and map fields which pass via toPrefunctor.
Here is what I got to work with prefunctors:

import Mathlib

variable (C D : Type _) [Quiver C] [Quiver D] (F : C ⥤q D)

/- -- uncomment this for nice pretty printing in the examples below.

@[app_unexpander Prefunctor.obj] def
  unexpandPrefunctorObj : Lean.PrettyPrinter.Unexpander
  | `($_ $F $X)  => `($(F).obj $X)
  | _           => throw ()

@[app_unexpander Prefunctor.map] def
  unexpandPrefunctorMap : Lean.PrettyPrinter.Unexpander
  | `($_ $F $X)  => `($(F).map $X)
  | _           => throw ()
-/

example (X Y : C) (h : X = Y) : F.obj X = F.obj Y := by
  rw [h]

example (X Y : C) (f g : X ⟶ Y) (h : f = g) : F.map f = F.map g := by
  rw [h]

How would I accomplish this for functors? I tried this:

@[app_unexpander CategoryTheory.Functor.toPrefunctor.obj] def
  unexpandFunctorObj : Lean.PrettyPrinter.Unexpander
  | `($_ $F $X)  => `($(F).obj $X)
  | _           => throw ()

but of course I get an error unknown constant 'CategoryTheory.Functor.toPrefunctor.obj'.

[Adam Topaz]

Here's a more minimal example:

import Mathlib

@[ext]
structure A where
  X : ℕ

@[ext]
structure B extends A

example (b c : B) (h : b.X = c.X) : b = c := by
  ext
  /-
  bc: B
  h: b.toA.X = c.toA.X   <-- I would like this to be h: b.X = c.X
  ⊢ b.toA.X = c.toA.X    <-- I would like this to be b.X = b.X
  -/
  rw [h]

I can't seem to figure out how to write an delaborator or an unexpander which accomplishes what I mention in the comments.

[Adam Topaz]

related discussion: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Annoying.20error.20with.20naming.20after.20structure.20fields/near/338300277

[Matthew Ballard]

I think you need something like Prefunctor.obj F.toPrefunctor

[Adam Topaz]

I think I tried that as well...

[Adam Topaz]

Hey!, this seems to work!

@[app_unexpander Prefunctor.obj] def
  unexpandFunctorObj : Lean.PrettyPrinter.Unexpander
  | `($_ $(F).toPrefunctor $X)  => `($(F).obj $X)
  | _           => throw ()

[Adam Topaz]

!4#2545

[Kevin Buzzard]

Nice! Will hopefully serve as a model for future issues of this nature.

[Kyle Miller]

With both the Prefunctor example and this Functor example, I'm seeing ⊢ F.obj✝ X = F.obj✝ Y in the infoview. What's causing the ✝'s to show up here? Presumably it's to do with hygiene?

[Sebastian Ullrich]

Right, this seems like a valid use case for just setting hygiene false. The generated identifier will never go through the elaborator after all.

[Eric Wieser]

Can we somehow have this unexpander work for all nested projections through extends?

[Sebastian Ullrich]

Not automatically, the unexpander framework knows nothing about structures

[Sebastian Ullrich]

It would make more sense to have a general pp option for using dot notation, like in Lean 3

[Adam Topaz]

I turned off hygiene in the actual PR

[Adam Topaz]

Sebastian Ullrich said:

It would make more sense to have a general pp option for using dot notation, like in Lean 3

In lean3, would this approach show F.toPrefunctor.obj or F.obj? I thought it was the former, but it would be really nice to have the latter.

[Adam Topaz]

:ping_pong: let me bring this up to the top for a moment.

What do folks think about !4#2545 ? It would really help porting the category theory library. I understand it's not the ideal solution, but if I understand correctly from @Sebastian Ullrich 's message, to do something properly would require changing core, and that's likely to take a while. So can we merge that PR now as a temporary fix with the plan to delete the unexpanders once (well, "if") core is updated in the future?

[Matthew Ballard]

What is the worst that can happen?

[Adam Topaz]

I think the worst that can happen is that some things are pretty printed as they should be, which is far from the end of the world

[Matthew Ballard]

That is already happening :)

[Adam Topaz]

exactly :)

[Eric Wieser]

I think we should have a Lean4 tracking issue to refer to before we add things like this to mathlib4; presumably we will find ourselves adding a handful of similar things elsewhere, and having a single issue to link them together is valuable

[Adam Topaz]

I'm happy to open a lean4 issue, but this isn't really an issue, rather a feature request. And I was under the impression that such requests are not yet welcome for lean4.

[Eric Wieser]

Maybe open it the mathlib4 repo then for now

[Scott Morrison]

I've hit merge on this one. @Adam Topaz, could you open a mathlib4 issue for now? I think Eric's suggestion that we keep track of this feature request is good.

[Adam Topaz]

Thanks! I’m away from the computer right now, but I will make sure to open a mathlib4 issue tomorrow. I also agree that we need to keep track of such things.

[Adam Topaz]

Adam Topaz said:

Thanks! I’m away from the computer right now, but I will make sure to open a mathlib4 issue tomorrow. I also agree that we need to keep track of such things.

!4#2724

[Adam Topaz]

!4#2791 adds similar unexpanders for natural transformations and natural isomorphisms.

[Scott Morrison]

The first error at https://github.com/leanprover-community/mathlib4/pull/2815 is:

tactic 'aesop' failed, failed to prove the goal after exhaustive search.
F: C ⥤ Type w
XYZ: Functor.Elements F
f: X ⟶ Y
g: Y ⟶ Z
⊢ Prefunctor.map F.toPrefunctor (↑f ≫ ↑g) X.snd = Z.snd

Does anyone know why the unexpander is not working here?

[Adam Topaz]

Is this isolated, or was there some regression?

[Adam Topaz]

I ran into a similar failure of the unexpander the other day, but didn’t think much of it. I’ll try to track it down

[Adam Topaz]

@Scott Morrison I think in this case the issue is that (F.map whatever) is a function which has been applied to X.snd.

[Adam Topaz]

but I don't understand unexpanders well enough to say whether this is expected behavior

[Scott Morrison]

I thought that might be relevant, but assumed that the unexpander would still get to see the head of the application.

[Adam Topaz]

All I know for sure is that the following fixed the pretty printing:

@[app_unexpander Prefunctor.map] def
  test : Lean.PrettyPrinter.Unexpander
  | `($_ $(F).toPrefunctor $X $Y) => set_option hygiene false in `($(F).map $X $Y)
  | _ => throw ()

[Adam Topaz]

what's the antiquotation syntax for $X $Y ... $?? with arbitrarily many terms?

[Adam Topaz]

okay, maybe this is better?

@[app_unexpander Prefunctor.map] def
  test : Lean.PrettyPrinter.Unexpander
  | `($_ $(F).toPrefunctor $(X)*) => set_option hygiene false in `($(F).map $(X)*)
  | _ => throw ()

[Adam Topaz]

At least that works in both cases of interest.

[Adam Topaz]

!4#3160 should be a fix, at least for now.

[Adam Topaz]

This also has the benefit that F.map without any morphism will not be displayed as Prefunctor.map F.toPrefunctor.