coq-core 8.20.0 (latest) · OCaml Package

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.

val is_quantified_hypothesis : Names.Id.t -> Proofview.Goal.t -> bool

Primitive tactics.

exception NotConvertible

val introduction : Names.Id.t -> unit Proofview.tactic

val convert_concl : 
  cast:bool ->
  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

val fix : Names.Id.t -> int -> unit Proofview.tactic

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

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

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

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

Introduction tactics.

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

val find_intro_names : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.rel_context ->
  Names.Id.t list

val intro : unit Proofview.tactic

val 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

val intros_move : 
  (Names.Id.t * Names.Id.t Logic.move_location) list ->
  unit Proofview.tactic

val 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

val intro_replacing : Names.Id.t -> unit Proofview.tactic

val 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

val intro_mustbe_force : Names.Id.t -> unit Proofview.tactic

val intros_mustbe_force : Names.Id.t list -> unit Proofview.tactic

val intro_then : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic

val 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

val intros_replacing : Names.Id.t list -> unit Proofview.tactic

val intros_possibly_replacing : Names.Id.t list -> unit Proofview.tactic

val auto_intros_tac : Names.Name.t list -> unit Proofview.tactic

auto_intros_tac names handles Automatic Introduction of binders

val intros : unit Proofview.tactic

val intros_until : Tactypes.quantified_hypothesis -> unit Proofview.tactic

val 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

type evars_flag = bool

type rec_flag = bool

type advanced_flag = bool

type clear_flag = bool option

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

type 'a core_destruction_arg =

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

type '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

val finish_evar_resolution : 
  ?flags:Pretyping.inference_flags ->
  Environ.env ->
  Evd.evar_map ->
  (Evd.evar_map option * EConstr.constr) ->
  Evd.evar_map * EConstr.constr

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

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

val assumption : unit Proofview.tactic

val exact_no_check : EConstr.constr -> unit Proofview.tactic

val vm_cast_no_check : EConstr.constr -> unit Proofview.tactic

val native_cast_no_check : EConstr.constr -> unit Proofview.tactic

val exact_check : EConstr.constr -> unit Proofview.tactic

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

Reduction tactics.

type tactic_reduction = Reductionops.reduction_function

type e_tactic_reduction = Reductionops.e_reduction_function

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

val 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 : 
  cast:bool ->
  check:bool ->
  (tactic_reduction * Constr.cast_kind) ->
  unit Proofview.tactic

val e_reduct_in_concl : 
  cast:bool ->
  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

val 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

val red_in_concl : unit Proofview.tactic

val red_in_hyp : Locus.hyp_location -> unit Proofview.tactic

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

val hnf_in_concl : unit Proofview.tactic

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

val hnf_option : Locus.goal_location -> unit Proofview.tactic

val simpl_in_concl : unit Proofview.tactic

val simpl_in_hyp : Locus.hyp_location -> unit Proofview.tactic

val simpl_option : Locus.goal_location -> unit Proofview.tactic

val normalise_in_concl : unit Proofview.tactic

val normalise_in_hyp : Locus.hyp_location -> unit Proofview.tactic

val normalise_option : Locus.goal_location -> unit Proofview.tactic

val normalise_vm_in_concl : unit Proofview.tactic

val unfold_in_concl : 
  (Locus.occurrences * Evaluable.t) list ->
  unit Proofview.tactic

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

val unfold_option : 
  (Locus.occurrences * Evaluable.t) 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

val reduce : Redexpr.red_expr -> Locus.clause -> unit Proofview.tactic

val unfold_constr : Names.GlobRef.t -> unit Proofview.tactic

Modification of the local context.

val clear : Names.Id.t list -> unit Proofview.tactic

val clear_body : Names.Id.t list -> unit Proofview.tactic

val unfold_body : Names.Id.t -> unit Proofview.tactic

val keep : Names.Id.t list -> unit Proofview.tactic

val apply_clear_request : 
  clear_flag ->
  bool ->
  Names.Id.t option ->
  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

val rename_hyp : (Names.Id.t * Names.Id.t) list -> unit Proofview.tactic

Resolution tactics.

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

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

val eapply : ?with_classes:bool -> EConstr.constr -> unit Proofview.tactic

val apply_with_bindings_gen : 
  ?with_classes:bool ->
  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 * EConstr.constr Tactypes.with_bindings Proofview.tactic CAst.t)
    list ->
  unit Proofview.tactic

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

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

val 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 * EConstr.constr Tactypes.with_bindings Proofview.tactic CAst.t)
    list ->
  Tactypes.intro_pattern option ->
  unit Proofview.tactic ->
  unit Proofview.tactic

Elimination tactics.

val general_elim_clause : 
  evars_flag ->
  Unification.unify_flags ->
  Names.Id.t option ->
  ((Constr.metavariable * Evd.clbinding) list * EConstr.t * EConstr.types) ->
  Names.Constant.t ->
  unit Proofview.tactic

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

val 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

Case analysis tactics.

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

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

Eliminations giving the type instead of the proof.

val exfalso : 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

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

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

val 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

val simplest_left : unit Proofview.tactic

val simplest_right : unit Proofview.tactic

val simplest_split : unit Proofview.tactic

Equality tactics.

val setoid_reflexivity : unit Proofview.tactic Hook.t

val reflexivity_red : bool -> unit Proofview.tactic

val reflexivity : unit Proofview.tactic

val intros_reflexivity : unit Proofview.tactic

val setoid_symmetry : unit Proofview.tactic Hook.t

val symmetry_red : bool -> unit Proofview.tactic

val symmetry : unit Proofview.tactic

val setoid_symmetry_in : (Names.Id.t -> unit Proofview.tactic) Hook.t

val intros_symmetry : Locus.clause -> unit Proofview.tactic

val setoid_transitivity : 
  (EConstr.constr option -> unit Proofview.tactic) Hook.t

val transitivity_red : bool -> EConstr.constr option -> unit Proofview.tactic

val transitivity : EConstr.constr -> unit Proofview.tactic

val etransitivity : unit Proofview.tactic

val 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

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

val assert_after : Names.Name.t -> EConstr.types -> 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

val 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

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

Tactics for adding local definitions.

val 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 option * EConstr.constr) ->
  Locus.clause ->
  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 evarconv_unify : 
  ?state:TransparentState.t ->
  ?with_ho:bool ->
  EConstr.constr ->
  EConstr.constr ->
  unit Proofview.tactic

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

module Simple : sig ... end

Simplified version of some of the above tactics

Tacticals defined directly in term of Proofview

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

val reduce_after_refine : unit Proofview.tactic

The reducing tactic called after refine.

Internals, do not use

module Internal : sig ... end

package coq-core