# Naming-rewrite-rules

Recommendations for writing understandable rule names.

#### Strong Recommendations

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* ...

#### Rationale

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
them.

#### Weak Recommendations

- 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:
(defthm append-of-cons
(equal (append (cons a x) y)
(cons a (append x y))))
(defthm true-listp-of-append
(equal (true-listp (append x y))
(true-listp y)))

- For rules describing the return-type of a function, we use a similar naming
convention, using of as a separator. Example:
(defthm consp-of-cons
(consp (cons x y)))

- For rules with one simple hypothesis, we add -when-hyp to the
name. Examples:
(defthm member-when-atom ;; lhs is (member a x)
(implies (atom x)
(not (member a x))))
(defthm logbitp-of-0-when-bitp
(implies (bitp b)
(equal (logbitp 0 b)
(equal b 1))))

- For rules about other equivalence relations, we add -under-equiv to the
name. Examples:
(defthm append-under-iff ;; lhs is (append x y)
(iff (append x y)
(or (consp x)
y)))
(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.

#### Rationale

Following these conventions can help lead to more consistently named rules
whose effect may be more easy to guess.