Recommendations for writing understandable rule names.
Do not non-locally use common names for local lemmas, such as:
lemma* crock* crux* a0 b0 c0 ...
temp* goal* main-goal* a1 b1 c1
stupid* wtf* corollary* ...
Using the above names may make your book hard to include for people
who (perhaps via macros) are already using these names or who may want to use
- For unconditional, equality-based rules, we base the rule name on a reading
of the left-hand side, using of as a separator. This is meant to boost
readability when the function names involved have their own hyphens. Examples:
(equal (append (cons a x) y)
(cons a (append x y))))
(equal (true-listp (append x y))
- For rules describing the return-type of a function, we use a similar naming
convention, using of as a separator. Example:
(consp (cons x y)))
- For rules with one simple hypothesis, we add -when-hyp to the
(defthm member-when-atom ;; lhs is (member a x)
(implies (atom x)
(not (member a x))))
(implies (bitp b)
(equal (logbitp 0 b)
(equal b 1))))
- For rules about other equivalence relations, we add -under-equiv to the
(defthm append-under-iff ;; lhs is (append x y)
(iff (append x y)
(or (consp x)
(defthm union-equal-under-set-equiv ;; lhs is (union-equal a b)
(set-equiv (union-equal a b)
(append a b)))
- For rules that specify the upper limit of a function's numerical return
value, we often add -limit.
- For rules that specify both the lower and upper limit of a function's
numerical return value, we often add -bounds.
Obviously you can take this too far. For complex theorems, these
recommendations would lead to names that are far too long. Think of them as a
starting point, not a mandate.
Following these conventions can help lead to more consistently named rules
whose effect may be more easy to guess.