A rudimentary hash function on strings.

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.

• The starting reference point is Nelson, Oppen, Fast decision procedures based on congruence closure, Journal of the ACM (1980)

• The congruence lemmas for dependent type theory as used in Lean are described in Congruence closure in intensional type theory (de Moura, Selsam IJCAR 2016).

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