advice about how to handle commonly occurring formulas as rewrite rules

Below we give you some guidelines for handling specific, commonly occurring situations.

* Associativity: If a function f is associative, prove

(equal (f (f x y) z) (f x (f y z)))
ACL2 will use this to flatten f-nests ``to the right.''

* Commutativity: If a function f is commutative, prove both

(equal (f x y) (f y x))
(equal (f x (f y z)) (f y (f x z)))
ACL2's heuristics will use these rules to order the arguments alphabetically, so that (f B (f D (f A C))) becomes (f A (f B (f C D))).

* Distributivity: If you have a pair of functions f and g so that (f x (g y z)) is (g (f x y) (f x z)) or some other form of distributivity is provable, arrange your rules to move the lighter function symbol up and the heavier one toward the variable symbols. For example, our arithmetic libraries drive multiplication through addition, producing sums of products rather than products of sums.

* Identity and Other Laws: Prove the obvious identity and zero laws (or at least anticipate that you might need them down the road) so as to eliminate operators.

* Get Rid of Tail Recursive Functions: A corollary to the above advice concerns tail recursive functions that use auxiliary variables. New users often define concepts using tail recursions, accumulating partial results in auxiliary variables, because creating such functions is similar to programming with while loops. Expert users will use tail recursion when necessary for execution efficiency. But tail recursive functions are messy to reason about: their auxiliary variables have to be properly initialized to make the functions compute the expected results, but to state inductively provable properties of tail recursive functions you must identify the invariants on those auxiliary variables. This problem tends not to happen with primitive recursive functions. A primitive recursive function is one that recurs down one variable and holds all the other variables constant in recursion. Most tail-recursive functions can be written elegantly as primitive recursive functions, though one might have to ignore the programmer's desire to make things efficient and define auxiliary functions to appropriately transform the value returned by the recursive call. The classic example is reverse defined in terms of the auxiliary function append versus reverse defined tail recursively with an accumulator. By introducing append you introduce a concept about which you can state lemmas and decompose the proofs of properties of reverse. So if your problem involves tail recursive functions with auxiliary variables, define the primitive recursive version, prove that the tail recursive function is equivalent to the primitive recursive one, and arrange the rewrite rule to eliminate the tail recursive function.

* Get Rid of Mutually Recursive Functions: Similarly, if you have used mutual-recursion to introduce a clique of mutually recursive functions, f1, f2, ..., you will find that to reason about any one function in the nest you have to reason about all of them. Any mutually recursive function can be defined in a singly recursive way. So do that and then prove a rewrite rule that gets rid of all the mutually recursive functions by proving

(and (equal (f1 ...) (g1 ...))
     (equal (f2 ...) (g2 ...))

where the gi are singly recursive. You may need to appeal to a trick to define the gi: define a singly recursive function that takes a flag argument and mimics whichever mutually recursive function the flag specifies. See mutual-recursion and see mutual-recursion-proof-example .

If you got to this documentation page from the tutorial discussion of rewrite rules, use your browser's Back Button now to return to introduction-to-rewrite-rules-part-2.