8526a9f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #4776 from buzden/fix-proof-docs

Proofs docs were fixed a little

commit8526a9f7df26a4e3e3e09b821ccdc154c4548ffa authorNiklas Larsson <metaniklas@gmail.com> dateTue 19 Nov 2019, 19:09 (7 years ago) parent6539ef4 1d5eb9c

2 files changed+39−35

compare with master

unifiedsplit

docs/proofs/interactive.rst+16−16 docs/proofs/propositional.rst+23−19

docs/proofs/interactive.rst+16−16

@@ -15,15 +15,15 @@ construct proofs as described on this page.

1515Elab and Pruviloj Libraries

1616===========================

1717

18−Elaborator reflection is defined in prelude/Language/Reflection/Elab.idr

19−and pruviloj is defined in Idris-dev/libs/pruviloj/

18+Elaborator reflection is defined in ``prelude/Language/Reflection/Elab.idr``

19+and ``pruviloj`` is defined in ``Idris-dev/libs/pruviloj/``.

2020

21−``Elab`` defines the basics such as: solve, attack, intro, compute,

22−rewriteWith and others.

21+``Elab`` defines the basics such as: ``solve``, ``attack``, ``intro``, ``compute``,

22+``rewriteWith`` and others.

2323``pruviloj`` defines some more advanced derived commands such as:

24−reflexivity and others.

24+``reflexivity`` and others.

2525

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:

2727

2828.. code-block:: idris

2929

@@ -34,7 +34,7 @@ to the top of your file.

3434

3535It is useful to get the docs at the REPL by using the ``:doc`` command, and

3636search 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

3838their docstrings:

3939

4040.. code-block:: idris

@@ -84,7 +84,7 @@ their docstrings:

8484 that the hole be immediately under its binder (use attack if it might

8585 not be).

8686

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

8888this page:

8989

9090.. code-block:: idris

@@ -136,11 +136,11 @@ On running , two global names are created, ``plusredZ_Z`` and

136136 For details type :warranty.

137137 Holes: Main.plusredZ_S, Main.plusredZ_Z

138138

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

140140these separately, ``plusredZ_Z`` is the simplest so we will do that first.

141141

142142The ``: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``.

144144

145145.. code-block:: idris

146146

@@ -150,7 +150,7 @@ complete the missing definition for plusredZ_Z.

150150 {hole_0} : 0 = 0

151151

152152This 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:

154154

155155.. code-block:: idris

156156

@@ -190,7 +190,7 @@ accessible by pattern matching) and ``ih`` — the local variable

190190containing the result of the recursive call. We can introduce these as

191191assumptions using the ``intro`` tactic twice. The parameter is entered as

192192a constant of type ``TTName`` which is entered as a backtick with double

193−braces \`{{ih}}. This gives:

193+braces ```{{ih}}``. This gives:

194194

195195.. code-block:: idris

196196

@@ -223,11 +223,11 @@ like to use this knowledge to replace ``plus k 0`` in the goal with

223223 {hole_0} : S k = S k

224224

225225The ``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

227−of type ``TTName`` which is entered as a backtick with double braces `{{ih}} but

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

228228``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

230−which is trivially provable using reflexivity:

229+so the ``Var`` constructor is used to make a variable. Here, it results in an equality

230+which is trivially provable using ``reflexivity``:

231231

232232.. code-block:: idris

233233

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

33Proving Propositional Equality

44==============================

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.

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.

1010So to take the previous example:

1111

12−plusReducesR : (n:Nat) -> plus n Z = n

12+.. code-block:: idris

13+

14+ plusReducesR : (n:Nat) -> plus n Z = n

1315

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``.

1517

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.

1719

1820So here:

1921

@@ -24,19 +26,21 @@ So here:

2426 plusReducesR {n = (S k)} = let rec = plus_commutes_Z {n=k} in

2527 rewrite rec in Refl

2628

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.

2830

2931Replace

3032=======

3133

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::

3337

3438 if x=y

3539 then P x = P y

3640

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``.

3842

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``.

4044

4145To use this in our proofs there is the following function in the prelude:

4246

@@ -46,14 +50,14 @@ To use this in our proofs there is the following function in the prelude:

4650 replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

4751 replace Refl prf = prf

4852

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``)

5054

5155.. code-block:: idris

5256

5357 > :t replace

5458 replace : (x = y) -> P x -> P y

5559

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``.

5761

5862.. code-block:: idris

5963

@@ -66,16 +70,16 @@ So, in the following example, if we supply p1 x which is a proof that x=2 and th

6670Rewrite

6771=======

6872

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.

7074

7175.. code-block:: idris

7276

7377 rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x

7478 rewrite__impl p Refl prf = prf

7579

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).

7781

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``.

7983

8084.. code-block:: idris

8185

@@ -87,16 +91,16 @@ Example: again we supply p1 which is a proof that x=2 and the equality x=y then

8791

8892We can think of rewrite doing this:

8993

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.

94+ * start with a equation ``x=y`` and a property ``P: x -> Type``;

95+ * search ``y`` in ``P``;

96+ * replace all occurrences of ``y`` with ``x`` in ``P``.

9397

9498That is, we are doing a substitution.

9599

96100Symmetry and Transitivity

97101=========================

98102

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:

100104

101105.. code-block:: idris

102106

@@ -111,7 +115,7 @@ In addition to 'reflexivity' equality also obeys 'symmetry' and 'transitivity' a

111115Heterogeneous Equality

112116======================

113117

114−Also included in the prelude:

118+Also included in the prelude:

115119

116120.. code-block:: idris

117121