565 lines
13 KiB
TeX
565 lines
13 KiB
TeX
\part{Backward Proofs}
|
|
|
|
\section{Motivation}
|
|
\frame[plain]{\partpage}
|
|
|
|
\begin{frame}[fragile]
|
|
\frametitle{Motivation I}
|
|
\begin{itemize}
|
|
\item let's prove \hol{!A B. A \holAnd{} B <=> B \holAnd{} A}
|
|
\begin{semiverbatim}
|
|
\scriptsize
|
|
\mlcomment{Show |- A \holAnd{} B ==> B \holAnd{} A}
|
|
val thm1a = ASSUME ``A \holAnd{} B``;
|
|
val thm1b = CONJ (CONJUNCT2 thm1a) (CONJUNCT1 thm1a);
|
|
val thm1 = DISCH ``A \holAnd{} B`` thm1b
|
|
|
|
\mlcomment{Show |- B \holAnd{} A ==> A \holAnd{} B}
|
|
val thm2a = ASSUME ``B \holAnd{} A``;
|
|
val thm2b = CONJ (CONJUNCT2 thm2a) (CONJUNCT1 thm2a);
|
|
val thm2 = DISCH ``B \holAnd{} A`` thm2b
|
|
|
|
\mlcomment{Combine to get |- A \holAnd{} B <=> B \holAnd{} A}
|
|
val thm3 = IMP_ANTISYM_RULE thm1 thm2
|
|
|
|
\mlcomment{Add quantifiers}
|
|
val thm4 = GENL [``A:bool``, ``B:bool``] thm3
|
|
\end{semiverbatim}
|
|
\bigskip
|
|
\item this is how you write down a proof
|
|
\item for finding a proof it is however often useful to think \emph{backwards}
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
|
|
\begin{frame}
|
|
\frametitle{Motivation II - thinking backwards}
|
|
\begin{itemize}
|
|
\item we want to prove \begin{itemize}
|
|
\item \hol{!A B. A \holAnd{} B <=> B \holAnd{} A}
|
|
\end{itemize}
|
|
\item all-quantifiers can easily be added later, so let's get rid of them \\
|
|
\begin{itemize}
|
|
\item \hol{A \holAnd{} B <=> B \holAnd{} A}
|
|
\end{itemize}
|
|
\item now we have an equivalence, let's show 2 implications \\
|
|
\begin{itemize}
|
|
\item \hol{A \holAnd{} B ==> B \holAnd{} A}
|
|
\item \hol{B \holAnd{} A ==> A \holAnd{} B}
|
|
\end{itemize}
|
|
\item we have an implication, so we can use the precondition as an assumption \\
|
|
\begin{itemize}
|
|
\item using \hol{A \holAnd{} B} show \hol{B \holAnd{} A}
|
|
\item \hol{A \holAnd{} B ==> B \holAnd{} A}
|
|
\end{itemize}
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
\begin{frame}
|
|
\frametitle{Motivation III - thinking backwards}
|
|
\begin{itemize}
|
|
\item we have a conjunction as assumption, let's split it
|
|
\begin{itemize}
|
|
\item using \hol{A} and \hol{B} show \hol{B \holAnd{} A}
|
|
\item \hol{A \holAnd{} B ==> B \holAnd{} A}
|
|
\end{itemize}
|
|
\item we have to show a conjunction, so let's show both parts
|
|
\begin{itemize}
|
|
\item using \hol{A} and \hol{B} show \hol{B}
|
|
\item using \hol{A} and \hol{B} show \hol{A}
|
|
\item \hol{A \holAnd{} B ==> B \holAnd{} A}
|
|
\end{itemize}
|
|
\item the first two proof obligations are trivial
|
|
\begin{itemize}
|
|
\item \hol{A \holAnd{} B ==> B \holAnd{} A}
|
|
\end{itemize}
|
|
\item \ldots
|
|
\item we are done
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
\begin{frame}
|
|
\frametitle{Motivation IV}
|
|
\begin{itemize}
|
|
\item common practise
|
|
\begin{itemize}
|
|
\item think backwards to find proof
|
|
\item write found proof down in forward style
|
|
\end{itemize}
|
|
\item often switch between backward and forward style within a proof\\
|
|
Example: induction proof
|
|
\begin{itemize}
|
|
\item backward step: induct on \ldots
|
|
\item forward steps: prove base case and induction case
|
|
\end{itemize}
|
|
\item whether to use forward or backward proofs depend on
|
|
\begin{itemize}
|
|
\item support by the interactive theorem prover you use
|
|
\begin{itemize}
|
|
\item HOL~4 and close family: emphasis on backward proof
|
|
\item Isabelle/HOL: emphasis on forward proof
|
|
\item Coq : emphasis on backward proof
|
|
\end{itemize}
|
|
\item your way of thinking
|
|
\item the theorem you try to prove
|
|
\end{itemize}
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
|
|
\begin{frame}
|
|
\frametitle{HOL Implementation of Backward Proofs}
|
|
\begin{itemize}
|
|
\item in HOL
|
|
\begin{itemize}
|
|
\item proof tactics / backward proofs used for most user-level proofs
|
|
\item forward proofs used usually for writing automation
|
|
\end{itemize}
|
|
\item backward proofs are implemented by \emph{tactics} in HOL
|
|
\begin{itemize}
|
|
\item decomposition into subgoals implemented in SML
|
|
\item SML datastructures used to keep track of all open subgoals
|
|
\item forward proof used to construct theorems
|
|
\end{itemize}
|
|
\item to understand backward proofs in HOL we need to look at
|
|
\begin{itemize}
|
|
\item \ml{goal} --- SML datatype for proof obligations
|
|
\item \ml{goalStack} --- library for keeping track of goals
|
|
\item \ml{tactic} --- SML type for functions performing backward proofs
|
|
\end{itemize}
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
|
|
\section{Backward Proofs}
|
|
|
|
\begin{frame}
|
|
\frametitle{Goals}
|
|
\begin{itemize}
|
|
\item goals represent proof obligations, \ie theorems we need/want to prove
|
|
\item the SML type \ml{goal} is an abbreviation for \ml{term list * term}
|
|
\item the goal \ml{([asm\_1, ..., asm\_n], c)} records that we need/want to prove the theorem
|
|
\ml{\{asm\_1, ..., asm\_n\} |- c}
|
|
\end{itemize}
|
|
|
|
\begin{exampleblock}{Example Goals}
|
|
\begin{tabular}{ll}
|
|
\textbf{Goal} & \textbf{Theorem} \\
|
|
\ml{([``A``, ``B``], ``A \holAnd{} B``)} & \ml{\{A, B\} |- A \holAnd{} B} \\
|
|
\ml{([``B``, ``A``], ``A \holAnd{} B``)} & \ml{\{A, B\} |- A \holAnd{} B} \\
|
|
\ml{([``B \holAnd{} A``], ``A \holAnd{} B``)} & \ml{\{B \holAnd{} A\} |- A \holAnd{} B} \\
|
|
\ml{([], ``(B \holAnd{} A) ==> (A \holAnd{} B)``)} & \ml{|- (B \holAnd{} A) ==> (A \holAnd{} B)} \\
|
|
\end{tabular}
|
|
\end{exampleblock}
|
|
|
|
\end{frame}
|
|
|
|
|
|
\begin{frame}
|
|
\frametitle{Tactics}
|
|
\begin{itemize}
|
|
\item the SML type \ml{tactic} is an abbreviation for\\ the type \ml{goal -> goal list * validation}
|
|
\item \ml{validation} is an abbreviation for \ml{thm list -> thm}
|
|
\item given a goal, a tactic
|
|
\begin{itemize}
|
|
\item decides into which subgoals to decompose the goal
|
|
\item returns this list of subgoals
|
|
\item returns a validation that
|
|
\begin{itemize}
|
|
\item given a list of theorems for the computed subgoals
|
|
\item produces a theorem for the original goal
|
|
\end{itemize}
|
|
\end{itemize}
|
|
\item special case: empty list of subgoals
|
|
\begin{itemize}
|
|
\item the validation (given \ml{[]}) needs to produce a theorem for the goal
|
|
\end{itemize}
|
|
\item notice: a tactic might be invalid
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
\begin{frame}[fragile]
|
|
\frametitle{Tactic Example --- \ml{CONJ\_TAC}}
|
|
\begin{center}
|
|
$\inferrule*[right={CONJ}]{\Gamma \entails p\\\Delta \entails q}{\Gamma \cup \Delta \entails p\ \wedge\ q}\qquad\qquad
|
|
\inferrule*{\texttt{t} \equiv \texttt{conj1 \holAnd{} conj2}\\\\
|
|
\texttt{asl} \entails \texttt{conj1}\\\texttt{asl} \entails \texttt{conj2}}
|
|
{\texttt{asl} \entails \texttt{t}}$
|
|
\end{center}
|
|
\begin{semiverbatim}
|
|
\small
|
|
val CONJ_TAC: tactic = fn (asl, t) =>
|
|
let
|
|
val (conj1, conj2) = dest_conj t
|
|
in
|
|
([(asl, conj1), (asl, conj2)],
|
|
fn [th1, th2] => CONJ th1 th2 | _ => raise Match)
|
|
end
|
|
handle HOL_ERR _ => raise ERR "CONJ_TAC" ""
|
|
\end{semiverbatim}
|
|
\end{frame}
|
|
|
|
\begin{frame}[fragile]
|
|
\frametitle{Tactic Example --- \ml{EQ\_TAC}}
|
|
\begin{center}
|
|
$\inferrule*[right=IMP\_ANTISYM\_RULE]{\Gamma \entails p \Longrightarrow q\\\\\Delta \entails q \Longrightarrow p}{\Gamma \cup \Delta \entails p = q}
|
|
\qquad\qquad
|
|
\inferrule*{\texttt{t} \equiv \texttt{lhs = rhs}\\\\
|
|
\texttt{asl} \entails \texttt{lhs ==> rhs}\\\\
|
|
\texttt{asl} \entails \texttt{rhs ==> lhs}}
|
|
{\texttt{asl} \entails \texttt{t}}$
|
|
\end{center}
|
|
\begin{semiverbatim}
|
|
\small
|
|
val EQ_TAC: tactic = fn (asl, t) =>
|
|
let
|
|
val (lhs, rhs) = dest_eq t
|
|
in
|
|
([(asl, mk_imp (lhs, rhs)), (asl, mk_imp (rhs, lhs))],
|
|
fn [th1, th2] => IMP_ANTISYM_RULE th1 th2
|
|
| _ => raise Match)
|
|
end
|
|
handle HOL_ERR _ => raise ERR "EQ_TAC" ""
|
|
\end{semiverbatim}
|
|
\end{frame}
|
|
|
|
\begin{frame}
|
|
\frametitle{proofManagerLib / goalStack}
|
|
\begin{itemize}
|
|
\item the \ml{proofManagerLib} keeps track of open goals
|
|
\item it uses \ml{goalStack} internally
|
|
\item important commands
|
|
\begin{itemize}
|
|
\item \emph{g} --- set up new goal
|
|
\item \emph{e} --- expand a tactic
|
|
\item \emph{p} --- print the current status
|
|
\item \emph{top\_thm} --- get the proved thm at the end
|
|
\end{itemize}
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
\begin{frame}[fragile]
|
|
\frametitle{Tactic Proof Example I}
|
|
|
|
\begin{block}{Previous Goalstack}
|
|
\begin{semiverbatim}
|
|
-
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{User Action}
|
|
\begin{semiverbatim}
|
|
g `!A B. A \holAnd{} B <=> B \holAnd{} A`;
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{New Goalstack}
|
|
\begin{semiverbatim}
|
|
Initial goal:
|
|
|
|
!A B. A \holAnd{} B <=> B \holAnd{} A
|
|
|
|
: proof
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
\end{frame}
|
|
|
|
|
|
\begin{frame}[fragile]
|
|
\frametitle{Tactic Proof Example II}
|
|
|
|
\begin{block}{Previous Goalstack}
|
|
\begin{semiverbatim}
|
|
Initial goal:
|
|
|
|
!A B. A \holAnd{} B <=> B \holAnd{} A
|
|
|
|
: proof
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{User Action}
|
|
\begin{semiverbatim}
|
|
e GEN_TAC;
|
|
e GEN_TAC;
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{New Goalstack}
|
|
\begin{semiverbatim}
|
|
A \holAnd{} B <=> B \holAnd{} A
|
|
|
|
: proof
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
\end{frame}
|
|
|
|
|
|
\begin{frame}[fragile]
|
|
\frametitle{Tactic Proof Example III}
|
|
|
|
\begin{block}{Previous Goalstack}
|
|
\begin{semiverbatim}
|
|
A \holAnd{} B <=> B \holAnd{} A
|
|
|
|
: proof
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{User Action}
|
|
\begin{semiverbatim}
|
|
e EQ_TAC;
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{New Goalstack}
|
|
\begin{semiverbatim}
|
|
B \holAnd{} A ==> A \holAnd{} B
|
|
|
|
A \holAnd{} B ==> B \holAnd{} A
|
|
|
|
: proof
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
\end{frame}
|
|
|
|
|
|
\begin{frame}[fragile]
|
|
\frametitle{Tactic Proof Example IV}
|
|
|
|
\begin{block}{Previous Goalstack}
|
|
\begin{semiverbatim}
|
|
B \holAnd{} A ==> A \holAnd{} B
|
|
|
|
A \holAnd{} B ==> B \holAnd{} A : proof
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{User Action}
|
|
\begin{semiverbatim}
|
|
e STRIP_TAC;
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{New Goalstack}
|
|
\begin{semiverbatim}
|
|
B \holAnd{} A
|
|
------------------------------------
|
|
0. A
|
|
1. B
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
\end{frame}
|
|
|
|
\begin{frame}[fragile]
|
|
\frametitle{Tactic Proof Example V}
|
|
|
|
\begin{block}{Previous Goalstack}
|
|
\begin{semiverbatim}
|
|
\scriptsize{}B \holAnd{} A
|
|
------------------------------------
|
|
0. A
|
|
1. B
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{User Action}
|
|
\begin{semiverbatim}
|
|
\scriptsize{}e CONJ_TAC;
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{New Goalstack}
|
|
\begin{semiverbatim}
|
|
\scriptsize{}A
|
|
------------------------------------
|
|
0. A
|
|
1. B
|
|
|
|
B
|
|
------------------------------------
|
|
0. A
|
|
1. B
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
\end{frame}
|
|
|
|
|
|
\begin{frame}[fragile]
|
|
\frametitle{Tactic Proof Example VI}
|
|
|
|
\begin{block}{Previous Goalstack}
|
|
\begin{semiverbatim}
|
|
\scriptsize{}A
|
|
------------------------------------
|
|
0. A
|
|
1. B
|
|
|
|
B
|
|
------------------------------------
|
|
0. A
|
|
1. B
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{User Action}
|
|
\begin{semiverbatim}
|
|
\scriptsize{}e (ACCEPT_TAC (ASSUME ``B:bool``));
|
|
e (ACCEPT_TAC (ASSUME ``A:bool``));
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{New Goalstack}
|
|
\begin{semiverbatim}
|
|
\scriptsize{}B \holAnd{} A ==> A \holAnd{} B
|
|
|
|
: proof
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
\end{frame}
|
|
|
|
|
|
\begin{frame}[fragile]
|
|
\frametitle{Tactic Proof Example VII}
|
|
|
|
\begin{block}{Previous Goalstack}
|
|
\begin{semiverbatim}
|
|
\scriptsize{}B \holAnd{} A ==> A \holAnd{} B
|
|
|
|
: proof
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{User Action}
|
|
\begin{semiverbatim}
|
|
\scriptsize{}e STRIP_TAC;
|
|
e (ASM_REWRITE_TAC[]);
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{New Goalstack}
|
|
\begin{semiverbatim}
|
|
\scriptsize{}Initial goal proved.
|
|
|- !A B. A \holAnd{} B <=> B \holAnd{} A:
|
|
proof
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
\end{frame}
|
|
|
|
|
|
\begin{frame}[fragile]
|
|
\frametitle{Tactic Proof Example VIII}
|
|
|
|
\begin{block}{Previous Goalstack}
|
|
\begin{semiverbatim}
|
|
\scriptsize{}Initial goal proved.
|
|
|- !A B. A \holAnd{} B <=> B \holAnd{} A:
|
|
proof
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{User Action}
|
|
\begin{semiverbatim}
|
|
\scriptsize{}val thm = top_thm();
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{Result}
|
|
\begin{semiverbatim}
|
|
\scriptsize{}val thm =
|
|
|- !A B. A \holAnd{} B <=> B \holAnd{} A:
|
|
thm
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\end{frame}
|
|
|
|
|
|
\begin{frame}[fragile]
|
|
\frametitle{Tactic Proof Example IX}
|
|
|
|
\begin{block}{Combined Tactic}
|
|
\begin{semiverbatim}
|
|
\scriptsize{}val thm = prove (``!A B. A \holAnd{} B <=> B \holAnd{} A``,
|
|
GEN_TAC >> GEN_TAC >>
|
|
EQ_TAC >| [
|
|
STRIP_TAC >>
|
|
STRIP_TAC >| [
|
|
ACCEPT_TAC (ASSUME ``B:bool``),
|
|
ACCEPT_TAC (ASSUME ``A:bool``)
|
|
],
|
|
|
|
STRIP_TAC >>
|
|
ASM_REWRITE_TAC[]
|
|
]);
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{Result}
|
|
\begin{semiverbatim}
|
|
\scriptsize{}val thm =
|
|
|- !A B. A \holAnd{} B <=> B \holAnd{} A:
|
|
thm
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
\end{frame}
|
|
|
|
\begin{frame}[fragile]
|
|
\frametitle{Tactic Proof Example X}
|
|
|
|
\begin{block}{Cleaned-up Tactic}
|
|
\begin{semiverbatim}
|
|
\scriptsize{}val thm = prove (``!A B. A \holAnd{} B <=> B \holAnd{} A``,
|
|
REPEAT GEN_TAC >>
|
|
EQ_TAC >> (
|
|
REPEAT STRIP_TAC >>
|
|
ASM_REWRITE_TAC []
|
|
));
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\begin{block}{Result}
|
|
\begin{semiverbatim}
|
|
\scriptsize{}val thm =
|
|
|- !A B. A \holAnd{} B <=> B \holAnd{} A:
|
|
thm
|
|
\end{semiverbatim}
|
|
\end{block}
|
|
|
|
\end{frame}
|
|
|
|
|
|
\section{General Discussion}
|
|
|
|
\begin{frame}
|
|
\frametitle{Summary Backward Proofs}
|
|
\begin{itemize}
|
|
\item in HOL most user-level proofs are tactic-based
|
|
\begin{itemize}
|
|
\item automation often written in forward style
|
|
\item low-level, basic proofs written in forward style
|
|
\item nearly everything else is written in backward (tactic) style
|
|
\end{itemize}
|
|
\item there are \emph{many} different tactics
|
|
\item in the lecture only the most basic ones will be discussed
|
|
\item \alert{you need to learn about tactics on your own}
|
|
\begin{itemize}
|
|
\item good starting point: \texttt{Quick} manual
|
|
\item learning finer points takes a lot of time
|
|
\item exercises require you to read up on tactics
|
|
\end{itemize}
|
|
\item often there are many ways to prove a statement, which tactics to use depends on
|
|
\begin{itemize}
|
|
\item personal way of thinking
|
|
\item personal style and preferences
|
|
\item maintainability, clarity, elegance, robustness
|
|
\item \ldots
|
|
\end{itemize}
|
|
\end{itemize}
|
|
\end{frame}
|
|
|
|
%%% Local Variables:
|
|
%%% mode: latex
|
|
%%% TeX-master: "current"
|
|
%%% End:
|