git.iko.soy/Idris-dev
on cf47310 help sign in
Idris-dev/docs/tutorial/theorems.rst
291 lines 9.5 kB history raw
1.. _sect-theorems:
3***************
4Theorem Proving
5***************
7Equality
8========
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:
14.. code-block:: idris
16 data (=) : a -> b -> Type where
17 Refl : x = x
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.
21For example:
23.. code-block:: idris
25 fiveIsFive : 5 = 5
26 fiveIsFive = Refl
28 twoPlusTwo : 2 + 2 = 4
29 twoPlusTwo = Refl
31.. _sect-empty:
33The Empty Type
34==============
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:
43.. code-block:: idris
45 disjoint : (n : Nat) -> Z = S n -> Void
46 disjoint n p = replace {P = disjointTy} p ()
47 where
48 disjointTy : Nat -> Type
49 disjointTy Z = ()
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
60contradiction.
62.. code-block:: idris
64 void : Void -> a
66Simple Theorems
67===============
69When type checking dependent types, the type itself gets *normalised*.
70So imagine we want to prove the following theorem about the reduction
71behaviour of ``plus``:
73.. code-block:: idris
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``:
87.. code-block:: idris
89 plusReduces n = Refl
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``.
95.. code-block:: idris
97 plusReducesZ : (n:Nat) -> n = plus n Z
98 plusReducesZ Z = Refl
99 plusReducesZ (S k) = cong (plusReducesZ k)
101``cong`` is a function defined in the library which states that equality
102respects function application:
104.. code-block:: idris
106 cong : {f : t -> u} -> a = b -> f a = f b
108We can do the same for the reduction behaviour of plus on successors:
110.. code-block:: idris
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 trival 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
119mode’.
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`.
125.. _sect-totality:
127Totality Checking
128=================
130If we really want to trust our proofs, it is important that they are
131defined by *total* functions — that is, a function which is defined for
132all possible inputs and is guaranteed to terminate. Otherwise we could
133construct an element of the empty type, from which we could prove
134anything:
136.. code-block:: idris
138 -- making use of 'hd' being partially defined
139 empty1 : Void
140 empty1 = hd [] where
141 hd : List a -> a
142 hd (x :: xs) = x
144 -- not terminating
145 empty2 : Void
146 empty2 = empty2
148Internally, Idris checks every definition for totality, and we can check at
149the prompt with the ``:total`` command. We see that neither of the above
150definitions is total:
152::
154 *theorems> :total empty1
155 possibly not total due to: empty1#hd
156 not total as there are missing cases
157 *theorems> :total empty2
158 possibly not total due to recursive path empty2
160Note the use of the word “possibly” — a totality check can, of course,
161never be certain due to the undecidability of the halting problem. The
162check is, therefore, conservative. It is also possible (and indeed
163advisable, in the case of proofs) to mark functions as total so that it
164will be a compile time error for the totality check to fail:
166.. code-block:: idris
168 total empty2 : Void
169 empty2 = empty2
171::
173 Type checking ./theorems.idr
174 theorems.idr:25:empty2 is possibly not total due to recursive path empty2
176Reassuringly, our proof in Section :ref:`sect-empty` that the zero and
177successor constructors are disjoint is total:
179.. code-block:: idris
181 *theorems> :total disjoint
182 Total
184The totality check is, necessarily, conservative. To be recorded as
185total, a function ``f`` must:
187- Cover all possible inputs
189- Be *well-founded* — i.e. by the time a sequence of (possibly
190 mutually) recursive calls reaches ``f`` again, it must be possible to
191 show that one of its arguments has decreased.
193- Not use any data types which are not *strictly positive*
195- Not call any non-total functions
197Directives and Compiler Flags for Totality
198------------------------------------------
200By default, Idris allows all well-typed definitions, whether total or not.
201However, it is desirable for functions to be total as far as possible, as this
202provides a guarantee that they provide a result for all possible inputs, in
203finite time. It is possible to make total functions a requirement, either:
205- By using the ``--total`` compiler flag.
207- By adding a ``%default total`` directive to a source file. All
208 definitions after this will be required to be total, unless
209 explicitly flagged as ``partial``.
211All functions *after* a ``%default total`` declaration are required to
212be total. Correspondingly, after a ``%default partial`` declaration, the
213requirement is relaxed.
215Finally, the compiler flag ``--warnpartial`` causes to print a warning
216for any undeclared partial function.
218Totality checking issues
219------------------------
221Please note that the totality checker is not perfect! Firstly, it is
222necessarily conservative due to the undecidability of the halting
223problem, so many programs which *are* total will not be detected as
224such. Secondly, the current implementation has had limited effort put
225into it so far, so there may still be cases where it believes a function
226is total which is not. Do not rely on it for your proofs yet!
228Hints for totality
229------------------
231In cases where you believe a program is total, but Idris does not agree, it is
232possible to give hints to the checker to give more detail for a termination
233argument. The checker works by ensuring that all chains of recursive calls
234eventually lead to one of the arguments decreasing towards a base case, but
235sometimes this is hard to spot. For example, the following definition cannot be
236checked as ``total`` because the checker cannot decide that ``filter (<= x) xs``
237will always be smaller than ``(x :: xs)``:
239.. code-block:: idris
241 qsort : Ord a => List a -> List a
242 qsort [] = []
243 qsort (x :: xs)
244 = qsort (filter (< x) xs) ++
245 (x :: qsort (filter (>= x) xs))
247The function ``assert_smaller``, defined in the Prelude, is intended to
248address this problem:
250.. code-block:: idris
252 assert_smaller : a -> a -> a
253 assert_smaller x y = y
255It simply evaluates to its second argument, but also asserts to the
256totality checker that ``y`` is structurally smaller than ``x``. This can
257be used to explain the reasoning for totality if the checker cannot work
258it out itself. The above example can now be written as:
260.. code-block:: idris
262 total
263 qsort : Ord a => List a -> List a
264 qsort [] = []
265 qsort (x :: xs)
266 = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
267 (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))
269The expression ``assert_smaller (x :: xs) (filter (<= x) xs)`` asserts
270that the result of the filter will always be smaller than the pattern
271``(x :: xs)``.
273In more extreme cases, the function ``assert_total`` marks a
274subexpression as always being total:
276.. code-block:: idris
278 assert_total : a -> a
279 assert_total x = x
281In general, this function should be avoided, but it can be very useful
282when reasoning about primitives or externally defined functions (for
283example from a C library) where totality can be shown by an external
284argument.
287.. [1] Timothy G. Griffin. 1989. A formulae-as-type notion of
288 control. In Proceedings of the 17th ACM SIGPLAN-SIGACT
289 symposium on Principles of programming languages (POPL
290 '90). ACM, New York, NY, USA, 47-58. DOI=10.1145/96709.96714
291 http://doi.acm.org/10.1145/96709.96714