ch04.tex

\chapter{Mathematical Induction}
\label{ch:mathematical-induction}

\section{Lists as Mathematical Objects}
\label{sec:lists-as-obj}
A \index{sequence}\index{list}sequence
is an ordered list of elements.
In fact, for our purposes, the terms ``list'' and ``sequence'' are synonyms.
Many things that computers do come down to keeping track of lists,
so lists are an important class of mathematical objects.
We will need a formal notation, including an algebra of formulas,
to discuss lists with the level of mathematical precision
required in specifications of computer hardware and software.

Informally, we will write lists as sequences of elements separated by spaces,
with square brackets marking the beginning and end of the list.
For example, \textsf{[8 3 7]} denotes a list with first element 8,
second element 3, and third element 7, and
\textsf{[9 8 3 7]} denotes a list with the same elements
plus an additional element 9 at the beginning.
\label{nil-def}\index{nil}\index{empty list (nil)}We
use the symbol \textsf{nil} for the empty list
(that is, the list with no elements).
\label{square-brackets}We use
\index{square brackets}\index{brackets!square}\index{list!square bracket notation}square brackets
rather than round ones in formulas
specifying lists, to avoid confusion with formulas that
invoke operators.\footnote{To \index{invoke (invocation)}\emph{invoke}
an operator is to apply it to its operands
to make a computation.
An \emph{invocation} is a formula that invokes an operator.}
For example, \textsf{[4 7 9]} denotes a three-element \index{list}list,
whereas \textsf{(+ 7 9)} is a numeric formula representing the value 16.
However, ACL2 does not employ this square-bracket notation.
When it displays the list \textsf{[4 7 9]},
it uses \index{parentheses}\index{brackets!round}round brackets: \textsf{(4 7 9)}.
The square-bracket notation helps keep data in computational formulas
straight in written discussion and also makes some
formulas more compact in writing, but square-bracket
notation for lists is not ACL2 notation.

One of the basic operators in the algebra of lists is the
\index{list!cons (\emph{see also} operator)}construction operator
\index{operator, by name!cons (insert at front)}\textsf{cons},
which inserts a new element at the beginning of a list.
Formulas using \textsf{cons}, like all formulas in
the mathematical notation we have been using to discuss software concepts,
are written in prefix form.
So, the formula \textsf{(cons $x$ $xs$)} denotes a list
with the same elements as the list $xs$
plus an additional element $x$ inserted at the beginning.
If $x$ stands for the number \textsf{9}
and $xs$ stands for the list \textsf{[8 3 7]},
then \textsf{(cons $x$ $xs$)} constructs the list \textsf{[9 8 3 7]}.

\begin{aside}{square-bracket-notation}{Square Bracket Notation for Lists: Paper-and-Pencil Only}
Most of the time, we will use square bracket
\index{square brackets}\index{brackets!square}\index{list!square bracket notation}notation for lists
to distinguish them from computational formulas.
However, ACL2 does not display lists with square brackets.
It uses round parentheses both for lists and for computational formulas.
\begin{center}
\begin{tabular}{cc}
 \emph{paper-and-pencil only} & \emph{formal ACL2 notation}\\
 \textsf{[1 2 1 5]}           & \textsf{(list 1 2 1 5)}\\
\end{tabular}
\end{center}
%\caption{Square Bracket Notation for Lists: Paper-and-Pencil Only}
%\label{square-bracket-notation}
\end{aside}

\begin{figure}
\begin{center}
\textsf{[$x_1$ $x_2$ \dots $x_n$]} $=$
\textsf{(list $x_1$ $x_2$ $\dots$ $x_n$)} $=$ \textsf{(cons $x_1$ (cons $x_2$ $\dots$ (cons $x_n$ nil) $\dots$))}\\
\addtolength{\tabcolsep}{-4pt}
\begin{tabular}{lclcl}
\hline \\[-1.0em]
\textsf{{[1 2]}}         &$=$ &\textsf{(list 1 2)}        &$=$ &\textsf{(cons 1 (cons 2 nil))}\\
\textsf{{[16 256 4096]}} &$=$ &\textsf{(list 16 256 4096})&$=$ &\textsf{(cons 16 (cons 256 (cons 4096 nil)))}\\
\textsf{{[1 9 4 7]}}     &$=$ &\textsf{(list 1 9 4 7)}    &$=$ &\textsf{(cons 1 (cons 9 (cons 4 (cons 7 nil))))}\\
\end{tabular}
\addtolength{\tabcolsep}{4pt}
\end{center}
\caption{Shorthand for nested \textsf{cons}: \textsf{list}.}
\label{fig:list-nested-cons}
\end{figure}

Any list can be constructed by starting from an \index{empty list (nil)}empty list
and using the construction operator to insert the elements of the list, one by one.
The empty list, \index{nil}\textsf{nil}, which is intrinsic in ACL2, needs no construction.
Nonempty \index{list!nonempty}lists are constructed using the \textsf{cons} operator.
The formula \textsf{[8 3 7]} is paper-and-pencil shorthand
for \textsf{(cons 8 (cons 3 (cons 7 nil)))}.
ACL2 also has shorthand
for nested \textsf{cons} operations
(figure \ref{fig:list-nested-cons}): %, page \pageref{fig:list-nested-cons}):
\textsf{(list 8 3 7)} is another way to write the formula
\textsf{(cons 8 (cons 3 (cons 7 nil)))}.

\begin{aside}{three-line-equal}{Equal by Definition: $\equiv$}
The
\index{equation!defining ($\equiv$)}\index{definition!equation ($\equiv$)}\index{equivalence!by definition ($\equiv$)}\index{three-line equal ($\equiv$)}\index{equal, three-line ($\equiv$)}three-line
variation of the equals sign
indicates that the term on the left stands
for the formula on the right \emph{by definition}.
\begin{center}
\addtolength{\tabcolsep}{-2pt}
\begin{tabular}{ll}
$term$ $\equiv$ $\dots$ \emph{some formula} $\dots$    &\emph{definition of term} \\
$P(xs, y, ys)$ $\equiv$ $(xs$ $=$ \textsf{(cons $y$ $ys$)}$)$ &$P(xs, y, ys)$ \emph{means} $(xs$ $=$ \textsf{(cons $y$ $ys$)}$)$  \\
\end{tabular}
\addtolength{\tabcolsep}{2pt}
\end{center}
%\caption{Equal by Definition: $\equiv$}
%\label{three-line-equal}
%%note: this aside mostly repeats an aside in ch02 predicates section, on purpose in case they skip that section
\end{aside}

Suppose we take $P(xs, y, ys)$ as shorthand
for the equation $xs$ $=$ \textsf{(cons $y$ $ys$)}.
\begin{center}
$P(xs, y, ys)$ $\equiv$ $(xs$ $=$ \textsf{(cons $y$ $ys$)}$)$
\end{center}

Given a particular list $xs$, together with a value $y$,
we can view the equation $P(xs, y, ys)$ as a set of propositions
indexed by the variable $ys$ whose universe of discourse is the set of
lists that can be constructed by ACL2.
In this set of propositions, the one corresponding to
the list $ys$ is the equation that $P(xs, y, ys)$ stands for:
$(xs$ $=$ \textsf{(cons $y$ $ys$)}$)$.
If that equation holds, the value of the proposition $P(xs, y, ys)$ is true.
Otherwise, it's false.
For example, if $xs$ denotes the list \textsf{[1 2 3]}
and $y$ denotes the natural number \textsf{1},
then $P(xs, y, ys)$ is $P($\textsf{[1 2 3]}, \textsf{1}, $ys)$,
which stands for an equation involving the variable $ys$.
There is one such equation for each different list $ys$.
Taken all together, those equations comprise a predicate
whose universe of discourse is ACL2 lists.

The operator
\index{predicate, by name!consp (nonempty list)}\seeonlyindex{consp}{predicate}\textsf{consp}
checks for nonempty lists.
That is, the formula \textsf{(consp $xs$)} delivers true
if $xs$ is a nonempty list and false otherwise.
The \{\emph{consp}\} axiom
(figure~\ref{consp-axiom}) %, page \pageref{consp-axiom})
formally asserts that all nonempty lists
are constructed with the \textsf{cons} operator.

The formula
$(\exists ys.P($\textsf{[1 2 3]}, \textsf{1}, $ys))$ is true
because \textsf{[1 2 3]} $=$ \textsf{(cons 1 [2 3])},
so there is a value of $ys$, namely, $ys$ $=$ \textsf{[2 3]},
for which $P($\textsf{[1 2 3]}, \textsf{1}, $ys)$ is true.
If there were no list that made the equation valid,
the formula $(\exists ys.P($[1 2 3], \textsf{1}, $ys))$
would be false.

If, on the other hand, $xs$ were the list \textsf{[1 2 3]}
and $y$ were the number 2, there would be no list
$ys$ that would make the equation \textsf{[1 2 3]} $=$ \textsf{(cons $2$ $ys$)} valid
because the list on the left-hand side of the equation
starts with 1 and the list on the right-hand side starts with 2.
So, the formula $(\exists ys.P($\textsf{[1 2 3]}, \textsf{2}, $ys))$
is false.

\begin{figure}
%\begin{center}
\begin{tabular}{c}
Axiom \{\emph{consp}\} \\
\hline
\textsf{(consp $xs$)} $=$  $(\exists y.(\exists ys.(xs$ $=$ \textsf{(cons $y$ $ys$)}$)))$
\end{tabular}
%\end{center}
\index{axiom, by name!\{consp\}}\index{operator, by name!consp (\emph{see} predicate)}\seeonlyindex{consp}{predicate}\index{predicate, by name!consp}
\caption{Nonempty list predicate: \textsf{consp}.}
\label{consp-axiom}
\end{figure}

Now, let's take a step back.
We can view the formula
($\exists ys.$ ($xs$ $=$ \textsf{(cons $y$ $ys$)}))
as a set of propositions,
one for each object $y$ that ACL2 can represent.
The formula
$(\exists ys.P(xs, y, ys))$ is one way to represent that
set of propositions.
Since any set of propositions is a predicate,
we can view $(\exists ys.P(xs, y, ys))$ as a predicate indexed
by the set of ACL2 objects $y$.

\begin{figure}
%\begin{center}
\begin{tabular}{c}
Axiom \{\emph{nlst}\}\\
\hline
\textsf{[$x_{m}$  $x_{m+1}$ \dots $x_{n}$]}  \emph{denotes a list with $n - m + 1$ elements} \{\emph{nlst}\} \\
\emph{Note: Denotes} \textsf{nil}\emph{, the empty list, if $m > n$}\\
\end{tabular}
%\end{center}
\index{numbered list notation}\index{list!numbered}\index{list!ellipsis}\index{axiom, by name!\{nlst\}}
\caption{Numbered list notation.}
\label{numbered-list-interpretation}
\end{figure}

We can convert the predicate $(\exists ys.P(xs, y, ys))$
into a true/false value (that is, convert it to a proposition)
by applying the $\exists$ quantifier again,
but this time with $y$ as the bound variable:
$(\exists y.(\exists ys.P(xs, y, ys)))$.
When $xs$ is a list for which this formula has the value true,
then \textsf{(consp $xs$)} is true.
That is, \textsf{consp} is the ACL2 predicate that means $(\exists y.(\exists ys.P(xs, y, ys)))$.
The universe of discourse of the predicate \textsf{consp}
is the set of all objects that ACL2 can represent.
That specification of \textsf{consp} is expressed in the \{\emph{consp}\} axiom
(figure~\ref{consp-axiom}, page \pageref{consp-axiom}).
So, \textsf{(consp $xs$)} is a way to write the formula
$(\exists y.(\exists ys.(xs$ $=$ \textsf{(cons $y$ $ys$)}$)))$ in ACL2.

