Attributes - mathlib docs

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.

Tags:

transport
environment

Related declarations

tactic.ancestor_attr

Import using

import tactic.algebra
import tactic.basic

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.

attribute [ext thunk, ext stream] funext

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

Tags:

rewrite
logic

Related declarations

extensional_attribute

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 higher-order functions.

Tags:

lemma derivation

Related declarations

tactic.higher_order_attr

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.

Tags:

rewrite
search

Related declarations

tactic.hint.hint_tactic_attribute

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]
```

Tags:

environment

Related declarations

tactic.interactive_attr

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.

Tags:

linting

Related declarations

linter_attr

Import using

import tactic.lint.basic
import tactic.basic

mk_iff

Applying the mk_iff attribute to an inductively-defined 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.

Tags:

logic
environment

Related declarations

mk_iff_attr

Import using

import tactic.mk_iff_of_inductive_prop
import tactic.basic

nolint

Defines the user attribute nolint for skipping #lint

Tags:

linting

Related declarations

nolint_attr

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://lean-forward.github.io/norm_cast/norm_cast.pdf.

Tags:

coercions
simplification

Related declarations

norm_cast.norm_cast_attr

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 non-applicability 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.

Tags:

arithmetic
decision_procedure

Related declarations

norm_num.attr

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.

@[protect_proj without baz bar] structure foo : Type :=
(bar : unit) (baz : unit) (qux : unit)

Tags:

parsing
environment
structures

Related declarations

tactic.protect_proj_attr

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.

Tags:

parsing
environment

Related declarations

tactic.protected_attr

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.

Tags:

category theory

Related declarations

tactic.reassoc_attr

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 prop-valued projections.
It will automatically reduce newly created beta-redexes, 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). See initialize_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 structures prod and pprod. You can give explicit projection names or change the value of simps_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
```
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 form foo.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 eta-expanded structure, we will eta-reduce 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 eta-expanded version of equiv.refl α in the definition of bar.

For configuration options, see the doc string of simps_cfg.
The precise syntax is ('simps' ident* e), where e is an expression of type simps_cfg.
@[simps] reduces let-expressions 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 both to_additive and simps to a definition, making sure that simps comes after to_additive. This will also generate the additive versions of all simp lemmas.

Tags:

simplification

Related declarations

simps_attr

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.

Tags:

search

Related declarations

tactic.tidy.tidy_attribute

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:

@[simp, to_additive] lemma mul_one' {G : Type*} [group G] (x : G) : x * 1 = x := mul_one x

The following attributes are supported and should be applied correctly by to_additive to the new additivized declaration, if they were present on the original one:

reducible, _refl_lemma, simp, norm_cast, instance, refl, symm, trans, elab_as_eliminator, no_rsimp,
continuity, ext, ematch, measurability, alias, _ext_core, _ext_lemma_core, nolint

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⟩⟩

Additionally the mono attribute is not handled by to_additive and should be applied afterwards to both the original and additivized lemma.

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 string-based 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' to add_comm',
comm_semigroup to add_comm_semigroup,
x * y to x + y and y * x to y + x, and
comm_semigroup.mul_comm' to add_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 identifier prod, 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 position n 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 type-class, but argument n does.
If an identifier has attribute @[to_additive_ignore_args n1 n2 ...] then all the arguments in positions n1, 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 form has_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 of d 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 type-class, @[to_additive] should have automatically added the attribute @[to_additive_relevant_arg] to the declaration. You can test this by running the following (where d is the full name of the declaration):
```
  run_cmd to_additive.relevant_arg_attr.get_param `d >>= tactic.trace
```
  The expected output is n where the n-th argument of d 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, where n is an argument with a multiplicative structure.
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 declaration d, and the k-th argument is not connected to the multiplicative structure on d, consider adding attribute [to_additive_ignore_args k] to d.
- If you want to disable the heuristic and replace all multiplicative identifiers with their additive counterpart, use @[to_additive!].
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 to x ^ n, but it is convenient that monoid.npow has this argument order, since it matches add_monoid.nsmul n x.
- If this is not possible, add the [to_additive_reorder k] to the multiplicative declaration to indicate that the k-th and (k+1)-st arguments are reordered in the additive version.

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.

In addition to transporting the “main” declaration, to_additive transports its equational lemmas and tags them as equational lemmas for the new declaration, attributes present on the original equational lemmas are also transferred first (notably _refl_lemma).

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 a name argument, then the new name is autogenerated. First, it takes the longest prefix of the source name that is already known to to_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 the quotient_group namespace will be created in the quotient_add_group namespaces.
If @[to_additive] is called with a name argument new_name /without a dot/, then to_additive updates the prefix as described above, then replaces the last part of the name with new_name.
If @[to_additive] is called with a name argument new_namespace.new_name /with a dot/, then to_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.

Tags:

transport
environment
lemma derivation

Related declarations

to_additive.attr

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.

Tags:

coercions
transport

Related declarations

zify.zify_attr

Import using

import tactic.zify
import tactic