Iteration with `loop$` over an interval of integers or a list

This topic assumes that you have read the introduction to

Examples of `loop$` expressions, including

The only allowed iteration clauses are

You may have as many iteration clauses as you wish, connected with

(loop$ for v of-type (and integer (not (satisfies zerop))) from 1 to 100 sum (/ 1 v))

Here is that same example with a more concise type specification.

(loop$ for v of-type (integer 1 *) from 1 to 100 sum (/ 1 v))

After all of the iteration clauses, you may have a termination test,
signaled by

Between the

(loop$ for u in lst1 as v in lst2 until :guard (invariantp u v) (test u v) collect (body u v))

ACL2 supports only five operators in

The special symbols noted above, sometimes called ``

Between the operator, e.g.,

(loop$ for u in lst1 as v in lst2 collect :guard (invariantp u v) (body u v))

This is sometimes necessary in the verification of the guards for
the

The syntax of Common Lisp

First we introduce the syntax of a ``target clause,'' a ``type-spec,'' and
the ``operators.'' Then we describe the most elaborate form of a

A *target clause* has one of four forms

IN *list-expr*ON *expr*FROM *lo-expr*TO *hi-expr*FROM *lo-expr*TO *hi-expr*BY *step-expr*

where *list-expr* is a term (which is expected to evaluate to a true
list), *expr* is a term, *lo-expr* and *hi-expr* are
terms (which are expected to evaluate to integers), and *step-expr* is a
term (which is expected to evaluate to a positive integer).

The legal *type-specs* are listed in `type-spec`.

The legal *operators* are

The most elaborate

*v1**spec1
target1*

*v2**spec2
target2*

...

*vn**specn targetn*

*guard1
until-expr*

*guard2
when-expr*

; Note the

*op**guard3
body-expr*

where each *vi* is a legal variable symbol and they are all
distinct, each *type-speci* is a `type-spec`, each
*targeti* is a target clause, each *guardi*,
*until-expr*, and *when-expr* is a term, *op* is
an operator, and *body-expr* is a term. Furthermore,
*until-expr*, *when-expr*, and *body-expr* must be
tame!

*The ALWAYS/THEREIS Exception:* Common Lisp prohibits loops
with both a

The following elements may be omitted.

- any line beginning with
AS ,UNTIL orWHEN , - any
OF-TYPE *speci*, and - any
:GUARD *guardi*.

As noted above, the

We give names to certain classes of the syntactic entities above. The
*v1*, ..., *vn* are called the *iteration variables*. The
*spec1*, ..., *specn* are called *type specs*, each
corresponds to a certain iteration variable, and each gives rise to a *type
term* about its variable in the sense that ``*list-expr* and
*expr* in ``*list-expr*'' and ``*expr*'' and
the *lo-expr*, *hi-expr* and optional *step-expr* in the
``*lo-expr* *hi-expr* *step-expr*''
targets are called *target terms*. Finally, the *until-expr*,
*when-expr*, and *body-expr* are called *iterative forms*.

We distinguish the target terms from the iterative forms because they are
handled very differently at evaluation time. When a

