diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 9e85d0e2151d..1f0ed91884f3 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -404,7 +404,7 @@ let register_struct is_rec (rec_order, fixpoint_exprl) = in (None, evd, List.rev rev_pconstants) | _ -> - let pm, p = ComFixpoint.do_mutually_recursive ~poly:false (CFixRecOrder rec_order, fixpoint_exprl) in + let pm, p = ComFixpoint.do_mutually_recursive ~program_mode:false ~poly:false (CFixRecOrder rec_order, fixpoint_exprl) in assert (Option.is_empty pm && Option.is_empty p); let evd, rev_pconstants = List.fold_left diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v index b98002667552..e28aa22f0f5d 100644 --- a/test-suite/success/proof_using.v +++ b/test-suite/success/proof_using.v @@ -241,6 +241,18 @@ CoFixpoint g' : Stream. exact (Cons g). Defined. +#[using="e"] +Lemma g1 (n:nat) : nat with g2 (n:nat) : m = m. +exact (match n with 0 => 0 | S n => match g2 n with eq_refl => n end end). +exact (match n with 0 => eq_refl | S n => match g1 n with 0 => eq_refl | S _ => eq_refl end end). +Defined. + +#[using="Type"] +Lemma g1' (n:nat) : nat with g2' (n:nat) : m = m. +exact (match n with 0 => 0 | S n => match g2' n with eq_refl => n end end). +exact (match n with 0 => eq_refl | S n => match g1' n with 0 => eq_refl | S _ => eq_refl end end). +Defined. + End S. Check eq_refl : a 0 (eq_refl 0) = 0. @@ -251,5 +263,7 @@ Check eq_refl : f1 10 2 = 1. Check eq_refl : f1' 10 2 = 1. Check g 0 eq_refl : Stream. Check g' 0 eq_refl : Stream. +Check eq_refl : g1 10 (eq_refl 10) 2 = 1. +Check eq_refl : g1' 10 2 = 1. End InteractiveUsing. diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 0b80fd9f45ec..fbc8a8410f51 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -315,20 +315,20 @@ let find_rec_annot ~program_mode ~function_mode Vernacexpr.{fname={CAst.loc}; bi | None, rfel -> default_order rfel in Some (r, mes), [] (* useless: will use Fix_sub *) -let interp_rec_annot ~program_mode ~function_mode fixl ctxl rec_order = +let interp_rec_annot ~program_mode ~function_mode sigma fixl ctxl ccll rec_order = let open Pretyping in - let fixkind, (possibly_cofix, fixwf_guard) = - match rec_order with + let nowf () = List.map (fun _ -> None) fixl in + match rec_order with (* If recursive argument was not given by user, we try all args. An earlier approach was to look only for inductive arguments, but doing it properly involves delta-reduction, and it finally doesn't seem to worth the effort (except for huge mutual fixpoints ?) *) - | CFixRecOrder fix_orders -> Decls.Fixpoint, (false, List.map3 (find_rec_annot ~program_mode ~function_mode) fixl ctxl fix_orders) - | CCoFixRecOrder -> Decls.CoFixpoint, (true, List.map (fun _ -> (None, [])) fixl) - | CUnknownRecOrder -> Decls.Definition, (true, List.map2 (fun fix ctx -> find_rec_annot ~program_mode ~function_mode fix ctx None) fixl ctxl) in - let fixwf, possible_fix_indices = List.split fixwf_guard in - (fixkind, fixwf, {possibly_cofix; possible_fix_indices}) + | CFixRecOrder fix_orders -> + let fixwf, possible_guard = List.split (List.map3 (find_rec_annot ~program_mode ~function_mode) fixl ctxl fix_orders) in + Decls.Fixpoint, fixwf, {possibly_cofix = false; possible_fix_indices = possible_guard} + | CCoFixRecOrder -> Decls.CoFixpoint, nowf (), {possibly_cofix = true; possible_fix_indices = List.map (fun _ -> []) fixl} + | CUnknownRecOrder -> Decls.Definition, nowf (), RecLemmas.find_mutually_recursive_statements sigma ctxl ccll let interp_fix_context ~program_mode env sigma {Vernacexpr.binders} = let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma binders in @@ -418,10 +418,10 @@ let interp_mutual_definition env ~program_mode ~function_mode rec_order fixl = let sigma, (fixenv, fixctxs, fixctximpenvs, fixctximps) = on_snd List.split4 @@ List.fold_left_map (fun sigma -> interp_fix_context ~program_mode env sigma) sigma fixl in - let fixkind, fixwfs, possible_guard = interp_rec_annot ~program_mode ~function_mode fixl fixctxs rec_order in let sigma, (fixccls,fixrs,fixcclimps) = on_snd List.split3 @@ List.fold_left3_map (interp_fix_ccl ~program_mode) sigma fixctximpenvs fixenv fixl in + let fixkind, fixwfs, possible_guard = interp_rec_annot ~program_mode ~function_mode sigma fixl fixctxs fixccls rec_order in let sigma, (fixextras, fixwfs, fixwfimps) = on_snd List.split3 @@ (List.fold_left4_map (interp_wf ~program_mode env) sigma fixnames fixctxs fixccls fixwfs) in let fixtypes = List.map3 (build_fix_type sigma) fixctxs fixccls fixextras in @@ -533,21 +533,22 @@ let finish_obligations env sigma rec_sign possible_guard poly udecl = function let fixrs = List.map (EConstr.ERelevance.kind sigma) fixrs in sigma, {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs}, obls, None -let finish_regular env sigma fix = - let sigma = Pretyping.(solve_remaining_evars all_no_fail_flags env sigma) in +let finish_regular env sigma use_inference_hook fix = + let inference_hook = if use_inference_hook then Some Declare.Obls.program_inference_hook else None in + let sigma = Pretyping.(solve_remaining_evars ?hook:inference_hook all_no_fail_flags env sigma) in sigma, ground_fixpoint env sigma fix, [], None -let do_mutually_recursive ?pm ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using (rec_order, fixl) +let do_mutually_recursive ?pm ~program_mode ?(use_inference_hook=false) ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using (rec_order, fixl) : Declare.OblState.t option * Declare.Proof.t option = let env = Global.env () in let env = Environ.update_typing_flags ?typing_flags env in - let (env,rec_sign,sigma),(fix,isfix,possible_guard,udecl) = interp_mutual_definition env ~program_mode:(Option.has_some pm) ~function_mode:false rec_order fixl in + let (env,rec_sign,sigma),(fix,isfix,possible_guard,udecl) = interp_mutual_definition env ~program_mode ~function_mode:false rec_order fixl in check_recursive ~isfix env sigma fix; let kind = Decls.IsDefinition isfix in let sigma, ({fixdefs=bodies;fixrs;fixtypes;fixwfs} as fix), obls, hook = match pm with | Some pm -> finish_obligations env sigma rec_sign possible_guard poly udecl fix - | None -> finish_regular env sigma fix in + | None -> finish_regular env sigma use_inference_hook fix in let info = Declare.Info.make ?scope ?clearbody ~kind ~poly ~udecl ?hook ?typing_flags ?user_warns ~ntns:fix.fixntns () in let cinfo = build_recthms fix in match pm with diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index fc21f06814cd..cf07d1fde6d7 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -16,14 +16,29 @@ open Vernacexpr val do_mutually_recursive : ?pm:Declare.OblState.t + (* Obligation mode turns unresolved evars into obligations *) + -> program_mode:bool + (* [program_mode] means here: + - a special treatment of subsets in pretyping + - a special treatment of type class inference in pretyping + - if a wf/measure fixpoint, encapsulation under a combinator (in which case, it requires [pm]) + Note: for turning unresolved evars into obligations, set also [pm] *) + -> ?use_inference_hook:bool + (* Tell to try the obligation tactic to solve evars *) -> ?scope:Locality.definition_scope + (* Local or Global visibility *) -> ?clearbody:bool + (* Hide body if in sections *) -> poly:bool + (* Use universe polymorphism *) -> ?typing_flags:Declarations.typing_flags -> ?user_warns:UserWarn.t + (* Warnings and deprecations *) -> ?using:Vernacexpr.section_subset_expr + (* Tell which section variables to use *) -> recursives_expr -> Declare.OblState.t option * Declare.Proof.t option + (* Returns open obligations and open proof, if any *) (************************************************************************) (** Internal API *) diff --git a/vernac/declare.ml b/vernac/declare.ml index 4e24505ddc34..0508e0af0550 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1538,6 +1538,7 @@ module Proof_ending = struct end (* Alias *) +module Proof_ = Proof module Proof = struct module Proof_info = struct @@ -2763,6 +2764,27 @@ let check_program_libraries () = Coqlib.check_required_library Coqlib.datatypes_module_name; Coqlib.check_required_library ["Coq";"Init";"Specif"] +let program_inference_hook env sigma ev = + let tac = !default_tactic in + let evi = Evd.find_undefined sigma ev in + let evi = Evarutil.nf_evar_info sigma evi in + let env = Evd.evar_filtered_env env evi in + try + let concl = Evd.evar_concl evi in + if not (Evarutil.is_ground_env sigma env && + Evarutil.is_ground_term sigma concl) + then None + else + let c, sigma = + Proof_.refine_by_tactic ~name:(Id.of_string "program_subproof") + ~poly:false env sigma concl (Tacticals.tclSOLVE [tac]) + in + Some (sigma, c) + with + | (Proof.OpenProof _ as e | Logic_monad.TacticFailure e) when CErrors.noncritical e -> + CErrors.user_err Pp.(str "The statement obligations could not be resolved \ + automatically, write a statement definition first.") + (* aliases *) let prepare_obligations = prepare_obligations let check_solved_obligations = diff --git a/vernac/declare.mli b/vernac/declare.mli index 3121491ee75b..253320102331 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -598,6 +598,8 @@ val admit_obligations : pm:OblState.t -> Names.Id.t option -> OblState.t val check_program_libraries : unit -> unit +val program_inference_hook : Environ.env -> Evd.evar_map -> Evar.t -> (Evd.evar_map * EConstr.t) option + end val is_local_constant : Constant.t -> bool diff --git a/vernac/recLemmas.ml b/vernac/recLemmas.ml index 4518be844370..1f49b411b22a 100644 --- a/vernac/recLemmas.ml +++ b/vernac/recLemmas.ml @@ -14,10 +14,10 @@ open Declarations module RelDecl = Context.Rel.Declaration -let find_mutually_recursive_statements sigma thms = - let inds = List.map (fun x -> - let typ = Declare.CInfo.get_typ x in - let (hyps,ccl) = EConstr.decompose_prod_decls sigma typ in +let find_mutually_recursive_statements sigma ctxs ccls = + let inds = List.map2 (fun ctx ccl -> + let (hyps,ccl) = EConstr.decompose_prod_decls sigma ccl in + let hyps = hyps @ ctx in let whnf_hyp_hds = EConstr.map_rel_context_in_env (fun env c -> fst (Reductionops.whd_all_stack env sigma c)) (Global.env()) hyps in @@ -28,7 +28,7 @@ let find_mutually_recursive_statements sigma thms = | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in mind.mind_finite <> Declarations.CoFinite -> - [ind,x,i] + [ind,i] | _ -> []) 0 (List.rev (List.filter Context.Rel.Declaration.is_local_assum whnf_hyp_hds))) in let ind_ccl = @@ -36,12 +36,12 @@ let find_mutually_recursive_statements sigma thms = let whnf_ccl,_ = Reductionops.whd_all_stack cclenv sigma ccl in match EConstr.kind sigma whnf_ccl with | Ind ((kn,_ as ind),u) when (Global.lookup_mind kn).mind_finite == Declarations.CoFinite -> - [ind,x,0] + [ind,0] | _ -> [] in - ind_hyps,ind_ccl) thms in + ind_hyps,ind_ccl) ctxs ccls in let inds_hyps,ind_ccls = List.split inds in - let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> Environ.QMutInd.equal (Global.env ()) kn kn' in + let of_same_mutind ((kn,_),_) = function ((kn',_),_) -> Environ.QMutInd.equal (Global.env ()) kn kn' in (* Check if all conclusions are coinductive in the same type *) (* (degenerated cartesian product since there is at most one coind ccl) *) let same_indccl = @@ -58,23 +58,9 @@ let find_mutually_recursive_statements sigma thms = | [] -> [] | _::_ -> (* assume the largest indices as possible *) - List.map (List.map pi3) inds_hyps in + List.map (List.map snd) inds_hyps in if not possibly_cofix && List.is_empty possible_fix_indices then CErrors.user_err Pp.(str ("Cannot find common (mutual) inductive premises or coinductive" ^ " conclusions in the statements.")); Pretyping.{possibly_cofix; possible_fix_indices} - -type mutual_info = - | NonMutual of EConstr.t Declare.CInfo.t - | Mutual of Pretyping.possible_guard - -let look_for_possibly_mutual_statements sigma thms : mutual_info = - match thms with - | [thm] -> - (* One non recursively proved theorem *) - NonMutual thm - | _::_ as thms -> - (* More than one statement and/or an explicit decreasing mark: *) - Mutual (find_mutually_recursive_statements sigma thms) - | [] -> CErrors.anomaly (Pp.str "Empty list of theorems.") diff --git a/vernac/recLemmas.mli b/vernac/recLemmas.mli index 221b4c164822..f6c4e36e2174 100644 --- a/vernac/recLemmas.mli +++ b/vernac/recLemmas.mli @@ -8,11 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -type mutual_info = - | NonMutual of EConstr.t Declare.CInfo.t - | Mutual of Pretyping.possible_guard - -val look_for_possibly_mutual_statements +val find_mutually_recursive_statements : Evd.evar_map - -> EConstr.t Declare.CInfo.t list - -> mutual_info + -> EConstr.rel_context list + -> EConstr.t list + -> Pretyping.possible_guard diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 504e8c49fa2d..fcb3e885a48d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -607,64 +607,26 @@ let check_name_freshness locality {CAst.loc;v=id} : unit = then user_err ?loc (Id.print id ++ str " already exists.") -let program_inference_hook env sigma ev = - let tac = !Declare.Obls.default_tactic in - let evi = Evd.find_undefined sigma ev in - let evi = Evarutil.nf_evar_info sigma evi in - let env = Evd.evar_filtered_env env evi in - try - let concl = Evd.evar_concl evi in - if not (Evarutil.is_ground_env sigma env && - Evarutil.is_ground_term sigma concl) - then None - else - let c, sigma = - Proof.refine_by_tactic ~name:(Id.of_string "program_subproof") - ~poly:false env sigma concl (Tacticals.tclSOLVE [tac]) - in - Some (sigma, c) - with - | Logic_monad.TacticFailure e when noncritical e -> - user_err Pp.(str "The statement obligations could not be resolved \ - automatically, write a statement definition first.") - -(* XXX: Interpretation of lemma command, duplication with ComFixpoint - / ComDefinition ? *) -let interp_lemma ~program_mode ~flags ~scope env0 evd thms = - let inference_hook = if program_mode then Some program_inference_hook else None in - List.fold_left_map (fun evd ((id, _), (bl, t)) -> - let evd, (impls, ((env, ctx), imps)) = - Constrintern.interp_context_evars ~program_mode env0 evd bl - in - let evd, (t', imps') = Constrintern.interp_type_evars_impls ~flags ~impls env evd t in - let flags = Pretyping.{ all_and_fail_flags with program_mode } in - let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in - let ids = List.map Context.Rel.Declaration.get_name ctx in - let typ = EConstr.it_mkProd_or_LetIn t' ctx in - let thm = Declare.CInfo.make ~name:id.CAst.v ~typ ~args:ids ~impargs:(imps @ imps') () in - evd, (EConstr.to_constr evd typ, thm)) - evd thms - -let start_lemma_com ~typing_flags ~program_mode ~poly ~scope ?clearbody ~kind ?user_warns ?using ?hook thms = +let start_lemma_com ~typing_flags ~program_mode ~poly ~scope ?clearbody ~kind ?user_warns ?using ?hook ((id, udecl), (bl, t)) = let env0 = Global.env () in let env0 = Environ.update_typing_flags ?typing_flags env0 in let flags = Pretyping.{ all_no_fail_flags with program_mode } in - let udecls = List.map (fun ((_,univs),_) -> univs) thms in - let evd, udecl = Constrintern.interp_mutual_univ_decl_opt env0 udecls in - let evd, thms = interp_lemma ~program_mode ~flags ~scope env0 evd thms in - let typs, thms = List.split thms in - let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in + let evd, udecl = Constrintern.interp_univ_decl_opt env0 udecl in + let evd, (impls, ((env, ctx), imps)) = Constrintern.interp_context_evars ~program_mode env0 evd bl in + let evd, (t', imps') = Constrintern.interp_type_evars_impls ~flags ~impls env evd t in + let ids = List.map Context.Rel.Declaration.get_name ctx in + let typ = EConstr.it_mkProd_or_LetIn t' ctx in + let evd = + let inference_hook = if program_mode then Some Declare.Obls.program_inference_hook else None in + Pretyping.solve_remaining_evars ?hook:inference_hook flags env0 evd in let evd = Evd.minimize_universes evd in + Pretyping.check_evars_are_solved ~program_mode env0 evd; let info = Declare.Info.make ?hook ~poly ~scope ?clearbody ~kind ~udecl ?typing_flags ?user_warns () in - Evd.check_univ_decl_early ~poly ~with_obls:false evd udecl typs; + let typ = EConstr.to_constr evd typ in + Evd.check_univ_decl_early ~poly ~with_obls:false evd udecl [typ]; let evd = if poly then evd else Evd.fix_undefined_variables evd in - match mut_analysis with - | RecLemmas.NonMutual thm -> - let thm = Declare.CInfo.to_constr evd thm in - Declare.Proof.start_definition ~info ~cinfo:thm ?using evd - | RecLemmas.Mutual possible_guard -> - let cinfo = List.map (Declare.CInfo.to_constr evd) thms in - Declare.Proof.start_mutual_definitions ~info ~cinfo ~possible_guard ?using evd + let thm = Declare.CInfo.make ~name:id.CAst.v ~typ ~args:ids ~impargs:(imps @ imps') () in + Declare.Proof.start_definition ~info ~cinfo:thm ?using evd let vernac_definition_hook ~canonical_instance ~local ~poly ~reversible = let open Decls in function | Coercion -> @@ -692,6 +654,7 @@ let vernac_definition_name lid local = | { v = Name.Name n; loc } -> CAst.make ?loc n in check_name_freshness local lid; let () = + if Dumpglob.dump () then match local with | Discharge -> Dumpglob.dump_definition lid true "var" | Global _ -> Dumpglob.dump_definition lid false "def" @@ -706,7 +669,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let hook = vernac_definition_hook ~canonical_instance ~local ~poly ~reversible kind in let name = vernac_definition_name lid scope in start_lemma_com ~typing_flags ~program_mode ~poly ~scope ?clearbody - ~kind:(Decls.IsDefinition kind) ?user_warns ?using ?hook [(name, pl), (bl, t)] + ~kind:(Decls.IsDefinition kind) ?user_warns ?using ?hook ((name, pl), (bl, t)) let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_opt = let open DefAttributes in @@ -738,14 +701,21 @@ let vernac_start_proof ~atts kind l = let open DefAttributes in if Dumpglob.dump () then List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; - let scope, poly, program_mode, user_warns, typing_flags, using = - atts.scope, atts.polymorphic, atts.program, atts.user_warns, atts.typing_flags, atts.using in + let scope, local, poly, program_mode, user_warns, typing_flags, using, clearbody = + atts.scope, atts.locality, atts.polymorphic, atts.program, atts.user_warns, atts.typing_flags, atts.using, atts.clearbody in List.iter (fun ((id, _), _) -> check_name_freshness scope id) l; - start_lemma_com - ~typing_flags - ~program_mode - ~poly - ~scope ~kind:(Decls.IsProof kind) ?user_warns ?using l + match l with + | [] -> assert false + | [decl] -> + start_lemma_com ~typing_flags ~program_mode ~poly ~scope ~kind:(Decls.IsProof kind) ?user_warns ?using decl + | _ -> + let fix = List.map (fun ((fname, univs), (binders, rtype)) -> + { fname; binders; rtype; body_def = None; univs; notations = []}) l in + let pm, proof = + ComFixpoint.do_mutually_recursive ~program_mode ~use_inference_hook:program_mode + ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using (CUnknownRecOrder, fix) in + assert (Option.is_empty pm); + Option.get proof let vernac_end_proof ~lemma ~pm = let open Vernacexpr in function | Admitted -> @@ -1079,9 +1049,9 @@ let vernac_fixpoint_common ~atts l = let with_obligations program_mode f pm = if program_mode then - f pm + f pm ~program_mode:true else - let pm', proof = f None in + let pm', proof = f None ~program_mode:false in assert (Option.is_empty pm'); pm, proof