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) |
