		Search-engine friendly clone of the ACL2 documentation.

Loop$-primer

Lp-section-11

Proving Theorems about FOR Loop$s

LP11: Proving Theorems about FOR Loop$s

Proving theorems about FOR loop$ in ACL2 is essentially no different than proving theorems about other constructs in ACL2. Indeed, since loop$s turn into calls of scions of apply$, proving things about them is exactly the problem of proving things about scions. However, loop$s raise some problems that are not fully technical.

Iteration is so common in programming — and the meaning of loop$ statements are intuitively obvious — that you often don't think anything logically complicated is going on! But when proofs are desired you must keep induction in mind and you must train yourself to see the need for generalization in order to allow the necessary inductions.
You're not syntactically aware of the presence of apply$ and the concomitant need for tameness and warrants.
You don't see the translations of loop$s when you type them but they appear “unexpectedly” in the checkpoints of failing proofs and that can throw you for a loop (so to speak).
The translations of loop$s, especially of fancy loop$, are pretty complicated in and of themselves and can be difficult to understand, much less generalize and manipulate formally.
The ACL2 user rarely has to think about local variable bindings, but those issues arise quite often in dealing with loop$s (and nested lambda objects in general).

With these points in mind we will now work through a proof about a fancy loop$. In the next section we'll challenge you to do some proofs about other loop$s. The proof description below is rather long because we cast it as a narrative of the proof discovery process and the actual chronology of events submitted, including failed events and our thoughts about the failures.

Sample Question: Define the function all-pairs recursively so that (all-pairs imax jmax) creates a list of all pairs (i . j) where 1 <= i <= imax and 1 <= j <= jmax. Then define the loop$ version of all-pairs and prove it is equivalent to all-pairs. Both versions must be guard verified.

Sample Solution (as a narrative of the discovery).

As usual, we make sure we're operating in a session where

(include-book "projects/apply/top" :dir :system)

We will construct our pairs with

(defun make-pair (i j)
  (declare (xargs :guard t))
  (cons i j))

Here is our recursive definition. It involves two helper functions. All-pairs-helper2 keeps i fixed and runs j from 1 to jmax to compute the list of pairs ((i . 1) (i . 2) ... (i . jmax)). All-pairs-helper1 just calls the former helper for each i from 1 to imax and appends the lists together. The top-level all-pairs calls all-pairs-helper1 with i properly initialized to 1.

(defun all-pairs-helper2 (i j jmax)
  (declare (xargs :measure (nfix (- (+ (nfix jmax) 1) (nfix j)))
                  :guard (and (natp i) (natp j) (natp jmax))))
  (let ((j (nfix j))
        (jmax (nfix jmax)))
    (cond
     ((> j jmax) nil)
     (t (cons (make-pair i j)
              (all-pairs-helper2 i (+ 1 j) jmax))))))

(defun all-pairs-helper1 (i imax jmax)
  (declare (xargs :measure (nfix (- (+ (nfix imax) 1) (nfix i)))
                  :guard (and (natp i) (natp imax) (natp jmax))))
  (let ((i (nfix i))
        (imax (nfix imax)))
    (cond
     ((> i imax) nil)
     (t (append (all-pairs-helper2 i 1 jmax)
                (all-pairs-helper1 (+ 1 i) imax jmax))))))

(defun all-pairs (imax jmax)
  (declare (xargs :guard (and (natp imax) (natp jmax))))
  (all-pairs-helper1 1 imax jmax))

Here is a simple test.

ACL2 !>(all-pairs 2 4)
((1 . 1)
 (1 . 2)
 (1 . 3)
 (1 . 4)
 (2 . 1)
 (2 . 2)
 (2 . 3)
 (2 . 4))

And here is our first attempt to define the loop$ version, which is considerably “simpler” (or, at least, shorter). But this will fail! Can you say why without reading the error message?

(defun all-pairs-loop$ (imax jmax)
  (declare (xargs :guard (and (natp imax) (natp jmax))))
  (loop$ for i from 1 to imax
         append
         (loop$ for j from 1 to jmax
                collect (make-pair i j)))))

