git.iko.soy/Idris-dev
on bc8da8d help sign in
Idris-dev/docs/proofs/inductive.rst
101 lines 4.1 kB history raw
1.. _sect-inductive:
3****************
4Inductive Proofs
5****************
7Before embarking on proving ``plus_commutes`` in Idris itself, let us
8consider the overall structure of a proof of some property of natural
9numbers. Recall that they are defined recursively, as follows:
11.. code-block:: idris
13 data Nat : Type where
14 Z : Nat
15 S : Nat -> Nat
17A *total* function over natural numbers must both terminate, and cover
18all possible inputs. Idris checks functions for totality by checking that
19all inputs are covered, and that all recursive calls are on
20*structurally smaller* values (so recursion will always reach a base
21case). Recalling ``plus``:
23.. code-block:: idris
25 plus : Nat -> Nat -> Nat
26 plus Z m = m
27 plus (S k) m = S (plus k m)
29This is total because it covers all possible inputs (the first argument
30can only be ``Z`` or ``S k`` for some ``k``, and the second argument
31``m`` covers all possible ``Nat``) and in the recursive call, ``k``
32is structurally smaller than ``S k`` so the first argument will always
33reach the base case ``Z`` in any sequence of recursive calls.
35In some sense, this resembles a mathematical proof by induction (and
36this is no coincidence!). For some property ``P`` of a natural number
37``x``, we can show that ``P`` holds for all ``x`` if:
39- ``P`` holds for zero (the base case).
41- Assuming that ``P`` holds for ``k``, we can show ``P`` also holds for
42 ``S k`` (the inductive step).
44In ``plus``, the property we are trying to show is somewhat trivial (for
45all natural numbers ``x``, there is a ``Nat`` which need not have any
46relation to ``x``). However, it still takes the form of a base case and
47an inductive step. In the base case, we show that there is a ``Nat``
48arising from ``plus n m`` when ``n = Z``, and in the inductive step we
49show that there is a ``Nat`` arising when ``n = S k`` and we know we can
50get a ``Nat`` inductively from ``plus k m``. We could even write a
51function capturing all such inductive definitions:
53.. code-block:: idris
55 nat_induction : (P : Nat -> Type) -> -- Property to show
56 (P Z) -> -- Base case
57 ((k : Nat) -> P k -> P (S k)) -> -- Inductive step
58 (x : Nat) -> -- Show for all x
59 P x
60 nat_induction P p_Z p_S Z = p_Z
61 nat_induction P p_Z p_S (S k) = p_S k (nat_induction P p_Z p_S k)
63Using ``nat_induction``, we can implement an equivalent inductive
64version of ``plus``:
66.. code-block:: idris
68 plus_ind : Nat -> Nat -> Nat
69 plus_ind n m
70 = nat_induction (\x => Nat)
71 m -- Base case, plus_ind Z m
72 (\k, k_rec => S k_rec) -- Inductive step plus_ind (S k) m
73 -- where k_rec = plus_ind k m
74 n
76To prove that ``plus n m = plus m n`` for all natural numbers ``n`` and
77``m``, we can also use induction. Either we can fix ``m`` and perform
78induction on ``n``, or vice versa. We can sketch an outline of a proof;
79performing induction on ``n``, we have:
81- Property ``P`` is ``\x => plus x m = plus m x``.
83- Show that ``P`` holds in the base case and inductive step:
85 - | Base case: ``P Z``, i.e.
86 | ``plus Z m = plus m Z``, which reduces to
87 | ``m = plus m Z`` due to the definition of ``plus``.
89 - | Inductive step: Inductively, we know that ``P k`` holds for a specific, fixed ``k``, i.e.
90 | ``plus k m = plus m k`` (the induction hypothesis). Given this, show ``P (S k)``, i.e.
91 | ``plus (S k) m = plus m (S k)``, which reduces to
92 | ``S (plus k m) = plus m (S k)``. From the induction hypothesis, we can rewrite this to
93 | ``S (plus m k) = plus m (S k)``.
95To complete the proof we therefore need to show that ``m = plus m Z``
96for all natural numbers ``m``, and that ``S (plus m k) = plus m (S k)``
97for all natural numbers ``m`` and ``k``. Each of these can also be
98proved by induction, this time on ``m``.
100We are now ready to embark on a proof of commutativity of ``plus``
101formally in Idris.