\documentclass{llncs}

\usepackage{acl2}
\usepackage{makeidx}

\newcommand{\html}[1]{\ptt{#1}}
\newcommand{\dsp}{\renewcommand{\baselinestretch}{1.5} \tiny \normalsize }

\begin{document}

\newcommand{\ptt}[1]{\begin{normalfont}\frenchspacing\texttt{#1}\end{normalfont}}

\newcommand{\SmallSkip}{\vspace{0.5cm}\noindent}

\setlength{\intextsep}{0.1in}

\title{How To Prove Theorems Formally}
\titlerunning{How To Prove Theorems Formally}
\author{Matt Kaufmann\inst{1} \and J Strother Moore\inst{2}}
\authorrunning{Kaufmann and Moore}
\tocauthor{Matt Kaufmann (AMD),
J Strother Moore (University of Texas at Austin)}
\institute{Advanced Micro Devices, Inc., 5900 East Ben White
  Blvd., Austin, TX 78741,\\
\email{matt.kaufmann@amd.com}
\and
Department of Computer Sciences, University of Texas at Austin,\\
 Taylor Hall 2.124, Austin, Texas 78712,\\
\email{moore@cs.utexas.edu}\\
August 5, 2005}

\maketitle

\section{Abstract}

Today it is impractical to prove -- formally and mechanically -- the
correctness of entire computing systems of commercial interest.  There are
many reasons for this, both technical and economic.
Mechanized theorem proving is nevertheless relevant in commercial hardware
and software production.  But practical considerations require that we focus
our attention on problems that are both technically feasible within the time
limits available and of interest to system designers.

Why might designers turn to a mechanical theorem prover?  Because the
problems -- even the little ones -- are so complicated they do not have
confidence that their reasoning is sound.  Formal, mechanized reasoning is
crucial.

In this paper we briefly will describe several such ``little theorems,'' that
is, theorems that address issues of concern to designers without trying to
address the complete correctness of the system.  The theorems have all been
formalized and proved with the ACL2 theorem prover.  ``ACL2'' stands for
{\underline{A}} {\underline{C}}omputational {\underline{L}}ogic for
{\underline{A}}pplicative {\underline{C}}ommon {\underline{L}}isp.  It is a
theorem prover in the Boyer-Moore tradition that uses rewriting, decision
procedures, mathematical induction and many other proof techniques to prove
theorems in a first-order mathematical theory of recursively defined functions and
inductively constructed objects \cite{kmm00a}.

However, these descriptions are just motivational.  The real purpose of this
paper is to answer the question how does one construct and manage large
mechanically checked proofs (in ACL2)?  After mention of the big industrial
examples, we turn our attention to truly simple formal theorems about list
processing and develop some advice to the reader.  Most of this advice is
meant to be helpful no matter what mechanized system or mathematical logic
you are using.

The paper contains exercises.  To learn how to do proofs, it is crucial that
you work the exercises.  The ACL2 system is available without charge on the
net; see the ACL2 home page \cite{km}.  

However, it is not necessary to use the ACL2 system to do the exercises.  They can
be done with pencil and paper or with other mechanical theorem proving systems
with which you might be familiar.  But the only way to learn how to do proofs is
to do proofs!

Answers to the exercises are available on the web.  See
\html{http://\-www\-.cs\-.utexas\-.edu\-/users\-/moore\-/publications\-/how\--to\--prove\--thms\-/index\-.html}.

Early exercises ask the reader to define some functions used in challenge
theorems in later exercises.  To ensure those challenges are understood, we
have included in Appendix \ref{alldefs} our definitions of all functions
mentioned in any challenge theorem.

\vspace*{.1in}

\noindent{\bf{Keywords}}: ACL2, hardware verification, software verification,
formal verification, theorem proving, automated reasoning.

\markboth{Matt Kaufmann and J Strother Moore}{}
\markright{How To Prove Theorems Formally}


\section{Background}

``ACL2'' is the name of a functional programming language (based on Common
Lisp), a first-order mathematical logic, and a mechanical
theorem prover.  ACL2, which is sometimes called an ``industrial strength
version of the Boyer-Moore system,'' is the product of Kaufmann and Moore,
with many early design contributions by Boyer.  It has been used for a
variety of important formal methods projects of industrial and commercial
interest, including:
\begin{itemize}
\item verification that the register-transfer level description of the
AMD Athlon$^{TM}$ processor's elementary floating point arithmetic circuitry implements the IEEE
floating point standard \cite{russinoff98,kmm00b-chap13}; similar work has been done
for components of the AMD-K5 processor \cite{mlk98}, the IBM Power 4 \cite{Sawada02}, and
the AMD Opteron$^{TM}$ processor.\footnote{AMD, the AMD logo, AMD Athlon, AMD
Opteron, and combinations thereof, are trademarks of Advanced Micro Devices, Inc.}

\item verification that a microarchitectural model of a Motorola digital
signal processor (DSP) implements a given microcode engine \cite{bh99} and
verification that specific microcode extracted from the ROM implements
certain DSP algorithms \cite{bm05};

\item verification that microcode for the Rockwell Collins AAMP7
implements a given security policy having to do with process separation
\cite{gw03};

\item verification that the JVM bytecode produced by the Sun compiler
{\tt{javac}} on certain simple Java classes implements the claimed
functionality \cite{moore02a} and the verification of properties of
importance to the Sun bytecode verifier as described in JSR-139 for J2ME JVMs
\cite{lm03};

\item verification of the soundness and completeness of a Lisp implementation
of a BDD package that has achieved runtime speeds of about 60\% those of the CUDD
package (however, unlike CUDD, the verified package does not support dynamic
variable reordering and is thus more limited in scope) \cite{sumners00};

\item verification of the soundness of a Lisp program that checks the proofs
produced by the Ivy theorem prover from Argonne National Labs; Ivy proofs may
thus be generated by unverified code but confirmed to be proofs by a verified
Lisp function \cite{kmm00b-chap16}.
\end{itemize}
Other applications are described in \cite{kmm00b} and in the papers distributed
as part of the periodic ACL2 workshops, the proceedings of which may be found
via the {\underline{Workshops}} link on the ACL2 home page \cite{km}.

As these examples demonstrate, it is possible to construct mechanically
checked proofs of properties of great interest in industrial hardware and
software designers.  The properties proved are typically not complete
characterizations of the correctness of the systems studied.  For example,
the proofs about the AMD microprocessors -- the AMD-K5 processor, the AMD Athlon processor, and the
AMD Opteron processor -- just deal with the IEEE compliance of certain floating point
operations modeled at the register transfer level.  The microprocessors
contain many unverified components and the verified ones could fail 
due to violations of their input conditions.

Nevertheless, these theorems were proved for good reason: the designers were
concerned about their designs.  Aspects of these designs are quite subtle or
complicated and formal specification and mechanized proof offer the most
complete way to relieve the concerns that something critical to correct
functionality had been overlooked in the designs.

In addition to being interesting, these theorems are hard to prove.  That is
a relative judgment of course.  Compared to longstanding open problems, these
theorems are all trivial.  But by many measures each of these proofs is much
more complicated than any proof ever encountered by most readers.  For
example, the IEEE compliance proof for the floating point division microcode
for the AMD-K5 processor (in 1995) required the formal statement and proof of
approximately 1,200 lemmas.  Subsequent AMD floating-point proofs are harder
to measure because they build on libraries of lemmas that have been
accumulating since 1995. The correspondence result between the Motorola DSP
microarchitecture and its microcode engine involved intermediate formulas
that, when printed, consumed 25 megabytes (approximately 5000 pages of
densely packed text) {\em{per formula}}.  And the proof involved hundreds of
such formulas.  The correctness argument for one particular DSP microcode
program required an extremely subtle generalization that took many days for
the author to craft.  The formal model of the Connected Limited Device
Configuration (CLDC) JVM and bytecode verifier is almost 700 pages of densely packed
text.  The proof that a simple Java class, which spawns an unbounded number
of threads, produces a monotonic increase in the value of a certain shared
counter produces about 19,000 subgoals and requires about 84 megabytes to
print.

In these senses, the theorems in which we are interested are little (but
hard) theorems about big systems, or put another way, they are valuable and
non-trivial theorems about parts of very complicated systems.

How do we prove theorems like this?  There is no mystery.  We prove theorems
like this the same way we prove simple theorems: by properly defining the
concepts and carefully stating the theorem, by separating concerns, by
appropriate decomposition of the proof into more general lemmas, and by the
recursive application of the same methodology.  But to do it on a grand scale
takes more than the usual attention to detail and good taste.  Minor
misjudgments that are tolerable in small proofs are blown out of proportion
in big ones.  Unnecessarily complicated function definitions or messy,
hand-guided proofs are things that can be tolerated in small projects without
endangering success; but in large projects, such things can doom
of the proof effort.

If you aim to produce big proofs, it pays to learn how to produce small ones
well.

\section{The Mechanics of Using the System}

You do not need to use the ACL2 system to learn from this paper.  This paper
is primarily about how to state and prove theorems in a particular formal
mathematical logic.  Students do not often do that!  Students studying
mathematical logic mostly read about {\em{meta}}-theorems proved {\em{about}}
formal logics, e.g., completeness, undecidability, etc.  Students studying
mathematics and computer science see ``theorems'' stated {\em{informally}}
(in a mixture of English and mathematical notation) and ``prove'' them
{\em{informally}}.

We study theorems and proofs in a rigorous setting.  Expressing every claim
{\em{formally}} -- as a formula in a well-defined syntax -- takes some
getting used to!  Proving them rigorously -- justifying every step with
formulas and appeals to rules of inference -- takes even more!  Our logic is
supported by a mechanized theorem prover that prints out its proofs in an
informal style that should be familiar to most mathematically literate
readers.  But when the theorem prover fails and you are called upon to help
it, that help almost always takes the form of a formula or a hint to use a
certain formula.  Thus, to use the theorem prover effectively you must learn
to think with formulas.

You may read this paper in conjunction with the ACL2 system to learn both how
to express your ideas in formulas and how to use the system.  We recommend
reading this section even if you do not intend to use the ACL2 system; at
least it will give you a sense of what is involved with producing large
mechanically checked proofs.

If you want to use the system, first install it on your machine (if it is not
already there), following the instructions in the {\underline{Obtaining and
Installing}} link of the ACL2 home page \cite{km}.

Next, learn to navigate {\underline{The User's Manual}} linked to from the home page.  In
particular, learn to use the {\underline{Index}}.  For example, find and read
the documentation under \ptt{STARTUP}.  Try the {\underline{SEARCH}} link near
the top of the home page.

Throughout the rest of this
document, when we say ``see {\underline{\em{name}}},'' we mean find and
read the documentation of {\em{name}} in the online documentation.

Most users use ACL2 from within Emacs.  See Appendix \ref{emacs} for a few
helpful notes.  Within Emacs, create a shell buffer (by typing \ptt{meta-x
shell enter}).  Typically, the buffer created is named \ptt{*shell*}.  Lines
typed into the bottom of the \ptt{*shell*} are fed as input to a Linux or
other operating system ``shell'' process running under Emacs; output is
streamed into the \ptt{*shell*} buffer.  In the \ptt{*shell*} buffer invoke
ACL2.  Thus, the \ptt{*shell*} buffer becomes an editable and searchable log
of all your transactions with ACL2.

ACL2 presents itself as a read-eval-print loop, with the prompt \ptt{ACL2
!>}.  Whatever you type after this prompt is read by ACL2, evaluated, and the
results are printed.  Then you are prompted for another input.  However, it
is rare that you will type directly to the ACL2 loop.  Instead, we create our
definitions and proof plans in another buffer and submit commands from that
buffer to ACL2.

So create another buffer, which here we call \ptt{script}, by typing
\ptt{ctrl-x b script enter}.  In this buffer you
will write down your proposed proof scripts.  It will typically consist of a
sequence of definitions and lemmas, concluding with your main theorem.  These
scripts typically contain many Lisp comments, preceded on each line by a semi-colon.  After
typing the initial draft of the problem and its solution, position the Emacs
cursor at the top of the \ptt{script} buffer.

We maintain the following invariant between the \ptt{script} buffer and the
\ptt{*shell*} buffer: every command in the \ptt{script} preceding the cursor
has been successfully executed in the \ptt{*shell*} (in the same order) and
those are the only commands that have been executed.  That is, the cursor
of the \ptt{script} buffer
defines a ``barrier'' between what has been done and what is left to do.  The
command immediately after the cursor is the ``next command'' to try.

You should learn how to copy that command into the \ptt{*shell*} buffer, at
the bottom, and to advance the \ptt{script} buffer cursor past the command.
This is how you will submit previously prepared ACL2 forms to ACL2.

Before continuing we answer two commonly asked questions.  First Question:
Why are we bothering to show Emacs in a discussion of how to use a
mechanical theorem prover?  Answer: It serves as a warning.  Don't aspire to
prove big theorems mechanically unless you are prepared to use a variety of
sophisticated text processing tools.  When you have to inspect multi-megabyte
formulas, you will be happy to know of the existence of Emacs commands like
\ptt{meta-1 meta-x compare-windows} (which compares two windows containing
s-expressions, ignoring differences in prettyprinting style).

Second Question: Why don't we implement an Emacs/ACL2 interface instead of
recommending that the user learn Emacs?  Answer: We have learned that users evolve
their own styles, both for ACL2 and for Emacs.  Using somebody else's style
is often cumbersome.  We are describing our style.  Use it as a starting
point but understand how personal it is and how flexible Emacs is.

Having prepared the initial draft of the \ptt{script}, we submit commands
successively.  If a command is successful (i.e., the definition is admitted
or the theorem is proved) we submit the next command.  If the command is
unsuccessful, we move the \ptt{script} cursor back in front of the failed
command and inspect the output of ACL2 in the \ptt{*shell*} buffer.

Typically, one of two things must be done.  Either the command is faulty
(e.g., syntactically ill-formed) and must be edited, or additional lemmas
must be proved before it can be successfully submitted.  Learning how to read
ACL2 output and determine what to do is the biggest task facing the new user
because it is usually tantamount to the theorem proving problem: how can this
theorem be decomposed into provable lemmas?  Ultimately, that is what this
paper is about.

But suppose we have determined, somehow, that the appropriate response to the
failed command, $\gamma$, is to prove two new lemmas, say $\alpha$ and
$\beta$.  Then we type them into the \ptt{script} buffer, one after the
other, immediately in front of $\gamma$.  Then we position the cursor in
front of $\alpha$ and resume our iterative submission process.

Note that if $\alpha$ fails, the process just described will lead us to begin
working on the subtask of how to prove $\alpha$, by inserting additional lemmas in
front of it.  When we ultimately succeed in proving them and $\alpha$, the
cursor will have moved just past $\alpha$ and be in front of $\beta$.  Only
after $\beta$ is proved will we confront $\gamma$ again, and by then our
proof plan for it, namely $\alpha$ and $\beta$, will be in place.  Had we
not written $\alpha$ and $\beta$ down when we analyzed the failure of $\gamma$
and used the \ptt{script} buffer in a disciplined way, we might well have
forgotten about $\beta$ and had to re-analyze the failure of $\gamma$
to re-discover the need for $\beta$.

There is no guarantee here that our plan for proving $\gamma$ will succeed.
If it doesn't, this method will cause us to insert additional lemmas for
$\gamma$ just after $\beta$.  A modular top-down proof development
methodology, in which we check and guarantee that $\alpha$ and $\beta$ permit
the proof of $\gamma$ before descending to prove them, is described in
\cite{kmm00b-chap6}.

We regularly save our work, by saving the \ptt{script} to a file, say
\ptt{script.lisp}.  This allows us to recreate our state, should we wish
to quit for the time being and resume later.  We typically put the command
\ptt{(i-am-here)} into the \ptt{script} buffer at the cursor, just to mark
the current location of the barrier.  When \ptt{(i-am-here)} is executed it
causes an error. 

When we are ready to resume our work, we start a new ACL2
in the \ptt{*shell*} buffer (if the old one has been lost) and type:
\begin{acl2p}
(ld "script.lisp" :ld-pre-eval-print t)
\end{acl2p}
which will execute all of the commands in the file until the first
error.  This recreates the ACL2 state we had when we saved the file,
re-establishing our
invariant between \ptt{script} and \ptt{*shell*}.  If the proofs take a long
time we might do
\begin{acl2p}
(ld "script.lisp" :ld-pre-eval-print t :ld-skip-proofs t)
\end{acl2p}
or, more briefly,
\begin{acl2p}
(rebuild "script.lisp" t)
\end{acl2p}
which {\em{just assumes}} the proof obligations of each command.  Given that
we have successfully executed them in a prior session, this is a reasonable way to
re-establish the invariant and leaves us in exactly the same state.

When we finally execute the last command in the \ptt{script}, we have
succeeded and \ptt{script.lisp} is a re-playable proof script for our main
theorem.  We usually try to certify it as a {\em{book}} so that it can be
easily referenced in future proofs.  See {\underline{\ptt{certify-book}}}.

So much for the mechanics of using ACL2.  We now get on the with task
of explaining what it all means, by describing the ACL2 functional
programming language, the logic, and the theorem prover.

\section{Programming in ACL2}

ACL2 is Lisp.  A typical term or expression is \ptt{(cons (car x) (len a))}.
In this expression, \ptt{x} and \ptt{a} are {\em{variable symbols}}, and
\ptt{cons}, \ptt{car}, and \ptt{len} are {\em{function symbols}}.  In more
traditional mathematical syntax, this expression would be written
$cons(car(x),len(a))$.  For the purposes of this paper, it is sufficient to
understand only the expressions of Figure \ref{primitives}.  ACL2 is much
richer than these few primitives would suggest, but throughout this paper we
limit ourselves to a tiny subset so we can discuss in detail how to develop
proofs.

Full ACL2 describes five kinds of data objects in detail -- numbers,
characters, strings, symbols, and (ordered) pairs -- and each can be written
as a constant and used in expressions.  The most commonly used numeric
constants are integers; rationals and complex constants are allowed, but we
will not have occasion to use them in early exercises.  We will not use
character constants here.  Strings are enclosed in single-character
double-quotation marks, \ptt{"Hello world!"}.  The special symbol constants
\ptt{nil} and \ptt{t} -- which have the apparent syntax of variable symbols
-- are written as shown, but all other symbol constants are preceded by a
single quotation mark, \ptt{'ok} and \ptt{'quick-sort}.  The constant
\ptt{nil} is used both as the ``false'' truth value and the ``empty list''
(or, more accurately, as the standard terminator of a nest of pairs used as a
list).  Pairs, or ``conses,'' are written in list notation, e.g.,
$\langle$\ptt{1},$\langle$\ptt{2},$\langle$\ptt{3},\ptt{nil}$\rangle$$\rangle$$\rangle$
is written \ptt{'(1 2 3)} and nests not right-terminated with \ptt{nil} are
written using ``dot notation,'' e.g.,
$\langle$\ptt{1},$\langle$\ptt{2},\ptt{3}$\rangle$$\rangle$ is written
\ptt{'(1 2 . 3)}.  Indeed, \ptt{'(1 2 3)} may also be written \ptt{'(1 2 3
. nil)}.

Newcomers are often confused by when to use the single-quote mark.  \ptt{'(1
2 3)} is a term that evaluates to the list constant \ptt{(1 2 3)}.  Why not
write \ptt{(1 2 3)}?  Well, consider the two terms \ptt{(car x)} and
\ptt{'(car x)}.  The first is how we write the application of the function
symbol \ptt{car} to the variable symbol \ptt{x}.  The second is a term that
evaluates to the list constant \ptt{(car x)}, i.e., list whose first element
is the symbol \ptt{car}.  If $\alpha$ is a parenthesized expression or a
symbol, like \ptt{car} or \ptt{x}, and you are writing a term, write
\ptt{'$\alpha$} if you mean the term that evaluates to $\alpha$, and
write $\alpha$ if you mean the term (function application or variable symbol)
$\alpha$.

Each of the five data types can be created and decomposed by various
functions.  But in this paper we omit all mention of the structural
properties of numbers, characters, strings and symbols and deal only with
pairs.  By limiting ourselves to pairs, we can quickly dispense with their
basic properties and get on with the task of learning how to define
recursive functions and prove theorems.

\begin{figure}
\label{primitives}
\begin{center}
\begin{tabular}{|l|l|}
\hline
\ptt{(cons $x$ $y$)} & construct the ordered pair $\langle x,y \rangle$ \\
\ptt{(car $x$)} & left component of $x$, if $x$ is a pair; \ptt{nil} otherwise  \\
\ptt{(cdr $x$)} & right component of $x$, if $x$ is a pair; \ptt{nil} otherwise  \\
\ptt{(consp $x$)} & \ptt{t} if $x$ is a pair; \ptt{nil} otherwise \\
\ptt{(if $x$ $y$ $z$)} & $z$ if $x$ is \ptt{nil}; $y$ otherwise \\
\ptt{(equal $x$ $y$)} & \ptt{t} if $x$ is $y$; \ptt{nil} otherwise \\
\hline
\end{tabular}
\end{center}
\caption{The Primitives for This Paper}
\end{figure}

To define a function, we use the form \ptt{(defun $f$ ($v_1 \ldots v_n$)
$\beta$)} where $f$ is the function symbol being defined, the $v_i$ are the
distinct formal variables, and $\beta$ is the body of the function.

Here are the Lisp definitions of the standard propositional logic connectives:
\begin{acl2p}
(defun not (p) (if p nil t))

(defun and (p q) (if p q nil))

(defun or (p q) (if p p q))

(defun implies (p q) (if p (if q t nil) t))

(defun iff (p q) (and (implies p q) (implies q p)))
\end{acl2p}
Note that in Lisp, \ptt{and} and \ptt{or} are not Boolean valued.  E.g.,
\ptt{(and t 3)} and \ptt{(or nil 3)} both return \ptt{3}.  This is
unimportant if they are only used propositionally, e.g., \ptt{(and t 3)}
$\leftrightarrow$ \ptt{(and 3 t)} $\leftrightarrow$ \ptt{t}, if
``$\leftrightarrow$'' means \ptt{iff}.  By convention, these two functions
are allowed to take more than two arguments and when so used abbreviate
right-associated nests, e.g., \ptt{(and p q r s)} is an abbreviation for
\ptt{(and p (and q (and r s)))}.  Technically, they are defined as
``macros.''

Most often we make definitions that are recursive, because ACL2 has no
iterative control structures or higher-order functions, and has only primitive
reasoning support for quantifiers.
Here is a function that ``copies'' a list replacing each element occurrence by
two adjacent occurrences.
\begin{acl2p}
(defun dup (x)
  (if (consp x)
      (cons (car x)
            (cons (car x)
                  (dup (cdr x))))
      nil))
\end{acl2p}
For example, the term \ptt{(dup '(1 2 3))} has value \ptt{(1 1 2 2 3 3)} and the
term
\ptt{(dup '(hello))} evaluates to \ptt{(hello hello)}.

Here is a function that concatenates two lists.
\begin{acl2p}
(defun app (x y)
  (if (consp x)
      (cons (car x) (app (cdr x) y))
    y))
\end{acl2p}
For example, \ptt{(app '(1 2 3) '(4 5 6))} has value \ptt{(1 2 3 4 5 6)} and
\ptt{(app '(A B C . D) '(E F))} has value \ptt{(A B C E F)}.

Here is a function that determines whether \ptt{e} is an element of list
\ptt{x}.
\begin{acl2p}
(defun memp (e x)
  (if (consp x)
      (if (equal e (car x))
          t
        (memp e (cdr x)))
    nil))
\end{acl2p}
For example, \ptt{(memp 1 '(0 1 2 3))} is \ptt{t} and
\ptt{(memp 5 '(0 1 2 3))} is \ptt{nil}.

Here is a function that reverses a list, e.g., \ptt{(rev '(1 2 3))} is
\ptt{(3 2 1)}.
\begin{acl2p}
(defun rev (x)
  (if (consp x)
      (app (rev (cdr x)) (cons (car x) nil))
    nil))
\end{acl2p}
Note that \ptt{(rev '(1 2 3 . ABC))}  is \ptt{(3 2 1)}, i.e., the
terminal marker of the input is not preserved (unless it happened to be
\ptt{nil}), given the way we defined \ptt{rev}.

Here is a ``tail-recursive'' version of rev that uses its second argument
as an ``accumulator'' to construct the answer more efficiently.
\begin{acl2p}
(defun rev1 (x a)
  (if (consp x)
      (rev1 (cdr x) (cons (car x) a))
    a))
\end{acl2p}
For example, \ptt{(rev1 '(1 2 3) nil)} is \ptt{(3 2 1)}.

\vspace*{.1in}
\noindent {\bf{Exercises}}
\vspace*{.1in}

You may wish to define auxiliary functions to solve some of the exercises
below.  If you are using the ACL2 system to experiment with your answers and
you try to re-define an existing ACL2 function you will get an error (unless
your definition is syntactically the same as ours).  To see how to inspect
the pre-existing definition, see {\underline{\ptt{pe}}}
(``print event'') and {\underline{\ptt{pf}}} (``print formula'').  When using the ACL2 system, be aware that it insists that
all functions terminate.  Thus, recursion on the list structure \ptt{x}
should be controlled by a \ptt{(consp x)} test, not \ptt{(equal x nil)}.

\vspace*{.05in}
{\noindent}{\bf{Problem 4.1}} Define the function \ptt{properp} to determine whether a list
``ends in \ptt{nil},'' i.e., whether the \ptt{cdr} of the right-most \ptt{cons} is
\ptt{nil}.  (In Lisp, functions that are used as predicates are commonly
given names that conclude with the letter ``\ptt{p}''.  Lists satisfying
\ptt{properp} are sometimes called ``proper lists'' or ``true lists.'')

\vspace*{.05in}
{\noindent}{\bf{Problem 4.2}} Define \ptt{mapnil} to ``copy'' a list, replacing each element
by \ptt{nil}.

\vspace*{.05in}
{\noindent}{\bf{Problem 4.3}} The result of ``swapping'' the pair $\langle x,y \rangle$ is
the pair $\langle y,x \rangle$.  Define \ptt{swaptree} to swap every
cons in the binary tree \ptt{x}.

\vspace*{.05in}
{\noindent}{\bf{Problem 4.4}} Define \ptt{ziplists} to take two lists and return a list as
long as the first whose successive elements are the pairs of corresponding
elements from the two lists.  If the second list is too short, extend it with
\ptt{nil}s.

\vspace*{.05in}
{\noindent}{\bf{Problem 4.5}} A proper list of pairs is called an ``association list'' or
``alist''.  The standard function \ptt{alistp} recognizes them.  Association
lists are frequently used as tables.  The value associated with the key $key$
in alist $a$ is the \ptt{cdr} of the first pair in $a$ whose \ptt{car} is $key$.
Define \ptt{lookup} to take a key and an alist and to return the value of the
key in the alist or else \ptt{nil} if no pair is found.

\vspace*{.05in}
{\noindent}{\bf{Problem 4.6}} Define \ptt{foundp} to determine whether a given key is found in a
given alist.

\vspace*{.05in}
{\noindent}{\bf{Problem 4.7}} Define the list analogue of subset, i.e., \ptt{(subp $x$ $y$)}
returns \ptt{t} or \ptt{nil} according to whether every element of $x$ is
an element of $y$.

\vspace*{.05in}
{\noindent}{\bf{Problem 4.8}} Define \ptt{int} to take two proper lists and to
return the proper list of elements that appear in both.

\vspace*{.05in}
{\noindent}{\bf{Problem 4.9}} Consider the leaves of a binary tree.  We say a leaf is
``lonesome'' if it occurs only once.  Define \ptt{lonesomes} to take a tree
and return its lonesome leaves.

\section{Elementary Proofs in the ACL2 Logic}

Some axioms corresponding to the six primitives in Figure \ref{primitives}
are shown in Figure \ref{primaxs}.  The actual axioms used by ACL2 are
somewhat different because they include axioms for all the data types.  For
example, Axiom 1 of the figure can be proved from ACL2's axioms concerning
the structure of symbols.  Axiom 8 of the figure, stating that \ptt{nil} is
not a \ptt{cons} pair, can be inferred from ACL2's axioms stating that
\ptt{nil} is a symbol and that symbols are disjoint from pairs.  For our
purposes, Axiom 8 is just an example of an infinite number of axioms stating
\ptt{consp} is \ptt{nil} on each symbol, on each number, etc., \ptt{(consp
nil)} = \ptt{(consp t)} = \ptt{(consp 'ok)} = \ptt{(consp 0)} = \ptt{(consp
1)} = \ptt{(consp 2)} = $\ldots$ = \ptt{nil}.

\begin{figure}
\label{primaxs}
\begin{center}
\begin{tabular}{|rl|l|}
\hline
1. & \ptt{t} $\neq$ \ptt{nil}\\

2. & \ptt{x} $\neq$ \ptt{nil} $\rightarrow$ \ptt{(if x y z)} = \ptt{y}\\

3. & \ptt{x} $=$ \ptt{nil} $\rightarrow$ \ptt{(if x y z)} = \ptt{z}\\

4. & \ptt{(equal x y)} = \ptt{nil} $\vee$ \ptt{(equal x y)} = \ptt{t}\\

5. & \ptt{x} = \ptt{y} $\leftrightarrow$ \ptt{(equal x y)} = \ptt{t}\\

6. & \ptt{(consp x)} = \ptt{nil} $\vee$ \ptt{(consp x)} = \ptt{t}\\

7. & \ptt{(consp (cons x y))} = \ptt{t}\\

8. & \ptt{(consp nil)} = \ptt{nil}\\

9. & \ptt{(car (cons x y))} = \ptt{x}\\

10. & \ptt{(cdr (cons x y))} = \ptt{y}\\

11. & \ptt{(consp x)} = \ptt{t} $\rightarrow$ \ptt{(cons (car x) (cdr x))} = \ptt{x}\\

\hline
\end{tabular}
\end{center}
\caption{The Primitive Axioms for This Paper}
\end{figure}

Implicit in this axiomatization is the logical infrastructure to do
propositional calculus and equality.  That is, we take for granted the axioms
and rules of inference allowing us to prove propositional tautologies,
perform substitution of equals for equals, etc.

We also give ourselves the ability to do induction on well-founded orderings.
This involves some additional logical infrastructure, including an Induction
Principle, the introduction of the ordinals up to $\epsilon_0 =
\omega^{\omega^{\omega^{\ldots}}}$, a well-founded relation \ptt{o<} on such
ordinals, and axioms defining the size (measured with the function
\ptt{acl2-count}) of ACL2 objects.  The most common use of \ptt{o<} is on
natural numbers, where it reduces to the ordinary \ptt{<} relation.

The inductive arguments required in this paper all use structural
inductions on lists and binary trees.  With the infrastructure described
above it can be shown that the sizes of \ptt{(car x)} and \ptt{(cdr x)} are
each smaller than the size of \ptt{x} when \ptt{(consp x)} is true.  We can
then use the Induction Principle to prove an arbitrary formula, \ptt{($\psi$
x y)}, where \ptt{x} and \ptt{y} are variable symbols, by proving a
\begin{acl2p}
{\em{Base Case:}}
(implies (not (consp x)) ($\psi$ x y))
\end{acl2p}
and an
\begin{acl2p}
{\em{Induction Step:}}
(implies (and (consp x)         ; {\em{test}}
              ($\psi$ (car x) $\alpha_1$)    $\,$; {\em{induction hypothesis 1}}
              ($\psi$ (cdr x) $\alpha_2$))   $\,$; {\em{induction hypothesis 2}}
         ($\psi$ x y))               ; {\em{induction conclusion}}
\end{acl2p}
where the $\alpha_i$ are arbitrary terms replacing the non-induction variable
\ptt{y}.  Of course, we often need only one of the two induction hypotheses;
we can provide as many different ``copies'' of a hypothesis we wish, using
different choices of $\alpha_i$ for \ptt{y}; and we can use nests of
\ptt{car}s and \ptt{cdr}s in the \ptt{x} position.  Indeed, we may provide as
an induction hypothesis any ($\psi$ $\delta$ $\alpha$) such that we can prove
\ptt{(implies (consp x) (o< (acl2-count $\delta$) (acl2-count x)))}.

It must be emphasized that ACL2's Induction Principle is much more general
than the scheme above suggests.  Below we state the Induction Principle
carefully, for those readers who are curious about it.  In general in this
document we take the position that you can learn to do much with ACL2 by
example and by elaboration, and in that spirit we shy away from the precise
details.  They may be found, however, in \cite{km97a}.

The Induction Principle allows one to derive an arbitrary formula, $\psi$, from
\begin{itemize}
\item {\em Base Case}:
\begin{acl2}
(implies (and (not $q_1$) $\ldots$ (not $q_k$)) $\psi$), {\rm and}
\end{acl2}
\item {\em Induction Step(s)}:  For each $1\leq i \leq k$,
\begin{acl2}
(implies (and $q_i$ $\psi/{\sigma_{i,1}}$ $\ldots$ $\psi/{\sigma_{i,h_i}}$)
         $\psi$){\rm ,}
\end{acl2}
\end{itemize}
provided that for terms $m$, $q_1, ... q_k$, and variable substitutions
$\sigma_{i,j}$ ($1 \leq i \leq k, 1 \leq j \leq h_i$), the following are
theorems:
\begin{itemize}
\item {\em Ordinal Condition}:
\begin{acl2}
(o-p $m$){\rm , and}
\end{acl2}
\item {\em Measure Condition(s)}:  For each $1 \leq i \leq k$, and $1 \leq j \leq h_i$,
\begin{acl2}
(implies $q_i$ (o< $m/{\sigma_{i,j}}$ $m$)){\rm .}
\end{acl2}
\end{itemize}

In the above, ``$\tau/{\sigma}$'' represents the term or formula obtained
by applying the variable substitution $\sigma$ to the term or formula
$\tau$, uniformly replacing all free occurrences of the variables as
indicated by the substitution.

In other words, to prove $\psi$ by induction, you may assume as many
arbitrary instances of $\psi$ as you want, as long as they make some
ordinal-valued measure of the variables in $\psi$ decrease.  The key to
induction is well-foundedness and the key to well-foundedness in ACL2 is the
notion of the ordinals.  The ordinals (up to $\epsilon_{0} =
\omega^{\omega^{\omega^{\ldots}}}$) in ACL2 are recognized by the function
{\ptt{o-p}} and compared with the relation {\ptt{o<}}.  To learn more, see
{\underline{\ptt{ordinals}}}.


ACL2 also has a Definitional Principle, implemented by \ptt{defun}.  When a
function definition is submitted, ACL2 must prove ``measure conjectures''
establishing that some measure of the arguments is decreasing in a
well-founded way under the tests governing the recursion.  Operationally, the
validity of the measure conjectures ensures that the recursion terminates;
logically, it ensures that there exists a function satisfying the
definitional equation.  Only after these conjectures are proved is the
definitional equation ``admitted'' as a new axiom.  We do not deal with
termination further in this paper.

So let's prove some theorems!  Here is a function that ``copies'' a
tree.  Prove it is the identity function.

\begin{acl2p}
(defun treecopy (x)
  (if (consp x)
      (cons (treecopy (car x))
            (treecopy (cdr x)))
     x))
\end{acl2p}

{\noindent}{\bf{Theorem}} \ptt{(equal (treecopy x) x)}.

{\noindent}{\bf{Proof}}.

Name the formula above *1.

We prove *1 by induction.  One induction scheme
is suggested by this conjecture -- namely the one
that unwinds the recursion in \ptt{treecopy}.

If we let  \ptt{($\psi$ x)} denote *1 above then the
induction scheme we'll use is
\begin{acl2p}
(and (implies (not (consp x)) ($\psi$ x))
     (implies (and (consp x)
                   ($\psi$ (car x))
                   ($\psi$ (cdr x)))
              ($\psi$ x))).
\end{acl2p}
This induction is justified by the same argument used
to ``admit'' \ptt{treecopy}, namely, the size of \ptt{x}
is decreasing according a certain well-founded relation.
When applied to the goal at hand the above induction scheme
produces the following two nontautological subgoals.

\begin{acl2p}
{\rm{Subgoal *1/2}}
(implies (not (consp x))
         (equal (treecopy x) x)).
\end{acl2p}
But simplification reduces this to \ptt{t}, using the definition of
\ptt{treecopy} and the primitive axioms.

\begin{acl2p}
{\rm{Subgoal *1/1}}
(implies (and (consp x)
              (equal (treecopy (car x)) (car x))
              (equal (treecopy (cdr x)) (cdr x)))
         (equal (treecopy x) x)).
\end{acl2p}
But simplification reduces this to \ptt{t}, using the definition of
\ptt{treecopy} and the primitive axioms.

That completes the proof of *1.

{\noindent}{\bf{Q.E.D.}}

\vspace*{.1in}

Let us look more closely at the reduction of Subgoal *1/1.  Consider the
left-hand side of the concluding equality.  Here is how it reduces to the
right-hand side under the hypotheses.
\begin{acl2p}
(treecopy x)
$=$                      {\em{\{def \ptt{treecopy}\}}}
(if (consp x)
    (cons (treecopy (car x))
          (treecopy (cdr x)))
    x)
$=$                      {\em{\{hypothesis 1 and Axiom 6\}}}
(if t
    (cons (treecopy (car x))
          (treecopy (cdr x)))
    x) 
$=$                      {\em{\{Axioms 2 and 1\}}}
(cons (treecopy (car x))
      (treecopy (cdr x)))
$=$                      {\em{\{hypothesis 2\}}}
(cons (car x)
      (treecopy (cdr x)))
$=$                      {\em{\{hypothesis 3\}}}
(cons (car x)
      (cdr x))
$=$                      {\em{\{Axiom 11 and hypothesis 1\}}}
x
\end{acl2p}

This proof is of a very routine nature: induct so as to unwind some
particular function appearing in the conjecture and then use the axioms and
definitions to simplify each case to \ptt{t}.

\vspace*{.1in}
\noindent {\bf{Exercises}}
\vspace*{.1in}

Prove each of the formulas below.  Don't use the ACL2 system!  Work out the
proofs by hand.  We want you to learn two things from these exercises: the
importance of choosing the right variable to induct upon and what it means to
simplify a formula using definitions and axioms.

\vspace*{.05in}
{\noindent}{\bf{Problem 5.1}} \ptt{(equal (app (app a b) c) (app a (app b c)))}.

\vspace*{.05in}
{\noindent}{\bf{Problem 5.2}} \ptt{(equal (dup (app a b)) (app (dup a) (dup b)))}.

\vspace*{.05in}
{\noindent}{\bf{Problem 5.3}} \ptt{(equal (dup (mapnil a)) (mapnil (dup a)))}.

\vspace*{.05in}
{\noindent}{\bf{Problem 5.4}} \ptt{(properp (app a nil))}.

\vspace*{.05in}
{\noindent}{\bf{Problem 5.5}} \ptt{(equal (swaptree (swaptree x)) x)}.

\vspace*{.05in}
{\noindent}{\bf{Problem 5.6}} 
\ptt{(equal (memp e (app a b)) (or (memp e a) (memp e b)))}.

\section{Three Basic Proof Techniques}

The proofs above are very routine -- if the right induction argument is
chosen.  Each proof has the ``induct and simplify'' structure mentioned
earlier.  The ACL2 theorem prover uses an elaboration of that same strategy.
In this section we briefly discuss three important techniques used by ACL2:
induction, rewriting, and inequality chaining (linear arithmetic).  The last
two are the key parts of the ACL2 simplifier.  The reader uninterested in the
ACL2 system should read this section anyway!  We explain why at the end.

\subsection{Induction}

The induction heuristic chooses an induction scheme based on the recursively
defined functions used in the conjecture.  Sometimes the system synthesizes a
scheme by combining two or more recursive schemes used in the formula.

Consider Problem 5.6 above,
\begin{acl2p}
(equal (memp e (app a b))
       (or (memp e a)
           (memp e b))).
\end{acl2p}
The successful proof will be by induction on \ptt{a}, i.e.,
by unwinding the recursion in \ptt{(memp e a)}.  Why not induction on \ptt{b}?
If you did the proof by hand you might have discovered that induction on
\ptt{b} doesn't work.

The basic idea is that if we induct on \ptt{a}, we get our induction
hypothesis by replacing each \ptt{a} by \ptt{(cdr a)}.  So where the
induction conclusion has an \ptt{a}, the induction hypothesis will have a
\ptt{(cdr a)}.  In particular, the terms \ptt{(memp e a)} and \ptt{(memp e
(app a b))}, in the conclusion, correspond to \ptt{(memp e (cdr a))} and
\ptt{(memp e (app (cdr a) b))} in the hypothesis.  But when we expand the
definitions of \ptt{memp} and \ptt{app} in the conclusion, those expressions
reduce to their correspondents in the hypothesis!

Now try the same induction on \ptt{b}.  Where the conclusion has \ptt{(memp e
(app a b))} the hypothesis will have \ptt{(memp e (app a (cdr b)))}.  And
there is no way we can use the definitions of \ptt{memp} and \ptt{app} to
reduce the conclusion term to the hypothesis term.  The key observation is
that the second argument of \ptt{app} is held constant in the recursion of
\ptt{app}, so inducting on it is probably a bad idea.  We say the induction
on \ptt{b} here is ``flawed.''

ACL2 uses a variety of heuristics to select an induction argument.  If the
system's chosen scheme is inappropriate, the user can specify a scheme with a
hint; see {\underline{\ptt{hints}}}.

Choosing the right induction is crucial to a successful proof.  But there
is an earlier, much more subtle step:  choosing the right theorem to try to
prove by induction!

\vspace*{.1in}
\noindent {\bf{Exercise}}
\vspace*{.1in}

{\noindent}{\bf{Problem}} Try to prove the following special case of
Problem 5.6 directly by induction: \ptt{(equal (memp e (app a a)) (mem e
a))}.

\vspace*{.1in}

If your goal is the above Problem, you will at some point have to prove
something much more general, e.g., Problem 5.6 first.

This is a particularly trivial example of a phenomenon familiar to people
trying to do inductive proofs.  In induction, your main tool is the induction
hypothesis, which is an instance of the conjecture you're trying to prove.
If the conjecture you're trying to prove is not strong enough, your
hypothesis will be useless.

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Induction
must be applied to strong theorems, not weak ones!  Always try to invent the
strongest theorems you can think of!}}
\vspace*{.1in}

By understanding the link between recursion and induction you can learn to
anticipate many problems.  The fact that \ptt{(app x y)} is defined to take the
\ptt{cdr} of \ptt{x} while holding \ptt{y} constant in the recursion is a sure
sign that if \ptt{y} is the induction variable the proof will either fail or
you will need a lemma that ``moves a \ptt{cdr} out of the second argument of
\ptt{app}'', i.e., a lemma that transforms \ptt{(app x (cdr y))} to something
involving \ptt{(app x y)} or vice versa.

\subsection{Simplification via Rewriting}

As important as induction is, the key to any successful proof is
simplification.  {\em{Simplification}} means the reduction of the formula to
some {\em{preferred form}} by the use of {\em{rules}}.  In ACL2, these rules are
derived from axioms, definitions and previously proved theorems.

The previous paragraph is incredibly important if you are going to learn to
use the ACL2 system!  You essentially {\em{program}} the ACL2 simplifier by
getting the system to prove theorems {\em{which are then turned into rules}}.
The preferred form enforced by the system is largely determined by your
rules.  All the rules ever produced in a session are available to ACL2's
simplifier, so once you have added a rule it may participate in any
subsequent proof unless you take active steps to disable it.  To use ACL2,
you must understand (a) how theorems are turned into rules, (b) what those
rules make the simplifier do, and (c) how to disable and enable rules.

There are about a dozen kinds of rules in ACL2 and when a theorem is posed,
the user specifies the kind of rule to be produced from the theorem.  See
{\underline{\ptt{rule-classes}}}.  In this document we see only three
specifications: make a rewrite rule, make a linear arithmetic rule, or make
no rule at all.  In practice, these three specifications often suffice.
The last is used when we have a theorem that cannot generate
a useful rule -- the only way such a theorem can participate in a subsequent
proof is by a user-specified hint; see {\underline{hints}}.

By far the most common form of rule is the rewrite rule.  It causes the
simplifier to replace one term by another, if certain hypotheses can be
established by rewriting.  Rewrite rules are the most direct way to program
the simplifier.

The rewrite rule derived from a formula of the form
\begin{acl2p}
(implies (and $hyp_1$ \ldots $hyp_n$) (equal $lhs$ $rhs$))
\end{acl2p}
makes the simplifier replace instances of $lhs$ (the {\bf{l}}eft-{\bf{h}}and {\bf{s}}ide) by the corresponding
instance of $rhs$, provided the corresponding instances of each of the
$hyp_i$ rewrites to true.

Equivalent logical forms may give rise to radically different rules and hence
radically different programmed behaviors!  Consider the effect of the (rule
generated from the) equivalent formula \ptt{(implies (and $hyp_1$ \ldots
$hyp_n$) (equal $rhs$ $lhs$))}.

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Give
careful thought to the ``preferred'' forms you use in your proofs and provide
yourself with lemmas that allow you, insofar as possible, to canonicalize
terms.}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{When using
the ACL2 system, {\em{never}} prove a named theorem without understanding its
effect as a rule!}}
\vspace*{.1in}

Some conventions make it possible to derive rewrite rules from a wide variety
of formulas.  The conclusion can be \ptt{(equal $lhs$ $rhs$)} or \ptt{(iff
$lhs$ $rhs$)}.  The latter kind of rule is used to replace $lhs$ by
$rhs$ in ``propositional'' settings.  ACL2 allows user-defined
equivalence relations in rewrite rules, but we do not discuss them; see
{\underline{\ptt{equivalence}}} and {\underline{\ptt{congruence}}}.  If the
conclusion, say, $concl$, is not an equivalence, it is treated as though it
were \ptt{(iff $concl$ t)}.  If there are no hypotheses, it is as though
there were just one: \ptt{t}.  See {\underline{rewrite}}.

\subsection{Simplification via Inequality Chaining}

We have not discussed arithmetic -- and we will not in this document, except
for a few important observations in this section.

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Realize
that when you are dealing with arithmetic, your sense of what is
``straightforward'' has been honed by many years of drill-and-practice
with manipulating algebraic properties of numbers.  Be prepared to
``explain'' formally why some arithmetic relations hold!}}
\vspace*{.1in}

Most of that drill-and-practice is, technically speaking, the application of
a large set of rewrite rules to put arithmetic expressions into a preferred
form.  ACL2 does not come pre-configured with those rules.  But they are
available in several different collections.  In ACL2 a collection of rules in
a file is called a ``book.''  The ACL2 distribution comes with several
arithmetic books and the community is constantly working on improving them.
That is one of the reasons we have several such books now.  Another is that
different books are designed for different kinds of problems: elementary
algebraic properties of numbers, modulo arithmetic, floating point
arithmetic.  See the \ptt{README.html} file in the \ptt{books} subdirectory
of your ACL2 source directory, or else visit the Mathematical Tools link on
the ACL2 home page.

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{If you are
doing arithmetic proofs with ACL2, start by including
one of the arithmetic books into your script.  The most
commonly used book is included by adding the command
\ptt{(include-book "arithmetic/top-with-meta" :dir :system)}.}}
\vspace*{.1in}

Finally, you should be aware that often in arithmetic reasoning you
do a kind a inequality chaining that ``feels'' like rewriting but is
not.

Consider a theorem that concludes with an arithmetic inequality, such as
\ptt{(<= 0 (* x x))}.  This says ``x squared is nonnegative.'' \footnote{This
is not always true: \ptt{x} may be complex.  But we're imagining this
inequality as the conclusion of a suitable implication.}  If it is used to
generate a rewrite rule, the rule will replace certain instances of \ptt{(<=
0 (* x x))} by \ptt{t}.  This does not help us much if we are trying to prove
that \ptt{(+ a (* b b))} is positive when \ptt{a} is positive.  But ACL2
maintains a graph of terms involved in the current conjecture and relates the
terms in this graph with inequalities.  It contains a decision procedure for
answering questions about linear arithmetic -- the fragment of arithmetic
consisting of inequalities, addition, and multiplication by constants --
based on the property that inequalities can be added.  People sometimes call
this ``inequality chaining.''  Such chaining can be used to derive \ptt{(<= 0
(+ a (* b b)))} from \ptt{(<= 0 a)} and \ptt{(<= 0 (* b b))}.  But if we are
trying to prove
\begin{acl2p}
(implies (and (<= 0 a) (rationalp b)) (<= 0 (+ a (* b b))))
\end{acl2p}
the graph contains no node for \ptt{(* b b)} -- because that term is not
compared to any other term -- and no chaining is possible.  However, if the
rule above about \ptt{(<= 0 (* x x))}
is available as a linear arithmetic rule instead of as a rewrite
rule it causes the following behavior: whenever an instance of \ptt{(* $x$
$x$)} enters the problem, the inequality graph is extended with a node for
the corresponding instance and it is linked to other nodes as described by
the conclusion of the linear rule.  This extends range of the chaining
decision procedure.  See {\underline{\ptt{linear-arithmetic}}}.

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Realize
that when you are dealing with arithmetic you may be doing inequality chaining,
not replacement of equals by equals, and make that form of reasoning explicit
in your notation.}}
\vspace*{.1in}

This discussion of rewrite versus linear rules is of general interest because
{\em{most mathematical facts have implicit operational import}}.  This
discussion illustrates that.  When you discover a new fact, what do you do
with it?  Do you store it, unanalyzed, in a long list of things you know and
revisit them all every time you are asked to prove something?  Or do you see
ways you can use and remember the new fact?  This is a difficult
introspective question to answer -- and the answer is probably ``some of
each'' -- but it is important to remember that many years of secondary school
and college mathematics have taught you how to use certain forms of facts,
e.g., associativity, commutativity, identities, idempotence, inequality
chaining, cancellation, etc.

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Every time you encounter
a new theorem you should give thought to how it is to be used in subsequent
proofs.}}
\vspace*{.1in}

\subsection{Some ACL2-Specific Details}

The rest of this section is mainly of interest to potential ACL2 users, but
contains a few useful hints of more general interest.

To prove a named theorem with ACL2, use \ptt{(defthm $name$ $term$)} if you
want $term$ used as a rewrite rule.  Use \ptt{(defthm $name$ $term$
:rule-classes :linear)} if you want $term$ used to extend the linear
arithmetic inequality graph.  This is possible only if $term$ is an
arithmetic inequality, i.e., \ptt{(< $lhs$ $rhs$)}, \ptt{(<= $lhs$ $rhs$)},
\ptt{(>= $lhs$ $rhs$)}, \ptt{(> $lhs$ $rhs$)}, \ptt{(equal $lhs$ $rhs$)}, or
\ptt{(not (equal $lhs$ $rhs$))}, where, for the last two, $lhs$ and $rhs$ are
numerically valued expressions.  If you want no rule generated from $term$,
use \ptt{(defthm $name$ $term$ :rule-classes nil)}.

Note carefully: if you just use the simple form of \ptt{defthm} to prove a
named theorem, you are telling ACL2 to use it as a rewrite rule!

If you need to supply hints to the theorem prover, use the optional
\ptt{:hints} ``keyword argument,'' e.g., write
\begin{acl2p}
(defthm $name$ $term$ :hints $hints$)
\end{acl2p}
or
\begin{acl2p}
(defthm $name$ $term$
   :hints $hints$
   :rule-classes $classes$).
\end{acl2p}.
See {\underline{\ptt{hints}}}.

Finally, if you have proved a rule named $name$ and want to disable it
so that ACL2 no longer considers applying it, use
\ptt{(in-theory (disable $name$))}.  To undo that, use \ptt{(in-theory
(enable $name$))}.  It is possible to collect groups of names together so as
to enable and disable them in concert.  Each such group represents a
strategy.  See {\underline{\ptt{theories}}}.

The command
\begin{acl2p}
(defthm app-right-identity
  (implies (properp x) (equal (app x nil) x)))
\end{acl2p}
commands ACL2 to prove the formula named \ptt{app-right-identity} and store
it as a rewrite rule if the proof is successful.  The rule generated rewrites
instances of \ptt{(app x nil)}.  After \ptt{app-right-identity} has been
proved, if the simplifier encounters a target term like \ptt{(app (rev (app a
b)) nil)} it will try the rule, because the target matches (is an instance
of) \ptt{(app x nil)}.  The substitution produced by the matching process
binds the variable symbol \ptt{x}, from the rule, to \ptt{(rev (app a b))},
from the target.  To apply the rule, the simplifier considers the
``corresponding instance'' of \ptt{(properp x)}, namely \ptt{(properp (rev
(app a b)))}.  It tries to rewrite this to true.  If it can, it will replace
the target by the ``corresponding instance'' of the right-hand side from the
rule.  Thus, it will replace the target by \ptt{(rev (app a b))}.

Consider what would happen if you proved a rule that rewrites $lhs$ to $rhs$
and another rule that rewrites $rhs$ to $lhs$.  More complicated cycles are
more likely, of course.  ACL2 has special heuristics for handling
commutativity and similarly simple permutative rules.  But in general ACL2's
simplifier can be made to loop forever by programming it with circular rules.
Such behavior will generally be reported by the simplifier together with
instructions for how to debug the failure.

\vspace*{.1in} {\noindent}{\bf{Hint on How To Prove Things:}} {\em{Ensure
that your rules do not loop!  One way to do this is to keep in mind some
ordering on your preferred terms and be sure that the right-hand side of each
rule is lower in this ordering than the left-hand side.}}
\vspace*{.1in}

You may sometimes wish to interrupt the theorem prover, e.g., because of a
``runaway proof.''  To interrupt the ACL2 prover while using it under Emacs, type
\ptt{ctrl-c ctrl-c}.  This will leave you in a Common Lisp (not ACL2!)
read-eval-print break.  To this break you should type the command that aborts
an interrupted Common Lisp computation.  That command varies according to
your host Lisp.  If you are running GCL, type \ptt{:q} followed by
\ptt{enter}; if you are running Allegro, type \ptt{:reset} followed by
\ptt{enter}; if you are running CMU CL, type \ptt{q}, followed by
\ptt{enter}; if you are running MCL, type \ptt{:pop}.

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}}
{\em{Definitions are (generally) used as expansion rules, i.e., function
calls are replaced by their instantiated bodies.  This imposes a restriction
on your choice of preferred forms: function bodies are preferable to function
calls.  If you want to override that built-in preference in ACL2, you should
disable the functions after proving the rules you need about them.}}
\vspace*{.1in}

You might wonder how ACL2 can replace function calls by their bodies and not
loop indefinitely on recursive definitions.  The answer is that ACL2 contains
heuristics for controlling the expansion of recursive definitions.  These
heuristics generally do a good job and most users find it better to arrange
their rewrite rules to be compatible with these heuristics than to fight the
heuristics.

To simplify a formula, the ACL2 simplifier rewrites the formula from
left-to-right and inside-out.  Thus, a rule with the left-hand side \ptt{(foo
(car (cons x y)))} will {\em{never}} be applied!  Why?  The only possible
target term for this problematic rule is of the form \ptt{(foo (car (cons
$\alpha$ $\beta$)))}.  But the ACL2 simplifier sweeps inside-out, so the
problematic rule is not tried until the interior terms of the target have
been rewritten.  Given the rule that reduces \ptt{(car (cons x y))} to
\ptt{x} (which is derived from primitive Axiom 9 of Figure \ref{primaxs}),
the target will have been transformed to \ptt{(foo $\alpha$)} before the
problematic rule is tried.  It will therefore fail to match.

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{When
designing your rewrite rules, be sure the left-hand sides are in your
preferred form!}}
\vspace*{.1in}

\section{ACL2's Proof Strategy}

Rather than ``induct and simplify,'' ACL2's strategy is ``simplify (and some
other things), induct and repeat.''  The reason ACL2's strategy looks like
``induct and simplify'' is that, often, the initial simplification does not
change the goal formula so it looks like ACL2 immediately went to induction.
Some theorems are proved by the initial simplification and no induction is
used.  It is possible to program ACL2's simplifier so that almost every proof
that ACL2 can do can be put into the ``simplify, induct and simplify'' form,
by proving appropriate lemmas first.  We recommend that new users concentrate
on producing proofs in that form.

\vspace*{.1in} {\noindent}{\bf{Hint on How To Prove Things:}} {\em{Keep your
proofs in the ``simplify, induct, simplify'' form.  That is, identify each
inductively proved lemma you need in a proof, write it down, and give it
a name.  Do not get into the habit of letting the ACL2 prover invent and inductively prove
lemmas ``on the fly'' in the middle of other proofs.  It is better that you
understand and control the lemma decomposition of your theorems.}}
\vspace*{.1in}


\vspace*{.1in}
\noindent {\bf{Exercise}}
\vspace*{.1in}

{\noindent}{\bf{Problem 7.1}}  Run the ACL2 theorem prover on each of
Problems 5.1 -- 5.6.  

\vspace*{.1in}

You will find that ACL2's strategy finds proofs for each of these
automatically -- at least if you defined the various functions the way we
did.  See Appendix \ref{alldefs}.

Here is the output produced by ACL2 Version 2.8 on Problem 4.6.  The first
form is our input, typed as a \ptt{defthm} command at the ACL2 prompt.  Note
that ACL2's initial simplification splits the conjecture into two parts,
\ptt{Subgoal 2} and \ptt{Subgoal 1}, according to whether \ptt{(memp e a)}.
Upon exploring the proof space a little further, ACL2 learns it will have to
tackle both by induction.  It then discards the simplification work, backs up
to the original theorem, and sets up an induction argument on that
instead.\footnote{In general, the original theorem is stronger than any
single special case of it and is often the better theorem to try by
induction.  In this particular case, the two subgoals are each strong enough
to be inductively provable.}

It uses \ptt{:p} to represent the theorem schematically, where we used $\psi$
above.  Its induction argument has two base cases; \ptt{Subgoal *1/3} handles
the case when \ptt{a} is not a \ptt{consp}; \ptt{Subgoal *1/1} handles the
case when \ptt{a} is a \ptt{consp} but its first element is \ptt{e}.  This is
the induction scheme necessary to unwind \ptt{(mem e a)}.

ACL2 prints terms in uppercase.  We have lowered the case below to keep the
typography consistent with this paper.  In the subset of ACL2 used in this
paper, Lisp is case insensitive except for string constants.

{\small{
\begin{verbatim}
ACL2 !>(defthm memp-app
         (equal (memp e (app a b))
                (or (memp e a) (memp e b))))

This simplifies, using the :type-prescription rule memp,
to the following two conjectures.

Subgoal 2
(implies (memp e a)
         (equal (memp e (app a b)) t)).

This simplifies, using primitive type reasoning and the
:type-prescription rule memp, to

Subgoal 2'
(implies (memp e a) (memp e (app a b))).

Name the formula above *1.

Subgoal 1
(implies (not (memp e a))
         (equal (memp e (app a b)) (memp e b))).

Normally we would attempt to prove this formula by induction.
However, we prefer in this instance to focus on the original
input conjecture rather than this simplified special case.
We therefore abandon our previous work on this conjecture
and reassign the name *1 to the original conjecture. 
(See :DOC otf-flg.)

Perhaps we can prove *1 by induction.  Four induction
schemes are suggested by this conjecture.  Subsumption
reduces that number to three.  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 (memp e a),
but modified to accommodate (app a b).  These suggestions
were produced using the :induction rules app and memp.
If we let  (:p a b e) denote *1 above then the induction
scheme we'll use is
(and (implies (not (consp a)) (:p a b e))
     (implies (and (consp a)
                   (not (equal e (car a)))
                   (:p (cdr a) b e))
              (:p a b e))
     (implies (and (consp a) (equal e (car a)))
              (:p a b e))).
This induction is justified by the same argument used
to admit memp, namely, the measure (acl2-count a) 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 three nontautological subgoals.

Subgoal *1/3
(implies (not (consp a))
         (equal (memp e (app a b))
                (or (memp e a) (memp e b)))).

But simplification reduces this to t, using the :definitions
app and memp and primitive type reasoning.

Subgoal *1/2
(implies (and (consp a)
              (not (equal e (car a)))
              (equal (memp e (app (cdr a) b))
                     (or (memp e (cdr a)) (memp e b))))
         (equal (memp e (app a b))
                (or (memp e a) (memp e b)))).

But simplification reduces this to t, using the :definitions
app and memp, the :executable-counterpart of equal, primitive
type reasoning, the :rewrite rules car-cons and cdr-cons
and the :type-prescription rule memp.

Subgoal *1/1
(implies (and (consp a) (equal e (car a)))
         (equal (memp e (app a b))
                (or (memp e a) (memp e b)))).

But simplification reduces this to t, using the :definitions
app and memp, the :executable-counterpart of equal, primitive
type reasoning and the :rewrite rule car-cons.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( defthm memp-app ...)
Rules: ((:definition app)
        (:definition memp)
        (:executable-counterpart equal)
        (:fake-rune-for-type-set nil)
        (:induction app)
        (:induction memp)
        (:rewrite car-cons)
        (:rewrite cdr-cons)
        (:type-prescription memp))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
 memp-app
ACL2 !>
\end{verbatim}}}

\section{Decomposition into Lemmas -- The Method}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{When
considering a new conjecture to prove, look for general theorems that can be
used to prove it by simplification -- rewriting and chaining -- before you consider
proving it by induction.}}
\vspace*{.1in}

This is probably the most important, and most vague, advice we have.  We
illustrate it below by proving a little theorem.  In our illustration, we use
the ACL2 theorem prover to do a lot of the work for us, but the general
principles apply whenever you are doing an ``induct and simplify'' proof.
The specific output we display was produced by ACL2 Version 2.8 after
defining the functions and proving the theorems in the exercises above.

Let us prove \ptt{(equal (rev (rev (rev x))) (rev x))}.  We call this theorem
``triple \ptt{rev}.''  What more general fact does it suggest?

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Look for
pairs of adjacent function symbols and try to think of rules that simplify
those expressions.}}
\vspace*{.1in}

You have probably thought of the conjecture \ptt{(equal (rev (rev z)) z)}.
But is \ptt{(equal (rev (rev z)) z)} a theorem?  Is it always true?  Consider
the possibility that \ptt{z} is \ptt{7}.  The left-hand side computes to
\ptt{nil} but the right-hand side is \ptt{7}.  So this is not a theorem.  We
might then restrict \ptt{z} to satisfy \ptt{consp}.  But would that be a
theorem?  Consider the case when \ptt{z} is \ptt{'(1 . 7)}.  The left-hand
side is \ptt{(1)} and the right-hand side is \ptt{(1 . 7)}.  

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{When
forming new conjectures, test them on constants.}}
\vspace*{.1in}

Since ACL2 is a programming language, you can usually run your conjectures on
a few examples.  One could type \ptt{(let ((x '(1 . 7))) (equal (rev (rev x))
x))} to run the second test above; the result is \ptt{nil}.  We often do
{\ptt{:set-guard-checking nil}} when we are running tests, so that ACL2 does
not reject the test simply because it violates the implicit type constraints
on Lisp primitives.  See {\underline{\ptt{set-guard-checking}}}.

Consider for a moment the expected input to \ptt{rev}.  \ptt{Rev} \ptt{cdr}s
down its argument until it is no longer a \ptt{consp} and then claims its
reverse is \ptt{nil}.  Implicitly then, \ptt{rev} ``expects'' its argument to
be a proper list.  Thus, the first part of our attack on the triple \ptt{rev}
problem is to prove:
\begin{acl2p}
(defthm rev-rev
  (implies (properp z)
           (equal (rev (rev z)) z)))
\end{acl2p}
In a fully-typed language, we might not need the explicit hypothesis that
\ptt{z} is a proper list.  But we are in an untyped language and must make
these restrictions explicit.

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Often you
will have to invent new concepts -- concepts not involved in your main
theorem -- to state the lemmas you need.}}
\vspace*{.1in}

It is surprising how often people resist adding a new definition, even of a
concept they clearly have in mind.  If you restrict your predicates to
things like \ptt{consp}, there is no way you can state an inductively
provable version of \ptt{(equal (rev (rev x)) x)}.  You have to introduce the
new concept of ``proper list'' to state the theorem.

Suppose we had proved \ptt{rev-rev}.  Could we prove the triple \ptt{rev}
theorem?  Answer:  Not unless we knew the following.
\begin{acl2p}
(defthm properp-rev
  (properp (rev x)))
\end{acl2p}

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{If you
have introduced hypotheses in your lemmas, be sure you prove that the
appropriate terms satisfy those hypotheses.}}
\vspace*{.1in}

Is the \ptt{properp-rev} conjecture true?  Does \ptt{rev} always return a
proper list, even when its input is improper?  Yes!  Because it either
returns \ptt{nil} or a list it produces by appending a proper list (a
singleton list) to the right of the recursively produced answer.  So here is
a theorem, \ptt{properp-rev}, that is stronger than we might have produced in a strongly typed
language, i.e., there is no restriction that \ptt{x} be proper.

Thus, we have designed the following proof script:
\begin{acl2p}
; --- Script for proving triple-rev ---
(defthm rev-rev
  (implies (properp z)
           (equal (rev (rev z)) z)))

(defthm properp-rev
  (properp (rev x)))

(defthm triple-rev
  (equal (rev (rev (rev a))) (rev a)))
; --- The End ---
\end{acl2p}

This plan illustrates an important adage:

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Separate your
concerns!}}
\vspace*{.1in}

In the triple \ptt{rev} problem, the concept of \ptt{properp} neatly divides
the problem.  We first prove that the composition of two \ptt{rev}s is the
identity {\em{on proper lists}}.  We then prove that \ptt{(rev a)} is a
proper list.  To separate the two parts of the problem we had to think of the
idea of a proper list.  Notice that this is not only a nice plan for proving
the triple \ptt{rev} theorem but it leaves us in excellent shape to prove
other theorems, like \ptt{(equal (rev (rev (dup a))) (dup a))}, where all we
have to do is prove that \ptt{dup} returns a proper list.

No further decomposition of our plan comes to mind, so now let us prove the
first one inductively.  What we are doing is following our method of using
the \ptt{script} buffer, with the ``cursor'' positioned just before the
\ptt{rev-rev} theorem.  When we submit the \ptt{rev-rev} event, a successful
proof description flashes by.  We cannot read it as it flashes by, but the
final two lines are:
\begin{acl2p}
Time:  0.03 seconds (prove: 0.02, print: 0.01, other: 0.00)
 REV-REV
\end{acl2p}
whereas the final line in a failed proof is always
\begin{acl2p}
*** FAILED *** See :DOC failure *** FAILED ***
\end{acl2p}

This success may appear to be good news, but a few lines above the
successful conclusion are the lines
{\small{
\begin{acl2p}
That completes the proofs of *1.1 and *1.

Q.E.D.
\end{acl2p}}}
which tell the informed reader that ACL2 did (at least) a second induction
(to prove \ptt{*1.1}) and so the proof is at least of the form ``induct,
simplify, induct, simplify.''  We don't know what intermediate lemma ACL2
discovered and proved, but we know it used induction twice in this proof!
Since we recommend that novices stick to the ``simplify, induct, simplify''
strategy, you should undo the newly proved theorem -- remember, it has just
added a rule to ACL2 database! -- with \ptt{:u} (see {\underline{\ptt{u}}},
{\underline{\ptt{ubt}}}, {\underline{\ptt{pbt}}}) and then read the generated
proof script {\em{from the top down}}.

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{We
recommend that the novice ACL2 user not rely on ACL2's creative contributions
in the beginning.  As the problems become harder, ACL2's creative
contributions count for less and less -- and its ability to carry out massive
automatic simplifications using user-specified rules counts for more and
more.  So the novice is encouraged to learn to spot the need for rules and to
program ACL2 to use them.}}
\vspace*{.1in}

Here is the first part of ACL2's proof attempt on \ptt{rev-rev}.  Read
it, just as you would a human-generated proof sketch.
{\small{
\begin{verbatim}
ACL2 !>(defthm rev-rev
         (implies (properp z)
                  (equal (rev (rev z)) z)))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Two induction schemes
are suggested by this conjecture.  Subsumption reduces
that number to one.  

We will induct according to a scheme suggested by (rev z).
This suggestion was produced using the :induction rules
properp and rev.  If we let  (:p z) denote *1 above then
the induction scheme we'll use is
(and (implies (not (consp z)) (:p z))
     (implies (and (consp z) (:p (cdr z)))
              (:p z))).
This induction is justified by the same argument used
to admit rev, namely, the measure (acl2-count z) 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 three nontautological subgoals.

Subgoal *1/3
(implies (and (not (consp z)) (properp z))
         (equal (rev (rev z)) z)).

But simplification reduces this to t, using the :definition
properp, the :executable-counterparts of consp, equal
and rev and primitive type reasoning.

Subgoal *1/2
(implies (and (consp z)
              (equal (rev (rev (cdr z))) (cdr z))
              (properp z))
         (equal (rev (rev z)) z)).

This simplifies, using the :definitions properp and rev,
to

Subgoal *1/2'
(implies (and (consp z)
              (equal (rev (rev (cdr z))) (cdr z))
              (properp (cdr z)))
         (equal (rev (app (rev (cdr z)) (list (car z))))
                z)).

The destructor terms (car z) and (cdr z) can be eliminated
by using car-cdr-elim to replace z by (cons z1 z2), (car z)
by z1 and (cdr z) by z2.  This produces the following
goal.
\end{verbatim}}}

