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:
If only a prefix of the description is enough to convey the meaning, the name may be made even shorter:
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:
Sometimes abbreviations or alternative descriptions are easier to work with.
For example, we use
nonneg rather than
Sometimes the word “left” or “right” is helpful to describe variants of a theorem.
We can also use the word “self” to indicate a repeated argument:
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)
Names for Symbols
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
The naming of locales follows the convention in the distribution, i.e. we use