# 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
 Γ x:A,y:A,A:Type Γ IdA(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
 Γ x:A Γ reflx: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:
 ```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:

• Start with a equation x=y and a property P: x -> Type
• Searches y in P
• Replaces all occurrences of y with x in P.

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?

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.      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.