The step after {\ptt{Subgoal *1/2'}} is not a simplification, so the proof
does not have the ``simplify, induct, simplify'' form we recommend for
novices.  In particular, {\ptt{Subgoal *1/2'}} is the first formula after the
induction that was not proved by simplification.  We call this formula a
checkpoint.  Learn to recognize them!

There are two main kinds of checkpoint formulas.  The first is any formula
proved by induction.  In reading ACL2 output, we avoid reading past an induction
without asking ourselves whether the formula being proved ``needs'' to be
proved by induction and whether the selected induction is appropriate for it.

The other kind of checkpoint formula is the first formula after an induction
that is not proved by repeated simplification.  That is the case for
\ptt{Subgoal *1/2'} above.

There is an Emacs utility that will automatically take you to the checkpoints
of a proof attempt; see {\underline{\ptt{proof-tree}}}.

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Whenever a
proof fails (or you want to reduce a proof to the recommended form), read the
formula at the first checkpoint and look for a lemma decomposition.
Sometimes, it helps to read a few formulas past the first checkpoint --
often ACL2's heuristics come fairly close to generating the needed lemma,
or at least creating a term that will suggest the lemma to you.  So if
the checkpoint does not suggest anything, read on.}}
\vspace*{.1in}

What lemma is suggested by the checkpoint formula?
\begin{acl2p}
Subgoal *1/2'
(implies (and (consp z)
              (equal (rev (rev (cdr z))) (cdr z))
              (properp (cdr z)))
         (equal (rev (app (rev (cdr z)) (list (car z))))
                z)).
\end{acl2p}

Recall an earlier Hint on How To Prove Things: {\em{Look for pairs of adjacent
function symbols and try to think of rules that simplify those expressions.}}
We see a subterm of the above checkpoint formula that has the form
\ptt{(rev (app ...))}.  Note that in the checkpoint formula, if we could
move that outer \ptt{rev} past the \ptt{app} so
that it nestles around the inner \ptt{rev}, we will have reproduced the
induction hypothesis term, \ptt{(rev (rev (cdr z)))} and could use our
induction hypothesis!

So what is a lemma that simplifies \ptt{(rev (app a b))}?  And, if you care to
use the ``Note'' just above, you could ask yourself:
What is a lemma that relates \ptt{(rev (app a b))} to \ptt{(rev a)}?
Some thought, and perhaps some testing, produces the beautiful lemma:
\begin{acl2p}
(defthm rev-app
  (equal (rev (app a b)) (app (rev b) (rev a))))
\end{acl2p}
Add this form to the \ptt{script} buffer, just in front of \ptt{rev-rev},
and repeat.

This proof fails, and the checkpoint formula is
\begin{acl2p}
Subgoal *1/2'
(implies (not (consp a))
         (equal (rev b) (app (rev b) nil))).
\end{acl2p}
What does this suggest?  Remember the hints on how to prove things!

The lemma suggested is that \ptt{nil} is a right identity for \ptt{app}.
But of course it is not quite!  It is a right identity for proper lists.
\begin{acl2p}
(defthm app-right-identity
  (implies (properp x)
           (equal (app x nil) x)))
\end{acl2p}
But to use this theorem we must also know that \ptt{(rev b)}, from
\ptt{Subgoal *1/2'}, is proper.  We've already posed that theorem in
our \ptt{script} -- we needed it for our proof sketch of \ptt{triple-rev} --
and so we move it forward in our \ptt{script}.\footnote{This fact, that lemmas
invented for one proof may actually be useful in earlier proofs, is
one of the reasons it is hard to build a rigid interface that enforces
some kind of stack of proof plans:  evolving plans can cause non-local
rearrangements.}

So now our \ptt{script} looks like this and we are still at the top!

\begin{acl2p}
; --- Script for proving triple-rev ---
(defthm app-right-identity
  (implies (properp x)
           (equal (app x nil) x)))

(defthm properp-rev
  (properp (rev x)))

(defthm rev-app
  (equal (rev (app a b))
         (app (rev b) (rev a))))

(defthm rev-rev
  (implies (properp z)
           (equal (rev (rev z)) z)))

(defthm triple-rev
  (equal (rev (rev (rev a))) (rev a)))
; --- The End ---
\end{acl2p}

When we submit \ptt{properp-rev} it succeeds but we see the line
that means multiple inductions were used:
\begin{acl2p}
That completes the proofs of *1.1 and *1.
\end{acl2p}
so we undo with \ptt{:u} and read the checkpoint.

\begin{acl2p}
Subgoal *1/1'
(implies (and (consp x) (properp (rev (cdr x))))
         (properp (app (rev (cdr x)) (list (car x)))))
\end{acl2p}

The pair of function symbols that leap out now are \ptt{properp} and
\ptt{app}.  Note that this is an instance of our advice about proving
rules to simplify terms involving pairs of adjacent function symbols.
Under what conditions is \ptt{(properp (app a b))} true?  It depends on
whether \ptt{(properp b)} is true.  This suggests \ptt{(implies (properp b)
(properp (app a b)))}.  But that is a fairly weak theorem and as a rewrite
rule it means: whenever you see \ptt{(properp (app a b))} backchain to
\ptt{(properp b)} and if you can establish it, rewrite the target to \ptt{t}.
Can we do better?

Yes!  Consider the theorem
\begin{acl2p}
(defthm properp-app
  (equal (properp (app a b))
         (properp b)))
\end{acl2p}
This is stronger than the mere implication.  Furthermore, it is indeed a theorem!
The rule generated from it allows the unconditional elimination of
\ptt{(properp (app a b))} in favor of the simpler \ptt{(properp b)}.
 
So we change our \ptt{script} again to what is shown below.  This time, every
successive form in it is processed successfully in the ``simplify, induct,
simplify'' strategy.

{\small{
\begin{acl2p}
; --- Script for proving triple-rev ---
(defthm properp-app
  (equal (properp (app a b))
         (properp b)))

(defthm app-right-identity
  (implies (properp x)
           (equal (app x nil) x)))

(defthm properp-rev
  (properp (rev x)))

(defthm rev-app
  (equal (rev (app a b))
         (app (rev b) (rev a))))

(defthm rev-rev
  (implies (properp z)
           (equal (rev (rev z)) z)))

(defthm triple-rev
  (equal (rev (rev (rev a))) (rev a)))
; --- The End ---
\end{acl2p}}}

The last proof above consists of a single simplification, just as
we planned.
{\small{
\begin{verbatim}
ACL2 !>(defthm triple-rev
         (equal (rev (rev (rev a))) (rev a)))

But simplification reduces this to t, using primitive
type reasoning and the :rewrite rules properp-rev and
rev-rev.

Q.E.D.

Summary
Form:  ( defthm triple-rev ...)
Rules: ((:fake-rune-for-type-set nil)
        (:rewrite properp-rev)
        (:rewrite rev-rev))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 triple-rev
\end{verbatim}}}

However, if we look one more time at the proof output, we again see the line
that means multiple inductions were used
\begin{acl2p}
That completes the proofs of *1.1 and *1.
\end{acl2p}
--- this time in the proof of \ptt{rev-app}.  So we undo with \ptt{:u} and read
the checkpoint.
\begin{verbatim}
Subgoal *1/1'
(implies (and (consp a)
              (equal (rev (app (cdr a) b))
                     (app (rev b) (rev (cdr a)))))
         (equal (app (rev (app (cdr a) b))
                     (list (car a)))
                (app (rev b)
                     (app (rev (cdr a)) (list (car a)))))).

The destructor terms (CAR A) and (CDR A) can be eliminated by
using CAR-CDR-ELIM to replace A by (CONS A1 A2), (CAR A) by A1
and (CDR A) by A2.  This produces the following goal.
\end{verbatim}
This time, no rules occur to us that would further the simplification process,
so we allow the theorem prover to use destructor elimination, and read further
to see if any subgoals suggest a rule that can avoid multiple inductions.
\begin{verbatim}
Subgoal *1/1'5'
(equal (app (app rv0 rv) (list a1))
       (app rv0 (app rv (list a1)))).

Name the formula above *1.1.
\end{verbatim}
We can now will discover a lemma stating that \ptt{app} is an associative
operation, shown as lemma \ptt{app-assoc} below.  With this addition, the proof
succeeds without multiple inductions.

{\small{
\begin{acl2p}
; --- Script for proving triple-rev ---
(defthm properp-app
  (equal (properp (app a b))
         (properp b)))

(defthm app-right-identity
  (implies (properp x)
           (equal (app x nil) x)))

(defthm properp-rev
  (properp (rev x)))

(defthm app-assoc
  (equal (app (app a b) c)
         (app a (app b c))))

(defthm rev-app
  (equal (rev (app a b))
         (app (rev b) (rev a))))

(defthm rev-rev
  (implies (properp z)
           (equal (rev (rev z)) z)))

(defthm triple-rev
  (equal (rev (rev (rev a))) (rev a)))
; --- The End ---
\end{acl2p}}}

Note that one side-effect of our recommended reliance on ``simplify, induct,
simplify'' is that it causes us to think about the general rules for
manipulating the function symbols of the problem and to state them as lemmas.
Had we relied on ACL2's creative contributions, we would not have identified
so many good rules about \ptt{rev}, \ptt{app}, and \ptt{properp}.

Note also that since the final theorem is proved by rewriting with two
existing rules, there is no need to enshrine \ptt{triple-rev} as a rule
itself.  Our subsequent rule library is a little smaller if we change the
last form in the script to
{\small{
\begin{acl2p}
(defthm triple-rev
  (equal (rev (rev (rev a))) (rev a))
  :rule-classes nil)
\end{acl2p}}}

The general procedure we have just described is called ``The Method'' in
\cite{kmm00a} and described in the documentation for
{\underline{\ptt{The-Method}}}.

\vspace*{.1in}
\noindent {\bf{Exercises}}
\vspace*{.1in}

Use The Method to find proofs for each of the theorems below using ACL2.

\vspace*{.05in}
{\noindent}{\bf{Problem 8.1}}
\begin{acl2p}
(implies (memp e c)
         (memp e (rev (dup (dup c))))
\end{acl2p}

\vspace*{.05in}
{\noindent}{\bf{Problem 8.2}}
\begin{acl2p}
(equal (leaves (swaptree x))
       (rev (leaves x)))
\end{acl2p}
where \ptt{leaves} is defined as
\begin{acl2p}
(defun leaves (x)
  (if (consp x)
      (app (leaves (car x)) (leaves (cdr x)))
      (cons x nil)))
\end{acl2p}

\vspace*{.05in}
{\noindent}{\bf{Problem 8.3}}
\begin{acl2p}
(subp x x)
\end{acl2p}

\vspace*{.05in}
{\noindent}{\bf{Problem 8.4}}
\begin{acl2p}
(implies (properp x)
         (equal (int x x) x))
\end{acl2p}

\vspace*{.05in}
{\noindent}{\bf{Problem 8.5}}
\begin{acl2p}
(implies (and (subp x y)
              (subp y z))
         (subp x z))
\end{acl2p}

\vspace*{.05in}
{\noindent}{\bf{Problem 8.6}}
\begin{acl2p}
(subp (app a a) a)
\end{acl2p}

\vspace*{.05in}
{\noindent}{\bf{Problem 8.7}}
\begin{acl2p}
(seteqp (rev a) a)
\end{acl2p}
where \ptt{seteqp} (``set equality'') is defined as
\begin{acl2p}
(defun seteqp (x y)
  (and (subp x y)
       (subp y x)))
\end{acl2p}
Note: Note that after proving that \ptt{(rev a)} is set-equivalent to \ptt{a}
there is a natural expectation that ACL2 will replace \ptt{(rev a)} by
\ptt{a} where ever it sees it used as a set.  But \ptt{seteqp} is not
\ptt{equal}!  But ACL2 supports the introduction of user-defined equivalence
rules and the kind of generalized rewriting just hinted at.  See
{\underline{\ptt{equivalence}}} and {\underline{\ptt{congruence}}}.


\vspace*{.05in}
{\noindent}{\bf{Problem 8.8}}
\begin{acl2p}
(seteqp (app a b) (app b a))
\end{acl2p}

\vspace*{.05in}
{\noindent}{\bf{Problem 8.9}}
\begin{acl2p}
(equal (leaves (leaves x)) (app (leaves x) '(nil)))
\end{acl2p}

\vspace*{.05in}
{\noindent}{\bf{Problem 8.10}}
\begin{acl2p}
(iff (memp e (lonesomes x))
     (and (memp e (leaves x))
          (lonesomep e (leaves x))))
\end{acl2p}

\vspace*{.05in}
{\noindent}{\bf{Problem 8.11}}
\begin{acl2p}
(equal (raise b (add i j))
       (mult (raise b i) (raise b j)))
\end{acl2p}
where \ptt{add}, \ptt{mult}, and \ptt{raise} are defined to be list-based
analogues of addition, multiplication, and exponentiation.  In this
analogical setting, numbers (recognized by \ptt{nump}) are represented by
lists of \ptt{nil}s of the appropriate length.  Of course, ACL2 supports
arithmetic but by simulating it in these exercises we force you to invent a
lot of lemmas!

\begin{acl2p}
(defun nump (x)
  (if (consp x)
      (and (equal (car x) nil)
           (nump (cdr x)))
    (equal x nil)))

(defun add (x y)
  (if (consp x)
      (cons nil (add (cdr x) y))
    (mapnil y)))

(defun mult (x y)
  (if (consp x)
      (add y (mult (cdr x) y))
    nil))

(defun raise (x y)
  (if (consp y)
      (mult x (raise x (cdr y)))
    '(nil)))
\end{acl2p}

\vspace*{.05in}
{\noindent}{\bf{Problem 8.12}}
\begin{acl2p}
(defthm add-commutativity
  (equal (add i j) (add j i)))
\end{acl2p}

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{When you know a
function is commutative, use that fact to arrange the arguments in
some canonical order.  Thus, if \ptt{add} is known to be commutative,
then whenever you see \ptt{(add b a)}, rewrite it to \ptt{(add a b)}.
But do not use the rule the other way -- to move things out of order --
or you will loop forever!  ACL2 uses this heuristic and uses a
lexicographic ordering on terms.}}
\vspace*{.1in}

{\noindent}{\bf{Problem 8.13}}
\begin{acl2p}
(defthm add-commutativity2
  (equal (add i (add j k)) (add j (add i k))))
\end{acl2p}

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{The heuristic
advice about commutative functions does not help you if you are rewriting
\ptt{(add b (add a c))} because the ordering (probably) will not
prefer \ptt{(add a c)} over \ptt{b}.  But the theorem above,
which we call a ``commutativity2'' theorem, allows an appropriate swap
and ACL2 uses such theorems to arrange the ordering of terms.
Given associativity, commutativity, commutativity2, and these heuristics,
you can arrange nests of such functions into right-associated form
with the arguments ascending in the order.  That is what ACL2 does.}}
\vspace*{.1in}

{\noindent}{\bf{Problem 8.14}}
\begin{acl2p}
(defthm mult-commutativity
  (equal (mult i j) (mult j i)))
\end{acl2p}

\vspace*{.05in}
{\noindent}{\bf{Problem 8.15}}
\begin{acl2p}
(defthm mult-commutativity2
  (equal (mult i (mult j k)) (mult j (mult i k))))
\end{acl2p}



\section{Accumulators}

A common form of recursion is to decrement some argument while building the
final answer in another.  This allows the function to inspect the partially
computed answer.  In addition, such functions are often the functional
expression of an iterative process and are preferred over other forms of
recursion because they are tail-recursive, thus allowing compilers to make
optimizations that (for example) avoid stack overflows.  The arguments that are being built
up are called ``accumulators.''  Proving theorems about accumulator-using
functions frequently requires care in stating sufficiently general theorems.

Consider, for example, the challenge of reversing a list.  One definition
is
\begin{acl2p}
(defun rev (x)
  (if (consp x)
      (app (rev (cdr x)) (cons (car x) nil))
    nil))
\end{acl2p}
This definition suffers two inefficiencies in terms of the resources required
to execute it.  The first is that it requires stack space proportional to the
length of the list, because for every \ptt{cons} in the \ptt{cdr}-chain of
the input, execution must push a new stack frame so that it can ``remember''
to do the \ptt{app}.  The second is that the \ptt{app} copies the list
returned by the recursive call and returns the copy; the memory allocated to
creating the recursive call's answer is unreachable ``garbage'' as soon as
the \ptt{app} has finished with it.

The following tail-recursive version eliminates both of these drawbacks.
\begin{acl2p}
(defun rev1 (x a)
  (if (consp x)
      (rev1 (cdr x) (cons (car x) a))
    a))
\end{acl2p}
This is the functional expression of the code fragment:
\begin{acl2p}
while consp(x) \{ a = cons(car(x),a); x = cdr(x);\};
return a;
\end{acl2p}
It is the same as \ptt{rev} if \ptt{a} is initialized to \ptt{nil}.  For
example, \ptt{(rev1 '(1 2 3) nil)} is \ptt{'(3 2 1)}.

Suppose we wanted to prove \ptt{(equal (rev1 x nil) (rev x))}.  Think about
proving this by induction.  It is clear we should induct on \ptt{x} by
\ptt{cdr}.  The induction hypothesis is about \ptt{(rev1 (cdr x) nil)}.  The
induction conclusion is about \ptt{(rev1 x nil)}.  When we expand that term
in the conclusion it becomes \ptt{(rev1 (cdr x) (cons (car x) nil))}.  Note
that the \ptt{rev1} term in the hypothesis does not match the \ptt{rev1} term
in the conclusion.  In the hypothesis, the accumulator is \ptt{nil} but in
the expanded conclusion it is \ptt{(cons (car x) nil)}.  We would like to ``instantiate''
\ptt{nil} to be \ptt{(cons (car x) nil)}, but of course we cannot instantiate
anything but a variable.

This theorem is not strong enough to be inductively provable.  If we think of
\ptt{rev1} as an expression of an iteration, then the main theorem we are
proving is about the {\em{first}} entry to the loop (when \ptt{a} is
\ptt{nil}) and we must think about an arbitrary entry to the loop.  Put
another way, instead of thinking about \ptt{(rev1 x nil)} we
must think about \ptt{(rev1 x a)}.
This is just the generalization problem.

So what is the relation between \ptt{(rev1 x a)} and \ptt{(rev x)}?
One way to help discover the general form of the theorem we are seeking is
to try a few examples.  For example, \ptt{(rev1 '(1 2 3) '(4 5 6))}
is \ptt{(3 2 1 4 5 6)}.

The obvious general form of the theorem is \ptt{(equal (rev1 x a) (app (rev
x) a))}.

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{When dealing with a
function that has an accumulator argument, never try to prove a theorem
about the function by induction unless the accumulator argument is a variable
symbol.  That is, think about the most general legal call of the function,
not the initial call.}}
\vspace*{.1in}

As soon as you replace the \ptt{nil} in \ptt{(rev1 x nil)} by a new variable
symbol \ptt{a} you are confronted with the problem: what happens to \ptt{a}
on the other side of the theorem?  In this case, we use \ptt{app} to
``connect'' the expected answer, \ptt{(rev x)}, to the initial value of
\ptt{a}.  It is nice that \ptt{app} is already known to us.  Often, however,
you will have to invent a new function to relate the final answer to the
initial value of the accumulator.  This suggests the advice given earlier: do
not be afraid to introduce new concepts to explain what is happening.

Now consider proving \ptt{(equal (rev1 x a) (app (rev x) a))} by induction.
The Induction Principle allows us to replace \ptt{a} in the hypothesis by any
term we wish, if we are inducting on \ptt{x} (replacing \ptt{x} by the
smaller \ptt{(cdr x)}).  So which \ptt{a} do we choose?  The answer is
obvious: the \ptt{a} that we will need if we expand \ptt{(rev1 x a)} in the
conclusion.  In particular, the choice of \ptt{a} in the hypothesis is
\ptt{(cons (car x) a)}.

Here is ACL2's proof of the theorem.  Note how trivial it is.
{\small{
\begin{verbatim}
(defthm rev1-is-app-rev
  (equal (rev1 x a) (app (rev x) a)))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Two induction schemes
are suggested by this conjecture.  Subsumption reduces
that number to one.  

We will induct according to a scheme suggested by (rev1 x a).
This suggestion was produced using the :induction rules
rev and rev1.  If we let  (:p a x) denote *1 above then
the induction scheme we'll use is
(and (implies (not (consp x)) (:p a x))
     (implies (and (consp x)
                   (:p (cons (car x) a) (cdr x)))
              (:p a x))).
This induction is justified by the same argument used
to admit rev1, 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).  Note, however,
that the unmeasured variable a is being instantiated.
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 (rev1 x a) (app (rev x) a))).

But simplification reduces this to t, using the :definitions
app, rev and rev1, the :executable-counterpart of consp
and primitive type reasoning.

Subgoal *1/1
(implies (and (consp x)
              (equal (rev1 (cdr x) (cons (car x) a))
                     (app (rev (cdr x)) (cons (car x) a))))
         (equal (rev1 x a) (app (rev x) a))).

But simplification reduces this to t, using the :definitions
app, rev and rev1, the :executable-counterpart of consp,
primitive type reasoning and the :rewrite rules associativity-
of-app, car-cons and cdr-cons.

That completes the proof of *1.

Q.E.D.

Summary
Form:  ( defthm rev1-is-app-rev ...)
Rules: ((:definition app)
        (:definition rev)
        (:definition rev1)
        (:executable-counterpart consp)
        (:fake-rune-for-type-set nil)
        (:induction rev)
        (:induction rev1)
        (:rewrite associativity-of-app)
        (:rewrite car-cons)
        (:rewrite cdr-cons))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
 rev1-is-app-rev
ACL2 !>
\end{verbatim}}}

Note how we oriented the rewrite rule generated from \ptt{rev1-is-app-rev}:
we eliminate \ptt{rev1} in favor of the nicer functions \ptt{app} and
\ptt{rev}.  While \ptt{rev1} is computationally efficient, it is often
hard to state inductively provable theorems about it because the
accumulator argument must always be occupied by a variable symbol.

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{When you discover a
general theorem about an accumulator-using function relating it
to primitive recursive functions, use the new theorem to eliminate
the accumulator-using function from future problems.}}
\vspace*{.1in}

\vspace*{.1in}
\noindent {\bf{Exercises}}
\vspace*{.1in}

Use The Method to find proofs for each of the theorems below.

\vspace*{.05in}
{\noindent}{\bf{Problem 9.1}}  The following two functions are
\ptt{nump} analogues of factorial.  Prove they are equivalent:
\begin{acl2p}
(equal (fact1 n '(nil)) (fact n))  ; '(nil) is ``one''
\end{acl2p}
where
\begin{acl2p}
(defun fact (n)
  (if (consp n)
      (mult n (fact (cdr n)))
    '(nil)))

(defun fact1 (n a)
  (if (consp n)
      (fact1 (cdr n) (mult n a))
    a))
\end{acl2p}

\vspace*{.05in}
{\noindent}{\bf{Problem 9.2}}
\begin{acl2p}
(equal (mc-flatten x nil) (leaves x))
\end{acl2p}
where
\begin{acl2p}
(defun mc-flatten (x a)
  (if (consp x)
      (mc-flatten (car x)
                  (mc-flatten (cdr x) a))
    (cons x a)))
\end{acl2p}
The function \ptt{mc-flatten} is an ``almost tail-recursive'' version of
\ptt{leaves} first written by John McCarthy.  It has the interesting
property that it produces no garbage:  every \ptt{cons} it creates is
in the final answer, unlike \ptt{leaves}. 

\section{Conclusion}


We have illustrated how to find simple rigorous proofs.  We first repeat all
the hints given so far, and then we add a few more.

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Induction
must be applied to strong theorems, not weak ones!  Always try to invent the
strongest theorems you can think of!}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Give
careful thought to the ``preferred'' forms you use in your proofs and provide
yourself with lemmas that allow you, insofar as possible, to canonicalize
terms.}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{When using
the ACL2 system, {\em{never}} prove a named theorem without understanding its
effect as a rule!}}
\vspace*{.1in}

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Realize
that when you are dealing with arithmetic, your sense of what is
``straightforward'' has been honed by many years of drill-and-practice
with manipulating algebraic properties of numbers.  Be prepared to
``explain'' formally why some arithmetic relations hold!}}
\vspace*{.1in}

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{If you are
doing arithmetic proofs with ACL2, start by including
one of the arithmetic books into your script.  The most
commonly used book is included by adding the command
\ptt{(include-book "arithmetic/top-with-meta" :dir :system)}.}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Realize
that when you are dealing with arithmetic you may be doing inequality chaining,
not replacement of equals by equals, and make that form of reasoning explicit
in your notation.}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Every time you encounter
a new theorem you should give thought to how it is to be used in subsequent
proofs.}}
\vspace*{.1in}

