package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module TacticsSource

Main tactics defined in ML. This file is huge and should probably be split in more reasonable units at some point. Because of its size and age, the implementation features various styles and stages of the proof engine. This has to be uniformized someday.

General functions.
Sourceval is_quantified_hypothesis : Names.Id.t -> Proofview.Goal.t -> bool
Primitive tactics.
Sourceval introduction : Names.Id.t -> unit Proofview.tactic
Sourceval convert_concl : cast:bool -> check:bool -> EConstr.types -> Constr.cast_kind -> unit Proofview.tactic
Sourceval convert_hyp : check:bool -> reorder:bool -> EConstr.named_declaration -> unit Proofview.tactic
Sourceval mutual_fix : Names.Id.t -> int -> (Names.Id.t * int * EConstr.constr) list -> int -> unit Proofview.tactic
Sourceval fix : Names.Id.t -> int -> unit Proofview.tactic
Sourceval mutual_cofix : Names.Id.t -> (Names.Id.t * EConstr.constr) list -> int -> unit Proofview.tactic
Introduction tactics.
Sourceval fresh_id_in_env : Names.Id.Set.t -> Names.Id.t -> Environ.env -> Names.Id.t
Sourceval find_intro_names : Environ.env -> Evd.evar_map -> EConstr.rel_context -> Names.Id.t list
Sourceval intro : unit Proofview.tactic
Sourceval introf : unit Proofview.tactic
Sourceval intro_avoiding : Names.Id.Set.t -> unit Proofview.tactic

intro_avoiding idl acts as intro but prevents the new Id.t to belong to idl

Sourceval intro_replacing : Names.Id.t -> unit Proofview.tactic
Sourceval intro_using : Names.Id.t -> unit Proofview.tactic
  • deprecated Prefer [intro_using_then] to avoid renaming issues.
