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{Simple Theorems}
34When type checking dependent types, the type itself gets \emph{normalised}. So imagine
35we want to prove the following theorem about the reduction behaviour of \texttt{plus}:
37\begin{SaveVerbatim}{plusred}
39plusReduces : (n:Nat) -> plus O n = n
45We've written down the statement of the theorem as a type, in just the same way
46as we would write the type of a program. In fact there is no real distinction
47between proofs and programs. A proof, as far as we are concerned here, is
48merely a program with a precise enough type to guarantee a particular property
51We won't go into details here, but the Curry-Howard
52correspondence~\cite{howard} explains this relationship.
53The proof itself is trivial, because \texttt{plus O n} normalises to \texttt{n}
54by the definition of \texttt{plus}:
56\begin{SaveVerbatim}{plusredp}
64It is slightly harder if we try the arguments the other way, because plus is
65defined by recursion on its first argument. The proof also works by recursion
66on the first argument to \texttt{plus}, namely \texttt{n}.
68\begin{SaveVerbatim}{plusRedO}
70plusReducesO : (n:Nat) -> n = plus n O
72plusReducesO (S k) = eqRespS (plusReducesO k)
78\texttt{eqRespS} is a function defined in the library which states that
79equality respects successor:
81\begin{SaveVerbatim}{resps}
83eqRespS : m = n -> S m = S n
89We can do the same for the reduction behaviour of plus on successors:
91\begin{SaveVerbatim}{plusRedS}
93plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
94plusReducesS O m = refl
95plusReducesS (S k) m = eqRespS (plusReducesS k m)
101Even for trival theorems like these, the proofs are a little tricky to
102construct in one go. When things get even slightly more complicated, it becomes
103too much to think about to construct proofs in this 'batch mode'. \Idris{}
104therefore provides an interactive proof mode.
106\subsection{Interactive theorem proving}
108Instead of writing the proof in one go, we can use \Idris{}'s interactive
109proof mode. To do this, we write the general \emph{structure} of the proof,
110and use the interactive mode to complete the details. We'll be constructing
111the proof by \emph{induction}, so we write the cases for \texttt{O} and
112\texttt{S}, with a recursive call in the \texttt{S} case giving the inductive
113hypothesis, and insert \emph{metavariables} for the rest of the definition:
115\begin{SaveVerbatim}{prOstruct}
117plusReducesO' : (n:Nat) -> n = plus n O
118plusReducesO' O = ?plusredO_O
119plusReducesO' (S k) = let ih = plusReducesO' k in
126On running \Idris{}, two global names are created, \texttt{plusredO\_O} and
127\texttt{plusredO\_S}, with no definition. We can use the \texttt{:m} command
128at the prompt to find out which metavariables are still to be solved (or, more
129precisely, which functions exist but have no definitions), then the
130\texttt{:t} command to see their types:
132\begin{SaveVerbatim}{showmetas}
136 [plusredO_S,plusredO_O]
140\begin{SaveVerbatim}{metatypes}
142*theorems> :t plusredO_O
143plusredO_O : O = plus O O
145*theorems> :t plusredO_S
146plusredO_S : (k : Nat) -> (k = plus k O) -> S k = S (plus k O)
154The \texttt{:p} command enters interactive proof mode, which can be used to complete
155the missing definitions.
157\begin{SaveVerbatim}{proveO}
159*theorems> :p plusredO_O
161---------------------------------- (plusredO_O) --------
162{hole0} : O = plus O O
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:
174\begin{SaveVerbatim}{compute}
178---------------------------------- (plusredO_O) --------
185Now we have to prove that \texttt{O} equals \texttt{O}, which is easy to prove by
186\texttt{refl}. To apply a function, such as \texttt{refl}, we use \texttt{refine}
187which introduces subgoals for each of the function's explicit arguments (\texttt{refl}
190\begin{SaveVerbatim}{refrefl}
192-plusredO_O> refine refl
193plusredO_O: no more goals
199Here, we could also have used the \texttt{trivial} tactic, which tries to refine by
200\texttt{refl}, and if that fails, tries to refine by each name in the local context.
201When a proof is complete, we use the \texttt{qed} tactic to add the proof to the
202global context, and remove the metavariable from the unsolved metavariables list.
203This also outputs a trace of the proof:
205\begin{SaveVerbatim}{prOprooftrace}
214\useverb{prOprooftrace}
216\begin{SaveVerbatim}{showmetasO}
226The \texttt{:addproof} command, at the interactive prompt, will add the proof to
227the source file (effectively in an appendix).
228Let us now prove the other required lemma, \texttt{plusredO\_S}:
230\begin{SaveVerbatim}{plusredOSprf}
232*theorems> :p plusredO_S
234---------------------------------- (plusredO_S) --------
235{hole0} : (k : Nat) -> (k = plus k O) -> S k = S (plus k O)
238\useverb{plusredOSprf}
241In this case, the goal is a function type, using \texttt{k} (the argument accessible by
242pattern matching) and \texttt{ih} (the local variable containing the result of
243the recursive call). We can introduce these as premisses using the \texttt{intro} tactic
244twice (or \texttt{intros}, which introduces all arguments as premisses). This gives:
246\begin{SaveVerbatim}{prSintros}
250---------------------------------- (plusredO_S) --------
251{hole2} : S k = S (plus k O)
257We know, from the type of \texttt{ih}, that \texttt{k = plus k O}, so we would like to
258use this knowledge to replace \texttt{plus k O} in the goal with \texttt{k}. We can
259achieve this with the \texttt{rewrite} tactic:
261\begin{SaveVerbatim}{}
263-plusredO_S> rewrite ih
267---------------------------------- (plusredO_S) --------
276The \texttt{rewrite} tactic takes an equality proof as an argument, and tries to rewrite
277the goal using that proof. Here, it results in an equality which is trivially provable:
279\begin{SaveVerbatim}{prOStrace}
282plusredO_S: no more goals
294Again, we can add this proof to the end of our source file using the \texttt{:addproof}
295command at the interactive prompt.
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