[function] always open a proof when used with `wf` or `measure`

9 files changed, 92 insertions, 44 deletions

diff --git a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst
new file mode 100644
index 0000000000..53828db951
--- /dev/null
+++ b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst
@@ -0,0 +1,5 @@
+- Function always opens a proof when used with a ``measure`` or ``wf``
+  annotation, see Description of the changes, with possible link to
+  :ref:`advanced-recursive-functions` of the updated documentation
+  (`#10215 <https://github.com/coq/coq/pull/10215>`_,
+  by Enrico Tassi).
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 8c5ad785e4..c93984661e 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -737,7 +737,7 @@ used by ``Function``. A more precise description is given below.
       decreases at each recursive call of :token:`term`. The order must be well-founded.
       Parameters of the function are bound in :token:`term`.
 
-   Depending on the annotation, the user is left with some proof
+   If the annotation is ``measure`` or ``fw``, the user is left with some proof
    obligations that will be used to define the function. These proofs
    are: proofs that each recursive call is actually decreasing with
    respect to the given criteria, and (if the criteria is `wf`) a proof
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index bdd30aae0a..833ff9f1ed 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -173,24 +173,41 @@ let () =
   let raw_printer env sigma _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in
   Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer
 
+let is_proof_termination_interactively_checked recsl =
+  List.exists (function
+  | _,((_,( Some { CAst.v = CMeasureRec _ }
+          | Some { CAst.v = CWfRec _}),_,_,_),_) -> true
+  | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_)
+  | _,((_,None,_,_,_),_) -> false) recsl
+
+let classify_as_Fixpoint recsl =
+ Vernac_classifier.classify_vernac
+    (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
+
+let classify_funind recsl =
+  match classify_as_Fixpoint recsl with
+  | Vernacextend.VtSideff ids, _
+    when is_proof_termination_interactively_checked recsl ->
+      Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater)
+  | x -> x
+
+let is_interactive recsl =
+  match classify_funind recsl with
+  | Vernacextend.VtStartProof _, _ -> true
+  | _ -> false
+
 }
 
-(* TASSI: n'importe quoi ! *)
-VERNAC COMMAND EXTEND Function STATE maybe_open_proof
+VERNAC COMMAND EXTEND Function STATE CUSTOM
 | ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
-    => { let hard = List.exists (function
-           | _,((_,(Some { CAst.v = CMeasureRec _ }
-             | Some { CAst.v = CWfRec _}),_,_,_),_) -> true
-           | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_)
-           | _,((_,None,_,_,_),_) -> false) recsl in
-         match
-           Vernac_classifier.classify_vernac
-             (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
-         with
-         | Vernacextend.VtSideff ids, _ when hard ->
-             Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater)
-         | x -> x }
-    -> { do_generate_principle false (List.map snd recsl) }
+    => { classify_funind recsl }
+    -> {
+         if is_interactive recsl then
+           Vernacextend.VtOpenProof (fun () ->
+             do_generate_principle_interactive (List.map snd recsl))
+         else
+           Vernacextend.VtDefault (fun () ->
+             do_generate_principle (List.map snd recsl)) }
 END
 
 {
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 7c6669d0fc..bb6db1f5cf 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -459,7 +459,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
     tcc_lemma_ref is_mes  rec_arg_num rec_arg_type relation
 
 
-let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
+let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
     pre_hook
     =
   let type_of_f = Constrexpr_ops.mkCProdN args ret_type in
@@ -500,8 +500,8 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
       (* No proof done *)
       ()
   in
-  Recdef.recursive_definition
-    is_mes fname rec_impls
+  Recdef.recursive_definition ~interactive_proof
+    ~is_mes fname rec_impls
     type_of_f
     wf_rel_expr
     rec_arg_num
@@ -510,7 +510,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
     using_lemmas
 
 
-let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas args ret_type body =
+let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas args ret_type body =
   let wf_arg_type,wf_arg =
     match wf_arg with
       | None ->
@@ -570,7 +570,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 	  in
 	  wf_rel_with_mes,false
   in			       
-  register_wf ~is_mes:is_mes fname rec_impls wf_rel_from_mes wf_arg
+  register_wf interactive_proof ~is_mes:is_mes fname rec_impls wf_rel_from_mes wf_arg
     using_lemmas args ret_type body
 
 let map_option f = function 
@@ -633,7 +633,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
   fixpoint_exprl_with_new_bl
   
 
-let do_generate_principle pconstants on_error register_built interactive_proof
+let do_generate_principle_aux pconstants on_error register_built interactive_proof
     (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.t option =
   List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl;
   let pstate, _is_struct =
@@ -660,7 +660,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	      true
 	  in
 	  if register_built
-          then register_wf name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false
+          then register_wf interactive_proof name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false
           else None, false
       |[((_,Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)},_,_,_),_) as fixpoint_expr] ->
           let (((({CAst.v=name},_),_,args,types,body)),_)  as fixpoint_expr =
@@ -684,7 +684,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	      true
 	  in
 	  if register_built
