grind on `CostructuredArrow.w`

Stream: mathlib4

[Robin Carlier]

I was experimenting with grind and was very surprised to see the result of annotating docs#CategoryTheory.CostructuredArrow.w with grind.

as a reminder, the lemma has type

∀ {C : Type u₁} [inst : Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : Category.{v₂, u₂} D] {T : D} {S : C ⥤ D}
  {A B : CostructuredArrow S T} (f : A ⟶ B), S.map f.left ≫ B.hom = A.hom

and the generated pattern is

/--
info: w: [@CategoryStruct.comp #6 _ (@Functor.obj #8 #7 _ #5 #3 (@Comma.left _ _ `[Discrete
     PUnit.{1}] `[discreteCategory
     PUnit.{1}] _ _ #3 (@Functor.obj _ _ (Functor `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) _ (Functor.const `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) #4) #2)) (@Functor.obj _ _ _ _ #3 (@Comma.left _ _ `[Discrete
     PUnit.{1}] `[discreteCategory
     PUnit.{1}] _ _ #3 (@Functor.obj _ _ (Functor `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) _ (Functor.const `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) #4) #1)) (@Functor.obj `[Discrete
    PUnit.{1}] `[discreteCategory
    PUnit.{1}] _ _ (@Functor.obj _ _ (Functor `[Discrete
      PUnit.{1}] `[discreteCategory
      PUnit.{1}] _ _) _ (Functor.const `[Discrete
      PUnit.{1}] `[discreteCategory
      PUnit.{1}] _ _) #4) (@Comma.right _ _ `[Discrete
     PUnit.{1}] `[discreteCategory
     PUnit.{1}] _ _ #3 (@Functor.obj _ _ (Functor `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) _ (Functor.const `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) #4) #1)) (@Functor.map _ _ _ _ #3 (@Comma.left _ _ `[Discrete
     PUnit.{1}] `[discreteCategory
     PUnit.{1}] _ _ #3 (@Functor.obj _ _ (Functor `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) _ (Functor.const `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) #4) #2) (@Comma.left _ _ `[Discrete
     PUnit.{1}] `[discreteCategory
     PUnit.{1}] _ _ #3 (@Functor.obj _ _ (Functor `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) _ (Functor.const `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) #4) #1) (@CommaMorphism.left _ _ `[Discrete
     PUnit.{1}] `[discreteCategory
     PUnit.{1}] _ _ #3 (@Functor.obj _ _ (Functor `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) _ (Functor.const `[Discrete
       PUnit.{1}] `[discreteCategory
       PUnit.{1}] _ _) #4) #2 #1 #0)) (@Comma.hom _ _ `[Discrete
    PUnit.{1}] `[discreteCategory
    PUnit.{1}] _ _ #3 (@Functor.obj _ _ (Functor `[Discrete
      PUnit.{1}] `[discreteCategory
      PUnit.{1}] _ _) _ (Functor.const `[Discrete PUnit.{1}] `[discreteCategory PUnit.{1}] _ _) #4) #1)]
-/
#guard_msgs in
attribute [grind?] _root_.CategoryTheory.CostructuredArrow.w

which looks like a problem for making it trigger in nice situations

I suspect grind is trying to unfold the definitions for CostructuredArrows and their morphisms (which under the hood are morphisms in Comma categories with functors involving Discrete PUnit), where it clearly shouldn’t (perhaps because calling left and hom on objects leave no choice but to infer them as objects /homs in commas, and the underlying problem is in fact that we abuse the defeq between CostructuredArrows and Commas?). @Kim Morrison do you have an idea of the culprit/know how to fix this?

[Kim Morrison]

The culprit is that Functor.fromPUnit is an abbrev:

abbrev fromPUnit (X : C) : Discrete PUnit.{w + 1} ⥤ C :=
  (Functor.const _).obj X

While CostructuredArrow itself is a def (not reducible), Functor.fromPUnit is reducible. When grind's pattern preprocessing calls unfoldReducible (EMatchTheorem.lean:284), it expands Functor.fromPUnit T → (Functor.const (Discrete PUnit)).obj T, exposing all the Discrete PUnit machinery.

Do you want to experiment with changing fromPUnit from abbrev to def?

[Robin Carlier]

Thanks for the explanation!
I won't have time to experiment seriously with this in the immediate future, but I'll keep in in the backburner and come back to it the next time I'll try to improve the grind experience in category theory (probably around April) if no one beats me to it.