5In this section, we will provide a proof of ``plus_commutes`` directly,
6by writing a pattern matching definition. We will use interactive
7editing features extensively, since it is significantly easier to
8produce a proof when the machine can give the types of intermediate
9values and construct components of the proof itself. The commands we
10will use are summarised below. Where we refer to commands
11directly, we will use the Vim version, but these commands have a direct
12mapping to Emacs commands.
14+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
15|Command | Vim binding | Emacs binding | Explanation |
16+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
17| Check type | ``\t`` | ``C-c C-t`` | Show type of identifier or hole under the cursor. |
18+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
19| Proof search | ``\o`` | ``C-c C-a`` | Attempt to solve hole under the cursor by applying simple proof search. |
20+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
21| Make new definition | ``\d`` | ``C-c C-s`` | Add a template definition for the type defined under the cursor. |
22+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
23| Make lemma | ``\l`` | ``C-c C-e`` | Add a top level function with a type which solves the hole under the cursor. |
24+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
25| Split cases | ``\c`` | ``C-c C-c`` | Create new constructor patterns for each possible case of the variable under the cursor. |
26+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
32To begin, create a file ``pluscomm.idr`` containing the following type
37 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
39To create a template definition for the proof, press ``\d`` (or the
40equivalent in your editor of choice) on the line with the type
41declaration. You should see:
45 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
46 plus_commutes n m = ?plus_commutes_rhs
48To prove this by induction on ``n``, as we sketched in Section
49:ref:`sect-inductive`, we begin with a case split on ``n`` (press
50``\c`` with the cursor over the ``n`` in the definition.) You
55 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
56 plus_commutes Z m = ?plus_commutes_rhs_1
57 plus_commutes (S k) m = ?plus_commutes_rhs_2
59If we inspect the types of the newly created holes,
60``plus_commutes_rhs_1`` and ``plus_commutes_rhs_2``, we see that the
61type of each reflects that ``n`` has been refined to ``Z`` and ``S k``
62in each respective case. Pressing ``\t`` over
63``plus_commutes_rhs_1`` shows:
68 --------------------------------------
69 plus_commutes_rhs_1 : m = plus m 0
71Note that ``Z`` renders as ``0`` because the pretty printer renders
72natural numbers as integer literals for readability. Similarly, for
73``plus_commutes_rhs_2``:
79 --------------------------------------
80 plus_commutes_rhs_2 : S (plus k m) = plus m (S k)
82It is a good idea to give these slightly more meaningful names:
86 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
87 plus_commutes Z m = ?plus_commutes_Z
88 plus_commutes (S k) m = ?plus_commutes_S
93We can create a separate lemma for the base case interactively, by
94pressing ``\l`` with the cursor over ``plus_commutes_Z``. This
99 plus_commutes_Z : m = plus m 0
101 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
102 plus_commutes Z m = plus_commutes_Z
103 plus_commutes (S k) m = ?plus_commutes_S
105That is, the hole has been filled with a call to a top level
106function ``plus_commutes_Z``. The argument ``m`` has been made implicit
107because it can be inferred from context when it is applied.
109Unfortunately, we cannot prove this lemma directly, since ``plus`` is
110defined by matching on its *first* argument, and here ``plus m 0`` has a
111specific value for its *second argument* (in fact, the left hand side of
112the equality has been reduced from ``plus 0 m``.) Again, we can prove
113this by induction, this time on ``m``.
115First, create a template definition with ``\d``:
119 plus_commutes_Z : m = plus m 0
120 plus_commutes_Z = ?plus_commutes_Z_rhs
122Since we are going to write this by induction on ``m``, which is
123implicit, we will need to bring ``m`` into scope manually:
127 plus_commutes_Z : m = plus m 0
128 plus_commutes_Z {m} = ?plus_commutes_Z_rhs
130Now, case split on ``m`` with ``\c``:
134 plus_commutes_Z : m = plus m 0
135 plus_commutes_Z {m = Z} = ?plus_commutes_Z_rhs_1
136 plus_commutes_Z {m = (S k)} = ?plus_commutes_Z_rhs_2
138Checking the type of ``plus_commutes_Z_rhs_1`` shows the following,
139which is easily proved by reflection:
143 --------------------------------------
144 plus_commutes_Z_rhs_1 : 0 = 0
146For such trivial proofs, we can let write the proof automatically by
147pressing ``\o`` with the cursor over ``plus_commutes_Z_rhs_1``.
152 plus_commutes_Z : m = plus m 0
153 plus_commutes_Z {m = Z} = Refl
154 plus_commutes_Z {m = (S k)} = ?plus_commutes_Z_rhs_2
156For ``plus_commutes_Z_rhs_2``, we are not so lucky:
161 --------------------------------------
162 plus_commutes_Z_rhs_2 : S k = S (plus k 0)
164Inductively, we should know that ``k = plus k 0``, and we can get access
165to this inductive hypothesis by making a recursive call on k, as
170 plus_commutes_Z : m = plus m 0
171 plus_commutes_Z {m = Z} = Refl
172 plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in
173 ?plus_commutes_Z_rhs_2
175For ``plus_commutes_Z_rhs_2``, we now see:
180 rec : k = plus k (fromInteger 0)
181 --------------------------------------
182 plus_commutes_Z_rhs_2 : S k = S (plus k 0)
184Again, the ``fromInteger 0`` is merely due to ``Nat`` having an implementation
185of the ``Num`` interface. So we know that ``k = plus k 0``, but how do
186we use this to update the goal to ``S k = S k``?
188To achieve this, Idris provides a ``replace`` function as part of the
193 *pluscomm> :t replace
194 replace : (x = y) -> P x -> P y
196Given a proof that ``x = y``, and a property ``P`` which holds for
197``x``, we can get a proof of the same property for ``y``, because we
198know ``x`` and ``y`` must be the same. In practice, this function can be
199a little tricky to use because in general the implicit argument ``P``
200can be hard to infer by unification, so Idris provides a high level
201syntax which calculates the property and applies ``replace``:
207If we have ``prf : x = y``, and the required type for ``expr`` is some
208property of ``x``, the ``rewrite ... in`` syntax will search for ``x``
209in the required type of ``expr`` and replace it with ``y``. Concretely,
210in our example, we can say:
214 plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in
215 rewrite rec in ?plus_commutes_Z_rhs_2
217Checking the type of ``plus_commutes_Z_rhs_2`` now gives:
222 rec : k = plus k (fromInteger 0)
223 _rewrite_rule : plus k 0 = k
224 --------------------------------------
225 plus_commutes_Z_rhs_2 : S (plus k 0) = S (plus k 0)
227Using the rewrite rule ``rec`` (which we can see in the context here as
228``_rewrite_rule``\ [1]_, the goal type has been updated with ``k``
229replaced by ``plus k 0``.
231Alternatively, we could have applied the rewrite in the other direction
232using the ``sym`` function:
237 sym : (l = r) -> r = l
241 plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in
242 rewrite sym rec in ?plus_commutes_Z_rhs_2
244In this case, inspecting the type of the hole gives:
249 rec : k = plus k (fromInteger 0)
250 _rewrite_rule : k = plus k 0
251 --------------------------------------
252 plus_commutes_Z_rhs_2 : S k = S k
254Either way, we can use proof search (``\o``) to complete the
259 plus_commutes_Z : m = plus m 0
260 plus_commutes_Z {m = Z} = Refl
261 plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in
264The base case is now complete.
269Our main theorem, ``plus_commutes`` should currently be in the following
274 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
275 plus_commutes Z m = plus_commutes_Z
276 plus_commutes (S k) m = ?plus_commutes_S
278Looking again at the type of ``plus_commutes_S``, we have:
284 --------------------------------------
285 plus_commutes_S : S (plus k m) = plus m (S k)
287Conveniently, by induction we can immediately tell that
288``plus k m = plus m k``, so let us rewrite directly by making a
289recursive call to ``plus_commutes``. We add this directly, by hand, as
294 plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
295 plus_commutes Z m = plus_commutes_Z
296 plus_commutes (S k) m = rewrite plus_commutes k m in ?plus_commutes_S
298Checking the type of ``plus_commutes_S`` now gives:
304 _rewrite_rule : plus m k = plus k m
305 --------------------------------------
306 plus_commutes_S : S (plus m k) = plus m (S k)
308The good news is that ``m`` and ``k`` now appear in the correct order.
309However, we still have to show that the successor symbol ``S`` can be
310moved to the front in the right hand side of this equality. This
311remaining lemma takes a similar form to the ``plus_commutes_Z``; we
312begin by making a new top level lemma with ``\l``. This gives:
316 plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
318Unlike the previous case, ``k`` and ``m`` are not made implicit because
319we cannot in general infer arguments to a function from its result.
320Again, we make a template definition with ``\d``:
324 plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
325 plus_commutes_S k m = ?plus_commutes_S_rhs
327Again, this is defined by induction over ``m``, since ``plus`` is
328defined by matching on its first argument. The complete definition is:
333 plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
334 plus_commutes_S k Z = Refl
335 plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl
337All holes have now been solved.
339The ``total`` annotation means that we require the final function to
340pass the totality checker; i.e. it will terminate on all possible
341well-typed inputs. This is important for proofs, since it provides a
342guarantee that the proof is valid in *all* cases, not just those for
343which it happens to be well-defined.
345Now that ``plus_commutes`` has a ``total`` annotation, we have completed the
346proof of commutativity of addition on natural numbers.
349 Note that the left and right hand sides of the equality have been
350 swapped, because ``replace`` takes a proof of ``x=y`` and the
351 property for ``x``, not ``y``.
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list