# 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:

• We can call Refl for every element of the variable (which requires recursion for infinite types).
• We can rely on the built-in rules in Idris.
 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)

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.

 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.