@@ -1,15 +1,110 @@
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 also 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 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.
11−mechanism for building proof automation which is beyond the scope of this
9+
12−tutorial. In this section, we briefly discus tactics.
10+Here we show how to use it to interactively construct proofs.
12+Elab and Pruviloj Libraries
13+===========================
15+Elaborator reflection is defined in prelude/Language/Reflection/Elab.idr
16+and pruviloj is defined in Idris-dev/libs/pruviloj/
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.
23+To use ``pruviloj`` then call Idris with the "-p pruviloj" option and add:
25+ import Pruviloj.Induction
26+to the top of your file.
28+Here are the basic commands from Elab that we will need for the example on
33+ ||| Substitute a guess into a hole.
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
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.
50+ attack = Prim__Attack
54+ ||| Introduce a lambda binding around the current hole and focus on
55+ ||| the body. Requires that the hole be in binding form (use
58+ ||| @ n the name to use for the argument
60+ intro : (n : TTName) -> Elab ()
61+ intro n = Prim__Intro (Just n)
65+ ||| Normalise the goal.
68+ compute = Prim__Compute
72+ ||| Attempt to rewrite the goal using an equality.
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.
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).
83+ rewriteWith : Raw -> Elab ()
84+ rewriteWith rule = Prim__Rewrite rule
86+Here is the command from pruviloj that we will need for the example on
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
95+ reflexivity : Elab ()
98+ `((=) {A=~a} {B=~_} ~x ~_) =>
99+ do fill `(Refl {A=~a} {x=~x})
101+ _ => fail [ TextPart "The goal is not an equality, so"
102+ , NamePart `{reflexivity}
103+ , TextPart "is not applicable."
106+Interactive Example: plusReduces
107+================================
14One way to write proofs interactively is to write the general *structure* of
109One way to write proofs interactively is to write the general *structure* of
15the proof, and use the interactive mode to complete the details.
110the proof, and use the interactive mode to complete the details.
@@ -25,145 +120,147 @@ hypothesis, and insert *holes* for the rest of the definition:
26.. code-block:: idris
121.. code-block:: idris
124+ import Pruviloj.Induction
28 plusReducesZ' : (n:Nat) -> n = plus n Z
126 plusReducesZ' : (n:Nat) -> n = plus n Z
29 plusReducesZ' Z = ?plusredZ_Z
127 plusReducesZ' Z = ?plusredZ_Z
30 plusReducesZ' (S k) = let ih = plusReducesZ' k in
128 plusReducesZ' (S k) = let ih = plusReducesZ' k in
31 ?plusredZ_S
129 ?plusredZ_S
33On running , two global names are created, ``plusredZ_Z`` and
131On running , two global names are created, ``plusredZ_Z`` and
34−``plusredZ_S``, with no definition. We can use the ``:m`` command at the
132+``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
134.. code-block:: idris
41− *theorems> :m
136+ *theorems> : idris plusReducesZ.idr -p pruviloj
43− [plusredZ_S,plusredZ_Z]
45−.. code-block:: idris
138+ . / _/___/ /____(_)____
139+ / // __ / ___/ / ___/ Version 1.2.0
140+ _/ // /_/ / / / (__ ) http://www.idris-lang.org/
141+ /___/\__,_/_/ /_/____/ Type :? for help
47− *theorems> :t plusredZ_Z
143+ Idris is free software with ABSOLUTELY NO WARRANTY.
48− plusredZ_Z : Z = plus Z Z
144+ For details type :warranty.
145+ Holes: Main.plusredZ_S, Main.plusredZ_Z
50− *theorems> :t plusredZ_S
147+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
148+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
150+The ``:elab plusredZ_Z`` command enters interactive proof mode, which can be used to
54−complete the missing definitions.
151+complete the missing definition for plusredZ_Z.
56.. code-block:: idris
153.. code-block:: idris
58− *theorems> :p plusredZ_Z
155+ *plusReducesZ> :elab plusredZ_Z
60− ---------------------------------- (plusredZ_Z) --------
157+ ---------- Goal: ----------
61− {hole0} : Z = plus Z Z
158+ {hole_0} : 0 = 0
63−This gives us a list of premises (above the line; there are none here)
160+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
161+is easy to prove by reflexivity from 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
163.. code-block:: idris
164+ -Main.plusredZ_Z> reflexivity
165+ plusredZ_Z: No more goals.
70− -plusredZ_Z> compute
167+This tells us that the proof is complete. We can now leave the interactive mode which
71−
168+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
170.. code-block:: idris
82− -plusredZ_Z> refine Refl
172+ -Main.plusredZ_Z> :qed
83− plusredZ_Z: no more goals
173+ Proof completed!
174+ Main.plusredZ_Z = %runElab (do reflexivity)
175+ Holes: Main.plusredZ_S
85−Here, we could also have used the ``trivial`` tactic, which tries to
177+This gives us a trace of the proof which is ``plusredZ_Z = %runElab (do reflexivity)``. We
86−refine by ``Refl``, and if that fails, tries to refine by each name in
178+can cut & paste this into the hole in the original file. This also tells us that we
87−the local context. When a proof is complete, we use the ``qed`` tactic
179+have another hole ``Main.plusredZ_S`` remaining.
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
181+This remaining proof is bit more complicated, the following diagram gives an overview:
93− -plusredZ_Z> qed
183+|image|
98−.. code-block:: idris
185+We approach this remaining proof in the same way by using the ``:elab`` command:
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``:
108.. code-block:: idris
187.. code-block:: idris
110− *theorems> :p plusredZ_S
189+ *plusReducesZ> :elab plusredZ_S
112− ---------------------------------- (plusredZ_S) --------
192+ ---------- Goal: ----------
113− {hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
193+ {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
195In this case, the goal is a function type, using ``k`` (the argument
116accessible by pattern matching) and ``ih`` — the local variable
196accessible by pattern matching) and ``ih`` — the local variable
117containing the result of the recursive call. We can introduce these as
197containing the result of the recursive call. We can introduce these as
118−premises using the ``intro`` tactic twice (or ``intros``, which
198+assumptions using the ``intro`` tactic twice. The parameter is entered as
119−introduces all arguments as premises). This gives:
199+a constant of type ``TTName`` which is entered as a backtick with double
200+braces `{{ih}}. This gives:
121.. code-block:: idris
202.. code-block:: idris
204+ -Main.plusredZ_S> intro `{{k}}
206+ ---------- Assumptions: ----------
124− ih : k = plus k Z
208+ ---------- Goal: ----------
125− ---------------------------------- (plusredZ_S) --------
209+ {hole_0} : (k = plus k 0) -> S k = S (plus k 0)
126− {hole2} : S k = plus (S k) Z
210+ -Main.plusredZ_S> intro `{{ih}}
212+ ---------- Assumptions: ----------
215+ ---------- Goal: ----------
216+ {hole_0} : S k = S (plus k 0)
128Since plus is defined by recursion on its first argument, the term
218Since 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``.
219``plus (S k) Z`` in the goal can be simplified, so we use ``compute``.
131.. code-block:: idris
221.. code-block:: idris
223+ -Main.plusredZ_S> compute
225+ ---------- Assumptions: ----------
134− ih : k = plus k Z
227+ ih : k = plus k 0
135− ---------------------------------- (plusredZ_S) --------
228+ ---------- Goal: ----------
136− {hole2} : S k = S (plus k Z)
229+ {hole_0} : S k = S (plus k 0)
138We know, from the type of ``ih``, that ``k = plus k Z``, so we would
232We 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
233like 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:
142.. code-block:: idris
236.. code-block:: idris
144− -plusredZ_S> rewrite ih
238+ -Main.plusredZ_S> rewriteWith (Var `{{ih}})
240+ ---------- Assumptions: ----------
147− ih : k = plus k Z
242+ ih : k = plus k 0
148− ---------------------------------- (plusredZ_S) --------
243+ ---------- Goal: ----------
149− {hole3} : S k = S k
244+ {hole_0} : S k = S k
153−The ``rewrite`` tactic takes an equality proof as an argument, and tries
246+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
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.
155−which is trivially provable:
250+Here, it results in an equality which is trivially provable using reflexivity:
157.. code-block:: idris
252.. code-block:: idris
159− -plusredZ_S> trivial
254+ -Main.plusredZ_S> reflexivity
160− plusredZ_S: no more goals
255+ plusredZ_S: No more goals.
161− -plusredZ_S> qed
256+ -Main.plusredZ_S> :qed
162− plusredZ_S = proof {
258+ Main.plusredZ_S = %runElab (do intro `{{k}}
163− intros;
259+ intro `{{ih}}
164− rewrite ih;
260+ compute
165− trivial;
261+ rewriteWith (Var `{{ih}})
264+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
266+.. |image| image:: ../image/plusReducesProof.png
169−``:addproof`` command at the interactive prompt.