git.iko.soy/Idris-dev
on ea745fc help sign in
Idris-dev/docs/proofs/interactive.rst
169 lines 5.3 kB history raw
1***************************************
2DEPRECATED: Interactive Theorem Proving
3***************************************
5.. warning::
6 The interactive theorem-proving interface documented here has been
7 deprecated in favor of :ref:`elaborator-reflection`.
9Idris also supports interactive theorem proving via tactics. This
10is generally not recommended to be used directly, but rather used as a
11mechanism for building proof automation which is beyond the scope of this
12tutorial. In this section, we briefly discus tactics.
14One way to write proofs interactively is to write the general *structure* of
15the proof, and use the interactive mode to complete the details.
16Consider the following definition, proved in :ref:`sect-theorems`:
18.. code-block:: idris
20 plusReduces : (n:Nat) -> plus Z n = n
22We’ll be constructing the proof by *induction*, so we write the cases for ``Z``
23and ``S``, with a recursive call in the ``S`` case giving the inductive
24hypothesis, and insert *holes* for the rest of the definition:
26.. code-block:: idris
28 plusReducesZ' : (n:Nat) -> n = plus n Z
29 plusReducesZ' Z = ?plusredZ_Z
30 plusReducesZ' (S k) = let ih = plusReducesZ' k in
31 ?plusredZ_S
33On running , two global names are created, ``plusredZ_Z`` and
34``plusredZ_S``, with no definition. We can use the ``:m`` command at the
35prompt to find out which holes are still to be solved (or, more
36precisely, which functions exist but have no definitions), then the
37``:t`` command to see their types:
39.. code-block:: idris
41 *theorems> :m
42 Global holes:
43 [plusredZ_S,plusredZ_Z]
45.. code-block:: idris
47 *theorems> :t plusredZ_Z
48 plusredZ_Z : Z = plus Z Z
50 *theorems> :t plusredZ_S
51 plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
53The ``:p`` command enters interactive proof mode, which can be used to
54complete the missing definitions.
56.. code-block:: idris
58 *theorems> :p plusredZ_Z
60 ---------------------------------- (plusredZ_Z) --------
61 {hole0} : Z = plus Z Z
63This gives us a list of premises (above the line; there are none here)
64and the current goal (below the line; named ``{hole0}`` here). At the
65prompt we can enter tactics to direct the construction of the proof. In
66this case, we can normalise the goal with the ``compute`` tactic:
68.. code-block:: idris
70 -plusredZ_Z> compute
72 ---------------------------------- (plusredZ_Z) --------
73 {hole0} : Z = Z
75Now we have to prove that ``Z`` equals ``Z``, which is easy to prove by
76``Refl``. To apply a function, such as ``Refl``, we use ``refine`` which
77introduces subgoals for each of the function’s explicit arguments
78(``Refl`` has none):
80.. code-block:: idris
82 -plusredZ_Z> refine Refl
83 plusredZ_Z: no more goals
85Here, we could also have used the ``trivial`` tactic, which tries to
86refine by ``Refl``, and if that fails, tries to refine by each name in
87the local context. When a proof is complete, we use the ``qed`` tactic
88to add the proof to the global context, and remove the hole from the
89unsolved holes list. This also outputs a trace of the proof:
91.. code-block:: idris
93 -plusredZ_Z> qed
94 plusredZ_Z = proof
95 compute
96 refine Refl
98.. code-block:: idris
100 *theorems> :m
101 Global holes:
102 [plusredZ_S]
104The ``:addproof`` command, at the interactive prompt, will add the proof
105to the source file (effectively in an appendix). Let us now prove the
106other required lemma, ``plusredZ_S``:
108.. code-block:: idris
110 *theorems> :p plusredZ_S
112 ---------------------------------- (plusredZ_S) --------
113 {hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
115In this case, the goal is a function type, using ``k`` (the argument
116accessible by pattern matching) and ``ih`` — the local variable
117containing the result of the recursive call. We can introduce these as
118premises using the ``intro`` tactic twice (or ``intros``, which
119introduces all arguments as premises). This gives:
121.. code-block:: idris
123 k : Nat
124 ih : k = plus k Z
125 ---------------------------------- (plusredZ_S) --------
126 {hole2} : S k = plus (S k) Z
128Since plus is defined by recursion on its first argument, the term
129``plus (S k) Z`` in the goal can be simplified, so we use ``compute``.
131.. code-block:: idris
133 k : Nat
134 ih : k = plus k Z
135 ---------------------------------- (plusredZ_S) --------
136 {hole2} : S k = S (plus k Z)
138We know, from the type of ``ih``, that ``k = plus k Z``, so we would
139like to use this knowledge to replace ``plus k Z`` in the goal with
140``k``. We can achieve this with the ``rewrite`` tactic:
142.. code-block:: idris
144 -plusredZ_S> rewrite ih
146 k : Nat
147 ih : k = plus k Z
148 ---------------------------------- (plusredZ_S) --------
149 {hole3} : S k = S k
151 -plusredZ_S>
153The ``rewrite`` tactic takes an equality proof as an argument, and tries
154to rewrite the goal using that proof. Here, it results in an equality
155which is trivially provable:
157.. code-block:: idris
159 -plusredZ_S> trivial
160 plusredZ_S: no more goals
161 -plusredZ_S> qed
162 plusredZ_S = proof {
163 intros;
164 rewrite ih;
165 trivial;
166 }
168Again, we can add this proof to the end of our source file using the
169``:addproof`` command at the interactive prompt.