-
Notifications
You must be signed in to change notification settings - Fork 2
/
reference.html
206 lines (187 loc) · 7.58 KB
/
reference.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>Tactics Reference</title>
<style>
sub, sup { font-size: 75%; line-height: 0; position: relative; vertical-align: baseline; } sup { top: -0.5em; } sub { bottom: -0.25em; }
</style>
</head>
<h2> Coq Tactics </h2>
<h3> Manipulating the Context </h3>
<table border="1" width="100%">
<col width="10%">
<col width="15%">
<col width="75%">
<tr>
<th>Tactic</th>
<th>Arguments</th>
<th>Effect</th>
</tr>
<tr>
<td><a href="https://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic28">intros</a></td>
<td><i>n<sub>1</sub> ... n<sub>n</sub></i></td>
<td>Introduce terms into the context, giving them
names <i>n<sub>1</sub></i> through <i>n<sub>n</sub></i></td>
</tr>
<tr>
<td><a href="https://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic39">revert</a></td>
<td><i>n<sub>1</sub> ... n<sub>n</sub></i></td>
<td>The opposite of intros, removes terms from context and quantifies over them in the goal.</td>
</tr>
<tr>
<td><a href="s://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic36">clear</a></td>
<td><i>n<sub>1</sub> ... n<sub>n</sub></i></td>
<td>Deletes the terms <i>n<sub>1</sub></i> through <i>n<sub>n</sub></i> from the context.</td>
</tr>
<tr>
<td><a href="https://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic137">unfold</a></td>
<td><i>name</i></td>
<td>Replaces the function <i>name</i> with its underlying definition.</td>
</tr>
<!-- <tr>
<td></td>
<td><i>name</i> in <i>H</i></td>
<td>Unfolds <i>name</i> in hypothesis <i>H</i>.</td>
</tr>
<tr>
<td></td>
<td><i>name</i> in *</td>
<td>Unfolds <i>name</i> in the goal and all hypotheses.</td>
</tr> -->
</table>
<!-- other options to include:
revert
generalize dependent
subst
remember
-->
<h3> Making Progress </h3>
<table border="1" width="100%">
<col width="10%">
<col width="15%">
<col width="75%">
<tr>
<td><a href="https://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic135">simpl</a></td>
<td></td>
<td>Simplifies the goal</td>
</tr>
<tr>
<td><a href="s://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic65">destruct</a></td>
<td><i>x</i></td>
<td>Considers all possible constructors of the term <i>x</i>, generating subgoals that need to be solved separately.</td>
</tr>
<tr>
<td></td>
<td><i>x</i> eqn:<i>eq</i></td>
<td>Destructs x, remembers which constructor is being considered in the equality hypothesis <i>eq</i>.</td>
<tr>
<td><a href="s://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic71">induction</a></td>
<td><i>x</i> as [ | <i>n<sub>1</sub> IH<sub>1</sub></i> | <i>n<sub>2</sub> IH<sub>2</sub></i> | ...] <td>Same as destruct but adds an inductive hypothesis to inductively defined cases. Names the variables and inductive hypotheses generated by induction with the given names.</td>
</tr>
<tr>
<td><a href="s://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic109">rewrite</a></td>
<td><i>H</i></td>
<td>Where <i>H</i> is of type <i>e<sub>1</sub> = e<sub>2</sub></i>, replaces <i>e<sub>1</sub></i> in the goal with <i>e<sub>2</sub></i>.</td>
</tr>
<tr>
<td></td>
<td> <- <i>H</i> </td>
<td>Replaces <i>e<sub>2</sub></i> with <i>e<sub>1</sub></i></td>
</tr>
<!-- <tr>
<td></td>
<td> (<i>H</i> <i>n</i>) </td>
<td>Where <i>H</i> is of type <i>forall x, e<sub>1</sub> = e<sub>2</sub></i>: Substitutes <i>n</i> for <i>x</i> in the rewrite.</td>
</tr> -->
<tr>
<td><a href="s://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic8">apply</a></td>
<td><i>H</i></td>
<td>Uses lemma or hypothesis <i>H</i> to solve the goal. If <i>H</i> has hypotheses, adds them as new goals.</td>
</tr>
<tr>
<td></td>
<td><i>PQ</i> in <i>HP</i></td>
<td> Allows us to conclude <i>Q</i> from hypotheses <i>P -> Q</i> and <i>P</i>. (In logic, <i>modus ponens</i>.)</td>
</tr>
<!-- apply in and apply with? -->
<tr>
<td><a href="s://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic87">inversion</a></td>
<td><i>H</i></td>
<td>If hypothesis <i>H</i> states that <i>e1 = e2</i>, where <i>e1</i> and <i>e2</i> are expressions that start with different constructors, then inversion <i>H</i> completes the current subgoal. If they start with the same constructor, it generates hypotheses relating the subterms.</td>
</tr>
<tr>
<td><a href="https://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic49">assert</a></td>
<td><i>H</i> : <i>P</i></td>
<td>Adds a new hypothesis <i>H</i> that <i>P</i> is true to the goal. Adds the new subgoal <i>P</i> as the current goal.</td>
</tr>
</table>
<!-- other options to include:
split
left, right
refine - Bonus
-->
<h3> Solving the Goal </h3>
<table border="1" width="100%">
<col width="10%">
<col width="90%">
<tr>
<th>Tactic</th>
<th>Effect</th>
</tr>
<tr>
<td><a href="s://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic118">reflexivity</a></td>
<td>Solves a goal of the form <i>x = x</i>.</td>
</tr>
<tr>
<td><a href="s://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic5">assumption</a></td>
<td> If we have a hypothesis that is equal to the goal, solves the goal. </td>
</tr>
<tr>
<td><a href="https://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic82">discriminate</a></td>
<td> If we have a contradictory hypothesis involving an equality, solves the goal. (A special case of the logical <i>ex falso quodlibet</i>.)</td>
</tr>
<tr>
<td><a href="https://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic62">contradiction</a></td>
<td> If we have a contradictory hypothesis not involving an equality, solves the goal. (A special case of the logical <i>ex falso quodlibet</i>.) </td>
</tr>
<tr>
<td><a href="https://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic142">trivial</a></td>
<td>Checks if the goal is trivially true or equivalent to a hypothesis, solves if so. Otherwise, does nothing (does not fail).</td>
</tr>
<tr>
<td><a href="https://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic141">auto</a></td>
<td>Tries a collection of basic tactics to solve the goal. Otherwise, does nothing (does not fail).</td>
</tr>
<tr>
<td><a href="https://coq.inria.fr/refman/Reference-Manual023.html#hevea_tactic193">congruence</a></td>
<td>A powerful automation technique that subsumes reflexivity, assumption, discriminate and contradiction.</td>
</tr>
<tr>
<tr>
<td><a href="https://coq.inria.fr/refman/Reference-Manual023.html#hevea_tactic193">omega</a></td>
<td>Solves arithmetic equations over natural numbers.</td>
</tr>
<tr>
<td><a href="https://coq.inria.fr/refman/Reference-Manual023.html#hevea_tactic193">lia</a></td>
<td>A more powerful sibling of omega.</td>
</tr>
<!-- other options to include:
auto with hints
auto with depth change
tauto
intuition
congruence
ring
lra
crush
-->
</table>
<!-- Tacticals
;
try
repeat
-->
<p>Note that these are often special cases and simplifications. Click through to the <a href="https://coq.inria.fr/refman/tactic-index.html">Coq documentation</a> for a description of the tactics' general behavior and underlying theory.</p>
<p>Also see Adam Chlipala's <a href="http://adam.chlipala.net/itp/tactic-reference.html">Coq Tactics Quick Reference</a> for additional tactics and automation.</p>
</html>