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
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.
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:
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.