An Example of ACL2 in Use

To introduce you to ACL2 we will consider the app function discussed in the Common Lisp page, except we will omit for the moment the declare form, which in ACL2 is called a guard.

Guards are arbitrary ACL2 terms that express the ``intended domain'' of functions. In that sense, guards are akin to type signatures. However, Common Lisp and ACL2 are untyped programming languages: while the language supports several different data types and the types of objects can be determined by predicates at runtime, any type of object may be passed to any function. Thus, guards are ``extra-logical.'' Recognizing both the practical and intellectual value of knowing that your functions are applied to the kinds of objects you intend, ACL2 imposes guards on Common Lisp and provides a means of proving that functions are used as intended. But the story is necessarily complicated and we do not recommend it to the new user. Get used to the fact that any ACL2 function may be applied to any objects and program accordingly. Read about guards later.

Here is the definition again 

(defun app (x y)
  (cond ((endp x) y)
        (t (cons (car x) 
                 (app (cdr x) y)))))

The next few stops along the Walking Tour will show you 

  * how to use the ACL2 documentation,
  * what happens when the above definition is submitted to ACL2,
  * what happens when you evaluate calls of app,
  * what one simple theorem about app looks like,
  * how ACL2 proves the theorem, and
  * how that theorem can be used in another proof.
Along the way we will talk about the definitional principle, types, the ACL2 read-eval-print loop, and how the theorem prover works.

When we complete this part of the tour we will return briefly to the notion of guards and revisit several of the topics above in that context.