@@ -1 +1,290 @@
11\section{Theorem Proving}
2+
3+\subsection{Equality}
4+
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:
8+
9+\begin{SaveVerbatim}{}
10+
11+data (=) : a -> b -> Set where
12+ refl : x = x;
13+
14+\end{SaveVerbatim}
15+\useverb{}
16+
17+\noindent
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:
20+
21+\begin{SaveVerbatim}{eqprf}
22+
23+fiveIsFive : 5 = 5;
24+fiveIsFive = refl;
25+
26+twoPlusTwo : 2 + 2 = 4;
27+twoPlusTwo = refl;
28+
29+\end{SaveVerbatim}
30+\useverb{eqprf}
31+
32+\subsection{Simple Theorems}
33+
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}:
36+
37+\begin{SaveVerbatim}{plusred}
38+
39+plusReduces : (n:Nat) -> plus O n = n;
40+
41+\end{SaveVerbatim}
42+\useverb{plusred}
43+
44+\noindent
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
49+of interest.
50+
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}:
55+
56+\begin{SaveVerbatim}{plusredp}
57+
58+plusReduces n = refl;
59+
60+\end{SaveVerbatim}
61+\useverb{plusredp}
62+
63+\noindent
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}.
67+
68+\begin{SaveVerbatim}{plusRedO}
69+
70+plusReducesO : (n:Nat) -> n = plus n O;
71+plusReducesO O = refl;
72+plusReducesO (S k) = eqRespS (plusReducesO k);
73+
74+\end{SaveVerbatim}
75+\useverb{plusRedO}
76+
77+\noindent
78+\texttt{eqRespS} is a function defined in the library which states that
79+equality respects successor:
80+
81+\begin{SaveVerbatim}{resps}
82+
83+eqRespS : m = n -> S m = S n;
84+
85+\end{SaveVerbatim}
86+\useverb{resps}
87+
88+\noindent
89+We can do the same for the reduction behaviour of plus on successors:
90+
91+\begin{SaveVerbatim}{plusRedS}
92+
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);
96+
97+\end{SaveVerbatim}
98+\useverb{plusRedS}
99+
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.
104+
105+\subsection{Interactive theorem proving}
106+
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:
113+
114+\begin{SaveVerbatim}{prOstruct}
115+
116+plusReducesO' : (n:Nat) -> n = plus n O;
117+plusReducesO' O = ?plusredO_O;
118+plusReducesO' (S k) = let ih = plusReducesO' k in
119+ ?plusredO_S;
120+
121+\end{SaveVerbatim}
122+\useverb{prOstruct}
123+
124+\noindent
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:
130+
131+\begin{SaveVerbatim}{showmetas}
132+
133+*theorems> :m
134+Global metavariables:
135+ [plusredO_S,plusredO_O]
136+
137+\end{SaveVerbatim}
138+
139+\begin{SaveVerbatim}{metatypes}
140+
141+*theorems> :t plusredO_O
142+plusredO_O : O = plus O O
143+
144+*theorems> :t plusredO_S
145+plusredO_S : (k : Nat) -> (k = plus k O) -> S k = S (plus k O)
146+
147+\end{SaveVerbatim}
148+\useverb{showmetas}
149+
150+\useverb{metatypes}
151+
152+\noindent
153+The \texttt{:p} command enters interactive proof mode, which can be used to complete
154+the missing definitions.
155+
156+\begin{SaveVerbatim}{proveO}
157+
158+*theorems> :p plusredO_O
159+
160+---------------------------------- (plusredO_O) --------
161+{hole0} : O = plus O O
162+
163+\end{SaveVerbatim}
164+\useverb{proveO}
165+
166+\noindent
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:
172+
173+\begin{SaveVerbatim}{compute}
174+
175+-plusredO_O> compute
176+
177+---------------------------------- (plusredO_O) --------
178+{hole0} : O = O
179+
180+\end{SaveVerbatim}
181+\useverb{compute}
182+
183+\noindent
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}
187+has none):
188+
189+\begin{SaveVerbatim}{refrefl}
190+
191+-plusredO_O> refine refl
192+plusredO_O: no more goals
193+
194+\end{SaveVerbatim}
195+\useverb{refrefl}
196+
197+\noindent
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:
203+
204+\begin{SaveVerbatim}{prOprooftrace}
205+
206+-plusredO_O> qed
207+plusredO_O = proof {
208+ compute;
209+ refine refl;
210+};
211+
212+*theorems> :m
213+Global metavariables:
214+ [plusredO_S]
215+
216+\end{SaveVerbatim}
217+\useverb{prOprooftrace}
218+
219+\noindent
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}:
223+
224+\begin{SaveVerbatim}{plusredOSprf}
225+
226+*theorems> :p plusredO_S
227+
228+---------------------------------- (plusredO_S) --------
229+{hole0} : (k : Nat) -> (k = plus k O) -> S k = S (plus k O)
230+
231+\end{SaveVerbatim}
232+\useverb{plusredOSprf}
233+
234+\noindent
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
238+twice. This gives:
239+
240+\begin{SaveVerbatim}{prSintros}
241+
242+ k : Nat
243+ ih : k = plus k O
244+---------------------------------- (plusredO_S) --------
245+{hole2} : S k = S (plus k O)
246+
247+\end{SaveVerbatim}
248+\useverb{prSintros}
249+
250+\noindent
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:
254+
255+\begin{SaveVerbatim}{}
256+
257+-plusredO_S> rewrite ih
258+
259+ k : Nat
260+ ih : k = plus k O
261+---------------------------------- (plusredO_S) --------
262+{hole3} : S k = S k
263+
264+-plusredO_S>
265+
266+\end{SaveVerbatim}
267+\useverb{}
268+
269+\noindent
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:
272+
273+\begin{SaveVerbatim}{prOStrace}
274+
275+-plusredO_S> trivial
276+plusredO_S: no more goals
277+-plusredO_S> qed
278+plusredO_S = proof {
279+ intro;
280+ intro;
281+ rewrite ih;
282+ trivial;
283+};
284+
285+\end{SaveVerbatim}
286+\useverb{prOStrace}
287+
288+\noindent
289+Again, we can add this proof to the end of our source file using the \texttt{:addproof}
290+command at the interactive prompt.