mathlib documentation

Attributes

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 core.init.meta.attribute.

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,stream]] funext

Those parameters are cumulative. The following are equivalent:

attribute [ext [(),thunk]] funext
attribute [ext [stream]] funext

and

attribute [ext [(),thunk,stream]] funext

One removes type names from the list for one lemma with:

attribute [ext [-stream,-thunk]] 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 *]
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 [*,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
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
Import using
  • import tactic.core
  • 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
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
Import using
  • import tactic.lint.basic
  • import tactic.basic

nolint

Defines the user attribute nolint for skipping #lint

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

Tags:
  • coercions
  • simplification
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 exprtactic (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
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
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
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
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).

  • 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. Give explicit projection names 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, even though Lean inserts an eta-expanded version of equiv.refl α in the definition of bar:

    @[simp] lemma bar_to_equiv :  {α : Sort u_1}, bar.to_equiv = equiv.refl α
    @[simp] lemma bar_data :  {α : Sort u_1}, bar.data = tt
    
  • 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.
  • If one of the fields is a partially applied constructor, we will eta-expand it (this likely never happens).
  • When option trace.simps.verbose is true, simps will print the projections it finds and the lemmas it generates.

Tags:
  • simplification
Related declarations
Import using
  • import tactic.simps
  • 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

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'.

Even when to_additive is unable to automatically generate the additive version of a declaration, it can be useful to 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.

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 two cases to_additive double checks that the new name differs from the original one.

Tags:
  • transport
  • environment
  • lemma derivation
Related declarations
Import using
  • import algebra.group.to_additive
  • import tactic

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
Import using
  • import tactic.zify
  • import tactic