package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.14.1.tar.gz

sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

doc/coq-core.tactics/Tactics/index.html

Module `Tactics`Source

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

val convert_concl : 
  check:bool ->
  EConstr.types ->
  Constr.cast_kind ->
  unit Proofview.tactic

val convert_hyp : 
  check:bool ->
  reorder:bool ->
  EConstr.named_declaration ->
  unit Proofview.tactic

val 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

val mutual_cofix : 
  Names.Id.t ->
  (Names.Id.t * EConstr.constr) list ->
  int ->
  unit Proofview.tactic

Sourceval cofix : Names.Id.t -> unit Proofview.tactic

Sourceval convert : EConstr.constr -> EConstr.constr -> unit Proofview.tactic

Sourceval convert_leq : EConstr.constr -> EConstr.constr -> unit Proofview.tactic

Introduction tactics.

Sourceval fresh_id_in_env : Names.Id.Set.t -> Names.Id.t -> Environ.env -> Names.Id.t

val fresh_id : 
  Names.Id.Set.t ->
  Names.Id.t ->
  Goal.goal Evd.sigma ->
  Names.Id.t

val find_intro_names : 
  EConstr.rel_context ->
  Goal.goal Evd.sigma ->
  Names.Id.t list

Sourceval intro : unit Proofview.tactic

Sourceval introf : unit Proofview.tactic

val intro_move : 
  Names.Id.t option ->
  Names.Id.t Logic.move_location ->
  unit Proofview.tactic

val intro_move_avoid : 
  Names.Id.t option ->
  Names.Id.Set.t ->
  Names.Id.t Logic.move_location ->
  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.

val 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.

val 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_until : Tactypes.quantified_hypothesis -> 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

val try_intros_until : 
  (Names.Id.t -> unit Proofview.tactic) ->
  Tactypes.quantified_hypothesis ->
  unit Proofview.tactic

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 =

| ElimOnConstr of 'a
| ElimOnIdent of Names.lident
| ElimOnAnonHyp of int

Sourcetype 'a destruction_arg = clear_flag * 'a core_destruction_arg

val onInductionArg : 
  (clear_flag ->
    EConstr.constr Tactypes.with_bindings ->
    unit Proofview.tactic) ->
  EConstr.constr Tactypes.with_bindings destruction_arg ->
  unit Proofview.tactic

val force_destruction_arg : 
  evars_flag ->
  Environ.env ->
  Evd.evar_map ->
  Tactypes.delayed_open_constr_with_bindings destruction_arg ->
  Evd.evar_map * EConstr.constr Tactypes.with_bindings 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.

val intro_patterns : 
  evars_flag ->
  Tactypes.intro_patterns ->
  unit Proofview.tactic

val intro_patterns_to : 
  evars_flag ->
  Names.Id.t Logic.move_location ->
  Tactypes.intro_patterns ->
  unit Proofview.tactic

val intro_patterns_bound_to : 
  evars_flag ->
  int ->
  Names.Id.t Logic.move_location ->
  Tactypes.intro_patterns ->
  unit Proofview.tactic

val intro_pattern_to : 
  evars_flag ->
  Names.Id.t Logic.move_location ->
  Tactypes.delayed_open_constr Tactypes.intro_pattern_expr ->
  unit Proofview.tactic

val intros_patterns : 
  evars_flag ->
  Tactypes.intro_patterns ->
  unit Proofview.tactic

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

Sourceval exact_proof : Constrexpr.constr_expr -> unit Proofview.tactic

Reduction tactics.

Sourcetype tactic_reduction = Reductionops.reduction_function

Sourcetype e_tactic_reduction = Reductionops.e_reduction_function

type change_arg =
  Ltac_pretype.patvar_map ->
  Environ.env ->
  Evd.evar_map ->
  Evd.evar_map * EConstr.constr

Sourceval make_change_arg : EConstr.constr -> change_arg

val reduct_in_hyp : 
  check:bool ->
  reorder:bool ->
  tactic_reduction ->
  Locus.hyp_location ->
  unit Proofview.tactic

val reduct_option : 
  check:bool ->
  (tactic_reduction * Constr.cast_kind) ->
  Locus.goal_location ->
  unit Proofview.tactic

val reduct_in_concl : 
  check:bool ->
  (tactic_reduction * Constr.cast_kind) ->
  unit Proofview.tactic

val e_reduct_in_concl : 
  check:bool ->
  (e_tactic_reduction * Constr.cast_kind) ->
  unit Proofview.tactic

val change_in_concl : 
  check:bool ->
  (Locus.occurrences * Pattern.constr_pattern) option ->
  change_arg ->
  unit Proofview.tactic

Sourceval change_concl : EConstr.constr -> unit Proofview.tactic

val 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 red_in_hyp : Locus.hyp_location -> unit Proofview.tactic

Sourceval red_option : Locus.goal_location -> unit Proofview.tactic

Sourceval hnf_in_concl : unit Proofview.tactic

Sourceval hnf_in_hyp : Locus.hyp_location -> unit Proofview.tactic

