git.iko.soy/Idris-dev
on bc8da8d help sign in
Idris-dev/docs/reference/tactics.rst
217 lines 6.4 kB history raw
1****************************************
2DEPRECATED: Tactics and Theorem Proving
3****************************************
5.. warning::
6 The interactive theorem-proving interface documented here has been
7 deprecated in favor of :ref:`elaborator-reflection`.
9Idris supports interactive theorem proving, and the analyse of context
10through holes. To list all unproven holes, use the command ``:m``.
11This will display their qualified names and the expected types. To
12interactively prove a holes, use the command ``:p name`` where ``name``
13is the hole. Once the proof is complete, the command ``:a`` will append
14it to the current module.
16Once in the interactive prover, the following commands are available:
18Basic commands
19==============
21- ``:q`` - Quits the prover (gives up on proving current lemma).
22- ``:abandon`` - Same as :q
23- ``:state`` - Displays the current state of the proof.
24- ``:term`` - Displays the current proof term complete with its
25 yet-to-be-filled holes (is only really useful for debugging).
26- ``:undo`` - Undoes the last tactic.
27- ``:qed`` - Once the interactive theorem prover tells you "No more
28 goals," you get to type this in celebration! (Completes the proof and
29 exits the prover)
31Commonly Used Tactics
32=====================
34Compute
35-------
37- ``compute`` - Normalises all terms in the goal (note: does not
38 normalise assumptions)
40::
42 ---------- Goal: ----------
43 (Vect (S (S Z + (S Z) + (S n))) Nat) -> Vect (S (S (S (S n)))) Nat
44 -lemma> compute
45 ---------- Goal: ----------
46 (Vect (S (S (S (S n)))) Nat) -> Vect (S (S (S (S n)))) Nat
47 -lemma>
49Exact
50-----
52- ``exact`` - Provide a term of the goal type directly.
54::
56 ---------- Goal: ----------
57 Nat
58 -lemma> exact Z
59 lemma: No more goals.
60 -lemma>
62Refine
63------
65- ``refine`` - Use a name to refine the goal. If the name needs
66 arguments, introduce them as new goals.
68Trivial
69-------
71- ``trivial`` - Satisfies the goal using an assumption that matches its
72 type.
74::
76 ---------- Assumptions: ----------
77 value : Nat
78 ---------- Goal: ----------
79 Nat
80 -lemma> trivial
81 lemma: No more goals.
82 -lemma>
84Intro
85-----
87- ``intro`` - If your goal is an arrow, turns the left term into an
88 assumption.
90::
92 ---------- Goal: ----------
93 Nat -> Nat -> Nat
94 -lemma> intro
95 ---------- Assumptions: ----------
96 n : Nat
97 ---------- Goal: ----------
98 Nat -> Nat
99 -lemma>
101You can also supply your own name for the assumption:
103::
105 ---------- Goal: ----------
106 Nat -> Nat -> Nat
107 -lemma> intro number
108 ---------- Assumptions: ----------
109 number : Nat
110 ---------- Goal: ----------
111 Nat -> Nat
114Intros
115------
117- ``intros`` - Exactly like intro, but it operates on all left terms at
118 once.
120::
122 ---------- Goal: ----------
123 Nat -> Nat -> Nat
124 -lemma> intros
125 ---------- Assumptions: ----------
126 n : Nat
127 m : Nat
128 ---------- Goal: ----------
129 Nat
130 -lemma>
132let
133---
135- ``let`` - Introduces a new assumption; you may use current
136 assumptions to define the new one.
138::
140 ---------- Assumptions: ----------
141 n : Nat
142 ---------- Goal: ----------
143 BigInt
144 -lemma> let x = toIntegerNat n
145 ---------- Assumptions: ----------
146 n : Nat
147 x = toIntegerNat n: BigInt
148 ---------- Goal: ----------
149 BigInt
150 -lemma>
152rewrite
153-------
155- ``rewrite`` - Takes an expression with an equality type (x = y), and
156 replaces all instances of x in the goal with y. Is often useful in
157 combination with 'sym'.
159::
161 ---------- Assumptions: ----------
162 n : Nat
163 a : Type
164 value : Vect Z a
165 ---------- Goal: ----------
166 Vect (mult n Z) a
167 -lemma> rewrite sym (multZeroRightZero n)
168 ---------- Assumptions: ----------
169 n : Nat
170 a : Type
171 value : Vect Z a
172 ---------- Goal: ----------
173 Vect Z a
174 -lemma>
176induction
177---------
179- ``induction`` - (``Note that this is still experimental`` and you may
180 get strange results and error messages. We are aware of these and
181 will finish the implementation eventually!) Prove the goal by
182 induction. Each constructor of the datatype becomes a goal.
183 Constructors with recursive arguments become induction steps, while
184 simple constructors become base cases. Note that this only works for
185 datatypes that have eliminators: a datatype definition must have the
186 ``%elim`` modifier.
189sourceLocation
190--------------
192- ``sourceLocation`` - Solve the current goal with information about
193 the location in the source code where the tactic was invoked. This is
194 mostly for embedded DSLs and programmer tools like assertions that
195 need to know where they are called. See
196 ``Language.Reflection.SourceLocation`` for more information.
198Less commonly-used tactics
199==========================
201- ``applyTactic`` - Apply a user-defined tactic. This should be a
202 function of type ``List (TTName, Binder TT) -> TT -> Tactic``, where
203 the first argument represents the proof context and the second
204 represents the goal. If your tactic will produce a proof term
205 directly, use the ``Exact`` constructor from ``Tactic``.
206- ``attack`` - ?
207- ``equiv`` - Replaces the goal with a new one that is convertible with
208 the old one
209- ``fill`` - ?
210- ``focus`` - ?
211- ``mrefine`` - Refining by matching against a type
212- ``reflect`` - ?
213- ``solve`` - Takes a guess with the correct type and fills a hole with
214 it, closing a proof obligation. This happens automatically in the
215 interactive prover, so ``solve`` is really only relevant in tactic
216 scripts used for helping implicit argument resolution.
217- ``try`` - ?