1\section{Theorem Proving}
5\Idris{} allows propositional equalities to be declared, allowing theorems about
6programs to be stated and proved. Equality is built in, but conceptually has
7the following definition:
11data (=) : a -> b -> Type where
18Equalities can be proposed between any values of any types, but the only way to
19construct a proof of equality is if values actually are equal. For example:
21\begin{SaveVerbatim}{eqprf}
32\subsection{The Empty Type}
36There is an empty type, \texttt{\_|\_}, which has no constructors. It is
37therefore impossible to construct an element of the empty type, at least
38without using a partially defined or general recursive function (see Section
39\ref{sect:totality} for more details). We can therefore use the empty type
40to prove that something is impossible, for example zero is never equal
43\begin{SaveVerbatim}{natdisjoint}
45disjoint : (n : Nat) -> O = S n -> _|_
46disjoint n p = replace {P = disjointTy} p ()
48 disjointTy : Nat -> Type
50 disjointTy (S k) = _|_
56There is no need to worry too much about how this function works --- essentially,
57it applies the library function \texttt{replace}, which uses an equality proof to
58transform a predicate. Here we use it to transform a value of a type which can exist,
59the empty tuple, to a value of a type which can't, by using a proof of something
62Once we have an element of the empty type, we can prove anything. \texttt{FalseElim}
63is defined in the library, to assist with proofs by contradiction.
65\begin{SaveVerbatim}{falseelim}
72\subsection{Simple Theorems}
74When type checking dependent types, the type itself gets \emph{normalised}. So imagine
75we want to prove the following theorem about the reduction behaviour of \texttt{plus}:
77\begin{SaveVerbatim}{plusred}
79plusReduces : (n:Nat) -> plus O n = n
85We've written down the statement of the theorem as a type, in just the same way
86as we would write the type of a program. In fact there is no real distinction
87between proofs and programs. A proof, as far as we are concerned here, is
88merely a program with a precise enough type to guarantee a particular property
91We won't go into details here, but the Curry-Howard
92correspondence~\cite{howard} explains this relationship.
93The proof itself is trivial, because \texttt{plus O n} normalises to \texttt{n}
94by the definition of \texttt{plus}:
96\begin{SaveVerbatim}{plusredp}
104It is slightly harder if we try the arguments the other way, because plus is
105defined by recursion on its first argument. The proof also works by recursion
106on the first argument to \texttt{plus}, namely \texttt{n}.
108\begin{SaveVerbatim}{plusRedO}
110plusReducesO : (n:Nat) -> n = plus n O
112plusReducesO (S k) = cong (plusReducesO k)
118\texttt{cong} is a function defined in the library which states that
119equality respects function application:
121\begin{SaveVerbatim}{resps}
123cong : {f : t -> u} -> a = b -> f a = f b
129We can do the same for the reduction behaviour of plus on successors:
131\begin{SaveVerbatim}{plusRedS}
133plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
134plusReducesS O m = refl
135plusReducesS (S k) m = cong (plusReducesS k m)
141Even for trival theorems like these, the proofs are a little tricky to
142construct in one go. When things get even slightly more complicated, it becomes
143too much to think about to construct proofs in this 'batch mode'. \Idris{}
144therefore provides an interactive proof mode.
146\subsection{Interactive theorem proving}
148Instead of writing the proof in one go, we can use \Idris{}'s interactive
149proof mode. To do this, we write the general \emph{structure} of the proof,
150and use the interactive mode to complete the details. We'll be constructing
151the proof by \emph{induction}, so we write the cases for \texttt{O} and
152\texttt{S}, with a recursive call in the \texttt{S} case giving the inductive
153hypothesis, and insert \emph{metavariables} for the rest of the definition:
155\begin{SaveVerbatim}{prOstruct}
157plusReducesO' : (n:Nat) -> n = plus n O
158plusReducesO' O = ?plusredO_O
159plusReducesO' (S k) = let ih = plusReducesO' k in
166On running \Idris{}, two global names are created, \texttt{plusredO\_O} and
167\texttt{plusredO\_S}, with no definition. We can use the \texttt{:m} command
168at the prompt to find out which metavariables are still to be solved (or, more
169precisely, which functions exist but have no definitions), then the
170\texttt{:t} command to see their types:
172\begin{SaveVerbatim}{showmetas}
176 [plusredO_S,plusredO_O]
180\begin{SaveVerbatim}{metatypes}
182*theorems> :t plusredO_O
183plusredO_O : O = plus O O
185*theorems> :t plusredO_S
186plusredO_S : (k : Nat) -> (k = plus k O) -> S k = S (plus k O)
194The \texttt{:p} command enters interactive proof mode, which can be used to complete
195the missing definitions.
197\begin{SaveVerbatim}{proveO}
199*theorems> :p plusredO_O
201---------------------------------- (plusredO_O) --------
202{hole0} : O = plus O O
208This gives us a list of premisses
209(above the line; there are none here) and the current goal (below the line;
210named \texttt{\{hole0\}} here).
211At the prompt we can enter tactics to direct the construction of the proof. In this case,
212we can normalise the goal with the \texttt{compute} tactic:
214\begin{SaveVerbatim}{compute}
218---------------------------------- (plusredO_O) --------
225Now we have to prove that \texttt{O} equals \texttt{O}, which is easy to prove by
226\texttt{refl}. To apply a function, such as \texttt{refl}, we use \texttt{refine}
227which introduces subgoals for each of the function's explicit arguments (\texttt{refl}
230\begin{SaveVerbatim}{refrefl}
232-plusredO_O> refine refl
233plusredO_O: no more goals
239Here, we could also have used the \texttt{trivial} tactic, which tries to refine by
240\texttt{refl}, and if that fails, tries to refine by each name in the local context.
241When a proof is complete, we use the \texttt{qed} tactic to add the proof to the
242global context, and remove the metavariable from the unsolved metavariables list.
243This also outputs a trace of the proof:
245\begin{SaveVerbatim}{prOprooftrace}
254\useverb{prOprooftrace}
256\begin{SaveVerbatim}{showmetasO}
266The \texttt{:addproof} command, at the interactive prompt, will add the proof to
267the source file (effectively in an appendix).
268Let us now prove the other required lemma, \texttt{plusredO\_S}:
270\begin{SaveVerbatim}{plusredOSprf}
272*theorems> :p plusredO_S
274---------------------------------- (plusredO_S) --------
275{hole0} : (k : Nat) -> (k = plus k O) -> S k = S (plus k O)
278\useverb{plusredOSprf}
281In this case, the goal is a function type, using \texttt{k} (the argument accessible by
282pattern matching) and \texttt{ih} (the local variable containing the result of
283the recursive call). We can introduce these as premisses using the \texttt{intro} tactic
284twice (or \texttt{intros}, which introduces all arguments as premisses). This gives:
286\begin{SaveVerbatim}{prSintros}
290---------------------------------- (plusredO_S) --------
291{hole2} : S k = S (plus k O)
297We know, from the type of \texttt{ih}, that \texttt{k = plus k O}, so we would like to
298use this knowledge to replace \texttt{plus k O} in the goal with \texttt{k}. We can
299achieve this with the \texttt{rewrite} tactic:
301\begin{SaveVerbatim}{}
303-plusredO_S> rewrite ih
307---------------------------------- (plusredO_S) --------
316The \texttt{rewrite} tactic takes an equality proof as an argument, and tries to rewrite
317the goal using that proof. Here, it results in an equality which is trivially provable:
319\begin{SaveVerbatim}{prOStrace}
322plusredO_S: no more goals
334Again, we can add this proof to the end of our source file using the \texttt{:addproof}
335command at the interactive prompt.
337\subsection{Totality Checking}
341If we really want to trust our proofs, it is important that they are defined by
342\emph{total} functions --- that is, a function which is defined for all
343possible inputs and is guaranteed to terminate. Otherwise we could construct an
344element of the empty type, from which we could prove anything:
346\begin{SaveVerbatim}{empties}
348-- making use of 'hd' being partially defined
362Internally, \Idris{} checks every definition for totality, and we can check at
363the prompt with the \texttt{:total} command. We see that neither of the above
366\begin{SaveVerbatim}{totalcheck}
368*theorems> :total empty1
369possibly not total due to: empty1#hd
370 not total as there are missing cases
371*theorems> :total empty2
372possibly not total due to recursive path empty2
378Note the use of the word ``possibly'' --- a totality check can, of course,
379never be certain due to the undecidability of the halting problem. The check
380is, therefore, conservative. It is also possible (and indeed advisable, in the
381case of proofs) to mark functions as total so that it will be a compile time
382error for the totality check to fail:
384\begin{SaveVerbatim}{emptyfail}
389Type checking ./theorems.idr
390theorems.idr:25:empty2 is possibly not total due to recursive path empty2
396Reassuringly, our proof in Section \ref{sect:empty} that the zero and successor constructors
397are disjoint is total:
399\begin{SaveVerbatim}{totdisjoint}
401*theorems> :total disjoint
408The totality check is, necessarily, conservative. To be recorded as total, a
409function \texttt{f} must:
412\item Cover all possible inputs
413\item Be \emph{well-founded} --- i.e. by the time a sequence of
414(possibly mutually) recursive calls reaches \texttt{f} again, it must
415be possible to show that one its has decreased.
416\item Not use any data types which are not \emph{strictly positive}
417\item Not call any non-total functions
420\subsubsection{Directives and Compiler Flags for Totality}
422By default, \Idris{} allows all definitions, whether total or not. However,
423it is desirable for functions to be total as far as possible, as this
424provides a guarantee that they provide a result for all possible inputs,
425in finite time. It is possible to make total functions a requirement,
429\item By using the \texttt{--total} compiler flag.
430\item By adding a \texttt{\%default total} directive to a source file.
431All definitions after this will be required to be total, unless
432explicitly flagged as \texttt{partial}.
436All functions \remph{after} a \texttt{\%default total} declaration are required
437to be total. Correspondingly, after a \texttt{\%default partial} declaration,
438the requirement is relaxed.
440Finally, the compiler flag \texttt{--warnpartial} causes \Idris{} to print
441a warning for any undeclared partial function.
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list