When we know that a list $ys$ is nonempty,
we can cite the \{\emph{consp}\} axiom
to rewrite $ys$ in the form \textsf{(cons $x$ $xs$)}.
When we do this, we choose the symbols $x$ and $xs$ carefully
to avoid conflicts with other symbols that appear in the context of the discussion.

The \{\emph{consp}\} axiom refers to \textsf{cons},
so we will need a \{\emph{cons}\} axiom.
The \{\emph{cons}\} axiom uses numbered list notation
(figure~\ref{numbered-list-interpretation}, page \pageref{numbered-list-interpretation})
to specify that \textsf{cons} delivers a nonempty list,
\textsf{[$x_1$ $x_2$ \dots $x_{n+1}$]},
where $n$ stands for a natural number.
Because that list has $n+1$ elements and $n+1$
is at least one when $n$ is a natural number,
the list cannot be empty.
Therefore, the list can be constructed by \textsf{cons}.

The construction operator, \textsf{cons}, cannot be the whole story, of course.
To compute with lists, we  need to be able to construct them,
but we also need to be able to take them apart.
There are two basic operators for taking lists apart: \textsf{first} and \textsf{rest}.
We express the relationship between these operators and
the construction operator in the form of equations,
\{\emph{fst}\} and \{\emph{rst}\}, that we take as axioms
(figure~\ref{first-rest-cons}). %, page \pageref{first-rest-cons}).

\begin{figure}
%\begin{center}
\begin{tabular}{ll}
 \multicolumn{2}{c}{Axioms \{\emph{cons}\}, \{\emph{first}\}, and \{\emph{rest}\}} \\
 \textsf{[$x_1$ $x_2$ \dots $x_{n+1}$]} $=$ \textsf{(cons $x_1$ [$x_2$ \dots $x_{n+1}$])} & \{\emph{cons}\} \\
 \hline
 \textsf{(first (cons $x$ $xs$))} $=$ $x$                                        & \{\emph{fst}\}\\
 \textsf{(rest (cons $x$ $xs$))}  $=$ $xs$                                       & \{\emph{rst}\} \\
 \textsf{(first nil)} $=$ \textsf{nil}                                           & \{\emph{fst0}\}\\
 \textsf{(rest nil)} $=$ \textsf{nil}                                            & \{\emph{rst0}\}\\
\end{tabular}
%\end{center}
\index{operator, by name!first (extract first element)}\index{operator, by name!rest (drop first element)}\index{axiom, by name!\{fst\}, \{fst0\}}\index{operator, by name!cons (insert at front)}\seeonlyindex{first}{operator}\seeonlyindex{rest}{operator}\seeonlyindex{cons}{operator}\index{list!cons (\emph{see also} operator)}\index{list!first (\emph{see also} operator)}\index{list!rest (\emph{see also} operator)}\index{axiom, by name!\{rst\}, \{rst0\}}\index{axiom, by name!\{cons\}}\index{equation, by name!\{fst\}, \{fst0\}}\index{equation, by name!\{rst\}, \{rst0\}}\index{equation, by name!\{snd\}}\index{equation, by name!\{cons\}}
\caption{List constructor and deconstructors: \textsf{cons}, \textsf{first}, \textsf{rest}.}
\label{first-rest-cons}
\end{figure}

The \{\emph{fst}\} axiom states formally that
the operator \textsf{first} delivers the first element from a nonempty list.
The \{\emph{rst}\} axiom states that the operator \textsf{rest} delivers
a list like its operand but without the first element.
Note that the lists to which the operators \textsf{first} and \textsf{rest}
are applied in the axioms have at least one element
because those lists are constructed by the \textsf{cons} operator.
The axioms
\{\emph{fst0}\} and \{\emph{rst0}\}
provide an interpretation of the formulas
\textsf{(first nil)} and \textsf{(rest nil)}
when the operand is a list with no elements.

We will use equations like the ones in these axioms in the
same way we used the logic equations in figure~\ref{fig-02-02}
(page \pageref{fig-02-02}) and the arithmetic equations of
figure~\ref{fig-02-01} (page \pageref{fig-02-01}).
That is, whenever we see a formula like \textsf{(first (cons $x$ $xs$))},
no matter what formulas $x$ and $xs$ stand for,
we will be able to cite equation \{\emph{fst}\} to replace
\textsf{(first (cons $x$ $xs$))} by the simpler formula $x$.
Equations go both ways, so we can also cite equation \{\emph{fst}\}
to replace any formula $x$ by the more complicated formula
\textsf{(first (cons $x$ $xs$))}, where $xs$ stands for any formula
we care to make up, as long as it is grammatically correct.

Similarly, we can cite the equation \{\emph{rst}\} to justify
replacing the formula \textsf{(rest (cons $x$ $xs$))} by $xs$
and vice versa, regardless of what formulas the symbols $x$ and $xs$ stand for.
In other words, these are ordinary algebraic equations.
The only new factors are
(1)~the kind of mathematical object they denote and
(2)~the syntactic quirk of prefix notation, instead of the more familiar infix notation.
All \index{property!of lists}\index{list!properties}properties of lists,
as mathematical objects,
derive from the \{\emph{cons}\}, \{\emph{fst}\}, and \{\emph{rst}\} axioms.

The operator \textsf{len} (page \pageref{len-op-informal})
delivers the number of elements in a list.
We can use \textsf{check-expect} to test \textsf{len} in some specific cases.

\begin{code}
\begin{verbatim}
(check-expect (len (cons 8 (cons 3 (cons 7 nil)))) 3)
(check-expect (len nil) 0)
\end{verbatim}
\end{code}

We can use the DoubleCheck facility for more general tests.
For example, we expect that the number of elements
in a list constructed by the \textsf{cons} operation is
one more than the number of elements in its second operand.
The following property tests this expectation:

\index{definition!property}\index{data, random test}\index{random data}\index{defproperty}
\begin{code}
\begin{verbatim}
(defproperty len-cons-test
  (x  :value (random-natural)
   xs :value (random-list-of (random-natural)))
  (= (len (cons x xs))
     (+ 1 (len xs))))
\end{verbatim}
\end{code}

By the same token, we expect that a list always
has one more element than it would have if
its first element were removed: \textsf{(len $xs$)} $=$ $1 +$ \textsf{(len (rest $xs$))}.
However, that is true only if the list $xs$
has some elements. It would not be true if $xs$ were \textsf{nil}.
What we want to test is an implication:
\textsf{(consp $xs$)} $\rightarrow$ (\textsf{(len $xs$)} $=$ $1$ $+$ \textsf{(len (rest $xs$))}$)$.
The ACL2 name for the implication operator is \textsf{implies},
and we can use that operator to specify a test that
constrains $xs$ to nonempty lists and thereby
makes the length equation in the test true.

\index{definition!property}\index{data, random test}\index{random data}\index{defproperty}
\begin{code}
\begin{verbatim}
(defproperty len-rest-test
  (xs :value (random-list-of (random-natural)))
  (implies (consp xs)
           (= (len xs)
              (+ 1 (len (rest xs))))))
\end{verbatim}
\end{code}

The equation in the len-rest test can serve
as an axiom for the \textsf{len} operator in the case
when its operand is a nonempty list.
The axiom for the empty case is simpler.
Figure~\ref{fig:len-axioms} (page \pageref{fig:len-axioms})
states these two axioms for
the len operator. Axiom \{\emph{len1}\} applies when
the operand is nonempty and the other axiom
applies in all other circumstances.\footnote{Normally
the operand of len will be either a nonempty list or nil, the empty list.
That is a good way to think of it for now,
but the operand may not be a list at all,
and according to axiom \{\emph{len0}\}, its value is zero in that case.
So, \textsf{(len nil)} $=$ $0$ but \textsf{(len $3$)} $=$ $0$ too since
$3$ is not a list. Later, we will say more about this kind of axiom.}