Sourceval hnf_option : Locus.goal_location -> 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

val unfold_in_concl : 
  (Locus.occurrences * Tacred.evaluable_global_reference) list ->
  unit Proofview.tactic

val unfold_in_hyp : 
  (Locus.occurrences * Tacred.evaluable_global_reference) list ->
  Locus.hyp_location ->
  unit Proofview.tactic

val unfold_option : 
  (Locus.occurrences * Tacred.evaluable_global_reference) list ->
  Locus.goal_location ->
  unit Proofview.tactic

val change : 
  check:bool ->
  Pattern.constr_pattern option ->
  change_arg ->
  Locus.clause ->
  unit Proofview.tactic

val pattern_option : 
  (Locus.occurrences * EConstr.constr) list ->
  Locus.goal_location ->
  unit Proofview.tactic

Sourceval reduce : Redexpr.red_expr -> 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

val apply_clear_request : 
  clear_flag ->
  bool ->
  EConstr.constr ->
  unit Proofview.tactic

val specialize : 
  EConstr.constr Tactypes.with_bindings ->
  Tactypes.intro_pattern option ->
  unit Proofview.tactic

val move_hyp : 
  Names.Id.t ->
  Names.Id.t Logic.move_location ->
  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.

val apply_type : 
  typecheck:bool ->
  EConstr.constr ->
  EConstr.constr list ->
  unit Proofview.tactic

Sourceval bring_hyps : EConstr.named_context -> unit Proofview.tactic

Sourceval apply : EConstr.constr -> unit Proofview.tactic

Sourceval eapply : EConstr.constr -> unit Proofview.tactic

val apply_with_bindings_gen : 
  advanced_flag ->
  evars_flag ->
  (clear_flag * EConstr.constr Tactypes.with_bindings CAst.t) list ->
  unit Proofview.tactic

val apply_with_delayed_bindings_gen : 
  advanced_flag ->
  evars_flag ->
  (clear_flag * Tactypes.delayed_open_constr_with_bindings CAst.t) list ->
  unit Proofview.tactic

val apply_with_bindings : 
  EConstr.constr Tactypes.with_bindings ->
  unit Proofview.tactic

val eapply_with_bindings : 
  EConstr.constr Tactypes.with_bindings ->
  unit Proofview.tactic

Sourceval cut_and_apply : EConstr.constr -> unit Proofview.tactic

val apply_in : 
  advanced_flag ->
  evars_flag ->
  Names.Id.t ->
  (clear_flag * EConstr.constr Tactypes.with_bindings CAst.t) list ->
  Tactypes.intro_pattern option ->
  unit Proofview.tactic

val apply_delayed_in : 
  advanced_flag ->
  evars_flag ->
  Names.Id.t ->
  (clear_flag * Tactypes.delayed_open_constr_with_bindings CAst.t) list ->
  Tactypes.intro_pattern option ->
  unit Proofview.tactic ->
  unit Proofview.tactic

Elimination tactics.

Sourcetype elim_scheme = {

elimt : EConstr.types;
indref : Names.GlobRef.t option;
params : EConstr.rel_context;
(*
(prm1,tprm1);(prm2,tprm2)...(prmp,tprmp)
*)
nparams : int;
(*
number of parameters
*)
predicates : EConstr.rel_context;
(*
(Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...)
*)
npredicates : int;
(*
Number of predicates
*)
branches : EConstr.rel_context;
(*
branchr,...,branch1
*)
nbranches : int;
(*
Number of branches
*)
args : EConstr.rel_context;
(*
(xni, Ti_ni) ... (x1, Ti_1)
*)
nargs : int;
(*
number of arguments
*)
indarg : EConstr.rel_declaration option;
(*
Some (H,I prm1..prmp x1...xni) if HI is in premisses, None otherwise
*)
concl : EConstr.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
*)

}

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

Sourcetype eliminator =

| ElimTerm of EConstr.constr
| ElimClause of EConstr.constr Tactypes.with_bindings

val general_elim : 
  evars_flag ->
  clear_flag ->
  EConstr.constr Tactypes.with_bindings ->
  eliminator ->
  unit Proofview.tactic

val general_elim_clause : 
  evars_flag ->
  Unification.unify_flags ->
  Names.Id.t option ->
  Clenv.clausenv ->
  eliminator ->
  unit Proofview.tactic

val default_elim : 
  evars_flag ->
  clear_flag ->
  EConstr.constr Tactypes.with_bindings ->
  unit Proofview.tactic

Sourceval simplest_elim : EConstr.constr -> unit Proofview.tactic

val elim : 
  evars_flag ->
  clear_flag ->
  EConstr.constr Tactypes.with_bindings ->
  EConstr.constr Tactypes.with_bindings option ->
  unit Proofview.tactic

val induction : 
  evars_flag ->
  clear_flag ->
  EConstr.constr ->
  Tactypes.or_and_intro_pattern option ->
  EConstr.constr Tactypes.with_bindings option ->
  unit Proofview.tactic

