git.iko.soy/Idris-dev
on master help sign in
Add section on theorem proving to tutorial
be93168Edwin Brady
docs/index.rst+14
compare with master
unifiedsplit
@@ -17,6 +17,7 @@ Documentation for the Idris Language
17
17
18* :ref:`tutorial-index`
18* :ref:`tutorial-index`
19* :ref:`eff-tutorial-index`
19* :ref:`eff-tutorial-index`
20+* :ref:`proofs-index`
20* :ref:`reference-index`
21* :ref:`reference-index`
21* :ref:`guides-index`
22* :ref:`guides-index`
22
23
@@ -63,6 +64,19 @@ Learning Effects
63 effects/conclusions
64 effects/conclusions
64 effects/summary
65 effects/summary
65
66
67+.. _proofs::
68+
69+###############
70+Theorem Proving
71+###############
72+
73+.. toctree::
74+ :maxdepth: 1
75+
76+ proofs/pluscomm
77+ proofs/inductive
78+ proofs/patterns
79+
66.. _reference:
80.. _reference:
67
81
68##################
82##################
docs/proofs/index.rstnew file+24
@@ -0,0 +1,24 @@
1+.. _proofs-index:
2+
3+###############
4+Theorem Proving
5+###############
6+
7+A tutorial on theorem proving in Idris.
8+
9+.. note::
10+
11+ The documentation for Idris has been published under the Creative
12+ Commons CC0 License. As such to the extent possible under law, *The
13+ Idris Community* has waived all copyright and related or neighboring
14+ rights to Documentation for Idris.
15+
16+ More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
17+
18+.. toctree::
19+ :maxdepth: 1
20+
21+ pluscomm
22+ inductive
23+ patterns
24+
docs/proofs/inductive.rstnew file+98
@@ -0,0 +1,98 @@
1+Inductive Proofs
2+================
3+
4+Before embarking on proving ``plus_commutes`` in Idris itself, let us
5+consider the overall structure of a proof of some property of natural
6+numbers. Recall that they are defined recursively, as follows:
7+
8+.. code-block:: idris
9+
10+ data Nat : Type where
11+ Z : Nat
12+ S : Nat -> Nat
13+
14+A *total* function over natural numbers must both terminate, and cover
15+all possible inputs. Idris checks functions for totality by cheking that
16+all inputs are covered, and that all recursive calls are on
17+*structurally smaller* values (so recursion will always reach a base
18+case). Recalling ``plus``:
19+
20+.. code-block:: idris
21+
22+ plus : Nat -> Nat -> Nat
23+ plus Z m = m
24+ plus (S k) m = S (plus k m)
25+
26+This is total because it covers all possible inputs (the first argument
27+can only be ``Z`` or ``S k`` for some ``k``, and the second argument
28+``m`` covers all possible ``Nat``\ s) and in the recursive call, ``k``
29+is structurally smaller than ``S k`` so the first argument will always
30+reach the base case ``Z`` in any sequence of recursive calls.
31+
32+In some sense, this resembles a mathematical proof by induction (and
33+this is no coincidence!). For some property ``P`` of a natural number
34+``x``, we can show that ``P`` holds for all ``x`` if:
35+
36+- ``P`` holds for zero (the base case).
37+
38+- Assuming that ``P`` holds for ``k``, we can show ``P`` also holds for
39+ ``S k`` (the inductive step).
40+
41+In ``plus``, the property we are trying to show is somewhat trivial (for
42+all natural numbers ``x``, there is a ``Nat`` which need not have any
43+relation to ``x``). However, it still takes the form of a base case and
44+an inductive step. In the base case, we show that there is a ``Nat``
45+arising from ``plus n m`` when ``n = Z``, and in the inductive step we
46+show that there is a ``Nat`` arising when ``n = S k`` and we know we can
47+get a ``Nat`` inductively from ``plus k m``. We could even write a
48+function capturing all such inductive definitions:
49+
50+.. code-block:: idris
51+
52+ nat_induction : (P : Nat -> Type) -> -- Property to show
53+ (P Z) -> -- Base case
54+ ((k : Nat) -> P k -> P (S k)) -> -- Inductive step
55+ (x : Nat) -> -- Show for all x
56+ P x
57+ nat_induction P p_Z p_S Z = p_Z
58+ nat_induction P p_Z p_S (S k) = p_S k (nat_induction P p_Z p_S k)
59+
60+Using ``nat_induction``, we can implement an equivalent inductive
61+version of ``plus``:
62+
63+.. code-block:: idris
64+
65+ plus_ind : Nat -> Nat -> Nat
66+ plus_ind n m
67+ = nat_induction (\x => Nat)
68+ m -- Base case, plus_ind Z m
69+ (\k, k_rec => S k_rec) -- Inductive step plus_ind (S k) m
70+ -- where k_rec = plus_ind k m
71+ n
72+
73+To prove that ``plus n m = plus m n`` for all natural numbers ``n`` and
74+``m``, we can also use induction. Either we can fix ``m`` and perform
75+induction on ``n``, or vice versa. We can sketch an outline of a proof;
76+performing induction on ``n``, we have:
77+
78+- Property ``P`` is ``\backslashx => plus x m = plus m x``.
79+
80+- Show that ``P`` holds in the base case and inductive step:
81+
82+ - | Base case: ``P Z``, i.e.
83+ | ``plus Z m = plus m Z``, which reduces to
84+ | ``m = plus m Z`` due to the definition of ``plus``.
85+
86+ - | Inductive step: Inductively, we know that ``P k`` holds for a specific, fixed ``k``, i.e.
87+ | ``plus k m = plus m k`` (the induction hypothesis). Given this, show ``P (S k)``, i.e.
88+ | ``plus (S k) m = plus m (S k)``, which reduces to
89+ | ``S (plus k m) = plus m (S k)``. From the induction hypothesis, we can rewrite this to
90+ | ``S (plus m k) = plus m (S k)``.
91+
92+To complete the proof we therefore need to show that ``m = plus m Z``
93+for all natural numbers ``m``, and that ``S (plus m k) = plus m (S k)``
94+for all natural numbers ``m`` and ``k``. Each of these can also be
95+proved by induction, this time on ``m``.
96+
97+We are now ready to embark on a proof of commutativity of ``plus``
98+formally in Idris.
docs/proofs/patterns.rstnew file+354
@@ -0,0 +1,354 @@
1+Pattern Matching Proofs
2+=======================
3+
4+In this section, we will provide a proof of ``plus_commutes`` directly,
5+by writing a pattern matching definition. We will use interactive
6+editing features extensively, since it is significantly easier to
7+produce a proof when the machine can give the types of intermediate
8+values and construct components of the proof itself. The commands we
9+will use are summarised below. Where we refer to commands
10+directly, we will use the Vim version, but these commands have a direct
11+mapping to Emacs commands.
12+
13++---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
14+|Command | Vim binding | Emacs binding | Explanation |
15++---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
16+| Check type | ``\t`` | ``C-c C-t`` | Show type of identifier or metavariable under the cursor. |
17++---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
18+| Proof search | ``\o`` | ``C-c C-a`` | Attempt to solve metavariable under the cursor by applying simple proof search. |
19++---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
20+| Make new definition | ``\d`` | ``C-c C-s`` | Add a template definition for the type defined under the cursor. |
21++---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
22+| Make lemma | ``\l`` | ``C-c C-e`` | Add a top level function with a type which solves the metavariable under the cursor. |
23++---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
24+| Split cases | ``\c`` | ``C-c C-c`` | Create new constructor patterns for each possible case of the variable under the cursor. |
25++---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
26+
27+
28+Creating a Definition
29+---------------------
30+
31+To begin, create a file ``pluscomm.idr`` containing the following type
32+declaration:
33+
34+.. code-block:: idris
35+
36+ total
37+ plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
38+
39+The ``total`` annotation means that we aim to write a function which
40+passes the totality checker; i.e. it will terminate on all possible
41+well-typed inputs. This is important for proofs, since it provides a
42+guarantee that the proof is valid in *all* cases, not just those for
43+which it happens to be well-defined.
44+
45+To create a template definition for the proof, press ``\backslashd`` the
46+equivalent in your editor of choice) on the line with the type
47+declaration. You should see:
48+
49+.. code-block:: idris
50+
51+ total
52+ plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
53+ plus_commutes n m = ?plus_commutes_rhs
54+
55+To prove this by induction on ``n``, as we sketched in Section
56+[sect:induction], we begin with a case split on ``n`` (press
57+``\backslashc`` with the cursor over the ``n`` in the definition.) You
58+should see:
59+
60+.. code-block:: idris
61+
62+ total
63+ plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
64+ plus_commutes Z m = ?plus_commutes_rhs_1
65+ plus_commutes (S k) m = ?plus_commutes_rhs_2
66+
67+If we inspect the types of the newly created metavariables,
68+``plus_commutes_rhs_1`` and ``plus_commutes_rhs_2``, we see that the
69+type of each reflects that ``n`` has been refined to ``Z`` and ``S k``
70+in each respective case. Pressing ``\backslasht`` over
71+``plus_commutes_rhs_1`` shows:
72+
73+.. code-block:: idris
74+
75+ m : Nat
76+ --------------------------------------
77+ plus_commutes_rhs_1 : m = plus m 0
78+
79+Note that ``Z`` renders as ``0`` because the pretty printer renders
80+natural numbers as integer literals for readability. Similarly, for
81+``plus_commutes_rhs_2``:
82+
83+.. code-block:: idris
84+
85+ k : Nat
86+ m : Nat
87+ --------------------------------------
88+ plus_commutes_rhs_2 : S (plus k m) = plus m (S k)
89+
90+It is a good idea to give these slightly more meaningful names:
91+
92+.. code-block:: idris
93+
94+ total
95+ plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
96+ plus_commutes Z m = ?plus_commutes_Z
97+ plus_commutes (S k) m = ?plus_commutes_S
98+
99+Base Case
100+---------
101+
102+We can create a separate lemma for the base case interactively, by
103+pressing ``\backslashl`` with the cursor over ``plus_commutes_Z``. This
104+yields:
105+
106+.. code-block:: idris
107+
108+ plus_commutes_Z : m = plus m 0
109+
110+ total
111+ plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
112+ plus_commutes Z m = plus_commutes_Z
113+ plus_commutes (S k) m = ?plus_commutes_S
114+
115+That is, the metavariable has been filled with a call to a top level
116+function ``plus_commutes_Z``. The argument ``m`` has been made implicit
117+because it can be inferred from context when it is applied.
118+
119+Unfortunately, we cannot prove this lemma directly, since ``plus`` is
120+defined by matching on its *first* argument, and here ``plus m 0`` has a
121+specific value for its *second argument* (in fact, the left hand side of
122+the equality has been reduced from ``plus 0 m``.) Again, we can prove
123+this by induction, this time on ``m``.
124+
125+First, create a template definition with ``\backslashd``:
126+
127+.. code-block:: idris
128+
129+ plus_commutes_Z : m = plus m 0
130+ plus_commutes_Z = ?plus_commutes_Z_rhs
131+
132+Since we are going to write this by induction on ``m``, which is
133+implciit, we will need to bring ``m`` into scope manually:
134+
135+.. code-block:: idris
136+
137+ plus_commutes_Z : m = plus m 0
138+ plus_commutes_Z {m} = ?plus_commutes_Z_rhs
139+
140+Now, case split on ``m`` with ``\backslashc``:
141+
142+.. code-block:: idris
143+
144+ plus_commutes_Z : m = plus m 0
145+ plus_commutes_Z {m = Z} = ?plus_commutes_Z_rhs_1
146+ plus_commutes_Z {m = (S k)} = ?plus_commutes_Z_rhs_2
147+
148+Checking the type of ``plus_commutes_Z_rhs_1`` shows the following,
149+which is easily proved by reflection:
150+
151+.. code-block:: idris
152+
153+ --------------------------------------
154+ plus_commutes_Z_rhs_1 : 0 = 0
155+
156+For such trivial proofs, we can let write the proof automatically by
157+pressing ``\backslasho`` with the cursor over ``plus_commutes_Z_rhs_1``.
158+This yields:
159+
160+.. code-block:: idris
161+
162+ plus_commutes_Z : m = plus m 0
163+ plus_commutes_Z {m = Z} = Refl
164+ plus_commutes_Z {m = (S k)} = ?plus_commutes_Z_rhs_2
165+
166+For ``plus_commutes_Z_rhs_2``, we are not so lucky:
167+
168+.. code-block:: idris
169+
170+ k : Nat
171+ --------------------------------------
172+ plus_commutes_Z_rhs_2 : S k = S (plus k 0)
173+
174+Inductively, we should know that ``k = plus k 0``, and we can get access
175+to this inductive hypothesis by making a recursive call on k, as
176+follows:
177+
178+.. code-block:: idris
179+
180+ plus_commutes_Z : m = plus m 0
181+ plus_commutes_Z {m = Z} = Refl
182+ plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in
183+ ?plus_commutes_Z_rhs_2
184+
185+For ``plus_commutes_Z_rhs_2``, we now see:
186+
187+.. code-block:: idris
188+
189+ k : Nat
190+ rec : k = plus k (fromInteger 0)
191+ --------------------------------------
192+ plus_commutes_Z_rhs_2 : S k = S (plus k 0)
193+
194+Again, the ``fromInteger 0`` is merely due to ``Nat`` being an instance
195+of the ``Num`` typeclass. So we know that ``k = plus k 0``, but how do
196+we use this to update the goal to ``S k = S k``?
197+
198+To achieve this, provides a ``replace`` function as part of the prelude:
199+
200+.. code-block:: idris
201+
202+ *pluscomm> :t replace
203+ replace : (x = y) -> P x -> P y
204+
205+Given a proof that ``x = y``, and a property ``P`` which holds for
206+``x``, we can get a proof of the same property for ``y``, because we
207+know ``x`` and ``y`` must be the same. In practice, this function can be
208+a little tricky to use because in general the implicit argument ``P``
209+can be hard to infer by unification, so provides a high level syntax
210+which calculates the property and applies replace:
211+
212+.. code-block:: idris
213+
214+ rewrite prf in expr
215+
216+If we have ``prf : x = y``, and the required type for ``expr`` is some
217+property of ``x``, the ``rewrite ... in`` syntax will search for ``x``
218+in the required type of ``expr`` and replace it with ``y``. Concretely,
219+in our example, we can say:
220+
221+.. code-block:: idris
222+
223+ plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in
224+ rewrite rec in ?plus_commutes_Z_rhs_2
225+
226+Checking the type of ``plus_commutes_Z_rhs_2`` now gives:
227+
228+.. code-block:: idris
229+
230+ k : Nat
231+ rec : k = plus k (fromInteger 0)
232+ _rewrite_rule : plus k 0 = k
233+ --------------------------------------
234+ plus_commutes_Z_rhs_2 : S (plus k 0) = S (plus k 0)
235+
236+Using the rewrite rule ``rec`` (which we can see in the context here as
237+``_rewrite_rule``\ [1]_, the goal type has been updated with ``k``
238+replaced by ``plus k 0``.
239+
240+Alternatively, we could have applied the rewrite in the other direction
241+using the ``sym`` function:
242+
243+.. code-block:: idris
244+
245+ *pluscomm> :t sym
246+ sym : (l = r) -> r = l
247+
248+.. code-block:: idris
249+
250+ plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in
251+ rewrite sym rec in ?plus_commutes_Z_rhs_2
252+
253+In this case, inspecting the type of the hole gives:
254+
255+.. code-block:: idris
256+
257+ k : Nat
258+ rec : k = plus k (fromInteger 0)
259+ _rewrite_rule : k = plus k 0
260+ --------------------------------------
261+ plus_commutes_Z_rhs_2 : S k = S k
262+
263+Either way, we can use proof search (``\backslasho``) to complete the
264+proof, giving:
265+
266+.. code-block:: idris
267+
268+ plus_commutes_Z : m = plus m 0
269+ plus_commutes_Z {m = Z} = Refl
270+ plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in
271+ rewrite rec in Refl
272+
273+The base case is now complete.
274+
275+Inductive Step
276+--------------
277+
278+Our main theorem, ``plus_commutes`` should currently be in the following
279+state:
280+
281+.. code-block:: idris
282+
283+ total
284+ plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
285+ plus_commutes Z m = plus_commutes_Z
286+ plus_commutes (S k) m = ?plus_commutes_S
287+
288+Looking again at the type of ``plus_commutes_S``, we have:
289+
290+.. code-block:: idris
291+
292+ k : Nat
293+ m : Nat
294+ --------------------------------------
295+ plus_commutes_S : S (plus k m) = plus m (S k)
296+
297+Conveniently, by induction we can immediately tell that
298+``plus k m = plus m k``, so let us rewrite directly by making a
299+recursive call to ``plus_commutes``. We add this directly, by hand, as
300+follows:
301+
302+.. code-block:: idris
303+
304+ total
305+ plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
306+ plus_commutes Z m = plus_commutes_Z
307+ plus_commutes (S k) m = rewrite plus_commutes k m in ?plus_commutes_S
308+
309+Checking the type of ``plus_commutes_S`` now gives:
310+
311+.. code-block:: idris
312+
313+ k : Nat
314+ m : Nat
315+ _rewrite_rule : plus m k = plus k m
316+ --------------------------------------
317+ plus_commutes_S : S (plus m k) = plus m (S k)
318+
319+The good news is that ``m`` and ``k`` now appear in the correct order.
320+However, we still have to show that the successor symbol ``S`` can be
321+moved to the front in the right hand side of this equality. This
322+remaining lemma takes a similar form to the ``plus_commutes_Z``; we
323+begin by making a new top level lemma with ``\backslashl``. This gives:
324+
325+.. code-block:: idris
326+
327+ plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
328+
329+Unlike the previous case, ``k`` and ``m`` are not made implicit because
330+we cannot in general infer arguments to a function from its result.
331+Again, we make a template definition with ``\backslashd``:
332+
333+.. code-block:: idris
334+
335+ plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
336+ plus_commutes_S k m = ?plus_commutes_S_rhs
337+
338+Again, this is defined by induction over ``m``, since ``plus`` is
339+defined by matching on its first argument. The complete definition is:
340+
341+.. code-block:: idris
342+
343+ plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
344+ plus_commutes_S k Z = Refl
345+ plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl
346+
347+All metavariables have now been solved, and ``plus_commutes`` has a
348+``total`` annotation, so we have completed the proof of commutativity of
349+addition on natural numbers.
350+
351+.. [1]
352+ Note that the left and right hand sides of the equality have been
353+ swapped, because ``replace`` takes a proof of ``x=y`` and the
354+ property for ``x``, not ``y``.
docs/proofs/pluscomm.rstnew file+188
@@ -0,0 +1,188 @@
1+Running example: Addition of Natural Numbers
2+============================================
3+
4+Throughout this tutorial, we will be working with the following
5+function, defined in the Idris prelude, which defines addition on
6+natural numbers:
7+
8+.. code-block:: idris
9+
10+ plus : Nat -> Nat -> Nat
11+ plus Z m = m
12+ plus (S k) m = S (plus k m)
13+
14+It is defined by the above equations, meaning that we have for free the
15+properties that adding ``m`` to zero always results in ``m``, and that
16+adding ``m`` to any non-zero number ``S k`` always results in
17+``S (plus k m)``. We can see this by evaluation at the Idris REPL (i.e.
18+the prompt, the read-eval-print loop):
19+
20+.. code-block:: idris
21+
22+ Idris> \m => plus Z m
23+ \m => m : Nat -> Nat
24+
25+ Idris> \k,m => plus (S k) m
26+ \k => \m => S (plus k m) : Nat -> Nat -> Nat
27+
28+Note that unlike many other language REPLs, the Idris REPL performs
29+evaluation on *open* terms, meaning that it can reduce terms which
30+appear inside lambda bindings, like those above. Therefore, we can
31+introduce unknowns ``k`` and ``m`` as lambda bindings and see how
32+``plus`` reduces.
33+
34+The ``plus`` function has a number of other useful properties, for
35+example:
36+
37+- It is *commutative*, that is for all ``Nat`` inputs ``n`` and ``m``,
38+ we know that ``plus n m = plus m n``.
39+
40+- It is *associative*, that is for all ``Nat`` inputs ``n``, ``m`` and
41+ ``p``, we know that ``plus n (plus m p) = plus (plus m n) p``.
42+
43+We can use these properties in an Idris program, but in order to do so
44+we must *prove* them.
45+
46+Equality Proofs
47+---------------
48+
49+Idris has a built-in propositional equality type, conceptually defined
50+as follows:
51+
52+.. code-block:: idris
53+
54+ data (=) : a -> b -> Type where
55+ Refl : x = x
56+
57+Note that this must be built-in, rather than defined in the library,
58+because ``=`` is a reserved operator — you cannot define this directly
59+in your own code.
60+
61+It is *propositional* equality, where the type states that any two
62+values in different types ``a`` and ``b`` may be proposed to be equal.
63+There is only one way to *prove* equality, however, which is by
64+reflexivity (``Refl``).
65+
66+We have a *type* for propositional equality here, and correspondingly a
67+*program* inhabiting an instance of this type can be seen as a proof of
68+the corresponding proposition [1]_. So, trivially, we can prove that
69+``4`` equals ``4``:
70+
71+.. code-block:: idris
72+
73+ four_eq : 4 = 4
74+ four_eq = Refl
75+
76+However, trying to prove that ``4 = 5`` results in failure:
77+
78+.. code-block:: idris
79+
80+ four_eq_five : 4 = 5
81+ four_eq_five = Refl
82+
83+The type ``4 = 5`` is a perfectly valid type, but is uninhabited, so
84+when trying to type check this definition, Idris gives the following
85+error:
86+
87+::
88+
89+ When elaborating right hand side of four_eq_five:
90+ Can't unify
91+ 5 = 5
92+ with
93+ 4 = 5
94+
95+Type checking equality proofs
96+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
97+
98+An important step in type checking Idris programs is *unification*,
99+which attempts to resolve implicit arguments such as the implicit
100+argument ``x`` in ``Refl``. As far as our understanding of type checking
101+proofs is concerned, it suffices to know that unifying two terms
102+involves reducing both to normal form then trying to find an assignment
103+to implicit arguments which will make those normal forms equal.
104+
105+When type checking ``Refl``, Idris requires that the type is of the form
106+``x = x``, as we see from the type of ``Refl``. In the case of
107+``four_eq_five``, Idris will try to unify the expected type ``4 = 5``
108+with the type of ``Refl``, ``x = x``, notice that a solution requires
109+that ``x`` be both ``4`` and ``5``, and therefore fail.
110+
111+Since type checking involves reduction to normal form, we can write the
112+following equalities directly:
113+
114+.. code-block:: idris
115+
116+ twoplustwo_eq_four : 2 + 2 = 4
117+ twoplustwo_eq_four = Refl
118+
119+ plus_reduces_Z : (m : Nat) -> plus Z m = m
120+ plus_reduces_Z m = Refl
121+
122+ plus_reduces_Sk : (k, m : Nat) -> plus (S k) m = S (plus k m)
123+ plus_reduces_Sk k m = Refl
124+
125+Heterogeneous Equality
126+----------------------
127+
128+Equality in Idris is *heterogeneous*, meaning that we can even propose
129+equalities between values in different types:
130+
131+.. code-block:: idris
132+
133+ idris_not_php : 2 = "2"
134+
135+Obviously, in Idris the type ``2 = 2`` is uninhabited, and one might
136+wonder why it is useful to be able to propose equalities between values
137+in different types. However, with dependent types, such equalities can
138+arise naturally. For example, if two vectors are equal, their lengths
139+must be equal:
140+
141+.. code-block:: idris
142+
143+ vect_eq_length : (xs : Vect n a) -> (ys : Vect m a) ->
144+ (xs = ys) -> n = m
145+
146+In the above declaration, ``xs`` and ``ys`` have different types because
147+their lengths are different, but we would still like to draw a
148+conclusion about the lengths if they happen to be equal. We can define
149+``vect_eq_length`` as follows:
150+
151+.. code-block:: idris
152+
153+ vect_eq_length xs xs Refl = Refl
154+
155+By matching on ``Refl`` for the third argument, we know that the only
156+valid value for ``ys`` is ``xs``, because they must be equal, and
157+therefore their types must be equal, so the lengths must be equal.
158+
159+Alternatively, we can put an underscore for the second ``xs``, since
160+there is only one value which will type check:
161+
162+.. code-block:: idris
163+
164+ vect_eq_length xs _ Refl = Refl
165+
166+Properties of ``plus``
167+----------------------
168+
169+Using the ``(=)`` type, we can now state the properties of ``plus``
170+given above as Idris type declarations:
171+
172+.. code-block:: idris
173+
174+ plus_commutes : (n, m : Nat) -> plus n m = plus m n
175+ plus_assoc : (n, m, p : Nat) -> plus n (plus m p) = plus (plus n m) p
176+
177+Both of these properties (and many others) are proved for natural number
178+addition in the Idris standard library, using ``(+)`` from the ``Num``
179+type class rather than using ``plus`` directly. They have the names
180+``plusCommutative`` and ``plusAssociatie`` respectively.
181+
182+In the remainder of this tutorial, we will explore several different
183+ways of proving ``plus_commutes`` (or, to put it another way, writing
184+the function.) We will also discuss how to use such equality proofs, and
185+see where the need for them arises in practice.
186+
187+.. [1]
188+ This is known as the Curry-Howard correspondence