\begin{figure}
%\begin{center}
\begin{tabular}{ll}
\multicolumn{2}{c}{Axioms \{\emph{len}\}} \\
\hline
\textsf{(len (cons $x$ $xs$))} $=$ \textsf{(+ 1 (len $xs$))} & \{\emph{len1}\} \\
\textsf{(len $e$)} $=$ 0                            & \{\emph{len0}\} \\
\multicolumn{2}{c}{\emph{Note: Cite }\{\emph{len0}\}\emph{ only if }\{\emph{len1}\}\emph{ doesn't match.}}\\
\end{tabular}
%\end{center}
\caption{Length of list: \textsf{len}.}
\label{len-equations}\label{fig:len-axioms}
\end{figure}

We expect the \textsf{len} operator to deliver a natural number,
regardless of the value of its operand.
For the record, we state this property as a theorem.
Later, you will have a chance to derive
this theorem from the \{\emph{len}\} axioms.
The theorem refers to the \textsf{natp} operator
(page \pageref{natp-op}),
which delivers true if its operand is a natural number and false otherwise.
\begin{samepage}
\label{len-nat-thm}\index{theorem, by name!\{len-nat\}}
\begin{center}
Theorem \{\emph{len-nat}\}: $\forall xs.$\textsf{(natp (len $xs$))}
\end{center}
\end{samepage}

A related fact is that the length of a nonempty list is strictly positive.
One way to state that fact is to observe that the formula \textsf{(consp $xs$)} is true
if \textsf{($>$ (len $xs$) 0)} and vice-versa. %(\verb+>+ (len $xs$) 0). %\textit{using math mode instead of \verb}
%In the notation from Chapter~\ref{ch:Boolean-Formulas}:  %\textit{never covered the equiv op}
%(consp $xs$)$\leftrightarrow$(\verb+>+ (len $xs$) 0).
This theorem too can be derived from the axioms for
\textsf{len}, \textsf{consp}, and \textsf{cons}.
For the moment, we state the theorem without proof.
\begin{samepage}
\label{consp-len-thm}
\index{theorem, by name!\{consp $= (len > 0)$\}}
\begin{center}
Theorem \{\emph{consp} $= (len > 0)$\}: $\forall xs.($\textsf{(consp $xs$)} $=$ \textsf{($>$ (len $xs$) 0)}$)$
\end{center}
\end{samepage}

\begin{aside}{acl2-single-quote}{Suppressing Computation with Single-Quote}
To specify the list \textsf{[1 2 3 4]} in an ACL2 formula
rather than in a paper-and-pencil formula,
we can, of course, use the \textsf{cons} operator to construct it:
\textsf{(cons 1 (cons 2 (cons 3 (cons 4 nil))))}.
Or, we can use the \textsf{list} operator (page \pageref{list-op-informal}) to write it more compactly:
\textsf{(list 1 2 3 4)}.

However, the single-quote trick provides a less bulky ACL2 formula for lists
whose elements are numbers (or literals denoting other ACL2 constants).
The formula
\textsf{'(1 2 3 4)} has the same meaning as \textsf{(list 1 2 3 4)}.
Normally, ACL2 interprets the first symbol after a left-parenthesis
as the name of an operator.
However, the single-quote mark suppresses that interpretation and
delivers a list made up of the elements in the parentheses.
Without the single-quote mark,
the formula would make no sense because 1 is not the name of an
operator.\index{single-quote mark}\index{quote mark, single}\index{square brackets}\index{brackets!square}\index{list!square bracket notation}
%\caption{Suppressing Computation with Single-quote}
%\label{acl2-single-quote}
\end{aside}

\begin{exercises}

\exer {\label{rst1}%
\index{theorem, by name!\{rst1\}}Prove theorem \{\emph{rst1}\}: \textsf{(rest (list $x$))} $=$ \textsf{nil}.\\
\emph{Hint}: Cite some equations from figure~\ref{first-rest-cons} (page \pageref{first-rest-cons})
and figure~\ref{fig:list-nested-cons} (page \pageref{fig:list-nested-cons}).}

\end{exercises}

\section{Mathematical Induction}
\label{sec:induction}
The \textsf{cons}, \textsf{first}, and \textsf{rest} operators
form the basis for computing with lists,
but there are lots of other operators for lists.
The operator \textsf{append}, previously discussed in terms of some \textsf{check-expect} tests
(page \pageref{append-op-informal}), concatenates two lists, as illustrated
in the following \textsf{check-expect} tests,
which use the single-quote notation (box~\ref{acl2-single-quote}, page \pageref{acl2-single-quote})
to make them more compact:

\begin{code}
\begin{verbatim}
(check-expect (append '(1 2 3 4) '(5 6 7)) '(1 2 3 4 5 6 7))
(check-expect (append '(1 2 3 4 5) nil) '(1 2 3 4 5))
\end{verbatim}
\end{code}
%'

The numbered-list notation
(figure~\ref{numbered-list-interpretation}, page \pageref{numbered-list-interpretation})
provides a way to define the \textsf{append} operator informally.
In this form, the definition implicitly reveals the number of elements in the lists
involved in the concatenation.
\label{list-schematic} In the following list schematics,
the $x$ list has $m$ elements, the $y$ list has $n$ elements,
and the concatenated list has $m+n$ elements:
\begin{samepage}
\begin{center}
\textsf{(append [$x_1$ $x_2$ $\dots$ $x_m$] [$y_1$ $y_2$ $\dots$ $y_n$])} $=$
\textsf{[$x_1$ $x_2$ $\dots$ $x_m$ $y_1$ $y_2$ $\dots$ $y_n$]}
\end{center}
\end{samepage}

Let's analyze the concatenation \textsf{(append $xs$ $ys$)}. %'
If $xs$ is the empty list, then we expect
the concatenation to deliver the list $ys$.
This is the  \{\emph{app0}\} case: \textsf{(append nil $ys$)} $=$ $ys$.
If $xs$ is not empty, then we expect the concatenation
to start with the first element of $xs$,
that is, \textsf{(first $xs$)}, and to continue
with the remaining elements of $xs$, that is, \textsf{(rest $xs$)},
and then the elements of $ys$ come after that.
Put another way, when $xs$ is not empty,
the result is the concatenation of \textsf{(rest $xs$)} and $ys$,
with \textsf{(first $xs$)} inserted at the front.
This is the \{\emph{app1}\} case: \textsf{(append $xs$ $ys$)} $=$
\textsf{(cons (first $xs$) (append (rest $xs$) $ys$))}.

We would like to express our expectations formally.
To do so, we use a special ACL2 operator
called \textsf{if} (figure~\ref{fig:if-axioms}), which has three operands.
It delivers its second operand if
its first operand is true (that is, not \textsf{nil})
and selects its third operand
if its first operand is false (that is, \textsf{nil}).
So, the \textsf{if} operator provides a way to select between
the two formulas supplied as its second and third operands.

\begin{figure}
%\begin{center}
\begin{tabular}{ll}
\multicolumn{2}{c}{Axioms \{\emph{if}\}} \\
\hline
\textsf{(if $p$ $x$ $y$}) $=$ $x$, \emph{if} $p$ $\neq$ \textsf{nil}  & \{\emph{if-true}\}  \\
\textsf{(if $p$ $x$ $y$)} $=$ $y$, \emph{if} $p$ $=$ \textsf{nil}     & \{\emph{if-false}\} \\
\end{tabular}
%\end{center}
\index{axiom!if-true, if-false}\index{axiom, by name!\{if-true\}, \{if-false\}}\index{equation, by name!\{if-true\}, \{if-false\}}\index{operator, by name!if (select formula)}\seeonlyindex{if}{operator}
\caption{Formula selector: \textsf{if}.}
\label{fig:if-axioms}
\end{figure}

With the \textsf{if} operator, we can use DoubleCheck
to test our expectations of \textsf{(append $xs$ $ys$)}
by comparing \textsf{(append $xs$ $ys$)} to the \{\emph{app1}\} formula
if $xs$ is nonempty and to the \{\emph{app0}\} formula if $xs$ is empty.
Figure~\ref{fig:append-test} (page \pageref{fig:append-test})
displays a property definition that formalizes this idea.
It uses an operator called
\textsf{equal} (box~\ref{equal}, page \pageref{equal})
to compare \textsf{(append $xs$ $ys$)}
to a formula selected by the \textsf{if} operator.

\begin{figure}
\index{definition!property}\index{data, random test}\index{random data}\index{defproperty}
\begin{code}
\begin{verbatim}
(defproperty append-test
  (xs :value (random-list-of (random-natural))
   ys :value (random-list-of (random-natural)))
  (equal (append xs ys)
         (if (consp xs)
             (cons (first xs)
                   (append (rest xs) ys))
             ys)))
\end{verbatim}
\end{code}
\caption{DoubleCheck test of \textsf{append}.}
\label{fig:append-test}
\end{figure}

\begin{aside}{equal}{``\textsf{equal}'' vs ``\textsf{=}''}
Why is it \textsf{(equal (append $xs$ $ys$) $\dots$)}?
Why not \textsf{(= (append $xs$ $ys$) $\dots$)}?
The ``\textsf{=}'' operator
is restricted to numbers, whereas the operator \textsf{equal} can check
for equality between any two values: numbers, lists, whatever.

The $=$ symbol reminds people who are
reading the formula that it compares numbers.
It reminds the computer, too, and that could
simplify mechanized reasoning or
promote efficient comparison.
Mostly, though, it's a matter of
taste.\index{equal, vs =}\seeonlyindex{equal}{predicate}\index{operator, by name!equal (\emph{see} predicate)}\index{predicate, by name!equal}\index{operator!numeric order ($<$, $<=$, $=$, $>=$, $>$)}\index{predicate!numeric order ($<$, $<=$, $=$, $>=$, $>$)}\index{order!numeric ($<$, $<=$, $=$, $>=$, $>$)}\index{number!order ($<$, $<=$, $=$, $>=$, $>$)}\index{compare!numbers ($<$, $<=$, $=$, $>=$, $>$)}\index{predicate!numeric order ($<$, $<=$, $=$, $>=$, $>$)}\index{compare!ACL2 values (equal)}
%We will be using ``='' when we can and hope it doesn't put too much of an extra burden on you.
%\caption{``\textsf{equal}'' vs ``\textsf{=}''}
%\label{equal}
\end{aside}

The append-test property might not be the first test you would think of,
but if the test failed to pass,
you would know for sure that something was wrong with the \textsf{append} operator.
The append-test property is so plainly correct that
we are going to state it in the form of equations that we accept as axioms
(figure~\ref{append-equations}). %, page \pageref{append-equations}).
As in the \{\emph{len}\} theorem, there are two \{\emph{append}\} equations,
which specify the meaning of the append operation in different situations.
One of them specifies the meaning when the first operand is a nonempty list,
the other specifies the meaning under all other circumstances.

\begin{figure}
%\begin{center}
\begin{tabular}{ll}
\multicolumn{2}{c}{Axioms \{\emph{append}\}} \\
\hline
\textsf{(append (cons $x$ $xs$) $ys$)} $=$ \textsf{(cons $x$ (append $xs$ $ys$))} & \{\emph{app1}\} \\
\textsf{(append nil $ys$)} $=$  $ys$                                     & \{\emph{app0}\} \\
\end{tabular}
%\end{center}
\index{axiom!append}\index{equation!append}\index{operator, by name!append}\index{append!operator}\index{concatenate}\index{equation, by name!\{app0\}, \{app1\}}\index{axiom, by name!\{app0\}, \{app1\}}
\caption{List concatenation: \textsf{append}.}
\label{append-equations}
\end{figure}
%\todo{Note 12/10/17, see also fig: Defining Concatenation
%      Not sure what to do here. Had the following for app0 axiom, with note:
%(append ~$e$~ $ys$) =  $ys$                                   & \{\emph{app0}\} \\
%~~~~\emph{Note: Cite \{\emph{app0}\} only if \{\emph{app1}\} doesn't match.}&\\
%      However, the ACL2 documentation requires first operand of append to be a truelist,
%      even though ACL2 with guards off allows it to violate that constraint.
%      For now (and it's late in the game), going back to the constraint.
%      Before reverting, the following comment stood here:
%      These axioms allow non-true-lists as first operand. However, when guards are in effect,
%      ACL2 chokes if first operand isn't a true list.
%      When guards are disabled (append 1 (list 2 3)) = (list 2 3)
%      I don't want to say anything about guards, but students may see error messages
%      that talk about guards. Not sure how to handle this.
%      }

These equations state simple properties of the \textsf{append} operation,
and it turns out that lots of other properties of the
\textsf{append} operation can be derived from them.
For example, we can prove that the length of
the concatenation of two lists is the sum of the lengths of the lists,
as tested by a DoubleCheck property in
chapter~\ref{ch:software-testing-prefix-notation} (page \pageref{additive-lengths-test}).
We call this theorem the \emph{additive law of concatenation}.
Let's see how a proof of this law could be carried out.

First, let's break it down into some special cases.
We will use L($n$) as shorthand for the proposition that
\textsf{(len (append [$x_1$ $x_2$ \dots $x_n$] $ys$))}
is the sum of \textsf{(len [$x_1$ $x_2$ $\dots$ $x_n$])} and \textsf{(len $ys$)}.
That makes L a predicate whose universe of discourse is
the natural numbers.
\label{additive-concat-law-predicate}
\begin{center}
% old prefix notation: \begin{tabbing}
% old prefix notation: L($n$) $\equiv$ (= \=(len (append [$x_1$ $x_2$ \dots $x_n$] $ys$))  \\
% old prefix notation:                   \>(+ (len [$x_1$ $x_2$ \dots $x_n$]) (len $ys$)))
% old prefix notation: \end{tabbing}
L($n$) $\equiv$ \textsf{(len (append [$x_1$ $x_2$ $\dots$ $x_n$] $ys$))} $=$
\textsf{(+ (len [$x_1$ $x_2$ $\dots$ $x_n$]) (len $ys$))}
\end{center}

For the first few values of $n$, L($n$) would stand for the following equations:\\
\hspace*{1cm}L(0) $\equiv$ \textsf{(len (append nil $ys$))} $=$ \textsf{(+ (len nil) (len $ys$))} \\
\hspace*{1cm}L(1) $\equiv$ \textsf{(len (append [$x_1$] $ys$))} $=$ \textsf{(+ (len [$x_1$]) (len $ys$))} \\
\hspace*{1cm}L(2) $\equiv$ \textsf{(len (append [$x_1$ $x_2$] $ys$))} $=$ \textsf{(+ (len [$x_1$ $x_2$]) (len $ys$))} \\
\hspace*{1cm}L(3) $\equiv$ \textsf{(len (append [$x_1$ $x_2$ $x_3$] $ys$))} $=$ \textsf{(+ (len [$x_1$ $x_2$ $x_3$]) (len $ys$))} \\
%\hspace*{1cm}L(4) $\equiv$ \textsf{(len (append [$x_1$ $x_2$ $x_3$ $x_4$] $ys$))} $=$ \textsf{(+ (len [$x_1$ $x_2$ $x_3$ $x_4$]) (len $ys$))}\\

%\todo{COMMENT ONLY, NO TODO
%in case we want to go back to the prefix =
%\begin{center}
%\begin{tabular}{llll}
%L(0) & $\equiv$ & \textsf{(=} &\textsf{(len (append nil $ys$))} \\
%     &          &    &\textsf{(+ (len nil) (len $ys$)))} \\
%L(1) & $\equiv$ & \textsf{(=} &\textsf{(len (append [$x_1$] $ys$))} \\
%     &          &    &\textsf{(+ (len [$x_1$]) (len $ys$))}) \\
%L(2) & $\equiv$ & \textsf{(=} &\textsf{(len (append [$x_1$ $x_2$] $ys$))}\\
%	 &          &    &\textsf{(+ (len [$x_1$ $x_2$]) (len $ys$)))} \\
%L(3) & $\equiv$ & \textsf{(=} &\textsf{(len (append [$x_1$ $x_2$ $x_3$] $ys$))} \\
%     &          &    &\textsf{(+ (len [$x_1$ $x_2$ $x_3$]) (len $ys$)))} \\
%L(4) & $\equiv$ & \textsf{(=} &\textsf{(len (append [$x_1$ $x_2$ $x_3$ $x_4$] $ys$))} \\
%     &          &    &\textsf{(+ (len [$x_1$ $x_2$ $x_3$ $x_4$]) (len $ys$)))}
%\end{tabular}
%\end{center}
%END OF TODO COMMENT}

We can derive L(0) from the \{\emph{append}\} and \{\emph{len}\} axioms as follows.
We start from the left-hand side of the equation that L(0) stands for and
cite some axioms about \textsf{append}, \textsf{len}, and numeric algebra,
one by one. We end up with the right-hand side of the equation L(0).
\begin{center}
\begin{tabular}{lll}
\multicolumn{3}{c}{\emph{Proof of L(0), citing axioms}}\\
\hline
    & \textsf{(len (append nil $ys$))}  &                                                \\
$=$ & \textsf{(len $ys$)}               & \{\emph{app0}\}     (page \pageref{append-equations})\\
$=$ & \textsf{(+ (len $ys$) 0)}         & \{$+$ identity\}    (page \pageref{fig-02-01}) \\
$=$ & \textsf{(+ 0 (len $ys$))}         & \{$+$ commutative\} (page \pageref{fig-02-01}) \\
$=$ & \textsf{(+ (len nil) (len $ys$))} & \{\emph{len0}\}     (page \pageref{len-equations})
\end{tabular}
\end{center}

That takes care of L(0). How about L(1)?
\begin{center}
\begin{tabular}{lll}
\multicolumn{3}{c}{\emph{Proof of L(1), citing axioms and proven equations}}\\
\hline
    & \textsf{(len (append [$x_1$] $ys$))}           &                     \\
$=$ & \textsf{(len (append (cons $x_1$ nil) $ys$))}  & \{\emph{cons}\} (page \pageref{first-rest-cons}) \\
$=$ & \textsf{(len (cons $x_1$ (append nil $ys$)))}  & \{\emph{app1}\}     \\
$=$ & \textsf{(+ 1 (len (append nil $ys$)))}         & \{\emph{len1}\}     \\
$=$ & \textsf{(+ 1 (+ (len nil) (len $ys$)))}        & \{L(0)\} ~~~~\emph{Note: L(0) already proved}\\
$=$ & \textsf{(+ (+ 1 (len nil)) (len $ys$))}        & \{$+$ associative\} (page \pageref{fig-02-01}) \\
$=$ & \textsf{(+ (len (cons $x_1$ nil)) (len $ys$))} & \{\emph{len1}\}     \\
$=$ & \textsf{(+ (len [$x_1$]) (len $ys$))}          & \{\emph{cons}\}     \\
\end{tabular}
\end{center}
That was a little harder. Will proving L(2) be still harder? Let's try it.
\begin{center}
\begin{tabular}{lll}
\multicolumn{3}{c}{\emph{Proof of L(2), citing axioms and proven equations}}\\
\hline\\[-1.0em]
    & \textsf{(len (append [$x_1$ $x_2$] $ys$))}         &                     \\
$=$ & \textsf{(len (append (cons $x_1$ [$x_2$]) $ys$))}  & \{\emph{cons}\}     \\
$=$ & \textsf{(len (cons $x_1$ (append [$x_2$] $ys$)))}  & \{\emph{app1}\}     \\
$=$ & \textsf{(+ 1 (len (append [$x_2$] $ys$)))}         & \{\emph{len1}\}     \\
$=$ & \textsf{(+ 1 (+ (len [$x_2$]) (len $ys$)))}        & \{L(1)\} ~~~~\emph{Note: L(1) already proved}\\
$=$ & \textsf{(+ (+ 1 (len [$x_2$])) (len $ys$))}        & \{$+$ associative\} \\
$=$ & \textsf{(+ (len (cons $x_1$ [$x_2$])) (len $ys$))} & \{\emph{len1}\}     \\
$=$ & \textsf{(+ (len [$x_1$ $x_2$]) (len $ys$))}        & \{\emph{cons}\}     \\
\end{tabular}
\end{center}
Proving L(2) was no harder than proving L(1).
In fact, the two proofs cite exactly the same equations all the way through
except in one place.
Where the proof of L(1) cited the equation L(0),
the proof of L(2) cited the equation L(1).
Maybe the proof of L(3) will work the same way.
\begin{center}
\begin{tabular}{lll}
\multicolumn{3}{c}{\emph{Proof of L(3), citing axioms and proven equations}}\\
\hline\\[-1.0em]
    & \textsf{(len (append [$x_1$ $x_2$ $x_3$] $ys$))}         &                     \\
$=$ & \textsf{(len (append (cons $x_1$ [$x_2$ $x_3$]) $ys$))}  & \{\emph{cons}\}     \\
$=$ & \textsf{(len (cons $x_1$ (append [$x_2$ $x_3$] $ys$)))}  & \{\emph{app1}\}     \\
$=$ & \textsf{(+ 1 (len (append [$x_2$ $x_3$] $ys$)))}         & \{\emph{len1}\}     \\
$=$ & \textsf{(+ 1 (+ (len [$x_2$ $x_3$]) (len $ys$)))}        & \{L(2)\} ~~~~\emph{Note: L(2) already proved}\\
$=$ & \textsf{(+ (+ 1 (len [$x_2$ $x_3$])) (len $ys$))}        & \{$+$ associative\} \\
$=$ & \textsf{(+ (len (cons $x_1$ [$x_2$ $x_3$])) (len $ys$))} & \{\emph{len1}\}     \\
$=$ & \textsf{(+ (len [$x_1$ $x_2$ $x_3$]) (len $ys$))}        & \{\emph{cons}\}     \\
\end{tabular}
\end{center}

\label{induction-rationale}\index{induction!rationale}\index{induction!proof by}
By now it's easy to see how to derive L(4) from L(3),
then L(5) from L(4), and so on.
If you had the patience, you could prove L(100), L(1000), or even L(1000000)
by following the established pattern.
It would not be hard to write a program to print out the proof of L($n$)
given any natural number $n$.
Since we know how to prove L($n$) for any natural number $n$,
it seems fair to say that we know all those equations are true.
That is, we think we know that the formula ($\forall$$n$.L($n$)) is true.
However, to prove that in a formal sense,
we need a rule of inference that allows us to make conclusions
from patterns like those we observed in proving L(1), L(2), and so on.
That rule of inference is known as \emph{mathematical induction}.

\seeonlyindex{mathematical induction}{induction}\index{induction!proof by}Mathematical induction
provides a way to prove that
formulas like ($\forall$$n$.P($n$)) are true
when P is a predicate whose universe of discourse is the natural numbers.
If for each natural number $n$, P($n$) stands for a proposition,
then mathematical induction is an inference rule that may be useful
in a proof that ($\forall$$n$.P($n$)) is true.
That is not to say that such a proof can always be constructed.
It's just that mathematical induction might provide some help in the process.
The inverse is also true: mathematical induction cannot help
if the universe of discourse is not the natural numbers.\footnote{Mathematical
induction is not the only form
of proof by induction, but all the other forms
(other than transfinite induction, which is a different animal)
can be contorted into proofs by mathematical induction.
We will stick with classical mathematical induction
and leave the variations for another time.
They are easy to learn for people who understand ordinary mathematical induction.}

The rule goes as follows. Infer the truth of ($\forall$$n$.P($n$)),
citing \{induction\} as a rule of inference,
from proofs of two propositions:
P(0) and $(\forall n.($P($n$) $\rightarrow$ P($n+1$)$))$.
\begin{center}
$(($P($0$) $\wedge$ $(\forall n.($P($n$) $\rightarrow$ P($n+1$)$)))$ $\rightarrow$ $(\forall n.$P($n$)$))$ $=$ $True$
~~~\{induction\}
\end{center}
%\begin{center}
%\begin{tabular}{lll}
%\emph{Prove:} & P($0$)                                      &     \emph{base case}\\
%\emph{Prove:} & ($\forall$$n$.(P($n$)$\rightarrow$P($n+1$)))&\emph{inductive case}\\
%              &---------------------------------------------& \\
%\emph{Infer:} & ($\forall$$n$.P($n$))                    & \emph{citing} \{induction\}\\
%\end{tabular}
%\end{center}

It's a very good deal if you think about it.
A direct proof of ($\forall$$n$.P($n$)) would require a proof of proposition P($n$)
for each value of $n$ ($0$, $1$, $2$, \dots).
But, in a \index{proof!by induction}proof by \index{induction!proof by}induction,
the only proposition that needs to be proved on its own is P($0$).
To justify any step in the proof of proposition P($n+1$)
(that is, any proposition in the predicate P with a nonzero index:
P($1$), P($2$), P($3$), \dots),
you are allowed to cite P($n$) as if it were a known theorem.
The proof of P($0$) is known as the
\seeonlyindex{base case}{induction}\index{induction!base case}\emph{base case}
in the proof by induction,
and the proof of (P($n$) $\rightarrow$ P($n+1$)) is known as the
\seeonlyindex{inductive case}{induction}\index{induction!inductive case}\emph{inductive case}.

The reason you can assume that P($n$) is true in the proof of P($n+1$)
(that is, in the inductive case)
is because the goal, according to part two of the inference rule
for induction, is to prove that the implication
P($n$)$\rightarrow$P($n+1$) is true.
When P($n$) is false, we know already from the truth table
of the implication operator (page \pageref{implication-truth-table})
that the implication P($n$)$\rightarrow$P($n+1$) is true.
There is no need to prove that again.
Therefore, in the proof of P($n+1$), we can assume P($n$) is true.
The assumption of P($n$) is known as the
\index{hypothesis!induction}\index{induction!hypothesis}\emph{induction hypothesis}.
It gives you a leg up in the proof of P($n+1$).

Figure~\ref{induction-rule} states the \{induction\} inference rule
in the form of natural deduction, a formal method of logic discussed
in section~\ref{sec:deduction}. You don't need to have studied that
section to understand inductive proofs, but in case you did study
natural deduction, figure~\ref{induction-rule} puts proof by
induction in that context.

\begin{figure}
%\begin{center}
\begin{spacing}{0.9}
\begin{tabular}{ll}
Prove P(0)                                         &\emph{base case}\\
 - - - - - - - - - - - - - - - - - - - - -         &\\
Prove ($\forall$$n$.(P($n$)$\rightarrow$P($n+1$))) &\emph{inductive case}\\
-------------------------------------\{induction\} &\\
Infer ($\forall$$n$.P($n$))                        &\\
\end{tabular}
\end{spacing}
%\end{center}
\caption{Mathematical induction: a rule of inference.}
\label{fig-04-01}\label{induction-rule}\index{induction!proof by}\index{proof!by induction}\index{inference rule, by name!\{induction\}}\index{induction!inference rule}
\end{figure}

\label{induction-hyp-def}Now,
let's apply mathematical induction to prove
the additive law of concatenation.
Here, the predicate that we will apply the method to is L
(page \pageref{additive-concat-law-predicate}).
\label{len-additive-thm}We
have already proved L(0), so we have already completed one of the
two proofs required to cite the mathematical induction inference rule.
All that is left is to prove ($\forall$$n$.(L($n$)$\rightarrow$L($n+1$))).
That is, we have to derive L($n+1$) from L($n$) for an arbitrary natural number $n$.
Fortunately, we know how to do this. Just copy the derivation of,
say, L(3) from L(2), but start with an append formula in which the first operand
is a list with $n+1$ elements and cite L($n$) where we would have cited L(2).
\begin{center}
\begin{tabular}{lll}
\multicolumn{3}{c}{\emph{Proof of L(n+1), citing axioms, proven equations, and L(n): L(n) $\rightarrow$ L(n+1)}}\\
\hline\\[-1.0em]
    & \textsf{(len (append [$x_1$ $x_2$ \dots $x_{n+1}$] $ys$))}         &\\
$=$ & \textsf{(len (append (cons $x_1$ [$x_2$ \dots $x_{n+1}$]) $ys$))}  & \{\emph{cons}\}\\
$=$ & \textsf{(len (cons $x_1$ (append [$x_2$ \dots $x_{n+1}$] $ys$)))}  & \{\emph{app1}\}\\
$=$ & \textsf{(+ 1 (len (append [$x_2$ \dots $x_{n+1}$] $ys$)))}         & \{\emph{len1}\}\\
$=$ & \textsf{(+ 1 (+ (len [$x_2$ \dots $x_{n+1}$]) (len $ys$)))}        & \{L($n$)\} ~~\emph{Note: induction hypothesis}\\
$=$ & \textsf{(+ (+ 1 (len [$x_2$ \dots $x_{n+1}$])) (len $ys$))}        & \{$+$ associative\}\\
$=$ & \textsf{(+ (len (cons $x_1$ [$x_2$ \dots $x_{n+1}$])) (len $ys$))} & \{\emph{len1}\}\\
$=$ & \textsf{(+ (len [$x_1$ $x_2$ \dots $x_{n+1}$]) (len $ys$))}        & \{\emph{cons}\}\\
\end{tabular}
\end{center}
\vspace*{5mm}
This completes the mathematical induction proving the
additive law of concatenation.

\begin{center}
\index{append!additive law}\index{theorem, by name!\{additive law of concatenation\}}\index{additive law of concatenation}\index{concatenate!additive law}\label{additive-law-concatenation}
\begin{tabular}{c}
Theorem \{\emph{additive law of concatenation}\} \\
\hline
$\forall n.($\textsf{(len (append [$x_1$ $x_2$ $\dots$ $x_n$] $ys$))}
$=$ \textsf{(+ (len [$x_1$ $x_2$ \dots $x_n$]) (len $ys$))}$)$\\
\end{tabular}
\end{center}

An important point to notice in this proof is that
we could not cite the \{\emph{cons}\} equation to replace \textsf{[$x_2$ $\dots$ $x_{n+1}$]}
with \textsf{(cons $x_2$ [$x_3$ $\dots$ $x_{n+1}$])}.
The reason we could not do this is that we are trying to derive
L($n+1$) from L($n$) without making any assumptions about $n$
other than the fact that it is a natural number.
Since zero is a natural number, the list \textsf{[$x_2$ $\dots$ $x_{n+1}$]}
could be empty,\footnote{The list [$x_2$ $\dots$ $x_{0+1}$] is empty
(\{\emph{nlst}\} numbered list notation,
figure~\ref{numbered-list-interpretation}, page \pageref{numbered-list-interpretation}).}
and the \textsf{cons} operator cannot deliver an empty list as its value.

In the next section, we will prove several properties of \textsf{append}
and its relationships with other operators.
These properties, and in fact all properties of the \textsf{append} operator,
can be derived from the \{\emph{append}\} axioms
(figure~\ref{append-equations}, page \pageref{append-equations}).
Those axioms state properties of the \textsf{append} operation
in two separate cases:
(1)~\{\emph{app0}\}: the first operand is the empty list and
(2)~\{\emph{app1}\}: the first operand is a nonempty list.
When the first operand is the empty list,
the result must be the second operand, no matter what.
When the first operand is not empty, it must have a first element,
and that element must be the first element of the concatenation.
The other elements of the concatenation are the ones you would get
if you appended the second operand to the rest of the first operand.

Both of these properties are so straightforward and easy to believe
that we would probably be willing to accept them as axioms with no proof at all,
so it might seem surprising that all of the other properties
of the \textsf{append} operation can be derived from
the two simple properties \{\emph{app0}\} and \{\emph{app1}\}.
That is the power of mathematical induction.
The two equations of the \{\emph{append}\} axioms
amount to an inductive definition of the \textsf{append} operator.

An inductive definition is circular in the sense
that some of the equations in the definition refer
to the operator on both sides of the equation.
Most of the time, people think of circular definitions
as unhelpful at best,
but they can be useful in mathematics.
You will see a lot of them and
gradually learn how to recognize and create useful,
circular (that is, inductive) definitions.

\begin{figure}
\begin{center}
\begin{tabular}{lp{3.5in}}
\emph{Complete} & All possible combinations of operands are covered by at least one equation in the definition. \\
\emph{Consistent} & Combinations of operands covered by two or more equations define the same value for the operation. \\
\emph{Computational} &
\begin{enumerate}
\item \emph{Noninductive Equation}: In at least one equation,
the operator being defined appears only on the left-hand side.
\item \emph{Reduced Computation}:
\index{three C's}\index{definition!inductive (circular)}On the right-hand side of an inductive equation,
each invocation of the operator being defined has operands that
are closer to the operands on the left-hand side of a noninductive equation
than to those on the left-hand side of the inductive equation.
\end{enumerate}
\end{tabular}
\end{center}
\vspace*{-6mm}
\caption{The three C's: a guide to inductive definitions.}
\label{fig:inductive-def-keys}
\end{figure}

It turns out that all operators that can be defined in
\index{software!as equations}\index{equation!software}software
have inductive definitions in the manner of the equations
of the \{\emph{append}\} axioms.
The keys to an inductive definition of an operator are  listed in
figure~\ref{fig:inductive-def-keys}. % (page \pageref{fig:inductive-def-keys}).
All of the software we will discuss will take the form of
inductive definitions of operators.
That makes it possible to use mathematical induction as
a fundamental tool in verifying, to a logical certainty,
properties of that software.

\begin{exercises}

\exer {Prove $\forall xs.$\textsf{(natp (len $xs$))}.
You may
cite\index{equation, by name!\{natp0\}, \{natp1\}}\index{axiom, by name!\{natp0\}, \{natp1\}}
\{natp0\} and \{natp1\},
defined as follows. (\emph{Note}: This definition will be adequate for this exercise but it is not the full definition of \textsf{natp}.)
\begin{center}
\begin{tabular}{ll}
\textsf{(natp 0)}                                            & \{natp0\}\\
$\forall x.($\textsf{(natp $x$)} $\rightarrow$ \textsf{(natp (+ $x$ 1))}$)$ & \{natp1\}\\
\hline
\multicolumn{2}{c}{$\forall x$ \emph{universe of discourse: numbers}}\\
\end{tabular}
\end{center}}

\exer {Prove: $\forall n.(\forall x.($\textsf{(expt $x$ $n$)} $=$ $x^n))$~~~\{\emph{expt}\}\\
$\forall n$ universe of discourse: natural numbers;
$\forall x$ universe of discourse: non-zero numbers\\
Assume the equations \{\emph{expt0}\} and \{\emph{expt1}\} are true.
\label{expt-equations}\label{expt-thm}\index{theorem, by name!\{expt\}}\index{axiom!exponent}\index{operator, by name!expt ($x^n$)}\seeonlyindex{expt}{operator}\index{axiom, by name!\{expt0\}, \{expt1\}}\index{equation, by name!\{expt0\}, \{expt1\}}
\begin{center}
\begin{tabular}{ll}
\textsf{(expt $x$ 0)} $=$ 1                                         & \{\emph{expt0}\} \\
\textsf{(expt $x$ (+ $n$ 1))} $=$ \textsf{($*$ $x$ (expt $x$ $n$))} & \{\emph{expt1}\} \\
\hline
\multicolumn{2}{c}{{\textsf{($*$ $x$ $y$)} $=$ $x \times y$}}\\
\end{tabular}
\end{center}
}

\end{exercises}

\section{Defun: Defining Operators in ACL2}
\label{sec:defun}

Now, we are going to let you in on a little secret.
The axioms we wrote for the \textsf{append} operator are very
close to an ACL2 definition of \textsf{append}.
Operators are defined in ACL2 with a \textsf{defun} command,
which has four \index{defun}\index{definition!defun}\index{definition!operator}\index{operator!defun}parts.
\vspace{2mm}

\begin{tabular}{ll}
\multicolumn{2}{c}{\textsf{(defun $f$ ($x_1$ $x_2$ $\dots$ $x_n$) $formula$)}}\\
\hline
\textsf{defun}                       & keyword\\
$f$                                  & name for the operator being defined\\
\textsf{($x_1$ $x_2$ $\dots$ $x_n$)} & names designating operands, surrounded by parentheses\\
$formula$                            & ACL2 formula specifying the value the operator will deliver\\
\end{tabular}
\\

Most of the time, the formula for the value the operator delivers
will have subformulas specifying alternative values for different cases.
Formulas interpreted as predicates select one of
the subformulas to compute the value.

In section \ref{sec:induction} (figure~\ref{append-equations}, page \pageref{append-equations}),
we defined the \textsf{append} operator with two equations,
one for the case when the first operand was a nonempty list
and the other for all other possibilities.
The ACL2 definition, following that pattern, has two subformulas,
one for each case.
The \textsf{if} operator (figure~\ref{fig:if-axioms}, page \pageref{fig:if-axioms})
selects the appropriate formula.

\begin{aside}{aside:why-inductive}{Why Inductive Definitions?}
\index{why inductive?}\index{definition!why inductive?}\index{inductive, why?}Inductive
definitions are one of many ways to specify software,
and other methods are more common in practice.
However, proving properties of software written using conventional methods
is clumsy at best, especially in the framework of classical logic.
So, in terms of understanding what computers do and how they do it,
inductive definitions provide solid footing.
Since reasoning is a central theme in this presentation,
it focuses on software written
in the form of inductive equations.
%\caption{Why Inductive Definitions?}
%\label{aside:why-inductive}
\end{aside}

Figure~\ref{fig:append-defun} (page \pageref{fig:append-defun})
repeats the axioms for the \textsf{append} operator from
figure~\ref{append-equations} (page \pageref{append-equations})
and also displays a definition of \textsf{append} using \textsf{defun},
which expresses the axioms in ACL2 notation.
As it happens, the \textsf{append} operator is an ACL2 intrinsic.
It is defined by the ACL2 system, so the definition
in figure~\ref{fig:append-defun} is redundant,
and the ACL2 system will tell you that if you try to define it.
Shortly, we will begin to define operators that are not
intrinsic, so those definitions won't be redundant.
This familiar example is just
a starting point to get on the right track.

\begin{figure}
\begin{center}
\begin{tabular}{ll}
\multicolumn{2}{c}{Axioms \{\emph{append}\}} \\
\hline
\textsf{(append (cons $x$ $xs$) $ys$)} $=$ \textsf{(cons $x$ (append $xs$ $ys$))} & \{\emph{app1}\} \\
\textsf{(append nil $ys$)} $=$  $ys$                                     & \{\emph{app0}\} \\
\end{tabular}
\begin{code}
\begin{verbatim}
(defun append (xs ys)    ; intrinsic operator, so defun is redundant
  (if (consp xs)                              ; select formula
      (cons (first xs) (append (rest xs) ys)) ; {app1}, xs not empty
      ys))                                    ; {app0}, xs is empty
\end{verbatim}
\end{code}
\end{center}
%Reverting to 2nd axiom requiring first arg to be truelist, as req'd in acl2 docuemtation.%'
%Was as follows:
%(append $a$ $ys$) =  $ys$                                     & \{\emph{app0}\} \\
%~~~~\emph{Note: Cite \{\emph{app0}\} only if \{\emph{app1}\} doesn't match.}&\\%'
\index{axiom!append}\index{append!operator}\index{operator, by name!append}\index{axiom, by name!\{app0\}, \{app1\}}\index{equation, by name!\{app0\}, \{app1\}}
\caption{Defining concatenation: \textsf{append}.}
\label{fig:append-defun}
\end{figure}

So, now you
\index{software!as axioms}\index{programs, as axioms}\index{axiom!software}\index{equation!software}know.
We've been writing programs on the sly, passing them off as axioms.
Why? Because that's how we want you to think of them.
A program is a collection of axioms expressed as equations
that specify properties that you want operators to have.
You can reason from those equations using the same methods
you have used in reasoning about Boolean equations or numeric equations.
The program is written in the syntax of a programming language,
which makes it look a bit stilted.
That is always the case in programming languages because
they have their own syntax, and you have to conform to it.
It pays off, though.
If you stick with the program, you can get the computer to carry out
computations, and you will have some confidence in the results
of those computations.

Since definitions must use the \index{equation!ACL2}\index{ACL2!equation}ACL2 syntax,
they don't look much like equations, %'
but if they are complete, consistent, and computational
(figure~\ref{fig:inductive-def-keys}, page \pageref{fig:inductive-def-keys}),
the values they deliver will have the properties you derive
from the equations.
They may not have all the properties you expected.
They may have bugs.
But you'll have a good chance of fixing them with %'
automated testing (\textsf{defproperty})
and the reasoning assistance of the ACL2 mechanized logic.

Going forward, we will define operators that aren't %'
intrinsic in ACL2 (and, therefore, need definitions)
both in the form of an ACL2 \textsf{defun}
and in the form of equations for paper-and-pencil reasoning.
The corresponding ACL2 definitions
make it possible to apply automated testing and mechanized logic
to confirm some of the properties of those operators.
When the operators we are discussing are intrinsic,
we will sometimes not provide \textsf{defun} versions of them,
just axioms for paper-and-pencil reasoning.
Automated testing and mechanized logic will make use
of their intrinsic definitions in the ACL2 system.

\section{Concatenation, Prefixes, and Suffixes}
\label{sec:append-prefix-suffix}
%%% in this section, prove the correctness of append
%%% with respect to a (prefix n xs) operator and (nthcdr n xs).

If you concatenate two lists, $xs$ and $ys$,
you would expect to be able to retrieve the elements
of $ys$ by dropping some of the elements of the concatenated lists.
How many elements would you need to drop?
That depends on the number of elements in $xs$.
If there are $n$ elements in $xs$ and you drop $n$ elements
from \textsf{(append $xs$ $ys$)}, you expect the result to be identical
to the list $ys$. To express that expectation, we can use
an intrinsic operator in ACL2 with the arcane name \textsf{nthcdr}.
The \textsf{nthcdr} operator has two operands: a natural number and a list.
The formula \textsf{(nthcdr $n$ $xs$)} delivers a list like $xs$
but without its first $n$ elements.
If $xs$ has fewer than $n$ elements,
then the formula delivers the empty list.
In any case, \textsf{nthcdr} delivers a suffix of the list
supplied as its second operand.

If the first operand (the number of elements to be dropped) is zero,
you would expect
\textsf{nthcdr} to deliver the entire list, having dropped no elements.
If the second operand has no elements,
you would expect
\textsf{nthcdr} to deliver a list just like that
(that is, a list with no elements).
Combining these two observations, we find that
$xs$ would be the appropriate value for \textsf{(nthcdr $n$ $xs$)}
if either $n$ is zero or $xs$ has no elements.

\begin{aside}{zp-def}{Natural Number Predicates: Zero (\textsf{zp}) and Nonzero (\textsf{posp})}
The predicate \textsf{posp} is used to test for nonzero values
in the domain of natural numbers.
In the ACL2 logic, the formula \textsf{(posp $n$)} has the value true if $n$ is
a nonzero, natural number (that is, a strictly positive integer).
The value of \textsf{(posp $n$)} is false if $n$ is not a natural number
or if $n$ is zero.
That makes \textsf{posp} especially useful
in definitions that are inductive on the natural numbers.
You might think that \textsf{(> $n$ 0)} would
work the same way but it doesn't because that formula %'
does not constrain $n$ to the natural numbers,
and many inductive definitions rely on that constraint.

The predicate \textsf{zp} imposes the same constraint,
but it is true when its operand is zero and false otherwise.
Both \textsf{zp} and \textsf{posp} are useful for inductive definitions that
rely on the domain of natural numbers to ensure that the defined operator
terminates.\index{operator, by name!posp (\emph{see} predicate)}\index{predicate, by name!posp (positive integer)}\seeonlyindex{posp}{predicate}\index{operator, by name!zp (\emph{see} predicate)}\index{predicate, by name!zp (natural number zero)}\seeonlyindex{zp}{predicate}
%\caption{Natural Number Predicates: Zero (\textsf{zp}) and Non-Zero (\textsf{posp})}
%\label{zp-def}
\end{aside}

The other possibility is that $n$ is not zero and $xs$ has some elements.
Since the first operand is a natural number,
being nonzero is the same as being one or more.
In that case you would expect \textsf{(nthcdr $n$ $xs$)} to deliver
the same list that it would deliver
if you dropped the first element of $xs$
and then, in addition, dropped $(n - 1)$ more elements.
Together, these two actions would drop $n$ elements.
The axioms in figure~\ref{fig:nthcdr-defun} (page \pageref{fig:nthcdr-defun})
express these observations as equations.

The figure also contains an ACL2 definition of \textsf{nthcdr}, which
is of course redundant because \textsf{nthcdr} is intrinsic in ACL2.\footnote{If
you submit a definition of \textsf{nthcdr},
the system will inform you of the redundancy.}
The definition uses the predicate \textsf{consp}
(figure~\ref{consp-axiom}, page \pageref{consp-axiom})
to find out whether the list contains some elements and
uses the predicate
\label{posp-def} \textsf{posp}
to determine whether
the number of elements to be dropped is one or more.
It combines these predicates with the \textsf{and} operator,
which is the ACL2 notation for the logical-and ($\wedge$).
\label{and-op=informal}
The value \textsf{(and $a$ $b$)} is false (nil)
if either $a$ or $b$ is false and true otherwise.

\begin{figure}
\begin{center}
\begin{tabular}{ll}
\multicolumn{2}{c}{Axioms \{\emph{nthcdr}\}} \\
\hline
\textsf{(nthcdr $(n+1)$ (cons $x$ $xs$))} $=$ \textsf{(nthcdr $n$ $xs$)} & \{\emph{sfx1}\} \\
\textsf{(nthcdr $n$ $xs$)} $=$ $xs$                            & \{\emph{sfx0}\}   \\
~~~~\emph{Note 1: Cite }\{\emph{sfx0}\}\emph{ only if }\{\emph{sfx1}\}\emph{ doesn't match.}&\\ %'
~~~~\emph{Note 2: $n$ is a natural number.}
\end{tabular}
\begin{code}
\begin{verbatim}
(defun nthcdr (n xs)    ; intrinsic operator, so defun is redundant
  (if (and (posp n) (consp xs))   ; select formula
      (nthcdr (- n 1) (rest xs))  ; {sfx1}
      xs))                        ; {sf0}
\end{verbatim}
\end{code}
\end{center}
\seeonlyindex{nthcdr}{operator}\index{operator, by name!nthcdr (suffix of list)}\index{axiom, by name!\{sfx0\}, \{sfx1\}}\index{equation, by name!\{sfx0\}, \{sfx1\}}
\caption{Defining list suffix extractor: \textsf{nthcdr}.}
\label{fig:nthcdr-defun}
% old label for nthcdr axioms: \label{nthcdr-equations}
\end{figure}

% NEW COMMENT 12-10-17 Not sure what the problem was before
%                      so maybe Ruben should look at it to make sure it's not wrong.
% FIXED NOW, REX THINKS as of 5SEP2017
% Rex: sfx1 isn't true, right?
% I'm not sure we want to introduce it as an axiom, if later we'll have to explain it isn't really true.
% Ruben: left as is for now, with (natp n) implicit, but inserted a comment about the type of n
% Updte (Rex 5Sep 2017: I think it's fixed, now.
%%%% error below

The equations in figure~\ref{fig:nthcdr-defun} cover all combinations
of values that the operands of \textsf{nthcdr} can have.
The first operand is a natural number,
so it's either zero or bigger than zero.
The second operand, a list, either has some elements or it doesn't.
So the definition is complete, having covered all the cases.
The cases do not overlap, so we don't need to worry about
consistency between the axioms.

\begin{aside}{fig:fall-through-axioms}{Fall-Through Axioms}
There is a subtlety in the axioms for \textsf{nthcdr} (figure~\ref{fig:nthcdr-defun})
that needs to be discussed.
The operand prototypes in the
\{\emph{sfx1}\} axiom match whenever the first operand is a nonzero natural number
($n+1$ cannot be zero when $n$ is a natural number)
and the second operand is a nonempty list.
However, the operand prototypes in the \{\emph{sfx0}\} axiom match anything.
There is a note restricting
citations of the second axiom to cases
where the first axiom does not apply.
The definition of the \textsf{len} operator
had a fall-through axiom like this too
(figure~\ref{fig:len-axioms}, page \pageref{fig:len-axioms}).

Usually we state axioms with operand prototypes that constrain
the operands to specific forms,
but in the case of \textsf{nthcdr}, Note 2 conforms to the meaning
of the \textsf{(if $p$ $a$ $b$)} formula, which chooses formula $b$
only if $p$ has the value \textsf{nil} (representing false).
Since \{\emph{sfx0}\} only applies if the operand prototypes in
\{\emph{sfx0}\} don't match the operands in a formula that refers to \textsf{nthcdr},
the two axioms do not share any combination of operands, so they cannot
cause an inconsistency in the specified results.
%\caption{Fall-Through Axioms}
%\label{fig:fall-through-axioms}
\end{aside}

That covers two of the three C's guidelines for inductive definitions of operators
(figure~\ref{fig:inductive-def-keys}, page \pageref{fig:inductive-def-keys}).
The equations are complete and consistent.
The third guideline (computational) has two parts, one of which is
a requirement that at least one axiom must be noninductive.
The \{\emph{sfx0}\} equation is not inductive because the \textsf{nthcdr} operator
is not invoked on the right-hand side of the equation.
In that case, \textsf{nthcdr} just delivers its second operand as is.
So, the axioms pass muster on that part of the computational guideline.

With regard to the inductive axiom \{\emph{sfx1}\},
the operands on the right-hand side of the equation are
smaller and shorter than the operands on the left-hand side,
which makes them closer to the noninductive case
since that axiom, \{\emph{sfx0}\}, will apply if either the first
operand is zero or the second one doesn't have any elements.
Therefore, the equations conform to the three C's guidelines,
and we can conclude that they define an operator.

At this point, we are in a position to verify the relationship
between the \textsf{append} and \textsf{nthcdr} operators that started this discussion.
Namely, we want to prove that if the lists $xs$ and $ys$ are concatenated
and then \textsf{(len $xs$)} elements are dropped from the beginning of the
concatenation, the result will be the list $ys$.
We will use S($n$) as a shorthand for this property
when $xs$ has $n$ elements.
\begin{center}
\label{append-suffix-thm-predicate}
S($n$) $\equiv$ $($\textsf{(nthcdr (len [$x_1$ $x_2$ $\dots$ $x_n$]) (append [$x_1$ $x_2$ $\dots$ $x_n$] $ys$))} $=$ $ys)$
\end{center}
%%error above
%\todo{COMMENT ONLY, NO TODO
%Just in case we decide to go back to ACL2 syntax for the def'n of S
%S($n$) $\equiv$ (equal & (nthcdr & (len [$x_1$ $x_2$ \dots $x_n$])          \\
%                       &         & (append [$x_1$ $x_2$ \dots $x_n$] $ys$)) \\
%                       & $ys$)   &                                          \\
%}
\label{append-suffix-thm-pencil-proof}
%\todo{COMMENT ONLY, NO TODO label added 16Sep2017}
S is a predicate indexed by the natural numbers,
so the formula $\forall n.$S$(n)$ is a candidate for proof by induction.
A proof of this formula by mathematical induction
(figure~\ref{induction-rule}, page \pageref{induction-rule})
requires two proofs:
(1)~the formula S(0) is true and
(2)~the formula S($n+1$) is true under the assumption that S($n$) is true,
regardless of what natural number $n$ stands for.

Let's do those two proofs.
First, we prove S(0).
When $n$ is zero, the list \textsf{[$x_1$ $x_2$ $\dots$ $x_n$]} is empty:
\textsf{[$x_1$ $x_2$ $\dots$ $x_0$]} $=$ \textsf{nil}, according to the \{\emph{nlst}\} axiom
(figure~\ref{numbered-list-interpretation}, page \pageref{numbered-list-interpretation}).
So, S(0) stands for the following equation:
\begin{center}
S(0) $\equiv$ $($\textsf{(nthcdr (len nil) (append nil $ys$))} $=$ $ys)$
\end{center}
%\todo{COMMENT ONLY, NO TODO
%Just in case we decide to go back to ACL2 syntax for the def'n of S
%\begin{samepage}
%\begin{center}
%\begin{tabular}{ll}
%S(0) $\equiv$ (equal & (nthcdr (len nil) (append nil $ys$)) \\
%                     & $ys$)                                \\
%\end{tabular}
%\end{center}
%\end{samepage}
%END OF COMMENT ONLY, NO TODO}
As usual in a proof of an equation,
we start with the formula on one side of the equation
and use known equations to gradually transform that formula
into the one on the other side.
\begin{center}
\begin{tabular}{lll}
    & \textsf{(nthcdr (len nil) (append nil $ys$))}  &                                                  \\
$=$ & \textsf{(nthcdr (len nil) $ys$)}               & \{\emph{app0}\} (page \pageref{fig:append-defun})\\
$=$ & \textsf{(nthcdr 0 $ys$)}                       & \{\emph{len0}\} (page \pageref{len-equations})   \\
$=$ & $ys$                                  & \{\emph{sfx0}\} (page \pageref{fig:nthcdr-defun})\\
\end{tabular}
\end{center}

That takes care of S(0). Figure~\ref{fig:append-suffix-induc-case}
(page \pageref{fig:append-suffix-induc-case})
displays a proof of S($n+1$), assuming that
the induction hypothesis S($n$) is true.
The last step in the proof is justified by citing S($n$).
This is a little tricky because the formula that S($n$)
stands for is not exactly the same as the formula in the next-to-last step of the proof.
We interpret the formula \textsf{[$x_1$ $x_2$ $\dots$ $x_n$]} in the definition of S($n$)
to stand for any list with $n$ elements.
The elements in the list \textsf{[$x_2$ $\dots$ $x_{n+1}$] }are numbered 2 through $n+1$,
which means there must be exactly $n$ of them
(\{\emph{nlst}\}, figure~\ref{numbered-list-interpretation}, page \pageref{numbered-list-interpretation}).
With this interpretation, the formula in the next-to-last step
matches the formula in the definition of S($n$),
which makes it legitimate to cite S($n$) to justify
the transformation to $ys$ in the last step of the proof.
We will cite axiom \{\emph{nlst}\}, the numbered-list interpretation,
frequently in proofs about lists.

\begin{figure}
\index{theorem, by name!\{append-suffix\}}\index{append!suffix theorem}
\begin{center}
%\begin{tabular}{lll}
S($n+1$) $\equiv$ $($\textsf{(nthcdr (len [$x_1$ $x_2$ $\dots$ $x_{n+1}$]) (append [$x_1$ $x_2$ $\dots$ $x_{n+1}$] $ys$))} $=$ $ys)$
%\end{tabular}
\end{center}

\begin{center}
\begin{tabular}{llll}
    & \textsf{(nthcdr} & \textsf{(len [$x_1$ $x_2$ $\dots$ $x_{n+1}$])}                 & \\
    &         & \textsf{(append [$x_1$ $x_2$ $\dots$ $x_{n+1}$] $ys$))}        & \\
$=$ & \textsf{(nthcdr} & \textsf{(len (cons $x_1$ [$x_2$ $\dots$ $x_{n+1}$]))}         & \{\emph{cons}\} (page \pageref{first-rest-cons}) \\
    &         & \textsf{(append (cons $x_1$ [$x_2$ $\dots$ $x_{n+1}$]) $ys$))} & \{\emph{cons}\}                                \\
$=$ & \textsf{(nthcdr} & \textsf{(+ 1 (len [$x_2$ $\dots$ $x_{n+1}$]))}                 & \{\emph{len1}\} (page \pageref{len-equations})       \\
    &         & \textsf{(cons $x_1$ (append [$x_2$ $\dots$ $x_{n+1}$]) $ys$))} & \{\emph{app1}\} (figure \ref{fig:append-defun}, page \pageref{fig:append-defun})\\
$=$ & \textsf{(nthcdr} & \textsf{(+ (len [$x_2$ $\dots$ $x_{n+1}$]) 1)}                 & \{$+$ commutative\} (page \pageref{fig-02-01})  \\
    &         & \textsf{(cons $x_1$ (append [$x_2$ $\dots$ $x_{n+1}$]) $ys$))} &                                                      \\
$=$ & \textsf{(nthcdr} & \textsf{(len [$x_2$ $\dots$ $x_{n+1}$])}                       & \{\emph{sfx1}\}                                      \\
    &         & \textsf{(append [$x_2$ $\dots$ $x_{n+1}$] $ys$))}              &                                                      \\
$=$ & $ys$    &                                                     & \{S($n$)\} (induction hypothesis)\\
\end{tabular}
\end{center}
\caption{Inductive case: S($n$) $\rightarrow$ S($n+1$).}
\label{fig:append-suffix-induc-case}
\end{figure}

At this point, we know that (append $xs$ $ys$) delivers
a list that has the right elements at the end.
How about the beginning?
We expect the concatenation to start with the elements of the list $xs$,
so if we extract the first $n$ elements of (append $xs$ $ys$), where $n$ is (len $xs$),
we would expect to get a list identical to $xs$.
To express this expectation formally, we need an operator that,
given a number $n$ and a list $xs$, delivers the first $n$ elements of $xs$.
Let's call that operator \textsf{prefix} and think about properties it would have to satisfy.

Of course, if $n$ is zero or if $xs$ is empty,
\textsf{(prefix $n$ $xs$)} must be the empty list.
If $n$ is a nonzero natural number and $xs$ is not empty,
then the first element of \textsf{(prefix $n$ $xs$)} must be the first element of $xs$
and the other elements must be the first $n-1$ elements of (rest $xs$).
Figure~\ref{prefix-equations} (page \pageref{prefix-equations}) displays
equations that define the \textsf{prefix} operator.
We can derive the prefix property of the \textsf{append} operator
from those equations and the axioms of the \textsf{append} operator
(figure~\ref{fig:append-defun}, page \pageref{fig:append-defun}).
We will
\label{app-pfx-thm-paper-and-pencil}prove $\forall n.$P($n$) by induction,
where the predicate
\label{append-prefix-thm-predicate}P is defined as follows:
\begin{center}
P($n$) $\equiv$ $($\textsf{(prefix (len [$x_1$ $x_2$ $\dots$ $x_n$]) (append [$x_1$ $x_2$ $\dots$ $x_n$] $ys$))}
                $=$ \textsf{[$x_1$ $x_2$ $\dots$ $x_n$]}$)$
\end{center}

As required in proofs by induction, we will prove that P(0) is true
and also that P($n+1$) is true whenever P($n$) is true.
Those two proofs will allow us to conclude that
$\forall n.$P($n$) is true, citing \{induction\}.

\begin{figure}
\begin{center}
Axioms \{\emph{prefix}\}                                           \\
\begin{tabular}{ll}
\hline
\textsf{(prefix $(n + 1)$ (cons $x$ $xs$))} $=$ \textsf{(cons $x$ (prefix $n$ $x$s))} & \{\emph{pfx1}\} \\
\textsf{(prefix $n$ $xs$)} $=$  \textsf{nil}                                          & \{\emph{pfx0}\} \\
~~~~\emph{Note 1: Cite }\{\emph{pfx0}\} \emph{only if} \{\emph{pfx1}\} \emph{doesn't match.}&\\
~~~~\emph{Note 2: $n$ is a natural number.}
\end{tabular}
\begin{code}
\begin{verbatim}
(defun prefix (n xs)
  (if (and (posp n) (consp xs))
      (cons (first xs) (prefix (- n 1) (rest xs)))  ; {pfx1}
      xs))                                          ; {pfx0}
\end{verbatim}
\end{code}
\end{center}
\seeonlyindex{prefix, of list}{operator}\index{operator, by name!prefix (of list)}\index{axiom, by name!\{pfx0\}, \{pfx1\}}\index{equation, by name!\{pfx0\}, \{pfx1\}}
\caption{Defining list prefix extractor: \textsf{prefix}.}
\label{prefix-equations}
\end{figure}

As in the proof of the append suffix theorem, we start
with the formula on one side of the P(0) equation
and use known equations to gradually transform
that formula into the one on the other side of the equation.
\begin{center}
\begin{tabular}{lll}
\multicolumn{3}{c}{P($0$) $\equiv$ $($\textsf{(prefix (len nil) (append nil $ys$))} $=$ \textsf{nil}$)$}\\
    & \textsf{(prefix (len nil) (append nil $ys$))}  &                                                  \\
$=$ & \textsf{(prefix 0 (append nil $ys$))}          & \{\emph{len0}\} (page \pageref{len-equations})   \\
$=$ & \textsf{nil}                                   & \{\emph{pfx0}\}                                  \\
\end{tabular}
\end{center}

That takes care of P(0). Figure~\ref{pfx-induc}
(page \pageref{pfx-induc}) displays a proof of P($n$) $\rightarrow$ P($n+1$).
At this point we know three important facts about the \textsf{append} operator:\\
\hspace*{1cm}\emph{Additive-length theorem}: \textsf{(len (append $xs$ $ys$))} $=$ \textsf{(+ (len $xs$) (len $ys$))}\index{theorem, by name!\{append-suffix\}}\index{theorem, by name!\{append-prefix\}}\index{append!prefix theorem}\label{app-pfx-thm}\\
\hspace*{1cm}\emph{Append-prefix theorem}: \textsf{(prefix (len $xs$) (append $xs$ $ys$))} $=$ $xs$\\
\hspace*{1cm}\emph{Append-suffix theorem}: \textsf{(nthcdr (len $xs$) (append $xs$ $ys$))} $=$ $ys$

\begin{figure}
\begin{center}
\begin{spacing}{0.9}
\addtolength{\tabcolsep}{-5pt}
\begin{tabular}{llll}
~~~~\textsf{(prefix} &\textsf{(len}    &\textsf{[$x_1$ $x_2$ $\dots$ $x_{n+1}$])}    &\\
            &\textsf{(append} &\textsf{[$x_1$ $x_2$ $\dots$ $x_{n+1}$] $ys$))}       &\\
$=$ \textsf{(prefix} &\textsf{(len}    &\textsf{(cons $x_1$ [$x_2$ $x_3$ $\dots$ $x_{n+1}$]))}&\{\emph{cons}\} (page \pageref{first-rest-cons})\\
            &\textsf{(append} &\textsf{(cons $x_1$ [$x_2$ $x_3$ $\dots$ $x_{n+1}$]) $ys$))}&\\
$=$	\textsf{(prefix} &\textsf{(+ ~ 1}  &\textsf{(len [$x_2$ $x_3$ $\dots$ $x_{n+1}$]))}       &\{\emph{len1}\} (page \pageref{len-equations})\\
            &\textsf{(cons $x_1$}  &\textsf{(append [$x_2$ $x_3$ $\dots$ $x_{n+1}$] $ys$)))}&\{\emph{app1}\} (page \pageref{append-equations})\\
$=$ \textsf{(cons}   &\textsf{(first}  &\textsf{(cons $x_1$ [$x_2$ $x_3$ $\dots$ $x_{n+1}$]))}&\\
            &\textsf{(prefix} &\textsf{(- (+ 1 (len [$x_2$ $x_3$ $\dots$ $x_{n+1}$])) 1)}&\{\emph{pfx1}\}\\
            &        &\textsf{(rest (cons $x_1$ (append [$x_2$ $x_3$ $\dots$ $x_{n+1}$] $ys$)))))}&\\
$=$ \textsf{(cons}   &$x_1$   &                                           &\{\emph{fst}\} (page \pageref{first-rest-cons})\\
            &\textsf{(prefix} &\textsf{(len [$x_2$ $x_3$ $\dots$ $x_{n+1}$])}        &\{\emph{arithmetic}\}\\
            &        &\textsf{(append [$x_2$ $x_3$ $\dots$ $x_{n+1}$] $ys$)))}& \{\emph{rst}\} (page \pageref{first-rest-cons})\\
$=$ \textsf{(cons}   &$x_1$   &                                          &\\
            &\textsf{[$x_2$ $x_3$} &\textsf{$\dots$ $x_{n+1}$])}                   &\{P($n$)\} \\
$=$ \textsf{[$x_1$ $x_2$} & \textsf{$\dots$ $x_{n+1}$]}                  &&\{\emph{cons}\} (page \pageref{first-rest-cons}) \\
\end{tabular}
\addtolength{\tabcolsep}{5pt}
\end{spacing}
~~\vspace{1mm}\\
P($n+1$)$\equiv($\textsf{(prefix (len[$x_1$ $x_2$ $\dots$ $x_{n+1}$]) (append [$x_1$ $x_2$ $\dots$ $x_{n+1}$] $ys$))} $=$
 \textsf{[$x_1$ $x_2$ $\dots$ $x_{n+1}$]}$)$
\end{center}
\caption{Inductive case: $\forall n.$ P($n$) $\rightarrow$ P($n+1$).}
\label{pfx-induc}
\end{figure}

Together, these theorems provide some assurance that \textsf{append} does what we
would expect for a concatenation operator.
We could think of them as
\index{property!correctness}\index{correctness property}correctness properties
for \textsf{append}.
Of course, the \textsf{append} operator has
an infinite variety of other properties too.
Their relative importance depends on how we are using the operation.
A property that is sometimes important to know is that concatenation is associative,
like addition and multiplication in numeric algebra
(figure~\ref{fig-02-01}, page \pageref{fig-02-01}).
That is, if there are three lists to be concatenated,
you could concatenate the first list with the concatenation of the last two.
Or, you could concatenate the first two, then append the third list at the end.
\begin{samepage}
\index{theorem, by name!\{app-assoc\}}
\label{app-assoc}
\begin{center}
Theorem \{\emph{app-assoc}\}: \textsf{(append $xs$ (append $ys$ $zs$))}$=$\textsf{(append (append $xs$ $ys$) $zs$)}
\end{center}
\end{samepage}

The associative property of \textsf{append} can be proved by mathematical induction,
starting from the following predicate with the natural numbers as its
universe of discourse.

The goal would be to prove that the formula $(\forall n.$A($n$)$)$ is true.
We leave the proof as an exercise.
\begin{samepage}
\begin{center}
A($n$) $\equiv$ \textsf{(append [$x_1$ $x_2$ $\dots$ $x_n$] (append $ys$ $zs$))}$=$\textsf{(append(append [$x_1$ $x_2$ $\dots$ $x_n$] $ys$) $zs$)}
\end{center}
\end{samepage}

\begin{exercises}

\exer {Prove the \{\emph{app-assoc}\} theorem (page \pageref{app-assoc}).}

\exer {Prove $\forall n.($\textsf{(rest [$x_1$ $x_2$ $\dots$ $x_n$])} $=$ \textsf{(nthcdr 1 [$x_1$ $x_2$ $\dots$ $x_n$])}$)$.}

%\todo{COMMENT ONLY, NO TODO
%Reviewer 2 points out that Ch4 talks about ACL2 programs and even about
%defun (in the following exercise), but does not provide a proper explanation.
%Ch5 then more-or-less assumes the reader already knows about defun.
%Also, Ch3 is already talking about testing ACL2 programs, and
%has a test of the reciprocals program, r, without a defun for r.
%This needs to be fixed.
%One way to handle it would be to add a section to Ch3 to explain defun.
%The intro material can be moved from Ch5,
%and this exercise or something like it could
%provide an example in this chapter (Ch4) for reasoning by induction
%with a defined, rather than intrinsic, operator.
%Update (Rex 10Sep2017): added the defun section and replace r(n).
%Plan to move and expand mechanized logic section and halting problem to chapter after ch04 (ch04a.tex, I guess)
%UPDATE 12/10/17: Halting problem is last section of ch04mechlogic.
%}
\exer {\label{rep-len}\index{theorem, by name!\{rep-len\}}%
Prove: $\forall n.($\textsf{(len (rep $n$ $x$))} $=$ $n)$~~~\{\emph{rep-len}\}\\
The operator \textsf{rep} is defined as follows:
\index{operator, by name!rep (list of duplicates)}\seeonlyindex{rep}{operator}\index{axiom, by name!\{rep0\}, \{rep1\}}\index{equation, by name!\{rep0\}, \{rep1\}}\label{rep-equations}}
\begin{code}
\begin{verbatim}
(defun rep (n x)
  (if (posp n)
      (cons x (rep (- n 1) x))   ; {rep1}
      nil))                      ; {rep0}
\end{verbatim}
\end{code}

\exer {\index{theorem, by name!\{app-nil\}}%
Prove theorem \{app-nil\}: $\forall n.$(\textsf{[$x_1$ $x_2$ $\dots$ $x_{n}$]} $=$ \textsf{(append [$x_1$ $x_2$ $\dots$ $x_{n}$] nil)})}

\exer {\label{ex:nthcdrtonil}%
Prove: $\forall n.($\textsf{(nthcdr (len [$x_1$ $x_2$ $\dots$ $x_n$]) (append [$x_1$ $x_2$ $\dots$ $x_n$]  nil))} $=$ \textsf{nil}$)$}

\exer {\label{member-equal-equations}\index{axiom!member-equal}\index{equation, by name!\{member-equal\}}\seeonlyindex{member-equal}{predicate}\index{operator, by name!member-equal (\emph{see} predicate)}\index{predicate, by name!member-equal (element of list)}\index{axiom, by name!\{mem0\}, \{mem1\}}\index{equation, by name!\{mem0\}, \{mem1\}}%
Prove the following implication:\\
\hspace*{16mm}$\forall n.($\textsf{(member-equal $y$ (rep $n$ $x$))} $\rightarrow$ \textsf{(member-equal y (cons $x$ nil))}$)$~~~\{\emph{rep-mem}\}\\
The operator \textsf{rep} is defined in exercise \ref{rep-len}, and
the equations \{\emph{mem0}\} and \{\emph{mem1}\} define the predicate \textsf{member-equal}.
\begin{center}
\begin{tabular}{ll}
\textsf{(member-equal $y$ (cons $x$ $xs$))} $=$ \textsf{(equal $y$ $x$)} $\vee$ \textsf{(member-equal $y$ $xs$)} & \{\emph{mem1}\} \\
\textsf{(member-equal $y$ nil)} $=$ \textsf{nil}                                                         & \{\emph{mem0}\}
\end{tabular}
\end{center}
}

\end{exercises}

%\todo{COMMENT ONLY, NO TODO
%next section will introduce defthm and proofs using the ACL2 mechanized logic
%by replaying all of the theorems of this section in ACL2 notation}

%% All references to Dracula taken out (30Aug2017 - rlp)
%% I think we should use Proof Pad for all doublecheck and other interface-to-ACL2 issues.
%% We can explain in an aside, when we first mention Proof Pad,
%%    that ACL2s and emacs are other interfaces,
%%    that ACL2s has its own, extensive, random-test facility,
%%    that it is perfectly reasonable for students to use another interface to ACL2,
%%    that if they use another interface, they will need to interpret our doublecheck examples in, say, ACL2 fashion.
%%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "book"
%%% End: