@@ -1,15 +1,102 @@
1−***************************************
1+***************************
2−DEPRECATED: Interactive Theorem Proving
2+Interactive Theorem Proving
3−***************************************
3+***************************
6− The interactive theorem-proving interface documented here has been
5+Idris supports interactive theorem proving via elaborator reflection.
7− deprecated in favor of :ref:`elaborator-reflection`.
9−Idris also supports interactive theorem proving via tactics. This
7+:ref:'elaborator-reflection' is also used to convert high-level Idris code into
10−is generally not recommended to be used directly, but rather used as a
8+the core language and for customising the language. Here we show how to use it
11−mechanism for building proof automation which is beyond the scope of this
9+to interactively construct proofs.
12−tutorial. In this section, we briefly discus tactics.
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.
15+Elab and Pruviloj Libraries
16+===========================
18+Elaborator reflection is defined in prelude/Language/Reflection/Elab.idr
19+and pruviloj is defined in Idris-dev/libs/pruviloj/
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.
26+To use ``pruviloj`` call Idris with the "-p pruviloj" option and add:
31+ import Pruviloj.Induction
33+to the top of your file.
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
42+ *plusReducesZ> :doc solve
43+ Language.Reflection.Elab.Tactics.solve : Elab ()
44+ Substitute a guess into a hole.
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.
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
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).
65+ n : TTName -- the name to use for the argument
69+ *plusReducesZ> :doc compute
70+ Language.Reflection.Elab.Tactics.compute : Elab ()
75+ *plusReducesZ> :doc rewriteWith
76+ Language.Reflection.Elab.Tactics.rewriteWith : Raw -> Elab ()
77+ Attempt to rewrite the goal using an equality.
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.
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
87+Here is the command from pruviloj that we will need for the example on
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.
98+Interactive Example: plusReduces
99+================================
14One way to write proofs interactively is to write the general *structure* of
101One way to write proofs interactively is to write the general *structure* of
15the proof, and use the interactive mode to complete the details.
102the proof, and use the interactive mode to complete the details.
@@ -25,145 +112,134 @@ hypothesis, and insert *holes* for the rest of the definition:
26.. code-block:: idris
113.. code-block:: idris
116+ import Pruviloj.Induction
28 plusReducesZ' : (n:Nat) -> n = plus n Z
118 plusReducesZ' : (n:Nat) -> n = plus n Z
29 plusReducesZ' Z = ?plusredZ_Z
119 plusReducesZ' Z = ?plusredZ_Z
30 plusReducesZ' (S k) = let ih = plusReducesZ' k in
120 plusReducesZ' (S k) = let ih = plusReducesZ' k in
31 ?plusredZ_S
121 ?plusredZ_S
33On running , two global names are created, ``plusredZ_Z`` and
123On running , two global names are created, ``plusredZ_Z`` and
34−``plusredZ_S``, with no definition. We can use the ``:m`` command at the
124+``plusredZ_S``, with no definition.
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:
39.. code-block:: idris
126.. code-block:: idris
41− *theorems> :m
128+ *theorems> : idris plusReducesZ.idr -p pruviloj
43− [plusredZ_S,plusredZ_Z]
45−.. code-block:: idris
130+ . / _/___/ /____(_)____
131+ / // __ / ___/ / ___/ Version 1.2.0
132+ _/ // /_/ / / / (__ ) http://www.idris-lang.org/
133+ /___/\__,_/_/ /_/____/ Type :? for help
47− *theorems> :t plusredZ_Z
135+ Idris is free software with ABSOLUTELY NO WARRANTY.
48− plusredZ_Z : Z = plus Z Z
136+ For details type :warranty.
137+ Holes: Main.plusredZ_S, Main.plusredZ_Z
50− *theorems> :t plusredZ_S
139+This tells us that we have two holes Main.plusredZ_S and Main.plusredZ_Z. We can solve
51− plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
140+these separately, ``plusredZ_Z`` is the simplest so we will do that first.
53−The ``:p`` command enters interactive proof mode, which can be used to
142+The ``:elab plusredZ_Z`` command enters interactive elaboration mode, which can be used to
54−complete the missing definitions.
143+complete the missing definition for plusredZ_Z.
56.. code-block:: idris
145.. code-block:: idris
58− *theorems> :p plusredZ_Z
147+ *plusReducesZ> :elab plusredZ_Z
60− ---------------------------------- (plusredZ_Z) --------
149+ ---------- Goal: ----------
61− {hole0} : Z = plus Z Z
150+ {hole_0} : 0 = 0
63−This gives us a list of premises (above the line; there are none here)
152+This has been normalised to ``0 = 0`` so now we have to prove that ``0`` equals ``0``, which
64−and the current goal (below the line; named ``{hole0}`` here). At the
153+is easy to prove by reflexivity from the pruviloj library:
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:
68.. code-block:: idris
155.. code-block:: idris
156+ -Main.plusredZ_Z> reflexivity
157+ plusredZ_Z: No more goals.
70− -plusredZ_Z> compute
159+This tells us that the proof is complete. We can now leave the interactive mode which
71−
160+we entered with the ``:elab`` command. We do this with the ``:qed`` command:
72− ---------------------------------- (plusredZ_Z) --------
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
80.. code-block:: idris
162.. code-block:: idris
82− -plusredZ_Z> refine Refl
164+ -Main.plusredZ_Z> :qed
83− plusredZ_Z: no more goals
165+ Proof completed!
84−
166+ Main.plusredZ_Z = %runElab (do reflexivity)
85−Here, we could also have used the ``trivial`` tactic, which tries to
167+ Holes: Main.plusredZ_S
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:
91−.. code-block:: idris
169+This gives us a trace of the proof which is ``plusredZ_Z = %runElab (do reflexivity)``. We
92−
170+can cut & paste this into the hole in the original file. This also tells us that we
93− -plusredZ_Z> qed
171+have another hole ``Main.plusredZ_S`` remaining.
98−.. code-block:: idris
173+This remaining proof is bit more complicated, the following diagram gives an overview:
100− *theorems> :m
175+|image|
104−The ``:addproof`` command, at the interactive prompt, will add the proof
177+We approach this remaining proof in the same way by using the ``:elab`` command:
105−to the source file (effectively in an appendix). Let us now prove the
106−other required lemma, ``plusredZ_S``:
108.. code-block:: idris
179.. code-block:: idris
110− *theorems> :p plusredZ_S
181+ *plusReducesZ> :elab plusredZ_S
112− ---------------------------------- (plusredZ_S) --------
183+
184+ ---------- Goal: ----------
113− {hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
185+ {hole_0} : (k : Nat) -> (k = plus k 0) -> S k = S (plus k 0)
115In this case, the goal is a function type, using ``k`` (the argument
187In this case, the goal is a function type, using ``k`` (the argument
116accessible by pattern matching) and ``ih`` — the local variable
188accessible by pattern matching) and ``ih`` — the local variable
117containing the result of the recursive call. We can introduce these as
189containing the result of the recursive call. We can introduce these as
118−premises using the ``intro`` tactic twice (or ``intros``, which
190+assumptions using the ``intro`` tactic twice. The parameter is entered as
119−introduces all arguments as premises). This gives:
191+a constant of type ``TTName`` which is entered as a backtick with double
192+braces `{{ih}}. This gives:
121.. code-block:: idris
194.. code-block:: idris
123− k : Nat
196+ -Main.plusredZ_S> intro `{{k}}
125− ---------------------------------- (plusredZ_S) --------
126− {hole2} : S k = plus (S k) Z
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``.
131−.. code-block:: idris
198+ ---------- Assumptions: ----------
200+ ---------- Goal: ----------
201+ {hole_0} : (k = plus k 0) -> S k = S (plus k 0)
202+ -Main.plusredZ_S> intro `{{ih}}
204+ ---------- Assumptions: ----------
134− ih : k = plus k Z
206+ ih : k = plus k 0
135− ---------------------------------- (plusredZ_S) --------
207+ ---------- Goal: ----------
136− {hole2} : S k = S (plus k Z)
208+ {hole_0} : S k = S (plus k 0)
138−We know, from the type of ``ih``, that ``k = plus k Z``, so we would
210+We know, from the type of ``ih``, that ``k = plus k 0``, so we would
139−like to use this knowledge to replace ``plus k Z`` in the goal with
211+like to use this knowledge to replace ``plus k 0`` in the goal with
140−``k``. We can achieve this with the ``rewrite`` tactic:
212+``k``. We can achieve this with the ``rewriteWith`` tactic:
142.. code-block:: idris
214.. code-block:: idris
144− -plusredZ_S> rewrite ih
216+ -Main.plusredZ_S> rewriteWith (Var `{{ih}})
218+ ---------- Assumptions: ----------
147− ih : k = plus k Z
220+ ih : k = plus k 0
148− ---------------------------------- (plusredZ_S) --------
221+ ---------- Goal: ----------
149− {hole3} : S k = S k
222+ {hole_0} : S k = S k
153−The ``rewrite`` tactic takes an equality proof as an argument, and tries
224+The ``rewriteWith`` tactic takes an equality proof as an argument, and tries
154−to rewrite the goal using that proof. Here, it results in an equality
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
155−which is trivially provable:
229+which is trivially provable using reflexivity:
157.. code-block:: idris
231.. code-block:: idris
159− -plusredZ_S> trivial
233+ -Main.plusredZ_S> reflexivity
160− plusredZ_S: no more goals
234+ plusredZ_S: No more goals.
161− -plusredZ_S> qed
235+ -Main.plusredZ_S> :qed
162− plusredZ_S = proof {
237+ Main.plusredZ_S = %runElab (do intro `{{k}}
163− intros;
238+ intro `{{ih}}
164− rewrite ih;
239+ compute
165− trivial;
240+ rewriteWith (Var `{{ih}})
243+Again, we can cut & paste this into the hole in the original file.
168−Again, we can add this proof to the end of our source file using the
245+.. |image| image:: ../image/plusReducesProof.png
169−``:addproof`` command at the interactive prompt.