diff options
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 51 |
1 files changed, 23 insertions, 28 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 8dea6c90f5..4acf82d000 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -12,6 +12,7 @@ open CErrors open Util open Names open Term +open Constr open EConstr open Vars open Pp @@ -55,12 +56,6 @@ let do_observe_tac s tac g = CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal )); iraise reraise;; - -let observe_tac_strm s tac g = - if do_observe () - then do_observe_tac s tac g - else tac g - let observe_tac s tac g = if do_observe () then do_observe_tac (str s) tac g @@ -86,10 +81,6 @@ let make_eq () = try EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ())) with _ -> assert false -let make_eq_refl () = - try - EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq_refl ())) - with _ -> assert false (* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true] @@ -131,9 +122,9 @@ let generate_type evd g_to_f f graph i = | Name id -> Some id | Anonymous -> None in - let named_ctxt = List.map_filter filter fun_ctxt in + let named_ctxt = Id.Set.of_list (List.map_filter filter fun_ctxt) in let res_id = Namegen.next_ident_away_in_goal (Id.of_string "_res") named_ctxt in - let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (res_id :: named_ctxt) in + let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (Id.Set.add res_id named_ctxt) in (*i we can then type the argument to be applied to the function [f] i*) let args_as_rels = Array.of_list (args_from_decl 1 [] fun_ctxt) in (*i @@ -189,14 +180,13 @@ let rec generate_fresh_id x avoid i = if i == 0 then [] else - let id = Namegen.next_ident_away_in_goal x avoid in + let id = Namegen.next_ident_away_in_goal x (Id.Set.of_list avoid) in id::(generate_fresh_id x (id::avoid) (pred i)) -(* [prove_fun_correct functional_induction funs_constr graphs_constr schemes lemmas_types_infos i ] +(* [prove_fun_correct funs_constr graphs_constr schemes lemmas_types_infos i ] is the tactic used to prove correctness lemma. - [functional_induction] is the tactic defined in [indfun] (dependency problem) [funs_constr], [graphs_constr] [schemes] [lemmas_types_infos] are the mutually recursive functions (resp. graphs of the functions and principles and correctness lemma types) to prove correct. @@ -217,7 +207,7 @@ let rec generate_fresh_id x avoid i = \end{enumerate} *) -let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic = +let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic = fun g -> (* first of all we recreate the lemmas types to be used as predicates of the induction principle that is~: @@ -239,7 +229,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes environment and due to the bug #1174, we will need to pose the principle using a name *) - let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in + let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") (Id.Set.of_list ids) in let ids = principle_id :: ids in (* We get the branches of the principle *) let branches = List.rev princ_infos.branches in @@ -396,7 +386,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let params_bindings,avoid = List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in p::bindings,id::avoid ) ([],pf_ids_of_hyps g) @@ -406,7 +396,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let lemmas_bindings = List.rev (fst (List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in (nf_zeta p)::bindings,id::avoid) ([],avoid) princ_infos.predicates @@ -570,6 +560,11 @@ let rec reflexivity_with_destruct_cases g = with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity in let eq_ind = make_eq () in + let my_inj_flags = Some { + Equality.keep_proof_equalities = false; + injection_in_context = false; (* for compatibility, necessary *) + injection_pattern_l2r_order = false; (* probably does not matter; except maybe with dependent hyps *) + } in let discr_inject = Tacticals.onAllHypsAndConcl ( fun sc g -> @@ -580,8 +575,8 @@ let rec reflexivity_with_destruct_cases g = | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind -> if Equality.discriminable (pf_env g) (project g) t1 t2 then Proofview.V82.of_tactic (Equality.discrHyp id) g - else if Equality.injectable (pf_env g) (project g) t1 t2 - then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite] g + else if Equality.injectable (pf_env g) (project g) ~keep_proofs:None t1 t2 + then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp my_inj_flags None id);thin [id];intros_with_rewrite] g else tclIDTAC g | _ -> tclIDTAC g ) @@ -746,20 +741,20 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti g -(* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness +(* [derive_correctness make_scheme funs graphs] create correctness and completeness lemmas for each function in [funs] w.r.t. [graphs] [make_scheme] is Functional_principle_types.make_scheme (dependency pb) and - [functional_induction] is Indfun.functional_induction (same pb) *) -let derive_correctness make_scheme functional_induction (funs: pconstant list) (graphs:inductive list) = +let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list) = assert (funs <> []); assert (graphs <> []); let funs = Array.of_list funs and graphs = Array.of_list graphs in let map (c, u) = mkConstU (c, EInstance.make u) in let funs_constr = Array.map map funs in - States.with_state_protection_on_exception + (* XXX STATE Why do we need this... why is the toplevel protection not enought *) + funind_purify (fun () -> let env = Global.env () in let evd = ref (Evd.from_env env) in @@ -797,12 +792,12 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( (fun entry -> (EConstr.of_constr (fst (fst(Future.force entry.Entries.const_entry_body))), EConstr.of_constr (Option.get entry.Entries.const_entry_type )) ) - (make_scheme evd (Array.map_to_list (fun const -> const,GType []) funs)) + (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs)) ) ) in let proving_tac = - prove_fun_correct !evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos + prove_fun_correct !evd funs_constr graphs_constr schemes lemmas_types_infos in Array.iteri (fun i f_as_constant -> @@ -844,7 +839,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in let type_of_lemma = nf_zeta type_of_lemma in - observe (str "type_of_lemma := " ++ Printer.pr_leconstr type_of_lemma); + observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma); type_of_lemma,type_info ) funs_constr |