\vspace*{.1in} {\noindent}{\bf{Hint on How To Prove Things:}} {\em{Ensure
that your rules do not loop!  One way to do this is to keep in mind some
ordering on your preferred terms and be sure that the right-hand side of each
rule is lower in this ordering than the left-hand side.}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}}
{\em{Definitions are (generally) used as expansion rules, i.e., function
calls are replaced by their instantiated bodies.  This imposes a restriction
on your choice of preferred forms: function bodies are preferable to function
calls.  If you want to override that built-in preference in ACL2, you should
disable the functions after proving the rules you need about them.}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{When
designing your rewrite rules, be sure the left-hand sides are in your
preferred form!}}
\vspace*{.1in}

\vspace*{.1in} {\noindent}{\bf{Hint on How To Prove Things:}} {\em{Keep your
proofs in the ``simplify, induct, simplify'' form.  That is, identify each
inductively proved lemma you need in a proof, write it down, and give it
a name.  Do not get into the habit of inventing and inductively proving
lemmas ``on the fly'' in the middle of other proofs.  It is better that you
understand and control the lemma decomposition of your theorems.}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{When
considering a new conjecture to prove, look for general theorems can will
prove it by simplification -- rewriting and chaining -- before you consider
proving it by induction.}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Look for
pairs of adjacent function symbols and try to think of rules that simplify
those expressions.}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{When
forming new conjectures, test them on constants.}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Often you
will have to invent new concepts -- concepts not involved in your main
theorem -- to state the lemmas you need.}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{If you
have introduced hypotheses in your lemmas, be sure you prove that the
appropriate terms satisfy those hypotheses.}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Separate your
concerns!}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{We
recommend that the novice ACL2 user not rely on ACL2's creative contributions
in the beginning.  As the problems become harder, ACL2's creative
contributions count for less and less -- and its ability to carry out massive
automatic simplifications using user-specified rules counts for more and
more.  So the novice is encouraged to learn to spot the need for rules and to
program ACL2 to use them.}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Whenever a
proof fails (or you want to reduce a proof to the recommended form), read the
formula at the first checkpoint and look for a lemma decomposition.
Sometimes, it helps to read a few formulas past the first checkpoint --
often ACL2's heuristics come fairly close to generating the needed lemma,
or at least creating a term that will suggest the lemma to you.  So if
the checkpoint does not suggest anything, read on.}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{When you know a
function is commutative, use that fact to arrange the arguments in
some canonical order.  Thus, if \ptt{add} is known to be commutative,
then whenever you see \ptt{(add b a)}, rewrite it to \ptt{(add a b)}.
But do not use the rule the other way -- to move things out of order --
or you will loop forever!  ACL2 uses this heuristic and uses a
lexicographic ordering on terms.}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{The heuristic
advice about commutative functions does not help you if you are rewriting
\ptt{(add b (add a c))} because the ordering (probably) will not
prefer \ptt{(add a c)} over \ptt{b}.  But the theorem above,
which we call a ``commutativity2'' theorem, allows that swap
and ACL2 uses such theorems to arrange the ordering of terms.
Given associativity, commutativity, commutativity2, and these heuristics,
you can arrange nests of such functions into right-associated form
with the arguments ascending in the order.  That is what ACL2 does.}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{When dealing with a
function that has an accumulator argument, never try to prove a theorem
about the function by induction unless the accumulator argument is a variable
symbol.  That is, think about the most general legal call of the function,
not the initial call.}}
\vspace*{.1in}

