Maths - Propositional Equality in Idris

Equality (identity) Types

Equality types (AKA identity types) are used in Idris to work with propositional equalities, that is equalities that may not be normalising and so need a proof.

An equality type is an equivalence relation, that is, a relation which is reflexive, symmetric, and transitive.

Equality types have been introduced on other pages but here we take a slightly more formal approach. In general types are defined by the formation, introduction and elimination rules and beta and gamma reductions.


The creation of equality types is done by a built-in infix '=' operator like this:

Logic Idris
Γright adjointx:A,y:A,A:Type
Γright adjointIdA(x,y):Type

This represents the proposition that 'a' is equal to 'b'. On its own it does not indicate if the proposition is true or not. The truth can only be established by constructing the type. That is only inhabited equality types are true.

Term Introduction Rule

The introduction rule allows us to create an instance of the equality type and an inhabited type represents truth it is a proof of the proposition.

There is only one way to introduce an equality type in Idris, that is refl (reflexitivity).

Logic Idris
Γright adjointx:A
Γright adjointreflx:IdA(x,x):Type
the (a=b) refl

So the above proves a=b if it compiles.

'refl' requires that its equality type contains 2 terms which are the same (definitionally equal) but we only want to prove propositional equality so how can we prove an equality that is propositional but not definitional? We can first case split the type then call 'refl' on each part.

Term Elimination Rule

The eliminator tells us how to use a type and it can also tell us what a type 'means'.

In programming a propositional equality between two types allows us to treat the two types interchangeably. Perhaps it is the loosest equality that allows this? How could we express such a conjecture?

If this was true then, given the identity type 'Id', we should be able to construct any other such relationship 'C' because C is always going to be weaker than Id:



We need to refine that a bit, we cant construct any relationship, C needs to be an equivalence relationship.

It turns out that it is sufficient to specify reflectivity then symmetry and transitivity can be implied from that.

IdA(x,y)   CA(x,x)
If we want proofs of these things we need to show these things are inhabited. So 'p' is a proof of Id and 't' is a proof of reflexivity. These proofs are combined to give J(t,p).
p:IdA(x,y)   t:C(x,x,r(x)):Type
To specify the implied types and make things more precise the indentity elimination rule is more fully specified something like this:
Γ,x:A,y:A, p:IdA(x,y)right adjointC(x,y,p):Type   Γ,x:A,right adjointC(x,x,r(x)):Type
Γ,x:A,y:A,p:IdA(x,y)right adjointJ(t; x,y,p):C(x,y,p)

By Induction

There are other ways to approach the Id term eliminator. We can look at it as an induction idea. We can use proofs to get more equal terms, then apply proofs to these and so on.

Eliminator in Idris

This eliminator is traditionally called J.

In Idris the type is notated with an equality so the distinction between the type and the equation is not really made.

The equality type can be used in function signatures, for example:

Myfunction (a:Nat) -> (b:Nat) -> a=b

Usually extra parameters in function signatures add more degrees of freedom but, in the case of adding a function type this reduces the degrees of freedom.

As an example:

myfunction: (a:Nat) -> (b:Nat) -> a=b -> Type
myfunction Z Z refl = (0=0)
myfunction (S a) Z refl = (1=0) -- cant happen
myfunction Z (S b) refl = (0=1) -- cant happen
myfunction (S a) (S b) refl = (1=1)

The cases where only one input is zero are not really needed because they can't happen because they are equal. I think later versions of Idris will be clever enough to accept the function as total without needing these cases.

The above function could be reduced to:

myfunction2: Nat -> Type
myfunction2 Z = (0=0)
myfunction2 (S a) = (1=1)

A more general form to illustrate the elimination of a=b is:

P: (a,b:t) -> a=b -> Type

MyBool Example

As an example lets take a very simple type, that is, a boolean type:
data MyBool = T | F

myNot: MyBool -> MyBool
myNot T = F
myNot F = T
data Id1 : MyBool -> MyBool -> Type where
   Refl11 : Id1 x x

data Id2 : MyBool -> MyBool -> Type where
   Refl22 : Id2 x (myNot x)
So that we can experiment, instead of using the built-in equality type, we can construct an identity type specifically for this:
We can now experiment with proving things about this type.
isItself: (x:MyBool) -> (Id1 x x)
isItself x = Refl11

isNot: (x:MyBool) -> (Id2 x (myNot x))
isNot x = Refl22

