thtuerk/ITP-Course
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

initial version

Browse Source 
cleaned-up the sources of the ITP course
- remove internal notes
- remove exercise solutions
- remove KTH logo
- add Creative Commons license
This commit is contained in:
Thomas Türk
2019-11-11 10:22:43 +01:00
commit 3c35cc25c3
71 changed files with 35906 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

40
lectures/00_webpage_intro.tex Normal file
View File

@ -0,0 +1,40 @@
\part{Preface}
\frame[plain]{\partpage}
\begin{frame}
\frametitle{Preface}
\begin{itemize}
\item these slides originate from a course for advanced master students
\item it was given by the PROSPER group at KTH in Stockholm in 2017 (see \small{\url{https://www.kth.se/social/group/interactive-theorem-}})
\item the course focused on how to use HOL~4
\item students taking the course were expected to
\begin{itemize}
\item know functional programming, esp.\ SML
\item understand predicate logic
\item have some experience with pen and paper proofs
\end{itemize}
\item the course consisted of 9 lectures, which each took 90 minutes
\item there were 19 supervised practical sessions, which each took 2 h
\item usually there was 1 lecture and 2 practical sessions each week
\item students were expected to work about 10 h each week on exercises
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Preface II}
\begin{itemize}
\item usually, these slides present concepts and some high-level entry points
\item often some more details were explained than covered on the slides
\item technical details were covered in the practical sessions
\item they are provided as they are in the hope that they are useful\footnote{if you find errors, please contact Thomas Tuerk} (there are no guarentees of correctness :-))
\item the exercise question-sheets are available as well
\item if you have questions, feel free to contact Thomas Tuerk (\texttt{thomas@tuerk-brechen.de})
\end{itemize}
\end{frame}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "hol"
%%% End:

261
lectures/01_introduction.tex Normal file
View File

@ -0,0 +1,261 @@
\part{Introduction}
\frame[plain]{\partpage}
\section{Motivation}
\begin{frame}
\frametitle{Motivation}
\begin{itemize}
\item Complex systems almost certainly contain bugs.
\item Critical systems (\eg avionics) need to meet very high standards.
\item It is infeasible in practice to achieve such high standards just by testing.
\item Debugging via testing suffers from diminishing returns.
\end{itemize}
\bigskip
\begin{raggedleft}
\emph{``Program testing can be used to show the presence\\
of bugs, but never to show their absence!''\\
--- Edsger W. Dijkstra\\}
\end{raggedleft}
\end{frame}
\begin{frame}
\frametitle{Famous Bugs}
\begin{itemize}
\item Pentium FDIV bug (1994)\\(missing entry in lookup table, \$475 million damage)
\item Ariane V explosion (1996)\\(integer overflow, \$1 billion prototype destroyed)
\item Mars Climate Orbiter (1999)\\(destroyed in Mars orbit, mixup of units pound-force and newtons)
\item Knight Capital Group Error in Ultra Short Time Trading (2012)\\
(faulty deployment, repurposing of critical flag, \$440 lost in 45 min on stock exchange)
\item \ldots
\end{itemize}
\begin{block}{Fun to read}
\url{http://www.cs.tau.ac.il/~nachumd/verify/horror.html}
\url{https://en.wikipedia.org/wiki/List_of_software_bugs}
\end{block}
\end{frame}
\begin{frame}
\frametitle{Proof}
\begin{itemize}
\item proof can show absence of errors in design
\item but proofs talk about a \emph{design}, not a \emph{real system}
\item $\Rightarrow$ testing and proving complement each other
\end{itemize}
\bigskip
\begin{raggedleft}
\emph{``As far as the laws of mathematics\\
refer to reality, they are not certain;\\
and as far as they are certain,\\
they do not refer to reality.''\\
--- Albert Einstein\\}
\end{raggedleft}
\end{frame}
\section{Types of Proofs}
\begin{frame}
\frametitle{Mathematical vs.\ Formal Proof}
\begin{columns}
\begin{column}{0.45\textwidth}
\begin{block}{Mathematical Proof}
\begin{itemize}
\item informal, convince other mathematicians
\item checked by community of domain experts
\item subtle errors are hard to find
\item often provide some new insight about our world
\item often short, but require creativity and a brilliant idea
\end{itemize}
\end{block}
\end{column}
\begin{column}{0.45\textwidth}
\begin{block}{Formal Proof}
\begin{itemize}
\item formal, rigorously use a logical formalism
\item checkable by \textit{stupid} machines
\item very reliable
\item often contain no new ideas and no amazing insights
\item often long, very tedious, but largely trivial
\end{itemize}
\end{block}
\end{column}
\end{columns}
\begin{center}
\textbf{We are interested in formal proofs in this lecture.}
\end{center}
\end{frame}
% \begin{frame}
% \frametitle{Detail Level of Formal Proof}
% \begin{center}
% In \emph{Principia Mathematica} it takes 300 pages to prove 1+1=2.
% \bigskip
% This is nicely illustrated in \emph{Logicomix - An Epic Search for Truth}.
% \includegraphics[width=10cm]{images/1+12_Logicomix.png}
% \end{center}
% \end{frame}
\begin{frame}
\frametitle{Automated vs Manual (Formal) Proof}
\begin{block}{Fully Manual Proof}
\begin{itemize}
\item very tedious; one has to grind through many trivial but detailed proofs
\item easy to make mistakes
\item hard to keep track of all assumptions and preconditions
\item hard to maintain, if something changes (see Ariane V)
\end{itemize}
\end{block}
\begin{block}{Automated Proof}
\begin{itemize}
\item amazing success in certain areas
\item but still often infeasible for interesting problems
\item hard to get insights in case a proof attempt fails
\item even if it works, it is often not that automated
\begin{itemize}
\item run automated tool for a few days
\item abort, change command line arguments to use different heuristics
\item run again and iterate till you find a set of heuristics that prove it fully automatically in a few seconds
\end{itemize}
\end{itemize}
\end{block}
\end{frame}
\begin{frame}
\frametitle{Interactive Proofs}
\begin{itemize}
\item combine strengths of manual and automated proofs
\item many different options to combine automated and manual proofs
\begin{itemize}
\item mainly check existing proofs (\eg HOL Zero)
\item user mainly provides lemmata statements, computer searches proofs using previous lemmata and very few hints (\eg ACL 2)
\item most systems are somewhere in the middle
\end{itemize}
\item typically the human user
\begin{itemize}
\item provides insights into the problem
\item structures the proof
\item provides main arguments
\end{itemize}
\item typically the computer
\begin{itemize}
\item checks proof
\item keeps track of all used assumptions
\item provides automation to grind through lengthy, but trivial proofs
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Typical Interactive Proof Activities}
\begin{itemize}
\item provide precise definitions of concepts
\item state properties of these concepts
\item prove these properties
\begin{itemize}
\item human provides insight and structure
\item computer does book-keeping and automates simple proofs
\end{itemize}
\item build and use libraries of formal definitions and proofs
\begin{itemize}
\item formalisations of mathematical theories like
\begin{itemize}
\item lists, sets, bags, \ldots
\item real numbers
\item probability theory
\end{itemize}
\item specifications of real-world artefacts like
\begin{itemize}
\item processors
\item programming languages
\item network protocols
\end{itemize}
\item reasoning tools
\end{itemize}
\end{itemize}
\begin{center}
\textbf{There is a strong connection with programming.\\Lessons learned in Software Engineering apply.}
\end{center}
\end{frame}
\section{Interactive Theorem Provers}
\begin{frame}
\frametitle{Different Interactive Provers}
\begin{itemize}
\item there are many different interactive provers, \eg
\begin{itemize}
\item Isabelle/HOL
\item Coq
\item PVS
\item HOL family of provers
\item ACL2
\item \ldots
\end{itemize}
\item important differences
\begin{itemize}
\item the formalism used
\item level of trustworthiness
\item level of automation
\item libraries
\item languages for writing proofs
\item user interface
\item \ldots
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Which theorem prover is the best one? :-)}
\begin{itemize}
\item there is no \alert{best} theorem prover
\item better question: Which is the \alert{best one for a certain purpose}?
\item important points to consider
\begin{itemize}
\item existing libraries
\item used logic
\item level of automation
\item user interface
\item importance development speed versus trustworthiness
\item How familiar are you with the different provers?
\item Which prover do people in your vicinity use?
\item your personal preferences
\item \ldots
\end{itemize}
\end{itemize}
\bottomstatement{In this course we use the HOL theorem prover,\\ because it is used by the TCS group.}
\end{frame}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "full"
%%% End:

159
lectures/02_organisational_matters.tex Normal file
View File

@ -0,0 +1,159 @@
\part{Organisational Matters}
\frame[plain]{\partpage}
\begin{frame}
\frametitle{Aims of this Course}
\begin{block}{Aims}
\begin{itemize}
\item introduction to interactive theorem proving (ITP)
\item being able to evaluate whether a problem can benefit from ITP
\item hands-on experience with HOL
\item learn how to build a formal model
\item learn how to express and prove important properties of such a model
\item learn about basic conformance testing
\item use a theorem prover on a small project
\end{itemize}
\end{block}
\begin{block}{Required Prerequisites}
\begin{itemize}
\item some experience with functional programming
\item knowing Standard ML syntax
\item basic knowledge about logic (\eg First Order Logic)
\end{itemize}
\end{block}
\end{frame}
\begin{frame}
\frametitle{Dates}
\begin{itemize}
\item Interactive Theorem Proving Course takes place in Period 4 of the academic year 2016/2017
\item always in room 4523 or 4532
\item each week\\\medskip\qquad
\begin{tabular}{lll}
Mondays & 10:15 - 11:45 & lecture \\
Wednesdays & 10:00 - 12:00 & practical session \\
Fridays & 13:00 - 15:00 & practical session
\end{tabular}
\item no lecture on Monday, 1st of May, instead on Wednesday, 3rd May
\item last lecture: 12th of June
\item last practical session: 21st of June
\item 9 lectures, 17 practical sessions
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Exercises}
\begin{itemize}
\item after each lecture an exercise sheet is handed out
\item work on these exercises alone, except if stated otherwise explicitly
\item exercise sheet contains due date
\begin{itemize}
\item usually 10 days time to work on it
\item hand in during practical sessions
\item lecture Monday $\longrightarrow$ hand in at latest in next week's Friday session
\end{itemize}
\item main purpose: understanding ITP and learn how to use HOL
\begin{itemize}
\item no detailed grading, just pass/fail
\item retries possible till pass
\item if stuck, ask me or one another
\item practical sessions intend to provide this opportunity
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Practical Sessions}
\begin{itemize}
\item very informal
\item main purpose: work on exercises
\begin{itemize}
\item I have a look and provide feedback
\item you can ask questions
\item I might sometimes explain things not covered in the lectures
\item I might provide some concrete tips and tricks
\item you can also discuss with each other
\end{itemize}
\item attendance not required, but highly recommended
\begin{itemize}
\item exception: session on 21st April
\end{itemize}
\item only requirement: turn up long enough to hand in exercises
\item \alert{you need to bring your own computer}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Handing-in Exercises}
\begin{itemize}
\item exercises are intended to be handed-in during practical sessions
\item attend at least one practical session each week
\item leave reasonable time to discuss exercises
\begin{itemize}
\item don't try to hand your solution in Friday 14:55
\end{itemize}
\item retries possible, but reasonable attempt before deadline required
\item handing-in outside practical sessions
\begin{itemize}
\item only if you have a good reason
\item decided on a case-by-case basis
\end{itemize}
\item electronic hand-ins
\begin{itemize}
\item only to get detailed feedback
\item does not replace personal hand-in
\item exceptions on a case-by-case basis if there is a good reason
\item I recommend using a KTH GitHub repo
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Passing the ITP Course}
\begin{itemize}
\item there is only a pass/fail mark
\item to pass you need to
\begin{itemize}
\item attend at least 7 of the 9 lectures
\item pass 8 of the 9 exercises
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Communication}
\begin{itemize}
\item we have the advantage of being a small group
\item therefore we are flexible
\item so please ask questions, even during lectures
\item there are many shy people, therefore
\begin{itemize}
\item anonymous checklist after each lecture
\item anonymous background questionnaire in first practical session
\end{itemize}
\item further information is posted on \emph{Interactive Theorem Proving Course} group on Group Web
\item contact me (Thomas Tuerk) directly, \eg via email \texttt{thomas@kth.se}
\end{itemize}
\end{frame}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "full"
%%% End:

175
lectures/03_hol_overview.tex Normal file
View File

