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

Proofs docs were fixed a little

Author: melted

docs/proofs/interactive.rst

@@ -15,15 +15,15 @@ construct proofs as described on this page.
 Elab and Pruviloj Libraries
 ===========================
 
-Elaborator reflection is defined in prelude/Language/Reflection/Elab.idr
-and pruviloj is defined in Idris-dev/libs/pruviloj/
+Elaborator reflection is defined in ``prelude/Language/Reflection/Elab.idr``
+and ``pruviloj`` is defined in ``Idris-dev/libs/pruviloj/``.
 
-``Elab`` defines the basics such as: solve, attack, intro, compute,
-rewriteWith and others.
+``Elab`` defines the basics such as: ``solve``, ``attack``, ``intro``, ``compute``,
+``rewriteWith`` and others.
 ``pruviloj`` defines some more advanced derived commands such as:
-reflexivity and others.
+``reflexivity`` and others.
 
-To use ``pruviloj`` call Idris with the "-p pruviloj" option and add:
+To use ``pruviloj`` call Idris with the ``-p pruviloj`` option and add:
 
 .. code-block:: idris
 
@@ -34,7 +34,7 @@ to the top of your file.
 
 It is useful to get the docs at the REPL by using the ``:doc`` command, and
 search the docstrings using ``:apropos``. So to introduce the functions from
-Elab and Pruviloj, that we will need for the following example, here are
+``Elab`` and ``Pruviloj``, that we will need for the following example, here are
 their docstrings:
 
 .. code-block:: idris
@@ -84,7 +84,7 @@ their docstrings:
         that the hole be immediately under its binder (use attack if it might
         not be).
 
-Here is the command from pruviloj that we will need for the example on
+Here is the command from ``pruviloj`` that we will need for the example on
 this page:
 
 .. code-block:: idris
@@ -136,11 +136,11 @@ On running , two global names are created, ``plusredZ_Z`` and
     For details type :warranty.
     Holes: Main.plusredZ_S, Main.plusredZ_Z
 
-This tells us that we have two holes Main.plusredZ_S and Main.plusredZ_Z. We can solve
+This tells us that we have two holes ``Main.plusredZ_S`` and ``Main.plusredZ_Z``. We can solve
 these separately, ``plusredZ_Z`` is the simplest so we will do that first.
 
 The ``:elab plusredZ_Z`` command enters interactive elaboration mode, which can be used to
-complete the missing definition for plusredZ_Z.
+complete the missing definition for ``plusredZ_Z``.
 
 .. code-block:: idris
 
@@ -150,7 +150,7 @@ complete the missing definition for plusredZ_Z.
     {hole_0} : 0 = 0
 
 This has been normalised to ``0 = 0`` so now we have to prove that ``0`` equals ``0``, which
-is easy to prove by reflexivity from the pruviloj library:
+is easy to prove by ``reflexivity`` from the ``pruviloj`` library:
 
 .. code-block:: idris
 
@@ -190,7 +190,7 @@ accessible by pattern matching) and ``ih`` — the local variable
 containing the result of the recursive call. We can introduce these as
 assumptions using the ``intro`` tactic twice. The parameter is entered as
 a constant of type ``TTName`` which is entered as a backtick with double
-braces \`{{ih}}. This gives:
+braces ```{{ih}}``. This gives:
 
 .. code-block:: idris
 
@@ -223,11 +223,11 @@ like to use this knowledge to replace ``plus k 0`` in the goal with
     {hole_0} : S k = S k
 
 The ``rewriteWith`` tactic takes an equality proof as an argument, and tries
-to rewrite the goal using that proof. The ih value is entered as a constant
-of type ``TTName`` which is entered as a backtick with double braces `{{ih}} but
+to rewrite the goal using that proof. The ``ih`` value is entered as a constant
+of type ``TTName`` which is entered as a backtick with double braces ```{{ih}}`` but
 ``rewriteWith`` requires an expression of type ``Raw``, rather than just a name,
