## Theorem Naming

Every theorem/lemma must have a unique name. Identifiers are generally lower case with underscores. However, upper case letters are used if it is standard to capitilise a given identifier (e.g. constructors). For the most part, we rely on descriptive names. Often the name of theorem simply describes the syntactic structure of the conclusion:

• `mul_zero`
• `mul_one`
• `sub_add_eq_add_sub`
• `le_iff_lt_or_eq`
• `Suc_ne_zero`
• `prime_5`

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

• `neg_neg`
• `pred_Suc`

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

• `lt_if_Suc_le`
• `lt_if_not_ge`
• `lt_if_le_if_ne`
• `add_lt_add_if_lt_if_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_if_nonneg_if_nonpos`
• `add_lt_if_lt_if_nonpos`
• `add_lt_if_nonpos_if_lt`

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

• `add_le_add_left`
• `add_le_add_right`
• `le_if_mul_le_mul_left`
• `le_if_mul_le_mul_right`

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

• `mul_inv_self`
• `neg_add_self`

If a statement is too long, think about creating a definition describing the property.

### Axiomatic Descriptions

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

• `*_def` (for unfolding a definition)
• `refl`
• `irrefl`
• `sym`
• `trans`
• `antisym`
• `asym`
• `cong`
• `comm`
• `assoc`
• `left_comm`
• `right_comm`
• `mul_left_cancel`
• `mul_right_cancel`
• `inj` (injective)

### Names for Symbols

• `imp`: implication
• `all`
• `ex`
• `ball`: bounded forall
• `bex`: bounded exists

### Introduction, Elimination, Destruction Rules

Intro, elim, and dest rules are identified by a suffix letter:

• `*I`: introduction rule
• `*E`: elimination rule
• `*D`: destruction rule

## Locale naming

The naming of locales follows the convention in the distribution, i.e. we use `lower_case_snake_case`.