This is documentation for ACL2 Version 4.3
Copyright (C) 2011  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

This manual documents ACL2 Version 4.3.

ABOUT-ACL2    about ACL2

This is ACL2 Version 4.3, copyright (C) 2011 University of Texas at
Austin, authored by Matt Kaufmann and J Strother Moore.

For past versions, see
`http://www.cs.utexas.edu/users/moore/acl2/current/other-releases.html'.

For statistics on ACL2 code size, see file doc/acl2-code-size.txt.

See DOCUMENTATION for how to access the user's manual.

See the home page at `http://www.cs.utexas.edu/users/moore/acl2/' for
additional information including tutorials, applications, mailing lists,
related publications, libraries, ACL2 workshops and seminars,
installation instructions, and acknowledgements.

See
`http://www.cs.utexas.edu/users/moore/acl2/current/installation/misc.html#License-and-Copyright'
for license and copyright information.

ACL2-TUTORIAL    tutorial introduction to ACL2

To learn about ACL2, read at least the following two links.

     * Industrial Applications of ACL2 (10 minutes) to help you
     understand what sophisticated users can do;

     * A Flying Tour (10 minutes) to get an overview of the system and
     what skills the user must have.

If you want to learn _how to use_ ACL2, we recommend that you read a
selection of the materials referenced below, depending on your learning
style, and do suggested exercises.

     * "A Walking Tour" (1 hour) provides an overview of the theorem
     prover.

     * "Introduction to the Theorem Prover" (10-40 hours) provides
     instruction on how to interact with the system.  Unlike the three
     documents above, this document expects you to _think_!  It cites
     the necessary background pages on programming in ACL2 and on the
     logic and then instructs you in The Method, which is how expert
     users use ACL2.  It concludes with some challenge problems for the
     ACL2 beginner (including solutions) and an FAQ.  Most users will
     spend several hours a day for several days working through this
     material.

     * The book "Computer-Aided Reasoning: An Approach" (see
     `http://www.cs.utexas.edu/users/moore/publications/acl2-books/car/index.html'
     is worth a careful read, as you work exercises and learn "The
     Method."

     * "Annotated ACL2 Scripts and Demos" contains relatively
     elementary proof scripts that have been annotated to help train
     the newcomer.

     * Many files ("books") in the books/ directory distributed with
     ACL2 are extensively annotated.  See the link to "Lemma Libraries
     and Utilities" on the ACL2 home page
     (`http://www.cs.utexas.edu/users/moore/acl2').

     * An "Alternative Introduction" document, while largely subsumed
     by the topic "Introduction to the Theorem Prover" mentioned above,
     still might be useful because it covers much of the tutorial
     material in a different way.

At this point you are probably ready to use ACL2 on your own _small_
projects.  A common mistake for beginners is to browse the
documentation and then try to do something that is too big!  Think of a
very small project and then simplify it!

Note that ACL2 has a very supportive user network.  See the link to
"Mailing Lists" on the ACL2 home page
(`http://www.cs.utexas.edu/users/moore/acl2').

The topics listed below are a hodge podge, developed over time.
Although some of these are not mentioned above, you might find some to
be useful as well.

ACL2-AS-STANDALONE-PROGRAM    Calling ACL2 from another program

ACL2 is intended for interactive use.  It is generally unrealistic to
expect it to prove theorems fully automatically; see
THE-METHOD, and see INTRODUCTION-TO-THE-THEOREM-PROVER for a
more detailed tutorial.

Nevertheless, here we describe an approach for how to call the ACL2
theorem prover noninteractively.  These steps can of course be modified
according to your needs.  Here, we illustrate how to call ACL2 from
another Lisp program (or an arbitrary program) to attempt to prove an
arithmetic theorem.

=== STEP 1: ===

Build a suitable ACL2 image by starting ACL2 and then executing the
following forms.  In particular, these define a macro, try-thm, that
causes ACL2 to exit with with an exit status indicating success or
failure of a proof attempt.

     (include-book "arithmetic-5/top" :dir :system)
     (defmacro try-thm (&rest args)
       `(mv-let (erp val state)
                (with-prover-time-limit 3 (thm ,@args))
                (declare (ignore val))
                (prog2$ (if erp (exit 1) (exit 0)) state))))
     (reset-prehistory) ; optional
     :q
     (save-exec "arith-acl2" "Included arithmetic-4/top")

If you prefer, above you can replace 3 by some other number of seconds
as a time limit for the prover.  Also, you can replace

     (with-prover-time-limit 3 (thm ,@args))

by

     (with-output :off :all (with-prover-time-limit 3 (thm ,@args)))

if you want to turn off output.  It may be best to leave the output on,
instead eliminating it in the calling program (see Step 3 below).

=== STEP 2: ===

Try a little test.  In that same directory try this:

     echo '(try-thm (equal x x))' | ./arith-acl2
     echo $?

The exit status should be 0, indicating success.  Now try this:

     echo '(try-thm (not (equal x x)))' | ./arith-acl2
     echo $?

The exit status should be 1, indicating failure.

=== STEP 3: ===

Create a shell script that automates Step 2, for example:

     #!/bin/sh
     (echo "(try-thm $1)" | ./arith-acl2) >& /dev/null
     exit $?

=== STEP 4: ===

Try your script from a Lisp program, if you like.  Here is how you can
do it in SBCL, for example.  ( Different Lisps have different ways to
do this, as summarized in function system-call in ACL2 source file
acl2-init.lisp.)

     (defun provable? (x)
       (let ((status
              (process-exit-code
               (sb-ext:run-program "./try-thm.sh" (list (format nil "~s" x))
                                   :output t :search t))))
         (eql status 0)))

Then here is a log:

       * (provable? '(equal x y))

       NIL
       * (provable? '(equal x x))

       T
       *

Certainly refinements are possible - for example the above doesn't
distinguish between unprovable and ill-formed input.  But it's a start.

ACL2-SEDAN    ACL2 Sedan interface

Many successful ACL2 users run in an shell under Emacs; see
EMACS.  However, those not familiar with Emacs may prefer to start
with an Eclipse-based interface developed by Peter Dillinger and Pete
Manolios called the "ACL2 Sedan", or "ACL2s".  As of this writing, the
home page for ACL2s is `http://acl2s.ccs.neu.edu/acl2s/doc/'.

ACL2 sessions in the ACL2 Sedan can utilize non-standard extensions and
enhancements, especially geared toward new users, termination
reasoning, and attaching rich user interfaces.  These extensions are
generally available as certifiable ACL2 books, and can be downloaded
from `http://acl2s.ccs.neu.edu/acl2s/src/acl2-extensions'.  (Some code
originating from this project has been migrated to the ACL2 system
books, but only after it was quite stable.)  Thanks to Peter Dillinger,
Pete Manolios, and Daron Vroon for their work on the ACL2 Sedan and for
making their books available to ACL2 users.

ALTERNATIVE-INTRODUCTION    introduction to ACL2

This section contains introductory material on ACL2 including what ACL2
is, how to get started using the system, how to read the output, and
other introductory topics.  It was written almost entirely by Bill
Young of Computational Logic, Inc.

You might also find CLI Technical Report 101 helpful, especially if you
are familiar with Nqthm.  If you would like more familiarity with
Nqthm, we suggest CLI Technical Report 100.

_OVERVIEW_

ACL2 is an automated reasoning system developed (for the first 9 years)
at Computational Logic, Inc. and (from January, 1997) at the University
of Texas at Austin.  It is the successor to the Nqthm (or Boyer-Moore)
logic and proof system and its Pc-Nqthm interactive enhancement.  The
acronym ACL2 actually stands for "A Computational Logic for Applicative
Common Lisp".  This title suggests several distinct but related aspects
of ACL2.

We assume that readers of the ACL2 documentation have at least a very
slight familiarity with some Lisp-like language.  We will address the
issue of prerequisites further, in "ABOUT THIS TUTORIAL" below.

As a logic, ACL2 is a formal system with rigorously defined syntax and
semantics.  In mathematical parlance, the ACL2 logic is a first-order
logic of total recursive functions providing mathematical induction on
the ordinals up to epsilon-0 and two extension principles: one for
recursive definition and one for constrained introduction of new
function symbols, here called encapsulation.  The syntax of ACL2 is
that of Common Lisp; ACL2 specifications are "also" Common Lisp
programs in a way that we will make clear later.  In less formal
language, the ACL2 logic is an integrated collection of rules for
defining (or axiomatizing) recursive functions, stating properties of
those functions, and rigorously establishing those properties.  Each of
these activities is mechanically supported.

As a specification language, ACL2 supports modeling of systems of
various kinds.  An ACL2 function can equally be used to express purely
formal relationships among mathematical entities, to describe
algorithms, or to capture the intended behavior of digital systems.
For digital systems, an ACL2 specification is a mathematical model that
is intended to formalize relevant aspects of system behavior.  Just as
physics allows us to model the behavior of continuous physical systems,
ACL2 allows us to model digital systems, including many with physical
realizations such as computer hardware.  As early as the 1930's Church,
Kleene, Turing and others established that recursive functions provide
an expressive formalism for modeling digital computation.  Digital
computation should be understood in a broad sense, covering a wide
variety of activities including almost any systematic or algorithmic
activity, or activity that can be reasonably approximated in that way.
This ranges from the behavior of a digital circuit to the behavior of a
programming language compiler to the behavior of a controller for a
physical system (as long as the system can be adequately modeled
discretely).  All of these have been modeled using ACL2 or its
predecessor Nqthm.

ACL2 is a computational logic in at least three distinct senses.
First, the theory of recursive functions is often considered the
mathematics of computation.  Church conjectured that any "effective
computation" can be modeled as a recursive function.  Thus, ACL2
provides an expressive language for modeling digital systems.  Second,
many ACL2 specifications are executable.  In fact, recursive functions
written in ACL2 are Common Lisp functions that can be submitted to any
compliant Common Lisp compiler and executed (in an environment where
suitable ACL2-specific macros and functions are defined).  Third, ACL2
is computational in the sense that calculation is heavily integrated
into the reasoning process.  Thus, an expression with explicit constant
values but no free variables can be simplified by calculation rather
than by complex logical manipulations.

ACL2 is a powerful, automated theorem prover or proof checker.  This
means that a competent user can utilize the ACL2 system to discover
proofs of theorems stated in the ACL2 logic or to check previously
discovered proofs.  The basic deductive steps in an ACL2-checked proof
are often quite large, due to the sophisticated combination of decision
procedures, conditional rewriting, mathematical and structural
induction, propositional simplification, and complex heuristics to
orchestrate the interactions of these capabilities.  Unlike some
automated proof systems, ACL2 does not produce a formal proof.
However, we believe that if ACL2 certifies the "theoremhood" of a given
conjecture, then such a formal proof exists and, therefore, the theorem
is valid.  The ultimate result of an ACL2 proof session is a collection
of "events," possibly grouped into "books," that can be replayed in
ACL2.  Therefore, a proof can be independently validated by any ACL2
user.

ACL2 may be used in purely automated mode in the shallow sense that
conjectures are submitted to the prover and the user does not interact
with the proof attempt (except possibly to stop it) until the proof
succeeds or fails.  However, any non-trivial proof attempt is actually
interactive, since successful proof "events" influence the subsequent
behavior of the prover.  For example, proving a lemma may introduce a
rule that subsequently is used automatically by the prover.  Thus, any
realistic proof attempt, even in "automatic" mode, is really an
interactive dialogue with the prover to craft a sequence of events
building an appropriate theory and proof rules leading up to the proof
of the desired result.  Also, ACL2 supports annotating a theorem with
"hints" designed to guide the proof attempt.  By supplying appropriate
hints, the user can suggest proof strategies that the prover would not
discover automatically.  There is a "proof-tree" facility (see
PROOF-TREE) that allows the user to monitor the progress and
structure of a proof attempt in real-time.  Exploring failed proof
attempts is actually where heavy-duty ACL2 users spend most of their
time.

ACL2 can also be used in a more explicitly interactive mode.  The
"proof-checker" subsystem of ACL2 allows exploration of a proof on a
fairly low level including expanding calls of selected function
symbols, invoking specific rewrite rules, and selectively navigating
around the proof.  This facility can be used to gain sufficient insight
into the proof to construct an automatic version, or to generate a
detailed interactive-style proof that can be replayed in batch mode.

Because ACL2 is all of these things -- computational logic,
specification language, programming system, and theorem prover -- it is
more than the sum of its parts.  The careful integration of these
diverse aspects has produced a versatile automated reasoning system
suitable for building highly reliable digital systems.  In the
remainder of this tutorial, we will illustrate some simple uses of this
automated reasoning system.

_ABOUT THIS TUTORIAL_

ACL2 is a complex system with a vast array of features, bells and
whistles.  However, it is possible to perform productive work with the
system using only a small portion of the available functionality.  The
goals of this tutorial are to:

     familiarize the new user with the most basic features of and modes
     of interaction with ACL2;

     familiarize her with the form of output of the system; and

     work through a graduated series of examples.

The more knowledge the user brings to this system, the easier it will
be to become proficient.  On one extreme:  the ideal user of ACL2 is an
expert Common Lisp programmer, has deep understanding of automated
reasoning, and is intimately familiar with the earlier Nqthm system.
Such ideal users are unlikely to need this tutorial.  However, without
some background knowledge, the beginning user is likely to become
extremely confused and frustrated by this system.  We suggest that a
new user of ACL2 should:

     (a) have a little familiarity with Lisp, including basic Lisp
     programming and prefix notation (a Lisp reference manual such as
     Guy Steele's "Common Lisp:  The Language" is also helpful);

     (b) be convinced of the utility of formal modeling; and

     (c) be willing to gain familiarity with basic automated theorem
     proving topics such as rewriting and algebraic simplification.

We will not assume any deep familiarity with Nqthm (the so-called
"Boyer-Moore Theorem Prover"), though the book "A Computational Logic
Handbook" by Boyer and Moore (Academic Press, 1988) is an extremely
useful reference for many of the topics required to become a competent
ACL2 user.  We'll refer to it as ACLH below.

As we said in the introduction, ACL2 has various facets.  For example,
it can be used as a Common Lisp programming system to construct
application programs.  In fact, the ACL2 system itself is a large
Common Lisp program constructed almost entirely within ACL2.  Another
use of ACL2 is as a specification and modeling tool.  That is the
aspect we will concentrate on in the remainder of this tutorial.

_GETTING STARTED_

This section is an abridged version of what's available elsewhere; feel
free to see STARTUP for more details.

How you start ACL2 will be system dependent, but you'll probably type
something like "acl2" at your operating system prompt.  Consult your
system administrator for details.

When you start up ACL2, you'll probably find yourself inside the ACL2
command loop, as indicated by the following prompt.

       ACL2 !>

If not, you should type (LP).  See LP, which has a lot more
information about the ACL2 command loop.

There are two "modes" for using ACL2, :logic and :program.  When you
begin ACL2, you will ordinarily be in the :logic mode.  This means that
any new function defined is not only executable but also is
axiomatically defined in the ACL2 logic.  (See DEFUN-MODE and
see DEFAULT-DEFUN-MODE.)  Roughly speaking, :program mode is
available for using ACL2 as a programming language without some of the
logical burdens necessary for formal reasoning.  In this tutorial we
will assume that we always remain in :logic mode and that our purpose is
to write formal models of digital systems and to reason about them.

Now, within the ACL2 command loop you can carry out various kinds of
activities, including the folllowing.  (We'll see examples later of
many of these.)

     define new functions (see DEFUN);

     execute functions on concrete data;

     pose and attempt to prove conjectures about previously defined
     functions (see DEFTHM);

     query the ACL2 "world" or database (e.g., see PE); and

     numerous other things.

In addition, there is extensive on-line documentation, of which this
tutorial introduction is a part.

_INTERACTING WITH ACL2_

The standard means of interacting with ACL2 is to submit a sequence of
forms for processing by the ACL2 system.  These forms are checked for
syntactic and semantic acceptability and appropriately processed by the
system.  These forms can be typed directly at the ACL2 prompt.
However, most successful ACL2 users prefer to do their work using the
Emacs text editor, maintaining an Emacs "working" buffer in which forms
are edited.  Those forms are then copied to the ACL2 interaction
buffer, which is often the "*shell*" buffer.

In some cases, processing succeeds and makes some change to the ACL2
"logical world," which affects the processing of subsequent forms.  How
can this processing fail?  For example, a proposed theorem will be
rejected unless all function symbols mentioned have been previously
defined.  Also the ability of ACL2 to discover the proof of a theorem
may depend on the user previously having proved other theorems.  Thus,
the order in which forms are submitted to ACL2 is quite important.
Maintaining forms in an appropriate order in your working buffer will
be helpful for re-playing the proof later.

One of the most common events in constructing a model is introducing
new functions.  New functions are usually introduced using the defun
form; we'll encounter some exceptions later.  Proposed function
definitions are checked to make sure that they are syntactically and
semantically acceptable (e.g., that all mentioned functions have been
previously defined) and, for recursive functions, that their recursive
calls terminate.  A recursive function definition is guaranteed to
terminate if there is some some "measure" of the arguments and a
"well-founded" ordering such that the arguments to the function get
smaller in each recursive call.  See WELL-FOUNDED-RELATION.

For example, suppose that we need a function that will append two lists
together.  (We already have one in the ACL2 append function; but
suppose perversely that we decide to define our own.)  Suppose we
submit the following definition (you should do so as well and study the
system output):

       (defun my-app (x y)
         (if (atom x)
             y
           (cons (car x) (my-app x y))))

The system responds with the following message:

       ACL2 Error in ( DEFUN MY-APP ...):  No :MEASURE was supplied with
       the definition of MY-APP.  Our heuristics for guessing one have not
       made any suggestions.  No argument of the function is tested along
       every branch and occurs as a proper subterm at the same argument
       position in every recursive call.  You must specify a :MEASURE.  See
       :DOC defun.

This means that the system could not find an expression involving the
formal parameters x and y that decreases under some well-founded order
in every recursive call (there is only one such call).  It should be
clear that there is no such measure in this case because the only
recursive call doesn't change the arguments at all.  The definition is
obviously flawed; if it were accepted and executed it would loop
forever.  Notice that a definition that is rejected is not stored in
the system database; there is no need to take any action to have it
"thrown away."  Let's try again with the correct definition.  The
interaction now looks like (we're also putting in the ACL2 prompt; you
don't type that):

       ACL2 !>(defun my-app (x y)
                (if (atom x)
                    y
                  (cons (car x) (my-app (cdr x) y))))

       The admission of MY-APP is trivial, using the relation O<
       (which is known to be well-founded on the domain recognized by
       O-P) and the measure (ACL2-COUNT X).  We observe that the
       type of MY-APP is described by the theorem
       (OR (CONSP (MY-APP X Y)) (EQUAL (MY-APP X Y) Y)).
       We used primitive type reasoning.

       Summary
       Form:  ( DEFUN MY-APP ...)
       Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
       Warnings:  None
       Time:  0.07 seconds (prove: 0.00, print: 0.00, other: 0.07)
       MY-APP

Notice that this time the function definition was accepted.  We didn't
have to supply a measure explicitly; the system inferred one from the
form of the definition.  On complex functions it may be necessary to
supply a measure explicitly.  (See XARGS.)

The system output provides several pieces of information.

     The revised definition is acceptable.  The system realized that
     there is a particular measure (namely, (acl2-count x)) and a
     well-founded relation (o<) under which the arguments of my-app get
     smaller in recursion.  Actually, the theorem prover proved several
     theorems to admit my-app.  The main one was that when (atom x) is
     false the acl2-count of (cdr x) is less than (in the o< sense) the
     acl2-count of x.  Acl2-count is the most commonly used measure of
     the "size" of an ACL2 object.  o< is the ordering relation on
     ordinals less than epsilon-0.  On the natural numbers it is just
     ordinary "<".

     The observation printed about "the type of MY-APP" means that
     calls of the function my-app will always return a value that is
     either a cons pair or is equal to the second parameter.

     The summary provides information about which previously introduced
     definitions and lemmas were used in this proof, about some notable
     things to watch out for (the Warnings), and about how long this
     event took to process.

Usually, it's not important to read this information.  However, it is a
good habit to scan it briefly to see if the type information is
surprising to you or if there are Warnings.  We'll see an example of
them later.

After a function is accepted, it is stored in the database and
available for use in other function definitions or lemmas.  To see the
definition of any function use the :pe command (see PE).  For
example,

       ACL2 !>:pe my-app
        L       73:x(DEFUN MY-APP (X Y)
                           (IF (ATOM X)
                               Y (CONS (CAR X) (MY-APP (CDR X) Y))))

This displays the definition along with some other relevant
information.  In this case, we know that this definition was processed
in :logic mode (the "L") and was the 73rd command processed in the
current session.

We can also try out our newly defined function on some sample data.  To
do that, just submit a form to be evaluated to ACL2.  For example,

       ACL2 !>(my-app '(0 1 2) '(3 4 5))
       (0 1 2 3 4 5)
       ACL2 !>(my-app nil nil)
       NIL
       ACL2 !>

Now suppose we want to prove something about the function just
introduced.  We conjecture, for example, that the length of the append
of two lists is the sum of their lengths.  We can formulate this
conjecture in the form of the following ACL2 defthm form.

       (defthm my-app-length
         (equal (len (my-app x y))
                (+ (len x) (len y))))

First of all, how did we know about the functions len and +, etc.?  The
answer to that is somewhat unsatisfying -- we know them from our past
experience in using Common Lisp and ACL2.  It's hard to know that a
function such as len exists without first knowing some Common Lisp.  If
we'd guessed that the appropriate function was called length (say, from
our knowledge of Lisp) and tried :pe length, we would have seen that
length is defined in terms of len, and we could have explored from
there.  Luckily, you can write a lot of ACL2 functions without knowing
too many of the primitive functions.

Secondly, why don't we need some "type" hypotheses?  Does it make sense
to append things that are not lists?  Well, yes.  ACL2 and Lisp are
both quite weakly typed.  For example, inspection of the definition of
my-app shows that if x is not a cons pair, then (my-app x y) always
returns y, no matter what y is.

Thirdly, would it matter if we rewrote the lemma with the equality
reversed, as follows?

       (defthm my-app-length2
         (equal (+ (len x) (len y))
                (len (my-app x y)))).

The two are logically equivalent, but...yes, it would make a big
difference.  Recall our remark that a lemma is not only a "fact" to be
proved; it also is used by the system to prove other later lemmas.  The
current lemma would be stored as a rewrite rule.  (See
RULE-CLASSES.)  For a rewrite rule, a conclusion of the form (EQUAL
LHS RHS) means to replace instances of the LHS by the appropriate
instance of the RHS.  Presumably, it's better to rewrite (len (my-app x
y)) to (+ (len x) (len y)) than the other way around.  The reason is
that the system "knows" more about + than it does about the new
function symbol my-app.

So let's see if we can prove this lemma.  Submitting our preferred
defthm to ACL2 (do it!), we get the following interaction:

               --------------------------------------------------
     ACL2 !>(defthm my-app-length
       (equal (len (my-app x y))
              (+ (len x) (len y))))

     Name the formula above *1.

     Perhaps we can prove *1 by induction.  Three induction schemes are
     suggested by this conjecture.  These merge into two derived
     induction schemes.  However, one of these is flawed and so we are
     left with one viable candidate.

     We will induct according to a scheme suggested by (LEN X), but
     modified to accommodate (MY-APP X Y).  If we let (:P X Y) denote *1
     above then the induction scheme we'll use is
     (AND (IMPLIES (NOT (CONSP X)) (:P X Y))
          (IMPLIES (AND (CONSP X) (:P (CDR X) Y))
                   (:P X Y))).
     This induction is justified by the same argument used to admit LEN,
     namely, the measure (ACL2-COUNT X) is decreasing according to the
     relation O< (which is known to be well-founded on the domain
     recognized by O-P).  When applied to the goal at hand the
     above induction scheme produces the following two nontautological
     subgoals.

     Subgoal *1/2
     (IMPLIES (NOT (CONSP X))
              (EQUAL (LEN (MY-APP X Y))
                     (+ (LEN X) (LEN Y)))).

     But simplification reduces this to T, using the :definitions of FIX,
     LEN and MY-APP, the :type-prescription rule LEN, the :rewrite rule
     UNICITY-OF-0 and primitive type reasoning.

     Subgoal *1/1
     (IMPLIES (AND (CONSP X)
                   (EQUAL (LEN (MY-APP (CDR X) Y))
                          (+ (LEN (CDR X)) (LEN Y))))
              (EQUAL (LEN (MY-APP X Y))
                     (+ (LEN X) (LEN Y)))).

     This simplifies, using the :definitions of LEN and MY-APP, primitive
     type reasoning and the :rewrite rules COMMUTATIVITY-OF-+ and
     CDR-CONS, to

     Subgoal *1/1'
     (IMPLIES (AND (CONSP X)
                   (EQUAL (LEN (MY-APP (CDR X) Y))
                          (+ (LEN Y) (LEN (CDR X)))))
              (EQUAL (+ 1 (LEN (MY-APP (CDR X) Y)))
                     (+ (LEN Y) 1 (LEN (CDR X))))).

     But simplification reduces this to T, using linear arithmetic,
     primitive type reasoning and the :type-prescription rule LEN.

     That completes the proof of *1.

     Q.E.D.

     Summary
     Form:  ( DEFTHM MY-APP-LENGTH ...)
     Rules: ((:REWRITE UNICITY-OF-0)
             (:DEFINITION FIX)
             (:REWRITE COMMUTATIVITY-OF-+)
             (:DEFINITION LEN)
             (:REWRITE CDR-CONS)
             (:DEFINITION MY-APP)
             (:TYPE-PRESCRIPTION LEN)
             (:FAKE-RUNE-FOR-TYPE-SET NIL)
             (:FAKE-RUNE-FOR-LINEAR NIL))
     Warnings:  None
     Time:  0.30 seconds (prove: 0.13, print: 0.05, other: 0.12)
      MY-APP-LENGTH
               --------------------------------------------------

Wow, it worked!  In brief, the system first tried to rewrite and
simplify as much as possible.  Nothing changed; we know that because it
said "Name the formula above *1."  Whenever the system decides to name
a formula in this way, we know that it has run out of techniques to use
other than proof by induction.

The induction performed by ACL2 is structural or "Noetherian"
induction.  You don't need to know much about that except that it is
induction based on the structure of some object.  The heuristics infer
the structure of the object from the way the object is recursively
decomposed by the functions used in the conjecture.  The heuristics of
ACL2 are reasonably good at selecting an induction scheme in simple
cases.  It is possible to override the heuristic choice by providing an
:induction hint (see HINTS).  In the case of the theorem above,
the system inducts on the structure of x as suggested by the
decomposition of x in both (my-app x y) and (len x).  In the base case,
we assume that x is not a consp.  In the inductive case, we assume that
it is a consp and assume that the conjecture holds for (cdr x).

There is a close connection between the analysis that goes on when a
function like my-app is accepted and when we try to prove something
inductively about it.  That connection is spelled out well in Boyer and
Moore's book "A Computational Logic," if you'd like to look it up.  But
it's pretty intuitive.  We accepted my-app because the "size" of the
first argument x decreases in the recursive call.  That tells us that
when we need to prove something inductively about my-app, it's a good
idea to try an induction on the size of the first argument.  Of course,
when you have a theorem involving several functions, it may be
necessary to concoct a more complicated induction schema, taking
several of them into account.  That's what's meant by "merging" the
induction schemas.

The proof involves two cases: the base case, and the inductive case.
You'll notice that the subgoal numbers go down rather than up, so you
always know how many subgoals are left to process.  The base case
(Subgoal *1/2) is handled by opening up the function definitions,
simplifying, doing a little rewriting, and performing some reasoning
based on the types of the arguments.  You'll often encounter references
to system defined lemmas (like unicity-of-0).  You can always look at
those with :pe; but, in general, assume that there's a lot of
simplification power under the hood that's not too important to
understand fully.

The inductive case (Subgoal *1/1) is also dispatched pretty easily.
Here we assume the conjecture true for the cdr of the list and try to
prove it for the entire list.  Notice that the prover does some
simplification and then prints out an updated version of the goal
(Subgoal *1/1').  Examining these gives you a pretty good idea of
what's going on in the proof.

Sometimes one goal is split into a number of subgoals, as happened with
the induction above.  Sometimes after some initial processing the
prover decides it needs to prove a subgoal by induction; this subgoal
is given a name and pushed onto a stack of goals.  Some steps, like
generalization (see ACLH), are not necessarily validity preserving;
that is, the system may adopt a false subgoal while trying to prove a
true one.  (Note that this is ok in the sense that it is not "unsound."
The system will fail in its attempt to establish the false subgoal and
the main proof attempt will fail.)  As you gain facility with using the
prover, you'll get pretty good at recognizing what to look for when
reading a proof script.  The prover's proof-tree utility helps with
monitoring an ongoing proof and jumping to designated locations in the
proof (see PROOF-TREE).  See TIPS for a number of useful
pointers on using the theorem prover effectively.

When the prover has successfully proved all subgoals, the proof is
finished.  As with a defun, a summary of the proof is printed.  This
was an extremely simple proof, needing no additional guidance.  More
realistic examples typically require the user to look carefully at the
failed proof log to find ways to influence the prover to do better on
its next attempt.  This means either:  proving some rules that will
then be available to the prover, changing the global state in ways that
will affect the proof, or providing some hints locally that will
influence the prover's behavior.  Proving this lemma (my-app-length) is
an example of the first.  Since this is a rewrite rule, whenever in a
later proof an instance of the form (LEN (MY-APP X Y)) is encountered,
it will be rewritten to the corresponding instance of (+ (LEN X) (LEN
Y)).  Disabling the rule by executing the command

       (in-theory (disable my-app-length)),

is an example of a global change to the behavior of the prover since
this rewrite will not be performed subsequently (unless the rule is
again enabled).  Finally, we can add a (local) disable "hint" to a
defthm, meaning to disable the lemma only in the proof of one or more
subgoals.  For example:

       (defthm my-app-length-commutativity
         (equal (len (my-app x y))
                (len (my-app y x)))
         :hints (("Goal" :in-theory (disable my-app-length))))

In this case, the hint supplied is a bad idea since the proof is much
harder with the hint than without it.  Try it both ways.

By the way, to undo the previous event use :u (see U).  To undo
back to some earlier event use :ubt (see UBT).  To view the
current event use :pe :here.  To list several events use :pbt (see
PBT).

Notice the form of the hint in the previous example (see
HINTS).  It specifies a goal to which the hint applies.  "Goal"
refers to the top-level goal of the theorem.  Subgoals are given unique
names as they are generated.  It may be useful to suggest that a
function symbol be disabled only for Subgoal 1.3.9, say, and a
different function enabled only on Subgoal 5.2.8.  Overuse of such
hints often suggests a poor global proof strategy.

We now recommend that you visit documentation on additional examples.
See ANNOTATED-ACL2-SCRIPTS.

ANNOTATED-ACL2-SCRIPTS    examples of ACL2 scripts

Beginning users may find these annotated scripts useful.  We suggest
that you read these in the following order:

     Tutorial1-Towers-of-Hanoi
     Tutorial2-Eights-Problem
     Tutorial3-Phonebook-Example
     Tutorial4-Defun-Sk-Example
     Tutorial5-Miscellaneous-Examples

The page
`http://www.cs.utexas.edu/users/moore/publications/tutorial/rev3.html'
contains a script that illustrates how it feels to use The Method to
prove an unusual list reverse function correct.  The screen shots of
ACL2's proof output are outdated - in the version shown, ACL2 does not
print Key Checkpoints, but the concept of key checkpoint is clear in
the discussion and the behavior of the user.

See
`http://www.cs.utexas.edu/users/moore/acl2/contrib/POLISHING-PROOFS-TUTORIAL.html'
for a tutorial on becoming successful at approaching a formalization and
proof problem in ACL2.  That tutorial, written by Shilpi Goel and
Sandip Ray, has two parts: it illustrates how to guide the theorem
prover to a successful proof, and it shows how to clean up the proof in
order to facilitate maintenance and extension of the resulting book
(see BOOKS).

At
`http://www.cs.utexas.edu/users/moore/publications/tutorial/kaufmann-TPHOLs08/index.html'
is the demo given by Matt Kaufmann at TPHOLs08, including all the
scripts.  There is a gzipped tar file containing the entire contents of
the demos.

At
`http://www.cs.utexas.edu/users/moore/publications/tutorial/sort-equivalence'
is a collection of scripts illustrating both high-level strategy and
lower-level tactics dealing with the functional equivalence of various
list sorting algorithms.  Start with the README on that directory.
There is also a gzipped tar file containing all the scripts, at
`http://www.cs.utexas.edu/users/moore/publications/tutorial/sort-equivalence.tgz'.

When you feel you have read enough examples, you might want to try the
following very simple example on your own. (See
SOLUTION-TO-SIMPLE-EXAMPLE for a solution, after you work on this
example.)  First define the notion of the "fringe" of a tree, where we
identify trees simply as cons structures, with atoms at the leaves.
For example:

       ACL2 !>(fringe '((a . b) c . d))
       (A B C D)

Next, define the notion of a "leaf" of a tree, i.e., a predicate leaf-p
that is true of an atom if and only if that atom appears at the tip of
the tree.  Define this notion without referencing the function fringe.
Finally, prove the following theorem, whose proof may well be automatic
(i.e., not require any lemmas).

       (defthm leaf-p-iff-member-fringe
         (iff (leaf-p atm x)
              (member-equal atm (fringe x))))

SOLUTION-TO-SIMPLE-EXAMPLE    solution to a simple example

To see a statement of the problem solved below, see
ANNOTATED-ACL2-SCRIPTS (in particular the end of that topic).

Here is a sequence of ACL2 events that illustrates the use of ACL2 to
make definitions and prove theorems.  We will introduce the notion of
the fringe of a tree, as well as the notion of a leaf of a tree, and
then prove that the members of the fringe are exactly the leaves.

We begin by defining the fringe of a tree, where we identify trees
simply as cons structures, with atoms at the leaves.  The definition is
recursive, breaking into two cases.  If x is a cons, then the fringe of
x is obtained by appending together the fringes of the car and cdr
(left and right child) of x.  Otherwise, x is an atom and its fringe is
the one-element list containing only x.

       (defun fringe (x)
         (if (consp x)
             (append (fringe (car x))
                     (fringe (cdr x)))
           (list x)))

Now that fringe has been defined, let us proceed by defining the notion
of an atom appearing as a "leaf", with the goal of proving that the
leaves of a tree are exactly the members of its fringe.

       (defun leaf-p (atm x)
         (if (consp x)
             (or (leaf-p atm (car x))
                 (leaf-p atm (cdr x)))
           (equal atm x)))

The main theorem is now as follows.  Note that the rewrite rule below
uses the equivalence relation iff (see EQUIVALENCE) rather than
equal, since member returns the tail of the given list that begins with
the indicated member, rather than returning a Boolean.  (Use :pe member
to see the definition of member.)

       (defthm leaf-p-iff-member-fringe
         (iff (leaf-p atm x)
              (member-equal atm (fringe x))))

TUTORIAL1-TOWERS-OF-HANOI    The Towers of Hanoi Example

This example was written almost entirely by Bill Young of Computational
Logic, Inc.

We will formalize and prove a small theorem about the famous "Towers of
Hanoi" problem.  This problem is illustrated by the following picture.

               |        |        |
               |        |        |
              ---       |        |
             -----      |        |
            -------     |        |

               A        B        C

We have three pegs -- a, b, and c -- and n disks of different sizes.
The disks are all initially on peg a.  The goal is to move all disks to
peg c while observing the following two rules.

1. Only one disk may be moved at a time, and it must start and finish
the move as the topmost disk on some peg;

2. A disk can never be placed on top of a smaller disk.

Let's consider some simple instances of this problem.  If n = 1, i.e.,
only one disk is to be moved, simply move it from a to c.  If n = 2,
i.e., two disks are to be moved, the following sequence of moves
suffices:  move from a to b, move from a to c, move from b to c.

In this doc topic we will show an ACL2 function that generates a
suitable list of moves for a tower of n disks.  Then we will use ACL2
to prove that the number of moves is (- (expt 2 n) 1).  For an ACL2
script that proves the correctness of (a version of) this function, see
the book "misc/hanoi.lisp" in the books directory of your ACL2 sources.

In general, this problem has a straightforward recursive solution.
Suppose that we desire to move n disks from a to c, using b as the
intermediate peg.  For the basis, we saw above that we can always move
a single disk from a to c.  Now if we have n disks and assume that we
can solve the problem for n-1 disks, we can move n disks as follows.
First, move n-1 disks from a to b using c as the intermediate peg; move
the single disk from a to c; then move n-1 disks from b to c using a as
the intermediate peg.

In ACL2, we can write a function that will return the sequence of
moves.  One such function is as follows.  Notice that we have two base
cases.  If (zp n) then n is not a positive integer; we treat that case
as if n were 0 and return an empty list of moves.  If n is 1, then we
return a list containing the single appropriate move.  Otherwise, we
return the list containing exactly the moves dictated by our recursive
analysis above.

       (defun move (a b)
         (list 'move a 'to b))

       (defun hanoi (a b c n)
         (if (zp n)
             nil
           (if (equal n 1)
               (list (move a c))
             (append (hanoi a c b (1- n))
                     (cons (move a c)
                           (hanoi b a c (1- n)))))))

Notice that we give hanoi four arguments:  the three pegs, and the
number of disks to move.  It is necessary to supply the pegs because,
in recursive calls, the roles of the pegs differ.  In any execution of
the algorithm, a given peg will sometimes be the source of a move,
sometimes the destination, and sometimes the intermediate peg.

After submitting these functions to ACL2, we can execute the hanoi
function on various specific arguments.  For example:

       ACL2 !>(hanoi 'a 'b 'c 1)
       ((MOVE A TO C))

       ACL2 !>(hanoi 'a 'b 'c 2)
       ((MOVE A TO B)
        (MOVE A TO C)
        (MOVE B TO C))

       ACL2 !>(hanoi 'a 'b 'c 3)
       ((MOVE A TO C)
        (MOVE A TO B)
        (MOVE C TO B)
        (MOVE A TO C)
        (MOVE B TO A)
        (MOVE B TO C)
        (MOVE A TO C))

From the algorithm it is clear that if it takes m moves to transfer n
disks, it will take (m + 1 + m) = 2m + 1 moves for n+1 disks.  From
some simple calculations, we see that we need the following number of
moves in specific cases:

        Disks   0   1   2   3   4   5   6   7  ...
        Moves   0   1   3   7  15  31  63  127 ...

The pattern is fairly clear.  To move n disks requires (2^n - 1) moves.
Let's attempt to use ACL2 to prove that fact.

First of all, how do we state our conjecture?  Recall that hanoi
returns a list of moves.  The length of the list (given by the function
len) is the number of moves required.  Thus, we can state the following
conjecture.

       (defthm hanoi-moves-required-first-try
         (equal (len (hanoi a b c n))
                (1- (expt 2 n))))

When we submit this to ACL2, the proof attempt fails.  Along the way we
notice subgoals such as:

       Subgoal *1/1'
       (IMPLIES (NOT (< 0 N))
                (EQUAL 0 (+ -1 (EXPT 2 N)))).

This tells us that the prover is considering cases that are
uninteresting to us, namely, cases in which n might be negative.  The
only cases that are really of interest are those in which n is a
non-negative natural number.  Therefore, we revise our theorem as
follows:

       (defthm hanoi-moves-required
         (implies (and (integerp n)
                       (<= 0 n))    ;; n is at least 0
                  (equal (len (hanoi a b c n))
                         (1- (expt 2 n)))))

and submit it to ACL2 again.

Again the proof fails.  Examining the proof script we encounter the
following text.  (How did we decide to focus on this goal?  Some
information is provided in ACLH, and the ACL2 documentation on tips may
be helpful.  But the simplest answer is:  this was the first goal
suggested by the "proof-tree" tool below the start of the proof by
induction.  See PROOF-TREE.)

       Subgoal *1/5''
       (IMPLIES (AND (INTEGERP N)
                     (< 0 N)
                     (NOT (EQUAL N 1))
                     (EQUAL (LEN (HANOI A C B (+ -1 N)))
                            (+ -1 (EXPT 2 (+ -1 N))))
                     (EQUAL (LEN (HANOI B A C (+ -1 N)))
                            (+ -1 (EXPT 2 (+ -1 N)))))
                (EQUAL (LEN (APPEND (HANOI A C B (+ -1 N))
                                    (CONS (LIST 'MOVE A 'TO C)
                                          (HANOI B A C (+ -1 N)))))
                       (+ -1 (* 2 (EXPT 2 (+ -1 N))))))

It is difficult to make much sense of such a complicated goal.
However, we do notice something interesting.  In the conclusion is a
term of the following shape.

        (LEN (APPEND ... ...))

We conjecture that the length of the append of two lists should be the
sum of the lengths of the lists.  If the prover knew that, it could
possibly have simplified this term earlier and made more progress in
the proof.  Therefore, we need a rewrite rule that will suggest such a
simplification to the prover.  The appropriate rule is:

       (defthm len-append
         (equal (len (append x y))
                (+ (len x) (len y))))

We submit this to the prover, which proves it by a straightforward
induction.  The prover stores this lemma as a rewrite rule and will
subsequently (unless we disable the rule) replace terms matching the
left hand side of the rule with the appropriate instance of the term on
the right hand side.

We now resubmit our lemma hanoi-moves-required to ACL2.  On this
attempt, the proof succeeds and we are done.

One bit of cleaning up is useful.  We needed the hypotheses that:

       (and (integerp n) (<= 0 n)).

This is an awkward way of saying that n is a natural number; natural is
not a primitive data type in ACL2.  We could define a function
naturalp, but it is somewhat more convenient to define a macro as
follows:

       (defmacro naturalp (x)
         (list 'and (list 'integerp x)
                       (list '<= 0 x)))

Subsequently, we can use (naturalp n) wherever we need to note that a
quantity is a natural number.  See DEFMACRO for more
information about ACL2 macros.  With this macro, we can reformulate our
theorem as follows:

       (defthm hanoi-moves-required
         (implies (naturalp n)
                  (equal (len (hanoi a b c n))
                         (1- (expt 2 n))))).

Another interesting (but much harder) theorem asserts that the list of
moves generated by our hanoi function actually accomplishes the desired
goal while following the rules.  When you can state and prove that
theorem, you'll be a very competent ACL2 user.

By the way, the name "Towers of Hanoi" derives from a legend that a
group of Vietnamese monks works day and night to move a stack of 64
gold disks from one diamond peg to another, following the rules set out
above.  We're told that the world will end when they complete this
task.  From the theorem above, we know that this requires
18,446,744,073,709,551,615 moves:

       ACL2 !>(1- (expt 2 64))
       18446744073709551615
       ACL2 !>

We're guessing they won't finish any time soon.

TUTORIAL2-EIGHTS-PROBLEM    The Eights Problem Example

This example was written almost entirely by Bill Young of Computational
Logic, Inc.

This simple example was brought to our attention as one that Paul
Jackson has solved using the NuPrl system.  The challenge is to prove
the theorem:

       for all n > 7, there exist naturals i and j such that: n = 3i + 5j.

In ACL2, we could phrase this theorem using quantification.  However we
will start with a constructive approach, i.e., we will show that values
of i and j exist by writing a function that will construct such values
for given n.  Suppose we had a function (split n) that returns an
appropriate pair (i . j).  Our theorem would be as follows:

       (defthm split-splits
         (let ((i (car (split n)))
               (j (cdr (split n))))
           (implies (and (integerp n)
                         (< 7 n))
                    (and (integerp i)
                         (<= 0 i)
                         (integerp j)
                         (<= 0 j)
                         (equal (+ (* 3 i) (* 5 j))
                                n)))))

That is, assuming that n is a natural number greater than 7, (split n)
returns values i and j that are in the appropriate relation to n.

Let's look at a few cases:

       8 = 3x1 + 5x1;    11 = 3x2 + 5x1;     14 = 3x3 + 5x1;   ...
       9 = 3x3 + 5x0;    12 = 3x4 + 5x0;     15 = 3x5 + 5x0;   ...
      10 = 3x0 + 5x2;    13 = 3x1 + 5x2;     16 = 3x2 + 5x2;   ...

Maybe you will have observed a pattern here; any natural number larger
than 10 can be obtained by adding some multiple of 3 to 8, 9, or 10.
This gives us the clue to constructing a proof.   It is clear that we
can write split as follows:

       (defun bump-i (x)
         ;; Bump the i component of the pair
         ;; (i . j) by 1.
         (cons (1+ (car x)) (cdr x)))

       (defun split (n)
         ;; Find a pair (i . j) such that
         ;; n = 3i + 5j.
         (if (or (zp n) (< n 8))
             nil ;; any value is really reasonable here
           (if (equal n 8)
               (cons 1 1)
             (if (equal n 9)
                 (cons 3 0)
               (if (equal n 10)
                   (cons 0 2)
                 (bump-i (split (- n 3))))))))

Notice that we explicitly compute the values of i and j for the cases
of 8, 9, and 10, and for the degenerate case when n is not a natural or
is less than 8.  For all naturals greater than n, we decrement n by 3
and bump the number of 3's (the value of i) by 1.  We know that the
recursion must terminate because any integer value greater than 10 can
eventually be reduced to 8, 9, or 10 by successively subtracting 3.

Let's try it on some examples:

       ACL2 !>(split 28)
       (6 . 2)

       ACL2 !>(split 45)
       (15 . 0)

       ACL2 !>(split 335)
       (110 . 1)

Finally, we submit our theorem split-splits, and the proof succeeds.
In this case, the prover is "smart" enough to induct according to the
pattern indicated by the function split.

For completeness, we'll note that we can state and prove a quantified
version of this theorem.  We introduce the notion split-able to mean
that appropriate i and j exist for n.

       (defun-sk split-able (n)
         (exists (i j)
                 (equal n (+ (* 3 i) (* 5 j)))))

Then our theorem is given below.  Notice that we prove it by observing
that our previous function split delivers just such an i and j (as we
proved above).

       (defthm split-splits2
         (implies (and (integerp n)
                       (< 7 n))
                  (split-able n))
         :hints (("Goal" :use (:instance split-able-suff
                                         (i (car (split n)))
                                         (j (cdr (split n)))))))

Unfortunately, understanding the mechanics of the proof requires
knowing something about the way defun-sk works.  See DEFUN-SK
or see TUTORIAL4-DEFUN-SK-EXAMPLE for more on that subject.

TUTORIAL3-PHONEBOOK-EXAMPLE    A Phonebook Specification

The other tutorial examples are rather small and entirely self
contained.  The present example is rather more elaborate, and makes use
of a feature that really adds great power and versatility to ACL2,
namely:  the use of previously defined collections of lemmas, in the
form of "books."

This example was written almost entirely by Bill Young of Computational
Logic, Inc.

This example is based on one developed by Ricky Butler and Sally
Johnson of NASA Langley for the PVS system, and subsequently revised by
Judy Crow, et al, at SRI.  It is a simple phone book specification.  We
will not bother to follow their versions closely, but will instead
present a style of specification natural for ACL2.

The idea is to model an electronic phone book with the following
properties.

     Our phone book will store the phone numbers of a city.

     It must be possible to retrieve a phone number, given a name.

     It must be possible to add and delete entries.

Of course, there are numerous ways to construct such a model.  A
natural approach within the Lisp/ACL2 context is to use "association
lists" or "alists."  Briefly, an alist is a list of pairs (key .
value) associating a value with a key.  A phone book could be an alist
of pairs (name . pnum).  To find the phone number associated with a
given name, we merely search the alist until we find the appropriate
pair.  For a large city, such a linear list would not be efficient, but
at this point we are interested only in modeling the problem, not in
deriving an efficient implementation.  We could address that question
later by proving our alist model equivalent, in some desired sense, to
a more efficient data structure.

We could build a theory of alists from scratch, or we can use a
previously constructed theory (book) of alist definitions and facts.
By using an existing book, we build upon the work of others, start our
specification and proof effort from a much richer foundation, and
hopefully devote more of our time to the problem at hand.
Unfortunately, it is not completely simple for the new user to know
what books are available and what they contain.  We hope later to
improve the documentation of the growing collection of books available
with the ACL2 distribution; for now, the reader is encouraged to look
in the README file in the books subdirectory.  For present purposes,
the beginning user can simply take our word that a book exists
containing useful alist definitions and facts.  These definitions and
lemmas can be introduced into the current theory using the command:

       (include-book "data-structures/alist-defthms" :dir :system)

This book has been "certified," which means that the definitions and
lemmas have been mechanically checked and stored in a safe manner.
(See BOOKS and see INCLUDE-BOOK for details.)

Including this book makes available a collection of functions including
the following:

     (ALISTP A)    ; is A an alist (actually a primitive ACL2 function)

     (BIND X V A)  ; associate the key X with value V in alist A

     (BINDING X A) ; return the value associated with key X in alist A

     (BOUND? X A)  ; is key X associated with any value in alist A

     (DOMAIN A)    ; return the list of keys bound in alist A

     (RANGE A)     ; return the list of values bound to keys in alist A

     (REMBIND X A) ; remove the binding of key X in alist A

Along with these function definitions, the book also provides a number
of proved lemmas that aid in simplifying expressions involving these
functions.  (See RULE-CLASSES for the way in which lemmas are
used in simplification and rewriting.)  For example,

       (defthm bound?-bind
         (equal (bound? x (bind y v a))
                (or (equal x y)
                    (bound? x a))))

asserts that x will be bound in (bind y v a) if and only if: either x =
y or x was already bound in a.  Also,

       (defthm binding-bind
         (equal (binding x (bind y v a))
                (if (equal x y)
                    v
                  (binding x a))))

asserts that the resulting binding will be v, if x = y, or the binding
that x had in a already, if not.

Thus, the inclusion of this book essentially extends our specification
and reasoning capabilities by the addition of new operations and facts
about these operations that allow us to build further specifications on
a richer and possibly more intuitive foundation.

However, it must be admitted that the use of a book such as this has
two potential limitations:

     the definitions available in a book may not be ideal for your
     particular problem;

     it is (extremely) likely that some useful facts (especially,
     rewrite rules) are not available in the book and will have to be
     proved.

For example, what is the value of binding when given a key that is not
bound in the alist?  We can find out by examining the function
definition.  Look at the definition of the binding function (or any
other defined function), using the :pe command:

       ACL2 !>:pe binding
          d     33  (INCLUDE-BOOK
                         "/slocal/src/acl2/v1-9/books/public/alist-defthms")

       >V d          (DEFUN BINDING (X A)
                            "The value bound to X in alist A."
                            (DECLARE (XARGS :GUARD (ALISTP A)))
                            (CDR (ASSOC-EQUAL X A)))

This tells us that binding was introduced by the given include-book
form, is currently disabled in the current theory, and has the
definition given by the displayed defun form.  We see that binding is
actually defined in terms of the primitive assoc-equal function.  If we
look at the definition of assoc-equal:

       ACL2 !>:pe assoc-equal
        V     -489  (DEFUN ASSOC-EQUAL (X ALIST)
                           (DECLARE (XARGS :GUARD (ALISTP ALIST)))
                           (COND ((ENDP ALIST) NIL)
                                 ((EQUAL X (CAR (CAR ALIST)))
                                  (CAR ALIST))
                                 (T (ASSOC-EQUAL X (CDR ALIST)))))

we can see that assoc-equal returns nil upon reaching the end of an
unsuccessful search down the alist.  So binding returns (cdr nil) in
that case, which is nil.  Notice that we could also have investigated
this question by trying some simple examples.

       ACL2 !>(binding 'a nil)
       NIL

       ACL2 !>(binding 'a (list (cons 'b 2)))
       NIL

These definitions aren't ideal for all purposes. For one thing, there's
nothing that keeps us from having nil as a value bound to some key in
the alist.  Thus, if binding returns nil we don't always know if that
is the value associated with the key in the alist, or if that key is
not bound.  We'll have to keep that ambiguity in mind whenever we use
binding in our specification.  Suppose instead that we wanted binding
to return some error string on unbound keys.  Well, then we'd just have
to write our own version of binding.  But then we'd lose much of the
value of using a previously defined book.  As with any specification
technique, certain tradeoffs are necessary.

Why not take a look at the definitions of other alist functions and see
how they work together to provide the ability to construct and search
alists?  We'll be using them rather heavily in what follows so it will
be good if you understand basically how they work.  Simply start up
ACL2 and execute the form shown earlier, but substituting our directory
name for the top-level ACL2 directory with yours.  Alternatively, just

       (include-book "data-structures/alist-defthms" :dir :system)

Then, you can use :pe to look at function definitions.  You'll soon
discover that almost all of the definitions are built on definitions of
other, more primitive functions, as binding is built on assoc-equal.
You can look at those as well, of course, or in many cases visit their
documentation.

The other problem with using a predefined book is that it will seldom
be "sufficiently complete," in the sense that the collection of rewrite
rules supplied won't be adequate to prove everything we'd like to know
about the interactions of the various functions.  If it were, there'd
be no real reason to know that binding is built on top of assoc-equal,
because everything we'd need to know about binding would be nicely
expressed in the collection of theorems supplied with the book.
However, that's very seldom the case.  Developing such a collection of
rules is currently more art than science and requires considerable
experience.  We'll encounter examples later of "missing" facts about
binding and our other alist functions.  So, let's get on with the
example.

Notice that alists are mappings of keys to values; but, there is no
notion of a "type" associated with the keys or with the values.  Our
phone book example, however, does have such a notion of types; we map
names to phone numbers.  We can introduce these "types" by explicitly
defining them, e.g., names are strings and phone numbers are integers.
Alternatively, we can partially define or axiomatize a recognizer for
names without giving a full definition.  A way to safely introduce such
"constrained" function symbols in ACL2 is with the encapsulate form.
For example, consider the following form.

       (encapsulate
         ;; Introduce a recognizer for names and give a ``type'' lemma.
         (((namep *) => *))
         ;;
         (local (defun namep (x)
                  ;; This declare is needed to tell
                  ;; ACL2 that we're aware that the
                  ;; argument x is not used in the body
                  ;; of the function.
                  (declare (ignore x))
                  t))
         ;;
         (defthm namep-booleanp
           (booleanp (namep x))))

This encapsulate form introduces the new function namep of one argument
and one result and constrains (namep x) to be Boolean, for all inputs
x.  More generally, an encapsulation establishes an environment in
which functions can be defined and theorems and rules added without
necessarily introducing those functions, theorems, and rules into the
environment outside the encapsulation.  To be admissible, all the
events in the body of an encapsulate must be admissible.  But the
effect of an encapsulate is to assume only the non-local events.

The first "argument" to encapsulate, ((namep (x) t)) above, declares
the intended signatures of new function symbols that will be "exported"
from the encapsulation without definition.  The local defun of name
defines name within the encapsulation always to return t.  The defthm
event establishes that namep is Boolean.  By making the defun local but
the defthm non-local this encapsulate constrains the undefined function
namep to be Boolean; the admissibility of the encapsulation establishes
that there exists a Boolean function (namely the constant function
returning t).

We can subsequently use namep as we use any other Boolean function,
with the proviso that we know nothing about it except that it always
returns either t or nil.  We use namep to "recognize" legal keys for
our phonebook alist.

We wish to do something similar to define what it means to be a legal
phone number.  We submit the following form to ACL2:

       (encapsulate
         ;; Introduce a recognizer for phone numbers.
         (((pnump *) => *))
         ;;
         (local (defun pnump (x)
                  (not (equal x nil))))
         ;;
         (defthm pnump-booleanp
           (booleanp (pnump x)))
         ;;
         (defthm nil-not-pnump
           (not (pnump nil)))).

This introduces a Boolean-valued recognizer pnump, with the additional
proviso that the constant nil is not a pnump.  We impose this
restriction to guarantee that we'll never bind a name to nil in our
phone book and thereby introduce the kind of ambiguity described above
regarding the use of binding.

Now a legal phone book is an alist mapping from nameps to pnumps.  We
can define this as follows:

       (defun name-phonenum-pairp (x)
         ;; Recognizes a pair of (name . pnum).
         (and (consp x)
              (namep (car x))
              (pnump (cdr x))))

       (defun phonebookp (l)
         ;; Recognizes a list of such pairs.
         (if (not (consp l))
             (null l)
           (and (name-phonenum-pairp (car l))
                (phonebookp (cdr l)))))

Thus, a phone book is really a list of pairs (name . pnum).  Notice
that we have not assumed that the keys of the phone book are distinct.
We'll worry about that question later.  (It is not always desirable to
insist that the keys of an alist be distinct.  But it may be a useful
requirement for our specific example.)

Now we are ready to define some of the functions necessary for our
phonebook example.  The functions we need are:

     (IN-BOOK? NM BK)          ; does NM have a phone number in BK

     (FIND-PHONE NM BK)        ; find NM's phone number in phonebook BK

     (ADD-PHONE NM PNUM BK)    ; give NM the phone number PNUM in BK

     (CHANGE-PHONE NM PNUM BK) ; change NM's phone number to PNUM in BK

     (DEL-PHONE NM PNUM)       ; remove NM's phone number from BK

Given our underlying theory of alists, it is easy to write these
functions.  But we must take care to specify appropriate "boundary"
behavior.  Thus, what behavior do we want when, say, we try to change
the phone number of a client who is not currently in the book?  As
usual, there are numerous possibilities; here we'll assume that we
return the phone book unchanged if we try anything "illegal."

Possible definitions of our phone book functions are as follows.
(Remember, an include-book form such as the ones shown earlier must be
executed in order to provide definitions for functions such as bound?.)

       (defun in-book? (nm bk)
         (bound? nm bk))

       (defun find-phone (nm bk)
         (binding nm bk))

       (defun add-phone (nm pnum bk)
         ;; If nm already in-book?, make no change.
         (if (in-book? nm bk)
             bk
           (bind nm pnum bk)))

       (defun change-phone (nm pnum bk)
         ;; Make a change only if nm already has a phone number.
         (if (in-book? nm bk)
             (bind nm pnum bk)
           bk))

       (defun del-phone (nm bk)
         ;; Remove the binding from bk, if there is one.
         (rembind nm bk))

Notice that we don't have to check whether a name is in the book before
deleting, because rembind is essentially a no-op if nm is not bound in
bk.

In some sense, this completes our specification.  But we can't have any
real confidence in its correctness without validating our specification
in some way.  One way to do so is by proving some properties of our
specification.  Some candidate properties are:

     1. A name will be in the book after we add it.

     2. We will find the most recently added phone number for a client.

     3. If we change a number, we'll find the change.

     4. Changing and then deleting a number is the same as just
     deleting.

     5. A name will not be in the book after we delete it.

Let's formulate some of these properties.  The first one, for example,
is:

       (defthm add-in-book
         (in-book? nm (add-phone nm pnum bk))).

You may wonder why we didn't need any hypotheses about the "types" of
the arguments.  In fact, add-in-book is really expressing a property
that is true of alists in general, not just of the particular variety
of alists we are dealing with.  Of course, we could have added some
extraneous hypotheses and proved:

       (defthm add-in-book
         (implies (and (namep nm)
                       (pnump pnum)
                       (phonebookp bk))
                  (in-book? nm (add-phone nm pnum bk)))),

but that would have yielded a weaker and less useful lemma because it
would apply to fewer situations.  In general, it is best to state
lemmas in the most general form possible and to eliminate unnecessary
hypotheses whenever possible.  The reason for that is simple: lemmas
are usually stored as rules and used in later proofs.  For a lemma to
be used, its hypotheses must be relieved (proved to hold in that
instance); extra hypotheses require extra work.  So we avoid them
whenever possible.

There is another, more important observation to make about our lemma.
Even in its simpler form (without the extraneous hypotheses), the lemma
add-in-book may be useless as a rewrite rule.  Notice that it is stated
in terms of the non-recursive functions in-book? and add-phone.  If such
functions appear in the left hand side of the conclusion of a lemma,
the lemma may not ever be used.  Suppose in a later proof, the theorem
prover encountered a term of the form:

       (in-book? nm (add-phone nm pnum bk)).

Since we've already proved add-in-book, you'd expect that this would be
immediately reduced to true.  However, the theorem prover will often
"expand" the non-recursive definitions of in-book?  and add-phone using
their definitions before it attempts rewriting with lemmas.  After this
expansion, lemma add-in-book won't "match" the term and so won't be
applied.  Look back at the proof script for add-in-proof and you'll
notice that at the very end the prover warned you of this potential
difficulty when it printed:

       Warnings:  Non-rec
       Time:  0.18 seconds (prove: 0.05, print: 0.00, other: 0.13)
       ADD-IN-BOOK

The "Warnings" line notifies you that there are non-recursive function
calls in the left hand side of the conclusion and that this problem
might arise.  Of course, it may be that you don't ever plan to use the
lemma for rewriting or that your intention is to disable these
functions.  Disabled functions are not expanded and the lemma should
apply.  However, you should always take note of such warnings and
consider an appropriate response.  By the way, we noted above that
binding is disabled.  If it were not, none of the lemmas about binding
in the book we included would likely be of much use for exactly the
reason we just gave.

For our current example, let's assume that we're just investigating the
properties of our specifications and not concerned about using our
lemmas for rewriting.  So let's go on.  If we really want to avoid the
warnings, we can add :rule-classes nil to each defthm event; see
RULE-CLASSES.

Property 2 is:  we always find the most recently added phone number for
a client.  Try the following formalization:

       (defthm find-add-first-cut
         (equal (find-phone nm (add-phone nm pnum bk))
                pnum))

and you'll find that the proof attempt fails.  Examining the proof
attempt and our function definitions, we see that the lemma is false if
nm is already in the book.  We can remedy this situation by
reformulating our lemma in at least two different ways:

       (defthm find-add1
         (implies (not (in-book? nm bk))
                  (equal (find-phone nm (add-phone nm pnum bk))
                         pnum)))

       (defthm find-add2
         (equal (find-phone nm (add-phone nm pnum bk))
                (if (in-book? nm bk)
                    (find-phone nm bk)
                    pnum)))

For technical reasons, lemmas such as find-add2, i.e., which do not
have hypotheses, are usually slightly preferable.  This lemma is stored
as an "unconditional" rewrite rule (i.e., has no hypotheses) and,
therefore, will apply more often than find-add1.  However, for our
current purposes either version is all right.

Property 3 says: If we change a number, we'll find the change.  This is
very similar to the previous example.  The formalization is as follows.

       (defthm find-change
         (equal (find-phone nm (change-phone nm pnum bk))
                (if (in-book? nm bk)
                    pnum
                  (find-phone nm bk))))

Property 4 says: changing and then deleting a number is the same as
just deleting.  We can model this as follows.

       (defthm del-change
         (equal (del-phone nm (change-phone nm pnum bk))
                (del-phone nm bk)))

Unfortunately, when we try to prove this, we encounter subgoals that
seem to be true, but for which the prover is stumped.  For example,
consider the following goal.  (Note:  endp holds of lists that are
empty.)

       Subgoal *1/4
       (IMPLIES (AND (NOT (ENDP BK))
                     (NOT (EQUAL NM (CAAR BK)))
                     (NOT (BOUND? NM (CDR BK)))
                     (BOUND? NM BK))
                (EQUAL (REMBIND NM (BIND NM PNUM BK))
                       (REMBIND NM BK))).

Our intuition about rembind and bind tells us that this goal should be
true even without the hypotheses.  We attempt to prove the following
lemma.

       (defthm rembind-bind
         (equal (rembind nm (bind nm pnum bk))
                (rembind nm bk)))

The prover proves this by induction, and stores it as a rewrite rule.
After that, the prover has no difficulty in proving del-change.

The need to prove lemma rembind-bind illustrates a point we made early
in this example:  the collection of rewrite rules supplied by a
previously certified book will almost never be everything you'll need.
It would be nice if we could operate purely in the realm of names,
phone numbers, and phone books without ever having to prove any new
facts about alists.  Unfortunately, we needed a fact about the relation
between rembind and bind that wasn't supplied with the alists theory.
Hopefully, such omissions will be rare.

Finally, let's consider our property 5 above:  a name will not be in
the book after we delete it.  We formalize this as follows:

       (defthm in-book-del
         (not (in-book? nm (del-phone nm bk))))

This proves easily.  But notice that it's only true because del-phone
(actually rembind) removes all occurrences of a name from the phone
book.  If it only removed, say, the first one it encountered, we'd need
a hypothesis that said that nm occurs at most once in bk.  Ah, maybe
that's a property you hadn't considered.  Maybe you want to ensure that
any name occurs at most once in any valid phonebook.

To complete this example, let's consider adding an invariant to our
specification.  In particular, suppose we want to assure that no client
has more than one associated phone number.  One way to ensure this is
to require that the domain of the alist is a "set" (has no duplicates).

       (defun setp (l)
         (if (atom l)
             (null l)
           (and (not (member-equal (car l) (cdr l)))
                (setp (cdr l)))))

       (defun valid-phonebookp (bk)
         (and (phonebookp bk)
              (setp (domain bk))))

Now, we want to show under what conditions our operations preserve the
property of being a valid-phonebookp.  The operations in-book?  and
find-phone don't return a phone book, so we don't really need to worry
about them.  Since we're really interested in the "types" of values
preserved by our phonebook functions, let's look at the types of those
operations as well.

       (defthm in-book-booleanp
         (booleanp (in-book? nm bk)))

       (defthm in-book-namep
         (implies (and (phonebookp bk)
                       (in-book? nm bk))
                  (namep nm))
         :hints (("Goal" :in-theory (enable bound?))))

       (defthm find-phone-pnump
         (implies (and (phonebookp bk)
                       (in-book? nm bk))
                  (pnump (find-phone nm bk)))
         :hints (("Goal" :in-theory (enable bound? binding))))

Note the ":hints" on the last two lemmas.  Neither of these would prove
without these hints, because once again there are some facts about
bound? and binding not available in our current context.  Now, we could
figure out what those facts are and try to prove them.  Alternatively,
we can enable bound? and binding and hope that by opening up these
functions, the conjectures will reduce to versions that the prover does
know enough about or can prove by induction.  In this case, this
strategy works.  The hints tell the prover to enable the functions in
question when considering the designated goal.

Below we develop the theorems showing that add-phone, change-phone, and
del-phone preserve our proposed invariant.  Notice that along the way
we have to prove some subsidiary facts, some of which are pretty ugly.
It would be a good idea for you to try, say,
add-phone-preserves-invariant without introducing the following four
lemmas first.  See if you can develop the proof and only add these
lemmas as you need assistance.  Then try
change-phone-preserves-invariant and del-phone-preserves-invariant.
They will be easier.  It is illuminating to think about why
del-phone-preserves-invariant does not need any "type" hypotheses.

       (defthm bind-preserves-phonebookp
         (implies (and (phonebookp bk)
                       (namep nm)
                       (pnump num))
                  (phonebookp (bind nm num bk))))

       (defthm member-equal-strip-cars-bind
         (implies (and (not (equal x y))
                       (not (member-equal x (strip-cars a))))
                  (not (member-equal x (strip-cars (bind y z a))))))

       (defthm bind-preserves-domain-setp
         (implies (and (alistp bk)
                       (setp (domain bk)))
                  (setp (domain (bind nm num bk))))
         :hints (("Goal" :in-theory (enable domain))))

       (defthm phonebookp-alistp
         (implies (phonebookp bk)
                  (alistp bk)))

       (defthm ADD-PHONE-PRESERVES-INVARIANT
         (implies (and (valid-phonebookp bk)
                       (namep nm)
                       (pnump num))
                  (valid-phonebookp (add-phone nm num bk)))
         :hints (("Goal" :in-theory (disable domain-bind))))

       (defthm CHANGE-PHONE-PRESERVES-INVARIANT
         (implies (and (valid-phonebookp bk)
                       (namep nm)
                       (pnump num))
                  (valid-phonebookp (change-phone nm num bk)))
         :hints (("Goal" :in-theory (disable domain-bind))))

       (defthm remove-equal-preserves-setp
         (implies (setp l)
                  (setp (remove-equal x l))))

       (defthm rembind-preserves-phonebookp
         (implies (phonebookp bk)
                  (phonebookp (rembind nm bk))))

       (defthm DEL-PHONE-PRESERVES-INVARIANT
         (implies (valid-phonebookp bk)
                  (valid-phonebookp (del-phone nm bk))))

As a final test of your understanding, try to formulate and prove an
invariant that says that no phone number is assigned to more than one
name.  The following hints may help.

     1. Define the appropriate invariant.  (Hint: remember the function
     range.)

     2. Do our current definitions of add-phone and change-phone
     necessarily preserve this property?  If not, consider what
     hypotheses are necessary in order to guarantee that they do
     preserve this property.

     3. Study the definition of the function range and notice that it
     is defined in terms of the function strip-cdrs.  Understand how
     this defines the range of an alist.

     4. Formulate the correctness theorems and attempt to prove them.
     You'll probably benefit from studying the invariant proof above.
     In particular, you may need some fact about the function strip-cdrs
     analogous to the lemma member-equal-strip-cars-bind above.

Below is one solution to this exercise.  Don't look at the solution,
however, until you've struggled a bit with it.  Notice that we didn't
actually change the definitions of add-phone and change-phone, but
added a hypothesis saying that the number is "new."  We could have
changed the definitions to check this and return the phonebook
unchanged if the number was already in use.

       (defun pnums-in-use (bk)
         (range bk))

       (defun phonenums-unique (bk)
         (setp (pnums-in-use bk)))

       (defun new-pnump (pnum bk)
         (not (member-equal pnum (pnums-in-use bk))))

       (defthm member-equal-strip-cdrs-rembind
         (implies (not (member-equal x (strip-cdrs y)))
                  (not (member-equal x (strip-cdrs (rembind z y))))))

       (defthm DEL-PHONE-PRESERVES-PHONENUMS-UNIQUE
         (implies (phonenums-unique bk)
                  (phonenums-unique (del-phone nm bk)))
         :hints (("Goal" :in-theory (enable range))))

       (defthm strip-cdrs-bind-non-member
         (implies (and (not (bound? x a))
                       (alistp a))
                  (equal (strip-cdrs (bind x y a))
                         (append (strip-cdrs a) (list y))))
         :hints (("Goal" :in-theory (enable bound?))))

       (defthm setp-append-list
         (implies (setp l)
                  (equal (setp (append l (list x)))
                         (not (member-equal x l)))))

       (defthm ADD-PHONE-PRESERVES-PHONENUMS-UNIQUE
         (implies (and (phonenums-unique bk)
                       (new-pnump pnum bk)
                       (alistp bk))
                  (phonenums-unique (add-phone nm pnum bk)))
         :hints (("Goal" :in-theory (enable range))))

       (defthm member-equal-strip-cdrs-bind
         (implies (and (not (member-equal z (strip-cdrs a)))
                       (not (equal z y)))
                  (not (member-equal z (strip-cdrs (bind x y a))))))

       (defthm CHANGE-PHONE-PRESERVES-PHONENUMS-UNIQUE
         (implies (and (phonenums-unique bk)
                       (new-pnump pnum bk)
                       (alistp bk))
                  (phonenums-unique (change-phone nm pnum bk)))
         :hints (("Goal" :in-theory (enable range))))

TUTORIAL4-DEFUN-SK-EXAMPLE    example of quantified notions

This example illustrates the use of defun-sk and defthm events to
reason about quantifiers.  See DEFUN-SK.  For a more through,
systematic beginner's introduction to quantification in ACL2, see
QUANTIFIER-TUTORIAL.

Many users prefer to avoid the use of quantifiers, since ACL2 provides
only very limited support for reasoning about quantifiers.

Here is a list of events that proves that if there are arbitrarily
large numbers satisfying the disjunction (OR P R), then either there
are arbitrarily large numbers satisfying P or there are arbitrarily
large numbers satisfying R.

     ; Introduce undefined predicates p and r.
     (defstub p (x) t)
     (defstub r (x) t)

     ; Define the notion that something bigger than x satisfies p.
     (defun-sk some-bigger-p (x)
       (exists y (and (< x y) (p y))))

     ; Define the notion that something bigger than x satisfies r.
     (defun-sk some-bigger-r (x)
       (exists y (and (< x y) (r y))))

     ; Define the notion that arbitrarily large x satisfy p.
     (defun-sk arb-lg-p ()
       (forall x (some-bigger-p x)))

     ; Define the notion that arbitrarily large x satisfy r.
     (defun-sk arb-lg-r ()
       (forall x (some-bigger-r x)))

     ; Define the notion that something bigger than x satisfies p or r.
     (defun-sk some-bigger-p-or-r (x)
       (exists y (and (< x y) (or (p y) (r y)))))

     ; Define the notion that arbitrarily large x satisfy p or r.
     (defun-sk arb-lg-p-or-r ()
       (forall x (some-bigger-p-or-r x)))

     ; Prove the theorem promised above.  Notice that the functions open
     ; automatically, but that we have to provide help for some rewrite
     ; rules because they have free variables in the hypotheses.  The
     ; ``witness functions'' mentioned below were introduced by DEFUN-SK.

     (thm
      (implies (arb-lg-p-or-r)
               (or (arb-lg-p)
                   (arb-lg-r)))
      :hints (("Goal"
               :use
               ((:instance some-bigger-p-suff
                           (x (arb-lg-p-witness))
                           (y (some-bigger-p-or-r-witness
                               (max (arb-lg-p-witness)
                                    (arb-lg-r-witness)))))
                (:instance some-bigger-r-suff
                           (x (arb-lg-r-witness))
                           (y (some-bigger-p-or-r-witness
                               (max (arb-lg-p-witness)
                                    (arb-lg-r-witness)))))
                (:instance arb-lg-p-or-r-necc
                           (x (max (arb-lg-p-witness)
                                   (arb-lg-r-witness))))))))

     ; And finally, here's a cute little example.  We have already
     ; defined above the notion (some-bigger-p x), which says that
     ; something bigger than x satisfies p.  Let us introduce a notion
     ; that asserts that there exists both y and z bigger than x which
     ; satisfy p.  On first glance this new notion may appear to be
     ; stronger than the old one, but careful inspection shows that y and
     ; z do not have to be distinct.  In fact ACL2 realizes this, and
     ; proves the theorem below automatically.

     (defun-sk two-bigger-p (x)
       (exists (y z) (and (< x y) (p y) (< x z) (p z))))

     (thm (implies (some-bigger-p x) (two-bigger-p x)))

     ; A technical point:  ACL2 fails to prove the theorem above
     ; automatically if we take its contrapositive, unless we disable
     ; two-bigger-p as shown below.  That is because ACL2 needs to expand
     ; some-bigger-p before applying the rewrite rule introduced for
     ; two-bigger-p, which contains free variables.  The moral of the
     ; story is:  Don't expect too much automatic support from ACL2 for
     ; reasoning about quantified notions.

     (thm (implies (not (two-bigger-p x)) (not (some-bigger-p x)))
          :hints (("Goal" :in-theory (disable two-bigger-p))))

TUTORIAL5-MISCELLANEOUS-EXAMPLES    miscellaneous ACL2 examples

The following examples are more advanced examples of usage of ACL2.
They are included largely for reference, in case someone finds them
useful.

FILE-READING-EXAMPLE    example of reading files in ACL2

This example illustrates the use of ACL2's IO primitives to read the
forms in a file.  See IO.

This example provides a solution to the following problem.  Let's say
that you have a file that contains s-expressions.  Suppose that you
want to build a list by starting with nil, and updating it
"appropriately" upon encountering each successive s-expression in the
file.  That is, suppose that you have written a function update-list
such that (update-list obj current-list) returns the list obtained by
"updating" current-list with the next object, obj, encountered in the
file.  The top-level function for processing such a file, returning the
final list, could be defined as follows.  Notice that because it opens
a channel to the given file, this function modifies state and hence
must return state.  Thus it actually returns two values:  the final
list and the new state.

       (defun process-file (filename state)
         (mv-let
          (channel state)
          (open-input-channel filename :object state)
          (mv-let (result state)
                  (process-file1 nil channel state) ;see below
                  (let ((state (close-input-channel channel state)))
                    (mv result state)))))

The function process-file1 referred to above takes the currently
constructed list (initially, nil), together with a channel to the file
being read and the state, and returns the final updated list.  Notice
that this function is tail recursive.  This is important because many
Lisp compilers will remove tail recursion, thus avoiding the potential
for stack overflows when the file contains a large number of forms.

       (defun process-file1 (current-list channel state)
         (mv-let (eofp obj state)
                 (read-object channel state)
                 (cond
                  (eofp (mv current-list state))
                  (t (process-file1 (update-list obj current-list)
                                    channel state)))))

FUNCTIONAL-INSTANTIATION-EXAMPLE    a small proof demonstrating functional instantiation

The example below demonstrates the use of functional instantiation,
that is, the use of a generic result in proving a result about specific
functions.  In this example we constrain a function to be associative
and commutative, with an identity or "root," on a given domain.  Next,
we define a corresponding function that applies the constrained
associative-commutative function to successive elements of a list.  We
then prove that the latter function gives the same value when we first
reverse the elements of the list.  Finally, we use functional
instantiation to derive the corresponding result for the function that
multiplies successive elements of a list.

The details of the proof (such as the in-theory event and particulars
of the lemmas) are not the point here.  Rather, the point is to
demonstrate the interaction of encapsulate events and
:functional-instance lemma-instances.  Of course, if you are interested
in details then you may find it helpful to run these events through
ACL2.

Also see CONSTRAINT for more about :functional-instance and see
LEMMA-INSTANCE for general information about the use of
previously-proved lemmas.

     (in-package "ACL2")

     (encapsulate
      (((ac-fn * *) => *)
       ((ac-fn-domain *) => *)
       ((ac-fn-root) => *))
      (local (defun ac-fn (x y) (+ x y)))
      (local (defun ac-fn-root () 0))
      (local (defun ac-fn-domain (x) (acl2-numberp x)))
      (defthm ac-fn-comm
        (equal (ac-fn x y)
               (ac-fn y x)))
      (defthm ac-fn-assoc
        (equal (ac-fn (ac-fn x y) z)
               (ac-fn x (ac-fn y z))))
      (defthm ac-fn-id
        (implies (ac-fn-domain x)
                 (equal (ac-fn (ac-fn-root) x)
                        x)))
      (defthm ac-fn-closed
        (and (ac-fn-domain (ac-fn x y))
             (ac-fn-domain (ac-fn-root)))))

     ;;;;;;;;;;;;;;;;;;;;;;;
     ; End of encapsulate. ;
     ;;;;;;;;;;;;;;;;;;;;;;;

     ; Define a ``fold'' function that iteratively applies ac-fn over a list.
     (defun ac-fn-list (x)
       (if (atom x)
           (ac-fn-root)
         (ac-fn (car x)
                (ac-fn-list (cdr x)))))

     ; Recognize lists all of whose elements are in the intended domain.
     (defun ac-fn-domain-list (x)
       (if (atom x)
           t
         (and (ac-fn-domain (car x))
              (ac-fn-domain-list (cdr x)))))

     ; Define a list reverse function.
     (defun rev (x)
       (if (atom x)
           nil
         (append (rev (cdr x))
                 (list (car x)))))

     ; The following is needed for proving ac-fn-list-append, which is
     ; needed for proving ac-fn-list-rev.
     (defthm ac-fn-list-closed
        (ac-fn-domain (ac-fn-list x)))

     ; Needed for proving ac-fn-list-rev:
     (defthm ac-fn-list-append
       (implies (and (ac-fn-domain-list x)
                     (ac-fn-domain-list y))
                (equal (ac-fn-list (append x y))
                       (ac-fn (ac-fn-list x)
                              (ac-fn-list y)))))

     ; Needed for proving ac-fn-list-rev:
     (defthm ac-fn-domain-list-rev
       (equal (ac-fn-domain-list (rev x))
              (ac-fn-domain-list x)))

     ; The following is a good idea because without it, the proof attempt
     ; for ac-fn-list-rev (see just below) fails with the term (HIDE
     ; (AC-FN-LIST NIL)).  It is often a good idea to disable
     ; executable-counterparts of functions that call constrained
     ; functions.
     (in-theory (disable (:executable-counterpart ac-fn-list)))

     (defthm ac-fn-list-rev
       (implies (ac-fn-domain-list x)
                (equal (ac-fn-list (rev x))
                       (ac-fn-list x))))

     ; Our goal now is to apply functional instantiation to ac-fn-list-rev
     ; in order to prove the corresponding theorem, times-list-rev, based
     ; on * instead of ac-fn.

     (defun times-list (x)
       (if (atom x)
           1
         (* (car x)
            (times-list (cdr x)))))

     (defun acl2-number-listp (x)
       (if (atom x)
           t
         (and (acl2-numberp (car x))
              (acl2-number-listp (cdr x)))))

     ; The following relies on the following built-in rules for * (whose
     ; statements correspond directly to their names): commutativity-of-*,
     ; associativity-of-*, and unicity-of-1.

     (defthm times-list-rev
       (implies (acl2-number-listp x)
                (equal (times-list (rev x))
                       (times-list x)))
       :hints (("Goal"
                :use
                ((:functional-instance
                  ac-fn-list-rev
                  ;; Instantiate the generic functions:
                  (ac-fn *)
                  (ac-fn-root (lambda () 1))
                  (ac-fn-domain acl2-numberp)
                  ;; Instantiate the other relevant functions:
                  (ac-fn-list times-list)
                  (ac-fn-domain-list acl2-number-listp))))))

GUARD-EXAMPLE    a brief transcript illustrating guards in ACL2

This note addresses the question:  what is the use of guards in ACL2?
Although we recommend that beginners try to avoid guards for a while,
we hope that the summary here is reasonably self-contained and will
provide a reasonable introduction to guards in ACL2.  For a more
systematic discussion, see GUARD.  For a summary of that topic,
see GUARD-QUICK-REFERENCE.

Before we get into the issue of guards, let us note that there are two
important "modes":

defun-mode -- "Does this defun add an axiom (`:logic mode') or not
(`:program mode')?"  (See DEFUN-MODE.)  Only :logic mode
functions can have their "guards verified" via mechanized proof; see
VERIFY-GUARDS.

set-guard-checking -- "Should runtime guard violations signal an error
(:all, and usually with t or :nowarn) or go undetected (nil, :none)?
Equivalently, are expressions evaluated in Common Lisp or in the
logic?"  (See SET-GUARD-CHECKING.)

_Prompt examples_

Here some examples of the relation between the ACL2 prompt and the
"modes" discussed above.  Also see DEFAULT-PRINT-PROMPT.  The
first examples all have ld-skip-proofsp nil; that is, proofs are _not_
skipped.

       ACL2 !>    ; logic mode with guard checking on
       ACL2 >     ; logic mode with guard checking off
       ACL2 p!>   ; program mode with guard checking on
       ACL2 p>    ; program mode with guard checking off

Here are some examples with default-defun-mode of :logic.

       ACL2 >     ; guard checking off, ld-skip-proofsp nil
       ACL2 s>    ; guard checking off, ld-skip-proofsp t
       ACL2 !>    ; guard checking on, ld-skip-proofsp nil
       ACL2 !s>   ; guard checking on, ld-skip-proofsp t

_Sample session_

     ACL2 !>(+ 'abc 3)

     ACL2 Error in TOP-LEVEL: The guard for the function symbol
     BINARY-+, which is (AND (ACL2-NUMBERP X) (ACL2-NUMBERP Y)),
     is violated by the arguments in the call (+ 'ABC 3).

     ACL2 !>:set-guard-checking nil
     ;;;; verbose output omitted here
     ACL2 >(+ 'abc 3)
     3
     ACL2 >(< 'abc 3)
     T
     ACL2 >(< 3 'abc)
     NIL
     ACL2 >(< -3 'abc)
     T
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(defun sum-list (x)
             (declare (xargs :guard (integer-listp x)
                             :verify-guards nil))
             (cond ((endp x) 0)
                   (t (+ (car x) (sum-list (cdr x))))))

     The admission of SUM-LIST is trivial, using the relation
     O< (which is known to be well-founded on the domain
     recognized by O-P) and the measure (ACL2-COUNT X).
     We observe that the type of SUM-LIST is described by the
     theorem (ACL2-NUMBERP (SUM-LIST X)).  We used primitive type
     reasoning.

     Summary
     Form:  ( DEFUN SUM-LIST ...)
     Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  None
     Time:  0.03 seconds
        (prove: 0.00, print: 0.00, proof tree: 0.00, other: 0.03)
      SUM-LIST
     ACL2 !>(sum-list '(1 2 3))

     ACL2 Warning [Guards] in TOP-LEVEL:  Guard-checking will be inhibited
     on recursive calls of the executable counterpart (i.e., in the ACL2
     logic) of SUM-LIST.  To check guards on all recursive calls:
       (set-guard-checking :all)
     To leave behavior unchanged except for inhibiting this message:
       (set-guard-checking :nowarn)

     6
     ACL2 !>(sum-list '(1 2 abc 3))

     ACL2 Error in TOP-LEVEL: The guard for the function symbol
     BINARY-+, which is (AND (ACL2-NUMBERP X) (ACL2-NUMBERP Y)),
     is violated by the arguments in the call (+ 'ABC 3).

     ACL2 !>:set-guard-checking nil
     ;;;; verbose output omitted here
     ACL2 >(sum-list '(1 2 abc 3))
     6
     ACL2 >(defthm sum-list-append
            (equal (sum-list (append a b))
                   (+ (sum-list a) (sum-list b))))

     << Starting proof tree logging >>

     Name the formula above *1.

     Perhaps we can prove *1 by induction.  Three induction
     schemes are suggested by this conjecture.  Subsumption
     reduces that number to two.  However, one of these is flawed
     and so we are left with one viable candidate.

     ...

     That completes the proof of *1.

     Q.E.D.

_Guard verification vs. defun_

           Declare Form                        Guards Verified?

       (declare (xargs :mode :program ...))          no
       (declare (xargs :guard g))                    yes
       (declare (xargs :guard g :verify-guards nil)) no
       (declare (xargs ...<no :guard>...))           no

     ACL2 >:pe sum-list
      l        8  (DEFUN SUM-LIST (X)
                   (DECLARE (XARGS :GUARD (INTEGER-LISTP X)
                                   :VERIFY-GUARDS NIL))
                   (COND ((ENDP X) 0)
                         (T (+ (CAR X) (SUM-LIST (CDR X))))))
     ACL2 >(verify-guards sum-list)
     The non-trivial part of the guard conjecture for SUM-LIST,
     given the :type-prescription rule SUM-LIST, is

     Goal
     (AND (IMPLIES (AND (INTEGER-LISTP X) (NOT (CONSP X)))
                   (EQUAL X NIL))
          (IMPLIES (AND (INTEGER-LISTP X) (NOT (ENDP X)))
                   (INTEGER-LISTP (CDR X)))
          (IMPLIES (AND (INTEGER-LISTP X) (NOT (ENDP X)))
                   (ACL2-NUMBERP (CAR X)))).

     ...

     ACL2 >:pe sum-list
      lv       8  (DEFUN SUM-LIST (X)
                   (DECLARE (XARGS :GUARD (INTEGER-LISTP X)
                                   :VERIFY-GUARDS NIL))
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(sum-list '(1 2 abc 3))

     ACL2 Error in TOP-LEVEL: The guard for the function symbol
     SUM-LIST, which is (INTEGER-LISTP X), is violated by the
     arguments in the call (SUM-LIST '(1 2 ABC ...)).  See :DOC trace for a useful
     debugging utility.  See :DOC set-guard-checking for information about
     suppressing this check with (set-guard-checking :none), as recommended for
     new users.

     ACL2 !>:set-guard-checking nil
     ;;;; verbose output omitted here
     ACL2 >(sum-list '(1 2 abc 3))
     6
     ACL2 >:comp sum-list
     Compiling gazonk0.lsp.
     End of Pass 1.
     End of Pass 2.
     Finished compiling gazonk0.lsp.
     Loading gazonk0.o
     start address -T 1bbf0b4 Finished loading gazonk0.o
     Compiling gazonk0.lsp.
     End of Pass 1.
     End of Pass 2.
     Finished compiling gazonk0.lsp.
     Loading gazonk0.o
     start address -T 1bc4408 Finished loading gazonk0.o
      SUM-LIST
     ACL2 >:q

     Exiting the ACL2 read-eval-print loop.
     ACL2>(trace sum-list)
     (SUM-LIST)

     ACL2>(lp)

     ACL2 Version 1.8.  Level 1.  Cbd "/slocal/src/acl2/v1-9/".
     Type :help for help.
     ACL2 >(sum-list '(1 2 abc 3))
     6
     ACL2 >(sum-list '(1 2 3))
       1> (SUM-LIST (1 2 3))>
         2> (SUM-LIST (2 3))>
           3> (SUM-LIST (3))>
             4> (SUM-LIST NIL)>
             <4 (SUM-LIST 0)>
           <3 (SUM-LIST 3)>
         <2 (SUM-LIST 5)>
       <1 (SUM-LIST 6)>
     6
     ACL2 >:pe sum-list-append
               9  (DEFTHM SUM-LIST-APPEND
                          (EQUAL (SUM-LIST (APPEND A B))
                                 (+ (SUM-LIST A) (SUM-LIST B))))
     ACL2 >(verify-guards sum-list-append)

     The non-trivial part of the guard conjecture for
     SUM-LIST-APPEND, given the :type-prescription rule SUM-LIST,
     is

     Goal
     (AND (TRUE-LISTP A)
          (INTEGER-LISTP (APPEND A B))
          (INTEGER-LISTP A)
          (INTEGER-LISTP B)).

     ...

     ****** FAILED ******* See :DOC failure ****** FAILED ******
     ACL2 >(defthm common-lisp-sum-list-append
              (if (and (integer-listp a)
                       (integer-listp b))
                  (equal (sum-list (append a b))
                         (+ (sum-list a) (sum-list b)))
                  t)
              :rule-classes nil)

     << Starting proof tree logging >>

     By the simple :rewrite rule SUM-LIST-APPEND we reduce the
     conjecture to

     Goal'
     (IMPLIES (AND (INTEGER-LISTP A)
                   (INTEGER-LISTP B))
              (EQUAL (+ (SUM-LIST A) (SUM-LIST B))
                     (+ (SUM-LIST A) (SUM-LIST B)))).

     But we reduce the conjecture to T, by primitive type
     reasoning.

     Q.E.D.
     ;;;; summary omitted here
     ACL2 >(verify-guards common-lisp-sum-list-append)

     The non-trivial part of the guard conjecture for
     COMMON-LISP-SUM-LIST-APPEND, given the :type-prescription
     rule SUM-LIST, is

     Goal
     (AND (IMPLIES (AND (INTEGER-LISTP A)
                        (INTEGER-LISTP B))
                   (TRUE-LISTP A))
          (IMPLIES (AND (INTEGER-LISTP A)
                        (INTEGER-LISTP B))
                   (INTEGER-LISTP (APPEND A B)))).

     ...

     Q.E.D.

     That completes the proof of the guard theorem for
     COMMON-LISP-SUM-LIST-APPEND.  COMMON-LISP-SUM-LIST-APPEND
     is compliant with Common Lisp.
     ;;;; Summary omitted here.
     ACL2 >(defthm foo (consp (mv x y)))

     ...

     Q.E.D.

     ACL2 >(verify-guards foo)

     ACL2 Error in (VERIFY-GUARDS FOO): The number of values we
     need to return is 1 but the number of values returned by the
     call (MV X Y) is 2.

     > (CONSP (MV X Y))

     ACL2 Error in (VERIFY-GUARDS FOO): The guards for FOO cannot
     be verified because the theorem has the wrong syntactic
     form.  See :DOC verify-guards.

MUTUAL-RECURSION-PROOF-EXAMPLE    a small proof about mutually recursive functions

Sometimes one wants to reason about mutually recursive functions.
Although this is possible in ACL2, it can be a bit awkward.  This
example is intended to give some ideas about how one can go about such
proofs.

For an introduction to mutual recursion in ACL2, see
MUTUAL-RECURSION.

We begin by defining two mutually recursive functions:  one that
collects the variables from a term, the other that collects the
variables from a list of terms.  We actually imagine the term argument
to be a pseudo-termp; see PSEUDO-TERMP.

     (mutual-recursion

     (defun free-vars1 (term ans)
       (cond ((atom term)
              (add-to-set-eq term ans))
             ((fquotep term) ans)
             (t (free-vars1-lst (fargs term) ans))))

     (defun free-vars1-lst (lst ans)
       (cond ((atom lst) ans)
             (t (free-vars1-lst (cdr lst)
                                (free-vars1 (car lst) ans)))))

     )

The idea of the following function is that it suggests a proof by
induction in two cases, according to the top-level if structure of the
body.  In one case, (atom x) is true, and the theorem to be proved
should be proved under no additional hypotheses except for (atom x).
In the other case, (not (atom x)) is assumed together with three
instances of the theorem to be proved, one for each recursive call in
this case.  So, one instance substitutes (car x) for x; one substitutes
(cdr x) for x; and the third substitutes (cdr x) for x and (free-vars1
(car x) ans) for ans.  If you think about how you would go about a hand
proof of the theorem to follow, you'll come up with a similar scheme.

     (defun symbol-listp-free-vars1-induction (x ans)
       (if (atom x)
     ; then we just make sure x and ans aren't considered irrelevant
           (list x ans)
         (list (symbol-listp-free-vars1-induction (car x) ans)
               (symbol-listp-free-vars1-induction (cdr x) ans)
               (symbol-listp-free-vars1-induction
                (cdr x)
                (free-vars1 (car x) ans)))))

We now prove the two theorems together as a conjunction, because the
inductive hypotheses for one are sometimes needed in the proof of the
other (even when you do this proof on paper!).

     (defthm symbol-listp-free-vars1
       (and (implies (and (pseudo-termp x)
                          (symbol-listp ans))
                     (symbol-listp (free-vars1 x ans)))
            (implies (and (pseudo-term-listp x)
                          (symbol-listp ans))
                     (symbol-listp (free-vars1-lst x ans))))
       :hints
       (("Goal" :induct (symbol-listp-free-vars1-induction x ans))))

The above works, but let's try for a more efficient proof, which avoids
cluttering the proof with irrelevant (false) inductive hypotheses.

     (ubt 'symbol-listp-free-vars1-induction)

     (defun symbol-listp-free-vars1-induction (flg x ans)

     ; Flg is non-nil (or t) if we are ``thinking'' of a single term.

       (if (atom x)
           (list x ans)
         (if flg
             (symbol-listp-free-vars1-induction nil (cdr x) ans)
           (list (symbol-listp-free-vars1-induction t (car x) ans)
                 (symbol-listp-free-vars1-induction
                  nil
                  (cdr x)
                  (free-vars1 (car x) ans))))))

We now state the theorem as a conditional, so that it can be proved
nicely using the induction scheme that we have just coded.  The prover
will not store an if term as a rewrite rule, but that's OK (as long as
we tell it not to try), because we're going to derive the corollaries
of interest later and make them into rewrite rules.

     (defthm symbol-listp-free-vars1-flg
       (if flg
           (implies (and (pseudo-termp x)
                         (symbol-listp ans))
                    (symbol-listp (free-vars1 x ans)))
         (implies (and (pseudo-term-listp x)
                       (symbol-listp ans))
                  (symbol-listp (free-vars1-lst x ans))))
       :hints
       (("Goal" :induct (symbol-listp-free-vars1-induction flg x ans)))
       :rule-classes nil)

And finally, we may derive the theorems we are interested in as
immediate corollaries.

     (defthm symbol-listp-free-vars1
       (implies (and (pseudo-termp x)
                     (symbol-listp ans))
                (symbol-listp (free-vars1 x ans)))
       :hints (("Goal" :by (:instance symbol-listp-free-vars1-flg
                                      (flg t)))))

     (defthm symbol-listp-free-vars1-lst
       (implies (and (pseudo-term-listp x)
                     (symbol-listp ans))
                (symbol-listp (free-vars1-lst x ans)))
       :hints (("Goal" :by (:instance symbol-listp-free-vars1-flg
                                      (flg nil)))))

EMACS    emacs support for ACL2

Many successful ACL2 users run in an shell under the Emacs editor.  If
you do so, then you may wish to load the distributed file
emacs/emacs-acl2.el.  The file begins with considerable comments
describing what it offers.  It is intended to work both with GNU Emacs
and XEmacs.

If you are not comfortable with Emacs, you may prefer to use an
Eclipse-based interface; see ACL2-SEDAN.

INTERESTING-APPLICATIONS    some industrial examples of ACL2 use

ACL2 is an interactive system in which you can model digital artifacts
and guide the system to mathematical proofs about the behavior of those
models.  It has been used at such places as AMD, Centaur, IBM, and
Rockwell Collins to verify interesting properties of commercial
designs.  It has been used to verify properties of models of
microprocessors, microcode, the Sun Java Virtual Machine, operating
system kernels, other verifiers, and interesting algorithms.

Here we list just a few of the industrially-relevant results obtained
with ACL2.  Reading the list may help you decide you want to learn how
to use ACL2.  If you do decide you want to learn more, we recommend
that you take The Tours after you leave this page.

ACL2 was used at Motorola Government Systems to certify several
microcode programs for the Motorola CAP digital signal processor,
including a comparator sort program that is particularly subtle. In the
same project, ACL2 was used to model the CAP at both the pipelined
architectural level and the instruction set level.  The architectural
model was bit- and cycle-accurate: it could be used to predict every
bit of memory on every cycle.  The models were proved equivalent under
certain hypotheses, the most important being a predicate that analyzed
the microcode for certain pipeline hazards. This predicate defined what
the hazards were, syntactically, and the equivalence of the two models
established the correctness of this syntactic characterization of
hazards.  Because ACL2 is a functional programming language, the ACL2
models and the hazard predicate could be executed.  ACL2 executed
microcode interpretr several times faster than the hardware simulator
could execute it - with assurance that the answers were equivalent.  In
addition, the ACL2 hazard predicate was executed on over fifty
microcode programs written by Motorola engineers and extracted from the
ROM mechanically. Hazards were found in some of these.  (See, for
example, Bishop Brock and Warren. A. Hunt, Jr. "Formal analysis of the
motorola CAP DSP." In Industrial-Strength Formal Methods.
Springer-Verlag, 1999.)

ACL2 was used at Advanced Micro Devices (AMD) to verify the compliance
of the AMD Athon's (TM) elementary floating point operations with their
IEEE 754 specifications. This followed ground-breaking work in 1995
when ACL2 was used to prove the correctness of the microcode for
floating-point division on the AMD K5. The AMD Athlon work proved
addition, subtraction, multiplication, division, and square root
compliant with the IEEE standard. Bugs were found in RTL designs. These
bugs had survived undetected in hundreds of millions of tests but were
uncovered by ACL2 proof attempts. The RTL in the fabricated Athlon FPU
has been mechanically verified by ACL2.  Similar ACL2 proofs have been
carried out for every major AMD FPU design fabricated since the Athlon.
(See for example, David Russinoff. "A mechanically checked proof of
correctness of the AMD5K86 floating-point square root microcode".
Formal Methods in System Design Special Issue on Arithmetic Circuits,
1997.)

ACL2 was used at IBM to verify the floating point divide and square root
on the IBM Power 4.  (See Jun Sawada. "Formal verification of divide
and square root algorithms using series calculation". In Proceedings of
the ACL2 Workshop 2002, Grenoble, April 2002.)

ACL2 was used to verify floating-point addition/subtraction
instructions for the media unit from Centaur Technology's 64-bit,
X86-compatible microprocessor. This unit implements over one hundred
instructions, with the most complex being floating-point
addition/subtraction. The media unit can add/subtract four pairs of
floating-point numbers every clock cycle with an industry-leading
two-cycle latency. The media unit was modeled by translating its
Verilog design into an HDL deeply embedded in the ACL2 logic. The proofs
used a combination of AIG- and BDD-based symbolic simulation, case
splitting, and theorem proving.  (See Warren A. Hunt, Jr. and Sol
Swords. "Centaur Technology Media Unit Verification". In CAV '09:
Proceedings of the 21st International Conference on Computer Aided
Verification, pages 353-367, Berlin, Heidelberg, 2009. Springer-Verlag.)

Rockwell Collins used ACL2 to prove information flow properties about
its Advanced Architecture MicroProcessor 7 Government Version (AAMP7G),
a Multiple Independent Levels of Security (MILS) device for use in
cryptographic applications. The AAMP7G provides MILS capability via a
verified secure hardware-based separation kernel. The AAMP7G's design
was proved to achieve MILS using ACL2, in accordance with the standards
set by EAL-7 of the Common Criteria and Rockwell Collins has received
National Security Agency (NSA) certification for the device based on
this work.  (See David S. Hardin, Eric W. Smith, and William. D. Young.
"A robust machine code proof framework for highly secure applications".
In Proceedings of the sixth international workshop on the ACL2 theorem
prover and its applications, pages 11-20, New York, NY, USA, 2006. ACM.)

Key properties of the Sun Java Virtual Machine and its bytecode
verifier were verified in ACL2. Among the properties proved were that
certain invariants are maintained by class loading and that the
bytecode verifier insures that execution is safe. In addition, various
JVM bytecode programs have been verified using this model of the JVM.
(See Hanbing Liu. Formal Specification and Verification of a JVM and
its Bytecode Verifier. PhD thesis, University of Texas at Austin, 2006.)

The Boyer-Moore fast string searching algorithm was verified with ACL2,
including a model of the JVM bytecode for the search algorithm itself
(but not the preprocessing).  (See J S. Moore and Matt Martinez. "A
mechanically checked proof of the correctness of the Boyer-Moore fast
string searching algorithm." In Engineering Methods and Tools for
Software Safety and Security pages 267-284. IOS Press, 2009.)

ACL2 was used to verify the fidelity between an ACL2-like theorem prover
and a simple ("trusted by inspection") proof checker, thereby
establishing (up to the soundness of ACL2) the soundness of the
ACL2-like theorem prover.  This project was only part of a much larger
project in which the resulting ACL2 proof script was then hand-massaged
into a script suitable for the ACL2-like theorem prover to process,
generating a formal proof of its fidelity that has been checked by the
trusted proof checker.  (See Jared Davis.  Milawa: A Self-Verifying
Theorem Prover.  Ph.D. Thesis, University of Texas at Austin, December,
2009.)

These are but a few of the interesting projects carried out with ACL2.
Many of the authors mentioned above have versions of the papers on
their web pages.  In addition, see the link to "Books and Papers about
ACL2 and Its Applications" on the ACL2 home page
(`http://www.cs.utexas.edu/users/moore/acl2').  Also see the
presentations in each of the workshops listed in the link to "ACL2
Workshops" on the ACL2 home page.

INTRODUCTION-TO-THE-THEOREM-PROVER    how the theorem prover works - level 0

Software is complex, and ACL2 is a piece of software that is used to
analyze software - adding another layer of complexity.  Furthermore,
instead of being limited to static analysis for certain fixed
properties, ACL2 allows you - indeed, forces you - to formalize the
problem and the questions.  It "knows" nothing inherent about your
problem before you start to interact with it.  But it can be used to
help answer the most complicated questions you can ask about software.

All this is to say that it is not the kind of tool that you just
install and then start to use effectively.  So OK, you've installed it
or confirmed that you can invoke it.  Good for you.  Now you have to
learn how to use it!  Your success ultimately comes down to your
understanding of your problem domain and your appropriate exploitation
of ACL2's strengths and avoidance of its weaknesses.  So put aside the
idea of sitting down and interacting with it.  Instead, learn about it.

We assume you know some of the industrial applications of ACL2.
Realizing that such things can be done may sustain you during the long
learning curve!  We also assume you have taken both the Flying Tour and
the Walking Tour.  The tours give you a good overview of the whole
system where this tutorial focuses on how to use the prover itself.

If you haven't visited these links, please do so now.

This tutorial will take you several hours - maybe several days - to work
through.  Do not breeze through it as you might a blog.  Think your way
through it.  Remember what you read.  Do not take short cuts.  If you
start to use ACL2 before you really know how, it will only frustrate
you.

We recommend that you read this tutorial with an HTML browser so that
you can see which links you've followed and which you have not.  To
give you a sense of what is in store, here is a map of this document.
But don't navigate through it from here! Read it linearly, following
the links when the text directs you to.

      INTRODUCTION-TO-THE-THEOREM-PROVER
          INTRODUCTION-TO-REWRITE-RULES-PART-1
              SPECIAL-CASES-FOR-REWRITE-RULES
              EQUIVALENT-FORMULAS-DIFFERENT-REWRITE-RULES
          INTRODUCTION-TO-KEY-CHECKPOINTS
              DEALING-WITH-KEY-COMBINATIONS-OF-FUNCTION-SYMBOLS
              GENERALIZING-KEY-CHECKPOINTS
              POST-INDUCTION-KEY-CHECKPOINTS
          INTRODUCTION-TO-REWRITE-RULES-PART-2
              STRONG-REWRITE-RULES
                  PRACTICE-FORMULATING-STRONG-RULES
                      PRACTICE-FORMULATING-STRONG-RULES-1
                      PRACTICE-FORMULATING-STRONG-RULES-2
                      PRACTICE-FORMULATING-STRONG-RULES-3
                      PRACTICE-FORMULATING-STRONG-RULES-4
                      PRACTICE-FORMULATING-STRONG-RULES-5
                      PRACTICE-FORMULATING-STRONG-RULES-6
              SPECIFIC-KINDS-OF-FORMULAS-AS-REWRITE-RULES
              FURTHER-INFORMATION-ON-REWRITING
          INTRODUCTION-TO-THE-DATABASE
          INTRODUCTION-TO-HINTS
          INTRODUCTION-TO-A-FEW-SYSTEM-CONSIDERATIONS
          INTRODUCTORY-CHALLENGES
              INTRODUCTORY-CHALLENGE-PROBLEM-1
              INTRODUCTORY-CHALLENGE-PROBLEM-2
              INTRODUCTORY-CHALLENGE-PROBLEM-3
              (there are others but at least do a few)
          FREQUENTLY-ASKED-QUESTIONS-BY-NEWCOMERS

If any of the links above are marked as "visited" by your browser, use
your browser's tools menu to mark all links as unvisited.  As you can
see, we really think you'll get the most out of this document if you
take it seriously.  As you read, you will see some links to "advanced"
topics.  These are marked with a tiny warning sign, "<>".  They lead
out of this linear tutorial and into ACL2's hypertext reference manual.
We recommend that you not visit any of these advanced links until you
have read the entire tutorial at least once.

After you finish this tutorial material, we recommend that you look at
the ACL2 Demos, at the "Demos" link of the ACL2 home page,
`http://www.cs.utexas.edu/users/moore/acl2'.

Most users of ACL2 have bought the book

Computer-Aided Reasoning: An Approach, Kaufmann, Manolios, and Moore,
Kluwer Academic Publishers, June, 2000

which is available in paperback from Lulu for approximately $20 (as of
2010).  See `http://www.lulu.com/content/1746161'.  That book contains
hundreds of exercises in programming, proof, and using The Method
described here to prove theorems.  Solutions to the exercises are
online.  For more information about the book and a companion one (also
available on Lulu) about industrial applications of ACL2, see

`http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html#Books'

Using ACL2 is akin to having a partner in the theorem proving
enterprise.  It will do some of the work and you will do some of the
work.  It can't really be any other way because theorem proving is
undecidable.  You bring a quirkly, error-prone, creative insight to the
problem, and ACL2 brings accuracy, logic, and perserverance.

Here we describe a "model" of how the system works and introduce some
of the ideas and terminology you'll use repeatedly when interacting
with it.

This article is about the theorem prover itself, not the programming
language and not the logic.  We assume you know enough about the ACL2
programming language that you can define simple functions, run them, and
read and write ACL2 constants and terms.  For some examples of what
we'll take for granted about ACL2 programming, see
PROGRAMMING-KNOWLEDGE-TAKEN-FOR-GRANTED.

We also assume you know enough about logic to understand, for example,
the words we use to talk about formulas and proofs.  To see some
examples of what we'll take for granted about your knowledge of logic
terminology, see LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED.

When you give the theorem prover a goal formula to prove, it tries to
prove it by breaking it down into subgoals, each of which must be
proved in order to prove the original goal.  This breaking apart of the
goal is done by various proof techniques built into ACL2.  Different
proof techniques break the formula apart in different ways.  For
example, the simplifier rips apart the propositional structure to
isolate the various cases and applies rewrite rules to simplify the
subterms of the formula, while the induction engine will attempt to
break the goal into some base cases and some induction steps.

The theorem prover's behavior is affected by a database of rules
derived from axioms, definitions, and previously proved theorems.  The
database also records the enabled status of each rule; only enabled
rules are seen by the prover and you can set the status of a rule.
There are many other user-settable switches and parameters affecting
the behavior of the prover; you'll learn about some of them later.

You guide the theorem prover most of the time simply by identifying
lemmas for it to prove.  (A lemma is just a theorem that you think is
useful in the proofs of other theorems.)

Why does this guide the theorem prover?  Because every time you get the
system to prove a theorem, it turns the theorem into a rule (unless you
tell it not to) and stores the rule in the database.  That changes how
the prover behaves subsequently.  But you determine the kind of rule
ACL2 stores.

To learn to "drive" the theorem prover you have to learn how various
rules affect the system's behavior and how it turns proved formulas
into rules.  But before we discuss this, we discuss a more mathematical
activity: how do you figure out the lemmas ACL2 will need in order for
it to prove interesting theorems?  ACL2 can often help you in this
activity, if you use it in the right way.

Here is the way we recommend you use ACL2.

The Method.

(1) you present ACL2 with the goal conjecture to prove

(2) typically, it fails to prove it (or you abort its attempt), but it
prints some Key Checkpoints

(3) you look at the Key Checkpoints and decide that you know a fact that
will help; this tutorial will present some helpful questions to keep in
mind

(4) you formalize your knowledge as a formula, along with directions
for how ACL2 should turn the formula into a rule; this tutorial will
tell you about the most commonly used rule, the rewrite rule

(5) you recursively apply The Method to get ACL2 to prove your formula
and to store it as the kind of rule you specified

(6) go to step (1)

Caveat: This approach simply won't work on some theorems!  Basically,
this is a "troubleshooting" approach, where you're letting ACL2
determine the basic strategy and you're just helping with the subgoals.
But for some theorems, ACL2's approach will be misguided and no amount
of troubleshooting will salvage its strategy.  You'll have a sense that
this is happening when it happens because the formulas ACL2 presents to
you will raise issues that feel irrelevant to you.  The basic truth is
that if you think a formula is always true there are usually strong
intuitive reasons behind your belief.  If you were asked to defend your
belief, you'd start to explain your reasons and with training you can
turn that into a proof.  So when ACL2's formulas present you with
things you haven't thought of either (a) you'll have an "Ah ha!"
moment when you realize you hadn't considered that case or (b) you'll
realize that ACL2's approach is different from your intuitive "proof."

But, surprisingly often, the troubleshooting approach to finding proofs
works quite well, especially as you rein in your expectations and
develop a sense of what ACL2 can handle on its own.  Of course, if you
can decompose the proof into a couple of main lemmas before you start,
so much the better: write down your sequence of lemmas, thinking about
the rules you want them to generate, and get ACL2 to prove each of them
before giving it the main theorem.  This proof planning approach will
gradually become an integral part of your use of The Method.

The only mechanized help we can offer with The Method, aside from the
theorem prover itself, are tools to help you manage the stack of
subgoals it generates when, in step (5) you recursively apply The
Method to a lemma.  There are both Emacs and Eclipse tools available.

To use The Method you have to read the Key Checkpoints printed at the
very end of failed proof attempts, just after the line that reads:

     The key checkpoint goals, below, may help you to debug this failure.

Most users do not read the output from successful proofs and do not
read the output during a proof - they just let it stream by as a sort
of gestalt meter on the theorem prover's progress or lack thereof.  For
example, you'll be able to tell it is in a loop and needs to be
interrupted.

You will respond to most Key Checkpoints by formulating new lemmas for
the system to prove and store as rules designed by you to alter ACL2's
behavior so that it proves the Key Checkpoints.  You will give each
lemma a name and write some formula to express the mathematical idea.
You'll command ACL2 to prove it by typing:

     (defthm name
             formula
             ...)

In the "..." you may provide two other kinds of information: hints for
how to prove formula and directives, called rule-classes, for how to
convert formula into a rule after it has proved formula.  Note that you
are in charge of determining what kind of rule ACL2 generates!  There
are over a dozen different types of rules with many opportunities to
specialize each type.  But the most common kind of rule you'll want to
generate is a rewrite rule.

We recommend that you read the following topics in the following order,
without skipping anything but links into the reference manual, which
are marked by the little warning sign, "<>".

(1) See INTRODUCTION-TO-REWRITE-RULES-PART-1 to read about the
use and design of rewrite rules.

(2) See INTRODUCTION-TO-KEY-CHECKPOINTS to see how to use The
Method to help you design rules.

(3) See INTRODUCTION-TO-REWRITE-RULES-PART-2 for general
guidance on how to turn formulas into effective rules.

(4) See INTRODUCTION-TO-THE-DATABASE to see how to issue
commands that build different kinds of rules and that affect the
enabled status of existing rules.

(5) See INTRODUCTION-TO-HINTS to see how to give the prover
hints for how to prove specific theorems or even subgoals of specific
proof attempts.

(6) See INTRODUCTION-TO-A-FEW-SYSTEM-CONSIDERATIONS for a few
words about system aspects of interacting with ACL2.

(7) See INTRODUCTORY-CHALLENGES for a graduated sequence of
good challenge problems for the new user to tackle.  Do not skip this
section!  It is here that you really learn how to use ACL2 - by using
it.

(8) See FREQUENTLY-ASKED-QUESTIONS-BY-NEWCOMERS for a list of
questions that new users frequently ask, answered mainly by providing
links into the reference manual.  We recommend that you skim through
these questions and remember that you can find the answers here later.
We are very interested in receiving suggestions for how to improve this
FAQ and this tutorial.  See the ACL2 home page, specifically the link
"Mailing Lists".

Please read all of the material cited above (skipping only the
reference-manual links ("<>")) before you try to use ACL2 on problems
of your own.

By this point you should have read, at least, the following topics from
this tutorial introduction to the theorem prover:

      INTRODUCTION-TO-THE-THEOREM-PROVER
          INTRODUCTION-TO-REWRITE-RULES-PART-1
              SPECIAL-CASES-FOR-REWRITE-RULES
              EQUIVALENT-FORMULAS-DIFFERENT-REWRITE-RULES
          INTRODUCTION-TO-KEY-CHECKPOINTS
              DEALING-WITH-KEY-COMBINATIONS-OF-FUNCTION-SYMBOLS
              GENERALIZING-KEY-CHECKPOINTS
              POST-INDUCTION-KEY-CHECKPOINTS
          INTRODUCTION-TO-REWRITE-RULES-PART-2
              STRONG-REWRITE-RULES
                  PRACTICE-FORMULATING-STRONG-RULES
                      PRACTICE-FORMULATING-STRONG-RULES-1
                      PRACTICE-FORMULATING-STRONG-RULES-2
                      PRACTICE-FORMULATING-STRONG-RULES-3
                      PRACTICE-FORMULATING-STRONG-RULES-4
                      PRACTICE-FORMULATING-STRONG-RULES-5
                      PRACTICE-FORMULATING-STRONG-RULES-6
              SPECIFIC-KINDS-OF-FORMULAS-AS-REWRITE-RULES
              FURTHER-INFORMATION-ON-REWRITING
          INTRODUCTION-TO-THE-DATABASE
          INTRODUCTION-TO-HINTS
          INTRODUCTION-TO-A-FEW-SYSTEM-CONSIDERATIONS
          INTRODUCTORY-CHALLENGES
              INTRODUCTORY-CHALLENGE-PROBLEM-1
              INTRODUCTORY-CHALLENGE-PROBLEM-2
              INTRODUCTORY-CHALLENGE-PROBLEM-3
              (there are others but at least do a few)
          FREQUENTLY-ASKED-QUESTIONS-BY-NEWCOMERS

We also recommend that you look at the ACL2 Demos, at the "demos" link
of the ACL2 home page `http://www.cs.utexas.edu/users/moore/acl2'.

Most users of ACL2 have bought the book

Computer-Aided Reasoning: An Approach, Kaufmann, Manolios, and Moore,
Kluwer Academic Publishers, June, 2000

which is available in paperback from Lulu for approximately $20 (as of
2010).  See `http://www.lulu.com/content/1746161'.  That book contains
hundreds of exercises in programming, proof, and using The Method to
prove theorems.  Solutions to the exercises are online.  For more
information about the book and a companion one (also available on Lulu)
about industrial applications of ACL2, see

`http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html#Books'

Thank you for spending the time to get acquainted with the basics of the
ACL2 theorem prover.  Don't hesitate to send further questions to the
ACL2 Help address on the "Mailing Lists" link of the ACL2 home page.

End of Tutorial Introduction to the Theorem Prover

Below is a list of all of the topics cited on this page.

ARCHITECTURE-OF-THE-PROVER    a simple overview of how the prover works

Six built-in proof techniques are used by ACL2 to decompose the goal
formula  into subgoals.

simplification - decision procedures and rewriting with previously
proved rules, but actually including a host of other techniques under
your  control.  Simplification is the only proof technique that can
reduce a  formula to 0 subgoals (i.e., prove it) rather than just
transform it to other  formulas.  The predominant activity in most
proofs is simplification.  There  are many ways you can affect what the
simplifier does to your formulas.   Good users spend most of their time
thinking about how to control the  simplifier.

destructor elimination - getting rid of "destructor terms" like  (CAR
X) and (CDR X) by replacing a variable, e.g., X, by a  "constructor"
term, e.g., (CONS A B).  But you can tell ACL2 about new
destructor/constructor combinations.

cross-fertilization - using an equivalence hypothesis by substituting
one side for the other into the conclusion  and then throwing the
hypothesis away.   This is a heuristic that helps use an inductive
hypothesis and prepare for  another induction.

generalization - replacing a term by a new variable and restricting
the new variable to have some of the properties of the term.  You can
control the restrictions imposed on the new variable.  This is a
heuristic  that prepares the goal for another induction.

elimination of irrelevance - throwing away unnecessary hypotheses.
This is a heuristic that prepares the goal for another induction.

induction - selecting an induction scheme to prove a formula.
Inductions  are "suggested" by the recursive functions appearing in the
formula.  But you  can control what inductions are suggested by terms.

But you can add additional techniques, called clause processors.

The various techniques are tried in turn, with simplification first and
induction last.  Each technique reports one of three outcomes: it found
nothing to change (i.e., the technique doesn't apply to that subgoal),
it decided to abort the proof attempt (typically because there is
reason to  believe the proof is failing), or it decomposed the goal
into k  subgoals.

The last outcome has a special case: if k is 0 then the technique proved
the goal.  Whenever k is non-0, the process starts over again with
simplification on each of the k subgoals.  However, it saves up all the
subgoals for which induction is the only proof technique left to try.
That  way you see how it performs on every base case and induction step
of one  induction before it launches into another induction.

It runs until you or one of the proof techniques aborts the proof
attempt or  until all subgoals have been proved.

Note that if simplification produces a subgoal, that subgoal is
re-simplified.  This process continues until the subgoal cannot be
simplified further.  Only then is the next proof technique is tried.
Such  suboals are said to be stable under simplification.

While this is happening, the prover prints an English narrative
describing  the process.  Basically, after each goal is printed, the
system prints an  English paragraph that names the next applicable
proof technique, gives a  brief description of what that technique does
to the subgoal, and says how  many new subgoals are produced.  Then
each subgoal is dealt with in turn.

If the proof is successful, you could read this log as a proof of the
conjecture.  But output from successful proofs is generally never read
because it is not important to The Method described in
introduction-to-the-theorem-prover.

The output of an unsuccessful proof attempt concludes with some key
checkpoints which usually bear looking at.

DEALING-WITH-KEY-COMBINATIONS-OF-FUNCTION-SYMBOLS    how to get rid of key combinations of function symbols

Suppose REV reverses a list, MEMBER checks that its first argument is
an element of its second, and SQUARES-PLUS-3P is some complicated
predicate.  Suppose you're proving some Main Theorem that involves those
concepts and the theorem prover presents you with the following hideous
formula as a key checkpoint.  What action should you take?

Hint: Don't read the formula "for sense," i.e., don't try to understand
what this formula is saying!  Just look at every subterm involving a
nest of two function symbols and ask if you know something about those
two symbols that allows you to simplify that one subterm.

     (IMPLIES (AND (CONSP X)
                   (MEMBER (+ 3 (* I I)) (REV X))
                   (LIST-OF-INTEGERS X)
                   (INTEGERP I)
                   (<= 0 I)
                   (INTEGERP K)
                   (<= 0 K)
                   (< I K)
                   (SQUARES-PLUS-3P K X)
                   (NOT (EQUAL (CAR X) (+ 3 (* I I))))
                   (NOT (MEMBER (+ 3 (* I I)) X)))
              (SQUARES-PLUS-3P K (REV X)))?

The experienced ACL2 user will stop reading at the second hypothesis!

                   (MEMBER (+ 3 (* I I)) (REV X))

The combination of MEMBER and REV can be simplified.  The question "is
e a member of (REV x)" can be answered by asking "is e a member of x".
The two questions are equivalent.  This insight comes from your
intuition about the semantics of REV - it just reorders the elements
but doesn't add or delete any.  The second question is simpler since it
doesn't mention REV, so this is a good transformation to make.  And the
theorem that they are equivalent is simpler than the key checkpoint
above because it involves fewer functions and smaller expressions.

You might formalize this insight as

     (equal (member e (rev x))
            (member e x))

But this conjecture is not a theorem, because (member e x) returns the
cdr of x that begins with e, not just a Boolean (t or nil) indicating
whether e is an element of x.  The location of the first e in (rev x)
is generally different than the location in x.  So when we say the two
questions are "equivalent" we don't mean they are equal.  We mean that
they're propositionally equivalent: both nil or both non-nil.  This
sense of equivalence is called "if and only if" and is checked by the
function iff.

So our intuitive insight can be phrased as this theorem:

     (iff (member e (rev x))
          (member e x))

Suggesting that this formulation of the insight is "obvious" begs many
questions.  Mathematically, we could have avoided iff and just written
two implications:

     (and (implies (member e x) (member e (rev x)))
          (implies (member e (rev x)) (member e x))).

or

     (and (implies (member e x) (member e (rev x)))
          (implies (not (member e x))  (not (member e (rev x))))).

Or we could have used iff but "oriented" it the other way:

     (iff (member e x)
          (member e (rev x)))

We choose to write

     (iff (member e (rev x))
          (member e x))

because of our knowledge of how ACL2 turns formulas into rules!

We deal with this at greater length later.  But just to drive the point
home, if we issue the command:

     (defthm member-rev
       (iff (member e (rev x))
            (member e x)))

ACL2 will build in a rule that causes every propositional occurrence of
(MEMBER e (REV x)) to be replaced by (MEMBER e x).  (By "propositional
occurrence" we mean an occurrence in which the value is tested, as by
IF or the propositional connectives.  Remember, one might use member to
determine the location of an element too.)

Note carefully: if you do not tell ACL2 how to make a rule from a
theorem, it makes a rewrite rule.  Rewrite rules always replace
instances of the left-hand side by the corresponding instances of the
right-hand side.  That is, when interpreted as a rewrite rule, (iff
alpha beta) makes ACL2 replace alpha by beta.

Probably the biggest mistake new users make is forgetting that every
theorem they prove creates a very specific rule.  You must remember
that you are programming ACL2 with these rules.  Being careless in your
statement of theorems is tantamount to being careless in your
programming.  What you get is a mess.

Had we proved the same equivalence, but with the iff commuted, we would
be giving ACL2 bad advice.  We would be telling it "replace instances
of (MEMBER e x) by the corresponding instances of (MEMBER e (REV x))"!
If ACL2 had that rule and ever tried to simplify any member expression,
e.g., (MEMBER A B), it would get into an infinite loop, e.g., producing
the following sequence of transformations:

     (MEMBER A B)
     (MEMBER A (REV B))
     (MEMBER A (REV (REV B)))
     ...

until it eventually exhausted some resource.

Recall that we entertained the idea of phrasing our insight about member
and rev with implications rather than iff.  Generally speaking,
implications produce weaker rules - rules that apply less often.  We
discuss that later.

Now suppose we've proved member-rev, oriented so as to rewrite (member
e (rev x)) to (member e x), and built it in as a rewrite rule.  Then
suppose we repeated the attempt to prove our Main Theorem.  This time,
when the prover is processing the hideous Key Checkpoint printed above,
our new lemma, member-rev, will hit it.  It will transform the formula
to:

     (IMPLIES (AND (CONSP X)
                   (MEMBER (+ 3 (* I I)) X)   ; <-- the hyp has simplified
                   (LIST-OF-INTEGERS X)
                   (INTEGERP I)
                   (<= 0 I)
                   (INTEGERP K)
                   (<= 0 K)
                   (< I K)
                   (SQUARES-PLUS-3P K X)
                   (NOT (EQUAL (CAR X) (+ 3 (* I I))))
                   (NOT (MEMBER (+ 3 (* I I)) X)))
              (SQUARES-PLUS-3P K (REV X)))?

and then that will collapse to T, since the IMPLIES has contradictory
hypotheses (note the last hypothesis above).

By proving member-rev we proved the hideous checkpoint.  We never had
to look at the rest of the formula or think about why it is a theorem.
Furthermore, attacking the main theorem again, from scratch, with
member-rev in the database, may eliminate other checkpoints that came
up the last time we tried to prove our main goal.  So we recommend
addressing one checkpoint at a time.

This example illustrates that purely local thinking - looking for
simplifiable combinations of function symbols - can sometimes lead to
proofs and should always be your first reaction to a key checkpoint:
what local fact do you know that would clean up the formula?  Don't
think about deep questions like "why is this true?"  until you can't
see any way to make it simpler.

It is important to train yourself to see combinations of function
symbols and to create strong rules for eliminating them.  We will give
you opportunities to practice this later in the tutorial.

If you have been reading the tutorial introduction to the theorem
prover, use your browser's Back Button now to return to
INTRODUCTION-TO-KEY-CHECKPOINTS.

EQUIVALENT-FORMULAS-DIFFERENT-REWRITE-RULES    logically equivalent formulas can generate radically different rules

Consider the rewrite rules that would be generated from the three
commands below.  In all three cases, the fact being stated relates the
nth element of the reverse of x to the nth element of x.  In fact, the
three formulas are simple rearrangements of each other and are all
equivalent.  The theorem prover treats all three formulas equivalently
when proving them.  But the rules generated from them are very
different.

     (defthm nth-rev-1
       (implies (and (natp n)
                     (< n (len x)))
                (equal (nth n (rev x))
                       (nth (- (len x) (+ 1 n)) x))))

     (defthm nth-rev-2
       (implies (and (natp n)
                     (< n (len x)))
                (equal (nth (- (len x) (+ 1 n)) x)
                       (nth n (rev x)))))

     (defthm nth-rev-3
       (implies (and (natp n)
                     (not (equal (nth n (rev x))
                                 (nth (- (len x) (+ 1 n)) x))))
                (not (< n (len x)))))

Here are the three rewrite rules:

nth-rev-1:
Replace instances of (NTH n (REV x))
by (NTH (- (LEN x) (+ 1 n)) x),
if you can establish that n is a natural number less than the length of
x.

nth-rev-2:
Replace instances of (NTH (- (LEN x) (+ 1 n)) x)
by (NTH n (REV x)),
if you can establish that n is a natural number less than the length of
x.

nth-rev-3:
Replace instances of (< n (LEN x))
by NIL
if you can establish that n is a natural number and that (NTH n (REV
x)) is different from (NTH (- (LEN x) (+ 1 n)) x).

As the driver of ACL2, you have to decide which rule you want when you
give the command to prove it.

If you tell the theorem prover to use both nth-rev-1 and nth-rev-2,
ACL2 will enter an infinite loop when it sees any term matching either
NTH expression.

Most users would choose form nth-rev-1 of the rule.  It eliminates rev
from the problem - at the expense of introducing some arithmetic.  But
arithmetic is so fundamental it is rarely possible to avoid it and it is
likely to be in the problem already since you're indexing into (rev x).
The nth-rev-2 form of the rule is "bad" because it introduces rev into a
problem where it might not have appeared.  The nth-rev-3 version is
"bad" because it makes the theorem prover shift its attention from a
simple arithmetic inequality to a complicated property of nth and rev,
which might not be in the problem.

Use your browser's Back Button now to return to
introduction-to-rewrite-rules-part-1.

EXAMPLE-INDUCTION-SCHEME-BINARY-TREES    induction on binary trees

See LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INDUCTIVE-PROOF for an
explanation of what we mean by the induction suggested by a recursive
function or a term.

Classical Induction on Binary Trees: To prove (p x), for all x, by
classical induction on binary tree structures, prove each of the
following:

     Base Case:
     (implies (atom x) (p x))

     Induction Step:
     (implies (and (not (atom x))
                   (p (car x))
                   (p (cdr x)))
              (p x))

An argument analogous to that given in example-induction-scheme-on-lists
should convince you that (p x) holds for every object.

A function that suggests this induction is:

     (defun flatten (x)
       (if (atom x)
           (list x)
           (app (flatten (car x))
                (flatten (cdr x))))).

EXAMPLE-INDUCTION-SCHEME-DOWN-BY-2    induction downwards 2 steps at a time

See LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INDUCTIVE-PROOF for an
explanation of what we mean by the induction suggested by a recursive
function or a term.

Classical Induction on Natural Numbers Preserving Parity: Here is
another way to decompose natural numbers.  To prove (p n), for all n,
prove each of the following:

     Base Case 1:
     (implies (zp n) (p n))

     Base Case 2:
     (implies (equal n 1) (p n))

     Induction Step:
     (implies (and (not (zp n))
                   (not (equal n 1))
                   (p (- n 2)))
              (p n))

Base Case 1 establishes that p holds for 0 (and all objects other than
positive naturals).

Base Case 2 establishes that p holds for 1.

The Induction Step establishes that if n is a natural number greater
than 1, and if p holds for n-2, then p holds for n.

Note that we have thus proved that (p n) holds, for all n.  For example,
(p -7), (p 'abc), and (p 0) are all established by Base Case 1.  (p 1)
is established by Base Case 2.  (p 2) is established from (p 0) and the
Induction Step.  Think about it!  (p 3) is established form (p 1) and
the Induction Step, etc.

A function that suggests this induction is:

     (defun parity (n)
       (if (zp n)
           'even
           (if (equal n 1)
               'odd
               (parity (- n 2))))).

EXAMPLE-INDUCTION-SCHEME-NAT-RECURSION    induction on natural numbers

See LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INDUCTIVE-PROOF for an
explanation of what we mean by the induction suggested by a recursive
function or a term.

Classical Induction on Natural Numbers: Induction is familiar in the
arithmetic setting.  To prove (p n), for all n, by classical induction
on the construction of the natural numbers, prove each of the following:

     Base Case:
     (implies (zp n) (p n))

     Induction Step:
     (implies (and (not (zp n))
                   (p (- n 1)))
              (p n))

The Base Case establishes that p holds for 0.  In fact, because of the
definition of zp <>, it establishes that (p n) holds when n is 0 and it
holds when n is not a natural number.

The Induction Step establishes that if n is a natural number other than
0, and if p holds for n-1, then p holds for n.  The hypothesis (p (- n
1)) above is called the induction hypothesis.

A function that suggests this induction is

     (defun nat-recursion (n)
       (if (zp n)
           n
           (nat-recursion (- n 1))))

Similarly, the term (fact n) suggests this induction if fact is defined:

      (defun fact (k)
       (if (zp k)
           1
           (* k (fact (- k 1))))).

even though the formal parameter of this definition of fact is k, not n.

EXAMPLE-INDUCTION-SCHEME-ON-LISTS    induction on lists

See LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INDUCTIVE-PROOF for an
explanation of what we mean by the induction suggested by a recursive
function or a term.

Classical Induction on Lists: To prove (p x), for all x, by classical
induction on the linear list structure, prove each of the following:

     Base Case:
     (implies (endp x) (p x))

     Induction Step:
     (implies (and (not (endp x))
                   (p (cdr x)))
              (p x))

An argument analogous to that given for natural numbers,
example-induction-scheme-nat-recursion, establishes (p x) for every x.
For example, (p -7), (p 'abc), and (p nil) are all established by the
Base Case.  (p '(Friday)) follows from (p nil), given the Induction
Step.  That sentence bears thinking about!  Think about it!  Similarly,
(p '(Yellow)) holds for the same reason.  (p '(Thursday Friday))
follows from (p '(Friday)) and the Induction Step, etc.

A function that suggests this induction is

     (defun app (x y)
       (if (endp x)
           y
           (cons (car x)
                 (app (cdr x) y)))).

EXAMPLE-INDUCTION-SCHEME-ON-SEVERAL-VARIABLES    induction on several variables

See LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INDUCTIVE-PROOF for an
explanation of what we mean by the induction suggested by a recursive
function or a term.

Induction on Several Variables  To (p n x) for all n and all x, prove
each of the following:

     Base Case 1:
     (implies (endp x)
              (p n x))

     Base Case 2:
     (implies (and (not (endp x))
                   (zp n))
              (p n x))

     Induction Step:
     (implies (and (not (endp x))
                   (not (zp n))
                   (p (- n 1) (cdr x)))
              (p n x))

A function that suggests this induction is

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

EXAMPLE-INDUCTION-SCHEME-UPWARDS    induction upwards

See LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INDUCTIVE-PROOF for an
explanation of what we mean by the induction suggested by a recursive
function or a term.

Induction Upwards:  To (p i max) for all i and all max, prove each of
the following:

     Base Case:
     (implies (not (and (natp i)
                        (natp max)
                        (< i max)))
              (p i max))

     Induction Step:
     (implies (and  (natp i)
                    (natp max)
                    (< i max)
                    (p (+ i 1) max))
              (p i max))

Note that the induction hypothesis is about an i that is bigger than
the i in in the conclusion.  In induction, as in recursion, the sense of
one thing being "smaller" than another is determined by an arbitrary
measure of all the variables, not the magnitude or extent of some
particular variable.

A function that suggests this induction is shown below.  ACL2 has to be
told the measure, namely the difference between max and i (coerced to a
natural number to insure that the measure is an ordinal).

     (defun count-up (i max)
       (declare (xargs :measure (nfix (- max i))))
       (if (and (natp i)
                (natp max)
                (< i max))
           (cons i (count-up (+ 1 i) max))
           nil)).

EXAMPLE-INDUCTION-SCHEME-WITH-ACCUMULATORS    induction scheme with accumulators

See LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INDUCTIVE-PROOF for an
explanation of what we mean by the induction suggested by a recursive
function or a term.

To prove (p x a) for all x and all a, prove each of the following:

     Base Case:
     (implies (endp x)
              (p x a))

     Induction Step:
     (implies (and (not (endp x))
                   (p (cdr x) (cons (car x) a)))
              (p x a))

Note that in the induction hypothesis we assume p for a smaller x but a
larger a.  In fact, we could include as many induction hypotheses as we
want and use any terms we want in the a position as long as the x
position is occupied by a smaller term.

A function that suggests this particular induction is shown below.

     (defun rev1 (x a)
       (if (endp x)
           a
           (rev1 (cdr x) (cons (car x) a)))).

A function that suggests a similar induction in which three induction
hypotheses are provided, one in which the a position is occupied by
(cons (car x) a), another in which the a position is occupied by some
arbitrary term b, and a third in which the a position is occupied by a,
is suggested by the term (rev1-modified x a b) where

     (defun rev1-modified (x a b)
       (if (endp x)
           (list x a b)
           (list (rev1-modified (cdr x) (cons (car x) a) b)
                 (rev1-modified (cdr x) b b)
                 (rev1-modified (cdr x) a b))))

Remember that the value of this term or function is irrelevant to the
induction suggested.  Because ACL2's definitional principle insists
that all the formal parameters play a role in the computation (at least
syntactically), it is common practice when defining functions for their
induction schemes to return the list of all the formals (to insure all
variables are involved) and to combine recursive calls on a given
branch with list (to avoid introducing additional case analysis as
would happen if and or or or other propositional functions are used).

If you tried to prove (p x a) and suggested the induct hint
(rev1-modified x a (fact k)), as by

     (thm (p x a)
          :hints (("Goal" :induct (rev1-modified x a (fact k)))))

the inductive argument would be:

     Base Case:
     (implies (endp x)
              (p x a))

      Inductive Step:
      (implies (and (not (endp x))
                    (p (cdr x) (cons (car x) a))
                    (p (cdr x) (fact k))
                    (p (cdr x) a))
               (p x a))

EXAMPLE-INDUCTION-SCHEME-WITH-MULTIPLE-INDUCTION-STEPS    induction scheme with more than one induction step

See LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INDUCTIVE-PROOF for an
explanation of what we mean by the induction suggested by a recursive
function or a term.

Several Induction Steps:  To (p x i a) for all x, i, and a, prove each
of the following:

     Base Case 1:
     (implies (zp i)
              (p x i a))

     Induction Step 1:
     (implies (and (not (zp i))
                   (equal (parity i) 'even)
                   (p (* x x)
                      (floor i 2)
                      a))
              (p x i a))

     Induction Step 2:
     (implies (and (not (zp i))
                   (not (equal (parity i) 'even))
                   (p x
                      (- i 1)
                      (* x a)))
              (p x i a))

A function that suggests this induction is the binary exponentiation
function for natural numbers.

     (defun bexpt (x i a)
       (cond ((zp i) a)
             ((equal (parity i) 'even)
              (bexpt (* x x)
                     (floor i 2)
                     a))
             (t (bexpt x
                       (- i 1)
                       (* x a)
                       )))).

In order to admit this function it is necessary to know that (floor i
2) is smaller than i in the case above.  This can be proved if the book
"arithmetic-5/top" has been included from the ACL2 system directory,
i.e.,

     (include-book "arithmetic-5/top" :dir :system)

should be executed before defining bexpt.

EXAMPLE-INDUCTIONS    some examples of induction schemes in ACL2

Here are some pages illustrating various induction schemes suggested by
recursive functions.

Classical Induction on Natural Numbers: see
EXAMPLE-INDUCTION-SCHEME-NAT-RECURSION.

Induction Preserving Even/Odd Parity or
Induction Downwards by 2 or
Induction with Multiple Base Cases: see
EXAMPLE-INDUCTION-SCHEME-DOWN-BY-2 for an induction in which the
induction hypothesis decreases the induction variable by an amount other
than 1.  This illustrates that the induction hypothesis can be about
whatever term or terms are needed to explain how the formula recurs.
The example also illustrates an induction with more than one Base Case.

Classical Induction on Lists: see
EXAMPLE-INDUCTION-SCHEME-ON-LISTS for an induction over linear lists,
in which we inductively assume the conjecture for (cdr x) and prove it
for x.  It doesn't matter whether the list is nil-terminated or not;
the Base Case addresses all the possibilities.

Classical Induction on Binary (Cons) Trees: see
EXAMPLE-INDUCTION-SCHEME-BINARY-TREES for an induction over the
simplest form of binary tree.  Here the Induction Step provides two
hypotheses, one about the left subtree and one about the right subtree.

Induction on Several Variables: see
EXAMPLE-INDUCTION-SCHEME-ON-SEVERAL-VARIABLES for an induction in
which several variables participate in the case analysis and induction
hypotheses.

Induction Upwards: see EXAMPLE-INDUCTION-SCHEME-UPWARDS for an
induction scheme in which the induction hypothesis is about something
"bigger than" the induction conclusion.  This illustrates that the
sense in which the hypothesis is about something "smaller" than the
conclusion is determined by a measure of all the variables, not the
magnitude or extent of some single variable.

Induction with Auxiliary Variables or
Induction with Accumulators: see
EXAMPLE-INDUCTION-SCHEME-WITH-ACCUMULATORS for an induction scheme in
which one variable "gets smaller" but another is completely arbitrary.
Such schemes are common when dealing with tail-recursive functions that
accumulate partial results in auxiliary variables.  This example also
shows how to provide several arbitrary terms in a non-inductive
variable of a scheme.

Induction with Multiple Induction Steps: see
EXAMPLE-INDUCTION-SCHEME-WITH-MULTIPLE-INDUCTION-STEPS for an
induction in which we make different inductive hypotheses depending on
which case we're in.  This example also illustrates the handling of
auxiliary variables or accumulators.

FREQUENTLY-ASKED-QUESTIONS-BY-NEWCOMERS    some questions newcomers frequently ask

This FAQ is for people who've read through all the other sections of the
tutorial introduction to the theorem prover (see
INTRODUCTION-TO-THE-THEOREM-PROVER and all the links from it that are
not marked with the little warning sign ("<>").  Do not expect to
understand our answers if you haven't taken the time to read through
the tutorial.  In the answers below you will see more links into the
hypertext reference manual.  While such links were marked "<>" in the
tutorial, they are not marked that way here.  When you enter the
reference manual be prepared to explore and assemble a mini-course on
the topic of interest, not a quick fix.

Q.  How do I find something in the ACL2 documentation?  A.  Try going
to the Search link on the ACL2 home page.

Q.  How does the theorem prover work?  A.  We really don't think you
need to know much about the inner workings of the prover to become an
effective user.  That doesn't mean the system is self-explanatory!  It
means that stuff you need to learn is not how the theorem prover works
but how to interact with it!  That is what
introduction-to-the-theorem-prover is about.  However, if you want the
most basic overview of the prover, see
ARCHITECTURE-OF-THE-PROVER.

Q. How do I define a new function?  A. See DEFUN.

Q. How do I define a new predicate?  A. See DEFUN.

Q. How do I define a new relation?  A. See DEFUN.

Q. How do I define a function or predicate that takes a varying number
of arguments?  A. You can't.  However, see DEFMACRO to learn
how to define a macro that takes a varying number of arguments and
expands into an arbitrary term that you compute.

Q. How do I define a macro that is sensitive to the state?  A.  You
can't.  However, advanced users should consider make-event.

Q. How do I define mutually recursive functions?  A.  See
MUTUAL-RECURSION.  However, you should realize that when two
functions, say f and g, are mutually recursive, properties of f
generally have to be stated simultaneously with properties of g, since
inductive proofs about one function require inductive hypotheses about
the other.  Furthermore, ACL2 does not know how to do inductions for
mutually recursive functions and must be told.  See
MUTUAL-RECURSION-PROOF-EXAMPLE.

Q. How do I declare the type signature of a function?  A.  You can't.
ACL2 is a syntactically untyped language and all functions are defined
on all objects in the ACL2 universe.  We recommend that the new user
get used to this and only then explore the use of ACL2 to express and
enforce a type regime.  In ACL2, the guard of a function is akin to the
type signature of a function in typed languages.  However, ACL2 guards
may be arbitrary terms, not just type conditions, they only concern the
inputs to the function (not its result), and do not affect the axiom
defining the function - all functions are defined on every combination
of objects.  You may, of course, prove theorems that establish that
every function called in a definition or theorem is supplied with input
satisfying its guards (which necessarily involves describe the outputs
too).  These formulas are called guard conjectures and the process of
proving them is called guard verification.  Since guards are arbitrary
ACL2 formulas, the "type regimes" one tends to enforce in ACL2 can be
much for flexible and expressive than those in most programming
languages.  However, that expressibility also means guard verification
can be challenging (indeed undecidable).  On the other hand, if one
limits oneself to simple type-like guards, lemmas can be proved that
make most guard verification fully automatic and one can configure ACL2
to do guard verification automatically at defun-time.  One may also
delay guard verification until "the right" lemmas have been proved.  By
doing guard verification one can make functions execute faster by
allowing the code to avoid runtime checks.  This is especially valuable
to industrial users who have large models used both in verification and
as simulation engines for designed artifacts.  In addition, guard
verification can give you the assurance that you are using your
functions within their intended domains and hence is a form of
functional specification and verification.  However, all these
advantages aside, it is remarkably easy to drift away from the simplest
type regimes and write a guard that raises deep mathematical problems.
New users should not try to confront these problems until they are
comfortable with the theorem prover and with lemma development.
Therefore, we strongly recommend that you forget about types and guards
and get used to reasoning about total functions.  When you do decide to
learn about them, be prepared for a complex story involving
specification, execution efficiency, and proof management.  See
GUARD.

Q. How do I tell defun what measure to use?  A. See XARGS,
specifically :measure.

Q.  I specified a measure that always returns a natural number but ACL2
is acting like it's not a natural number.  A.  There are two likely
problems.  The most likely one is that your measure isn't really always
a natural!  Suppose the formals of your defun are x and y and your
measure is (m x y).  Suppose the recursive calls of your function are
protected by tests that insure that x and y are naturals.  Then you
might assume x and y are naturals in the measure.  But ACL2 has to
prove (o-p (m x y)), where o-p is the predicate that recognizes
ordinals (and naturals are ordinals).  Note that the theorem doesn't
have any hypotheses!  You might intuitively think that your measure has
to be an ordinal just under the conditions that lead to recursive
calls.  That's not what ACL2 enforces.  It has to be an ordinal,
always.  So you must change your specified measure.  For example,
consider wrapping nfix around it or around its uses of x and y to
coerce those quantities to naturals.  The second most likely
explanation is that your measure returns a natural, always, but ACL2
doesn't know that and it takes induction to prove.  This might happen
if m involves some recursive functions.  In this case, prove (natp (m x
y)) before your defun.  Perhaps you should consider making the natp
lemma a :type-prescription lemma to make ACL2's typing algorithm aware
of it.

Q. How do I tell defun what well-founded relation to use?  A. See
XARGS, specifically :well-founded-relation.

Q. How do I show that a relation is well-founded?  A. Prove a theorem
establishing that there is an order preserving embedding into the
ordinals and store it with :rule-classes :well-founded-relation.

Q.  What is an ordinal?  What does it mean to be well-founded?  A.
Ordinals are an extension of the natural numbers used to insure that a
process can't go on forever.  Like naturals, they can be added,
multiplied, and exponentiated.  There is a sense of one ordinal being
less than another.  Unlike the naturals, each of which is finite, the
ordinals include infinite objects.  Now imagine "standing" on an
ordinal and "stepping" to a smaller one.  Like the naturals, this "walk
down the ordinals" can't go on forever, even if you start on an
infinite ordinal.  That is because the ordinals are well-founded.  See
o-p for more information about ordinals in ACL2 and about
well-foundedness.  See ORDINALS for a deeper discussion and a
discussion of books that can help configure ACL2 to reason about
ordinals.

Q. How can provide hints for the termination proofs in defun?  A. See
XARGS, specifically :hints (for the termination proofs) and
:guard-hints (for the guard verification proofs).

Q. How do I define a constant (something like a global variable)?  A.
See DEFCONST.  But remember that as an applicative programming
language, ACL2 does not have global variables!  You can define a symbol
to have a fixed value and use the symbol sort of like a global variable
in function definitions: you may refer to the value of the symbol in
your functions without passing the variable in as formal parameter.  But
you may not ever change the value of the symbol!

Q. How do I save the value of a top-level computation for future use?
A. See ASSIGN and see @.

Q. How do I introduce new syntactic form or abbreviation?  A. See
DEFMACRO.

Q.  How can create and modify an array?  A.  ACL2 is a functional
language, so it is impossible to destructively modify an existing
object; technically, all "updates" to objects must be implemented by
"copy-on-write" semantics.  That said, ACL2 provides support for
arrays, provided you use them in a restricted way.  They give you
constant-time access and change under the use restrictions.

Q.  How do I read from or write to a file?  How do I do IO?  A.  To
manipulate files, your function must have state as an argument, so you
should read about the restrictions that imposes.  For input/output
facilities, see IO.

Q. How do I define a structure that can be destructively modified?  A.
ACL2 is an applicative programming language.  You can't modify objects
arbitrarily!  You basically have to "copy on write," which means you
construct new objects from old ones, making the changes you want in the
new one.  If the car of some object is 1 at one moment and 2 later,
then the basic logical axiom (car x) = (car x) is violated!  However,
if the only reference to the old object, e.g., x, was to pass it to the
code that copied and "changed" it, then ACL2 can re-use the old object
to produce the new one and the axioms would not object.  Such syntactic
restrictions can make x a modifiable structure but they will impose a
heavy burden on you as a programmer: if pass such an x to a function
and the function modifies it, then you must pass x only to that
function and you must return the modified value and use it henceforth.
Such objects are said to be single threaded.  See DEFSTOBJ.

Q.  How do I write a universal quantifier?  An existential quantifier?
How can I say "for all" or "there exists"?  A  You can't literally
write quantifiers.  But ACL2 has the power of full first order logic
with quantification.  See QUANTIFIERS.

Q.  How do I introduce an undefined or uninterpreted function symbol?
Can I constrain it to have certain properties?  A.  See
ENCAPSULATE.

Q.  How can I hide a lemma?  I want to prove a lemma temporarily to use
in another proof but I don't want the lemma around thereafter.  A.  One
way to get a similar effect is to prove the lemma and then disable it
with an (in-theory (disable ...)) event; see IN-THEORY.
Another way is to put the lemma and the theorem that needs it into an
encapsulate and wrap a local around the lemma.

Q. What is an event?  A. An event is a command that adds information to
the ACL2 database (the "logical world"), like defun or defthm.  See
EVENTS.

Q. How do I say that I do not want a rewrite rule generated from a
theorem?  A. The command

     (defthm name formula
             :rule-classes nil)

will attempt to prove formula and, if successful, give formula the name
name, which you may use in hints as a theorem, but it will build no
rules from the formula.

Q. How do I say that I want a formula to be stored as a rewrite rule?
A. The command

     (defthm name formula)

will attempt to prove formula and, if successful, it will give formula
the name name and generate a rewrite rule from it, with the runic name
(:rewrite name)].  It could happen that formula generates more than one
rewrite rule, e.g., this happens if the conclusion is an AND.  In this
case, each conjunctive branch through the conclusion generates a rule
named (:rewrite name . i), for i=1,2,...  For more details, see
REWRITE.

Q. How do I say that I want a formula to be stored as a rewrite rule
and some other kinds of rules?  A. The command

     (defthm name formula
             :rule-classes (:class1 ... classk))

will attempt to prove formula and, if successful, it will give formula
the name name and generate a rule of each :classi specified.  Each
:classi should either be a keyword, like :REWRITE or :GENERALIZE,
naming a rule class (see RULE-CLASSES), or else should be a
list that starts with a rule class and then lists the relevant
modifiers.  Be sure to include :REWRITE among the rule classes if you
want the formula to generate a rewrite rule.  It doesn't do that
automatically if you explicitly specify :rule-classes!

Q. How do I rearrange the shape of a formula before generating a rule
from it?  A. See RULE-CLASSES and read about the :corollary
modifier.

Q. What is a type-prescription?  A. ACL2 has an algorithm for
determining the type of object returned by a term, where a type is one
of the Common Lisp primitive datatypes such as natural, integer,
Boolean, cons, true-listp, etc.  Rules provided by you can influence
this algorithm.  See TYPE-PRESCRIPTION.

Q. How do rewrite rules work?  A. Re-read the tutorial sections:
introduction-to-rewrite-rules-part-1 and
introduction-to-rewrite-rules-part-2.

Q. How do I see what's in the database?  A. You can't look at the
entire database with user-friendly tools.  You can print the command
that introduced a particular name, print the entire sequence of user
commands, print the commands in the region between two commands, print
all the rewrite rules that apply to a given term or function symbol,
and many other options.  See HISTORY.  If you have loaded a
book from another user, you might wish to read the source file.  For
example, the source file for (include-book "arithmetic-5/top" :dir
:system) is the file named arithmetic-5/top.lisp on the
acl2-sources/books/ directory where ever your ACL2 sources are
installed.  Often, books are well-documented by comments by their
authors.  Some books have Readme or README files on the same directory.

Q. How do I undo a command?  A. See HISTORY, especially see
U ("undo") and see UBT ("undo back through"). Q. What
rewrite rules match a given term?  A. See PL.

Q.  What were those questions to ask when looking at key checkpoints?
A.  See INTRODUCTION-TO-KEY-CHECKPOINTS.

Q. How do I figure out why a rewrite rule won't fire?  A. If you
activate rewrite rule monitoring (see BRR) and then install a
monitor (see MONITOR) on the rule in question, ACL2 will enter
an interactive break whenever the pattern of the rule is matched
against a target in a proof.  So after installing the monitor, re-try
the proof and then interact with the rewriter via break commands (see
BRR-COMMANDS).  Like all trace and break packages, you have to
know what you're doing to use the break rewrite facility, so read the
material in the reference manual.  If no interactive break happens
after you've installed the monitor on your rule and re-tried the proof,
it means no suitable target ever arose.  Don't forget to turn off
monitoring when you're done as it slows down the system.

Q. Why is a proof taking so long?  A. Unexpectedly poor performance on
simple problems is usually a sign of cyclic rewriting or combinatoric
explosion.  See DMR and see ACCUMULATED-PERSISTENCE.

Q. How do I tell ACL2 what induction to do for a particular formula?
A. When issuing the defthm command for the formula, supply an :induct
hint:

     (defthm name
             formula
             :hints (("Goal" :induct (f x1 ... xn))))

where f is a function that recurs the way you want the induction to
unfold and x1 ... xn are the relevant variables in formula.  You
usually have to define f appropriately for each formula that needs an
induct hint, though sometimes you can re-use an earlier f or one of the
functions in the formula itself.  It doesn't matter what value (f x1
... xn) returns.  All that matters is how it recurs.  The termination
analysis for f justifies the induction done.  See HINTS,
especially the section on :induct hints; also see INDUCTION.

Q. ACL2 doesn't know simple arithmetic that can simplify the term (+ 1
-1 x).  A. You should load an arithmetic book whenever you're dealing
with an arithmetic problem.  The simplest arithmetic book is loaded
with the event (include-book "arithmetic/top-with-meta" :dir :system).
If you're using floor and mod or non-linear arithmetic like (* x y) you
should use (include-book "arithmetic-5/top" :dir :system).  See    also
the discussion of arithmetic books under the "Lemma Libraries and
Utilities" link of the ACL2 home page.

Q. ACL2 is not using an arithmetic lemma that I proved.  A. Lemmas
concluding with arithmetic inequalities, like

     (implies (member e x)
              (< (len (delete e x)) (len x)))

are not good rewrite rules because they rarely match targets because of
intervening arithmetic operators.  For example, the above conclusion
doesn't match (< (LEN (DELETE E X)) (+ 1 (LEN X))).  You should store
such lemmas as :linear rules by using the command:

     (defthm len-delete
       (implies (member e x)
                (< (len (delete e x)) (len x)))
       :rule-classes :linear)

See LINEAR.

Q.  What is a linear rule?  A.  See LINEAR.

Q. How do I make ACL2 treat a relation as an equality?  A. We assume
you mean to treat the relation as an equivalence, i.e., replace one
term by another when they are equivalent under your relation.  See
EQUIVALENCE, see CONGRUENCE, and see REFINEMENT.

Q. One of my rewrite rules has a hypothesis that doesn't rewrite to
true.  What do I do?  A. Prove a rewrite rule that establishes that
hypothesis under the relevant assumptions from the context of the
intended target.  Alternatively, undo the rule and restate it with a
force around the problematic hypothesis, making ACL2 assume the
hypothesis when the rule is applied and raising the truth of the
hypothesis as an explicit subgoal of the proof.  See also case-split.
Of course, you should always state the strongest rewrite rules you can
think of, eliminating hypotheses or shifting them to the right-hand
side inside of IFs; see STRONG-REWRITE-RULES.

Q. How do I make ACL2 "guess" the right instantiation of a free
variable?  A. You can provide a :restrict hint that names the
problematic lemma and provides an instantiation of the free variable.
See HINTS, specifically :restrict.  You could alternatively
give a hint that :uses the rule and provides the appropriate
instantiation in full.  See HINTS, specifically :use.  Recall
that ACL2 guesses free variable instantiations by matching the
problematic hypothesis to the assumptions in the context of the target.
If the appropriate assumption is present but ACL2 is finding another
one, try undoing the problematic rule and proving it again, specifying
the :match-free :all modifier of the :rewrite or :linear rule class.
See RULE-CLASSES.  Alternatively, undo and prove the
problematic rule again and use a bind-free form to compute the
appropriate instantiation.

Q. How can I make ACL2 do a case split to prove a certain subgoal?  A.
See HINTS, specifically :cases.

Q. How can I prevent ACL2 from using a rewrite rule?  A.  See
HINTS, specifically :in-theory (disable ...).  If the use of the rule
is problematic in only one subgoal and the lemma is needed in other
subgoals, disable the lemma only in the problematic subgoal by
specifying the subgoal name (e.g., "Subgoal 1/3.2.1") as the goal
specifier in the hint.  If the rule isn't needed anywhere in the proof,
you could use the specifier "Goal".  If you don't think the rule will
ever be needed for a while, you could globally disable it with the
event (in-theory (disable ...))  (see IN-THEORY) executed
before the first problematic proof.  If the rule has never been used or
must always be disabled, undo it and prove it again with :rule-classes
nil.

Q.  How can I prevent ACL2 from running a definition on constants?  I
tried disabling the function but that didn't work.  A.  If you have a
function named f then disabling f will disable the definitional axiom
about f.  But ACL2 has another kind of rule about f, telling it how to
evaluate f.  The rune of this rule is (:executable-counterpart f).  Try
disabling that, as in the :hints ((...  :in-theory (disable
(:executable-counterpart f)) ...c[)).

Q. How can I make ACL2 use a rule in a proof?  A. See HINTS,
specifically :use.

Q.  How can I make ACL2 expand a function call in a proof?  A.  You can
give an :See EXPAND hint.

Q.  ACL2 sometimes aborts the proof attempt before showing me all of the
subgoals.  How can I make it just keep going instead of aborting early?
A. See OTF-FLG, which stands for Onward Thru the Fog FLaG.

Q. How can I compute when I want a rule to fire?  A.  See
SYNTAXP.

Q.  How can I add pragmatic advice to a lemma after it has been proved?
For example, how can add a forced hypothesis, a backchain limit, or a
syntaxp test?  A.  You can't.  You can undo the lemma, restate it
appropriately, and prove it again.  This produces the cleanest database.
Alternatively, you can prove the restated lemma under a new name - a
task that should be easy since the old version is in the database and
will presumably make the proof trivial - and then disable the old name.

Q. How can I stop ACL2 from rewriting a term?  A. If you need rewriting
done but want to prevent some particular terms from being rewritten,
see HINTS, specifically :hands-off.  Alternatively, consider
embedding the problematic term in a hide.  Users sometime develop
special theories (see THEORY) containing just the rules they
want and then use hints to switch to those theories on the appropriate
subgoals.

Q.  Can I compute which subgoals a hint refers to?  A.  Yes, see
COMPUTED-HINTS.  This topic is for advanced users but knowing that it
is possible might come in handy someday.

Q.  I want the rewriter to always use one theory and then switch to
another so that it doesn't use my most complicated before until doing
the simple things.  A.  This is possible but is something for the
advanced user.  It can be done using a form of computed-hints.  See
USING-COMPUTED-HINTS-7.

Q.  Is there a way to attach the same hint to every defthm?  A.  See
DEFAULT-HINTS.

Q.  How can I just tell ACL2 the proof steps?  A.  See VERIFY
and see PROOF-CHECKER.

Q. How can I write my own simplifier?  A.  See META.

Q. How can I add an axiom or just assume some lemma without proof?  A.
This is very dangerous but is a good strategy for exploring whether or
not a certain set of lemmas (and their rules) is sufficient to prove
your goal.  See DEFAXIOM and see SKIP-PROOFS.

Q. How can redefine a user-defined function?  A.  This is tricky.  What
if you've already proved theorems about the old definition and then
wish to change it?  There are several options.  See
LD-REDEFINITION-ACTION (and note specifically the discussion of
updater function for it, set-ld-redefinition-action); also see
REDEF, see REDEF!, see REDEF+,  and see
REDEF-.

Q. How do I change a function from :program mode to :logic mode?  A.
See VERIFY-TERMINATION.

Q. How do I change the guards on a function?  A. You can't.  Undo it
and redefine it.

Q. What is program mode?  A. See PROGRAM.

Q. What does the ACL2 prompt mean?  A.  See
INTRODUCTION-TO-A-FEW-SYSTEM-CONSIDERATIONS or, specifically, see
PROMPT.

Q. What is logic mode?  A. See LOGIC.

Q. How do I get into or out of :program mode?  :Logic mode?  A. See
PROGRAM and see LOGIC.  You can enter these modes
temporarily for a particular defun by using (declare (xargs :mode
:program)) or (declare (xargs :mode :logic)) after the list of formal
parameters to the definition.

Q.  How do I quit from ACL2?  A.  This varies depending on the
interface you're using.  See
INTRODUCTION-TO-A-FEW-SYSTEM-CONSIDERATIONS.

Q. How do I load a file of definitions and theorems created by someone
else?  A. See INCLUDE-BOOK.

Q. How do I create my own book of definitions and theorems?  A. See
BOOKS.

Q. Where are the "distributed books" referenced by :dir :system on my
machine?  A. If your ACL2 is installed on the directory
dir/acl2-sources, then the distributed books are the files under the
directory dir/acl2-sources/books/.

Q. How can I find out what books are available?  A. Go to the ACL2 home
page, http://www.cs.utexas.edu/u/moore/acl2/ and look at the link
labeled "Lemma Libraries and Utilities."

Q. How do I produce my own book?  A. See BOOKS.

Q. What is a decision procedure?  What decision procedures does ACL2
have?  A. A decision procedure is an algorithm that given enough time
and space can determine, for all the formulas in a certain syntactic
class of formulas, whether the formula is a theorem or not.  The most
well-known decision procedure is for propositional calculus: by testing
a formula under all the combinations Boolean assignments to the
variables, one can decide if a propositional formula is a theorem.  The
syntactic class consists of all formulas you can write using just
variables, constants, and compositions of the functions and, or, not,
implies, iff, and if.  There are, of course, an exponential number of
different assignments so the algorithm can be slow.  ACL2 contains a
propositional decision procedure based on symbolic normalization that
can be faster than trying all the combinations of truthvalues - but is
not guaranteed to be faster.  ACL2 also contains an optional bdd
procedure.  ACL2 also contains a decision procedure for rational
arithmetic involving variables, rational constants, addition,
multiplication by rational constants, equality, and the various
versions of arithmetic inequality (<, <=, >=, and >).  It can be
extended with :linear lemmas.  ACL2 is complete for equality over
uninterpreted (e.g., undefined and unconstrained) function symbols
using an algorithm based on transitive closure of equivalence classes
under functional substitutivity.  Finally, you can make ACL2 use other
decision procedures, even ones implemented outside of ACL2; see
CLAUSE-PROCESSOR.

Q. ACL2 has the change of variable trick (destructor elimination) that
it does to get rid of (CAR X) and (CDR X) by replacing x by (CONS A B).
Is there a way to make ACL2 do that for other terms?  A. Yes.  See
ELIM.

Q. How can I prevent destructor elimination?  A. See HINTS,
specifically :do-not '(eliminate-destructors).

Q. How can I prevent cross-fertilization?  A. See HINTS,
specifically :do-not '(fertilize).

Q. How can I prevent generalization?  A. See HINTS,
specifically :do-not '(generalize).

Q. How can I make ACL2 impose a restriction on a new variable
introduced by destructor elimination or generalization?  A.  See
GENERALIZE.

Q. What rule classes are there?  A. See RULE-CLASSES.

Q. What is a theory?  A. See THEORIES.

Q. How are hints inherited by the children of a subgoal?  A. See
HINTS-AND-THE-WATERFALL.

Q.  How do I use ACL2 under Emacs?  A. See EMACS.

Q.  How do I use ACL2 under Eclipse?  A. See ACL2-SEDAN.

Q.  How do I interrupt the prover?  A.  The keyboard sequence for
interrupting a running process depends your operating system, host
Common Lisp, and user interface (e.g., Emacs, Eclipse, etc.).  But
perhaps a few examples will help you discover what you need to know.
If your host Common Lisp is GCL or Allegro and you are typing directly
to the Common Lisp process, then you can interrupt a computation by
typing "ctrl-c" (hold down the Control key and hit the "c" key once).
But other Lisps may require some other control sequence.  If you are
typing to an Emacs process which is running the GCL or Allegro Common
Lisp process in a shell buffer, you should type ctrl-c ctrl-c - that
is, you have to type the previously mentioned sequence twice in
succession.  If you are running the ACL2 Sedan, you can use the
Interrupt Session button on the tool bar.  The environment you enter
when you interrupt depends on various factors and basically you should
endeavor to get back to the top level ACL2 command loop, perhaps by
typing some kind of Lisp depenent "abort" command like A or :q, or
:abort!.  You can usually determine what environment you're in by
paying attention to the prompt.

Q.  What is the ACL2 loop?  A.  That is the name given to the
interactive environment ACL2 provides, a "read-eval-print loop" in which
the user submits successive commands by typing ACL2 expressions and
keyword commands.  See
INTRODUCTION-TO-A-FEW-SYSTEM-CONSIDERATIONS.

Q.  What is raw lisp?  A.  That is our name for the host Common Lisp in
which ACL2 is implemented.  See
INTRODUCTION-TO-A-FEW-SYSTEM-CONSIDERATIONS.  There is an ACL2 mode
named raw mode which is different from "raw lisp."  See
SET-RAW-MODE.

Q.  Can I get a tree-like view of a proof?  A.  See PROOF-TREE
for an Emacs utility that displays proof trees and allows you to
navigate through a proof from the proof tree.  The ACL2 Sedan also
supports proof trees and you should see the ACL2s documention on that
topic.

Q.  I used the earlier Boyer-Moore theorem prover, Nqthm.  How is ACL2
different?  A. See NQTHM-TO-ACL2.

If you are reading this as part of the tutorial introduction to the
theorem prover, use your browser's Back Button now to return to
introduction-to-the-theorem-prover.

FURTHER-INFORMATION-ON-REWRITING    a grab bag of advice and information on rewriting

In the following paragraphs we give some links to advanced topics,
marked with "<>".  If you are reading this topic as part of the
tutorial on the theorem prover, do not follow these links upon your
first reading.  Just take note of the existence of the facilities and
ideas mentioned.

Arithmetic:  If your goal theorem involves even trivial arithmetic,
such as adding or subtracting 1, we recommend that you do

     (include-book "arithmetic/top-with-meta" :dir :system)

which loads into ACL2 all the rules in one of the books distributed with
ACL2.  (Books are certified files of definitions, lemmas, etc., usually
prepared by other ACL2 users and explicitly shared with the community.)
The book "top-with-meta" is the most elementary and most widely used
arithmetic book.  Others that come with the ACL2 distribution include
"arithmetic-5/top" and various hardware and floating-point arithmetic
books.

Rules Concluding with Arithmetic Inequalities:  If you are tempted to
create a rewrite rule with an arithmetic inequality as its conclusion or
left-hand side, think again.  Inequalities such as

     (<= (len (delete e x)) (len x))

make poor left-hand sides for rewrite rules.  For example, the
inequality above does not match the target

     (<= (LEN (DELETE E X)) (+ 1 (LEN X)))

even though it is sufficient to prove the target (given some simple
arithmetic).  We recommend that if you have a theorem that establishes
an arithmetic inequality, you make it a linear rule.  See
LINEAR <>.

Rearranging Formulas Before Making Rules: It is possible to rearrange
the propositional structure of a proved formula before processing it as
a rule.  This allows you to state a theorem one way "for publication"
and rearrange it to be stored as a more effective rule.  See
INTRODUCTION-TO-THE-DATABASE (a tutorial topic you'll come to later)
and its discussion of the concept of corollary.  Also, see the
discussion of corollary in rule-classes <>.

Rewriting with New Equivalence Relations: You may introduce new
equivalence relations, like "set-equal" or "is-a-permutation" and cause
the rewriter to replace equivalents by equivalents in suitable
contexts, where you use congruence rules to inform ACL2 of where these
more relaxed notions of equivalence may be used; see
EQUIVALENCE <> and see CONGRUENCE <>.

Pragmatic Advice to Control Rules:  You may attach various pragmas to a
rule that allow you rather fine heuristic control over whether and how
the rule is applied.  For example, you may mark a hypothesis to be
forced (see FORCE <>) meaning that the rule is to be applied
even if that hypothesis is not relieved - but if the proof is
successful the system will turn its attention to all forced subgoals.
You may similarly mark a hypothesis so as to cause a case split,
allowing the relief of the hypothesis on one branch and spawning
another branch explicitly denying the hypothesis; see
CASE-SPLIT <>.  You may add a bogus hypothesis that looks at the
intended application of the rule and decides whether to apply the rule
or not, performing an arbitrary computation on the syntactic context of
the application; see SYNTAXP <>.  By providing a :match-free
modifier to the :rewrite rule declaration in your rule-classes, you may
tell ACL2 to try all or only the first free variable value it guesses
(see RULE-CLASSES <>).  You may provide a bogus hypothesis that
computes from the syntactic environment the values to guess for the
free variables in a rule; see BIND-FREE <>.  You may mark a
term so that the rewriter does not dive into it; see HIDE <>.

Programming Your Own Rewriter: If you cannot find a way to use rewrite
rules to make the transformations you desire, you might investigate the
use of metafunctions.  A metafunction is just a little theorem prover
of your own design.  It takes as input a list structure representing a
term and returns a list structure representing a term.  If you can
prove that the meaning of the input and output terms are equivalent,
you can extend the ACL2 simplifier to call your metafunction.  See
META <>.

The Order in which Targets are Rewritten: The rewriter sweeps through
terms "inside-out" otherwise known as "left-most innermost first".
Thus, before trying to apply rewrite rules to (f a1 ... an), rules are
applied to the ai.  This has the good effect of normalizing the ai.

This fact might help you understand why sometimes your rules "don't
seem to fire."  For example, suppose you have a rule for rewriting (len
(rev x)) to (len x) and suppose you wish to prove a theorem about (LEN
(REV (CONS A B))).  Suppose rev is defined in terms of append, as shown
in programming-knowledge-taken-for-granted.  Then you might see a
checkpoint in which the (LEN (REV ...)) above has been simplified to
(LEN (APPEND (REV B) (LIST A))) instead of to (LEN (CONS A B)).  Why
wasn't your rule about (len (rev x)) applied?  The reason is that (REV
(CONS A B)) rewrote to (APPEND (REV B) (LIST A)) before rules were
applied to (LEN (REV ...)).  You need a rule about (len (append x y)),
as you will see from the checkpoint.

The Order in which Rules are Tried: The rewriter tries the most
recently proved rules first.  For example, suppose f, g, and h are
functions defined so that the following two theorems are provable and
suppose you executed the following two events in the order shown:

     (defthm rule1 (equal (f (g x)) (h 1 x)))
     (defthm rule2 (equal (f (g x)) (h 2 X)))

Then if rewrite rules are applied to (F (G A)), the result will be (H 2
A), because the latter rule, rule2, is applied first.  It is generally
best not to have conflicting rules or, at least, to understand how such
conflicts are resolved.  The system will warn you when you propose a
rule that conflicts with an existing one.

If you were reading this topic as part of the tutorial introduction to
the theorem prover, use your browser's Back Button now to return to
introduction-to-rewrite-rules-part-2.

GENERALIZING-KEY-CHECKPOINTS    getting rid of unnecessary specificity

Suppose MEMBER determines whether its first argument is a member of its
second, and SUBSETP determines whether every element of its first
argument is a member of its second.  Suppose that you're trying to prove
some Main Theorem and are told the formula below is a key checkpoint.
What should you do?

     Key Checkpoint:
     (IMPLIES (AND (CONSP A)
                   (INTEGERP (CAR A))
                   (MEMBER (CAR A) B)
                   (SUBSETP (CDR A) B)
                   (NOT (SUBSETP (CDR A) (APPEND B C))))
              (MEMBER (CAR A) C))

The key observation is that the third hypothesis implies the negation
of the fourth.  Writing it in the contrapositive:

     (IMPLIES (AND ...
                   (SUBSETP (CDR A) B)
                   ...)
              (SUBSETP (CDR A) (APPEND B C)))

In fact, that is more complicated than it needs to be.  A "correct"
response to the key checkpoint above is to prove

     (defthm subsetp-append
       (implies (subsetp a b)
                (subsetp a (append b c)))).

A still better response is to prove this:

     (defthm subsetp-append-2
       (implies (or (subsetp a b)
                    (subsetp a c))
                (subsetp a (append b c)))).

This version is better because it handles both of the possibilities
regarding whether a is a subset of the arguments of the append.

It would be nice if we could think of a "strong" version, one in which
(SUBSETP a (APPEND b c)) is rewritten to some clearly simpler term, but
nothing comes to mind.

In any case, if you cannot see any obvious simplification of the
individual terms in the Key Checkpoint, you should ask yourself whether
there are connections beween the various propositional parts (as here,
with the third and fourth hypotheses).  It is a good heuristic to look
for relations between parts with the same top-level function symbol (as
here, with SUBSETP).  It is also a good heuristic to throw out parts of
the formula that seem disconnected (as here, with the terms involving
(CAR A)).

This discussion suggests several "modes" of looking at key checkpoints
and the idea of trying the modes in sequence:

(1) look for simplifiable combinations of function symbols within
propositional components,

(2) look for relations between propositional components, and

(3) throw out irrelevant or weakly connected components.

In all cases you are bringing to bear your intuitions about the
semantics of the terms.  That is, you're not just slinging symbols.  You
should be looking out for obvious truths about individual parts of the
checkpoints...  truths that are obvious to you but not to ACL2!

Ultimately the three "modes" are the same and we do not really recommend
adhering to the given sequence.  You're just looking for simpler
theorems that, in combination, imply the checkpoint.  Keeping the
"modes" in mind may help focus your attention so you consider all the
plausible possibilities.  After a little experience you'll find
yourself looking for all these things simultaneously as part "cleaning
up" the checkpoints.

When your main goal theorems are harder than these, your main concern
will be looking at a Key Checkpoint and asking yourself "why is this
true?"  But you don't want to do that until you've cleaned it up
"locally" as much as possible and sometimes - more often than you might
think - local considerations can prove many of your checkpoints.

If you have been working your way through the tutorial introduction to
the theorem prover, use your browser's Back Button now to return to
introduction-to-key-checkpoints.

INTRODUCTION-TO-A-FEW-SYSTEM-CONSIDERATIONS    the mechanics of interaction with the theorem prover

ACL2 is implemented in Common Lisp.  There are many different Common
Lisps and they differ in details relating to interacting with the
system.  We sometimes refer to the host Common Lisp as "raw Lisp."  The
new user is advised not to operate in raw Lisp as it is possible to,
say, redefine ACL2 system faclities like defthm.

Most people use Emacs (see EMACS <>) or the ACL2 Sedan
(Eclipse) interface (see ACL2-SEDAN <>).  They provide
protection against certain common mistakes, e.g., trying to edit a
block of input text after the operating system has buffered it up and
sent it to the Lisp reader which is parsing it as you type.  More on
this below.  In addition, the Sedan provides helpful syntax checking
and a disciplined approach to the stack of lemmas generated by The
Method.  But the variety of interfaces to the variety of Lisps mean
that there is great variation in what one must type to interact with
ACL2.

The best example is perhaps trying to interrupt a running proof.  If
your host Common Lisp is GCL or Allegro and you are typing directly to
the Common Lisp process, then you can interrupt a computation by typing
"ctrl-c" (hold down the Control key and hit the "c" key once).  But
other Lisps may require some other control sequence.  If you are typing
to an Emacs process which is running the GCL or Allegro Common Lisp
process in a shell buffer, you should type ctrl-c ctrl-c.  If you are
running the ACL2 Sedan, you can use the Interrupt Session button on the
tool bar.  The environment you enter when you interrupt depends on
various factors and basically you should endeavor to get back to the
top level ACL2 command loop, perhaps by typing some kind of Lisp
depenent "abort" command like A or :q, or :abort!.  You can usually
determine what environment you're in by paying attention to the prompt,
which we discuss below.

The ACL2 "interactive loop" is called LP (<>) and is generally invoked
automatically from your Common Lisp when you start up the ACL2 process.
LP is just a special case of an ACL2 function called LD <>, which the
user can call from within the ACL2 interactive loop to enter the loop
recursively.  New users don't have to know this except that it helps
explain why some commands have the string "-ld-" in their names!

ACL2 presents itself as a "read-eval-print" loop: you're repeatedly
prompted for some type-in, which is read, evaluated, and may cause some
printing.  The prompt tells you something about ACL2's state.  In the
standard environment, the prompt is

     ACL2 !>

The "ACL2" tells you that the symbols you use in your command are those
defined in the standard ACL2 namespace (or, in the jargon of Lisp, the
"current package," see CURRENT-PACKAGE <>).  You could create a
new namespace (see DEFPKG <>) and set the current package to it
(see IN-PACKAGE <>).  The next part of the prompt above ("!"),
the exclamation mark) tells you that before ACL2 evaluates your type-in
it will check to see whether guards (<>) are respected, i.e., whether
the functions used in your command are being supplied arguments in
their "expected domains."  If evaluation is allowed by the guards, it
proceeds exactly according to the ACL2 axioms; if evaluation is not
allowed, an error is signaled.  ACL2 event commands check their
arguments thoroughly at run-time, regardless of Lisp's notion of
"expected domains."

If the exclamation mark is missing from the prompt,

     ACL2 >

then evaluation occurs strictly according to the ACL2 axioms, without
regard for any declared guards.

You can switch between these two prompts by typing

     ACL2 !>:set-guard-checking nil

to turn guard checking off and

     ACL2 >:set-guard-checking t

to turn it on.  Try typing (car 7) to each prompt.

If there is a "p" in the prompt,

     ACL2 p!>

with or without the exclamation mark:

     ACL2 p>

it means you are in :program (<>) mode rather than :logic (<>) mode.
In :program mode, defun just defines Common Lisp programs that you can
evaluation but it adds no axioms and you cannot use such defined
functions in theorems or invoke defthm.  :Program mode is often used to
prototype a model.

Most commands are just typical parenthesized Lisp expressions, like

     ACL2 !>(defthm rev-rev
              (implies (true-listp x)
                       (equal (rev (rev x)) x)))

but some are typed as keywords followed by a certain number of
arguments.

For example, to undo the last event you may type

     ACL2 !>:u

or to undo back through the introduction of rev you may type

     ACL2 !>:ubt rev

The first is equivalent to evaluating (u) and the second is equivalent
to evaluating (ubt 'rev).  See KEYWORD-COMMANDS <>.  So if you
see a sentence like "to turn on the break rewrite facility, execute
:brr t," we mean type

     ACL2 !>:brr t

or equivalently

     ACL2 !>(brr t)

If you see a prompt that doesn't look like those above you are probably
not typing commands to the standard ACL2 read-eval-print loop!  If
you've somehow called LD recursively, the prompt "gets deeper," e.g.,

     ACL2 !>>

and you can pop out one level with :q <> (for "quit") or pop to the
outermost ACL2 loop with :abort! <>.  If you are in the outermost call
of the ACL2 interactive loop and you type :q, you pop out into raw
lisp.  The prompt there is generally different from the ACL2 prompt but
that is outside our our control and varies from Lisp to Lisp.  We have
arranged for many (but not all) Lisps to use a raw lisp prompt
involving the string "[RAW LISP]".  To get back into the ACL2
interactive loop from raw lisp, evaluate (LP).

If you see a prompt that looks like an ACL2 prompt but has a number in
front of it, e.g.,

     1 ACL2 >

then you're talking to the break rewrite facility (and you are 1 level
deep in the example above).  Presumably at earlier time in this session
you enabled that facility, with :brr t, installed a monitor on some
rule, invoked the prover, entered the break, and forgot.  Everything
you have done (e.g., lemmas you might have proved with defthm) inside
that break will be lost when you exit the break.

Since the break rewrite facility is "ours" we can tell you how to exit
it!  To exit our breaks and return to the top-level ACL2 loop, execute
:abort!.

If you discover you've been working in a brr break, exit, turn off the
break facility wih :brr nil, and redo whatever defuns and defthms you
did while in that break.

Users of the Emacs interface may occasionally type commands directly in
the *shell* buffer running ACL2.  This can be "dangerous" for two
reasons.  One is that if you type an event, like a defun or defthm,
directly to the shell, it will not be recorded in your "script" buffer
and you may forget it in your final script.  The other is that if you
attempt to edit a multi-line command on any but the most recent line,
e.g., to correct the spelling of defthm below after you've typed the
"(implies (true-listp x)" you will confuse the Lisp parser because it
has already read "(defth rev-rev".

     ACL2 !>(defth rev-rev
              (implies (true-listp x)

This usually provokes the raw Lisp to enter a low level error break
from which you must abort, possibly reenter the ACL2 loop, and re-type
the corrected command from scratch.

Another common mistake when using interfaces other than the ACL2 Sedan
is to type an ill-formed ACL2 expression containing dots or commas,
which also often provokes a break into the raw Lisp's error handler.

The fundamental lesson is that you should pay attention to the prompt
and learn what the different prompts mean - or use the ACL2 Sedan.

If you have been working your way through the tutorial introduction to
the theorem prover, use your browser's Back Button now to return to
introduction-to-the-theorem-prover.

INTRODUCTION-TO-HINTS    how to provide hints to the theorem prover

We assume you've read introduction-to-rewrite-rules-part-1,
introduction-to-key-checkpoints, and introduction-to-the-database.

You may give the theorem prover a hint that is specific to a particular
subgoal generated during a proof attempt.  Of course, you learn the
name of the subgoal by inspecting the key checkpoints or other proof
output.  You are not expected to anticipate the need for hints at
specific subgoals; instead, you usually deduce that a hint is required
because the subgoals is not proved but you see that existing rules and
context make it provable.

The most common hint is to enable and/or disable a particular rule on
some particular subgoal.

     (defthm name
             formula
             :hints (("Subgoal *1/3.2''" :in-theory (disable nth-nthcdr))))

The hint above tells the rewriter that just before it begins to work on
Subgoal *1/3.2" it should switch to a local theory in which all of the
rules generated from the event nth-nthcdr are disabled.  That local
theory remains the one in use for all descendent subgoals generated
from the one named, until and unless one of those descendent subgoals
has an :in-theory hint associated with it.  There are many kinds of
hints besides :in-theory and in general, after each subgoal name, you
can give various forms of advice and list various adjustments you wish
to make to the context in which the prover is operating when it begins
addressing the subgoal named.

The top-level goal is always named Goal.  Thus

     (defthm name
             formula
             :hints (("Goal" ...hints1...)
                     ("Subgoal *1/3.2''" ...hints2...)))

has the effect of using hints1 for the top-level goal and all of its
children throughout the entire proof, except for Subgoal *1/3.2" and
its children, where hints2 is used instead.

There are a few hints which "take effect" exactly on the subgoal to
which they are attached and are not inherited by their descendents.

Here is an incomplete list of some of the more common hints; we note the
ones that do not pass on their effects to their descendents.  We
recommend that you not follow the advanced links (marked "<>") below
until you have read the entire tutorial.

See IN-THEORY <>  for how to enable and/or disable rules.  The
new theory is computed by a "theory expression" (see THEORIES
<>) such as (disable nth-nthcdr) and typically makes adjustments such
as additions or deletions to the global current theory.  All the
relevant new theories are computed before the proof begins.  Thus, in

     (defthm name
             formula
             :hints (("Goal" :in-theory (disable rule1))
                     ("Subgoal *1/3.2''" (disable rule2))))

the theory mentioned for Goal is the global current theory minus rule1,
while the theory mentioned for its descendent, Subgoal *1/3.2", is the
global current theory minus rule2.  In particular, if both rule1 and
rule2 are enabled in the global current theory, then rule1 is enabled
during the processing of Subgoal *1/3.2" because it was not removed
explicitly there.

See USE <> for how to force the theorem prover to take note of
particular instances of particular theorems; in particular, the
instances are created and added as hypotheses to the subgoal in
question.  The hint is not inherited by the descendents of the subgoal
(since the formula being proved has been modified by the hint).  If the
rule you are using (with a :use hint) is an enabled rewrite rule, it
might interfere with the added hypothesis - by rewriting itself to T -
and thus often you will both :use ... and :in-theory (disable ...).

See EXPAND <> for how to tell the theorem prover to expand one
or more function calls whenever encountered.

See CASES <> for how to force the theorem prover to do a case
split to prove the subgoal under each of an exhaustive list of cases
given in the hint.  This hint takes action specifically at the named
subgoal and is not passed down to its children.

See INDUCT <> for how to tell the theorem prover to go
immediately into induction for the subgoal in question, and to use the
induction scheme suggested by the hint rather than the one suggested by
the terms in the subgoal itself.  This hint is not inherited by its
descendents.

See HINTS <> for a complete list of all hints, and see
HINTS-AND-THE-WATERFALL <> for a more thorough description of how the
effects of hints at a subgoal are inherited by the descendents.

If you are reading this as part of the tutorial introduction to the
theorem prover, use your browser's Back Button now to return to
introduction-to-the-theorem-prover.

INTRODUCTION-TO-KEY-CHECKPOINTS    What questions to ask at key checkpoints

We assume you've read about rewrite rules; see
INTRODUCTION-TO-REWRITE-RULES-PART-1.

When a proof attempt fails, ACL2 prints some key checkpoints.  These are
formulas that we think you should look at.  There are two kinds
printed: key checkpoints before an induction, and key checkpoints under
a top-level induction.  (Key checkpoints under deeper inductions and
checkpoints that aren't considered "key" may exist in the proof
attempt, but ACL2 doesn't print them at the end of failed proofs
because you shouldn't be distracted by them.)

Below is a list of questions to ask yourself about the key checkpoints.
Initially, we recommend just picking one key checkpoint before an
induction (perhaps the simplest looking one) and asking these questions.
These questions may lead you to look at other key checkpoints.  As you
gain more experience you'll elaborate and generalize this advice.

(1) Do you believe this formula is a theorem?  If you don't think it is,
it's pointless to try to prove it!  You should reconsider your top-level
formula in light of the special case suggested by this key checkpoint.

(2) Can it be simplified?  Is there some combination of function
symbols in it that could be eliminated or simplified by exploiting some
simpler fact?  By a "simpler fact" we mean a theorem about a few of the
symbols in this formula.  For an example of this see
DEALING-WITH-KEY-COMBINATIONS-OF-FUNCTION-SYMBOLS.  Don't think about
the deep question "how can I prove the checkpoint?" until you've got it
into its simplest form.

(3) Is the simpler fact already in the database?  If there is some
simpler fact that would help clean up the checkpoint but you believe the
simpler fact is already in the database, you can use :pl <>, :pc <>,
:pbt <>, and other history commands to inspect the database; (see
HISTORY <>).  But if you find the allegedly relevant simpler fact in
the database, you must ask: why wasn't it used?  There are four
principal reasons:

(3a) it is disabled - so enable it; you'll learn how when you read the
coming sections on introduction-to-the-database and
introduction-to-hints.

(3b) its left-hand side doesn't match the target - so improve the rule
by generalizing its left-hand side or prove a new rule for this
situation; if you decide to remove the old rule from the database, see
undo commands in history <>.

(3c) it is an IFF rule but the target doesn't occur propositionally -
so see if you you can strengthen the rule to an EQUAL rule or weaken the
context of the target by changing the conjecture to use the target
propositionally; if you decide to remove the old rule from the
database, see undo commands in history <>.

(3d) the hypotheses of the rule cannot be relieved for this occurrence
of the target; this can be caused by the rule's hypotheses being too
strong (requiring more than they should), or by the hypotheses of the
current conjecture being too weak (you forgot some key hypothesis), or
by ACL2 not having the rules it needs to prove that the conjecture's
hypotheses really do imply the rule's.  Tools are available (:see
BRR <>) help you figure out why the rule failed, so use them and
improve the rule, or the current conjecture, or the database as
appropriate.

(4) If the simpler fact is not already known, prove it.  This means you
must create a new defthm event with appropriate rule-classes to store
your new theorem so that it will be used.  See
DEALING-WITH-KEY-COMBINATIONS-OF-FUNCTION-SYMBOLS.  Then you must
start using The Method recursively to prove your new lemma.

(5) Otherwise, is this formula something you'd prove by induction?  If
you can't simplify it, it may be because you "need this fact to prove
this fact," in which case, induction is the right thing to do.  But
first, remember that in order for a formulas to be provable by
induction, it must be very general.  Why must it be general?  Because
in an inductive proof, the main thing you have to work with is the
induction hypothesis, which is an instance of the theorem you're
proving.  If the theorem is not general enough, you won't be able to
assume an instance that will help you.  ACL2 may try induction even on
formulas that are not general enough.  Don't assume that the formula is
ripe for induction just because ACL2 found an induction to do!  Before
you "approve" a formula for induction, ask whether it is perhaps a
special case of some more general theorem.  See
GENERALIZING-KEY-CHECKPOINTS now and then come back here.  If you
found a generalization, you should probably be proving that formula
instead of this one.  So formulate the appropriate defthm and use The
Method recursively to prove it.

(6) If the formula is right for induction, did ACL2 do an induction for
it?  You can answer that without looking at the proof.  Just see if
there are any key checkpoints after induction.  If not, why didn't ACL2
induct?  Perhaps you told ACL2 not to induct!  Perhaps no term in the
conjecture suggests an appropriate induction?  You could remedy this by
extending ACL2's induction analysis by adding to the database.  Or you
could just tell ACL2 what induction to do for this formula.  You'll
learn about both later (when you read coming sections of the tutorial).

(7) If ACL2 did do an induction, was it the right one?  You can find
the induction scheme used by reading the first induction message in the
output log after you submitted the conjecture to ACL2.  But most often
you will realize the "wrong" induction was done just by looking at the
post-induction key checkpoints, keeping in mind that each is supposed
to be a natural special case of the theorem you're proving.  Is the
case analysis inappropriate?  Are induction hypotheses missing?  If so,
you should look at the induction scheme.  If you determine the wrong
induction was done, extend ACL2's induction analysis or tell it which
induction to do, which you'll learn about in the coming sections of the
tutorial.  For more advice about looking at post-induction key
checkpoints, see POST-INDUCTION-KEY-CHECKPOINTS now and then
come back here.

(8) If the post-induction key checkpoints seems plausible, then repeat
the questions above for each one of them, perhaps starting with the
simplest.

In any case, after successfully taking whatever action you've decided
on, e.g., proving some new lemma and adding it as a rule:

Start over trying to prove your main conjecture.  This is important!
Do not just scroll back to the key checkpoints generated the last time
you tried to prove it.  Instead, re-generate them in the context of
your new, improved database and hints.

You will be following this general outline almost all of the time that
you're interacting with ACL2.  You will not often be asking "Why is
ACL2 making me think about this subgoal?  What did ACL2 do to get here?
How does ACL2 work?"

Two other ideas are helpful to keep in mind.

Is a key checkpoint unexpectedly complicated?  Pay special attention to
the case where the complication seems to be the introduction of
low-level details you thought you'd dealt with or by the introduction
of symbols you didn't expect to see in this proof.  These can be signs
that you ought to disable some rules in the database (e.g., a
definition of a complicated function about which you've proved all the
necessary lemmas or some lemma that transforms the problem as was
appropriate for some other proof).

Does the theorem prover just hang up, printing nothing?  If this
happens, you must interrupt it.  How you interrupt the prover is
dependent on which Common Lisp and which interface you're using.  But
most Common Lisps treat control-c as a console interrupt.  If you're in
Emacs running ACL2 as a shell process, you must type control-c
control-c.  If you're in ACL2s, hit the Interrupt Session button.
Interrupting ACL2 can leave you in an interactive loop similar in
appearance but different from ACL2's top-level!  So pay careful
attention to the prompt and see BREAKS <>.

Once you've regained control from the "runaway" theorem prover, there
are several tools you can use to find out what it is doing in real-time.
Generally speaking, when the theorem prover goes silent for a very long
time it is either in some kind of rewrite loop caused by rules that
cause it to flip back and forth between various supposedly normal
forms, or else it has split the problem into a huge number of cases and
suffering a combinatoric explosion.  See DMR <> and, perhaps,
see ACCUMULATED-PERSISTENCE <>.

If you are reading this as part of the tutorial introduction to the
theorem prover, use your browser's Back Button now to return to
introduction-to-the-theorem-prover.

INTRODUCTION-TO-REWRITE-RULES-PART-1    introduction to ACL2's notion of rewrite rules

Rewrite rules make ACL2 replace one term by another.  This is done by
the rewriter, which is part of ACL2's simplifier.  The rewriter sweeps
through the goal formula trying all the rewrite rules it knows.  Here's
an example.  Just pretend that you have made a rewrite rule from the
formula below.

     (implies (and (natp i)
                   (< i (len a)))
              (equal (put i v (append a b))
                     (append (put i v a) b)))

Then every time the rewriter sees a target term that matches

     (put i v (append a b))

it considers the rule, with the variables i, v, a, and b of the rule
bound to whatever terms matched them in the target, say the terms i, v,
a, and b.  To consider the rule, the rewriter first tries to establish
("relieve") the hypotheses.  In particular, it rewrites:

     (natp i)           ; hyp 1

and

     (< i (len a)). ; hyp 2

If both hyptheses rewrite to true, then the rule fires and replaces the
target by:

     (append (put i v a) b).

In short, rewrite rules direct ACL2 to rearrange the terms in the goal
formulas.

We are more precise later, but for now we turn to the question of how
do you make a rewrite rule from a formula?  The answer is, you prove
the formula with the defthm command.  Recall that

     (defthm name
             formula
             ...)

commands ACL2 to try to prove formula and, if successful, build it into
the database as a rule according to your specification in the
rule-classes argument of the ... part of the command.

To make it easy for you to generate rewrite rules, defthm has a simple
heuristic: if you don't tell it what kind of rule to generate from
formula, it generates a rewrite rule!  Thus, if this command

     (defthm name
             formula)

is successful, ACL2 will have a new rewrite rule in the database, even
though you did not explicitly tell it to add a rule.

A common mistake for the new users is to forget that the above command
adds a rewrite rule.  This often results in a tangle of rules that lead
nowhere or to infinite rewriting that you will have to interrupt.  It
is also good to remember that the command only adds a rule.  It does
not magically make ACL2 aware of all the mathematical consequences of
the formula: it just makes a rewrite rule.

When you prove a theorem with defthm you are programming ACL2.  Being
careless in your statement of lemmas is tantamount to being careless in
your programming.

ACL2 can generate rewrite rules from formulas that look like this:

     (IMPLIES (AND hyp1 ... hypk)
              (eqv lhs rhs))

where eqv is either EQUAL or IFF, and lhs is not a variable symbol, not
a constant, and not a call of the function IF, and not a call of an
abbreviation ("macro") that expands to any of these.  So illegal lhs
include X, 0, (IF X Y Y), and (OR p q).  The last is illegal because OR
is just an abbreviation for a certain IF-expression.

Technical Note: This tutorial introduction to the theorem prover takes
liberties with the truth!  We are trying to give you a useful predictive
model of the system without burdening you with all the details, which
are discussed in the reference manual.  For example, using directives
in the rule-classes you can rearrange the proved formula into the form
you want your rule to take, and you can make ACL2 take advantage of
equivalence relations eqv other than just EQUAL and IFF.  But we'll
ignore these fine points for now.

We call the hyp terms the hypotheses of the rule.  We call lhs the
left-hand side of the rule, and we call rhs the right-hand side of the
rule.  If the conclusion of the rule is an EQUAL term we call it an
equality rule.  Otherwise, it is a propositional equivalence rule.  If
there are no hypotheses, k=0, we say the rule is an unconditional
rewrite rule; otherwise it is conditional.

ACL2 allows several special cases of the shapes above.  See
SPECIAL-CASES-FOR-REWRITE-RULES, but come back here and continue.

A rewrite rule makes ACL2 seek out occurrences of terms that match the
left-hand side of the rule and replace those occurrences using the
right-hand side, provided all the hypotheses rewrite to true in the
context of the application of the rule.

That is, the left-hand side is treated as a pattern that triggers the
rule.  The hypotheses are conditions that have to be proved in order for
the rule to fire.  The right-hand side is the replacement and is put
into the formula where the pattern occurred.

Now for some clarifications. ACL2 only considers enabled rules.  And
ACL2 will use a propositional rule to replace a target only if the
target occurs in a propositional place in the formula.  Generally that
means it occurs in the argument of a propositional connective, like
AND, OR, NOT, IMPLIES, and IFF, or in the test of an IF.  When we say
that the left-hand side of the rule must match the target we mean that
we can instantiate the variables in the rule to make the left-hand side
identical to the target.  To relieve or establish the hypotheses of the
rule, ACL2 just applies other rewrite rules to try to prove the
instantiated hypotheses from the assumptions governing the occurrence
of the target.  When ACL2 replaces the target, it replaces it with the
instantiated right-hand side of the rule and then applies rewrite rules
to that.

If a hypothesis has variables that do not occur in the left-hand side
of the rule, then the pattern matching process won't find values for
those variables.  We call those free variables.  They must be
instantiated before ACL2 can relieve that hypothesis.  To instantiate
them, ACL2 has to guess values that would make the hypothesis true in
this context, i.e., true given the assumptions of the goal theorem.  So
if you're trying to prove

     (IMPLIES (AND (TRUE-LISTP A)
                   (MEMBER (CAR P) A)
                   (MEMBER (CDR P) A))
              ...)

and the target you're rewriting is in the "..." part of the formula,
the rewriter knows that (TRUE-LISTP A) (MEMBER (CAR P) A) and (MEMBER
(CDR P) A) are true.  So if a rewrite rule is considered and the rule
has (member e x) as a hypothesis, where e is a free variable but x was
bound to A in the pattern matching, then it will guess that e must be
(CAR P) or (CDR P), even though there are many other possibilities that
would make (MEMBER e A) true.  Of course, whatever guess it makes must
also satisfy all the other hypotheses that mention e in the rule.  It
simply isn't very imaginative at guessing!

The most predictable rewrite rules have no free variables.  You can add
pragmatic advice to help ACL2 with free variables, telling it to try all
the possibilities it finds, to try just the first, or even to compute a
"creative" guess.

It is possible to make the rewriting process loop forever, e.g., by
rewriting alpha to beta with one set of rules and rewriting beta to
alpha with another.  Even a single rule can make the process loop;
we'll show you an example of that later in the tutorial.  ACL2 can
handle commutativity rules without looping.  It uses (equal (+ x y) (+
y x)) to replace (+ B A) by (+ A B), but not vice versa.  (It is
sensitive to alphabetic ordering when dealing with permutative rules.)

Logically equivalent formulas can generate radically different rewrite
rules!  Rearranging the propositional structure of the formula or
swapping the left and right sides of an equality - while having no
effect on the mathematical meaning of a formula - can have a drastic
impact on the pragmatic meaning as a rule.  To see an illustration of
this, see EQUIVALENT-FORMULAS-DIFFERENT-REWRITE-RULES.

Developing an effective set of rewrite rules is key to success at using
ACL2.  We'll look more at this later in the tutorial.

If you are working your way through the tutorial for the theorem
prover, use your browser's Back Button now to return to
introduction-to-the-theorem-prover.  If you are reading just about how
to make effective rewrite rules, go on to
introduction-to-rewrite-rules-part-2.

INTRODUCTION-TO-REWRITE-RULES-PART-2    how to arrange rewrite rules

You should design your rewrite rules to canonicalize the terms in your
problem, that is, your rules should drive terms into some normal form so
that different but equivalent terms are rewritten into the preferred
shape, making equivalent terms identical.  You are very familiar with
this idea from algebra, where you learned to normalize polynomials.
Thus, when you see (2x + 6)(3x - 9) you automaticaly normalize it, by
"multiplying out and collecting like terms," to get (6x^2 - 54).  This
normalization strategy allows you to recognize equivalent terms
presented differently, such as 6(x^2 - 9).

The ACL2 user is responsible for making up the rules.  (Standard "books"
- files of ACL2 definitions and theorems - can often provide rules for
some sets of functions, e.g., arithmetic.)  This is a heavy burden on
you but it means you are in charge of your own normal forms.  For
example, if you use the function nthcdr, which returns the nth cdr of a
list, you might see both (cdr (nthcdr i x)) and (nthcdr i (cdr x)).
These two expressions are equivalent but not identical.  You will want
to decide which you want to see and prove the rewrite rule that
converts the other to that preferred form.

Most good users develop an implicit ordering on terms and rewrite
"heavy" terms to "lighter" ones.  This insures that there are no loops
in their rewrite rules.  But this ordering changes according to the
user and the problem.

Generally, the lightest terms are primitives such as IF, EQUAL,
arithmetic, etc.  Functions defined without explicit recursion tend to
be ignored because they are just expanded away (but see below).
Recursively defined functions tend to be heavier than any other
recursive function used in their definitions, so, for example, if rev
is defined in terms of append, rev is heavier than append.  But the
size and subtlety of recursively defined functions also affects their
place in the ordering.

But rewrite rules are surprisingly subtle.  Recall that a rewrite rule
can be made from a formula of this form:

     (IMPLIES (AND hyp1 ... hypk)
              (eqv lhs rhs))

where eqv is either EQUAL or IFF, and lhs is a call of a function other
than IF.  In such a rule, lhs is the pattern responsible for triggering
the rule, the hypi are conditions which must be satisfied by the
context of the target being rewritten, and rhs is the replacement.  The
replacement only happens if the rule is enabled, the pattern matches,
the conditions are satisfied, and (in the case of an IFF rule) the
target occurs propositionally.  There are other heuristic restrictions
that we won't discuss here.

So how should you phrase a theorem in order to make it an effective
rule?

General Principles:

* Strengthen the Formula: The fewer hypotheses a formula has the better
the rewrite rule formed from it.  The more general the left-hand side
the better the rule.  The fewer free variables in the hypothesis, the
better.  The idea is to form a rule that fires predictably.  Later in
this tutorial you'll get some practice formulating strong rules.

* Choosing the Conclusion: If a lemma is an implication, you have to
choose what the conclusion will be. (You'll also have to "orient" that
conclusion by choosing a left-hand side and a right-hand side, but we
discuss that below).  You can swap the conclusion and any hypothesis by
negating both, producing a different conclusion.  There are generally
two (possibly conflicting) heuristics for deciding which part of the
formula should be the conclusion:

Choosing the Conclusion Heuristic 1: Can you make the conclusion be an
EQUAL or IFF expression that has a "heavy term" on one side?  That will
make a rule that replaces the heavy term with a lighter one.  We
discuss this situation more below.

Choosing the Conclusion Heuristic 2: Can you make the conclusion be a
non-propositional term that contains all the variables mentioned in the
hypotheses?  By "non-propositional" we mean a term that is not just the
propositional combination (e.g., with AND or OR) of other terms but
instead some call of some "heavy" function?  If your conclusion contains
all the variables mentioned in the hypotheses, matching it will
instantiate all the variables in the hypotheses.  That way ACL2 will
not have to guess instantiations of unbound variables when it tries to
relieve the hypotheses.  It is not very good at guessing.

* Orienting the Conclusion: If the conclusion is an EQUAL or an IFF,
you have to decide which is the left-hand side and which is the right.
If the conclusion is (NOT lhs), then the left-hand side is lhs and the
right-hand side is NIL.  If the conclusion is not an EQUAL, an IFF, or
a NOT then the conclusion itself will be the left-hand side and the
right-hand side will be T.  If your lemma was created by looking a Key
Checkpoints while using The Method, the left-hand side should match
some term in that checkpoint.

Remember, the left-hand side is the "trigger" that will make the rule
fire.  It is the pattern that ACL2 will be looking for.

* Pay attention to the free variables: Look at the variables that occur
in the pattern (the left-hand side) and compare them to the variables
that occur in the hypotheses.  Does some hypothesis contain a variable,
say v, that is not in the pattern?  We call v a free variable because
it will not be assigned a value ("bound") by the process of pattern
matching.  ACL2 will have to guess a value for v.  If some hypothesis
contains v as a free variable, ask whether more than one hypothesis
contains v?  ACL2 uses the first hypothesis containing a free v to
guide its guess for v.  To "guess" a value for v, ACL2 uses that
hypothesis as a pattern and tries to match it against the assumptions
in the checkpoint formula being proved.  This means that key hypothesis
must be in normal form, to match the rewritten assumptions of the goal.
It also means that you should reorder the hypotheses to put the most
unusual hypothesis containing a free v first in the list of conjuncts.
For example, if v is free in two hypotheses, (natp v) and (member
(nthcdr v a) b), then we recommend putting the member term first.
There are likely to be many terms in the goal satisfying the natp
hypothesis - or none if natp has expanded to an integer inequality -
while there are likely to be few terms satisfying the member
hypothesis, especially if a and b are bound by the left-hand side of
the rule.

Here are some (possibly conflicting) heuristics for choosing the
left-hand side:

Choose a Left-Hand Side that Occurs in a Key Checkpoint: If you use the
Method you will tend to do this anyway, because you'll see terms in the
Key Checkpoints that you want to get rid of.  But many moderately
experienced users "look ahead" to how the proof will go and formulate a
few anticipatory rules with the idea of guiding ACL2 down the preferred
path to the proof.  When you do that, you risk choosing left-hand sides
that won't actually arise in the problem.  So when you formulate
anticipatory rules, pay special attention to the functions and terms
you put in the left-hand sides.  The next few paragraphs deal with
specific cases.

Avoid Non-Recursive Functions in the Left-Hand Side: If the left-hand
side contains a call of a defined function whose definition is not
recursive, then it will almost never match any target in the formula
being rewritten unless the function is disabled.  Suppose for example
you have defined SQ so that (SQ x) is (* x x).  Suppose you considered
choosing a left-hand side like (+ (SQ x) (SQ y)).  Suppose you hoped it
would hit the target (+ (SQ A) (SQ B)) in some formula.  But when ACL2
simplifies the formula, it will first rewrite that target to
     (+ (* A A) (* B B))

by expanding the definition of SQ, since it could do so without
introducing any recursive calls.  But now the target won't match your
rule.  By choosing a left-hand side that occurs in a Key Checkpoint
(and is not one of a handful of abbreviations ACL2 uses in its output
like AND, NOT), you'll avoid this problem since SQ will have already
been expanded before the Key Checkpoint is printed.

Disable Non-Recursive Functions: If you insist on a left-hand side that
contains calls of non-recursive functions, remember to disable those
non-recursive functions after you've proved all the rules you want
about them.  By disabling SQ you can prevent ACL2 from expanding the
definition as it did above.  Sometimes you will define a function
non-recursively to formalize some concept that is common in your
application and you will want to create a sort of algebra of rules
about the function.  By all means do so, so you can conduct your formal
reasoning in terms of the concepts you're informally manipulating.  But
after proving the required laws, disable the non-recursive concept so
that ACL2 just uses your laws and not the messy definition.

Choose a Left-Hand Side Already in Simplest Form: This is a
generalization of the advice above.  If any rule will rewrite your
left-hand side, it will prevent your rule from matching any target.
For example, if you write a left-hand side like (foo (car (cons x y)))
then it would never match any target!  The reason is that even if (FOO
(CAR (CONS A B))) did occur in some goal formula, before ACL2 would try
your rule about foo it will use the obvious rule about CAR and CONS to
transform your imagined target to (FOO A).  Thus, your rule would not
match.  So you have to keep in mind all your other rules when you choose
a left-hand side (and when you choose the hypotheses to guide free
variable selection).  If you always choose a pattern that matches a
term in a Key Checkpoint, you avoid this problem.

Make Sure the Left-Hand Side is "Heavier" than the Right: Sometimes
this is obvious, as when you choose (REV (REV x)) for the left-hand side
and x for the right.  But what do you about (REV (APPEND x y)) versus
(APPEND (REV y) (REV x))?  Most of the time we choose to drive the
heaviest function (in this case REV) down toward the variables, lifting
the lighter function (APPEND) up so that we can reason about the
lighter function's interaction with the surrounding "matrix" of the
formula.  So we'd rewrite (REV (APPEND x y)) to (APPEND (REV y) (REV
x)), not vice versa.

Alternative Ways to Talk About the Same Thing: If your problem and
specification use two different ways to talk about the same thing,
choose one form and rewrite the other into that form.  For example, the
ACL2 built-in nth returns the nth element of a list, and the built-in
function nthcdr returns the nth cdr of a list.  They are defined
independently.  But (nth n x) is the same thing as (car (nthcdr n x)).
Since nth can be expressed in terms of nthcdr but not vice versa, it is
clear we should prove (equal (nth n x) (car (nthcdr n x))) as a rewrite
rule if both nth and nthcdr are involved in the problem.

Don't Let Computational Efficiency Dictate the Terms: If you have two
functions that are equivalent (perhaps one was defined to be
computationally more efficient), prove their equivalence as a rewrite
rule that eliminates the more complicated function.  An extreme example
would be a model that uses a sophisticated data structure (like a
balanced binary tree, red-black tree, ordered array, or hash table) to
implement something simple like an association of keys to values.  By
proving the equivalence as stated you can eliminate the messy function
early and do the bulk of your reasoning in terms of its simple
specification.

The best ACL2 users become very good at keeping all these things in mind
when designing their rewrite rules.  Practice makes perfect.  Don't be
afraid during your learning of ACL2 to undo the rules you first
invented and try to make better ones.

Finally, be patient!  There will be times when you think to yourself
"Why should I spend my time thinking of rules that guide ACL2?  I know
the proof!"  There are two reasons.  First, you may "know" the proof
but you may well be wrong and part-way through this whole exercise you
may realize that you're missing a major hypothesis or special case that
breaks your whole conception of the problem.  The proof is in the
details.  Second, most of the time the library of rules you develop in
this process will be used over and over again on variants of the main
problem in the months and years ahead.  This is sometimes called the
proof maintenance problem.  Theorems don't suffer bit rot!  But the
artifacts you're modeling change and you will need to prove new
versions of old theorems.  A good general purpose library makes this
much easier.

We now recommend that you practice inventing strong rules; see
STRONG-REWRITE-RULES.

For advice on handling specific kinds of formulas and definitions, see
SPECIFIC-KINDS-OF-FORMULAS-AS-REWRITE-RULES.

For more information about the rewriter works and how rules are
created, see FURTHER-INFORMATION-ON-REWRITING.

If you are working your way through the tutorial introduction to the
theorem prover, use your browser's Back Button to return to
introduction-to-the-theorem-prover.

INTRODUCTION-TO-THE-DATABASE    how to update the database

We assume you've read introduction-to-rewrite-rules-part-1 and
introduction-to-key-checkpoints.

The theorem prover's heuristics are influenced by the database of rules
and the enabled/disabled status of the rules.  You can think of the
database as a global hint, potentially affecting all parts of a proof
attempt.

However, in addition to the "global hint," it is possible to give local
hints that affect the theorem prover's behavior on specific subgoals.
We discuss the database here and discuss local hints later in the
tutorial.

The theorem prover's "database" is called the ACL2 world.  You change
the world by issuing commands called events.  The most common events are
defun for defining new functions (and predicates) and defthm for
proving new theorems.  Both add rules to the database.  Here are some
commonly used events.

We recommend that upon the first reading of this tutorial you do not
follow the links shown below!  The links take you into the hypertext
reference manual, where it is easy to get lost unless you're looking
for detail about one specific feature.

See DEFUN <> to define a new function or predicate symbol.
Definitional axioms are just a kind of rewrite rule, but defun may also
add rules affecting the determination of the type of a term and rules
affecting the induction analysis.  When you issue a defun command you
will always supply the name of the function or predicate, the list of
formal parameters, v1,...vn, and the body:

     (defun name (v1 ... vn)
        body)

If the event is accepted, a definitional axiom is added to the world,
(name v1...vn)=body, stored as a special kind of unconditional rewrite
rule.  However, the defun event may require theorems to be proved.
Specifically, measure theorems must be proved to establish that
recursively defined functions always terminate, by proving that an
ordinal measure of the formal parameters decreases in a well-founded
way in every recursive call.  In addition, if guards are being used to
declare the expected domain of the newly defined function, guard
theorems might be proved to establish that all functions stay within
their expected domains.  In any case, you may provide additional
information to the defun event, coded as part of the declaration that
Common Lisp allows:

     (defun name (v1 ... vn)
        (declare (xargs ...))
        body)

The xargs ("extra arguments to defun") entry may specify, among other
things, the measure to use in the termination proof, hints for use by
the prover during the termination proof, the guard of the new function,
and hints for use by the prover during the guard verification step.

See DEFTHM <> to prove a theorem and to add it as a rule of one
or more specified rule-classes.  When you issue a defthm command you
always specify a name for the theorem you're trying to prove and a
formula stating the theorem.  You may optionally supply some local
hints as we describe later in the tutorial.  You may also optionally
supply some rule classes indicating how you want your formula stored as
a rule, after it is proved.  We discuss the defthm rule classes below.

See IN-THEORY <> to enable or disable rules.  Rules have names
derived from the names you give to functions and theorems, e.g.,
(:REWRITE LEFT-IDENTITY-OF-FOO . 2) for the second rewrite rule you
created from the theorem named LEFT-IDENTITY-OF-FOO.  Rule names are
called runes.  A theory is just a set (list) of runes.  The current
theory is the list of enabled runes and the in-theory event can add
runes to or delete runes from the current theory.

See INCLUDE-BOOK <> to change the world by loading a certified
file of other events.  The most common use of include-book is to load
"system" books - books written by other ACL2 users who have released
them for distribution to the community.  The most common books loaded
are probably the arithmetic books:

     ; * for the most elementary arithmetic, needed for any problem
     ;   that involves even simple addition and multiplication like
     ;   (+ x (* 2 y) -3):

         (include-book "arithmetic/top-with-meta" :dir :system)

     ; * for more complicated arithmetic involving non-linear terms like
     ;   (* x y), (expt x (+ i j)), and floor and mod

         (include-book "arithmetic-5/top" :dir :system)

But for a complete list of system books, see BOOKS <>.

See CERTIFY-BOOK <> to certify a file of events for reuse later.

See DEFCONST <> to define a new constant, allowing you to write
a symbol, e.g., *weekdays* in place of some object, e.g., '(MON TUE WED
THU FRI) in formulas.

See DEFMACRO <> to define a new syntactic abbreviation.  The
macro facility in Lisp is quite powerful, allowing you to compute the
form to which some type-in expands.  For example, the primitive macro
COND is defined so that (COND ((P X) 1)((Q X) 2)(T 3)) expands to (IF
(P X) 1 (IF (Q X) 2 3)).

See DEFSTOBJ <> to introduce a single-threaded object that your
functions may modify "destructively" provided they follow strict
syntactic rules.

See EVENTS <> for a complete list of the ACL2 events.  There
are events to allow mutually recursive definitions, to introduce some
new function symbols constrained to satisfy given axioms, to allow the
temporary introduction of a "local" event to help prove some goal
theorem and then disappear, to provide the power of first-order
quantification and a choice operator, and many other features.

There are also commands that allow you to inspect the world, e.g., to
print the command that introduced a given name, to show all the
commands back to a certain one, undo the last command or more generally
roll-back to an earlier command.  See HISTORY <>.

The Defthm Rule-Classes

We've already discussed the key role that rules play in controlling the
behavior of the system.  New rules are introduced primiarily with the
defthm event, though defun and other events may introduce rules.

To prove formula and generate, say a :rewrite rule and a :generalize
rule from it, you would write

     (defthm name
             formula
             :rule-classes (:rewrite :generalize))

If you wanted to rearrange the shape of the formula before generating
the :rewrite rule you could provide a :corollary modifier to the
:rewrite rule class:

     (defthm name
             formula
             :rule-classes ((:rewrite :corollary ...)
                            :generalize)).

There are many classes of rules, affecting different parts of the
system.  Each class is denoted by a keyword, e.g., :REWRITE, :LINEAR,
etc.  You are responsible for specifying the class(es) of rules to be
generated from a given formula and several different rules (possibly of
different classes) may be derived from a single formula.  Each class
admits optional modifiers that allow you finer control over each rule.
Each class admits the :corollary modifier with which you can rearrange
the formula before a rule of that class is generated.  This allows you
to state a theorem in its most elegant form for publication purposes
but store it as a rule with the most appropriate hypotheses and
conclusion.  Other modifiers tend to be specific to certain rule
classes, but for example, :rewrite rule modifiers include an optional
limit on the depth of backchaining and options for handling free
variables.

We give some links below to other classes of rules.  However, we
recommend that you not follow these links upon your first reading of
this tutorial!

See REWRITE <> for a description of how to create a rewrite
rule.

See LINEAR <>  for a description of how to store theorems
concluding with arithmetic inequalities.  The trouble with storing

     (<= (len (delete e x)) (len x))

as a rewrite rule is that it only matches instances of that inequality
and thus fails to match

     (<= (LEN (DELETE E X)) (+ 1 (LEN X)))

ACL2 contains an extensible linear arithmetic decision procedure and by
storing inequalities as :linear rules you can make that decision
procedure aware of the basic inequalities between non-primitive
numerically valued terms.

See EQUIVALENCE <>, see CONGRUENCE <>, and see
REFINEMENT <> to learn how to introduce a new equivalence relation to
the rewriter.  For example, suppose you define set-equal so that it
returns t precisely if its two arguments are lists containing the same
elements, regardless of order or number of occurrences.  Note that
under this sense of "equivalence", (rev x) is the identity function and
append is commutative, for example.

     (set-equal (rev x) x)

     (set-equal (append x y) (append y x))

You can make ACL2 use these two theorems as :rewrite rules to replace
instances of (REV x) and (APPEND x y) by set-equal terms, even though
the results are not actually EQUAL.  This is possible provided the
target occurs in a context admitting set-equal as a congruence relation.
For example, the :congruence rule:

     (implies (set-equal a b)
              (iff (member e a)
                   (member e b)))

gives the rewriter permission to use the above set-equal rules as
rewrite rules in the second argument of any member expression being used
in a propositional way.

See ELIM <> for a description of how to make the system adopt a
"change of variable" tactic that can trade in destructor functions for
constructor functions.  In analogy with how ACL2 eliminates (CAR X) and
(CDR X) by replacing X with (CONS A B), you can make it eliminate other
destructors.  For example, the system book "arithmetic-5/top" provides
an elim rule that eliminates (floor x y) and (mod x y) by replacing x
by (+ r (* y q)), so that the floor expression becomes q and the mod
expression becomes r.  When introducing your own elim rules you will
probably also need to introduce generalize rules (see below) so that
the new variables are appropriately constrained.

See GENERALIZE <> for a description of how you can make ACL2
restrict the new variables it introduces when generalizing.  ACL2 will
sometimes replace a term by a new variable and with generalize rules
you can insure that the new variable symbol has certain properties of
the term it replaces.

See INDUCTION <> for a description of how to tailor the
inductions suggested by a term.  Most of the time when ACL2 chooses the
"wrong" induction, the easiest fix is with a local :induct hint (see
below).  But if the same problem arises repeatedly in several theorems,
you might want to "educate" ACL2's induction heuristic.

For a complete list of rule-classes, See RULE-CLASSES <>.

If you are reading this as part of the tutorial introduction to the
theorem prover, use your browser's Back Button now to return to
introduction-to-the-theorem-prover.

INTRODUCTORY-CHALLENGE-PROBLEM-1    challenge problem 1 for the new user of ACL2

Start in a fresh ACL2, either by restarting your ACL2 image from
scratch or executing

     :ubt! 1

which will undo everything since the first user event.

Then define this function:

     (defun rev (x)
       (if (endp x)
           nil
           (append (rev (cdr x)) (list (car x)))))

Then use The Method to prove:

     (defthm triple-rev
       (equal (rev (rev (rev x))) (rev x)))

When you've solved this problem, compare your answer to ours; see
INTRODUCTORY-CHALLENGE-PROBLEM-1-ANSWER.

Then, use your browser's Back Button to return to
introductory-challenges.

INTRODUCTORY-CHALLENGE-PROBLEM-1-ANSWER    answer to challenge problem 1 for the new user of ACL2

This answer is in the form of an ACL2 script sufficient to lead ACL2 to
a proof.

     (defun rev (x)
       (if (endp x)
           nil
           (append (rev (cdr x)) (list (car x)))))

     ; Trying triple-rev at this point produces a key checkpoint containing
     ; (REV (APPEND (REV (CDR X)) (LIST (CAR X)))), which suggests:

     (defthm rev-append
       (equal (rev (append a b))
              (append (rev b) (rev a))))

     ; And now triple-rev succeeds.

     (defthm triple-rev
       (equal (rev (rev (rev x))) (rev x)))

     ; An alternative, and more elegant, solution is to prove the rev-rev
     ; instead of rev-append:

     ; (defthm rev-rev
     ;   (implies (true-listp x)
     ;            (equal (rev (rev x)) x)))

     ; Rev-rev is also discoverable by The Method because it is
     ; suggested by the statement of triple-rev itself:  rev-rev
     ; simplifies a simpler composition of the functions in triple-rev.

     ; Both solutions produce lemmas likely to be of use in future proofs
     ; about rev.

Use your browser's Back Button now to return to
introductory-challenge-problem-1.

INTRODUCTORY-CHALLENGE-PROBLEM-2    challenge problem 2 for the new user of ACL2

Start in a fresh ACL2, either by restarting your ACL2 image from
scratch or executing :ubt! 1.

Use The Method to prove

     (defthm subsetp-reflexive
       (subsetp x x))

When you've solved this problem, compare your answer to ours; see
INTRODUCTORY-CHALLENGE-PROBLEM-2-ANSWER.

Then, use your browser's Back Button to return to
introductory-challenges.

INTRODUCTORY-CHALLENGE-PROBLEM-2-ANSWER    answer to challenge problem 2 for the new user of ACL2

This answer is in the form of a script sufficient to lead ACL2 to a
proof.

     ; Trying subsetp-reflexive at this point produces the key checkpoint:

     ; (IMPLIES (AND (CONSP X)
     ;               (SUBSETP (CDR X) (CDR X)))
     ;          (SUBSETP (CDR X) X))

     ; which suggests the generalization:

     (defthm subsetp-cdr
       (implies (subsetp a (cdr b))
                (subsetp a b)))

     ; And now subsetp-reflexive succeeds.

     (defthm subsetp-reflexive
       (subsetp x x))

     ; A weaker version of the lemma, namely the one in which we
     ; add the hypothesis that b is a cons, is also sufficient.

     ;    (defthm subsetp-cdr-weak
     ;      (implies (and (consp b)
     ;                    (subsetp a (cdr b)))
     ;               (subsetp a b)))

     ; But the (consp b) hypothesis is not really necessary in
     ; ACL2's type-free logic because (cdr b) is nil if b is
     ; not a cons.  For the reasons explained in the tutorial, we
     ; prefer the strong version.

Use your browser's Back Button now to return to
introductory-challenge-problem-2.

INTRODUCTORY-CHALLENGE-PROBLEM-3    challenge problem 3 for the new user of ACL2

Start in a fresh ACL2, either by restarting your ACL2 image from
scratch or executing :ubt! 1.

Define the following functions and use The Method to prove the theorem
at the bottom:

     (defun rev (x)
       (if (endp x)
           nil
           (append (rev (cdr x)) (list (car x)))))

     (defun dupsp (x)  ; does x contain duplicate elements?
       (if (endp x)
           nil
           (if (member (car x) (cdr x))
               t
               (dupsp (cdr x)))))

     (defthm dupsp-rev
       (equal (dupsp (rev x)) (dupsp x)))

When you've solved this problem, compare your answer to ours; see
INTRODUCTORY-CHALLENGE-PROBLEM-3-ANSWER.

Then, use your browser's Back Button to return to
introductory-challenges.

INTRODUCTORY-CHALLENGE-PROBLEM-3-ANSWER    answer to challenge problem 3 for the new user of ACL2

This answer is in the form of a script sufficient to lead ACL2 to a
proof.

     ; Trying dupsp-rev at this point produces the key checkpoint:

     ; (IMPLIES (AND (CONSP X)
     ;               (NOT (MEMBER (CAR X) (CDR X)))
     ;               (EQUAL (DUPSP (REV (CDR X)))
     ;                      (DUPSP (CDR X))))
     ;          (EQUAL (DUPSP (APPEND (REV (CDR X)) (LIST (CAR X))))
     ;                 (DUPSP (CDR X))))

     ; which suggests the lemma

     ; (defthm dupsp-append
     ;   (implies (not (member e x))
     ;            (equal (dupsp (append x (list e)))
     ;                   (dupsp x))))

     ; However, attempting to prove that, produces a key checkpoint
     ; containing (MEMBER (CAR X) (APPEND (CDR X) (LIST E))).
     ; So we prove the lemma:

     (defthm member-append
       (iff (member e (append a b))
            (or (member e a)
                (member e b))))

     ; Note that we had to use iff instead of equal since member is not a
     ; Boolean function.

     ; Having proved this lemma, we return to dupsp-append and succeed:

     (defthm dupsp-append
       (implies (not (member e x))
                (equal (dupsp (append x (list e)))
                       (dupsp x))))

     ; So now we return to dups-rev, expecting success.  But it fails
     ; with the same key checkpoint:

     ; (IMPLIES (AND (CONSP X)
     ;               (NOT (MEMBER (CAR X) (CDR X)))
     ;               (EQUAL (DUPSP (REV (CDR X)))
     ;                      (DUPSP (CDR X))))
     ;          (EQUAL (DUPSP (APPEND (REV (CDR X)) (LIST (CAR X))))
     ;                 (DUPSP (CDR X))))

     ; Why wasn't our dupsp-append lemma applied?  We have two choices here:
     ; (1) Think.  (2) Use tools.

     ; Think:  When an enabled rewrite rule doesn't fire even though the left-hand
     ; side matches the target, the hypothesis couldn't be relieved.  The dups-append
     ; rule has the hypothesis (not (member e x)) and after the match with the left-hand side,
     ; e is (CAR X) and x is (REV (CDR X)).  So the system couldn't rewrite
     ; (NOT (MEMBER (CAR X) (REV (CDR X)))) to true, even though it knows that
     ; (NOT (MEMBER (CAR X) (CDR X))) from the second hypothesis of the checkpoint.
     ; Obviously, we need to prove member-rev below.

     ; Use tools:  We could enable the ``break rewrite'' facility, with

     ; ACL2 !>:brr t

     ; and then install an unconditional monitor on the rewrite rule
     ; dupsp-append, whose rune is (:REWRITE DUPSP-APPEND), with:

     ; :monitor (:rewrite dupsp-append) t

     ; Then we could re-try our main theorem, dupsp-rev.  At the resulting
     ; interactive break we type :eval to evaluate the attempt to relieve the
     ; hypotheses of the rule.

     ; (1 Breaking (:REWRITE DUPSP-APPEND) on
     ; (DUPSP (BINARY-APPEND (REV #) (CONS # #))):
     ; 1 ACL2 >:eval

     ; 1x (:REWRITE DUPSP-APPEND) failed because :HYP 1 rewrote to
     ; (NOT (MEMBER (CAR X) (REV #))).

     ; Note that the report above shows that hypothesis 1 of the rule
     ; did not rewrite to T but instead rewrote to an expression
     ; involving (member ... (rev ...)).  Thus, we're led to the
     ; same conclusion that Thinking produced.  To get out of the
     ; interactive break we type:

     ; 1 ACL2 >:a!
     ; Abort to ACL2 top-level

     ; and then turn off the break rewrite tool since we won't need it
     ; again right now, with:

     ; ACL2 !>:brr nil

     ; In either case, by thinking or using tools, we decide to prove:

     (defthm member-rev
       (iff (member e (rev x))
            (member e x)))

     ; which succeeds.  Now when we try to prove dups-rev, it succeeds.

     (defthm dupsp-rev
       (equal (dupsp (rev x))
              (dupsp x)))

Use your browser's Back Button now to return to
introductory-challenge-problem-3.

INTRODUCTORY-CHALLENGE-PROBLEM-4    challenge problem 4 for the new user of ACL2

Start in a fresh ACL2, either by restarting your ACL2 image from
scratch or executing :ubt! 1.

This problem is much more open ended than the preceding ones.  The
challenge is to define a function that collects exactly one copy of
each element of a list and to prove that it returns a subset of the
list with no duplications.

Hint:  We recommend that you read this hint to align your function names
with our solution, to make comparisons easier.  Our answer is shown in
see INTRODUCTORY-CHALLENGE-PROBLEM-4-ANSWER.  In that page
you'll see a definition of a function collect-once and the proofs of
two theorems:

     (defthm main-theorem-1-about-collect-once
       (subsetp (collect-once x) x))

     (defthm main-theorem-2-about-collect-once
       (not (dupsp (collect-once x))))

The function dupsp is as defined in see
INTRODUCTORY-CHALLENGE-PROBLEM-3.  This is quite easy.

Then, we define a tail-recursive version of the method based on the
pseudo-code:

      a = nil;
      while (x not empty) {
       a = if (member (car x) a) then a else (cons (car x) a);
       x = (cdr x);
       }
      return a;

We formalize this with the function while-loop-version, where
(while-loop-version x nil) is the "semantics" of the code above.  I.e.,
the function while-loop-version captures the while loop in the
pseudo-code above and returns the final value of a, and it should be
invoked with the initial value of a being nil.

We prove (while-loop-version x nil) returns a subset of x that contains
no duplications.  Furthermore, we do it two ways: first "indirectly" by
relating while-loop-version to collect-once, and second ("directly")
without using collect-once.  Both of these proofs are much harder than
the collect-once approach, involving about a dozen lemmas each.

Compare your solutions to ours at see
INTRODUCTORY-CHALLENGE-PROBLEM-4-ANSWER.

Then, use your browser's Back Button to return to
introductory-challenges.