mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-20 12:27:44 +03:00
00fc9a603d
Source and build directory are seperate. References and footnotes are named. Other than that, tried to do no changes in the docs. Fixed multi label in proofs-index. Fixed most of the warnings in make html. HTML and PDF are building.
321 lines
11 KiB
ReStructuredText
321 lines
11 KiB
ReStructuredText
***********************
|
|
Pattern Matching Proofs
|
|
***********************
|
|
|
|
In this section, we will provide a proof of ``plus_commutes`` directly,
|
|
by writing a pattern matching definition. We will use interactive
|
|
editing features extensively, since it is significantly easier to
|
|
produce a proof when the machine can give the types of intermediate
|
|
values and construct components of the proof itself. The commands we
|
|
will use are summarised below. Where we refer to commands
|
|
directly, we will use the Vim version, but these commands have a direct
|
|
mapping 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 type
|
|
declaration:
|
|
|
|
.. code-block:: idris
|
|
|
|
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
|
|
|
|
To create a template definition for the proof, press ``\a`` (or the
|
|
equivalent in your editor of choice) on the line with the type
|
|
declaration. 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.) You
|
|
should 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 the
|
|
type 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, by
|
|
pressing ``\l`` with the cursor over ``plus_commutes_Z``. This
|
|
yields:
|
|
|
|
.. 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 level
|
|
function ``plus_commutes_Z``, applied to the variable in scope ``m``.
|
|
|
|
Unfortunately, we cannot prove this lemma directly, since ``plus`` is
|
|
defined by matching on its *first* argument, and here ``plus m Z`` has a
|
|
concrete value for its *second argument* (in fact, the left hand side of
|
|
the equality has been reduced from ``plus Z m``.) Again, we can prove
|
|
this 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 by
|
|
pressing ``\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 access
|
|
to this inductive hypothesis by making a recursive call on k, as
|
|
follows:
|
|
|
|
.. 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 the
|
|
prelude:
|
|
|
|
.. 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 we
|
|
know ``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 be
|
|
a little tricky to use because in general the implicit argument ``p``
|
|
can be hard to infer by unification, so Idris provides a high level
|
|
syntax 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 some
|
|
property of ``x``, the ``rewrite ... in`` syntax will search for all
|
|
occurrences of ``x``
|
|
in the required type of ``expr`` and replace them with ``y``. We want
|
|
to 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 following
|
|
state:
|
|
|
|
.. 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 a
|
|
recursive call to ``plus_commutes``. We add this directly, by hand, as
|
|
follows:
|
|
|
|
.. 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 be
|
|
moved to the front in the right hand side of this equality. This
|
|
remaining lemma takes a similar form to the ``plus_commutes_Z``; we
|
|
begin 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 definition
|
|
is:
|
|
|
|
.. 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 to
|
|
pass the totality checker; i.e. it will terminate on all possible
|
|
well-typed inputs. This is important for proofs, since it provides a
|
|
guarantee that the proof is valid in *all* cases, not just those for
|
|
which it happens to be well-defined.
|
|
|
|
Now that ``plus_commutes`` has a ``total`` annotation, we have completed the
|
|
proof of commutativity of addition on natural numbers.
|