isNotNot: (x:MyBool) -> (Id1 x (myNot (myNot x)))
isNotNot T = Refl11
isNotNot F = Refl11


This implements the 'indiscernability of identicals' principle, if two terms are equal then they have the same properties. In other words, if x=y then we can substitute y for x in any expression. In our proofs we can express this as:

   if x=y
   then P x = P y

where P is a pure function representing the property. In the examples below P is an expression in some variable with a type like this: P: n -> Type

So if n is a natural number variable then P could be something like 2*n + 3.

To use this in our proofs we use the replace or rewrite functions in the prelude:

||| Perform substitution in a term according to some equality.
replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
replace Refl prf = prf
Removing the implicit's, 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)
> :t replace
replace : (x = y) -> P x -> P y
p1: Nat -> Type
p1 n = (n=2)

testReplace: (x=y) -> (p1 x) -> (p1 y)
testReplace a b = replace a b
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


Similar to 'replace' above but Idris provides a nicer syntax which makes 'rewrite' easier to use in common cases.

p1: Nat -> Type
p1 x = (x=2)

testRewrite: (x=y) -> (p1 y) -> (p1 x)
testRewrite a b = rewrite__impl p1 a b

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.

The difference from 'replace' above is that the property p1 is explicitly supplied and it goes in the opposite direction (input and output reversed)

Idris provides a nicer syntax, rewrite a in b like this,

p1: Nat -> Type
p1 x = (x=2)

testRewrite2: (x=y) -> (p1 y) -> (p1 x)
testRewrite2 a b = rewrite a in b

Same example with nicer syntax.

We can think of rewrite doing this:

That is, we are doing a substitution.

Examples from Nat in Idris library:

total plusZeroRightNeutral : (left : Nat) -> left + 0 = left
plusZeroRightNeutral Z     = Refl
plusZeroRightNeutral (S n) =
  let inductiveHypothesis = plusZeroRightNeutral n in
    rewrite inductiveHypothesis in Refl

total plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
  S (left + right) = left + (S right)
plusSuccRightSucc Z right        = Refl
plusSuccRightSucc (S left) right =
  let inductiveHypothesis = plusSuccRightSucc left right in
    rewrite inductiveHypothesis in Refl

total plusCommutative : (left : Nat) -> (right : Nat) ->
  left + right = right + left
plusCommutative Z        right = rewrite plusZeroRightNeutral right in Refl
plusCommutative (S left) right =
  let inductiveHypothesis = plusCommutative left right in
    rewrite inductiveHypothesis in
      rewrite plusSuccRightSucc right left in Refl

total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
  left + (centre + right) = (left + centre) + right
plusAssociative Z        centre right = Refl
plusAssociative (S left) centre right =
  let inductiveHypothesis = plusAssociative left centre right in
    rewrite inductiveHypothesis in Refl

from here

plus_comm : (n : Nat) -> (m : Nat) -> (n + m = m + n)

-- Base case
-- (Z + m = m + Z) <== plus_comm = -- broken by typecase check
plus_comm Z m =
    rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>
            (Z + m = m) in Refl

-- Step case
-- (S k + m = m + S k) <== plus_comm =
plus_comm (S len) m =
    rewrite ((len + m = m + len) <== plus_comm) in
    rewrite ((S (m + len) = m + S len) <== plusSuccRightSucc) in

Symmetry and Transitivity

In addition to 'reflexivity' equality also obeys 'symmetry' and 'transitivity' and these are also included in the prelude:

||| Symmetry of propositional equality
sym : {left:a} -> {right:b} -> left = right -> right = left
sym Refl = Refl

||| Transitivity of propositional equality
trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c
trans Refl Refl = Refl

Heterogeneous Equality

Also included in the prelude:

||| Explicit heterogeneous ("John Major") equality. Use this when Idris
||| incorrectly chooses homogeneous equality for `(=)`.
||| @ a the type of the left side
||| @ b the type of the right side
||| @ x the left side
||| @ y the right side
(~=~) : (x : a) -> (y : b) -> Type
(~=~) x y = (x = y)


from here

import Reflect

testReflect0 : (xs, ys : List a) -> ((xs ++ (ys ++ xs)) = ((xs ++ ys) ++ xs))
testReflect0 {a} xs ys = AssocProof a

I think this uses depreciated tactic proof?

metadata block
see also:
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 Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.


Terminology and Notation

Specific to this page here:


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

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