mathlib3 documentation

tactic.doc_commands

Documentation commands #

We generate html documentation from mathlib. It is convenient to collect lists of tactics, commands, notes, etc. To facilitate this, we declare these documentation entries in the library using special commands.

Since these commands are used in files imported by tactic.core, this file has no imports.

Implementation details #

library_note note_id note_msg creates a declaration `library_note.i for some i. This declaration is a pair of strings note_id and note_msg, and it gets tagged with the library_note attribute.

Similarly, add_tactic_doc creates a declaration `tactic_doc.i that stores the provided information.

def string.hash (s : string) :

A rudimentary hash function on strings.

Equations
meta def name.last  :

Get the last component of a name, and convert it to a string.

meta def tactic.copy_doc_string (fr : name) (to : list name) :

copy_doc_string fr to copies the docstring from the declaration named fr to each declaration named in the list to.

meta def copy_doc_string_cmd (_x : interactive.parse (lean.parser.tk "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.

The library_note command #

A user attribute library_note for tagging decls of type string × string for use in note output.

meta def mk_reflected_definition (decl_name : name) {type : Sort u_1} [reflected (Sort u_1) type] (body : type) [reflected type body] :

mk_reflected_definition name val constructs a definition declaration by reflection.

Example: mk_reflected_definition `foo 17 constructs the definition declaration corresponding to def foo : ℕ := 17

meta def tactic.add_library_note (note_name note : string) :

If note_name and note are strings, add_library_note note_name note adds a declaration named library_note.<note_name> with note as the docstring and tags it with the library_note attribute.

A command to add library notes. Syntax:

/--
note message
-/
library_note "note id"

Collects all notes in the current environment. Returns a list of pairs (note_id, note_content)

The add_tactic_doc_entry command #

inductive doc_category  :

The categories of tactic doc entry.

Instances for doc_category
@[protected, instance]
@[protected, instance]
@[protected, instance]
structure tactic_doc_entry  :

The information used to generate a tactic doc entry

Instances for tactic_doc_entry

Turns a tactic_doc_entry into a JSON representation.

A user attribute tactic_doc for tagging decls of type tactic_doc_entry for use in doc output

Collects everything in the environment tagged with the attribute tactic_doc.

add_tactic_doc tde adds a declaration to the environment with tde as its body and tags it with the tactic_doc attribute. If tde.decl_names has exactly one entry `decl and if tde.description is the empty string, add_tactic_doc uses the doc string of decl as the description.

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.

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

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.

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.

The congruence closure tactic cc tries to solve the goal by chaining equalities from context and applying congruence (i.e. if a = b, then f a = f b). It is a finishing tactic, i.e. it is meant to close the current goal, not to make some inconclusive progress. A mostly trivial example would be:

example (a b c : ) (f :   ) (h: a = b) (h' : b = c) : f a = f c := by cc

As an example requiring some thinking to do by hand, consider:

example (f :   ) (x : )
  (H1 : f (f (f x)) = x) (H2 : f (f (f (f (f x)))) = x) :
  f x = x :=
by cc

The tactic works by building an equality matching graph. It's a graph where the vertices are terms and they are linked by edges if they are known to be equal. Once you've added all the equalities in your context, you take the transitive closure of the graph and, for each connected component (i.e. equivalence class) you can elect a term that will represent the whole class and store proofs that the other elements are equal to it. You then take the transitive closure of these equalities under the congruence lemmas.

The cc implementation in Lean does a few more tricks: for example it derives a=b from nat.succ a = nat.succ b, and nat.succ a != nat.zero for any a.

conv {...} allows the user to perform targeted rewriting on a goal or hypothesis, by focusing on particular subexpressions.

See https://leanprover-community.github.io/extras/conv.html for more details.

Inside conv blocks, mathlib currently additionally provides

  • erw,
  • ring, ring2 and ring_exp,
  • norm_num,
  • norm_cast,
  • apply_congr, and
  • conv (within another conv).

apply_congr applies congruence lemmas to step further inside expressions, and sometimes gives better results than the automatically generated congruence lemmas used by congr.

Using conv inside a conv block allows the user to return to the previous state of the outer conv block after it is finished. Thus you can continue editing an expression without having to start a new conv block and re-scoping everything. For example:

example (a b c d : ) (h₁ : b = c) (h₂ : a + c = a + d) : a + b = a + d :=
by conv
{ to_lhs,
  conv
  { congr, skip,
    rw h₁ },
  rw h₂, }

Without conv, the above example would need to be proved using two successive conv blocks, each beginning with to_lhs.

Also, as a shorthand, conv_lhs and conv_rhs are provided, so that

example : 0 + 0 = 0 :=
begin
  conv_lhs { simp }
end

just means

example : 0 + 0 = 0 :=
begin
  conv { to_lhs, simp }
end

and likewise for to_rhs.

The simp tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses. It has many variants.

simp simplifies the main goal target using lemmas tagged with the attribute [simp].

simp [h₁ h₂ ... hₙ] simplifies the main goal target using the lemmas tagged with the attribute [simp] and the given hᵢ's, where the hᵢ's are expressions. If hᵢ is preceded by left arrow ( or <-), the simplification is performed in the reverse direction. If an hᵢ is a defined constant f, then the equational lemmas associated with f are used. This provides a convenient way to unfold f.

simp [*] simplifies the main goal target using the lemmas tagged with the attribute [simp] and all hypotheses.

simp * is a shorthand for simp [*].

simp only [h₁ h₂ ... hₙ] is like simp [h₁ h₂ ... hₙ] but does not use [simp] lemmas

simp [-id_1, ... -id_n] simplifies the main goal target using the lemmas tagged with the attribute [simp], but removes the ones named idᵢ.

simp at h₁ h₂ ... hₙ simplifies the non-dependent hypotheses h₁ : T₁ ... hₙ : Tₙ. The tactic fails if the target or another hypothesis depends on one of them. The token or |- can be added to the list to include the target.

simp at * simplifies all the hypotheses and the target.

simp * at * simplifies target and all (non-dependent propositional) hypotheses using the other hypotheses.

simp with attr₁ ... attrₙ simplifies the main goal target using the lemmas tagged with any of the attributes [attr₁], ..., [attrₙ] or [simp].

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

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

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