@@ -1,15 +1,102 @@
1−***************************************
2−DEPRECATED: Interactive Theorem Proving
3−***************************************
1+***************************
2+Interactive Theorem Proving
3+***************************
44
5−.. warning::
6− The interactive theorem-proving interface documented here has been
7− deprecated in favor of :ref:`elaborator-reflection`.
5+Idris supports interactive theorem proving via elaborator reflection.
86
9−Idris also supports interactive theorem proving via tactics. This
10−is generally not recommended to be used directly, but rather used as a
11−mechanism for building proof automation which is beyond the scope of this
12−tutorial. In this section, we briefly discus tactics.
7+:ref:'elaborator-reflection' is also used to convert high-level Idris code into
8+the core language and for customising the language. Here we show how to use it
9+to interactively construct proofs.
10+
11+The primary purpose of the elaboration mechanism is to elaborate Idris and so it
12+is not optimised to work as a proof assistant, however it can interactively
13+construct proofs as described on this page.
14+
15+Elab and Pruviloj Libraries
16+===========================
17+
18+Elaborator reflection is defined in prelude/Language/Reflection/Elab.idr
19+and pruviloj is defined in Idris-dev/libs/pruviloj/
20+
21+``Elab`` defines the basics such as: solve, attack, intro, compute,
22+rewriteWith and others.
23+``pruviloj`` defines some more advanced derived commands such as:
24+reflexivity and others.
25+
26+To use ``pruviloj`` call Idris with the "-p pruviloj" option and add:
27+
28+.. code-block:: idris
29+
30+ import Pruviloj
31+ import Pruviloj.Induction
32+
33+to the top of your file.
34+
35+It is useful to get the docs at the REPL by using the ``:doc`` command, and
36+search the docstrings using ``:apropos``. So to introduce the functions from
37+Elab and Pruviloj, that we will need for the following example, here are
38+their docstrings:
39+
40+.. code-block:: idris
41+
42+ *plusReducesZ> :doc solve
43+ Language.Reflection.Elab.Tactics.solve : Elab ()
44+ Substitute a guess into a hole.
45+
46+.. code-block:: idris
47+
48+ *plusReducesZ> :doc attack
49+ Language.Reflection.Elab.Tactics.attack : Elab ()
50+ Convert a hole to make it suitable for bindings - that is, transform
51+ it such that it has the form ?h : t . h as opposed to ?h : t . f h.
52+
53+ The binding tactics require that a hole be directly under its binding,
54+ or else the scopes of the generated terms won't make sense. This
55+ tactic creates a new hole of the proper form, and points the old hole
56+ at it.
57+
58+.. code-block:: idris
59+
60+ *plusReducesZ> :doc intro
61+ Language.Reflection.Elab.Tactics.intro : (n : TTName) -> Elab ()
62+ Introduce a lambda binding around the current hole and focus on the
63+ body. Requires that the hole be in binding form (use attack).
64+ Arguments:
65+ n : TTName -- the name to use for the argument
66+
67+.. code-block:: idris
68+
69+ *plusReducesZ> :doc compute
70+ Language.Reflection.Elab.Tactics.compute : Elab ()
71+ Normalise the goal.
72+
73+.. code-block:: idris
74+
75+ *plusReducesZ> :doc rewriteWith
76+ Language.Reflection.Elab.Tactics.rewriteWith : Raw -> Elab ()
77+ Attempt to rewrite the goal using an equality.
78+
79+ The tactic searches the goal for applicable subterms, and constructs a
80+ context for replace using them. In some cases, this is not possible,
81+ and replace must be called manually with an appropriate context.
82+
83+ Because this tactic internally introduces a let binding, it requires
84+ that the hole be immediately under its binder (use attack if it might
85+ not be).
86+
87+Here is the command from pruviloj that we will need for the example on
88+this page:
89+
90+.. code-block:: idris
91+
92+ *plusReducesZ> :doc reflexivity
93+ Pruviloj.Core.reflexivity : Elab ()
94+ A special-purpose tactic that attempts to solve a goal using Refl.
95+ This is useful for ensuring that goals in fact are trivial when
96+ developing or testing other tactics; otherwise, consider using search.
97+
98+Interactive Example: plusReduces
99+================================
13100
14101One way to write proofs interactively is to write the general *structure* of
15102the proof, and use the interactive mode to complete the details.
@@ -25,145 +112,134 @@ hypothesis, and insert *holes* for the rest of the definition:
25112
26113.. code-block:: idris
27114
115+ import Pruviloj
116+ import Pruviloj.Induction
117+
28118 plusReducesZ' : (n:Nat) -> n = plus n Z
29119 plusReducesZ' Z = ?plusredZ_Z
30120 plusReducesZ' (S k) = let ih = plusReducesZ' k in
31121 ?plusredZ_S
32122
33123On running , two global names are created, ``plusredZ_Z`` and
34−``plusredZ_S``, with no definition. We can use the ``:m`` command at the
35−prompt to find out which holes are still to be solved (or, more
36−precisely, which functions exist but have no definitions), then the
37−``:t`` command to see their types:
124+``plusredZ_S``, with no definition.
38125
39126.. code-block:: idris
40127
41− *theorems> :m
42− Global holes:
43− [plusredZ_S,plusredZ_Z]
128+ *theorems> : idris plusReducesZ.idr -p pruviloj
44129
45−.. code-block:: idris
130+ . / _/___/ /____(_)____
131+ / // __ / ___/ / ___/ Version 1.2.0
132+ _/ // /_/ / / / (__ ) http://www.idris-lang.org/
133+ /___/\__,_/_/ /_/____/ Type :? for help
46134
47− *theorems> :t plusredZ_Z
48− plusredZ_Z : Z = plus Z Z
135+ Idris is free software with ABSOLUTELY NO WARRANTY.
136+ For details type :warranty.
137+ Holes: Main.plusredZ_S, Main.plusredZ_Z
49138
50− *theorems> :t plusredZ_S
51− plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
139+This tells us that we have two holes Main.plusredZ_S and Main.plusredZ_Z. We can solve
140+these separately, ``plusredZ_Z`` is the simplest so we will do that first.
52141
53−The ``:p`` command enters interactive proof mode, which can be used to
54−complete the missing definitions.
142+The ``:elab plusredZ_Z`` command enters interactive elaboration mode, which can be used to
143+complete the missing definition for plusredZ_Z.
55144
56145.. code-block:: idris
57146
58− *theorems> :p plusredZ_Z
147+ *plusReducesZ> :elab plusredZ_Z
59148
60− ---------------------------------- (plusredZ_Z) --------
61− {hole0} : Z = plus Z Z
149+ ---------- Goal: ----------
150+ {hole_0} : 0 = 0
62151
63−This gives us a list of premises (above the line; there are none here)
64−and the current goal (below the line; named ``{hole0}`` here). At the
65−prompt we can enter tactics to direct the construction of the proof. In
66−this case, we can normalise the goal with the ``compute`` tactic:
152+This has been normalised to ``0 = 0`` so now we have to prove that ``0`` equals ``0``, which
153+is easy to prove by reflexivity from the pruviloj library:
67154
68155.. code-block:: idris
156+ -Main.plusredZ_Z> reflexivity
157+ plusredZ_Z: No more goals.
69158
70− -plusredZ_Z> compute
71−
72− ---------------------------------- (plusredZ_Z) --------
73− {hole0} : Z = Z
74−
75−Now 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
77−introduces subgoals for each of the function’s explicit arguments
78−(``Refl`` has none):
159+This tells us that the proof is complete. We can now leave the interactive mode which
160+we entered with the ``:elab`` command. We do this with the ``:qed`` command:
79161
80162.. code-block:: idris
81163
82− -plusredZ_Z> refine Refl
83− plusredZ_Z: no more goals
84−
85−Here, we could also have used the ``trivial`` tactic, which tries to
86−refine by ``Refl``, and if that fails, tries to refine by each name in
87−the local context. When a proof is complete, we use the ``qed`` tactic
88−to add the proof to the global context, and remove the hole from the
89−unsolved holes list. This also outputs a trace of the proof:
164+ -Main.plusredZ_Z> :qed
165+ Proof completed!
166+ Main.plusredZ_Z = %runElab (do reflexivity)
167+ Holes: Main.plusredZ_S
90168
91−.. code-block:: idris
92−
93− -plusredZ_Z> qed
94− plusredZ_Z = proof
95− compute
96− refine Refl
169+This gives us a trace of the proof which is ``plusredZ_Z = %runElab (do reflexivity)``. We
170+can cut & paste this into the hole in the original file. This also tells us that we
171+have another hole ``Main.plusredZ_S`` remaining.
97172
98−.. code-block:: idris
173+This remaining proof is bit more complicated, the following diagram gives an overview:
99174
100− *theorems> :m
101− Global holes:
102− [plusredZ_S]
175+|image|
103176
104−The ``:addproof`` command, at the interactive prompt, will add the proof
105−to the source file (effectively in an appendix). Let us now prove the
106−other required lemma, ``plusredZ_S``:
177+We approach this remaining proof in the same way by using the ``:elab`` command:
107178
108179.. code-block:: idris
109180
110− *theorems> :p plusredZ_S
181+ *plusReducesZ> :elab plusredZ_S
111182
112− ---------------------------------- (plusredZ_S) --------
113− {hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
183+
184+ ---------- Goal: ----------
185+ {hole_0} : (k : Nat) -> (k = plus k 0) -> S k = S (plus k 0)
114186
115187In this case, the goal is a function type, using ``k`` (the argument
116188accessible by pattern matching) and ``ih`` — the local variable
117189containing the result of the recursive call. We can introduce these as
118−premises using the ``intro`` tactic twice (or ``intros``, which
119−introduces all arguments as premises). This gives:
190+assumptions using the ``intro`` tactic twice. The parameter is entered as
191+a constant of type ``TTName`` which is entered as a backtick with double
192+braces `{{ih}}. This gives:
120193
121194.. code-block:: idris
122195
123− k : Nat
124− ih : k = plus k Z
125− ---------------------------------- (plusredZ_S) --------
126− {hole2} : S k = plus (S k) Z
127−
128−Since 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``.
196+ -Main.plusredZ_S> intro `{{k}}
130197
131−.. code-block:: idris
198+ ---------- Assumptions: ----------
199+ k : Nat
200+ ---------- Goal: ----------
201+ {hole_0} : (k = plus k 0) -> S k = S (plus k 0)
202+ -Main.plusredZ_S> intro `{{ih}}
132203
133− k : Nat
134− ih : k = plus k Z
135− ---------------------------------- (plusredZ_S) --------
136− {hole2} : S k = S (plus k Z)
204+ ---------- Assumptions: ----------
205+ k : Nat
206+ ih : k = plus k 0
207+ ---------- Goal: ----------
208+ {hole_0} : S k = S (plus k 0)
137209
138−We know, from the type of ``ih``, that ``k = plus k Z``, so we would
139−like to use this knowledge to replace ``plus k Z`` in the goal with
140−``k``. We can achieve this with the ``rewrite`` tactic:
210+We know, from the type of ``ih``, that ``k = plus k 0``, so we would
211+like to use this knowledge to replace ``plus k 0`` in the goal with
212+``k``. We can achieve this with the ``rewriteWith`` tactic:
141213
142214.. code-block:: idris
143215
144− -plusredZ_S> rewrite ih
216+ -Main.plusredZ_S> rewriteWith (Var `{{ih}})
145217
146− k : Nat
147− ih : k = plus k Z
148− ---------------------------------- (plusredZ_S) --------
149− {hole3} : S k = S k
218+ ---------- Assumptions: ----------
219+ k : Nat
220+ ih : k = plus k 0
221+ ---------- Goal: ----------
222+ {hole_0} : S k = S k
150223
151− -plusredZ_S>
152−
153−The ``rewrite`` tactic takes an equality proof as an argument, and tries
154−to rewrite the goal using that proof. Here, it results in an equality
155−which is trivially provable:
224+The ``rewriteWith`` tactic takes an equality proof as an argument, and tries
225+to rewrite the goal using that proof. The ih value is entered as a constant
226+of type ``TTName`` which is entered as a backtick with double braces `{{ih}} but
227+``rewriteWith`` requires an expression of type ``Raw``, rather than just a name,
228+so the Var constructor is used to make a variable. Here, it results in an equality
229+which is trivially provable using reflexivity:
156230
157231.. code-block:: idris
158232
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− }
233+ -Main.plusredZ_S> reflexivity
234+ plusredZ_S: No more goals.
235+ -Main.plusredZ_S> :qed
236+ Proof completed!
237+ Main.plusredZ_S = %runElab (do intro `{{k}}
238+ intro `{{ih}}
239+ compute
240+ rewriteWith (Var `{{ih}})
241+ reflexivity)
242+
243+Again, we can cut & paste this into the hole in the original file.
167244
168−Again, we can add this proof to the end of our source file using the
169−``:addproof`` command at the interactive prompt.
245+.. |image| image:: ../image/plusReducesProof.png