Sourceval intro_using_then : Names.Id.t -> (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval intro_mustbe_force : Names.Id.t -> unit Proofview.tactic
Sourceval intros_mustbe_force : Names.Id.t list -> unit Proofview.tactic
Sourceval intro_then : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval intros_using : Names.Id.t list -> unit Proofview.tactic
  • deprecated Prefer [intros_using_then] to avoid renaming issues.
Sourceval intros_using_then : Names.Id.t list -> (Names.Id.t list -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval intros_replacing : Names.Id.t list -> unit Proofview.tactic
Sourceval intros_possibly_replacing : Names.Id.t list -> unit Proofview.tactic
Sourceval auto_intros_tac : Names.Name.t list -> unit Proofview.tactic

auto_intros_tac names handles Automatic Introduction of binders

Sourceval intros : unit Proofview.tactic
Sourceval intros_clearing : bool list -> unit Proofview.tactic

Assuming a tactic tac depending on an hypothesis Id.t, 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

Sourcetype evars_flag = bool
Sourcetype rec_flag = bool
Sourcetype advanced_flag = bool
Sourcetype clear_flag = bool option

Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings

Sourcetype 'a core_destruction_arg =
  1. | ElimOnConstr of 'a
  2. | ElimOnIdent of Names.lident
  3. | ElimOnAnonHyp of int
Sourcetype 'a destruction_arg = clear_flag * 'a core_destruction_arg

Tell if a used hypothesis should be cleared by default or not

Sourceval use_clear_hyp_by_default : unit -> bool
Introduction tactics with eliminations.

Implements user-level "intros", with standing for "**"

Exact tactics.
Sourceval assumption : unit Proofview.tactic
Sourceval exact_no_check : EConstr.constr -> unit Proofview.tactic
Sourceval vm_cast_no_check : EConstr.constr -> unit Proofview.tactic
Sourceval native_cast_no_check : EConstr.constr -> unit Proofview.tactic
Sourceval exact_check : EConstr.constr -> unit Proofview.tactic
Reduction tactics.
Sourcetype e_tactic_reduction = Reductionops.e_reduction_function
Sourceval make_change_arg : EConstr.constr -> change_arg
Sourceval reduct_in_hyp : check:bool -> reorder:bool -> tactic_reduction -> Locus.hyp_location -> unit Proofview.tactic
Sourceval reduct_option : check:bool -> (tactic_reduction * Constr.cast_kind) -> Locus.goal_location -> unit Proofview.tactic
Sourceval reduct_in_concl : cast:bool -> check:bool -> (tactic_reduction * Constr.cast_kind) -> unit Proofview.tactic
Sourceval e_reduct_in_concl : cast:bool -> check:bool -> (e_tactic_reduction * Constr.cast_kind) -> unit Proofview.tactic
Sourceval change_in_concl : check:bool -> (Locus.occurrences * Pattern.constr_pattern) option -> change_arg -> unit Proofview.tactic
Sourceval change_concl : EConstr.constr -> unit Proofview.tactic
Sourceval change_in_hyp : check:bool -> (Locus.occurrences * Pattern.constr_pattern) option -> change_arg -> Locus.hyp_location -> unit Proofview.tactic
Sourceval red_in_concl : unit Proofview.tactic
Sourceval hnf_in_concl : unit Proofview.tactic
Sourceval simpl_in_concl : unit Proofview.tactic
Sourceval simpl_in_hyp : Locus.hyp_location -> unit Proofview.tactic
Sourceval simpl_option : Locus.goal_location -> unit Proofview.tactic
Sourceval normalise_in_concl : unit Proofview.tactic
Sourceval normalise_in_hyp : Locus.hyp_location -> unit Proofview.tactic
Sourceval normalise_option : Locus.goal_location -> unit Proofview.tactic
Sourceval normalise_vm_in_concl : unit Proofview.tactic
Sourceval change : check:bool -> Pattern.constr_pattern option -> change_arg -> Locus.clause -> unit Proofview.tactic
Sourceval unfold_constr : Names.GlobRef.t -> unit Proofview.tactic
Modification of the local context.
Sourceval clear : Names.Id.t list -> unit Proofview.tactic
Sourceval clear_body : Names.Id.t list -> unit Proofview.tactic
Sourceval unfold_body : Names.Id.t -> unit Proofview.tactic
Sourceval keep : Names.Id.t list -> unit Proofview.tactic
Sourceval apply_clear_request : clear_flag -> bool -> Names.Id.t option -> unit Proofview.tactic
Sourceval rename_hyp : (Names.Id.t * Names.Id.t) list -> unit Proofview.tactic
Sourceval revert : Names.Id.t list -> unit Proofview.tactic
Resolution tactics.
Sourceval apply_type : typecheck:bool -> EConstr.constr -> EConstr.constr list -> unit Proofview.tactic
Sourceval eapply : ?with_classes:bool -> EConstr.constr -> unit Proofview.tactic
Sourceval apply_with_bindings_gen : ?with_classes:bool -> advanced_flag -> evars_flag -> (clear_flag * EConstr.constr Tactypes.with_bindings CAst.t) list -> unit Proofview.tactic
Sourceval eapply_with_bindings : ?with_classes:bool -> EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic
Sourceval cut_and_apply : EConstr.constr -> unit Proofview.tactic
Elimination tactics.
Sourcetype elim_scheme = {
  1. elimt : EConstr.types;
  2. indref : Names.GlobRef.t option;
  3. params : EConstr.rel_context;
    (*

    (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp)

    *)
  4. nparams : int;
    (*

    number of parameters

    *)
  5. predicates : EConstr.rel_context;
    (*

    (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...)

    *)
  6. npredicates : int;
    (*

    Number of predicates

    *)
  7. branches : EConstr.rel_context;
    (*

    branchr,...,branch1

    *)
  8. nbranches : int;
    (*

    Number of branches

    *)
  9. args : EConstr.rel_context;
    (*

    (xni, Ti_ni) ... (x1, Ti_1)

    *)
  10. nargs : int;
    (*

    number of arguments

    *)
  11. indarg : EConstr.rel_declaration option;
    (*

    Some (H,I prm1..prmp x1...xni) if HI is in premisses, None otherwise

    *)
  12. concl : EConstr.types;
    (*

    Qi x1...xni HI (f...), HI and (f...) are optional and mutually exclusive

    *)
  13. indarg_in_concl : bool;
    (*

    true if HI appears at the end of conclusion

    *)
  14. farg_in_concl : bool;
    (*

    true if (f...) appears at the end of conclusion

    *)
}

rel_contexts and rel_declaration actually contain triples, and lists are actually in reverse order to fit compose_prod.

Sourceval compute_elim_sig : Evd.evar_map -> EConstr.types -> elim_scheme
Sourceval simplest_elim : EConstr.constr -> unit Proofview.tactic
Case analysis tactics.
Sourceval simplest_case : EConstr.constr -> unit Proofview.tactic
Generic case analysis / induction tactics.

Implements user-level "destruct" and "induction"

Eliminations giving the type instead of the proof.
Sourceval case_type : EConstr.types -> unit Proofview.tactic
Sourceval elim_type : EConstr.types -> unit Proofview.tactic
Constructor tactics.
Sourceval constructor_tac : evars_flag -> int option -> int -> EConstr.constr Tactypes.bindings -> unit Proofview.tactic
Sourceval any_constructor : evars_flag -> unit Proofview.tactic option -> unit Proofview.tactic
Sourceval one_constructor : int -> EConstr.constr Tactypes.bindings -> unit Proofview.tactic
Sourceval split_with_bindings : evars_flag -> EConstr.constr Tactypes.bindings list -> unit Proofview.tactic
Sourceval simplest_left : unit Proofview.tactic
Sourceval simplest_right : unit Proofview.tactic
Sourceval simplest_split : unit Proofview.tactic
Equality tactics.
Sourceval setoid_reflexivity : unit Proofview.tactic Hook.t
Sourceval reflexivity_red : bool -> unit Proofview.tactic
Sourceval reflexivity : unit Proofview.tactic
Sourceval intros_reflexivity : unit Proofview.tactic
Sourceval setoid_symmetry : unit Proofview.tactic Hook.t
Sourceval symmetry_red : bool -> unit Proofview.tactic
Sourceval symmetry : unit Proofview.tactic
Sourceval setoid_symmetry_in : (Names.Id.t -> unit Proofview.tactic) Hook.t
Sourceval intros_symmetry : Locus.clause -> unit Proofview.tactic
Sourceval setoid_transitivity : (EConstr.constr option -> unit Proofview.tactic) Hook.t
Sourceval transitivity_red : bool -> EConstr.constr option -> unit Proofview.tactic
Sourceval transitivity : EConstr.constr -> unit Proofview.tactic
Sourceval etransitivity : unit Proofview.tactic
Sourceval intros_transitivity : EConstr.constr option -> unit Proofview.tactic
Cut tactics.
Sourceval assert_before_replacing : Names.Id.t -> EConstr.types -> unit Proofview.tactic
Sourceval assert_after_replacing : Names.Id.t -> EConstr.types -> unit Proofview.tactic
Sourceval assert_before : Names.Name.t -> EConstr.types -> unit Proofview.tactic
Sourceval assert_after : Names.Name.t -> EConstr.types -> unit Proofview.tactic
Sourceval assert_as : bool -> Names.Id.t option -> Tactypes.intro_pattern option -> EConstr.constr -> unit Proofview.tactic

Implements the tactics assert, enough and pose proof; note that "by" applies on the first goal for both assert and enough

Common entry point for user-level "assert", "enough" and "pose proof"

Sourceval forward : bool -> unit Proofview.tactic option option -> Tactypes.intro_pattern option -> EConstr.constr -> unit Proofview.tactic

Implements the tactic cut, actually a modus ponens rule

Tactics for adding local definitions.

Common entry point for user-level "set", "pose" and "remember"

Generalize tactics.
Sourceval generalize : EConstr.constr list -> unit Proofview.tactic
Sourceval new_generalize_gen : ((Locus.occurrences * EConstr.constr) * Names.Name.t) list -> unit Proofview.tactic
Sourceval generalize_dep : ?with_let:bool -> EConstr.constr -> unit Proofview.tactic
Other tactics.
Sourceval constr_eq : strict:bool -> EConstr.constr -> EConstr.constr -> unit Proofview.tactic

Syntactic equality up to universes. With strict the universe constraints must be already true to succeed, without strict they are added to the evar map.

Sourceval abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Names.Id.t -> unit Proofview.tactic
Sourceval specialize_eqs : Names.Id.t -> unit Proofview.tactic
Sourceval general_rewrite_clause : (bool -> evars_flag -> EConstr.constr Tactypes.with_bindings -> Locus.clause -> unit Proofview.tactic) Hook.t
Sourceval subst_one : (bool -> Names.Id.t -> (Names.Id.t * EConstr.constr * bool) -> unit Proofview.tactic) Hook.t
Sourceval declare_intro_decomp_eq : ((int -> unit Proofview.tactic) -> (Coqlib.coq_eq_data * EConstr.types * (EConstr.types * EConstr.constr * EConstr.constr)) -> (EConstr.constr * EConstr.types) -> unit Proofview.tactic) -> unit
Sourceval with_set_strategy : (Conv_oracle.level * Names.GlobRef.t list) list -> 'a Proofview.tactic -> 'a Proofview.tactic

Tactic analogous to the Strategy vernacular, but only applied locally to the tactic argument

Simple form of basic tactics.
Sourcemodule Simple : sig ... end

Simplified version of some of the above tactics

Tacticals defined directly in term of Proofview
Sourceval refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic

refine ~typecheck c is Refine.refine ~typecheck c followed by beta-iota-reduction of the conclusion.

Sourceval reduce_after_refine : unit Proofview.tactic

The reducing tactic called after refine.