mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-11 16:05:51 +03:00
More documentation refreshing
This commit is contained in:
parent
0be0c27d1a
commit
16ae7994e7
@ -24,5 +24,6 @@ and yet to be updated, so use with caution!
|
||||
|
||||
tutorial/index
|
||||
updates/updates
|
||||
proofs/index
|
||||
faq/faq
|
||||
reference/index
|
||||
|
231
docs/proofs/definitional.rst
Normal file
231
docs/proofs/definitional.rst
Normal file
@ -0,0 +1,231 @@
|
||||
In order to understand how to write proofs in Idris I think its worth clarifying some fundamentals, such as,
|
||||
|
||||
- Propositions and judgments
|
||||
- Boolean and constructive logic
|
||||
- Curry-Howard correspondence
|
||||
- Definitional and propositional equalities
|
||||
- Axiomatic and constructive approaches
|
||||
|
||||
Propositions and Judgments
|
||||
==========================
|
||||
|
||||
Propositions are the subject of our proofs, before the proof then we can't formally say if they are true or not. If the proof is successful then the result is a 'judgment'.
|
||||
For instance, if the ``proposition`` is,
|
||||
|
||||
+-------+
|
||||
| 1+1=2 |
|
||||
+-------+
|
||||
|
||||
When we prove it, the ``judgment`` is,
|
||||
|
||||
+------------+
|
||||
| 1+1=2 true |
|
||||
+------------+
|
||||
|
||||
Or if the ``proposition`` is,
|
||||
|
||||
+-------+
|
||||
| 1+1=3 |
|
||||
+-------+
|
||||
|
||||
Obviously we can't prove it is true, but it is still a valid proposition and perhaps we can prove it is false so the ``judgment`` is,
|
||||
|
||||
+-------------+
|
||||
| 1+1=3 false |
|
||||
+-------------+
|
||||
|
||||
This may seem a bit pedantic but it is important to be careful, in mathematics not every proposition is true or false for instance, a proposition may be unproven or even unprovable.
|
||||
|
||||
So the logic here is different from the logic that comes from boolean algebra. In that case what is not true is false and what is not false is true. The logic we are using here does not have this 'law of excluded middle' so we have to be careful not to use it.
|
||||
|
||||
A false proposition is taken to be a contradiction and if we have a contradiction then we can prove anything, so we need to avoid this. Some languages, used in proof assistants, prevent contradictions but such languages cannot be Turing complete, so Idris does not prevent contradictions.
|
||||
|
||||
The logic we are using is called constructive (or sometimes intuitional) because we are constructing a 'database' of judgments.
|
||||
|
||||
There are also many other types of logic, another important type of logic for Idris programmers is '``linear logic``' but that's not discussed on this page.
|
||||
|
||||
Curry-Howard correspondence
|
||||
===========================
|
||||
|
||||
So how to we relate these proofs to Idris programs? It turns out that there is a correspondence between constructive logic and type theory. They are the same structure and we can switch backward and forward between the two notations because they are the same thing.
|
||||
|
||||
The way that this works is that a proposition is a type so this,
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Idris> 1+1=2
|
||||
2 = 2 : Type
|
||||
|
||||
is a proposition and it is also a type. This is built into Idris so when an '=' equals sign appears in a function type an equality type is generated. The following will also produce an equality type:
|
||||
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Idris> 1+1=3
|
||||
2 = 3 : Type
|
||||
|
||||
Both of these are valid propositions so both are valid equality types. But how do we represent true judgment, that is, how do we denote 1+1=2 is true but not 1+1=3.
|
||||
A type that is true is inhabited, that is, it can be constructed. An equality type has only one constructor 'Refl' so a proof of 1+1=2 is
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
onePlusOne : 1+1=2
|
||||
onePlusOne = Refl
|
||||
|
||||
So how can Refl, which is a constructor without any parameters, construct an equality type? If we type it on its own then it can't:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Idris> Refl
|
||||
(input):Can't infer argument A to Refl, Can't infer argument x to Refl
|
||||
|
||||
So it must pattern match on its return type:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Idris> the (1=1) Refl
|
||||
Refl : 1 = 1
|
||||
|
||||
So now that we can represent propositions as types other aspects of propositional logic can also be translated to types as follows:
|
||||
|
||||
+----------+-------------------+--------------------------+
|
||||
| | propositions | example of possible type |
|
||||
+----------+-------------------+--------------------------+
|
||||
| A | x=y | |
|
||||
+----------+-------------------+--------------------------+
|
||||
| B | y=z | |
|
||||
+----------+-------------------+--------------------------+
|
||||
| and | A /\ B | Pair(x=y,y=z) |
|
||||
+----------+-------------------+--------------------------+
|
||||
| or | A \/ B | Either(x=y,y=z) |
|
||||
+----------+-------------------+--------------------------+
|
||||
| implies | A -> B | (x=y) -> (y=x) |
|
||||
+----------+-------------------+--------------------------+
|
||||
| for all | y=z | |
|
||||
+----------+-------------------+--------------------------+
|
||||
| exists | y=z | |
|
||||
+----------+-------------------+--------------------------+
|
||||
|
||||
|
||||
And (conjunction)
|
||||
-----------------
|
||||
|
||||
We can have a type which corresponds to conjunction:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
AndIntro : a -> b -> A a b
|
||||
|
||||
There is a built in type called 'Pair'.
|
||||
|
||||
Or (disjunction)
|
||||
----------------
|
||||
|
||||
We can have a type which corresponds to disjunction:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Or : Type -> Type -> Type where
|
||||
OrIntroLeft : a -> A a b
|
||||
OrIntroRight : b -> A a b
|
||||
|
||||
There is a built in type called 'Either'.
|
||||
|
||||
Definitional and Propositional Equalities
|
||||
=========================================
|
||||
|
||||
We have seen that we can 'prove' a type by finding a way to construct a term. In the case of equality types there is only one constructor which is 'Refl'.
|
||||
We have also seen that each side of the equation does not have to be identical like '2=2'. It is enough that both sides are ``definitionaly equal`` like this:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
onePlusOne : 1+1=2
|
||||
onePlusOne = Refl
|
||||
|
||||
So both sides of this equation nomalise to 2 and so Refl will type match and the proposition is proved.
|
||||
|
||||
We don't have to stick to terms, can also use symbolic parameters so the following will compile:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
varIdentity : m = m
|
||||
varIdentity = Refl
|
||||
|
||||
If a proposition/equality type is not definitionaly equal but is still true then it is ``propositionaly equal``. In this case we may still be able to prove it but some steps in the proof may require us to add something into the terms or at least to take some sideways steps to get to a proof.
|
||||
|
||||
Especially when working with equalities containing variable terms (inside functions) it can be hard to know which equality types are definitially equal, in this example plusReducesL is '``definitially equal``' but plusReducesR is not (although it is '``propositionaly equal``'). The only difference between them is the order of the operands.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plusReducesL : (n:Nat) -> plus Z n = n
|
||||
plusReducesL n = Refl
|
||||
|
||||
plusReducesR : (n:Nat) -> plus n Z = n
|
||||
plusReducesR n = Refl
|
||||
|
||||
plusReducesR gives the following error:
|
||||
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
- + Errors (1)
|
||||
`-- proof.idr line 6 col 17:
|
||||
When checking right hand side of plusReducesR with expected type
|
||||
plus n 0 = n
|
||||
|
||||
Type mismatch between
|
||||
n = n (Type of Refl)
|
||||
and
|
||||
plus n 0 = n (Expected type)
|
||||
|
||||
Specifically:
|
||||
Type mismatch between
|
||||
n
|
||||
and
|
||||
plus n 0
|
||||
|
||||
So why is 'Refl' able to prove some equality types but not others?
|
||||
|
||||
The first answer is that 'plus' is defined in such a way that it splits on its first argument so it is simple to prove when 0 is the first argument but not the second. So what is the general way to know if Refl will work?
|
||||
|
||||
If an equality type can be proved/constructed by using Refl alone it is known as a ``definitional equality``. In order to be definitinally equal both sides of the equation must normalise to unique values. That is, each step in the proof must reduce the term so each step is effectively forced.
|
||||
|
||||
So when we type 1+1 in Idris it is immediately converted to 2 because definitional equality is built in.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Idris> 1+1
|
||||
2 : Integer
|
||||
|
||||
In the following pages we discuss how to resolve propositionaly equalies.
|
||||
|
||||
Axiomatic and Constructive Approaches
|
||||
=====================================
|
||||
|
||||
How should we define types so that we can do proofs on them? In the natural numbers with plus example we could have started by treating it as a group based on the plus operator. So we have axioms:
|
||||
|
||||
- for all x,y : ``x+y=y+x``
|
||||
- for all x: ``x + 0 = x = 0 + x``
|
||||
- for all x,y,z: ``(x + y) + z = x + (x + z)``
|
||||
|
||||
Then we can implement '+' so that it respects these axioms (presumably implemented in hardware).
|
||||
|
||||
These are axioms, that is a propositions/types that are asserted to be true without proof. In Idris we can use the 'postulate' keyword
|
||||
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
commutePlus ``postulate``: x -> y -> plus x y = plus y x
|
||||
|
||||
Alternatively we could define the natural numbers based on Zero and Successor. The axioms above then become derived rules and we also gain the ability to do inductive proofs.
|
||||
|
||||
As we know, Idris uses both of these approaches with automatic coercion between them which gives the best of both worlds.
|
||||
|
||||
So what can we learn from this to implement out own types:
|
||||
|
||||
- Should we try to implement both approaches?
|
||||
- Should we define our types by constructing up from primitive types?
|
||||
|
||||
Proof theory affects these design decisions.
|
||||
|
||||
|
30
docs/proofs/index.rst
Normal file
30
docs/proofs/index.rst
Normal file
@ -0,0 +1,30 @@
|
||||
.. _proofs-index:
|
||||
|
||||
###############
|
||||
Theorem Proving
|
||||
###############
|
||||
|
||||
A tutorial on theorem proving in Idris.
|
||||
|
||||
NOT YET UPDATED FOR IDRIS 2!
|
||||
|
||||
.. note::
|
||||
|
||||
The documentation for Idris has been published under the Creative
|
||||
Commons CC0 License. As such to the extent possible under law, *The
|
||||
Idris Community* has waived all copyright and related or neighboring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
.. toctree::
|
||||
:maxdepth: 1
|
||||
|
||||
definitional
|
||||
pluscomm
|
||||
inductive
|
||||
patterns
|
||||
propositional
|
||||
interactive
|
||||
interactiveOld
|
||||
|
101
docs/proofs/inductive.rst
Normal file
101
docs/proofs/inductive.rst
Normal file
@ -0,0 +1,101 @@
|
||||
.. _sect-inductive:
|
||||
|
||||
****************
|
||||
Inductive Proofs
|
||||
****************
|
||||
|
||||
Before embarking on proving ``plus_commutes`` in Idris itself, let us
|
||||
consider the overall structure of a proof of some property of natural
|
||||
numbers. Recall that they are defined recursively, as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Nat : Type where
|
||||
Z : Nat
|
||||
S : Nat -> Nat
|
||||
|
||||
A *total* function over natural numbers must both terminate, and cover
|
||||
all possible inputs. Idris checks functions for totality by checking that
|
||||
all inputs are covered, and that all recursive calls are on
|
||||
*structurally smaller* values (so recursion will always reach a base
|
||||
case). Recalling ``plus``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus : Nat -> Nat -> Nat
|
||||
plus Z m = m
|
||||
plus (S k) m = S (plus k m)
|
||||
|
||||
This is total because it covers all possible inputs (the first argument
|
||||
can only be ``Z`` or ``S k`` for some ``k``, and the second argument
|
||||
``m`` covers all possible ``Nat``) and in the recursive call, ``k``
|
||||
is structurally smaller than ``S k`` so the first argument will always
|
||||
reach the base case ``Z`` in any sequence of recursive calls.
|
||||
|
||||
In some sense, this resembles a mathematical proof by induction (and
|
||||
this is no coincidence!). For some property ``P`` of a natural number
|
||||
``x``, we can show that ``P`` holds for all ``x`` if:
|
||||
|
||||
- ``P`` holds for zero (the base case).
|
||||
|
||||
- Assuming that ``P`` holds for ``k``, we can show ``P`` also holds for
|
||||
``S k`` (the inductive step).
|
||||
|
||||
In ``plus``, the property we are trying to show is somewhat trivial (for
|
||||
all natural numbers ``x``, there is a ``Nat`` which need not have any
|
||||
relation to ``x``). However, it still takes the form of a base case and
|
||||
an inductive step. In the base case, we show that there is a ``Nat``
|
||||
arising from ``plus n m`` when ``n = Z``, and in the inductive step we
|
||||
show that there is a ``Nat`` arising when ``n = S k`` and we know we can
|
||||
get a ``Nat`` inductively from ``plus k m``. We could even write a
|
||||
function capturing all such inductive definitions:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
nat_induction : (P : Nat -> Type) -> -- Property to show
|
||||
(P Z) -> -- Base case
|
||||
((k : Nat) -> P k -> P (S k)) -> -- Inductive step
|
||||
(x : Nat) -> -- Show for all x
|
||||
P x
|
||||
nat_induction P p_Z p_S Z = p_Z
|
||||
nat_induction P p_Z p_S (S k) = p_S k (nat_induction P p_Z p_S k)
|
||||
|
||||
Using ``nat_induction``, we can implement an equivalent inductive
|
||||
version of ``plus``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_ind : Nat -> Nat -> Nat
|
||||
plus_ind n m
|
||||
= nat_induction (\x => Nat)
|
||||
m -- Base case, plus_ind Z m
|
||||
(\k, k_rec => S k_rec) -- Inductive step plus_ind (S k) m
|
||||
-- where k_rec = plus_ind k m
|
||||
n
|
||||
|
||||
To prove that ``plus n m = plus m n`` for all natural numbers ``n`` and
|
||||
``m``, we can also use induction. Either we can fix ``m`` and perform
|
||||
induction on ``n``, or vice versa. We can sketch an outline of a proof;
|
||||
performing induction on ``n``, we have:
|
||||
|
||||
- Property ``P`` is ``\x => plus x m = plus m x``.
|
||||
|
||||
- Show that ``P`` holds in the base case and inductive step:
|
||||
|
||||
- | Base case: ``P Z``, i.e.
|
||||
| ``plus Z m = plus m Z``, which reduces to
|
||||
| ``m = plus m Z`` due to the definition of ``plus``.
|
||||
|
||||
- | Inductive step: Inductively, we know that ``P k`` holds for a specific, fixed ``k``, i.e.
|
||||
| ``plus k m = plus m k`` (the induction hypothesis). Given this, show ``P (S k)``, i.e.
|
||||
| ``plus (S k) m = plus m (S k)``, which reduces to
|
||||
| ``S (plus k m) = plus m (S k)``. From the induction hypothesis, we can rewrite this to
|
||||
| ``S (plus m k) = plus m (S k)``.
|
||||
|
||||
To complete the proof we therefore need to show that ``m = plus m Z``
|
||||
for all natural numbers ``m``, and that ``S (plus m k) = plus m (S k)``
|
||||
for all natural numbers ``m`` and ``k``. Each of these can also be
|
||||
proved by induction, this time on ``m``.
|
||||
|
||||
We are now ready to embark on a proof of commutativity of ``plus``
|
||||
formally in Idris.
|
296
docs/proofs/interactive.rst
Normal file
296
docs/proofs/interactive.rst
Normal file
@ -0,0 +1,296 @@
|
||||
***************************
|
||||
Interactive Theorem Proving
|
||||
***************************
|
||||
|
||||
Idris supports interactive theorem proving via elaborator reflection.
|
||||
|
||||
:ref:`elaborator-reflection` is also used to convert high-level Idris code into
|
||||
the core language and for customising the language. Here we show how to use it
|
||||
to interactively construct proofs.
|
||||
|
||||
The primary purpose of the elaboration mechanism is to elaborate Idris and so it
|
||||
is not optimised to work as a proof assistant, however it can interactively
|
||||
construct proofs as described on this page.
|
||||
|
||||
Elab and Pruviloj Libraries
|
||||
===========================
|
||||
|
||||
Elaborator reflection is defined in prelude/Language/Reflection/Elab.idr
|
||||
and pruviloj is defined in Idris-dev/libs/pruviloj/
|
||||
|
||||
``Elab`` defines the basics such as: solve, attack, intro, compute,
|
||||
rewriteWith and others.
|
||||
``pruviloj`` defines some more advanced derived commands such as:
|
||||
reflexivity and others.
|
||||
|
||||
To use ``pruviloj`` call Idris with the "-p pruviloj" option and add:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
import Pruviloj
|
||||
import Pruviloj.Induction
|
||||
|
||||
to the top of your file.
|
||||
|
||||
It is useful to get the docs at the REPL by using the ``:doc`` command, and
|
||||
search the docstrings using ``:apropos``. So to introduce the functions from
|
||||
Elab and Pruviloj, that we will need for the following example, here are
|
||||
their docstrings:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*plusReducesZ> :doc solve
|
||||
Language.Reflection.Elab.Tactics.solve : Elab ()
|
||||
Substitute a guess into a hole.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*plusReducesZ> :doc attack
|
||||
Language.Reflection.Elab.Tactics.attack : Elab ()
|
||||
Convert a hole to make it suitable for bindings - that is, transform
|
||||
it such that it has the form ?h : t . h as opposed to ?h : t . f h.
|
||||
|
||||
The binding tactics require that a hole be directly under its binding,
|
||||
or else the scopes of the generated terms won't make sense. This
|
||||
tactic creates a new hole of the proper form, and points the old hole
|
||||
at it.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*plusReducesZ> :doc intro
|
||||
Language.Reflection.Elab.Tactics.intro : (n : TTName) -> Elab ()
|
||||
Introduce a lambda binding around the current hole and focus on the
|
||||
body. Requires that the hole be in binding form (use attack).
|
||||
Arguments:
|
||||
n : TTName -- the name to use for the argument
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*plusReducesZ> :doc compute
|
||||
Language.Reflection.Elab.Tactics.compute : Elab ()
|
||||
Normalise the goal.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*plusReducesZ> :doc rewriteWith
|
||||
Language.Reflection.Elab.Tactics.rewriteWith : Raw -> Elab ()
|
||||
Attempt to rewrite the goal using an equality.
|
||||
|
||||
The tactic searches the goal for applicable subterms, and constructs a
|
||||
context for replace using them. In some cases, this is not possible,
|
||||
and replace must be called manually with an appropriate context.
|
||||
|
||||
Because this tactic internally introduces a let binding, it requires
|
||||
that the hole be immediately under its binder (use attack if it might
|
||||
not be).
|
||||
|
||||
Here is the command from pruviloj that we will need for the example on
|
||||
this page:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*plusReducesZ> :doc reflexivity
|
||||
Pruviloj.Core.reflexivity : Elab ()
|
||||
A special-purpose tactic that attempts to solve a goal using Refl.
|
||||
This is useful for ensuring that goals in fact are trivial when
|
||||
developing or testing other tactics; otherwise, consider using search.
|
||||
|
||||
Interactive Example: plusReduces
|
||||
================================
|
||||
|
||||
One way to write proofs interactively is to write the general *structure* of
|
||||
the proof, and use the interactive mode to complete the details.
|
||||
Consider the following definition, proved in :ref:`sect-theorems`:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plusReduces : (n:Nat) -> plus Z n = n
|
||||
|
||||
We’ll be constructing the proof by *induction*, so we write the cases for ``Z``
|
||||
and ``S``, with a recursive call in the ``S`` case giving the inductive
|
||||
hypothesis, and insert *holes* for the rest of the definition:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
import Pruviloj
|
||||
import Pruviloj.Induction
|
||||
|
||||
plusReducesZ' : (n:Nat) -> n = plus n Z
|
||||
plusReducesZ' Z = ?plusredZ_Z
|
||||
plusReducesZ' (S k) = let ih = plusReducesZ' k in
|
||||
?plusredZ_S
|
||||
|
||||
On running , two global names are created, ``plusredZ_Z`` and
|
||||
``plusredZ_S``, with no definition.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*theorems> : idris plusReducesZ.idr -p pruviloj
|
||||
|
||||
. / _/___/ /____(_)____
|
||||
/ // __ / ___/ / ___/ Version 1.2.0
|
||||
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
|
||||
/___/\__,_/_/ /_/____/ Type :? for help
|
||||
|
||||
Idris is free software with ABSOLUTELY NO WARRANTY.
|
||||
For details type :warranty.
|
||||
Holes: Main.plusredZ_S, Main.plusredZ_Z
|
||||
|
||||
This tells us that we have two holes Main.plusredZ_S and Main.plusredZ_Z. We can solve
|
||||
these separately, ``plusredZ_Z`` is the simplest so we will do that first.
|
||||
|
||||
The ``:elab plusredZ_Z`` command enters interactive elaboration mode, which can be used to
|
||||
complete the missing definition for plusredZ_Z.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*plusReducesZ> :elab plusredZ_Z
|
||||
|
||||
---------- Goal: ----------
|
||||
{hole_0} : 0 = 0
|
||||
|
||||
This has been normalised to ``0 = 0`` so now we have to prove that ``0`` equals ``0``, which
|
||||
is easy to prove by reflexivity from the pruviloj library:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
-Main.plusredZ_Z> reflexivity
|
||||
plusredZ_Z: No more goals.
|
||||
|
||||
This tells us that the proof is complete. We can now leave the interactive mode which
|
||||
we entered with the ``:elab`` command. We do this with the ``:qed`` command:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
-Main.plusredZ_Z> :qed
|
||||
Proof completed!
|
||||
Main.plusredZ_Z = %runElab (do reflexivity)
|
||||
Holes: Main.plusredZ_S
|
||||
|
||||
This gives us a trace of the proof which is ``plusredZ_Z = %runElab (do reflexivity)``. We
|
||||
can cut & paste this into the hole in the original file. This also tells us that we
|
||||
have another hole ``Main.plusredZ_S`` remaining.
|
||||
|
||||
This remaining proof is bit more complicated, the following diagram gives an overview:
|
||||
|
||||
|image|
|
||||
|
||||
We approach this remaining proof in the same way by using the ``:elab`` command:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*plusReducesZ> :elab plusredZ_S
|
||||
|
||||
|
||||
---------- Goal: ----------
|
||||
{hole_0} : (k : Nat) -> (k = plus k 0) -> S k = S (plus k 0)
|
||||
|
||||
In this case, the goal is a function type, using ``k`` (the argument
|
||||
accessible by pattern matching) and ``ih`` — the local variable
|
||||
containing the result of the recursive call. We can introduce these as
|
||||
assumptions using the ``intro`` tactic twice. The parameter is entered as
|
||||
a constant of type ``TTName`` which is entered as a backtick with double
|
||||
braces \`{{ih}}. This gives:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
-Main.plusredZ_S> intro `{{k}}
|
||||
|
||||
---------- Assumptions: ----------
|
||||
k : Nat
|
||||
---------- Goal: ----------
|
||||
{hole_0} : (k = plus k 0) -> S k = S (plus k 0)
|
||||
-Main.plusredZ_S> intro `{{ih}}
|
||||
|
||||
---------- Assumptions: ----------
|
||||
k : Nat
|
||||
ih : k = plus k 0
|
||||
---------- Goal: ----------
|
||||
{hole_0} : S k = S (plus k 0)
|
||||
|
||||
We know, from the type of ``ih``, that ``k = plus k 0``, so we would
|
||||
like to use this knowledge to replace ``plus k 0`` in the goal with
|
||||
``k``. We can achieve this with the ``rewriteWith`` tactic:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
-Main.plusredZ_S> rewriteWith (Var `{{ih}})
|
||||
|
||||
---------- Assumptions: ----------
|
||||
k : Nat
|
||||
ih : k = plus k 0
|
||||
---------- Goal: ----------
|
||||
{hole_0} : S k = S k
|
||||
|
||||
The ``rewriteWith`` tactic takes an equality proof as an argument, and tries
|
||||
to rewrite the goal using that proof. The ih value is entered as a constant
|
||||
of type ``TTName`` which is entered as a backtick with double braces `{{ih}} but
|
||||
``rewriteWith`` requires an expression of type ``Raw``, rather than just a name,
|
||||
so the Var constructor is used to make a variable. Here, it results in an equality
|
||||
which is trivially provable using reflexivity:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
-Main.plusredZ_S> reflexivity
|
||||
plusredZ_S: No more goals.
|
||||
-Main.plusredZ_S> :qed
|
||||
Proof completed!
|
||||
Main.plusredZ_S = %runElab (do intro `{{k}}
|
||||
intro `{{ih}}
|
||||
rewriteWith (Var `{{ih}})
|
||||
reflexivity)
|
||||
|
||||
We can't just cut & paste this into the hole in the original file like this:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
import Pruviloj
|
||||
import Pruviloj.Induction
|
||||
|
||||
%language ElabReflection
|
||||
|
||||
plusReducesZ' : (n:Nat) -> n = plus n Z
|
||||
plusReducesZ' Z = %runElab (do reflexivity)
|
||||
plusReducesZ' (S k) = let ih = plusReducesZ' k in
|
||||
(%runElab (do intro `{{k}}
|
||||
intro `{{ih}}
|
||||
rewriteWith (Var `{{ih}})
|
||||
reflexivity)
|
||||
)
|
||||
|
||||
because this gives the following error:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Idris> :load elabInteractiveEx2.idr
|
||||
elabInteractiveEx2.idr:10:32:
|
||||
|
|
||||
10 | intro `{{ih}}
|
||||
| ^
|
||||
unexpected "in"
|
||||
expecting dependent type signature
|
||||
|
||||
However if we put the proof into a separate function like this:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
import Pruviloj
|
||||
import Pruviloj.Induction
|
||||
|
||||
%language ElabReflection
|
||||
|
||||
plusredZ_S : (k : Nat) -> (ih:(k = plus k Z)) -> (S k = S (plus k Z))
|
||||
plusredZ_S = %runElab (do intro `{{k}}
|
||||
intro `{{ih}}
|
||||
rewriteWith (Var `{{ih}})
|
||||
reflexivity)
|
||||
|
||||
plusReducesZ' : (n:Nat) -> n = plus n Z
|
||||
plusReducesZ' Z = %runElab (do reflexivity)
|
||||
plusReducesZ' (S k) = let ih = plusReducesZ' k in plusredZ_S k ih
|
||||
|
||||
This then loads [#f1]_ .
|
||||
|
||||
.. [#f1] https://github.com/idris-lang/Idris-dev/issues/4556
|
||||
|
||||
.. |image| image:: ../image/plusReducesProof.png
|
169
docs/proofs/interactiveOld.rst
Normal file
169
docs/proofs/interactiveOld.rst
Normal file
@ -0,0 +1,169 @@
|
||||
**************************************************************
|
||||
DEPRECATED: Interactive Theorem Proving Using Old Tactics Code
|
||||
**************************************************************
|
||||
|
||||
.. warning::
|
||||
The interactive theorem-proving interface documented here has been
|
||||
deprecated in favor of :ref:`elaborator-reflection`.
|
||||
|
||||
Idris also supports interactive theorem proving via tactics. This
|
||||
is generally not recommended to be used directly, but rather used as a
|
||||
mechanism for building proof automation which is beyond the scope of this
|
||||
tutorial. In this section, we briefly discus tactics.
|
||||
|
||||
One way to write proofs interactively is to write the general *structure* of
|
||||
the proof, and use the interactive mode to complete the details.
|
||||
Consider the following definition, proved in :ref:`sect-theorems`:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plusReduces : (n:Nat) -> plus Z n = n
|
||||
|
||||
We’ll be constructing the proof by *induction*, so we write the cases for ``Z``
|
||||
and ``S``, with a recursive call in the ``S`` case giving the inductive
|
||||
hypothesis, and insert *holes* for the rest of the definition:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plusReducesZ' : (n:Nat) -> n = plus n Z
|
||||
plusReducesZ' Z = ?plusredZ_Z
|
||||
plusReducesZ' (S k) = let ih = plusReducesZ' k in
|
||||
?plusredZ_S
|
||||
|
||||
On running , two global names are created, ``plusredZ_Z`` and
|
||||
``plusredZ_S``, with no definition. We can use the ``:m`` command at the
|
||||
prompt to find out which holes are still to be solved (or, more
|
||||
precisely, which functions exist but have no definitions), then the
|
||||
``:t`` command to see their types:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*theorems> :m
|
||||
Global holes:
|
||||
[plusredZ_S,plusredZ_Z]
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*theorems> :t plusredZ_Z
|
||||
plusredZ_Z : Z = plus Z Z
|
||||
|
||||
*theorems> :t plusredZ_S
|
||||
plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
|
||||
|
||||
The ``:p`` command enters interactive proof mode, which can be used to
|
||||
complete the missing definitions.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*theorems> :p plusredZ_Z
|
||||
|
||||
---------------------------------- (plusredZ_Z) --------
|
||||
{hole0} : Z = plus Z Z
|
||||
|
||||
This gives us a list of premises (above the line; there are none here)
|
||||
and the current goal (below the line; named ``{hole0}`` here). At the
|
||||
prompt we can enter tactics to direct the construction of the proof. In
|
||||
this case, we can normalise the goal with the ``compute`` tactic:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
-plusredZ_Z> compute
|
||||
|
||||
---------------------------------- (plusredZ_Z) --------
|
||||
{hole0} : Z = Z
|
||||
|
||||
Now we have to prove that ``Z`` equals ``Z``, which is easy to prove by
|
||||
``Refl``. To apply a function, such as ``Refl``, we use ``refine`` which
|
||||
introduces subgoals for each of the function’s explicit arguments
|
||||
(``Refl`` has none):
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
-plusredZ_Z> refine Refl
|
||||
plusredZ_Z: no more goals
|
||||
|
||||
Here, we could also have used the ``trivial`` tactic, which tries to
|
||||
refine by ``Refl``, and if that fails, tries to refine by each name in
|
||||
the local context. When a proof is complete, we use the ``qed`` tactic
|
||||
to add the proof to the global context, and remove the hole from the
|
||||
unsolved holes list. This also outputs a trace of the proof:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
-plusredZ_Z> qed
|
||||
plusredZ_Z = proof
|
||||
compute
|
||||
refine Refl
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*theorems> :m
|
||||
Global holes:
|
||||
[plusredZ_S]
|
||||
|
||||
The ``:addproof`` command, at the interactive prompt, will add the proof
|
||||
to the source file (effectively in an appendix). Let us now prove the
|
||||
other required lemma, ``plusredZ_S``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*theorems> :p plusredZ_S
|
||||
|
||||
---------------------------------- (plusredZ_S) --------
|
||||
{hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
|
||||
|
||||
In this case, the goal is a function type, using ``k`` (the argument
|
||||
accessible by pattern matching) and ``ih`` — the local variable
|
||||
containing the result of the recursive call. We can introduce these as
|
||||
premises using the ``intro`` tactic twice (or ``intros``, which
|
||||
introduces all arguments as premises). This gives:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
k : Nat
|
||||
ih : k = plus k Z
|
||||
---------------------------------- (plusredZ_S) --------
|
||||
{hole2} : S k = plus (S k) Z
|
||||
|
||||
Since plus is defined by recursion on its first argument, the term
|
||||
``plus (S k) Z`` in the goal can be simplified, so we use ``compute``.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
k : Nat
|
||||
ih : k = plus k Z
|
||||
---------------------------------- (plusredZ_S) --------
|
||||
{hole2} : S k = S (plus k Z)
|
||||
|
||||
We know, from the type of ``ih``, that ``k = plus k Z``, so we would
|
||||
like to use this knowledge to replace ``plus k Z`` in the goal with
|
||||
``k``. We can achieve this with the ``rewrite`` tactic:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
-plusredZ_S> rewrite ih
|
||||
|
||||
k : Nat
|
||||
ih : k = plus k Z
|
||||
---------------------------------- (plusredZ_S) --------
|
||||
{hole3} : S k = S k
|
||||
|
||||
-plusredZ_S>
|
||||
|
||||
The ``rewrite`` tactic takes an equality proof as an argument, and tries
|
||||
to rewrite the goal using that proof. Here, it results in an equality
|
||||
which is trivially provable:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
-plusredZ_S> trivial
|
||||
plusredZ_S: no more goals
|
||||
-plusredZ_S> qed
|
||||
plusredZ_S = proof {
|
||||
intros;
|
||||
rewrite ih;
|
||||
trivial;
|
||||
}
|
||||
|
||||
Again, we can add this proof to the end of our source file using the
|
||||
``:addproof`` command at the interactive prompt.
|
351
docs/proofs/patterns.rst
Normal file
351
docs/proofs/patterns.rst
Normal file
@ -0,0 +1,351 @@
|
||||
***********************
|
||||
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 | ``\o`` | ``C-c C-a`` | Attempt to solve hole under the cursor by applying simple proof search. |
|
||||
+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
|
||||
| Make new definition | ``\d`` | ``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 ``\d`` (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 0
|
||||
|
||||
Note that ``Z`` renders as ``0`` because the pretty printer renders
|
||||
natural numbers as integer literals for readability. 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 = plus m 0
|
||||
|
||||
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
|
||||
|
||||
That is, the hole has been filled with a call to a top level
|
||||
function ``plus_commutes_Z``. The argument ``m`` has been made implicit
|
||||
because it can be inferred from context when it is applied.
|
||||
|
||||
Unfortunately, we cannot prove this lemma directly, since ``plus`` is
|
||||
defined by matching on its *first* argument, and here ``plus m 0`` has a
|
||||
specific value for its *second argument* (in fact, the left hand side of
|
||||
the equality has been reduced from ``plus 0 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 = plus m 0
|
||||
plus_commutes_Z = ?plus_commutes_Z_rhs
|
||||
|
||||
Since we are going to write this by induction on ``m``, which is
|
||||
implicit, we will need to bring ``m`` into scope manually:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes_Z : m = plus m 0
|
||||
plus_commutes_Z {m} = ?plus_commutes_Z_rhs
|
||||
|
||||
Now, case split on ``m`` with ``\c``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes_Z : m = plus m 0
|
||||
plus_commutes_Z {m = Z} = ?plus_commutes_Z_rhs_1
|
||||
plus_commutes_Z {m = (S k)} = ?plus_commutes_Z_rhs_2
|
||||
|
||||
Checking the type of ``plus_commutes_Z_rhs_1`` shows the following,
|
||||
which is easily proved by reflection:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
--------------------------------------
|
||||
plus_commutes_Z_rhs_1 : 0 = 0
|
||||
|
||||
For such trivial proofs, we can let write the proof automatically by
|
||||
pressing ``\o`` with the cursor over ``plus_commutes_Z_rhs_1``.
|
||||
This yields:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes_Z : m = plus m 0
|
||||
plus_commutes_Z {m = Z} = Refl
|
||||
plus_commutes_Z {m = (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 0)
|
||||
|
||||
Inductively, we should know that ``k = plus k 0``, 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 = plus m 0
|
||||
plus_commutes_Z {m = Z} = Refl
|
||||
plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=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 (fromInteger 0)
|
||||
--------------------------------------
|
||||
plus_commutes_Z_rhs_2 : S k = S (plus k 0)
|
||||
|
||||
Again, the ``fromInteger 0`` is merely due to ``Nat`` having an implementation
|
||||
of the ``Num`` interface. So we know that ``k = plus k 0``, 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
|
||||
|
||||
*pluscomm> :t replace
|
||||
replace : (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. 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 ``x``
|
||||
in the required type of ``expr`` and replace it with ``y``. Concretely,
|
||||
in our example, we can say:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in
|
||||
rewrite 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 (fromInteger 0)
|
||||
_rewrite_rule : plus k 0 = k
|
||||
--------------------------------------
|
||||
plus_commutes_Z_rhs_2 : S (plus k 0) = S (plus k 0)
|
||||
|
||||
Using the rewrite rule ``rec`` (which we can see in the context here as
|
||||
``_rewrite_rule``\ [1]_, the goal type has been updated with ``k``
|
||||
replaced by ``plus k 0``.
|
||||
|
||||
Alternatively, we could have applied the rewrite in the other direction
|
||||
using the ``sym`` function:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*pluscomm> :t sym
|
||||
sym : (l = r) -> r = l
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in
|
||||
rewrite sym rec in ?plus_commutes_Z_rhs_2
|
||||
|
||||
In this case, inspecting the type of the hole gives:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
k : Nat
|
||||
rec : k = plus k (fromInteger 0)
|
||||
_rewrite_rule : k = plus k 0
|
||||
--------------------------------------
|
||||
plus_commutes_Z_rhs_2 : S k = S k
|
||||
|
||||
Either way, we can use proof search (``\o``) to complete the
|
||||
proof, giving:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes_Z : m = plus m 0
|
||||
plus_commutes_Z {m = Z} = Refl
|
||||
plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in
|
||||
rewrite rec in Refl
|
||||
|
||||
The base case 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
|
||||
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
|
||||
_rewrite_rule : plus m k = plus k m
|
||||
--------------------------------------
|
||||
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)
|
||||
|
||||
Unlike the previous case, ``k`` and ``m`` are not made implicit because
|
||||
we cannot in general infer arguments to a function from its result.
|
||||
Again, we make a template definition with ``\d``:
|
||||
|
||||
.. 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
|
||||
|
||||
Again, this is defined 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.
|
||||
|
||||
.. [1]
|
||||
Note that the left and right hand sides of the equality have been
|
||||
swapped, because ``replace`` takes a proof of ``x=y`` and the
|
||||
property for ``x``, not ``y``.
|
189
docs/proofs/pluscomm.rst
Normal file
189
docs/proofs/pluscomm.rst
Normal file
@ -0,0 +1,189 @@
|
||||
********************************************
|
||||
Running example: Addition of Natural Numbers
|
||||
********************************************
|
||||
|
||||
Throughout this tutorial, we will be working with the following
|
||||
function, defined in the Idris prelude, which defines addition on
|
||||
natural 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 the
|
||||
properties that adding ``m`` to zero always results in ``m``, and that
|
||||
adding ``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
|
||||
|
||||
Idris> \m => plus Z m
|
||||
\m => m : Nat -> Nat
|
||||
|
||||
Idris> \k,m => plus (S k) m
|
||||
\k => \m => S (plus k m) : Nat -> Nat -> Nat
|
||||
|
||||
Note that unlike many other language REPLs, the Idris REPL performs
|
||||
evaluation on *open* terms, meaning that it can reduce terms which
|
||||
appear inside lambda bindings, like those above. Therefore, we can
|
||||
introduce unknowns ``k`` and ``m`` as lambda bindings and see how
|
||||
``plus`` reduces.
|
||||
|
||||
The ``plus`` function has a number of other useful properties, for
|
||||
example:
|
||||
|
||||
- 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 so
|
||||
we must *prove* them.
|
||||
|
||||
Equality Proofs
|
||||
===============
|
||||
|
||||
Idris has a built-in propositional equality type, conceptually defined
|
||||
as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data (=) : a -> b -> Type where
|
||||
Refl : x = x
|
||||
|
||||
Note that this must be built-in, rather than defined in the library,
|
||||
because ``=`` is a reserved operator — you cannot define this directly
|
||||
in your own code.
|
||||
|
||||
It is *propositional* equality, where the type states that any two
|
||||
values in different types ``a`` and ``b`` may be proposed to be equal.
|
||||
There is only one way to *prove* equality, however, which is by
|
||||
reflexivity (``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 of
|
||||
the 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, so
|
||||
when trying to type check this definition, Idris gives the following
|
||||
error:
|
||||
|
||||
::
|
||||
|
||||
When elaborating right hand side of four_eq_five:
|
||||
Type mismatch between
|
||||
x = x (Type of Refl)
|
||||
and
|
||||
4 = 5 (Expected type)
|
||||
|
||||
Type checking equality proofs
|
||||
-----------------------------
|
||||
|
||||
An important step in type checking Idris programs is *unification*,
|
||||
which attempts to resolve implicit arguments such as the implicit
|
||||
argument ``x`` in ``Refl``. As far as our understanding of type checking
|
||||
proofs is concerned, it suffices to know that unifying two terms
|
||||
involves reducing both to normal form then trying to find an assignment
|
||||
to 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 requires
|
||||
that ``x`` be both ``4`` and ``5``, and therefore fail.
|
||||
|
||||
Since type checking involves reduction to normal form, we can write the
|
||||
following 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 propose
|
||||
equalities between values in different types:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
idris_not_php : 2 = "2"
|
||||
|
||||
Obviously, in Idris the type ``2 = "2"`` is uninhabited, and one might
|
||||
wonder why it is useful to be able to propose equalities between values
|
||||
in different types. However, with dependent types, such equalities can
|
||||
arise naturally. For example, if two vectors 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 because
|
||||
their lengths are different, but we would still like to draw a
|
||||
conclusion 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 only
|
||||
valid value for ``ys`` is ``xs``, because they must be equal, and
|
||||
therefore their types must be equal, so the lengths must be equal.
|
||||
|
||||
Alternatively, we can put an underscore for the second ``xs``, since
|
||||
there 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 number
|
||||
addition 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 different
|
||||
ways of proving ``plus_commutes`` (or, to put it another way, writing
|
||||
the function.) We will also discuss how to use such equality proofs, and
|
||||
see where the need for them arises in practice.
|
||||
|
||||
.. [1]
|
||||
This is known as the Curry-Howard correspondence.
|
128
docs/proofs/propositional.rst
Normal file
128
docs/proofs/propositional.rst
Normal file
@ -0,0 +1,128 @@
|
||||
This page attempts to explain some of the techniques used in Idris to prove propositional equalities.
|
||||
|
||||
Proving Propositional Equality
|
||||
==============================
|
||||
|
||||
We have seen that definitional equalities can be proved using Refl since they always normalise to unique values that can be compared directly.
|
||||
|
||||
However with propositional equalities we are using symbolic variables they do not always normalse.
|
||||
|
||||
So to take the previous example:
|
||||
|
||||
plusReducesR : (n:Nat) -> plus n Z = n
|
||||
|
||||
In this case 'plus n Z' does not normalise to n. Even though both sides are equal we cannot pattern match Refl.
|
||||
|
||||
If the pattern match cannot match for all 'n' then the way around this is to separately match all possible values of 'n'. In the case of natural numbers we do this by induction.
|
||||
|
||||
So here:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plusReducesR : n = plus n 0
|
||||
plusReducesR {n = Z} = Refl
|
||||
plusReducesR {n = (S k)} = let rec = plus_commutes_Z {n=k} in
|
||||
rewrite rec in Refl
|
||||
|
||||
we don't call Refl to match on 'n = plus n 0' forall 'n' we call it for every number separately. So, in the second line, the pattern matcher knows to substitute Z for n in the type being matched. This uses 'rewrite' which is explained below.
|
||||
|
||||
Replace
|
||||
=======
|
||||
|
||||
This implements the 'indiscernability of identicals' principle, if two terms are equal then they have the same properties. In other words, if x=y, then we can substitute y for x in any expression. In our proofs we can express this as:
|
||||
|
||||
if x=y
|
||||
then P x = P y
|
||||
|
||||
where P is a pure function representing the property. In the examples below P is an expression in some variable with a type like this: P: n -> Type
|
||||
|
||||
So if n is a natural number variable then P could be something like 2*n + 3.
|
||||
|
||||
To use this in our proofs there is the following function in the prelude:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
||| Perform substitution in a term according to some equality.
|
||||
replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
|
||||
replace Refl prf = prf
|
||||
|
||||
Removing the implicits, if we supply an equality (x=y) and a proof of a property of x (P x) then we get a proof of a property of y (P y)
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
> :t replace
|
||||
replace : (x = y) -> P x -> P y
|
||||
|
||||
So, in the following example, if we supply p1 x which is a proof that x=2 and the equality x=y then we get a proof that y=2.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
p1: Nat -> Type
|
||||
p1 n = (n=2)
|
||||
|
||||
testReplace: (x=y) -> (p1 x) -> (p1 y)
|
||||
testReplace a b = replace a b
|
||||
|
||||
Rewrite
|
||||
=======
|
||||
|
||||
Similar to 'replace' above but Idris provides a nicer syntax which makes 'rewrite' easier to use in examples like plusReducesR above.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x
|
||||
rewrite__impl p Refl prf = prf
|
||||
|
||||
The difference from 'replace' above is nicer syntax and the property p1 is explicitly supplied and it goes in the opposite direction (input and output reversed).
|
||||
|
||||
Example: again we supply p1 which is a proof that x=2 and the equality x=y then we get a proof that y=2.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
p1: Nat -> Type
|
||||
p1 x = (x=2)
|
||||
|
||||
testRewrite2: (x=y) -> (p1 y) -> (p1 x)
|
||||
testRewrite2 a b = rewrite a in b
|
||||
|
||||
We can think of rewrite doing this:
|
||||
|
||||
* Start with a equation x=y and a property P: x -> Type
|
||||
* Searches y in P
|
||||
* Replaces all occurrences of y with x in P.
|
||||
|
||||
That is, we are doing a substitution.
|
||||
|
||||
Symmetry and Transitivity
|
||||
=========================
|
||||
|
||||
In addition to 'reflexivity' equality also obeys 'symmetry' and 'transitivity' and these are also included in the prelude:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
||| Symmetry of propositional equality
|
||||
sym : {left:a} -> {right:b} -> left = right -> right = left
|
||||
sym Refl = Refl
|
||||
|
||||
||| Transitivity of propositional equality
|
||||
trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c
|
||||
trans Refl Refl = Refl
|
||||
|
||||
Heterogeneous Equality
|
||||
======================
|
||||
|
||||
Also included in the prelude:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
||| Explicit heterogeneous ("John Major") equality. Use this when Idris
|
||||
||| incorrectly chooses homogeneous equality for `(=)`.
|
||||
||| @ a the type of the left side
|
||||
||| @ b the type of the right side
|
||||
||| @ x the left side
|
||||
||| @ y the right side
|
||||
(~=~) : (x : a) -> (y : b) -> Type
|
||||
(~=~) x y = (x = y)
|
||||
|
||||
|
||||
|
@ -35,7 +35,6 @@ changes since Idris 1, see :ref:`updates-index`.
|
||||
interp
|
||||
views
|
||||
theorems
|
||||
provisional
|
||||
interactive
|
||||
syntax
|
||||
miscellany
|
||||
|
@ -1,279 +0,0 @@
|
||||
.. _sect-provisional:
|
||||
|
||||
***********************
|
||||
Provisional Definitions
|
||||
***********************
|
||||
|
||||
[NOT UPDATED FOR IDRIS 2 YET, AND PROBABLY TO BE DELETED]
|
||||
|
||||
Sometimes when programming with dependent types, the type required by
|
||||
the type checker and the type of the program we have written will be
|
||||
different (in that they do not have the same normal form), but
|
||||
nevertheless provably equal. For example, recall the ``parity``
|
||||
function:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Parity : Nat -> Type where
|
||||
Even : Parity (n + n)
|
||||
Odd : Parity (S (n + n))
|
||||
|
||||
We’d like to implement this as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
parity : (n:Nat) -> Parity n
|
||||
parity Z = Even {n=Z}
|
||||
parity (S Z) = Odd {n=Z}
|
||||
parity (S (S k)) with (parity k)
|
||||
parity (S (S (j + j))) | Even = Even {n=S j}
|
||||
parity (S (S (S (j + j)))) | Odd = Odd {n=S j}
|
||||
|
||||
This simply states that zero is even, one is odd, and recursively, the
|
||||
parity of ``k+2`` is the same as the parity of ``k``. Explicitly marking
|
||||
the value of ``n`` is even and odd is necessary to help type inference.
|
||||
Unfortunately, the type checker rejects this:
|
||||
|
||||
::
|
||||
|
||||
viewsbroken.idr:12:10:When elaborating right hand side of ViewsBroken.parity:
|
||||
Type mismatch between
|
||||
Parity (plus (S j) (S j))
|
||||
and
|
||||
Parity (S (S (plus j j)))
|
||||
|
||||
Specifically:
|
||||
Type mismatch between
|
||||
plus (S j) (S j)
|
||||
and
|
||||
S (S (plus j j))
|
||||
|
||||
The type checker is telling us that ``(j+1)+(j+1)`` and ``2+j+j`` do not
|
||||
normalise to the same value. This is because ``plus`` is defined by
|
||||
recursion on its first argument, and in the second value, there is a
|
||||
successor symbol on the second argument, so this will not help with
|
||||
reduction. These values are obviously equal — how can we rewrite the
|
||||
program to fix this problem?
|
||||
|
||||
Provisional definitions
|
||||
=======================
|
||||
|
||||
*Provisional definitions* help with this problem by allowing us to defer
|
||||
the proof details until a later point. There are two main reasons why
|
||||
they are useful.
|
||||
|
||||
- When *prototyping*, it is useful to be able to test programs before
|
||||
finishing all the details of proofs.
|
||||
|
||||
- When *reading* a program, it is often much clearer to defer the proof
|
||||
details so that they do not distract the reader from the underlying
|
||||
algorithm.
|
||||
|
||||
Provisional definitions are written in the same way as ordinary
|
||||
definitions, except that they introduce the right hand side with a
|
||||
``?=`` rather than ``=``. We define ``parity`` as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
parity : (n:Nat) -> Parity n
|
||||
parity Z = Even {n=Z}
|
||||
parity (S Z) = Odd {n=Z}
|
||||
parity (S (S k)) with (parity k)
|
||||
parity (S (S (j + j))) | Even ?= Even {n=S j}
|
||||
parity (S (S (S (j + j)))) | Odd ?= Odd {n=S j}
|
||||
|
||||
When written in this form, instead of reporting a type error, Idris
|
||||
will insert a hole standing for a theorem which will correct the
|
||||
type error. Idris tells us we have two proof obligations, with names
|
||||
generated from the module and function names:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*views> :m
|
||||
Global holes:
|
||||
[views.parity_lemma_2,views.parity_lemma_1]
|
||||
|
||||
The first of these has the following type:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*views> :p views.parity_lemma_1
|
||||
|
||||
---------------------------------- (views.parity_lemma_1) --------
|
||||
{hole0} : (j : Nat) -> (Parity (plus (S j) (S j))) -> Parity (S (S (plus j j)))
|
||||
|
||||
-views.parity_lemma_1>
|
||||
|
||||
The two arguments are ``j``, the variable in scope from the pattern
|
||||
match, and ``value``, which is the value we gave in the right hand side
|
||||
of the provisional definition. Our goal is to rewrite the type so that
|
||||
we can use this value. We can achieve this using the following theorem
|
||||
from the prelude:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
|
||||
S (left + right) = left + (S right)
|
||||
|
||||
We need to use ``compute`` again to unfold the definition of ``plus``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
-views.parity_lemma_1> compute
|
||||
|
||||
|
||||
---------------------------------- (views.parity_lemma_1) --------
|
||||
{hole0} : (j : Nat) -> (Parity (S (plus j (S j)))) -> Parity (S (S (plus j j)))
|
||||
|
||||
After applying ``intros`` we have:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
-views.parity_lemma_1> intros
|
||||
|
||||
j : Nat
|
||||
value : Parity (S (plus j (S j)))
|
||||
---------------------------------- (views.parity_lemma_1) --------
|
||||
{hole2} : Parity (S (S (plus j j)))
|
||||
|
||||
Then we apply the ``plusSuccRightSucc`` rewrite rule, symmetrically, to
|
||||
``j`` and ``j``, giving:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
-views.parity_lemma_1> rewrite sym (plusSuccRightSucc j j)
|
||||
|
||||
j : Nat
|
||||
value : Parity (S (plus j (S j)))
|
||||
---------------------------------- (views.parity_lemma_1) --------
|
||||
{hole3} : Parity (S (plus j (S j)))
|
||||
|
||||
``sym`` is a function, defined in the library, which reverses the order
|
||||
of the rewrite:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
sym : l = r -> r = l
|
||||
sym Refl = Refl
|
||||
|
||||
We can complete this proof using the ``trivial`` tactic, which finds
|
||||
``value`` in the premises. The proof of the second lemma proceeds in
|
||||
exactly the same way.
|
||||
|
||||
We can now test the ``natToBin`` function from Section :ref:`sect-nattobin`
|
||||
at the prompt. The number 42 is 101010 in binary. The binary digits are
|
||||
reversed:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*views> show (natToBin 42)
|
||||
"[False, True, False, True, False, True]" : String
|
||||
|
||||
Suspension of Disbelief
|
||||
=======================
|
||||
|
||||
Idris requires that proofs be complete before compiling programs
|
||||
(although evaluation at the prompt is possible without proof details).
|
||||
Sometimes, especially when prototyping, it is easier not to have to do
|
||||
this. It might even be beneficial to test programs before attempting to
|
||||
prove things about them — if testing finds an error, you know you had
|
||||
better not waste your time proving something!
|
||||
|
||||
Therefore, Idris provides a built-in coercion function, which allows
|
||||
you to use a value of the incorrect types:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
believe_me : a -> b
|
||||
|
||||
Obviously, this should be used with extreme caution. It is useful when
|
||||
prototyping, and can also be appropriate when asserting properties of
|
||||
external code (perhaps in an external C library). The “proof” of
|
||||
``views.parity_lemma_1`` using this is:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
views.parity_lemma_2 = proof {
|
||||
intro;
|
||||
intro;
|
||||
exact believe_me value;
|
||||
}
|
||||
|
||||
The ``exact`` tactic allows us to provide an exact value for the proof.
|
||||
In this case, we assert that the value we gave was correct.
|
||||
|
||||
Example: Binary numbers
|
||||
=======================
|
||||
|
||||
Previously, we implemented conversion to binary numbers using the
|
||||
``Parity`` view. Here, we show how to use the same view to implement a
|
||||
verified conversion to binary. We begin by indexing binary numbers over
|
||||
their ``Nat`` equivalent. This is a common pattern, linking a
|
||||
representation (in this case ``Binary``) with a meaning (in this case
|
||||
``Nat``):
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Binary : Nat -> Type where
|
||||
BEnd : Binary Z
|
||||
BO : Binary n -> Binary (n + n)
|
||||
BI : Binary n -> Binary (S (n + n))
|
||||
|
||||
``BO`` and ``BI`` take a binary number as an argument and effectively
|
||||
shift it one bit left, adding either a zero or one as the new least
|
||||
significant bit. The index, ``n + n`` or ``S (n + n)`` states the result
|
||||
that this left shift then add will have to the meaning of the number.
|
||||
This will result in a representation with the least significant bit at
|
||||
the front.
|
||||
|
||||
Now a function which converts a Nat to binary will state, in the type,
|
||||
that the resulting binary number is a faithful representation of the
|
||||
original Nat:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
natToBin : (n:Nat) -> Binary n
|
||||
|
||||
The ``Parity`` view makes the definition fairly simple — halving the
|
||||
number is effectively a right shift after all — although we need to use
|
||||
a provisional definition in the Odd case:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
natToBin : (n:Nat) -> Binary n
|
||||
natToBin Z = BEnd
|
||||
natToBin (S k) with (parity k)
|
||||
natToBin (S (j + j)) | Even = BI (natToBin j)
|
||||
natToBin (S (S (j + j))) | Odd ?= BO (natToBin (S j))
|
||||
|
||||
The problem with the Odd case is the same as in the definition of
|
||||
``parity``, and the proof proceeds in the same way:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
natToBin_lemma_1 = proof {
|
||||
intro;
|
||||
intro;
|
||||
rewrite sym (plusSuccRightSucc j j);
|
||||
trivial;
|
||||
}
|
||||
|
||||
To finish, we’ll implement a main program which reads an integer from
|
||||
the user and outputs it in binary.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
main : IO ()
|
||||
main = do putStr "Enter a number: "
|
||||
x <- getLine
|
||||
print (natToBin (fromInteger (cast x)))
|
||||
|
||||
For this to work, of course, we need a ``Show`` implementation for
|
||||
``Binary n``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Show (Binary n) where
|
||||
show (BO x) = show x ++ "0"
|
||||
show (BI x) = show x ++ "1"
|
||||
show BEnd = ""
|
@ -98,14 +98,14 @@ by recursion on the first argument to ``plus``, namely ``n``.
|
||||
|
||||
plusReducesZ : (n:Nat) -> n = plus n Z
|
||||
plusReducesZ Z = Refl
|
||||
plusReducesZ (S k) = cong (plusReducesZ k)
|
||||
plusReducesZ (S k) = cong S (plusReducesZ k)
|
||||
|
||||
``cong`` is a function defined in the library which states that equality
|
||||
respects function application:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
cong : {f : t -> u} -> a = b -> f a = f b
|
||||
cong : (f : t -> u) -> a = b -> f a = f b
|
||||
|
||||
We can do the same for the reduction behaviour of plus on successors:
|
||||
|
||||
@ -113,9 +113,9 @@ We can do the same for the reduction behaviour of plus on successors:
|
||||
|
||||
plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
|
||||
plusReducesS Z m = Refl
|
||||
plusReducesS (S k) m = cong (plusReducesS k m)
|
||||
plusReducesS (S k) m = cong S (plusReducesS k m)
|
||||
|
||||
Even for trivial theorems like these, the proofs are a little tricky to
|
||||
Even for small theorems like these, the proofs are a little tricky to
|
||||
construct in one go. When things get even slightly more complicated, it
|
||||
becomes too much to think about to construct proofs in this “batch
|
||||
mode”.
|
||||
@ -137,8 +137,8 @@ previously (:ref:`sec-views`) we implemented ``natToBin`` using a function
|
||||
|
||||
parity : (n:Nat) -> Parity n
|
||||
|
||||
However, we didn't provide a definition for ``parity``. We might expect it
|
||||
to look something like the following:
|
||||
We provided a definition for ``parity``, but without explanation. We might
|
||||
hope that it would look something like the following:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -153,13 +153,11 @@ Unfortunately, this fails with a type error:
|
||||
|
||||
::
|
||||
|
||||
When checking right hand side of with block in views.parity with expected type
|
||||
Parity (S (S (j + j)))
|
||||
|
||||
Type mismatch between
|
||||
Parity (S j + S j) (Type of Even)
|
||||
With.idr:26:17--27:3:While processing right hand side of Main.with block in 2419 at With.idr:24:3--27:3:
|
||||
Can't solve constraint between:
|
||||
plus j (S j)
|
||||
and
|
||||
Parity (S (S (plus j j))) (Expected type)
|
||||
S (plus j j)
|
||||
|
||||
The problem is that normalising ``S j + S j``, in the type of ``Even``
|
||||
doesn't result in what we need for the type of the right hand side of
|
||||
@ -236,10 +234,10 @@ the type of the equation we just used (as the type of ``_rewrite_rule``):
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
j : Nat
|
||||
p : Parity (S (plus j (S j)))
|
||||
_rewrite_rule : S (plus j j) = plus j (S j)
|
||||
--------------------------------------
|
||||
Main> :t helpEven_rhs
|
||||
j : Nat
|
||||
p : Parity (S (plus j (S j)))
|
||||
-------------------------------------
|
||||
helpEven_rhs : Parity (S (plus j (S j)))
|
||||
|
||||
Using ``rewrite`` and another helper for the ``Odd`` case, we can complete
|
||||
@ -292,35 +290,29 @@ definitions is total:
|
||||
|
||||
::
|
||||
|
||||
*Theorems> :total empty1
|
||||
possibly not total due to: empty1#hd
|
||||
not total as there are missing cases
|
||||
*Theorems> :total empty2
|
||||
possibly not total due to recursive path empty2
|
||||
Void> :total empty1
|
||||
Void.empty1 is not covering due to call to function empty1:hd
|
||||
Void> :total empty2
|
||||
Void.empty2 is possibly not terminating due to recursive path Void.empty2
|
||||
|
||||
Note the use of the word “possibly” — a totality check can, of course,
|
||||
never be certain due to the undecidability of the halting problem. The
|
||||
check is, therefore, conservative. It is also possible (and indeed
|
||||
advisable, in the case of proofs) to mark functions as total so that it
|
||||
will be a compile time error for the totality check to fail:
|
||||
Note the use of the word “possibly” — a totality check can never be certain due
|
||||
to the undecidability of the halting problem. The check is, therefore,
|
||||
conservative. It is also possible (and indeed advisable, in the case of proofs)
|
||||
to mark functions as total so that it will be a compile time error for the
|
||||
totality check to fail:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
total empty2 : Void
|
||||
empty2 = empty2
|
||||
|
||||
::
|
||||
|
||||
Type checking ./theorems.idr
|
||||
theorems.idr:25:empty2 is possibly not total due to recursive path empty2
|
||||
|
||||
Reassuringly, our proof in Section :ref:`sect-empty` that the zero and
|
||||
successor constructors are disjoint is total:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
*theorems> :total disjoint
|
||||
Total
|
||||
Main> :total disjoint
|
||||
Main.disjoint is Total
|
||||
|
||||
The totality check is, necessarily, conservative. To be recorded as
|
||||
total, a function ``f`` must:
|
||||
@ -338,6 +330,8 @@ total, a function ``f`` must:
|
||||
Directives and Compiler Flags for Totality
|
||||
------------------------------------------
|
||||
|
||||
[NOTE: Not all of this is implemented yet for Idris 2]
|
||||
|
||||
By default, Idris allows all well-typed definitions, whether total or not.
|
||||
However, it is desirable for functions to be total as far as possible, as this
|
||||
provides a guarantee that they provide a result for all possible inputs, in
|
||||
|
@ -65,8 +65,8 @@ extraneous and may be omitted:
|
||||
.. code-block:: idris
|
||||
|
||||
foo : Int -> Int -> Bool
|
||||
foo n m with (succ n)
|
||||
foo _ m | 2 with (succ m)
|
||||
foo n m with (n + 1)
|
||||
foo _ m | 2 with (m + 1)
|
||||
foo _ _ | 2 | 3 = True
|
||||
foo _ _ | 2 | _ = False
|
||||
foo _ _ | _ = False
|
||||
@ -81,12 +81,13 @@ Otherwise, it is the sum of two equal ``Nat`` plus one:
|
||||
.. code-block:: idris
|
||||
|
||||
data Parity : Nat -> Type where
|
||||
Even : Parity (n + n)
|
||||
Odd : Parity (S (n + n))
|
||||
Even : {n : _} -> Parity (n + n)
|
||||
Odd : {n : _} -> Parity (S (n + n))
|
||||
|
||||
We say ``Parity`` is a *view* of ``Nat``. It has a *covering function*
|
||||
which tests whether it is even or odd and constructs the predicate
|
||||
accordingly.
|
||||
accordingly. Note that we're going to need access to ``n`` at run time, so
|
||||
although it's an implicit argument, it has unrestricted multiplicity.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -129,29 +130,26 @@ Note that there is a function in the patterns (``+``) and repeated
|
||||
occurrences of ``j`` - this is allowed because another argument has
|
||||
determined the form of these patterns.
|
||||
|
||||
We will return to this function in the next section :ref:`sect-parity` to
|
||||
complete the definition of ``parity``.
|
||||
Defining ``parity``
|
||||
===================
|
||||
|
||||
With and proofs
|
||||
===============
|
||||
To use a dependent pattern match for theorem proving, it is sometimes necessary
|
||||
to explicitly construct the proof resulting from the pattern match.
|
||||
To do this, you can postfix the with clause with ``proof p`` and the proof
|
||||
generated by the pattern match will be in scope and named ``p``. For example:
|
||||
The definition of ``parity`` is a little tricky, and requires some knowledge of
|
||||
theorem proving (see Section :ref:`sect-theorems`), but for completeness, here
|
||||
it is:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Foo = FInt Int | FBool Bool
|
||||
|
||||
optional : Foo -> Maybe Int
|
||||
optional (FInt x) = Just x
|
||||
optional (FBool b) = Nothing
|
||||
|
||||
isFInt : (foo:Foo) -> Maybe (x : Int ** (optional foo = Just x))
|
||||
isFInt foo with (optional foo) proof p
|
||||
isFInt foo | Nothing = Nothing -- here, p : Nothing = optional foo
|
||||
isFInt foo | (Just x) = Just (x ** Refl) -- here, p : Just x = optional foo
|
||||
parity : (n : Nat) -> Parity n
|
||||
parity Z = Even {n = Z}
|
||||
parity (S Z) = Odd {n = Z}
|
||||
parity (S (S k)) with (parity k)
|
||||
parity (S (S (j + j))) | Even
|
||||
= rewrite plusSuccRightSucc j j in Even {n = S j}
|
||||
parity (S (S (S (j + j)))) | Odd
|
||||
= rewrite plusSuccRightSucc j j in Odd {n = S j}
|
||||
|
||||
For full details on ``rewrite`` in particular, please refer to the theorem
|
||||
proving tutorial, in Section :ref:`proofs-index`.
|
||||
|
||||
.. [1] Conor McBride and James McKinna. 2004. The view from the
|
||||
left. J. Funct. Program. 14, 1 (January 2004),
|
||||
|
23
samples/Proofs.idr
Normal file
23
samples/Proofs.idr
Normal file
@ -0,0 +1,23 @@
|
||||
fiveIsFive : 5 = 5
|
||||
fiveIsFive = Refl
|
||||
|
||||
twoPlusTwo : 2 + 2 = 4
|
||||
twoPlusTwo = Refl
|
||||
|
||||
disjoint : (n : Nat) -> Z = S n -> Void
|
||||
disjoint n prf = replace {p = disjointTy} prf ()
|
||||
where
|
||||
disjointTy : Nat -> Type
|
||||
disjointTy Z = ()
|
||||
disjointTy (S k) = Void
|
||||
|
||||
plusReduces : (n:Nat) -> plus Z n = n
|
||||
plusReduces n = Refl
|
||||
|
||||
plusReducesZ : (n:Nat) -> n = plus n Z
|
||||
plusReducesZ Z = Refl
|
||||
plusReducesZ (S k) = cong S (plusReducesZ k)
|
||||
|
||||
plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
|
||||
plusReducesS Z m = Refl
|
||||
plusReducesS (S k) m = cong S (plusReducesS k m)
|
11
samples/Void.idr
Normal file
11
samples/Void.idr
Normal file
@ -0,0 +1,11 @@
|
||||
module Void
|
||||
|
||||
-- making use of 'hd' being partially defined
|
||||
empty1 : Void
|
||||
empty1 = hd [] where
|
||||
hd : List a -> a
|
||||
hd (x :: xs) = x
|
||||
|
||||
-- not terminating
|
||||
empty2 : Void
|
||||
empty2 = empty2
|
47
samples/With.idr
Normal file
47
samples/With.idr
Normal file
@ -0,0 +1,47 @@
|
||||
import Data.Vect
|
||||
import Data.Nat
|
||||
|
||||
my_filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
|
||||
my_filter p [] = ( _ ** [] )
|
||||
my_filter p (x :: xs) with (filter p xs)
|
||||
my_filter p (x :: xs) | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
|
||||
|
||||
foo : Int -> Int -> Bool
|
||||
foo n m with (n + 1)
|
||||
foo _ m | 2 with (m + 1)
|
||||
foo _ _ | 2 | 3 = True
|
||||
foo _ _ | 2 | _ = False
|
||||
foo _ _ | _ = False
|
||||
|
||||
data Parity : Nat -> Type where
|
||||
Even : {n : _} -> Parity (n + n)
|
||||
Odd : {n : _} ->Parity (S (n + n))
|
||||
|
||||
-- parity : (n : Nat) -> Parity n
|
||||
-- parity Z = Even {n = Z}
|
||||
-- parity (S Z) = Odd {n = Z}
|
||||
-- parity (S (S k)) with (parity k)
|
||||
-- parity (S (S (j + j))) | Even
|
||||
-- = rewrite plusSuccRightSucc j j in Even {n = S j}
|
||||
-- parity (S (S (S (j + j)))) | Odd
|
||||
-- = rewrite plusSuccRightSucc j j in Odd {n = S j}
|
||||
|
||||
helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
|
||||
helpEven j p = rewrite plusSuccRightSucc j j in p
|
||||
|
||||
helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))
|
||||
helpOdd j p = rewrite plusSuccRightSucc j j in p
|
||||
|
||||
parity : (n:Nat) -> Parity n
|
||||
parity Z = Even {n=Z}
|
||||
parity (S Z) = Odd {n=Z}
|
||||
parity (S (S k)) with (parity k)
|
||||
parity (S (S (j + j))) | Even = helpEven j (Even {n = S j})
|
||||
parity (S (S (S (j + j)))) | Odd = helpOdd j (Odd {n = S j})
|
||||
|
||||
natToBin : Nat -> List Bool
|
||||
natToBin Z = Nil
|
||||
natToBin k with (parity k)
|
||||
natToBin (j + j) | Even = False :: natToBin j
|
||||
natToBin (S (j + j)) | Odd = True :: natToBin j
|
||||
|
@ -588,11 +588,11 @@ export
|
||||
Show PartialReason where
|
||||
show NotStrictlyPositive = "not strictly positive"
|
||||
show (BadCall [n])
|
||||
= "not terminating due to call to " ++ show n
|
||||
= "possibly not terminating due to call to " ++ show n
|
||||
show (BadCall ns)
|
||||
= "not terminating due to calls to " ++ showSep ", " (map show ns)
|
||||
= "possibly not terminating due to calls to " ++ showSep ", " (map show ns)
|
||||
show (RecPath ns)
|
||||
= "not terminating due to recursive path " ++ showSep " -> " (map show ns)
|
||||
= "possibly not terminating due to recursive path " ++ showSep " -> " (map show ns)
|
||||
|
||||
public export
|
||||
data Terminating
|
||||
|
@ -4,14 +4,14 @@ Main> Main.foo is total
|
||||
Main> Main.ordElim is total
|
||||
Main> Main.bar is total
|
||||
Main> Main.swapR is total
|
||||
Main> Main.loopy is not terminating due to recursive path Main.loopy
|
||||
Main> Main.loopy is possibly not terminating due to recursive path Main.loopy
|
||||
Main> Main.foom is total
|
||||
Main> Main.pfoom is not terminating due to recursive path Main.pfoom -> Main.pfoom
|
||||
Main> Main.pfoom is possibly not terminating due to recursive path Main.pfoom -> Main.pfoom
|
||||
Main> Main.even is total
|
||||
Main> Main.vtrans is not terminating due to recursive path Main.vtrans -> Main.vtrans
|
||||
Main> Main.vtrans is possibly not terminating due to recursive path Main.vtrans -> Main.vtrans
|
||||
Main> Main.GTree is total
|
||||
Main> Main.size is total
|
||||
Main> Main.qsortBad is not terminating due to recursive path Main.qsortBad -> Main.qsortBad
|
||||
Main> Main.qsortBad is possibly not terminating due to recursive path Main.qsortBad -> Main.qsortBad
|
||||
Main> Main.qsort is total
|
||||
Main> Main.qsort' is total
|
||||
Main> Main.mySorted is total
|
||||
|
@ -1,9 +1,9 @@
|
||||
1/1: Building Total (Total.idr)
|
||||
Main> Main.Bad is not strictly positive
|
||||
Main> Main.Bad1 is not strictly positive
|
||||
Main> Main.Bad2 is not terminating due to call to Main.Bad1
|
||||
Main> Main.foo is not terminating due to call to Main.MkBad'
|
||||
Main> Main.foo2 is not terminating due to call to Main.MkBad'
|
||||
Main> Main.Bad2 is possibly not terminating due to call to Main.Bad1
|
||||
Main> Main.foo is possibly not terminating due to call to Main.MkBad'
|
||||
Main> Main.foo2 is possibly not terminating due to call to Main.MkBad'
|
||||
Main> Main.T is not strictly positive
|
||||
Main> Main.T2 is not terminating due to call to Main.T
|
||||
Main> Main.T2 is possibly not terminating due to call to Main.T
|
||||
Main> Bye for now!
|
||||
|
@ -1,8 +1,8 @@
|
||||
1/1: Building Total (Total.idr)
|
||||
Main> Main.count is total
|
||||
Main> Main.badCount is not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:873:1--877:1 -> Prelude.map
|
||||
Main> Main.badCount is possibly not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:873:1--877:1 -> Prelude.map
|
||||
Main> Main.process is total
|
||||
Main> Main.badProcess is not terminating due to recursive path Main.badProcess -> Main.badProcess -> Main.badProcess
|
||||
Main> Main.badProcess is possibly not terminating due to recursive path Main.badProcess -> Main.badProcess -> Main.badProcess
|
||||
Main> Main.doubleInt is total
|
||||
Main> Main.main is total
|
||||
Main> Bye for now!
|
||||
|
@ -5,5 +5,5 @@ Yaffle> Main.ack is total
|
||||
Yaffle> Main.foo is total
|
||||
Yaffle> Main.foo' is total
|
||||
Yaffle> Main.foom is total
|
||||
Yaffle> Main.pfoom is not terminating due to recursive path Main.pfoom -> Main.pfoom -> Main.pfoom
|
||||
Yaffle> Main.pfoom is possibly not terminating due to recursive path Main.pfoom -> Main.pfoom -> Main.pfoom
|
||||
Yaffle> Bye for now!
|
||||
|
@ -3,6 +3,6 @@ Written TTC
|
||||
Yaffle> Main.Bad is not strictly positive
|
||||
Yaffle> Main.MkBad is not strictly positive
|
||||
Yaffle> Main.MkBad' is not strictly positive
|
||||
Yaffle> Main.foo is not terminating due to call to Main.MkBad'
|
||||
Yaffle> Main.foo is possibly not terminating due to call to Main.MkBad'
|
||||
Yaffle> Main.T is not strictly positive
|
||||
Yaffle> Bye for now!
|
||||
|
Loading…
Reference in New Issue
Block a user