From 89170371b597086626a69637f802e855a1693f84 Mon Sep 17 00:00:00 2001 From: courtieu Date: Wed, 5 Apr 2006 09:21:27 +0000 Subject: ajout d'un rattrapage d'erreur pour "induction using". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8679 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/tactics.ml | 116 ++++++++++++++++++++++++++++++----------------------- 1 file changed, 65 insertions(+), 51 deletions(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index bddb82c54..c16a0303d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1615,7 +1615,7 @@ let compute_elim_sig ?elimc elimt = let concl_with_args = it_mkProd_or_LetIn ccl args_indargs in let nparams = Intset.cardinal (free_rels concl_with_args) in let preds,params = cut_list (List.length params_preds - nparams) params_preds in - + (* A first approximation, further anlysis will tweak it *) let res = ref { empty_scheme with (* This fields are ok: *) @@ -1848,24 +1848,26 @@ let induction_tac_felim indvars (* (elimc,lbindelimc) elimt *) scheme gl = FIXME: REUNIF AVEC induction_tac_felim? *) let induction_from_context_l isrec elim_info lid names gl = let indsign,scheme = elim_info in - (* hyp0 is the first element of the list of variables on which to - induct. It is most probably the first of them appearing in the - context. So it seems to be a good value for hyp0, which is used - for re-introducing hyps at the right place afterward. *) + (* number of all args, counting farg and indarg if present. *) + let nargs_indarg_farg = scheme.nargs + + (if scheme.farg_in_concl then 1 else 0) + + (if scheme.indarg <> None then 1 else 0) in + (* Number of given induction args must be exact. *) + if List.length lid <> nargs_indarg_farg + scheme.nparams then + error "not the right number of arguments given to induction scheme"; let env = pf_env gl in + (* hyp0 is used for re-introducing hyps at the right place afterward. + We chose the first element of the list of variables on which to + induct. It is probably the first of them appearing in the + context. *) let hyp0,indvars,lid_params = match lid with | [] -> anomaly "induction_from_context_l" | e::l -> - let nargs_without_indarg = - scheme.nargs - 1 - + (if scheme.farg_in_concl then 1 else 0) - + (if scheme.indarg <> None then 1 else 0) in - let ivs,lp = cut_list nargs_without_indarg l in + let nargs_without_first = nargs_indarg_farg - 1 in + let ivs,lp = cut_list nargs_without_first l in e, ivs, lp in - let statlists,lhyp0,indhyps,deps = - (* if scheme.indarg<>None then cook_sign (Some hyp0) indvars env - else *) cook_sign None (hyp0::indvars) env in + let statlists,lhyp0,indhyps,deps = cook_sign None (hyp0::indvars) env in let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in let names = compute_induction_names (Array.length indsign) names in let dephyps = List.map (fun (id,_,_) -> id) deps in @@ -1948,11 +1950,10 @@ let induction_from_context isrec elim_info hyp0 names gl = -exception TryNewInduct +exception TryNewInduct of exn let induction_with_atomization_of_ind_arg isrec elim names hyp0 gl = - let (indsign,scheme as elim_info) = - find_elim_signature isrec elim hyp0 gl in + let (indsign,scheme as elim_info) = find_elim_signature isrec elim hyp0 gl in if scheme.indarg = None then (* This is not a standard induction scheme (the argument is probably a parameter) So try the more general induction mechanism. *) @@ -2009,56 +2010,69 @@ let new_induct_gen_l isrec elim names lc gl = | _ -> let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) Anonymous in + let id = fresh_id [] x gl in + let newl' =(* List.map (replace_term c (mkVar id)) *) l' in let _ = newlc:=id::!newlc in tclTHEN (letin_tac true (Name id) c allClauses) - (atomize_list l') gl in + (*(tclTHEN (assert_tac (mkEq typofc c (mkVar id))) + (tclLAST_HYP generalize_dep) + )*) + (atomize_list newl') gl in tclTHEN (atomize_list lc) (fun gl' -> (* recompute each time to have the new value of newlc *) induction_without_atomization isrec elim names !newlc gl') gl +let induct_destruct_l isrec lc elim names = + (* Several induction hyps: induction scheme is mandatory *) + let _ = + if elim = None + then + error ("Induction scheme must be given when several induction hypothesis.\n" + ^ "Example: induction x1 x2 x3 using my_scheme.") in + let newlc = + List.map + (fun x -> + match x with (* FIXME: should we deal with ElimOnIdent? *) + | ElimOnConstr x -> x + | _ -> error "don't know where to find some argument") + lc in + new_induct_gen_l isrec elim names newlc + + (* Induction either over a term, over a quantified premisse, or over several quantified premisses (like with functional induction - principles). *) -let new_induct_destruct_l isrec lc elim names = + principles). + TODO: really unify induction with one and induction with several + args *) +let induct_destruct isrec lc elim names = assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *) - try - if List.length lc = 1 then (* induction on one arg *) - try - let c = List.hd lc in - match c with - | ElimOnConstr c -> new_induct_gen isrec elim names c - | ElimOnAnonHyp n -> - tclTHEN (intros_until_n n) - (tclLAST_HYP (new_induct_gen isrec elim names)) - (* Identifier apart because id can be quantified in goal and not typable *) - | ElimOnIdent (_,id) -> - tclTHEN (tclTRY (intros_until_id id)) - (new_induct_gen isrec elim names (mkVar id)) - with _ -> raise TryNewInduct - else raise TryNewInduct - with TryNewInduct -> - (* Several induction hyps: induction scheme is mandatory *) - let _ = - if elim = None - then - error ("Induction scheme must be given when several induction hypothesis.\n" - ^ "Example: induction x1 x2 x3 using my_scheme.") in - let newlc = - List.map - (fun x -> - match x with (* FIXME: should we deal with ElimOnIdent? *) - | ElimOnConstr x -> x - | _ -> error "don't know where to find some argument") - lc in - new_induct_gen_l isrec elim names newlc + if List.length lc = 1 then (* induction on one arg: use old mechanism *) + let _ = print_string "\nOne arg\n" in + try + let c = List.hd lc in + match c with + | ElimOnConstr c -> new_induct_gen isrec elim names c + | ElimOnAnonHyp n -> + tclTHEN (intros_until_n n) + (tclLAST_HYP (new_induct_gen isrec elim names)) + (* Identifier apart because id can be quantified in goal and not typable *) + | ElimOnIdent (_,id) -> + tclTHEN (tclTRY (intros_until_id id)) + (new_induct_gen isrec elim names (mkVar id)) + with (* If this fails, try with new mechanism but if it fails too, + then the exception is the first one. *) + | x -> (print_string "\nfailed\n";try induct_destruct_l isrec lc elim names with _ -> raise x) + else induct_destruct_l isrec lc elim names + + -let new_induct = new_induct_destruct_l true -let new_destruct c = new_induct_destruct_l false c +let new_induct = induct_destruct true +let new_destruct = induct_destruct false (* The registered tactic, which calls the default elimination * if no elimination constant is provided. *) -- cgit v1.2.3