@@ -120,163 +120,7 @@ mode’.
120120
121121Idris provides interactive editing capabilities, which can help with
122122building proofs. For more details on building proofs interactively in
123−an editor, see :ref:`proofs-index`. In the rest of this section, we discuss
124−Idris's interactive proof mode.
125−
126−Interactive theorem proving
127−---------------------------
128−
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:
135−
136−.. code-block:: idris
137−
138− plusReducesZ' : (n:Nat) -> n = plus n Z
139− plusReducesZ' Z = ?plusredZ_Z
140− plusReducesZ' (S k) = let ih = plusReducesZ' k in
141− ?plusredZ_S
142−
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:
148−
149−.. code-block:: idris
150−
151− *theorems> :m
152− Global metavariables:
153− [plusredZ_S,plusredZ_Z]
154−
155−.. code-block:: idris
156−
157− *theorems> :t plusredZ_Z
158− plusredZ_Z : Z = plus Z Z
159−
160− *theorems> :t plusredZ_S
161− plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
162−
163−The ``:p`` command enters interactive proof mode, which can be used to
164−complete the missing definitions.
165−
166−.. code-block:: idris
167−
168− *theorems> :p plusredZ_Z
169−
170− ---------------------------------- (plusredZ_Z) --------
171− {hole0} : Z = plus Z Z
172−
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:
177−
178−.. code-block:: idris
179−
180− -plusredZ_Z> compute
181−
182− ---------------------------------- (plusredZ_Z) --------
183− {hole0} : Z = Z
184−
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
188−(``Refl`` has none):
189−
190−.. code-block:: idris
191−
192− -plusredZ_Z> refine Refl
193− plusredZ_Z: no more goals
194−
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:
200−
201−.. code-block:: idris
202−
203− -plusredZ_Z> qed
204− plusredZ_Z = proof
205− compute
206− refine Refl
207−
208−.. code-block:: idris
209−
210− *theorems> :m
211− Global metavariables:
212− [plusredZ_S]
213−
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``:
217−
218−.. code-block:: idris
219−
220− *theorems> :p plusredZ_S
221−
222− ---------------------------------- (plusredZ_S) --------
223− {hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
224−
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:
230−
231−.. code-block:: idris
232−
233− k : Nat
234− ih : k = plus k Z
235− ---------------------------------- (plusredZ_S) --------
236− {hole2} : S k = plus (S k) Z
237−
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``.
240−
241−.. code-block:: idris
242−
243− k : Nat
244− ih : k = plus k Z
245− ---------------------------------- (plusredZ_S) --------
246− {hole2} : S k = S (plus k Z)
247−
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:
251−
252−.. code-block:: idris
253−
254− -plusredZ_S> rewrite ih
255−
256− k : Nat
257− ih : k = plus k Z
258− ---------------------------------- (plusredZ_S) --------
259− {hole3} : S k = S k
260−
261− -plusredZ_S>
262−
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:
266−
267−.. code-block:: idris
268−
269− -plusredZ_S> trivial
270− plusredZ_S: no more goals
271− -plusredZ_S> qed
272− plusredZ_S = proof {
273− intros;
274− rewrite ih;
275− trivial;
276− }
277−
278−Again, we can add this proof to the end of our source file using the
279−``:addproof`` command at the interactive prompt.
123+an editor, see :ref:`proofs-index`.
280124
281125.. _sect-totality:
282126