reassoc and simp

Stream: mathlib4

[Kevin Buzzard]

I'm trying to write a @[reassoc] docstring (see here). I learnt yesterday, coincidentally from reading someone else's comment on a PR, that if you want a reassociated lemma attached to a simp lemma to also be a simp lemma, then apparently you need to tag it @[simp, reassoc] rather than @[reassoc, simp]. This is exactly the sort of thing that should be documented in a place which a user can find easily, if it's true. But in Lean 4 it seems to be much much harder to figure out which attributes a declaration is tagged with. I tried to test this claim:

import Mathlib.CategoryTheory.Whiskering

open CategoryTheory

universe v u

@[simp, reassoc]
lemma foo (C : Type u) [Category.{v} C] (x y z : C) (f : x ⟶ y) (h : y ⟶ z) (g : x ⟶ z) :
    f ≫ h = g := sorry

example (C : Type) [Category C] (x y z : C) (f : x ⟶ y) (h : y ⟶ z) (g : x ⟶ z)
  {Z : C} (h_1 : z ⟶ Z) : f ≫ h ≫ h_1 = g ≫ h_1 := by simp -- fails

But my example fails, and rw [foo_assoc] works. So now I don't know whether this is a case of simp failing and rw working, or whether the claim about reassoc simp lemmas is wrong, and don't know how to find out either. Can someone help?

[Markus Himmel]

I think your foo cannot be applied by simp, as by simp only [foo_assoc] doesn't work either. The order of reassoc and simp mattered in Lean 3. In Lean 4, the correct way to mark both versions of the lemma is to write @[reassoc (attr := simp)], and if you don't want the reassoc version to be simp then you write @[simp, reassoc].

[Markus Himmel]

You can use this code to test the various combinations of reassoc and simp:

import Mathlib.CategoryTheory.Whiskering

open CategoryTheory

universe v u

@[reassoc (attr := simp)]
lemma foo (C : Type u) [Category.{v} C] (x y z : C) (f : x ⟶ y) (h : y ⟶ z) (g : x ⟶ z) :
    f ≫ h = g := sorry

open Lean

run_meta do
  let env ← getEnv
  dbg_trace "{hasSimpAttribute env `foo}"
  dbg_trace "{hasSimpAttribute env `foo_assoc}"

[Kevin Buzzard]

Thanks! #14447

[Kyle Miller]

It looks like @[elementwise] got the explanation, if you want to compare: https://github.com/leanprover-community/mathlib4/blob/d2e8846f9bb14855a6d84e36552bc60e38bab88f/Mathlib/Tactic/CategoryTheory/Elementwise.lean#L145-L183 (The tactics are somewhat similar)

The idea behind (attr := simp) comes from Floris via @[to_additive]. (Well, more precisely, via from sharing an office with Floris and discussing the issue.)

[Kevin Buzzard]

Oh nice -- I hadn't even heard of that attribute (or I had heard about it and then I'd forgotten about it), and the docstring is exactly what I'd want to see if I saw it in code I was reviewing.

[Kevin Buzzard]

I would naively imagine that there could be a nice tutorial written about how to write an @[elementwise] attribute which implemented the specification in that docstring. Or is it much much more complicated than I imagine? Is everything in that one file?

[Kyle Miller]

Everything for elementwise is in that one file. That particular attribute is sort of complicated because it needs to insert a new instance argument and a universe level parameter to specialize to a concrete category, but maybe someone could clean it up and simplify it.

[Kevin Buzzard]

My naive mental model is that "meta code" (or whatever it's called now) is able to manipulate Exprs, and so dropping in a new instance argument and a universe level parameter into a term should be basic operations :-)