@@ -2,31 +2,35 @@
2Tactics and Theorem Proving
2Tactics and Theorem Proving
3***************************
3***************************
5+Idris supports interactive theorem proving, and theh analyse of
5−To list all unproven metavariables, use the command ``:m``. This will
6+context through metavariables. To list all unproven metavariables,
7+use the command ``:m``. This will display their qualified names and
6−display their qualified names and the expected types. To interactively
8+the expected types. To interactively prove a metavariable, use the
7−prove a metavariable, use the command ``:p name`` where ``name`` is the
9+command ``:p name`` where ``name`` is the metavariable. Once the proof
8−metavariable. Once the proof is complete, the command ``:a`` will append
10+is complete, the command ``:a`` will append it to the current module.
9−it to the current module.
11Once in the interactive prover, the following commands are available:
12Once in the interactive prover, the following commands are available:
13Basic commands
14Basic commands
14==============
15==============
16−- **:q** - Quits the prover (gives up on proving current lemma).
17+- ``:q`` - Quits the prover (gives up on proving current lemma).
17−- **abandon** - Same as :q
18+- ``abandon`` - Same as :q
18−- **state** - Displays the current state of the proof.
19+- ``state`` - Displays the current state of the proof.
19−- **term** - Displays the current proof term complete with its
20+- ``term`` - Displays the current proof term complete with its
20 yet-to-be-filled holes (is only really useful for debugging).
21 yet-to-be-filled holes (is only really useful for debugging).
21−- **undo** - Undoes the last tactic.
22+- ``undo`` - Undoes the last tactic.
22−- **qed** - Once the interactive theorem prover tells you "No more
23+- ``qed`` - Once the interactive theorem prover tells you "No more
23 goals," you get to type this in celebration! (Completes the proof and
24 goals," you get to type this in celebration! (Completes the proof and
24 exits the prover)
25 exits the prover)
26−Most common tactics
27+Commonly Used Tactics
27−===================
28+=====================
29−- **compute** - Normalizes all terms in the goal (note: does not
33+- ``compute`` - Normalizes all terms in the goal (note: does not
30 normalize assumptions)
34 normalize assumptions)
@@ -38,7 +42,10 @@ Most common tactics
38 (Vect (S (S (S (S n)))) Nat) -> Vect (S (S (S (S n)))) Nat
42 (Vect (S (S (S (S n)))) Nat) -> Vect (S (S (S (S n)))) Nat
41−- **exact** - Provide a term of the goal type directly.
48+- ``exact`` - Provide a term of the goal type directly.
@@ -48,10 +55,16 @@ Most common tactics
48 lemma: No more goals.
55 lemma: No more goals.
51−- **refine** - Use a name to refine the goal. If the name needs
61+- ``refine`` - Use a name to refine the goal. If the name needs
52 arguments, introduce them as new goals.
62 arguments, introduce them as new goals.
54−- **trivial** - Satisfies the goal using an assumption that matches its
67+- ``trivial`` - Satisfies the goal using an assumption that matches its
@@ -64,7 +77,10 @@ Most common tactics
64 lemma: No more goals.
77 lemma: No more goals.
67−- **intro** - If your goal is an arrow, turns the left term into an
83+- ``intro`` - If your goal is an arrow, turns the left term into an
68 assumption.
84 assumption.
@@ -90,7 +106,11 @@ You can also supply your own name for the assumption:
90 ---------- Goal: ----------
106 ---------- Goal: ----------
91 Nat -> Nat
107 Nat -> Nat
93−- **intros** - Exactly like intro, but it operates on all left terms at
113+- ``intros`` - Exactly like intro, but it operates on all left terms at
@@ -105,7 +125,10 @@ You can also supply your own name for the assumption:
108−- **let** - Introduces a new assumption; you may use current
131+- ``let`` - Introduces a new assumption; you may use current
109 assumptions to define the new one.
132 assumptions to define the new one.
@@ -122,7 +145,10 @@ You can also supply your own name for the assumption:
125−- **rewrite** - Takes an expression with an equality type (x = y), and
151+- ``rewrite`` - Takes an expression with an equality type (x = y), and
126 replaces all instances of x in the goal with y. Is often useful in
152 replaces all instances of x in the goal with y. Is often useful in
127 combination with 'sym'.
153 combination with 'sym'.
@@ -143,7 +169,10 @@ You can also supply your own name for the assumption:
146−- **induction** - (**Note that this is still experimental** and you may
175+- ``induction`` - (``Note that this is still experimental`` and you may
147 get strange results and error messages. We are aware of these and
176 get strange results and error messages. We are aware of these and
148 will finish the implementation eventually!) Prove the goal by
177 will finish the implementation eventually!) Prove the goal by
149 induction. Each constructor of the datatype becomes a goal.
178 induction. Each constructor of the datatype becomes a goal.
@@ -153,7 +182,10 @@ You can also supply your own name for the assumption:
153 ``%elim`` modifier.
182 ``%elim`` modifier.
156−- **sourceLocation** - Solve the current goal with information about
188+- ``sourceLocation`` - Solve the current goal with information about
157 the location in the source code where the tactic was invoked. This is
189 the location in the source code where the tactic was invoked. This is
158 mostly for embedded DSLs and programmer tools like assertions that
190 mostly for embedded DSLs and programmer tools like assertions that
159 need to know where they are called. See
191 need to know where they are called. See
@@ -162,20 +194,20 @@ You can also supply your own name for the assumption:
162Less commonly-used tactics
194Less commonly-used tactics
163==========================
195==========================
165−- **applyTactic** - Apply a user-defined tactic. This should be a
197+- ``applyTactic`` - Apply a user-defined tactic. This should be a
166 function of type ``List (TTName, Binder TT) -> TT -> Tactic``, where
198 function of type ``List (TTName, Binder TT) -> TT -> Tactic``, where
167 the first argument represents the proof context and the second
199 the first argument represents the proof context and the second
168 represents the goal. If your tactic will produce a proof term
200 represents the goal. If your tactic will produce a proof term
169 directly, use the ``Exact`` constructor from ``Tactic``.
201 directly, use the ``Exact`` constructor from ``Tactic``.
170−- **attack** - ?
202+- ``attack`` - ?
171−- **equiv** - Replaces the goal with a new one that is convertible with
203+- ``equiv`` - Replaces the goal with a new one that is convertible with
172 the old one
204 the old one
173−- **fill** - ?
205+- ``fill`` - ?
174−- **focus** - ?
206+- ``focus`` - ?
175−- **mrefine** - Refining by matching against a type
207+- ``mrefine`` - Refining by matching against a type
176−- **reflect** - ?
208+- ``reflect`` - ?
177−- **solve** - Takes a guess with the correct type and fills a hole with
209+- ``solve`` - Takes a guess with the correct type and fills a hole with
178 it, closing a proof obligation. This happens automatically in the
210 it, closing a proof obligation. This happens automatically in the
179 interactive prover, so ``solve`` is really only relevant in tactic
211 interactive prover, so ``solve`` is really only relevant in tactic
180 scripts used for helping implicit argument resolution.
212 scripts used for helping implicit argument resolution.
181−- **try** - ?
213+- ``try`` - ?