aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml26
-rw-r--r--plugins/funind/g_indfun.mlg2
-rw-r--r--plugins/funind/gen_principle.ml126
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/funind/glob_termops.ml14
-rw-r--r--plugins/funind/glob_termops.mli10
-rw-r--r--plugins/funind/indfun.ml212
-rw-r--r--plugins/funind/indfun.mli12
-rw-r--r--plugins/funind/indfun_common.ml48
-rw-r--r--plugins/funind/indfun_common.mli14
-rw-r--r--plugins/funind/invfun.ml71
11 files changed, 279 insertions, 258 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 5a939b4adf..ca33e4e757 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -941,7 +941,11 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g =
let equation_lemma =
try
- let finfos = find_Function_infos (fst (destConst !evd f)) (*FIXME*) in
+ let finfos =
+ match find_Function_infos (fst (destConst !evd f)) (*FIXME*) with
+ | None -> raise Not_found
+ | Some finfos -> finfos
+ in
mkConst (Option.get finfos.equation_lemma)
with (Not_found | Option.IsNone as e) ->
let f_id = Label.to_id (Constant.label (fst (destConst !evd f))) in
@@ -953,14 +957,18 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
let _ =
match e with
| Option.IsNone ->
- let finfos = find_Function_infos (fst (destConst !evd f)) in
- update_Function
- {finfos with
- equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
- GlobRef.ConstRef c -> c
- | _ -> CErrors.anomaly (Pp.str "Not a constant.")
- )
- }
+ let finfos = match find_Function_infos (fst (destConst !evd f)) with
+ | None -> raise Not_found
+ | Some finfos -> finfos
+ in
+ update_Function
+ {finfos with
+ equation_lemma = Some (
+ match Nametab.locate (qualid_of_ident equation_lemma_id) with
+ | GlobRef.ConstRef c -> c
+ | _ -> CErrors.anomaly (Pp.str "Not a constant.")
+ )
+ }
| _ -> ()
in
(* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *)
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 92a93489f4..2b990400e3 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -91,7 +91,7 @@ END
{
let functional_induction b c x pat =
- Proofview.V82.tactic (functional_induction true c x (Option.map out_disjunctive pat))
+ functional_induction true c x (Option.map out_disjunctive pat)
}
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index a836335d4d..570b72136c 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -164,7 +164,7 @@ let prepare_body { Vernacexpr.binders } rt =
let fun_args,rt' = chop_rlambda_n n rt in
(fun_args,rt')
-let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook =
+let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook =
(* First we get the type of the old graph principle *)
let mutr_nparams = (Tactics.compute_elim_sig !evd (EConstr.of_constr old_princ_type)).Tactics.nparams in
(* let time1 = System.get_time () in *)
@@ -199,10 +199,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
(* end; *)
let open Proof_global in
- let { name; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
+ let { name; entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in
match entries with
| [entry] ->
- name, entry, hook
+ entry, hook
| _ ->
CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
@@ -234,6 +234,23 @@ let change_property_sort evd toSort princ princName =
)
(List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_info.Tactics.params)
+(* XXX: To be cleaned up soon in favor of common save path. *)
+let save name const ?hook uctx scope kind =
+ let open Declare in
+ let open DeclareDef in
+ let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in
+ let r = match scope with
+ | Discharge ->
+ let c = SectionLocalDef const in
+ let () = declare_variable ~name ~kind c in
+ GlobRef.VarRef name
+ | Global local ->
+ let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in
+ GlobRef.ConstRef kn
+ in
+ DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r });
+ definition_message name
+
let generate_functional_principle (evd: Evd.evar_map ref)
interactive_proof
old_princ_type sorts new_princ_name funs i proof_tac
@@ -282,7 +299,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
register_with_sort Sorts.InProp;
register_with_sort Sorts.InSet
in
- let id,entry,hook =
+ let entry, hook =
build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
proof_tac hook
in
@@ -495,14 +512,17 @@ let find_induction_principle evd f =
| Constr.Const c' -> c'
| _ -> CErrors.user_err Pp.(str "Must be used with a function")
in
- let infos = find_Function_infos f_as_constant in
- match infos.rect_lemma with
- | None -> raise Not_found
- | Some rect_lemma ->
- let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (GlobRef.ConstRef rect_lemma) in
- let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
- evd:=evd';
- rect_lemma,typ
+ match find_Function_infos f_as_constant with
+ | None ->
+ raise Not_found
+ | Some infos ->
+ match infos.rect_lemma with
+ | None -> raise Not_found
+ | Some rect_lemma ->
+ let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (GlobRef.ConstRef rect_lemma) in
+ let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
+ evd:=evd';
+ rect_lemma,typ
(* [prove_fun_correct funs_constr graphs_constr schemes lemmas_types_infos i ]
is the tactic used to prove correctness lemma.
@@ -1016,12 +1036,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
*)
let rewrite_tac j ids : Tacmach.tactic =
let graph_def = graphs.(j) in
- let infos =
- try find_Function_infos (fst (destConst (project g) funcs.(j)))
- with Not_found -> CErrors.user_err Pp.(str "No graph found")
+ let infos = match find_Function_infos (fst (destConst (project g) funcs.(j))) with
+ | None ->
+ CErrors.user_err Pp.(str "No graph found")
+ | Some infos -> infos
in
- if infos.is_general
- || Rtree.is_infinite Declareops.eq_recarg graph_def.Declarations.mind_recargs
+ if infos.is_general || Rtree.is_infinite Declareops.eq_recarg graph_def.Declarations.mind_recargs
then
let eq_lemma =
try Option.get (infos).equation_lemma
@@ -1167,16 +1187,16 @@ let get_funs_constant mp =
in
l_const
-let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_effects Proof_global.proof_entry list =
+let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_effects Declare.proof_entry list =
let exception Found_type of int in
let env = Global.env () in
let funs = List.map fst fas in
let first_fun = List.hd funs in
let funs_mp = KerName.modpath (Constant.canonical (fst first_fun)) in
let first_fun_kn =
- try
- fst (find_Function_infos (fst first_fun)).graph_ind
- with Not_found -> raise No_graph_found
+ match find_Function_infos (fst first_fun) with
+ | None -> raise No_graph_found
+ | Some finfos -> fst finfos.graph_ind
in
let this_block_funs_indexes = get_funs_constant funs_mp (fst first_fun) in
let this_block_funs = Array.map (fun (c,_) -> (c,snd first_fun)) this_block_funs_indexes in
@@ -1216,9 +1236,21 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
s::l_schemes -> s,l_schemes
| _ -> CErrors.anomaly (Pp.str "")
in
- let _,const,_ =
+ let opaque =
+ let finfos =
+ match find_Function_infos (fst first_fun) with
+ | None -> raise Not_found
+ | Some finfos -> finfos
+ in
+ let open Proof_global in
+ match finfos.equation_lemma with
+ | None -> Transparent (* non recursive definition *)
+ | Some equation ->
+ if Declareops.is_opaque (Global.lookup_constant equation) then Opaque else Transparent
+ in
+ let entry, _hook =
try
- build_functional_principle evd false
+ build_functional_principle ~opaque evd false
first_type
(Array.of_list sorts)
this_block_funs
@@ -1230,27 +1262,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
in
incr i;
- let opacity =
- let finfos = find_Function_infos (fst first_fun) in
- try
- let equation = Option.get finfos.equation_lemma in
- Declareops.is_opaque (Global.lookup_constant equation)
- with Option.IsNone -> (* non recursive definition *)
- false
- in
- let const = {const with Proof_global.proof_entry_opaque = opacity } in
(* The others are just deduced *)
if List.is_empty other_princ_types
- then
- [const]
+ then [entry]
else
let other_fun_princ_types =
let funs = Array.map Constr.mkConstU this_block_funs in
let sorts = Array.of_list sorts in
List.map (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types
in
- let open Proof_global in
- let first_princ_body,first_princ_type = const.proof_entry_body, const.proof_entry_type in
+ let first_princ_body,first_princ_type = Declare.(entry.proof_entry_body, entry.proof_entry_type) in
let ctxt,fix = Term.decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
let (idxs,_),(_,ta,_ as decl) = Constr.destFix fix in
let other_result =
@@ -1277,7 +1298,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
(* If we reach this point, the two principle are not mutually recursive
We fall back to the previous method
*)
- let _,const,_ =
+ let entry, _hook =
build_functional_principle
evd
false
@@ -1288,20 +1309,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
(Functional_principles_proofs.prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs)))
(fun _ _ -> ())
in
- const
+ entry
with Found_type i ->
let princ_body =
Termops.it_mkLambda_or_LetIn (Constr.mkFix((idxs,i),decl)) ctxt
in
- {const with
- proof_entry_body =
- (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects));
- proof_entry_type = Some scheme_type
- }
+ Declare.definition_entry ~types:scheme_type princ_body
)
other_fun_princ_types
in
- const::other_result
+ entry::other_result
(* [derive_correctness funs graphs] create correctness and completeness
lemmas for each function in [funs] w.r.t. [graphs]
@@ -1352,7 +1369,8 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
Array.of_list
(List.map
(fun entry ->
- (EConstr.of_constr (fst (fst(Future.force entry.Proof_global.proof_entry_body))), EConstr.of_constr (Option.get entry.Proof_global.proof_entry_type ))
+ (EConstr.of_constr (fst (fst (Future.force entry.Declare.proof_entry_body))),
+ EConstr.of_constr (Option.get entry.Declare.proof_entry_type ))
)
(make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs))
)
@@ -1381,7 +1399,11 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
let lemma = fst @@ Lemmas.by
(Proofview.V82.tactic (proving_tac i)) lemma in
let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
- let finfo = find_Function_infos (fst f_as_constant) in
+ let finfo =
+ match find_Function_infos (fst f_as_constant) with
+ | None -> raise Not_found
+ | Some finfo -> finfo
+ 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
@@ -1443,7 +1465,11 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
(Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
(proving_tac i))) lemma) in
let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
- let finfo = find_Function_infos (fst f_as_constant) in
+ let finfo =
+ match find_Function_infos (fst f_as_constant) with
+ | None -> raise Not_found
+ | Some finfo -> finfo
+ in
let _,lem_cst_constr = Evd.fresh_global
(Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
let (lem_cst,_) = destConst !evd lem_cst_constr in
@@ -2028,7 +2054,11 @@ let build_case_scheme fa =
let sigma, (_,u) = Evd.fresh_constant_instance env sigma funs in
let first_fun = funs in
let funs_mp = Constant.modpath first_fun in
- let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in
+ let first_fun_kn =
+ match find_Function_infos first_fun with
+ | None -> raise No_graph_found
+ | Some finfos -> fst finfos.graph_ind
+ in
let this_block_funs_indexes = get_funs_constant funs_mp first_fun in
let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in
let prop_sort = Sorts.InProp in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index ddd6ecfb5c..7c17ecdba0 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1252,7 +1252,7 @@ let rec compute_cst_params relnames params gt = DAst.with_val (function
| GSort _ -> params
| GHole _ -> params
| GIf _ | GRec _ | GCast _ ->
- raise (UserError(Some "compute_cst_params", str "Not handled case"))
+ CErrors.user_err ~hdr:"compute_cst_params" (str "Not handled case")
) gt
and compute_cst_params_from_app acc (params,rtl) =
let is_gid id c = match DAst.get c with GVar id' -> Id.equal id id' | _ -> false in
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index fbf63c69dd..8abccabae6 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -1,4 +1,13 @@
-open Pp
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
open Constr
open Glob_term
open CErrors
@@ -433,7 +442,8 @@ let replace_var_by_term x_id term =
replace_var_by_pattern lhs,
replace_var_by_pattern rhs
)
- | GRec _ -> raise (UserError(None,str "Not handled GRec"))
+ | GRec _ ->
+ CErrors.user_err (Pp.str "Not handled GRec")
| GSort _
| GHole _ as rt -> rt
| GInt _ as rt -> rt
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 24b3690138..70211a1860 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -1,3 +1,13 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
open Names
open Glob_term
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index eeb2f246c2..a205c0744a 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -8,15 +8,19 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open CErrors
-open Sorts
+open Pp
open Util
+open CErrors
open Names
+open Sorts
open Constr
open EConstr
-open Pp
+
+open Tacmach.New
+open Tacticals.New
+open Tactics
+
open Indfun_common
-open Tactypes
module RelDecl = Context.Rel.Declaration
@@ -37,111 +41,107 @@ let choose_dest_or_ind scheme_info args =
Tactics.induction_destruct (is_rec_info sigma scheme_info) false args)
let functional_induction with_clean c princl pat =
- let res =
- fun g ->
- let sigma = Tacmach.project g in
+ let open Proofview.Notations in
+ Proofview.Goal.enter_one (fun gl ->
+ let sigma = project gl in
let f,args = decompose_app sigma c in
- let princ,bindings, princ_type,g' =
- match princl with
- | None -> (* No principle is given let's find the good one *)
- begin
- match EConstr.kind sigma f with
- | Const (c',u) ->
- let princ_option =
- let finfo = (* we first try to find out a graph on f *)
- try find_Function_infos c'
- with Not_found ->
- user_err (str "Cannot find induction information on "++
- Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
- in
- match Tacticals.elimination_sort_of_goal g with
- | InSProp -> finfo.sprop_lemma
- | InProp -> finfo.prop_lemma
- | InSet -> finfo.rec_lemma
- | InType -> finfo.rect_lemma
+ match princl with
+ | None -> (* No principle is given let's find the good one *)
+ begin
+ match EConstr.kind sigma f with
+ | Const (c',u) ->
+ let princ_option =
+ let finfo = (* we first try to find out a graph on f *)
+ match find_Function_infos c' with
+ | Some finfo -> finfo
+ | None ->
+ user_err (str "Cannot find induction information on "++
+ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
+ in
+ match elimination_sort_of_goal gl with
+ | InSProp -> finfo.sprop_lemma
+ | InProp -> finfo.prop_lemma
+ | InSet -> finfo.rec_lemma
+ | InType -> finfo.rect_lemma
+ in
+ let princ = (* then we get the principle *)
+ match princ_option with
+ | Some princ ->
+ let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) (GlobRef.ConstRef princ) in
+ Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+ Proofview.tclUNIT princ
+ | None ->
+ (*i If there is not default lemma defined then,
+ we cross our finger and try to find a lemma named f_ind
+ (or f_rec, f_rect) i*)
+ let princ_name =
+ Indrec.make_elimination_ident
+ (Label.to_id (Constant.label c'))
+ (elimination_sort_of_goal gl)
in
- let princ,g' = (* then we get the principle *)
+ let princ_ref =
try
- let g',princ =
- Tacmach.pf_eapply (Evd.fresh_global) g (GlobRef.ConstRef (Option.get princ_option )) in
- princ,g'
- with Option.IsNone ->
- (*i If there is not default lemma defined then,
- we cross our finger and try to find a lemma named f_ind
- (or f_rec, f_rect) i*)
- let princ_name =
- Indrec.make_elimination_ident
- (Label.to_id (Constant.label c'))
- (Tacticals.elimination_sort_of_goal g)
- in
- try
- let princ_ref = const_of_id princ_name in
- let (a,b) = Tacmach.pf_eapply (Evd.fresh_global) g princ_ref in
- (b,a)
- (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *)
- with Not_found -> (* This one is neither defined ! *)
- user_err (str "Cannot find induction principle for "
- ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
+ Constrintern.locate_reference (Libnames.qualid_of_ident princ_name)
+ with
+ | Not_found ->
+ user_err (str "Cannot find induction principle for "
+ ++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
in
- (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g')
- | _ -> raise (UserError(None,str "functional induction must be used with a function" ))
- end
- | Some ((princ,binding)) ->
- princ,binding,Tacmach.pf_unsafe_type_of g princ,g
- in
- let sigma = Tacmach.project g' in
- let princ_infos = Tactics.compute_elim_sig (Tacmach.project g') princ_type in
- let args_as_induction_constr =
- let c_list =
- if princ_infos.Tactics.farg_in_concl
- then [c] else []
- in
- if List.length args + List.length c_list = 0
- then user_err Pp.(str "Cannot recognize a valid functional scheme" );
- let encoded_pat_as_patlist =
- List.make (List.length args + List.length c_list - 1) None @ [pat]
- in
- List.map2
- (fun c pat ->
- ((None,
- Tactics.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)))),
- (None,pat),
- None))
- (args@c_list)
- encoded_pat_as_patlist
- in
- let princ' = Some (princ,bindings) in
- let princ_vars =
- List.fold_right
- (fun a acc -> try Id.Set.add (destVar sigma a) acc with DestKO -> acc)
- args
- Id.Set.empty
+ let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) princ_ref in
+ Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+ Proofview.tclUNIT princ
+ in
+ princ >>= fun princ ->
+ (* We need to refresh gl due to the updated evar_map in princ *)
+ Proofview.Goal.enter_one (fun gl ->
+ Proofview.tclUNIT (princ, Tactypes.NoBindings, pf_unsafe_type_of gl princ, args))
+ | _ ->
+ CErrors.user_err (str "functional induction must be used with a function" )
+ end
+ | Some ((princ,binding)) ->
+ Proofview.tclUNIT (princ, binding, pf_unsafe_type_of gl princ, args)
+ ) >>= fun (princ, bindings, princ_type, args) ->
+ Proofview.Goal.enter (fun gl ->
+ let sigma = project gl in
+ let princ_infos = compute_elim_sig (project gl) princ_type in
+ let args_as_induction_constr =
+ let c_list =
+ if princ_infos.Tactics.farg_in_concl
+ then [c] else []
in
- let old_idl = List.fold_right Id.Set.add (Tacmach.pf_ids_of_hyps g) Id.Set.empty in
- let old_idl = Id.Set.diff old_idl princ_vars in
- let subst_and_reduce g =
- if with_clean
- then
- let idl =
- List.filter (fun id -> not (Id.Set.mem id old_idl))
- (Tacmach.pf_ids_of_hyps g)
- in
- let flag =
- Genredexpr.Cbv
- {Redops.all_flags
- with Genredexpr.rDelta = false;
- }
- in
- Tacticals.tclTHEN
- (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Proofview.V82.of_tactic (Equality.subst_gen (do_rewrite_dependent ()) [id]))) idl )
- (Proofview.V82.of_tactic (Tactics.reduce flag Locusops.allHypsAndConcl))
- g
- else Tacticals.tclIDTAC g
+ if List.length args + List.length c_list = 0
+ then user_err Pp.(str "Cannot recognize a valid functional scheme" );
+ let encoded_pat_as_patlist =
+ List.make (List.length args + List.length c_list - 1) None @ [pat]
in
- Tacticals.tclTHEN
- (Proofview.V82.of_tactic (choose_dest_or_ind
- princ_infos
- (args_as_induction_constr,princ')))
- subst_and_reduce
- g'
- in res
+ List.map2
+ (fun c pat ->
+ ((None, ElimOnConstr (fun env sigma -> (sigma,(c,Tactypes.NoBindings)))),
+ (None,pat), None))
+ (args@c_list)
+ encoded_pat_as_patlist
+ in
+ let princ' = Some (princ,bindings) in
+ let princ_vars =
+ List.fold_right
+ (fun a acc -> try Id.Set.add (destVar sigma a) acc with DestKO -> acc)
+ args
+ Id.Set.empty
+ in
+ let old_idl = List.fold_right Id.Set.add (pf_ids_of_hyps gl) Id.Set.empty in
+ let old_idl = Id.Set.diff old_idl princ_vars in
+ let subst_and_reduce gl =
+ if with_clean
+ then
+ let idl = List.filter (fun id -> not (Id.Set.mem id old_idl))(pf_ids_of_hyps gl) in
+ let flag = Genredexpr.Cbv { Redops.all_flags with Genredexpr.rDelta = false } in
+ tclTHEN
+ (tclMAP (fun id -> tclTRY (Equality.subst_gen (do_rewrite_dependent ()) [id])) idl)
+ (reduce flag Locusops.allHypsAndConcl)
+ else tclIDTAC
+ in
+ tclTHEN
+ (choose_dest_or_ind
+ princ_infos
+ (args_as_induction_constr,princ'))
+ (Proofview.Goal.enter subst_and_reduce))
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 97a840e950..476d74b3f8 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -8,9 +8,9 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-val functional_induction :
- bool ->
- EConstr.constr ->
- (EConstr.constr * EConstr.constr Tactypes.bindings) option ->
- Ltac_plugin.Tacexpr.or_and_intro_pattern option ->
- Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+val functional_induction
+ : bool
+ -> EConstr.constr
+ -> (EConstr.constr * EConstr.constr Tactypes.bindings) option
+ -> Ltac_plugin.Tacexpr.or_and_intro_pattern option
+ -> unit Proofview.tactic
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 52a29fb559..80fc64fe65 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -40,7 +40,9 @@ let locate_constant ref =
let locate_with_msg msg f x =
try f x
- with Not_found -> raise (CErrors.UserError(None, msg))
+ with
+ | Not_found ->
+ CErrors.user_err msg
let filter_map filter f =
@@ -64,8 +66,7 @@ let chop_rlambda_n =
| Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b
| Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b
| _ ->
- raise (CErrors.UserError(Some "chop_rlambda_n",
- str "chop_rlambda_n: Not enough Lambdas"))
+ CErrors.user_err ~hdr:"chop_rlambda_n" (str "chop_rlambda_n: Not enough Lambdas")
in
chop_lambda_n []
@@ -76,7 +77,8 @@ let chop_rprod_n =
else
match DAst.get rt with
| Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
- | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products"))
+ | _ ->
+ CErrors.user_err ~hdr:"chop_rprod_n" (str "chop_rprod_n: Not enough products")
in
chop_prod_n []
@@ -92,13 +94,6 @@ let list_union_eq eq_fun l1 l2 =
let list_add_set_eq eq_fun x l =
if List.exists (eq_fun x) l then l else x::l
-let const_of_id id =
- let princ_ref = qualid_of_ident id in
- try Constrintern.locate_reference princ_ref
- with Not_found ->
- CErrors.user_err ~hdr:"IndFun.const_of_id"
- (str "cannot find " ++ Id.print id)
-
[@@@ocaml.warning "-3"]
let coq_constant s =
UnivGen.constr_of_monomorphic_global @@
@@ -112,29 +107,6 @@ let find_reference sl s =
let eq = lazy(EConstr.of_constr (coq_constant "eq"))
let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl"))
-(*****************************************************************)
-(* Copy of the standard save mechanism but without the much too *)
-(* slow reduction function *)
-(*****************************************************************)
-open Declare
-open DeclareDef
-
-let definition_message = Declare.definition_message
-
-let save name const ?hook uctx scope kind =
- let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in
- let r = match scope with
- | Discharge ->
- let c = SectionLocalDef const in
- let () = declare_variable ~name ~kind c in
- GlobRef.VarRef name
- | Global local ->
- let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in
- GlobRef.ConstRef kn
- in
- DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r });
- definition_message name
-
let with_full_print f a =
let old_implicit_args = Impargs.is_implicit_args ()
and old_strict_implicit_args = Impargs.is_strict_implicit_args ()
@@ -301,20 +273,16 @@ let find_or_none id =
)
with Not_found -> None
-
-
let find_Function_infos f =
- Cmap_env.find f !from_function
-
+ Cmap_env.find_opt f !from_function
let find_Function_of_graph ind =
- Indmap.find ind !from_graph
+ Indmap.find_opt ind !from_graph
let update_Function finfo =
(* Pp.msgnl (pr_info finfo); *)
Lib.add_anonymous_leaf (in_Function finfo)
-
let add_Function is_general f =
let f_id = Label.to_id (Constant.label f) in
let equation_lemma = find_or_none (mk_equation_id f_id)
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index fff4711044..cd5202a6c7 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -38,20 +38,10 @@ val chop_rprod_n : int -> Glob_term.glob_constr ->
val eq : EConstr.constr Lazy.t
val refl_equal : EConstr.constr Lazy.t
-val const_of_id: Id.t -> GlobRef.t(* constantyes *)
val jmeq : unit -> EConstr.constr
val jmeq_refl : unit -> EConstr.constr
val make_eq : unit -> EConstr.constr
-val save
- : Id.t
- -> Evd.side_effects Proof_global.proof_entry
- -> ?hook:DeclareDef.Hook.t
- -> UState.t
- -> DeclareDef.locality
- -> Decls.logical_kind
- -> unit
-
(* [with_full_print f a] applies [f] to [a] in full printing environment.
This function preserves the print settings
@@ -75,8 +65,8 @@ type function_info =
is_general : bool;
}
-val find_Function_infos : Constant.t -> function_info
-val find_Function_of_graph : inductive -> function_info
+val find_Function_infos : Constant.t -> function_info option
+val find_Function_of_graph : inductive -> function_info option
(* WARNING: To be used just after the graph definition !!! *)
val add_Function : bool -> Constant.t -> unit
val update_Function : function_info -> unit
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 38fdd789a3..d72319d078 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -34,9 +34,10 @@ let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl ->
let ((kn',num) as ind'),u = destInd sigma i in
if MutInd.equal kn kn'
then (* We have generated a graph hypothesis so that we must change it if we can *)
- let info =
- try find_Function_of_graph ind'
- with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*)
+ let info = match find_Function_of_graph ind' with
+ | Some info -> info
+ | None ->
+ (* The graphs are mutually recursive but we cannot find one of them !*)
CErrors.anomaly (Pp.str "Cannot retrieve infos about a mutual block.")
in
(* if we can find a completeness lemma for this function
@@ -108,18 +109,20 @@ let invfun qhyp f =
| _ ->
CErrors.user_err Pp.(str "Not a function")
in
- try
- let finfos = find_Function_infos f in
- let f_correct = mkConst(Option.get finfos.correctness_lemma)
- and kn = fst finfos.graph_ind in
- Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f) f_correct) qhyp
- with
- | Not_found -> CErrors.user_err (Pp.str "No graph found")
- | Option.IsNone -> CErrors.user_err (Pp.str "Cannot use equivalence with graph!")
-
-exception NoFunction
+ match find_Function_infos f with
+ | None ->
+ CErrors.user_err (Pp.str "No graph found")
+ | Some finfos ->
+ match finfos.correctness_lemma with
+ | None ->
+ CErrors.user_err (Pp.str "Cannot use equivalence with graph!")
+ | Some f_correct ->
+ let f_correct = mkConst f_correct
+ and kn = fst finfos.graph_ind in
+ Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f) f_correct) qhyp
let invfun qhyp f =
+ let exception NoFunction in
match f with
| Some f -> invfun qhyp f
| None ->
@@ -132,31 +135,33 @@ let invfun qhyp f =
let f1,_ = decompose_app sigma args.(1) in
try
if not (isConst sigma f1) then raise NoFunction;
- let finfos = find_Function_infos (fst (destConst sigma f1)) in
+ let finfos = Option.get (find_Function_infos (fst (destConst sigma f1))) in
let f_correct = mkConst(Option.get finfos.correctness_lemma)
and kn = fst finfos.graph_ind
in
functional_inversion kn hid f1 f_correct
- with | NoFunction | Option.IsNone | Not_found ->
- try
- let f2,_ = decompose_app sigma args.(2) in
- if not (isConst sigma f2) then raise NoFunction;
- let finfos = find_Function_infos (fst (destConst sigma f2)) in
- let f_correct = mkConst(Option.get finfos.correctness_lemma)
- and kn = fst finfos.graph_ind
- in
- functional_inversion kn hid f2 f_correct
with
- | NoFunction ->
- CErrors.user_err Pp.(str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
- | Option.IsNone ->
- if do_observe ()
- then CErrors.user_err (Pp.str "Cannot use equivalence with graph for any side of the equality")
- else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
- | Not_found ->
- if do_observe ()
- then CErrors.user_err (Pp.str "No graph found for any side of equality")
- else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+ | NoFunction | Option.IsNone ->
+ let f2,_ = decompose_app sigma args.(2) in
+ if isConst sigma f2 then
+ match find_Function_infos (fst (destConst sigma f2)) with
+ | None ->
+ if do_observe ()
+ then CErrors.user_err (Pp.str "No graph found for any side of equality")
+ else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+ | Some finfos ->
+ match finfos.correctness_lemma with
+ | None ->
+ if do_observe ()
+ then CErrors.user_err (Pp.str "Cannot use equivalence with graph for any side of the equality")
+ else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+ | Some f_correct ->
+ let f_correct = mkConst f_correct
+ and kn = fst finfos.graph_ind
+ in
+ functional_inversion kn hid f2 f_correct
+ else (* NoFunction *)
+ CErrors.user_err Pp.(str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
end
| _ -> CErrors.user_err Pp.(Ppconstr.pr_id hid ++ str " must be an equality ")
in
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 05:01:57 +0000