A *simple loop$* (or, sometimes, a

(loop$ for x in lst when (evenp x) collect (+ 1 (sq x)))

A *fancy loop$* if it
is not simple. Both of the following

(loop$ for x in xlst as y on ylst collect (expr x y)) (loop$ for x in xlst collect (expr x z))

The first is fancy because it has two iteration variables. The second is
fancy because the body freely uses the variable

loop$ simple fancy keyword scion scion ______________________________________________ SUM sum$ sum$+ COLLECT collect$ collect$+ ALWAYS always$ always$+ THEREIS thereis$ thereis$+ APPEND append$ append$+ UNTIL until$ until$+ WHEN when$ when$+

We deal with simple

For example, the simple

(loop$ for x in lst collect (+ 1 (sq x)))

translates to (a term equivalent to)

(collect$ (lambda$ (x) (declare (ignorable x)) (+ 1 (sq x))) lst).

**Note:** The actual translation is tagged with various markers that
play a role in evaluation but which are logically irrelevant and which are
removed during proof. In this discussion we will not display the marked-up
translations but logically equivalent terms instead. You can see the actual
translations for yourself with `trans`.

In the translation the target term, `lambda$` expression, which means its translation
becomes a component of a quoted

(loop$ for x in lst until (> x 100) when (evenp x) collect (+ 1 (sq x)))

becomes

(collect$ (lambda$ (x) (declare (ignorable x)) (+ 1 (sq x))) (when$ (lambda$ (x) (declare (ignorable x)) (evenp x)) (until$ (lambda$ (x) (declare (ignorable x)) (> x 100)) lst)))

So from a logical perspective, the presence of an

(loop$ for x on lst collect (expr x))

which maps

(collect$ (lambda$ (x) (expr x)) (tails lst))

where, for example,

Spiritually similarly,

(loop$ for i from 1 to max by step collect (expr x))

logically becomes

(collect$ (lambda$ (x) (expr x)) (from-to-by 1 max step))

where, for example,

Similar translations are done for the other operators, e.g.,

The following example illustrates basic guard proof obligations, in
particular showing that `lambda` objects
be guard verifiable in isolation, not confined to the context in which a
particular

(include-book "projects/apply/top" :dir :system) (defun$ sq (n) (declare (xargs :guard (natp n))) (* n n)) (defun foo (lst) (declare (xargs :guard (nat-listp lst))) (loop$ for x of-type (satisfies nat-listp) on lst when (consp x) sum (sq (car x))))

Guard verification fails for `pso` we can see that the

Subgoal 1.2 (IMPLIES (NAT-LISTP LOOP$-IVAR) (INTEGERP (CAR LOOP$-IVAR))).

Let's see what is going on by looking at the following simplified
translation of the

(sum$ '(lambda (loop$-ivar) (declare (type (satisfies nat-listp) loop$-ivar)) (sq (car loop$-ivar))) (when$ '(lambda ...) (tails lst)))

Notice that the

(defun foo (lst) (declare (xargs :guard (nat-listp lst))) (loop$ for x of-type (satisfies nat-listp) on lst when (consp x) sum :guard (consp x) ; note new :guard (sq (car x))))

This new

A simplified translation of the

(sum$ '(lambda (loop$-ivar) (declare (type (satisfies nat-listp) loop$-ivar) (xargs :guard (consp loop$-ivar))) (sq (car loop$-ivar))) (when$ '(lambda ...) (tails lst)))

Naively we might have expected that the guard proof obligation for the
`lambda` objects must be guard-verifiable on their own.
The reason for the latter requirement is that our implementation caches
guard-verified

An example of a fancy

(loop$ for x in xlst as y in ylst collect (expr x y z))

This loop exhibits both characteristics (a) and (b): it has an

(collect$+ (lambda$ (loop$-gvars loop$-ivars) (declare (xargs :guard (and (true-listp loop$-gvars) (equal (len loop$-gvars) 1) (true-listp loop$-ivars) (equal (len loop$-ivars) 2)))) (let ((z (car loop$-gvars)) (x (car loop$-ivars)) (y (car (cdr loop$-ivars)))) (declare (ignorable x y)) (expr x y z))) (list z) (loop$-as (list xlst ylst)))

Before we show the definition of

The definition of

(defun collect$+ (fn loop$-gvars lst) (if (endp lst) nil (cons (apply$ fn (list loop$-gvars (car lst))) (collect$+ fn loop$-gvars (cdr lst)))))

We have omitted the guard and an `mbe` form that make it run more
efficiently. All the fancy

Inspection of the

The names of the formals for the

Since every `true-listp`.

But in addition to the expected guard conjectures, we generate some
special ones for the terms produced by translating

- First, every element (or tail, in the case of
ON loop$ s)) satisfies the type-spec, if any, and theloop$ body's:GUARD , if any. - Second, the
loop$ body produces a value acceptable to theloop$ operator, e.g., the body of aSUM loop$ produces a number and the body of anAPPEND loop$ produces a true list.

All of the simple

