git.iko.soy/Idris-dev
on da8b88a help sign in
Idris-dev/docs/tutorial/provisional.rst
268 lines 8.4 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 Can't unify
39 Parity (plus (S j) (S j))
40 with
41 Parity (S (S (plus j j)))
43 Specifically:
44 Can't unify
45 plus (S j) (S j)
46 with
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:
74When written in this form, instead of reporting a type error, Idris
75will insert a metavariable standing for a theorem which will correct the
76type error. Idris tells us we have two proof obligations, with names
77generated from the module and function names:
79.. code-block:: idris
81 *views> :m
82 Global metavariables:
83 [views.parity_lemma_2,views.parity_lemma_1]
85The first of these has the following type:
87.. code-block:: idris
89 *views> :p views.parity_lemma_1
91 ---------------------------------- (views.parity_lemma_1) --------
92 {hole0} : (j : Nat) -> (Parity (plus (S j) (S j))) -> Parity (S (S (plus j j)))
94 -views.parity_lemma_1>
96The two arguments are ``j``, the variable in scope from the pattern
97match, and ``value``, which is the value we gave in the right hand side
98of the provisional definition. Our goal is to rewrite the type so that
99we can use this value. We can achieve this using the following theorem
100from the prelude:
102.. code-block:: idris
104 plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
105 S (left + right) = left + (S right)
107We need to use ``compute`` again to unfold the definition of ``plus``:
109.. code-block:: idris
111 -views.parity_lemma_1> compute
114 ---------------------------------- (views.parity_lemma_1) --------
115 {hole0} : (j : Nat) -> (Parity (S (plus j (S j)))) -> Parity (S (S (plus j j)))
117After applying ``intros`` we have:
119.. code-block:: idris
121 -views.parity_lemma_1> intros
123 j : Nat
124 value : Parity (S (plus j (S j)))
125 ---------------------------------- (views.parity_lemma_1) --------
126 {hole2} : Parity (S (S (plus j j)))
128Then we apply the ``plusSuccRightSucc`` rewrite rule, symmetrically, to
129``j`` and ``j``, giving:
131.. code-block:: idris
133 -views.parity_lemma_1> rewrite sym (plusSuccRightSucc j j)
135 j : Nat
136 value : Parity (S (plus j (S j)))
137 ---------------------------------- (views.parity_lemma_1) --------
138 {hole3} : Parity (S (plus j (S j)))
140``sym`` is a function, defined in the library, which reverses the order
141of the rewrite:
143.. code-block:: idris
145 sym : l = r -> r = l
146 sym Refl = Refl
148We can complete this proof using the ``trivial`` tactic, which finds
149``value`` in the premises. The proof of the second lemma proceeds in
150exactly the same way.
152We can now test the ``natToBin`` function from Section :ref:`sect-nattobin`
153at the prompt. The number 42 is 101010 in binary. The binary digits are
154reversed:
156.. code-block:: idris
158 *views> show (natToBin 42)
159 "[False, True, False, True, False, True]" : String
161Suspension of Disbelief
162=======================
164Idris requires that proofs be complete before compiling programs
165(although evaluation at the prompt is possible without proof details).
166Sometimes, especially when prototyping, it is easier not to have to do
167this. It might even be beneficial to test programs before attempting to
168prove things about them — if testing finds an error, you know you had
169better not waste your time proving something!
171Therefore, Idris provides a built-in coercion function, which allows
172you to use a value of the incorrect types:
174.. code-block:: idris
176 believe_me : a -> b
178Obviously, this should be used with extreme caution. It is useful when
179prototyping, and can also be appropriate when asserting properties of
180external code (perhaps in an external C library). The “proof” of
181``views.parity_lemma_1`` using this is:
183.. code-block:: idris
185 views.parity_lemma_2 = proof {
186 intro;
187 intro;
188 exact believe_me value;
189 }
191The ``exact`` tactic allows us to provide an exact value for the proof.
192In this case, we assert that the value we gave was correct.
194Example: Binary numbers
195=======================
197Previously, we implemented conversion to binary numbers using the
198``Parity`` view. Here, we show how to use the same view to implement a
199verified conversion to binary. We begin by indexing binary numbers over
200their ``Nat`` equivalent. This is a common pattern, linking a
201representation (in this case ``Binary``) with a meaning (in this case
202``Nat``):
204.. code-block:: idris
206 data Binary : Nat -> Type where
207 bEnd : Binary Z
208 bO : Binary n -> Binary (n + n)
209 bI : Binary n -> Binary (S (n + n))
211``bO`` and ``bI`` take a binary number as an argument and effectively
212shift it one bit left, adding either a zero or one as the new least
213significant bit. The index, ``n + n`` or ``S (n + n)`` states the result
214that this left shift then add will have to the meaning of the number.
215This will result in a representation with the least significant bit at
216the front.
218Now a function which converts a Nat to binary will state, in the type,
219that the resulting binary number is a faithful representation of the
220original Nat:
222.. code-block:: idris
224 natToBin : (n:Nat) -> Binary n
226The ``Parity`` view makes the definition fairly simple — halving the
227number is effectively a right shift after all — although we need to use
228a provisional definition in the odd case:
230.. code-block:: idris
232 natToBin : (n:Nat) -> Binary n
233 natToBin Z = bEnd
234 natToBin (S k) with (parity k)
235 natToBin (S (j + j)) | even = bI (natToBin j)
236 natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))
238The problem with the odd case is the same as in the definition of
239``parity``, and the proof proceeds in the same way:
241.. code-block:: idris
243 natToBin_lemma_1 = proof {
244 intro;
245 intro;
246 rewrite sym (plusSuccRightSucc j j);
247 trivial;
248 }
250To finish, we’ll implement a main program which reads an integer from
251the user and outputs it in binary.
253.. code-block:: idris
255 main : IO ()
256 main = do putStr "Enter a number: "
257 x <- getLine
258 print (natToBin (fromInteger (cast x)))
260For this to work, of course, we need a ``Show`` instance for
261``Binary n``:
263.. code-block:: idris
265 instance Show (Binary n) where
266 show (bO x) = show x ++ "0"
267 show (bI x) = show x ++ "1"
268 show bEnd = ""