@@ -1,15 +1,110 @@
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 also 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 used to convert high-level Idris code into
8+the core language and for customising the language.
9+
10+Here we show how to use it to interactively construct proofs.
11+
12+Elab and Pruviloj Libraries
13+===========================
14+
15+Elaborator reflection is defined in prelude/Language/Reflection/Elab.idr
16+and pruviloj is defined in Idris-dev/libs/pruviloj/
17+
18+``Elab`` defines the basics such as: solve, attack, intro, compute,
19+rewriteWith and others.
20+``pruviloj`` defines some more advanced derived commands such as:
21+reflexivity and others.
22+
23+To use ``pruviloj`` then call Idris with the "-p pruviloj" option and add:
24+ import Pruviloj
25+ import Pruviloj.Induction
26+to the top of your file.
27+
28+Here are the basic commands from Elab that we will need for the example on
29+this page:
30+
31+.. code-block:: idris
32+
33+ ||| Substitute a guess into a hole.
34+ export
35+ solve : Elab ()
36+ solve = Prim__Solve
37+
38+.. code-block:: idris
39+
40+ ||| Convert a hole to make it suitable for bindings - that is,
41+ ||| transform it such that it has the form `?h : t . h` as opposed to
42+ ||| `?h : t . f h`.
43+ |||
44+ ||| The binding tactics require that a hole be directly under its
45+ ||| binding, or else the scopes of the generated terms won't make
46+ ||| sense. This tactic creates a new hole of the proper form, and
47+ ||| points the old hole at it.
48+ export
49+ attack : Elab ()
50+ attack = Prim__Attack
51+
52+.. code-block:: idris
53+
54+ ||| Introduce a lambda binding around the current hole and focus on
55+ ||| the body. Requires that the hole be in binding form (use
56+ ||| `attack`).
57+ |||
58+ ||| @ n the name to use for the argument
59+ export
60+ intro : (n : TTName) -> Elab ()
61+ intro n = Prim__Intro (Just n)
62+
63+.. code-block:: idris
64+
65+ ||| Normalise the goal.
66+ export
67+ compute : Elab ()
68+ compute = Prim__Compute
69+
70+.. code-block:: idris
71+
72+ ||| Attempt to rewrite the goal using an equality.
73+ |||
74+ ||| The tactic searches the goal for applicable subterms, and
75+ ||| constructs a context for `replace` using them. In some cases,
76+ ||| this is not possible, and `replace` must be called manually with
77+ ||| an appropriate context.
78+ |||
79+ ||| Because this tactic internally introduces a `let` binding, it
80+ ||| requires that the hole be immediately under its binder (use
81+ ||| `attack` if it might not be).
82+ export
83+ rewriteWith : Raw -> Elab ()
84+ rewriteWith rule = Prim__Rewrite rule
85+
86+Here is the command from pruviloj that we will need for the example on
87+this page:
88+
89+.. code-block:: idris
90+
91+ ||| A special-purpose tactic that attempts to solve a goal using
92+ ||| `Refl`. This is useful for ensuring that goals in fact are trivial
93+ ||| when developing or testing other tactics; otherwise, consider
94+ ||| using `search`.
95+ reflexivity : Elab ()
96+ reflexivity =
97+ case !goalType of
98+ `((=) {A=~a} {B=~_} ~x ~_) =>
99+ do fill `(Refl {A=~a} {x=~x})
100+ solve
101+ _ => fail [ TextPart "The goal is not an equality, so"
102+ , NamePart `{reflexivity}
103+ , TextPart "is not applicable."
104+ ]
105+
106+Interactive Example: plusReduces
107+================================
13108
14109One way to write proofs interactively is to write the general *structure* of
15110the proof, and use the interactive mode to complete the details.
@@ -25,145 +120,147 @@ hypothesis, and insert *holes* for the rest of the definition:
25120
26121.. code-block:: idris
27122
123+ import Pruviloj
124+ import Pruviloj.Induction
125+
28126 plusReducesZ' : (n:Nat) -> n = plus n Z
29127 plusReducesZ' Z = ?plusredZ_Z
30128 plusReducesZ' (S k) = let ih = plusReducesZ' k in
31129 ?plusredZ_S
32130
33131On 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:
132+``plusredZ_S``, with no definition.
38133
39134.. code-block:: idris
40135
41− *theorems> :m
42− Global holes:
43− [plusredZ_S,plusredZ_Z]
136+ *theorems> : idris plusReducesZ.idr -p pruviloj
44137
45−.. code-block:: idris
138+ . / _/___/ /____(_)____
139+ / // __ / ___/ / ___/ Version 1.2.0
140+ _/ // /_/ / / / (__ ) http://www.idris-lang.org/
141+ /___/\__,_/_/ /_/____/ Type :? for help
46142
47− *theorems> :t plusredZ_Z
48− plusredZ_Z : Z = plus Z Z
143+ Idris is free software with ABSOLUTELY NO WARRANTY.
144+ For details type :warranty.
145+ Holes: Main.plusredZ_S, Main.plusredZ_Z
49146
50− *theorems> :t plusredZ_S
51− plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
147+This tells us that we have two holes Main.plusredZ_S and Main.plusredZ_Z. We can solve
148+these separately, ``plusredZ_Z`` is the simplest so we will do that first.
52149
53−The ``:p`` command enters interactive proof mode, which can be used to
54−complete the missing definitions.
150+The ``:elab plusredZ_Z`` command enters interactive proof mode, which can be used to
151+complete the missing definition for plusredZ_Z.
55152
56153.. code-block:: idris
57154
58− *theorems> :p plusredZ_Z
155+ *plusReducesZ> :elab plusredZ_Z
59156
60− ---------------------------------- (plusredZ_Z) --------
61− {hole0} : Z = plus Z Z
157+ ---------- Goal: ----------
158+ {hole_0} : 0 = 0
62159
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:
160+This has been normalised to ``0 = 0`` so now we have to prove that ``0`` equals ``0``, which
161+is easy to prove by reflexivity from pruviloj library:
67162
68163.. code-block:: idris
164+ -Main.plusredZ_Z> reflexivity
165+ plusredZ_Z: No more goals.
69166
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):
167+This tells us that the proof is complete. We can now leave the interactive mode which
168+we entered with the ``:elab`` command. We do this with the ``:qed`` command:
79169
80170.. code-block:: idris
81171
82− -plusredZ_Z> refine Refl
83− plusredZ_Z: no more goals
172+ -Main.plusredZ_Z> :qed
173+ Proof completed!
174+ Main.plusredZ_Z = %runElab (do reflexivity)
175+ Holes: Main.plusredZ_S
84176
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:
177+This gives us a trace of the proof which is ``plusredZ_Z = %runElab (do reflexivity)``. We
178+can cut & paste this into the hole in the original file. This also tells us that we
179+have another hole ``Main.plusredZ_S`` remaining.
90180
91−.. code-block:: idris
181+This remaining proof is bit more complicated, the following diagram gives an overview:
92182
93− -plusredZ_Z> qed
94− plusredZ_Z = proof
95− compute
96− refine Refl
183+|image|
97184
98−.. code-block:: idris
99−
100− *theorems> :m
101− Global holes:
102− [plusredZ_S]
103−
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``:
185+We approach this remaining proof in the same way by using the ``:elab`` command:
107186
108187.. code-block:: idris
109188
110− *theorems> :p plusredZ_S
189+ *plusReducesZ> :elab plusredZ_S
190+
111191
112− ---------------------------------- (plusredZ_S) --------
113− {hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
192+ ---------- Goal: ----------
193+ {hole_0} : (k : Nat) -> (k = plus k 0) -> S k = S (plus k 0)
114194
115195In this case, the goal is a function type, using ``k`` (the argument
116196accessible by pattern matching) and ``ih`` — the local variable
117197containing 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:
198+assumptions using the ``intro`` tactic twice. The parameter is entered as
199+a constant of type ``TTName`` which is entered as a backtick with double
200+braces `{{ih}}. This gives:
120201
121202.. code-block:: idris
122203
123− k : Nat
124− ih : k = plus k Z
125− ---------------------------------- (plusredZ_S) --------
126− {hole2} : S k = plus (S k) Z
204+ -Main.plusredZ_S> intro `{{k}}
205+
206+ ---------- Assumptions: ----------
207+ k : Nat
208+ ---------- Goal: ----------
209+ {hole_0} : (k = plus k 0) -> S k = S (plus k 0)
210+ -Main.plusredZ_S> intro `{{ih}}
211+
212+ ---------- Assumptions: ----------
213+ k : Nat
214+ ih : k = plus k 0
215+ ---------- Goal: ----------
216+ {hole_0} : S k = S (plus k 0)
127217
128218Since plus is defined by recursion on its first argument, the term
129219``plus (S k) Z`` in the goal can be simplified, so we use ``compute``.
130220
131221.. code-block:: idris
132222
133− k : Nat
134− ih : k = plus k Z
135− ---------------------------------- (plusredZ_S) --------
136− {hole2} : S k = S (plus k Z)
223+ -Main.plusredZ_S> compute
224+
225+ ---------- Assumptions: ----------
226+ k : Nat
227+ ih : k = plus k 0
228+ ---------- Goal: ----------
229+ {hole_0} : S k = S (plus k 0)
230+
137231
138232We know, from the type of ``ih``, that ``k = plus k Z``, so we would
139233like to use this knowledge to replace ``plus k Z`` in the goal with
140−``k``. We can achieve this with the ``rewrite`` tactic:
234+``k``. We can achieve this with the ``rewriteWith`` tactic:
141235
142236.. code-block:: idris
143237
144− -plusredZ_S> rewrite ih
238+ -Main.plusredZ_S> rewriteWith (Var `{{ih}})
145239
146− k : Nat
147− ih : k = plus k Z
148− ---------------------------------- (plusredZ_S) --------
149− {hole3} : S k = S k
240+ ---------- Assumptions: ----------
241+ k : Nat
242+ ih : k = plus k 0
243+ ---------- Goal: ----------
244+ {hole_0} : S k = S k
150245
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:
246+The ``rewriteWith`` tactic takes an equality proof as an argument, and tries
247+to rewrite the goal using that proof. The ih value is entered as a constant
248+of type ``TTName`` which is entered as a backtick with double braces `{{ih}} but
249+``rewriteWith`` requires a ``raw`` value so we use ``Var`` to do this conversion.
250+Here, it results in an equality which is trivially provable using reflexivity:
156251
157252.. code-block:: idris
158253
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− }
254+ -Main.plusredZ_S> reflexivity
255+ plusredZ_S: No more goals.
256+ -Main.plusredZ_S> :qed
257+ Proof completed!
258+ Main.plusredZ_S = %runElab (do intro `{{k}}
259+ intro `{{ih}}
260+ compute
261+ rewriteWith (Var `{{ih}})
262+ reflexivity)
263+
264+Again, we can cut & paste this into the hole in the original file.
167265
168−Again, we can add this proof to the end of our source file using the
169−``:addproof`` command at the interactive prompt.
266+.. |image| image:: ../image/plusReducesProof.png