naming.md

Mathlib naming conventions

Author: Jeremy Avigad

General conventions

Identifiers are generally lower case with underscores. For the most part, we rely on descriptive names. Often the name of theorem simply describes the conclusion:

• succ_ne_zero

• mul_zero

• mul_one

• sub_add_eq_add_sub

• le_iff_lt_or_eq

If only a prefix of the description is enough to convey the meaning, the name may be made even shorter:

• neg_neg

• pred_succ

Sometimes, to disambiguate the name of theorem or better convey the intended reference, it is necessary to describe some of the hypotheses. The word "of" is used to separate these hypotheses:

• lt_of_succ_le

• lt_of_not_ge

• lt_of_le_of_ne

• add_lt_add_of_lt_of_le

Sometimes abbreviations or alternative descriptions are easier to work with. For example, we use pos, neg, nonpos, nonneg rather than zero_lt, lt_zero, le_zero, and zero_le.

• mul_pos

• mul_nonpos_of_nonneg_of_nonpos

• add_lt_of_lt_of_nonpos

• add_lt_of_nonpos_of_lt

Sometimes the word "left" or "right" is helpful to describe variants of a theorem.

• add_le_add_left

• add_le_add_right

• le_of_mul_le_mul_left

• le_of_mul_le_mul_right

We can also use the word "self" to indicate a repeated argument:

• mul_inv_self

• neg_add_self

Dots

Dots are used for namespaces, and also for automatically generated names like recursors, eliminators and structure projections. They can also be introduced manually, for example, where projector notation is useful. Thus they are used in all of the following situations.

Intro, elim, and destruct rules for logical connectives, whether they are automatically generated or not:

• and.intro

• and.elim

• and.left

• and.right

• or.inl

• or.inr

• or.intro_left

• or.intro_right

• iff.intro

• iff.elim

• iff.mp

• iff.mpr

• not.intro

• not.elim

• eq.refl

• eq.rec

• eq.subst

• heq.refl

• heq.rec

• heq.subst

• exists.intro

• exists.elim

• true.intro

• false.elim

Places where projection notation is useful, for example:

• and.symm

• or.symm

• or.resolve_left

• or.resolve_right

• eq.symm

• eq.trans

• heq.symm

• heq.trans

• iff.symm

• iff.refl

We generally restrict the use of dots to inductive types. So, for example, we use:

• dvd_intro

• dvd_dest

• dvd_elim

• le_refl

• le_trans

Axiomatic descriptions

Some theorems are described using axiomatic names, rather than describing their conclusions.

• def (for unfolding a definition)

• refl

• irrefl

• symm

• trans

• antisymm

• asymm

• congr

• comm

• assoc

• left_comm

• right_comm

• mul_left_cancel

• mul_right_cancel

• inj (injective)

Variable conventions

• u, v, w, ... for universes

• α, β, γ, ... for types

• a, b, c, ... for propositions

• x, y, z, ... for elements of a generic type

• h, h₁, ... for assumptions

• p, q, r, ... for predicates and relations

• s, t, ... for lists

• s, t, ... for sets

• m, n, k, ... for natural numbers

• i, j, k, ... for integers

Names for symbols

• imp: implication

• forall

• exists

• ball: bounded forall

• bex: bounded exists

Identifiers and theorem names

We generally use lower case with underscores for theorem names and definitions. Sometimes upper case is used for bundled structures, such as Group. In that case, use CamelCase for compound names, such as AbelianGroup.

We adopt the following naming guidelines to make it easier for users to guess the name of a theorem or find it using tab completion. Common "axiomatic" properties of an operation like conjunction or multiplication are put in a namespace that begins with the name of the operation:

import standard algebra.ordered_ring

check and.comm
check mul.comm
check and.assoc
check mul.assoc
check @mul.left_cancel  -- multiplication is left cancelative

In particular, this includes intro and elim operations for logical connectives, and properties of relations:

import standard algebra.ordered_ring

check and.intro
check and.elim
check or.intro_left
check or.intro_right
check or.elim

check eq.refl
check eq.symm
check eq.trans

For the most part, however, we rely on descriptive names. Often the name of theorem simply describes the conclusion:

import standard algebra.ordered_ring
open nat
check succ_ne_zero
check mul_zero
check mul_one
check @sub_add_eq_add_sub
check @le_iff_lt_or_eq

If only a prefix of the description is enough to convey the meaning, the name may be made even shorter:

import standard algebra.ordered_ring

check @neg_neg
check nat.pred_succ

When an operation is written as infix, the theorem names follow suit. For example, we write neg_mul_neg rather than mul_neg_neg to describe the patter -a * -b.

Sometimes, to disambiguate the name of theorem or better convey the intended reference, it is necessary to describe some of the hypotheses. The word "of" is used to separate these hypotheses:

import standard algebra.ordered_ring
open nat
check lt_of_succ_le
check lt_of_not_ge
check lt_of_le_of_ne
check add_lt_add_of_lt_of_le

The hypotheses are listed in the order they appear, not reverse order. For example, the theorem A → B → C would be named C_of_A_of_B.

Sometimes abbreviations or alternative descriptions are easier to work with. For example, we use pos, neg, nonpos, nonneg rather than zero_lt, lt_zero, le_zero, and zero_le.

import standard algebra.ordered_ring
open nat
check mul_pos
check mul_nonpos_of_nonneg_of_nonpos
check add_lt_of_lt_of_nonpos
check add_lt_of_nonpos_of_lt

These conventions are not perfect. They cannot distinguish compound expressions up to associativity, or repeated occurrences in a pattern. For that, we make do as best we can. For example, a + b - b = a could be named either add_sub_self or add_sub_cancel.

Sometimes the word "left" or "right" is helpful to describe variants of a theorem.

import standard algebra.ordered_ring

check add_le_add_left
check add_le_add_right
check le_of_mul_le_mul_left
check le_of_mul_le_mul_right

---

Copyright (c) 2016 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad