1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: tactics.mli 11735 2009-01-02 17:22:31Z herbelin $ i*)
33
val inj_open : constr -> open_constr
34
val inj_red_expr : red_expr -> (open_constr, evaluable_global_reference) red_expr_gen
35
val inj_ebindings : constr bindings -> open_constr bindings
39
(*s General functions. *)
41
val type_clenv_binding : goal sigma ->
42
constr * constr -> open_constr bindings -> constr
44
val string_of_inductive : constr -> string
45
val head_constr : constr -> constr * constr list
46
val head_constr_bound : constr -> constr * constr list
47
val is_quantified_hypothesis : identifier -> goal sigma -> bool
51
(*s Primitive tactics. *)
53
val introduction : identifier -> tactic
54
val refine : constr -> tactic
55
val convert_concl : constr -> cast_kind -> tactic
56
val convert_hyp : named_declaration -> tactic
57
val thin : identifier list -> tactic
59
identifier -> int -> (identifier * int * constr) list -> tactic
60
val fix : identifier option -> int -> tactic
61
val mutual_cofix : identifier -> (identifier * constr) list -> tactic
62
val cofix : identifier option -> tactic
64
(*s Introduction tactics. *)
66
val fresh_id : identifier list -> identifier -> goal sigma -> identifier
67
val find_intro_names : rel_context -> goal sigma -> identifier list
71
val intro_force : bool -> tactic
72
val intro_move : identifier option -> identifier move_location -> tactic
74
(* [intro_avoiding idl] acts as intro but prevents the new identifier
76
val intro_avoiding : identifier list -> tactic
78
val intro_replacing : identifier -> tactic
79
val intro_using : identifier -> tactic
80
val intro_mustbe_force : identifier -> tactic
81
val intros_using : identifier list -> tactic
82
val intro_erasing : identifier -> tactic
83
val intros_replacing : identifier list -> tactic
87
(* [depth_of_quantified_hypothesis b h g] returns the index of [h] in
88
the conclusion of goal [g], up to head-reduction if [b] is [true] *)
89
val depth_of_quantified_hypothesis :
90
bool -> quantified_hypothesis -> goal sigma -> int
92
val intros_until_n_wored : int -> tactic
93
val intros_until : quantified_hypothesis -> tactic
95
val intros_clearing : bool list -> tactic
97
(* Assuming a tactic [tac] depending on an hypothesis identifier,
98
[try_intros_until tac arg] first assumes that arg denotes a
99
quantified hypothesis (denoted by name or by index) and try to
100
introduce it in context before to apply [tac], otherwise assume the
101
hypothesis is already in context and directly apply [tac] *)
103
val try_intros_until :
104
(identifier -> tactic) -> quantified_hypothesis -> tactic
106
(* Apply a tactic on a quantified hypothesis, an hypothesis in context
107
or a term with bindings *)
110
(constr with_ebindings -> tactic) ->
111
constr with_ebindings induction_arg -> tactic
113
(*s Introduction tactics with eliminations. *)
115
val intro_pattern : identifier move_location -> intro_pattern_expr -> tactic
116
val intro_patterns : intro_pattern_expr located list -> tactic
118
identifier move_location -> intro_pattern_expr located list -> tactic
120
(*s Exact tactics. *)
122
val assumption : tactic
123
val exact_no_check : constr -> tactic
124
val vm_cast_no_check : constr -> tactic
125
val exact_check : constr -> tactic
126
val exact_proof : Topconstr.constr_expr -> tactic
128
(*s Reduction tactics. *)
130
type tactic_reduction = env -> evar_map -> constr -> constr
132
val reduct_in_hyp : tactic_reduction -> hyp_location -> tactic
133
val reduct_option : tactic_reduction * cast_kind -> simple_clause -> tactic
134
val reduct_in_concl : tactic_reduction * cast_kind -> tactic
135
val change_in_concl : (occurrences * constr) option -> constr -> tactic
136
val change_in_hyp : (occurrences * constr) option -> constr ->
137
hyp_location -> tactic
138
val red_in_concl : tactic
139
val red_in_hyp : hyp_location -> tactic
140
val red_option : simple_clause -> tactic
141
val hnf_in_concl : tactic
142
val hnf_in_hyp : hyp_location -> tactic
143
val hnf_option : simple_clause -> tactic
144
val simpl_in_concl : tactic
145
val simpl_in_hyp : hyp_location -> tactic
146
val simpl_option : simple_clause -> tactic
147
val normalise_in_concl : tactic
148
val normalise_in_hyp : hyp_location -> tactic
149
val normalise_option : simple_clause -> tactic
150
val normalise_vm_in_concl : tactic
151
val unfold_in_concl :
152
(occurrences * evaluable_global_reference) list -> tactic
154
(occurrences * evaluable_global_reference) list -> hyp_location -> tactic
156
(occurrences * evaluable_global_reference) list -> simple_clause
159
(occurrences * constr) option -> constr -> clause -> tactic
161
(occurrences * constr) list -> simple_clause -> tactic
162
val reduce : red_expr -> clause -> tactic
163
val unfold_constr : global_reference -> tactic
165
(*s Modification of the local context. *)
167
val clear : identifier list -> tactic
168
val clear_body : identifier list -> tactic
169
val keep : identifier list -> tactic
171
val specialize : int option -> constr with_ebindings -> tactic
173
val move_hyp : bool -> identifier -> identifier move_location -> tactic
174
val rename_hyp : (identifier * identifier) list -> tactic
176
val revert : identifier list -> tactic
178
(*s Resolution tactics. *)
180
val apply_type : constr -> constr list -> tactic
181
val apply_term : constr -> constr list -> tactic
182
val bring_hyps : named_context -> tactic
184
val apply : constr -> tactic
185
val apply_without_reduce : constr -> tactic
186
val apply_list : constr list -> tactic
188
val apply_with_ebindings_gen :
189
advanced_flag -> evars_flag -> open_constr with_ebindings list -> tactic
191
val apply_with_bindings : constr with_bindings -> tactic
192
val eapply_with_bindings : constr with_bindings -> tactic
194
val apply_with_ebindings : open_constr with_ebindings -> tactic
195
val eapply_with_ebindings : open_constr with_ebindings -> tactic
197
val cut_and_apply : constr -> tactic
200
advanced_flag -> evars_flag -> identifier ->
201
open_constr with_ebindings list ->
202
intro_pattern_expr located option -> tactic
204
(*s Elimination tactics. *)
208
The general form of an induction principle is the following:
210
forall prm1 prm2 ... prmp, (induction parameters)
211
forall Q1...,(Qi:Ti_1 -> Ti_2 ->...-> Ti_ni),...Qq, (predicates)
212
branch1, branch2, ... , branchr, (branches of the principle)
213
forall (x1:Ti_1) (x2:Ti_2) ... (xni:Ti_ni), (induction arguments)
214
(HI: I prm1..prmp x1...xni) (optional main induction arg)
215
-> (Qi x1...xni HI (f prm1...prmp x1...xni)).(conclusion)
216
^^ ^^^^^^^^^^^^^^^^^^^^^^^^
218
even if HI argument added if principle
219
present above generated by functional induction
222
HI is not present when the induction principle does not come directly from an
223
inductive type (like when it is generated by functional induction for
224
example). HI is present otherwise BUT may not appear in the conclusion
225
(dependent principle). HI and (f...) cannot be both present.
227
Principles taken from functional induction have the final (f...).
230
(* [rel_contexts] and [rel_declaration] actually contain triples, and
231
lists are actually in reverse order to fit [compose_prod]. *)
233
elimc: constr with_ebindings option;
235
indref: global_reference option;
236
params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
237
nparams: int; (* number of parameters *)
238
predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
239
npredicates: int; (* Number of predicates *)
240
branches: rel_context; (* branchr,...,branch1 *)
241
nbranches: int; (* Number of branches *)
242
args: rel_context; (* (xni, Ti_ni) ... (x1, Ti_1) *)
243
nargs: int; (* number of arguments *)
244
indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni)
245
if HI is in premisses, None otherwise *)
246
concl: types; (* Qi x1...xni HI (f...), HI and (f...)
247
are optional and mutually exclusive *)
248
indarg_in_concl: bool; (* true if HI appears at the end of conclusion *)
249
farg_in_concl: bool; (* true if (f...) appears at the end of conclusion *)
253
val compute_elim_sig : ?elimc: constr with_ebindings -> types -> elim_scheme
254
val rebuild_elimtype_from_scheme: elim_scheme -> types
256
val general_elim : evars_flag ->
257
constr with_ebindings -> constr with_ebindings -> ?allow_K:bool -> tactic
258
val general_elim_in : evars_flag ->
259
identifier -> constr with_ebindings -> constr with_ebindings -> tactic
261
val default_elim : evars_flag -> constr with_ebindings -> tactic
262
val simplest_elim : constr -> tactic
264
evars_flag -> constr with_ebindings -> constr with_ebindings option -> tactic
266
val simple_induct : quantified_hypothesis -> tactic
268
val new_induct : evars_flag -> constr with_ebindings induction_arg list ->
269
constr with_ebindings option ->
270
intro_pattern_expr located option * intro_pattern_expr located option ->
271
clause option -> tactic
273
(*s Case analysis tactics. *)
275
val general_case_analysis : evars_flag -> constr with_ebindings -> tactic
276
val simplest_case : constr -> tactic
278
val simple_destruct : quantified_hypothesis -> tactic
279
val new_destruct : evars_flag -> constr with_ebindings induction_arg list ->
280
constr with_ebindings option ->
281
intro_pattern_expr located option * intro_pattern_expr located option ->
282
clause option -> tactic
284
(*s Generic case analysis / induction tactics. *)
286
val induction_destruct : evars_flag -> rec_flag ->
287
(constr with_ebindings induction_arg list *
288
constr with_ebindings option *
289
(intro_pattern_expr located option * intro_pattern_expr located option) *
290
clause option) list ->
293
(*s Eliminations giving the type instead of the proof. *)
295
val case_type : constr -> tactic
296
val elim_type : constr -> tactic
298
(*s Some eliminations which are frequently used. *)
300
val impE : identifier -> tactic
301
val andE : identifier -> tactic
302
val orE : identifier -> tactic
303
val dImp : clause -> tactic
304
val dAnd : clause -> tactic
305
val dorE : bool -> clause ->tactic
308
(*s Introduction tactics. *)
310
val constructor_tac : evars_flag -> int option -> int ->
311
open_constr bindings -> tactic
312
val any_constructor : evars_flag -> tactic option -> tactic
313
val one_constructor : int -> open_constr bindings -> tactic
315
val left : constr bindings -> tactic
316
val right : constr bindings -> tactic
317
val split : constr bindings -> tactic
319
val left_with_ebindings : evars_flag -> open_constr bindings -> tactic
320
val right_with_ebindings : evars_flag -> open_constr bindings -> tactic
321
val split_with_ebindings : evars_flag -> open_constr bindings -> tactic
323
val simplest_left : tactic
324
val simplest_right : tactic
325
val simplest_split : tactic
327
(*s Logical connective tactics. *)
329
val register_setoid_reflexivity : tactic -> unit
330
val reflexivity_red : bool -> goal sigma -> tactic option
331
val reflexivity : tactic
332
val intros_reflexivity : tactic
334
val register_setoid_symmetry : tactic -> unit
335
val symmetry_red : bool -> goal sigma -> tactic option
336
val symmetry : tactic
337
val register_setoid_symmetry_in : (identifier -> tactic) -> unit
338
val symmetry_in : identifier -> tactic
339
val intros_symmetry : clause -> tactic
341
val register_setoid_transitivity : (constr -> tactic) -> unit
342
val transitivity_red : bool -> constr -> goal sigma -> tactic option
343
val transitivity : constr -> tactic
344
val intros_transitivity : constr -> tactic
346
val cut : constr -> tactic
347
val cut_intro : constr -> tactic
349
identifier -> constr -> (tactic -> tactic) -> tactic
350
val cut_in_parallel : constr list -> tactic
352
val assert_as : bool -> intro_pattern_expr located option -> constr -> tactic
353
val forward : tactic option -> intro_pattern_expr located option -> constr -> tactic
354
val letin_tac : (bool * intro_pattern_expr located) option -> name ->
355
constr -> types option -> clause -> tactic
356
val assert_tac : name -> types -> tactic
357
val assert_by : name -> types -> tactic -> tactic
358
val pose_proof : name -> constr -> tactic
360
val generalize : constr list -> tactic
361
val generalize_gen : ((occurrences * constr) * name) list -> tactic
362
val generalize_dep : constr -> tactic
364
val unify : ?state:Names.transparent_state -> constr -> constr -> tactic
365
val resolve_classes : tactic
367
val tclABSTRACT : identifier option -> tactic -> tactic
369
val admit_as_an_axiom : tactic
371
val abstract_generalize : identifier -> ?generalize_vars:bool -> tactic
373
val dependent_pattern : constr -> tactic
375
val register_general_multi_rewrite :
376
(bool -> evars_flag -> open_constr with_bindings -> clause -> tactic) -> unit
added
removed
tactics/tactics.mli
