use cases of custom attributes

Stream: lean4

[Arthur Paulino]

@Siddharth Bhat and I are brainstorming about the use cases of custom attributes for the metaprogramming book and we came up with "simply recovering tagged declarations and then doing something else with them"

The problem is that "something else" is not super clear for us. Also, we are aware that it's possible to implement our own env modification function when those declarations are tagged with our custom attributes.

That said, we want to ask the community: what are interesting use cases of custom attributes you know?

[Patrick Massot]

tactic#norm_cast is an important case.

[Patrick Massot]

It relies on the eponymous attribute.

[Gabriel Ebner]

what are interesting use cases of custom attributes you know?

I can think of roughly two big classes of attributes:

1. Attributes that generate definitions. For example @[ext] structure foo generates @[ext] theorem foo.ext. (Other attributes in this class are to_additive, simps, etc.)
2. Tags that influence tactics. For example @[simp]. But also @[ext] is used as a tag on theorems, and to_additive is used as a tag that influences the to-additive-translation.

[Tomas Skrivan]

With the recent discussion about testing, I'm thinking about marking certain definitions with attribute unit_test. Then you can create a command that goes over the whole project and runs these tests.

[Siddharth Bhat]

Thanks! I'll try and explain these use-cases in the tutorial I'm writing: https://github.com/arthurpaulino/lean4-metaprogramming-book/pull/31

[Arthur Paulino]

@Siddharth Bhat we don't need to go too deep on every use case. If we can get one use case well explained, that should be enough for the goal of displaying part of the API as the tooling. Other use cases can be mentioned as ideas for the reader to think about.

[Siddhartha Gadgil]

Similar to the @[ext] attribute one can use @[symm] and @[trans] for symmetry and transitivity results. Indeed code using this is in my (long dormant) pull request https://github.com/leanprover-community/mathlib4/pull/253 to mathlib4.

[Siddhartha Gadgil]

Maybe the symm tactic can be an example of a writing a tactic too.

[Siddhartha Gadgil]

I can write this part if appropriate.

[Arthur Paulino]

@Siddhartha Gadgil it's not clear to me what the symm tactic teaches in terms of "building tactics". Maybe it's a better example of use cases of custom attributes. Let's see how the chapter will look once @Siddharth Bhat finishes it :+1:

[Siddhartha Gadgil]

Sure. I meant as an example of custom attributes, with a free tactic example thrown in. If there are alternative examples with custom attributes put to good use that would be fine.