Attributes
Attributes are a tool for associating information with declarations.
In the simplest case, an attribute is a tag that can be applied to a declaration.
simp
is a common example of this. A lemma
@[simp] lemma foo : ...
has been tagged with the simp
attribute.
When the simplifier runs, it will collect all lemmas that have been tagged with this attribute.
More complicated attributes take parameters. An example of this is the nolint
attribute.
It takes a list of linter names when it is applied, and for each declaration tagged with @[nolint linter_1 linter_2]
,
this list can be accessed by a metaprogram.
Attributes can also be applied to declarations with the syntax:
attribute [attr_name] decl_name_1 decl_name_2 decl_name 3
The core API for creating and using attributes can be found in init.meta.attribute.
ancestor
The ancestor
attributes is used to record the names of structures which appear in the
extends clause of a structure
or class
declared with old_structure_cmd
set to true.
As an example:
set_option old_structure_cmd true
structure base_one := (one : ℕ)
structure base_two (α : Type*) := (two : ℕ)
@[ancestor base_one base_two]
structure bar extends base_one, base_two α
The list of ancestors should be in the order they appear in the extends
clause, and should
contain only the names of the ancestor structures, without any arguments.
Related declarations
Import using
 import tactic.algebra
 import tactic.basic
elementwise
The elementwise
attribute can be applied to a lemma
@[elementwise]
lemma some_lemma {C : Type*} [category C]
{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : X ⟶ Z) (w : ...) : f ≫ g = h := ...
and will produce
lemma some_lemma_apply {C : Type*} [category C] [concrete_category C]
{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : X ⟶ Z) (w : ...) (x : X) : g (f x) = h x := ...
Here X
is being coerced to a type via concrete_category.has_coe_to_sort
and
f
, g
, and h
are being coerced to functions via concrete_category.has_coe_to_fun
.
Further, we simplify the type using concrete_category.coe_id : ((𝟙 X) : X → X) x = x
and
concrete_category.coe_comp : (f ≫ g) x = g (f x)
,
replacing morphism composition with function composition.
The [concrete_category C]
argument will be omitted if it is possible to synthesize an instance.
The name of the produced lemma can be specified with @[elementwise other_lemma_name]
.
If simp
is added first, the generated lemma will also have the simp
attribute.
Related declarations
Import using
 import tactic.elementwise
