***********************Pattern Matching Proofs*********************** In this section, we will provide a proof of ``plus_commutes`` directly,by writing a pattern matching definition. We will use interactiveediting features extensively, since it is significantly easier toproduce a proof when the machine can give the types of intermediatevalues and construct components of the proof itself. The commands wewill use are summarised below. Where we refer to commandsdirectly, we will use the Vim version, but these commands have a directmapping to Emacs commands. +---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+|Command              | Vim binding     | Emacs binding | Explanation                                                                                |+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+| Check type          | ``\t``          | ``C-c C-t``   | Show type of identifier or hole under the cursor.                                          |+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+| Proof search        | ``\s``          | ``C-c C-a``   | Attempt to solve hole under the cursor by applying simple proof search.                    |+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+| Make new definition | ``\a``          | ``C-c C-s``   | Add a template definition for the type defined under the cursor.                           |+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+| Make lemma          | ``\l``          | ``C-c C-e``   | Add a top level function with a type which solves the hole under the cursor.               |+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+| Split cases         | ``\c``          | ``C-c C-c``   | Create new constructor patterns for each possible case of the variable under the cursor.   |+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+  Creating a Definition===================== To begin, create a file ``pluscomm.idr`` containing the following typedeclaration: .. code-block:: idris     plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n To create a template definition for the proof, press ``\a`` (or theequivalent in your editor of choice) on the line with the typedeclaration. You should see: .. code-block:: idris     plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n    plus_commutes n m = ?plus_commutes_rhs To prove this by induction on ``n``, as we sketched in Section:ref:`sect-inductive`, we begin with a case split on ``n`` (press``\c`` with the cursor over the ``n`` in the definition.) Youshould see: .. code-block:: idris     plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n    plus_commutes Z m = ?plus_commutes_rhs_1    plus_commutes (S k) m = ?plus_commutes_rhs_2 If we inspect the types of the newly created holes,``plus_commutes_rhs_1`` and ``plus_commutes_rhs_2``, we see that thetype of each reflects that ``n`` has been refined to ``Z`` and ``S k``in each respective case. Pressing ``\t`` over``plus_commutes_rhs_1`` shows: .. code-block:: idris        m : Nat    -------------------------------------    plus_commutes_rhs_1 : m = plus m Z Similarly, for ``plus_commutes_rhs_2``: .. code-block:: idris       k : Nat      m : Nat    --------------------------------------    plus_commutes_rhs_2 : (S (plus k m)) = (plus m (S k)) It is a good idea to give these slightly more meaningful names: .. code-block:: idris     plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n    plus_commutes Z m = ?plus_commutes_Z    plus_commutes (S k) m = ?plus_commutes_S Base Case========= We can create a separate lemma for the base case interactively, bypressing ``\l`` with the cursor over ``plus_commutes_Z``. Thisyields: .. code-block:: idris     plus_commutes_Z : (m : Nat) -> m = plus m Z     plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n    plus_commutes Z m = plus_commutes_Z m    plus_commutes (S k) m = ?plus_commutes_S That is, the hole has been filled with a call to a top levelfunction ``plus_commutes_Z``, applied to the variable in scope ``m``.  Unfortunately, we cannot prove this lemma directly, since ``plus`` isdefined by matching on its *first* argument, and here ``plus m Z`` has aconcrete value for its *second argument* (in fact, the left hand side ofthe equality has been reduced from ``plus Z m``.) Again, we can provethis by induction, this time on ``m``. First, create a template definition with ``\d``: .. code-block:: idris     plus_commutes_Z : (m : Nat) -> m = plus m Z     plus_commutes_Z m = ?plus_commutes_Z_rhs Now, case split on ``m`` with ``\c``: .. code-block:: idris     plus_commutes_Z : (m : Nat) -> m = plus m Z     plus_commutes_Z Z = ?plus_commutes_Z_rhs_1    plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2 Checking the type of ``plus_commutes_Z_rhs_1`` shows the following,which is provable by ``Refl``: .. code-block:: idris     --------------------------------------    plus_commutes_Z_rhs_1 : Z = Z For such immediate proofs, we can let write the proof automatically bypressing ``\s`` with the cursor over ``plus_commutes_Z_rhs_1``.This yields: .. code-block:: idris     plus_commutes_Z : (m : Nat) -> m = plus m Z    plus_commutes_Z Z = Refl    plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2 For ``plus_commutes_Z_rhs_2``, we are not so lucky: .. code-block:: idris        k : Nat    -------------------------------------    plus_commutes_Z_rhs_2 : S k = S (plus k Z) Inductively, we should know that ``k = plus k Z``, and we can get accessto this inductive hypothesis by making a recursive call on k, asfollows: .. code-block:: idris     plus_commutes_Z : (m : Nat) -> m = plus m Z    plus_commutes_Z Z = Refl    plus_commutes_Z (S k)       = let rec = plus_commutes_Z k in             ?plus_commutes_Z_rhs_2 For ``plus_commutes_Z_rhs_2``, we now see: .. code-block:: idris        k : Nat       rec : k = plus k Z    -------------------------------------    plus_commutes_Z_rhs_2 : S k = S (plus k Z) So we know that ``k = plus k Z``, but how do we use this to update the goal to``S k = S k``? To achieve this, Idris provides a ``replace`` function as part of theprelude: .. code-block:: idris     Main> :t replace    Builtin.replace : (0 rule : x = y) -> p x -> p y Given a proof that ``x = y``, and a property ``p`` which holds for``x``, we can get a proof of the same property for ``y``, because weknow ``x`` and ``y`` must be the same. Note the multiplicity on ``rule``means that it's guaranteed to be erased at run time.In practice, this function can bea little tricky to use because in general the implicit argument ``p``can be hard to infer by unification, so Idris provides a high levelsyntax which calculates the property and applies ``replace``: .. code-block:: idris     rewrite prf in expr If we have ``prf : x = y``, and the required type for ``expr`` is someproperty of ``x``, the ``rewrite ... in`` syntax will search for alloccurrences of ``x``in the required type of ``expr`` and replace them with ``y``. We wantto replace ``plus k Z`` with ``k``, so we need to apply our rule``rec`` in reverse, which we can do using ``sym`` from the Prelude .. code-block:: idris     Main> :t sym    Builtin.sym : (0 rule : x = y) -> y = x Concretely, in our example, we can say: .. code-block:: idris     plus_commutes_Z (S k)       = let rec = plus_commutes_Z k in             rewrite sym rec in ?plus_commutes_Z_rhs_2 Checking the type of ``plus_commutes_Z_rhs_2`` now gives: .. code-block:: idris        k : Nat       rec : k = plus k Z    -------------------------------------    plus_commutes_Z_rhs_2 : S k = S k Using the rewrite rule ``rec``, the goal type has been updated with ``plus k Z``replaced by ``k``. We can use proof search (``\s``) to complete the proof, giving: .. code-block:: idris     plus_commutes_Z : (m : Nat) -> m = plus m Z    plus_commutes_Z Z = Refl    plus_commutes_Z (S k)       = let rec = plus_commutes_Z k in             rewrite sym rec in Refl The base case of ``plus_commutes`` is now complete. Inductive Step============== Our main theorem, ``plus_commutes`` should currently be in the followingstate: .. code-block:: idris     plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n    plus_commutes Z m = plus_commutes_Z m    plus_commutes (S k) m = ?plus_commutes_S Looking again at the type of ``plus_commutes_S``, we have: .. code-block:: idris        k : Nat       m : Nat    -------------------------------------    plus_commutes_S : S (plus k m) = plus m (S k) Conveniently, by induction we can immediately tell that``plus k m = plus m k``, so let us rewrite directly by making arecursive call to ``plus_commutes``. We add this directly, by hand, asfollows: .. code-block:: idris     plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n    plus_commutes Z m = plus_commutes_Z    plus_commutes (S k) m = rewrite plus_commutes k m in ?plus_commutes_S Checking the type of ``plus_commutes_S`` now gives: .. code-block:: idris        k : Nat       m : Nat    -------------------------------------    plus_commutes_S : S (plus m k) = plus m (S k) The good news is that ``m`` and ``k`` now appear in the correct order.However, we still have to show that the successor symbol ``S`` can bemoved to the front in the right hand side of this equality. Thisremaining lemma takes a similar form to the ``plus_commutes_Z``; webegin by making a new top level lemma with ``\l``. This gives: .. code-block:: idris     plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k) Again, we make a template definition with ``\a``: .. code-block:: idris     plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)    plus_commutes_S k m = ?plus_commutes_S_rhs Like ``plus_commutes_Z``, we can define this by induction over ``m``, since``plus`` is defined by matching on its first argument. The complete definitionis: .. code-block:: idris     total    plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)    plus_commutes_S k Z = Refl    plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl All holes have now been solved. The ``total`` annotation means that we require the final function topass the totality checker; i.e. it will terminate on all possiblewell-typed inputs. This is important for proofs, since it provides aguarantee that the proof is valid in *all* cases, not just those forwhich it happens to be well-defined. Now that ``plus_commutes`` has a ``total`` annotation, we have completed theproof of commutativity of addition on natural numbers.