@@ -24,87 +24,75 @@ rewriteWith and others.
24reflexivity and others.
24reflexivity and others.
26To use ``pruviloj`` then call Idris with the "-p pruviloj" option and add:
26To use ``pruviloj`` then call Idris with the "-p pruviloj" option and add:
27− import Pruviloj
29+ import Pruviloj
28− import Pruviloj.Induction
30+ import Pruviloj.Induction
29to the top of your file.
32to the top of your file.
34+It is useful to get the docs at the REPL by using the ``:doc`` command, and
35+search the docstrings using ``:apropos``. So to introduce the functions from
31−Here are the basic commands from Elab that we will need for the example on
36+Elab and Pruviloj, that we will need for the following example, here are
32−this page:
37+their docstrings:
34.. code-block:: idris
39.. code-block:: idris
41+ *plusReducesZ> :doc solve
42+ Language.Reflection.Elab.Tactics.solve : Elab ()
36− ||| Substitute a guess into a hole.
43+ Substitute a guess into a hole.
41.. code-block:: idris
45.. code-block:: idris
47+ *plusReducesZ> :doc attack
48+ Language.Reflection.Elab.Tactics.attack : Elab ()
43− ||| Convert a hole to make it suitable for bindings - that is,
49+ Convert a hole to make it suitable for bindings - that is, transform
44− ||| transform it such that it has the form `?h : t . h` as opposed to
50+ it such that it has the form ?h : t . h as opposed to ?h : t . f h.
45− ||| `?h : t . f h`.
51+
47− ||| The binding tactics require that a hole be directly under its
52+ The binding tactics require that a hole be directly under its binding,
48− ||| binding, or else the scopes of the generated terms won't make
53+ or else the scopes of the generated terms won't make sense. This
49− ||| sense. This tactic creates a new hole of the proper form, and
54+ tactic creates a new hole of the proper form, and points the old hole
50− ||| points the old hole at it.
55+ at it.
53− attack = Prim__Attack
55.. code-block:: idris
57.. code-block:: idris
59+*plusReducesZ> :doc intro
60+ Language.Reflection.Elab.Tactics.intro : (n : TTName) -> Elab ()
57− ||| Introduce a lambda binding around the current hole and focus on
61+ Introduce a lambda binding around the current hole and focus on the
58− ||| the body. Requires that the hole be in binding form (use
62+ body. Requires that the hole be in binding form (use attack).
59− ||| `attack`).
63+ Arguments:
61− ||| @ n the name to use for the argument
64+ n : TTName -- the name to use for the argument
63− intro : (n : TTName) -> Elab ()
64− intro n = Prim__Intro (Just n)
66.. code-block:: idris
66.. code-block:: idris
68+ *plusReducesZ> :doc compute
69+ Language.Reflection.Elab.Tactics.compute : Elab ()
68− ||| Normalise the goal.
70+ Normalise the goal.
71− compute = Prim__Compute
73.. code-block:: idris
72.. code-block:: idris
74+*plusReducesZ> :doc rewriteWith
75+ Language.Reflection.Elab.Tactics.rewriteWith : Raw -> Elab ()
75− ||| Attempt to rewrite the goal using an equality.
76+ Attempt to rewrite the goal using an equality.
77− ||| The tactic searches the goal for applicable subterms, and
78+ The tactic searches the goal for applicable subterms, and constructs a
78− ||| constructs a context for `replace` using them. In some cases,
79+ context for replace using them. In some cases, this is not possible,
79− ||| this is not possible, and `replace` must be called manually with
80+ and replace must be called manually with an appropriate context.
80− ||| an appropriate context.
81+
82− ||| Because this tactic internally introduces a `let` binding, it
82+ Because this tactic internally introduces a let binding, it requires
83− ||| requires that the hole be immediately under its binder (use
83+ that the hole be immediately under its binder (use attack if it might
84− ||| `attack` if it might not be).
84+ not be).
86− rewriteWith : Raw -> Elab ()
87− rewriteWith rule = Prim__Rewrite rule
89Here is the command from pruviloj that we will need for the example on
86Here is the command from pruviloj that we will need for the example on
92.. code-block:: idris
89.. code-block:: idris
91+ *plusReducesZ> :doc reflexivity
92+ Pruviloj.Core.reflexivity : Elab ()
94− ||| A special-purpose tactic that attempts to solve a goal using
93+ A special-purpose tactic that attempts to solve a goal using Refl.
95− ||| `Refl`. This is useful for ensuring that goals in fact are trivial
94+ This is useful for ensuring that goals in fact are trivial when
96− ||| when developing or testing other tactics; otherwise, consider
95+ developing or testing other tactics; otherwise, consider using search.
98− reflexivity : Elab ()
101− `((=) {A=~a} {B=~_} ~x ~_) =>
102− do fill `(Refl {A=~a} {x=~x})
104− _ => fail [ TextPart "The goal is not an equality, so"
105− , NamePart `{reflexivity}
106− , TextPart "is not applicable."
109Interactive Example: plusReduces
97Interactive Example: plusReduces
110================================
98================================
@@ -150,7 +138,7 @@ On running , two global names are created, ``plusredZ_Z`` and
150This tells us that we have two holes Main.plusredZ_S and Main.plusredZ_Z. We can solve
138This tells us that we have two holes Main.plusredZ_S and Main.plusredZ_Z. We can solve
151these separately, ``plusredZ_Z`` is the simplest so we will do that first.
139these separately, ``plusredZ_Z`` is the simplest so we will do that first.
153−The ``:elab plusredZ_Z`` command enters interactive proof mode, which can be used to
141+The ``:elab plusredZ_Z`` command enters interactive elaboration mode, which can be used to
154complete the missing definition for plusredZ_Z.
142complete the missing definition for plusredZ_Z.
156.. code-block:: idris
144.. code-block:: idris
@@ -161,7 +149,7 @@ complete the missing definition for plusredZ_Z.
161 {hole_0} : 0 = 0
149 {hole_0} : 0 = 0
163This has been normalised to ``0 = 0`` so now we have to prove that ``0`` equals ``0``, which
151This has been normalised to ``0 = 0`` so now we have to prove that ``0`` equals ``0``, which
164−is easy to prove by reflexivity from pruviloj library:
152+is easy to prove by reflexivity from the pruviloj library:
166.. code-block:: idris
154.. code-block:: idris
167 -Main.plusredZ_Z> reflexivity
155 -Main.plusredZ_Z> reflexivity
@@ -218,22 +206,8 @@ braces `{{ih}}. This gives:
218 ---------- Goal: ----------
206 ---------- Goal: ----------
219 {hole_0} : S k = S (plus k 0)
207 {hole_0} : S k = S (plus k 0)
221−Since plus is defined by recursion on its first argument, the term
222−``plus (S k) Z`` in the goal can be simplified, so we use ``compute``.
224−.. code-block:: idris
226− -Main.plusredZ_S> compute
228− ---------- Assumptions: ----------
231− ---------- Goal: ----------
232− {hole_0} : S k = S (plus k 0)
235−We know, from the type of ``ih``, that ``k = plus k Z``, so we would
209+We know, from the type of ``ih``, that ``k = plus k 0``, so we would
236−like to use this knowledge to replace ``plus k Z`` in the goal with
210+like to use this knowledge to replace ``plus k 0`` in the goal with
237``k``. We can achieve this with the ``rewriteWith`` tactic:
211``k``. We can achieve this with the ``rewriteWith`` tactic:
239.. code-block:: idris
213.. code-block:: idris
@@ -249,8 +223,9 @@ like to use this knowledge to replace ``plus k Z`` in the goal with
249The ``rewriteWith`` tactic takes an equality proof as an argument, and tries
223The ``rewriteWith`` tactic takes an equality proof as an argument, and tries
250to rewrite the goal using that proof. The ih value is entered as a constant
224to rewrite the goal using that proof. The ih value is entered as a constant
251of type ``TTName`` which is entered as a backtick with double braces `{{ih}} but
225of type ``TTName`` which is entered as a backtick with double braces `{{ih}} but
252−``rewriteWith`` requires a ``raw`` value so we use ``Var`` to do this conversion.
226+``rewriteWith`` requires an expression of type ``Raw``, rather than just a name,
227+so the Var constructor is used to make a variable. Here, it results in an equality
253−Here, it results in an equality which is trivially provable using reflexivity:
228+which is trivially provable using reflexivity:
255.. code-block:: idris
230.. code-block:: idris