\documentclass[11pt]{article}
\usepackage{color}
\definecolor{light}{gray}{.93}
\usepackage[plainpages=false,pdftex,colorlinks,backref]{hyperref}

\title{Proving Theorems with Athena}

\author{David R. Musser \and Aytekin Vargun}

\date{August 28, 2003, revised January 26, 2005}

\newcommand{\first}{\mbox{\texttt{first}}}
\newcommand{\last}{\mbox{\texttt{last}}}
\newcommand{\midpoint}{\mbox{\texttt{midpoint}}}
\newcommand{\current}{\mbox{\texttt{current}}}
\newcommand{\method}[2]{~\\ \noindent #1\\ ~\\ \noindent #2 }

\newtheorem{theorem}{Theorem}

\begin{document}

\maketitle

\tableofcontents

\section{Introduction}

The Athena language and proof system
\cite{arkoudas-DPL,arkoudas-athena-tutorial} developed at MIT by K.\
Arkoudas provides a way to present and work with mathematical proofs
so that they are both human-readable and mach\-ine-checkable.  In this
document we work through several examples showing how one can express
axioms and carry out proofs of theorems using a variety of proof
techniques.  In section~\ref{order} we work with a few laws of order
relations such as irreflexivity and transitivity (the axioms of a
strict partial-order relation, \texttt{<}) and prove that additional
laws such as asymmetry are logical consequences of the axioms.  These
proofs illustrate some of Athena's primitive deduction methods
\cite{arkoudas-athena-tutorial}, such as modus ponens, universal
specialization, and proof by contradiction.  In Sections~\ref{nats}
and \ref{lists} we illustrate reasoning about inductive (recursive)
data structures via examples involving natural numbers and list
structures.  We define these types inductively via Athena's
\texttt{datatype} construct, and bring into play the powerful
inference method of proof-by-induction via Athena's
\texttt{by-induction} construct.  Since the properties we are proving,
such as the associative law for appending lists together, are written
as equations, we make extensive use of \emph{term rewriting}
capabilities that we have introduced as
(user-defined) inference methods.  These rewriting methods, which are
documented at the beginning of Section~\ref{nats}, should be useful in
many other proofs that involve equations.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Proofs about order relations}
\label{order}

In this section we illustrate some basic proof methods in Athena
with formalization of some properties of an order relation.

We first load the rewriting file, which defines auxiliary inference
methods for carrying out term rewriting inferences (described in
Section~\ref{nats} and used in Sections~\ref{nats} and \ref{lists}),
plus a method called \texttt{conclude} that allows tracing of
proof attempts as an aid to debugging (illustrated in this section).


@e foo @{
(load-file "rewriting.ath")         @}

Unless you have a copy of \texttt{rewriting.ath} in the directory in
which you started Athena, you'll need to insert in the above directive
the directory path where \texttt{rewriting.ath} resides; e.g., on
CSLab machines you would write 

@e foo @{
 (load-file "/cs/musser/public.html/gsd/athena/rewriting.ath")         @}

We next declare the arity of an operator we call \texttt{is<} in terms of an
arbitrary domain we call \texttt{D}:\footnote{There is already a
declaration of \texttt{<} on the predefined domain \texttt{Num}.}

@e foo @{
(domain D)

(declare is< (-> (D D) Boolean))         @}

We now assert as axioms the irreflexive and transitive laws
for \texttt{is<}:

@e foo @{
(define Order-Irreflexive
  (forall ?x
    (not (is< ?x ?x))))

(define Order-Transitive
  (forall ?x ?y ?z
	  (if (and (is< ?x ?y) (is< ?y ?z))
	      (is< ?x ?z))))

(assert Order-Irreflexive Order-Transitive)         @}

These axioms characterize \texttt{is<} as a \emph{strict partial order}
relation.  From these axioms we can prove another law, asymmetry:

