diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 8e9a6b6add..1b8e678421 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -167,6 +167,51 @@ val cut_and_apply : constr -> tactic (*s 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 = { + elimc: Term.constr * constr Rawterm.bindings; + elimt: types; + indref: global_reference 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,...) *) + branches: rel_context; (* branchr,...,branch1 *) + 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 : Term.constr * constr Rawterm.bindings -> types -> elim_scheme + val general_elim : constr with_bindings -> constr with_bindings -> ?allow_K:bool -> tactic val general_elim_in : |