@@ -1 +1,307 @@
11\section{Provisional Definitions}
2+
3+Sometimes when programming with dependent types, the type required by the type
4+checker and the type of the program we have written will be different (in that
5+they do not have the same normal form), but nevertheless provably equal. For
6+example, recall the \texttt{parity} function:
7+
8+\begin{SaveVerbatim}{pardecl}
9+
10+data Parity : Nat -> Set where
11+ even : Parity (n + n)
12+ | odd : Parity (S (n + n));
13+
14+parity : (n:Nat) -> Parity n;
15+
16+\end{SaveVerbatim}
17+\useverb{pardecl}
18+
19+\noindent
20+We'd like to implement this as follows:
21+
22+\begin{SaveVerbatim}{parfail}
23+
24+parity : (n:Nat) -> Parity n;
25+parity O = even {n=O};
26+parity (S O) = odd {n=O};
27+parity (S (S k)) with parity k {
28+ parity (S (S (j + j))) | even = even {n=S j};
29+ parity (S (S (S (j + j)))) | odd = odd {n=S j};
30+}
31+
32+\end{SaveVerbatim}
33+\useverb{parfail}
34+
35+\noindent
36+this simply states that zero is even, one is odd, and recursively, the parity
37+of \texttt{k+2} is the same as the parity of \texttt{k}.
38+Explicitly marking the value of \texttt{n} in
39+even and odd is necessary to help type inference. Unfortunately, the type
40+checker rejects this:
41+
42+\begin{SaveVerbatim}{parerror}
43+
44+views.idr:12:Can't unify Parity (plus (S j) (S j)) with
45+Parity (S (S (plus j j)))
46+
47+\end{SaveVerbatim}
48+\useverb{parerror}
49+
50+\noindent
51+The type checker
52+is telling us that \texttt{(j+1)+(j+1)} and \texttt{2+j+j}
53+do not normalise to the same value.
54+This is because \texttt{plus} is defined by recursion on its first argument, and in the
55+second value, there is a successor symbol on the second argument, so this will
56+not help with reduction. These values are obviously equal --- how can we rewrite
57+the program to fix this problem?
58+
59+\subsection{Provisional definitions}
60+
61+\emph{Provisional definitions} help with this problem by allowing us to defer the
62+proof details until a later point. There are two main reasons why they are
63+useful.
64+
65+\begin{itemize}
66+\item When \emph{prototyping}, it is useful to be able to test programs before
67+finishing all the details of proofs.
68+\item When \emph{reading} a program, it is often much clearer to defer the proof
69+details so that they do not distract the reader from the underlying algorithm.
70+\end{itemize}
71+
72+\noindent
73+Provisional definitions are written in the same way as ordinary definitions,
74+except that they introduce the right hand side with a \texttt{?=} rathar than
75+\texttt{=}. We define
76+\texttt{parity} as follows:
77+
78+\begin{SaveVerbatim}{paritypro}
79+
80+parity : (n:Nat) -> Parity n;
81+parity O = even {n=O};
82+parity (S O) = odd {n=O};
83+parity (S (S k)) with parity k {
84+ parity (S (S (j + j))) | even ?= even {n=S j};
85+ parity (S (S (S (j + j)))) | odd ?= odd {n=S j};
86+}
87+
88+\end{SaveVerbatim}
89+\useverb{paritypro}
90+
91+When written in this form, instead of reporting a type error, \Idris{} will insert
92+a metavariable standing for a theorem which will correct the type error. \Idris{}
93+tells us we have two proof obligations, with names generated from the module and
94+function names:
95+
96+\begin{SaveVerbatim}{prometas}
97+
98+*views> :m
99+Global metavariables:
100+ [views.parity_lemma_2,views.parity_lemma_1]
101+
102+\end{SaveVerbatim}
103+\useverb{prometas}
104+
105+\noindent
106+The first of these has the following type:
107+
108+\begin{SaveVerbatim}{prolem1}
109+
110+*views> :p views.parity_lemma_1
111+
112+---------------------------------- (views.parity_lemma_1) --------
113+{hole0} : (j : Nat) -> (Parity (plus (S j) (S j))) -> Parity (S (S (plus j j)))
114+
115+-views.parity_lemma_1>
116+
117+\end{SaveVerbatim}
118+\useverb{prolem1}
119+
120+\noindent
121+The two arguments are \texttt{j}, the variable in scope from the pattern match,
122+and \texttt{value}, which is the value we gave in the right hand side of the
123+provisional definition. Our goal is to rewrite the type so that we can use
124+this value.
125+We can achieve this using the following theorem from
126+the prelude:
127+
128+\begin{SaveVerbatim}{plusnsm}
129+
130+plusn_Sm : (n : Nat) -> (m : Nat) -> (plus n (S m)) = S (plus n m);
131+
132+\end{SaveVerbatim}
133+\useverb{plusnsm}
134+
135+\noindent
136+After applying \texttt{intro} twice, we have:
137+
138+\begin{SaveVerbatim}{prolemii}
139+
140+-views.parity_lemma_1> intro
141+
142+ j : Nat
143+ value : Parity (S (plus j (S j)))
144+---------------------------------- (views.parity_lemma_1) --------
145+{hole2} : Parity (S (S (plus j j)))
146+
147+\end{SaveVerbatim}
148+\useverb{prolemii}
149+
150+\noindent
151+Then we apply the \texttt{plusn\_Sm} function to \texttt{j} and \texttt{j}, giving:
152+
153+\begin{SaveVerbatim}{prolemr}
154+
155+-views.parity_lemma_1> rewrite plusn_Sm j j
156+
157+ j : Nat
158+ value : Parity (S (plus j (S j)))
159+---------------------------------- (views.parity_lemma_1) --------
160+{hole3} : Parity (S (plus j (S j)))
161+
162+\end{SaveVerbatim}
163+\useverb{prolemr}
164+
165+\noindent
166+We can complete this proof using the \texttt{trivial} tactic, which finds
167+\texttt{value} in the premisses. The proof of the second lemma proceeds in
168+exactly the same way.
169+
170+\subsection{Suspension of Disbelief}
171+
172+\Idris{} requires that proofs be complete before compiling programs (although
173+evaluation at the prompt is possible without proof details). Sometimes,
174+especially when prototyping, it is easier not to have to do this. It might even
175+be beneficial to test programs before attempting to prove things about them ---
176+if testing finds an error, you know you had better not waste your time proving
177+something!
178+
179+Therefore, \Idris{} provides a built-in coercion function, which allows you to use
180+a value of the incorrect types:
181+
182+\begin{SaveVerbatim}{believe}
183+
184+believe_me : a -> b;
185+
186+\end{SaveVerbatim}
187+\useverb{believe}
188+
189+\noindent
190+Obviously, this should be used with extreme caution. It is useful when prototyping, and
191+can also be appropriate when asserting properties of external code (perhaps in an
192+external C library). The ``proof'' of \texttt{views.parity\_lemma\_1} using this is:
193+
194+\begin{SaveVerbatim}{pladodgy}
195+
196+views.parity_lemma_2 = proof {
197+ intro;
198+ intro;
199+ exact believe_me value;
200+};
201+
202+\end{SaveVerbatim}
203+\useverb{pladodgy}
204+
205+\noindent
206+The \texttt{exact} tactic allows us to provide an exact value for the proof. In this case,
207+we assert that the value we gave was correct.
208+
209+\subsection{Example: Binary numbers}
210+
211+Previously, we implemented conversion to binary numbers using the \texttt{Parity} view.
212+Here, we show how to use the same view to implement a verified conversion to
213+binary.
214+We begin by indexing binary numbers over their \texttt{Nat} equivalent. This is a common
215+pattern, linking a representation (in this case \texttt{Binary}) with a meaning (in this
216+case \texttt{Nat}):
217+
218+\begin{SaveVerbatim}{bindef}
219+
220+data Binary : Nat -> Set where
221+ bEnd : Binary O
222+ | bO : Binary n -> Binary (n + n)
223+ | bI : Binary n -> Binary (S (n + n));
224+
225+\end{SaveVerbatim}
226+\useverb{bindef}
227+
228+\texttt{bO} and \texttt{bI} take a binary number as an argument and effectively shift it one bit
229+left, adding either a zero or one as the new least significant bit. The index,
230+\texttt{n + n} or \texttt{S (n + n)} states the result that this left shift then add will
231+have to the meaning of the number. This will result in a representation with
232+the least significant bit at the front.
233+
234+Now a function which converts a Nat to binary will state, in the type, that the
235+resulting binary number is a faithful representation of the original Nat:
236+
237+\begin{SaveVerbatim}{ntbty}
238+
239+natToBin : (n:Nat) -> Binary n;
240+
241+\end{SaveVerbatim}
242+\useverb{ntbty}
243+
244+\noindent
245+The \texttt{Parity} view makes the definition fairly simple --- halving the
246+number is effectively a right shift after all --- although we need to use a
247+provisional definition in the odd case:
248+
249+\begin{SaveVerbatim}{ntbdef}
250+
251+natToBin : (n:Nat) -> Binary n;
252+natToBin O = bEnd;
253+natToBin (S k) with parity k {
254+ natToBin (S (j + j)) | even = bI (natToBin j);
255+ natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j));
256+}
257+
258+\end{SaveVerbatim}
259+\useverb{ntbdef}
260+
261+\noindent
262+The problem with the odd case is the same as in the definition of \texttt{parity}, and
263+the proof proceeds in the same way:
264+
265+\begin{SaveVerbatim}{ntboddprf}
266+
267+natToBin_lemma_1 = proof {
268+ intro;
269+ intro;
270+ rewrite plusn_Sm j j;
271+ trivial;
272+};
273+
274+\end{SaveVerbatim}
275+\useverb{ntboddprf}
276+
277+\noindent
278+To finish, we'll implement a main program which reads an integer from the user and
279+outputs it in binary.
280+
281+\begin{SaveVerbatim}{binmain}
282+
283+main : IO ();
284+main = do { putStr "Enter a number: ";
285+ x <- getLine;
286+ let n = prim__strToInt x;
287+ let b = natToBin (fromInteger n);
288+ print b;
289+ };
290+
291+\end{SaveVerbatim}
292+\useverb{binmain}
293+
294+\noindent
295+For this to work, of course, we need a \texttt{Show} instance for \texttt{Binary n}:
296+
297+\begin{SaveVerbatim}{showbin}
298+
299+instance Show (Binary n) where {
300+ show (bO x) = show x ++ "0";
301+ show (bI x) = show x ++ "1";
302+ show bEnd = "";
303+}
304+
305+\end{SaveVerbatim}
306+\useverb{showbin}
307+