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 -> Type where
12 odd : Parity (S (n + n))
14parity : (n:Nat) -> Parity n
20We'd like to implement this as follows:
22\begin{SaveVerbatim}{parfail}
24parity : (n:Nat) -> Parity n
26parity (S Z) = odd {n=Z}
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}
35This simply states that zero is even, one is odd, and recursively, the parity
36of \texttt{k+2} is the same as the parity of \texttt{k}.
37Explicitly marking the value of \texttt{n} in
38even and odd is necessary to help type inference. Unfortunately, the type
41\begin{SaveVerbatim}{parerror}
43views.idr:12:Can't unify Parity (plus (S j) (S j)) with
44Parity (S (S (plus j j)))
51is telling us that \texttt{(j+1)+(j+1)} and \texttt{2+j+j}
52do not normalise to the same value.
53This is because \texttt{plus} is defined by recursion on its first argument, and in the
54second value, there is a successor symbol on the second argument, so this will
55not help with reduction. These values are obviously equal --- how can we rewrite
56the program to fix this problem?
58\subsection{Provisional definitions}
60\emph{Provisional definitions} help with this problem by allowing us to defer the
61proof details until a later point. There are two main reasons why they are
65\item When \emph{prototyping}, it is useful to be able to test programs before
66finishing all the details of proofs.
67\item When \emph{reading} a program, it is often much clearer to defer the proof
68details so that they do not distract the reader from the underlying algorithm.
72Provisional definitions are written in the same way as ordinary definitions,
73except that they introduce the right hand side with a \texttt{?=} rathar than
75\texttt{parity} as follows:
77\begin{SaveVerbatim}{paritypro}
79parity : (n:Nat) -> Parity n
81parity (S Z) = odd {n=Z}
82parity (S (S k)) with (parity k)
83 parity (S (S (j + j))) | even ?= even {n=S j}
84 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
90When written in this form, instead of reporting a type error, \Idris{} will insert
91a metavariable standing for a theorem which will correct the type error. \Idris{}
92tells us we have two proof obligations, with names generated from the module and
95\begin{SaveVerbatim}{prometas}
99 [views.parity_lemma_2,views.parity_lemma_1]
105The first of these has the following type:
107\begin{SaveVerbatim}{prolem1}
109*views> :p views.parity_lemma_1
111---------------------------------- (views.parity_lemma_1) --------
112{hole0} : (j : Nat) -> (Parity (plus (S j) (S j))) -> Parity (S (S (j + j)))
114-views.parity_lemma_1>
120The two arguments are \texttt{j}, the variable in scope from the pattern match,
121and \texttt{value}, which is the value we gave in the right hand side of the
122provisional definition. Our goal is to rewrite the type so that we can use
124We can achieve this using the following theorem from
127\begin{SaveVerbatim}{plusnsm}
129plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
130 S (left + right) = left + (S right)
137After applying \texttt{intro} twice, we have:
139\begin{SaveVerbatim}{prolemii}
141-views.parity_lemma_1> intro
144 value : Parity (S (plus j (S j)))
145---------------------------------- (views.parity_lemma_1) --------
146{hole2} : Parity (S (S (j + j)))
152We need to use \texttt{compute} again to unfold the definition of \texttt{(+)}.
154\begin{SaveVerbatim}{prolemcomp}
156-views.parity_lemma_1> intro
159 value : Parity (S (plus j (S j)))
160---------------------------------- (views.parity_lemma_1) --------
161{hole2} : Parity (S (S (plus j j)))
167Then we apply the \texttt{plusSuccRightSucc} rewrite rule, symmetrically,
168to \texttt{j} and \texttt{j}, giving:
170\begin{SaveVerbatim}{prolemr}
172-views.parity_lemma_1> rewrite sym (plusSuccRightSucc j j)
175 value : Parity (S (plus j (S j)))
176---------------------------------- (views.parity_lemma_1) --------
177{hole3} : Parity (S (plus j (S j)))
183\texttt{sym} is a function, defined in the library, which reverses the order of the rewrite:
185\begin{SaveVerbatim}{sym}
194We can complete this proof using the \texttt{trivial} tactic, which finds
195\texttt{value} in the premisses. The proof of the second lemma proceeds in
198\subsection{Suspension of Disbelief}
200\Idris{} requires that proofs be complete before compiling programs (although
201evaluation at the prompt is possible without proof details). Sometimes,
202especially when prototyping, it is easier not to have to do this. It might even
203be beneficial to test programs before attempting to prove things about them ---
204if testing finds an error, you know you had better not waste your time proving
207Therefore, \Idris{} provides a built-in coercion function, which allows you to use
208a value of the incorrect types:
210\begin{SaveVerbatim}{believe}
218Obviously, this should be used with extreme caution. It is useful when prototyping, and
219can also be appropriate when asserting properties of external code (perhaps in an
220external C library). The ``proof'' of \texttt{views.parity\_lemma\_1} using this is:
222\begin{SaveVerbatim}{pladodgy}
224views.parity_lemma_2 = proof {
227 exact believe_me value;
234The \texttt{exact} tactic allows us to provide an exact value for the proof. In this case,
235we assert that the value we gave was correct.
237\subsection{Example: Binary numbers}
239Previously, we implemented conversion to binary numbers using the \texttt{Parity} view.
240Here, we show how to use the same view to implement a verified conversion to
242We begin by indexing binary numbers over their \texttt{Nat} equivalent. This is a common
243pattern, linking a representation (in this case \texttt{Binary}) with a meaning (in this
246\begin{SaveVerbatim}{bindef}
248data Binary : Nat -> Type where
250 bO : Binary n -> Binary (n + n)
251 bI : Binary n -> Binary (S (n + n))
257\texttt{bO} and \texttt{bI} take a binary number as an argument and effectively shift it one bit
258left, adding either a zero or one as the new least significant bit. The index,
259\texttt{n + n} or \texttt{S (n + n)} states the result that this left shift then add will
260have to the meaning of the number. This will result in a representation with
261the least significant bit at the front.
263Now a function which converts a Nat to binary will state, in the type, that the
264resulting binary number is a faithful representation of the original Nat:
266\begin{SaveVerbatim}{ntbty}
268natToBin : (n:Nat) -> Binary n
274The \texttt{Parity} view makes the definition fairly simple --- halving the
275number is effectively a right shift after all --- although we need to use a
276provisional definition in the odd case:
278\begin{SaveVerbatim}{ntbdef}
280natToBin : (n:Nat) -> Binary n
282natToBin (S k) with (parity k)
283 natToBin (S (j + j)) | even = bI (natToBin j)
284 natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))
290The problem with the odd case is the same as in the definition of \texttt{parity}, and
291the proof proceeds in the same way:
293\begin{SaveVerbatim}{ntboddprf}
295natToBin_lemma_1 = proof {
298 rewrite sym (plusSuccRightSucc j j);
306To finish, we'll implement a main program which reads an integer from the user and
309\begin{SaveVerbatim}{binmain}
312main = do putStr "Enter a number: "
314 print (natToBin (fromInteger (cast x)))
320For this to work, of course, we need a \texttt{Show} instance for \texttt{Binary n}:
322\begin{SaveVerbatim}{showbin}
324instance Show (Binary n) where
325 show (bO x) = show x ++ "0"
326 show (bI x) = show x ++ "1"
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list