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