@e foo @{
(define Order-Asymmetry 
  (forall ?x ?y
	  (if (is< ?x ?y)
	      (not (is< ?y ?x)))))         @}

The proof is by contradiction, which is expressed in Athena with
its primitive method \texttt{by-contradiction}: 

@e foo @{
(Order-Asymmetry
 BY (pick-any x y
	      (assume (is< x y)
		(!by-contradiction 
		 (assume (is< y x)
		   (dseq
		    ((is< x x)
		     BY (!mp (!uspec* Order-Transitive [x y x]) 
			     (!both (is< x y) 
				    (is< y x))))
		    ((not (is< x x))
		     BY (!uspec Order-Irreflexive x))
		    (!absurd (is< x x) (not (is< x x)))))))))               @}

The result of executing this proof is

@e foo @{
Theorem: (forall ?x:D
           (forall ?y:D
             (if (is< ?x ?y)
                 (not (is< ?y ?x)))))           @}

The contradiction we get, expressed in the arguments to
\texttt{absurd}, is \texttt{(is< x x)} and \texttt{(not (is< x
x))}. The method \texttt{uspec*} used in proving the first of these
relations is an extension of the primitive universal specialization
method, \texttt{uspec}:

\method{uspec* $P$ $[t_1 \ldots t_n]$}
%
{replaces the first $n$ quantified variables in $P$ with
the terms $t_1, \ldots, t_n$.}\\
    
Thus, we've shown that the asymmetry law is a theorem when
one has a partial order relation; one does not have to 
assert it as a separate axiom.

In the above proof we used Athena's \texttt{BY} method, which
has the syntax\footnote{This is Athena's only infix operator.}

\begin{tabbing}
.....\=\kill
 \texttt{(}$\langle$\emph{proposition}$\rangle$ \\
  \> \texttt{BY}  $\langle$\emph{deduction}$\rangle$\texttt{)}
\end{tabbing}
%
which sets up \emph{proposition} as the one to be proved
by the deduction that follows \texttt{BY}.  That is, Athena checks
that the result proved by the deduction is the same proposition
as $\langle$\emph{proposition}$\rangle$; if it is different, Athena
reports an error.  Using \texttt{BY} at intermediate
steps within the proof helps document the subgoals into which
the deduction divides the overall proof.  If something is
wrong at any stage of the deduction, however, it can be 
difficult to tell where the problem is.  For this reason,
we have devised a method called \texttt{conclude} that
provides for tracing of the progress of the proof.
The \texttt{conclude} method is called with the syntax

\begin{tabbing}
.....\=\kill
 \texttt{(!(conclude~}$\langle$\emph{proposition}$\rangle$\texttt{)}\\
   \> $\langle$\emph{deduction}$\rangle$\texttt{)}
\end{tabbing}
%
which, like \texttt{BY}, sets up $\langle$\emph{proposition}$\rangle$ as a
proposition to be proved by the deduction that follows. With
\texttt{conclude}, however, we can turn proof tracing on
with\footnote{Note that the exclamation point \emph{follows}
\texttt{set} rather than preceding it; this is not a method call but
simply a call of a function named \texttt{set!}.  The inclusion of an
exclamation point in the name of an Athena function means that it is
an imperative procedure executed for its effect rather than for
computing value, a convention borrowed from the Scheme language.}

@e foo @{
(set! tracing true)            @}

Now if we redo the above proof using \texttt{conclude},

@e foo @{
(!(conclude Order-Asymmetry)
  (pick-any x y
	    (assume (is< x y)
	      (!by-contradiction 
	       (assume (is< y x)
		 (dseq
		  (!(conclude (is< x x))
		    (!mp (!uspec* Order-Transitive [x y x]) 
			   (!both (is< x y) 
				  (is< y x))))
		  (!(conclude (not (is< x x)))
		    (!uspec Order-Irreflexive x))
		  (!absurd (is< x x) (not (is< x x)))))))))               @}

the output is

 @e foo @{
  Proving at level 1:
    (forall ?x:D
  (forall ?y:D
    (if (is< ?x ?y)
        (not (is< ?y ?x)))))
        Proving at level 2:
        (is< ?v318 ?v318)
        Done at level 2
        Proving at level 2:
        (not (is< ?v318 ?v318))
        Done at level 2
    Done at level 1

Theorem: (forall ?x:D
           (forall ?y:D
             (if (is< ?x ?y)
                 (not (is< ?y ?x)))))         @}

With such tracing, if there is an error at any step of the 
proof, it is easier to see where the problem is.  In
all subsequent proofs we will use the \texttt{conclude} 
method.  However, in showing output we will assume tracing
is turned off:

@e foo @{
(set! tracing false)            @}

Now suppose we define a binary relation \texttt{E} 
as follows:

@e foo @{
(declare E (-> (D D) Boolean))

(define E-Definition
  (forall ?x ?y
	  (iff (E ?x ?y) 
	       (and (not (is< ?x ?y)) 
		    (not (is< ?y ?x))))))         @}

The name \texttt{E} for this relation is motivated by fact that we can
show that if \texttt{E} is assumed to be transitive then in combination
with the partial order axioms for \texttt{is<} we can prove that \texttt{E}
is in fact an equivalence relation; i.e., that it also obeys the other two
axioms of an equivalence relation besides the transitive law, namely
the reflexive and symmetric laws.

@E foo @{
(define E-Transitive
  (forall ?x ?y ?z
	  (if (and (E ?x ?y) (E ?y ?z))
	      (E ?x ?z))))

(assert E-Definition E-Transitive)

(define E-Reflexive
  (forall ?x
    (E ?x ?x)))

(!(conclude E-Reflexive)
  (pick-any x
    (dseq
     (!(conclude (not (is< x x)))
       (!uspec Order-Irreflexive x))
     (!(conclude (E x x))
       (!mp (!right-iff (!uspec* E-Definition [x x]))
	    (!both (not (is< x x)) 
		   (not (is< x x))))))))
 
(define E-Symmetric
  (forall ?x ?y
    (if (E ?x ?y)
	(E ?y ?x))))

(!(conclude E-Symmetric)
  (pick-any x y
	    (assume (E x y)
	      (dlet ((both-not 
		      (and (not (is< x y)) 
			   (not (is< y x)))))
		(dseq
		 (!(conclude both-not)
		   (!mp (!left-iff (!uspec* E-Definition [x y]))
			(E x y)))
		 (!(conclude (E y x))
		   (!mp (!right-iff (!uspec* E-Definition [y x]))
			(!both (!right-and both-not) 
			       (!left-and both-not)))))))))

(define E-Equivalent
  (and E-Reflexive 
       (and E-Symmetric 
	    E-Transitive)))

(!(conclude E-Equivalent)
  (!both E-Reflexive 
	 (!both E-Symmetric 
		E-Transitive)))         @}

The output from this last deduction is

@e foo @{
Theorem: (and (forall ?x:D
                (E ?x ?x))
              (and (forall ?x:D
                     (forall ?y:D
                       (if (E ?x ?y)
                           (E ?y ?x))))
                   (forall ?x:D
                     (forall ?y:D
                       (forall ?z:D
                         (if (and (E ?x ?y)
                                  (E ?y ?z))
                             (E ?x ?z)))))))        @}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Proofs about natural numbers}
\label{nats}

Now we turn to some simple proofs by induction.  We first declare a
natural numbers type as an inductive datatype.

@e foo @{
(datatype Nat zero (succ Nat))         @}

We next define a \texttt{Plus} function, except that instead of actually
defining it as a function, we specify its behavior axiomatically in
terms of a \texttt{Plus} symbol.

The \texttt{Plus} function will take two \texttt{Nat} values as
parameters and return their sum as a \texttt{Nat} value.

@e foo @{
(declare Plus (-> (Nat Nat) Nat))         @}

We next define the propositions we intend to use to define the meaning
of \texttt{Plus} axiomatically.

@e foo @{
(define Plus-zero-axiom
  (forall ?n (= (Plus ?n zero) ?n)))         @}

@e foo @{
(define Plus-succ-axiom
  (forall ?n ?m 
	  (= (Plus ?n (succ ?m)) 
	     (succ (Plus ?n ?m)))))         @}

After defining these propositions, we add them as axioms to Athena's
assumption base.  We can only use the axioms in the assumption base to
prove new propositions.  

@e foo @{
(assert Plus-zero-axiom Plus-succ-axiom)         @}

\subsection{Term rewriting methods}

Note that these axioms are stated using equations.  When working with
equations, one often structures a proof as sequence of
\emph{rewriting} steps, in which a term is shown to be equal to
another term by means of a substitution that is justified by an
universally quantified equation (or just a simple unquantified equation)
in the assumption base.  For example,
we can rewrite the term 
\begin{center}
$t = $\texttt{(succ (Plus zero (succ (succ zero))))}\\ ~~~~ (representing $(0+2)+1$)
\end{center}
to
\begin{center}
$u = $\texttt{(succ (succ (Plus zero (succ zero))))}\\ ~~~~ (representing $(0+1)+2)$
\end{center}
using our universally quantified equation 
@e foo @{
(define Plus-succ-axiom
  (forall ?n ?m 
	  (= (Plus ?n (succ ?m)) 
	     (succ (Plus ?n ?m)))))         @}
This can be done by substituting \texttt{zero} for \texttt{?n} and \texttt{(succ (succ zero))}
for \texttt{?m}, producing the specialized equation
\begin{center}
\texttt{(= (Plus zero (succ (succ zero))) (succ (Plus zero (succ zero))))}
\end{center}
and then replacing the occurrence of the left hand side of this equation
\begin{center}
\texttt{(Plus zero (succ (succ zero)))}
\end{center}
within $t$ 
with the right hand side 
\begin{center}
\texttt{(succ (Plus zero (succ zero)))}
\end{center}
to produce $u$.  We say that the equation is
being used ``left-to-right'' or as a 
``left-to-right rewriting rule.''  (If the equation has no
quantifiers, no substitution need be computed; the identity 
substitution is used.)

Athena does not currently have such rewriting methods built
in, so we have created the following rewriting methods (implemented
in the \texttt{rewriting.ath} file).

\method{setup $c$ $t$}{initializes cell $c$ to hold term $t$. Actually
it internally holds the equation $(= t ~ t)$, and the reduce and
expand methods transform the right hand side of this equation. There
are two predefined cells named left and right.}
                                                                              
\method{reduce $c$ $u$ $E$}{attempts to transform the term $t$ in cell $c$ to be
identical with the given term $u$ by using equation $E$ left-to-right.}

\method{expand $c$ $u$ $E$}{attempts to transform the term $u$ to the
term $t$ in cell $c$ by using equation $E$ left-to-right.}

\method{combine left right}{attempts to combine the equation
internally stored in cell left, say $(= t ~ t')$, with the equation
internally stored in cell right, say $(= u ~ u')$, to deduce $(= t ~ u)$
 (which succeeds if $t'$ and $u'$ are identical).}\\

As a simple example consider the following deduction in which
we prove an equality by reducing both its left and its right hand side
term to the same term, \texttt{(succ (succ (succ zero)))}.

@e foo @{
(!(conclude (= (Plus zero (succ (succ (succ zero))))
	       (succ (succ (succ (Plus zero zero))))))
 (dseq
  (!setup left   (Plus zero (succ (succ (succ zero)))))
  (!setup right  (succ (succ (succ (Plus zero zero)))))
  (!reduce left (succ (Plus zero (succ (succ zero)))) 
	   Plus-succ-axiom)
  (!reduce left (succ (succ (Plus zero (succ zero)))) 
	   Plus-succ-axiom)
  (!reduce left (succ (succ (succ (Plus zero zero)))) 
	   Plus-succ-axiom)
  (!reduce left (succ (succ (succ zero ))) Plus-zero-axiom)
  (!reduce right (succ (succ (succ zero))) Plus-zero-axiom)
  (!combine left right)))         @}

This produces

@e foo @{
Theorem: (= (Plus zero
                  (succ (succ (succ zero))))
            (succ (succ (succ (Plus zero zero)))))    @}

It's possible to trace the execution of rewriting methods
with 

@e foo @{
(set! tracing-rewrites true)                       @}

Then reentering the above deduction produces

@E foo @{
   Rewriting
    (Plus zero
      (succ (succ (succ zero))))
    -->
    (succ (Plus zero
            (succ (succ zero))))
    -->
    (succ (succ (Plus zero
                  (succ zero))))
    -->
    (succ (succ (succ (Plus zero zero))))
    -->
    (succ (succ (succ zero)))
    Rewriting
    (succ (succ (succ (Plus zero zero))))
    -->
    (succ (succ (succ zero)))

Theorem: (= (Plus zero
                  (succ (succ (succ zero))))
            (succ (succ (succ (Plus zero zero)))))        @}

When we show output in subsequent examples we assume tracing
of rewrites is turned off:

@e foo @{
(set! tracing-rewrites false)                       @}

It should be noted that these rewriting methods, although not in the
base Athena system, are guaranteed to be logically sound (relative to
the soundness of Athena's logical system) because they are programmed
in terms of Athena's primitive methods and all of the means that
Athena provides for composing methods preserve soundness.

\subsection{Proof by induction}

The proof of the equational property above would be much simpler if
had as a general property of \texttt{Plus},

@e foo @{
(define Plus-zero-property
  (forall ?n (= (Plus zero ?n) ?n)))         @}

Whereas \texttt{Plus-zero-axiom} states that \texttt{zero} serves as a
right-identity element for the \texttt{Plus} operator, this
proposition states that it is also a left-identity element.  The
validity of this property is, however, \emph{not} a consequence simply
of the equational axioms we've stated about \texttt{Plus} and
\texttt{zero}; it depends on the fact that \texttt{Nat} is
inductively defined by the datatype declaration \texttt{(datatype
Nat zero (succ Nat))}.  According to the built-in semantics of
\texttt{datatype}, the only values of type \texttt{Nat} are those
that can be expressed with syntatically-correct and type-correct
combinations of \texttt{zero} and \texttt{succ} terms:
@e foo @{
  zero
  (succ zero)
  (succ (succ zero))
  (succ (succ (succ zero)))
  ...                               @}

For such inductively-defined types, we can prove propositions
using the method of proof by induction.

\subsection{Steps of a proof of an Nat inductive property.}

There are two main steps in a proof by induction.
\begin{itemize}

 \item The basis case. In our \texttt{Nat} datatype example, this is a special
case in which the proposition to be proved is instantiated with \texttt{zero}.

 \item The induction step.  In our \texttt{Nat} datatype example, we
instantiate the proposition with $\mbox{(succ $n$)}$ and attempt to
prove it, assuming the proposition is true for $n$.

\end{itemize} These separate proofs can be combined using Athena's
\texttt{by-induction} construct to conclude the proposition is true
for all $n$.


\subsection{Basis case proof}

Before doing the full proof, let's just check the basis case first.  

@e foo @{
(!(conclude (= (Plus zero zero) zero))
  (dseq
   (!setup left (Plus zero zero))
   (!setup right zero)
   (!reduce left zero Plus-zero-axiom)
   (!combine left right)))                   @} 

In the proof itself, the \texttt{setup} calls set up \texttt{left} and
\texttt{right} to hold the left and right hand sides of the equation
to be proved.  In this simple case only one application of
\texttt{reduce}, applied to \texttt{left}, is sufficient to produce
the same term, \texttt{zero}, as we have placed in \texttt{right}.
Note that \texttt{reduce} has to specialize the quantified variable
\texttt{?n} in Plus-zero-axiom to \texttt{zero} in order to use the
result \texttt{(= (Plus zero zero) zero)} to substitute \texttt{zero}
for \texttt{(Plus zero zero)}.

\subsection{Induction step proof}

We next proceed with the induction step of the proof:

@e foo @{
(!(conclude (forall ?n (if (= (Plus zero ?n) ?n)
			   (= (Plus zero (succ ?n))
			      (succ ?n)))))
  (pick-any n
    (assume (= (Plus zero n) n)
      (dseq
       (!setup left (Plus zero (succ n)))
       (!setup right (succ n))
       (!reduce left (succ (Plus zero n)) Plus-succ-axiom)
       (!reduce left (succ n) (= (Plus zero n) n))
       (!combine left right)))))  @}

Note that in the last call of \texttt{reduce} we used
an unquantified equation to do the reduction; we could do
that since the left hand side, \texttt{Plus zero n}, is
an exact match for a subterm of \texttt{(succ (Plus zero n))}.

\subsection{The full proof}

After the basis case and inductive step proofs given
above have been executed, the assumption base will contain
the necessary ingredients for completion of the proof
using Athena's \texttt{by-induction} deduction:

@e foo @{
(by-induction
 Plus-zero-property
 (zero
  (!claim (= (Plus zero zero) zero))) 
 ((succ n)
  (!mp (!uspec (forall ?n (if (= (Plus zero ?n) ?n)
			      (= (Plus zero (succ ?n))
				 (succ ?n))))
	       n)
       (= (Plus zero n) n))))                     @}

This produces
@e foo @{
Theorem: (forall ?n:Nat
           (= (Plus zero ?n) ?n))               @}

While this approach --- successively doing the basis case, the
induction step, and then applying \texttt{by-induction} --- works, it
seems a bit awkward.  Why is it necessary to apply \texttt{uspec} and
\texttt{mp} in the \texttt{succ} clause of the \texttt{by-induction}
application?  It's because \texttt{by-induction} actually sets
up the induction hypothesis and puts it into the
assumption base automatically, so one doesn't really to 
need to do it manually the way we did in proving the induction
step as a separate proof.  We can simply package the full proof
into an application of \texttt{by-induction}, as follows:

@e foo @{
(by-induction
 Plus-zero-property
 (zero
  (!(conclude (= (Plus zero zero) zero))
    (dseq
     (!setup left (Plus zero zero))
     (!setup right zero)
     (!reduce left zero Plus-zero-axiom)
     (!combine left right))))
 ((succ n)
  (!(conclude (= (Plus zero (succ n)) (succ n)))
    (dlet ((induction-hypothesis 
	    (= (Plus zero n) n)))
      (dseq 
       (!setup left (Plus zero (succ n)))
       (!setup right (succ n))
       (!reduce left (succ (Plus zero n)) Plus-succ-axiom)
       (!reduce left (succ n) induction-hypothesis)
       (!combine left right))))))                     @}

Again, this produces:

@e foo @{
Theorem: (forall ?n:Nat
           (= (Plus zero ?n) ?n))               @}

In this proof, we defined and used the induction hypothesis, but we
didn't have to assume it. Again, this is because \texttt{by-induction}
automatically adds induction hypotheses to the assumption base
according to the inductive structure of the type.

The possible drawback of packaging the full proof into a call of
\texttt{by-induction} is that if there is an error somewhere, it can
be harder to pinpoint it than if the basis case and inductive step
proofs are done separately.  However, we can avoid this problem by
using \texttt{conclude} method calls as in the above proof (rather
than \texttt{BY}) so that we can turn tracing on to show progress
through the proofs of the individual subgoals.

In developing a proof within \texttt{by-induction}, we may want
to test out the basis case proof before starting on the
induction step proof.  This is possible; we just have to 
include the inductive step clause with correct syntax. For example,

@e foo @{
(by-induction
 Plus-zero-property
 (zero
  (!(conclude (= (Plus zero zero) zero))
    (dseq
     (!setup left (Plus zero zero))
     (!setup right zero)
     (!reduce left zero Plus-zero-axiom)
     (!combine left right))))
 ((succ n)
  (!claim true)))            @}

parses and executes; it produces an error

@e foo @{
Error, top level, 11.3: A Inductive subdeduction failed to establish
the right conclusion. The required conclusion was:
(= (Plus zero
         (succ ?v296))
   (succ ?v296))
but the derived one was: 
true
(where the fresh variable ?v296 has replaced the pattern variable n).@}

but the error is just with the inductive step part, indicating
that the basis case proof went through.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Proofs about lists}
\label{lists}

In this section we axiomatize list datatypes and prove a couple of
useful properties based on the axioms using proof by induction.  Although
this example exhibits strong similarities to the inductive
structure and proof we introduced in the previous section about natural
numbers, there are some additional twists that reveal
a few more of the capabilities of Athena.  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Append Nil Property}
\label{function}

Athena's type system allows polymorphism: we can 
declare polymorphic lists as a datatype.  In fact, the following
declaration is predefined:

@e foo @{
 (datatype (List-Of T) Nil (Cons T (List-Of T)))         @}

Here \texttt{T} is a type variable that can be instantiated with
any type, so that, for example, \begin{itemize}

  \item \texttt{(Cons zero (Cons (succ zero) Nil))} is a term of type
\texttt{(List Nat)} (if \texttt{Nat} has been introduced as a datatype as in
the previous section);

  \item \texttt{(Cons true Nil)} is a term of type \texttt{(List Boolean)};

  \item however, \texttt{(Cons zero (Cons true Nil))} is an error
     (``Ill-sorted term'') since all elements of a \texttt{List} must have the
     same type.

\end{itemize} 
% 
We define an \texttt{Append} function on \texttt{List}s, except that
instead of actually defining it as a function, we specify its behavior
axiomatically in terms of an \texttt{Append} symbol.  \texttt{Append} takes two
\texttt{List}s as parameters and returns a single list.

@e foo @{
(declare Append ((T) -> ((List-Of T) (List-Of T)) (List-Of T)))         @}

Note that Athena allows a list of type parameters to precede the
function arrow; in this case there is only one, \texttt{T}.

The semantics we want for $\mbox{(Append $p$ $q$)}$ is it contains all
of the elements of $p$ followed by all of the elements of $q$.
We next define the propositions we intend to use to define the meaning
of Append axiomatically.

@e foo @{
(define Append-Nil-axiom
  (forall ?q 
    (= (Append Nil ?q) ?q)))         @}

@e foo @{
(define Append-Cons-axiom
  (forall ?x ?r ?q
	  (= (Append (Cons ?x ?r) ?q)
	     (Cons ?x (Append ?r ?q)))))))         @}

After defining these propositions, we add them as axioms to Athena's
assumption base.  

@e foo @{
(assert Append-Nil-axiom Append-Cons-axiom)         @}

There are of course other properties of \texttt{Append} that could be
stated and asserted as axioms.  For example, the Append-Nil-axiom
above says that the \texttt{Nil} list acts as a left-identity element
for the \texttt{Append} operator.  As in the case of \texttt{zero} in
the \texttt{Nat} example in the previous section, it is natural to
ask, is \texttt{Nil} also a right-identity element?  I.e., is it also
true that

@e foo @{
(define Append-Nil-property
  (forall ?q (= (Append ?q Nil) ?q)))         @}

In fact, we can prove that this proposition is a consequence of the
two axioms for \texttt{Append}, using proof by induction.  In Athena
such proofs are supported by \texttt{by-induction}, which works just
as well with the \texttt{List} datatype as we saw it did with
\texttt{Nat} in the previous section.

\subsection{Steps of a proof of a List inductive property}

Again, there are two main parts of such a proof by induction.
\begin{itemize}

 \item The basis case. In our \texttt{List} datatype example, this is a
special case in which the proposition is instantiated with \texttt{Nil}.

 \item The induction step.  In our \texttt{List} datatype example, we
instantiate the proposition with $\mbox{(Cons $x$ $q$)}$ and attempt to
prove it, assuming the proposition is true for $q$.

\end{itemize} These proofs can be combined using Athena's
\texttt{by-induction} construct to conclude the proposition is true
for all $q$.

@e foo @{
(by-induction
 Append-Nil-property
 (Nil
  (!(conclude (= (Append Nil Nil) Nil))
    (dseq
     (!setup left (Append Nil Nil))
     (!setup right Nil)
     (!reduce left Nil Append-Nil-axiom)
     (!combine left right))))
 ((Cons x p)
  (!(conclude (= (Append (Cons x p) Nil) (Cons x p)))
    (dlet ((induction-hypothesis 
	    (= (Append p Nil) p)))
      (dseq
       (!setup left  (Append (Cons x p) Nil))
       (!setup right (Cons x p))
       (!reduce left (Cons x (Append p Nil)) Append-Cons-axiom)
       (!reduce left (Cons x p) induction-hypothesis)
       (!combine left right))))))          @}

\subsection{Another proof about Append}

The final example is the proof of another property of \texttt{Append},
again by induction.

@e foo @{
(define Append-Associative
  (forall ?p ?q ?r
	  (= (Append (Append ?p ?q) ?r) 
	     (Append ?p (Append ?q ?r)))))         @}

The new twist here is that we have two additional quantified variables
 (\texttt{?q} and \texttt{?r}) besides the one (\texttt{?p}) on which
we do the induction.  These quantified variables must be dealt with in the
proof.  The Athena deduction that allows us to deal with them properly
is \texttt{pick-any}.

@e foo @{
(by-induction
 Append-Associative
 (Nil 
  (!(conclude (forall ?q ?r (= (Append (Append Nil ?q) ?r)
			       (Append Nil (Append ?q ?r)))))
    (pick-any q r
	      (dseq
	       (!setup left (Append (Append Nil q) r))
	       (!setup right (Append Nil (Append q r)))
	       (!reduce left (Append q r) Append-Nil-axiom)
	       (!reduce right (Append q r) Append-Nil-axiom)
	       (!combine left right)))))
 ((Cons x p)
  (!(conclude (forall ?q ?r (= (Append (Append (Cons x p) ?q) ?r)
			       (Append (Cons x p) (Append ?q ?r)))))
    (dlet ((induction-hypothesis
	    (forall ?q ?r (= (Append (Append p ?q) ?r)
			     (Append p (Append ?q ?r))))))
      (pick-any q r
		(dseq
		 (!setup left  (Append (Append (Cons x p) q) r))
		 (!setup right (Append (Cons x p) (Append q r)))
		 (!reduce left  (Append (Cons x (Append p q)) r) 
			  Append-Cons-axiom)
		 (!reduce left  (Cons x (Append (Append p q) r)) 
			  Append-Cons-axiom)
		 (!reduce left  (Cons x (Append p (Append q r))) 
			  induction-hypothesis)
		 (!reduce right (Cons x (Append p (Append q r))) 
			  Append-Cons-axiom)
		 (!combine left right)))))))                      @}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\bibliographystyle{keyplain}

\bibliography{ccp}

\end{document}

@O proof-examples2.ath @{
@<foo@>
@}