Lp-section-18
Conclusion
LP18: Conclusion
Here are two pieces of advice.
First, if you can think of a good name for the concept implemented by a
loop$ statement, use defun to define that name. This is especially
the case if you intend to reason about that loop$ statement or to write
more than one instance of it.
For example, rather than write instances of
(loop$ for a in x as b in y sum (* a b))
it is better to define (dot-product x y) with that loop$ as its body
and then write calls of dot-product.
Basically, names are good as long as you can remember them. They give you
a place to hang lemmas and the lemmas match without having to think about
rewriting lambdas, local variables, etc. Not all loop$s compute concepts
with obvious, memorable names, but just because you can write
“anonymous” iterations doesn't mean you should!
Second, remember when you create a lemma intended to rewrite a loop$
statement you should normalize the body under your intended rewrite theory.
As an experienced ACL2 user you would never write a lemma that tried to
rewrite an endp or nfix or zp term. The lemma will never
“see” such terms because the rewriter will have opened them up.
You should apply that same kind of thinking when you write lemmas intended to
rewrite loop$s.
That's it. We can't think of anything else to say! We urge you to resort
to the ACL2 user's manual for further information.
Some relevant topics are
The End of the Loop$ Primer. (Return to the Table of Contents).
