diff options
Diffstat (limited to 'contrib/funind/functional_principles_proofs.ml')
| -rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 88 |
1 files changed, 51 insertions, 37 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 975cf60b..3d80bd00 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -47,7 +47,7 @@ let observe_tac_stream s tac g = let observe_tac s tac g = observe_tac_stream (str s) tac g (* let tclTRYD tac = *) -(* if !Options.debug || do_observe () *) +(* if !Flags.debug || do_observe () *) (* then (fun g -> try (\* do_observe_tac "" *\)tac g with _ -> tclIDTAC g) *) (* else tac *) @@ -140,7 +140,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic = [tclTHENLIST [ (* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]); - (* observe_tac "change_hyp_with_using rename " *) (h_rename prov_id hyp_id) + (* observe_tac "change_hyp_with_using rename " *) (h_rename [prov_id,hyp_id]) ]] g exception TOREMOVE @@ -573,7 +573,7 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id tclTHENLIST[ forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args)); thin [hid]; - (h_rename prov_hid hid) + h_rename [prov_hid,hid] ] g ) ( (* @@ -637,7 +637,7 @@ let build_proof [ h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); thin dyn_infos.rec_hyps; - pattern_option [[-1],t] None; + pattern_option [(false,[1]),t] None; h_simplest_case t; (fun g' -> let g'_nb_prod = nb_prod (pf_concl g') in @@ -882,7 +882,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let f_def = Global.lookup_constant (destConst f) in let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in let f_body = - force (out_some f_def.const_body) + force (Option.get f_def.const_body) in let params,f_body_with_params = decompose_lam_n nb_params f_body in let (_,num),(_,_,bodies) = destFix f_body_with_params in @@ -910,7 +910,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let rec_id = pf_nth_hyp_id g 1 in tclTHENSEQ [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id); - (* observe_tac "h_case" *) (h_case (mkVar rec_id,Rawterm.NoBindings)); + (* observe_tac "h_case" *) (h_case false (mkVar rec_id,Rawterm.NoBindings)); intros_reflexivity] g ) ] @@ -933,8 +933,8 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = let equation_lemma = try let finfos = find_Function_infos (destConst f) in - mkConst (out_some finfos.equation_lemma) - with (Not_found | Failure "out_some" as e) -> + mkConst (Option.get finfos.equation_lemma) + with (Not_found | Option.IsNone as e) -> let f_id = id_of_label (con_label (destConst f)) in (*i The next call to mk_equation_id is valid since we will construct the lemma Ensures by: obvious @@ -943,7 +943,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = generate_equation_lemma all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num; let _ = match e with - | Failure "out_some" -> + | Option.IsNone -> let finfos = find_Function_infos (destConst f) in update_Function {finfos with @@ -1141,7 +1141,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : then (* observe_tac ("h_fix") *) (h_fix (Some this_fix_info.name) (this_fix_info.idx +1)) else - h_mutual_fix this_fix_info.name (this_fix_info.idx + 1) + h_mutual_fix false this_fix_info.name (this_fix_info.idx + 1) other_fix_infos | _ -> anomaly "Not a valid information" in @@ -1246,7 +1246,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : in let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in tclTHENSEQ - [unfold_in_concl [([],Names.EvalConstRef fname)]; + [unfold_in_concl [(all_occurrences,Names.EvalConstRef fname)]; let do_prove = build_proof interactive_proof @@ -1347,19 +1347,27 @@ let build_clause eqs = { Tacexpr.onhyps = Some (List.map - (fun id -> ([],id),Tacexpr.InHyp) + (fun id -> (Rawterm.all_occurrences_expr,id),Tacexpr.InHyp) eqs ); - Tacexpr.onconcl = false; - Tacexpr.concl_occs = [] + Tacexpr.concl_occs = Rawterm.no_occurrences_expr } let rec rewrite_eqs_in_eqs eqs = match eqs with | [] -> tclIDTAC | eq::eqs -> + tclTHEN - (tclMAP (fun id -> tclTRY (Equality.general_rewrite_in true id (mkVar eq))) eqs) + (tclMAP + (fun id gl -> + observe_tac + (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id)) + (tclTRY (Equality.general_rewrite_in true all_occurrences id (mkVar eq) false)) + gl + ) + eqs + ) (rewrite_eqs_in_eqs eqs) let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = @@ -1373,21 +1381,26 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = [ tclTHENSEQ [ keep (tcc_hyps@eqs); - apply (Lazy.force acc_inv); (fun g -> if is_mes then - unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))] g + unfold_in_concl [(all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g else tclIDTAC g ); observe_tac "rew_and_finish" (tclTHENLIST [tclTRY(Recdef.list_rewrite false (List.map mkVar eqs)); - rewrite_eqs_in_eqs eqs; - (observe_tac "finishing" - (tclCOMPLETE ( - Eauto.gen_eauto false (false,5) [] (Some [])) + observe_tac "rewrite_eqs_in_eqs" (rewrite_eqs_in_eqs eqs); + (observe_tac "finishing using" + ( + tclCOMPLETE( + Eauto.eauto_with_bases + false + (true,5) + [Lazy.force refl_equal] + [empty_transparent_state, Auto.Hint_db.empty] + ) ) ) ] @@ -1445,7 +1458,7 @@ let prove_principle_for_gen let wf_tac = if is_mes then - (fun b -> Recdef.tclUSER_if_not_mes b None) + (fun b -> Recdef.tclUSER_if_not_mes tclIDTAC b None) else fun _ -> prove_with_tcc tcc_lemma_ref [] in let real_rec_arg_num = rec_arg_num - princ_info.nparams in @@ -1502,16 +1515,16 @@ let prove_principle_for_gen | None -> anomaly ( "No tcc proof !!") | Some lemma -> lemma in - let rec list_diff del_list check_list = - match del_list with - [] -> - [] - | f::r -> - if List.mem f check_list then - list_diff r check_list - else - f::(list_diff r check_list) - in +(* let rec list_diff del_list check_list = *) +(* match del_list with *) +(* [] -> *) +(* [] *) +(* | f::r -> *) +(* if List.mem f check_list then *) +(* list_diff r check_list *) +(* else *) +(* f::(list_diff r check_list) *) +(* in *) let tcc_list = ref [] in let start_tac gls = let hyps = pf_ids_of_hyps gls in @@ -1527,7 +1540,7 @@ let prove_principle_for_gen Elim.h_decompose_and (mkVar hid); (fun g -> let new_hyps = pf_ids_of_hyps g in - tcc_list := list_diff new_hyps (hid::hyps); + tcc_list := List.rev (list_subtract new_hyps (hid::hyps)); if !tcc_list = [] then begin @@ -1593,14 +1606,15 @@ let prove_principle_for_gen (* msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id eqs); *) (* observe_tac "new_prove_with_tcc" *) - (new_prove_with_tcc + (new_prove_with_tcc is_mes acc_inv fix_id - !tcc_list - ((List.map + + (!tcc_list@(List.map (fun (na,_,_) -> (Nameops.out_name na)) (princ_info.args@princ_info.params) - )@ (acc_rec_arg_id::eqs)) + )@ ([acc_rec_arg_id])) eqs ) + ); is_valid = is_valid_hypothesis predicates_names } |