@@ -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``.