@ -0,0 +1,175 @@
\part{HOL~4 History and Architecture}
\frame[plain]{\partpage}
\section{LCF}
\begin{frame}
\frametitle{LCF - Logic of Computable Functions}
\begin{itemize}
\item \emph{Standford LCF} 1971-72 by Milner et al.
\item formalism devised by Dana Scott in 1969
\item intended to reason about recursively defined functions
\item intended for computer science applications
\item strengths
\begin{itemize}
\item powerful simplification mechanism
\item support for backward proof
\end{itemize}
\item limitations
\begin{itemize}
\item proofs need a lot of memory
\item fixed, hard-coded set of proof commands
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{LCF - Logic of Computable Functions II}
\begin{itemize}
\item Milner worked on improving LCF in Edinburgh
\item research assistants
\begin{itemize}
\item Lockwood Morris
\item Malcolm Newey
\item Chris Wadsworth
\item Mike Gordon
\end{itemize}
\item \emph{Edinburgh LCF} 1979
\item introduction of \emph{Meta Language} (ML)
\item ML was invented to write proof procedures
\item ML became an influential functional programming language
\item using ML allowed implementing the \emph{LCF approach}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{LCF Approach}
\begin{itemize}
\item implement an abstract datatype \alert{thm} to represent theorems
\item semantics of ML ensure that values of type thm can only be created using its interface
\item interface is very small
\begin{itemize}
\item predefined theorems are axioms
\item function with result type theorem are inferences
\end{itemize}
\item interface is carefully designed and checked
\begin{itemize}
\item size of interface and implementation allow careful checking
\item one checks that the interface really implements only axioms and inferences that are valid in the used logic
\end{itemize}
\item \emph{However you create a theorem, there is a proof for it.}
\item together with similar abstract datatypes for types and terms, this forms the \alert{kernel}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{LCF Approach II}
\begin{exampleblock}{Modus Ponens Example}
\begin{columns}
\begin{column}{.4\textwidth}
\textbf{Inference Rule}\\\medskip
\inferrule{\Gamma \vdash a \Rightarrow b \\ \Delta \entails a}{\Gamma \cup \Delta \entails b}
\end{column}
\begin{column}{.5\textwidth}
\textbf{SML function}\\\medskip
\texttt{val MP\ :\ thm -> thm -> thm}
$\texttt{MP} (\Gamma \vdash a \Rightarrow b) (\Delta \entails a) = (\Gamma \cup \Delta \entails b)$
\end{column}
\end{columns}
\end{exampleblock}
\begin{itemize}
\item very trustworthy --- only the small kernel needs to be trusted
\item efficient --- no need to store proofs
\begin{block}{Easy to extend and automate}
However complicated and potentially buggy your code is, if a value of type theorem is produced, it has been created through the small trusted interface. Therefore the statement really holds.
\end{block}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{LCF Style Systems}
There are now many interactive theorem provers out there that use
an approach similar to that of Edinburgh LCF.
\begin{itemize}
\item HOL family
\begin{itemize}
\item HOL theorem prover
\item HOL Light
\item HOL Zero
\item Proof Power
\item $\ldots$
\end{itemize}
\item Isabelle
\item Nuprl
\item Coq
\item \ldots
\end{itemize}
\end{frame}
\section{History and Family of HOL}
\begin{frame}
\frametitle{History of HOL}
\begin{itemize}
\item 1979 Edinburgh LCF by Milner, Gordon, et al.
\item 1981 Mike Gordon becomes lecturer in Cambridge
\item 1985 Cambridge LCF
\begin{itemize}
\item Larry Paulson and G\`{e}rard Huet
\item implementation of ML compiler
\item powerful simplifier
\item various improvements and extensions
\end{itemize}
\item 1988 HOL
\begin{itemize}
\item Mike Gordon and Keith Hanna
\item adaption of Cambridge LCF to classical higher order logic
\item intention: hardware verification
\end{itemize}
\item 1990 HOL90\\ reimplementation in SML by Konrad Slind at University of Calgary
\item 1998 HOL98\\ implementation in Moscow ML and new library and theory mechanism
\item since then HOL Kananaskis releases, called informally \alert{HOL~4}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Family of HOL}
\begin{columns}
\begin{column}{.65\textwidth}
\begin{itemize}
\item \emph{ProofPower}\\commercial version of HOL88 by Roger Jones, Rob Arthan et al.
\item \emph{HOL Light}\\lean CAML / OCaml port by John Harrison
\item \emph{HOL Zero}\\trustworthy proof checker by Mark Adams
\item \emph{Isabelle}
\begin{itemize}
\item 1990 by Larry Paulson
\item meta-theorem prover that supports multiple logics
\item however, mainly HOL used, ZF a little
\item nowadays probably the most widely used HOL system
\item originally designed for software verification
\end{itemize}
\end{itemize}
\end{column}
\qquad
\begin{column}{.3\textwidth}
\includegraphics[width=3.2cm]{images/hol-family}
\end{column}
\end{columns}
\end{frame}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "hol"
%%% End:

267
lectures/04_hol_logic.tex Normal file
View File

@ -0,0 +1,267 @@
\part{HOL's Logic}
\frame[plain]{\partpage}
\section{HOL Logic}
\begin{frame}
\frametitle{HOL Logic}
\begin{itemize}
\item the HOL theorem prover uses a version of classical \textbf{h}igher \textbf{o}rder \textbf{l}ogic:\\
classical higher order predicate calculus with \\
terms from the typed lambda calculus (\ie simple type theory)
\item this sounds complicated, but is intuitive for SML programmers
\item (S)ML and HOL logic designed to fit each other
\item if you understand SML, you understand HOL logic
\bigskip
\begin{center}
\emph{HOL = functional programming + logic}
\end{center}
\bigskip
\begin{alertblock}{Ambiguity Warning}
The acronym \textit{HOL} refers to both the \textit{HOL interactive theorem prover} and the \textit{HOL logic} used by it. It's also a common abbreviation for \textit{higher order logic} in general.
\end{alertblock}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Types}
\begin{itemize}
\item SML datatype for types
\begin{itemize}
\item \emph{Type Variables} ($\texttt{'a},\ \alpha,\ \texttt{'b},\ \beta,\ \ldots$)\\
Type variables are implicitly universally quantified. Theorems containing type variables
hold for all instantiations of these. Proofs using type variables can be seen as proof schemata.
\item \emph{Atomic Types} ($\texttt{c}$)\\
Atomic types denote fixed types. Examples: \texttt{num}, \texttt{bool}, \texttt{unit}
\item \emph{Compound Types} ($(\sigma_1, \ldots, \sigma_n) \textit{op}$)\\
\textit{op} is a \alert{type operator} of arity \textit{n} and $\sigma_1, \ldots, \sigma_n$ \alert{argument types}. Type operators denote operations for constructing types.\\
Examples: \texttt{num list} or \texttt{'a \# 'b}.
\item \emph{Function Types} ($\sigma_1 \to \sigma_2$)\\
$\sigma_1 \to \sigma_2$ is the type of \alert{total} functions from $\sigma_1$ to $\sigma_2$.
\end{itemize}
\item types are never empty in HOL, \ie\\
for each type at least one value exists
\item all HOL functions are total
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Terms}
\begin{itemize}
\item SML datatype for terms
\begin{itemize}
\item \emph{Variables} ($\texttt{x}, \texttt{y}, \ldots$)
\item \emph{Constants} ($\texttt{c}, \ldots$)
\item \emph{Function Application} ($\texttt{f a}$)
\item \emph{Lambda Abstraction} ($\texttt{\textbackslash x.\ f x}$\ \ or\ \ $\lambda x.\ f x$)\\
Lambda abstraction represents anonymous function definition.\\The corresponding SML syntax is \texttt{fn x => f x}.
\end{itemize}
\item terms have to be well-typed
\item same typing rules and same type-inference as in SML take place
\item terms very similar to SML expressions
\item notice: predicates are functions with return type \texttt{bool}, \ie
no distinction between functions and predicates, terms and formulae
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Terms II}
\begin{tabular}{lll}
\textbf{HOL term} & \textbf{SML expression} & \textbf{type HOL / SML} \\
\hol{0} & \ml{0} & \hol{num} / \ml{int} \\
\hol{x:'a} & \ml{x:'a} & variable of type \hol{'a} \\
\hol{x:bool} & \ml{x:bool} & variable of type \hol{bool} \\
\hol{x + 5} & \ml{x + 5} & applying function \hol{+} to \hol{x} and \hol{5} \\
\hol{\textbackslash x.\ x + 5} & \ml{fn x => x + 5} & anonymous (\aka inline) function \\
& & of type \hol{num -> num} \\
\hol{(5, T)} & \ml{(5, true)} & \hol{num \# bool} / \ml{int * bool}\\
\hol{[5;3;2]++[6]} & \ml{[5,3,2]@[6]} & \hol{num list} / \ml{int list}
\end{tabular}
\end{frame}
\begin{frame}
\frametitle{Free and Bound Variables / Alpha Equivalence}
\begin{itemize}
\item in SML, the names of function arguments does not matter (much)
\item similarly in HOL, the names of variables used by lambda-abstractions does not matter (much)
\item the lambda-expression $\lambda x.\ t$ is said to \emph{bind} the variables $x$ in term $t$
\item variables that are guarded by a lambda expression are called \emph{bound}
\item all other variables are \emph{free}
\item Example: $x$ is free and $y$ is bound in \hol{$(x = 5) \wedge (\lambda y.\ (y < x))\ 3$}
\item the names of bound variables are unimportant semantically
\item two terms are called \emph{alpha-equivalent} iff they differ only in the names of bound variables
\item Example: \hol{$\lambda{}x.\ x$} and \hol{$\lambda{}y.\ y$} are alpha-equivalent
\item Example: \hol{$x$} and \hol{$y$} are not alpha-equivalent
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Theorems}
\begin{itemize}
\item theorems are of the form $\Gamma \entails p$ where
\begin{itemize}
\item $\Gamma$ is a set of hypothesis
\item $p$ is the conclusion of the theorem
\item all elements of $\Gamma$ and $p$ are formulae, \ie terms of type \texttt{bool}
\end{itemize}
\item $\Gamma \entails p$ records that using $\Gamma$ the statement $p$ \alert{has been} proved\\
\item notice difference to logic: there it means \alert{can be} proved
\item the proof itself is not recorded
\item theorems can only be created through a small interface in the \emph{kernel}
\end{itemize}
\end{frame}
\section{Kernel}
\begin{frame}
\frametitle{HOL Light Kernel}
\begin{itemize}
\item the HOL kernel is hard to explain
\begin{itemize}
\item for historic reasons some concepts are represented rather complicated
\item for speed reasons some derivable concepts have been added
\end{itemize}
\item instead consider the HOL Light kernel, which is a cleaned-up version
\item there are two predefined constants
\begin{itemize}
\item \texttt{= :\ 'a -> 'a -> bool}
\item \texttt{@ :\ ('a -> bool) -> 'a}
\end{itemize}
\item there are two predefined types
\begin{itemize}
\item \texttt{bool}
\item \texttt{ind}
\end{itemize}
\item the meaning of these types and constants is given by inference rules and axioms
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{HOL Light Inferences I}
\begin{columns}
\begin{column}{.45\textwidth}
\begin{center}
$\inferrule* [right=REFL] {\ }{\entails t = t}$\\[1em]
$\inferrule*[right=TRANS] {\Gamma \entails s = t\\\Delta \entails t = u}{\Gamma \cup \Delta \entails s = u}$\\[1em]
$\inferrule*[right=COMB]{\Gamma \entails s = t\\\Delta \entails u = v \\\\ \textit{types fit}}{\Gamma \cup \Delta \entails s(u) = t(v)}$\\[1em]
\end{center}
\end{column}
\begin{column}{.45\textwidth}
\begin{center}
$\inferrule*[right=ABS]{\Gamma \entails s = t\\x\ \textit{not free in}\ \Gamma}{\Gamma \entails \lambda{}x.\ s = \lambda{}x.\ t}$\\[1em]
$\inferrule*[right=BETA]{\ }{\entails (\lambda{}x.\ t)\, x = t}$\\[1em]
$\inferrule*[right=ASSUME]{\ }{\{p\}\entails p}$
\end{center}
\end{column}
\end{columns}
\end{frame}
\begin{frame}
\frametitle{HOL Light Inferences II}
\begin{center}
$\inferrule*[right=EQ\_MP]{\Gamma \entails p \Leftrightarrow q\\\Delta \entails p}{\Gamma \cup \Delta \entails q}$\\[1em]
$\inferrule*[right=DEDUCT\_ANTISYM\_RULE]{\Gamma \entails p\\\Delta \entails q}
{(\Gamma-\{q\}) \cup (\Delta - \{p\}) \entails p \Leftrightarrow q}$\\[1em]
$\inferrule*[right=INST]{\Gamma[x_1, \ldots, x_n] \entails p[x_1, \ldots, x_n]}
{\Gamma[t_1, \ldots, t_n] \entails p[t_1, \ldots, t_n]}$\\[1em]
$\inferrule*[right=INST\_TYPE]{\Gamma[\alpha_1, \ldots, \alpha_n] \entails p[\alpha_1, \ldots, \alpha_n]}
{\Gamma[\gamma_1, \ldots, \gamma_n] \entails p[\gamma_1, \ldots, \gamma_n]}$\\[1em]
\end{center}
\end{frame}
\newcommand{\tabitem}{~~\llap{\textbullet}~~}
\begin{frame}
\frametitle{HOL Light Axioms and Definition Principles}
\begin{itemize}
\item 3 axioms needed\medskip\\\qquad
\begin{tabular}{ll}
ETA\_AX & $|- (\lambda{}x.\ t\ x) = t$ \\
SELECT\_AX & $|- P\ x \Longrightarrow P ((@) P))$ \\
INFINITY\_AX & predefined type \texttt{ind} is infinite
\end{tabular}
\item definition principle for constants
\begin{itemize}
\item constants can be introduced as abbreviations
\item constraint: no free vars and no new type vars
\end{itemize}
\item definition principle for types
\begin{itemize}
\item new types can be defined as non-empty subtypes of existing types
\end{itemize}
\item both principles
\begin{itemize}
\item lead to conservative extensions
\item preserve consistency
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{HOL Light derived concepts}
Everything else is derived from this small kernel.
\[
\begin{array}{ccl}
T & =_{\textit{def}} & (\lambda{}p.\ p) = (\lambda{}p.\ p)\\
\wedge & =_{\textit{def}} & \lambda{}p\,q.\ (\lambda f.\ f\ p\ q) = (\lambda{}f.\ f\ T\ T) \\
\Longrightarrow & =_{\textit{def}} & \lambda{}p\,q.\ (p \wedge q \Leftrightarrow p) \\
\forall & =_{\textit{def}} & \lambda{}P.\ (P = \lambda{}x.\ T) \\
\exists & =_{\textit{def}} & \lambda{}P.\ (\forall{}q.\ (\forall{}x.\ P(x) \Longrightarrow q) \Longrightarrow q) \\
\ldots \\
\end{array}
\]
\end{frame}
\begin{frame}
\frametitle{Multiple Kernels}
\begin{itemize}
\item Kernel defines abstract datatypes for types, terms and theorems
\item one does not need to look at the internal implementation
\item therefore, easy to exchange
\item there are at least 3 different kernels for HOL
\begin{itemize}
\item standard kernel (de Bruijn indices)
\item experimental kernel (name / type pairs)
\item OpenTheory kernel (for proof recording)
\end{itemize}
\end{itemize}
\end{frame}
\section{HOL Logic Summary}
\begin{frame}
\frametitle{HOL Logic Summary}
\begin{itemize}
\item HOL theorem prover uses classical higher order logic
\item HOL logic is very similar to SML
\begin{itemize}
\item syntax
\item type system
\item type inference
\end{itemize}
\item HOL theorem prover very trustworthy because of LCF approach
\begin{itemize}
\item there is a small kernel
\item proofs are not stored explicitly
\end{itemize}
\item you don't need to know the details of the kernel
\item usually one works at a much higher level of abstraction
\end{itemize}
\end{frame}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "current"
%%% End:

181
lectures/05_usage.tex Normal file
View File

@ -0,0 +1,181 @@
\part{Basic HOL Usage}
\frame[plain]{\partpage}
\begin{frame}
\frametitle{HOL Technical Usage Issues}
\begin{itemize}
\item practical issues are discussed in practical sessions
\begin{itemize}
\item how to install HOL
\item which key-combinations to use in emacs-mode
\item detailed signature of libraries and theories
\item all parameters and options of certain tools
\item \ldots
\end{itemize}
\item exercise sheets sometimes
\begin{itemize}
\item ask to read some documentation
\item provide examples
\item list references where to get additional information
\end{itemize}
\item if you have problems, ask me outside lecture (\href{mailto:thomas@tuerk-brechen.de}{thomas@tuerk-brechen.de})
\item covered only very briefly in lectures
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Installing HOL}
\begin{itemize}
\item webpage: \url{https://hol-theorem-prover.org}
\item HOL supports two SML implementations
\begin{itemize}
\item Moscow ML (\url{http://mosml.org})
\item \alert{PolyML} (\url{http://www.polyml.org})
\end{itemize}
\item I recommend using PolyML
\item please use emacs with
\begin{itemize}
\item hol-mode
\item sml-mode
\item hol-unicode, if you want to type Unicode
\end{itemize}
\item please install recent revision from git repo or Kananaskis 11 release
\item documentation found on HOL webpage and with sources
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{General Architecture}
\begin{itemize}
\item HOL is a collection of SML modules
\item starting HOL starts a SML Read-Eval-Print-Loop (REPL) with
\begin{itemize}
\item some HOL modules loaded
\item some default modules opened
\item an input wrapper to help parsing terms called \texttt{unquote}
\end{itemize}
\item \texttt{unquote} provides special quotes for terms and types
\begin{itemize}
\item implemented as input filter
\item \hol{``my-term``\ } becomes \ml{Parse.Term [QUOTE "my-term"]}
\item \hol{``:my-type``} becomes \ml{Parse.Type [QUOTE ":my-type"]}
\end{itemize}
\item main interfaces
\begin{itemize}
\item \emph{emacs} (used in the course)
\item vim
\item bare shell
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Filenames}
\begin{itemize}
\item \emph{\texttt{*Script.sml}} --- HOL proof script file
\begin{itemize}
\item script files contain definitions and proof scripts
\item executing them results in HOL searching and checking proofs
\item this might take very long
\item resulting theorems are stored in \texttt{*Theory.\{sml|sig\}} files
\end{itemize}
\item \emph{\texttt{*Theory.\{sml|sig\}}} --- HOL theory\\
\begin{itemize}
\item auto-generated by corresponding script file
\item load quickly, because they don't search/check proofs
\item do not edit theory files
\end{itemize}
\item \emph{\texttt{*Syntax.\{sml|sig\}}} --- syntax libraries \\
\begin{itemize}
\item contain syntax related functions
\item \ie functions to construct and destruct terms and types
\end{itemize}
\item \emph{\texttt{*Lib.\{sml|sig\}}} --- general libraries
\item \emph{\texttt{*Simps.\{sml|sig\}}} --- simplifications
\item \emph{\texttt{selftest.sml}} --- selftest for current directory
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Directory Structure}
\begin{itemize}
\item \emph{\texttt{bin}} --- HOL binaries
\item \emph{\texttt{src}} --- HOL sources
\item \emph{\texttt{examples}} --- HOL examples
\begin{itemize}
\item interesting projects by various people
\item examples owned by their developer
\item coding style and level of maintenance differ a lot
\end{itemize}
\item \emph{\texttt{help}} --- sources for reference manual
\begin{itemize}
\item after compilation home of reference HTML page
\end{itemize}
\item \emph{\texttt{Manual}} --- HOL manuals
\begin{itemize}
\item Tutorial
\item Description
\item Reference (PDF version)
\item Interaction
\item Quick (cheat pages)
\item Style-guide
\item \ldots
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Unicode}
\begin{itemize}
\item HOL supports both Unicode and pure ASCII input and output
\item advantages of Unicode compared to ASCII
\begin{itemize}
\item easier to read (good fonts provided)
\item no need to learn special ASCII syntax
\end{itemize}
\item disadvanges of Unicode compared to ASCII
\begin{itemize}
\item harder to type (even with \texttt{hol-unicode.el})
\item less portable between systems
\end{itemize}
\item whether you like Unicode is highly a matter of personal taste
\item HOL's policy
\begin{itemize}
\item no Unicode in HOL's source directory \texttt{src}
\item Unicode in examples directory \texttt{examples} is fine
\end{itemize}
\item I recommend turning Unicode output off initially
\begin{itemize}
\item this simplifies learning the ASCII syntax
\item no need for special fonts
\item it is easier to copy and paste terms from HOL's output
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Where to find help?}
\begin{itemize}
\item reference manual
\begin{itemize}
\item available as HTML pages, single PDF file and in-system help
\end{itemize}
\item description manual
\item Style-guide (still under development)
\item HOL webpage (\url{https://hol-theorem-prover.org})
\item mailing-list \texttt{hol-info}
\item \ml{DB.match} and \ml{DB.find}
\item \ml{*Theory.sig} and \ml{selftest.sml} files
\item ask someone, \eg me :-) (\href{mailto:thomas@tuerk-brechen.de}{thomas@tuerk-brechen.de})
\end{itemize}
\end{frame}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "current"
%%% End:

419
lectures/06_forward_proofs.tex Normal file
View File

@ -0,0 +1,419 @@
\part{Forward Proofs}
\frame[plain]{\partpage}
\begin{frame}
\frametitle{Kernel too detailed}
\begin{itemize}
\item we already discussed the HOL Logic
\item the kernel itself does not even contain basic logic operators
\item usually one uses a much higher level of abstraction
\begin{itemize}
\item many operations and datatypes are defined
\item high-level derived inference rules are used
\end{itemize}
\item let's now look at this more common abstraction level
\end{itemize}
\end{frame}
\section{Term Syntax}
\begin{frame}
\frametitle{Common Terms and Types}
\begin{tabular}{lcc}
& \emph{Unicode} & \emph{ASCII} \\
type vars & \hol{$\alpha$}, \hol{$\beta$}, \ldots & \hol{'a}, \hol{'b}, \ldots \\
type annotated term & \hol{term:type} & \hol{term:type} \\
true & \hol{T} & \hol{T} \\
false & \hol{F} & \hol{F} \\
negation & \hol{$\neg$b} & \hol{\holNeg{}b} \\
conjunction & \hol{b1\ $\wedge$\ b2} & \hol{b1 \holAnd{} b2} \\
disjunction & \hol{b1\ $\vee$\ b2} & \hol{b1 \holOr{} b2} \\
implication & \hol{b1\ $\Longrightarrow$\ b2} & \hol{b1 \holImp{} b2} \\
equivalence & \hol{b1\ $\Longleftrightarrow$\ b2} & \hol{b1 \holEquiv{} b2} \\
disequation & \hol{v1\ $\neq$\ v2} & \hol{v1 <> v2} \\
all-quantification & \hol{$\forall$x.\ P x} & \hol{!x.\ P x} \\
existential quantification & \hol{$\exists$x.\ P x} & \hol{?x.\ P x} \\
Hilbert's choice operator & \hol{@x.\ P x} & \hol{@x.\ P x}
\end{tabular}
\bigskip
There are similar restrictions to constant and variable names as in SML.\\
HOL specific: don't start variable names with an underscore
\end{frame}
\begin{frame}
\frametitle{Syntax conventions}
\begin{itemize}
\item common function syntax
\begin{itemize}
\item prefix notation, \eg \hol{SUC x}
\item infix notation, \eg \hol{x + y}
\item quantifier notation, \eg \hol{$\forall$x.\ P x} means \hol{($\forall$)\ ($\lambda$x.\ P x)}
\end{itemize}
\item infix and quantifier notation can be turned into prefix notation \\
Example: \hol{(+)\ x\ y} and \hol{\$+\ x\ y} are the same as \hol{x + y}
\item quantifiers of the same type don't need to be repeated \\
Example:\
\hol{$\forall$x\ y.\ P\ x\ y} is short for
\hol{$\forall$x.\ $\forall$y.\ P\ x\ y}
\item there is special syntax for some functions\\
Example:\
\hol{if c then v1 else v2} is nice syntax for
\hol{COND c v1 v2}
\item associative infix operators are usually right-associative\\
Example:\
\hol{b1 \holAnd{} b2 \holAnd{} b3} is parsed as
\hol{b1 \holAnd{} (b2 \holAnd{} b3)}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Creating Terms}
\begin{block}{Term Parser}
Use special quotation provided by \texttt{unquote}.
\end{block}
\begin{alertblock}{Operator Precedence}
It is easy to misjudge the binding strength of certain operators. Therefore use plenty of parenthesis.
\end{alertblock}
\begin{block}{Use Syntax Functions}
Terms are just SML values of type \texttt{term}. You can use syntax functions (usually defined in \texttt{*Syntax.sml} files) to create them.
\end{block}
\end{frame}
\begin{frame}
\frametitle{Creating Terms II}
\begin{tabular}{lll}
\emph{Parser} & \emph{Syntax Funs} & \\
\hol{``:bool``} & \ml{mk\_type ("bool", [])} or \ml{bool} & type of Booleans \\
\hol{``T``} & \ml{mk\_const ("T", bool)} or \ml{T} & term true \\
\hol{``\holNeg{}b``} & \hol{mk\_neg (} & negation of \\
& \hol{\ \ mk\_var ("b", bool))} & \ \ Boolean var b\\
\hol{``\ldots\ \holAnd{} \ldots``} & \hol{mk\_conj (\ldots, \ldots)} & conjunction \\
\hol{``\ldots\ \holOr{} \ldots``} & \hol{mk\_disj (\ldots, \ldots)} & disjunction \\
\hol{``\ldots\ \holImp{} \ldots``} & \hol{mk\_imp (\ldots, \ldots)} & implication \\
\hol{``\ldots\ = \ldots``} & \hol{mk\_eq (\ldots, \ldots)} & equation \\
\hol{``\ldots\ <=> \ldots``} & \hol{mk\_eq (\ldots, \ldots)} & equivalence \\
\hol{``\ldots\ <> \ldots``} & \hol{mk\_neg (mk\_eq (\ldots, \ldots))} & negated equation
\end{tabular}
\end{frame}
\section{Inference Rules}
\begin{frame}
\frametitle{Inference Rules for Equality}
\begin{columns}
\begin{column}{.45\textwidth}
\begin{center}
$\inferrule*[right=REFL] {\ }{\entails t = t}$\\[1em]
$\inferrule*[right=ABS]{\Gamma \entails s = t\\x\ \textit{not free in}\ \Gamma}{\Gamma \entails \lambda{}x.\ s = \lambda{}x. t}$\\[1em]
$\inferrule*[right=MK\_COMB]{\Gamma \entails s = t\\\Delta \entails u = v \\\\ \textit{types fit}}{\Gamma \cup \Delta \entails s(u) = t(v)}$\\[1em]
\end{center}
\end{column}
\begin{column}{.45\textwidth}
\begin{center}
$\inferrule* [right={GSYM}] {\Gamma \entails s = t}{\Gamma \entails t = s}$\\[1em]
$\inferrule*[right=TRANS] {\Gamma \entails s = t\\\Delta \entails t = u}{\Gamma \cup \Delta \entails s = u}$\\[1em]
$\inferrule*[right=EQ\_MP]{\Gamma \entails p \Leftrightarrow q\\\Delta \entails p}{\Gamma \cup \Delta \entails q}$\\[1em]
$\inferrule*[right=BETA\_CONV]{\ }{\entails (\lambda{}x.\ t) v = t[v/x]}$\\[1em]
\end{center}
\end{column}
\end{columns}
\end{frame}
\begin{frame}
\frametitle{Inference Rules for free Variables}
\begin{center}
$\inferrule*[right=INST]{\Gamma[x_1, \ldots, x_n] \entails p[x_1, \ldots, x_n]}
{\Gamma[t_1, \ldots, t_n] \entails p[t_1, \ldots, t_n]}$\\[1em]
$\inferrule*[right=INST\_TYPE]{\Gamma[\alpha_1, \ldots, \alpha_n] \entails p[\alpha_1, \ldots, \alpha_n]}
{\Gamma[\gamma_1, \ldots, \gamma_n] \entails p[\gamma_1, \ldots, \gamma_n]}$\\[1em]
\end{center}
\end{frame}
\begin{frame}
\frametitle{Inference Rules for Implication}
\begin{columns}
\begin{column}{.45\textwidth}
\begin{center}
$\inferrule*[right={MP, MATCH\_MP}]{\Gamma \entails p \Longrightarrow q\\\Delta \entails p}{\Gamma \cup \Delta \entails q}$\\[1em]
$\inferrule*[right=EQ\_IMP\_RULE] {\Gamma \entails p = q}{\Gamma \entails p \Longrightarrow q\\\\\Gamma \entails q \Longrightarrow p}$\\[1em]
$\inferrule*[right=IMP\_ANTISYM\_RULE]{\Gamma \entails p \Longrightarrow q\\\\\Delta \entails q \Longrightarrow p}{\Gamma \cup \Delta \entails p = q}$\\[1em]
$\inferrule*[right=IMP\_TRANS] {\Gamma \entails p \Longrightarrow q\\\Delta \entails q \Longrightarrow r}{\Gamma \cup \Delta \entails p \Longrightarrow r}$\\[1em]
\end{center}
\end{column}
\begin{column}{.45\textwidth}
\begin{center}
$\inferrule*[right=DISCH]{\Gamma \entails p}{\Gamma - \{q\} \entails q \Longrightarrow p}$\\[1em]
$\inferrule*[right=UNDISCH]{\Gamma \entails q \Longrightarrow p}{\Gamma \cup \{q\} \entails p}$\\[1em]
$\inferrule*[right=NOT\_INTRO]{\Gamma \entails p \Longrightarrow \text{F}}{\Gamma \entails \holNeg{}p}$\\[1em]
$\inferrule*[right=NOT\_ELIM]{\Gamma \entails \holNeg{}p}{\Gamma \entails p \Longrightarrow \text{F}}$\\[1em]
\end{center}
\end{column}
\end{columns}
\end{frame}
\begin{frame}
\frametitle{Inference Rules for Conjunction / Disjunction}
\begin{columns}
\begin{column}{.45\textwidth}
\begin{center}
$\inferrule*[right={CONJ}]{\Gamma \entails p\\\Delta \entails q}{\Gamma \cup \Delta \entails p\ \wedge\ q}$\\[1em]
$\inferrule*[right={CONJUNCT1}]{\Gamma \entails p\ \wedge\ q}{\Gamma \entails p}$\\[1em]
$\inferrule*[right={CONJUNCT2}]{\Gamma \entails p\ \wedge\ q}{\Gamma \entails q}$\\[1em]
\end{center}
\end{column}
\begin{column}{.45\textwidth}
\begin{center}
$\inferrule*[right={DISJ1}]{\Gamma \entails p}{\Gamma \entails p\ \vee\ q}$\\[1em]
$\inferrule*[right={DISJ2}]{\Gamma \entails q}{\Gamma \entails p\ \vee\ q}$\\[1em]
$\inferrule*[right={DISJ\_CASES}]{\Gamma \entails p \vee q\\\Delta_1 \cup \{p\} \entails r\\\Delta_2 \cup \{q\} \entails r}{\Gamma \cup \Delta_1 \cup \Delta_2 \entails r}$\\[1em]
\end{center}
\end{column}
\end{columns}
\end{frame}
\begin{frame}
\frametitle{Inference Rules for Quantifiers}
\begin{columns}
\begin{column}{.45\textwidth}
\begin{center}
$\inferrule*[right={GEN}]{\Gamma \entails p\\x \text{\ not free in\ }\Gamma}{\Gamma \entails \forall{}x.\ p}$\\[1em]
$\inferrule*[right={SPEC}]{\Gamma \entails \forall{}x.\ p}{\Gamma \entails p[u/x]}$\\[1em]
\end{center}
\end{column}
\begin{column}{.45\textwidth}
\begin{center}
$\inferrule*[right={EXISTS}]{\Gamma \entails p[u/x]}{\Gamma \entails \exists{}x.\ p}$\\[1em]
$\inferrule*[right={CHOOSE}]{\Gamma \entails \exists{}x.\ p\\\Delta \cup \{p[u/x]\} \entails r\\
u \text{\ not free in\ } \Gamma, \Delta, p \text{ and } r}
{\Gamma \cup \Delta \entails r}$\\[1em]
\end{center}
\end{column}
\end{columns}
\end{frame}
\section{Forward Proofs}
\begin{frame}
\frametitle{Forward Proofs}
\begin{itemize}
\item axioms and inference rules are used to derive theorems
\item this method is called \emph{forward proof}
\begin{itemize}
\item one starts with basic building blocks
\item one moves step by step forward
\item finally the theorem one is interested in is derived
\end{itemize}
\item one can also implement own proof tools
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Forward Proofs --- Example I}
Let's prove $\forall{}p.\ p \Longrightarrow p$.
\bigskip
\begin{columns}
\begin{column}{.45\textwidth}
\begin{semiverbatim}
val IMP_REFL_THM = let
val tm1 = ``p:bool``;
val thm1 = ASSUME tm1;
val thm2 = DISCH tm1 thm1;
in
GEN tm1 thm2
end
fun IMP_REFL t =
SPEC t IMP_REFL_THM;
\end{semiverbatim}
\end{column}
\begin{column}{.45\textwidth}
\begin{semiverbatim}
> val tm1 = ``p``: term
> val thm1 = [p] |- p: thm
> val thm2 = |- p ==> p: thm
> val IMP_REFL_THM =
|- !p. p ==> p: thm
> val IMP_REFL =
fn: term -> thm
\end{semiverbatim}
\end{column}
\end{columns}
\end{frame}
\begin{frame}[fragile]
\frametitle{Forward Proofs --- Example II}
Let's prove $\forall{}P\,v.\ (\exists{}x.\ (x = v) \wedge P\ x) \Longleftrightarrow P\ v$.
\bigskip
\begin{columns}
\scriptsize
\begin{column}{.45\textwidth}
\begin{semiverbatim}
val tm_v = ``v:'a``;
val tm_P = ``P:'a -> bool``;
val tm_lhs = ``?x. (x = v) \holAnd{} P x``
val tm_rhs = mk_comb (tm_P, tm_v);
val thm1 = let
val thm1a = ASSUME tm_rhs;
val thm1b =
CONJ (REFL tm_v) thm1a;
val thm1c =
EXISTS (tm_lhs, tm_v) thm1b
in
DISCH tm_rhs thm1c
end
\end{semiverbatim}
\end{column}
\begin{column}{.45\textwidth}
\begin{semiverbatim}
> val thm1a = [P v] |- P v: thm
> val thm1b =
[P v] |- (v = v) \holAnd{} P v: thm
> val thm1c =
[P v] |- ?x. (x = v) \holAnd{} P x
> val thm1 = [] |-
P v ==> ?x. (x = v) \holAnd{} P x: thm
\end{semiverbatim}
\end{column}
\end{columns}
\end{frame}
\begin{frame}[fragile]
\frametitle{Forward Proofs --- Example II cont.}
\begin{columns}
\scriptsize
\begin{column}{.45\textwidth}
\begin{semiverbatim}
val thm2 = let
val thm2a =
ASSUME ``(u:'a = v) \holAnd{} P u``
val thm2b = AP_TERM tm_P
(CONJUNCT1 thm2a);
val thm2c = EQ_MP thm2b
(CONJUNCT2 thm2a);
val thm2d =
CHOOSE (``u:'a``,
ASSUME tm_lhs) thm2c
in
DISCH tm_lhs thm2d
end
val thm3 = IMP_ANTISYM_RULE thm2 thm1
val thm4 = GENL [tm_P, tm_v] thm3
\end{semiverbatim}
\end{column}
\begin{column}{.45\textwidth}
\begin{semiverbatim}
> val thm2a = [(u = v) \holAnd{} P u] |-
(u = v) \holAnd{} P u: thm
> val thm2b = [(u = v) \holAnd{} P u] |-
P u <=> P v
> val thm2c = [(u = v) \holAnd{} P u] |-
P v
> val thm2d = [?x. (x = v) \holAnd{} P x] |-
P v
> val thm2 = [] |-
?x. (x = v) \holAnd{} P x ==> P v
> val thm3 = [] |-
?x. (x = v) \holAnd{} P x <=> P v
> val thm4 = [] |- !P v.
?x. (x = v) \holAnd{} P x <=> P v
\end{semiverbatim}
\end{column}
\end{columns}
\end{frame}
% \section{Rules and Conversions}
% \begin{frame}
% \frametitle{Derived Tools}
% \begin{itemize}
% \item HOL lives from implementing reasoning tools in SML
% \item \emph{rules} --- use theorems to produce new theorems\\
% \begin{itemize}
% \item SML-type \ml{thm -> thm}
% \item functions with similar type often called rule as well
% \end{itemize}
% \item \emph{conversions} --- convert a term into an equal one\\
% \begin{itemize}
% \item SML-type \ml{term -> thm}
% \item given term \ml{t} produces theorem of form \ml{[] |- t = t'}
% \item may raise exceptions \ml{HOL\_ERR} or \ml{UNCHANGED}
% \end{itemize}
% \item \ldots
% \end{itemize}
% \end{frame}
% \begin{frame}
% \frametitle{Conversions}
% \begin{itemize}
% \item HOL has very good tool support for equality reasoning
% \item \emph{conversions} are important for HOL's automation
% \item there is a lot of infrastructure for conversions
% \begin{itemize}
% \item \ml{RAND\_CONV}, \ml{RATOR\_CONV}, \ml{ABS\_CONV}
% \item \ml{DEPTH\_CONV}
% \item \ml{THENC}, \ml{TRY\_CONV}, \ml{FIRST\_CONV}
% \item \ml{REPEAT\_CONV}
% \item \ml{CHANGED\_CONV}, \ml{QCHANGED\_CONV}
% \item \ml{NO\_CONV}, \ml{ALL\_CONV}
% \item \ldots
% \end{itemize}
% \item important conversions
% \begin{itemize}
% \item \ml{REWR\_CONV}
% \item \ml{REWRITE\_CONV}
% \item \ldots
% \end{itemize}
% \end{itemize}
% \end{frame}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "current"
%%% End:

564
lectures/07_backward_proofs.tex Normal file
View File

@ -0,0 +1,564 @@
\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:

675
lectures/08_basic_tactics.tex Normal file
View File

@ -0,0 +1,675 @@
\part{Basic Tactics}
\frame[plain]{\partpage}
\begin{frame}
\frametitle{Syntax of Tactics in HOL}
\begin{itemize}
\item originally tactics were written all in capital letters with underscores\\
Example: \hol{ALL\_TAC}
\item since 2010 more and more tactics have overloaded lower-case syntax\\
Example: \hol{all\_tac}
\item sometimes, the lower-case version is shortened\\
Example: \hol{REPEAT}, \hol{rpt}
\item sometimes, there is special syntax\\
Example: \hol{THEN}, \hol{\textbsl{}\textbsl{}}, \hol{>>}
\item which one to use is mostly a matter of personal taste
\begin{itemize}
\item all-capital names are hard to read and type
\item however, not for all tactics there are lower-case versions
\item mixed lower- and upper-case tactics are even harder to read
\item often shortened lower-case name is not \textit{speaking}
\end{itemize}
\end{itemize}
\bottomstatement{In the lecture we will use mostly the old-style names.}
\end{frame}
\section{Basic Tactics}
\begin{frame}
\frametitle{Some Basic Tactics}
\begin{tabular}{ll}
\hol{GEN\_TAC} & remove outermost all-quantifier \\
\hol{DISCH\_TAC} & move antecedent of goal into assumptions \\
\hol{CONJ\_TAC} & splits conjunctive goal \\
\hol{STRIP\_TAC} & splits on outermost connective (combination\\
& \quad of \hol{GEN\_TAC}, \hol{CONJ\_TAC}, \hol{DISCH\_TAC}, \ldots) \\
\hol{DISJ1\_TAC} & selects left disjunct \\
\hol{DISJ2\_TAC} & selects right disjunct \\
\hol{EQ\_TAC} & reduce Boolean equality to implications \\
\hol{ASSUME\_TAC}\ thm & add theorem to list of assumptions \\
\hol{EXISTS\_TAC} term & provide witness for existential goal \\
\end{tabular}
\end{frame}
\begin{frame}
\frametitle{Tacticals}
\begin{itemize}
\item tacticals are SML functions that combine tactics to form new tactics
\item common workflow
\begin{itemize}
\item develop large tactic interactively
\item using \hol{goalStack} and editor support to execute tactics one by one
\item combine tactics manually with tacticals to create larger tactics
\item finally end up with one large tactic that solves your goal
\item use \hol{prove} or \hol{store\_thm} instead of \hol{goalStack}
\end{itemize}
\item make sure to \alert{clearly mark proof structure} by \eg
\begin{itemize}
\item use indentation
\item use parentheses
\item use appropriate connectives
\item \ldots
\end{itemize}
\item goalStack commands like \hol{e} or \hol{g} should not appear in your final proof
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Some Basic Tacticals}
\begin{tabular}{lll}
tac1 \hol{>>} tac2 & \hol{THEN}, \hol{\textbsl{}\textbsl{}} & applies tactics in sequence \\
tac \hol{>|} tacL & \hol{THENL} & applies list of tactics to subgoals \\
tac1 \hol{>-} tac2 & \hol{THEN1} & applies tac2 to the first subgoal of tac1 \\
\hol{REPEAT} tac & \hol{rpt} & repeats tac until it fails \\
\hol{NTAC} n tac & & apply tac n times \\
\hol{REVERSE} tac & \hol{reverse} & reverses the order of subgoals \\
tac1 \hol{ORELSE} tac2 & & applies tac1 only if tac2 fails \\
\hol{TRY} tac & & do nothing if tac fails \\
\hol{ALL\_TAC} & \hol{all\_tac} & do nothing \\
\hol{NO\_TAC} & & fail
\end{tabular}
\end{frame}
\begin{frame}
\frametitle{Basic Rewrite Tactics}
\begin{itemize}
\item (equational) rewriting is at the core of HOL's automation
\item we will discuss it in detail later
\item details complex, but basic usage is straightforward
\begin{itemize}
\item given a theorem \hol{rewr\_thm} of form \hol{|- P\ x = Q\ x} and a term \hol{t}
\item rewriting \hol{t} with \hol{rewr\_thm} means
\item replacing each occurrence of a term \hol{P c} for some \hol{c} with \hol{Q c} in \hol{t}
\end{itemize}
\item \alert{warning:} rewriting may loop\\Example: rewriting with theorem \hol{|- X <=> (X \holAnd{} T)}
\end{itemize}
\begin{tabular}{ll}
\hol{REWRITE\_TAC} thms & rewrite goal using equations found\\
& in given list of theorems \\
\hol{ASM\_REWRITE\_TAC} thms & in addition use assumptions \\
\hol{ONCE\_REWRITE\_TAC} thms & rewrite once in goal using equations\\
\hol{ONCE\_ASM\_REWRITE\_TAC} thms & rewrite once using assumptions
\end{tabular}
\end{frame}
\begin{frame}
\frametitle{Case-Split and Induction Tactics}
\begin{tabular}{ll}
\hol{Induct\_on} `term` & induct on \texttt{term} \\
\hol{Induct} & induct on all-quantifier \\
\hol{Cases\_on} `term` & case-split on \texttt{term} \\
\hol{Cases} & case-split on all-quantifier \\
\hol{MATCH\_MP\_TAC} thm & apply rule \\
\hol{IRULE\_TAC} thm & generalised apply rule
\end{tabular}
\end{frame}
\begin{frame}
\frametitle{Assumption Tactics}
\begin{tabular}{ll}
\hol{POP\_ASSUM} thm-tac & use and remove first assumption \\
& \-\quad common usage \hol{POP\_ASSUM MP\_TAC} \\[1em]
\hol{PAT\_ASSUM} term thm-tac& use (and remove) first \\
\-\quad also \hol{PAT\_X\_ASSUM} term thm-tac& \quad assumption matching pattern \\[1em]
\hol{WEAKEN\_TAC} term-pred & removes first assumption \\
& \quad{}satisfying predicate
\end{tabular}
\end{frame}
\begin{frame}
\frametitle{Decision Procedure Tactics}
\begin{itemize}
\item decision procedures try to solve the current goal completely
\item they either succeed or fail
\item no partial progress
\item decision procedures vital for automation
\end{itemize}
\bigskip
\begin{tabular}{ll}
\hol{TAUT\_TAC} & propositional logic tautology checker \\
\hol{DECIDE\_TAC} & linear arithmetic for \texttt{num} \\
\hol{METIS\_TAC} thms & first order prover \\
\hol{numLib.ARITH\_TAC} & Presburger arithmetic \\
\hol{intLib.ARITH\_TAC} & uses Omega test
\end{tabular}
\end{frame}
\begin{frame}
\frametitle{Subgoal Tactics}
\begin{itemize}
\item it is vital to structure your proofs well
\begin{itemize}
\item improved maintainability
\item improved readability
\item improved reusability
\item saves time in medium-run
\end{itemize}
\item therefore, use many small lemmata
\item also, use many explicit subgoals
\end{itemize}
\bigskip
\begin{tabular}{ll}
`term-frag` \hol{by} tac & show term with tac and\\
& add it to assumptions \\
`term-frag` \hol{suffices\_by} tac & show it suffices to prove term
\end{tabular}
\end{frame}
\begin{frame}
\frametitle{Term Fragments / Term Quotations}
\begin{itemize}
\item notice that \hol{by} and \hol{suffices\_by} take \emph{term fragments}
\item term fragments are also called \emph{term quotations}
\item they represent (partially) unparsed terms
\item parsing takes place during execution of tactic in context of goal
\item this helps to avoid type annotations
\item however, this means syntax errors show late as well
\item the library \emph{Q} defines many tactics using term fragments
\end{itemize}
\end{frame}
\section{Examples}
\begin{frame}
\frametitle{Importance of Exercises}
\begin{itemize}
\item here many tactics are presented in a very short amount of time
\item there are many, many more important tactics out there
\item few people can learn a programming language just by reading manuals
\item similar few people can learn HOL just by reading and listening
\item you should write your own proofs and play around with these tactics
\item solving the exercises is highly recommended\\(and actually required if you want credits for this course)
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Tactical Proof - Example I - Slide 1}
\begin{itemize}
\item we want to prove \hol{!l.\ LENGTH (APPEND l l) = 2 * LENGTH l}
\item first step: set up goal on \hol{goalStack}
\item at same time start writing proof script
\end{itemize}
\begin{block}{Proof Script}
\begin{semiverbatim}\small
val LENGTH_APPEND_SAME = prove (
``!l. LENGTH (APPEND l l) = 2 * LENGTH l``,
\end{semiverbatim}
\end{block}
\begin{block}{Actions}
\begin{itemize}
\item run \texttt{g ``!l.\ LENGTH (APPEND l l) = 2 * LENGTH l``}
\item this is done by hol-mode
\item move cursor inside term and press \texttt{M-h g}\\
(menu-entry \texttt{HOL - Goalstack - New goal})
\end{itemize}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Tactical Proof - Example I - Slide 2}
\begin{block}{Current Goal}
\begin{semiverbatim}\small
!l. LENGTH (l ++ l) = 2 * LENGTH l
\end{semiverbatim}
\end{block}
\begin{itemize}
\item the outermost connective is an all-quantifier
\item let's get rid of it via \hol{GEN\_TAC}
\end{itemize}
\begin{block}{Proof Script}
\begin{semiverbatim}\small
val LENGTH_APPEND_SAME = prove (
``!l. LENGTH (l ++ l) = 2 * LENGTH l``,
GEN_TAC
\end{semiverbatim}
\end{block}
\begin{block}{Actions}
\begin{itemize}
\item run \texttt{e GEN\_TAC}
\item this is done by hol-mode
\item mark line with \texttt{GEN\_TAC} and press \texttt{M-h e}\\
(menu-entry \texttt{HOL - Goalstack - Apply tactic})
\end{itemize}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Tactical Proof - Example I - Slide 3}
\begin{block}{Current Goal}
\begin{semiverbatim}\small
LENGTH (l ++ l) = 2 * LENGTH l
\end{semiverbatim}
\end{block}
\begin{itemize}
\item \hol{LENGTH} of \hol{APPEND} can be simplified
\item let's search an appropriate lemma with \ml{DB.match}
\end{itemize}
\begin{block}{Actions}
\begin{itemize}
\item run \ml{DB.print\_match [] ``LENGTH (\_ ++ \_)``}
\item this is done via hol-mode
\item press \texttt{M-h m} and enter term pattern\\
(menu-entry \texttt{HOL - Misc - DB match})
\item this finds the theorem \ml{listTheory.LENGTH\_APPEND}\\
\hol{|- !l1 l2. LENGTH (l1 ++ l2) = LENGTH l1 + LENGTH l2}
\end{itemize}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Tactical Proof - Example I - Slide 4}
\begin{block}{Current Goal}
\begin{semiverbatim}\small
LENGTH (l ++ l) = 2 * LENGTH l
\end{semiverbatim}
\end{block}
\begin{itemize}
\item let's rewrite with found theorem \ml{listTheory.LENGTH\_APPEND}
\end{itemize}
\begin{block}{Proof Script}
\begin{semiverbatim}\small
val LENGTH_APPEND_SAME = prove (
``!l. LENGTH (APPEND l l) = 2 * LENGTH l``,
GEN_TAC >>
REWRITE_TAC[listTheory.LENGTH\_APPEND]
\end{semiverbatim}
\end{block}
\begin{block}{Actions}
\begin{itemize}
\item connect the new tactic with tactical \hol{>>} (\hol{THEN})
\item use hol-mode to expand the new tactic
\end{itemize}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Tactical Proof - Example I - Slide 5}
\begin{block}{Current Goal}
\begin{semiverbatim}\small
LENGTH l + LENGTH l = 2 * LENGTH l
\end{semiverbatim}
\end{block}
\begin{itemize}
\item let's search a theorem for simplifying \hol{2 * LENGTH l}
\item prepare for extending the previous rewrite tactic
\end{itemize}
\begin{block}{Proof Script}
\begin{semiverbatim}\small
val LENGTH_APPEND_SAME = prove (
``!l. LENGTH (APPEND l l) = 2 * LENGTH l``,
GEN_TAC >>
REWRITE_TAC[listTheory.LENGTH\_APPEND]
\end{semiverbatim}
\end{block}
\begin{block}{Actions}
\begin{itemize}
\item \hol{DB.match} finds theorem \hol{arithmeticTheory.TIMES2}
\item press \texttt{M-h b} and undo last tactic expansion\\
(menu-entry \texttt{HOL - Goalstack - Back up})
\end{itemize}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Tactical Proof - Example I - Slide 6}
\begin{block}{Current Goal}
\begin{semiverbatim}\small
LENGTH (l ++ l) = 2 * LENGTH l
\end{semiverbatim}
\end{block}
\begin{itemize}
\item extend the previous rewrite tactic
\item finish proof
\end{itemize}
\begin{block}{Proof Script}
\begin{semiverbatim}\small
val LENGTH_APPEND_SAME = prove (
``!l. LENGTH (APPEND l l) = 2 * LENGTH l``,
GEN_TAC >>
REWRITE_TAC[listTheory.LENGTH\_APPEND, arithmeticTheory.TIMES2]);
\end{semiverbatim}
\end{block}
\begin{block}{Actions}
\begin{itemize}
\item add \hol{TIMES2} to the list of theorems used by rewrite tactic
\item use hol-mode to expand the extended rewrite tactic
\item goal is solved, so let's add closing parenthesis and semicolon
\end{itemize}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Tactical Proof - Example I - Slide 7}
\begin{itemize}
\item we have a finished tactic proving our goal
\item notice that \hol{GEN\_TAC} is not needed
\item let's polish the proof script
\end{itemize}
\begin{block}{Proof Script}
\begin{semiverbatim}\small
val LENGTH_APPEND_SAME = prove (
``!l. LENGTH (APPEND l l) = 2 * LENGTH l``,
GEN_TAC >>
REWRITE_TAC[listTheory.LENGTH\_APPEND, arithmeticTheory.TIMES2]);
\end{semiverbatim}
\end{block}
\begin{block}{Polished Proof Script}
\begin{semiverbatim}\small
val LENGTH_APPEND_SAME = prove (
``!l. LENGTH (APPEND l l) = 2 * LENGTH l``,
REWRITE_TAC[listTheory.LENGTH\_APPEND, arithmeticTheory.TIMES2]);
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Tactical Proof - Example II - Slide 1}
\begin{itemize}
\item let's prove something slightly more complicated
\item drop old goal by pressing \texttt{M-h d}\\
(menu-entry \texttt{HOL - Goalstack - Drop goal})
\item set up goal on \hol{goalStack} (\texttt{M-h g})
\item at same time start writing proof script
\end{itemize}
\begin{block}{Proof Script}
\begin{semiverbatim}\small
val NOT_ALL_DISTINCT_LEMMA = prove (``!x1 x2 x3 l1 l2 l3.
(MEM x1 l1 \holAnd{} MEM x2 l2 \holAnd{} MEM x3 l3) \holAnd{}
((x1 <= x2) \holAnd{} (x2 <= x3) \holAnd{} x3 <= SUC x1) ==>
~(ALL_DISTINCT (l1 ++ l2 ++ l3))``,
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Tactical Proof - Example II - Slide 2}
\begin{block}{Current Goal}
\begin{semiverbatim}\small
!x1 x2 x3 l1 l2 l3.
(MEM x1 l1 \holAnd{} MEM x2 l2 \holAnd{} MEM x3 l3) \holAnd{}
x1 <= x2 \holAnd{} x2 <= x3 \holAnd{} x3 <= SUC x1 ==>
~ALL_DISTINCT (l1 ++ l2 ++ l3)
\end{semiverbatim}
\end{block}
\begin{itemize}
\item let's strip the goal
\end{itemize}
\begin{block}{Proof Script}
\begin{semiverbatim}\small
val NOT_ALL_DISTINCT_LEMMA = prove (``!x1 x2 x3 l1 l2 l3.
(MEM x1 l1 \holAnd{} MEM x2 l2 \holAnd{} MEM x3 l3) \holAnd{}
((x1 <= x2) \holAnd{} (x2 <= x3) \holAnd{} x3 <= SUC x1) ==>
~(ALL_DISTINCT (l1 ++ l2 ++ l3))``,
REPEAT STRIP\_TAC
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Tactical Proof - Example II - Slide 2}
\begin{block}{Current Goal}
\begin{semiverbatim}\small
!x1 x2 x3 l1 l2 l3.
(MEM x1 l1 \holAnd{} MEM x2 l2 \holAnd{} MEM x3 l3) \holAnd{}
x1 <= x2 \holAnd{} x2 <= x3 \holAnd{} x3 <= SUC x1 ==>
~ALL_DISTINCT (l1 ++ l2 ++ l3)
\end{semiverbatim}
\end{block}
\begin{itemize}
\item let's strip the goal
\end{itemize}
\begin{block}{Proof Script}
\begin{semiverbatim}\small
val LENGTH_APPEND_SAME = prove (
``!l. LENGTH (APPEND l l) = 2 * LENGTH l``,
REPEAT STRIP\_TAC
\end{semiverbatim}
\end{block}
\begin{block}{Actions}
\begin{itemize}
\item add \hol{REPEAT STRIP\_TAC} to proof script
\item expand this tactic using hol-mode
\end{itemize}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Tactical Proof - Example II - Slide 3}
\begin{block}{Current Goal}
\begin{semiverbatim}\small
F
------------------------------------
0. MEM x1 l1 4. x2 <= x3
1. MEM x2 l2 5. x3 <= SUC x1
2. MEM x3 l3 6. ALL_DISTINCT (l1 ++ l2 ++ l3)
3. x1 <= x2
\end{semiverbatim}
\end{block}
\begin{itemize}
\item oops, we did too much, we would like to keep \texttt{ALL\_DISTINCT} in goal
\end{itemize}
\begin{block}{Proof Script}
\begin{semiverbatim}\small
val NOT_ALL_DISTINCT_LEMMA = prove (``...``,
REPEAT GEN\_TAC >> STRIP\_TAC
\end{semiverbatim}
\end{block}
\begin{block}{Actions}
\begin{itemize}
\item undo \hol{REPEAT STRIP\_TAC} (\texttt{M-h b})
\item expand more fine-tuned strip tactic
\end{itemize}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Tactical Proof - Example II - Slide 4}
\begin{block}{Current Goal}
\begin{semiverbatim}\small
~ALL_DISTINCT (l1 ++ l2 ++ l3)
------------------------------------
0. MEM x1 l1 3. x1 <= x2
1. MEM x2 l2 4. x2 <= x3
2. MEM x3 l3 5. x3 <= SUC x1
\end{semiverbatim}
\end{block}
\begin{itemize}
\item now let's simplify \hol{ALL\_DISTINCT}
\item search suitable theorems with \hol{DB.match}
\item use them with rewrite tactic
\end{itemize}
\begin{block}{Proof Script}
\begin{semiverbatim}\small
val NOT_ALL_DISTINCT_LEMMA = prove (``...``,
REPEAT GEN\_TAC >> STRIP\_TAC >>
REWRITE\_TAC[listTheory.ALL_DISTINCT\_APPEND, listTheory.MEM\_APPEND]
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Tactical Proof - Example II - Slide 5}
\begin{block}{Current Goal}
\begin{semiverbatim}\scriptsize
~((ALL_DISTINCT l1 \holAnd{} ALL_DISTINCT l2 \holAnd{} !e. MEM e l1 ==> ~MEM e l2) \holAnd{}
ALL_DISTINCT l3 \holAnd{} !e. MEM e l1 \holOr{} MEM e l2 ==> ~MEM e l3)
------------------------------------
0. MEM x1 l1 3. x1 <= x2
1. MEM x2 l2 4. x2 <= x3
2. MEM x3 l3 5. x3 <= SUC x1
\end{semiverbatim}
\end{block}
\begin{itemize}
\item from assumptions 3, 4 and 5 we know \hol{x2 = x1 \holOr{} x2 = x3}
\item let's deduce this fact by \hol{DECIDE\_TAC}
\end{itemize}
\begin{block}{Proof Script}
\begin{semiverbatim}\scriptsize
val NOT_ALL_DISTINCT_LEMMA = prove (``...``,
REPEAT GEN\_TAC >> STRIP\_TAC >>
REWRITE\_TAC[listTheory.ALL_DISTINCT\_APPEND, listTheory.MEM\_APPEND] >>
`(x2 = x1) \holOr{} (x2 = x3)` by DECIDE_TAC
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Tactical Proof - Example II - Slide 6}
\begin{block}{Current Goals --- 2 subgoals, one for each disjunct}
\begin{semiverbatim}\scriptsize
~((ALL_DISTINCT l1 \holAnd{} ALL_DISTINCT l2 \holAnd{} !e. MEM e l1 ==> ~MEM e l2) \holAnd{}
ALL_DISTINCT l3 \holAnd{} !e. MEM e l1 \holOr{} MEM e l2 ==> ~MEM e l3)
------------------------------------
0. MEM x1 l1 4. x2 <= x3
1. MEM x2 l2 5. x3 <= SUC x1
2. MEM x3 l3 6a. x2 = x1
3. x1 <= x2 6b. x2 = x3
\end{semiverbatim}
\end{block}
\begin{itemize}
\item both goals are easily solved by first-order reasoning
\item let's use \hol{METIS\_TAC[]} for both subgoals
\end{itemize}
\begin{block}{Proof Script}
\begin{semiverbatim}\scriptsize
val NOT_ALL_DISTINCT_LEMMA = prove (``...``,
REPEAT GEN\_TAC >> STRIP\_TAC >>
REWRITE\_TAC[listTheory.ALL_DISTINCT\_APPEND, listTheory.MEM\_APPEND] >>
`(x2 = x1) \holOr{} (x2 = x3)` by DECIDE_TAC >> (
METIS\_TAC[]
));
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Tactical Proof - Example II - Slide 7}
\begin{block}{Finished Proof Script}
\begin{semiverbatim}\scriptsize
val NOT_ALL_DISTINCT_LEMMA = prove (
``!x1 x2 x3 l1 l2 l3.
(MEM x1 l1 \holAnd{} MEM x2 l2 \holAnd{} MEM x3 l3) \holAnd{}
((x1 <= x2) \holAnd{} (x2 <= x3) \holAnd{} x3 <= SUC x1) ==>
~(ALL_DISTINCT (l1 ++ l2 ++ l3))``,
REPEAT GEN\_TAC >> STRIP\_TAC >>
REWRITE\_TAC[listTheory.ALL_DISTINCT\_APPEND, listTheory.MEM\_APPEND] >>
`(x2 = x1) \holOr{} (x2 = x3)` by DECIDE_TAC >> (
METIS\_TAC[]
));
\end{semiverbatim}
\end{block}
\begin{itemize}
\item notice that proof structure is explicit
\item parentheses and indentation used to mark new subgoals
\end{itemize}
\end{frame}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "current"
%%% End:

174
lectures/09_induction.tex Normal file
View File

@ -0,0 +1,174 @@
\part{Induction Proofs}
\frame[plain]{\partpage}
\begin{frame}
\frametitle{Mathematical Induction}
\begin{itemize}
\item mathematical (\aka natural) induction principle:\\
If a property $P$ holds for 0 and $P(n)$ implies $P(n+1)$ for all n,\\
then $P(n)$ holds for all $n$.
\item HOL is expressive enough to encode this principle as a theorem.\\\medskip
\hol{|- !P. P 0 \holAnd{} (!n.\ P n ==> P (SUC n)) ==> !n.\ P n}\medskip
\item Performing mathematical induction in HOL means applying this theorem (\eg via \hol{HO\_MATCH\_MP\_TAC})
\item there are many similarish induction theorems in HOL
\item Example: complete induction principle\\\medskip
\hol{|- !P. (!n.\ (!m.\ m < n ==> P m) ==> P n) ==> !n.\ P n}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Structural Induction Theorems}
\begin{itemize}
\item \emph{structural induction} theorems are an important special form of induction theorems
\item they describe performing induction on the structure of a datatype
\item Example: \hol{\scriptsize|- !P.\ P [] \holAnd{} (!t.\ P t ==> !h.\ P (h::t)) ==> !l.\ P l}
\item structural induction is used very frequently in HOL
\item for each algabraic datatype, there is an induction theorem
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Other Induction Theorems}
\begin{itemize}
\item there are many induction theorems in HOL
\begin{itemize}
\item datatype definitions lead to induction theorems
\item recursive function definitions produce corresponding induction theorems
\item recursive relation definitions give rise to induction theorems
\item many are manually defined
\end{itemize}
\item Examples\\\bigskip{\scriptsize
\hol{|- !P.\ P [] \holAnd{} (!l.\ P l ==> !x.\ P (SNOC x l)) ==> !l.\ P l}\\\bigskip
\hol{|- !P.\ P FEMPTY \holAnd{} \\
\-\qquad\quad(!f.\ P f ==> !x y.\ x NOTIN FDOM f ==> P (f |+ (x,y))) ==> !f.\ P f}\\\bigskip
\hol{|- !P.\ P \{\} \holAnd{} \\
\-\qquad\quad(!s.\ FINITE s \holAnd{} P s ==> !e.\ e NOTIN s ==> P (e INSERT s)) ==> \\
\-\qquad\quad!s.\ FINITE s ==> P s}\\\bigskip
\hol{|- !R P.\ (!x y.\ R x y ==> P x y) \holAnd{} (!x y z.\ P x y \holAnd{} P y z ==> P x z) ==>\\
\-\qquad\quad!u v.\ R$^+$ u v ==> P u v}}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Induction (and Case-Split) Tactics}
\begin{itemize}
\item the tactic \hol{Induct} (or \hol{Induct\_on}) is usually used to start induction proofs
\item it looks at the type of the quantifier (or its argument) and applies the default induction theorem for this type
\item this is usually what one needs
\item other (non default) induction theorems can be applied via \hol{INDUCT\_THEN} or \hol{HO\_MATCH\_MP\_TAC}
\item similarish \hol{Cases\_on} picks and applies default case-split theorems
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Induction Proof - Example I - Slide 1}
\begin{itemize}
\item let's prove via induction\\
\hol{!l1 l2.\ REVERSE (l1 ++ l2) = REVERSE l2 ++ REVERSE l1}
\item we set up the goal and start an induction proof on \hol{l1}
\end{itemize}
\begin{block}{Proof Script}
\begin{semiverbatim}\small
val REVERSE_APPEND = prove (
``!l1 l2.\ REVERSE (l1 ++ l2) = REVERSE l2 ++ REVERSE l1``,
Induct
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Induction Proof - Example I - Slide 2}
\begin{itemize}
\item the induction tactic produced two cases
\item base case:\\
{\scriptsize\hol{!l2.\ REVERSE ([] ++ l2) = REVERSE l2 ++ REVERSE []}}
\item induction step:\\
{\scriptsize
\begin{semiverbatim}
\hol{!h l2.\ REVERSE (h::l1 ++ l2) = REVERSE l2 ++ REVERSE (h::l1)}
-----------------------------------------------------------
\hol{!l2.\ REVERSE (l1 ++ l2) = REVERSE l2 ++ REVERSE l1}
\end{semiverbatim}}
\item both goals can be easily proved by rewriting
\end{itemize}
\begin{block}{Proof Script}
\begin{semiverbatim}\scriptsize
val REVERSE_APPEND = prove (``
!l1 l2.\ REVERSE (l1 ++ l2) = REVERSE l2 ++ REVERSE l1``,
Induct >| [
REWRITE_TAC[REVERSE_DEF, APPEND, APPEND_NIL],
ASM_REWRITE_TAC[REVERSE_DEF, APPEND, APPEND_ASSOC]
]);
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Induction Proof - Example II - Slide 2}
\begin{itemize}
\item let's prove via induction\\
\hol{!l.\ REVERSE (REVERSE l) = l}
\item we set up the goal and start an induction proof on \hol{l}
\end{itemize}
\begin{block}{Proof Script}
\begin{semiverbatim}\small
val REVERSE_REVERSE = prove (
``!l.\ REVERSE (REVERSE l) = l``,
Induct
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Induction Proof - Example II - Slide 2}
\begin{itemize}
\item the induction tactic produced two cases
\item base case:\\
{\scriptsize\hol{REVERSE (REVERSE []) = []}}
\item induction step:\\
{\scriptsize
\begin{semiverbatim}
\hol{!h.\ REVERSE (REVERSE (h::l1)) = h::l1}
--------------------------------------------
\hol{REVERSE (REVERSE l) = l}
\end{semiverbatim}}
\item again both goals can be easily proved by rewriting
\end{itemize}
\begin{block}{Proof Script}
\begin{semiverbatim}\scriptsize
val REVERSE_REVERSE = prove (
``!l.\ REVERSE (REVERSE l) = l``,
Induct >| [
REWRITE_TAC[REVERSE_DEF],
ASM_REWRITE_TAC[REVERSE_DEF, REVERSE_APPEND, APPEND]
]);
\end{semiverbatim}
\end{block}
\end{frame}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "current"
%%% End:

987
lectures/10_definitions.tex Normal file
View File

@ -0,0 +1,987 @@
\part{Basic Definitions}
\frame[plain]{\partpage}
\section{Definitions, Axioms and Oracles}
\begin{frame}
\frametitle{Definitional Extensions}
\begin{itemize}
\item there are \emph{conservative definition principles} for types and constants
\item conservative means that all theorems that can be proved in extended theory can also be proved in original one
\item however, such extensions make the theory more comfortable
\item definitions introduce \alert{no new inconsistencies}
\item the HOL community has a very strong tradition of a purely definitional approach
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Axiomatic Extensions}
\begin{itemize}
\item \alert{axioms} are a different approach
\item they allow postulating arbitrary properties, \ie extending the logic with arbitrary theorems
\item this approach might introduce new inconsistencies
\item in HOL axioms are very rarely needed
\item using definitions is often considered more elegant
\item it is hard to keep track of axioms
\item use axioms only if you really know what you are doing
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Oracles}
\begin{itemize}
\item \alert{oracles} are families of axioms
\item however, they are used differently than axioms
\item they are used to enable usage of external tools and knowledge
\item you might want to use an external automated prover
\item this external tool acts as an oracle
\begin{itemize}
\item it provides answers
\item it does not explain or justify these answers
\end{itemize}
\item you don't know, whether this external tool might be buggy
\item all theorems proved via it are tagged with a special oracle-tag
\item tags are propagated
\item this allows keeping track of everything depending on the correctness of this tool
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Oracles II}
\begin{itemize}
\item Common oracle-tags
\begin{itemize}
\item \ml{DISK\_THM} --- theorem was written to disk and read again
\item \ml{HolSatLib} --- proved by MiniSat
\item \ml{HolSmtLib} --- proved by external SMT solver
\item \ml{fast\_proof} --- proof was skipped to compile a theory rapidly
\item \ml{cheat} --- we cheated :-)
\end{itemize}
\item \alert{cheating} via \eg the \hol{cheat} tactic means skipping proofs
\item it can be helpful during proof development
\begin{itemize}
\item test whether some lemmata allow you finishing the proof
\item skip lengthy but boring cases and focus on critical parts first
\item experiment with exact form of invariants
\item \ldots
\end{itemize}
\item cheats should be removed reasonable quickly
\item HOL warns about cheats and skipped proofs
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Pitfalls of Definitional Approach}
\begin{itemize}
\item definitions can't introduce new inconsistencies
\item they force you to state all assumed properties at one location
\item however, you still need to be careful
\item Is your definition really expressing what you had in mind ?
\item Does your formalisation correspond to the real world artefact ?
\item How can you convince others that this is the case ?
\item we will discuss methods to deal with this later in this course
\begin{itemize}
\item formal sanity
\item conformance testing
\item code review
\item comments, good names, clear coding style
\item \ldots
\end{itemize}
\item this is highly complex and needs a lot of effort in general
\end{itemize}
\end{frame}
\section{Primitive Definition Principles}
\begin{frame}[fragile]
\frametitle{Specifications}
\begin{itemize}
\item HOL allows to introduce new constants with certain properties, provided the
existence of such constants has been shown
\begin{exampleblock}{Specification of \texttt{EVEN} and \texttt{ODD}}
\begin{semiverbatim}\scriptsize
> EVEN\_ODD\_EXISTS
val it = |- ?even odd. even 0 \holAnd{} ~odd 0 \holAnd{} (!n. even (SUC n) <=> odd n) \holAnd{}
(!n. odd (SUC n) <=> even n)
> val EO\_SPEC = new\_specification ("EO\_SPEC", ["EVEN", "ODD"], EVEN\_ODD\_EXISTS);
val EO\_SPEC = |- EVEN 0 \holAnd{} ~ODD 0 \holAnd{} (!n. EVEN (SUC n) <=> ODD n) \holAnd{}
(!n. ODD (SUC n) <=> EVEN n)
\end{semiverbatim}
\end{exampleblock}
\item \hol{new\_specification} is a convenience wrapper
\begin{itemize}
\item it uses existential quantification instead of Hilbert's choice
\item deals with pair syntax
\item stores resulting definitions in theory
\end{itemize}
\item \hol{new\_specification} captures the underlying principle nicely
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Definitions}
\begin{itemize}
\item special case: new constant defined by equality
\begin{exampleblock}{Specification with Equality}
\begin{semiverbatim}\scriptsize
> double_EXISTS
val it =
|- ?double. (!n. double n = (n + n))
> val double_def = new_specification ("double_def", ["double"], double_EXISTS);
val double_def =
|- !n. double n = n + n
\end{semiverbatim}
\end{exampleblock}
\item there is a specialised methods for such simple definitions
\begin{exampleblock}{Non Recursive Definitions}
\begin{semiverbatim}\scriptsize
> val DOUBLE_DEF = new_definition ("DOUBLE_DEF", ``DOUBLE n = n + n``)
val DOUBLE_DEF =
|- !n. DOUBLE n = n + n
\end{semiverbatim}
\end{exampleblock}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Restrictions for Definitions}
\begin{itemize}
\item all variables occurring on right-hand-side (rhs) need to be arguments
\begin{itemize}
\item \eg \hol{new\_definition (..., ``F n = n + m``)} fails
\item \hol{m} is free on rhs
\end{itemize}
\item all type variables occurring on rhs need to occur on lhs
\begin{itemize}
\item \eg \hol{new\_definition ("IS\_FIN\_TY", \\
\-\qquad\quad``IS\_FIN\_TY = FINITE (UNIV : 'a set)``)} fails
\item \hol{IS\_FIN\_TY} would lead to inconsistency
\item \hol{|- FINITE (UNIV : bool set)}
\item \hol{|- \holNeg{}FINITE (UNIV : num set)}
\item \hol {T <=> FINITE (UNIV:bool set) <=> \\ IS\_FIN\_TY <=>\\ FINITE (UNIV:num set) <=> F}
\item therefore, such definitions can't be allowed
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Underspecified Functions}
\begin{itemize}
\item function specification do not need to define the function precisely
\item multiple different functions satisfying one spec are possible
\item functions resulting from such specs are called \emph{underspecified}
\item underspecified functions are still total, one just lacks knowledge
\item one common application: modelling \emph{partial functions}
\begin{itemize}
\item functions like \eg \hol{HD} and \hol{TL} are total
\item they are defined for empty lists
\item however, it is not specified, which value they have for empty lists
\item only known: \hol{HD [] = HD []} and \hol{TL [] = TL []}
\begin{minipage}{.7\textwidth}\medskip
\begin{semiverbatim}\scriptsize
val MY_HD_EXISTS = prove (``?hd. !x xs. (hd (x::xs) = x)``, ...);
val MY_HD_SPEC =
new_specification ("MY_HD_SPEC", ["MY_HD"], MY_HD_EXISTS)
\end{semiverbatim}
\end{minipage}
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Primitive Type Definitions}
\begin{itemize}
\item HOL allows introducing non-empty subtypes of existing types
\item a predicate \hol{P : ty -> bool} describes a subset of an existing type \hol{ty}
\item \hol{ty} may contain type variables
\item only \emph{non-empty} types are allowed
\item therefore a non-emptyness proof \hol{ex-thm} of form \hol{?e.\ P e} is needed
\item \hol{new\_type\_definition (op-name, ex-thm)} then introduces a new type \hol{op-name}
specified by \hol{P}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Primitive Type Definitions - Example 1}
\begin{itemize}
\item lets try to define a type \hol{dlist} of lists containing no duplicates
\item predicate \hol{ALL\_DISTINCT : 'a list -> bool} is used to define it
\item easy to prove theorem \texttt{dlist\_exists}: \hol{|- ?l.\ ALL\_DISTINCT l}
\item \hol{val dlist\_TY\_DEF = new\_type\_definitions("dlist", dlist\_exists)} defines
a new type \ml{'a dlist} and returns a theorem\bigskip
\begin{semiverbatim}
|- ?(rep :'a dlist -> 'a list).
TYPE_DEFINITION ALL_DISTINCT rep
\end{semiverbatim}\bigskip
\item \ml{rep} is a function taking a \hol{'a dlist} to the list representing it
\begin{itemize}
\item \hol{rep} is injective
\item a list satisfies \hol{ALL\_DISTINCT} iff there is a corresponding \hol{dlist}
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Primitive Type Definitions - Example 2}
\begin{itemize}
\item \hol{define\_new\_type\_bijections} can be used to define bijections between old and new type
\medskip
\begin{semiverbatim}\scriptsize
> \hol{define_new_type_bijections \{name="dlist_tybij", ABS="abs_dlist",
REP="rep_dlist", tyax=\alert{dlist_TY_DEF}\}}
val it =
|- (!a. abs_dlist (rep_dlist a) = a) \holAnd{}
(!r. ALL_DISTINCT r <=> (rep_dlist (abs_dlist r) = r))
\end{semiverbatim}\medskip
\item other useful theorems can be automatically proved by
\begin{itemize}
\item \hol{prove\_abs\_fn\_one\_one}
\item \hol{prove\_abs\_fn\_onto}
\item \hol{prove\_rep\_fn\_one\_one}
\item \hol{prove\_rep\_fn\_onto}
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Primitive Definition Principles Summary}
\begin{itemize}
\item primitive definition principles are easily explained
\item they lead to conservative extensions
\item however, they are cumbersome to use
\item LCF approach allows implementing more convenient definition tools
\begin{itemize}
\item \alert{\texttt{Datatype}} package
\item \alert{\texttt{TFL}} (Total Functional Language) package
\item \ml{IndDef} (Inductive Definition) package
\item \ml{quotientLib} Quotient Types Library
\item ...
\end{itemize}
\end{itemize}
\end{frame}
\section{Functional Programming}
\begin{frame}
\frametitle{Functional Programming}
\begin{itemize}
\item the \hol{Datatype} package allows to define datatypes conveniently
\item the \hol{TFL} package allows to define (mutually recursive) functions
\item the \hol{EVAL} conversion allows evaluating those definitions
\item this gives many HOL developments the feeling of a functional program
\item there is really a close connection between functional programming and definitions in HOL
\begin{itemize}
\item functional programming design principles apply
\item \hol{EVAL} is a great way to test quickly, whether your definitions are working as intended
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Functional Programming Example}
\begin{semiverbatim}\scriptsize
> \hol{Datatype `mylist = E | L 'a mylist`}
val it = (): unit
> \hol{Define `(mylen E = 0) \holAnd{} (mylen (L x xs) = SUC (mylen xs))`}
Definition has been stored under "mylen\_def"
val it =
|- (mylen E = 0) \holAnd{} !x xs. mylen (L x xs) = SUC (mylen xs):
thm
> \hol{EVAL ``mylen (L 2 (L 3 (L 1 E)))``}
val it =
|- mylen (L 2 (L 3 (L 1 E))) = 3:
thm
\end{semiverbatim}
\end{frame}
\section{Datatype Definitions}
\begin{frame}[fragile]
\frametitle{Datatype Package}
\begin{itemize}
\item the \hol{Datatype} package allows to define SML style datatypes easily
\item there is support for
\begin{itemize}
\item algebraic datatypes
\item record types
\item mutually recursive types
\item ...
\end{itemize}
\item many constants are automatically introduced
\begin{itemize}
\item constructors
\item case-split constant
\item size function
\item field-update and accessor functions for records
\item ...
\end{itemize}
\item many theorems are derived and stored in current theory
\begin{itemize}
\item injectivity and distinctness of constructors
\item nchotomy and structural induction theorems
\item rewrites for case-split, size and record update functions
\item ...
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Datatype Package - Example I}
\begin{block}{Tree Datatype in SML}
\begin{semiverbatim}\scriptsize
datatype ('a,'b) btree = Leaf of 'a
| Node of ('a,'b) btree * 'b * ('a,'b) btree
\end{semiverbatim}
\end{block}
\begin{block}{Tree Datatype in HOL}
\begin{semiverbatim}\scriptsize
Datatype `btree = Leaf 'a
| Node btree 'b btree`
\end{semiverbatim}
\end{block}
\begin{block}{Tree Datatype in HOL --- Deprecated Syntax}
\begin{semiverbatim}\scriptsize
Hol_datatype `btree = Leaf of 'a
| Node of btree => 'b => btree`
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Datatype Package - Example I - Derived Theorems 1}
\begin{block}{\texttt{btree\_distinct}}
\begin{semiverbatim}\scriptsize
|- !a2 a1 a0 a. Leaf a <> Node a0 a1 a2
\end{semiverbatim}
\end{block}
\begin{block}{\texttt{btree\_11}}
\begin{semiverbatim}\scriptsize
|- (!a a'. (Leaf a = Leaf a') <=> (a = a')) \holAnd{}
(!a0 a1 a2 a0' a1' a2'.
(Node a0 a1 a2 = Node a0' a1' a2') <=>
(a0 = a0') \holAnd{} (a1 = a1') \holAnd{} (a2 = a2'))
\end{semiverbatim}
\end{block}
\begin{block}{\texttt{btree\_nchotomy}}
\begin{semiverbatim}\scriptsize
|- !bb. (?a. bb = Leaf a) \holOr{} (?b b1 b0. bb = Node b b1 b0)
\end{semiverbatim}
\end{block}
\begin{block}{\texttt{btree\_induction}}
\begin{semiverbatim}\scriptsize
|- !P. (!a. P (Leaf a)) \holAnd{}
(!b b0. P b \holAnd{} P b0 ==> !b1. P (Node b b1 b0)) ==>
!b. P b
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Datatype Package - Example I - Derived Theorems 2}
\begin{block}{\texttt{btree\_size\_def}}
\begin{semiverbatim}\scriptsize
|- (!f f1 a. btree_size f f1 (Leaf a) = 1 + f a) \holAnd{}
(!f f1 a0 a1 a2.
btree_size f f1 (Node a0 a1 a2) =
1 + (btree_size f f1 a0 + (f1 a1 + btree_size f f1 a2)))
\end{semiverbatim}
\end{block}
\begin{block}{\texttt{btree\_case\_def}}
\begin{semiverbatim}\scriptsize
|- (!a f f1. btree_CASE (Leaf a) f f1 = f a) \holAnd{}
(!a0 a1 a2 f f1. btree_CASE (Node a0 a1 a2) f f1 = f1 a0 a1 a2)
\end{semiverbatim}
\end{block}
\begin{block}{\texttt{btree\_case\_cong}}
\begin{semiverbatim}\scriptsize
|- !M M' f f1.
(M = M') \holAnd{} (!a. (M' = Leaf a) ==> (f a = f' a)) \holAnd{}
(!a0 a1 a2.
(M' = Node a0 a1 a2) ==> (f1 a0 a1 a2 = f1' a0 a1 a2)) ==>
(btree_CASE M f f1 = btree_CASE M' f' f1')
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Datatype Package - Example II}
\begin{block}{Enumeration type in SML}
\begin{semiverbatim}\scriptsize
datatype my_enum = E1 | E2 | E3
\end{semiverbatim}
\end{block}
\begin{block}{Enumeration type in HOL}
\begin{semiverbatim}\scriptsize
Datatype `my_enum = E1 | E2 | E3`
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Datatype Package - Example II - Derived Theorems}
\begin{block}{\texttt{my\_enum\_nchotomy}}
\begin{semiverbatim}\scriptsize
|- !P. P E1 \holAnd{} P E2 \holAnd{} P E3 ==> !a. P a
\end{semiverbatim}
\end{block}
\begin{block}{\texttt{my\_enum\_distinct}}
\begin{semiverbatim}\scriptsize
|- E1 <> E2 \holAnd{} E1 <> E3 \holAnd{} E2 <> E3
\end{semiverbatim}
\end{block}
\begin{block}{\texttt{my\_enum2num\_thm}}
\begin{semiverbatim}\scriptsize
|- (my_enum2num E1 = 0) \holAnd{} (my_enum2num E2 = 1) \holAnd{} (my_enum2num E3 = 2)
\end{semiverbatim}
\end{block}
\begin{block}{\texttt{my\_enum2num\_num2my\_enum}}
\begin{semiverbatim}\scriptsize
|- !r. r < 3 <=> (my_enum2num (num2my_enum r) = r)
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Datatype Package - Example III}
\begin{block}{Record type in SML}
\begin{semiverbatim}\scriptsize
type rgb = \{ r : int, g : int, b : int \}
\end{semiverbatim}
\end{block}
\begin{block}{Record type in HOL}
\begin{semiverbatim}\scriptsize
Datatype `rgb = <| r : num; g : num; b : num |>`
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Datatype Package - Example III - Derived Theorems}
\begin{block}{\texttt{rgb\_component\_equality}}
\begin{semiverbatim}\scriptsize
|- !r1 r2. (r1 = r2) <=>
(r1.r = r2.r) \holAnd{} (r1.g = r2.g) \holAnd{} (r1.b = r2.b)
\end{semiverbatim}
\end{block}
\begin{block}{\texttt{rgb\_nchotomy}}
\begin{semiverbatim}\scriptsize
|- !rr. ?n n0 n1. rr = rgb n n0 n1
\end{semiverbatim}
\end{block}
\begin{block}{\texttt{rgb\_r\_fupd}}
\begin{semiverbatim}\scriptsize
|- !f n n0 n1. rgb n n0 n1 with r updated_by f = rgb (f n) n0 n1
\end{semiverbatim}
\end{block}
\begin{block}{\texttt{rgb\_updates\_eq\_literal}}
\begin{semiverbatim}\scriptsize
|- !r n1 n0 n.
r with <|r := n1; g := n0; b := n|> = <|r := n1; g := n0; b := n|>
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Datatype Package - Example IV}
\begin{itemize}
\item nested record types are not allowed
\item however, mutual recursive types can mitigate this restriction
\end{itemize}
\begin{block}{Filesystem Datatype in SML}
\begin{semiverbatim}\scriptsize
datatype file = Text of string
| Dir of \{owner : string ,
files : (string * file) list\}
\end{semiverbatim}
\end{block}
\begin{alertblock}{\textbf{Not Supported} Nested Record Type Example in HOL}
\begin{semiverbatim}\scriptsize
Datatype `file = Text string
| Dir <| owner : string ;
files : (string # file) list |>`
\end{semiverbatim}
\end{alertblock}
\begin{block}{Filesystem Datatype - Mutual Recursion in HOL}
\begin{semiverbatim}\scriptsize
Datatype `file = Text string
| Dir directory
;
directory = <| owner : string ;
files : (string # file) list |>`
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Datatype Package - No support for Co-Algebraic Types}
\begin{itemize}
\item there is no support for co-algebraic types
\item the \texttt{Datatype} package could be extended to do so
\item other systems like Isabelle/HOL provide high-level methods for defining such types
\end{itemize}
\begin{block}{Co-algebraic Type Example in SML --- Lazy Lists}
\begin{semiverbatim}\scriptsize
datatype 'a lazylist = Nil
| Cons of ('a * (unit -> 'a lazylist))
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Datatype Package - Discussion}
\begin{itemize}
\item \texttt{Datatype} package allows to define many useful datatypes
\item however, there are many limitations
\begin{itemize}
\item some types cannot be defined in HOL, \eg empty types
\item some types are not supported, \eg co-algebraic types
\item there are bugs (currently \eg some trouble with certain mutually recursive definitions)
\end{itemize}
\item biggest restrictions in practice (in my opinion and my line of work)
\begin{itemize}
\item no support for co-algebraic datatypes
\item no nested record datatypes
\end{itemize}
\item depending on datatype, different sets of useful lemmata are derived
\item most important ones are added to \hol{TypeBase}
\begin{itemize}
\item tools like \hol{Induct\_on}, \hol{Cases\_on} use them
\item there is support for pattern matching
\end{itemize}
\end{itemize}
\end{frame}
\section{Recursive Function Definitions}
\begin{frame}
\frametitle{Total Functional Language (\texttt{TFL}) package}
\begin{itemize}
\item \ml{TFL} package implements support for terminating functional definitions
\item \hol{Define} defines functions from high-level descriptions
\item there is support for pattern matching
\item look and feel is like function definitions in SML
\item based on \emph{well-founded recursion} principle
\item \hol{Define} is the most common way for definitions in HOL
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Well-Founded Relations}
\begin{itemize}
\item a relation \texttt{R : 'a -> 'a -> bool} is called \emph{well-founded}, iff
there are no infinite descending chains\\[.5em]
\hol{wellfounded R = \holNeg{}?f.\ !n.\ R (f (SUC n)) (f n)}
\bigskip
\item Example: \texttt{\$< :\ num -> num -> bool} is well-founded
\item if arguments of recursive calls are smaller according to well-founded relation,
the recursion terminates
\item this is the essence of termination proofs
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Well-Founded Recursion}
\begin{itemize}
\item a well-founded relation \hol{R} can be used to define recursive functions
\item this recursion principle is called \hol{WFREC} in HOL
\item idea of \hol{WFREC}
\begin{itemize}
\item if arguments get smaller according to \hol{R}, perform recursive call
\item otherwise abort and return \hol{ARB}
\end{itemize}
\item \hol{WFREC} always defines a function
\item if all recursive calls indeed decrease according to \hol{R}, the original recursive
equations can be derived from the \hol{WFREC} representation
\item TFL uses this internally
\item however, this is well-hidden from the user
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{\texttt{Define} - Initial Examples}
\begin{block}{Simple Definitions}
\begin{semiverbatim}\scriptsize
> \hol{val DOUBLE_def = Define `DOUBLE n = n + n`}
val DOUBLE_def =
|- !n. DOUBLE n = n + n:
thm
> \hol{val MY_LENGTH_def = Define `(MY_LENGTH [] = 0) \holAnd{}
(MY_LENGTH (x::xs) = SUC (MY_LENGTH xs))`}
val MY_LENGTH_def =
|- (MY_LENGTH [] = 0) \holAnd{} !x xs. MY_LENGTH (x::xs) = SUC (MY_LENGTH xs):
thm
> \hol{val MY_APPEND_def = Define `(MY_APPEND [] ys = ys) \holAnd{}
(MY_APPEND (x::xs) ys = x :: (MY_APPEND xs ys))`}
val MY_APPEND_def =
|- (!ys. MY_APPEND [] ys = ys) \holAnd{}
(!x xs ys. MY_APPEND (x::xs) ys = x::MY_APPEND xs ys):
thm
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}
\frametitle{\texttt{Define} discussion}
\begin{itemize}
\item \hol{Define} feels like a function definition in HOL
\item it can be used to define "terminating" recursive functions
\item \hol{Define} is implemented by a large, non-trivial piece of SML code
\item it uses many heuristics
\item outcome of \hol{Define} sometimes hard to predict
\item the input descriptions are only hints
\begin{itemize}
\item the produced function and the definitional theorem might be different
\item in simple examples, quantifiers added
\item pattern compilation takes place
\item earlier ``conjuncts'' have precedence
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{\texttt{Define} - More Examples}
\begin{block}{}
\begin{semiverbatim}\scriptsize
> \hol{val MY_HD_def = Define `MY_HD (x :: xs) = x`}
val MY_HD_def = |- !x xs. MY_HD (x::xs) = x : thm
> \hol{val IS_SORTED_def = Define `
(IS_SORTED (x1 :: x2 :: xs) = ((x1 < x2) \holAnd{} (IS_SORTED (x2::xs)))) \holAnd{}
(IS_SORTED _ = T)`}
val IS_SORTED_def =
|- (!xs x2 x1. IS_SORTED (x1::x2::xs) <=> x1 < x2 \holAnd{} IS_SORTED (x2::xs)) \holAnd{}
(IS_SORTED [] <=> T) \holAnd{} (!v. IS_SORTED [v] <=> T)
> \hol{val EVEN_def = Define `(EVEN 0 = T) \holAnd{} (ODD 0 = F) \holAnd{}
(EVEN (SUC n) = ODD n) \holAnd{} (ODD (SUC n) = EVEN n)`}
val EVEN_def =
|- (EVEN 0 <=> T) \holAnd{} (ODD 0 <=> F) \holAnd{} (!n. EVEN (SUC n) <=> ODD n) \holAnd{}
(!n. ODD (SUC n) <=> EVEN n) : thm
> \hol{val ZIP_def = Define `(ZIP (x::xs) (y::ys) = (x,y)::(ZIP xs ys)) \holAnd{}
(ZIP \_ \_ = [])`}
val ZIP_def =
|- (!ys y xs x. ZIP (x::xs) (y::ys) = (x,y)::ZIP xs ys) \holAnd{}
(!v1. ZIP [] v1 = []) \holAnd{} (!v4 v3. ZIP (v3::v4) [] = []) : thm
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Primitive Definitions}
\begin{itemize}
\item \hol{Define} introduces (if needed) the function using \hol{WFREC}
\item intended definition derived as a theorem
\item the theorems are stored in current theory
\item usually, one never needs to look at it
\end{itemize}
\begin{block}{Examples}
\begin{semiverbatim}\scriptsize
val IS_SORTED_primitive_def =
|- IS_SORTED =
WFREC (@R.\ WF R \holAnd{} !x1 xs x2. R (x2::xs) (x1::x2::xs))
(\textbsl{}IS_SORTED a.
case a of
[] => I T
| [x1] => I T
| x1::x2::xs => I (x1 < x2 \holAnd{} IS_SORTED (x2::xs)))
|- !R M. WF R ==> !x. WFREC R M x = M (RESTRICT (WFREC R M) R x) x
|- !f R x. RESTRICT f R x = (\textbsl{}y. if R y x then f y else ARB)
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Induction Theorems}
\begin{itemize}
\item \hol{Define} automatically defines induction theorems
\item these theorems are stored in current theory with suffix \hol{ind}
\item use \hol{DB.fetch "-" "something\_ind"} to retrieve them
\item these induction theorems are useful to reason about corresponding recursive functions
\end{itemize}
\begin{block}{Example}
\begin{semiverbatim}\scriptsize
val IS_SORTED_ind = |- !P.
((!x1 x2 xs. P (x2::xs) ==> P (x1::x2::xs)) \holAnd{}
P [] \holAnd{}
(!v. P [v])) ==>
!v. P v
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{\texttt{Define} failing}
\begin{itemize}
\item \hol{Define} might fail for various reasons to define a function
\begin{itemize}
\item such a function cannot be defined in HOL
\item such a function can be defined, but not via the methods used by TFL
\item TFL can define such a function, but its heuristics are too weak and user guidance is required
\item there is a bug :-)
\end{itemize}
\item \emph{termination} is an important concept for \hol{Define}
\item it is easy to misunderstand termination in the context of HOL
\item we need to understand what is meant by termination
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Termination in HOL}
\begin{itemize}
\item in SML it is natural to talk about termination of functions
\item in the HOL logic there is no concept of execution
\item thus, there is no concept of termination in HOL
\begin{minipage}{.8\textwidth}
\begin{exampleblock}{3 characterisations of a function \texttt{f :\ num -> num}}
\begin{itemize}
\item \hol{|- !n.\ f n = 0}
\item \hol{|- (f 0 = 0) \holAnd{} !n.\ (f (SUC n) = f n)}
\item \hol{|- (f 0 = 0) \holAnd{} !n.\ (f n = f (SUC n))}
\end{itemize}
Is \hol{f} terminating? All 3 theorems are equivalent.
\end{exampleblock}
\end{minipage}\bigskip
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Termination in HOL II}
\begin{itemize}
\item it is useful to think in terms of termination
\item the TFL package implements heuristics to define functions that would terminate in SML
\item the TFL package uses well-founded recursion
\item the required well-founded relation corresponds to a termination proof
\item therefore, it is very natural to think of \hol{Define} searching a termination proof
\item important: this is the idea behind this function definition package, not a property of HOL
\end{itemize}
\bottomstatement{\alert{HOL is not limited to "terminating" functions}}
\end{frame}
\begin{frame}[fragile]
\frametitle{Termination in HOL III}
\begin{itemize}
\item one can define "non-terminating" functions in HOL
\item however, one cannot do so (easily) with \hol{Define}
\end{itemize}
\begin{exampleblock}{Definition of \texttt{WHILE} in HOL}
\begin{semiverbatim}\scriptsize
\emph{|- !P g x. WHILE P g x = if P x then WHILE P g (g x) else x}
\end{semiverbatim}
\end{exampleblock}
\begin{exampleblock}{Execution Order}\scriptsize
There is no "execution order". One can easily define a complicated constant function:
\vspace{-.7em}
\begin{semiverbatim}
\emph{(myk : num -> num) (n:num) = (let x = myk (n+1) in 0)}
\end{semiverbatim}
\end{exampleblock}
\begin{alertblock}{Unsound Definitions}\scriptsize
A function \hol{f : num -> num} with the following property cannot be defined in HOL unless HOL has an inconsistancy:
\begin{semiverbatim}
\hol{!n. f n = ((f n) + 1)}
\end{semiverbatim}
Such a function would allow to prove \hol{0 = 1}.
\end{alertblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Manual Termination Proofs I}
\begin{itemize}
\item TFL uses various heuristics to find a well-founded relation
\item however, these heuristics may not be strong enough
\item in such cases the user can provide a well-founded relation manually
\item the most common well-founded relations are \emph{measures}
\item measures map values to natural numbers and use the less relation\\
\hol{|- !(\alert{f:'a -> num}) x y.\ measure f x y <=> (f x < f y)}
\item all measures are well-founded: \hol{|- !f.\ WF (measure f)}
\item moreover, existing well-founded relations can be combined
\begin{itemize}
\item lexicographic order \hol{LEX}
\item list lexicographic order \hol{LLEX}
\item \ldots
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Manual Termination Proofs II}
\begin{itemize}
\item if \hol{Define} fails to find a termination proof, \hol{Hol\_defn} can be used
\item \hol{Hol\_defn} defers termination proofs
\item it derives termination conditions and
sets up the function definitions
\item all results are packaged as a value of type \hol{defn}
\item after calling \hol{Hol\_defn} the defined function(s) can be used
\item however, the intended definition theorem has not been derived yet
\item to derive it, one needs to
\begin{itemize}
\item provide a well-founded relation
\item show that termination conditions respect that relation
\end{itemize}
\item \hol{Defn.tprove} and \hol{Defn.tgoal} are intended for this
\item proofs usually start by providing relation via tactic \hol{WF\_REL\_TAC}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Manual Termination Proof Example 1}
\begin{semiverbatim}\scriptsize
> \hol{val qsort_defn = Hol_defn "qsort" `
(qsort ord [] = []) \holAnd{}
(qsort ord (x::rst) =
(qsort ord (FILTER (\$\holNeg{} o ord x) rst)) ++
[x] ++
(qsort ord (FILTER (ord x) rst)))`}
val qsort_defn = HOL function definition (recursive)
Equation(s) :
[...] |- qsort ord [] = []
[...] |- qsort ord (x::rst) =
qsort ord (FILTER ($\holNeg{} o ord x) rst) ++ [x] ++
qsort ord (FILTER (ord x) rst)
Induction : ...
Termination conditions :
0. !rst x ord. R (ord,FILTER (ord x) rst) (ord,x::rst)
1. !rst x ord. R (ord,FILTER ($\holNeg{} o ord x) rst) (ord,x::rst)
2. WF R
\end{semiverbatim}
\end{frame}
\begin{frame}[fragile]
\frametitle{Manual Termination Proof Example 2}
\begin{semiverbatim}\scriptsize
> \hol{Defn.tgoal qsort_defn}
Initial goal:
?R.
WF R \holAnd{}
(!rst x ord. R (ord,FILTER (ord x) rst) (ord,x::rst)) \holAnd{}
(!rst x ord. R (ord,FILTER (\$\holNeg{} o ord x) rst) (ord,x::rst))
\pause
> \hol{e (WF_REL_TAC `measure (\textbsl{}(\_, l).\ LENGTH l)`)}
1 subgoal :
(!rst x ord. LENGTH (FILTER (ord x) rst) < LENGTH (x::rst)) \holAnd{}
(!rst x ord. LENGTH (FILTER (\textbsl{}x'.\ \holNeg{}ord x x') rst) < LENGTH (x::rst))
> \hol{...}
\end{semiverbatim}
\end{frame}
\begin{frame}[fragile]
\frametitle{Manual Termination Proof Example 3}
\begin{semiverbatim}\scriptsize
> \hol{val (qsort_def, qsort_ind) =
Defn.tprove (qsort_defn,
WF_REL_TAC `measure (\textbsl{}(\_, l).\ LENGTH l)`) >> ...)}
val qsort_def =
|- (qsort ord [] = []) \holAnd{}
(qsort ord (x::rst) =
qsort ord (FILTER ($~ o ord x) rst) ++ [x] ++
qsort ord (FILTER (ord x) rst))
val qsort_ind =
|- !P. (!ord. P ord []) \holAnd{}
(!ord x rst.
P ord (FILTER (ord x) rst) \holAnd{}
P ord (FILTER ($~ o ord x) rst) ==>
P ord (x::rst)) ==>
!v v1. P v v1
\end{semiverbatim}
\end{frame}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "current"
%%% End:

