mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-23 20:22:34 +03:00
Update proof tutorial for Idris 2
This commit is contained in:
parent
1e567ab2d4
commit
1bb028ae47
@ -1,4 +1,5 @@
|
|||||||
In order to understand how to write proofs in Idris I think its worth clarifying some fundamentals, such as,
|
Before we discuss the details of theorem proving in Idris, we will describe
|
||||||
|
some fundamental concepts:
|
||||||
|
|
||||||
- Propositions and judgments
|
- Propositions and judgments
|
||||||
- Boolean and constructive logic
|
- Boolean and constructive logic
|
||||||
@ -9,8 +10,9 @@ In order to understand how to write proofs in Idris I think its worth clarifying
|
|||||||
Propositions and Judgments
|
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'.
|
Propositions are the subject of our proofs. Before the proof, we can't
|
||||||
For instance, if the ``proposition`` is,
|
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 |
|
| 1+1=2 |
|
||||||
@ -28,65 +30,67 @@ Or if the ``proposition`` is,
|
|||||||
| 1+1=3 |
|
| 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,
|
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 |
|
| 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.
|
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.
|
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, the "Law of Excluded Middle", so we
|
||||||
|
cannot 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.
|
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.
|
||||||
|
|
||||||
The logic we are using is called constructive (or sometimes intuitional) because we are constructing a 'database' of judgments.
|
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
|
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.
|
So how do we relate these proofs to Idris programs? It turns out that there is
|
||||||
|
a correspondence between constructive logic and type theory. They have the same
|
||||||
|
structure and we can switch back and forth between the two notations.
|
||||||
|
|
||||||
The way that this works is that a proposition is a type so this,
|
The way that this works is that a proposition is a type so...
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
Idris> 1+1=2
|
Main> 1 + 1 = 2
|
||||||
2 = 2 : Type
|
2 = 2
|
||||||
|
|
||||||
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:
|
Main> :t 1 + 1 = 2
|
||||||
|
(fromInteger 1 + fromInteger 1) === fromInteger 2 : Type
|
||||||
|
|
||||||
|
...is a proposition and it is also a type. The
|
||||||
|
following will also produce an equality type:
|
||||||
|
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
Idris> 1+1=3
|
Main> 1 + 1 = 3
|
||||||
2 = 3 : Type
|
2 = 3
|
||||||
|
|
||||||
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.
|
Both of these are valid propositions so both are valid equality types. But how
|
||||||
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
|
do we represent a 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
|
.. code-block:: idris
|
||||||
|
|
||||||
onePlusOne : 1+1=2
|
onePlusOne : 1+1=2
|
||||||
onePlusOne = Refl
|
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:
|
Now that we can represent propositions as types other aspects of
|
||||||
|
propositional logic can also be translated to types as follows:
|
||||||
.. 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 |
|
| | propositions | example of possible type |
|
||||||
@ -132,28 +136,39 @@ We can have a type which corresponds to disjunction:
|
|||||||
There is a built in type called 'Either'.
|
There is a built in type called 'Either'.
|
||||||
|
|
||||||
Definitional and Propositional Equalities
|
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 seen that we can 'prove' a type by finding a way to construct a term.
|
||||||
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:
|
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
|
.. code-block:: idris
|
||||||
|
|
||||||
onePlusOne : 1+1=2
|
onePlusOne : 1+1=2
|
||||||
onePlusOne = Refl
|
onePlusOne = Refl
|
||||||
|
|
||||||
So both sides of this equation nomalise to 2 and so Refl will type match and the proposition is proved.
|
Both sides of this equation nomalise to 2 and so Refl matches and the
|
||||||
|
proposition is proved.
|
||||||
|
|
||||||
We don't have to stick to terms, can also use symbolic parameters so the following will compile:
|
We don't have to stick to terms, we can also use symbolic parameters so the
|
||||||
|
following type checks:
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
varIdentity : m = m
|
varIdentity : m = m
|
||||||
varIdentity = Refl
|
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.
|
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.
|
Especially when working with equalities containing variable terms (inside
|
||||||
|
functions) it can be hard to know which equality types are definitionally equal,
|
||||||
|
in this example ``plusReducesL`` is *definitionally equal* but ``plusReducesR`` is
|
||||||
|
not (although it is *propositionaly equal*). The only difference between
|
||||||
|
them is the order of the operands.
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
@ -163,69 +178,33 @@ Especially when working with equalities containing variable terms (inside functi
|
|||||||
plusReducesR : (n:Nat) -> plus n Z = n
|
plusReducesR : (n:Nat) -> plus n Z = n
|
||||||
plusReducesR n = Refl
|
plusReducesR n = Refl
|
||||||
|
|
||||||
plusReducesR gives the following error:
|
Checking ``plusReducesR`` gives the following error:
|
||||||
|
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
- + Errors (1)
|
Proofs.idr:21:18--23:1:While processing right hand side of Main.plusReducesR at Proofs.idr:21:1--23:1:
|
||||||
`-- proof.idr line 6 col 17:
|
Can't solve constraint between:
|
||||||
When checking right hand side of plusReducesR with expected type
|
plus n Z
|
||||||
plus n 0 = n
|
and
|
||||||
|
n
|
||||||
|
|
||||||
Type mismatch between
|
So why is ``Refl`` able to prove some equality types but not others?
|
||||||
n = n (Type of Refl)
|
|
||||||
and
|
|
||||||
plus n 0 = n (Expected type)
|
|
||||||
|
|
||||||
Specifically:
|
The first answer is that ``plus`` is defined by recursion on its first
|
||||||
Type mismatch between
|
argument. So, when the first argument is ``Z``, it reduces, but not when the
|
||||||
n
|
second argument is ``Z``.
|
||||||
and
|
|
||||||
plus n 0
|
|
||||||
|
|
||||||
So why is 'Refl' able to prove some equality types but not others?
|
If an equality type can be proved/constructed by using ``Refl`` alone it is known
|
||||||
|
as a *definitional equality*. In order to be definitionally equal both sides
|
||||||
|
of the equation must normalise to the same value.
|
||||||
|
|
||||||
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?
|
So when we type ``1+1`` in Idris it is immediately reduced to 2 because
|
||||||
|
definitional equality is built in
|
||||||
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
|
.. code-block:: idris
|
||||||
|
|
||||||
Idris> 1+1
|
Main> 1+1
|
||||||
2 : Integer
|
2
|
||||||
|
|
||||||
In the following pages we discuss how to resolve propositionaly equalies.
|
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.
|
|
||||||
|
|
||||||
|
|
||||||
|
@ -4,9 +4,7 @@
|
|||||||
Theorem Proving
|
Theorem Proving
|
||||||
###############
|
###############
|
||||||
|
|
||||||
A tutorial on theorem proving in Idris.
|
A tutorial on theorem proving in Idris 2.
|
||||||
|
|
||||||
NOT YET UPDATED FOR IDRIS 2!
|
|
||||||
|
|
||||||
.. note::
|
.. note::
|
||||||
|
|
||||||
@ -25,6 +23,3 @@ NOT YET UPDATED FOR IDRIS 2!
|
|||||||
inductive
|
inductive
|
||||||
patterns
|
patterns
|
||||||
propositional
|
propositional
|
||||||
interactive
|
|
||||||
interactiveOld
|
|
||||||
|
|
||||||
|
@ -52,13 +52,14 @@ function capturing all such inductive definitions:
|
|||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
nat_induction : (P : Nat -> Type) -> -- Property to show
|
nat_induction :
|
||||||
(P Z) -> -- Base case
|
(prop : Nat -> Type) -> -- Property to show
|
||||||
((k : Nat) -> P k -> P (S k)) -> -- Inductive step
|
(prop Z) -> -- Base case
|
||||||
(x : Nat) -> -- Show for all x
|
((k : Nat) -> prop k -> prop (S k)) -> -- Inductive step
|
||||||
P x
|
(x : Nat) -> -- Show for all x
|
||||||
nat_induction P p_Z p_S Z = p_Z
|
prop x
|
||||||
nat_induction P p_Z p_S (S k) = p_S k (nat_induction P p_Z p_S k)
|
nat_induction prop p_Z p_S Z = p_Z
|
||||||
|
nat_induction prop p_Z p_S (S k) = p_S k (nat_induction prop p_Z p_S k)
|
||||||
|
|
||||||
Using ``nat_induction``, we can implement an equivalent inductive
|
Using ``nat_induction``, we can implement an equivalent inductive
|
||||||
version of ``plus``:
|
version of ``plus``:
|
||||||
@ -78,16 +79,16 @@ To prove that ``plus n m = plus m n`` for all natural numbers ``n`` and
|
|||||||
induction on ``n``, or vice versa. We can sketch an outline of a proof;
|
induction on ``n``, or vice versa. We can sketch an outline of a proof;
|
||||||
performing induction on ``n``, we have:
|
performing induction on ``n``, we have:
|
||||||
|
|
||||||
- Property ``P`` is ``\x => plus x m = plus m x``.
|
- Property ``prop`` is ``\x => plus x m = plus m x``.
|
||||||
|
|
||||||
- Show that ``P`` holds in the base case and inductive step:
|
- Show that ``prop`` holds in the base case and inductive step:
|
||||||
|
|
||||||
- | Base case: ``P Z``, i.e.
|
- | Base case: ``prop Z``, i.e.
|
||||||
| ``plus Z m = plus m Z``, which reduces to
|
| ``plus Z m = plus m Z``, which reduces to
|
||||||
| ``m = plus m Z`` due to the definition of ``plus``.
|
| ``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.
|
- | Inductive step: Inductively, we know that ``prop 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 k m = plus m k`` (the induction hypothesis). Given this, show ``prop (S k)``, i.e.
|
||||||
| ``plus (S k) m = plus m (S k)``, which reduces to
|
| ``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 k m) = plus m (S k)``. From the induction hypothesis, we can rewrite this to
|
||||||
| ``S (plus m k) = plus m (S k)``.
|
| ``S (plus m k) = plus m (S k)``.
|
||||||
|
@ -1,296 +0,0 @@
|
|||||||
***************************
|
|
||||||
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
|
|
@ -1,169 +0,0 @@
|
|||||||
**************************************************************
|
|
||||||
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.
|
|
@ -16,9 +16,9 @@ mapping to Emacs commands.
|
|||||||
+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
|
+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
|
||||||
| Check type | ``\t`` | ``C-c C-t`` | Show type of identifier or hole under the cursor. |
|
| 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. |
|
| Proof search | ``\s`` | ``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 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. |
|
| Make lemma | ``\l`` | ``C-c C-e`` | Add a top level function with a type which solves the hole under the cursor. |
|
||||||
+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
|
+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
|
||||||
@ -36,7 +36,7 @@ declaration:
|
|||||||
|
|
||||||
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
|
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
|
||||||
|
|
||||||
To create a template definition for the proof, press ``\d`` (or the
|
To create a template definition for the proof, press ``\a`` (or the
|
||||||
equivalent in your editor of choice) on the line with the type
|
equivalent in your editor of choice) on the line with the type
|
||||||
declaration. You should see:
|
declaration. You should see:
|
||||||
|
|
||||||
@ -64,20 +64,18 @@ in each respective case. Pressing ``\t`` over
|
|||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
m : Nat
|
m : Nat
|
||||||
--------------------------------------
|
-------------------------------------
|
||||||
plus_commutes_rhs_1 : m = plus m 0
|
plus_commutes_rhs_1 : m = plus m Z
|
||||||
|
|
||||||
Note that ``Z`` renders as ``0`` because the pretty printer renders
|
Similarly, for ``plus_commutes_rhs_2``:
|
||||||
natural numbers as integer literals for readability. Similarly, for
|
|
||||||
``plus_commutes_rhs_2``:
|
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
k : Nat
|
k : Nat
|
||||||
m : Nat
|
m : Nat
|
||||||
--------------------------------------
|
--------------------------------------
|
||||||
plus_commutes_rhs_2 : S (plus k m) = plus m (S k)
|
plus_commutes_rhs_2 : (S (plus k m)) = (plus m (S k))
|
||||||
|
|
||||||
It is a good idea to give these slightly more meaningful names:
|
It is a good idea to give these slightly more meaningful names:
|
||||||
|
|
||||||
@ -96,107 +94,100 @@ yields:
|
|||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
plus_commutes_Z : m = plus m 0
|
plus_commutes_Z : (m : Nat) -> m = plus m Z
|
||||||
|
|
||||||
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
|
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
|
||||||
plus_commutes Z m = plus_commutes_Z
|
plus_commutes Z m = plus_commutes_Z m
|
||||||
plus_commutes (S k) m = ?plus_commutes_S
|
plus_commutes (S k) m = ?plus_commutes_S
|
||||||
|
|
||||||
That is, the hole has been filled with a call to a top level
|
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
|
function ``plus_commutes_Z``, applied to the variable in scope ``m``.
|
||||||
because it can be inferred from context when it is applied.
|
|
||||||
|
|
||||||
Unfortunately, we cannot prove this lemma directly, since ``plus`` is
|
Unfortunately, we cannot prove this lemma directly, since ``plus`` is
|
||||||
defined by matching on its *first* argument, and here ``plus m 0`` has a
|
defined by matching on its *first* argument, and here ``plus m Z`` has a
|
||||||
specific value for its *second argument* (in fact, the left hand side of
|
concrete 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
|
the equality has been reduced from ``plus Z m``.) Again, we can prove
|
||||||
this by induction, this time on ``m``.
|
this by induction, this time on ``m``.
|
||||||
|
|
||||||
First, create a template definition with ``\d``:
|
First, create a template definition with ``\d``:
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
plus_commutes_Z : m = plus m 0
|
plus_commutes_Z : (m : Nat) -> m = plus m Z
|
||||||
plus_commutes_Z = ?plus_commutes_Z_rhs
|
plus_commutes_Z m = ?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``:
|
Now, case split on ``m`` with ``\c``:
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
plus_commutes_Z : m = plus m 0
|
plus_commutes_Z : (m : Nat) -> m = plus m Z
|
||||||
plus_commutes_Z {m = Z} = ?plus_commutes_Z_rhs_1
|
plus_commutes_Z Z = ?plus_commutes_Z_rhs_1
|
||||||
plus_commutes_Z {m = (S k)} = ?plus_commutes_Z_rhs_2
|
plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2
|
||||||
|
|
||||||
Checking the type of ``plus_commutes_Z_rhs_1`` shows the following,
|
Checking the type of ``plus_commutes_Z_rhs_1`` shows the following,
|
||||||
which is easily proved by reflection:
|
which is provable by ``Refl``:
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
--------------------------------------
|
--------------------------------------
|
||||||
plus_commutes_Z_rhs_1 : 0 = 0
|
plus_commutes_Z_rhs_1 : Z = Z
|
||||||
|
|
||||||
For such trivial proofs, we can let write the proof automatically by
|
For such immediate proofs, we can let write the proof automatically by
|
||||||
pressing ``\o`` with the cursor over ``plus_commutes_Z_rhs_1``.
|
pressing ``\s`` with the cursor over ``plus_commutes_Z_rhs_1``.
|
||||||
This yields:
|
This yields:
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
plus_commutes_Z : m = plus m 0
|
plus_commutes_Z : (m : Nat) -> m = plus m Z
|
||||||
plus_commutes_Z {m = Z} = Refl
|
plus_commutes_Z Z = Refl
|
||||||
plus_commutes_Z {m = (S k)} = ?plus_commutes_Z_rhs_2
|
plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2
|
||||||
|
|
||||||
For ``plus_commutes_Z_rhs_2``, we are not so lucky:
|
For ``plus_commutes_Z_rhs_2``, we are not so lucky:
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
k : Nat
|
k : Nat
|
||||||
--------------------------------------
|
-------------------------------------
|
||||||
plus_commutes_Z_rhs_2 : S k = S (plus k 0)
|
plus_commutes_Z_rhs_2 : S k = S (plus k Z)
|
||||||
|
|
||||||
Inductively, we should know that ``k = plus k 0``, and we can get access
|
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
|
to this inductive hypothesis by making a recursive call on k, as
|
||||||
follows:
|
follows:
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
plus_commutes_Z : m = plus m 0
|
plus_commutes_Z : (m : Nat) -> m = plus m Z
|
||||||
plus_commutes_Z {m = Z} = Refl
|
plus_commutes_Z Z = Refl
|
||||||
plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in
|
plus_commutes_Z (S k)
|
||||||
?plus_commutes_Z_rhs_2
|
= let rec = plus_commutes_Z k in
|
||||||
|
?plus_commutes_Z_rhs_2
|
||||||
|
|
||||||
For ``plus_commutes_Z_rhs_2``, we now see:
|
For ``plus_commutes_Z_rhs_2``, we now see:
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
k : Nat
|
k : Nat
|
||||||
rec : k = plus k (fromInteger 0)
|
rec : k = plus k Z
|
||||||
--------------------------------------
|
-------------------------------------
|
||||||
plus_commutes_Z_rhs_2 : S k = S (plus k 0)
|
plus_commutes_Z_rhs_2 : S k = S (plus k Z)
|
||||||
|
|
||||||
Again, the ``fromInteger 0`` is merely due to ``Nat`` having an implementation
|
So we know that ``k = plus k Z``, but how do we use this to update the goal to
|
||||||
of the ``Num`` interface. So we know that ``k = plus k 0``, but how do
|
``S k = S k``?
|
||||||
we use this to update the goal to ``S k = S k``?
|
|
||||||
|
|
||||||
To achieve this, Idris provides a ``replace`` function as part of the
|
To achieve this, Idris provides a ``replace`` function as part of the
|
||||||
prelude:
|
prelude:
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
*pluscomm> :t replace
|
Main> :t replace
|
||||||
replace : (x = y) -> P x -> P y
|
Builtin.replace : (0 rule : x = y) -> p x -> p y
|
||||||
|
|
||||||
Given a proof that ``x = y``, and a property ``P`` which holds for
|
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
|
``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
|
know ``x`` and ``y`` must be the same. Note the multiplicity on ``rule``
|
||||||
a little tricky to use because in general the implicit argument ``P``
|
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
|
can be hard to infer by unification, so Idris provides a high level
|
||||||
syntax which calculates the property and applies ``replace``:
|
syntax which calculates the property and applies ``replace``:
|
||||||
|
|
||||||
@ -205,63 +196,48 @@ syntax which calculates the property and applies ``replace``:
|
|||||||
rewrite prf in expr
|
rewrite prf in expr
|
||||||
|
|
||||||
If we have ``prf : x = y``, and the required type for ``expr`` is some
|
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``
|
property of ``x``, the ``rewrite ... in`` syntax will search for all
|
||||||
in the required type of ``expr`` and replace it with ``y``. Concretely,
|
occurrences of ``x``
|
||||||
in our example, we can say:
|
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
|
.. code-block:: idris
|
||||||
|
|
||||||
plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in
|
Main> :t sym
|
||||||
rewrite rec in ?plus_commutes_Z_rhs_2
|
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:
|
Checking the type of ``plus_commutes_Z_rhs_2`` now gives:
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
k : Nat
|
k : Nat
|
||||||
rec : k = plus k (fromInteger 0)
|
rec : k = plus k Z
|
||||||
_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
|
plus_commutes_Z_rhs_2 : S k = S k
|
||||||
|
|
||||||
Either way, we can use proof search (``\o``) to complete the
|
Using the rewrite rule ``rec``, the goal type has been updated with ``plus k Z``
|
||||||
proof, giving:
|
replaced by ``k``.
|
||||||
|
|
||||||
|
We can use proof search (``\s``) to complete the proof, giving:
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
plus_commutes_Z : m = plus m 0
|
plus_commutes_Z : (m : Nat) -> m = plus m Z
|
||||||
plus_commutes_Z {m = Z} = Refl
|
plus_commutes_Z Z = Refl
|
||||||
plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in
|
plus_commutes_Z (S k)
|
||||||
rewrite rec in Refl
|
= let rec = plus_commutes_Z k in
|
||||||
|
rewrite sym rec in Refl
|
||||||
|
|
||||||
The base case is now complete.
|
The base case of ``plus_commutes`` is now complete.
|
||||||
|
|
||||||
Inductive Step
|
Inductive Step
|
||||||
==============
|
==============
|
||||||
@ -272,16 +248,16 @@ state:
|
|||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
|
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
|
||||||
plus_commutes Z m = plus_commutes_Z
|
plus_commutes Z m = plus_commutes_Z m
|
||||||
plus_commutes (S k) m = ?plus_commutes_S
|
plus_commutes (S k) m = ?plus_commutes_S
|
||||||
|
|
||||||
Looking again at the type of ``plus_commutes_S``, we have:
|
Looking again at the type of ``plus_commutes_S``, we have:
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
k : Nat
|
k : Nat
|
||||||
m : Nat
|
m : Nat
|
||||||
--------------------------------------
|
-------------------------------------
|
||||||
plus_commutes_S : S (plus k m) = plus m (S k)
|
plus_commutes_S : S (plus k m) = plus m (S k)
|
||||||
|
|
||||||
Conveniently, by induction we can immediately tell that
|
Conveniently, by induction we can immediately tell that
|
||||||
@ -299,10 +275,9 @@ Checking the type of ``plus_commutes_S`` now gives:
|
|||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
k : Nat
|
k : Nat
|
||||||
m : Nat
|
m : Nat
|
||||||
_rewrite_rule : plus m k = plus k m
|
-------------------------------------
|
||||||
--------------------------------------
|
|
||||||
plus_commutes_S : S (plus m k) = plus m (S k)
|
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.
|
The good news is that ``m`` and ``k`` now appear in the correct order.
|
||||||
@ -315,17 +290,16 @@ begin by making a new top level lemma with ``\l``. This gives:
|
|||||||
|
|
||||||
plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
|
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
|
Again, we make a template definition with ``\a``:
|
||||||
we cannot in general infer arguments to a function from its result.
|
|
||||||
Again, we make a template definition with ``\d``:
|
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
|
plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
|
||||||
plus_commutes_S k m = ?plus_commutes_S_rhs
|
plus_commutes_S k m = ?plus_commutes_S_rhs
|
||||||
|
|
||||||
Again, this is defined by induction over ``m``, since ``plus`` is
|
Like ``plus_commutes_Z``, we can define this by induction over ``m``, since
|
||||||
defined by matching on its first argument. The complete definition is:
|
``plus`` is defined by matching on its first argument. The complete definition
|
||||||
|
is:
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
@ -344,8 +318,3 @@ which it happens to be well-defined.
|
|||||||
|
|
||||||
Now that ``plus_commutes`` has a ``total`` annotation, we have completed the
|
Now that ``plus_commutes`` has a ``total`` annotation, we have completed the
|
||||||
proof of commutativity of addition on natural numbers.
|
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``.
|
|
||||||
|
@ -20,11 +20,11 @@ the prompt, the read-eval-print loop):
|
|||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
Idris> \m => plus Z m
|
Main> \m => plus Z m
|
||||||
\m => m : Nat -> Nat
|
\m => m
|
||||||
|
|
||||||
Idris> \k,m => plus (S k) m
|
Idris> \k,m => plus (S k) m
|
||||||
\k => \m => S (plus k m) : Nat -> Nat -> Nat
|
\k => \m => S (plus k m)
|
||||||
|
|
||||||
Note that unlike many other language REPLs, the Idris REPL performs
|
Note that unlike many other language REPLs, the Idris REPL performs
|
||||||
evaluation on *open* terms, meaning that it can reduce terms which
|
evaluation on *open* terms, meaning that it can reduce terms which
|
||||||
@ -47,17 +47,14 @@ we must *prove* them.
|
|||||||
Equality Proofs
|
Equality Proofs
|
||||||
===============
|
===============
|
||||||
|
|
||||||
Idris has a built-in propositional equality type, conceptually defined
|
Idris defines a propositional equality type as follows:
|
||||||
as follows:
|
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
data (=) : a -> b -> Type where
|
data Equal : a -> b -> Type where
|
||||||
Refl : x = x
|
Refl : Equal x x
|
||||||
|
|
||||||
Note that this must be built-in, rather than defined in the library,
|
As syntactic sugar, ``Equal x y`` can be written as ``x = y``.
|
||||||
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
|
It is *propositional* equality, where the type states that any two
|
||||||
values in different types ``a`` and ``b`` may be proposed to be equal.
|
values in different types ``a`` and ``b`` may be proposed to be equal.
|
||||||
@ -87,11 +84,11 @@ error:
|
|||||||
|
|
||||||
::
|
::
|
||||||
|
|
||||||
When elaborating right hand side of four_eq_five:
|
When unifying 4 = 4 and (fromInteger 4) = (fromInteger 5)
|
||||||
Type mismatch between
|
Mismatch between:
|
||||||
x = x (Type of Refl)
|
4
|
||||||
and
|
and
|
||||||
4 = 5 (Expected type)
|
5
|
||||||
|
|
||||||
Type checking equality proofs
|
Type checking equality proofs
|
||||||
-----------------------------
|
-----------------------------
|
||||||
@ -131,13 +128,12 @@ equalities between values in different types:
|
|||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
idris_not_php : 2 = "2"
|
idris_not_php : Z = "Z"
|
||||||
|
|
||||||
Obviously, in Idris the type ``2 = "2"`` is uninhabited, and one might
|
The type ``Z = "Z"`` is uninhabited, and one might wonder why it is useful to
|
||||||
wonder why it is useful to be able to propose equalities between values
|
be able to propose equalities between values in different types. However, with
|
||||||
in different types. However, with dependent types, such equalities can
|
dependent types, such equalities can arise naturally. For example, if two
|
||||||
arise naturally. For example, if two vectors are equal, their lengths
|
vectors are equal, their lengths must be equal:
|
||||||
must be equal:
|
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
|
@ -1,59 +1,68 @@
|
|||||||
This page attempts to explain some of the techniques used in Idris to prove propositional equalities.
|
This page attempts to explain some of the techniques used in Idris to prove
|
||||||
|
propositional equalities.
|
||||||
|
|
||||||
Proving Propositional Equality
|
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.
|
We have seen that definitional equalities can be proved using ``Refl`` since they
|
||||||
|
always normalise to values that can be compared directly.
|
||||||
|
|
||||||
However with propositional equalities we are using symbolic variables they do not always normalse.
|
However with propositional equalities we are using symbolic variables, which do
|
||||||
|
not always normalse.
|
||||||
|
|
||||||
So to take the previous example:
|
So to take the previous example:
|
||||||
|
|
||||||
plusReducesR : (n:Nat) -> plus n Z = n
|
.. code-block:: idris
|
||||||
|
|
||||||
In this case 'plus n Z' does not normalise to n. Even though both sides are equal we cannot pattern match Refl.
|
plusReducesR : (n : Nat) -> plus n Z = n
|
||||||
|
|
||||||
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.
|
In this case ``plus n Z`` does not normalise to n. Even though both sides of
|
||||||
|
the equality are provably equal we cannot claim ``Refl`` as a proof.
|
||||||
|
|
||||||
So here:
|
If the pattern match cannot match for all ``n`` then we need to
|
||||||
|
match all possible values of ``n``. In this case
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
plusReducesR : n = plus n 0
|
plusReducesR : (n : Nat) -> plus n Z = n
|
||||||
plusReducesR {n = Z} = Refl
|
plusReducesR Z = Refl
|
||||||
plusReducesR {n = (S k)} = let rec = plus_commutes_Z {n=k} in
|
plusReducesR (S k)
|
||||||
rewrite rec in Refl
|
= let rec = plusReducesR k in
|
||||||
|
rewrite sym 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.
|
we can't use ``Refl`` to prove ``n = plus n 0`` for all ``n``. Instead, we call
|
||||||
|
it for each case separately. So, in the second line for example, the type checker
|
||||||
|
substitutes ``Z`` for ``n`` in the type being matched, and reduces the type
|
||||||
|
accordingly.
|
||||||
|
|
||||||
Replace
|
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:
|
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
|
if x=y
|
||||||
then P x = P y
|
then prop x = prop 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
|
where prop is a pure function representing the property. In the examples below
|
||||||
|
prop is an expression in some variable with a type like this: ``prop: n -> Type``
|
||||||
|
|
||||||
So if n is a natural number variable then P could be something like 2*n + 3.
|
So if ``n`` is a natural number variable then ``prop`` could be something
|
||||||
|
like ``\n => 2*n + 3``.
|
||||||
|
|
||||||
To use this in our proofs there is the following function in the prelude:
|
To use this in our proofs there is the following function in the prelude:
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
||| Perform substitution in a term according to some equality.
|
||| Perform substitution in a term according to some equality.
|
||||||
replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
|
replace : forall x, y, prop . (0 rule : x = y) -> prop x -> prop y
|
||||||
replace Refl prf = prf
|
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)
|
If we supply an equality (x=y) and a proof of a property of x (``prop x``) then we get
|
||||||
|
a proof of a property of y (``prop y``).
|
||||||
.. code-block:: idris
|
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``.
|
||||||
> :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
|
.. code-block:: idris
|
||||||
|
|
||||||
@ -66,16 +75,13 @@ So, in the following example, if we supply p1 x which is a proof that x=2 and th
|
|||||||
Rewrite
|
Rewrite
|
||||||
=======
|
=======
|
||||||
|
|
||||||
Similar to 'replace' above but Idris provides a nicer syntax which makes 'rewrite' easier to use in examples like plusReducesR above.
|
In practice, ``replace`` can be
|
||||||
|
a little tricky to use because in general the implicit argument ``prop``
|
||||||
|
can be hard to infer for the machine, so Idris provides a high level
|
||||||
|
syntax which calculates the property and applies ``replace``.
|
||||||
|
|
||||||
.. code-block:: idris
|
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``.
|
||||||
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
|
.. code-block:: idris
|
||||||
|
|
||||||
@ -85,27 +91,28 @@ Example: again we supply p1 which is a proof that x=2 and the equality x=y then
|
|||||||
testRewrite2: (x=y) -> (p1 y) -> (p1 x)
|
testRewrite2: (x=y) -> (p1 y) -> (p1 x)
|
||||||
testRewrite2 a b = rewrite a in b
|
testRewrite2 a b = rewrite a in b
|
||||||
|
|
||||||
We can think of rewrite doing this:
|
We can think of ``rewrite`` as working in this way:
|
||||||
|
|
||||||
* Start with a equation x=y and a property P: x -> Type
|
* Start with a equation ``x=y`` and a property ``prop : x -> Type``
|
||||||
* Searches y in P
|
* Search for ``x`` in ``prop``
|
||||||
* Replaces all occurrences of y with x in P.
|
* Replaces all occurrences of ``x`` with ``y`` in ``prop``.
|
||||||
|
|
||||||
That is, we are doing a substitution.
|
That is, we are doing a substitution.
|
||||||
|
|
||||||
Symmetry and Transitivity
|
Symmetry and Transitivity
|
||||||
=========================
|
=========================
|
||||||
|
|
||||||
In addition to 'reflexivity' equality also obeys 'symmetry' and 'transitivity' and these are also included in the prelude:
|
In addition to 'reflexivity' equality also obeys 'symmetry' and 'transitivity'
|
||||||
|
and these are also included in the prelude:
|
||||||
|
|
||||||
.. code-block:: idris
|
.. code-block:: idris
|
||||||
|
|
||||||
||| Symmetry of propositional equality
|
||| Symmetry of propositional equality
|
||||||
sym : {left:a} -> {right:b} -> left = right -> right = left
|
sym : forall x, y . (0 rule : x = y) -> y = x
|
||||||
sym Refl = Refl
|
sym Refl = Refl
|
||||||
|
|
||||||
||| Transitivity of propositional equality
|
||| Transitivity of propositional equality
|
||||||
trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c
|
trans : forall a, b, c . (0 l : a = b) -> (0 r : b = c) -> a = c
|
||||||
trans Refl Refl = Refl
|
trans Refl Refl = Refl
|
||||||
|
|
||||||
Heterogeneous Equality
|
Heterogeneous Equality
|
||||||
|
@ -17,6 +17,9 @@ disjoint n prf = replace {p = disjointTy} prf ()
|
|||||||
plusReduces : (n:Nat) -> plus Z n = n
|
plusReduces : (n:Nat) -> plus Z n = n
|
||||||
plusReduces n = Refl
|
plusReduces n = Refl
|
||||||
|
|
||||||
|
plusReducesR : (n:Nat) -> plus n Z = n
|
||||||
|
plusReducesR n = Refl
|
||||||
|
|
||||||
plusReducesZ : (n:Nat) -> n = plus n Z
|
plusReducesZ : (n:Nat) -> n = plus n Z
|
||||||
plusReducesZ Z = Refl
|
plusReducesZ Z = Refl
|
||||||
plusReducesZ (S k) = cong S (plusReducesZ k)
|
plusReducesZ (S k) = cong S (plusReducesZ k)
|
||||||
|
@ -312,7 +312,7 @@ addMadeLemma n ty app line content
|
|||||||
where
|
where
|
||||||
-- Put n : ty in the first blank line
|
-- Put n : ty in the first blank line
|
||||||
insertInBlank : List String -> List String
|
insertInBlank : List String -> List String
|
||||||
insertInBlank [] = [show n ++ " : " ++ ty ++ "\n\n"]
|
insertInBlank [] = [show n ++ " : " ++ ty ++ "\n"]
|
||||||
insertInBlank (x :: xs)
|
insertInBlank (x :: xs)
|
||||||
= if trim x == ""
|
= if trim x == ""
|
||||||
then ("\n" ++ show n ++ " : " ++ ty ++ "\n") :: xs
|
then ("\n" ++ show n ++ " : " ++ ty ++ "\n") :: xs
|
||||||
|
@ -102,7 +102,11 @@ sugarApp tm@(PApp fc (PApp _ (PRef _ (UN "DPair")) l) rb)
|
|||||||
sugarApp (PApp fc (PApp _ (PRef _ (UN "MkDPair")) l) r)
|
sugarApp (PApp fc (PApp _ (PRef _ (UN "MkDPair")) l) r)
|
||||||
= PDPair fc (unbracket l) (PImplicit fc) (unbracket r)
|
= PDPair fc (unbracket l) (PImplicit fc) (unbracket r)
|
||||||
sugarApp (PApp fc (PApp _ (PRef _ (UN "Equal")) l) r)
|
sugarApp (PApp fc (PApp _ (PRef _ (UN "Equal")) l) r)
|
||||||
= PEq fc l r
|
= PEq fc (unbracket l) (unbracket r)
|
||||||
|
sugarApp (PApp fc (PApp _ (PRef _ (UN "===")) l) r)
|
||||||
|
= PEq fc (unbracket l) (unbracket r)
|
||||||
|
sugarApp (PApp fc (PApp _ (PRef _ (UN "~=~")) l) r)
|
||||||
|
= PEq fc (unbracket l) (unbracket r)
|
||||||
sugarApp (PRef fc (UN "Nil")) = PList fc []
|
sugarApp (PRef fc (UN "Nil")) = PList fc []
|
||||||
sugarApp (PRef fc (UN "Unit")) = PUnit fc
|
sugarApp (PRef fc (UN "Unit")) = PUnit fc
|
||||||
sugarApp (PRef fc (UN "MkUnit")) = PUnit fc
|
sugarApp (PRef fc (UN "MkUnit")) = PUnit fc
|
||||||
|
@ -41,8 +41,8 @@ getArgs : {auto c : Ref Ctxt Defs} ->
|
|||||||
Env Term vars -> Nat -> Term vars ->
|
Env Term vars -> Nat -> Term vars ->
|
||||||
Core (List (Name, Maybe Name, PiInfo RawImp, RigCount, RawImp), RawImp)
|
Core (List (Name, Maybe Name, PiInfo RawImp, RigCount, RawImp), RawImp)
|
||||||
getArgs {vars} env (S k) (Bind _ x (Pi c p ty) sc)
|
getArgs {vars} env (S k) (Bind _ x (Pi c p ty) sc)
|
||||||
= do ty' <- unelab env ty
|
= do defs <- get Ctxt
|
||||||
defs <- get Ctxt
|
ty' <- unelab env !(normalise defs env ty)
|
||||||
let x' = UN !(uniqueName defs (map nameRoot vars) (nameRoot x))
|
let x' = UN !(uniqueName defs (map nameRoot vars) (nameRoot x))
|
||||||
(sc', ty) <- getArgs (Pi c p ty :: env) k (renameTop x' sc)
|
(sc', ty) <- getArgs (Pi c p ty :: env) k (renameTop x' sc)
|
||||||
-- Don't need to use the name if it's not used in the scope type
|
-- Don't need to use the name if it's not used in the scope type
|
||||||
@ -56,7 +56,8 @@ getArgs {vars} env (S k) (Bind _ x (Pi c p ty) sc)
|
|||||||
else Implicit
|
else Implicit
|
||||||
pure ((x, mn, p', c, ty') :: sc', ty)
|
pure ((x, mn, p', c, ty') :: sc', ty)
|
||||||
getArgs env k ty
|
getArgs env k ty
|
||||||
= do ty' <- unelab env ty
|
= do defs <- get Ctxt
|
||||||
|
ty' <- unelab env !(normalise defs env ty)
|
||||||
pure ([], ty')
|
pure ([], ty')
|
||||||
|
|
||||||
mkType : FC -> List (Name, Maybe Name, PiInfo RawImp, RigCount, RawImp) ->
|
mkType : FC -> List (Name, Maybe Name, PiInfo RawImp, RigCount, RawImp) ->
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
1/1: Building Rewrite (Rewrite.idr)
|
1/1: Building Rewrite (Rewrite.idr)
|
||||||
Rewrite.idr:15:25--17:1:While processing right hand side of Main.wrongCommutes at Rewrite.idr:15:1--17:1:
|
Rewrite.idr:15:25--17:1:While processing right hand side of Main.wrongCommutes at Rewrite.idr:15:1--17:1:
|
||||||
Rewriting by (m + k) = (k + m) did not change type (S k + m) = (m + S k)
|
Rewriting by m + k = k + m did not change type S k + m = m + S k
|
||||||
Rewrite.idr:19:26--20:1:While processing right hand side of Main.wrongCommutes2 at Rewrite.idr:19:1--20:1:
|
Rewrite.idr:19:26--20:1:While processing right hand side of Main.wrongCommutes2 at Rewrite.idr:19:1--20:1:
|
||||||
Nat is not a rewrite rule type
|
Nat is not a rewrite rule type
|
||||||
|
@ -1,19 +1,19 @@
|
|||||||
1/1: Building Eta (Eta.idr)
|
1/1: Building Eta (Eta.idr)
|
||||||
Eta.idr:14:10--15:1:While processing right hand side of Main.etaBad at Eta.idr:14:1--15:1:
|
Eta.idr:14:10--15:1:While processing right hand side of Main.etaBad at Eta.idr:14:1--15:1:
|
||||||
When unifying ?x = ?x and MkTest = (\x => (\y => (MkTest ?_ ?_)))
|
When unifying ?x = ?x and MkTest = \x => (\y => (MkTest ?_ ?_))
|
||||||
Mismatch between:
|
Mismatch between:
|
||||||
Integer
|
Integer
|
||||||
and
|
and
|
||||||
Nat
|
Nat
|
||||||
1/1: Building Eta2 (Eta2.idr)
|
1/1: Building Eta2 (Eta2.idr)
|
||||||
Eta2.idr:2:8--4:1:While processing right hand side of Main.test at Eta2.idr:2:1--4:1:
|
Eta2.idr:2:8--4:1:While processing right hand side of Main.test at Eta2.idr:2:1--4:1:
|
||||||
When unifying ?x = ?x and S = (\x => (S ?_))
|
When unifying ?x = ?x and S = \x => (S ?_)
|
||||||
Mismatch between:
|
Mismatch between:
|
||||||
Nat
|
Nat
|
||||||
and
|
and
|
||||||
a
|
a
|
||||||
Eta2.idr:5:44--6:1:While processing right hand side of Main.test2 at Eta2.idr:5:1--6:1:
|
Eta2.idr:5:44--6:1:While processing right hand side of Main.test2 at Eta2.idr:5:1--6:1:
|
||||||
When unifying ?x = ?x and S = (\x => (S ?_))
|
When unifying ?x = ?x and S = \x => (S ?_)
|
||||||
Mismatch between:
|
Mismatch between:
|
||||||
Nat
|
Nat
|
||||||
and
|
and
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
1/1: Building WithLift (WithLift.idr)
|
1/1: Building WithLift (WithLift.idr)
|
||||||
Main> succNotZero : (S k) = Z -> Void
|
Main> succNotZero : S k = Z -> Void
|
||||||
succNotZero
|
succNotZero
|
||||||
Main> recNotEqLift : (k = j -> Void) -> (S k) = (S j) -> Void
|
Main> recNotEqLift : (k = j -> Void) -> S k = S j -> Void
|
||||||
(recNotEqLift contra)
|
(recNotEqLift contra)
|
||||||
Main> recNotEq f Refl = f Refl
|
Main> recNotEq f Refl = f Refl
|
||||||
Main> Bye for now!
|
Main> Bye for now!
|
||||||
|
Loading…
Reference in New Issue
Block a user