Specific-kinds-of-formulas-as-rewrite-rules
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))
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.
