@@ -24,19 +24,21 @@ So here:
24 plusReducesR {n = (S k)} = let rec = plus_commutes_Z {n=k} in
24 plusReducesR {n = (S k)} = let rec = plus_commutes_Z {n=k} in
25 rewrite rec in Refl
25 rewrite rec in Refl
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.
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:
35 then P x = P y
35 then P x = P y
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
39+So if n is a natural number variable then P could be something like 2*n + 3.
39−To use this in our proofs there is the following function in the prelude:
41+To use this in our proofs there is the following function in the prelude:
41.. code-block:: idris
43.. code-block:: idris
@@ -44,6 +46,23 @@ To use this in our proofs there is the following function in the prelude:
44 replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
46 replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
45 replace Refl prf = prf
47 replace Refl prf = prf
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)
54+ replace : (x = y) -> P x -> P y
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.
63+ testReplace: (x=y) -> (p1 x) -> (p1 y)
64+ testReplace a b = replace a b
@@ -51,14 +70,29 @@ Similar to 'replace' above but Idris provides a nicer syntax which makes 'rewrit
52.. code-block:: idris
71.. code-block:: idris
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
73 rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x
60 rewrite__impl p Refl prf = prf
74 rewrite__impl p Refl prf = prf
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).
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.
85+ testRewrite2: (x=y) -> (p1 y) -> (p1 x)
86+ testRewrite2 a b = rewrite a in b
88+We can think of rewrite doing this:
90+ * Start with a equation x=y and a property P: x -> Type
92+ * Replaces all occurrences of y with x in P.
94+That is, we are doing a substitution.
62Symmetry and Transitivity
96Symmetry and Transitivity
63=========================
97=========================