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.