-          then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true
+          then register_mes interactive_proof name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true
           else None, true
       | _ ->
           List.iter (function ((_na,ord,_args,_body,_type),_not) ->
@@ -902,11 +902,27 @@ let make_graph (f_ref : GlobRef.t) =
                  [((CAst.make id,None),None,nal_tas,t,Some b),[]]
 	 in
          let mp = Constant.modpath c in
-         let pstate = do_generate_principle [c,Univ.Instance.empty] error_error  false false expr_list in
+         let pstate = do_generate_principle_aux [c,Univ.Instance.empty] error_error  false false expr_list in
          assert (Option.is_empty pstate);
 	 (* We register the infos *)
 	 List.iter
            (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id)))
            expr_list)
 
-let do_generate_principle = do_generate_principle [] warning_error true
+(* *************** statically typed entrypoints ************************* *)
+
+let do_generate_principle_interactive fixl : Proof_global.t =
+  match
+    do_generate_principle_aux [] warning_error true true fixl
+  with
+  | Some pstate -> pstate
+  | None ->
+      CErrors.anomaly
+       (Pp.str"indfun: leaving no open proof in interactive mode")
+
+let do_generate_principle fixl : unit =
+  match do_generate_principle_aux [] warning_error true false fixl  with
+  | Some _pstate ->
+      CErrors.anomaly
+        (Pp.str"indfun: leaving a goal open in non-interactive mode")
+  | None -> ()
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 47d37b29a5..1ba245a45d 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -6,9 +6,11 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 
 val do_generate_principle :
-  bool ->
+  (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit
+
+val do_generate_principle_interactive :
   (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list ->
-  Proof_global.t option
+  Proof_global.t
 
 val functional_induction :
   bool ->
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5a682e7231..e2321d233c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1395,12 +1395,10 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type
 	       ) tclIDTAC)
             g end) pstate
   in
-  try
-    Some (fst @@ by (Proofview.V82.tactic tclIDTAC) pstate) (* raises UserError _ if the proof is complete *)
-  with UserError _ ->
-    (defined pstate; None)
+  if Proof_global.get_open_goals pstate = 0 then (defined pstate; None) else Some pstate
 
 let com_terminate
+    interactive_proof
     tcc_lemma_name
     tcc_lemma_ref
     is_mes
@@ -1430,8 +1428,8 @@ let com_terminate
   with EmptySubgoals ->
     (* a non recursive function declared with measure ! *)
     tcc_lemma_ref := Not_needed;
-    defined pstate;
-    None
+    if interactive_proof then Some pstate
+    else (defined pstate; None)
 
 let start_equation (f:GlobRef.t) (term_f:GlobRef.t)
   (cont_tactic:Id.t list -> tactic) g =
@@ -1494,7 +1492,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
 (*      Pp.msgnl (fun _ _ -> str "eqn finished"); *)
 
 
-let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
+let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type_of_f r rec_arg_num eq
     generate_induction_principle using_lemmas : Proof_global.t option =
   let open Term in
   let open Constr in
@@ -1585,6 +1583,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   (* XXX STATE Why do we need this... why is the toplevel protection not enough *)
   funind_purify (fun () ->
       let pstate = com_terminate
+          interactive_proof
           tcc_lemma_name
           tcc_lemma_constr
           is_mes functional_ref
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 90f9c449b1..b92ac3a0ec 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -5,13 +5,19 @@ val tclUSER_if_not_mes :
   bool -> 
   Names.Id.t list option -> 
   Tacmach.tactic
+
 val recursive_definition :  
-bool ->
-           Names.Id.t ->
-           Constrintern.internalization_env ->
-           Constrexpr.constr_expr ->
-           Constrexpr.constr_expr ->
-           int -> Constrexpr.constr_expr -> (pconstant ->
-            Indfun_common.tcc_lemma_value ref ->
-            pconstant ->
-            pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.t option
+  interactive_proof:bool ->
+  is_mes:bool ->
+  Names.Id.t ->
+  Constrintern.internalization_env ->
+  Constrexpr.constr_expr ->
+  Constrexpr.constr_expr ->
+  int ->
+  Constrexpr.constr_expr ->
+  (pconstant ->
+   Indfun_common.tcc_lemma_value ref ->
+   pconstant ->
+   pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) ->
+  Constrexpr.constr_expr list ->
+    Proof_global.t option
diff --git a/test-suite/bugs/closed/bug_1618.v b/test-suite/bugs/closed/bug_1618.v
index a7be12e26f..041055a38f 100644
--- a/test-suite/bugs/closed/bug_1618.v
+++ b/test-suite/bugs/closed/bug_1618.v
@@ -20,3 +20,4 @@ a :=
   match a return (P a) with
     | A1 n => f n
   end.
+Proof. Defined.
diff --git a/test-suite/bugs/closed/bug_4306.v b/test-suite/bugs/closed/bug_4306.v
index 80c348d207..f1bce04451 100644
--- a/test-suite/bugs/closed/bug_4306.v
+++ b/test-suite/bugs/closed/bug_4306.v
@@ -30,3 +30,5 @@ Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys)
                                 | Gt => y :: foo (xs, ys')
                               end
   end.
+Proof.
+Defined.