Challenge Problems about

The questions below ask you to write and evaluate some

Our answers to the problems in this section are in community-books
file

Don't forget to start your session by including the standard book for

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

Don't bother with adding

Let a “bag” be a true list of symbols. The function below returns a
constant list of bags. You may use

(defun bags () '((a b c) (d x e f) (g h i x) (j) (x k l)))

Here is a sample question and how you might check that your

Sample Question: Build an alist that pairs the first symbol in every bag
of

Sample Check of a Solution:

(equal (loop$ for bag in (bags) collect (cons (car bag) (len (cdr bag)))) '((A . 2) (D . 3) (G . 3) (J . 0) (X . 2)))

Of course, you could just type the

(defthm check-sample-question (equal (loop$ for bag in (bags) collect (cons (car bag) (len (cdr bag)))) '((A . 2) (D . 3) (G . 3) (J . 0) (X . 2))) :rule-classes nil)

However, if your

(defun my-len (x) (if (atom x) 0 (+ 1 (my-len (cdr x))))) (defwarrant my-len) (defthm check-my-sample-question (implies (warrant my-len) (equal (loop$ for bag in (bags) collect (cons (car bag) (my-len (cdr bag)))) '((A . 2) (D . 3) (G . 3) (J . 0) (X . 2)))) :rule-classes nil)——————————

**LP6-1:** Concatenate all the bags in

**Expected Value:**

**LP6-2:** Collect the bags that contain the symbol

**Expected Value:**

**LP6-3:** If you used some version of

**Expected Value:**

Don't use any version of

**LP6-4:** Remove all the

**Expected Value:**

**LP6-5:** Collect the first symbol of each of the bags in

**Expected Value:**

**LP6-6:** From each bag in

**Expected Value:**

**LP6-7:** Let's say the “alternating sum of signed squares” of a
list of numbers is the sum of the squares of the elements, except the squares
of elements in even positions (0-based) are added and the squares in odd
positions are subtracted. So the alternating sum of signed squares of

**Expected Value:**

**LP6-8:** Collect all the function symbols in the current ACL2
world with an arity greater than 9.

Three Hints: First, the term `state` may
not be used in `let` bind

Second, every `rune` returned by

Third, the arity of a symbol

**Expected Value:** As of ACL2 Version 8.5 (after including the

**LP6-9:** Collect the name of every theorem about

Three More Hints: First, the ACL2 world is a list of triples of the form

Second, each event that named a theorem has a triple of the form

Third, the ACL2 term

**Expected Value:** As of ACL2 Version 8.5 (after including the

These exercises highlight three important lessons about

The first is that with

The second is that it is not always a good idea to “inline”

Another example of this second lesson is in question LP6-7. Depending on
the project at hand, the notion of “alternating sum of signed squares”
might be a useful one in its own right. So perhaps if such a problem came up
you might define

(alternating-sum-of-signed-squares (loop$ for bag in (bags) collect (len bag)))

to compute the quantity requested in LP6-7.

The question raised by this second lesson isn't so much whether you use a
*if the concept has a natural
name, define it!*

Of course, there is the usual trade-off between execution efficiency and
modularity. There are various ways to deal with this trade-off in ACL2 but
since they are not unique to

The third lesson is highlighted by LP6-8 and LP6-9.

Now go to lp-section-7 (or return to the