simpNF linter not flagging a generated simp lemma

Stream: mathlib4

[Calle Sönne]

I noticed that the automatically generated simp lemma CategoryTheory.OplaxFunctor.bicategory_comp_naturality is already provable by simp, but the simpNF linter does not seem to flag it. Does anyone know why this is not flagged?

Here is an example corresponding to this lemma, showing its provable by simp.

example (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂)
[inst_1 : CategoryTheory.Bicategory C]
        {X Y Z : CategoryTheory.OplaxFunctor B C} (η : X ⟶ Y)
        (θ : CategoryTheory.OplaxNatTrans Y Z) {a b : B} (f : a ⟶ b) :
        (η ≫ θ).naturality f =
          (α_ (X.map f) (η.app b) (θ.app b)).inv ≫
            η.naturality f ▷ θ.app b ≫
              (α_ (η.app a) (Y.map f) (θ.app b)).hom ≫ η.app a ◁ θ.naturality f ≫
(α_ (η.app a) (θ.app a) (Z.map f)).inv := by
  simp

Here is the full file Bicategory/FunctorBicategory, with the above example added before the bicategory instance, to show that it is provable by simp before the simp lemma is added:

/-
Copyright (c) 2022 Yuma Mizuno. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yuma Mizuno
-/
import Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

/-!
# The bicategory of oplax functors between two bicategories

Given bicategories `B` and `C`, we give a bicategory structure on `OplaxFunctor B C` whose
* objects are oplax functors,
* 1-morphisms are oplax natural transformations, and
* 2-morphisms are modifications.
-/


namespace CategoryTheory

open Category Bicategory

open scoped Bicategory

universe w₁ w₂ v₁ v₂ u₁ u₂

variable {B : Type u₁} [Bicategory.{w₁, v₁} B] {C : Type u₂} [Bicategory.{w₂, v₂} C]
variable {F G H I : OplaxFunctor B C}

namespace OplaxNatTrans

/-- Left whiskering of an oplax natural transformation and a modification. -/
@[simps]
def whiskerLeft (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) : η ≫ θ ⟶ η ≫ ι where
  app a := η.app a ◁ Γ.app a
  naturality {a b} f := by
    dsimp
    rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc]
    simp

/-- Right whiskering of an oplax natural transformation and a modification. -/
@[simps]
def whiskerRight {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) : η ≫ ι ⟶ θ ≫ ι where
  app a := Γ.app a ▷ ι.app a
  naturality {a b} f := by
    dsimp
    simp_rw [assoc, ← associator_inv_naturality_left, whisker_exchange_assoc]
    simp

/-- Associator for the vertical composition of oplax natural transformations. -/
-- Porting note: verified that projections are correct and changed @[simps] to @[simps!]
@[simps!]
def associator (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) : (η ≫ θ) ≫ ι ≅ η ≫ θ ≫ ι :=
  ModificationIso.ofComponents (fun a => α_ (η.app a) (θ.app a) (ι.app a)) (by aesop_cat)

/-- Left unitor for the vertical composition of oplax natural transformations. -/
-- Porting note: verified that projections are correct and changed @[simps] to @[simps!]
@[simps!]
def leftUnitor (η : F ⟶ G) : 𝟙 F ≫ η ≅ η :=
  ModificationIso.ofComponents (fun a => λ_ (η.app a)) (by aesop_cat)

/-- Right unitor for the vertical composition of oplax natural transformations. -/
-- Porting note: verified that projections are correct and changed @[simps] to @[simps!]
@[simps!]
def rightUnitor (η : F ⟶ G) : η ≫ 𝟙 G ≅ η :=
  ModificationIso.ofComponents (fun a => ρ_ (η.app a)) (by aesop_cat)

end OplaxNatTrans

variable (B C)

example (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂)
[inst_1 : CategoryTheory.Bicategory C]
        {X Y Z : CategoryTheory.OplaxFunctor B C} (η : X ⟶ Y)
        (θ : CategoryTheory.OplaxNatTrans Y Z) {a b : B} (f : a ⟶ b) :
        (η ≫ θ).naturality f =
          (α_ (X.map f) (η.app b) (θ.app b)).inv ≫
            η.naturality f ▷ θ.app b ≫
              (α_ (η.app a) (Y.map f) (θ.app b)).hom ≫ η.app a ◁ θ.naturality f ≫
(α_ (η.app a) (θ.app a) (Z.map f)).inv := by
  simp

/-- A bicategory structure on the oplax functors between bicategories. -/
-- Porting note: verified that projections are correct and changed @[simps] to @[simps!]
@[simps!]
instance OplaxFunctor.bicategory : Bicategory (OplaxFunctor B C) where
  whiskerLeft {F G H} η _ _ Γ := OplaxNatTrans.whiskerLeft η Γ
  whiskerRight {F G H} _ _ Γ η := OplaxNatTrans.whiskerRight Γ η
  associator {F G H} I := OplaxNatTrans.associator
  leftUnitor {F G} := OplaxNatTrans.leftUnitor
  rightUnitor {F G} := OplaxNatTrans.rightUnitor
  whisker_exchange {a b c f g h i} η θ := by
    ext
    exact whisker_exchange _ _

end CategoryTheory

[Calle Sönne]

The reason I found this out is because I am trying to set up the analogous bicategory for pseudofunctors (but with strong transformations), and in that case the simpNF linter does complain about the analogous lemma.

[Johan Commelin]

Is it currently being proved by rfl? If so, then it becomes a dsimp-lemma. Can dsimp already prove the lemma?

[Calle Sönne]

Yeah dsimp can also already prove the lemma

[Violeta Hernández]

Note that a lemma being provable by simp isn't quite the same as simp being able to fire on it. Consider a scenario like the following

import Mathlib.Logic.Unique

def card (α : Type*) : Nat := sorry

@[simp]
theorem card_eq_one (α : Type*) : card a = 1 ↔ Nonempty (Unique α) :=
  sorry

@[simp]
theorem unique_unit : Nonempty (Unique Unit) :=
  ⟨inferInstance⟩

  -- simp can prove this
theorem card_unit : card Unit = 1 := by
  simp

-- but not this!
theorem card_sum : card Unit + card Unit = 2 := by
  simp -- no progress

[Violeta Hernández]

Sorry, I've got no idea how to minify links and I can't copy and paste from mobile

[Richard Copley]

Violeta Hernández said:

Sorry, I've got no idea how to minify links and I can't copy and paste from mobile

There's no need: if you enter the (self-contained) code in a markdown code block, a "View in Live Playground" link appears in the top-right corner when you hover over (or tap) the rendered block.

[Violeta Hernández]

Yeah, but I can't copy the code from the playground :frown:

[Violeta Hernández]

on my computer now, formatted my example better

[Calle Sönne]

Violeta Hernández said:

Note that a lemma being provable by simp isn't quite the same as simp being able to fire on it. Consider a scenario like the following

import Mathlib.Logic.Unique

def card (α : Type*) : Nat := sorry

@[simp]
theorem card_eq_one (α : Type*) : card a = 1 ↔ Nonempty (Unique α) :=
  sorry

@[simp]
theorem unique_unit : Nonempty (Unique Unit) :=
  ⟨inferInstance⟩

  -- simp can prove this
theorem card_unit : card Unit = 1 := by
  simp

-- but not this!
theorem card_sum : card Unit + card Unit = 2 := by
  simp -- no progress

I feel like this is a separate issue, to me "provable by simp" means that by simp proves it (and in my example above by dsimp proves it even).

[Violeta Hernández]

I can't read the category theory files, so really I'm just pointing out a possible cause.