********************************************Running example: Addition of Natural Numbers******************************************** Throughout this tutorial, we will be working with the followingfunction, defined in the Idris prelude, which defines addition onnatural numbers: .. code-block:: idris     plus : Nat -> Nat -> Nat    plus Z     m = m    plus (S k) m = S (plus k m) It is defined by the above equations, meaning that we have for free theproperties that adding ``m`` to zero always results in ``m``, and thatadding ``m`` to any non-zero number ``S k`` always results in``S (plus k m)``. We can see this by evaluation at the Idris REPL (i.e.the prompt, the read-eval-print loop): .. code-block:: idris     Main> \m => plus Z m    \m => m     Idris> \k,m => plus (S k) m    \k => \m => S (plus k m) Note that unlike many other language REPLs, the Idris REPL performsevaluation on *open* terms, meaning that it can reduce terms whichappear inside lambda bindings, like those above. Therefore, we canintroduce unknowns ``k`` and ``m`` as lambda bindings and see how``plus`` reduces. The ``plus`` function has a number of other useful properties, forexample: -  It is *commutative*, that is for all ``Nat`` inputs ``n`` and ``m``,   we know that ``plus n m = plus m n``. -  It is *associative*, that is for all ``Nat`` inputs ``n``, ``m`` and   ``p``, we know that ``plus n (plus m p) = plus (plus m n) p``. We can use these properties in an Idris program, but in order to do sowe must *prove* them. Equality Proofs=============== Idris defines a propositional equality type as follows: .. code-block:: idris     data Equal : a -> b -> Type where       Refl : Equal x x As syntactic sugar, ``Equal x y`` can be written as ``x = y``. It is *propositional* equality, where the type states that any twovalues in different types ``a`` and ``b`` may be proposed to be equal.There is only one way to *prove* equality, however, which is byreflexivity (``Refl``). We have a *type* for propositional equality here, and correspondingly a*program* inhabiting an instance of this type can be seen as a proof ofthe corresponding proposition [1]_. So, trivially, we can prove that``4`` equals ``4``: .. code-block:: idris     four_eq : 4 = 4    four_eq = Refl However, trying to prove that ``4 = 5`` results in failure: .. code-block:: idris     four_eq_five : 4 = 5    four_eq_five = Refl The type ``4 = 5`` is a perfectly valid type, but is uninhabited, sowhen trying to type check this definition, Idris gives the followingerror: ::     When unifying 4 = 4 and (fromInteger 4) = (fromInteger 5)    Mismatch between:            4    and            5 Type checking equality proofs----------------------------- An important step in type checking Idris programs is *unification*,which attempts to resolve implicit arguments such as the implicitargument ``x`` in ``Refl``. As far as our understanding of type checkingproofs is concerned, it suffices to know that unifying two termsinvolves reducing both to normal form then trying to find an assignmentto implicit arguments which will make those normal forms equal. When type checking ``Refl``, Idris requires that the type is of the form``x = x``, as we see from the type of ``Refl``. In the case of``four_eq_five``, Idris will try to unify the expected type ``4 = 5``with the type of ``Refl``, ``x = x``, notice that a solution requiresthat ``x`` be both ``4`` and ``5``, and therefore fail. Since type checking involves reduction to normal form, we can write thefollowing equalities directly: .. code-block:: idris     twoplustwo_eq_four : 2 + 2 = 4    twoplustwo_eq_four = Refl     plus_reduces_Z : (m : Nat) -> plus Z m = m    plus_reduces_Z m = Refl     plus_reduces_Sk : (k, m : Nat) -> plus (S k) m = S (plus k m)    plus_reduces_Sk k m = Refl Heterogeneous Equality====================== Equality in Idris is *heterogeneous*, meaning that we can even proposeequalities between values in different types: .. code-block:: idris     idris_not_php : Z = "Z" The type ``Z = "Z"`` is uninhabited, and one might wonder why it is useful tobe able to propose equalities between values in different types. However, withdependent types, such equalities can arise naturally. For example, if twovectors are equal, their lengths must be equal: .. code-block:: idris     vect_eq_length : (xs : Vect n a) -> (ys : Vect m a) ->                     (xs = ys) -> n = m In the above declaration, ``xs`` and ``ys`` have different types becausetheir lengths are different, but we would still like to draw aconclusion about the lengths if they happen to be equal. We can define``vect_eq_length`` as follows: .. code-block:: idris     vect_eq_length xs xs Refl = Refl By matching on ``Refl`` for the third argument, we know that the onlyvalid value for ``ys`` is ``xs``, because they must be equal, andtherefore their types must be equal, so the lengths must be equal. Alternatively, we can put an underscore for the second ``xs``, sincethere is only one value which will type check: .. code-block:: idris     vect_eq_length xs _ Refl = Refl Properties of ``plus``====================== Using the ``(=)`` type, we can now state the properties of ``plus``given above as Idris type declarations: .. code-block:: idris     plus_commutes : (n, m : Nat) -> plus n m = plus m n    plus_assoc : (n, m, p : Nat) -> plus n (plus m p) = plus (plus n m) p Both of these properties (and many others) are proved for natural numberaddition in the Idris standard library, using ``(+)`` from the ``Num``interface rather than using ``plus`` directly. They have the names``plusCommutative`` and ``plusAssociative`` respectively. In the remainder of this tutorial, we will explore several differentways of proving ``plus_commutes`` (or, to put it another way, writingthe function.) We will also discuss how to use such equality proofs, andsee where the need for them arises in practice. .. [1]   This is known as the Curry-Howard correspondence.