mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-22 14:38:20 +03:00
87039fb0a7
+ Fixed minor reST inconsistencies. + Normalised syntax used for headers to become inline with the [convention used for Python](http://sphinx.readthedocs.org/en/latest/rest.html#sections)
292 lines
9.3 KiB
ReStructuredText
292 lines
9.3 KiB
ReStructuredText
.. _sect-theorems:
|
||
|
||
***************
|
||
Theorem Proving
|
||
***************
|
||
|
||
Equality
|
||
========
|
||
|
||
Idris allows propositional equalities to be declared, allowing theorems about
|
||
programs to be stated and proved. Equality is built in, but conceptually
|
||
has the following definition:
|
||
|
||
.. code-block:: idris
|
||
|
||
data (=) : a -> b -> Type where
|
||
Refl : x = x
|
||
|
||
Equalities can be proposed between any values of any types, but the only
|
||
way to construct a proof of equality is if values actually are equal.
|
||
For example:
|
||
|
||
.. code-block:: idris
|
||
|
||
fiveIsFive : 5 = 5
|
||
fiveIsFive = Refl
|
||
|
||
twoPlusTwo : 2 + 2 = 4
|
||
twoPlusTwo = Refl
|
||
|
||
.. _sect-empty:
|
||
|
||
The Empty Type
|
||
==============
|
||
|
||
There is an empty type, :math:`\bot`, which has no constructors. It is
|
||
therefore impossible to construct an element of the empty type, at least
|
||
without using a partially defined or general recursive function (see
|
||
Section :ref:`sect-totality` for more details). We can therefore use the
|
||
empty type to prove that something is impossible, for example zero is
|
||
never equal to a successor:
|
||
|
||
.. code-block:: idris
|
||
|
||
disjoint : (n : Nat) -> Z = S n -> Void
|
||
disjoint n p = replace {P = disjointTy} p ()
|
||
where
|
||
disjointTy : Nat -> Type
|
||
disjointTy Z = ()
|
||
disjointTy (S k) = Void
|
||
|
||
There is no need to worry too much about how this function works —
|
||
essentially, it applies the library function ``replace``, which uses an
|
||
equality proof to transform a predicate. Here we use it to transform a
|
||
value of a type which can exist, the empty tuple, to a value of a type
|
||
which can’t, by using a proof of something which can’t exist.
|
||
|
||
Once we have an element of the empty type, we can prove anything.
|
||
``void`` is defined in the library, to assist with proofs by
|
||
contradiction.
|
||
|
||
.. code-block:: idris
|
||
|
||
void : Void -> a
|
||
|
||
Simple Theorems
|
||
===============
|
||
|
||
When type checking dependent types, the type itself gets *normalised*.
|
||
So imagine we want to prove the following theorem about the reduction
|
||
behaviour of ``plus``:
|
||
|
||
.. code-block:: idris
|
||
|
||
plusReduces : (n:Nat) -> plus Z n = n
|
||
|
||
We’ve written down the statement of the theorem as a type, in just the
|
||
same way as we would write the type of a program. In fact there is no
|
||
real distinction between proofs and programs. A proof, as far as we are
|
||
concerned here, is merely a program with a precise enough type to
|
||
guarantee a particular property of interest.
|
||
|
||
We won’t go into details here, but the Curry-Howard correspondence [1]_
|
||
explains this relationship. The proof itself is trivial, because
|
||
``plus Z n`` normalises to ``n`` by the definition of ``plus``:
|
||
|
||
.. code-block:: idris
|
||
|
||
plusReduces n = Refl
|
||
|
||
It is slightly harder if we try the arguments the other way, because
|
||
plus is defined by recursion on its first argument. The proof also works
|
||
by recursion on the first argument to ``plus``, namely ``n``.
|
||
|
||
.. code-block:: idris
|
||
|
||
plusReducesZ : (n:Nat) -> n = plus n Z
|
||
plusReducesZ Z = Refl
|
||
plusReducesZ (S k) = cong (plusReducesZ k)
|
||
|
||
``cong`` is a function defined in the library which states that equality
|
||
respects function application:
|
||
|
||
.. code-block:: idris
|
||
|
||
cong : {f : t -> u} -> a = b -> f a = f b
|
||
|
||
We can do the same for the reduction behaviour of plus on successors:
|
||
|
||
.. code-block:: idris
|
||
|
||
plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
|
||
plusReducesS Z m = Refl
|
||
plusReducesS (S k) m = cong (plusReducesS k m)
|
||
|
||
Even for trival theorems like these, the proofs are a little tricky to
|
||
construct in one go. When things get even slightly more complicated, it
|
||
becomes too much to think about to construct proofs in this ‘batch
|
||
mode’.
|
||
|
||
Idris provides interactive editing capabilities, which can help with
|
||
building proofs. For more details on building proofs interactively in
|
||
an editor, see :ref:`proofs-index`.
|
||
|
||
.. _sect-totality:
|
||
|
||
Totality Checking
|
||
=================
|
||
|
||
If we really want to trust our proofs, it is important that they are
|
||
defined by *total* functions — that is, a function which is defined for
|
||
all possible inputs and is guaranteed to terminate. Otherwise we could
|
||
construct an element of the empty type, from which we could prove
|
||
anything:
|
||
|
||
.. code-block:: idris
|
||
|
||
-- making use of 'hd' being partially defined
|
||
empty1 : Void
|
||
empty1 = hd [] where
|
||
hd : List a -> a
|
||
hd (x :: xs) = x
|
||
|
||
-- not terminating
|
||
empty2 : Void
|
||
empty2 = empty2
|
||
|
||
Internally, Idris checks every definition for totality, and we can check at
|
||
the prompt with the ``:total`` command. We see that neither of the above
|
||
definitions is total:
|
||
|
||
::
|
||
|
||
*theorems> :total empty1
|
||
possibly not total due to: empty1#hd
|
||
not total as there are missing cases
|
||
*theorems> :total empty2
|
||
possibly not total due to recursive path empty2
|
||
|
||
Note the use of the word “possibly” — a totality check can, of course,
|
||
never be certain due to the undecidability of the halting problem. The
|
||
check is, therefore, conservative. It is also possible (and indeed
|
||
advisable, in the case of proofs) to mark functions as total so that it
|
||
will be a compile time error for the totality check to fail:
|
||
|
||
.. code-block:: idris
|
||
|
||
total empty2 : Void
|
||
empty2 = empty2
|
||
|
||
::
|
||
|
||
Type checking ./theorems.idr
|
||
theorems.idr:25:empty2 is possibly not total due to recursive path empty2
|
||
|
||
Reassuringly, our proof in Section :ref:`sect-empty` that the zero and
|
||
successor constructors are disjoint is total:
|
||
|
||
.. code-block:: idris
|
||
|
||
*theorems> :total disjoint
|
||
Total
|
||
|
||
The totality check is, necessarily, conservative. To be recorded as
|
||
total, a function ``f`` must:
|
||
|
||
- Cover all possible inputs
|
||
|
||
- Be *well-founded* — i.e. by the time a sequence of (possibly
|
||
mutually) recursive calls reaches ``f`` again, it must be possible to
|
||
show that one of its arguments has decreased.
|
||
|
||
- Not use any data types which are not *strictly positive*
|
||
|
||
- Not call any non-total functions
|
||
|
||
Directives and Compiler Flags for Totality
|
||
------------------------------------------
|
||
|
||
By default, Idris allows all well-typed definitions, whether total or not.
|
||
However, it is desirable for functions to be total as far as possible, as this
|
||
provides a guarantee that they provide a result for all possible inputs, in
|
||
finite time. It is possible to make total functions a requirement, either:
|
||
|
||
- By using the ``--total`` compiler flag.
|
||
|
||
- By adding a ``%default total`` directive to a source file. All
|
||
definitions after this will be required to be total, unless
|
||
explicitly flagged as ``partial``.
|
||
|
||
All functions *after* a ``%default total`` declaration are required to
|
||
be total. Correspondingly, after a ``%default partial`` declaration, the
|
||
requirement is relaxed.
|
||
|
||
Finally, the compiler flag ``--warnpartial`` causes to print a warning
|
||
for any undeclared partial function.
|
||
|
||
Totality checking issues
|
||
------------------------
|
||
|
||
Please note that the totality checker is not perfect! Firstly, it is
|
||
necessarily conservative due to the undecidability of the halting
|
||
problem, so many programs which *are* total will not be detected as
|
||
such. Secondly, the current implementation has had limited effort put
|
||
into it so far, so there may still be cases where it believes a function
|
||
is total which is not. Do not rely on it for your proofs yet!
|
||
|
||
Hints for totality
|
||
------------------
|
||
|
||
In cases where you believe a program is total, but Idris does not agree, it is
|
||
possible to give hints to the checker to give more detail for a termination
|
||
argument. The checker works by ensuring that all chains of recursive calls
|
||
eventually lead to one of the arguments decreasing towards a base case, but
|
||
sometimes this is hard to spot. For example, the following definition cannot be
|
||
checked as ``total`` because the checker cannot decide that ``filter (<= x) xs``
|
||
will always be smaller than ``(x :: xs)``:
|
||
|
||
.. code-block:: idris
|
||
|
||
qsort : Ord a => List a -> List a
|
||
qsort [] = []
|
||
qsort (x :: xs)
|
||
= qsort (filter (< x) xs) ++
|
||
(x :: qsort (filter (>= x) xs))
|
||
|
||
The function ``assert_smaller``, defined in the Prelude, is intended to
|
||
address this problem:
|
||
|
||
.. code-block:: idris
|
||
|
||
assert_smaller : a -> a -> a
|
||
assert_smaller x y = y
|
||
|
||
It simply evaluates to its second argument, but also asserts to the
|
||
totality checker that ``y`` is structurally smaller than ``x``. This can
|
||
be used to explain the reasoning for totality if the checker cannot work
|
||
it out itself. The above example can now be written as:
|
||
|
||
.. code-block:: idris
|
||
|
||
total
|
||
qsort : Ord a => List a -> List a
|
||
qsort [] = []
|
||
qsort (x :: xs)
|
||
= qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
|
||
(x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))
|
||
|
||
The expression ``assert_smaller (x :: xs) (filter (<= x) xs)`` asserts
|
||
that the result of the filter will always be smaller than the pattern
|
||
``(x :: xs)``.
|
||
|
||
In more extreme cases, the function ``assert_total`` marks a
|
||
subexpression as always being total:
|
||
|
||
.. code-block:: idris
|
||
|
||
assert_total : a -> a
|
||
assert_total x = x
|
||
|
||
In general, this function should be avoided, but it can be very useful
|
||
when reasoning about primitives or externally defined functions (for
|
||
example from a C library) where totality can be shown by an external
|
||
argument.
|
||
|
||
|
||
.. [1] Timothy G. Griffin. 1989. A formulae-as-type notion of
|
||
control. In Proceedings of the 17th ACM SIGPLAN-SIGACT
|
||
symposium on Principles of programming languages (POPL
|
||
'90). ACM, New York, NY, USA, 47-58. DOI=10.1145/96709.96714
|
||
http://doi.acm.org/10.1145/96709.96714
|