511
lectures/11_good_definitions.tex Normal file
View File

@ -0,0 +1,511 @@
\part{Good Definitions}
\frame[plain]{\partpage}
\section{General Discussion}
\begin{frame}
\frametitle{Importance of Good Definitions}
\begin{itemize}
\item using \textit{good} definitions is very important
\begin{itemize}
\item good definitions are vital for \emph{clarity}
\item \emph{proofs} depend a lot on the form of definitions
\end{itemize}
\item unluckily, it is hard to state what a good definition is
\item even harder to come up with good definitions
\item let's look at it a bit closer anyhow
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Importance of Good Definitions --- Clarity I}
\begin{itemize}
\item HOL guarantees that theorems do indeed hold
\item However, does the theorem mean what you think it does?
\item you can separate your development in
\begin{itemize}
\item main theorems you care for
\item auxiliary stuff used to derive your main theorems
\end{itemize}
\item it is essential to understand your main theorems
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Importance of Good Definitions --- Clarity II}
\begin{minipage}[t]{.45\textwidth}
\begin{block}{Guarded by HOL}
\begin{itemize}
\item proofs checked
\item internal, technical definitions
\item technical lemmata
\item proof tools
\end{itemize}
\end{block}
\end{minipage}
\qquad
\begin{minipage}[t]{.45\textwidth}
\begin{block}{Manual review needed for}
\begin{itemize}
\item meaning of main theorems
\item meaning of definitions used by main theorems
\item meaning of types used by main theorems
\end{itemize}
\end{block}
\end{minipage}
\end{frame}
\begin{frame}
\frametitle{Importance of Good Definitions --- Clarity III}
\begin{itemize}
\item it is essential to understand your main theorems
\begin{itemize}
\item you need to understand all the definitions directly used
\item you need to understand the indirectly used ones as well
\item you need to convince others that you express the intended statement
\item therefore, it is vital to \alert{use very simple, clear definitions}
\end{itemize}
\item defining concepts is often the main development task
\item checking resulting model against real artefact is vital
\begin{itemize}
\item testing via \eg \hol{EVAL}
\item formal sanity
\item conformance testing
\end{itemize}
\item wrong models are main source of error when using HOL
\item proofs, auxiliary lemmata and auxiliary definitions
\begin{itemize}
\item can be as technical and complicated as you like
\item correctness is guaranteed by HOL
\item reviewers don't need to care
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Importance of Good Definitions --- Proofs}
\begin{itemize}
\item good definitions can shorten proofs significantly
\item they improve maintainability
\item they can improve automation drastically
\item unluckily for proofs definitions often need to be technical
\item this contradicts clarity aims
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{How to come up with good definitions}
\begin{itemize}
\item unluckily, it is hard to state what a good definition is
\item it is even harder to come up with them
\begin{itemize}
\item there are often many competing interests
\item a lot of experience and detailed tool knowledge is needed
\item much depends on personal style and taste
\end{itemize}
\item general advice: use more than one definition
\begin{itemize}
\item in HOL you can derive equivalent definitions as theorems
\item define a concept as clearly and easily as possible
\item derive equivalent definitions for various purposes
\begin{itemize}
\item one very close to your favourite textbook
\item one nice for certain types of proofs
\item another one good for evaluation
\item \ldots
\end{itemize}
\end{itemize}
\item lessons from functional programming apply
\end{itemize}
\end{frame}
\section{Functional Programming}
\begin{frame}
\frametitle{Good Definitions in Functional Programming}
\begin{block}{Objectives}
\begin{itemize}
\item clarity (readability, maintainability)
\item performance (runtime speed, memory usage, ...)
\end{itemize}
\end{block}
\begin{block}{General Advice}
\begin{itemize}
\item use the powerful type-system
\item use many small function definitions
\item encode invariants in types and function signatures
\end{itemize}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Good Definitions -- no number encodings}
\begin{itemize}
\item many programmers familiar with C encode everything as a number
\item enumeration types are very cheap in SML and HOL
\item use them instead
\end{itemize}
\begin{exampleblock}{Example Enumeration Types}\scriptsize
In C the result of an order comparison is an integer with 3 equivalence classes:
0, negative and positive integers. In SML and HOL, it is better to use a variant type.
\begin{semiverbatim}
val _ = Datatype `ordering = LESS | EQUAL | GREATER`;
val compare_def = Define `
(compare LESS lt eq gt = lt)
\holAnd{} (compare EQUAL lt eq gt = eq)
\holAnd{} (compare GREATER lt eq gt = gt) `;
val list_compare_def = Define `
(list_compare cmp [] [] = EQUAL) \holAnd{} (list_compare cmp [] l2 = LESS)
\holAnd{} (list_compare cmp l1 [] = GREATER)
\holAnd{} (list_compare cmp (x::l1) (y::l2) = compare (cmp (x:'a) y)
(* x<y *) LESS
(* x=y *) (list_compare cmp l1 l2)
(* x>y *) GREATER) `;
\end{semiverbatim}
\end{exampleblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Good Definitions --- Isomorphic Types}
\begin{itemize}
\item the type-checker is your friend
\begin{itemize}
\item it helps you find errors
\item code becomes more robust
\item using good types is a great way of writing self-documenting code
\end{itemize}
\item therefore, use many types
\item even use types isomorphic to existing ones
\end{itemize}
\begin{exampleblock}{Virtual and Physical Memory Addresses}\scriptsize
Virtual and physical addresses might in a development both be numbers. It is
still nice to use separate types to avoid mixing them up.
\begin{semiverbatim}
val _ = Datatype `vaddr = VAddr num`;
val _ = Datatype `paddr = PAddr num`;
val virt_to_phys_addr_def = Define `
virt_to_phys_addr (VAddr a) = PAddr( \textrm{\textit{translation of}} a )`;
\end{semiverbatim}
\end{exampleblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Good Definitions --- Record Types I}
\begin{itemize}
\item often people use tuples where records would be more appropriate
\item using large tuples quickly becomes awkward
\begin{itemize}
\item it is easy to mix up order of tuple entries
\begin{itemize}
\item often types coincide, so type-checker does not help
\end{itemize}
\item no good error messages for tuples
\begin{itemize}
\item hard to decipher type mismatch messages for long product types
\item hard to figure out which entry is missing at which position
\item non-local error messages
\item variable in last entry can hide missing entries
\end{itemize}
\end{itemize}
\item records sometimes require slightly more proof effort
\item however, records have many benefits
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Good Definitions --- Record Types II}
\begin{itemize}
\item using records
\begin{itemize}
\item introduces field names
\item provides automatically defined accessor and update functions
\item leads to better type-checking error messages
\end{itemize}
\item records improve readability
\begin{itemize}
\item accessors and update functions lead to shorter code
\item field names act as documentation
\end{itemize}
\item records improve maintainability
\begin{itemize}
\item improved error messages
\item much easier to add extra fields
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Good Definitions --- Encoding Invariants}
\begin{itemize}
\item try to encode as many invariants as possible in the types
\item this allows the type-checker to ensure them for you
\item you don't have to check them manually any more
\item your code becomes more robust and clearer
\end{itemize}
\begin{exampleblock}{Network Connections (Example by Yaron Minsky from Jane Street)}\scriptsize
Consider the following datatype for network connections. It has many implicit invariants.
\begin{semiverbatim}
datatype connection_state = Connected | Disconnected | Connecting;
type connection_info = \{
state : connection_state,
server : inet_address,
last_ping_time : time option,
last_ping_id : int option,
session_id : string option,
when_initiated : time option,
when_disconnected : time option
\}
\end{semiverbatim}
\end{exampleblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Good Definitions --- Encoding Invariants II}
\begin{exampleblock}{Network Connections (Example by Yaron Minsky from Jane Street) II}\scriptsize
The following definition of \texttt{connection\_info} makes the invariants explicit:
\begin{semiverbatim}
type connected = \{ last_ping : (time * int) option,
session_id : string \};
type disconnected = \{ when_disconnected : time \};
type connecting = \{ when_initiated : time \};
datatype connection_state =
Connected of connected
| Disconnected of disconneted
| Connecting of connecting;
type connection_info = \{
state : connection_state,
server : inet_address
\}
\end{semiverbatim}
\end{exampleblock}
\end{frame}
\section{HOL}
\begin{frame}
\frametitle{Good Definitions in HOL}
\begin{block}{Objectives}
\begin{itemize}
\item clarity (readability)
\item good for proofs
\item performance (good for automation, easily evaluatable, ...)
\end{itemize}
\end{block}
\begin{block}{General Advice}
\begin{itemize}
\item same advice as for functional programming applies
\item use even smaller definitions
\begin{itemize}
\item introduce auxiliary definitions for important function parts
\item use extra definitions for important constants
\item ...
\end{itemize}
\item tiny definitions
\begin{itemize}
\item allow keeping proof state small by unfolding only needed ones
\item allow many small lemmata
\item improve maintainability
\end{itemize}
\end{itemize}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Good Definitions in HOL II}
\begin{block}{Technical Issues}
\begin{itemize}
\item write definitions such that they work well with HOL's tools
\item this requires you to know HOL well
\item a lot of experience is required
\item general advice
\begin{itemize}
\item avoid explicit case-expressions
\item prefer curried functions
\end{itemize}
\end{itemize}
\end{block}
\begin{block}{Example}
\begin{semiverbatim}\scriptsize
val ZIP_GOOD_def = Define `(ZIP (x::xs) (y::ys) = (x,y)::(ZIP xs ys)) \holAnd{}
(ZIP _ _ = [])`
val ZIP_BAD1_def = Define `ZIP xs ys = case (xs, ys) of
(x::xs, y::ys) => (x,y)::(ZIP xs ys)
| (_, _) => []`
val ZIP_BAD2_def = Define `(ZIP (x::xs, y::ys) = (x,y)::(ZIP (xs, ys))) \holAnd{}
(ZIP _ = [])`
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Good Definitions in HOL III}
\begin{block}{Multiple Equivalent Definitions}
\begin{itemize}
\item satisfy competing requirements by having multiple equivalent definitions
\item derive them as theorems
\item initial definition should be as clear as possible
\begin{itemize}
\item clarity allows simpler reviews
\item simplicity reduces the likelihood of errors
\end{itemize}
\end{itemize}
\end{block}
\begin{block}{Example - \texttt{ALL\_DISTINCT}}
\begin{semiverbatim}\scriptsize
|- (ALL_DISTINCT [] <=> T) \holAnd{}
(!h t. ALL_DISTINCT (h::t) <=> \holNeg{}MEM h t \holAnd{} ALL_DISTINCT t)
|- !l. ALL_DISTINCT l <=>
(!x. MEM x l ==> (FILTER (\$= x) l = [x]))
|- !ls. ALL_DISTINCT ls <=> (CARD (set ls) = LENGTH ls):
\end{semiverbatim}
\end{block}
\end{frame}
\section{Formal Sanity}
\begin{frame}[fragile]
\frametitle{Formal Sanity}
\begin{block}{Formal Sanity}
\begin{itemize}
\item to ensure correctness test your definitions via \eg \hol{EVAL}
\item in HOL testing means symbolic evaluation, \ie proving lemmata
\item \emph{formally proving sanity check lemmata} is very beneficial
\begin{itemize}
\item they should express core properties of your definition
\item thereby they check your intuition against your actual definitions
\item these lemmata are often useful for following proofs
\item using them improves robustness and maintainability of your development
\end{itemize}
\item I highly recommend using formal sanity checks
\end{itemize}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Formal Sanity Example I}
\begin{semiverbatim}\scriptsize
> \hol{val ALL_DISTINCT = Define `
(ALL_DISTINCT [] = T) \holAnd{}
(ALL_DISTINCT (h::t) = \holNeg{}MEM h t \holAnd{} ALL_DISTINCT t)`};
\end{semiverbatim}
\begin{block}{Example Sanity Check Lemmata}
\begin{semiverbatim}\scriptsize
|- ALL_DISTINCT []\smallskip
|- !x xs. ALL_DISTINCT (x::xs) <=> \holNeg{}MEM x xs \holAnd{} ALL_DISTINCT xs\smallskip
|- !x. ALL_DISTINCT [x]\smallskip
|- !x xs. \holNeg{}(ALL_DISTINCT (x::x::xs))\smallskip
|- !l. ALL_DISTINCT (REVERSE l) <=> ALL_DISTINCT l\smallskip
|- !x l. ALL_DISTINCT (SNOC x l) <=> \holNeg{}MEM x l \holAnd{} ALL_DISTINCT l\smallskip
|- !l1 l2. ALL_DISTINCT (l1 ++ l2) <=>
ALL_DISTINCT l1 \holAnd{} ALL_DISTINCT l2 \holAnd{} !e. MEM e l1 ==> \holNeg{}MEM e l2
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Formal Sanity Example II 1}
\begin{semiverbatim}\scriptsize
> \hol{val ZIP_def = Define `
(ZIP [] ys = []) \holAnd{} (ZIP xs [] = []) \holAnd{}
(ZIP (x::xs) (y::ys) = (x, y)::(ZIP xs ys))`}
val ZIP_def =
|- (!ys. ZIP [] ys = []) \holAnd{} (!v3 v2. ZIP (v2::v3) [] = []) \holAnd{}
(!ys y xs x. ZIP (x::xs) (y::ys) = (x,y)::ZIP xs ys)
\end{semiverbatim}\vspace{-1em}
\begin{itemize}
\item above definition of \hol{ZIP} looks straightforward
\item small changes cause heuristics to produce different theorems
\item use formal sanity lemmata to compensate
\end{itemize}
\begin{semiverbatim}\scriptsize
> \hol{val ZIP_def = Define `
(ZIP xs [] = []) \holAnd{} (ZIP [] ys = []) \holAnd{}
(ZIP (x::xs) (y::ys) = (x, y)::(ZIP xs ys))`}
val ZIP_def =
|- (!xs. ZIP xs [] = []) \holAnd{} (!v3 v2. ZIP [] (v2::v3) = []) \holAnd{}
(!ys y xs x. ZIP (x::xs) (y::ys) = (x,y)::ZIP xs ys0
\end{semiverbatim}
\end{frame}
\begin{frame}[fragile]
\frametitle{Formal Sanity Example II 2}
\begin{semiverbatim}\scriptsize
val ZIP_def =
|- (!ys. ZIP [] ys = []) \holAnd{} (!v3 v2. ZIP (v2::v3) [] = []) \holAnd{}
(!ys y xs x. ZIP (x::xs) (y::ys) = (x,y)::ZIP xs ys)
\end{semiverbatim}
\begin{block}{Example Formal Sanity Lemmata}
\begin{semiverbatim}\scriptsize
|- (!xs. ZIP xs [] = []) \holAnd{} (!ys. ZIP [] ys = []) \holAnd{}
(!y ys x xs. ZIP (x::xs) (y::ys) = (x,y)::ZIP xs ys)\smallskip
|- !xs ys. LENGTH (ZIP xs ys) = MIN (LENGTH xs) (LENGTH ys)\smallskip
|- !x y xs ys. MEM (x, y) (ZIP xs ys) ==> (MEM x xs \holAnd{} MEM y ys)\smallskip
|- !xs1 xs2 ys1 ys2. LENGTH xs1 = LENGTH ys1 ==>
(ZIP (xs1++xs2) (ys1++ys2) = (ZIP xs1 ys1 ++ ZIP xs2 ys2))\smallskip
...
\end{semiverbatim}
\end{block}
\begin{itemize}
\item in your proofs use sanity lemmata, not original definition
\item this makes your development robust against
\begin{itemize}
\item small changes to the definition required later
\item changes to \hol{Define} and its heuristics
\item bugs in function definition package
\end{itemize}
\end{itemize}
\end{frame}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "current"
%%% End:

195
lectures/12_deep_shallow.tex Normal file
View File

@ -0,0 +1,195 @@
\part{Deep and Shallow Embeddings}
\frame[plain]{\partpage}
\begin{frame}
\frametitle{Deep and Shallow Embeddings}
\begin{itemize}
\item often one models some kind of formal language
\item important design decision: use \emph{deep} or \emph{shallow} embedding
\item in a nutshell:
\begin{itemize}
\item shallow embeddings just model semantics
\item deep embeddings model syntax as well
\end{itemize}
\item a shallow embedding directly uses the HOL logic
\item a deep embedding
\begin{itemize}
\item defines a datatype for the syntax of the language
\item provides a function to map this syntax to a semantic
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Example: Embedding of Propositional Logic I}
\begin{itemize}
\item propositional logic is a subset of HOL
\item a shallow embedding is therefore trivial
\end{itemize}
\begin{semiverbatim}\scriptsize
val sh_true_def = Define `sh_true = T`;
val sh_var_def = Define `sh_var (v:bool) = v`;
val sh_not_def = Define `sh_not b = \holNeg{}b`;
val sh_and_def = Define `sh_and b1 b2 = (b1 \holAnd{} b2)`;
val sh_or_def = Define `sh_or b1 b2 = (b1 \holOr{} b2)`;
val sh_implies_def = Define `sh_implies b1 b2 = (b1 ==> b2)`;
\end{semiverbatim}
\end{frame}
\begin{frame}[fragile]
\frametitle{Example: Embedding of Propositional Logic II}
\begin{itemize}
\item we can also define a datatype for propositional logic
\item this leads to a deep embedding
\begin{semiverbatim}\scriptsize
val _ = Datatype `bvar = BVar num`
val _ = Datatype `prop = d_true | d_var bvar | d_not prop
| d_and prop prop | d_or prop prop
| d_implies prop prop`;
val _ = Datatype `var_assignment = BAssign (bvar -> bool)`
val VAR_VALUE_def = Define `VAR_VALUE (BAssign a) v = (a v)`
val PROP_SEM_def = Define `
(PROP_SEM a d_true = T) \holAnd{}
(PROP_SEM a (d_var v) = VAR_VALUE a v) \holAnd{}
(PROP_SEM a (d_not p) = \holNeg{}(PROP_SEM a p)) \holAnd{}
(PROP_SEM a (d_and p1 p2) = (PROP_SEM a p1 \holAnd{} PROP_SEM a p2)) \holAnd{}
(PROP_SEM a (d_or p1 p2) = (PROP_SEM a p1 \holOr{} PROP_SEM a p2)) \holAnd{}
(PROP_SEM a (d_implies p1 p2) = (PROP_SEM a p1 ==> PROP_SEM a p2))`
\end{semiverbatim}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Shallow vs.\ Deep Embeddings}
\newcommand{\dummyitem}{\item[] \leavevmode\phantom{gg}}
\begin{minipage}[t]{.46\textwidth}
\begin{block}{Shallow}
\begin{itemize}
\item quick and easy to build
\item extensions are simple
\end{itemize}
\end{block}
\end{minipage}\qquad
\begin{minipage}[t]{.46\textwidth}
\begin{block}{Deep}
\begin{itemize}
\item can reason about syntax
\item allows verified implementations
\item sometimes tricky to define
\begin{itemize}
\item \eg bound variables
\end{itemize}
\end{itemize}
\end{block}
\end{minipage}
\bigskip
\begin{block}{Important Questions for Deciding}
\begin{itemize}
\item Do I need to reason about syntax?
\item Do I have hard to define syntax like bound variables?
\item How much time do I have?
\end{itemize}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Example: Embedding of Propositional Logic III}
\begin{itemize}
\item with deep embedding one can easily formalise syntactic properties like
\begin{itemize}
\item Which variables does a propositional formula contain?
\item Is a formula in negation-normal-form (NNF)?
\end{itemize}
\item with shallow embeddings
\begin{itemize}
\item syntactic concepts can't be defined in HOL
\item however, they can be defined in SML
\item no proofs about them possible
\end{itemize}
\end{itemize}
\begin{semiverbatim}\scriptsize
val _ = Define `
(IS_NNF (d_not d_true) = T) \holAnd{} (IS_NNF (d_not (d_var v)) = T) \holAnd{}
(IS_NNF (d_not _) = F) \holAnd{}\medskip
(IS_NNF d_true = T) \holAnd{} (IS_NNF (d_var v) = T) \holAnd{}
(IS_NNF (d_and p1 p2) = (IS_NNF p1 \holAnd{} IS_NNF p2)) \holAnd{}
(IS_NNF (d_or p1 p2) = (IS_NNF p1 \holAnd{} IS_NNF p2)) \holAnd{}
(IS_NNF (d_implies p1 p2) = (IS_NNF p1 \holAnd{} IS_NNF p2))`
\end{semiverbatim}
\end{frame}
\begin{frame}
\frametitle{Verified vs.\ Verifying Program}
\newcommand{\dummyitem}{\item[] \leavevmode\phantom{gg}}
\begin{minipage}[t]{.46\textwidth}
\begin{block}{Verified Programs}
\begin{itemize}
\item are formalised in HOL
\item their properties have been proven once and for all
\item all runs have proven properties
\item are usually less sophisticated, since they need verification
\item is what one wants ideally
\item often require deep embedding
\end{itemize}
\end{block}
\end{minipage}\qquad
\begin{minipage}[t]{.46\textwidth}
\begin{block}{Verifying Programs}
\begin{itemize}
\item are written in meta-language
\item they produce a separate proof for each run
\item only certain that current run has properties
\item allow more flexibility, \eg fancy heuristics
\item good pragmatic solution
\item shallow embedding fine
\end{itemize}
\end{block}
\end{minipage}
\end{frame}
\begin{frame}
\frametitle{Summary Deep vs.\ Shallow Embeddings}
\begin{itemize}
\item deep embeddings require more work
\item they however allow reasoning about syntax
\begin{itemize}
\item induction and case-splits possible
\item a semantic subset can be carved out syntactically
\end{itemize}
\item syntax sometimes hard to define for deep embeddings
\item combinations of deep and shallow embeddings common
\begin{itemize}
\item certain parts are deeply embedded
\item others are embedded shallowly
\end{itemize}
\end{itemize}
\end{frame}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "current"
%%% End:

