Loop$-recursion-induction
Advice on inductive theorems about loop$-recursive functions
Warning: This documentation topic is fairly preliminary
because we do not have a lot of experience yet with apply$, loop$, and loop$-recursion. We assume here that readers are familiar
with the topics cited above.
Definductor
The principles sketched here are illustrated concretely in the tutorial
community book projects/apply/copy-nat-tree.lisp. As noted in that
book, the inductions are hinted manually so the reader can see from first
principles what is involved. However, in the book projects/apply/top we
provide a utility that sometimes automates the creation of the inductive hint
function and associates it with the given loop$-recursive function. See
definductor. The examples worked manually in copy-nat-tree.lisp
are recapitulated towards the end of
projects/apply/definductor-tests.lisp, without the manually provided
hints. In addition, the book
projects/apply/loop-recursion-examples.lisp gives some other examples of
loop$-recursive functions and inductive theorems about them.
Some Basic Principles for Inductive Proofs about Loop$-Recursive Functions
If ACL2 did not have loop$, functions defined in terms of
loop$-recursion would have to be defined with mutual-recursion.
Reconsider the example presented in loop$-recursion.
(defun$ nat-treep (x)
(declare (xargs :loop$-recursion t
:measure (acl2-count x)))
(cond
((atom x) (natp x))
(t (and (true-listp x)
(eq (car x) 'NATS)
(loop$ for e in (cdr x) always (nat-treep e))))))
(defun$ copy-nat-tree (x)
(declare (xargs :loop$-recursion t
:measure (acl2-count x)))
(cond
((atom x)
(if (natp x)
(if (equal x 0)
0
(+ 1 (copy-nat-tree (- x 1))))
x))
(t (cons 'nats
(loop$ for e in (cdr x) collect (copy-nat-tree e))))))
Without loop$ the latter function would have to be defined this way.
We name it mr-copy-nat-tree, where the ``mr'' reminds us this is
part of a mutually recursive clique.
(mutual-recursion
(defun mr-copy-nat-tree (x)
(cond
((atom x)
(if (natp x)
(if (equal x 0)
0
(+ 1 (mr-copy-nat-tree (- x 1))))
x))
(t (cons 'nats
(mr-copy-nat-tree-list (cdr x))))))
(defun mr-copy-nat-tree-list (x)
(cond
((endp x) nil)
(t (cons (mr-copy-nat-tree (car x))
(mr-copy-nat-tree-list (cdr x)))))))
Note that we define mr-copy-nat-tree by copying the definition of
copy-nat-tree (renaming recursive calls appropriately) but replacing the
use of loop$ in copy-nat-tree with a call of a mutually-recursive
function here called mr-copy-nat-tree-list. We call
mr-copy-nat-tree-list the ``list counterpart'' of mr-copy-nat-tree.
However, in general there may be more than just two functions in the clique
and so we refer generically to mr-copy-nat-tree-list as a ``co-member''
of the clique.
How would you prove theorems about mr-copy-nat-tree? Four principles
are known to most ACL2 users of mutual-recursion. These principles
apply to loop$-recursive functions as well as to mutually recursive
ones. We state them here in terms of both kinds of definitions.
- While simple recursive functions suggest ``appropriate'' inductions,
mutually recursive functions and loop$-recursive functions do not. If
you want to prove a theorem about such functions you have to arrange some
kind of induction hint.
- You can't generally prove an isolated theorem about a single member of a
mutually recursive clique or a loop$-recursive function. Instead, you
must state a conjecture about every member of the clique, conjoin all those
theorems together, and prove them inductively all at once. Applied to
proving a theorem about mr-copy-nat-tree this advice means we must
conjoin the theorem about that function with ``the same'' theorem about
mr-copy-nat-tree-list, and more generally with theorems about every
co-member of the clique. Of course, what we mean by ``the same'' theorem
about different members of the clique depends on what each member contributes
to the overall computation. Applied to the loop$-recursive function
copy-nat-tree this advice means we must simultaneously prove a theorem
about every loop$ in the function.
- Inductively provable theorems must be sufficiently general. When dealing
with a mutually recursive clique, each conjunct must address itself to the
``general'' call of the co-member in question, e.g., to
(mr-copy-nat-tree-list x) not to the specific call inside
mr-copy-nat-tree, which is (mr-copy-nat-tree-list (cdr x)). When
dealing with a loop$-recursive function, each conjunct must address
itself to the general target, not to specific target in the loop$
recursive function. In the case of the loop$-recursive function
copy-nat-tree we need a conjunct about (loop$ for e in x
collect (copy-nat-tree e)), not about (loop$ for e in (cdr x)
collect (copy-nat-tree e)).
- Finally, the induction scheme used must provide an inductive hypothesis
about every recursive call of every co-member of the clique or, in the case
of loop$-recursion, about every recursive unwinding of each
loop$.
Remember: Because loop$-recursive functions call themselves
recursively with apply$, any theorem about a loop$ recursive
function must almost certainly include a warrant hypothesis for that
function!
We illustrate these principles in the community book
projects/apply/copy-nat-list.lisp.
