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 propertyprop : x -> Type
Search for
x
inprop
Replaces all occurrences of
x
withy
inprop
.
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)