ressoc (attr := simp)

Stream: mathlib4

[Adam Topaz]

Here is yet another issue I ran into while porting monoidal natural transformations.
The line

attribute [simp, reassoc (attr := simp)] MonoidalNatTrans.tensor

gives me a warning:

The source declaration CategoryTheory.MonoidalNatTrans.tensor was given attribute simp before calling @[reassoc]. The preferred method is to use `@[reassoc (attr := simp)]` to apply the attribute to both CategoryTheory.MonoidalNatTrans.tensor and the target declaration CategoryTheory.MonoidalNatTrans.tensor_assoc. [linter.existingAttributeWarning]

This is !4#2466
Is this a bug in reassoc?

[Matthew Ballard]

What do you want to attach simp to?

[Adam Topaz]

MonoidalNatTrans.tensor and MonoidalNatTrans.tensor_assoc

[Floris van Doorn]

Oh, that might be a copy-paste mistake when porting the attr := feature from to_additive to reassoc.

[Matthew Ballard]

I’ve been blindly following the linter suggestions here with the thought that you could simp from the assoc version to the regular version or that it did it for both.

[Adam Topaz]

Doing this in the other direction (i.e. attribute [reassoc (attr := simp), simp] MonoidalNatTrans.tensor) gets rid of the warning.

[Floris van Doorn]

Although, I think that reassoc (attr := simp) indeed applies simp to both the original declaration and the _assoc declaration.

[Adam Topaz]

Ah so you're saying that attribute [reassoc (attr := simp)] MonoidalNatTrans.tensor suffices here?

[Floris van Doorn]

yes

[Adam Topaz]

ok, thanks. I'll go with that for now.

[Adam Topaz]

Is there a quick way to verify whether a lemma has a simp attribute?

[Jireh Loreaux]

I'm not saying I love it, but you should just be able to copy it and try proving with by simp. There's probably a better way though.

[Matthew Ballard]

Try to remove it

[Matthew Ballard]

You’ll get yelled at if it isn’t tagged

[Adam Topaz]

okay, using the by simp check does indeed verify what Floris said above :)

[Floris van Doorn]

Another way: (the two declarations are in PR !4#2397)

open Lean Meta Elab Command Tactic Simp

/-- Checks whether `declName` is in `SimpTheorems` as either a lemma or definition to unfold. -/
def Lean.Meta.SimpTheorems.hasAttribute (d : SimpTheorems) (declName : Name) :=
  d.isLemma (.decl declName) || d.isDeclToUnfold declName

/-- Tests whether `decl` has `simp`-attribute `simpAttr`. Returns `false` is `simpAttr` is not a
valid simp-attribute. -/
def isInSimpSet (simpAttr decl : Name) : CoreM Bool := do
  let .some simpDecl ← getSimpExtension? simpAttr | return false
  return (← simpDecl.getTheorems).hasAttribute decl

run_cmd liftCoreM do logInfo m!"{← isInSimpSet `simp `myLemma}" -- replace myLemma