		Search-engine friendly clone of the ACL2 documentation.

Loop$-primer

Lp-section-17

Challenge Proof Problems for DO Loop$s

LP17: Challenge Proof Problems for DO Loop$s

In the following problems please write DO loop$s even though some of the problems can be solved with FOR loop$s.

Our answers to the problems in this section are in community-books file demos/loop-primer/lp17.lisp.

——————————

LP17-1: Write a DO loop$ that reverses the list lst. For example, if lst is (A B C) the result should be (C B A). Prove that your DO loop$ is equal to (rev lst), where

(defun rev (x)
  (if (endp x)
      nil
      (append (rev (cdr x)) (list (car x)))))

——————————

LP17-2: Write a DO loop$ that computes (member e lst) and prove it correct.

Hint: Sometimes the main theorem suggests the right induction on its own.

——————————

LP17-3: Prove the following:

(defthm lp17-3-main
  (equal (loop$ with x = lst
                with ans = 0
                do
                 (cond ((endp x) (return ans))
                       (t (progn (setq ans (+ 1 ans))
                                 (setq x (cdr x))))))
         (len lst)))

——————————

LP17-4: Write a DO loop$ that computes (nth n lst), when n is a natural number. Prove it correct.

——————————

LP17-5: Prove the following.

(defthm lp17-5-main
  (implies (true-listp lst)
           (equal (loop$ with x = lst
                         with ans = nil
                         do
                         (cond
                          ((endp x) (return ans))
                          (t (progn (setq ans (append ans (list (car x))))
                                    (setq x (cdr x))))))
                  lst)))

——————————

LP17-6: Prove the following.

(defthm lp17-6-main
  (implies (and (natp m)
                (natp n))
           (equal (loop$ with i = m
                         with j = n
                         do
                         (if (zp i)
                             (return j)
                             (progn (setq i (- i 1))
                                    (setq j (+ j 1)))))
                  (+ m n))))

——————————

LP17-7: Write a DO loop$ that computes (fact n), for natural number n, where

(defun fact (n)
  (if (zp n)
      1
      (* n (fact (- n 1)))))

——————————

LP17-8: Write a DO loop$ that scans a list of numbers, lst, once and returns the sum of the elements and the sum of the squares (with sq as defined below) of the elements of lst as a cons pair. E.g., given (1 2 3 4 5) return (cons (+ 1 2 3 4 5) (+ (sq 1) (sq 2) (sq 3) (sq 4) (sq 5))) = (15 . 55).

Prove that your do loop$ is equal to

(cons (loop$ for e in lst sum e)
      (loop$ for e in lst sum (sq e)))

Use the following definition of sq.

(defun sq (x) (* x x))

——————————

LP17-9: Define (partition-symbols lst) with a DO loop$ that partitions lst into two lists, one containing all the symbols in lst and the other containing all the non-symbols. Return the cons of the two partitions and prove partition-symbols correct.

Hint: Since you are likely to collect the elements in reverse order, a suitable specification for these purposes is that partition-symbols is equal to

(cons (rev (loop$ for e in lst when (symbolp e) collect e))
      (rev (loop$ for e in lst when (not (symbolp e)) collect e)))

——————————

LP17-10: Write a DO loop$ that returns the list of naturals from n down to 0, where n is a natural. For example, if n is 10 the answer is (10 9 8 7 6 5 4 3 2 1 0). Prove that when n is a natural, your DO loop$ returns the same thing as (loop$ for i from 0 to n collect (- n i)).

Hints: Remember that in order for your “lemma1” to be applied in the proof of your main theorem it must match the rewritten lambda objects of the main theorem. We've focused on matching the do-body lambda. But it must also match the measure lambda. So when you formulate your “lemma1”, pay attention to how your measure term normalizes under rewrite. And by the way, if you use non-recursive functions in a term and you don't want them opened up when the lambda objects are rewritten in the main theorem, try disabling them. (Some non-recursive functions cannot be disabled. But another workaround is to define the whole measure as a function and disable it when appropriate.)

——————————

LP17-11: Define (all-pairs-do-loop$ imax jmax) to compute the same (all-pairs imax jmax) as was defined in section 11 (and below). But use DO loop$s instead of FOR loop$s in your definition of all-pairs-do-loop$. Below we comment on what you should prove.

The definition of all-pairs was as follows.

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

(defwarrant make-pair)

(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))

Hints: In following our advice on proving do loop$s you will define functions that compute the same things as your DO loop$s. In our solution we called these two functions apdh1 and apdh2, where “apdh” stands for @ldquo;all-pairs-do-helper”. You will prove two “lemma1” theorems, one for each loop$. The second of those theorems will establish allow you to prove that your all-pairs-do-loop$ is apdh1.

The next step in our recipe is to prove that the apdh1 is all-pairs as above. This will not involve loop$s of any sort. It's just a normal proof about the relation between some recursively defined functions. But we found this step surprisingly challenging!

Since that second step does not involve loop$s, you may consider your answer correct if you just prove the two “lemma1” theorems! But if you want a non-loop$ challenge, finish the proof all the way to all-pairs.

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