| title |
|---|
Naming Conventions |
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_zeromul_onesub_add_eq_add_suble_iff_lt_or_eqSuc_ne_zeroprime_5
If only a prefix of the description is enough to convey the meaning, the name may be made even shorter:
neg_negpred_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_lelt_if_not_gelt_if_le_if_neadd_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_posmul_nonpos_if_nonneg_if_nonposadd_lt_if_lt_if_nonposadd_lt_if_nonpos_if_lt
Sometimes the word "left" or "right" is helpful to describe variants of a theorem.
add_le_add_leftadd_le_add_rightle_if_mul_le_mul_leftle_if_mul_le_mul_right
We can also use the word "self" to indicate a repeated argument:
mul_inv_selfneg_add_self
If a statement is too long, think about creating a definition describing the property.
Some theorems are described using axiomatic names, rather than describing their conclusions.
*_def(for unfolding a definition)reflirreflsymtransantisymasymcongcommassocleft_commright_commmul_left_cancelmul_right_cancelinj(injective)
imp: implicationallexball: bounded forallbex: bounded exists
Intro, elim, and dest rules are identified by a suffix letter:
*I: introduction rule*E: elimination rule*D: destruction rule
The naming of locales follows the convention in the distribution, i.e. we use lower_case_snake_case.