ext
Tag lemmas of the form:
@[ext]
lemma my_collection.ext (a b : my_collection)
(h : ∀ x, a.lookup x = b.lookup y) :
a = b := ...
The attribute indexes extensionality lemma using the type of the
objects (i.e. my_collection
) which it gets from the statement of
the lemma. In some cases, the same lemma can be used to state the
extensionality of multiple types that are definitionally equivalent.
Also, the following:
@[ext]
lemma my_collection.ext (a b : my_collection)
(h : ∀ x, a.lookup x = b.lookup y) :
a = b := ...
is equivalent to
@[ext my_collection]
lemma my_collection.ext (a b : my_collection)
(h : ∀ x, a.lookup x = b.lookup y) :
a = b := ...
This allows us specify type synonyms along with the type that is referred to in the lemma statement.
@[ext, ext my_type_synonym]
lemma my_collection.ext (a b : my_collection)
(h : ∀ x, a.lookup x = b.lookup y) :
a = b := ...
The ext
attribute can be applied to a structure to generate its extensionality lemmas:
@[ext]
structure foo (α : Type*) :=
(x y : ℕ)
(z : {z // z < x})
(k : α)
(h : x < y)
will generate:
@[ext] lemma foo.ext : ∀ {α : Type u_1} (x y : foo α),
x.x = y.x → x.y = y.y → x.z == y.z → x.k = y.k → x = y
lemma foo.ext_iff : ∀ {α : Type u_1} (x y : foo α),
x = y ↔ x.x = y.x ∧ x.y = y.y ∧ x.z == y.z ∧ x.k = y.k
Related declarations
Import using
 import tactic.ext
 import tactic.basic
higher_order
A user attribute that applies to lemmas of the shape ∀ x, f (g x) = h x
.
It derives an auxiliary lemma of the form f ∘ g = h
for reasoning about higherorder functions.
Related declarations
Import using
 import tactic.core
 import tactic.basic
hint_tactic
An attribute marking a tactic unit
or tactic string
which should be used by the hint
tactic.
Related declarations
Import using
 import tactic.hint
 import tactic.basic
interactive
Copies a definition into the tactic.interactive
namespace to make it usable
in proof scripts. It allows one to write
@[interactive]
meta def my_tactic := ...
instead of
meta def my_tactic := ...
run_cmd add_interactive [``my_tactic]
```
Related declarations
Import using
 import tactic.core
 import tactic.basic
linter
Defines the user attribute linter
for adding a linter to the default set.
Linters should be defined in the linter
namespace.
A linter linter.my_new_linter
is referred to as my_new_linter
(without the linter
namespace)
when used in #lint
.
Related declarations
Import using
 import tactic.lint.basic
 import tactic.basic
mk_iff
Applying the mk_iff
attribute to an inductivelydefined proposition mk_iff
makes an iff
rule
r
with the shape ∀ps is, i as ↔ ⋁_j, ∃cs, is = cs
, where ps
are the type parameters, is
are
the indices, j
ranges over all possible constructors, the cs
are the parameters for each of the
constructors, and the equalities is = cs
are the instantiations for each constructor for each of
the indices to the inductive type i
.
In each case, we remove constructor parameters (i.e. cs
) when the corresponding equality would
be just c = i
for some index i
.
For example, if we try the following:
@[mk_iff] structure foo (m n : ℕ) : Prop :=
(equal : m = n)
(sum_eq_two : m + n = 2)
Then #check foo_iff
returns:
foo_iff : ∀ (m n : ℕ), foo m n ↔ m = n ∧ m + n = 2
You can add an optional string after mk_iff
to change the name of the generated lemma.
For example, if we try the following:
@[mk_iff bar] structure foo (m n : ℕ) : Prop :=
(equal : m = n)
(sum_eq_two : m + n = 2)
Then #check bar
returns:
bar : ∀ (m n : ℕ), foo m n ↔ m = n ∧ m + n = 2
See also the user command mk_iff_of_inductive_prop
.
Related declarations
Import using
 import tactic.mk_iff_of_inductive_prop
 import tactic.basic
nolint
Defines the user attribute nolint
for skipping #lint
Related declarations
Import using
 import tactic.lint.basic
 import tactic.basic
norm_cast attributes
The norm_cast
attribute should be given to lemmas that describe the
behaviour of a coercion in regard to an operator, a relation, or a particular
function.
It only concerns equality or iff lemmas involving ↑
, ⇑
and ↥
, describing the behavior of
the coercion functions.
It does not apply to the explicit functions that define the coercions.
Examples:
@[norm_cast] theorem coe_nat_inj' {m n : ℕ} : (↑m : ℤ) = ↑n ↔ m = n
@[norm_cast] theorem coe_int_denom (n : ℤ) : (n : ℚ).denom = 1
@[norm_cast] theorem cast_id : ∀ n : ℚ, ↑n = n
@[norm_cast] theorem coe_nat_add (m n : ℕ) : (↑(m + n) : ℤ) = ↑m + ↑n
@[norm_cast] theorem cast_sub [add_group α] [has_one α] {m n} (h : m ≤ n) :
((n  m : ℕ) : α) = n  m
@[norm_cast] theorem coe_nat_bit0 (n : ℕ) : (↑(bit0 n) : ℤ) = bit0 ↑n
@[norm_cast] theorem cast_coe_nat (n : ℕ) : ((n : ℤ) : α) = n
@[norm_cast] theorem cast_one : ((1 : ℚ) : α) = 1
Lemmas tagged with @[norm_cast]
are classified into three categories: move
, elim
, and
squash
. They are classified roughly as follows:
 elim lemma: LHS has 0 head coes and ≥ 1 internal coe
 move lemma: LHS has 1 head coe and 0 internal coes, RHS has 0 head coes and ≥ 1 internal coes
 squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes
norm_cast
uses move
and elim
lemmas to factor coercions toward the root of an expression
and to cancel them from both sides of an equation or relation. It uses squash
lemmas to clean
up the result.
Occasionally you may want to override the automatic classification.
You can do this by giving an optional elim
, move
, or squash
parameter to the attribute.
@[simp, norm_cast elim] lemma nat_cast_re (n : ℕ) : (n : ℂ).re = n :=
by rw [← of_real_nat_cast, of_real_re]
Don't do this unless you understand what you are doing.
A full description of the tactic, and the use of each lemma category, can be found at https://leanforward.github.io/norm_cast/norm_cast.pdf.
Related declarations
Import using
 import tactic.norm_cast
 import tactic.basic
norm_num
An attribute for adding additional extensions to norm_num
. To use this attribute, put
@[norm_num]
on a tactic of type expr → tactic (expr × expr)
; the tactic will be called on
subterms by norm_num
, and it is responsible for identifying that the expression is a numerical
function applied to numerals, for example nat.fib 17
, and should return the reduced numerical
expression (which must be in norm_num
normal form: a natural or rational numeral, i.e. 37
,
12 / 7
or (2 / 3)
, although this can be an expression in any type), and the proof that the
original expression is equal to the rewritten expression.
Failure is used to indicate that this tactic does not apply to the term. For performance reasons, it is best to detect nonapplicability as soon as possible so that the next tactic can have a go, so generally it will start with a pattern match and then checking that the arguments to the term are numerals or of the appropriate form, followed by proof construction, which should not fail.
Propositions are treated like any other term. The normal form for propositions is true
or
false
, so it should produce a proof of the form p = true
or p = false
. eq_true_intro
can be
used to help here.
Related declarations
Import using
 import tactic.norm_num
 import tactic
protect_proj
Attribute to protect the projections of a structure.
If a structure foo
is marked with the protect_proj
user attribute, then
all of the projections become protected, meaning they must always be referred to by
their full name foo.bar
, even when the foo
namespace is open.
protect_proj without bar baz
will protect all projections except for bar
and baz
.
Related declarations
Import using
 import tactic.protected
 import tactic.basic
protected
Attribute to protect a declaration.
If a declaration foo.bar
is marked protected, then it must be referred to
by its full name foo.bar
, even when the foo
namespace is open.
Protectedness is a built in parser feature that is independent of this attribute.
A declaration may be protected even if it does not have the @[protected]
attribute.
This provides a convenient way to protect many declarations at once.
Related declarations
Import using
 import tactic.protected
 import tactic.basic
reassoc
The reassoc
attribute can be applied to a lemma
@[reassoc]
lemma some_lemma : foo ≫ bar = baz := ...
to produce
lemma some_lemma_assoc {Y : C} (f : X ⟶ Y) : foo ≫ bar ≫ f = baz ≫ f := ...
The name of the produced lemma can be specified with @[reassoc other_lemma_name]
. If
simp
is added first, the generated lemma will also have the simp
attribute.
Related declarations
Import using
 import tactic.reassoc_axiom
 import tactic
simps
The @[simps]
attribute automatically derives lemmas specifying the projections of this
declaration.
Example:
@[simps] def foo : ℕ × ℤ := (1, 2)
derives two simp
lemmas:
@[simp] lemma foo_fst : foo.fst = 1
@[simp] lemma foo_snd : foo.snd = 2

It does not derive
simp
lemmas for the propvalued projections. 
It will automatically reduce newly created betaredexes, but will not unfold any definitions.

If the structure has a coercion to either sorts or functions, and this is defined to be one of the projections, then this coercion will be used instead of the projection.

If the structure is a class that has an instance to a notation class, like
has_mul
, then this notation is used instead of the corresponding projection. 
You can specify custom projections, by giving a declaration with name
{structure_name}.simps.{projection_name}
. See Note [custom simps projection].Example:
def equiv.simps.inv_fun (e : α ≃ β) : β → α := e.symm @[simps] def equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ := ⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
generates
@[simp] lemma equiv.trans_to_fun : ∀ {α β γ} (e₁ e₂) (a : α), ⇑(e₁.trans e₂) a = (⇑e₂ ∘ ⇑e₁) a @[simp] lemma equiv.trans_inv_fun : ∀ {α β γ} (e₁ e₂) (a : γ), ⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a

You can specify custom projection names, by specifying the new projection names using
initialize_simps_projections
. Example:initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply)
. Seeinitialize_simps_projections_cmd
for more information. 
If one of the fields itself is a structure, this command will recursively create
simp
lemmas for all fields in that structure. Exception: by default it will not recursively create
simp
lemmas for fields in the structuresprod
andpprod
. You can give explicit projection names or change the value ofsimps_cfg.not_recursive
to override this behavior.
Example:
structure my_prod (α β : Type*) := (fst : α) (snd : β) @[simps] def foo : prod ℕ ℕ × my_prod ℕ ℕ := ⟨⟨1, 2⟩, 3, 4⟩
generates
@[simp] lemma foo_fst : foo.fst = (1, 2) @[simp] lemma foo_snd_fst : foo.snd.fst = 3 @[simp] lemma foo_snd_snd : foo.snd.snd = 4
 Exception: by default it will not recursively create

You can use
@[simps proj1 proj2 ...]
to only generate the projection lemmas for the specified projections. 
Recursive projection names can be specified using
proj1_proj2_proj3
. This will create a lemma of the formfoo.proj1.proj2.proj3 = ...
.Example:
structure my_prod (α β : Type*) := (fst : α) (snd : β) @[simps fst fst_fst snd] def foo : prod ℕ ℕ × my_prod ℕ ℕ := ⟨⟨1, 2⟩, 3, 4⟩
generates
@[simp] lemma foo_fst : foo.fst = (1, 2) @[simp] lemma foo_fst_fst : foo.fst.fst = 1 @[simp] lemma foo_snd : foo.snd = {fst := 3, snd := 4}

If one of the values is an etaexpanded structure, we will etareduce this structure.
Example:
structure equiv_plus_data (α β) extends α ≃ β := (data : bool) @[simps] def bar {α} : equiv_plus_data α α := { data := tt, ..equiv.refl α }
generates the following:
@[simp] lemma bar_to_equiv : ∀ {α : Sort*}, bar.to_equiv = equiv.refl α @[simp] lemma bar_data : ∀ {α : Sort*}, bar.data = tt
This is true, even though Lean inserts an etaexpanded version of
equiv.refl α
in the definition ofbar
. 
For configuration options, see the doc string of
simps_cfg
. 
The precise syntax is
('simps' ident* e)
, wheree
is an expression of typesimps_cfg
. 
@[simps]
reduces letexpressions where necessary. 
When option
trace.simps.verbose
is true,simps
will print the projections it finds and the lemmas it generates. The same can be achieved by using@[simps?]
, except that in this case it will not print projection information. 
Use
@[to_additive, simps]
to apply bothto_additive
andsimps
to a definition, making sure thatsimps
comes afterto_additive
. This will also generate the additive versions of allsimp
lemmas.
Related declarations
Import using
 import tactic.simps
 import tactic.basic
tidy
Tag interactive tactics (locally) with [tidy]
to add them to the list of default tactics
called by tidy
.
Related declarations
Import using
 import tactic.tidy
 import tactic.basic
to_additive
The attribute to_additive
can be used to automatically transport theorems
and definitions (but not inductive types and structures) from a multiplicative
theory to an additive theory.
To use this attribute, just write:
@[to_additive]
theorem mul_comm' {α} [comm_semigroup α] (x y : α) : x * y = y * x := comm_semigroup.mul_comm
This code will generate a theorem named add_comm'
. It is also
possible to manually specify the name of the new declaration, and
provide a documentation string:
@[to_additive add_foo "add_foo doc string"]
/ foo doc string /
theorem foo := sorry
The transport tries to do the right thing in most cases using several heuristics described below. However, in some cases it fails, and requires manual intervention.
If the declaration to be transported has attributes which need to be
copied to the additive version, then to_additive
should come last:
The exception to this rule is the simps
attribute, which should come after to_additive
:
@[to_additive, simps]
instance {M N} [has_mul M] [has_mul N] : has_mul (M × N) := ⟨λ p q, ⟨p.1 * q.1, p.2 * q.2⟩⟩
Implementation notes #
The transport process generally works by taking all the names of
identifiers appearing in the name, type, and body of a declaration and
creating a new declaration by mapping those names to additive versions
using a simple stringbased dictionary and also using all declarations
that have previously been labeled with to_additive
.
In the mul_comm'
example above, to_additive
maps:
mul_comm'
toadd_comm'
,comm_semigroup
toadd_comm_semigroup
,x * y
tox + y
andy * x
toy + x
, andcomm_semigroup.mul_comm'
toadd_comm_semigroup.add_comm'
.
Heuristics #
to_additive
uses heuristics to determine whether a particular identifier has to be
mapped to its additive version. The basic heuristic is
 Only map an identifier to its additive version if its first argument doesn't contain any unapplied identifiers.
Examples:
@has_mul.mul ℕ n m
(i.e.(n * m : ℕ)
) will not change to+
, since its first argument isℕ
, an identifier not applied to any arguments.@has_mul.mul (α × β) x y
will change to+
. It's first argument contains only the identifierprod
, but this is applied to arguments,α
andβ
.@has_mul.mul (α × ℤ) x y
will not change to+
, since its first argument containsℤ
.
The reasoning behind the heuristic is that the first argument is the type which is "additivized", and this usually doesn't make sense if this is on a fixed type.
There are some exceptions to this heuristic:
 Identifiers that have the
@[to_additive]
attribute are ignored. For example, multiplication in↥Semigroup
is replaced by addition in↥AddSemigroup
.  If an identifier
d
has attribute@[to_additive_relevant_arg n]
then the argument in positionn
is checked for a fixed type, instead of checking the first argument.@[to_additive]
will automatically add the attribute@[to_additive_relevant_arg n]
to a declaration when the first argument has no multiplicative typeclass, but argumentn
does.  If an identifier has attribute
@[to_additive_ignore_args n1 n2 ...]
then all the arguments in positionsn1
,n2
, ... will not be checked for unapplied identifiers (start counting from 1). For example,times_cont_mdiff_map
has attribute@[to_additive_ignore_args 21]
, which means that its 21st argument(n : with_top ℕ)
can containℕ
(usually in the formhas_top.top ℕ ...
) and still be additivized. So@has_mul.mul (C^∞⟮I, N; I', G⟯) _ f g
will be additivized.
Troubleshooting #
If @[to_additive]
fails because the additive declaration raises a type mismatch, there are
various things you can try.
The first thing to do is to figure out what @[to_additive]
did wrong by looking at the type
mismatch error.
 Option 1: It additivized a declaration
d
that should remain multiplicative. Solution: Make sure the first argument of
d
is a type with a multiplicative structure. If not, can you reorder the (implicit) arguments ofd
so that the first argument becomes a type with a multiplicative structure (and not some indexing type)? The reason is that@[to_additive]
doesn't additivize declarations if their first argument contains fixed types likeℕ
orℝ
. See section Heuristics. If the first argument is not the argument with a multiplicative typeclass,@[to_additive]
should have automatically added the attribute@[to_additive_relevant_arg]
to the declaration. You can test this by running the following (whered
is the full name of the declaration):The expected output isrun_cmd to_additive.relevant_arg_attr.get_param `d >>= tactic.trace
n
where then
th argument ofd
is a type (family) with a multiplicative structure on it. If you get a different output (or a failure), you could add the attribute@[to_additive_relevant_arg n]
manually, wheren
is an argument with a multiplicative structure.
 Make sure the first argument of
 Option 2: It didn't additivize a declaration that should be additivized.
This happened because the heuristic applied, and the first argument contains a fixed type,
like
ℕ
orℝ
. Solutions: If the fixed type has an additive counterpart (like
↥Semigroup
), give it the@[to_additive]
attribute.  If the fixed type occurs inside the
k
th argument of a declarationd
, and thek
th argument is not connected to the multiplicative structure ond
, consider adding attribute[to_additive_ignore_args k]
tod
.  If you want to disable the heuristic and replace all multiplicative
identifiers with their additive counterpart, use
@[to_additive!]
.
 If the fixed type has an additive counterpart (like
 Option 3: Arguments / universe levels are incorrectly ordered in the additive version.
This likely only happens when the multiplicative declaration involves
pow
/^
. Solutions: Ensure that the order of arguments of all relevant declarations are the same for the
multiplicative and additive version. This might mean that arguments have an "unnatural" order
(e.g.
monoid.npow n x
corresponds tox ^ n
, but it is convenient thatmonoid.npow
has this argument order, since it matchesadd_monoid.nsmul n x
.  If this is not possible, add the
[to_additive_reorder k]
to the multiplicative declaration to indicate that thek
th and(k+1)
st arguments are reordered in the additive version.
 Ensure that the order of arguments of all relevant declarations are the same for the
multiplicative and additive version. This might mean that arguments have an "unnatural" order
(e.g.
If neither of these solutions work, and to_additive
is unable to automatically generate the
additive version of a declaration, manually write and prove the additive version.
Often the proof of a lemma/theorem can just be the multiplicative version of the lemma applied to
multiplicative G
.
Afterwards, apply the attribute manually:
attribute [to_additive foo_add_bar] foo_bar
This will allow future uses of to_additive
to recognize that
foo_bar
should be replaced with foo_add_bar
.
Handling of hidden definitions #
Before transporting the “main” declaration src
, to_additive
first
scans its type and value for names starting with src
, and transports
them. This includes auxiliary definitions like src._match_1
,
src._proof_1
.
After transporting the “main” declaration, to_additive
transports
its equational lemmas.
Structure fields and constructors #
If src
is a structure, then to_additive
automatically adds
structure fields to its mapping, and similarly for constructors of
inductive types.
For new structures this means that to_additive
automatically handles
coercions, and for old structures it does the same, if ancestry
information is present in @[ancestor]
attributes. The ancestor
attribute must come before the to_additive
attribute, and it is
essential that the order of the base structures passed to ancestor
matches
between the multiplicative and additive versions of the structure.
Name generation #

If
@[to_additive]
is called without aname
argument, then the new name is autogenerated. First, it takes the longest prefix of the source name that is already known toto_additive
, and replaces this prefix with its additive counterpart. Second, it takes the last part of the name (i.e., after the last dot), and replaces common name parts (“mul”, “one”, “inv”, “prod”) with their additive versions. 
Namespaces can be transformed using
map_namespace
. For example:run_cmd to_additive.map_namespace `quotient_group `quotient_add_group
Later uses of
to_additive
on declarations in thequotient_group
namespace will be created in thequotient_add_group
namespaces. 
If
@[to_additive]
is called with aname
argumentnew_name
/without a dot/, thento_additive
updates the prefix as described above, then replaces the last part of the name withnew_name
. 
If
@[to_additive]
is called with aname
argumentnew_namespace.new_name
/with a dot/, thento_additive
uses this new name as is.
As a safety check, in the first case to_additive
double checks
that the new name differs from the original one.
Related declarations
Import using
 import algebra.group.to_additive
 import tactic.basic
zify
The zify
attribute is used by the zify
tactic. It applies to lemmas that shift propositions
between nat
and int
.
zify
lemmas should have the form ∀ a₁ ... aₙ : ℕ, Pz (a₁ : ℤ) ... (aₙ : ℤ) ↔ Pn a₁ ... aₙ
.
For example, int.coe_nat_le_coe_nat_iff : ∀ (m n : ℕ), ↑m ≤ ↑n ↔ m ≤ n
is a zify
lemma.
Related declarations
Import using
 import tactic.zify
 import tactic