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:

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