		Search-engine friendly clone of the ACL2 documentation.

Basic-tutorial

8. Exercises

Here are some exercises you can use to get some experience with using GL.

These exercises will get you into some rough spots, so that you can learn how to get out. If you get stuck, you can see our solutions in the file centaur/gl/solutions.lsp.

We recommend trying to carry out these exercises in a new file. You will probably want to start your file with:

(in-package "ACL2")
(include-book "centaur/gl/gl" :dir :system)

At certain points in the exercises, we assume your computer has at least 8 GB of memory.

Arithmetic Exercises

1a. Use GL to prove that addition commutes for 4-bit unsigned numbers:

(implies (and (unsigned-byte-p 4 x)
              (unsigned-byte-p 4 y))
         (equal (+ x y) (+ y x)))

1b. Carry out the same proof as in 1a, but construct your G-bindings:

Using auto-bindings
Using g-int
"Manually", without using either of these.

Hints: you may want to consult 6. Writing :g-bindings forms and shape-specs.

1c. Extend your proof from 1a to 20-bit numbers. How long does the proof take? How much memory did it use? Try the hons-summary command get a sense of the memory usage.

1d. In the same ACL2 session, undo your proof of 1c and submit it again. How long did it take this time? Can you explain what happened?

1e. Figure out how to optimize your G-bindings to make the proof in 1c go through quickly. For reliable timings, use clear-memoize-tables and hons-clear before each proof attempt. Implement your solution using both g-int and auto-bindings.

1f. Use GL to prove that addition commutes up to 3,000 bits. Hint: the debugging section might be able to help you.