@@ -24,19 +24,21 @@ So here:
2424 plusReducesR {n = (S k)} = let rec = plus_commutes_Z {n=k} in
2525 rewrite rec in Refl
2626
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.
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, the pattern matcher knows to substitute Z for n in the type being matched. This uses 'rewrite' which is explained below.
2828
2929Replace
3030=======
3131
32−If two terms are equal then they have the same properties. In our proofs we can express this as:
32+This implements the 'indiscernability of identicals' principle, if two terms are equal then they have the same properties. In other words, if x=y, then we can substitute y for x in any expression. In our proofs we can express this as:
3333
3434 if x=y
3535 then P x = P y
3636
37−where P is a pure function.
37+where P is a pure function representing the property. In the examples below P is an expression in some variable with a type like this: P: n -> Type
3838
39−To use this in our proofs there is the following function in the prelude:
39+So if n is a natural number variable then P could be something like 2*n + 3.
40+
41+To use this in our proofs there is the following function in the prelude:
4042
4143.. code-block:: idris
4244
@@ -44,6 +46,23 @@ To use this in our proofs there is the following function in the prelude:
4446 replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
4547 replace Refl prf = prf
4648
49+Removing the implicits, if we supply an equality (x=y) and a proof of a property of x (P x) then we get a proof of a property of y (P y)
50+
51+.. code-block:: idris
52+
53+ > :t replace
54+ replace : (x = y) -> P x -> P y
55+
56+So, in the following example, if we supply p1 x which is a proof that x=2 and the equality x=y then we get a proof that y=2.
57+
58+.. code-block:: idris
59+
60+ p1: Nat -> Type
61+ p1 n = (n=2)
62+
63+ testReplace: (x=y) -> (p1 x) -> (p1 y)
64+ testReplace a b = replace a b
65+
4766Rewrite
4867=======
4968
@@ -51,14 +70,29 @@ Similar to 'replace' above but Idris provides a nicer syntax which makes 'rewrit
5170
5271.. code-block:: idris
5372
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.
5973 rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x
6074 rewrite__impl p Refl prf = prf
6175
76+The difference from 'replace' above is nicer syntax and the property p1 is explicitly supplied and it goes in the opposite direction (input and output reversed).
77+
78+Example: again we supply p1 which is a proof that x=2 and the equality x=y then we get a proof that y=2.
79+
80+.. code-block:: idris
81+
82+ p1: Nat -> Type
83+ p1 x = (x=2)
84+
85+ testRewrite2: (x=y) -> (p1 y) -> (p1 x)
86+ testRewrite2 a b = rewrite a in b
87+
88+We can think of rewrite doing this:
89+
90+ * Start with a equation x=y and a property P: x -> Type
91+ * Searches y in P
92+ * Replaces all occurrences of y with x in P.
93+
94+That is, we are doing a substitution.
95+
6296Symmetry and Transitivity
6397=========================
6498