ACL2 Error [Translate] in ( DEFUN ALL-PAIRS-LOOP$ ...):  The body of
a LAMBDA object, lambda$ term, or loop$ statement should be fully badged
but MAKE-PAIR is used in
((LAMBDA (I J) (MAKE-PAIR I J)) (CAR LOOP$-GVARS) (CAR LOOP$-IVARS))
and has no badge. ...
... Note:  this error occurred in the context
(LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)
         (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOOP$-GVARS)
                                     (EQUAL # 1)
                                     (TRUE-LISTP LOOP$-IVARS)
                                    (EQUAL # 1))))
         (LET ((I (CAR LOOP$-GVARS))
               (J (CAR LOOP$-IVARS)))
              (DECLARE (IGNORABLE I J))
              (MAKE-PAIR I J))).

The error message above includes some extraneous possible explanation of the error which we've omitted.

The error tells us we forgot to assign a badge to make-pair. We could call (defbadge make-pair) at this point. But since we intend to prove things about all-pairs-loop$ we'll actually need the warrant for the make-pair, since make-pair is user-defined and is used in the body of a loop$. So we'll go ahead and create the warrant.

(defwarrant make-pair)

(Had we just badged make-pair at this point and proceeded another error message would crop up in due course and tell us to warrant it.)

Trying the defun again causes another failure with the checkpoint shown below.

(defun all-pairs-loop$ (imax jmax)
  (declare (xargs :guard (and (natp imax) (natp jmax))))
  (loop$ for i from 1 to imax
         append
         (loop$ for j from 1 to jmax
                collect (make-pair i j)))))

*** Key checkpoint at the top level: ***

Subgoal 1.2'
(IMPLIES (AND (CONSP LOOP$-IVARS)
              (NOT (CDR LOOP$-IVARS))
              (CONSP LOOP$-GVARS)
              (NOT (CDR LOOP$-GVARS)))
         (INTEGERP (CAR LOOP$-GVARS)))

ACL2 Error [Failure] in ( DEFUN ALL-PAIRS-LOOP$ ...):  The proof of
the guard conjecture for ALL-PAIRS-LOOP$ has failed; see the discussion
above about :VERIFY-GUARDS and :GUARD-DEBUG.  See :DOC failure.

We need to prove, as part of the guard verification, that (CAR LOOP$-GVARS) is an integer. At this point we might want to refresh our idea of what the formal semantics of that nested loop$ is!

We do not recommend using :trans for that refreshment! You can try it and you'll see 67 lines of output with a lot of extra stuff in it used to help evaluate such forms efficiently. Instead we'll use :tca (“translate, clean, and annotate”) which produces about half as much output and shows the original form of each loop$ together with formal semantics, complete with :guard declarations on the LAMBDA objects and correspondences between the variable names used in the original statement with the components of the formals LOOP$-GVARS and LOOP$-IVARS in the lambda$ terms generated.

(Note: We have manually inserted some comments to identify certain lines of the display below.)

ACL2 !>:tca (loop$ for i from 1 to imax
                   append
                   (loop$ for j from 1 to jmax
                          collect (make-pair i j)))
(PROG2$
  '(LOOP$ FOR I FROM 1 TO IMAX
          APPEND
          (LOOP$ FOR J FROM 1 TO JMAX
                 COLLECT (MAKE-PAIR I J)))
  (APPEND$+                                                      ; [0]
   (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)                            ; [1]
     (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOOP$-GVARS)        ; [2]
                                 (EQUAL (LEN LOOP$-GVARS) 1)
                                 (TRUE-LISTP LOOP$-IVARS)
                                 (EQUAL (LEN LOOP$-IVARS) 1))
                     :SPLIT-TYPES T))
     (LET ((JMAX (CAR LOOP$-GVARS))                              ; [3]
           (I (CAR LOOP$-IVARS)))
       (PROG2$
        '(LOOP$ FOR J FROM 1 TO JMAX COLLECT (MAKE-PAIR I J))
        (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) 1))
                           :SPLIT-TYPES T))
           (LET ((I (CAR LOOP$-GVARS))
                 (J (CAR LOOP$-IVARS)))
             (MAKE-PAIR I J)))
         (LIST I)
         (LOOP$-AS (LIST (FROM-TO-BY 1 JMAX 1)))))))             ; [4]
   (LIST JMAX)                                                   ; [5]
   (LOOP$-AS (LIST (FROM-TO-BY 1 IMAX 1)))))                     ; [6]

We're trying to verify the guards all the functions in that expression, and we have the :guard in the defun of all-pairs-loop$ to work with. That :guard is (and (natp imax) (natp jmax)).

