git.iko.soy/Idris-dev
on 2df4ef6 help sign in
Idris-dev/docs/reference/tactics.rst
213 lines 6.2 kB history raw
1***************************
2Tactics and Theorem Proving
3***************************
5Idris supports interactive theorem proving, and the analyse of context
6through holes. To list all unproven holes, use the command ``:m``.
7This will display their qualified names and the expected types. To
8interactively prove a holes, use the command ``:p name`` where ``name``
9is the hole. Once the proof is complete, the command ``:a`` will append
10it to the current module.
12Once in the interactive prover, the following commands are available:
14Basic commands
15==============
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
21 yet-to-be-filled holes (is only really useful for debugging).
22- ``undo`` - Undoes the last tactic.
23- ``qed`` - Once the interactive theorem prover tells you "No more
24 goals," you get to type this in celebration! (Completes the proof and
25 exits the prover)
27Commonly Used Tactics
28=====================
30Compute
31-------
33- ``compute`` - Normalizes all terms in the goal (note: does not
34 normalize assumptions)
36::
38 ---------- Goal: ----------
39 (Vect (S (S Z + (S Z) + (S n))) Nat) -> Vect (S (S (S (S n)))) Nat
40 -lemma> compute
41 ---------- Goal: ----------
42 (Vect (S (S (S (S n)))) Nat) -> Vect (S (S (S (S n)))) Nat
43 -lemma>
45Exact
46-----
48- ``exact`` - Provide a term of the goal type directly.
50::
52 ---------- Goal: ----------
53 Nat
54 -lemma> exact Z
55 lemma: No more goals.
56 -lemma>
58Refine
59------
61- ``refine`` - Use a name to refine the goal. If the name needs
62 arguments, introduce them as new goals.
64Trivial
65-------
67- ``trivial`` - Satisfies the goal using an assumption that matches its
68 type.
70::
72 ---------- Assumptions: ----------
73 value : Nat
74 ---------- Goal: ----------
75 Nat
76 -lemma> trivial
77 lemma: No more goals.
78 -lemma>
80Intro
81-----
83- ``intro`` - If your goal is an arrow, turns the left term into an
84 assumption.
86::
88 ---------- Goal: ----------
89 Nat -> Nat -> Nat
90 -lemma> intro
91 ---------- Assumptions: ----------
92 n : Nat
93 ---------- Goal: ----------
94 Nat -> Nat
95 -lemma>
97You can also supply your own name for the assumption:
99::
101 ---------- Goal: ----------
102 Nat -> Nat -> Nat
103 -lemma> intro number
104 ---------- Assumptions: ----------
105 number : Nat
106 ---------- Goal: ----------
107 Nat -> Nat
110Intros
111------
113- ``intros`` - Exactly like intro, but it operates on all left terms at
114 once.
116::
118 ---------- Goal: ----------
119 Nat -> Nat -> Nat
120 -lemma> intros
121 ---------- Assumptions: ----------
122 n : Nat
123 m : Nat
124 ---------- Goal: ----------
125 Nat
126 -lemma>
128let
129---
131- ``let`` - Introduces a new assumption; you may use current
132 assumptions to define the new one.
134::
136 ---------- Assumptions: ----------
137 n : Nat
138 ---------- Goal: ----------
139 BigInt
140 -lemma> let x = toIntegerNat n
141 ---------- Assumptions: ----------
142 n : Nat
143 x = toIntegerNat n: BigInt
144 ---------- Goal: ----------
145 BigInt
146 -lemma>
148rewrite
149-------
151- ``rewrite`` - Takes an expression with an equality type (x = y), and
152 replaces all instances of x in the goal with y. Is often useful in
153 combination with 'sym'.
155::
157 ---------- Assumptions: ----------
158 n : Nat
159 a : Type
160 value : Vect Z a
161 ---------- Goal: ----------
162 Vect (mult n Z) a
163 -lemma> rewrite sym (multZeroRightZero n)
164 ---------- Assumptions: ----------
165 n : Nat
166 a : Type
167 value : Vect Z a
168 ---------- Goal: ----------
169 Vect Z a
170 -lemma>
172induction
173---------
175- ``induction`` - (``Note that this is still experimental`` and you may
176 get strange results and error messages. We are aware of these and
177 will finish the implementation eventually!) Prove the goal by
178 induction. Each constructor of the datatype becomes a goal.
179 Constructors with recursive arguments become induction steps, while
180 simple constructors become base cases. Note that this only works for
181 datatypes that have eliminators: a datatype definition must have the
182 ``%elim`` modifier.
185sourceLocation
186--------------
188- ``sourceLocation`` - Solve the current goal with information about
189 the location in the source code where the tactic was invoked. This is
190 mostly for embedded DSLs and programmer tools like assertions that
191 need to know where they are called. See
192 ``Language.Reflection.SourceLocation`` for more information.
194Less commonly-used tactics
195==========================
197- ``applyTactic`` - Apply a user-defined tactic. This should be a
198 function of type ``List (TTName, Binder TT) -> TT -> Tactic``, where
199 the first argument represents the proof context and the second
200 represents the goal. If your tactic will produce a proof term
201 directly, use the ``Exact`` constructor from ``Tactic``.
202- ``attack`` - ?
203- ``equiv`` - Replaces the goal with a new one that is convertible with
204 the old one
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
210 it, closing a proof obligation. This happens automatically in the
211 interactive prover, so ``solve`` is really only relevant in tactic
212 scripts used for helping implicit argument resolution.
213- ``try`` - ?