@@ -1 +1,290 @@
1\section{Theorem Proving}
1\section{Theorem Proving}
5+\Idris{} allows propositional equalities to be declared, allowing theorems about
6+programs to be stated and proved. Equality is built in, but conceptually has
7+the following definition:
11+data (=) : a -> b -> Set where
18+Equalities can be proposed between any values of any types, but the only way to
19+construct a proof of equality is if values actually are equal. For example:
21+\begin{SaveVerbatim}{eqprf}
26+twoPlusTwo : 2 + 2 = 4;
32+\subsection{Simple Theorems}
34+When type checking dependent types, the type itself gets \emph{normalised}. So imagine
35+we want to prove the following theorem about the reduction behaviour of \texttt{plus}:
37+\begin{SaveVerbatim}{plusred}
39+plusReduces : (n:Nat) -> plus O n = n;
45+We've written down the statement of the theorem as a type, in just the same way
46+as we would write the type of a program. In fact there is no real distinction
47+between proofs and programs. A proof, as far as we are concerned here, is
48+merely a program with a precise enough type to guarantee a particular property
51+We won't go into details here, but the Curry-Howard
52+correspondence~\cite{howard} explains this relationship.
53+The proof itself is trivial, because \texttt{plus O n} normalises to \texttt{n}
54+by the definition of \texttt{plus}:
56+\begin{SaveVerbatim}{plusredp}
64+It is slightly harder if we try the arguments the other way, because plus is
65+defined by recursion on its first argument. The proof also works by recursion
66+on the first argument to \texttt{plus}, namely \texttt{n}.
68+\begin{SaveVerbatim}{plusRedO}
70+plusReducesO : (n:Nat) -> n = plus n O;
71+plusReducesO O = refl;
72+plusReducesO (S k) = eqRespS (plusReducesO k);
78+\texttt{eqRespS} is a function defined in the library which states that
79+equality respects successor:
81+\begin{SaveVerbatim}{resps}
83+eqRespS : m = n -> S m = S n;
89+We can do the same for the reduction behaviour of plus on successors:
91+\begin{SaveVerbatim}{plusRedS}
93+plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m);
94+plusReducesS O m = refl;
95+plusReducesS (S k) m = eqRespS (plusReducesS k m);
100+Even for trival theorems like these, the proofs are a little tricky to
101+construct in one go. When things get even slightly more complicated, it becomes
102+too much to think about to construct proofs in this 'batch mode'. \Idris{}
103+therefore provides an interactive proof mode.
105+\subsection{Interactive theorem proving}
107+Instead of writing the proof in one go, we can use \Idris{}'s interactive
108+proof mode. To do this, we write the general \emph{structure} of the proof,
109+and use the interactive mode to complete the details. We'll be constructing
110+the proof by \emph{induction}, so we write the cases for \texttt{O} and
111+\texttt{S}, with a recursive call in the \texttt{S} case giving the inductive
112+hypothesis, and insert \emph{metavariables} for the rest of the definition:
114+\begin{SaveVerbatim}{prOstruct}
116+plusReducesO' : (n:Nat) -> n = plus n O;
117+plusReducesO' O = ?plusredO_O;
118+plusReducesO' (S k) = let ih = plusReducesO' k in
125+On running \Idris{}, two global names are created, \texttt{plusredO\_O} and
126+\texttt{plusredO\_S}, with no definition. We can use the \texttt{:m} command
127+at the prompt to find out which metavariables are still to be solved (or, more
128+precisely, which functions exist but have no definitions). Then we can use the
129+\texttt{:t} command to see what their types are:
131+\begin{SaveVerbatim}{showmetas}
134+Global metavariables:
135+ [plusredO_S,plusredO_O]
139+\begin{SaveVerbatim}{metatypes}
141+*theorems> :t plusredO_O
142+plusredO_O : O = plus O O
144+*theorems> :t plusredO_S
145+plusredO_S : (k : Nat) -> (k = plus k O) -> S k = S (plus k O)
153+The \texttt{:p} command enters interactive proof mode, which can be used to complete
154+the missing definitions.
156+\begin{SaveVerbatim}{proveO}
158+*theorems> :p plusredO_O
160+---------------------------------- (plusredO_O) --------
161+{hole0} : O = plus O O
167+This gives us a list of premisses
168+(above the line; there are none here) and the current goal (below the line;
169+named \texttt{\{hole0\}} here).
170+At the prompt we can enter tactics to direct the construction of the proof. In this case,
171+we can normalise the goal with the \texttt{compute} tactic:
173+\begin{SaveVerbatim}{compute}
177+---------------------------------- (plusredO_O) --------
184+Now we have to prove that \texttt{O} equals \texttt{O}, which is easy to prove by
185+\texttt{refl}. To apply a function, such as \texttt{refl}, we use the \texttt{refine} tactic
186+which introduces subgoals for each of the function's explicit arguments (though \texttt{refl}
189+\begin{SaveVerbatim}{refrefl}
191+-plusredO_O> refine refl
192+plusredO_O: no more goals
198+Here, we could also have used the \texttt{trivial} tactic, which tries to refine by
199+\texttt{refl}, and if that fails, tries to refine by each name in the local context.
200+When a proof is complete, we use the \texttt{qed} tactic to add the proof to the
201+global context, and remove the metavariable from the unsolved metavariables list.
202+This also outputs a trace of the proof:
204+\begin{SaveVerbatim}{prOprooftrace}
213+Global metavariables:
217+\useverb{prOprooftrace}
220+The \texttt{:addproof} command, at the interactive prompt, will add the proof to
221+the source file (effectively in an appendix).
222+Let us now prove the other required lemma, \texttt{plusredO\_S}:
224+\begin{SaveVerbatim}{plusredOSprf}
226+*theorems> :p plusredO_S
228+---------------------------------- (plusredO_S) --------
229+{hole0} : (k : Nat) -> (k = plus k O) -> S k = S (plus k O)
232+\useverb{plusredOSprf}
235+In this case, the goal is a function type, using \texttt{k} (the argument accessible by
236+pattern matching) and \texttt{ih} (the local variable containing the result of
237+the recursive call). We can introduce these as premisses using the \texttt{intro} tactic
240+\begin{SaveVerbatim}{prSintros}
244+---------------------------------- (plusredO_S) --------
245+{hole2} : S k = S (plus k O)
251+We know, from the type of \texttt{ih}, that \texttt{k = plus k O}, so we would like to
252+use this knowledge to replace \texttt{plus k O} in the goal with \texttt{k}. We can
253+achieve this with the \texttt{rewrite} tactic:
255+\begin{SaveVerbatim}{}
257+-plusredO_S> rewrite ih
261+---------------------------------- (plusredO_S) --------
270+The \texttt{rewrite} tactic takes an equality proof as an argument, and tries to rewrite
271+the goal using that proof. Here, it results in an equality which is trivially provable:
273+\begin{SaveVerbatim}{prOStrace}
276+plusredO_S: no more goals
289+Again, we can add this proof to the end of our source file using the \texttt{:addproof}
290+command at the interactive prompt.