Commands - mathlib3 docs

#explode / #explode_widget

#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_widget decl_name renders a widget that displays an #explode proof.

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

Related declarations

tactic.explode_cmd
tactic.explode_widget_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:

search

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

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

Tags:

simplification
arithmetic
decision procedure

Related declarations

tactic.norm_num_cmd

Import using

import tactic.norm_num
import tactic

#push_neg

The syntax is #push_neg e, where e is an expression, which will print the push_neg form of e.

#push_neg understands local variables, so you can use them to introduce parameters.

Tags:

logic

Related declarations

tactic.push_neg_cmd

Import using

import tactic.push_neg
import tactic.basic

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

search

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

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 a has_coe_to_fun instance has been declared, or the notation of a notation class (like has_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 declaration foo and you want to apply the projections snd, coe (which is a prefix) and fst, in that order you can run @[simps snd_coe_fst] def foo ... and this will generate a lemma with the name coe_foo_snd_fst.
- Run initialize_simps_projections? (or set_option trace.simps.verbose true) to see the generated projections.
You can declare a new name for a projection that is the composite of multiple projections, e.g.
```
  structure A := (proj : ℕ)
  structure B extends A
  initialize_simps_projections? B (to_A_proj → proj, -to_A)
```
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 old_structure_cmd). In the above example, it is desirable to add -to_A, so that @[simps] doesn't automatically apply the B.to_A projection and then recursively the A.proj projection in the lemmas it generates. If you want to get both the foo_proj and foo_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] or initialize_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 run initialize_simps_projections after defining the has_coe_to_fun instance
```
  instance {mM : has_mul M} {mN : has_mul N} : has_coe_to_fun (M →ₙ* N) := ...
  initialize_simps_projections mul_hom (to_fun → apply)
```
This will generate foo_apply lemmas for each declaration foo.
If you prefer coe_foo lemmas that state equalities between functions, use initialize_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
```
  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)
```
In the first case, you can get both lemmas using @[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) (like rel_embedding), then you have to specify explicitly that you want to use a coercion as a custom projection. For example
```
  def 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)

Tags:

simplification

Related declarations

initialize_simps_projections_cmd

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

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_nonempty_instance checks whether every type has an associated inhabited, unique or nonempty 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.
check_type checks that the statement of a declaration is well-typed.
check_univs checks that there are no bad max 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.

The following linters are not run by default:

doc_blame_thm, checks for missing doc strings on lemmas and theorems.
explicit_vars_of_iff checks if there are explicit variables used on both sides of an iff.

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

Declare notation which is localized to a locale using:

localized "infix (name := my_add) ` ⊹ `: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 (name := my_add) ⊹ :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.
Note: In mathlib, you should always provide names for localized notations using the (name := ...) parameter. This prevents issues if the localized notation overrides an existing notation when it gets opened.
Warning: Due to limitations in the implementation, you cannot use _ in localized notations. (Otherwise open_locale foo will fail if foo is already opened or partially opened.) Instead, you should use the hole! notation as a drop-in replacement. For example:

-- BAD
-- localized "infix (name := my_add) ` ⊹[` R `] ` := my_add _ R" in foo
-- GOOD
localized "infix (name := my_add) ` ⊹[` R `] ` := my_add hole! R" in foo

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

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.mk_simp_attribute
import tactic.basic

print_sorry_in

The command

#print_sorry_in nm

prints all declarations that (transitively) occur in the value of declaration nm and depend on sorry. This command assumes that no sorry occurs in mathlib. To find sorry in mathlib, use #eval print_sorry_in `nm ff instead. Example:

def foo1 : false := sorry
def foo2 : false ∧ false := ⟨sorry, foo1⟩
def foo3 : false := foo2.left
def foo4 : true := trivial
def foo5 : true ∧ false := ⟨foo4, foo3⟩
#print_sorry_in foo5

prints

foo5 depends on foo3.
foo3 depends on foo2.
foo2 contains sorry and depends on foo1.
foo1 contains sorry.

Tags:

search
environment
debugging

Related declarations

print_sorry_in_cmd

Import using

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

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.

Tags:

parsing

Related declarations

lean.parser.run_parser_cmd

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.

Tags:

parsing
notation

Related declarations

tactic.setup_tactic_parser_cmd

Import using

import tactic.core
import tactic.basic