{\noindent}{\bf{Hint on How To Prove Things:}} {\em{When you discover a
general theorem about an accumulator-using function relating it
to primitive recursive functions, use the new theorem to eliminate
the accumulator-using function from future problems.}}
\vspace*{.1in}

See {\underline{\ptt{acl2-tutorial}}} for further introduction, with subtopics
containing many other helpful tips for using the ACL2 logic and theorem prover,
and with many more examples.

One important tip there is that there are many books of rules developed by
ACL2 users.  We did not stress the use of books here simply because we
are trying to train you to use The Method and to program the simplifier
yourself.  Those are skills you will need.  But as you master those
skills and move on to bigger projects, it is very helpful when you can
build on the work of others.  That is how mathematics has built such a
magnificent body of results.  So now we enshrine this advice as a hint.

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Build on the work of
others instead of inventing everything yourself.  In the ACL2 setting, learn
about the books available (by visiting the Mathematical Tools link on the
ACL2 home page), learn about and use \ptt{include-book} (see
{\underline{\ptt{include-book}}}) to load books into your scripts, and learn
to use \ptt{certify-book} (see {\underline{\ptt{certify-book}}}) to create
books others can use.}}
\vspace*{.1in}

If you want to learn more about ACL2, we recommend you buy the book
{\em{Computer-Aided Reasoning: An Approach}} by Kaufmann, Manolios, and Moore
\cite{kmm00a}.  While Kluwer Academic Press owns the electronic and hardback
copyrights, the authors own the paperback
rights and sell a spiral-bound version for close to their cost, about \$15 plus
shipping.  (You can find the book in hardback elsewhere, for well over its
original price of about \$120.)  See
the Books and Papers link on the ACL2 home page for ordering details.
The book contains about 150 exercises and the solutions are on the web.

