`(reverse xs)`

is a built-in function that takes a list and returns a list with
all of the elements in the opposite order. We’ll be defining another version of
it called `rev`

.

In order to define a recursive function in ACL2, we need to think about what it
would return in a couple of different cases. The first case is when the
argument, `xs`

, is empty (or `nil`

). The reverse of an empty list is just an
empty list:

Now, what if `xs`

is not empty? If it’s not empty, we can break it up into its
first element and the rest of the list, using `(first xs)`

and `(rest xs)`

,
respectively. We want to take these parts and assemble a new, reversed list. We
can just use `(rev (rest xs))`

to reverse the rest of the list, but what do we
do with `(first xs)`

?

Consider an example: `(rev (list 1 2 3 4 5))`

. After we split it up into two
parts, `1`

and `(list 2 3 4 5)`

, we can reverse the list part to get ```
(list 5 4
3 2)
```

. And what we want for the whole list is `(list 5 4 3 2 1)`

. So we need to
put `1`

at the end of the reversed list.

For `(put-at-end x xs)`

, we can use `(append)`

:

Putting it all together, we get:

Now that we have a good working definition for reverse, we need to test it to see that it works.

The quickest way to test a function you’ve defined is with the REPL. The REPL is
the part of Proof Pad below the definitions area. After you’ve typed the
definitions for `put-at-end`

and `rev`

into the main definitions area, type
`(rev (list 1 2 3 4 5))`

into the text field at the very bottom of Proof Pad,
and click “Run” (or press “Enter”). You instantly see the result, which is ```
(5 4
3 2 1)
```

.

We can automate this process to make sure that `rev`

continues to match our
expectations, even if we change or rewrite it. The simplest automatic test
provided by Proof Pad is `check-expect`

. To use it, first include the “testing”
book:

Now write a test like this:

`check-expect`

will automatically run the test and show a green bar to the left
when it passes. A test passes when the two arguments to `check-expect`

evaluate
to the same thing (in this case, the list `(5 4 3 2 1)`

).

We could write some more check-expect style tests, but they can only get us so far. It would be even better if we could write a test that will check several types of lists to see that our function does what we want. To do this, we need to write a property-style test. First, include the “doublecheck” book (DoubleCheck is the name of the testing library):

A doublecheck test has three parts: a name, a set of data generators, and a
body. The body is evaluated several times with different, randomly generated
data, and if it evaluates to `t`

(which is Lisp’s version of `true`

), then the
test passes. If a single case fails, the test fails.

One property we can test with DoubleCheck is that reversing a list twice gives you the same list you started with. I’ll start by showing the test, then talk about the parts:

The name of the test is `rev-rev-test`

. The name isn’t important, except that
each one has to be unique. This test has one generator. It generates values
called `xs`

, using the `(random-integer-list)`

generator. You can see what kinds
of values this generator returns by typing it in the REPL.

Finally, we have the body: we want to show that `(rev (rev xs))`

is equal to
just `xs`

.

To run the test, just paste it into the definitions area. It will run, and if it passes, a green bar will appear to the left of the test.

Try changing the `nil`

in the definition of `rev`

above to something else, like
`1`

. You can see that this makes the test fail. When a test fails, it shows you
which cases it failed on. In this case, it fails all cases, but it might help
you to diagnose the problem if only some of the cases fail too. When a test
fails, it’s often a good idea to go back to the REPL and try some of the failed
values to see what you get.

`rev-rev`

DoubleCheck properties are nice, but they aren’t perfect. They only test the types of values that you generate, and you might have a bug that impacts only a small subset of cases, which means the generated test cases are unlikely to expose the bug.

To strengthen our properties, we can run them through ACL2’s theorem prover to try to prove that it holds for all input values, not just the randomly selected ones that DoubleCheck uses.

In this case, our test as written will fail. The reason for the failure is that
it doesn’t quite hold for any value of `xs`

. In particular, to ACL2’s logic,
`(rev 1)`

= `nil`

. If you try to run `(rev 1)`

in the REPL, you’ll get a guard
error. Guards are restrictions on what values a function will take; in this
case, `(endp xs)`

expects a list, and we gave it a number. However, ACL2’s
internal logic will run the theorem just fine, with `(endp xs)`

returning `t`

when `xs`

is 1, making `(rev 1)`

return `nil`

.

In order to correct this, we need to add a hypothesis to our property:

This way, ACL2 will know to only concern itself with values that satisfy
`true-listp`

– values that are lists.

With this correction in place, you can run the property through ACL2’s logic by clicking on the green bar to the left of it. If everything has been entered correctly, ACL2 will succeed, and the bar will turn dark green (with a checkmark), indicating that the property has been proven correct.

The whole file so far is: