Commands
Commands provide a way to interact with and modify a Lean environment outside of the context of a proof.
Familiar commands from core Lean include #check
, #eval
, and run_cmd
.
Mathlib provides a number of commands that offer customized behavior. These commands fall into two categories:
-
Transient commands are used to query the environment for information, but do not modify it, and have no effect on the following proofs. These are useful as a user to get information from Lean. They should not appear in "finished" files. Transient commands typically begin with the symbol
#
.#check
is a standard example of a transient command. -
Permanent commands modify the environment. Removing a permanent command from a file may affect the following proofs.
set_option class.instance_max_depth 500
is a standard example of a permanent command.
User-defined commands can have unintuitive interactions with the parser. For the most part, this is
not something to worry about. However, you may occasionally see strange error messages when using
mathlib commands: for instance, running these commands immediately after import file.name
will
produce an error. An easy solution is to run a built-in no-op command in between, for example:
import data.nat.basic
run_cmd tactic.skip -- this serves as a "barrier" between `import` and `#find`
#find _ + _ = _ + _
#find
The find
command from tactic.find
allows to find definitions lemmas using
pattern matching on the type. For instance:
import tactic.find
run_cmd tactic.skip
#find _ + _ = _ + _
#find (_ : ℕ) + _ = _ + _
#find ℕ → ℕ
The tactic library_search
is an alternate way to find lemmas in the library.
Related declarations
Import using
- import tactic.find
- import tactic.basic
#norm_num
The basic usage is #norm_num e
, where e
is an expression,
which will print the norm_num
form of e
.
Syntax: #norm_num
(only
)? ([
simp lemma list ]
)? (with
simp sets)? :
? expression
This accepts the same options as the #simp
command.
You can specify additional simp lemmas as usual, for example using
#norm_num [f, g] : e
, or #norm_num with attr : e
.
(The colon is optional but helpful for the parser.)
The only
restricts norm_num
to using only the provided lemmas, and so
#norm_num only : e
behaves similarly to norm_num1
.
Unlike norm_num
, this command does not fail when no simplifications are made.
#norm_num
understands local variables, so you can use them to
introduce parameters.
Related declarations
Import using
- import tactic.norm_num
- import tactic
#simp
The basic usage is #simp e
, where e
is an expression,
which will print the simplified form of e
.
You can specify additional simp lemmas as usual for example using
#simp [f, g] : e
, or #simp with attr : e
.
(The colon is optional, but helpful for the parser.)
#simp
understands local variables, so you can use them to
introduce parameters.
Related declarations
Import using
- import tactic.simp_command
- import tactic.basic
#where
When working in a Lean file with namespaces, parameters, and variables, it can be confusing to
identify what the current "parser context" is. The command #where
identifies and prints
information about the current location, including the active namespace, open namespaces, and
declared variables.
It is a bug for #where
to incorrectly report this information (this was not formerly the case);
please file an issue on GitHub if you observe a failure.
Related declarations
Import using
- import tactic.where
- import tactic.basic
add_decl_doc
The add_decl_doc
command is used to add a doc string to an existing declaration.
def foo := 5
/--
Doc string for foo.
-/
add_decl_doc foo
```
Related declarations
Import using
- import tactic.doc_commands
- import tactic.basic
add_hint_tactic
add_hint_tactic t
runs the tactic t
whenever hint
is invoked.
The typical use case is add_hint_tactic "foo"
for some interactive tactic foo
.
Related declarations
Import using
- import tactic.hint
- import tactic.basic
add_tactic_doc
A command used to add documentation for a tactic, command, hole command, or attribute.
Usage: after defining an interactive tactic, command, or attribute, add its documentation as follows.
/--
describe what the command does here
-/
add_tactic_doc
{ name := "display name of the tactic",
category := cat,
decl_names := [`dcl_1, `dcl_2],
tags := ["tag_1", "tag_2"] }
The argument to add_tactic_doc
is a structure of type tactic_doc_entry
.
name
refers to the display name of the tactic; it is used as the header of the doc entry.cat
refers to the category of doc entry. Options:doc_category.tactic
,doc_category.cmd
,doc_category.hole_cmd
,doc_category.attr
decl_names
is a list of the declarations associated with this doc. For instance, the entry forlinarith
would setdecl_names := [`tactic.interactive.linarith]
. Some entries may cover multiple declarations. It is only necessary to list the interactive versions of tactics.tags
is an optional list of strings used to categorize entries.- The doc string is the body of the entry. It can be formatted with markdown.
What you are reading now is the description of
add_tactic_doc
.
If only one related declaration is listed in decl_names
and if this
invocation of add_tactic_doc
does not have a doc string, the doc string of
that declaration will become the body of the tactic doc entry. If there are
multiple declarations, you can select the one to be used by passing a name to
the inherit_description_from
field.
If you prefer a tactic to have a doc string that is different then the doc entry,
you should write the doc entry as a doc string for the add_tactic_doc
invocation.
Note that providing a badly formed tactic_doc_entry
to the command can result in strange error
messages.
Related declarations
Import using
- import tactic.doc_commands
- import tactic.basic
alias
The alias
command can be used to create copies
of a theorem or definition with different names.
Syntax:
/-- doc string -/
alias my_theorem ← alias1 alias2 ...
This produces defs or theorems of the form:
/-- doc string -/
@[alias] theorem alias1 : <type of my_theorem> := my_theorem
/-- doc string -/
@[alias] theorem alias2 : <type of my_theorem> := my_theorem
Iff alias syntax:
alias A_iff_B ↔ B_of_A A_of_B
alias A_iff_B ↔ ..
This gets an existing biconditional theorem A_iff_B
and produces
the one-way implications B_of_A
and A_of_B
(with no change in
implicit arguments). A blank _
can be used to avoid generating one direction.
The ..
notation attempts to generate the 'of'-names automatically when the
input theorem has the form A_iff_B
or A_iff_B_left
etc.
Related declarations
Import using
- import tactic.alias
- import tactic.basic
copy_doc_string
copy_doc_string source → target_1 target_2 ... target_n
copies the doc string of the
declaration named source
to each of target_1
, target_2
, ..., target_n
.
Related declarations
Import using
- import tactic.doc_commands
- import tactic.basic
def_replacer
def_replacer foo
sets up a stub definition foo : tactic unit
, which can
effectively be defined and re-defined later, by tagging definitions with @[foo]
.
@[foo] meta def foo_1 : tactic unit := ...
replaces the current definition offoo
.@[foo] meta def foo_2 (old : tactic unit) : tactic unit := ...
replaces the current definition offoo
, and provides access to the previous definition viaold
. (The argument can also be anoption (tactic unit)
, which is provided asnone
if this is the first definition tagged with@[foo]
sincedef_replacer
was invoked.)
def_replacer foo : α → β → tactic γ
allows the specification of a replacer with
custom input and output types. In this case all subsequent redefinitions must have the
same type, or the type α → β → tactic γ → tactic γ
or
α → β → option (tactic γ) → tactic γ
analogously to the previous cases.
Related declarations
Import using
- import tactic.replacer
- import tactic.basic
import_private
import_private foo from bar
finds a private declaration foo
in the same file as bar
and creates a local notation to refer to it.
import_private foo
looks for foo
in all imported files.
When possible, make foo
non-private rather than using this feature.
Related declarations
Import using
- import tactic.core
- import tactic.basic
initialize_simps_projections
This command specifies custom names and custom projections for the simp attribute simps_attr
.
- You can specify custom names by writing e.g.
initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply)
. - See Note [custom simps projection] and the examples below for information how to declare custom projections.
- If no custom projection is specified, the projection will be
coe_fn
/⇑
if ahas_coe_to_fun
instance has been declared, or the notation of a notation class (likehas_mul
) if such an instance is available. If none of these cases apply, the projection itself will be used. - You can disable a projection by default by running
initialize_simps_projections equiv (-inv_fun)
This will ensure that no simp lemmas are generated for this projection, unless this projection is explicitly specified by the user. - If you want the projection name added as a prefix in the generated lemma name, you can add the
as_prefix
modifier:initialize_simps_projections equiv (to_fun → coe as_prefix)
Note that this does not influence the parsing of projection names: if you have a declarationfoo
and you want to apply the projectionssnd
,coe
(which is a prefix) andfst
, in that order you can run@[simps snd_coe_fst] def foo ...
and this will generate a lemma with the namecoe_foo_snd_fst
.- Run
initialize_simps_projections?
(orset_option trace.simps.verbose true
) to see the generated projections.
- Run
- You can declare a new name for a projection that is the composite of multiple projections, e.g.
You can also make your custom projection that is definitionally equal to a composite of projections. In this case, coercions and notation classes are not automatically recognized, and should be manually given by giving a custom projection. This is especially useful when extending a structure (without
structure A := (proj : ℕ) structure B extends A initialize_simps_projections? B (to_A_proj → proj, -to_A)
old_structure_cmd
). In the above example, it is desirable to add-to_A
, so that@[simps]
doesn't automatically apply theB.to_A
projection and then recursively theA.proj
projection in the lemmas it generates. If you want to get both thefoo_proj
andfoo_to_A
simp lemmas, you can use@[simps, simps to_A]
. - Running
initialize_simps_projections my_struc
without arguments is not necessary, it has the same effect if you just add@[simps]
to a declaration. - If you do anything to change the default projections, make sure to call either
@[simps]
orinitialize_simps_projections
in the same file as the structure declaration. Otherwise, you might have a file that imports the structure, but not your custom projections.
Some common uses:
- If you define a new homomorphism-like structure (like
mul_hom
) you can just runinitialize_simps_projections
after defining thehas_coe_to_fun
instanceThis will generateinstance {mM : has_mul M} {mN : has_mul N} : has_coe_to_fun (M →ₙ* N) := ... initialize_simps_projections mul_hom (to_fun → apply)
foo_apply
lemmas for each declarationfoo
. - If you prefer
coe_foo
lemmas that state equalities between functions, useinitialize_simps_projections mul_hom (to_fun → coe as_prefix)
In this case you have to use@[simps {fully_applied := ff}]
or equivalently@[simps as_fn]
whenever you call@[simps]
. - You can also initialize to use both, in which case you have to choose which one to use by default,
by using either of the following
In the first case, you can get both lemmas using
initialize_simps_projections mul_hom (to_fun → apply, to_fun → coe, -coe as_prefix) initialize_simps_projections mul_hom (to_fun → apply, to_fun → coe as_prefix, -apply)
@[simps, simps coe as_fn]
and in the second case you can get both lemmas using@[simps as_fn, simps apply]
. - If your new homomorphism-like structure extends another structure (without
old_structure_cmd
) (likerel_embedding
), then you have to specify explicitly that you want to use a coercion as a custom projection. For exampledef rel_embedding.simps.apply (h : r ↪r s) : α → β := h initialize_simps_projections rel_embedding (to_embedding_to_fun → apply, -to_embedding)
- If you have an isomorphism-like structure (like
equiv
) you often want to define a custom projection for the inverse:def equiv.simps.symm_apply (e : α ≃ β) : β → α := e.symm initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply)
Related declarations
Import using
- import tactic.simps
- import tactic.basic
library_note
At various places in mathlib, we leave implementation notes that are referenced from many other
files. To keep track of these notes, we use the command library_note
. This makes it easy to
retrieve a list of all notes, e.g. for documentation output.
These notes can be referenced in mathlib with the syntax Note [note id]
.
Often, these references will be made in code comments (--
) that won't be displayed in docs.
If such a reference is made in a doc string or module doc, it will be linked to the corresponding
note in the doc display.
Syntax:
/--
note message
-/
library_note "note id"
An example from meta.expr
:
/--
Some declarations work with open expressions, i.e. an expr that has free variables.
Terms will free variables are not well-typed, and one should not use them in tactics like
`infer_type` or `unify`. You can still do syntactic analysis/manipulation on them.
The reason for working with open types is for performance: instantiating variables requires
iterating through the expression. In one performance test `pi_binders` was more than 6x
quicker than `mk_local_pis` (when applied to the type of all imported declarations 100x).
-/
library_note "open expressions"
This note can be referenced near a usage of pi_binders
:
-- See Note [open expressions]
/-- behavior of f -/
def f := pi_binders ...
Related declarations
Import using
- import tactic.doc_commands
- import tactic.basic
linting commands
User commands to spot common mistakes in the code
#lint
: check all declarations in the current file#lint_mathlib
: check all declarations in mathlib (so excluding core or other projects, and also excluding the current file)#lint_all
: check all declarations in the environment (the current file and all imported files)
The following linters are run by default:
unused_arguments
checks for unused arguments in declarations.def_lemma
checks whether a declaration is incorrectly marked as a def/lemma.dup_namespce
checks whether a namespace is duplicated in the name of a declaration.ge_or_gt
checks whether ≥/> is used in the declaration.instance_priority
checks that instances that always apply have priority below default.doc_blame
checks for missing doc strings on definitions and constants.has_inhabited_instance
checks whether every type has an associatedinhabited
instance.impossible_instance
checks for instances that can never fire.incorrect_type_class_argument
checks for arguments in [square brackets] that are not classes.dangerous_instance
checks for instances that generate type-class problems with metavariables.fails_quickly
tests that type-class inference ends (relatively) quickly when applied to variables.has_coe_variable
tests that there are no instances of typehas_coe α t
for a variableα
.inhabited_nonempty
checks forinhabited
instance arguments that should be changed tononempty
.simp_nf
checks that the left-hand side of simp lemmas is in simp-normal form.simp_var_head
checks that there are no variables as head symbol of left-hand sides of simp lemmas.simp_comm
checks that no commutativity lemmas (such asadd_comm
) are marked simp.decidable_classical
checks fordecidable
hypotheses that are used in the proof of a proposition but not in the statement, and could be removed usingclassical
. Theorems in thedecidable
namespace are exempt.has_coe_to_fun
checks that every type that coerces to a function has a directhas_coe_to_fun
instance.check_type
checks that the statement of a declaration is well-typed.check_univs
checks that there are no badmax u v
universe levels.syn_taut
checks that declarations are not syntactic tautologies.check_reducibility
checks whether non-instances with a class as type are reducible.unprintable_interactive
checks that interactive tactics have parser documentation.to_additive_doc
checks if additive versions of lemmas have documentation
Another linter, doc_blame_thm
, checks for missing doc strings on lemmas and theorems.
This is not run by default.
The command #list_linters
prints a list of the names of all available linters.
You can append a *
to any command (e.g. #lint_mathlib*
) to omit the slow tests (4).
You can append a -
to any command (e.g. #lint_mathlib-
) to run a silent lint
that suppresses the output if all checks pass.
A silent lint will fail if any test fails.
You can append a +
to any command (e.g. #lint_mathlib+
) to run a verbose lint
that reports the result of each linter, including the successes.
You can append a sequence of linter names to any command to run extra tests, in addition to the
default ones. e.g. #lint doc_blame_thm
will run all default tests and doc_blame_thm
.
You can append only name1 name2 ...
to any command to run a subset of linters, e.g.
#lint only unused_arguments
You can add custom linters by defining a term of type linter
in the linter
namespace.
A linter defined with the name linter.my_new_check
can be run with #lint my_new_check
or lint only my_new_check
.
If you add the attribute @[linter]
to linter.my_new_check
it will run by default.
Adding the attribute @[nolint doc_blame unused_arguments]
to a declaration
omits it from only the specified linter checks.
Related declarations
Import using
- import tactic.lint.frontend
- import tactic.basic
localized notation
This consists of two user-commands which allow you to declare notation and commands localized to a locale.
- Declare notation which is localized to a locale using:
localized "infix ` ⊹ `:60 := my_add" in my.add
-
After this command it will be available in the same section/namespace/file, just as if you wrote
local infix
⊹:60 := my_add
-
You can open it in other places. The following command will declare the notation again as local notation in that section/namespace/file:
open_locale my.add
- More generally, the following will declare all localized notation in the specified locales.
open_locale locale1 locale2 ...
- You can also declare other localized commands, like local attributes
localized "attribute [simp] le_refl" in le
- To see all localized commands in a given locale, run:
run_cmd print_localized_commands [`my.add].
- To see a list of all locales with localized commands, run:
run_cmd do
m ← localized_attr.get_cache,
tactic.trace m.keys -- change to `tactic.trace m.to_list` to list all the commands in each locale
- Warning: You have to give full names of all declarations used in localized notation, so that the localized notation also works when the appropriate namespaces are not opened.
Related declarations
Import using
- import tactic.localized
- import tactic.basic
mk_iff_of_inductive_prop
mk_iff_of_inductive_prop i r
makes an iff
rule for the inductively-defined proposition i
.
The new rule r
has 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, mk_iff_of_inductive_prop
on list.chain
produces:
∀ {α : Type*} (R : α → α → Prop) (a : α) (l : list α),
chain R a l ↔ l = [] ∨ ∃{b : α} {l' : list α}, R a b ∧ chain R b l ∧ l = b :: l'
See also the mk_iff
user attribute.
Related declarations
Import using
- import tactic.mk_iff_of_inductive_prop
- import tactic.basic
mk_simp_attribute
The command mk_simp_attribute simp_name "description"
creates a simp set with name simp_name
.
Lemmas tagged with @[simp_name]
will be included when simp with simp_name
is called.
mk_simp_attribute simp_name none
will use a default description.
Appending the command with with attr1 attr2 ...
will include all declarations tagged with
attr1
, attr2
, ... in the new simp set.
This command is preferred to using run_cmd mk_simp_attr `simp_name
since it adds a doc string
to the attribute that is defined. If you need to create a simp set in a file where this command is
not available, you should use
run_cmd mk_simp_attr `simp_name
run_cmd add_doc_string `simp_attr.simp_name "Description of the simp set here"
Related declarations
Import using
- import tactic.core
- import tactic.basic
reassoc_axiom
When declaring a class of categories, the axioms can be reformulated to be more amenable to manipulation in right associated expressions:
class some_class (C : Type) [category C] :=
(foo : Π X : C, X ⟶ X)
(bar : ∀ {X Y : C} (f : X ⟶ Y), foo X ≫ f = f ≫ foo Y)
reassoc_axiom some_class.bar
The above will produce:
lemma some_class.bar_assoc {Z : C} (g : Y ⟶ Z) :
foo X ≫ f ≫ g = f ≫ foo Y ≫ g := ...
Here too, the reassoc
attribute can be used instead. It works well when combined with
simp
:
attribute [simp, reassoc] some_class.bar
Related declarations
Import using
- import tactic.reassoc_axiom
- import tactic
restate_axiom
restate_axiom
makes a new copy of a structure field, first definitionally simplifying the type.
This is useful to remove auto_param
or opt_param
from the statement.
As an example, we have:
structure A :=
(x : ℕ)
(a' : x = 1 . skip)
example (z : A) : z.x = 1 := by rw A.a' -- rewrite tactic failed, lemma is not an equality nor a iff
restate_axiom A.a'
example (z : A) : z.x = 1 := by rw A.a
By default, restate_axiom
names the new lemma by removing a trailing '
, or otherwise appending
_lemma
if there is no trailing '
. You can also give restate_axiom
a second argument to
specify the new name, as in
restate_axiom A.a f
example (z : A) : z.x = 1 := by rw A.f
Related declarations
Import using
- import tactic.restate_axiom
- import tactic.basic
run_parser
run_parser p
is like run_cmd
but for the parser monad. It executes parser p
at the
top level, giving access to operations like emit_code_here
.
Related declarations
Import using
- import tactic.core
- import tactic.basic
setup_tactic_parser
setup_tactic_parser
is a user command that opens the namespaces used in writing
interactive tactics, and declares the local postfix notation ?
for optional
and *
for many
.
It does not use the namespace
command, so it will typically be used after
namespace tactic.interactive
.
Related declarations
Import using
- import tactic.core
- import tactic.basic