Proofs in Idris

In order to understand how to write proofs in Idris I think its worth clarifying some fundamentals, such as,

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:

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
(S n) + 0 = (S n)
Then
n + 0 = n

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
both sides of an equation)

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:

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
plusReducesL n = Refl

plusReducesR : (n:Nat) -> plus n Z = n
plusReducesR n = Refl

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.

total testm1 : {a,b,c : Nat} -> a = b -> b = c -> c = a
testm1 Refl Refl = Refl

The work, for this proof, is done by the type system. We just need to give the type system the information it needs. so,

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'

test1 : x=plus Z x
test1 = Refl
Sometimes a proof of one proposition depends on the proof of another proposition, like this:
incBothSides : x = y -> S x = S y
incBothSides Refl = Refl

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.

total testm3 : {x,y,n : Nat} -> x = (S n) -> (S n) = y -> y = x
testm3 Refl Refl = Refl

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

total testm4 : {x,y,n : Nat} -> x = (S n) -> y = (S n) -> x = y
testm4 Refl Refl = ?holem4

Errors

Although n = S n is a valid proposition it can never be a true proposition so it can't be constructed by Refl
*proof> (n:Nat) -> n = S n
(n : Nat) -> n = S n : Type
*proof> 
      

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:
Eq Nat where
  Z == Z         = True
  (S l) == (S r) = l == r
  _ == _         = False
      

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.
sameSub : (k : Nat) -> (j : Nat) -> (k=j) -> ((S k)=(S j))
sameSub k k Refl = Refl

ckEqNat : (n : Nat) -> (m : Nat) -> Maybe (n = m)
ckEqNat Z Z = Just Refl
ckEqNat Z (S j) = Nothing
ckEqNat (S i) Z = Nothing
ckEqNat (S i) (S j) = case ckEqNat i j of
                           Nothing => Nothing
                           --Just eq => Just (S i=S j)
                           -- This is what we want but we can't
                           -- write this without proof that S i=S j
                           -- eq is a proof that i=j we want
                           -- to turn this into a proof that
                           -- S i = S j
                           --Just eq => Just (rewrite Refl eq)
                           Just eq => Just (sameSub i j eq)
      
This works like this:
Type checking ./proof.idr
*proof> ckEqNat 4 4
Just Refl : Maybe (4 = 4)
*proof> ckEqNat 4 3
Nothing : Maybe (4 = 3)
*proof> ckEqNat 3 4
Nothing : Maybe (3 = 4)
*proof> ckEqNat 20 20
Just Refl : Maybe (20 = 20)
*proof> :total sameSub
Main.sameSub is Total
*proof> sameSub 4 4 Refl
Refl : 5 = 5
*proof> sameSub 4 3 Refl
(input):1:1-16:When checking an application of function Main.sameSub:
        Type mismatch between
                x = x (Type of Refl)
        and
                4 = 3 (Expected type)
        
        Specifically:
                Type mismatch between
                        1
                and
                        0

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

||| Equality is a congruence.
cong : {f : t -> u} -> (a = b) -> f a = f b
cong Refl = Refl
So the proof for equality of Natural numbers becomes:
ckEqNat : (n : Nat) -> (m : Nat) -> Maybe (n = m)
ckEqNat Z Z = Just Refl
ckEqNat Z (S j) = Nothing
ckEqNat (S i) Z = Nothing
ckEqNat (S i) (S j) = case ckEqNat i j of
                           Nothing => Nothing
                           Just eq => Just (cong eq)

Definition from Wikipedia

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:

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:

Next Stages

Here are some further pages on this site:


metadata block
see also:
  • For more information about propositional logic see page here
  • For more information about type theory see page here
  • Specifically about how constructors and deconstructors relate to introduction and elimination see page here
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Type-Driven Development with Idris

 

Commercial Software Shop

Where I can, I have put links to Amazon for commercial software, not directly related to the software project, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2022 Martin John Baker - All rights reserved - privacy policy.