So what functions above require an argument to be an integer? Hint: There is only one such function but it occurs in two places.

From-to-by requires all three of its arguments to be integers and that function appears on lines [4] and [6]. Line [4] requires jmax to be an integer and line [6] requires imax to be an integer. But line [6] is the formal term representing the “from 1 to imax” range of the append loop$ formalized with the fancy scion APPEND$+ at line [0]. That imax is literally the first formal variable of the defun of all-pairs-loop$ whose :guard says imax and jmax are a naturals. So [6] is not the problem.

The jmax in line [4], on the other hand, is actually a let-bound variable (see line [3]) within the lambda object (line [1]) that is the body of the append loop$ [line 0]. jmax is bound inside that lambda on line [3] to (car loop$-gvars) and the :guard (line [2]) of that lambda does not require (car loop$-gvars) to be an integer. We need to add that requirement to [2].

So how do we change the :guard of a lambda generated by the translation of the append loop$? We add “:guard (natp jmax)” after the append operator. (Note that (integerp jmax) would suffice here but we added the stronger condition ensured by the all-pairs-loop$'s guard.)

Using :tca again on the modified loop$ confirms our change.

ACL2 !>:tca (loop$ for i from 1 to imax
                        append
                        :guard (natp jmax)                   ; [new]
                        (loop$ for j from 1 to jmax
                               collect (make-pair i j)))
(PROG2$
  '(LOOP$ FOR I FROM 1 TO IMAX
          APPEND
          (LOOP$ FOR J FROM 1 TO JMAX
                 COLLECT (MAKE-PAIR I J)))
  (APPEND$+                                                  ; [0]
   (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)                        ; [1]
     (DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOOP$-GVARS)    ; [2']
                                 (EQUAL (LEN LOOP$-GVARS) 1)
                                 (TRUE-LISTP LOOP$-IVARS)
                                 (EQUAL (LEN LOOP$-IVARS) 1)
                                 (NATP (CAR LOOP$-GVARS)))   ; [new]
                     :SPLIT-TYPES T))
     (LET ((JMAX (CAR LOOP$-GVARS))                          ; [3]
           (I (CAR LOOP$-IVARS)))
       (PROG2$
        '(LOOP$ FOR J FROM 1 TO JMAX COLLECT (MAKE-PAIR I J))
        (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) 1))
                           :SPLIT-TYPES T))
           (LET ((I (CAR LOOP$-GVARS))
                 (J (CAR LOOP$-IVARS)))
             (MAKE-PAIR I J)))
         (LIST I)
         (LOOP$-AS (LIST (FROM-TO-BY 1 JMAX 1)))))))         ; [4]
   (LIST JMAX)                                               ; [5]
   (LOOP$-AS (LIST (FROM-TO-BY 1 IMAX 1)))))                 ; [6]

Observe the difference between the :guard on the original line [2] and the :guard on the new line [2']. The latter includes (natp (car loop$-gvars)).

If we think in terms of scions, we're saying “Every time this lambda object is applied, its two formals must satisfy the conjunction beginning at line [2'].”

Finally, how do we know every application of the lambda by the fancy scion append$+ (line [0]) will satisfy this guard? We know from the definition of append$+ that every application supplies the (list jmax) from line [5] as the value of loop$-gvars. That occurrence of jmax is at the top-level of the body and in the scope of the guard of all-pairs-loop$, which says jmax is a natural. So the guards can be proved now.

So now we can admit and verify the guards of our loop$ version of all-pairs.

(defun all-pairs-loop$ (imax jmax)
  (declare (xargs :guard (and (natp imax) (natp jmax))))
  (loop$ for i from 1 to imax
         append
         :guard (natp jmax)
         (loop$ for j from 1 to jmax
                collect (make-pair i j))))

Our goal is to prove the theorem below. We use The-Method, with which we assume you're familiar but which we narrate below.

First we try to prove our main goal. It fails with the checkpoint shown.

(defthm main
  (implies (and (natp imax)
                (natp jmax))
           (equal (all-pairs-loop$ imax jmax)
                  (all-pairs imax jmax)))))

*** Key checkpoint at the top level: ***

Goal''
(IMPLIES
 (AND (INTEGERP IMAX)
      (<= 0 IMAX)
      (INTEGERP JMAX)
      (<= 0 JMAX))
 (EQUAL
  (APPEND$+
   (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)
            (COLLECT$+ (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)
                                (CONS (CAR LOOP$-GVARS)
                                      (CAR LOOP$-IVARS)))
                       (LIST (CAR LOOP$-IVARS))
                       (LOOP$-AS (LIST (FROM-TO-BY 1 (CAR LOOP$-GVARS) 1)))))
   (LIST JMAX)
   (LOOP$-AS (LIST (FROM-TO-BY 1 IMAX 1))))
  (ALL-PAIRS-HELPER1 1 IMAX JMAX)))

Looking at the conclusion we see need to prove that the append$+ term is equal to the all-pairs-helper1 term. From our ACL2 experience with recursive functions like all-pairs-helper1 we know this is an inductive proof. But no induction is suggested by (all-pairs-helper1 1 imax jmax) because the constant 1 is in a controller position. We need to generalize the 1 by replacing it with i0, a general initial value of i. Note that we replace the 1 in two places, namely, the first 1 in (loop$-as (list (from-to-by 1 imax 1))), and the 1 in (all-pairs-helper1 1 imax jmax). Those two 1s are the concrete initial values of two i counters on opposite sides of the equality. There are three other occurrences of the number 1 in the conjecture. The first one is the initial value of the variable j, the second is the step size for counting up from j to jmax, and the third one is the step size for counting up from i to imax. We do not change those three occurrences of i.

We submit the proposed generalization as lemma1. The conclusion of lemma1 is exactly the equality conclusion above except for the replacement of those two 1s by the new variable i0. The hypothesis of lemma1 requires all the variables to be naturals. But the proof attempt fails! The checkpoint is shown below.

(defthm lemma1
  (implies
   (and (natp imax)
        (natp jmax)
        (natp i0))
   (equal
    (append$+
     (lambda$ (loop$-gvars loop$-ivars)
              (collect$+ (lambda$ (loop$-gvars loop$-ivars)
                                  (cons (car loop$-gvars)
                                        (car loop$-ivars)))
                         (list (car loop$-ivars))
                         (loop$-as (list (from-to-by 1 (car loop$-gvars) 1)))))
     (list jmax)
     (loop$-as (list (from-to-by i0 imax 1))))
    (all-pairs-helper1 i0 imax jmax)))))

*** Key checkpoint under a top-level induction: ***

Subgoal *1/6''
(IMPLIES
 (AND
  (<= I0 IMAX)
  (EQUAL
   (APPEND$+
       (LAMBDA$
            (LOOP$-GVARS LOOP$-IVARS)
            (COLLECT$+ (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)
                                (CONS (CAR LOOP$-GVARS)
                                      (CAR LOOP$-IVARS)))
                       (LIST (CAR LOOP$-IVARS))
                       (LOOP$-AS (LIST (FROM-TO-BY 1 (CAR LOOP$-GVARS) 1)))))
       (LIST JMAX)
       (LOOP$-AS (LIST (FROM-TO-BY (+ 1 I0) IMAX 1))))
   (ALL-PAIRS-HELPER1 (+ 1 I0) IMAX JMAX))
  (INTEGERP IMAX)
  (<= 0 IMAX)
  (INTEGERP JMAX)
  (<= 0 JMAX)
  (INTEGERP I0)
  (<= 0 I0))
 (EQUAL (APPEND (COLLECT$+ (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)
                                    (CONS (CAR LOOP$-GVARS)
                                          (CAR LOOP$-IVARS)))
                           (LIST I0)
                           (LOOP$-AS (LIST (FROM-TO-BY 1 JMAX 1))))
                (ALL-PAIRS-HELPER1 (+ 1 I0) IMAX JMAX))
        (APPEND (ALL-PAIRS-HELPER2 I0 1 JMAX)
                (ALL-PAIRS-HELPER1 (+ 1 I0) IMAX JMAX))))

Notice that we're trying to prove something of the form

(EQUAL (APPEND a1 b1)
       (APPEND a2 b2))

where b1 and b2 are identical. So we will prove (EQUAL a1 a2).

But again, this is inductive. The (from-to-by 1 jmax 1) and the (all-pairs-helper2 i0 1 jmax) are both counting up from 1 as the initial value of j. We need to generalize those 1s to j0. So we submit the following as lemma2. And it succeeds!

