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.

Formation

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
a=b

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 takes a propositional equality and returns a type for all terms a and b. The type is inhabited when a and b are propositionally equal.

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:

total
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


total
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

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

Replace

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

   if x=y
   then P x = P y

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

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

To use this in our proofs 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

Rewrite

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
Refl

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)

Assoc

from here

import Reflect

total
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-2022 Martin John Baker - All rights reserved - privacy policy.