(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************)
open Names open EConstr open Evd open Tactypes open Locus open Tactics
(** {6 Elimination tactics. } *)
(* 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 = {
elimt: types;
indref: GlobRef.t 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 : evar_map -> types -> elim_scheme
val induction : evars_flag -> clear_flag -> constr -> or_and_intro_pattern option ->
constr with_bindings option -> unit Proofview.tactic
val destruct : evars_flag -> clear_flag -> constr -> or_and_intro_pattern option ->
constr with_bindings option -> unit Proofview.tactic
(** {6 Generic case analysis / induction tactics. } *)
(** Implements user-level "destruct" and "induction" *)
val induction_destruct : rec_flag -> evars_flag ->
(delayed_open_constr_with_bindings Tactics.destruction_arg
* (intro_pattern_naming option * or_and_intro_pattern option)
* clause option) list *
constr with_bindings option -> unit Proofview.tactic
¤ Dauer der Verarbeitung: 0.24 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
