Simp normal form in category of types

Stream: mathlib4

[Christian Merten]

When I want to simplify some term in the category of types, because of docs#CategoryTheory.types_comp_apply, simp often turns the term in something that it can't work with afterwards. Example:

import Mathlib

open CategoryTheory Limits

example {α β γ : Type} (f : α → γ) (g : β → γ) (a : α) (b : β) (h : f a = g b) :
    (pullback.fst : _ ⟶ α) ((Types.pullbackIsoPullback f g).inv ⟨(a, b), h⟩) = a := by
  simp -- does not work

example {α β γ : Type} (f : α → γ) (g : β → γ) (a : α) (b : β) (h : f a = g b) :
    (pullback.fst : _ ⟶ α) ((Types.pullbackIsoPullback f g).inv ⟨(a, b), h⟩) = a := by
  -- manually rewriting to apply the necessary lemma
  show ((Types.pullbackIsoPullback f g).inv  ≫ pullback.fst) ⟨(a, b), h⟩ = a
  -- rw with this explicit lemma (using simp here undoes the above line)
  rw [Types.pullbackIsoPullback_inv_fst]

How can I circumvent that? Can I locally disable usage of types_comp_apply? (which does not help if the statement is already in the applied form)
Or should the simp lemmas in docs#CategoryTheory.Limits.Shapes.Types be formulated in the applied form?

[Adam Topaz]

The structured answer is that we are supposed to use the "elementwise" tag to generate good simp lemmas when working in concrete categories. But in reality, I have also found working in the category of types to be quite annoying at time, for essentially this reason.

[Christian Merten]

Where would I use the "elementwise" tag? On docs#Types.pullbackIsoPullback ?

[Adam Topaz]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/CategoryTheory/Elementwise.html#Tactic.Elementwise.elementwise

[Adam Topaz]

Personally I think we should redefine the category of types along the following lines:

import Mathlib.CategoryTheory.Category.Basic

open CategoryTheory

universe u

structure BundledFunction (A B : Type*) where
  toFun : A → B

instance {A B} : FunLike (BundledFunction A B) A (fun _ => B) where
  coe f := f.toFun
  coe_injective' := fun ⟨f⟩ ⟨g⟩ _ => by congr

instance : Category (Type u) where
  Hom := BundledFunction
  id X := ⟨id⟩
  comp f g := .mk <| g.toFun ∘ f.toFun

[Christian Merten]

Can you explain how that would solve this issue?

[Adam Topaz]

It would provide a layer of separation that distinguishes between morphisms and functions. So if you have a morphism f in Type u, the function would be f.toFun. In most cases where I've been annoyed by this the issue seemed that lean can't distinguish between when f should be a morphism and when it should be a function. This approach would add a syntactic separation between the two.

[Adam Topaz]

We had a similar issue with morphisms in the category of sheaves being defined as natural transformations, and making docs#CategoryTheory.Sheaf.Hom made it much better

[Christian Merten]

Adding

@[simp, elementwise]

to pullbackIsoPullback_inv_fst strangely yields this lemma

CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst_apply.{u} {X Y Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z)
  (x : (Types.pullbackCone f g).pt) : pullback.fst ((Types.pullbackConeIsoPullback f g).inv.hom x) = (fun p ↦ (↑p).1) x

which says something about Types.pullbackConeIsoPullback f g instead of Types.pullbackIsoPullback f g. Is this expected?

[Adam Topaz]

this might be a bug in the elementwise attribute. probably one should apply docs#Lean.Expr.headBeta at some point

[Christian Merten]

Adam Topaz said:

It would provide a layer of separation that distinguishes between morphisms and functions. So if you have a morphism f in Type u, the function would be f.toFun. In most cases where I've been annoyed by this the issue seemed that lean can't distinguish between when f should be a morphism and when it should be a function. This approach would add a syntactic separation between the two.

Makes sense, would you still want a types_comp_apply style lemma? If yes, it would probably not solve this issue, right?

[Adam Topaz]

Yes, there would still be such lemmas so you can use the simplifier to go back and forth between morphisms and functions.

[Christian Merten]

So also with your approach, we would need to tag everything as elementwise to have it work with types_comp_apply?

[Adam Topaz]

It's possible that elementwise wouldn't be needed anymore, but I don't know. I think the only way to see if this is a good solution is to try it out and see if things become easier!

[Adam Topaz]

FWIW I think it would make sense to do similar things for other "bundled" categories like Top, GroupCat, etc.

[Adam Topaz]

Especially in TopCat I found that lean often gets confused by the fact that morphisms are defined as terms of C(X,Y).

[Kyle Miller]

There's an elementwise_of% term elaborator for transforming lemmas by the way, but it doesn't do a final simp on the LHS and RHS. (@Adam Topaz @[elementwise] is supposed to do simp on its result, so I'm not sure why the RHS is (fun p ↦ (↑p).1) x.)

[Christian Merten]

I am more irritated about the appearance of Types.pullbackConeIsoPullback instead of Types.pullbackIsoPullback. Or can this be circumvented by using elementwise_of?

[Kyle Miller]

I'm guessing it's being caused by @[elementwise] doing simp and there's some simp lemma doing that transformation. The reason for simp by the way is that @[simp] lemmas need a LHS in simp normal form.

elementwise_of% should help you circumvent this, though I don't know if it will give you a lemma in a usable form.

[Christian Merten]

Kyle Miller said:

I'm guessing it's being caused by @[elementwise] doing simp and there's some simp lemma doing that transformation. The reason for simp by the way is that @[simp] lemmas need a LHS in simp normal form.

elementwise_of% should help you circumvent this, though I don't know if it will give you a lemma in a usable form.

This does indeed generate the correct lemma. Can I tag pullbackIsoPullback_inv_fst somehow like for the elementwise attribute or do I have to write the lemma myself and use

rw [elementwise_of% pullbackIsoPullback_inv_fst]

as the proof?

[Christian Merten]

I am confused by this line in the docstring:

@[elementwise nosimp] to not use simp on both sides of the generated lemma

If I do this, the result is even worse, so apparently there is still some rewriting going on that is beyond CategoryTheory.coe_comp and CategoryTheory.coe_id?