User defined attributes in lean 3

Stream: general

[Bolton Bailey]

I would like to define an attribute to use with the simp tactic. However, when I try attribute [foo] my_lemma I get "unknown attribute [foo]".

This page of the Lean reference manual https://leanprover.github.io/reference/other_commands.html#attributes says that "users can declare additional attributes in Lean (see Chapter 7." but the link to this "chapter" contains a title, two subheadings and nothing else. :neutral:

Is it actually possible to make user defined attributes in Lean, and if so, how?

[Kevin Buzzard]

It is certainly possible -- mathlib adds many attributes to the system, but unfortunately I don't know the details.

[Floris van Doorn]

@[user_attribute] meta def my_attribute : user_attribute :=
{ name := `foo,
  descr := "My own attribute!" }

attribute [foo] nat.add_comm

Look around in the documentation for user_attribute for some more options (cache, parameters, tactics to be executed when you add an attribute).

[Floris van Doorn]

Or search mathlib for @[user_attribute] to see some examples.

[Bolton Bailey]

Thanks, this is great!

[Bolton Bailey]

Actually, I tried this example

@[user_attribute] meta def my_attribute : user_attribute :=
{ name := `foo,
  descr := "My own attribute!" }

attribute [foo] nat.add_assoc

lemma foo (a b : ℕ) : a + b + 2 = a + (b + 2) :=
begin
  simp with foo,
end

And got the error "unknown identifier 'simp_attr.foo'". After some digging in mathlib for an example, I came up with

run_cmd mk_simp_attr `bar
run_cmd tactic.add_doc_string `simp_attr.bar "String"

attribute [bar] nat.add_assoc

lemma test2 (a b : ℕ) : a + b + 2 = a + (b + 2) :=
begin
  simp with bar,
end

Which throws no errors.

[Bryan Gin-ge Chen]

mathlib has command#mk_simp_attribute which helps create new custom simp attributes.

[Floris van Doorn]

Oh my bad, I didn't read carefully enough that you meant simp attributes. In that case you indeed want mk_simp_attribute foo "My simp attribute".