diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 108 |
1 files changed, 84 insertions, 24 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 1155d845..5d04da9a 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tactics.mli,v 1.59.2.2 2005/01/21 16:41:52 herbelin Exp $ i*) +(*i $Id: tactics.mli 8698 2006-04-11 15:12:48Z jforest $ i*) (*i*) open Names @@ -19,7 +19,7 @@ open Reduction open Evd open Evar_refiner open Clenv -open Tacred +open Redexpr open Tacticals open Libnames open Genarg @@ -32,7 +32,7 @@ open Rawterm (*s General functions. *) -val type_clenv_binding : named_context sigma -> +val type_clenv_binding : goal sigma -> constr * constr -> constr bindings -> constr val string_of_inductive : constr -> string @@ -46,7 +46,7 @@ exception Bound val introduction : identifier -> tactic val refine : constr -> tactic -val convert_concl : constr -> tactic +val convert_concl : constr -> cast_kind -> tactic val convert_hyp : named_declaration -> tactic val thin : identifier list -> tactic val mutual_fix : @@ -63,6 +63,9 @@ val intro : tactic val introf : tactic val intro_force : bool -> tactic val intro_move : identifier option -> identifier option -> tactic + (* [intro_avoiding idl] acts as intro but prevents the new identifier + to belong to [idl] *) +val intro_avoiding : identifier list -> tactic val intro_replacing : identifier -> tactic val intro_using : identifier -> tactic @@ -110,8 +113,8 @@ val exact_proof : Topconstr.constr_expr -> tactic 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 reduct_option : tactic_reduction * cast_kind -> simple_clause -> tactic +val reduct_in_concl : tactic_reduction * cast_kind -> tactic val change_in_concl : constr occurrences option -> constr -> tactic val change_in_hyp : constr occurrences option -> constr -> hyp_location -> tactic @@ -124,9 +127,10 @@ 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_concl : tactic val normalise_in_hyp : hyp_location -> tactic val normalise_option : simple_clause -> tactic +val normalise_vm_in_concl : 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 @@ -144,6 +148,7 @@ val pattern_option : (int list * constr) list -> simple_clause -> tactic val clear : identifier list -> tactic val clear_body : identifier list -> tactic +val keep : identifier list -> tactic val new_hyp : int option -> constr with_bindings -> tactic @@ -165,21 +170,67 @@ val cut_and_apply : constr -> tactic (*s Elimination tactics. *) -val general_elim : constr with_bindings -> constr with_bindings -> - ?allow_K:bool -> tactic + +(* + The general form of an induction principle is the following: + + forall prm1 prm2 ... prmp, (induction parameters) + forall Q1...,(Qi:Ti_1 -> Ti_2 ->...-> Ti_ni),...Qq, (predicates) + branch1, branch2, ... , branchr, (branches of the principle) + forall (x1:Ti_1) (x2:Ti_2) ... (xni:Ti_ni), (induction arguments) + (HI: I prm1..prmp x1...xni) (optional main induction arg) + -> (Qi x1...xni HI (f prm1...prmp x1...xni)).(conclusion) + ^^ ^^^^^^^^^^^^^^^^^^^^^^^^ + optional optional + even if HI argument added if principle + present above generated by functional induction + [indarg] [farg] + + HI is not present when the induction principle does not come directly from an + inductive type (like when it is generated by functional induction for + example). HI is present otherwise BUT may not appear in the conclusion + (dependent principle). HI and (f...) cannot be both present. + + Principles taken from functional induction have the final (f...). +*) + +(* [rel_contexts] and [rel_declaration] actually contain triples, and + lists are actually in reverse order to fit [compose_prod]. *) +type elim_scheme = { + elimc: (Term.constr * constr Rawterm.bindings) option; + elimt: types; + indref: global_reference option; + params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) + nparams: int; (* number of parameters *) + predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) + npredicates: int; (* Number of predicates *) + branches: rel_context; (* branchr,...,branch1 *) + nbranches: int; (* Number of branches *) + args: rel_context; (* (xni, Ti_ni) ... (x1, Ti_1) *) + nargs: int; (* number of arguments *) + indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni) + if HI is in premisses, None otherwise *) + concl: types; (* Qi x1...xni HI (f...), HI and (f...) + are optional and mutually exclusive *) + indarg_in_concl: bool; (* true if HI appears at the end of conclusion *) + farg_in_concl: bool; (* true if (f...) appears at the end of conclusion *) +} + + +val compute_elim_sig : ?elimc: (Term.constr * constr Rawterm.bindings) -> types -> elim_scheme + +val general_elim : + constr with_bindings -> constr with_bindings -> ?allow_K:bool -> tactic +val general_elim_in : + identifier -> constr with_bindings -> constr with_bindings -> 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 -> 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 +val new_induct : constr induction_arg list -> constr with_bindings option -> + intro_pattern_expr -> tactic (*s Case analysis tactics. *) @@ -187,9 +238,8 @@ 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 +val new_destruct : constr induction_arg list -> constr with_bindings option -> + intro_pattern_expr -> tactic (*s Eliminations giving the type instead of the proof. *) @@ -221,26 +271,36 @@ val simplest_split : tactic (*s Logical connective tactics. *) +val register_setoid_reflexivity : tactic -> unit val reflexivity : tactic val intros_reflexivity : tactic +val register_setoid_symmetry : tactic -> unit val symmetry : tactic +val register_setoid_symmetry_in : (identifier -> tactic) -> unit val symmetry_in : identifier -> tactic val intros_symmetry : clause -> tactic +val register_setoid_transitivity : (constr -> tactic) -> unit 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_replacing : + identifier -> constr -> (tactic -> tactic) -> tactic val cut_in_parallel : constr list -> tactic -val assert_tac : bool -> name -> constr -> tactic +val assert_as : bool -> intro_pattern_expr -> constr -> tactic +val forward : tactic option -> intro_pattern_expr -> constr -> tactic + val true_cut : name -> constr -> tactic val letin_tac : bool -> name -> constr -> clause -> tactic -val forward : bool -> name -> constr -> tactic +val assert_tac : bool -> name -> constr -> tactic val generalize : constr list -> tactic val generalize_dep : constr -> tactic val tclABSTRACT : identifier option -> tactic -> tactic + +val admit_as_an_axiom : tactic + |