The companion book, {\em{Computer-Aided Reasoning: ACL2 Case Studies}},
edited by the same authors \cite{kmm00b}, is also a very valuable resource
because it presents detailed notes on many large-scale proof projects and the
actual source scripts are available on the web.  The companion book is
available under the same copyrighting terms and approximately the same prices
as the first.

A detailed account of proof development for a non-trivial example may be
found in \cite{kp96}. The proof described there was carried out with ACL2's
predecessor, Nqthm, but lessons therein pertain to ACL2 usage as well.

The Workshops link on the home page is also a good source of material.  ACL2
workshop papers are usually accompanied by complete proof scripts, which are
posted on the ACL2 home page.

One more hint is in order.  

\vspace*{.1in}
{\noindent}{\bf{Hint on How To Prove Things:}} {\em{Practice makes perfect.
There is no substitute for experience.  Think of theorems to prove and work
out the proofs!}}

\appendix

\section{Definitions}
\label{alldefs}

In this appendix we include definitions of all the functions mentioned in our
exercises.  This appendix thus answers the exercises that just require
definitions!  So don't look here until you do those exercises.  But to do the proof-based exercises,
it might be best to use our definitions.

We have presented the definitions in alphabetical order so you can find them.
ACL2 requires definitions to be presented bottom-up: define concepts before
using them.

