git.iko.soy/Idris-dev
on master help sign in
Idris-dev/docs/tutorial/provisional.rst
277 lines 8.7 kB history raw
1.. _sect-provisional:
3***********************
4Provisional Definitions
5***********************
7Sometimes when programming with dependent types, the type required by
8the type checker and the type of the program we have written will be
9different (in that they do not have the same normal form), but
10nevertheless provably equal. For example, recall the ``parity``
11function:
13.. code-block:: idris
15 data Parity : Nat -> Type where
16 Even : Parity (n + n)
17 Odd : Parity (S (n + n))
19We’d like to implement this as follows:
21.. code-block:: idris
23 parity : (n:Nat) -> Parity n
24 parity Z = Even {n=Z}
25 parity (S Z) = Odd {n=Z}
26 parity (S (S k)) with (parity k)
27 parity (S (S (j + j))) | Even = Even {n=S j}
28 parity (S (S (S (j + j)))) | Odd = Odd {n=S j}
30This simply states that zero is even, one is odd, and recursively, the
31parity of ``k+2`` is the same as the parity of ``k``. Explicitly marking
32the value of ``n`` is even and odd is necessary to help type inference.
33Unfortunately, the type checker rejects this:
35::
37 viewsbroken.idr:12:10:When elaborating right hand side of ViewsBroken.parity:
38 Type mismatch between
39 Parity (plus (S j) (S j))
40 and
41 Parity (S (S (plus j j)))
43 Specifically:
44 Type mismatch between
45 plus (S j) (S j)
46 and
47 S (S (plus j j))
49The type checker is telling us that ``(j+1)+(j+1)`` and ``2+j+j`` do not
50normalise to the same value. This is because ``plus`` is defined by
51recursion on its first argument, and in the second value, there is a
52successor symbol on the second argument, so this will not help with
53reduction. These values are obviously equal — how can we rewrite the
54program to fix this problem?
56Provisional definitions
57=======================
59*Provisional definitions* help with this problem by allowing us to defer
60the proof details until a later point. There are two main reasons why
61they are useful.
63- When *prototyping*, it is useful to be able to test programs before
64 finishing all the details of proofs.
66- When *reading* a program, it is often much clearer to defer the proof
67 details so that they do not distract the reader from the underlying
68 algorithm.
70Provisional definitions are written in the same way as ordinary
71definitions, except that they introduce the right hand side with a
72``?=`` rather than ``=``. We define ``parity`` as follows:
74.. code-block:: idris
76 parity : (n:Nat) -> Parity n
77 parity Z = Even {n=Z}
78 parity (S Z) = Odd {n=Z}
79 parity (S (S k)) with (parity k)
80 parity (S (S (j + j))) | Even ?= Even {n=S j}
81 parity (S (S (S (j + j)))) | Odd ?= Odd {n=S j}
83When written in this form, instead of reporting a type error, Idris
84will insert a hole standing for a theorem which will correct the
85type error. Idris tells us we have two proof obligations, with names
86generated from the module and function names:
88.. code-block:: idris
90 *views> :m
91 Global holes:
92 [views.parity_lemma_2,views.parity_lemma_1]
94The first of these has the following type:
96.. code-block:: idris
98 *views> :p views.parity_lemma_1
100 ---------------------------------- (views.parity_lemma_1) --------
101 {hole0} : (j : Nat) -> (Parity (plus (S j) (S j))) -> Parity (S (S (plus j j)))
103 -views.parity_lemma_1>
105The two arguments are ``j``, the variable in scope from the pattern
106match, and ``value``, which is the value we gave in the right hand side
107of the provisional definition. Our goal is to rewrite the type so that
108we can use this value. We can achieve this using the following theorem
109from the prelude:
111.. code-block:: idris
113 plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
114 S (left + right) = left + (S right)
116We need to use ``compute`` again to unfold the definition of ``plus``:
118.. code-block:: idris
120 -views.parity_lemma_1> compute
123 ---------------------------------- (views.parity_lemma_1) --------
124 {hole0} : (j : Nat) -> (Parity (S (plus j (S j)))) -> Parity (S (S (plus j j)))
126After applying ``intros`` we have:
128.. code-block:: idris
130 -views.parity_lemma_1> intros
132 j : Nat
133 value : Parity (S (plus j (S j)))
134 ---------------------------------- (views.parity_lemma_1) --------
135 {hole2} : Parity (S (S (plus j j)))
137Then we apply the ``plusSuccRightSucc`` rewrite rule, symmetrically, to
138``j`` and ``j``, giving:
140.. code-block:: idris
142 -views.parity_lemma_1> rewrite sym (plusSuccRightSucc j j)
144 j : Nat
145 value : Parity (S (plus j (S j)))
146 ---------------------------------- (views.parity_lemma_1) --------
147 {hole3} : Parity (S (plus j (S j)))
149``sym`` is a function, defined in the library, which reverses the order
150of the rewrite:
152.. code-block:: idris
154 sym : l = r -> r = l
155 sym Refl = Refl
157We can complete this proof using the ``trivial`` tactic, which finds
158``value`` in the premises. The proof of the second lemma proceeds in
159exactly the same way.
161We can now test the ``natToBin`` function from Section :ref:`sect-nattobin`
162at the prompt. The number 42 is 101010 in binary. The binary digits are
163reversed:
165.. code-block:: idris
167 *views> show (natToBin 42)
168 "[False, True, False, True, False, True]" : String
170Suspension of Disbelief
171=======================
173Idris requires that proofs be complete before compiling programs
174(although evaluation at the prompt is possible without proof details).
175Sometimes, especially when prototyping, it is easier not to have to do
176this. It might even be beneficial to test programs before attempting to
177prove things about them — if testing finds an error, you know you had
178better not waste your time proving something!
180Therefore, Idris provides a built-in coercion function, which allows
181you to use a value of the incorrect types:
183.. code-block:: idris
185 believe_me : a -> b
187Obviously, this should be used with extreme caution. It is useful when
188prototyping, and can also be appropriate when asserting properties of
189external code (perhaps in an external C library). The “proof” of
190``views.parity_lemma_1`` using this is:
192.. code-block:: idris
194 views.parity_lemma_2 = proof {
195 intro;
196 intro;
197 exact believe_me value;
198 }
200The ``exact`` tactic allows us to provide an exact value for the proof.
201In this case, we assert that the value we gave was correct.
203Example: Binary numbers
204=======================
206Previously, we implemented conversion to binary numbers using the
207``Parity`` view. Here, we show how to use the same view to implement a
208verified conversion to binary. We begin by indexing binary numbers over
209their ``Nat`` equivalent. This is a common pattern, linking a
210representation (in this case ``Binary``) with a meaning (in this case
211``Nat``):
213.. code-block:: idris
215 data Binary : Nat -> Type where
216 BEnd : Binary Z
217 BO : Binary n -> Binary (n + n)
218 BI : Binary n -> Binary (S (n + n))
220``BO`` and ``BI`` take a binary number as an argument and effectively
221shift it one bit left, adding either a zero or one as the new least
222significant bit. The index, ``n + n`` or ``S (n + n)`` states the result
223that this left shift then add will have to the meaning of the number.
224This will result in a representation with the least significant bit at
225the front.
227Now a function which converts a Nat to binary will state, in the type,
228that the resulting binary number is a faithful representation of the
229original Nat:
231.. code-block:: idris
233 natToBin : (n:Nat) -> Binary n
235The ``Parity`` view makes the definition fairly simple — halving the
236number is effectively a right shift after all — although we need to use
237a provisional definition in the Odd case:
239.. code-block:: idris
241 natToBin : (n:Nat) -> Binary n
242 natToBin Z = BEnd
243 natToBin (S k) with (parity k)
244 natToBin (S (j + j)) | Even = BI (natToBin j)
245 natToBin (S (S (j + j))) | Odd ?= BO (natToBin (S j))
247The problem with the Odd case is the same as in the definition of
248``parity``, and the proof proceeds in the same way:
250.. code-block:: idris
252 natToBin_lemma_1 = proof {
253 intro;
254 intro;
255 rewrite sym (plusSuccRightSucc j j);
256 trivial;
257 }
259To finish, we’ll implement a main program which reads an integer from
260the user and outputs it in binary.
262.. code-block:: idris
264 main : IO ()
265 main = do putStr "Enter a number: "
266 x <- getLine
267 print (natToBin (fromInteger (cast x)))
269For this to work, of course, we need a ``Show`` implementation for
270``Binary n``:
272.. code-block:: idris
274 Show (Binary n) where
275 show (BO x) = show x ++ "0"
276 show (BI x) = show x ++ "1"
277 show BEnd = ""