Case analysis tactics.

val general_case_analysis : 
  evars_flag ->
  clear_flag ->
  EConstr.constr Tactypes.with_bindings ->
  unit Proofview.tactic

Sourceval simplest_case : EConstr.constr -> unit Proofview.tactic

val destruct : 
  evars_flag ->
  clear_flag ->
  EConstr.constr ->
  Tactypes.or_and_intro_pattern option ->
  EConstr.constr Tactypes.with_bindings option ->
  unit Proofview.tactic

Generic case analysis / induction tactics.

Implements user-level "destruct" and "induction"

val induction_destruct : 
  rec_flag ->
  evars_flag ->
  ((Tactypes.delayed_open_constr_with_bindings destruction_arg
    * (Tactypes.intro_pattern_naming option
       * Tactypes.or_and_intro_pattern option)
    * Locus.clause option)
     list
   * EConstr.constr Tactypes.with_bindings option) ->
  unit Proofview.tactic

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.

val constructor_tac : 
  evars_flag ->
  int option ->
  int ->
  EConstr.constr Tactypes.bindings ->
  unit Proofview.tactic

val any_constructor : 
  evars_flag ->
  unit Proofview.tactic option ->
  unit Proofview.tactic

val one_constructor : 
  int ->
  EConstr.constr Tactypes.bindings ->
  unit Proofview.tactic

Sourceval left : EConstr.constr Tactypes.bindings -> unit Proofview.tactic

Sourceval right : EConstr.constr Tactypes.bindings -> unit Proofview.tactic

Sourceval split : EConstr.constr Tactypes.bindings -> unit Proofview.tactic

val left_with_bindings : 
  evars_flag ->
  EConstr.constr Tactypes.bindings ->
  unit Proofview.tactic

val right_with_bindings : 
  evars_flag ->
  EConstr.constr Tactypes.bindings ->
  unit Proofview.tactic

val split_with_bindings : 
  evars_flag ->
  EConstr.constr Tactypes.bindings list ->
  unit Proofview.tactic

val split_with_delayed_bindings : 
  evars_flag ->
  EConstr.constr Tactypes.bindings Tactypes.delayed_open 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

val 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.

val assert_before_replacing : 
  Names.Id.t ->
  EConstr.types ->
  unit Proofview.tactic

val 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

val 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

val assert_by : 
  Names.Name.t ->
  EConstr.types ->
  unit Proofview.tactic ->
  unit Proofview.tactic

val enough_by : 
  Names.Name.t ->
  EConstr.types ->
  unit Proofview.tactic ->
  unit Proofview.tactic

Sourceval pose_proof : Names.Name.t -> EConstr.constr -> unit Proofview.tactic

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

val 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

Sourceval cut : EConstr.types -> unit Proofview.tactic

Tactics for adding local definitions.

Sourceval pose_tac : Names.Name.t -> EConstr.constr -> unit Proofview.tactic

val letin_tac : 
  (bool * Tactypes.intro_pattern_naming) option ->
  Names.Name.t ->
  EConstr.constr ->
  EConstr.types option ->
  Locus.clause ->
  unit Proofview.tactic

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

val letin_pat_tac : 
  evars_flag ->
  (bool * Tactypes.intro_pattern_naming) option ->
  Names.Name.t ->
  (Evd.evar_map * EConstr.constr) ->
  Locus.clause ->
  unit Proofview.tactic

Generalize tactics.

Sourceval generalize : EConstr.constr list -> unit Proofview.tactic

val generalize_gen : 
  (EConstr.constr Locus.with_occurrences * Names.Name.t) list ->
  unit Proofview.tactic

val 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.

val 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.

val unify : 
  ?state:TransparentState.t ->
  EConstr.constr ->
  EConstr.constr ->
  unit Proofview.tactic

val abstract_generalize : 
  ?generalize_vars:bool ->
  ?force_dep:bool ->
  Names.Id.t ->
  unit Proofview.tactic

Sourceval specialize_eqs : Names.Id.t -> unit Proofview.tactic

val general_rewrite_clause : 
  (bool ->
    evars_flag ->
    EConstr.constr Tactypes.with_bindings ->
    Locus.clause ->
    unit Proofview.tactic)
    Hook.t

val subst_one : 
  (bool ->
    Names.Id.t ->
    (Names.Id.t * EConstr.constr * bool) ->
    unit Proofview.tactic)
    Hook.t

val 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

val 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

Sourcemodule New : sig ... end

On This Page

General functions.
Primitive tactics.
Introduction tactics.
Introduction tactics with eliminations.
Exact tactics.
Reduction tactics.
Modification of the local context.
Resolution tactics.
Elimination tactics.
Case analysis tactics.
Generic case analysis / induction tactics.
Eliminations giving the type instead of the proof.
Constructor tactics.
Equality tactics.
Cut tactics.
Tactics for adding local definitions.
Generalize tactics.
Other tactics.
Simple form of basic tactics.
Tacticals defined directly in term of Proofview