(defthm lemma2
  (implies (and (natp imax)
                (natp jmax)
                (natp i0)
                (natp j0))
           (equal (collect$+ (lambda$ (loop$-gvars loop$-ivars)
                                      (cons (car loop$-gvars)
                                            (car loop$-ivars)))
                             (list i0)
                             (loop$-as (list (from-to-by j0 jmax 1))))
                  (all-pairs-helper2 i0 j0 jmax))))

So now we return to lemma1, whose checkpoint suggested lemma2. But it fails again, this time with a different checkpoint

(defthm lemma1
  (implies
   (and (natp imax)
        (natp jmax)
        (natp i0))
   (equal
    (append$+
     (lambda$ (loop$-gvars loop$-ivars)
              (collect$+ (lambda$ (loop$-gvars loop$-ivars)
                                  (cons (car loop$-gvars)
                                        (car loop$-ivars)))
                         (list (car loop$-ivars))
                         (loop$-as (list (from-to-by 1 (car loop$-gvars) 1)))))
     (list jmax)
     (loop$-as (list (from-to-by i0 imax 1))))
    (all-pairs-helper1 i0 imax jmax)))))

*** Key checkpoint at the top level: ***

[1]Goal
(APPLY$-WARRANT-COLLECT$+)

Note that this checkpoint comes from a forcing round (the clue is the “[1] prefix to the Goal), which means the proof succeeded except for some hypotheses that were forced so that certain lemmas could fire and now have to be proved. But the hypothesis above is the warrant for collect$+. We need the warrant for collect$+ because that function is being applied with apply$ every time append$+ iterates. This is easy to fix. We just add the warrant as a hypothesis to lemma1.

(defthm lemma1
  (IMPLIES
   (AND (warrant collect$+)
        (natp imax)
        (natp jmax)
        (natp i0))
   (equal
    (append$+
     (lambda$ (loop$-gvars loop$-ivars)
              (collect$+ (lambda$ (loop$-gvars loop$-ivars)
                                  (cons (car loop$-gvars)
                                        (car loop$-ivars)))
                         (list (car loop$-ivars))
                         (loop$-as (list (from-to-by 1 (car loop$-gvars) 1)))))
     (list jmax)
     (loop$-as (list (from-to-by i0 imax 1))))
    (all-pairs-helper1 i0 imax jmax))))

This proof succeeds.

So now we return to main. By the way, because we expect the theorem to be proved by applying lemma1, we provide the hint that tells the prover not to even try induction. This just reduces the output if the proof fails.

Unfortunately this attempt fails, but with two easy-to-fix checkpoints.

(defthm main
  (implies (and (natp imax)
                (natp jmax))
           (equal (all-pairs-loop$ imax jmax)
                  (all-pairs imax jmax)))
  :hints (("Goal" :do-not-induct t))))

*** Key checkpoints at the top level: ***

[1]Subgoal 2
(APPLY$-WARRANT-MAKE-PAIR)

[1]Subgoal 1
(APPLY$-WARRANT-COLLECT$+)

Note that the checkpoints are forcing round subgoals showing that we need two warrants. So we add both warrants to main's hypotheses. And we're done.

(defthm main
  (implies (and (warrant collect$+ make-pair)
                (natp imax)
                (natp jmax))
           (equal (all-pairs-loop$ imax jmax)
                  (all-pairs imax jmax)))
  :hints (("Goal" :do-not-induct t)))

Note: The :do-not-induct hint could be deleted because the theorem is proved without appealing to induction anyway.

You might wonder why we need the warrant on make-pairs. It never arose in any checkpoint except in the very last failed proof.

The first time we tried to prove main we failed, and got this checkpoint.

Goal''
(IMPLIES
 (AND (INTEGERP IMAX)
      (<= 0 IMAX)
      (INTEGERP JMAX)
      (<= 0 JMAX))
 (EQUAL
  (APPEND$+
   (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)
            (COLLECT$+ (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)
                                (CONS (CAR LOOP$-GVARS)
                                      (CAR LOOP$-IVARS)))
                       (LIST (CAR LOOP$-IVARS))
                       (LOOP$-AS (LIST (FROM-TO-BY 1 (CAR LOOP$-GVARS) 1)))))
   (LIST JMAX)
   (LOOP$-AS (LIST (FROM-TO-BY 1 IMAX 1))))
  (ALL-PAIRS-HELPER1 1 IMAX JMAX)))

