Merge PR coq#19259: Merge the code paths for "CoFixpoint"/"Fixpoint" …

…and "Theorem with" Reviewed-by: SkySkimmer Ack-by: ejgallego Ack-by: Alizter Co-authored-by: SkySkimmer <[email protected]>
SkySkimmer · Jul 3, 2024 · 4d68031 · 4d68031
2 parents 16e3f49 + 5bc7f5a
commit 4d68031
Show file tree

Hide file tree

Showing 9 changed files with 114 additions and 107 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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,20 +28,20 @@ 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 =
         let cclenv = EConstr.push_rel_context hyps (Global.env()) in
         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
@@ -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
@@ -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
-Original file line number
+Diff line change
@@ Expand Up @@
     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
@@ Expand Down @@