Annoying error with naming after structure fields

Stream: lean4

[Chris Hughes]

This came up in the port of CategoryTheory.Filtered !4#2493 . I can't make a definition called Y.x because it's the field of a structure, but the definition Y.x is not already there

structure X : Type :=
  (x : Nat)

structure Y extends X

def Y.x (y : Y) := X.x y.toX -- invalid declaration name 'Y.x', structure 'Y' has field 'x'

#print Y.x -- unknown constant 'Y.x'

[Eric Wieser]

Can we drop the def in mathlib3?

[Chris Hughes]

I'd rather not. I merged the PR, but I do consider this a TODO, i.e. we want the mathlib4 setup to eventually match the current mathlib3 setup.

[Eric Wieser]

What's the reason we have the def in lean3 (and what is the def in question?)

[Chris Hughes]

It puts something from the IsFilteredOrEmpty namespace into the IsFiltered namespace, but the lemmas still apply to the IsFilteredOrEmpty class. It's done like that so people usually don't have to think about the IsFilteredOrEmpty class, because it's usually the IsFiltered class that they want, even if a lot of the lemmas don't use the nonempty assumption of IsFiltered.

[Eric Wieser]

What's an example of a def we're talking about here?

[Chris Hughes]

https://github.com/leanprover-community/mathlib4/blob/5107462b5e8dba552debeb8b1a1b9c2e536430d9/Mathlib/CategoryTheory/Filtered.lean#L142

[Eric Wieser]

docs#category_theory.is_filtered.cocone_objs

[Eric Wieser]

Ah, so the motivation here is that we're actually working with a class not a structure, so there's no reasonable way to use dot notation

[Kevin Buzzard]

Here's another example of where this shows up: when porting CategoryTheory.Bicategory.Functor I was faced with a Lean 4 goal of

⊢ PrelaxFunctor.map₂ G.toPrelaxFunctor (PrelaxFunctor.map₂ F.toPrelaxFunctor (α_ f g h).hom) ≫
    (PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F f (g ≫ h)) ≫
        mapComp G (Prefunctor.map (↑F.toPrelaxFunctor) f) (Prefunctor.map (↑F.toPrelaxFunctor) (g ≫ h))) ≫
      Prefunctor.map (↑G.toPrelaxFunctor) (Prefunctor.map (↑F.toPrelaxFunctor) f) ◁
        (PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F g h) ≫
          mapComp G (Prefunctor.map (↑F.toPrelaxFunctor) g) (Prefunctor.map (↑F.toPrelaxFunctor) h)) =
  (PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F (f ≫ g) h) ≫
      mapComp G (Prefunctor.map (↑F.toPrelaxFunctor) (f ≫ g)) (Prefunctor.map (↑F.toPrelaxFunctor) h)) ≫
    (PrelaxFunctor.map₂ G.toPrelaxFunctor (mapComp F f g) ≫
          mapComp G (Prefunctor.map (↑F.toPrelaxFunctor) f) (Prefunctor.map (↑F.toPrelaxFunctor) g)) ▷
        Prefunctor.map (↑G.toPrelaxFunctor) (Prefunctor.map (↑F.toPrelaxFunctor) h) ≫
      (α_ (Prefunctor.map (↑G.toPrelaxFunctor) (Prefunctor.map (↑F.toPrelaxFunctor) f))
          (Prefunctor.map (↑G.toPrelaxFunctor) (Prefunctor.map (↑F.toPrelaxFunctor) g))
          (Prefunctor.map (↑G.toPrelaxFunctor) (Prefunctor.map (↑F.toPrelaxFunctor) h))).hom

where the corresponding Lean 3 goal was the defeq but far more controlled

G.map₂ (F.map₂ (α_ f g h).hom) ≫ (G.map₂ (F.map_comp f (g ≫ h)) ≫ G.map_comp (F.map f) (F.map (g ≫ h))) ≫ G.map (F.map f) ◁ (G.map₂ (F.map_comp g h) ≫ G.map_comp (F.map g) (F.map h)) = (G.map₂ (F.map_comp (f ≫ g) h) ≫ G.map_comp (F.map (f ≫ g)) (F.map h)) ≫ (G.map₂ (F.map_comp f g) ≫ G.map_comp (F.map f) (F.map g)) ▷ G.map (F.map h) ≫ (α_ (G.map (F.map f)) (G.map (F.map g)) (G.map (F.map h))).hom

The autoported proof didn't work so I had to get my hands dirty and figure out why. Here G : OplaxFunctor C D, and OplaxFunctor extends PrelaxFunctor, which has a map₂. The Lean 3 G.map₂ was being expanded to PrelaxFunctor.map₂ G.toPrelaxFunctor and because it was showing up often, it was pretty horrible. I tried to tame the goal by defining OplaxFunctor.map₂ to equal PrelaxFunctor.map₂ and ran into precisely this issue, so I had to work with these super-unwieldy goals whilst debugging. Note that here everything is a structure.

[Eric Wieser]

This sounds like something that the pretty-printing ought to handle

[Eric Wieser]

That is, it should have an option to display PrelaxFunctor.map₂ G.toPrelaxFunctor as G.map₂, and it should probably be the default

[Adam Topaz]

This is also an issue with plain old (category-theoretic) functors. We need to add some delaborators, I guess...

[Kevin Buzzard]

What's a delaborator and where can I learn about them?

[Adam Topaz]

https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/master/md/extra/pretty-printing.md

[Adam Topaz]

NB: I don't know if "delaborator" is precisely the right thing we need in this case.

[Adam Topaz]

BTW @Arthur Paulino I just noticed a (very) minor typo on https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/70a8ebaf5ac931eedf08761c0d1af5975641b233/md/extra/pretty-printing.md?plain=1#L20 (one of the elaborators should be a delaborator)

[Kevin Buzzard]

heh, I noticed that too and opened a PR :-)