@@ -0,0 +1,94 @@
1+This page attempts to explain some of the techniques used in Idris to prove propositional equalities.
2+
3+Proving Propositional Equality
4+==============================
5+
6+We have seen that definitional equalities can be proved using Refl since they always normalise to unique values that can be compared directly.
7+
8+However with propositional equalities we are using symbolic variables they do not always normalse.
9+
10+So to take the previous example:
11+
12+plusReducesR : (n:Nat) -> plus n Z = n
13+
14+In this case 'plus n Z' does not normalise to n. Even though both sides are equal we cannot pattern match Refl.
15+
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.
17+
18+So here:
19+
20+.. code-block:: idris
21+
22+ plusReducesR : n = plus n 0
23+ plusReducesR {n = Z} = Refl
24+ plusReducesR {n = (S k)} = let rec = plus_commutes_Z {n=k} in
25+ rewrite rec in Refl
26+
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.
28+
29+Replace
30+=======
31+
32+If two terms are equal then they have the same properties. In our proofs we can express this as:
33+
34+ if x=y
35+ then P x = P y
36+
37+where P is a pure function.
38+
39+To use this in our proofs there is the following function in the prelude:
40+
41+.. code-block:: idris
42+
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
46+
47+Rewrite
48+=======
49+
50+Similar to 'replace' above but Idris provides a nicer syntax which makes 'rewrite' easier to use in examples like plusReducesR above.
51+
52+.. code-block:: idris
53+
54+ ||| Perform substitution in a term according to some equality.
55+ |||
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`
58+ ||| tactic and term.
59+ rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x
60+ rewrite__impl p Refl prf = prf
61+
62+Symmetry and Transitivity
63+=========================
64+
65+In addition to 'reflexivity' equality also obeys 'symmetry' and 'transitivity' and these are also included in the prelude:
66+
67+.. code-block:: idris
68+
69+ ||| Symmetry of propositional equality
70+ sym : {left:a} -> {right:b} -> left = right -> right = left
71+ sym Refl = Refl
72+
73+ ||| Transitivity of propositional equality
74+ trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c
75+ trans Refl Refl = Refl
76+
77+Heterogeneous Equality
78+======================
79+
80+Also included in the prelude:
81+
82+.. code-block:: idris
83+
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
91+ (~=~) x y = (x = y)
92+
93+
94+