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:
10data (=) : a -> b -> Type where
15Equalities can be proposed between any values of any types, but the only way to
16construct a proof of equality is if values actually are equal. For example:
26\subsection{The Empty Type}
30There is an empty type, \texttt{\_|\_}, which has no constructors. It is
31therefore impossible to construct an element of the empty type, at least
32without using a partially defined or general recursive function (see Section
33\ref{sect:totality} for more details). We can therefore use the empty type
34to prove that something is impossible, for example zero is never equal
38disjoint : (n : Nat) -> Z = S n -> _|_
39disjoint n p = replace {P = disjointTy} p ()
41 disjointTy : Nat -> Type
43 disjointTy (S k) = _|_
47There is no need to worry too much about how this function works --- essentially,
48it applies the library function \texttt{replace}, which uses an equality proof to
49transform a predicate. Here we use it to transform a value of a type which can exist,
50the empty tuple, to a value of a type which can't, by using a proof of something which can't exist.
52Once we have an element of the empty type, we can prove anything. \texttt{FalseElim}
53is defined in the library, to assist with proofs by contradiction.
59\subsection{Simple Theorems}
61When type checking dependent types, the type itself gets \emph{normalised}. So imagine
62we want to prove the following theorem about the reduction behaviour of \texttt{plus}:
65plusReduces : (n:Nat) -> plus Z n = n
69We've written down the statement of the theorem as a type, in just the same way
70as we would write the type of a program. In fact there is no real distinction
71between proofs and programs. A proof, as far as we are concerned here, is
72merely a program with a precise enough type to guarantee a particular property
75We won't go into details here, but the Curry-Howard
76correspondence~\cite{howard} explains this relationship.
77The proof itself is trivial, because \texttt{plus Z n} normalises to \texttt{n}
78by the definition of \texttt{plus}:
85It is slightly harder if we try the arguments the other way, because plus is
86defined by recursion on its first argument. The proof also works by recursion
87on the first argument to \texttt{plus}, namely \texttt{n}.
90plusReducesZ : (n:Nat) -> n = plus n Z
92plusReducesZ (S k) = cong (plusReducesZ k)
96\texttt{cong} is a function defined in the library which states that
97equality respects function application:
100cong : {f : t -> u} -> a = b -> f a = f b
104We can do the same for the reduction behaviour of plus on successors:
107plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
108plusReducesS Z m = refl
109plusReducesS (S k) m = cong (plusReducesS k m)
113Even for trival theorems like these, the proofs are a little tricky to
114construct in one go. When things get even slightly more complicated, it becomes
115too much to think about to construct proofs in this 'batch mode'. \Idris{}
116therefore provides an interactive proof mode.
118\subsection{Interactive theorem proving}
120Instead of writing the proof in one go, we can use \Idris{}'s interactive
121proof mode. To do this, we write the general \emph{structure} of the proof,
122and use the interactive mode to complete the details. We'll be constructing
123the proof by \emph{induction}, so we write the cases for \texttt{Z} and
124\texttt{S}, with a recursive call in the \texttt{S} case giving the inductive
125hypothesis, and insert \emph{metavariables} for the rest of the definition:
128plusReducesZ' : (n:Nat) -> n = plus n Z
129plusReducesZ' Z = ?plusredZ_Z
130plusReducesZ' (S k) = let ih = plusReducesZ' k in
135On running \Idris{}, two global names are created, \texttt{plusredZ\_O} and
136\texttt{plusredZ\_S}, with no definition. We can use the \texttt{:m} command
137at the prompt to find out which metavariables are still to be solved (or, more
138precisely, which functions exist but have no definitions), then the
139\texttt{:t} command to see their types:
144 [plusredZ_S,plusredZ_Z]
149*theorems> :t plusredZ_Z
150plusredZ_Z : Z = plus Z Z
152*theorems> :t plusredZ_S
153plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
157The \texttt{:p} command enters interactive proof mode, which can be used to complete
158the missing definitions.
161*theorems> :p plusredZ_Z
163---------------------------------- (plusredZ_Z) --------
164{hole0} : Z = plus Z Z
168This gives us a list of premisses
169(above the line; there are none here) and the current goal (below the line;
170named \texttt{\{hole0\}} here).
171At the prompt we can enter tactics to direct the construction of the proof. In this case,
172we can normalise the goal with the \texttt{compute} tactic:
177---------------------------------- (plusredZ_Z) --------
182Now we have to prove that \texttt{Z} equals \texttt{Z}, which is easy to prove by
183\texttt{refl}. To apply a function, such as \texttt{refl}, we use \texttt{refine}
184which introduces subgoals for each of the function's explicit arguments (\texttt{refl}
188-plusredZ_Z> refine refl
189plusredZ_Z: no more goals
193Here, we could also have used the \texttt{trivial} tactic, which tries to refine by
194\texttt{refl}, and if that fails, tries to refine by each name in the local context.
195When a proof is complete, we use the \texttt{qed} tactic to add the proof to the
196global context, and remove the metavariable from the unsolved metavariables list.
197This also outputs a trace of the proof:
214The \texttt{:addproof} command, at the interactive prompt, will add the proof to
215the source file (effectively in an appendix).
216Let us now prove the other required lemma, \texttt{plusredZ\_S}:
219*theorems> :p plusredZ_S
221---------------------------------- (plusredZ_S) --------
222{hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
226In this case, the goal is a function type, using \texttt{k} (the argument accessible by
227pattern matching) and \texttt{ih} (the local variable containing the result of
228the recursive call). We can introduce these as premisses using the \texttt{intro} tactic
229twice (or \texttt{intros}, which introduces all arguments as premisses). This gives:
234---------------------------------- (plusredZ_S) --------
235{hole2} : S k = plus (S k) Z
239Since plus is defined is defined by recursion on its first argument, the term
240\texttt{plus (S k) Z} in the goal can be simplified, so we use
246---------------------------------- (plusredZ_S) --------
247{hole2} : S k = S (plus k Z)
251We know, from the type of \texttt{ih}, that \texttt{k = plus k Z}, so we would like to
252use this knowledge to replace \texttt{plus k Z} in the goal with \texttt{k}. We can
253achieve this with the \texttt{rewrite} tactic:
256-plusredZ_S> rewrite ih
260---------------------------------- (plusredZ_S) --------
267The \texttt{rewrite} tactic takes an equality proof as an argument, and tries to rewrite
268the goal using that proof. Here, it results in an equality which is trivially provable:
272plusredZ_S: no more goals
282Again, we can add this proof to the end of our source file using the \texttt{:addproof}
283command at the interactive prompt.
285\subsection{Totality Checking}
289If we really want to trust our proofs, it is important that they are defined by
290\emph{total} functions --- that is, a function which is defined for all
291possible inputs and is guaranteed to terminate. Otherwise we could construct an
292element of the empty type, from which we could prove anything:
295-- making use of 'hd' being partially defined
307Internally, \Idris{} checks every definition for totality, and we can check at
308the prompt with the \texttt{:total} command. We see that neither of the above
312*theorems> :total empty1
313possibly not total due to: empty1#hd
314 not total as there are missing cases
315*theorems> :total empty2
316possibly not total due to recursive path empty2
320Note the use of the word ``possibly'' --- a totality check can, of course,
321never be certain due to the undecidability of the halting problem. The check
322is, therefore, conservative. It is also possible (and indeed advisable, in the
323case of proofs) to mark functions as total so that it will be a compile time
324error for the totality check to fail:
330Type checking ./theorems.idr
331theorems.idr:25:empty2 is possibly not total due to recursive path empty2
335Reassuringly, our proof in Section \ref{sect:empty} that the zero and successor constructors
336are disjoint is total:
339*theorems> :total disjoint
344The totality check is, necessarily, conservative. To be recorded as total, a
345function \texttt{f} must:
348\item Cover all possible inputs
349\item Be \emph{well-founded} --- i.e. by the time a sequence of
350(possibly mutually) recursive calls reaches \texttt{f} again, it must
351be possible to show that one of its arguments has decreased.
352\item Not use any data types which are not \emph{strictly positive}
353\item Not call any non-total functions
356\subsubsection{Directives and Compiler Flags for Totality}
358By default, \Idris{} allows all definitions, whether total or not. However,
359it is desirable for functions to be total as far as possible, as this
360provides a guarantee that they provide a result for all possible inputs,
361in finite time. It is possible to make total functions a requirement,
365\item By using the \texttt{--total} compiler flag.
366\item By adding a \texttt{\%default total} directive to a source file.
367All definitions after this will be required to be total, unless
368explicitly flagged as \texttt{partial}.
372All functions \remph{after} a \texttt{\%default total} declaration are required
373to be total. Correspondingly, after a \texttt{\%default partial} declaration,
374the requirement is relaxed.
376Finally, the compiler flag \texttt{--warnpartial} causes \Idris{} to print
377a 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