Help with simpNF linter

Stream: mathlib4

[Adam Topaz]

Can someone who understands simps better than I do help me in linting !4#2424 ? It seems that simps! on the following line
https://github.com/leanprover-community/mathlib4/blob/5492db0c40ee02d592f04adb0219fb88800b4916/Mathlib/CategoryTheory/Adjunction/Opposites.lean#L37
is generating some lemmas which are not passing the simpNF linter.
Is this a bug in simps or is something else going on here? I'm not sure.

[Adam Topaz]

The lemmas generated by simps also look quite different from the analogous ones in mathlib3. I think the issue might be that some simp lemmas like docs4#CategoryTheory.Adjunction.homEquiv_unit and docs4#CategoryTheory.Adjunction.homEquiv_counit are not firing.

[Adam Topaz]

That's despite the fact that they're tagged with simp here:
https://github.com/leanprover-community/mathlib4/blob/b21620a738bdb033f8e5b97ca769d89ae650bfbc/Mathlib/CategoryTheory/Adjunction/Basic.lean#L133

[Floris van Doorn]

@[simps] never calls simp on the LHS of a lemma, so it has nothing to do with simp not firing.
The (LHS of) lemma CategoryTheory.Adjunction.adjointOfOpAdjointOp_homEquiv_apply looks entirely analogue to docs#category_theory.adjunction.adjoint_of_op_adjoint_op_hom_equiv_apply.

I'm not sure why this didn't trigger the simp_nf linter in Lean 3.
It seems a bit dangerous to generate simp lemmas where the LHS can be simplified further by CategoryTheory.Adjunction.homEquiv_unit.
It might have to do that the fact that in Lean 3 this simp lemma had low priority, which is not there in Lean 4. You could try making the priority of those simp attributes low in Lean 4, too. Alternatively, consider using something like initialize_simps_projections Adjunction (-homEquiv) to not generate lemmas for the homEquiv field. Or if you want the homEquiv lemma, but not the homEquiv_apply lemma, you can do this by using @[simps homEquiv unit counit] (this would have to be done for each simps-attribute on an adjunction). Though the last 2 options diverge from the behavior in Lean 3.

[Adam Topaz]

The mathlib4 lemma in question has this form:

CategoryTheory.Adjunction.adjointOfOpAdjointOp_homEquiv_apply:
      ∀ {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst_1 : CategoryTheory.Category D] (F : C ⥤ D)
        (G : D ⥤ C) (h : CategoryTheory.Functor.op G ⊣ CategoryTheory.Functor.op F) (X : C) (Y : D)
        (a :
          Opposite.unop (Prefunctor.obj (CategoryTheory.Functor.op F).toPrefunctor (Opposite.op X)) ⟶
            Opposite.unop (Opposite.op Y)),
        ↑(CategoryTheory.Adjunction.homEquiv (CategoryTheory.Adjunction.adjointOfOpAdjointOp F G h) X Y) a =
          ↑(CategoryTheory.opEquiv (Opposite.op (Prefunctor.obj G.toPrefunctor Y)) (Opposite.op X))
            (↑(Equiv.symm (CategoryTheory.Adjunction.homEquiv h (Opposite.op Y) (Opposite.op X)))
              (↑(Equiv.symm (CategoryTheory.opEquiv (Opposite.op Y) (Opposite.op (Prefunctor.obj F.toPrefunctor X))))
                a))

and the mathlib3 version is docs#category_theory.adjunction.adjoint_of_op_adjoint_op_hom_equiv_apply

[Adam Topaz]

The opEquiv/homEquiv in the RHS of the mathlib4 version is never simplified to something involving counit

[Adam Topaz]

I think I do want a lemma involving homEquiv_apply in this case.

[Adam Topaz]

in any case, docs4#CategoryTheory.opEquiv is tagged with simps as well, so it should dsimplify away from the RHS, right?

[Adam Topaz]

oh wait, I had things backwards.

[Adam Topaz]

sorry, I'm just thinking out loud here...

[Adam Topaz]

okay, I still think there might be an issue. the linter says

#check @adjointOfOpAdjointOp_homEquiv_apply /- Left-hand side simplifies from
  ↑(homEquiv (adjointOfOpAdjointOp F G h) X Y) a✝
to
  ↑(opEquiv (Opposite.op (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X))) (Opposite.op X))
    (↑(Equiv.symm (homEquiv h (Opposite.op (Prefunctor.obj F.toPrefunctor X)) (Opposite.op X)))
      (↑(Equiv.symm
            (opEquiv (Opposite.op (Prefunctor.obj F.toPrefunctor X)) (Opposite.op (Prefunctor.obj F.toPrefunctor X))))
        (𝟙 (Prefunctor.obj F.toPrefunctor X)))) ≫
  Prefunctor.map G.toPrefunctor a✝

but why isn't the opEquiv simplified away?

[Floris van Doorn]

The simpNF linter only cares about the LHS of lemmas. The RHS of the lemma might be different than in Lean 3, and that will likely have to do with simp lemmas firing or not, but it won't solve the simpNF linter.

but why isn't the opEquiv simplified away?

That is not really a relevant question. To appease the simpNF linter, the LHS should not simplify at all. Which in Lean 3 apparently didn't happen because of low priorities

[Adam Topaz]

Ah I see. Thanks for the explanation! I'm not sure what is the best way to proceed. Any ideas?

[Floris van Doorn]

I think attribute [simp low] is a thing in Lean 4, use that for every [priority 10, simp] that was in Lean 3.

[Floris van Doorn]

so my suggestion is to modify simp priorities in the already ported Adjunction file, to match Lean 3

[Adam Topaz]

I see. Perhaps it wouldn't hurt to only generate a homEquiv lemma without the homEquiv_apply variant.

[Floris van Doorn]

I think that would be an improvement (albeit not what we did in Lean 3).

[Floris van Doorn]

Though it might have downsides, since the right-hand sides of such lemmas could be really large.

[Adam Topaz]

yeah, but it's large even with the apply variant because nothing gets simplified away :rofl:

[Floris van Doorn]

That is something else worth investigating, yeah. I wonder why docs4#CategoryTheory.opEquiv_apply doesn't apply. Maybe the coercion is different? I'm going to stop investigating for now.

[Adam Topaz]

Yeah same here... I need to cook dinner. BTW, for my own understanding, what's the rationale for why simps doesnt simplify the LHS?

[Floris van Doorn]

Because there shouldn't be another simp lemma that applies to the LHS.