diff options
Diffstat (limited to 'contrib/funind')
-rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 60 | ||||
-rw-r--r-- | contrib/funind/indfun.ml | 55 | ||||
-rw-r--r-- | contrib/funind/indfun_main.ml4 | 5 | ||||
-rw-r--r-- | contrib/funind/invfun.ml | 165 | ||||
-rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 6 | ||||
-rw-r--r-- | contrib/funind/rawtermops.ml | 35 |
6 files changed, 193 insertions, 133 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index ff4f7499..dec7273b 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -621,33 +621,39 @@ let build_proof fun g -> (* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*) - match kind_of_term dyn_infos.info with - | Case(_,_,t,_) -> - let g_nb_prod = nb_prod (pf_concl g) in - let type_of_term = pf_type_of g t in - let term_eq = - make_refl_eq type_of_term t + match kind_of_term dyn_infos.info with | Case(ci,ct,t,cb) -> + let do_finalize_t dyn_info' = + fun g -> + let t = dyn_info'.info in + let dyn_infos = {dyn_info' with info = + mkCase(ci,ct,t,cb)} in + let g_nb_prod = nb_prod (pf_concl g) in + let type_of_term = pf_type_of g t in + let term_eq = + make_refl_eq type_of_term t + in + tclTHENSEQ + [ + h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); + thin dyn_infos.rec_hyps; + pattern_option [[-1],t] None; + h_simplest_case t; + (fun g' -> + let g'_nb_prod = nb_prod (pf_concl g') in + let nb_instanciate_partial = g'_nb_prod - g_nb_prod in + observe_tac "treat_new_case" + (treat_new_case + ptes_infos + nb_instanciate_partial + (build_proof do_finalize) + t + dyn_infos) + g' + ) + + ] g in - tclTHENSEQ - [ - h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); - thin dyn_infos.rec_hyps; - pattern_option [[-1],t] None; - h_simplest_case t; - (fun g' -> - let g'_nb_prod = nb_prod (pf_concl g') in - let nb_instanciate_partial = g'_nb_prod - g_nb_prod in - observe_tac "treat_new_case" - (treat_new_case - ptes_infos - nb_instanciate_partial - (build_proof do_finalize) - t - dyn_infos) - g' - ) - - ] g + build_proof do_finalize_t {dyn_infos with info = t} g | Lambda(n,t,b) -> begin match kind_of_term( pf_concl g) with @@ -1474,7 +1480,7 @@ let prove_principle_for_gen (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])) ); observe_tac "reverting" (revert (List.rev (acc_rec_arg_id::args_ids))); - observe_tac "h_fix" (h_fix (Some fix_id) (npost_rec_arg + 1)); + observe_tac "h_fix" (h_fix (Some fix_id) (List.length args_ids + 1)); h_intros (List.rev (acc_rec_arg_id::args_ids)); Equality.rewriteLR (mkConst eq_ref); observe_tac "finish" (fun gl' -> diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 6e2af224..82bee01f 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -209,7 +209,7 @@ let rec is_rec names = let rec lookup names = function | RVar(_,id) -> check_id id names | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false - | RCast(_,b,_,_) -> lookup names b + | RCast(_,b,_) -> lookup names b | RRec _ -> error "RRec not handled" | RIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) @@ -270,7 +270,30 @@ let derive_inversion fix_names = if do_observe () then Cerrors.explain_exn e else mt ()) with _ -> () -let generate_principle +let warning_error names e = + match e with + | Building_graph e -> + Pp.msg_warning + (str "Cannot define graph(s) for " ++ + h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ + if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()) + | Defining_principle e -> + Pp.msg_warning + (str "Cannot define principle(s) for "++ + h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ + if do_observe () then Cerrors.explain_exn e else mt ()) + | _ -> anomaly "" + +let error_error names e = + match e with + | Building_graph e -> + errorlabstrm "" + (str "Cannot define graph(s) for " ++ + h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ + if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()) + | _ -> anomaly "" + +let generate_principle on_error is_general do_built fix_rec_l recdefs interactive_proof (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) : unit = @@ -324,18 +347,7 @@ let generate_principle () end with e -> - match e with - | Building_graph e -> - Pp.msg_warning - (str "Cannot define graph(s) for " ++ - h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ - if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()) - | Defining_principle e -> - Pp.msg_warning - (str "Cannot define principle(s) for "++ - h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ - if do_observe () then Cerrors.explain_exn e else mt ()) - | _ -> anomaly "" + on_error names e let register_struct is_rec fixpoint_exprl = match fixpoint_exprl with @@ -459,13 +471,14 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b using_lemmas args ret_type body -let do_generate_principle register_built interactive_proof fixpoint_exprl = +let do_generate_principle on_error register_built interactive_proof fixpoint_exprl = let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let _is_struct = match fixpoint_exprl with | [((name,Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> let pre_hook = generate_principle + on_error true register_built fixpoint_exprl @@ -478,6 +491,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl = | [((name,Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> let pre_hook = generate_principle + on_error true register_built fixpoint_exprl @@ -530,6 +544,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl = let is_rec = List.exists (is_rec fix_names) recdefs in if register_built then register_struct is_rec old_fixpoint_exprl; generate_principle + on_error false register_built fixpoint_exprl @@ -596,8 +611,10 @@ let rec add_args id new_args b = | CPatVar _ -> b | CEvar _ -> b | CSort _ -> b - | CCast(loc,b1,ck,b2) -> - CCast(loc,add_args id new_args b1,ck,add_args id new_args b2) + | CCast(loc,b1,CastConv(ck,b2)) -> + CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2)) + | CCast(loc,b1,CastCoerce) -> + CCast(loc,add_args id new_args b1,CastCoerce) | CNotation _ -> anomaly "add_args : CNotation" | CPrim _ -> b | CDelimiters _ -> anomaly "add_args : CDelimiters" @@ -732,7 +749,7 @@ let make_graph (f_ref:global_reference) = let id = id_of_label (con_label c) in [(id,None,nal_tas,t,b)] in - do_generate_principle false false expr_list; + do_generate_principle error_error false false expr_list; (* We register the infos *) let mp,dp,_ = repr_con c in List.iter @@ -742,6 +759,6 @@ let make_graph (f_ref:global_reference) = (* let make_graph _ = assert false *) -let do_generate_principle = do_generate_principle true +let do_generate_principle = do_generate_principle warning_error true diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4 index 26a1066c..9cee9edc 100644 --- a/contrib/funind/indfun_main.ml4 +++ b/contrib/funind/indfun_main.ml4 @@ -203,7 +203,10 @@ VERNAC COMMAND EXTEND NewFunctionalScheme match fas with | (_,fun_name,_)::_ -> begin - make_graph (Nametab.global fun_name); + begin + make_graph (Nametab.global fun_name) + end + ; try Functional_principles_types.build_scheme fas with Functional_principles_types.No_graph_found -> Util.error ("Cannot generate induction principle(s)") diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index 04110ea9..9ec02d4c 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -478,7 +478,72 @@ let generalize_depedent_of x hyp g = - + (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis + (unfolding, substituting, destructing cases \ldots) + *) +let rec intros_with_rewrite g = + observe_tac "intros_with_rewrite" intros_with_rewrite_aux g +and intros_with_rewrite_aux : tactic = + fun g -> + let eq_ind = Coqlib.build_coq_eq () in + match kind_of_term (pf_concl g) with + | Prod(_,t,t') -> + begin + match kind_of_term t with + | App(eq,args) when (eq_constr eq eq_ind) -> + if isVar args.(1) + then + let id = pf_get_new_id (id_of_string "y") g in + tclTHENSEQ [ h_intro id; + generalize_depedent_of (destVar args.(1)) id; + tclTRY (Equality.rewriteLR (mkVar id)); + intros_with_rewrite + ] + g + else + begin + let id = pf_get_new_id (id_of_string "y") g in + tclTHENSEQ[ + h_intro id; + tclTRY (Equality.rewriteLR (mkVar id)); + intros_with_rewrite + ] g + end + | Ind _ when eq_constr t (Coqlib.build_coq_False ()) -> + Tauto.tauto g + | Case(_,_,v,_) -> + tclTHENSEQ[ + h_case (v,Rawterm.NoBindings); + intros_with_rewrite + ] g + | LetIn _ -> + tclTHENSEQ[ + h_reduce + (Rawterm.Cbv + {Rawterm.all_flags + with Rawterm.rDelta = false; + }) + onConcl + ; + intros_with_rewrite + ] g + | _ -> + let id = pf_get_new_id (id_of_string "y") g in + tclTHENSEQ [ h_intro id;intros_with_rewrite] g + end + | LetIn _ -> + tclTHENSEQ[ + h_reduce + (Rawterm.Cbv + {Rawterm.all_flags + with Rawterm.rDelta = false; + }) + onConcl + ; + intros_with_rewrite + ] g + | _ -> tclIDTAC g + let rec reflexivity_with_destruct_cases g = let destruct_case () = try @@ -492,10 +557,34 @@ let rec reflexivity_with_destruct_cases g = | _ -> reflexivity with _ -> reflexivity in - tclFIRST + let eq_ind = Coqlib.build_coq_eq () in + let discr_inject = + Tacticals.onAllClauses ( + fun sc g -> + match sc with + None -> tclIDTAC g + | Some ((_,id),_) -> + match kind_of_term (pf_type_of g (mkVar id)) with + | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind -> + if Equality.discriminable (pf_env g) (project g) t1 t2 + then Equality.discr id g + else if Equality.injectable (pf_env g) (project g) t1 t2 + then tclTHEN (Equality.inj [] id) intros_with_rewrite g + else tclIDTAC g + | _ -> tclIDTAC g + ) + in + (tclFIRST [ reflexivity; - destruct_case () - ] + destruct_case (); + (* We reach this point ONLY if + the same value is matched (at least) two times + along binding path. + In this case, either we have a discriminable hypothesis and we are done, + either at least an injectable one and we do the injection before continuing + *) + tclTHEN (tclPROGRESS discr_inject ) reflexivity_with_destruct_cases + ]) g @@ -566,7 +655,6 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = ) branches in - let eq_ind = Coqlib.build_coq_eq () in (* We will need to change the function by its body using [f_equation] if it is recursive (that is the graph is infinite or unfold if the graph is finite @@ -596,71 +684,6 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = ] else unfold_in_concl [([],Names.EvalConstRef (destConst f))] in - (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis - (unfolding, substituting, destructing cases \ldots) - *) - let rec intros_with_rewrite_aux : tactic = - fun g -> - match kind_of_term (pf_concl g) with - | Prod(_,t,t') -> - begin - match kind_of_term t with - | App(eq,args) when (eq_constr eq eq_ind) -> - if isVar args.(1) - then - let id = pf_get_new_id (id_of_string "y") g in - tclTHENSEQ [ h_intro id; - generalize_depedent_of (destVar args.(1)) id; - tclTRY (Equality.rewriteLR (mkVar id)); - intros_with_rewrite - ] - g - else - begin - let id = pf_get_new_id (id_of_string "y") g in - tclTHENSEQ[ - h_intro id; - tclTRY (Equality.rewriteLR (mkVar id)); - intros_with_rewrite - ] g - end - | Ind _ when eq_constr t (Coqlib.build_coq_False ()) -> - Tauto.tauto g - | Case(_,_,v,_) -> - tclTHENSEQ[ - h_case (v,Rawterm.NoBindings); - intros_with_rewrite - ] g - | LetIn _ -> - tclTHENSEQ[ - h_reduce - (Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; - }) - onConcl - ; - intros_with_rewrite - ] g - | _ -> - let id = pf_get_new_id (id_of_string "y") g in - tclTHENSEQ [ h_intro id;intros_with_rewrite] g - end - | LetIn _ -> - tclTHENSEQ[ - h_reduce - (Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; - }) - onConcl - ; - intros_with_rewrite - ] g - | _ -> tclIDTAC g - and intros_with_rewrite g = - observe_tac "intros_with_rewrite" intros_with_rewrite_aux g - in (* The proof of each branche itself *) let ind_number = ref 0 in let min_constr_number = ref 0 in @@ -698,7 +721,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = h_intro graph_principle_id; observe_tac "" (tclTHEN_i (observe_tac "elim" ((elim (mkVar hres,Rawterm.NoBindings) (Some (mkVar graph_principle_id,Rawterm.NoBindings))))) - (fun i g -> prove_branche i g )) + (fun i g -> observe_tac "prove_branche" (prove_branche i) g )) ] g diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index aca84f06..b34a1097 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -351,7 +351,7 @@ let rec find_type_of nb b = then raise (Invalid_argument "find_type_of : not a valid inductive"); ind_type end - | RCast(_,b,_,_) -> find_type_of nb b + | RCast(_,b,_) -> find_type_of nb b | RApp _ -> assert false (* we have decomposed any application via raw_decompose_app *) | _ -> raise (Invalid_argument "not a ref") @@ -575,7 +575,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = let f_res = build_entry_lc env funnames args_res.to_avoid f in combine_results combine_app f_res args_res | RDynamic _ ->error "Not handled RDynamic" - | RCast(_,b,_,_) -> + | RCast(_,b,_) -> (* for an applied cast we just trash the cast part and restart the work. @@ -685,7 +685,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = end | RRec _ -> error "Not handled RRec" - | RCast(_,b,_,_) -> + | RCast(_,b,_) -> build_entry_lc env funnames avoid b | RDynamic _ -> error "Not handled RDynamic" and build_entry_lc_from_case env funname make_discr diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml index ba5c2bbd..113ddd8b 100644 --- a/contrib/funind/rawtermops.ml +++ b/contrib/funind/rawtermops.ml @@ -18,7 +18,7 @@ let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b) let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl) let mkRSort s = RSort(dummy_loc,s) let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous) -let mkRCast(b,t) = RCast(dummy_loc,b,CastCoerce,t) +let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t)) (* Some basic functions to decompose rawconstrs @@ -145,8 +145,10 @@ let change_vars = | RRec _ -> error "Local (co)fixes are not supported" | RSort _ -> rt | RHole _ -> rt - | RCast(loc,b,k,t) -> - RCast(loc,change_vars mapping b,k,change_vars mapping t) + | RCast(loc,b,CastConv (k,t)) -> + RCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t)) + | RCast(loc,b,CastCoerce) -> + RCast(loc,change_vars mapping b,CastCoerce) | RDynamic _ -> error "Not handled RDynamic" and change_vars_br mapping ((loc,idl,patl,res) as br) = let new_mapping = List.fold_right Idmap.remove idl mapping in @@ -324,8 +326,10 @@ let rec alpha_rt excluded rt = | RRec _ -> error "Not handled RRec" | RSort _ -> rt | RHole _ -> rt - | RCast (loc,b,k,t) -> - RCast(loc,alpha_rt excluded b,k,alpha_rt excluded t) + | RCast (loc,b,CastConv (k,t)) -> + RCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t)) + | RCast (loc,b,CastCoerce) -> + RCast(loc,alpha_rt excluded b,CastCoerce) | RDynamic _ -> error "Not handled RDynamic" | RApp(loc,f,args) -> RApp(loc, @@ -375,7 +379,8 @@ let is_free_in id = | RRec _ -> raise (UserError("",str "Not handled RRec")) | RSort _ -> false | RHole _ -> false - | RCast (_,b,_,t) -> is_free_in b || is_free_in t + | RCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t + | RCast (_,b,CastCoerce) -> is_free_in b | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) and is_free_in_br (_,ids,_,rt) = (not (List.mem id ids)) && is_free_in rt @@ -469,8 +474,10 @@ let replace_var_by_term x_id term = | RRec _ -> raise (UserError("",str "Not handled RRec")) | RSort _ -> rt | RHole _ -> rt - | RCast(loc,b,k,t) -> - RCast(loc,replace_var_by_pattern b,k,replace_var_by_pattern t) + | RCast(loc,b,CastConv(k,t)) -> + RCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t)) + | RCast(loc,b,CastCoerce) -> + RCast(loc,replace_var_by_pattern b,CastCoerce) | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) and replace_var_by_pattern_br ((loc,idl,patl,res) as br) = if List.exists (fun id -> id_ord id x_id == 0) idl @@ -554,7 +561,8 @@ let ids_of_rawterm c = | RLambda (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc | RProd (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc | RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc - | RCast (loc,c,k,t) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc + | RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc + | RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc | RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc | RLetTuple (_,nal,(na,po),b,c) -> List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc @@ -619,8 +627,10 @@ let zeta_normalize = | RRec _ -> raise (UserError("",str "Not handled RRec")) | RSort _ -> rt | RHole _ -> rt - | RCast(loc,b,k,t) -> - RCast(loc,zeta_normalize_term b,k,zeta_normalize_term t) + | RCast(loc,b,CastConv(k,t)) -> + RCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t)) + | RCast(loc,b,CastCoerce) -> + RCast(loc,zeta_normalize_term b,CastCoerce) | RDynamic _ -> raise (UserError("",str "Not handled RDynamic")) and zeta_normalize_br (loc,idl,patl,res) = (loc,idl,patl,zeta_normalize_term res) @@ -660,7 +670,8 @@ let expand_as = expand_as map br1, expand_as map br2) | RRec _ -> error "Not handled RRec" | RDynamic _ -> error "Not handled RDynamic" - | RCast(loc,b,kind,t) -> RCast(loc,expand_as map b,kind,expand_as map t) + | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t)) + | RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce) | RCases(loc,po,el,brl) -> RCases(loc, option_map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) |