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 | ||
|---|---|---|---|
|
a=b |
x:A,y:A,A:TypeThis 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 | ||
|---|---|---|---|
|
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. |
|
||||||
| 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). |
|
||||||
| To specify the implied types and make things more precise the indentity elimination rule is more fully specified something like this: |
|
||||||
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:
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: |
|
|
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. |
|
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?
