@@ -24,87 +24,75 @@ rewriteWith and others.
2424reflexivity and others.
2525
2626To use ``pruviloj`` then call Idris with the "-p pruviloj" option and add:
27− import Pruviloj
28− import Pruviloj.Induction
27+
28+.. code-block:: idris
29+ import Pruviloj
30+ import Pruviloj.Induction
31+
2932to the top of your file.
3033
31−Here are the basic commands from Elab that we will need for the example on
32−this page:
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
36+Elab and Pruviloj, that we will need for the following example, here are
37+their docstrings:
3338
3439.. code-block:: idris
3540
36− ||| Substitute a guess into a hole.
37− export
38− solve : Elab ()
39− solve = Prim__Solve
41+ *plusReducesZ> :doc solve
42+ Language.Reflection.Elab.Tactics.solve : Elab ()
43+ Substitute a guess into a hole.
4044
4145.. code-block:: idris
4246
43− ||| Convert a hole to make it suitable for bindings - that is,
44− ||| transform it such that it has the form `?h : t . h` as opposed to
45− ||| `?h : t . f h`.
46− |||
47− ||| The binding tactics require that a hole be directly under its
48− ||| binding, or else the scopes of the generated terms won't make
49− ||| sense. This tactic creates a new hole of the proper form, and
50− ||| points the old hole at it.
51− export
52− attack : Elab ()
53− attack = Prim__Attack
47+ *plusReducesZ> :doc attack
48+ Language.Reflection.Elab.Tactics.attack : Elab ()
49+ Convert a hole to make it suitable for bindings - that is, transform
50+ it such that it has the form ?h : t . h as opposed to ?h : t . f h.
51+
52+ The binding tactics require that a hole be directly under its binding,
53+ or else the scopes of the generated terms won't make sense. This
54+ tactic creates a new hole of the proper form, and points the old hole
55+ at it.
5456
5557.. code-block:: idris
5658
57− ||| Introduce a lambda binding around the current hole and focus on
58− ||| the body. Requires that the hole be in binding form (use
59− ||| `attack`).
60− |||
61− ||| @ n the name to use for the argument
62− export
63− intro : (n : TTName) -> Elab ()
64− intro n = Prim__Intro (Just n)
59+*plusReducesZ> :doc intro
60+ Language.Reflection.Elab.Tactics.intro : (n : TTName) -> Elab ()
61+ Introduce a lambda binding around the current hole and focus on the
62+ body. Requires that the hole be in binding form (use attack).
63+ Arguments:
64+ n : TTName -- the name to use for the argument
6565
6666.. code-block:: idris
6767
68− ||| Normalise the goal.
69− export
70− compute : Elab ()
71− compute = Prim__Compute
68+ *plusReducesZ> :doc compute
69+ Language.Reflection.Elab.Tactics.compute : Elab ()
70+ Normalise the goal.
7271
7372.. code-block:: idris
7473
75− ||| Attempt to rewrite the goal using an equality.
76− |||
77− ||| The tactic searches the goal for applicable subterms, and
78− ||| constructs a context for `replace` using them. In some cases,
79− ||| this is not possible, and `replace` must be called manually with
80− ||| an appropriate context.
81− |||
82− ||| Because this tactic internally introduces a `let` binding, it
83− ||| requires that the hole be immediately under its binder (use
84− ||| `attack` if it might not be).
85− export
86− rewriteWith : Raw -> Elab ()
87− rewriteWith rule = Prim__Rewrite rule
74+*plusReducesZ> :doc rewriteWith
75+ Language.Reflection.Elab.Tactics.rewriteWith : Raw -> Elab ()
76+ Attempt to rewrite the goal using an equality.
77+
78+ The tactic searches the goal for applicable subterms, and constructs a
79+ context for replace using them. In some cases, this is not possible,
80+ and replace must be called manually with an appropriate context.
81+
82+ Because this tactic internally introduces a let binding, it requires
83+ that the hole be immediately under its binder (use attack if it might
84+ not be).
8885
8986Here is the command from pruviloj that we will need for the example on
9087this page:
9188
9289.. code-block:: idris
9390
94− ||| A special-purpose tactic that attempts to solve a goal using
95− ||| `Refl`. This is useful for ensuring that goals in fact are trivial
96− ||| when developing or testing other tactics; otherwise, consider
97− ||| using `search`.
98− reflexivity : Elab ()
99− reflexivity =
100− case !goalType of
101− `((=) {A=~a} {B=~_} ~x ~_) =>
102− do fill `(Refl {A=~a} {x=~x})
103− solve
104− _ => fail [ TextPart "The goal is not an equality, so"
105− , NamePart `{reflexivity}
106− , TextPart "is not applicable."
107− ]
91+ *plusReducesZ> :doc reflexivity
92+ Pruviloj.Core.reflexivity : Elab ()
93+ A special-purpose tactic that attempts to solve a goal using Refl.
94+ This is useful for ensuring that goals in fact are trivial when
95+ developing or testing other tactics; otherwise, consider using search.
10896
10997Interactive Example: plusReduces
11098================================
@@ -150,7 +138,7 @@ On running , two global names are created, ``plusredZ_Z`` and
150138This tells us that we have two holes Main.plusredZ_S and Main.plusredZ_Z. We can solve
151139these separately, ``plusredZ_Z`` is the simplest so we will do that first.
152140
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
154142complete the missing definition for plusredZ_Z.
155143
156144.. code-block:: idris
@@ -161,7 +149,7 @@ complete the missing definition for plusredZ_Z.
161149 {hole_0} : 0 = 0
162150
163151This 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:
165153
166154.. code-block:: idris
167155 -Main.plusredZ_Z> reflexivity
@@ -218,22 +206,8 @@ braces `{{ih}}. This gives:
218206 ---------- Goal: ----------
219207 {hole_0} : S k = S (plus k 0)
220208
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``.
223−
224−.. code-block:: idris
225−
226− -Main.plusredZ_S> compute
227−
228− ---------- Assumptions: ----------
229− k : Nat
230− ih : k = plus k 0
231− ---------- Goal: ----------
232− {hole_0} : S k = S (plus k 0)
233−
234−
235−We know, from the type of ``ih``, that ``k = plus k Z``, so we would
236−like to use this knowledge to replace ``plus k Z`` in the goal with
209+We know, from the type of ``ih``, that ``k = plus k 0``, so we would
210+like to use this knowledge to replace ``plus k 0`` in the goal with
237211``k``. We can achieve this with the ``rewriteWith`` tactic:
238212
239213.. code-block:: idris
@@ -249,8 +223,9 @@ like to use this knowledge to replace ``plus k Z`` in the goal with
249223The ``rewriteWith`` tactic takes an equality proof as an argument, and tries
250224to rewrite the goal using that proof. The ih value is entered as a constant
251225of 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.
253−Here, it results in an equality which is trivially provable using reflexivity:
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
228+which is trivially provable using reflexivity:
254229
255230.. code-block:: idris
256231