10allows 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 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’. therefore provides an interactive proof mode.
121Interactive theorem proving
122---------------------------
124Instead of writing the proof in one go, we can use ’s interactive proof
125mode. To do this, we write the general *structure* of the proof, and use
126the interactive mode to complete the details. We’ll be constructing the
127proof by *induction*, so we write the cases for ``Z`` and ``S``, with a
128recursive call in the ``S`` case giving the inductive hypothesis, and
129insert *metavariables* for the rest of the definition:
133 plusReducesZ' : (n:Nat) -> n = plus n Z
134 plusReducesZ' Z = ?plusredZ_Z
135 plusReducesZ' (S k) = let ih = plusReducesZ' k in
138On running , two global names are created, ``plusredZ_Z`` and
139``plusredZ_S``, with no definition. We can use the ``:m`` command at the
140prompt to find out which metavariables are still to be solved (or, more
141precisely, which functions exist but have no definitions), then the
142``:t`` command to see their types:
147 Global metavariables:
148 [plusredZ_S,plusredZ_Z]
152 *theorems> :t plusredZ_Z
153 plusredZ_Z : Z = plus Z Z
155 *theorems> :t plusredZ_S
156 plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
158The ``:p`` command enters interactive proof mode, which can be used to
159complete the missing definitions.
163 *theorems> :p plusredZ_Z
165 ---------------------------------- (plusredZ_Z) --------
166 {hole0} : Z = plus Z Z
168This gives us a list of premises (above the line; there are none here)
169and the current goal (below the line; named ``{hole0}`` here). At the
170prompt we can enter tactics to direct the construction of the proof. In
171this case, we can normalise the goal with the ``compute`` tactic:
177 ---------------------------------- (plusredZ_Z) --------
180Now we have to prove that ``Z`` equals ``Z``, which is easy to prove by
181``Refl``. To apply a function, such as ``Refl``, we use ``refine`` which
182introduces subgoals for each of the function’s explicit arguments
187 -plusredZ_Z> refine Refl
188 plusredZ_Z: no more goals
190Here, we could also have used the ``trivial`` tactic, which tries to
191refine by ``Refl``, and if that fails, tries to refine by each name in
192the local context. When a proof is complete, we use the ``qed`` tactic
193to add the proof to the global context, and remove the metavariable from
194the unsolved metavariables list. This also outputs a trace of the proof:
206 Global metavariables:
209The ``:addproof`` command, at the interactive prompt, will add the proof
210to the source file (effectively in an appendix). Let us now prove the
211other required lemma, ``plusredZ_S``:
215 *theorems> :p plusredZ_S
217 ---------------------------------- (plusredZ_S) --------
218 {hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
220In this case, the goal is a function type, using ``k`` (the argument
221accessible by pattern matching) and ``ih`` — the local variable
222containing the result of the recursive call. We can introduce these as
223premisses using the ``intro`` tactic twice (or ``intros``, which
224introduces all arguments as premisses). This gives:
230 ---------------------------------- (plusredZ_S) --------
231 {hole2} : S k = plus (S k) Z
233Since plus is defined by recursion on its first argument, the term
234``plus (S k) Z`` in the goal can be simplified, so we use ``compute``.
240 ---------------------------------- (plusredZ_S) --------
241 {hole2} : S k = S (plus k Z)
243We know, from the type of ``ih``, that ``k = plus k Z``, so we would
244like to use this knowledge to replace ``plus k Z`` in the goal with
245``k``. We can achieve this with the ``rewrite`` tactic:
249 -plusredZ_S> rewrite ih
253 ---------------------------------- (plusredZ_S) --------
258The ``rewrite`` tactic takes an equality proof as an argument, and tries
259to rewrite the goal using that proof. Here, it results in an equality
260which is trivially provable:
265 plusredZ_S: no more goals
273Again, we can add this proof to the end of our source file using the
274``:addproof`` command at the interactive prompt.
281If we really want to trust our proofs, it is important that they are
282defined by *total* functions — that is, a function which is defined for
283all possible inputs and is guaranteed to terminate. Otherwise we could
284construct an element of the empty type, from which we could prove
289 -- making use of 'hd' being partially defined
299Internally, checks every definition for totality, and we can check at
300the prompt with the ``:total`` command. We see that neither of the above
305 *theorems> :total empty1
306 possibly not total due to: empty1#hd
307 not total as there are missing cases
308 *theorems> :total empty2
309 possibly not total due to recursive path empty2
311Note the use of the word “possibly” — a totality check can, of course,
312never be certain due to the undecidability of the halting problem. The
313check is, therefore, conservative. It is also possible (and indeed
314advisable, in the case of proofs) to mark functions as total so that it
315will be a compile time error for the totality check to fail:
324 Type checking ./theorems.idr
325 theorems.idr:25:empty2 is possibly not total due to recursive path empty2
327Reassuringly, our proof in Section :ref:`sect-empty` that the zero and
328successor constructors are disjoint is total:
332 *theorems> :total disjoint
335The totality check is, necessarily, conservative. To be recorded as
336total, a function ``f`` must:
338- Cover all possible inputs
340- Be *well-founded* — i.e. by the time a sequence of (possibly
341 mutually) recursive calls reaches ``f`` again, it must be possible to
342 show that one of its arguments has decreased.
344- Not use any data types which are not *strictly positive*
346- Not call any non-total functions
348Directives and Compiler Flags for Totality
349~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
351By default, allows all definitions, whether total or not. However, it is
352desirable for functions to be total as far as possible, as this provides
353a guarantee that they provide a result for all possible inputs, in
354finite time. It is possible to make total functions a requirement,
357- By using the ``--total`` compiler flag.
359- By adding a ``%default total`` directive to a source file. All
360 definitions after this will be required to be total, unless
361 explicitly flagged as ``partial``.
363All functions *after* a ``%default total`` declaration are required to
364be total. Correspondingly, after a ``%default partial`` declaration, the
365requirement is relaxed.
367Finally, the compiler flag ``--warnpartial`` causes to print a warning
368for any undeclared partial function.
370Totality checking issues
371~~~~~~~~~~~~~~~~~~~~~~~~
373Please note that the totality checker is not perfect! Firstly, it is
374necessarily conservative due to the undecidability of the halting
375problem, so many programs which *are* total will not be detected as
376such. Secondly, the current implementation has had limited effort put
377into it so far, so there may still be cases where it believes a function
378is total which is not. Do not rely on it for your proofs yet!
383In cases where you believe a program is total, but does not agree, it is
384possible to give hints to the checker to give more detail for a
385termination argument. The checker works by ensuring that all chains of
386recursive calls eventually lead to one of the arguments decreasing
387towards a base case, but sometimes this is hard to spot. For example,
388the following definition cannot be checked as ``total`` because the
389checker cannot decide that ``filter (<= x) xs`` will always be smaller
394 qsort : Ord a => List a -> List a
397 = qsort (filter (< x) xs) ++
398 (x :: qsort (filter (>= x) xs))
400The function ``assert_smaller``, defined in the Prelude, is intended to
405 assert_smaller : a -> a -> a
406 assert_smaller x y = y
408It simply evaluates to its second argument, but also asserts to the
409totality checker that ``y`` is structurally smaller than ``x``. This can
410be used to explain the reasoning for totality if the checker cannot work
411it out itself. The above example can now be written as:
416 qsort : Ord a => List a -> List a
419 = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
420 (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))
422The expression ``assert_smaller (x :: xs) (filter (<= x) xs)`` asserts
423that the result of the filter will always be smaller than the pattern
426In more extreme cases, the function ``assert_total`` marks a
427subexpression as always being total:
431 assert_total : a -> a
434In general, this function should be avoided, but it can be very useful
435when reasoning about primitives or externally defined functions (for
436example from a C library) where totality can be shown by an external
440.. [1] Timothy G. Griffin. 1989. A formulae-as-type notion of
441 control. In Proceedings of the 17th ACM SIGPLAN-SIGACT
442 symposium on Principles of programming languages (POPL
443 '90). ACM, New York, NY, USA, 47-58. DOI=10.1145/96709.96714
444 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