Module Induction

Elimination tactics.
type 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.

val compute_elim_sig : Evd.evar_map -> EConstr.types -> elim_scheme
val induction : Tactics.evars_flag -> Tactics.clear_flag -> EConstr.constr -> Tactypes.or_and_intro_pattern option -> EConstr.constr Tactypes.with_bindings option -> unit Proofview.tactic
val destruct : Tactics.evars_flag -> Tactics.clear_flag -> EConstr.constr -> Tactypes.or_and_intro_pattern option -> EConstr.constr Tactypes.with_bindings option -> unit Proofview.tactic
Generic case analysis / induction tactics.
val induction_destruct : Tactics.rec_flag -> Tactics.evars_flag -> ((Tactypes.delayed_open_constr_with_bindings Tactics.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