blob: 6e67a9cda4cd55f967eafd0f361d5af7174a1cb4 (
plain)
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
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: tactics.mli,v 1.59.2.1 2004/07/16 19:30:55 herbelin Exp $ i*)
(*i*)
open Names
open Term
open Environ
open Sign
open Tacmach
open Proof_type
open Reduction
open Evd
open Evar_refiner
open Clenv
open Tacred
open Tacticals
open Libnames
open Genarg
open Tacexpr
open Nametab
open Rawterm
(* Main tactics. *)
(*s General functions. *)
val type_clenv_binding : named_context sigma ->
constr * constr -> constr bindings -> constr
val string_of_inductive : constr -> string
val head_constr : constr -> constr list
val head_constr_bound : constr -> constr list -> constr list
val is_quantified_hypothesis : identifier -> goal sigma -> bool
exception Bound
(*s Primitive tactics. *)
val introduction : identifier -> tactic
val refine : constr -> tactic
val convert_concl : constr -> tactic
val convert_hyp : named_declaration -> tactic
val thin : identifier list -> tactic
val mutual_fix :
identifier -> int -> (identifier * int * constr) list -> tactic
val fix : identifier option -> int -> tactic
val mutual_cofix : identifier -> (identifier * constr) list -> tactic
val cofix : identifier option -> tactic
(*s Introduction tactics. *)
val fresh_id : identifier list -> identifier -> goal sigma -> identifier
val intro : tactic
val introf : tactic
val intro_force : bool -> tactic
val intro_move : identifier option -> identifier option -> tactic
val intro_replacing : identifier -> tactic
val intro_using : identifier -> tactic
val intro_mustbe_force : identifier -> tactic
val intros_using : identifier list -> tactic
val intro_erasing : identifier -> tactic
val intros_replacing : identifier list -> tactic
val intros : tactic
(* [depth_of_quantified_hypothesis b h g] returns the index of [h] in
the conclusion of goal [g], up to head-reduction if [b] is [true] *)
val depth_of_quantified_hypothesis :
bool -> quantified_hypothesis -> goal sigma -> int
val intros_until_n_wored : int -> tactic
val intros_until : quantified_hypothesis -> tactic
val intros_clearing : bool list -> tactic
(* Assuming a tactic [tac] depending on an hypothesis identifier,
[try_intros_until tac arg] first assumes that arg denotes a
quantified hypothesis (denoted by name or by index) and try to
introduce it in context before to apply [tac], otherwise assume the
hypothesis is already in context and directly apply [tac] *)
val try_intros_until :
(identifier -> tactic) -> quantified_hypothesis -> tactic
(*s Introduction tactics with eliminations. *)
val intro_pattern : identifier option -> intro_pattern_expr -> tactic
val intro_patterns : intro_pattern_expr list -> tactic
val intros_pattern : identifier option -> intro_pattern_expr list -> tactic
(*s Exact tactics. *)
val assumption : tactic
val exact_no_check : constr -> tactic
val exact_check : constr -> tactic
val exact_proof : Topconstr.constr_expr -> tactic
(*s Reduction tactics. *)
type tactic_reduction = env -> evar_map -> constr -> constr
val reduct_in_hyp : tactic_reduction -> hyp_location -> tactic
val reduct_option : tactic_reduction -> simple_clause -> tactic
val reduct_in_concl : tactic_reduction -> tactic
val change_in_concl : constr occurrences option -> constr -> tactic
val change_in_hyp : constr occurrences option -> constr -> hyp_location ->
tactic
val red_in_concl : tactic
val red_in_hyp : hyp_location -> tactic
val red_option : simple_clause -> tactic
val hnf_in_concl : tactic
val hnf_in_hyp : hyp_location -> tactic
val hnf_option : simple_clause -> tactic
val simpl_in_concl : tactic
val simpl_in_hyp : hyp_location -> tactic
val simpl_option : simple_clause -> tactic
val normalise_in_concl: tactic
val normalise_in_hyp : hyp_location -> tactic
val normalise_option : simple_clause -> tactic
val unfold_in_concl : (int list * evaluable_global_reference) list -> tactic
val unfold_in_hyp :
(int list * evaluable_global_reference) list -> hyp_location -> tactic
val unfold_option :
(int list * evaluable_global_reference) list -> simple_clause
-> tactic
val reduce : red_expr -> clause -> tactic
val change :
constr occurrences option -> constr -> clause -> tactic
val unfold_constr : global_reference -> tactic
val pattern_option : (int list * constr) list -> simple_clause -> tactic
(*s Modification of the local context. *)
val clear : identifier list -> tactic
val clear_body : identifier list -> tactic
val new_hyp : int option -> constr with_bindings -> tactic
val move_hyp : bool -> identifier -> identifier -> tactic
val rename_hyp : identifier -> identifier -> tactic
(*s Resolution tactics. *)
val apply_type : constr -> constr list -> tactic
val apply_term : constr -> constr list -> tactic
val bring_hyps : named_context -> tactic
val apply : constr -> tactic
val apply_without_reduce : constr -> tactic
val apply_list : constr list -> tactic
val apply_with_bindings : constr with_bindings -> tactic
val cut_and_apply : constr -> tactic
(*s Elimination tactics. *)
val general_elim : constr with_bindings -> constr with_bindings ->
?allow_K:bool -> tactic
val default_elim : constr with_bindings -> tactic
val simplest_elim : constr -> tactic
val elim : constr with_bindings -> constr with_bindings option -> tactic
val general_elim_in : identifier -> constr * constr bindings ->
constr * constr bindings -> tactic
val simple_induct : quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref -> tactic
val general_elim_in : identifier -> constr * constr bindings ->
constr * constr bindings -> tactic
val new_induct : constr induction_arg -> constr with_bindings option ->
intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
-> tactic
(*s Case analysis tactics. *)
val general_case_analysis : constr with_bindings -> tactic
val simplest_case : constr -> tactic
val simple_destruct : quantified_hypothesis -> tactic
val new_destruct : constr induction_arg -> constr with_bindings option ->
intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
-> tactic
(*s Eliminations giving the type instead of the proof. *)
val case_type : constr -> tactic
val elim_type : constr -> tactic
(*s Some eliminations which are frequently used. *)
val impE : identifier -> tactic
val andE : identifier -> tactic
val orE : identifier -> tactic
val dImp : clause -> tactic
val dAnd : clause -> tactic
val dorE : bool -> clause ->tactic
(*s Introduction tactics. *)
val constructor_tac : int option -> int ->
constr bindings -> tactic
val one_constructor : int -> constr bindings -> tactic
val any_constructor : tactic option -> tactic
val left : constr bindings -> tactic
val simplest_left : tactic
val right : constr bindings -> tactic
val simplest_right : tactic
val split : constr bindings -> tactic
val simplest_split : tactic
(*s Logical connective tactics. *)
val reflexivity : tactic
val intros_reflexivity : tactic
val symmetry : tactic
val symmetry_in : identifier -> tactic
val intros_symmetry : clause -> tactic
val transitivity : constr -> tactic
val intros_transitivity : constr -> tactic
val cut : constr -> tactic
val cut_intro : constr -> tactic
val cut_replacing : identifier -> constr -> tactic
val cut_in_parallel : constr list -> tactic
val assert_tac : bool -> name -> constr -> tactic
val true_cut : name -> constr -> tactic
val letin_tac : bool -> name -> constr -> clause -> tactic
val forward : bool -> name -> constr -> tactic
val generalize : constr list -> tactic
val generalize_dep : constr -> tactic
val tclABSTRACT : identifier option -> tactic -> tactic
|
