Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
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))and
(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.
