aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/invfun.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/invfun.ml')
-rw-r--r--plugins/funind/invfun.ml59
1 files changed, 25 insertions, 34 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 2743a8a2f9..d1a227d517 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -23,7 +23,7 @@ open Tacticals
open Tactics
open Indfun_common
open Tacmach
-open Misctypes
+open Tactypes
open Termops
open Context.Rel.Declaration
@@ -63,12 +63,6 @@ let observe_tac s tac g =
then do_observe_tac (str s) tac g
else tac g
-(* [nf_zeta] $\zeta$-normalization of a term *)
-let nf_zeta =
- Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
- Environ.empty_env
- Evd.empty
-
let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
(* (\* [id_to_constr id] finds the term associated to [id] in the global environment *\) *)
@@ -81,10 +75,9 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
let make_eq () =
try
- EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
- with _ -> assert false
+ EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type"))
+ with _ -> assert false
-
(* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true]
(resp. g_to_f = false) where [graph] is the graph of [f] and is the [i]th function in the block.
@@ -102,9 +95,9 @@ let generate_type evd g_to_f f graph i =
let evd',graph =
Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd !evd graph)))
in
- let graph = EConstr.of_constr graph in
evd:=evd';
- let graph_arity = Typing.e_type_of (Global.env ()) evd graph in
+ let sigma, graph_arity = Typing.type_of (Global.env ()) !evd graph in
+ evd := sigma;
let ctxt,_ = decompose_prod_assum !evd graph_arity in
let fun_ctxt,res_type =
match ctxt with
@@ -172,7 +165,6 @@ let find_induction_principle evd f =
| None -> raise Not_found
| Some rect_lemma ->
let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in
- let rect_lemma = EConstr.of_constr rect_lemma in
let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
evd:=evd';
rect_lemma,typ
@@ -221,7 +213,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
let mib,_ = Global.lookup_inductive graph_ind in
(* and the principle to use in this lemma in $\zeta$ normal form *)
let f_principle,princ_type = schemes.(i) in
- let princ_type = nf_zeta princ_type in
+ let princ_type = Reductionops.nf_zeta (Global.env ()) evd princ_type in
let princ_infos = Tactics.compute_elim_sig evd princ_type in
(* The number of args of the function is then easily computable *)
let nb_fun_args = nb_prod (project g) (pf_concl g) - 2 in
@@ -240,7 +232,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
List.map
(fun decl ->
List.map
- (fun id -> CAst.make @@ IntroNaming (IntroIdentifier id))
+ (fun id -> CAst.make @@ IntroNaming (Namegen.IntroIdentifier id))
(generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl)))))
)
branches
@@ -258,7 +250,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
List.fold_right
(fun {CAst.v=pat} acc ->
match pat with
- | IntroNaming (IntroIdentifier id) -> id::acc
+ | IntroNaming (Namegen.IntroIdentifier id) -> id::acc
| _ -> anomaly (Pp.str "Not an identifier.")
)
(List.nth intro_pats (pred i))
@@ -352,7 +344,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
Locusops.onConcl);
observe_tac ("toto ") tclIDTAC;
- (* introducing the the result of the graph and the equality hypothesis *)
+ (* introducing the result of the graph and the equality hypothesis *)
observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]);
(* replacing [res] with its value *)
observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
@@ -399,7 +391,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
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)) (Id.Set.of_list avoid) in
- (nf_zeta p)::bindings,id::avoid)
+ (Reductionops.nf_zeta (pf_env g) (project g) p)::bindings,id::avoid)
([],avoid)
princ_infos.predicates
(lemmas)))
@@ -451,7 +443,7 @@ let generalize_dependent_of x hyp g =
let tauto =
let dp = List.map Id.of_string ["Tauto" ; "Init"; "Coq"] in
let mp = ModPath.MPfile (DirPath.make dp) in
- let kn = KerName.make2 mp (Label.make "tauto") in
+ let kn = KerName.make mp (Label.make "tauto") in
Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
let body = Tacenv.interp_ltac kn in
Tacinterp.eval_tactic body
@@ -513,7 +505,7 @@ and intros_with_rewrite_aux : Tacmach.tactic =
intros_with_rewrite
] g
end
- | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) ->
+ | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) ->
Proofview.V82.of_tactic tauto g
| Case(_,_,v,_) ->
tclTHENLIST[
@@ -632,12 +624,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
*)
let lemmas =
Array.map
- (fun (_,(ctxt,concl)) -> nf_zeta (EConstr.it_mkLambda_or_LetIn concl ctxt))
+ (fun (_,(ctxt,concl)) -> Reductionops.nf_zeta (pf_env g) (project g) (EConstr.it_mkLambda_or_LetIn concl ctxt))
lemmas_types_infos
in
(* We get the constant and the principle corresponding to this lemma *)
let f = funcs.(i) in
- let graph_principle = nf_zeta (EConstr.of_constr schemes.(i)) in
+ let graph_principle = Reductionops.nf_zeta (pf_env g) (project g) (EConstr.of_constr schemes.(i)) in
let princ_type = pf_unsafe_type_of g graph_principle in
let princ_infos = Tactics.compute_elim_sig (project g) princ_type in
(* Then we get the number of argument of the function
@@ -771,8 +763,9 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
graphs_constr.(i) <- graph;
let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
- let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in
- let type_of_lemma = nf_zeta type_of_lemma in
+ let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in
+ evd := sigma;
+ let type_of_lemma = Reductionops.nf_zeta (Global.env ()) !evd type_of_lemma in
observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma);
type_of_lemma,type_info
)
@@ -811,20 +804,19 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
let (typ,_) = lemmas_types_infos.(i) in
Lemmas.start_proof
lem_id
- (Decl_kinds.Global,Flags.is_universe_polymorphism (),((Decl_kinds.Proof Decl_kinds.Theorem)))
+ (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem)))
!evd
typ
(Lemmas.mk_hook (fun _ _ -> ()));
ignore (Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
(proving_tac i))));
- (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))));
+ (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))));
let finfo = find_Function_infos (fst f_as_constant) in
(* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
let _,lem_cst_constr = Evd.fresh_global
(Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
- let lem_cst_constr = EConstr.of_constr lem_cst_constr in
- let (lem_cst,_) = destConst !evd lem_cst_constr in
+ let (lem_cst,_) = destConst !evd lem_cst_constr in
update_Function {finfo with correctness_lemma = Some lem_cst};
)
@@ -840,7 +832,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
let type_of_lemma =
EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
in
- let type_of_lemma = nf_zeta type_of_lemma in
+ let type_of_lemma = Reductionops.nf_zeta env !evd type_of_lemma in
observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma);
type_of_lemma,type_info
)
@@ -874,18 +866,17 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
i*)
let lem_id = mk_complete_id f_id in
Lemmas.start_proof lem_id
- (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
+ (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
(fst lemmas_types_infos.(i))
(Lemmas.mk_hook (fun _ _ -> ()));
ignore (Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
(proving_tac i)))) ;
- (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))));
+ (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))));
let finfo = find_Function_infos (fst f_as_constant) in
let _,lem_cst_constr = Evd.fresh_global
(Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
- let lem_cst_constr = EConstr.of_constr lem_cst_constr in
- let (lem_cst,_) = destConst !evd lem_cst_constr in
+ let (lem_cst,_) = destConst !evd lem_cst_constr in
update_Function {finfo with completeness_lemma = Some lem_cst}
)
funs)
@@ -969,7 +960,7 @@ let functional_inversion kn hid fconst f_correct : Tacmach.tactic =
Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]);
thin [hid];
Proofview.V82.of_tactic (Simple.intro hid);
- Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid));
+ Proofview.V82.of_tactic (Inv.inv Inv.FullInversion None (NamedHyp hid));
(fun g ->
let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in
tclMAP (revert_graph kn pre_tac) (hid::new_ids) g
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 10:54:09 +0000