General guidelines:
-
Generally use lowercase with underscores.
-
Brevity is a virtue, but it is more important to have the expressions easy to read, understand, and remember.
-
Be consistent with names and abbreviations.
-
When ordering the arguments and deciding which arguments to make implicit, remember that functions and theorems will often be partially applied; think about common usage.
-
Use lower case for important types, like "nat", "int", "real".
-
Use uppercase for structures and classes, like "Group" and "AbelianGroup".
-
Use "eq" for equations, like "abs_nonneg_eq".
-
Use "iff" for equivalences, like "lt_iff_not_le".
-
Use "imp" for implications, like "lt_imp_le".
-
For properties of an object or operation, put the object or operation first, as in "add_comm", "mul_distrib".
-
Otherwise, for mnemonic purposes, it is often helpful to approximate the statement itself, such as "succ_poss", "le_imp_lt_or_eq", "lt_imp_not_le".
Some specifics:
-
Use pos, neg, nonneg, nonpos.
-
Favor lt, le over gt, ge.