Proofs Equality

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

Equalities

We use the equals sign a lot in programming languages, sometimes it is used to make an assignment. In some languages ':=' denotes an assignment but (unfortunately) Idris (and Haskell) the '=' is used for assignments.

Here we are mostly interested in mathematical equalities, as opposed to assignments, these are equivalence relations (that is they are reflexive, symmetric and transitive).

In mathematics we can use equations in different ways:

The first of these is what we need for proofs in the type system but I am also interested in proving things like quadratic equations.

In the first type (identities) we are saying this equation is true for all values of the variable. In some languages, like Agda, a 3-bar equality (≡) is used for identities like this. In mathematical terms we use quantifiers likefor allx : x = x+ 0 to indicate that it is true for all values of x.

In the second type we are saying there is at least one value of x for all values of a, b and c:

there existsxfor alla,b,c : a * x * x + b * x + c = 0 (assume x is a complex number to avoid complications)

another example of this are things like:

x = sine(t)

If the function 'sine' is total then we are saying that there is one output for every input.

there existsxfor allt : x = sine(t)

Equality in Martin Löf Type Theory

Usually in Idris, if we want to check equality for a term, we must implement the Eq interface for that type:

||| The Eq interface defines inequality and equality.
interface Eq ty where
    (==) : ty -> ty -> Bool
    (/=) : ty -> ty -> Bool

However, when we are doing proofs, we work with constructive logic instead of Boolean Logic. The mathematics of constructive logic and types is essentially the same (Curry-Howard correspondence) so we use types to represent propositions.

Therefore an equality is conceptually defined like this:

data (=) : a -> b -> Type where
    Refl : x = x

So it is a type-family, a type which depends on the terms 'a' and 'b'.

In Martin Löf type theory each type, in this case equality type, has three rules associated with it:

formation (=) : a -> b -> Type
constructor Refl : x = x
eliminator (deconstructor)
postulate J : (P : (a,b:t) -> (a~~b) -> Type) ->
    ((a:t) -> P a a (refl_ a)) ->
    ((a,b:t) -> (p:a~~b) -> P a b p)

Reflexitivity does not fully define equality, for example ≥is reflexive but is not the same as =. The eliminator 'J' is the 'least reflexive relation' that is, only types on the diagonal are inhabited, this is its universal property (extreemal clause).

If the types which are not on the diagonal are not inhabited we can say anything about them, so we need a function going in the other direction (the eliminator).

J=Q[M/a]

Identity (Propositional Equality) Constructor

If we have an identity type

 
x = x : Type

then we can construct it with a simple constructor with no parameters

 
Refl : x = x

That is, if x=x is inhabited by Refl that constitutes a proof that x=x.

However this hides a lot of complexity, if we use the same symbol on both sides of the equation - what does that mean? We might say that the meaning comes from the deconstuctor but how is this all implemented?

In some ways we could think of rewrite as like a second constructor for an equality type. So it behaves a bit like an inductively defined type where Refl can construct a definitional equality on its own but requires the help of rewrites to identity as inductive type

Proving Propositional Equality

We have seen that definitional equalities can be proved using Refl since they always normalise to unique values that can be compared directly.

However with propositional equalities we are using symbolic variables they do not always normalse.

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 are equal we cannot pattern match refl.

If the pattern match cannot match for all 'n' then the way around this is to separately match all possible values of 'n'. In the case of natural numbers we do this by induction.

So here:

plusReducesR : n = plus n 0
plusReducesR {n = Z} = Refl
plusReducesR {n = (S k)} =
    let rec = plus_commutes_Z {n=k} in
        rewrite sym rec in Refl
plus reduces proof

where:

sym - is in Idris library proof of symmetry

So this is like calling it for every number separately rather than calling Refl to match on 'n = plus n 0' forall 'n'.

If we want to prove something for the natural numbers the most powerful approach is proof by induction, that is:

If P(n) is a property of number 'n' and:

then P is true for all numbers:

So if we want to prove 'n = plus n 0' then we must prove:

However, induction is done using recursion, there is a sort of reversal of direction going on here:

So the hole we are trying to prove goes in the opposite direction:

{hole_0} : (k : Nat) -> (k = plus k 0) -> S k = S (plus k 0)

Replace

If two terms are equal then they have the same properties. In our proofs we can express this as:

   if x=y
   then P x = P y

where P is a pure function.

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

||| Perform substitution in a term according to some equality.
replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
replace Refl prf = prf

Rewrite

Similar to 'replace' above but Idris provides a nicer syntax which makes 'rewrite' easier to use in examples like plusReducesR above.

||| Perform substitution in a term according to some equality.
|||
||| Like `replace`, but with an explicit predicate, and applying the rewrite
||| in the other direction, which puts it in a form usable by the `rewrite`
||| tactic and term.
rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x
rewrite__impl p Refl prf = prf

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 : {left:a} -> {right:b} -> left = right -> right = left
sym Refl = Refl

||| Transitivity of propositional equality
trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c
trans Refl Refl = Refl

data (=) : a -> b -> Type where
   Refl : x = x

In case the infix notation make it harder to understand here is a prefix version (see this video):

data Id : a -> b -> Type where
   Reflexive : Id x x 

This is a GADT with one constructor that will only work if both parameters are the same.

a and b can be either a type or a value

contrast with

data Point2D : Type where
   Pt  : Double -> Double -> Point2D

So to construct this type/proposition

twoPlusTwo : 1 + 1 = 2
twoPlusTwo = Refl

I assume Refl must pattern match on its return type so that it constructs the correct type (1 + 1 = 2).

x

Rewrite

If both sides of the equation dont normalise to the same value/type then we may be able to use rewrite so they do:

plus_commutes_Z : m = plus m 0
plus_commutes_Z {m = Z} = Refl
plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in
                                  rewrite rec in Refl

So how does that work? 'm' and 'plus m 0' dont normalise to the same value so how can Refl construct the type 'm = plus m 0' ?

If we have   X:x=z
then   rewrite X in Y

will do a substitution to replace all occurences of x with y in Y.

replace : (x = y) -> P x -> P y

Given a proof that x = y, and a property P which holds for x, we can get a proof of the same property for y, because we know x and y must be the same. In practice, this function can be a little tricky to use because in general the implicit argument P can be hard to infer by unification, so Idris provides a high level syntax which calculates the property and applies replace:

rewrite prf in expr

see this thread

One of the difficulties of writing programs with dependent types is that when you write a function
implementation, you have to prove that the type of the returned value is the same as that in the definition.

Replace and rewrite do that but the syntax used in them can hinder the readability of the code,
making very simple proofs very difficult for no reason.

There is a nice syntax for rewrite that is like this:

rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>
        (Z + m = m) in Refl

as can be seen in misc.rst
but it is not adequately documented.

This syntax is nice because when someone reviews the proof, they can see the changed type
 as is common in mathematical proofs.

A secondary issue regarding the readability of the code when using rewrite and the "match" 
application syntax can be found in #3425.

Tactics

There are several tactics available, some of which have been used above. The tactics are briefly described here:

Next Stages

More pages about equalities on this site:

Back to proofs page.

 


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-2022 Martin John Baker - All rights reserved - privacy policy.