@@ -2,31 +2,35 @@
22Tactics and Theorem Proving
33***************************
44
5−To list all unproven metavariables, use the command ``:m``. This will
6−display their qualified names and the expected types. To interactively
7−prove a metavariable, use the command ``:p name`` where ``name`` is the
8−metavariable. Once the proof is complete, the command ``:a`` will append
9−it to the current module.
5+Idris supports interactive theorem proving, and theh analyse of
6+context through metavariables. To list all unproven metavariables,
7+use the command ``:m``. This will display their qualified names and
8+the expected types. To interactively prove a metavariable, use the
9+command ``:p name`` where ``name`` is the metavariable. Once the proof
10+is complete, the command ``:a`` will append it to the current module.
1011
1112Once in the interactive prover, the following commands are available:
1213
1314Basic commands
1415==============
1516
16−- **:q** - Quits the prover (gives up on proving current lemma).
17−- **abandon** - Same as :q
18−- **state** - Displays the current state of the proof.
19−- **term** - Displays the current proof term complete with its
17+- ``:q`` - Quits the prover (gives up on proving current lemma).
18+- ``abandon`` - Same as :q
19+- ``state`` - Displays the current state of the proof.
20+- ``term`` - Displays the current proof term complete with its
2021 yet-to-be-filled holes (is only really useful for debugging).
21−- **undo** - Undoes the last tactic.
22−- **qed** - Once the interactive theorem prover tells you "No more
22+- ``undo`` - Undoes the last tactic.
23+- ``qed`` - Once the interactive theorem prover tells you "No more
2324 goals," you get to type this in celebration! (Completes the proof and
2425 exits the prover)
2526
26−Most common tactics
27−===================
27+Commonly Used Tactics
28+=====================
2829
29−- **compute** - Normalizes all terms in the goal (note: does not
30+Compute
31+-------
32+
33+- ``compute`` - Normalizes all terms in the goal (note: does not
3034 normalize assumptions)
3135
3236::
@@ -38,7 +42,10 @@ Most common tactics
3842 (Vect (S (S (S (S n)))) Nat) -> Vect (S (S (S (S n)))) Nat
3943 -lemma>
4044
41−- **exact** - Provide a term of the goal type directly.
45+Exact
46+-----
47+
48+- ``exact`` - Provide a term of the goal type directly.
4249
4350::
4451
@@ -48,10 +55,16 @@ Most common tactics
4855 lemma: No more goals.
4956 -lemma>
5057
51−- **refine** - Use a name to refine the goal. If the name needs
58+Refine
59+------
60+
61+- ``refine`` - Use a name to refine the goal. If the name needs
5262 arguments, introduce them as new goals.
5363
54−- **trivial** - Satisfies the goal using an assumption that matches its
64+Trivial
65+-------
66+
67+- ``trivial`` - Satisfies the goal using an assumption that matches its
5568 type.
5669
5770::
@@ -64,7 +77,10 @@ Most common tactics
6477 lemma: No more goals.
6578 -lemma>
6679
67−- **intro** - If your goal is an arrow, turns the left term into an
80+Intro
81+-----
82+
83+- ``intro`` - If your goal is an arrow, turns the left term into an
6884 assumption.
6985
7086::
@@ -90,7 +106,11 @@ You can also supply your own name for the assumption:
90106 ---------- Goal: ----------
91107 Nat -> Nat
92108
93−- **intros** - Exactly like intro, but it operates on all left terms at
109+
110+Intros
111+------
112+
113+- ``intros`` - Exactly like intro, but it operates on all left terms at
94114 once.
95115
96116::
@@ -105,7 +125,10 @@ You can also supply your own name for the assumption:
105125 Nat
106126 -lemma>
107127
108−- **let** - Introduces a new assumption; you may use current
128+let
129+---
130+
131+- ``let`` - Introduces a new assumption; you may use current
109132 assumptions to define the new one.
110133
111134::
@@ -122,7 +145,10 @@ You can also supply your own name for the assumption:
122145 BigInt
123146 -lemma>
124147
125−- **rewrite** - Takes an expression with an equality type (x = y), and
148+rewrite
149+-------
150+
151+- ``rewrite`` - Takes an expression with an equality type (x = y), and
126152 replaces all instances of x in the goal with y. Is often useful in
127153 combination with 'sym'.
128154
@@ -143,7 +169,10 @@ You can also supply your own name for the assumption:
143169 Vect Z a
144170 -lemma>
145171
146−- **induction** - (**Note that this is still experimental** and you may
172+induction
173+---------
174+
175+- ``induction`` - (``Note that this is still experimental`` and you may
147176 get strange results and error messages. We are aware of these and
148177 will finish the implementation eventually!) Prove the goal by
149178 induction. Each constructor of the datatype becomes a goal.
@@ -153,7 +182,10 @@ You can also supply your own name for the assumption:
153182 ``%elim`` modifier.
154183
155184
156−- **sourceLocation** - Solve the current goal with information about
185+sourceLocation
186+--------------
187+
188+- ``sourceLocation`` - Solve the current goal with information about
157189 the location in the source code where the tactic was invoked. This is
158190 mostly for embedded DSLs and programmer tools like assertions that
159191 need to know where they are called. See
@@ -162,20 +194,20 @@ You can also supply your own name for the assumption:
162194Less commonly-used tactics
163195==========================
164196
165−- **applyTactic** - Apply a user-defined tactic. This should be a
197+- ``applyTactic`` - Apply a user-defined tactic. This should be a
166198 function of type ``List (TTName, Binder TT) -> TT -> Tactic``, where
167199 the first argument represents the proof context and the second
168200 represents the goal. If your tactic will produce a proof term
169201 directly, use the ``Exact`` constructor from ``Tactic``.
170−- **attack** - ?
171−- **equiv** - Replaces the goal with a new one that is convertible with
202+- ``attack`` - ?
203+- ``equiv`` - Replaces the goal with a new one that is convertible with
172204 the old one
173−- **fill** - ?
174−- **focus** - ?
175−- **mrefine** - Refining by matching against a type
176−- **reflect** - ?
177−- **solve** - Takes a guess with the correct type and fills a hole with
205+- ``fill`` - ?
206+- ``focus`` - ?
207+- ``mrefine`` - Refining by matching against a type
208+- ``reflect`` - ?
209+- ``solve`` - Takes a guess with the correct type and fills a hole with
178210 it, closing a proof obligation. This happens automatically in the
179211 interactive prover, so ``solve`` is really only relevant in tactic
180212 scripts used for helping implicit argument resolution.
181−- **try** - ?
213+- ``try`` - ?