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 -> Set 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 -> Set
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 possible inputs
343and is guaranteed to terminate. Otherwise we could construct an element of the empty type,
344from 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 the prompt
363with the \texttt{:total} command. We see that neither of the above definitions is total:
365\begin{SaveVerbatim}{totalcheck}
367*theorems> :total empty1
368possibly not total due to: empty1#hd
369 not total as there are missing cases
370*theorems> :total empty2
371possibly not total as it is not well founded
377Note the use of the word ``possibly'' --- a totality check can, of course, never be certain
378due to the undecidability of the halting problem. The check is, therefore, conservative.
379It is also possible (and indeed advisable, in the case of proofs) to mark functions as
380total so that it will be a compile time error for the totality check to fail:
382\begin{SaveVerbatim}{emptyfail}
387Type checking ./theorems.idr
388theorems.idr:25:empty2 is possibly not total as it is not well founded
394Reassuringly, our proof in Section \ref{sect:empty} that the zero and successor constructors
395are disjoint is total:
397\begin{SaveVerbatim}{totdisjoint}
399*theorems> :total disjoint
406The totality check is currently very conservative. To be recorded as total, a function must:
409\item Cover all possible inputs
410\item Be \emph{well-founded} --- i.e. each recursive call must have a decreasing argument
411\item Not call any non-total functions
412\item Not use any data types which are not \emph{strictly positive}
413\item (In version 0.9.2) Not be mutually recursive
417The last of these conditions may be relaxed in the future.
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