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
If you have experience in logic or using proof assistants like Coq then you may already know this stuff so you can skip this page.
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,
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:
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 on constructor 'Refl' so a proof of 1+1=2 is
onePlusOne : 1+1=2 onePlusOne = Refl |
So how can Refl, which is a constructor without any parameters, construct and equality type? If we type it on its own then it can't:
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:
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:
data And : Type -> Type -> Type where 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:
data Or : Type -> Type -> Type where OrIntroLeft : a -> A a b OrIntroRight : b -> A a b |
There is a built in type called 'Either'.
Equations in Idris
So, in addition to the equals symbol, an equation can contain:
- Numbers
- Identifiers (names starting with lower case)
- Functions
We can make a proposition dependent on a given type like this:
p1: Nat -> Type p1 n = (n=2) |
Approaches to solving
Equations without variables such as:
| 1+1=2 |
Are usually normalisable and can be solved by Refl.
oneandone : plus 1 1 = 2 oneandone = Refl |
If we have variables then it is still possible that both sides of the equation will normalise to the same value and we can just use Refl. Otherwise we need to show that it is true for all values. In this example, from libs/contrib Data.Bool.Extra, it is easy to list all possibilities
notInvolutive : (x : Bool) -> not (not x) = x notInvolutive True = Refl notInvolutive False = Refl |
This situation is different from the more usual situation where we have a given type and many constructors for that type. For example, we may have a Bool type with the constructors True and False or the nat type with the number literals as constructors. By contrast here we have many types each with a single constructor which is Refl. Our proof must construct all these types. In some cases, for example natural numbers, we will need to use recursion, following example from Idris-dev/libs/prelude/Prelude/Nat.idr:
total plusZeroRightNeutral : (left : Nat) -> left + 0 = left
plusZeroRightNeutral Z = Refl
plusZeroRightNeutral (S n) =
let inductiveHypothesis = plusZeroRightNeutral n in
rewrite inductiveHypothesis in Refl |
Here the type depends on Nat, if it is true for n then we can show it is true for S n. So
| if |
|
Then |
|
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:
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.
Equations
We don't have to stick to terms, can also use symbolic parameters so the following will compile:
varIdentity : m = m varIdentity = Refl |
Although we must use specific values for the variables when we call it.
*proof> varIdentity
(input):Can't infer argument phTy to varIdentity,
Can't infer argument m to varIdentity
*proof> the (m=m) varIdentity
When checking argument x to type constructor =:
No such variable m
*proof> the (3=3) varIdentity
Refl : 3 = 3
|
Properties of Equations
An equation is defined as an equivalence relation (reflexivity, symmetry, transitivity), there are also rules that come from compatiblity with the algebraic structure.
| equivalence relation |
Reflexivity | x=x | |
| Symmetry | x = y iif y = x | ||
| Transitivity | if x = y and y = z then x = z | total testm1 : {a,b,c : Nat} ->
a = b ->
b = c ->
c = a
testm1 Refl Refl = Refl |
|
congruence (we can do the same thing to |
if x=y then f x = f y | cong : {f : t -> u} ->
(a = b) ->
f a = f b |
|
| substitution of variables (indiscernability of identicals) | replace : {P : a -> Type} ->
x = y ->
P x -> P y
rewrite__impl : (P : a -> Type) ->
x = y ->
P y -> P x |
||
Variables
We can represent variables in an equation by using dependent types, like this:
plusZeroRightNeutral: (x:Nat) -> (x = plus x Z)
So this generates a family of types:
- 0 = plus 0 Z
- 1 = plus 1 Z
- 2 = plus 2 Z
- ...
To prove it we must be able to construct for every value of x (it must be total).
Here are some more examples, the following will compile:
test0 : x=plus Z x test0 = Refl test1 : x=plus Z x -> x=plus Z x test1 p = p -- does not normalise --test2 : x=plus x Z --test2 = Refl test3 : x=plus x Z -> x=plus x Z test3 p = p |
Again, when we use the functions we must specify the values of the variables:
*proof> test0 (input):Can't infer argument x to test0 *proof> test1 (the (3=plus Z 3) Refl) Refl : 3 = 3 *proof> test3 (the (3=plus 3 Z) Refl) Refl : 3 = 3 *proof> |
Propositional Equality
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.
plusReducesL : (n:Nat) -> plus Z n = n plusReducesR : (n:Nat) -> plus n Z = n |
plusReducesR gives the following error:
- + 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.
Idris> 1+1 2 : Integer |
In the following pages we discuss how to resolve propositionaly equalies.
Here is a proof of the transitive properties of natural numbers. |
|
The work, for this proof, is done by the type system. We just need to give the type system the information it needs. so,
- The first Refl is a proof of a = b
- The second Refl is a proof of b = c
This is enough proof to return a proof (Refl) of c = a.
Proof
Following on from Curry-Howard correspondence (proposition as a type) then proofs correspond to functions of types. That is a function that results in a constructor for a type, usually Refl to construct an equality type.
So this function represents a proof that 'x=plus Z x' |
|
| Sometimes a proof of one proposition depends on the proof of another proposition, like this: |
|
Sometimes the Idris type system can't work out proofs for itself so we have to give it some help.
Proof Issues
There can be a lot of unexpected complications when doing proofs:
This is similar to the transitive example above and it works fine. |
|
|
Here the left and right sides of two of the equations have been transposed and now we get the following error: Type mismatch between S n and x |
|
Errors
| Although n = S n is a valid proposition it can never be a true proposition so it can't be constructed by Refl |
|
So Idris detects an error in the following function definition:
total e1 : {n : Nat} -> n = S n -> Nat
e1 Refl = Z |
|
177 | e1 Refl = Z
| ~~~~~~~
When checking left hand side of e1:
When checking an application of Main.e1:
Unifying n and S n would lead to infinite value |
Here swapping the left and right sides of the equation changes whether the function compiles or not:
e2 : {x,n : Nat} -> (S n) = x -> Nat
e2 Refl = Z |
this compiles fine |
e3 : {x,n : Nat} -> x = (S n) -> Nat
e3 Refl = Z |
|
204 | e3 Refl = Z
| ~~
When checking left hand side of e3:
When checking an application of Main.e3:
Type mismatch between
S n = S n (Type of Refl)
and
x = S n (Expected type)
Specifically:
Type mismatch between
S n
and
x |
Not sure why the asymmetry although the equality can't be total for all values of n and x because there is no 'n' that where S n = Z.
Natural Number Proofs in Idris
More detailed information about Natural Number Proofs in Idris on this page.
As an example look at proofs in Nat.
| The prelude has a function (==) that will check if two Nats are equal: |
|
But, even if this returns true, this is not a proof. If we have dependant types, where two types can be considered equal if they depend on equal Nat values, the type system can only use this if it has a proof that the Nat's are the same.
| Here is some code that returns a proof if two Nat's are equal. |
|
| This works like this: |
|
Congruence
We can do the same thing to both sides of an equation. That is if we have a proof that a = b then f a = f b.
We can replace sameSub above with a more generic function 'cong' defined like this: defined in module Prelude.Basics |
|
| So the proof for equality of Natural numbers becomes: |
|
|
The definition of a congruence depends on the type of algebraic structure under consideration. Particular definitions of congruence can be made for groups, rings, vector spaces, modules, semigroups, lattices, and so forth. The common theme is that a congruence is an equivalence relation on an algebraic object that is compatible with the algebraic structure, in the sense that the operations are well-defined on the equivalence classes. |
In this case the equality of these natural numbers is not true for all n and m.
In other cases we may want an equation to be true for all values, for instance:
x = x + 0
For more about this see page here.
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
comutePlus 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?
Next Stages
Here are some further pages on this site:
