This page attempts to explain some of the techniques used in Idris to prove propositional equalities.

# Proving Propositional Equality

We have seen that definitional equalities can be proved using `Refl`

since they
always normalise to values that can be compared directly.

However with propositional equalities we are using symbolic variables, which do not always normalise.

So to take the previous example:

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

In this case `plus n Z`

does not normalise to n. Even though both sides of
the equality are provably equal we cannot claim `Refl`

as a proof.

If the pattern match cannot match for all `n`

then we need to
match all possible values of `n`

. In this case

```
plusReducesR : (n : Nat) -> plus n Z = n
plusReducesR Z = Refl
plusReducesR (S k)
= let rec = plusReducesR k in
rewrite rec in Refl
```

we can’t use `Refl`

to prove `plus n 0 = n`

for all `n`

. Instead, we call
it for each case separately. So, in the second line for example, the type checker
substitutes `Z`

for `n`

in the type being matched, and reduces the type
accordingly.

# 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 prop x = prop y

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

So if `n`

is a natural number variable then `prop`

could be something
like `\n => 2*n + 3`

.

To use this in our proofs there is the following function in the prelude:

```
||| Perform substitution in a term according to some equality.
replace : forall x, y, prop . (0 rule : x = y) -> prop x -> prop y
replace Refl prf = prf
```

If we supply an equality (x=y) and a proof of a property of x (`prop x`

) then we get
a proof of a property of y (`prop y`

).
So, in the following 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`

.

```
p1: Nat -> Type
p1 n = (n=2)
testReplace: (x=y) -> (p1 x) -> (p1 y)
testReplace a b = replace a b
```

# Rewrite

In practice, `replace`

can be
a little tricky to use because in general the implicit argument `prop`

can be hard to infer for the machine, so Idris provides a high level
syntax which calculates the property and applies `replace`

.

Example: again we supply `p1 x`

which is a proof that `x=2`

and the equality
`y=x`

then we get a proof that `y=2`

.

```
p1: Nat -> Type
p1 x = (x=2)
testRewrite: (y=x) -> (p1 x) -> (p1 y)
testRewrite a b = rewrite a in b
```

We can think of `rewrite`

as working in this way:

Start with a equation

`x=y`

and a property`prop : x -> Type`

Search for

`x`

in`prop`

Replaces all occurrences of

`x`

with`y`

in`prop`

.

That is, we are doing a substitution.

Notice that here we need to supply reverse equality, i.e. `y=x`

instead of `x=y`

.
This is because `rewrite`

performs the substitution of left part of equality to the right part
and this substitution is done in the *return type*.
Thus, here in the return type `y=2`

we need to apply `y=x`

in order to match the type of the argument `x=2`

.

# 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 : forall x, y . (0 rule : x = y) -> y = x
sym Refl = Refl
||| Transitivity of propositional equality
trans : forall a, b, c . (0 l : a = b) -> (0 r : 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)
```