|
|
|---|
|
|
|
|---|
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 nils! 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.
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 nth 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: