\documentstyle[10pt,epsf,fuzz]{article}

\input{./handout}

\newtheorem{defn}{Definition}

\begin{document}

\handout{3}{11 September 1995}{Other Proof Techniques and Proof Hints}
\begin{symbolfootnotes}
\footnotetext[0]{\copyright 1995 Jeannette M. Wing} 
\end{symbolfootnotes}

Natural deduction and equational reasoning, which you have seen
already,
and induction, which you will see shortly, are examples
of different proof techniques to have in
your
bag of proof tricks.  This handout covers some others.  All but the
first
are probably familiar to you, which is why we are not going to dwell
on any of them.  Much of this handout is inspired
by [GS]; parts are copied verbatim from Chapters 3 and 4.

\section{One Point Rule}

The One Point Rule is useful for dealing with existential quantifiers.
It says that if you have an existentially quantified statement and
part
of it pins down an exact value for the quantified variable, then you
can remove the quantification and {\em replace} the variable by the
value
whereever that variable appears in the rest of the statement.

\begin{center}
$\frac{\displaystyle{\exists x: S \bullet (p \wedge x =
t)}}{\displaystyle{t \in S \wedge p[t/x]}}~~~~~~~~~\neg(occurs(x, t))$
\end{center}

\noindent Note the {\em side condition} that you must check before applying
this rule: The variable,
$x$, must not be free in the term, $t$, that you are using in the substitution.

For example, $\exists n: \nat \bullet (n < 10 \wedge n = 2 \ast 3)$ is
equivalent to $2 \ast 3 \in \nat \wedge 2 \ast 3 < 10$.  The first
conjunct checks that the term is member of the right set; it is usually
easy to discharge that check.  Then, you are left with just the part
of the predicate in which the substitution has been made, e.g.,
$2 \ast 3 < 10$.

\section{Implication [GS]}
\label{sec:implication}

If your predicate has an implication in it, sometimes it's easier
to work with the equivalent disjunctive formulation:

\begin{center}
$p \Rightarrow q \equiv \neg p \vee q$
\end{center}

Here are some other useful properties about implication and boolean
constants:
\begin{verse}
\begin{tabbing}
$p \Rightarrow p \equiv true$\hspace{.2in}\=({\bf Reflexivity})\\
$p \Rightarrow true \equiv true$\>({\bf Right zero})\\
$true \Rightarrow p \equiv p$\>({\bf Left identity})\\
$p \Rightarrow false \equiv \neg p$\\
$false \Rightarrow p \equiv true$
\end{tabbing}
\end{verse}

Here are some useful theorems about implication:

\begin{verse}
\begin{tabbing}
$p \wedge q \Rightarrow r \equiv p \Rightarrow (q \Rightarrow r)$\hspace{.2in}\=({\bf Shunting})\\
$p \wedge (p \Rightarrow q) \equiv p \wedge q$\\
$p \vee (p \Rightarrow q) \equiv true$
\end{tabbing}
\end{verse}

\section{Assuming the Antecedent [GS]}

It is common in mathematics to prove an implication $p \Rightarrow q$
by assuming the antecedent $p$ and proving the consequent $q$.  By
``assuming the antecedent'' we momentarily think of it as an axiom
and thus equivalent to {\em true}.
The formal justification of this proof technique relies
on the {\bf Deduction Theorem} from mathematical logic.\footnote{
{\bf Deduction Theorem}: Suppose adding $p_1, \ldots, p_n$ as axioms
to
propositional logic, with the variables of the $p_i$ considered to be
constants, allows $q$ to be proved.  Then $p_1 \wedge \ldots \wedge
p_n \Rightarrow q$ is a theorem.}

Here is a simple example (from [GS]):  Suppose we want to prove
$a \wedge b \Rightarrow (a = b)$.  In the proof we get to assume
the conjuncts of the antecedent.  We are required to prove $a = b$:

{\em Proof}:
\begin{verse}
\begin{tabbing}
{\bf Ass}\={\bf ume}\=$~~~~~a, b.$\\
\>$a$\\
=\>\>\% Assumption of a.\\
\>$true$\\
=\>\>\% Assumption of b.\\
\>$b$
\end{tabbing}
\end{verse}

Warning:
For the proof of $p \Rightarrow q$,
the {\bf Deduction Theorem} requires that all variables in the assumed
expression, $p$, be viewed as constants throughout the proof of $q$, so
that you cannot substitute expressions in for the ``variables'' that
appear
in the assumptions.  The following incorrect proof of
$(b = c) \Rightarrow (d = c)$ (which is not valid) shows why
this is necessary.  The proof is incorrect because $b$ in the
assumption is replaced.

{\em Proof} (Incorrect):
\begin{verse}
\begin{tabbing}
{\bf Ass}\={\bf ume}\=$~~~~~b = c.$\\
\>$d$\\
=\>\>\% Assumption of $(b = c)[d/b]$, i.e., $d = c$\\
\>$c$
\end{tabbing}
\end{verse}

\noindent Notice that the expression in which we are attempting to do
the
substitution is $b = c$.

\section{Case Analysis [GS]}

A proof of $r$ by case analysis proceeds as follows.  Find the
cases $p$ and $q$ such that $p \vee q$ holds.  Then show that $r$
holds in each case: $p \Rightarrow r$ and $q \Rightarrow r$.
The justification of this proof technique relies on this property of
implication:

\begin{verse}
$(p \Rightarrow r) \wedge (q \Rightarrow r) \equiv (p \vee q \Rightarrow r)$\hspace{.2in}({\bf Case Analysis})
\end{verse}

\noindent Notice the common (and simpler) version of this property when $q \equiv \neg p$:

\begin{verse}
$(p \Rightarrow r) \wedge (\neg p \Rightarrow r) \equiv r$\hspace{.2in}({\bf Simple Case Analysis})
\end{verse}

This proof technique generalizes to a case analysis of more
than two cases in the obvious way: The disjunction of all the cases
must be {\em true} and each case must imply $r$.

\section{Proof by Contradiction [GS]}

It is common in mathematics to prove a theorem $p$ by assuming it
is {\em false} and deriving a contradiction, i.e., derive {\em false}
or something equivalent to {\em false}, like $q \wedge \neg q$.  The justification for this
proof technique is the following property about implication, repeated
from Section \ref{sec:implication}:

\begin{verse}
$p \Rightarrow false \equiv \neg p$
\end{verse}

\noindent By substituting $\neg p$ for $p$ and using double negation, we derive
the theorem:

\begin{verse}
$\neg p \Rightarrow false \equiv p$\hspace{.2in}({\bf Proof by Contradiction})
\end{verse}

\noindent  Hence, having proved that $\neg p \Rightarrow false$ is a
theorem,
you may conclude that $p$ is a theorem.

\section{Proof by Contrapositive [GS]}


A typical proof of the implication $p \Rightarrow q$ might proceed as
follows (notice a combination of proof techniques, assuming the
antecedent and proof by contradiction):

\begin{itemize}
\item Assume $p$.
\item Prove $q$ by contradiction.  That is, assume $\neg q$ and prove
{\em false}.
\end{itemize}

\noindent This technique is really a proof by contrapositive in disguise:

\begin{verse}
$p \Rightarrow q \equiv \neg q \Rightarrow \neg p$\hspace{.2in}({\bf Contrapositive})
\end{verse}

\section{Proof Hints}

\begin{itemize}
\item Use the structure of an expression to guide what proof step to take
next.
\begin{itemize}
\item Look for subexpressions that you can replace with equivalent
expresssions.
\item Use algebraic and logical properties of logical connectives
and quantifiers
to rewrite formulae.  For example, use the One Point Rule to eliminate
the existential; use properties of implication (Section
\ref{sec:implication}) to get rid of implications; use properties
about quantifiers to move them outward across connectives.
\end{itemize}

\item Use lemmas and auxiliary definitions to add structure to your
proof.
\begin{itemize}
\item Introduce them to avoid repeating
the same subexpressions or subproofs.  (Sound familiar from your
programming
experience?)
\item Use them to make your proofs more readable, shorter, and more modular.
\end{itemize}

\item Suppose you have an expression, $e$, given in terms of an operator $f$.
(In fact you may introduced $f$ yourself following the hint above.)
\begin{itemize}
\item Expand the expression $e$ by replacing $f$ with its definition.
\item Then use properties about operators, $g$, in $f$'s definition to
manipulate and
simplify the expanded $e$.
\item At the end, reintroduce (if convenient or necessary)
the original $f$ using its definition (in the other direction).
\end{itemize}
\end{itemize}

\end{document}