diff options
| -rw-r--r-- | kernel/term.ml | 2 | ||||
| -rw-r--r-- | kernel/term.mli | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 15 | ||||
| -rw-r--r-- | tactics/tactics.mli | 45 |
4 files changed, 52 insertions, 11 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index f83e69fcf..e83c32821 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -390,6 +390,8 @@ let destApplication = destApp let isApp c = match kind_of_term c with App _ -> true | _ -> false +let isProd c = match kind_of_term c with | Prod(_) -> true | _ -> false + (* Destructs a constant *) let destConst c = match kind_of_term c with | Const kn -> kn diff --git a/kernel/term.mli b/kernel/term.mli index c0c57959f..160ef767b 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -236,6 +236,7 @@ val isMeta : constr -> bool val isSort : constr -> bool val isCast : constr -> bool val isApp : constr -> bool +val isProd : constr -> bool val isConst : constr -> bool val isConstruct : constr -> bool diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cc4ac6d10..b21ffd96d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1300,7 +1300,7 @@ let find_atomic_param_of_ind nparams indtyp = main arg hyp. hyp0 is now optional, meaning that it is possible that there is no main induction hypotheses. In this case, we consider the last "parameter" (in [indvars]) as the limit between - "left" and "right". + "left" and "right", BUT it must be included in indhyps. Other solutions are still welcome @@ -1457,10 +1457,6 @@ let count_nonfree_rels_from n c = !cpt else raise Not_found -let isProd c = - match kind_of_term c with - | Prod(_) -> true - | _ -> false (* cuts a list in two parts, first of size n. Size must be greater than n *) let cut_list n l = @@ -1578,9 +1574,6 @@ type elim_scheme = { exception NoLastArg exception NoLastArgCcl -(* TODO: traiter les principes avec seulement des parametres (pas - d'argument), par exemple: lt_wf_ind / lt_wf_rec *) - let compute_elim_sig elimc elimt = (* We first separate branches (easily identified because they have a special form AND correpsponding rels do not appear in the @@ -1637,7 +1630,7 @@ let compute_elim_sig elimc elimt = try List.hd args_indargs with Failure "hd" -> raise NoLastArg in match last_arg with - | hiname,Some _,hi -> error "cannot recognise an induction schema" + | hiname,Some _,hi -> error "cannot recognize an induction schema" | hiname,None,hi -> let hi_ind, hi_args = decompose_app hi in let hi_is_ind = @@ -1653,7 +1646,7 @@ let compute_elim_sig elimc elimt = NoLastArgCcl -> List.tl args_indargs , Some (List.hd args_indargs) , false , false | NoLastArg -> args_indargs , None , false , false - | Failure s -> error "cannot recognise an induction schema" in + | Failure s -> error "cannot recognize an induction schema" in let indref = match indarg with @@ -1941,7 +1934,7 @@ let induction_from_context_noind isrec elim_info lid names gl = let deps_cstr = List.fold_left (fun a (id,b,_) -> if b = None then (mkVar id)::a else a) [] deps in - (* terms to patternify we must patternify indarg or farg if any *) + (* terms to patternify we must patternify indarg or farg if present in concl *) let lid_in_pattern = if scheme.indarg_in_concl || scheme.farg_in_concl then hyp0::indvars else indvars in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 8e9a6b6ad..1b8e67842 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 : |