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:
- identities like x = x+ 0
- other relations like a * x * x + b * x + c = 0
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 like
x : 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:
xa,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.
xt : 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 |  |
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 |
 |
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:
- P(0) is true
- P(n) -> P(S n)
then P is true for all numbers:
So if we want to prove 'n = plus n 0' then we must prove:
- '0 = plus 0 0'
- 'n = plus n 0' -> '(S n) = plus (s n) 0'
However, induction is done using recursion, there is a sort of reversal of direction going on here:
- proofs go from hypothesis to conclusion
- tactics tend to start with the conclusion we want and work back to the hypothesis (via holes)
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:
- intro: If the goal is of the form (a:A) -> B, introduce a premiss a, and replace the goal with B.
- intro x,y,...: Introduce several premisses at once.
- compute: Normalise the goal
- refl: Solve a goal of the form x=y where x and y have the same normal form.
- induction t: Solve a goal by induction on t. Creates subgoals for each possible constructor of t.
- rewrite t: If t has type x=y replace any instance of y in the goal with x
- rewrite <- t: If t has type x=y replace any instance of x in the goal with y
- fill x: If x has type T, then fill x solves a goal of type T.
- refine x: If x has a function type, returning a value of type T, refine x introduces subgoals for each argument of x, attempting to solve as many as possible automatically by unification.
- trivial: If there is a premiss which solves the goal immediately, use it.
- undo: Undo the previous tactic.
- generalise t: Abstract the goal over a variable x and replace any occurence of the term t in the goal with x
- unfold n: Replace any occurrence of the name n in the goal with its definition, if possible.
- decide t: This is a slightly complicated tactic, but can be useful for creating and applying decision procedures. If the goal is of the form T a b c, and t has type t : (a:A) -> (b:B) -> (c:C) -> Maybe (T a b c), apply t a b c. If the result is Just x, solve the goal with x, otherwise fail.
Next Stages
More pages about equalities on this site:
Back to proofs page.