(AND (APPLY$-GUARD FN '(NIL)) (TRUE-LISTP LST)),

and all the fancy

(AND (APPLY$-GUARD FN '(NIL NIL)) (TRUE-LISTP LOOP$-GVARS) (TRUE-LIST-LISTP LST)).

In addition to the normal guard conjectures that would be generated by
calls of these scions, ACL2 generates some special guard conjectures because
the normal guard conjectures are insufficient to guarantee the error-free
execution of the corresponding Common Lisp

For example, the simplified translation of the body of

(defun foo (lst) (declare (xargs :guard (foo-guardp lst))) (loop$ for x of-type (satisfies spec) on lst sum (expr x)))

is as follows. (One might expect the second argument of the

(sum$ (lambda$ (loop$-ivar) (declare (type (satisfies spec) loop$-ivar)) (expr loop$-ivar)) (tails (prog2$ (let ((loop$-last-cdr (last-cdr lst))) (declare (type (satisfies spec) loop$-last-cdr)) loop$-last-cdr) lst)))

Prior to the provision for special guards, the normal guard conjectures
generated for

(and (implies (foo-guardp lst) ; [1] (apply$-guard (lambda$ (loop$-ivar) (expr loop$-ivar)) '(nil))) (implies (foo-guardp lst) ; [2] (true-listp (tails lst))) (implies (spec loop$-ivar) (expr-guardp loop$-ivar))) ; [3] (implies (foo-guardp lst) ; [4] (let ((loop$-last-cdr (last-cdr lst))) (spec loop$-last-cdr)))

Conjectures [1] and [2] stem from the guard for `last-cdr` may also be from [4].

(Technical Note. The production of [4] is accomplished as follows for an
expression

(prog2$ (let ((loop$-last-cdr (last-cdr lst))) (declare (type type-spec loop$-last-cdr)) loop$-last-cdr) lst)

The `declare` form causes formula [4] above to be generated as a
guard proof obligation. End of Technical Note.)

The guard proof obligation shown as [4] above, for an expression

But consider the raw Lisp

(loop for x of-type (satisfies spec) on lst sum (expr x)).

For this

So when ACL2's guard verification process encounters a

(implies (and (warrant ...) ; see below ; [5] (foo-guardp lst) (member-equal newv (tails lst))) (spec newv)) (implies (and (warrant ...) ; see below ; [6] (foo-guardp lst) (member-equal newv (tails lst))) (acl2-numberp (apply$ (lambda$ (loop$-ivar) (expr loop$-ivar)) (list newv))))

Notice the addition of hypotheses above of the form *warrant hypotheses* for function symbols that
might be `apply$`'d during evaluation of a scion call (in this case,

In general, you may notice that ACL2 generates such ``special'' guard
conjectures for all calls of `true-listp` (instead of an `ACL2-numberp` as required by the

The translation of

One sign of that compromise is our use of scions to handle

(loop$ for x in lst until ... when ... collect ...)

into

(collect$ ... (when$ ... (until$ ... lst)))

we're forcing the evaluation of the formal semantics to copy the target
twice before collecting. But it gives us the ability to reason
compositionally about

Another example of compositionality is to consider a simple

(loop$ for x in (append a b) collect (expr x)) (loop$ for x on (append a b) collect (expr x)) (loop$ for x in (append a b) until (stop x) collect (expr x)) (loop$ for x on (append a b) until (stop x) collect (expr x)) (loop$ for x in (append a b) when (test x) collect (expr x)) (loop$ for x on (append a b) when (test x) collect (expr x)) (loop$ for x in (append a b) until (stop x) when (test x) collect (expr x)) (loop$ for x on (append a b) until (stop x) when (test x) collect (expr x))

Similarly, there are 8 ways to

(equal (collect$ fn (append a b)) (append (collect$ fn a) (collect$ fn b))) (equal (sum$ fn (append a b)) (+ (sum$ fn a) (sum$ fn b))) (equal (always$ fn (append a b)) (and (always$ fn a) (always$ fn b))) (equal (thereis$ fn (append a b)) (or (thereis$ fn a) (thereis$ fn b))) (equal (append$ fn (append a b)) (append (append$ fn a) (append$ fn b))) (equal (until$ fn (append a b)) (if (exists$ fn a) (until$ fn a) (append a (until$ fn b)))) (equal (when$ fn (append a b)) (append (when$ fn a) (when$ fn b)))

Thus, you can reason about

To deal with fancy

By the way, if you want the prover to convert every simple scion to its fancy counterpart you could prove rewrite rules like that below.

(defthm convert-collect$-to-collect$+ (implies (ok-fnp fn) (equal (collect$ fn lst) (collect$+ `(lambda (loop$-gvars loop$-ivars) (,fn (car loop$-ivars))) nil (loop$-as (list lst))))) :hints (("[1]Goal" :expand ((tamep (cons fn '(x))) (tamep (cons fn '((car loop$-ivars))))))))