{\small{
\begin{verbatim}
(defun add (x y)
  (if (consp x)
      (cons nil (add (cdr x) y))
    (mapnil y)))

(defun app (x y)
  (if (consp x)
      (cons (car x) (app (cdr x) y))
    y))

(defun collect-lonesomep (a b)
; collect elements of a that are lonesome in b
  (if (consp a)
      (if (lonesomep (car a) b)
          (cons (car a)
                (collect-lonesomep (cdr a) b))
        (collect-lonesomep (cdr a) b))
    nil))

(defun dup (x)
  (if (consp x)
      (cons (car x)
            (cons (car x)
                  (dup (cdr x))))
      nil))

(defun fact (n)
  (if (consp n)
      (mult n (fact (cdr n)))
    '(nil)))

(defun fact1 (n a)
  (if (consp n)
      (fact1 (cdr n) (mult n a))
    a))

(defun foundp (x a)
  (if (consp a)
      (if (equal x (car (car a)))
          t
        (foundp x (cdr a)))
    nil))

(defun int (x y)
  (if (consp x)
      (if (memp (car x) y)
          (cons (car x) (int (cdr x) y))
        (int (cdr x) y))
    nil))

(defun leaves (x) ; the leaves of x
  (if (consp x)
      (app (leaves (car x))
           (leaves (cdr x)))
    (cons x nil)))

(defun lonesomep (e lst)
  (if (mem e lst)
      (not (mem e (cdr (mem e lst))))
    nil))

(defun lonesomes (x)
  (collect-lonesomep (leaves x) (leaves x)))

(defun lookup (x a)
  (if (consp a)
      (if (equal x (car (car a)))
          (cdr (car a))
        (lookup x (cdr a)))
    nil))

(defun mapnil (x)
  (if (consp x)
      (cons nil (mapnil (cdr x)))
    nil))

(defun mc-flatten (x a)
  (if (consp x)
      (mc-flatten (car x)
                  (mc-flatten (cdr x) a))
    (cons x a)))

(defun mem (e x) ; where does e occur in x?
  (if (consp x)
      (if (equal e (car x))
          x
        (mem e (cdr x)))
    nil))

(defun memp (e x)
  (if (consp x)
      (if (equal e (car x))
          t
        (memp e (cdr x)))
    nil))

(defun mult (x y)
  (if (consp x)
      (add y (mult (cdr x) y))
    nil))

(defun nump (x)
  (if (consp x)
      (and (equal (car x) nil)
           (nump (cdr x)))
    (equal x nil)))

(defun properp (x)
  (if (consp x)
      (properp (cdr x))
    (equal x nil)))

(defun raise (x y)
  (if (consp y)
      (mult x (raise x (cdr y)))
    '(nil)))

(defun rev (x)
  (if (consp x)
      (app (rev (cdr x)) (cons (car x) nil))
    nil))

(defun rev1 (x a)
  (if (consp x)
      (rev1 (cdr x) (cons (car x) a))
    a))

(defun seteqp (x y)
  (and (subp x y)
       (subp y x)))

(defun swaptree (x)
  (if (consp x)
      (cons (swaptree (cdr x))
            (swaptree (car x)))
    x))

(defun subp (x y)
  (if (consp x)
      (if (memp (car x) y)
          (subp (cdr x) y)
        nil)
    t))

(defun treecopy (x)
  (if (consp x)
      (cons (treecopy (car x))
            (treecopy (cdr x)))
     x))

(defun ziplists (x y)
  (if (consp x)
      (cons (cons (car x) (car y))
            (ziplists (cdr x) (cdr y)))
    nil))
\end{verbatim}}}

\section{Emacs}
\label{emacs}

Emacs has an interactive tutorial.  Type \ptt{meta-x help-with-tutorial enter}.
Here are some commonly used commands.

{\noindent}{\bf{To Insert Text}}

\begin{tabular}{ll}
just type it &
\end{tabular}

{\noindent}{\bf{To Move Around}}

\begin{tabular}{ll}
ctrl-f & move forward one character \\
ctrl-b & move backward one character \\
ctrl-n & move down to next line \\
ctrl-p & move up to previous line \\
ctrl-meta-f & moves forward over balanced expression \\
ctrl-meta-b & moves backward over balanced expression \\
ctrl-meta-u & moves up one level of parens. \\
meta-$<$ & move to the beginning of the buffer \\
meta-$>$ & move to the end of the buffer
\end{tabular}

{\noindent}{\bf{To Cut and Paste}}

\begin{tabular}{ll}
ctrl-d & delete one character \\
ctrl-k & kill one line -- and put it in the ``kill ring'' \\
ctrl-meta-k & kill one balanced expression - and put it in the ``kill ring'' \\
ctrl-y & to yank (paste) text from the kill \\
       & ring back into the buffer \\
\end{tabular}

{\noindent}{\bf{Other}}

\begin{tabular}{ll}
ctrl-x b & select another buffer (type buffer name) \\
ctrl-x ctrl-f & read a file into a buffer of that name \\
ctrl-x ctrl-s & write a buffer to the file it came from \\
ctrl-x ctrl-w & write a buffer to the file you name \\
ctrl-meta-q & indent the list expression immediately after \\
            & the cursor in a way consistent with the parentheses
\end{tabular}

The ACL2 source code distribution comes with a pre-defined Emacs library that
contains many useful commands for interacting with ACL2.  Just put the
following in the \ptt{.emacs} file in your home directory, replacing
\ptt{<dir>} by the absolute pathname of your local ACL2 source code directory.
\begin{verbatim}
(load "<dir>/emacs/emacs-acl2.el")
\end{verbatim}
This library also enables navigation of proofs and checkpoints with an
emacs-based tool; see {\underline{proof-tree-emacs}}.

\bibliographystyle{plain}
\bibliography{main}

\end{document}

