Proving Equalities

On this page we give lots of very simple examples of proofs to illustrate the 'design patterns' when proving.

We can prove various equalities by just using Refl if both sides normalise to the same.

oneEqOne : 1=1
oneEqOne = Refl
Literal values are equal if they are the same.
oneEqTwo : (1=2) -> Void
oneEqTwo Refl impossible
1=2 is a type but it can't be constructed, this is how this situation is modeled in Idris
onePlusOne : 1+1=2
onePlusOne = Refl
Both sides of the equation are normalised before comparison so this proof works.
typeEquality : Bool = Bool
typeEquality = Refl
Since Idris allows dependant types we can compare types.
varIdentity : m = m
varIdentity = Refl
We can also compare variables. Here we have identity types, this is a special case, see below for more about variables in equalities.

Variables

When we have equations with variables then in most cases the type of the parameter will need to be given (explicitly of implicitly) so that we can prove it for all values of the variable.

When dealing with variables there are two main approaches to proving:

orFalseNeutral : (x : Bool) -> x || False = x
orFalseNeutral False = Refl
orFalseNeutral True = Refl

This is an example of a proof, with a variable, that generates Refl for every value of the variable.

This is a proof from the Idris library Data.Bool.Extra.

plusZx : x=plus Z x
plusZx = Refl
Here the type of x is known because the compiler knows the parameter type of plus.
x=plus x Z
'plus Z x' above normalises to x but this example: x=plus x Z does not even though it is provably true. So we need to give the compiler extra help to prove it.

Equality Parameters

In this case we are considering parameters of the form x=y

We can think of the parameters of a proof function as being analogous to the antecedent or context of a proof. When a proposition is true but we can't constuct it directly with Refl the compiler needs some help, one way to help the compiler is to give more information through extra parameters.

testP1 : 1=1 -> 1+1=2
testP1 Refl = Refl
Here the parameter 1=1 is not required and does not do anything. It can always be constructed with Refl.
plusxZ2 : x=plus x Z -> x=plus x Z
plusxZ2 p = p
Here is a trivial example which says, given a proof of x=plus x Z then x=plus x Z.
plusxZ2 Refl = Refl -- gives error
We can't prove the above like this though.
incBothSides : x = y -> S x = S y
incBothSides Refl = Refl

If we have a proof of x=y then we can get a proof of S x = S y

This is a specific example of a more general idea cong (congruence) defined in libs/prelude/Prelude/Basics.idr

Why does this work, but the example above does not?

If an equality is provable but the above methods still don't allow Idris to complete the proof then we may need to substitute a variable using the Idris replace or rewrite constructions. This is described on this page.

incx : (x : Nat) -> x = (plus x Z) -> S x = S (plus x Z)
incx x p = rewrite p in Refl 
rewrites x to plus x 0 in S x = S (plus x Z)

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 Type-Driven Development with Idris

 

Commercial Software Shop

Where I can, I have put links to Amazon for commercial software, not directly related to the software project, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.