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 (plus 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 (plus left right) = plus 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 (plus j j)))
152Then we apply the \texttt{plusSuccRightSucc} rewrite rule, symmetrically,
153to \texttt{j} and \texttt{j}, giving:
155\begin{SaveVerbatim}{prolemr}
157-views.parity_lemma_1> rewrite sym (plusSuccRightSucc j j)
160 value : Parity (S (plus j (S j)))
161---------------------------------- (views.parity_lemma_1) --------
162{hole3} : Parity (S (plus j (S j)))
168\texttt{sym} is a function, defined in the library, which reverses the order of the rewrite:
170\begin{SaveVerbatim}{sym}
179We can complete this proof using the \texttt{trivial} tactic, which finds
180\texttt{value} in the premisses. The proof of the second lemma proceeds in
183\subsection{Suspension of Disbelief}
185\Idris{} requires that proofs be complete before compiling programs (although
186evaluation at the prompt is possible without proof details). Sometimes,
187especially when prototyping, it is easier not to have to do this. It might even
188be beneficial to test programs before attempting to prove things about them ---
189if testing finds an error, you know you had better not waste your time proving
192Therefore, \Idris{} provides a built-in coercion function, which allows you to use
193a value of the incorrect types:
195\begin{SaveVerbatim}{believe}
203Obviously, this should be used with extreme caution. It is useful when prototyping, and
204can also be appropriate when asserting properties of external code (perhaps in an
205external C library). The ``proof'' of \texttt{views.parity\_lemma\_1} using this is:
207\begin{SaveVerbatim}{pladodgy}
209views.parity_lemma_2 = proof {
212 exact believe_me value;
219The \texttt{exact} tactic allows us to provide an exact value for the proof. In this case,
220we assert that the value we gave was correct.
222\subsection{Example: Binary numbers}
224Previously, we implemented conversion to binary numbers using the \texttt{Parity} view.
225Here, we show how to use the same view to implement a verified conversion to
227We begin by indexing binary numbers over their \texttt{Nat} equivalent. This is a common
228pattern, linking a representation (in this case \texttt{Binary}) with a meaning (in this
231\begin{SaveVerbatim}{bindef}
233data Binary : Nat -> Type where
235 bO : Binary n -> Binary (n + n)
236 bI : Binary n -> Binary (S (n + n))
242\texttt{bO} and \texttt{bI} take a binary number as an argument and effectively shift it one bit
243left, adding either a zero or one as the new least significant bit. The index,
244\texttt{n + n} or \texttt{S (n + n)} states the result that this left shift then add will
245have to the meaning of the number. This will result in a representation with
246the least significant bit at the front.
248Now a function which converts a Nat to binary will state, in the type, that the
249resulting binary number is a faithful representation of the original Nat:
251\begin{SaveVerbatim}{ntbty}
253natToBin : (n:Nat) -> Binary n
259The \texttt{Parity} view makes the definition fairly simple --- halving the
260number is effectively a right shift after all --- although we need to use a
261provisional definition in the odd case:
263\begin{SaveVerbatim}{ntbdef}
265natToBin : (n:Nat) -> Binary n
267natToBin (S k) with (parity k)
268 natToBin (S (j + j)) | even = bI (natToBin j)
269 natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))
275The problem with the odd case is the same as in the definition of \texttt{parity}, and
276the proof proceeds in the same way:
278\begin{SaveVerbatim}{ntboddprf}
280natToBin_lemma_1 = proof {
283 rewrite sym (plusSuccRightSucc j j);
291To finish, we'll implement a main program which reads an integer from the user and
294\begin{SaveVerbatim}{binmain}
297main = do putStr "Enter a number: "
299 print (natToBin (fromInteger (cast x)))
305For this to work, of course, we need a \texttt{Show} instance for \texttt{Binary n}:
307\begin{SaveVerbatim}{showbin}
309instance Show (Binary n) where
310 show (bO x) = show x ++ "0"
311 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