1208
lectures/13_rewriting.tex Normal file
View File

File diff suppressed because it is too large Load Diff

469
lectures/14_advanced_definitions.tex Normal file
View File

@ -0,0 +1,469 @@
\part{Advanced Definition Principles}
\frame[plain]{\partpage}
\section{Inductive and Coinductive Relations}
\begin{frame}
\frametitle{Relations}
\begin{itemize}
\item a relation is a function from some arguments to \texttt{bool}
\item the following example types are all types of relations:
\begin{itemize}
\item \hol{:\ 'a -> 'a -> bool}
\item \hol{:\ 'a -> 'b -> bool}
\item \hol{:\ 'a -> 'b -> 'c -> 'd -> bool}
\item \hol{:\ ('a \# 'b \# 'c) -> bool}
\item \hol{:\ bool}
\item \hol{:\ 'a -> bool}
\end{itemize}
\item relations are closely related to sets
\begin{itemize}
\item \hol{R a b c <=> (a, b, c) IN \{(a, b, c) | R a b c\}}
\item \hol{(a, b, c) IN S <=> (\textbsl{}a b c.\ (a, b, c) IN S) a b c}
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Relations II}
\begin{itemize}
\item relations are often defined by a set of \emph{rules}
\begin{minipage}{.9\textwidth}
\begin{exampleblock}{Definition of Reflexive-Transitive Closure}
The transitive reflexive closure of a relation \hol{R : 'a -> 'a -> bool} can
be defined as the least relation \hol{RTC R} that satisfies the following rules:
\bigskip
\begin{center}
$\inferrule*{\hol{R x y}}{\hol{RTC R x y}}$\quad
$\inferrule*{\ }{\hol{RTC R x x}}$\quad
$\inferrule*{\hol{RTC R x y}\\\hol{RTC R y z}}{\hol{RTC R x z}}$
\end{center}
\end{exampleblock}
\end{minipage}
\item if the rules are monoton, a least and a greatest fix point exists (Knaster-Tarski theorem)
\item least fixpoints give rise to \emph{inductive relations}
\item greatest fixpoints give rise to \emph{coinductive relations}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{(Co)inductive Relations in HOL}
\begin{itemize}
\item \ml{(Co)IndDefLib} provides infrastructure for defining (co)inductive relations
\item given a set of rules \hol{Hol\_(co)reln} defines (co)inductive relations
\item 3 theorems are returned and stored in current theory
\begin{itemize}
\item a rules theorem --- it states that the defined constant satisfies the rules
\item a cases theorem --- this is an equational form of the rules showing that the defined relation is indeed a fixpoint
\item a (co)induction theorem
\end{itemize}
\item additionally a strong (co)induction theorem is stored in current theory
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Example: Transitive Reflexive Closure}
\begin{semiverbatim}\scriptsize
> \hol{val (RTC_REL_rules, RTC_REL_ind, RTC_REL_cases) = Hol_reln `
(!x y. R x y ==> RTC_REL R x y) \holAnd{}
(!x. RTC_REL R x x) \holAnd{}
(!x y z. RTC_REL R x y \holAnd{} RTC_REL R y z ==> RTC_REL R x z)`}
val RTC_REL_rules = |- !R.
(!x y. R x y ==> RTC_REL R x y) \holAnd{} (!x. RTC_REL R x x) \holAnd{}
(!x y z. RTC_REL R x y \holAnd{} RTC_REL R y z ==> RTC_REL R x z)
val RTC_REL_cases = |- !R a0 a1.
RTC_REL R a0 a1 <=>
(R a0 a1 \holOr{} (a1 = a0) \holOr{} ?y. RTC_REL R a0 y \holAnd{} RTC_REL R y a1)
\end{semiverbatim}
\end{frame}
\begin{frame}[fragile]
\frametitle{Example: Transitive Reflexive Closure II}
\begin{semiverbatim}\scriptsize
val RTC_REL_ind = |- !R RTC_REL'.
((!x y. R x y ==> RTC_REL' x y) \holAnd{} (!x. RTC_REL' x x) \holAnd{}
(!x y z. RTC_REL' x y \holAnd{} RTC_REL' y z ==> RTC_REL' x z)) ==>
(!a0 a1. RTC_REL R a0 a1 ==> RTC_REL' a0 a1)
> \hol{val RTC_REL_strongind = DB.fetch "-" "RTC_REL_strongind"}
val RTC_REL_strongind = |- !R RTC_REL'.
(!x y. R x y ==> RTC_REL' x y) \holAnd{} (!x. RTC_REL' x x) \holAnd{}
(!x y z.
RTC_REL R x y \holAnd{} RTC_REL' x y \holAnd{} RTC_REL R y z \holAnd{}
RTC_REL' y z ==>
RTC_REL' x z) ==>
( !a0 a1. RTC_REL R a0 a1 ==> RTC_REL' a0 a1)
\end{semiverbatim}
\end{frame}
\begin{frame}[fragile]
\frametitle{Example: \hol{EVEN}}
\begin{semiverbatim}\scriptsize
> \hol{val (EVEN_REL_rules, EVEN_REL_ind, EVEN_REL_cases) = Hol_reln
`(EVEN_REL 0) \holAnd{} (!n. EVEN_REL n ==> (EVEN_REL (n + 2)))`};
val EVEN_REL_cases =
|- !a0. EVEN_REL a0 <=> (a0 = 0) \holOr{} ?n. (a0 = n + 2) \holAnd{} EVEN_REL n
val EVEN_REL_rules =
|- EVEN_REL 0 \holAnd{} !n. EVEN_REL n ==> EVEN_REL (n + 2)
val EVEN_REL_ind = |- !EVEN_REL'.
(EVEN_REL' 0 \holAnd{} (!n. EVEN_REL' n ==> EVEN_REL' (n + 2))) ==>
(!a0. EVEN_REL a0 ==> EVEN_REL' a0)
\end{semiverbatim}
\begin{itemize}
\item notice that in this example there is exactly one fixpoint
\item therefore, for these rules the inductive and coinductive relation coincide
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Example: Dummy Relations}
\begin{semiverbatim}\scriptsize
> \hol{val (DF_rules, DF_ind, DF_cases) = Hol_reln
`(!n. DF (n+1) ==> (DF n))`}
> \hol{val (DT_rules, DT_coind, DT_cases) = Hol_coreln
`(!n. DT (n+1) ==> (DT n))`}
val DT_coind =
|- !DT'. (!a0. DT' a0 ==> DT' (a0 + 1)) ==> !a0. DT' a0 ==> DT a0
val DF_ind =
|- !DF'. (!n. DF' (n + 1) ==> DF' n) ==> !a0. DF a0 ==> DF' a0
val DT_cases = |- !a0. DT a0 <=> DT (a0 + 1):
val DF_cases = |- !a0. DF a0 <=> DF (a0 + 1):
\end{semiverbatim}
\begin{itemize}
\item notice that the definitions of \hol{DT} and \hol{DF} look like a non-terminating recursive definition
\item \hol{DT} is always true, \ie \hol{|- !n.\ DT n}
\item \hol{DF} is always false, \ie \hol{|- !n.\ \holNeg{}(DF n)}
\end{itemize}
\end{frame}
\section{Quotient Types}
\begin{frame}
\frametitle{Quotient Types}
\begin{itemize}
\item \ml{quotientLib} allows to define types as quotients of existing types with respect to \emph{partial equivalence relation}
\item each equivalence class becomes a value of the new type
\item partiality allows ignoring certain values of original type
\item \ml{quotientLib} allows to lift definitions and lemmata as well
\item details are technical and won't be presented here
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Quotient Types Example}
\begin{itemize}
\item let's assume we have an implementation of finite sets of numbers as
binary trees with
\begin{itemize}
\item type \hol{binset}
\item binary tree invariant \hol{WF\_BINSET :\ binset -> bool}
\item constant \hol{empty\_binset}
\item add and member functions \hol{add :\ num -> binset -> binset},\\ \hol{mem :\ binset -> num -> bool}
\end{itemize}
\item we can define a partial equivalence relation by\\
\hol{binset\_equiv b1 b2 := (\\
\-\ \ WF\_BINSET b1 \holAnd{} WF\_BINSET b2 \holAnd{}\\
\-\ \ (!n.\ mem b1 n <=> mem b2 n))}
\item this allows defining a quotient type of sets of numbers
\item functions \hol{empty\_binset}, \hol{add} and \hol{mem} as well as lemmata about them can be lifted automatically
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Quotient Types Summary}
\begin{itemize}
\item quotient types are sometimes very useful
\begin{itemize}
\item \eg rational numbers are defined as a quotient type
\end{itemize}
\item there is powerful infrastructure for them
\item many tasks are automated
\item however, the details are technical and won't be discussed here
\end{itemize}
\end{frame}
\section{Case Expressions}
\begin{frame}
\frametitle{Pattern Matching / Case Expressions}
\begin{itemize}
\item pattern matching ubiquitous in functional programming
\item pattern matching is a powerful technique
\item it helps to write concise, readable definitions
\item very handy and frequently used for interactive theorem proving
\item however, it is \alert{not directly supported} by HOL's logic
\item representations in HOL
\begin{itemize}
\item sets of equations as produced by \hol{Define}
\item decision trees (printed as case-expressions)
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{TFL / \texttt{Define}}
\begin{itemize}
\item we have already used top-level pattern matches with the TFL package
\item \hol{Define} is able to handle them
\begin{itemize}
\item all the semantic complexity is taken care of
\item no special syntax or functions remain
\item no special rewrite rules, reasoning tools needed afterwards
\end{itemize}
\item \hol{Define} produces a set of equations
\item this is the recommended way of using pattern matching in HOL
\end{itemize}
\begin{exampleblock}{Example}
\begin{semiverbatim}\scriptsize
> \hol{val ZIP_def = Define `(ZIP (x::xs) (y::ys) = (x,y)::(ZIP xs ys)) \holAnd{}
(ZIP [] [] = [])`}
val ZIP_def = |- (!ys y xs x. ZIP (x::xs) (y::ys) = (x,y)::ZIP xs ys) \holAnd{}
(ZIP [] [] = [])
\end{semiverbatim}
\end{exampleblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Case Expressions}
\begin{itemize}
\item sometimes one does not want to use this compilation by TFL
\begin{itemize}
\item one wants to use pattern-matches somewhere nested in a term
\item one might not want to introduce a new constant
\item one might want to avoid using TFL for technical reasons
\end{itemize}
\item in such situations, case-expressions can be used
\item their syntax is similar to the syntax used by SML
\end{itemize}
\begin{exampleblock}{Example}
\begin{semiverbatim}\scriptsize
> \hol{val ZIP_def = Define `ZIP xs ys = case (xs, ys) of
(x::xs, y::ys) => (x,y)::(ZIP xs ys)
| ([], []) => []`}
val ZIP_def = |- !ys xs. ZIP xs ys =
case (xs,ys) of
([],[]) => []
| ([],v4::v5) => ARB
| (x::xs',[]) => ARB
| (x::xs',y::ys') => (x,y)::ZIP xs' ys'
\end{semiverbatim}
\end{exampleblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Case Expressions II}
\begin{itemize}
\item the datatype package defines case-constants for each datatype
\item the parser contains a pattern compilation algorithm
\item case-expressions are by the parser compiled to decision trees using case-constants
\item pretty printer prints these decision trees as case-expressions again
\end{itemize}
\begin{exampleblock}{Example}
\begin{semiverbatim}\scriptsize
val ZIP_def = |- !ys xs. ZIP xs ys =
pair_CASE (xs,ys)
(\textbsl{}v v1.
list_CASE v (list_CASE v1 [] (\textbsl{}v4 v5. ARB))
(\textbsl{}x xs'. list_CASE v1 ARB (\textbsl{}y ys'. (x,y)::ZIP xs' ys'))):
\end{semiverbatim}
\end{exampleblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Case Expression Issues}
\begin{itemize}
\item using case expressions feels very natural to functional programmers
\item case-expressions allow concise, well-readable definitions
\item however, there are also many drawbacks
\item there is large, complicated code in the parser and pretty printer
\begin{itemize}
\item this is outside the kernel
\item parsing a pretty-printed term can result in a non $\alpha$-equivalent one
\item there are bugs in this code (see \eg Issue \#416 reported 8 May 2017)
\end{itemize}
\item the results are hard to predict
\begin{itemize}
\item heuristics involved in creating decision tree
\item however, it is beneficial that proofs follow this internal, volatile structure
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Case Expression Issues II}
\begin{itemize}
\item technical issues
\begin{itemize}
\item it is tricky to reason about decision trees
\item rewrite rules about case-constants needs to be fetched from \hol{TypeBase}
\begin{itemize}
\item alternative \hol{srw\_ss} often does more than wanted
\end{itemize}
\item partially evaluated decision-trees are not pretty printed nicely any more
\end{itemize}
\item underspecified functions
\begin{itemize}
\item decision trees are exhaustive
\item they list underspecified cases explicitly with value \hol{ARB}
\item this can be lengthy
\item \hol{Define} in contrast hides underspecified cases
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Case Expression Example I}
\begin{block}{Partial Proof Script}
\begin{semiverbatim}\scriptsize
val _ = prove (``!l1 l2.
(LENGTH l1 = LENGTH l2) ==>
((ZIP l1 l2 = []) <=> ((l1 = []) \holAnd{} (l2 = [])))``,
ONCE_REWRITE_TAC [ZIP_def]
\end{semiverbatim}
\end{block}
\begin{block}{Current Goal}
\begin{semiverbatim}\scriptsize
!l1 l2.
(LENGTH l1 = LENGTH l2) ==>
(((case (l1,l2) of
([],[]) => []
| ([],v4::v5) => ARB
| (x::xs',[]) => ARB
| (x::xs',y::ys') => (x,y)::ZIP xs' ys') =
[]) <=> (l1 = []) \holAnd{} (l2 = []))
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Case Expression Example IIa -- partial evaluation}
\begin{block}{Partial Proof Script}
\begin{semiverbatim}\scriptsize
val _ = prove (``!l1 l2.
(LENGTH l1 = LENGTH l2) ==>
((ZIP l1 l2 = []) <=> ((l1 = []) \holAnd{} (l2 = [])))``,
ONCE_REWRITE_TAC [ZIP_def] >>
REWRITE_TAC[pairTheory.pair_case_def] >> BETA_TAC
\end{semiverbatim}
\end{block}
\begin{block}{Current Goal}
\begin{semiverbatim}\scriptsize
!l1 l2.
(LENGTH l1 = LENGTH l2) ==>
(((case l1 of
[] => (case l2 of [] => [] | v4::v5 => ARB)
| x::xs' => case l2 of [] => ARB | y::ys' => (x,y)::ZIP xs' ys') =
[]) <=> (l1 = []) \holAnd{} (l2 = []))
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Case Expression Example IIb --- following tree structure}
\begin{block}{Partial Proof Script}
\begin{semiverbatim}\scriptsize
val _ = prove (``!l1 l2.
(LENGTH l1 = LENGTH l2) ==>
((ZIP l1 l2 = []) <=> ((l1 = []) \holAnd{} (l2 = [])))``,
ONCE_REWRITE_TAC [ZIP_def] >>
Cases_on `l1` >| [
REWRITE_TAC[listTheory.list_case_def]
\end{semiverbatim}
\end{block}
\begin{block}{Current Goal}
\begin{semiverbatim}\scriptsize
!l2.
(LENGTH [] = LENGTH l2) ==>
(((case ([],l2) of
([],[]) => []
| ([],v4::v5) => ARB
| (x::xs',[]) => ARB
| (x::xs',y::ys') => (x,y)::ZIP xs' ys') =
[]) <=> (l2 = []))
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Case Expression Summary}
\begin{itemize}
\item case expressions are natural to functional programmers
\item they allow concise, readable definitions
\item however, fancy parser and pretty-printer needed
\begin{itemize}
\item trustworthiness issues
\item sanity check lemmata advisable
\end{itemize}
\item reasoning about case expressions can be tricky and lengthy
\item proofs about case expression often hard to maintain
\item therefore, use top-level pattern matching via \hol{Define} if easily possible
\end{itemize}
\end{frame}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "current"
%%% End:

472
lectures/14a_final_project.tex Normal file
View File

@ -0,0 +1,472 @@
\part{Advanced Definition Principles}
\frame[plain]{\partpage}
\section{Inductive and Coinductive Relations}
\begin{frame}
\frametitle{Relations}
\begin{itemize}
\item a relation is a function from some arguments to \texttt{bool}
\item the following example types are all types of relations:
\begin{itemize}
\item \hol{:\ 'a -> 'a -> bool}
\item \hol{:\ 'a -> 'b -> bool}
\item \hol{:\ 'a -> 'b -> 'c -> 'd -> bool}
\item \hol{:\ ('a \# 'b \# 'c) -> bool}
\item \hol{:\ bool}
\item \hol{:\ 'a -> bool}
\end{itemize}
\item relations are closely related to sets
\begin{itemize}
\item \hol{R a b c <=> (a, b, c) IN \{(a, b, c) | R a b c\}}
\item \hol{(a, b, c) IN S <=> (\textbsl{}a b c.\ (a, b, c) IN S) a b c}
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Relations II}
\begin{itemize}
\item relations are often defined by a set of \emph{rules}
\begin{minipage}{.9\textwidth}
\begin{exampleblock}{Definition of Reflexive-Transitive Closure}
The transitive reflexive closure of a relation \hol{R : 'a -> 'a -> bool} can
be defined as the least relation \hol{RTC R} that satisfies the following rules:
\bigskip
\begin{center}
$\inferrule*{\hol{R x y}}{\hol{RTC R x y}}$\quad
$\inferrule*{\ }{\hol{RTC R x x}}$\quad
$\inferrule*{\hol{RTC R x y}\\\hol{RTC R y z}}{\hol{RTC R x z}}$
\end{center}
\end{exampleblock}
\end{minipage}
\item if the rules are monoton, a least and a greatest fix point exists (Knaster-Tarski theorem)
\item least fixpoints give rise to \emph{inductive relations}
\item greatest fixpoints give rise to \emph{coinductive relations}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{(Co)inductive Relations in HOL}
\begin{itemize}
\item \ml{(Co)IndDefLib} provides infrastructure for defining (co)inductive relations
\item given a set of rules \hol{Hol\_(co)reln} defines (co)inductive relations
\item 3 theorems are returned and stored in current theory
\begin{itemize}
\item a rules theorem --- it states that the defined constant satisfies the rules
\item a cases theorem --- this is an equational form of the rules showing that the defined relation is indeed a fixpoint
\item a (co)induction theorem
\end{itemize}
\item additionally a strong (co)induction theorem is stored in current theory
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Example: Transitive Reflexive Closure}
\begin{semiverbatim}\scriptsize
> \hol{val (RTC_REL_rules, RTC_REL_ind, RTC_REL_cases) = Hol_reln `
(!x y. R x y ==> RTC_REL R x y) \holAnd{}
(!x. RTC_REL R x x) \holAnd{}
(!x y z. RTC_REL R x y \holAnd{} RTC_REL R x z ==> RTC_REL R x z)`}
val RTC_REL_rules = |- !R.
(!x y. R x y ==> RTC_REL R x y) \holAnd{} (!x. RTC_REL R x x) \holAnd{}
(!x y z. RTC_REL R x y \holAnd{} RTC_REL R x z ==> RTC_REL R x z)
val RTC_REL_cases = |- !R a0 a1.
RTC_REL R a0 a1 <=>
(R a0 a1 \holOr{} (a1 = a0) \holOr{} ?y. RTC_REL R a0 y \holAnd{} RTC_REL R a0 a1)
\end{semiverbatim}
\end{frame}
\begin{frame}[fragile]
\frametitle{Example: Transitive Reflexive Closure II}
\begin{semiverbatim}\scriptsize
val RTC_REL_ind = |- !R RTC_REL'.
((!x y. R x y ==> RTC_REL' x y) \holAnd{} (!x. RTC_REL' x x) \holAnd{}
(!x y z. RTC_REL' x y \holAnd{} RTC_REL' x z ==> RTC_REL' x z)) ==>
(!a0 a1. RTC_REL R a0 a1 ==> RTC_REL' a0 a1)
> \hol{val RTC_REL_strongind = DB.fetch "-" "RTC_REL_strongind"}
val RTC_REL_strongind = |- !R RTC_REL'.
(!x y. R x y ==> RTC_REL' x y) \holAnd{} (!x. RTC_REL' x x) \holAnd{}
(!x y z.
RTC_REL R x y \holAnd{} RTC_REL' x y \holAnd{} RTC_REL R x z \holAnd{}
RTC_REL' x z ==>
RTC_REL' x z) ==>
( !a0 a1. RTC_REL R a0 a1 ==> RTC_REL' a0 a1)
\end{semiverbatim}
\end{frame}
\begin{frame}[fragile]
\frametitle{Example: \hol{EVEN}}
\begin{semiverbatim}\scriptsize
> \hol{val (EVEN_REL_rules, EVEN_REL_ind, EVEN_REL_cases) = Hol_reln
`(EVEN_REL 0) \holAnd{} (!n. EVEN_REL n ==> (EVEN_REL (n + 2)))`};
val EVEN_REL_cases =
|- !a0. EVEN_REL a0 <=> (a0 = 0) \holOr{} ?n. (a0 = n + 2) \holAnd{} EVEN_REL n
val EVEN_REL_rules =
|- EVEN_REL 0 \holAnd{} !n. EVEN_REL n ==> EVEN_REL (n + 2)
val EVEN_REL_ind = |- !EVEN_REL'.
(!a0.
EVEN_REL' a0 ==>
(a0 = 0) \holOr{} ?n. (a0 = n + 2) \holAnd{} EVEN_REL' n) ==>
(!a0. EVEN_REL' a0 ==> EVEN_REL a0)
\end{semiverbatim}
\begin{itemize}
\item notice that in this example there is exactly one fixpoint
\item therefore for these rule, the induction and coinductive relation coincide
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Example: Dummy Relations}
\begin{semiverbatim}\scriptsize
> \hol{val (DF_rules, DF_ind, DF_cases) = Hol_reln
`(!n. DF (n+1) ==> (DF n))`}
> \hol{val (DT_rules, DT_coind, DT_cases) = Hol_coreln
`(!n. DT (n+1) ==> (DT n))`}
val DT_coind =
|- !DT'. (!a0. DT' a0 ==> DT' (a0 + 1)) ==> !a0. DT' a0 ==> DT a0
val DF_ind =
|- !DF'. (!n. DF' (n + 1) ==> DF' n) ==> !a0. DF a0 ==> DF' a0
val DT_cases = |- !a0. DT a0 <=> DT (a0 + 1):
val DF_cases = |- !a0. DF a0 <=> DF (a0 + 1):
\end{semiverbatim}
\begin{itemize}
\item notice that for both \hol{DT} and \hol{DF} we used essentially a non-terminating recursion
\item \hol{DT} is always true, \ie \hol{|- !n.\ DT n}
\item \hol{DF} is always false, \ie \hol{|- !n.\ \holNeg{}(DF n)}
\end{itemize}
\end{frame}
\section{Quotient Types}
\begin{frame}
\frametitle{Quotient Types}
\begin{itemize}
\item \ml{quotientLib} allows to define types as quotients of existing types with respect to \emph{partial equivalence relation}
\item each equivalence class becomes a value of the new type
\item partiality allows ignoring certain types
\item \ml{quotientLib} allows to lift definitions and lemmata as well
\item details are technical and won't be presented here
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Quotient Types Example}
\begin{itemize}
\item let's assume we have an implementation of finite sets of numbers as
binary trees with
\begin{itemize}
\item type \hol{binset}
\item binary tree invariant \hol{WF\_BINSET :\ binset -> bool}
\item constant \hol{empty\_binset}
\item add and member functions \hol{add :\ num -> binset -> binset},\\ \hol{mem :\ binset -> num -> bool}
\end{itemize}
\item we can define a partial equivalence relation by\\
\hol{binset\_equiv b1 b2 := (\\
\-\ \ WF\_BINSET b1 \holAnd{} WF\_BINSET b2 \holAnd{}\\
\-\ \ (!n.\ mem b1 n <=> mem b2 n))}
\item this allows defining a quotient type of sets of numbers
\item functions \hol{empty\_binset}, \hol{add} and \hol{mem} as well as lemmata about them can be lifted automatically
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Quotient Types Summary}
\begin{itemize}
\item quotient types are sometimes very useful
\begin{itemize}
\item \eg rational numbers are defined as a quotient type
\end{itemize}
\item there is powerful infrastructure for them
\item many tasks are automated
\item however, the details are technical and won't be discussed here
\end{itemize}
\end{frame}
\section{Case Expressions}
\begin{frame}
\frametitle{Pattern Matching / Case Expressions}
\begin{itemize}
\item pattern matching ubiquitous in functional programming
\item pattern matching is a powerful technique
\item it helps to write concise, readable definitions
\item very handy and frequently used for interactive theorem proving in higher-order logic (HOL)
\item however, it is \alert{not directly supported} by HOL's logic
\item representations in HOL
\begin{itemize}
\item sets of equations as produced by \hol{Define}
\item decision trees (printed as case-expressions)
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{TFL / \texttt{Define}}
\begin{itemize}
\item we have already used top-level pattern matches with the TFL package
\item \hol{Define} is able to handle them
\begin{itemize}
\item all the semantic complexity is taken care of
\item no special syntax or functions remain
\item no special rewrite rules, reasoning tools needed afterwards
\end{itemize}
\item \hol{Define} produces a set of equations
\item this is the recommended way of using pattern matching in HOL
\end{itemize}
\begin{exampleblock}{Example}
\begin{semiverbatim}\scriptsize
> \hol{val ZIP_def = Define `(ZIP (x::xs) (y::ys) = (x,y)::(ZIP xs ys)) \holAnd{}
(ZIP [] [] = [])`}
val ZIP_def = |- (!ys y xs x. ZIP (x::xs) (y::ys) = (x,y)::ZIP xs ys) \holAnd{}
(ZIP [] [] = [])
\end{semiverbatim}
\end{exampleblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Case Expressions}
\begin{itemize}
\item sometimes one does not want to use this compilation by TFL
\begin{itemize}
\item one wants to use pattern-matches somewhere nested in a term
\item one might not want to introduce a new constant
\item one might want to avoid using TFL for technical reasons
\end{itemize}
\item in such situations, case-expressions can be used
\item their syntax is similar to the syntax used by SML
\end{itemize}
\begin{exampleblock}{Example}
\begin{semiverbatim}\scriptsize
> \hol{val ZIP_def = Define `ZIP xs ys = case (xs, ys) of
(x::xs, y::ys) => (x,y)::(ZIP xs ys)
| ([], []) => []`}
val ZIP_def = |- !ys xs. ZIP xs ys =
case (xs,ys) of
([],[]) => []
| ([],v4::v5) => ARB
| (x::xs',[]) => ARB
| (x::xs',y::ys') => (x,y)::ZIP xs' ys'
\end{semiverbatim}
\end{exampleblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Case Expressions II}
\begin{itemize}
\item the datatype package define case-constants for each datatype
\item the parser contains a pattern compilation algorithm
\item case-expressions are by the parser compiled to decision trees using case-constants
\item pretty printer prints these decision trees as case-expressions again
\end{itemize}
\begin{exampleblock}{Example}
\begin{semiverbatim}\scriptsize
val ZIP_def = |- !ys xs. ZIP xs ys =
pair_CASE (xs,ys)
(\textbsl{}v v1.
list_CASE v (list_CASE v1 [] (\textbsl{}v4 v5. ARB))
(\textbsl{}x xs'. list_CASE v1 ARB (\textbsl{}y ys'. (x,y)::ZIP xs' ys'))):
\end{semiverbatim}
\end{exampleblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Case Expression Issues}
\begin{itemize}
\item using case expressions feels very natural to functional programmers
\item case-expressions allow concise, well-readable definitions
\item however, there are also many drawbacks
\item there is large, complicated code in the parser and pretty printer
\begin{itemize}
\item this is outside the kernel
\item parsing a pretty-printed term can result in a non $\alpha$-equivalent one
\item there are bugs in this code (see \eg Issue \#416 reported 8 May 2017)
\end{itemize}
\item the results are hard to predict
\begin{itemize}
\item heuristics involved in creating decision tree
\item results sometimes hard to predict
\item however, it is beneficial that proofs follow this internal, volatile structure
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Case Expression Issues II}
\begin{itemize}
\item technical issues
\begin{itemize}
\item it is tricky to reason about decision trees
\item rewrite rules about case-constants needs to be fetched from \hol{TypeBase}
\begin{itemize}
\item alternative \hol{srw\_ss} often does more than wanted
\end{itemize}
\item partially evaluated decision-trees are not pretty printed nicely any more
\end{itemize}
\item underspecified functions
\begin{itemize}
\item decision trees are exhaustive
\item they list underspecified cases explicitly with value \hol{ARB}
\item this can be lengthy
\item \hol{Define} in contrast hides underspecified cases
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Case Expression Example I}
\begin{block}{Partial Proof Script}
\begin{semiverbatim}\scriptsize
val _ = prove (``!l1 l2.
(LENGTH l1 = LENGTH l2) ==>
((ZIP l1 l2 = []) <=> ((l1 = []) \holAnd{} (l2 = [])))``,
ONCE_REWRITE_TAC [ZIP_def]
\end{semiverbatim}
\end{block}
\begin{block}{Current Goal}
\begin{semiverbatim}\scriptsize
!l1 l2.
(LENGTH l1 = LENGTH l2) ==>
(((case (l1,l2) of
([],[]) => []
| ([],v4::v5) => ARB
| (x::xs',[]) => ARB
| (x::xs',y::ys') => (x,y)::ZIP xs' ys') =
[]) <=> (l1 = []) \holAnd{} (l2 = []))
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Case Expression Example IIa -- partial evaluation}
\begin{block}{Partial Proof Script}
\begin{semiverbatim}\scriptsize
val _ = prove (``!l1 l2.
(LENGTH l1 = LENGTH l2) ==>
((ZIP l1 l2 = []) <=> ((l1 = []) \holAnd{} (l2 = [])))``,
ONCE_REWRITE_TAC [ZIP_def] >>
REWRITE_TAC[pairTheory.pair_case_def] >> BETA_TAC
\end{semiverbatim}
\end{block}
\begin{block}{Current Goal}
\begin{semiverbatim}\scriptsize
!l1 l2.
(LENGTH l1 = LENGTH l2) ==>
(((case l1 of
[] => (case l2 of [] => [] | v4::v5 => ARB)
| x::xs' => case l2 of [] => ARB | y::ys' => (x,y)::ZIP xs' ys') =
[]) <=> (l1 = []) \holAnd{} (l2 = []))
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Case Expression Example IIb --- following tree structure}
\begin{block}{Partial Proof Script}
\begin{semiverbatim}\scriptsize
val _ = prove (``!l1 l2.
(LENGTH l1 = LENGTH l2) ==>
((ZIP l1 l2 = []) <=> ((l1 = []) \holAnd{} (l2 = [])))``,
ONCE_REWRITE_TAC [ZIP_def] >>
Cases_on `l1` >| [
REWRITE_TAC[listTheory.list_case_def]
\end{semiverbatim}
\end{block}
\begin{block}{Current Goal}
\begin{semiverbatim}\scriptsize
!l2.
(LENGTH [] = LENGTH l2) ==>
(((case ([],l2) of
([],[]) => []
| ([],v4::v5) => ARB
| (x::xs',[]) => ARB
| (x::xs',y::ys') => (x,y)::ZIP xs' ys') =
[]) <=> (l2 = []))
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Case Expression Summary}
\begin{itemize}
\item case expressions are natural to functional programmers
\item they allow concise, readable definitions
\item however, fancy parser and pretty-printer needed
\begin{itemize}
\item trustworthiness issues
\item sanity check lemmata advisable
\end{itemize}
\item reasoning about case expressions can be tricky and lengthy
\item proofs about case expression often hard to maintain
\item therefore, use top-level pattern matching via \hol{Define} if easily possible
\end{itemize}
\end{frame}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "current"
%%% End:

543
lectures/15_maintainable_proofs.tex Normal file
View File

@ -0,0 +1,543 @@
\part{Maintainable Proofs}
\frame[plain]{\partpage}
\begin{frame}
\frametitle{Motivation}
\begin{itemize}
\item proofs are hopefully still used in a few weeks, months or even years
\item often the environment changes slightly during the lifetime of a proof
\begin{itemize}
\item your definitions change slightly
\item your own lemmata change (\eg become more general)
\item used libraries change
\item HOL changes
\begin{itemize}
\item automation becomes more powerful
\item rewrite rules in certain simpsets change
\item definition packages produce slightly different theorems
\item autogenerated variable-names change
\item \ldots
\end{itemize}
\end{itemize}
\item even if HOL and used libraries are stable, proofs often go through several iterations
\item often they are adapted by someone else than the original author
\item \alert{therefore it is important that proofs are easily maintainable}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Nice Properties of Proofs}
\begin{itemize}
\item maintainability is closely linked to other desirable properties of proofs
\item proofs should be
\begin{itemize}
\item easily understandable
\item well-structured
\item robust
\begin{itemize}
\item they should be able to cope with minor changes to environment
\item if they fail they should do so at sensible points
\end{itemize}
\item reusable
\end{itemize}
\item How can one write proofs with such properties?
\item as usual, there are no easy answers but plenty of good advice
\item I recommend following the advice of \emph{ProofStyle} manual
\item parts of this advice as well as a few extra points are discussed in the following
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Formatting}
\begin{itemize}
\item format your proof such that it easily understandable
\item make the structure of the proof very clear
\item \alert{show clearly where subgoals start and stop}
\item use indentation to mark proofs of subgoals
\item use empty lines to separate large proofs of subgoals
\item use comments where appropriate
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Formatting Example I}
\begin{alertblock}{Bad Example Term Formatting}
\begin{semiverbatim}\scriptsize
prove (``!l1 l2. l1 <> [] ==> LENGTH l2 <
LENGTH (l1 ++ l2)``,
...)
\end{semiverbatim}
\end{alertblock}
\begin{exampleblock}{Good Example Term Formatting}
\begin{semiverbatim}\scriptsize
prove (``!l1 l2. l1 <> [] ==>
(LENGTH l2 < LENGTH (l1 ++ l2))``,
...)
\end{semiverbatim}
\end{exampleblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Formatting Example II}
\begin{alertblock}{Bad Example Subgoals}
\begin{semiverbatim}\scriptsize
prove (``!l1 l2. l1 <> [] ==> (LENGTH l2 < LENGTH (l1 ++ l2))``,
Cases >>
REWRITE_TAC[] >>
REWRITE_TAC[listTheory.LENGTH, listTheory.LENGTH_APPEND] >>
REPEAT STRIP_TAC >>
DECIDE_TAC)
\end{semiverbatim}
\end{alertblock}
\begin{alertblock}{Improved Example Subgoals}
At least show when a subgoal starts and ends
\begin{semiverbatim}\scriptsize
prove (``!l1 l2. l1 <> [] ==> (LENGTH l2 < LENGTH (l1 ++ l2))``,
Cases >> (
REWRITE_TAC[]
) >>
REWRITE_TAC[listTheory.LENGTH, listTheory.LENGTH_APPEND] >>
REPEAT STRIP_TAC >>
DECIDE_TAC)
\end{semiverbatim}
\end{alertblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Formatting Example II 2}
\begin{exampleblock}{Good Example Subgoals}
Make sure \texttt{REWRITE\_TAC} is only applied to first subgoal and
proof fails, if it does not solve this subgoal.
\begin{semiverbatim}\scriptsize
prove (``!l1 l2. l1 <> [] ==> (LENGTH l2 < LENGTH (l1 ++ l2))``,
Cases >- (
REWRITE_TAC[]
) >>
REWRITE_TAC[listTheory.LENGTH, listTheory.LENGTH_APPEND] >>
REPEAT STRIP_TAC >>
DECIDE_TAC)
\end{semiverbatim}
\end{exampleblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Formatting Example II 3}
\begin{exampleblock}{Alternative Good Example Subgoals}
Alternative good formatting using \texttt{THENL}
\begin{semiverbatim}\scriptsize
prove (``!l1 l2. l1 <> [] ==> (LENGTH l2 < LENGTH (l1 ++ l2))``,
Cases >| [
REWRITE_TAC[],
REWRITE_TAC[listTheory.LENGTH, listTheory.LENGTH_APPEND] >>
REPEAT STRIP_TAC >>
DECIDE_TAC
])
\end{semiverbatim}
\end{exampleblock}
\begin{alertblock}{Another Bad Example Subgoals}
Bad formatting using \texttt{THENL}
\begin{semiverbatim}\scriptsize
prove (``!l1 l2. l1 <> [] ==> (LENGTH l2 < LENGTH (l1 ++ l2))``,
Cases >| [REWRITE_TAC[],
REWRITE_TAC[listTheory.LENGTH, listTheory.LENGTH_APPEND] >>
REPEAT STRIP_TAC >> DECIDE_TAC])
\end{semiverbatim}
\end{alertblock}
\end{frame}
\begin{frame}
\frametitle{Some basic advice}
\begin{itemize}
\item use semicoli after each declaration
\begin{itemize}
\item if exception is raised during interactive processing (\eg by a failing proof), previous successful declarations are kept
\item it sometimes leads to better error messages in case of parsing errors
\end{itemize}
\item use plenty of parentheses to make structure very clear
\item don't ignore parser warnings
\begin{itemize}
\item especially warnings about multiple possible parse trees are likely to lead to unstable proofs
\item understand why such warnings occur and make sure there is no problem
\end{itemize}
\item format your development well
\begin{itemize}
\item use indentation
\item use linebreaks at sensible points
\item don't use overlong lines
\item \ldots
\end{itemize}
\item don't use \ml{open} in middle of files
\item personal opinion: avoid unicode in source files
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{KISS and Premature Optimisation}
\begin{itemize}
\item follow standard design principles
\begin{itemize}
\item \emph{KISS} principle
\item ``\emph{premature optimization is the root of all evil}'' (Donald Knuth)
\end{itemize}
\item don't try to be overly clever
\item simple proofs are preferable
\item proof-checking-speed mostly unimportant
\item conciseness not a value in itself but desirable if it helps
\begin{itemize}
\item readability
\item maintainability
\end{itemize}
\item abstraction is often desirable, but also has a price
\begin{itemize}
\item don't use too complex, artificial definitions and lemmata
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Too much abstraction}
\begin{alertblock}{Too much abstraction Example}
\begin{semiverbatim}\scriptsize
val TOO_ABSTRACT_LEMMA = prove (``
!(size :'a -> num) (P : 'a -> bool) (combine : 'a -> 'a -> 'a).
(!x. P x ==> (0 < size x)) \holAnd{}
(!x1 x2. size x1 + size x2 <= size (combine x1 x2)) ==>
(!x1 x2. P x1 ==> (size x2 < size (combine x1 x2)))``,
...)
prove (``!l1 l2. l1 <> [] ==> (LENGTH l2 < LENGTH (l1 ++ l2))``,
\textrm{some proof using} ABSTRACT_LEMMA
)
\end{semiverbatim}
\end{alertblock}
\end{frame}
\begin{frame}
\frametitle{Too clever tactics}
\begin{itemize}
\item a common mistake is to use too clever tactics
\begin{itemize}
\item intended to work on many (sub)goals
\item using \hol{TRY} and other fancy trial and error mechanisms
\item intended to replace multiple simple, clear tactics
\end{itemize}
\item typical case: a tactic containing \hol{TRY} applied to many subgoals
\item it is often hard to see why such tactics work
\item if something goes wrong, they are hard to debug
\item general advice: don't factor with tactics, instead use definitions and lemmata
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Too Clever Tactics Example I}
\begin{alertblock}{Bad Example Subgoals}
\begin{semiverbatim}\scriptsize
prove (``!l1 l2. l1 <> [] ==> (LENGTH l2 < LENGTH (l1 ++ l2))``,
Cases >> (
REWRITE_TAC[listTheory.LENGTH, listTheory.LENGTH_APPEND] >>
REPEAT STRIP_TAC >>
DECIDE_TAC
))
\end{semiverbatim}
\end{alertblock}
\begin{exampleblock}{Alternative Good Example Subgoals II}
\begin{semiverbatim}\scriptsize
prove (``!l1 l2. l1 <> [] ==> (LENGTH l2 < LENGTH (l1 ++ l2))``,
Cases >> SIMP_TAC list_ss [])
prove (``!l1 l2. l1 <> [] ==> (LENGTH l2 < LENGTH (l1 ++ l2))``,
Cases >| [
REWRITE_TAC[],
REWRITE_TAC[listTheory.LENGTH, listTheory.LENGTH_APPEND] >>
REPEAT STRIP_TAC >>
DECIDE_TAC
])
\end{semiverbatim}
\end{exampleblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Too Clever Tactics Example II}
\begin{alertblock}{Bad Example}
\begin{semiverbatim}\scriptsize
val oadd_def = Define `(oadd (SOME n1) (SOME n2) = (SOME (n1 + n2))) \holAnd{}
(oadd _ _ = NONE)`;
val osub_def = Define `(osub (SOME n1) (SOME n2) = (SOME (n1 - n2))) \holAnd{}
(osub _ _ = NONE)`;
val omul_def = Define `(omul (SOME n1) (SOME n2) = (SOME (n1 * n2))) \holAnd{}
(omul _ _ = NONE)`;
val obin_NONE_TAC =
Cases_on `o1` >> Cases_on `o2` >>
SIMP_TAC std_ss [oadd_def, osub_def, omul_def];
val oadd_NONE = prove (
``!o1 o2. (oadd o1 o2 = NONE) <=> (o1 = NONE) \holOr{} (o2 = NONE)``,
obin_NONE_TAC);
val osub_NONE = prove (
``!o1 o2. (osub o1 o2 = NONE) <=> (o1 = NONE) \holOr{} (o2 = NONE)``,
obin_NONE_TAC);
val omul_NONE = prove (
``!o1 o2. (omul o1 o2 = NONE) <=> (o1 = NONE) \holOr{} (o2 = NONE)``,
obin_NONE_TAC);
\end{semiverbatim}
\end{alertblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Too Clever Tactics Example II}
\begin{exampleblock}{Good Example}
\begin{semiverbatim}\scriptsize
val obin_def = Define `(obin op (SOME n1) (SOME n2) = (SOME (op n1 n2))) \holAnd{}
(obin _ _ _ = NONE)`;
val oadd_def = Define `oadd = obin \$+`;
val osub_def = Define `osub = obin \$-`;
val omul_def = Define `omul = obin \$*`;
val obin_NONE = prove (
``!op o1 o2. (obin op o1 o2 = NONE) <=> (o1 = NONE) \holOr{} (o2 = NONE)``,
Cases_on `o1` >> Cases_on `o2` >> SIMP_TAC std_ss [obin_def]);
val oadd_NONE = prove (
``!o1 o2. (oadd o1 o2 = NONE) <=> (o1 = NONE) \holOr{} (o2 = NONE)``,
REWRITE_TAC[oadd_def, obin_NONE]);
val osub_NONE = prove (
``!o1 o2. (osub o1 o2 = NONE) <=> (o1 = NONE) \holOr{} (o2 = NONE)``,
REWRITE_TAC[osub_def, obin_NONE]);
val omul_NONE = prove (
``!o1 o2. (omul o1 o2 = NONE) <=> (o1 = NONE) \holOr{} (o2 = NONE)``,
REWRITE_TAC[omul_def, obin_NONE]);
\end{semiverbatim}
\end{exampleblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Use many subgoals and lemmata}
\begin{itemize}
\item often it is beneficial to use subgoals
\begin{itemize}
\item they structure long proofs well
\item they help keeping the proof state clean
\item they mark clearly what one tries to proof
\item they provide points where proofs can break sensibly
\end{itemize}
\item general enough subgoals should become lemmata
\begin{itemize}
\item this improves reusability
\item proof script for main lemma becomes shorter
\item proofs are disentangled
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Subgoal Example}
\begin{itemize}
\item the following example is taken from exercise 5
\item we try to prove \hol{\texttt{!l.\ IS\_WEAK\_SUBLIST\_FILTER l l}}
\item given are following definitions and lemmata
\end{itemize}
\begin{block}{}
\begin{semiverbatim}\scriptsize
val FILTER_BY_BOOLS_def = Define `
FILTER_BY_BOOLS bl l = MAP SND (FILTER FST (ZIP (bl, l)))`;
val IS_WEAK_SUBLIST_FILTER_def = Define `IS_WEAK_SUBLIST_FILTER l1 l2 =
?(bl : bool list). (LENGTH bl = LENGTH l1) \holAnd{} (l2 = FILTER_BY_BOOLS bl l1)`;
val FILTER_BY_BOOLS_REWRITES = store_thm ("FILTER_BY_BOOLS_REWRITES",
``(FILTER_BY_BOOLS [] [] = []) \holAnd{}
(!b bl x xs. (FILTER_BY_BOOLS (b::bl) (x::xs) =
if b then x::(FILTER_BY_BOOLS bl xs) else FILTER_BY_BOOLS bl xs))``,
REWRITE_TAC [FILTER_BY_BOOLS_def, ZIP, MAP, FILTER] >>
Cases_on `b` >> REWRITE_TAC [MAP]);
\end{semiverbatim}
\end{block}
\end{frame}
\begin{frame}[fragile]
\frametitle{Subgoal Example II}
\begin{alertblock}{First Version}
\begin{semiverbatim}\scriptsize
val IS_WEAK_SUBLIST_FILTER_REFL = store_thm ("IS_WEAK_SUBLIST_FILTER_REFL",
``!l. IS_WEAK_SUBLIST_FILTER l l``,
REWRITE_TAC[IS_WEAK_SUBLIST_FILTER_def] >>
Induct_on `l` >- (
Q.EXISTS_TAC `[]` >>
SIMP_TAC list_ss [FILTER_BY_BOOLS_REWRITES]
) >>
FULL_SIMP_TAC std_ss [] >>
GEN_TAC >>
Q.EXISTS_TAC `T::bl` >>
ASM_SIMP_TAC list_ss [FILTER_BY_BOOLS_REWRITES])
\end{semiverbatim}
\end{alertblock}
\begin{itemize}
\item the proof mixes properties of \texttt{IS\_WEAK\_SUBLIST\_FILTER} and
properties of \texttt{FILTER\_BY\_BOOLS}
\item it is hard to see what the main idea is
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Subgoal Example III}
\begin{itemize}
\item the following proof separates the property of \texttt{FILTER\_BY\_BOOLS} as a subgoal
\item the main idea becomes clearer
\end{itemize}
\begin{exampleblock}{Subgoal Version}
\begin{semiverbatim}\scriptsize
val IS_WEAK_SUBLIST_FILTER_REFL = store_thm ("IS_WEAK_SUBLIST_FILTER_REFL",
``!l. IS_WEAK_SUBLIST_FILTER l l``,
GEN_TAC >>
REWRITE_TAC[IS_WEAK_SUBLIST_FILTER_def] >>
`FILTER_BY_BOOLS (REPLICATE (LENGTH l) T) l = l` suffices_by (
METIS_TAC[LENGTH_REPLICATE]
) >>
Induct_on `l` >> (
ASM_SIMP_TAC list_ss [FILTER_BY_BOOLS_REWRITES, REPLICATE]
))
\end{semiverbatim}
\end{exampleblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Subgoal Example IV}
\begin{itemize}
\item the subgoal is general enough to justify a lemma
\item the structure becomes even cleaner
\item this improves reusability
\end{itemize}
\begin{exampleblock}{Lemma Version}
\begin{semiverbatim}\scriptsize
val FILTER_BY_BOOLS_REPL_T = store_thm ("FILTER_BY_BOOLS_REPL_T",
``!l. FILTER_BY_BOOLS (REPLICATE (LENGTH l) T) l = l``,
Induct >> ASM_REWRITE_TAC [REPLICATE, FILTER_BY_BOOLS_REWRITES, LENGTH]);
val IS_WEAK_SUBLIST_FILTER_REFL = store_thm ("IS_WEAK_SUBLIST_FILTER_REFL",
``!l. IS_WEAK_SUBLIST_FILTER l l``,
GEN_TAC >>
REWRITE_TAC[IS_WEAK_SUBLIST_FILTER_def] >>
Q.EXISTS_TAC `REPLICATE (LENGTH l) T` >>
SIMP_TAC list_ss [FILTER_BY_BOOLS_REPL_T, LENGTH_REPLICATE])
\end{semiverbatim}
\end{exampleblock}
\end{frame}
\begin{frame}[fragile]
\frametitle{Avoid Autogenerated Names}
\begin{itemize}
\item many HOL-tactics introduce new variable names
\begin{itemize}
\item \hol{Induct}
\item \hol{Cases}
\item \ldots
\end{itemize}
\item the new names are often very artificial
\item even worse, generated names might change in future
\item proof scripts using autogenerated names are therefore
\begin{itemize}
\item hard to read
\item potentially fragile
\end{itemize}
\item therefore rename variables after they have been introduced
\item HOL has multiple tactics supporting renaming
\item most useful is \hol{rename1 `pat`}, it searches for pattern and renames vars accordingly
\end{itemize}
\end{frame}
\begin{frame}[fragile]
\frametitle{Autogenerated Names Example}
\begin{alertblock}{Bad Example}
\begin{semiverbatim}\scriptsize
prove (``!l. 1 < LENGTH l ==> (?x1 x2 l'. l = x1::x2::l')``,
GEN_TAC >>
Cases_on `l` >> SIMP_TAC list_ss [] >>
Cases_on `t` >> SIMP_TAC list_ss [])
\end{semiverbatim}
\end{alertblock}
\begin{exampleblock}{Good Example}
\begin{semiverbatim}\scriptsize
prove (``!l. 1 < LENGTH l ==> (?x1 x2 l'. l = x1::x2::l')``,
GEN_TAC >>
Cases_on `l` >> SIMP_TAC list_ss [] >>
rename1 `LENGTH l2` >>
Cases_on `l2` >> SIMP_TAC list_ss [])
\end{semiverbatim}
\end{exampleblock}
\begin{block}{Proof State before \hol{rename1}}
\begin{semiverbatim}\scriptsize
1 < SUC (LENGTH t) ==> ?x2 l'. t = x2::l'
\end{semiverbatim}
\end{block}
\begin{block}{Proof State after \hol{rename1}}
\begin{semiverbatim}\scriptsize
1 < SUC (LENGTH l2) ==> ?x2 l'. l2 = x2::l'
\end{semiverbatim}
\end{block}
\end{frame}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "current"
%%% End:

226
lectures/16_hol_overview.tex Normal file
View File

@ -0,0 +1,226 @@
\part{Overview of HOL~4}
\frame[plain]{\partpage}
\begin{frame}
\frametitle{Overview of HOL 4}
\begin{itemize}
\item in this course we discussed the basics of HOL 4
\item you were encouraged to learn more on your own in exercises
\item there is a lot more to learn even after the end of the course
\begin{itemize}
\item many more libraries
\item proof tools
\item existing formalisations
\item ...
\end{itemize}
\item to really use HOL well, you should continue learning
\item to help getting started, a short overview is presented here
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{HOL Bare Source Directories}
The following source directories are the very basis of HOL. They
are required to build \hol{hol.bare}.
\begin{itemize}
\item \hol{src/portableML} -- common stuff for PolyML and MoscowML
\item \hol{src/prekernel}
\item \hol{src/0} -- Standard Kernel
\item \hol{src/logging-kernel} -- Logging Kernel
\item \hol{src/experimental-kernel} -- Experimental Kernel
\item \hol{src/postkernel}
\item \hol{src/opentheory}
\item \hol{src/parse}
\item \hol{src/bool}
\item \hol{src/1}
\item \hol{src/proofman}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{HOL Basic Directories I}
On top of \texttt{hol.bare}, there are many basic theories and tools. These
are all required for building the main \texttt{hol} executable.
\begin{itemize}
\item \hol{src/compute} -- fast ground term rewriting
\item \hol{src/HolSat} -- SAT solver interfaces
\item \hol{src/taut} -- propositional proofs using \texttt{HolSat}
\item \hol{src/marker} -- marking terms
\item \hol{src/q} -- parsing support
\item \hol{src/combin} -- combinators
\item \hol{src/lite} -- some simple lib with various stuff
\item \hol{src/refute} -- refutation prover, normal forms
\item \hol{src/metis} -- first order resolution prover
\item \hol{src/meson} -- first order model elimination prover
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{HOL Basic Directories II}
\begin{itemize}
\item \hol{src/simp} -- simplifier
\item \hol{src/holyhammer} -- tool for finding Metis proofs
\item \hol{src/tactictoe} -- machine learning tool for finding proofs
\item \hol{src/IndDef} -- (co)inductive relation definitions
\item \hol{src/basicProof} -- library containing proof tools
\item \hol{src/relation} -- relations and order theory
\item \hol{src/one} -- unit type theory
\item \hol{src/pair} -- tuples
\item \hol{src/sum} -- sum types
\item \hol{src/tfl} -- defining terminating functions
\item \hol{src/option} -- option types
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{HOL Basic Directories III}
\begin{itemize}
\item \hol{src/num} -- numbers and arithmetic
\item \hol{src/pred\_set} -- predicate sets
\item \hol{src/datatype} -- Datatype package
\item \hol{src/list} -- list theories
\item \hol{src/monad} -- monads
\item \hol{src/quantHeuristics} -- instantiating quantifiers
\item \hol{src/unwind} -- lib for unwinding structural hardware definitions
\item \hol{src/pattern\_matches} -- pattern matches alternative
\item \hol{src/bossLib} -- main HOL lib loaded at start
\end{itemize}
\bigskip
\hol{bossLib} is one central library. It loads all basic theories and libraries and
provides convenient wrappers for the most common tools.
\end{frame}
\begin{frame}
\frametitle{HOL More Theories I}
Besides the basic libraries and theories that are required and loaded by \ml{hol}, there
are many more developements in HOL's source directory.
\begin{itemize}
\item \hol{src/sort} -- sorting lists
\item \hol{src/string} -- strings
\item \hol{src/TeX} -- exporting LaTeX code
\item \hol{src/res\_quan} -- restricted quantifiers
\item \hol{src/quotient} -- quotient type package
\item \hol{src/finite\_map} -- finite map theory
\item \hol{src/bag} -- bags \aka multisets
\item \hol{src/n-bit} -- machine words
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{HOL More Theories II}
\begin{itemize}
\item \hol{src/ring} -- reasoning about rings
\item \hol{src/integer} -- integers
\item \hol{src/llists} -- lazy lists
\item \hol{src/path} -- finite and infinite paths through a transition system
\item \hol{src/patricia} -- efficient finite map implementations using trees
\item \hol{src/emit} -- emitting SML and OCaml code
\item \hol{src/search} -- traversal of graphs that may contain cycles
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{HOL More Theories III}
\begin{itemize}
\item \hol{src/rational} -- rational numbers
\item \hol{src/real} -- real numbers
\item \hol{src/complex} -- comples numbers
\item \hol{src/HolQbf} -- quantified boolean formulas
\item \hol{src/HolSmt} -- support for external SMT solvers
\item \hol{src/float} -- IEEE floating point numbers
\item \hol{src/floating-point} -- new version of IEEE floating point numbers
\item \hol{src/probability} -- some propability theory
\item \hol{src/temporal} -- shallow embedding of temporal logic
\item \ldots
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{HOL Selected Examples I}
The directory examples hosts many theories and libraries as well. There is not
always a clear distinction between an example and a development in \ml{src}. However,
in general examples are more specialised and often larger. They are not required to
follow HOL's coding style as much as developments in \ml{src}.
\bigskip
\begin{itemize}
\item \hol{examples/balanced\_bst} -- finite maps via balanced trees
\item \hol{examples/unification} -- (nominal) unification
\item \hol{examples/Crypto} -- various block ciphers
\item \hol{examples/elliptic} -- elliptic curve cryptography
\item \hol{examples/formal-languages} -- regular and context free formal languages
\item \hol{examples/computability} -- basic computability theory
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{HOL Selected Examples II}
\begin{itemize}
\item \hol{examples/set-theory} -- axiomatic formalisation of set theory
\item \hol{examples/lambda} -- lambda calculus
\item \hol{examples/acl2} -- connection to ACL2 prover
\item \hol{examples/theorem-prover} -- soundness proof of Milawa prover
\item \hol{examples/PSL} -- formalisation of PSL
\item \hol{examples/HolBdd} -- Binary Decision Diagrams
\item \hol{examples/HolCheck} -- basic model checker
\item \hol{examples/temporal\_deep} -- deep embedding of temporal logics and automata
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{HOL Selected Examples III}
\begin{itemize}
\item \hol{examples/pgcl} formalisation of pGCL (the Probabilistic Guarded Command Language)
\item \hol{examples/dev} -- some hardware compilation
\item \hol{examples/STE} -- symbolic trajectory evalutation
\item \hol{examples/separationLogic} -- formalisation of separation logic
\item \hol{examples/ARM} -- formalisation of ARM architecture
\item \hol{examples/l3-machine-code} -- l3 language
\item \hol{examples/machine-code} -- compilers and decompilers to machine-code
\item \ldots
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Concluding Remarks}
\begin{itemize}
\item some useful tools are a bit hidden in the HOL sources
\item moreover there are developments outside the main HOL 4 sources
\begin{itemize}
\item CakeML \emph{\url{https://cakeml.org}}
\end{itemize}
\item keep in touch with community to continue learning about HOL 4
\begin{itemize}
\item mailing-list \ml{hol-info}
\item GitHub \emph{\url{https://github.com/HOL-Theorem-Prover/HOL}}
\item \emph{\url{https://hol-theorem-prover.org}}
\end{itemize}
\item if you continue using HOL, please consider sharing your work with the community
\end{itemize}
\end{frame}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "current"
%%% End:

266
lectures/17_other_provers.tex Normal file
View File

@ -0,0 +1,266 @@
\part{Other Interactive Theorem Provers}
\frame[plain]{\partpage}
\begin{frame}
\frametitle{Other Interactive Theorem Provers}
\begin{itemize}
\item at the beginning we very briefly discussed other theorem provers
\item now, with more knowledge about HOL 4 we can discuss other provers and their differences to HOL 4 in more detail
\item HOL 4 is a good system
\item it is very well suited for the tasks required by the PROSPER project
\item however, as always \emph{choose the right tool for your task}
\item you might find a different prover more suitable for your needs
\item hopefully this course has enabled you to learn to use other provers on your own without much trouble
\end{itemize}
\end{frame}
\section{HOL 4}
\begin{frame}
\frametitle{HOL 4}
\begin{itemize}
\item based on classical higher order logic
\item logic is sweet spot between expressivity and automation
\pro very trustworthy thanks to LCF approach
\pro simple enough to understand easily
\pro very easy to write custom proof tools, \ie own automation
\pro reasonably fast and efficient
\item decent automation
\con no user-interface
\con no special proof language
\con no IDE, very little editor support
\end{itemize}
\end{frame}
\section{HOL Omega}
\begin{frame}
\frametitle{HOL Omega}
\begin{itemize}
\item mainly developed by Peter Homeier \emph{\url{http://www.trustworthytools.com/}}
\item extension of HOL 4
\begin{itemize}
\pro logic extended by kinds
\pro allows type operator variables
\pro allows quantification over type variables
\end{itemize}
\pro sometimes handy to \eg model category theory
\con not very actively developed
\con HOL 4 usually sufficient and better supported
\end{itemize}
\end{frame}
\section{HOL Light}
\begin{frame}
\frametitle{HOL Light}
\begin{itemize}
\item mainly developed by John Harrison
\item \emph{\url{https://github.com/jrh13/hol-light}}
\item cleanup and reimplementation of HOL in OCaml
\item little legacy code
\item however, still very similar to HOL 4
\pro much better automation for real analysis
\pro cleaner
\con OCaml introduces some minor issues with trustworthiness
\con some other libs and tools of HOL 4 are missing
\con HOL 4 has bigger community
\end{itemize}
\end{frame}
\section{Isabelle}
\begin{frame}
\frametitle{Isabelle}
\begin{itemize}
\item Isabelle is also a descendant of LCF
\item originally developed by Larry Paulson in Cambridge\\
\emph{\url{https://www.cl.cam.ac.uk/research/hvg/Isabelle/}}
\item meanwhile also developed at TU Munich by Tobias Nipkow
\emph{\url{http://www21.in.tum.de}}
\item huge contributions by Markarius Wenzel\\
\emph{\url{http://sketis.net}}
\item Isabelle is a generic theorem prover
\item most used instantiation is Isabelle/HOL
\item other important one is Isabelle/ZF
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Isabelle / HOL - Logic}
\begin{itemize}
\item logic of Isabelle / HOL very similar to HOL's logic
\begin{itemize}
\item meta logic leads to meta level quantification and object level quantification
\pro type classes
\pro powerful module system
\pro existential variables
\item \ldots
\end{itemize}
\item Isabelle is implemented using the LCF approach
\item it uses SML (Poly/ML)
\item many original tools (\eg simplifier) similar to HOL
\item focused as HOL on equational reasoning
\item many tools are exchanged between HOL 4 and Isabelle / HOL
\begin{itemize}
\item Metis
\item Sledgehammer
\item \ldots
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Isabelle / HOL - Engineering}
\begin{itemize}
\pro a lot of engineering went into Isabelle/HOL
\pro it has a very nice GUI
\begin{itemize}
\item IDE based on JEdit
\item special language for proofs (Isar)
\item good error messages
\item \ldots
\end{itemize}
\pro very good automation
\pro efficient implementations
\pro many libraries (Archive of Formal Proof)
\pro excellent code extraction
\pro good documentation
\pro easy for new users
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Isabelle / HOL - Isar}
\begin{itemize}
\item special proof language Isar used
\item this allows to write \emph{declarative proofs}
\begin{itemize}
\item very high level
\item easy to read by humans
\item very robust
\item very good tool support
\item \ldots
\end{itemize}
\con however, tactical proofs are not easily accessible any more
\begin{itemize}
\item many intermediate goals need to be stated (declared) explicitly
\item this can be very tedious
\item tools like verification condition generators are hard to use
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Isabelle / HOL - Drawbacks}
\begin{itemize}
\pro Isabelle/HOL provides excellent out of the box automation
\pro it provides a very nice user interface
\pro it is very nice for new users
\con however, this comes at a price
\begin{itemize}
\item multiple layers added between kernel and user
\item hard to understand all these layers
\item a lot of knowledge is needed to write your own automation
\end{itemize}
\con hard to write own automation
\con Isabelle/HOL due to focus on declarative proofs not well suited for \eg PROSPER
\end{itemize}
\end{frame}
\section{Coq}
\begin{frame}
\frametitle{Coq}
\begin{itemize}
\item Coq is a proof assistant using the Calculus of Inductive Constructions
\item inspired by HOL 88
\item backward proofs as in HOL 4 used
\item however, very big differences
\begin{itemize}
\item much more powerful logic
\item dependent types
\item constructive logic
\item not exactly following LCF approach
\end{itemize}
\pro good user interface
\pro very good community support
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Coq - Logic}
\begin{itemize}
\pro Coq's logic is very powerful
\pro it is very natural for mathematicians
\pro very natural for language theory
\pro allows reasoning about proofs
\item allows to add axioms as needed
\item as a result, Coq is used often to
\begin{itemize}
\item formalise mathematics
\item formalise programming language semantics
\item reason about proof theory
\end{itemize}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Coq - Drawbacks}
\begin{itemize}
\item Coq's power comes at a price
\con there is not much automation
\con proofs tend to be very long
\begin{itemize}
\item they are very simple though
\pro comparably easy to maintain
\end{itemize}
\con Coq's proof checking can be very slow
\con when verifying programs or hardware you notice that HOL was designed for this purpose
\begin{itemize}
\item need for \emph{obvious} termination is tedious
\item missing automation
\item very slow
\end{itemize}
\end{itemize}
\end{frame}
\section{Conclusion}
\begin{frame}
\frametitle{Summary}
\begin{itemize}
\item there are many good theorem provers out there
\item \emph{pick the right tool for your purpose}
\item the HOL theorem prover is a good system for many purposes
\item for PROSPER it is a good choice
\item I encourage you to continue learning about HOL and interactive theorem proving in general
\item if you have any questions feel free to contact me (Thomas Tuerk, email \emph{thomas@tuerk-brechen.de})
\end{itemize}
\end{frame}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "current"
%%% End:

65
lectures/Makefile Normal file
View File

@ -0,0 +1,65 @@
.PHONY: full full-print current current-print all_parts all_parts_print all clean cleanAll all-slides all-print all_parts-all full-all default
default : all
PARTS = $(wildcard itp_parts_*.tex)
current: version.inc
@./mk_slides.sh current current
full: version.inc
@./mk_slides.sh full itp-course
full-print: version.inc
@./mk_handout.sh full itp-course-print
full-all: version.inc
@./mk_slides.sh full itp-course
@./mk_handout.sh full itp-course-print
hol: version.inc
@./mk_slides.sh hol hol-course
hol-print: version.inc
@./mk_handout.sh hol hol-course-print
hol-all: version.inc
@./mk_slides.sh hol hol-course
@./mk_handout.sh hol hol-course-print
current-print: version.inc
@./mk_handout.sh current current-print
itp_parts_%: version.inc
@./mk_slides.sh $@ $@
itp_parts_%-print: version.inc
@./mk_handout.sh $(patsubst %-print,%,$@) $@
itp_parts_%-all: version.inc
@./mk_slides.sh $(patsubst %-all,%,$@) $(patsubst %-all,%,$@)
@./mk_handout.sh $(patsubst %-all,%,$@) $(patsubst %-all,%-print,$@)
all_parts : $(PARTS:.tex=)
all_parts-print : $(PARTS:.tex=-print)
all_parts-all : $(PARTS:.tex=-all)
all-slides: version.inc full hol all_parts
all-print: version.inc hol-print full-print all_parts-print
all: full-all hol-all all_parts-all
clean:
rm -rf *.ps *.pdf *~ *.dvi *.aux *.log *.idx *.toc *.nav *.out *.snm *.flc *.vrb version.inc tmp
cleanAll: clean
rm -rf pdfs
version.inc: ../.git/logs/HEAD
@echo "%%% This file is generated by Makefile." > version.inc
@echo "%%% Do not edit this file!\n%%%" >> version.inc
@git log -1 --date=local --format="format:\
\\gdef\\GITAbrHash{%h}\
\\gdef\\GITAuthorDate{%ad}\
\\gdef\\GITAuthorName{%an}" >> version.inc

109
lectures/common.inc Normal file
View File

@ -0,0 +1,109 @@
\documentclass{beamer}
\usepackage{pgf,pgfnodes,pgfarrows}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{graphicx}
\usepackage[utf8]{inputenc}
\usepackage{hyperref}
\usepackage{booktabs}
\usepackage{mathpartir}
\usepackage{latexsym}
\usepackage{textcomp}
\newcommand{\ie}{i.\,e.\ }
\newcommand{\eg}{e.\,g.\ }
\newcommand{\wrt}{w.\,r.\,t.\ }
\newcommand{\aka}{a.\,k.\,a.\ }
\newcommand{\cf}{cf.\ }
\newcommand{\etc}{etc.\ }
\newcommand{\cearrow}{\url{~}>}
\renewcommand{\emph}[1]{\structure{\textbf{#1}}}
\newcommand{\entails}{\vdash}
\newcommand{\hol}[1]{\emph{\texttt{#1}}}
\newcommand{\ml}[1]{\emph{\texttt{#1}}}
\newcommand{\textbsl}{\char`\\{}}
\newcommand{\holAnd}{/\textbsl{}}
\newcommand{\holOr}{\textbsl{}/}
\newcommand{\holLambda}{\textbsl{}}
\newcommand{\holImp}{==>}
\newcommand{\holEquiv}{<=>}
\newcommand{\holNeg}{\raisebox{0.5ex}{\texttildelow}}
\newcommand{\mlcomment}[1]{\structure{(* #1 *)}}
\newcommand{\aequiv}{\ensuremath{\stackrel{\alpha}{\equiv}}\ }
\newcommand\pro{\item[$+$]}
\newcommand\con{\item[$-$]}
\newcommand{\bottomstatement}[1]{
\begin{center}
\textbf{#1}
\end{center}
}
\input{version.inc}
\title{Interactive Theorem Proving (ITP) Course}
\institute{
\includegraphics[width=1.25cm]{images/cc/cc.eps}
\includegraphics[width=1.25cm]{images/cc/by.eps}
\includegraphics[width=1.25cm]{images/cc/sa.eps}\\
\scriptsize{Except where otherwise noted, this work is licened under\\
\href{http://creativecommons.org/licenses/by-sa/4.0/}{Creative Commons Attribution-ShareAlike 4.0 International License}}}
\author{Thomas Tuerk (thomas@tuerk-brechen.de)}
\date{Academic Year 2016/17, Period 4}
\newcommand{\partstitle}[1]{\title{Interactive Theorem Proving (ITP) Course\\#1}}
\newcommand{\titleframe}{\frame[plain]{\titlepage\hfill\tiny version \GITAbrHash{} of \GITAuthorDate{}}}
\newcommand{\partstitleframe}[1]{\partstitle{#1}\titleframe}
\usetheme{Boadilla}
\setbeamertemplate{footline}[frame number]{}
\logo{\pgfputat{\pgfxy(-.5,8.7)}{\pgfbox[center,top]{\includegraphics[width=8mm]{images/cc/by-sa.eps}}}}
\setbeamertemplate{part page}
{
\begin{centering}
{\usebeamerfont{part name}\usebeamercolor[fg]{part name}\partname~\insertromanpartnumber}
\vskip1em\par
\begin{beamercolorbox}[sep=16pt,center]{part title}
\usebeamerfont{part title}\insertpart\par
\end{beamercolorbox}
\vfill
\begin{center}
\includegraphics[width=0.75cm]{images/cc/cc.eps}
\includegraphics[width=0.75cm]{images/cc/by.eps}
\includegraphics[width=0.75cm]{images/cc/sa.eps}\\
\tiny{Except where otherwise noted, this work is licened under\\
\href{http://creativecommons.org/licenses/by-sa/4.0/}{Creative Commons Attribution-ShareAlike 4.0 International License}}.
\end{center}
\end{centering}
}
\makeatletter
\AtBeginPart{%
\addtocontents{toc}{\protect\beamer@partintoc{\the\c@part}{\beamer@partnameshort}{\the\c@page}{\the\numexpr\value{framenumber}+1\relax}}%
}
%% number, shortname, page.
\providecommand\beamer@partintoc[4]{%
\ifnum\c@tocdepth=-1\relax
% requesting onlyparts.
\qquad\makebox[5em][l]{\hyperlink{page.#3}{\emph{Part {\uppercase\expandafter{\romannumeral #1\relax}}}}} \makebox[18em][l]{\hyperlink{page.#3}{#2}}
\makebox[3em][r]{\hyperlink{page.#3}{#4}}
\par
\fi
}
\define@key{beamertoc}{onlyparts}[]{%
\c@tocdepth=-1\relax
}
\makeatother
%\usefonttheme[onlylarge]{structurebold}
%\usepackage{times}
\ifdefined\ttbwflag
\usecolortheme{seagull}
\beamertemplatenavigationsymbolsempty
\fi

32
lectures/current.tex Normal file
View File

@ -0,0 +1,32 @@
\input{common.inc}
%\setbeamertemplate{footline}{}
\setcounter{part}{2}
\setcounter{framenumber}{291}
\begin{document}
\partstitleframe{Parts III}
%\input{00_webpage_intro.tex}
%\input{01_introduction.tex}
%\input{02_organisational_matters.tex}
\input{03_hol_overview.tex}
%\input{04_hol_logic.tex}
%\input{05_usage.tex}
%\input{06_forward_proofs.tex}
%\input{07_backward_proofs.tex}
%\input{08_basic_tactics.tex}
%\input{09_induction.tex}
%\input{10_definitions.tex}
%\input{11_good_definitions.tex}
%\input{12_deep_shallow.tex}
%\input{13_rewriting.tex}
%\input{14_advanced_definitions.tex}
%\input{15_maintainable_proofs.tex}
%\input{16_hol_overview.tex}
%\input{17_other_provers.tex}
\end{document}

37
lectures/full.tex Normal file
View File

@ -0,0 +1,37 @@
\input{common.inc}
\begin{document}
\titleframe
\begin{frame}{Contents}
\footnotesize
\tableofcontents[onlyparts]
\end{frame}
\input{01_introduction.tex}
\input{02_organisational_matters.tex}
\input{03_hol_overview.tex}
\input{04_hol_logic.tex}
\input{05_usage.tex}
\input{06_forward_proofs.tex}
\input{07_backward_proofs.tex}
\input{08_basic_tactics.tex}
\input{09_induction.tex}
\input{10_definitions.tex}
\input{11_good_definitions.tex}
\input{12_deep_shallow.tex}
\input{13_rewriting.tex}
\input{14_advanced_definitions.tex}
\input{15_maintainable_proofs.tex}
\input{16_hol_overview.tex}
\input{17_other_provers.tex}
% code extraction / cake ML
% conformance testing
% maintainable proofs
% overview over main tools / libs
% wordLib
% decision procedures
\end{document}

34
lectures/hol.tex Normal file
View File

@ -0,0 +1,34 @@
\input{common.inc}
\date{}
\begin{document}
\author{Thomas Tuerk (tuerk@thomas-tuerk.de)}
\partstitleframe{Web Version}
\begin{frame}{Contents}
\footnotesize
\tableofcontents[onlyparts]
\end{frame}
\input{00_webpage_intro.tex}
\input{01_introduction.tex}
\input{03_hol_overview.tex}
\input{04_hol_logic.tex}
\input{05_usage.tex}
\input{06_forward_proofs.tex}
\input{07_backward_proofs.tex}
\input{08_basic_tactics.tex}
\input{09_induction.tex}
\input{10_definitions.tex}
\input{11_good_definitions.tex}
\input{12_deep_shallow.tex}
\input{13_rewriting.tex}
\input{14_advanced_definitions.tex}
\input{15_maintainable_proofs.tex}
\input{16_hol_overview.tex}
\input{17_other_provers.tex}
\end{document}

8
lectures/images/Makefile Executable file
View File

@ -0,0 +1,8 @@
all:
latex hol-family.tex
dvips hol-family.dvi
ps2eps hol-family.ps
clean:
rm -f *.dvi *.toc *.aux *.ps *.log *.lof *.bbl *.blg *.hix *.tid *.tde *.out *~

3
lectures/images/cc/LICENSE Normal file
View File

@ -0,0 +1,3 @@
The images in this directory are trademarks of creative-commons,
which are covered by the Creative Commons Trademark Policy
(https://creativecommons.org/policies).

2727
lectures/images/cc/by-sa.eps Normal file
View File

File diff suppressed because one or more lines are too long

5902
lectures/images/cc/by.eps Normal file
View File

File diff suppressed because one or more lines are too long

5902
lectures/images/cc/cc.eps Normal file
View File

File diff suppressed because one or more lines are too long

5902
lectures/images/cc/sa.eps Normal file
View File

File diff suppressed because one or more lines are too long

3452
lectures/images/hol-family.eps Normal file
View File

File diff suppressed because it is too large Load Diff

38
lectures/images/hol-family.tex Normal file
View File

@ -0,0 +1,38 @@
\documentclass{minimal}
\usepackage{pstricks}
\pagestyle{empty}
\begin{document}
\begin{pspicture}(0,6)(8,22)
\usefont{T1}{ppl}{m}{n}
\rput(3,20){Edinburgh LCF}
\rput(3,18){Cambridge LCF}
\rput(3,16){HOL88}
\rput(1,14){hol90}
\rput(5,13.5){ProofPower}
\rput(5,14.5){Isabelle/HOL}
\rput(3,12){HOL Light}
\rput(1,10){hol98}
\rput(5,10){HOL Zero}
\rput(1,8){HOL4}
\psline{->}(3,19.7)(3,18.3)
\psline{->}(3,17.7)(3,16.3)
\psline{->}(1,13.7)(1,10.3)
\psline{->}(1,9.7)(1,8.3)
\psline{->}(3,11.7)(1,10.3)
\psline{->}(3,11.7)(5,10.3)
\psline{->}(5,13.2)(5,10.3)
\psline{->}(3,15.7)(3,12.3)
\psline{->}(3,15.7)(1,14.3)
\psline{->}(3,15.7)(3.8,14.5)
\psline{->}(3,15.7)(3.8,13.5)
\psline{->}(1,13.7)(3,12.3)
\end{pspicture}
\end{document}

14
lectures/itp_parts_01-04.tex Normal file
View File

@ -0,0 +1,14 @@
\input{common.inc}
\setcounter{framenumber}{1}
\begin{document}
\partstitleframe{Parts I - IV}
\input{01_introduction.tex}
\input{02_organisational_matters.tex}
\input{03_hol_overview.tex}
\input{04_hol_logic.tex}
\end{document}

16
lectures/itp_parts_05-06.tex Normal file
View File

@ -0,0 +1,16 @@
\input{common.inc}
%\setbeamertemplate{footline}{}
\setcounter{part}{4}
\setcounter{framenumber}{42}
\begin{document}
\partstitleframe{Parts V, VI}
\input{05_usage.tex}
\input{06_forward_proofs.tex}
\end{document}

16
lectures/itp_parts_07-09.tex Normal file
View File

@ -0,0 +1,16 @@
\input{common.inc}
%\setbeamertemplate{footline}{}
\setcounter{part}{6}
\setcounter{framenumber}{65}
\begin{document}
\partstitleframe{Parts VII - IX}
\input{07_backward_proofs.tex}
\input{08_basic_tactics.tex}
\input{09_induction.tex}
\end{document}

16
lectures/itp_parts_10-12.tex Normal file
View File

@ -0,0 +1,16 @@
\input{common.inc}
%\setbeamertemplate{footline}{}
\setcounter{part}{9}
\setcounter{framenumber}{123}
\begin{document}
\partstitleframe{Parts X - XII}
\input{10_definitions.tex}
\input{11_good_definitions.tex}
\input{12_deep_shallow.tex}
\end{document}

18
lectures/itp_parts_13.tex Normal file
View File

@ -0,0 +1,18 @@
\input{common.inc}
%\setbeamertemplate{footline}{}
\setcounter{part}{12}
\setcounter{framenumber}{196}
\begin{document}
\partstitleframe{Part XIII}
%\input{10_definitions.tex}
%\input{11_good_definitions.tex}
%\input{12_deep_shallow.tex}
\input{13_rewriting.tex}
%\input{14_advanced_definitions.tex}
\end{document}

14
lectures/itp_parts_14.tex Normal file
View File

@ -0,0 +1,14 @@
\input{common.inc}
%\setbeamertemplate{footline}{}
\setcounter{part}{13}
\setcounter{framenumber}{250}
\begin{document}
\partstitleframe{Part XIV}
\input{14_advanced_definitions.tex}
\end{document}

14
lectures/itp_parts_15.tex Normal file
View File

@ -0,0 +1,14 @@
\input{common.inc}
%\setbeamertemplate{footline}{}
\setcounter{part}{14}
\setcounter{framenumber}{271}
\begin{document}
\partstitleframe{Part XV}
\input{15_maintainable_proofs.tex}
\end{document}

15
lectures/itp_parts_16-17.tex Normal file
View File

@ -0,0 +1,15 @@
\input{common.inc}
%\setbeamertemplate{footline}{}
\setcounter{part}{15}
\setcounter{framenumber}{293}
\begin{document}
\partstitleframe{Part XVI, XVII}
\input{16_hol_overview.tex}
\input{17_other_provers.tex}
\end{document}

10
lectures/mk_handout.sh Executable file
View File

@ -0,0 +1,10 @@
#!/bin/sh
echo "creating $2.pdf"
mkdir -p tmp
pdflatex -interaction=batchmode -output-directory=tmp "\PassOptionsToClass{handout}{beamer}\def\ttbwflag{}\input{$1.tex}" > /dev/null
pdflatex -interaction=batchmode -output-directory=tmp "\PassOptionsToClass{handout}{beamer}\def\ttbwflag{}\input{$1.tex}" > /dev/null
cd tmp
pdfjam --landscape --a4paper --nup 2x2 --scale 0.9 $1.pdf -o $1-4.pdf -q
cd ..
mkdir -p pdfs
mv tmp/$1-4.pdf pdfs/$2.pdf

8
lectures/mk_slides.sh Executable file
View File

@ -0,0 +1,8 @@
#!/bin/sh
echo "creating $2.pdf"
mkdir -p tmp
pdflatex -interaction=batchmode -output-directory=tmp $1.tex > /dev/null
pdflatex -interaction=batchmode -output-directory=tmp $1.tex > /dev/null
mkdir -p pdfs
mv tmp/$1.pdf pdfs/$2.pdf