@@ -120,163 +120,7 @@ mode’.
121Idris provides interactive editing capabilities, which can help with
121Idris provides interactive editing capabilities, which can help with
122building proofs. For more details on building proofs interactively in
122building proofs. For more details on building proofs interactively in
123−an editor, see :ref:`proofs-index`. In the rest of this section, we discuss
123+an editor, see :ref:`proofs-index`.
124−Idris's interactive proof mode.
126−Interactive theorem proving
127−---------------------------
129−Instead of writing the proof in one go, we can use Idris’s interactive proof
130−mode. To do this, we write the general *structure* of the proof, and use
131−the interactive mode to complete the details. We’ll be constructing the
132−proof by *induction*, so we write the cases for ``Z`` and ``S``, with a
133−recursive call in the ``S`` case giving the inductive hypothesis, and
134−insert *metavariables* for the rest of the definition:
136−.. code-block:: idris
138− plusReducesZ' : (n:Nat) -> n = plus n Z
139− plusReducesZ' Z = ?plusredZ_Z
140− plusReducesZ' (S k) = let ih = plusReducesZ' k in
143−On running , two global names are created, ``plusredZ_Z`` and
144−``plusredZ_S``, with no definition. We can use the ``:m`` command at the
145−prompt to find out which metavariables are still to be solved (or, more
146−precisely, which functions exist but have no definitions), then the
147−``:t`` command to see their types:
149−.. code-block:: idris
152− Global metavariables:
153− [plusredZ_S,plusredZ_Z]
155−.. code-block:: idris
157− *theorems> :t plusredZ_Z
158− plusredZ_Z : Z = plus Z Z
160− *theorems> :t plusredZ_S
161− plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
163−The ``:p`` command enters interactive proof mode, which can be used to
164−complete the missing definitions.
166−.. code-block:: idris
168− *theorems> :p plusredZ_Z
170− ---------------------------------- (plusredZ_Z) --------
171− {hole0} : Z = plus Z Z
173−This gives us a list of premises (above the line; there are none here)
174−and the current goal (below the line; named ``{hole0}`` here). At the
175−prompt we can enter tactics to direct the construction of the proof. In
176−this case, we can normalise the goal with the ``compute`` tactic:
178−.. code-block:: idris
180− -plusredZ_Z> compute
182− ---------------------------------- (plusredZ_Z) --------
185−Now we have to prove that ``Z`` equals ``Z``, which is easy to prove by
186−``Refl``. To apply a function, such as ``Refl``, we use ``refine`` which
187−introduces subgoals for each of the function’s explicit arguments
190−.. code-block:: idris
192− -plusredZ_Z> refine Refl
193− plusredZ_Z: no more goals
195−Here, we could also have used the ``trivial`` tactic, which tries to
196−refine by ``Refl``, and if that fails, tries to refine by each name in
197−the local context. When a proof is complete, we use the ``qed`` tactic
198−to add the proof to the global context, and remove the metavariable from
199−the unsolved metavariables list. This also outputs a trace of the proof:
201−.. code-block:: idris
208−.. code-block:: idris
211− Global metavariables:
214−The ``:addproof`` command, at the interactive prompt, will add the proof
215−to the source file (effectively in an appendix). Let us now prove the
216−other required lemma, ``plusredZ_S``:
218−.. code-block:: idris
220− *theorems> :p plusredZ_S
222− ---------------------------------- (plusredZ_S) --------
223− {hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
225−In this case, the goal is a function type, using ``k`` (the argument
226−accessible by pattern matching) and ``ih`` — the local variable
227−containing the result of the recursive call. We can introduce these as
228−premisses using the ``intro`` tactic twice (or ``intros``, which
229−introduces all arguments as premisses). This gives:
231−.. code-block:: idris
235− ---------------------------------- (plusredZ_S) --------
236− {hole2} : S k = plus (S k) Z
238−Since plus is defined by recursion on its first argument, the term
239−``plus (S k) Z`` in the goal can be simplified, so we use ``compute``.
241−.. code-block:: idris
245− ---------------------------------- (plusredZ_S) --------
246− {hole2} : S k = S (plus k Z)
248−We know, from the type of ``ih``, that ``k = plus k Z``, so we would
249−like to use this knowledge to replace ``plus k Z`` in the goal with
250−``k``. We can achieve this with the ``rewrite`` tactic:
252−.. code-block:: idris
254− -plusredZ_S> rewrite ih
258− ---------------------------------- (plusredZ_S) --------
263−The ``rewrite`` tactic takes an equality proof as an argument, and tries
264−to rewrite the goal using that proof. Here, it results in an equality
265−which is trivially provable:
267−.. code-block:: idris
269− -plusredZ_S> trivial
270− plusredZ_S: no more goals
272− plusredZ_S = proof {
278−Again, we can add this proof to the end of our source file using the
279−``:addproof`` command at the interactive prompt.
281.. _sect-totality:
125.. _sect-totality: