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