The innermost lambda$ is the body of the innermost loop$ statement, (loop$ for j from 1 to jmax collect (make-pair i j)), except it has been simplified by the expansion of (make-pair i j) to (cons i j). That expansion of make-pair inside a lambda$ required the warrant for make-pair and that was forced to produce the cons.

Had that first proof attempt at main succeeded except for that forced subgoal, a forcing round would have brought to our attention the need for the warrant on make-pair. But that proof attempt failed because the prover could not do a suitable induction to prove Goal''. Indeed, that is what led us to lemma1.

But forced subgoals are not reported if the proof fails for other reasons. So we were left unaware that we were depending on the warrant for make-pair. In the penultimate failed proof main just above, the same forced expansion of make-pair occurred and this time the proof succeeded except for the forced subgoals requiring warrants for make-pair and collect$+. That finally brought the make-pair expansion to our attention.

The more experienced ACL2 user would have noticed (indeed, did notice!) the expansion of make-pair in Goal'' above and understood the warrant for make-pair was needed but wanted to see what would happen if that fact was overlooked.

The final series of events to solve this problem is shown below.

; Include standard apply$ book.
(include-book "projects/apply/top" :dir :system)}

; Define and verify the guards of the recursive all-pairs.
(defun make-pair (i j)
  (declare (xargs :guard t))
  (cons i j))

(defun all-pairs-helper2 (i j jmax)
  (declare (xargs :measure (nfix (- (+ (nfix jmax) 1) (nfix j)))
                  :guard (and (natp i) (natp j) (natp jmax))))
  (let ((j (nfix j))
        (jmax (nfix jmax)))
    (cond
     ((> j jmax) nil)
     (t (cons (make-pair i j)
              (all-pairs-helper2 i (+ 1 j) jmax))))))

(defun all-pairs-helper1 (i imax jmax)
  (declare (xargs :measure (nfix (- (+ (nfix imax) 1) (nfix i)))
                  :guard (and (natp i) (natp imax) (natp jmax))))
  (let ((i (nfix i))
        (imax (nfix imax)))
    (cond
     ((> i imax) nil)
     (t (append (all-pairs-helper2 i 1 jmax)
                (all-pairs-helper1 (+ 1 i) imax jmax))))))

(defun all-pairs (imax jmax)
  (declare (xargs :guard (and (natp imax) (natp jmax))))
  (all-pairs-helper1 1 imax jmax))

; Warrant make-pair so we can use it in a loop$.
(defwarrant make-pair)

; Define and verify the guards of the loop$ version.
(defun all-pairs-loop$ (imax jmax)
  (declare (xargs :guard (and (natp imax) (natp jmax))))
  (loop$ for i from 1 to imax
         append
         :guard (natp jmax)
         (loop$ for j from 1 to jmax
                collect (make-pair i j))))

; Prove that the generalized inner loop$ is all-pairs-helper2.
(defthm lemma2
  (implies (and (natp imax)
                (natp jmax)
                (natp i0)
                (natp j0))
           (equal (collect$+ (lambda$ (loop$-gvars loop$-ivars)
                                      (cons (car loop$-gvars)
                                            (car loop$-ivars)))
                             (list i0)
                             (loop$-as (list (from-to-by j0 jmax 1))))
                  (all-pairs-helper2 i0 j0 jmax))))

; Prove that the generalized outer loop$ is all-pairs-helper1.
(defthm lemma1
  (implies
   (and (warrant collect$+)
        (natp imax)
        (natp jmax)
        (natp i0))
   (equal
    (append$+
     (lambda$ (loop$-gvars loop$-ivars)
              (collect$+ (lambda$ (loop$-gvars loop$-ivars)
                                  (cons (car loop$-gvars)
                                        (car loop$-ivars)))
                         (list (car loop$-ivars))
                         (loop$-as (list (from-to-by 1 (car loop$-gvars) 1)))))
     (list jmax)
     (loop$-as (list (from-to-by i0 imax 1))))
    (all-pairs-helper1 i0 imax jmax))))

; Main theorem
(defthm main
  (implies (and (warrant collect$+ make-pair)
                (natp imax)
                (natp jmax))
           (equal (all-pairs-loop$ imax jmax)
                  (all-pairs imax jmax))))

Now go to lp-section-12 (or return to the Table of Contents).