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 _ + _ = _ + _

#explode

#explode decl_name displays a proof term in a line-by-line format somewhat akin to a Fitch-style proof or the Metamath proof style.

#explode iff_true_intro produces

iff_true_intro : ∀ {a : Prop}, a → (a ↔ true)
0│   │ a         ├ Prop
1│   │ h         ├ a
2│   │ hl        │ ┌ a
3│   │ trivial   │ │ true
4│2,3│ ∀I        │ a → true
5│   │ hr        │ ┌ true
6│5,1│ ∀I        │ true → a
7│4,6│ iff.intro │ a ↔ true
8│1,7│ ∀I        │ a → (a ↔ true)
9│0,8│ ∀I        │ ∀ {a : Prop}, a → (a ↔ true)

In more detail:

The output of #explode is a Fitch-style proof in a four-column diagram modeled after Metamath proof displays like this. The headers of the columns are "Step", "Hyp", "Ref", "Type" (or "Expression" in the case of Metamath):

Step: An increasing sequence of numbers to number each step in the proof, used in the Hyp field.
Hyp: The direct children of the current step. Most theorems are implications like A -> B -> C, and so on the step proving C the Hyp field will refer to the steps that prove A and B.
Ref: The name of the theorem being applied. This is well-defined in Metamath, but in Lean there are some special steps that may have long names because the structure of proof terms doesn't exactly match this mold.
- If the theorem is foo (x y : Z) : A x -> B y -> C x y:
- the Ref field will contain foo,
- x and y will be suppressed, because term construction is not interesting, and
- the Hyp field will reference steps proving A x and B y. This corresponds to a proof term like @foo x y pA pB where pA and pB are subproofs.
- If the head of the proof term is a local constant or lambda, then in this case the Ref will say ∀E for forall-elimination. This happens when you have for example h : A -> B and ha : A and prove b by h ha; we reinterpret this as if it said ∀E h ha where ∀E is (n-ary) modus ponens.
- If the proof term is a lambda, we will also use ∀I for forall-introduction, referencing the body of the lambda. The indentation level will increase, and a bracket will surround the proof of the body of the lambda, starting at a proof step labeled with the name of the lambda variable and its type, and ending with the ∀I step. Metamath doesn't have steps like this, but the style is based on Fitch proofs in first-order logic.
Type: This contains the type of the proof term, the theorem being proven at the current step. This proof layout differs from #print in using lots of intermediate step displays so that you can follow along and don't have to see term construction steps because they are implicitly in the intermediate step displays.

Also, it is common for a Lean theorem to begin with a sequence of lambdas introducing local constants of the theorem. In order to minimize the indentation level, the ∀I steps at the end of the proof will be introduced in a group and the indentation will stay fixed. (The indentation brackets are only needed in order to delimit the scope of assumptions, and these assumptions have global scope anyway so detailed tracking is not necessary.)

Tags:

proof display

Related declarations

tactic.explode_cmd

Import using

import tactic.explode
import tactic.basic

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

Tags:

Related declarations

find_cmd

Import using

import tactic.find
import tactic.basic

#html

Accepts terms with the type component tactic_state string or html empty and renders them interactively. Requires a compatible version of the vscode extension to view the resulting widget.

Example:

/-- A simple counter that can be incremented or decremented with some buttons. -/
meta def counter_widget {π α : Type} : component π α :=
component.ignore_props $ component.mk_simple int int 0 (λ _ x y, (x + y, none)) (λ _ s,
  h "div" [] [
    button "+" (1 : int),
    html.of_string $ to_string $ s,
    button "-" (-1)
  ]
)

#html counter_widget

Tags:

core
widgets

Related declarations

show_widget_cmd

Import using

imported by default

#list_unused_decls

The command #list_unused_decls lists the declarations that that are not used the main features of the present file. The main features of a file are taken as the declaration tagged with @[main_declaration].

A list of files can be given to #list_unused_decls as follows:

#list_unused_decls ["src/tactic/core.lean","src/tactic/interactive.lean"]

They are given in a list that contains file names written as Lean strings. With a list of files, the declarations from all those files in addition to the declarations above #list_unused_decls in the current file will be considered and their interdependencies will be analyzed to see which declarations are unused by declarations marked as @[main_declaration]. The files listed must be imported by the current file. The path of the file names is expected to be relative to the root of the project (i.e. the location of leanpkg.toml when it is present).

Neither #list_unused_decls nor @[main_declaration] should appear in a finished mathlib development.

Tags:

debugging

Related declarations

tactic.unused_decls_cmd

Import using

import tactic.find_unused

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

Tags:

simplification

Related declarations

tactic.simp_cmd

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.

Tags:

environment

Related declarations

where.where_cmd

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

Tags:

documentation

Related declarations

add_decl_doc_command

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.

Tags:

Related declarations

tactic.hint.add_hint_tactic

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 for linarith would set decl_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.

Tags:

documentation

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.

Tags:

renaming

Related declarations

tactic.alias.alias_cmd

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.

Tags:

documentation

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 of foo.
@[foo] meta def foo_2 (old : tactic unit) : tactic unit := ... replaces the current definition of foo, and provides access to the previous definition via old. (The argument can also be an option (tactic unit), which is provided as none if this is the first definition tagged with @[foo] since def_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.

Tags:

environment
renaming

Related declarations

tactic.def_replacer_cmd

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.

Tags:

renaming

Related declarations

tactic.import_private_cmd

Import using

import tactic.core
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 ...

Tags:

documentation

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 associated inhabited 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 type has_coe α t for a variable α.
inhabited_nonempty checks for inhabited instance arguments that should be changed to nonempty.
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 as add_comm) are marked simp.
decidable_classical checks for decidable hypotheses that are used in the proof of a proposition but not in the statement, and could be removed using classical. Theorems in the decidable namespace are exempt.
has_coe_to_fun checks that every type that coerces to a function has a direct has_coe_to_fun instance.

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.

Tags:

linting

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

Declare notation which is localized to a namespace 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/files:
```
open_locale my.add
```
More generally, the following will declare all localized notation in the specified namespaces.
```
open_locale namespace1 namespace2 ...
```
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 namespace, run:
```
run_cmd print_localized_commands [`my.add].
```

To see a list of all namespaces 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 namespace

Warning 1: as a limitation on user commands, you cannot put open_locale directly after your imports. You have to write another command first (e.g. open, namespace, universe variables, noncomputable theory, run_cmd tactic.skip, ...).
Warning 2: You have to fully specify the names used in localized notation, so that the localized notation also works when the appropriate namespaces are not opened.

Tags:

notation
type classes

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 constructors, 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'

Tags:

logic
environment

Related declarations

mk_iff_of_inductive_prop_cmd

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"

Tags:

simplification

Related declarations

tactic.mk_simp_attribute_cmd

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

Tags:

category theory

Related declarations

tactic.reassoc_cmd

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

Tags:

renaming
environment

Related declarations

restate_axiom_cmd

Import using

import tactic.restate_axiom
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.

Tags:

parsing
notation

Related declarations

tactic.setup_tactic_parser_cmd

Import using

import tactic.core
import tactic.basic

mathlib documentation

Commands

Commands

#explode

#find

#html

Example:

#list_unused_decls

#simp

#where

add_decl_doc

add_hint_tactic

add_tactic_doc

alias

copy_doc_string

def_replacer

import_private

library_note

linting commands

localized notation

mk_iff_of_inductive_prop

mk_simp_attribute

reassoc_axiom

restate_axiom

setup_tactic_parser

General documentation

Additional documentation

Library