-so the Var constructor is used to make a variable. Here, it results in an equality
-which is trivially provable using reflexivity:
+so the ``Var`` constructor is used to make a variable. Here, it results in an equality
+which is trivially provable using ``reflexivity``:
 
 .. code-block:: idris
 

docs/proofs/propositional.rst

@@ -3,17 +3,19 @@ This page attempts to explain some of the techniques used in Idris to prove prop
 Proving Propositional Equality
 ==============================
 
-We have seen that definitional equalities can be proved using Refl since they always normalise to unique values that can be compared directly.
+We have seen that definitional equalities can be proved using ``Refl`` since they always normalise to unique values that can be compared directly.
 
-However with propositional equalities we are using symbolic variables they do not always normalse.
+However with propositional equalities we are using symbolic variables they do not always normalise.
 
 So to take the previous example:
 
-plusReducesR : (n:Nat) -> plus n Z = n
+.. code-block:: idris
+
+   plusReducesR : (n:Nat) -> plus n Z = n
 
-In this case 'plus n Z' does not normalise to n. Even though both sides are equal we cannot pattern match Refl.
+In this case ``plus n Z`` does not normalise to ``n``. Even though both sides are equal we cannot pattern match ``Refl``.
 
-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.
+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.
 
 So here:
 
@@ -24,19 +26,21 @@ So here:
    plusReducesR {n = (S k)} = let rec = plus_commutes_Z {n=k} in
                                   rewrite rec in Refl
 
-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.
+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.
 
 Replace
 =======
 
-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:
+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:
+
+.. code-block::
 
    if x=y
    then P x = P y
 
-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
+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``.
 
-So if n is a natural number variable then P could be something like 2*n + 3.
+So if ``n`` is a natural number variable then ``P`` could be something like ``2*n + 3``.
 
 To use this in our proofs there is the following function in the prelude:
 
@@ -46,14 +50,14 @@ To use this in our proofs there is the following function in the prelude:
    replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
    replace Refl prf = prf
 
-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)
+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``)
 
 .. code-block:: idris
 
    > :t replace
    replace : (x = y) -> P x -> P y
 
-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.
+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``.
 
 .. code-block:: idris
 
@@ -66,16 +70,16 @@ So, in the following example, if we supply p1 x which is a proof that x=2 and th
 Rewrite
 =======
 
-Similar to 'replace' above but Idris provides a nicer syntax which makes 'rewrite' easier to use in examples like plusReducesR above.
+Similar to ``replace`` above but Idris provides a nicer syntax which makes ``rewrite`` easier to use in examples like ``plusReducesR`` above.
 
 .. code-block:: idris
 
    rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x
    rewrite__impl p Refl prf = prf
 
-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).
+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).
 
-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.
+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``.
 
 .. code-block:: idris
 
@@ -87,16 +91,16 @@ Example: again we supply p1 which is a proof that x=2 and the equality x=y then
 
 We can think of rewrite doing this:
 
- * Start with a equation x=y and a property P: x -> Type
- * Searches y in P
- * Replaces all occurrences of y with x in P.
+ * start with a equation ``x=y`` and a property ``P: x -> Type``;
+ * search ``y`` in ``P``;
+ * replace all occurrences of ``y`` with ``x`` in ``P``.
 
 That is, we are doing a substitution.
 
 Symmetry and Transitivity
 =========================
 
-In addition to 'reflexivity' equality also obeys 'symmetry' and 'transitivity' and these are also included in the prelude:
+In addition to *reflexivity* equality also obeys *symmetry* and *transitivity* and these are also included in the prelude:
 
 .. code-block:: idris
 
@@ -111,7 +115,7 @@ In addition to 'reflexivity' equality also obeys 'symmetry' and 'transitivity' a
 Heterogeneous Equality
 ======================
 
-Also included in the prelude: 
+Also included in the prelude:
 
 .. code-block:: idris