edwinb/Idris-dev forked from idris-lang/Idris-dev

Subversion checkout URL

You can clone with
or
.
Fetching contributors…

Cannot retrieve contributors at this time

418 lines (295 sloc) 11.633 kB
 \section{Theorem Proving} \subsection{Equality} \Idris{} allows propositional equalities to be declared, allowing theorems about programs to be stated and proved. Equality is built in, but conceptually has the following definition: \begin{SaveVerbatim}{} data (=) : a -> b -> Set where refl : x = x \end{SaveVerbatim} \useverb{} \noindent Equalities can be proposed between any values of any types, but the only way to construct a proof of equality is if values actually are equal. For example: \begin{SaveVerbatim}{eqprf} fiveIsFive : 5 = 5 fiveIsFive = refl twoPlusTwo : 2 + 2 = 4 twoPlusTwo = refl \end{SaveVerbatim} \useverb{eqprf} \subsection{The Empty Type} \label{sect:empty} There is an empty type, \texttt{\_|\_}, which has no constructors. It is therefore impossible to construct an element of the empty type, at least without using a partially defined or general recursive function (see Section \ref{sect:totality} for more details). We can therefore use the empty type to prove that something is impossible, for example zero is never equal to a successor: \begin{SaveVerbatim}{natdisjoint} disjoint : (n : Nat) -> O = S n -> _|_ disjoint n p = replace {P = disjointTy} p () where disjointTy : Nat -> Set disjointTy O = () disjointTy (S k) = _|_ \end{SaveVerbatim} \useverb{natdisjoint} \noindent There is no need to worry too much about how this function works --- essentially, it applies the library function \texttt{replace}, which uses an equality proof to transform a predicate. Here we use it to transform a value of a type which can exist, the empty tuple, to a value of a type which can't, by using a proof of something which can't exist. Once we have an element of the empty type, we can prove anything. \texttt{FalseElim} is defined in the library, to assist with proofs by contradiction. \begin{SaveVerbatim}{falseelim} FalseElim : _|_ -> a \end{SaveVerbatim} \useverb{falseelim} \subsection{Simple Theorems} When type checking dependent types, the type itself gets \emph{normalised}. So imagine we want to prove the following theorem about the reduction behaviour of \texttt{plus}: \begin{SaveVerbatim}{plusred} plusReduces : (n:Nat) -> plus O n = n \end{SaveVerbatim} \useverb{plusred} \noindent We've written down the statement of the theorem as a type, in just the same way as we would write the type of a program. In fact there is no real distinction between proofs and programs. A proof, as far as we are concerned here, is merely a program with a precise enough type to guarantee a particular property of interest. We won't go into details here, but the Curry-Howard correspondence~\cite{howard} explains this relationship. The proof itself is trivial, because \texttt{plus O n} normalises to \texttt{n} by the definition of \texttt{plus}: \begin{SaveVerbatim}{plusredp} plusReduces n = refl \end{SaveVerbatim} \useverb{plusredp} \noindent It is slightly harder if we try the arguments the other way, because plus is defined by recursion on its first argument. The proof also works by recursion on the first argument to \texttt{plus}, namely \texttt{n}. \begin{SaveVerbatim}{plusRedO} plusReducesO : (n:Nat) -> n = plus n O plusReducesO O = refl plusReducesO (S k) = cong (plusReducesO k) \end{SaveVerbatim} \useverb{plusRedO} \noindent \texttt{cong} is a function defined in the library which states that equality respects function application: \begin{SaveVerbatim}{resps} cong : {f : t -> u} -> a = b -> f a = f b \end{SaveVerbatim} \useverb{resps} \noindent We can do the same for the reduction behaviour of plus on successors: \begin{SaveVerbatim}{plusRedS} plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m) plusReducesS O m = refl plusReducesS (S k) m = cong (plusReducesS k m) \end{SaveVerbatim} \useverb{plusRedS} \noindent Even for trival theorems like these, the proofs are a little tricky to construct in one go. When things get even slightly more complicated, it becomes too much to think about to construct proofs in this 'batch mode'. \Idris{} therefore provides an interactive proof mode. \subsection{Interactive theorem proving} Instead of writing the proof in one go, we can use \Idris{}'s interactive proof mode. To do this, we write the general \emph{structure} of the proof, and use the interactive mode to complete the details. We'll be constructing the proof by \emph{induction}, so we write the cases for \texttt{O} and \texttt{S}, with a recursive call in the \texttt{S} case giving the inductive hypothesis, and insert \emph{metavariables} for the rest of the definition: \begin{SaveVerbatim}{prOstruct} plusReducesO' : (n:Nat) -> n = plus n O plusReducesO' O = ?plusredO_O plusReducesO' (S k) = let ih = plusReducesO' k in ?plusredO_S \end{SaveVerbatim} \useverb{prOstruct} \noindent On running \Idris{}, two global names are created, \texttt{plusredO\_O} and \texttt{plusredO\_S}, with no definition. We can use the \texttt{:m} command at the prompt to find out which metavariables are still to be solved (or, more precisely, which functions exist but have no definitions), then the \texttt{:t} command to see their types: \begin{SaveVerbatim}{showmetas} *theorems> :m Global metavariables: [plusredO_S,plusredO_O] \end{SaveVerbatim} \begin{SaveVerbatim}{metatypes} *theorems> :t plusredO_O plusredO_O : O = plus O O *theorems> :t plusredO_S plusredO_S : (k : Nat) -> (k = plus k O) -> S k = S (plus k O) \end{SaveVerbatim} \useverb{showmetas} \useverb{metatypes} \noindent The \texttt{:p} command enters interactive proof mode, which can be used to complete the missing definitions. \begin{SaveVerbatim}{proveO} *theorems> :p plusredO_O ---------------------------------- (plusredO_O) -------- {hole0} : O = plus O O \end{SaveVerbatim} \useverb{proveO} \noindent This gives us a list of premisses (above the line; there are none here) and the current goal (below the line; named \texttt{\{hole0\}} here). At the prompt we can enter tactics to direct the construction of the proof. In this case, we can normalise the goal with the \texttt{compute} tactic: \begin{SaveVerbatim}{compute} -plusredO_O> compute ---------------------------------- (plusredO_O) -------- {hole0} : O = O \end{SaveVerbatim} \useverb{compute} \noindent Now we have to prove that \texttt{O} equals \texttt{O}, which is easy to prove by \texttt{refl}. To apply a function, such as \texttt{refl}, we use \texttt{refine} which introduces subgoals for each of the function's explicit arguments (\texttt{refl} has none): \begin{SaveVerbatim}{refrefl} -plusredO_O> refine refl plusredO_O: no more goals \end{SaveVerbatim} \useverb{refrefl} \noindent Here, we could also have used the \texttt{trivial} tactic, which tries to refine by \texttt{refl}, and if that fails, tries to refine by each name in the local context. When a proof is complete, we use the \texttt{qed} tactic to add the proof to the global context, and remove the metavariable from the unsolved metavariables list. This also outputs a trace of the proof: \begin{SaveVerbatim}{prOprooftrace} -plusredO_O> qed plusredO_O = proof { compute; refine refl; } \end{SaveVerbatim} \useverb{prOprooftrace} \begin{SaveVerbatim}{showmetasO} *theorems> :m Global metavariables: [plusredO_S] \end{SaveVerbatim} \useverb{showmetasO} \noindent The \texttt{:addproof} command, at the interactive prompt, will add the proof to the source file (effectively in an appendix). Let us now prove the other required lemma, \texttt{plusredO\_S}: \begin{SaveVerbatim}{plusredOSprf} *theorems> :p plusredO_S ---------------------------------- (plusredO_S) -------- {hole0} : (k : Nat) -> (k = plus k O) -> S k = S (plus k O) \end{SaveVerbatim} \useverb{plusredOSprf} \noindent In this case, the goal is a function type, using \texttt{k} (the argument accessible by pattern matching) and \texttt{ih} (the local variable containing the result of the recursive call). We can introduce these as premisses using the \texttt{intro} tactic twice (or \texttt{intros}, which introduces all arguments as premisses). This gives: \begin{SaveVerbatim}{prSintros} k : Nat ih : k = plus k O ---------------------------------- (plusredO_S) -------- {hole2} : S k = S (plus k O) \end{SaveVerbatim} \useverb{prSintros} \noindent We know, from the type of \texttt{ih}, that \texttt{k = plus k O}, so we would like to use this knowledge to replace \texttt{plus k O} in the goal with \texttt{k}. We can achieve this with the \texttt{rewrite} tactic: \begin{SaveVerbatim}{} -plusredO_S> rewrite ih k : Nat ih : k = plus k O ---------------------------------- (plusredO_S) -------- {hole3} : S k = S k -plusredO_S> \end{SaveVerbatim} \useverb{} \noindent The \texttt{rewrite} tactic takes an equality proof as an argument, and tries to rewrite the goal using that proof. Here, it results in an equality which is trivially provable: \begin{SaveVerbatim}{prOStrace} -plusredO_S> trivial plusredO_S: no more goals -plusredO_S> qed plusredO_S = proof { intros; rewrite ih; trivial; } \end{SaveVerbatim} \useverb{prOStrace} \noindent Again, we can add this proof to the end of our source file using the \texttt{:addproof} command at the interactive prompt. \subsection{Totality Checking} \label{sect:totality} If we really want to trust our proofs, it is important that they are defined by \emph{total} functions --- that is, a function which is defined for all possible inputs and is guaranteed to terminate. Otherwise we could construct an element of the empty type, from which we could prove anything: \begin{SaveVerbatim}{empties} -- making use of 'hd' being partially defined empty1 : _|_ empty1 = hd [] where hd : List a -> a hd (x :: xs) = x -- not terminating empty2 : _|_ empty2 = empty2 \end{SaveVerbatim} \useverb{empties} \noindent Internally, \Idris{} checks every definition for totality, and we can check at the prompt with the \texttt{:total} command. We see that neither of the above definitions is total: \begin{SaveVerbatim}{totalcheck} *theorems> :total empty1 possibly not total due to: empty1#hd not total as there are missing cases *theorems> :total empty2 possibly not total as it is not well founded \end{SaveVerbatim} \useverb{totalcheck} \noindent Note the use of the word possibly'' --- a totality check can, of course, never be certain due to the undecidability of the halting problem. The check is, therefore, conservative. It is also possible (and indeed advisable, in the case of proofs) to mark functions as total so that it will be a compile time error for the totality check to fail: \begin{SaveVerbatim}{emptyfail} total empty2 : _|_ empty2 = empty2 Type checking ./theorems.idr theorems.idr:25:empty2 is possibly not total as it is not well founded \end{SaveVerbatim} \useverb{emptyfail} \noindent Reassuringly, our proof in Section \ref{sect:empty} that the zero and successor constructors are disjoint is total: \begin{SaveVerbatim}{totdisjoint} *theorems> :total disjoint Total \end{SaveVerbatim} \useverb{totdisjoint} \noindent The totality check is currently very conservative. To be recorded as total, a function must: \begin{itemize} \item Cover all possible inputs \item Be \emph{well-founded} --- i.e. each recursive call must have a decreasing argument \item Not call any non-total functions \item Not use any data types which are not \emph{strictly positive} \item (In version 0.9.2) Not be mutually recursive \end{itemize} \noindent The last of these conditions may be relaxed in the future.
Something went wrong with that request. Please try again.