		Search-engine friendly clone of the ACL2 documentation.

Best-practices

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.