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