		Search-engine friendly clone of the ACL2 documentation.

Loop$-primer

Lp-section-12

Challenge Proof Problems about FOR Loop$s

LP12: Challenge Proof Problems about FOR Loop$s

If you have not already, warm up by proving the correctness of your solutions to the problems in lp-section-8.

Remember to operate in a session in which you have included the standard loop$ book.

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

Our answers to the problems in lp-section-8 are in community-books file demos/loop-primer/lp8.lisp, and our answers to the problems below are in community-books file demos/loop-primer/lp12.lisp.

——————————

LP12-1 Define (assoc-equal-loop$ x alist) to be equal to (assoc-equal x alist) when (alistp alist). Verify the guards of assoc-equal-loop$ and prove that your function satisfies the specification above. Is your function in fact unconditionally equal to assoc-equal? If so, prove it; if not, show a counterexample.

——————————

LP12-2 Under what conditions is the following a theorem? Fill in the blank and prove the theorem.

(defthm LP12-2
  (implies ...
           (equal (loop$ for x in keys as y in vals collect (cons x y))
                  (pairlis$ keys vals)))
  :rule-classes nil)

——————————

LP12-3 Prove

(defthm LP12-3
  (equal (* 2 (len (loop$ for tl on lst append tl)))
         (* (len lst) (+ (len lst) 1))))

Hint: By phrasing the challenge with the multiplication by 2 on the left-hand side, we produce a conjecture that can be proved (perhaps with a few lemmas) without the need for “heavy duty” arithmetic books. Had we divided by 2 on the right-hand side, we'd have brought division into the problem which we intentionally avoided. You will still need a lemma or two, discoverable by The Method.

——————————

LP12-4 Define

(defun nats (n)
  (cond ((zp n) (list 0))
        (t (append (nats (- n 1)) (list n)))))

and prove that the obvious loop$ statement is equivalent to (nats n) when n is a natural. Make your defthm have :rule-classes nil so as not to interfere with your work on the next problem.

——————————

LP12-5 Define

(defun nats-up (i n)
  (declare (xargs :measure (nfix (- (+ (nfix n) 1) (nfix i)))))
  (let ((i (nfix i))
        (n (nfix n)))
    (cond ((> i n) nil)
          (t (cons i (nats-up (+ i 1) n))))))

Prove

(defthm LP12-5
  (implies (natp n)
           (equal (loop$ for i from 0 to n collect i)
                  (nats-up 0 n)))
  :rule-classes nil)

——————————

LP12-6 Fill in the blanks below and prove the theorem. You may need hints. If not, just delete the :hints setting.

(defthm LP12-6
  (implies (true-listp lst)
           (equal (loop$ ...)
                  (strip-cars lst)))
  :hints ...
  :rule-classes nil)

——————————

LP12-7 Prove the following, adding hints if necessary. Otherwise, just delete the :hints setting.

(defthm LP12-7
  (loop$ for pair in (loop$ for key in keys
                            as  val from 0 to (+ (len keys) -1)
                            collect (cons key val))
         always (integerp (cdr pair)))
  :hints ...)

——————————

LP12-8 Fill in the blanks below and then prove the theorem. You may need hints. If not, just delete the :hints setting.

(defthm LP12-8
  (implies (natp n)
           (equal (loop$ ...)
                  (nth n lst)))
  :hints ...
  :rule-classes nil)

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