diff options
| -rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 37 | ||||
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 47 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 7 | ||||
| -rw-r--r-- | tactics/eauto.mli | 6 |
4 files changed, 67 insertions, 30 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index a10241a7c..bb0d3335c 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -1382,7 +1382,6 @@ 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 @@ -1394,9 +1393,15 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = (tclTHENLIST [tclTRY(Recdef.list_rewrite false (List.map mkVar eqs)); observe_tac "rewrite_eqs_in_eqs" (rewrite_eqs_in_eqs eqs); - (observe_tac "finishing" - (tclCOMPLETE ( - Eauto.gen_eauto false (false,5) [] (Some [])) + (observe_tac "finishing using" + ( + tclCOMPLETE( + Eauto.eauto_with_bases + false + (true,5) + [Lazy.force refl_equal] + [Auto.Hint_db.empty] + ) ) ) ] @@ -1511,16 +1516,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 @@ -1536,7 +1541,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 @@ -1602,7 +1607,7 @@ 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 diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 87c4d9bc7..dd776088c 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -851,7 +851,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a let get_current_subgoals_types () = let pts = get_pftreestate () in let _,subs = extract_open_pftreestate pts in - List.map snd (List.sort (fun (x,_) (y,_) -> x -y )subs ) + List.map snd ((* List.sort (fun (x,_) (y,_) -> x -y ) *)subs ) let build_and_l l = let and_constr = Coqlib.build_coq_and () in @@ -900,7 +900,7 @@ let build_new_goal_type () = res - + (* let prove_with_tcc lemma _ : tactic = fun gls -> let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in @@ -913,11 +913,11 @@ let prove_with_tcc lemma _ : tactic = (* default_auto *) ] gls - + *) -let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref goal_name (gls_type,decompose_and_tac,nb_goal) = +let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = let current_proof_name = get_current_proof_name () in let name = match goal_name with | Some s -> s @@ -942,12 +942,9 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref goal_n | _ -> anomaly "equation_lemma: not a constant" in let lemma = mkConst (Lib.make_con na) in -(* Array.iteri *) -(* (fun i _ -> *) -(* by (observe_tac ("reusing lemma "^(string_of_id na)) (prove_with_tcc lemma (nb_goal - i)))) *) -(* (Array.make nb_goal ()) *) -(* ; *) - ref := Some lemma ; + ref_ := Some lemma ; + let lid = ref [] in + let h_num = ref (-1) in Flags.silently Vernacentries.interp (Vernacexpr.VernacAbort None); build_proof ( fun gls -> @@ -956,9 +953,35 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref goal_n [ h_generalize [lemma]; h_intro hid; - Elim.h_decompose_and (mkVar hid); + (fun g -> + let ids = pf_ids_of_hyps g in + tclTHEN + (Elim.h_decompose_and (mkVar hid)) + (fun g -> + let ids' = pf_ids_of_hyps g in + lid := List.rev (list_subtract ids' ids); + if !lid = [] then lid := [hid]; +(* list_iter_i *) +(* (fun i v -> *) +(* msgnl (str "hyp" ++ int i ++ str " " ++ *) +(* Nameops.pr_id v ++ fnl () ++ fnl())) *) +(* !lid; *) + tclIDTAC g + ) + g + ); ] gls) - (gen_eauto(* default_eauto *) false (false,5) [] (Some [])); + (fun g -> + match kind_of_term (pf_concl g) with + | App(f,_) when eq_constr f (well_founded ()) -> + Auto.h_auto None [] (Some []) g + | _ -> + incr h_num; + tclTHEN + (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)) + e_assumption + g) +; Command.save_named opacity; in start_proof diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 706ba9840..ab62aa9cf 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -365,7 +365,10 @@ let e_search_auto debug (in_depth,p) lems db_list gl = open Evd -let eauto debug np lems dbnames = +let eauto_with_bases debug np lems db_list = + tclTRY (e_search_auto debug np lems db_list) + +let eauto debug np lems dbnames = let db_list = List.map (fun x -> @@ -374,7 +377,7 @@ let eauto debug np lems dbnames = ("core"::dbnames) in tclTRY (e_search_auto debug np lems db_list) - + let full_eauto debug n lems gl = let dbnames = current_db_names () in let dbnames = list_subtract dbnames ["v62"] in diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 34655b134..d1883aa66 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -29,3 +29,9 @@ val e_give_exact_constr : constr -> tactic val gen_eauto : bool -> bool * int -> constr list -> hint_db_name list option -> tactic + + +val eauto_with_bases : + bool -> + bool * int -> + Term.constr list -> Auto.Hint_db.t list -> Proof_type.tactic |