git.iko.soy/Idris-dev
on 357cd83 help sign in
Idris-dev/tutorial/content/provisional.tex
284 lines 8.7 kB history raw
1\section{Provisional Definitions}
3\label{sect:provisional}
5Sometimes when programming with dependent types, the type required by the type
6checker and the type of the program we have written will be different (in that
7they do not have the same normal form), but nevertheless provably equal. For
8example, recall the \texttt{parity} function:
10\begin{code}
11data Parity : Nat -> Type where
12 even : Parity (n + n)
13 odd : Parity (S (n + n))
15parity : (n:Nat) -> Parity n
16\end{code}
18\noindent
19We'd like to implement this as follows:
21\begin{code}
22parity : (n:Nat) -> Parity n
23parity Z = even {n=Z}
24parity (S Z) = odd {n=Z}
25parity (S (S k)) with (parity k)
26 parity (S (S (j + j))) | even = even {n=S j}
27 parity (S (S (S (j + j)))) | odd = odd {n=S j}
28\end{code}
30\noindent
31This simply states that zero is even, one is odd, and recursively, the parity
32of \texttt{k+2} is the same as the parity of \texttt{k}.
33Explicitly marking the value of \texttt{n} in
34even and odd is necessary to help type inference. Unfortunately, the type
35checker rejects this:
37\begin{code}
38views.idr:12:Can't unify Parity (plus (S j) (S j)) with
39Parity (S (S (plus j j)))
40\end{code}
42\noindent
43The type checker
44is telling us that \texttt{(j+1)+(j+1)} and \texttt{2+j+j}
45do not normalise to the same value.
46This is because \texttt{plus} is defined by recursion on its first argument, and in the
47second value, there is a successor symbol on the second argument, so this will
48not help with reduction. These values are obviously equal --- how can we rewrite the program to fix this problem?
50\subsection{Provisional definitions}
52\emph{Provisional definitions} help with this problem by allowing us to defer the
53proof details until a later point. There are two main reasons why they are
54useful.
56\begin{itemize}
57\item When \emph{prototyping}, it is useful to be able to test programs before
58finishing all the details of proofs.
59\item When \emph{reading} a program, it is often much clearer to defer the proof
60details so that they do not distract the reader from the underlying algorithm.
61\end{itemize}
63\noindent
64Provisional definitions are written in the same way as ordinary definitions,
65except that they introduce the right hand side with a \texttt{?=} rathar than
66\texttt{=}. We define
67\texttt{parity} as follows:
69\begin{code}
70parity : (n:Nat) -> Parity n
71parity Z = even {n=Z}
72parity (S Z) = odd {n=Z}
73parity (S (S k)) with (parity k)
74 parity (S (S (j + j))) | even ?= even {n=S j}
75 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
76\end{code}
78\noindent
79When written in this form, instead of reporting a type error, \Idris{} will insert
80a metavariable standing for a theorem which will correct the type error. \Idris{}
81tells us we have two proof obligations, with names generated from the module and
82function names:
84\begin{lstlisting}
85*views> :m
86Global metavariables:
87 [views.parity_lemma_2,views.parity_lemma_1]
88\end{lstlisting}
90\noindent
91The first of these has the following type:
93\begin{lstlisting}
94*views> :p views.parity_lemma_1
96---------------------------------- (views.parity_lemma_1) --------
97{hole0} : (j : Nat) -> (Parity (plus (S j) (S j))) -> Parity (S (S (j + j)))
99-views.parity_lemma_1>
100\end{lstlisting}
102\noindent
103The two arguments are \texttt{j}, the variable in scope from the pattern match,
104and \texttt{value}, which is the value we gave in the right hand side of the
105provisional definition. Our goal is to rewrite the type so that we can use
106this value.
107We can achieve this using the following theorem from
108the prelude:
110\begin{code}
111plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
112 S (left + right) = left + (S right)
113\end{code}
115\noindent
116After applying \texttt{intro} twice, we have:
118\begin{lstlisting}
119-views.parity_lemma_1> intro
121 j : Nat
122 value : Parity (S (plus j (S j)))
123---------------------------------- (views.parity_lemma_1) --------
124{hole2} : Parity (S (S (j + j)))
125\end{lstlisting}
127\noindent
128We need to use \texttt{compute} again to unfold the definition of \texttt{(+)}.
130\begin{lstlisting}
131-views.parity_lemma_1> intro
133 j : Nat
134 value : Parity (S (plus j (S j)))
135---------------------------------- (views.parity_lemma_1) --------
136{hole2} : Parity (S (S (plus j j)))
137\end{lstlisting}
139\noindent
140Then we apply the \texttt{plusSuccRightSucc} rewrite rule, symmetrically,
141to \texttt{j} and \texttt{j}, giving:
143\begin{lstlisting}
144-views.parity_lemma_1> rewrite sym (plusSuccRightSucc j j)
146 j : Nat
147 value : Parity (S (plus j (S j)))
148---------------------------------- (views.parity_lemma_1) --------
149{hole3} : Parity (S (plus j (S j)))
150\end{lstlisting}
152\noindent
153\texttt{sym} is a function, defined in the library, which reverses the order of the rewrite:
155\begin{lstlisting}
156sym : l = r -> r = l
157sym refl = refl
158\end{lstlisting}
160\noindent
161We can complete this proof using the \texttt{trivial} tactic, which finds
162\texttt{value} in the premisses. The proof of the second lemma proceeds in
163exactly the same way.
165We can now test the \texttt{natToBin} function from Section
166\ref{sect:nattobin} at the prompt. 42 is 101010 in
167binary. The binary digits are reversed:
169\begin{lstlisting}
170*views> show (natToBin 42)
171"[False, True, False, True, False, True]" : String
172\end{lstlisting}
175\subsection{Suspension of Disbelief}
177\Idris{} requires that proofs be complete before compiling programs (although
178evaluation at the prompt is possible without proof details). Sometimes,
179especially when prototyping, it is easier not to have to do this. It might even
180be beneficial to test programs before attempting to prove things about them ---
181if testing finds an error, you know you had better not waste your time proving
182something!
184Therefore, \Idris{} provides a built-in coercion function, which allows you to use
185a value of the incorrect types:
187\begin{code}
188believe_me : a -> b
189\end{code}
191\noindent
192Obviously, this should be used with extreme caution. It is useful when prototyping, and
193can also be appropriate when asserting properties of external code (perhaps in an
194external C library). The ``proof'' of \texttt{views.parity\_lemma\_1} using this is:
196\begin{lstlisting}
197views.parity_lemma_2 = proof {
198 intro;
199 intro;
200 exact believe_me value;
202\end{lstlisting}
204\noindent
205The \texttt{exact} tactic allows us to provide an exact value for the proof. In this case,
206we assert that the value we gave was correct.
208\subsection{Example: Binary numbers}
210Previously, we implemented conversion to binary numbers using the \texttt{Parity} view.
211Here, we show how to use the same view to implement a verified conversion to
212binary.
213We begin by indexing binary numbers over their \texttt{Nat} equivalent. This is a common
214pattern, linking a representation (in this case \texttt{Binary}) with a meaning (in this
215case \texttt{Nat}):
217\begin{code}
218data Binary : Nat -> Type where
219 bEnd : Binary Z
220 bO : Binary n -> Binary (n + n)
221 bI : Binary n -> Binary (S (n + n))
222\end{code}
224\noindent
225\texttt{bO} and \texttt{bI} take a binary number as an argument and effectively shift it one bit
226left, adding either a zero or one as the new least significant bit. The index,
227\texttt{n + n} or \texttt{S (n + n)} states the result that this left shift then add will
228have to the meaning of the number. This will result in a representation with
229the least significant bit at the front.
231Now a function which converts a Nat to binary will state, in the type, that the
232resulting binary number is a faithful representation of the original Nat:
234\begin{code}
235natToBin : (n:Nat) -> Binary n
236\end{code}
238\noindent
239The \texttt{Parity} view makes the definition fairly simple --- halving the
240number is effectively a right shift after all --- although we need to use a
241provisional definition in the odd case:
243\begin{code}
244natToBin : (n:Nat) -> Binary n
245natToBin Z = bEnd
246natToBin (S k) with (parity k)
247 natToBin (S (j + j)) | even = bI (natToBin j)
248 natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))
249\end{code}
251\noindent
252The problem with the odd case is the same as in the definition of \texttt{parity}, and
253the proof proceeds in the same way:
255\begin{code}
256natToBin_lemma_1 = proof {
257 intro;
258 intro;
259 rewrite sym (plusSuccRightSucc j j);
260 trivial;
262\end{code}
264\noindent
265To finish, we'll implement a main program which reads an integer from the user and
266outputs it in binary.
268\begin{code}
269main : IO ()
270main = do putStr "Enter a number: "
271 x <- getLine
272 print (natToBin (fromInteger (cast x)))
273\end{code}
275\noindent
276For this to work, of course, we need a \texttt{Show} instance for \texttt{Binary n}:
278\begin{code}
279instance Show (Binary n) where
280 show (bO x) = show x ++ "0"
281 show (bI x) = show x ++ "1"
282 show bEnd = ""
283\end{code}