git.iko.soy/Idris-dev
on master help sign in
Proofs docs were fixed a little.
1d5eb9cDenis Buzdalov
docs/proofs/interactive.rst+16−16
compare with master
unifiedsplit
@@ -15,15 +15,15 @@ construct proofs as described on this page.
15Elab and Pruviloj Libraries
15Elab and Pruviloj Libraries
16===========================
16===========================
17
17
18−Elaborator reflection is defined in prelude/Language/Reflection/Elab.idr
18+Elaborator reflection is defined in ``prelude/Language/Reflection/Elab.idr``
19−and pruviloj is defined in Idris-dev/libs/pruviloj/
19+and ``pruviloj`` is defined in ``Idris-dev/libs/pruviloj/``.
20
20
21−``Elab`` defines the basics such as: solve, attack, intro, compute,
21+``Elab`` defines the basics such as: ``solve``, ``attack``, ``intro``, ``compute``,
22−rewriteWith and others.
22+``rewriteWith`` and others.
23``pruviloj`` defines some more advanced derived commands such as:
23``pruviloj`` defines some more advanced derived commands such as:
24−reflexivity and others.
24+``reflexivity`` and others.
25
25
26−To use ``pruviloj`` call Idris with the "-p pruviloj" option and add:
26+To use ``pruviloj`` call Idris with the ``-p pruviloj`` option and add:
27
27
28.. code-block:: idris
28.. code-block:: idris
29
29
@@ -34,7 +34,7 @@ to the top of your file.
34
34
35It is useful to get the docs at the REPL by using the ``:doc`` command, and
35It is useful to get the docs at the REPL by using the ``:doc`` command, and
36search the docstrings using ``:apropos``. So to introduce the functions from
36search the docstrings using ``:apropos``. So to introduce the functions from
37−Elab and Pruviloj, that we will need for the following example, here are
37+``Elab`` and ``Pruviloj``, that we will need for the following example, here are
38their docstrings:
38their docstrings:
39
39
40.. code-block:: idris
40.. code-block:: idris
@@ -84,7 +84,7 @@ their docstrings:
84 that the hole be immediately under its binder (use attack if it might
84 that the hole be immediately under its binder (use attack if it might
85 not be).
85 not be).
86
86
87−Here is the command from pruviloj that we will need for the example on
87+Here is the command from ``pruviloj`` that we will need for the example on
88this page:
88this page:
89
89
90.. code-block:: idris
90.. code-block:: idris
@@ -136,11 +136,11 @@ On running , two global names are created, ``plusredZ_Z`` and
136 For details type :warranty.
136 For details type :warranty.
137 Holes: Main.plusredZ_S, Main.plusredZ_Z
137 Holes: Main.plusredZ_S, Main.plusredZ_Z
138
138
139−This tells us that we have two holes Main.plusredZ_S and Main.plusredZ_Z. We can solve
139+This tells us that we have two holes ``Main.plusredZ_S`` and ``Main.plusredZ_Z``. We can solve
140these separately, ``plusredZ_Z`` is the simplest so we will do that first.
140these separately, ``plusredZ_Z`` is the simplest so we will do that first.
141
141
142The ``:elab plusredZ_Z`` command enters interactive elaboration mode, which can be used to
142The ``:elab plusredZ_Z`` command enters interactive elaboration mode, which can be used to
143−complete the missing definition for plusredZ_Z.
143+complete the missing definition for ``plusredZ_Z``.
144
144
145.. code-block:: idris
145.. code-block:: idris
146
146
@@ -150,7 +150,7 @@ complete the missing definition for plusredZ_Z.
150 {hole_0} : 0 = 0
150 {hole_0} : 0 = 0
151
151
152This has been normalised to ``0 = 0`` so now we have to prove that ``0`` equals ``0``, which
152This has been normalised to ``0 = 0`` so now we have to prove that ``0`` equals ``0``, which
153−is easy to prove by reflexivity from the pruviloj library:
153+is easy to prove by ``reflexivity`` from the ``pruviloj`` library:
154
154
155.. code-block:: idris
155.. code-block:: idris
156
156
@@ -190,7 +190,7 @@ accessible by pattern matching) and ``ih`` — the local variable
190containing the result of the recursive call. We can introduce these as
190containing the result of the recursive call. We can introduce these as
191assumptions using the ``intro`` tactic twice. The parameter is entered as
191assumptions using the ``intro`` tactic twice. The parameter is entered as
192a constant of type ``TTName`` which is entered as a backtick with double
192a constant of type ``TTName`` which is entered as a backtick with double
193−braces \`{{ih}}. This gives:
193+braces ```{{ih}}``. This gives:
194
194
195.. code-block:: idris
195.. code-block:: idris
196
196
@@ -223,11 +223,11 @@ like to use this knowledge to replace ``plus k 0`` in the goal with
223 {hole_0} : S k = S k
223 {hole_0} : S k = S k
224
224
225The ``rewriteWith`` tactic takes an equality proof as an argument, and tries
225The ``rewriteWith`` tactic takes an equality proof as an argument, and tries
226−to rewrite the goal using that proof. The ih value is entered as a constant
226+to rewrite the goal using that proof. The ``ih`` value is entered as a constant
227−of type ``TTName`` which is entered as a backtick with double braces `{{ih}} but
227+of type ``TTName`` which is entered as a backtick with double braces ```{{ih}}`` but
228``rewriteWith`` requires an expression of type ``Raw``, rather than just a name,
228``rewriteWith`` requires an expression of type ``Raw``, rather than just a name,
229−so the Var constructor is used to make a variable. Here, it results in an equality
229+so the ``Var`` constructor is used to make a variable. Here, it results in an equality
230−which is trivially provable using reflexivity:
230+which is trivially provable using ``reflexivity``:
231
231
232.. code-block:: idris
232.. code-block:: idris
233
233
docs/proofs/propositional.rst+23−19
@@ -3,17 +3,19 @@ This page attempts to explain some of the techniques used in Idris to prove prop
3Proving Propositional Equality
3Proving Propositional Equality
4==============================
4==============================
5
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.
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
7
8−However with propositional equalities we are using symbolic variables they do not always normalse.
8+However with propositional equalities we are using symbolic variables they do not always normalise.
9
9
10So to take the previous example:
10So to take the previous example:
11
11
12+.. code-block:: idris
13+
12−plusReducesR : (n:Nat) -> plus n Z = n
14+ plusReducesR : (n:Nat) -> plus n Z = n
13
15
14−In this case 'plus n Z' does not normalise to n. Even though both sides are equal we cannot pattern match Refl.
16+In this case ``plus n Z`` does not normalise to ``n``. Even though both sides are equal we cannot pattern match ``Refl``.
15
17
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.
18+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
19
18So here:
20So here:
19
21
@@ -24,19 +26,21 @@ So here:
24 plusReducesR {n = (S k)} = let rec = plus_commutes_Z {n=k} in
26 plusReducesR {n = (S k)} = let rec = plus_commutes_Z {n=k} in
25 rewrite rec in Refl
27 rewrite rec in Refl
26
28
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.
29+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.
28
30
29Replace
31Replace
30=======
32=======
31
33
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:
34+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+
36+.. code-block::
33
37
34 if x=y
38 if x=y
35 then P x = P y
39 then P x = P y
36
40
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
41+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``.
38
42
39−So if n is a natural number variable then P could be something like 2*n + 3.
43+So if ``n`` is a natural number variable then ``P`` could be something like ``2*n + 3``.
40
44
41To use this in our proofs there is the following function in the prelude:
45To use this in our proofs there is the following function in the prelude:
42
46
@@ -46,14 +50,14 @@ To use this in our proofs there is the following function in the prelude:
46 replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
50 replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
47 replace Refl prf = prf
51 replace Refl prf = prf
48
52
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)
53+Removing the implicits, if we supply an equality ``x=y`` and a proof of a property of ``x`` (i.e. ``P x``) then we get a proof of a property of ``y`` (i.e. ``P y``)
50
54
51.. code-block:: idris
55.. code-block:: idris
52
56
53 > :t replace
57 > :t replace
54 replace : (x = y) -> P x -> P y
58 replace : (x = y) -> P x -> P y
55
59
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.
60+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
61
58.. code-block:: idris
62.. code-block:: idris
59
63
@@ -66,16 +70,16 @@ So, in the following example, if we supply p1 x which is a proof that x=2 and th
66Rewrite
70Rewrite
67=======
71=======
68
72
69−Similar to 'replace' above but Idris provides a nicer syntax which makes 'rewrite' easier to use in examples like plusReducesR above.
73+Similar to ``replace`` above but Idris provides a nicer syntax which makes ``rewrite`` easier to use in examples like ``plusReducesR`` above.
70
74
71.. code-block:: idris
75.. code-block:: idris
72
76
73 rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x
77 rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x
74 rewrite__impl p Refl prf = prf
78 rewrite__impl p Refl prf = prf
75
79
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).
80+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
81
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.
82+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
83
80.. code-block:: idris
84.. code-block:: idris
81
85
@@ -87,16 +91,16 @@ Example: again we supply p1 which is a proof that x=2 and the equality x=y then
87
91
88We can think of rewrite doing this:
92We can think of rewrite doing this:
89
93
90− * Start with a equation x=y and a property P: x -> Type
94+ * start with a equation ``x=y`` and a property ``P: x -> Type``;
91− * Searches y in P
95+ * search ``y`` in ``P``;
92− * Replaces all occurrences of y with x in P.
96+ * replace all occurrences of ``y`` with ``x`` in ``P``.
93
97
94That is, we are doing a substitution.
98That is, we are doing a substitution.
95
99
96Symmetry and Transitivity
100Symmetry and Transitivity
97=========================
101=========================
98
102
99−In addition to 'reflexivity' equality also obeys 'symmetry' and 'transitivity' and these are also included in the prelude:
103+In addition to *reflexivity* equality also obeys *symmetry* and *transitivity* and these are also included in the prelude:
100
104
101.. code-block:: idris
105.. code-block:: idris
102
106
@@ -111,7 +115,7 @@ In addition to 'reflexivity' equality also obeys 'symmetry' and 'transitivity' a
111Heterogeneous Equality
115Heterogeneous Equality
112======================
116======================
113
117
114−Also included in the prelude:
118+Also included in the prelude:
115
119
116.. code-block:: idris
120.. code-block:: idris
117
121