10Idris allows propositional equalities to be declared, allowing theorems about
11programs to be stated and proved. Equality is built in, but conceptually
12has the following definition:
16 data (=) : a -> b -> Type where
19Equalities can be proposed between any values of any types, but the only
20way to construct a proof of equality is if values actually are equal.
28 twoPlusTwo : 2 + 2 = 4
36There is an empty type, :math:`\bot`, which has no constructors. It is
37therefore impossible to construct an element of the empty type, at least
38without using a partially defined or general recursive function (see
39Section :ref:`sect-totality` for more details). We can therefore use the
40empty type to prove that something is impossible, for example zero is
41never equal to a successor:
45 disjoint : (n : Nat) -> Z = S n -> Void
46 disjoint n p = replace {P = disjointTy} p ()
48 disjointTy : Nat -> Type
50 disjointTy (S k) = Void
52There is no need to worry too much about how this function works —
53essentially, it applies the library function ``replace``, which uses an
54equality proof to transform a predicate. Here we use it to transform a
55value of a type which can exist, the empty tuple, to a value of a type
56which can’t, by using a proof of something which can’t exist.
58Once we have an element of the empty type, we can prove anything.
59``void`` is defined in the library, to assist with proofs by
69When type checking dependent types, the type itself gets *normalised*.
70So imagine we want to prove the following theorem about the reduction
75 plusReduces : (n:Nat) -> plus Z n = n
77We’ve written down the statement of the theorem as a type, in just the
78same way as we would write the type of a program. In fact there is no
79real distinction between proofs and programs. A proof, as far as we are
80concerned here, is merely a program with a precise enough type to
81guarantee a particular property of interest.
83We won’t go into details here, but the Curry-Howard correspondence [1]_
84explains this relationship. The proof itself is trivial, because
85``plus Z n`` normalises to ``n`` by the definition of ``plus``:
91It is slightly harder if we try the arguments the other way, because
92plus is defined by recursion on its first argument. The proof also works
93by recursion on the first argument to ``plus``, namely ``n``.
97 plusReducesZ : (n:Nat) -> n = plus n Z
99 plusReducesZ (S k) = cong (plusReducesZ k)
101``cong`` is a function defined in the library which states that equality
102respects function application:
106 cong : {f : t -> u} -> a = b -> f a = f b
108We can do the same for the reduction behaviour of plus on successors:
112 plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
113 plusReducesS Z m = Refl
114 plusReducesS (S k) m = cong (plusReducesS k m)
116Even for trivial theorems like these, the proofs are a little tricky to
117construct in one go. When things get even slightly more complicated, it
118becomes too much to think about to construct proofs in this ‘batch
121Idris provides interactive editing capabilities, which can help with
122building proofs. For more details on building proofs interactively in
123an editor, see :ref:`proofs-index`.
130The need to prove theorems can arise naturally in practice. For example,
131previously (:ref:`sec-views`) we implemented ``natToBin`` using a function
136 parity : (n:Nat) -> Parity n
138However, we didn't provide a definition for ``parity``. We might expect it
139to look something like the following:
143 parity : (n:Nat) -> Parity n
144 parity Z = Even {n=Z}
145 parity (S Z) = Odd {n=Z}
146 parity (S (S k)) with (parity k)
147 parity (S (S (j + j))) | Even = Even {n=S j}
148 parity (S (S (S (j + j)))) | Odd = Odd {n=S j}
150Unfortunately, this fails with a type error:
154 When checking right hand side of with block in views.parity with expected type
155 Parity (S (S (j + j)))
157 Type mismatch between
158 Parity (S j + S j) (Type of Even)
160 Parity (S (S (plus j j))) (Expected type)
162The problem is that normalising ``S j + S j``, in the type of ``Even``
163doesn't result in what we need for the type of the right hand side of
164``Parity``. We know that ``S (S (plus j j))`` is going to be equal to
165``S j + S j``, but we need to explain it to Idris with a proof. We can
166begin by adding some *holes* (see :ref:`sect-holes`) to the definition:
170 parity : (n:Nat) -> Parity n
171 parity Z = Even {n=Z}
172 parity (S Z) = Odd {n=Z}
173 parity (S (S k)) with (parity k)
174 parity (S (S (j + j))) | Even = let result = Even {n=S j} in
176 parity (S (S (S (j + j)))) | Odd = let result = Odd {n=S j} in
179Checking the type of ``helpEven`` shows us what we need to prove for the
185 result : Parity (S (plus j (S j)))
186 --------------------------------------
187 helpEven : Parity (S (S (plus j j)))
189We can therefore write a helper function to *rewrite* the type to the form
194 helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
195 helpEven j p = rewrite plusSuccRightSucc j j in p
197The ``rewrite ... in`` syntax allows you to change the required type of an
198expression by rewriting it according to an equality proof. Here, we have
199used ``plusSuccRightSucc``, which has the following type:
203 plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right
205We can see the effect of ``rewrite`` by replacing the right hand side of
206``helpEven`` with a hole, and working step by step. Beginning with the following:
210 helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
211 helpEven j p = ?helpEven_rhs
213We can look at the type of ``helpEven_rhs``:
218 p : Parity (S (plus j (S j)))
219 --------------------------------------
220 helpEven_rhs : Parity (S (S (plus j j)))
222Then we can ``rewrite`` by applying ``plusSuccRightSucc j j``, which gives
223an equation ``S (j + j) = j + S j``, thus replacing ``S (j + j)`` (or,
224in this case, ``S (plus j j)`` since ``S (j + j)`` reduces to that) in the
225type with ``j + S j``:
229 helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
230 helpEven j p = rewrite plusSuccRightSucc j j in ?helpEven_rhs
232Checking the type of ``helpEven_rhs`` now shows what has happened, including
233the type of the equation we just used (as the type of ``_rewrite_rule``):
238 p : Parity (S (plus j (S j)))
239 _rewrite_rule : S (plus j j) = plus j (S j)
240 --------------------------------------
241 helpEven_rhs : Parity (S (plus j (S j)))
243Using ``rewrite`` and another helper for the ``Odd`` case, we can complete
244``parity`` as follows:
248 helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
249 helpEven j p = rewrite plusSuccRightSucc j j in p
251 helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))
252 helpOdd j p = rewrite plusSuccRightSucc j j in p
254 parity : (n:Nat) -> Parity n
255 parity Z = Even {n=Z}
256 parity (S Z) = Odd {n=Z}
257 parity (S (S k)) with (parity k)
258 parity (S (S (j + j))) | Even = helpEven j (Even {n = S j})
259 parity (S (S (S (j + j)))) | Odd = helpOdd j (Odd {n = S j})
261Full details of ``rewrite`` are beyond the scope of this introductory tutorial,
262but it is covered in the theorem proving tutorial (see :ref:`proofs-index`).
269If we really want to trust our proofs, it is important that they are
270defined by *total* functions — that is, a function which is defined for
271all possible inputs and is guaranteed to terminate. Otherwise we could
272construct an element of the empty type, from which we could prove
277 -- making use of 'hd' being partially defined
287Internally, Idris checks every definition for totality, and we can check at
288the prompt with the ``:total`` command. We see that neither of the above
293 *Theorems> :total empty1
294 possibly not total due to: empty1#hd
295 not total as there are missing cases
296 *Theorems> :total empty2
297 possibly not total due to recursive path empty2
299Note the use of the word “possibly” — a totality check can, of course,
300never be certain due to the undecidability of the halting problem. The
301check is, therefore, conservative. It is also possible (and indeed
302advisable, in the case of proofs) to mark functions as total so that it
303will be a compile time error for the totality check to fail:
312 Type checking ./theorems.idr
313 theorems.idr:25:empty2 is possibly not total due to recursive path empty2
315Reassuringly, our proof in Section :ref:`sect-empty` that the zero and
316successor constructors are disjoint is total:
320 *theorems> :total disjoint
323The totality check is, necessarily, conservative. To be recorded as
324total, a function ``f`` must:
326- Cover all possible inputs
328- Be *well-founded* — i.e. by the time a sequence of (possibly
329 mutually) recursive calls reaches ``f`` again, it must be possible to
330 show that one of its arguments has decreased.
332- Not use any data types which are not *strictly positive*
334- Not call any non-total functions
336Directives and Compiler Flags for Totality
337------------------------------------------
339By default, Idris allows all well-typed definitions, whether total or not.
340However, it is desirable for functions to be total as far as possible, as this
341provides a guarantee that they provide a result for all possible inputs, in
342finite time. It is possible to make total functions a requirement, either:
344- By using the ``--total`` compiler flag.
346- By adding a ``%default total`` directive to a source file. All
347 definitions after this will be required to be total, unless
348 explicitly flagged as ``partial``.
350All functions *after* a ``%default total`` declaration are required to
351be total. Correspondingly, after a ``%default partial`` declaration, the
352requirement is relaxed.
354Finally, the compiler flag ``--warnpartial`` causes to print a warning
355for any undeclared partial function.
357Totality checking issues
358------------------------
360Please note that the totality checker is not perfect! Firstly, it is
361necessarily conservative due to the undecidability of the halting
362problem, so many programs which *are* total will not be detected as
363such. Secondly, the current implementation has had limited effort put
364into it so far, so there may still be cases where it believes a function
365is total which is not. Do not rely on it for your proofs yet!
370In cases where you believe a program is total, but Idris does not agree, it is
371possible to give hints to the checker to give more detail for a termination
372argument. The checker works by ensuring that all chains of recursive calls
373eventually lead to one of the arguments decreasing towards a base case, but
374sometimes this is hard to spot. For example, the following definition cannot be
375checked as ``total`` because the checker cannot decide that ``filter (< x) xs``
376will always be smaller than ``(x :: xs)``:
380 qsort : Ord a => List a -> List a
383 = qsort (filter (< x) xs) ++
384 (x :: qsort (filter (>= x) xs))
386The function ``assert_smaller``, defined in the Prelude, is intended to
391 assert_smaller : a -> a -> a
392 assert_smaller x y = y
394It simply evaluates to its second argument, but also asserts to the
395totality checker that ``y`` is structurally smaller than ``x``. This can
396be used to explain the reasoning for totality if the checker cannot work
397it out itself. The above example can now be written as:
402 qsort : Ord a => List a -> List a
405 = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
406 (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))
408The expression ``assert_smaller (x :: xs) (filter (<= x) xs)`` asserts
409that the result of the filter will always be smaller than the pattern
412In more extreme cases, the function ``assert_total`` marks a
413subexpression as always being total:
417 assert_total : a -> a
420In general, this function should be avoided, but it can be very useful
421when reasoning about primitives or externally defined functions (for
422example from a C library) where totality can be shown by an external
426.. [1] Timothy G. Griffin. 1989. A formulae-as-type notion of
427 control. In Proceedings of the 17th ACM SIGPLAN-SIGACT
428 symposium on Principles of programming languages (POPL
429 '90). ACM, New York, NY, USA, 47-58. DOI=10.1145/96709.96714
430 http://doi.acm.org/10.1145/96709.96714
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