@@ -0,0 +1,94 @@
1+This page attempts to explain some of the techniques used in Idris to prove propositional equalities.
3+Proving Propositional Equality
4+==============================
6+We have seen that definitional equalities can be proved using Refl since they always normalise to unique values that can be compared directly.
8+However with propositional equalities we are using symbolic variables they do not always normalse.
10+So to take the previous example:
12+plusReducesR : (n:Nat) -> plus n Z = n
14+In this case 'plus n Z' does not normalise to n. Even though both sides are equal we cannot pattern match Refl.
16+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.
22+ plusReducesR : n = plus n 0
23+ plusReducesR {n = Z} = Refl
24+ plusReducesR {n = (S k)} = let rec = plus_commutes_Z {n=k} in
27+we don't call Refl to match on 'n = plus n 0' forall 'n' we call it for every number separately. So, in the second line, somehow the pattern matcher knows to substitute Z for n in the type being matched.
32+If two terms are equal then they have the same properties. In our proofs we can express this as:
37+where P is a pure function.
39+To use this in our proofs there is the following function in the prelude:
43+ ||| Perform substitution in a term according to some equality.
44+ replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
45+ replace Refl prf = prf
50+Similar to 'replace' above but Idris provides a nicer syntax which makes 'rewrite' easier to use in examples like plusReducesR above.
54+ ||| Perform substitution in a term according to some equality.
56+ ||| Like `replace`, but with an explicit predicate, and applying the rewrite
57+ ||| in the other direction, which puts it in a form usable by the `rewrite`
59+ rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x
60+ rewrite__impl p Refl prf = prf
62+Symmetry and Transitivity
63+=========================
65+In addition to 'reflexivity' equality also obeys 'symmetry' and 'transitivity' and these are also included in the prelude:
69+ ||| Symmetry of propositional equality
70+ sym : {left:a} -> {right:b} -> left = right -> right = left
73+ ||| Transitivity of propositional equality
74+ trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c
75+ trans Refl Refl = Refl
77+Heterogeneous Equality
78+======================
80+Also included in the prelude:
84+ ||| Explicit heterogeneous ("John Major") equality. Use this when Idris
85+ ||| incorrectly chooses homogeneous equality for `(=)`.
86+ ||| @ a the type of the left side
87+ ||| @ b the type of the right side
88+ ||| @ x the left side
89+ ||| @ y the right side
90+ (~=~) : (x : a) -> (y : b) -> Type