Recursion and Induction: ACL2 Arithmetic

The techniques we have studied so far suffice to prove the most elementary facts of natural number arithmetic. In fact, we could conduct our entire study of recursion and induction in the domain of number theory. But it is more fun to deal with less familiar “data structures” where basic properties can be discovered. So we will skip past formal arithmetic with a few brief remarks.

ACL2 provides the numbers as a data type distinct from conses, symbols,
strings, and characters. They are not lists of `nil`s! The naturals are
among the integers, the integers are among the rationals, and the rationals
are among the ACL2 numbers. The complex rationals are also among the ACL2
numbers; in fact they are complex numbers whose real and imaginary parts are
rational and whose imaginary parts are non-`0`.

Here are a few commonly used functions in ACL2.

`(natp x)`- recognizes natural numbers`(integerp x)`- recognizes integers`(rationalp x)`- recognizes rationals`(zp x)`-`t`if x is`0`or not a natural;`nil`otherwise`(nfix x)`-`x`if`x`is a natural;`0`otherwise`(+ x y)`- sum of the numbers`x`and`y``(- x y)`- difference of the numbers`x`and`y``(* x y)`- product of the numbers`x`and`y``(/ x y)`- rational quotient of the numbers`x`and`y``(< x y)`- predicate recognizing that the number`x`is less than the number`y``(<= x y)`- predicate recognizing that the number`x`is less than or equal to the number`y`

The functions `+`, `-`, `*`, `/`, `<`,
and `<=` default their arguments to `0` in the sense that if
some argument is not an ACL2 number then `0` is used instead.

The predicate `zp` is commonly used in recursive definitions that treat
an argument as though it were a natural number and count it down to zero.

Here is a “definition” that accesses the `n`th element of a list,
treating `n` as a natural. (This definition is unacceptable under our
current Principle of Structural Recursion because `(consp x)` does not
rule the recursive call. We will return to this point momentarily.)

(defun nth (n x) (if (zp n) (car x) (nth (- n 1) (cdr x))))

Thus, `(nth 2 '(A B C D))` is `C`. `(Nth 0 '(A B C D))` is
`A`. Interestingly, `(nth -1 '(A B C D))` is also `A`, because
`-1` satisfies `zp`. Thus, we can use `nth` with any first
argument. (In ACL2, `nth` is defined differently, but equivalently.)

The numbers are axiomatized with the standard axioms for rational fields.
See

**Henceforth, you may use arithmetic freely in your proofs and assume any
theorem of ACL2 arithmetic. That is, you may assume any ACL2 theorem that
can be written with the function symbols described above and use it in
routine arithmetic simplification. But be careful about what you assume!**

For example, the following familiar arithmetic facts are not (quite) theorems:

(equal (+ x 0) x) ; Additive Identity (iff (equal (+ x y) (+ x z)) ; Additive Cancellation (equal y z))

Why aren't the formulas above theorems?

In addition, the following strange fact is a theorem:

(not (equal (* x x) 2))

That is, we can prove that the square root of 2 is not rational and hence not in ACL2.

(Maybe explore ACL2 arithmetic? You won't need ACL2 arithmetic libraries
to do the problems here. But that is good because there is probably not an
area of mathematics that the typical computer science student knows better
than arithmetic. Furthermore, you likely know much more about arithmetic than
ACL2 does when it is first fired up. Its performance can be improved by
including “certified books” of definitions and theorems about
arithmetic. The ACL2 Community Books Repository [4] contains thousands of
books created by the community. To load a book into an ACL2 session the
command <<`include-book`>> is used. But there are many
kinds of arithmetic books to choose from depending on what sort of operations
are involved in your conjectures. You might explore books on elementary
<<arithmetic>> including some number theory books, or books
on the arithmetic of <<bit-vectors>> (which deal with
concepts like shifting or bitwise logical operations on number), or floating
point books (see <<rtl>>; these are useful for verifying
implementations of floating point operations) or a book on the <<gl>> utility (which provides a bit-blaster for finite arithmetic), or
<<algebra>> books (e.g., properties of rings and fields),
to name a few.)

Next: