Merge PR #17576: Let with Qed: produce really-Qed side definition

Reviewed-by: proux01
Co-authored-by: proux01 <proux01@users.noreply.github.com>

dev/ci/user-overlays/17576-SkySkimmer-let-abstract.sh

@@ -0,0 +1 @@
+overlay metacoq https://github.com/SkySkimmer/metacoq let-abstract 17576

doc/changelog/08-vernac-commands-and-options/17576-let-abstract.rst

@@ -0,0 +1,6 @@
+- **Changed:**
+  :cmd:`Let` with :cmd:`Qed` produces an opaque side definition
+  instead of being treated as a transparent `let` after the section is closed.
+  The previous behaviour can be recovered using :attr:`clearbody` and :cmd:`Defined`
+  (`#17576 <https://github.com/coq/coq/pull/17576>`_,
+  by Gaëtan Gilbert).

doc/sphinx/language/core/sections.rst

@@ -75,10 +75,15 @@ usable outside the section as shown in this :ref:`example <section_local_declara
    clears the body of the definition in the proof context of following proofs.
    The kernel will still use the body when checking.
 
-.. warn:: @ident is declared opaque but this is not fully respected inside the section and not at all outside the section.
+.. note::
+
+   Terminating the proof for a :cmd:`Let` with :cmd:`Qed` produces an opaque side definition.
+   `Let foo : T. tactics. Qed.` is equivalent to
+
+   .. coqdoc::
 
-   Terminating the proof for a :cmd:`Let` with :cmd:`Qed` is deprecated.
-   It has the same behavior as :attr:`clearbody` with :cmd:`Defined`.
+      Lemma foo_subproof : T. tactics. Qed.
+      #[clearbody] Let foo := foo_subproof.
 
 .. cmd:: Context {+ @binder }
 

test-suite/bugs/bug_17576_1.v

@@ -0,0 +1,34 @@
+(* Let doesn't respect (default) Proof using *)
+
+(* Maybe we will want to change this behaviour someday
+   but keep in mind that if we do then "bar'" should get 2 A arguments.
+*)
+
+Set Default Proof Using "Type".
+Set Warnings "-opaque-let".
+
+Section S.
+
+  Variable A : Type.
+  Variable a : A.
+
+  Let foo : A.
+  Proof. (* Default Proof Using silently ignored *)
+    exact a.
+  Qed.
+
+  Definition bar := foo.
+
+  Variable b : A.
+
+  Let foo' : A.
+  Fail Proof using a b.
+    exact b.
+  Qed.
+
+  Definition bar' := foo'.
+
+End S.
+
+Check bar : forall A, A -> A.
+Check bar' : forall A, A -> A.

vernac/comAssumption.ml

@@ -22,7 +22,7 @@ module RelDecl = Context.Rel.Declaration
 
 let declare_variable is_coe ~kind typ univs imps impl {CAst.v=name} =
   let kind = Decls.IsAssumption kind in
-  let () = Declare.declare_variable ~name ~kind ~typ ~impl ~univs in
+  let () = Declare.declare_variable ~name ~kind ~typing_flags:None ~typ ~impl ~univs in
   let () = Declare.assumption_message name in
   let r = GlobRef.VarRef name in
   let () = maybe_declare_manual_implicits true r imps in

vernac/declare.ml

@@ -486,15 +486,7 @@ let objVariable : Id.t Libobject.Dyn.tag =
 
 let inVariable v = Libobject.Dyn.Easy.inj v objVariable
 
-let warn_opaque_let = CWarnings.create ~name:"opaque-let" ~category:Deprecation.Version.v8_18
-  Pp.(fun name ->
-    Id.print name ++
-    strbrk " is declared opaque (Qed) but this is not fully respected" ++
-    strbrk " inside the section and not at all outside the section." ++ fnl() ++
-    strbrk "Use attribute #[clearbody] to get the current behaviour of clearing" ++
-    strbrk " the body at the start of proofs in a forward compatible way.")
-
-let declare_variable_core ~name ~kind d =
+let declare_variable_core ~name ~kind ~typing_flags d =
   (* Variables are distinguished by only short names *)
   if Decls.variable_exists name then
     raise (DeclareUniv.AlreadyDeclared (None, name));
@@ -521,14 +513,34 @@ let declare_variable_core ~name ~kind d =
       (* We must declare the universe constraints before type-checking the
          term. *)
       let () = DeclareUctx.declare_universe_context ~poly univs in
-      (* NB: de.proof_entry_secctx is ignored *)
-      let se = {
+      let opaque = de.proof_entry_opaque in
+      let se = if opaque then
+          let cname = Id.of_string (Id.to_string name ^ "_subproof") in
+          let cname = Namegen.next_global_ident_away cname Id.Set.empty in
+          let de = {
+            proof_entry_body = Future.from_val ((body, Univ.ContextSet.empty), Evd.empty_side_effects);
+            proof_entry_secctx = None; (* de.proof_entry_secctx is NOT respected *)
+            proof_entry_feedback = de.proof_entry_feedback;
+            proof_entry_type = de.proof_entry_type;
+            proof_entry_universes = UState.univ_entry ~poly UState.empty;
+            proof_entry_opaque = true;
+            proof_entry_inline_code = de.proof_entry_inline_code;
+          }
+          in
+          let kn = declare_constant ~name:cname
+              ~local:ImportNeedQualified ~kind:(IsProof Lemma) ~typing_flags
+              (DefinitionEntry de)
+          in
+          {
+            Entries.secdef_body = Constr.mkConstU (kn, Univ.Instance.empty);
+            secdef_type = None;
+          }
+        else {
         Entries.secdef_body = body;
         secdef_type = de.proof_entry_type;
       } in
       let () = Global.push_named_def (name, se) in
-      let opaque = de.proof_entry_opaque in
-      let () = if opaque then warn_opaque_let name in
+      (* opaque implies clearbody, so we don't see useless "foo := foo_subproof" in the context *)
       Glob_term.Explicit, opaque || clearbody, de.proof_entry_universes
   in
   Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
@@ -537,8 +549,8 @@ let declare_variable_core ~name ~kind d =
   Impargs.declare_var_implicits ~impl name;
   Notation.declare_ref_arguments_scope (GlobRef.VarRef name)
 
-let declare_variable ~name ~kind ~typ ~impl ~univs =
-  declare_variable_core ~name ~kind (SectionLocalAssum { typ; impl; univs })
+let declare_variable ~name ~kind ~typing_flags ~typ ~impl ~univs =
+  declare_variable_core ~name ~kind ~typing_flags (SectionLocalAssum { typ; impl; univs })
 
 (* Declaration messages *)
 
@@ -666,7 +678,7 @@ let declare_entry_core ~name ?(scope=Locality.default_scope) ?(clearbody=false)
   in
   let dref = match scope with
   | Locality.Discharge ->
-    let () = declare_variable_core ~name ~kind (SectionLocalDef {clearbody; entry}) in
+    let () = declare_variable_core ~typing_flags ~name ~kind (SectionLocalDef {clearbody; entry}) in
     if should_suggest then Proof_using.suggest_variable (Global.env ()) name;
     Names.GlobRef.VarRef name
   | Locality.Global local ->
@@ -1652,6 +1664,8 @@ let get_recnames pf =
   else
     []
 
+let definition_scope ps = ps.pinfo.info.scope
+
 let set_used_variables ps ~using =
   let open Context.Named.Declaration in
   let env = Global.env () in

vernac/declare.mli

@@ -256,6 +256,8 @@ module Proof : sig
   (** Sets the tactic to be used when a tactic line is closed with [...] *)
   val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
 
+  val definition_scope : t -> Locality.definition_scope
+
   (** Sets the section variables assumed by the proof, returns its closure
    * (w.r.t. type dependencies and let-ins covered by it) *)
   val set_used_variables : t -> using:Proof_using.t -> Constr.named_context * t
@@ -386,6 +388,7 @@ val declare_entry
 val declare_variable
   :  name:variable
   -> kind:Decls.logical_kind
+  -> typing_flags:Declarations.typing_flags option
   -> typ:Constr.types
   -> impl:Glob_term.binding_kind
   -> univs:UState.named_universes_entry

vernac/vernacentries.ml

@@ -570,7 +570,7 @@ let program_inference_hook env sigma ev =
     user_err Pp.(str "The statement obligations could not be resolved \
                       automatically, write a statement definition first.")
 
-let vernac_set_used_variables ~pstate using : Declare.Proof.t =
+let vernac_set_used_variables pstate using : Declare.Proof.t =
   let env = Global.env () in
   let sigma, _ = Declare.Proof.get_current_context pstate in
   let fixnames = Declare.Proof.get_recnames pstate in
@@ -583,7 +583,7 @@ let vernac_set_used_variables ~pstate using : Declare.Proof.t =
 let vernac_set_used_variables_opt ?using pstate =
   match using with
   | None -> pstate
-  | Some expr -> vernac_set_used_variables ~pstate expr
+  | Some expr -> vernac_set_used_variables pstate expr
 
 (* XXX: Interpretation of lemma command, duplication with ComFixpoint
    / ComDefinition ? *)
@@ -1491,7 +1491,7 @@ let vernac_existing_class id =
 let command_focus = Proof.new_focus_kind ()
 let focus_command_cond = Proof.no_cond command_focus
 
-let vernac_set_end_tac ~pstate tac =
+let vernac_set_end_tac pstate tac =
   let env = Genintern.empty_glob_sign ~strict:true (Global.env ()) in
   let _, tac = Genintern.generic_intern env tac in
   (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
@@ -2208,6 +2208,25 @@ let vernac_validate_proof ~pstate =
     str "No issues found."
   else prlist_with_sep fnl snd (Evar.Map.bindings evar_issues)
 
+let vernac_proof pstate tac using =
+  let is_let = match Declare.Proof.definition_scope pstate with
+    | Discharge -> true
+    | Global _ -> false
+  in
+  let using = if not is_let then Option.append using (Proof_using.get_default_proof_using ())
+    else
+      let () = if Option.has_some using
+        then CErrors.user_err Pp.(str "Let does not support Proof using.")
+      in
+      None
+  in
+  let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in
+  let usings = if Option.is_empty using then "using:no" else "using:yes" in
+  Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings);
+  let pstate = Option.fold_left vernac_set_end_tac pstate tac in
+  let pstate = Option.fold_left vernac_set_used_variables pstate using in
+  pstate
+
 let translate_vernac_synterp ?loc ~atts v = let open Vernactypes in match v with
   | EVernacNotation { local; decl } ->
     vtdefault(fun () -> Metasyntax.add_notation_interpretation ~local (Global.env()) decl)
@@ -2535,12 +2554,7 @@ let translate_pure_vernac ?loc ~atts v = let open Vernactypes in match v with
   | VernacProof (tac, using) ->
     vtmodifyproof(fun ~pstate ->
     unsupported_attributes atts;
-    let using = Option.append using (Proof_using.get_default_proof_using ()) in
-    let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in
-    let usings = if Option.is_empty using then "using:no" else "using:yes" in
-    Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings);
-    let pstate = Option.cata (vernac_set_end_tac ~pstate) pstate tac in
-    Option.cata (vernac_set_used_variables ~pstate) pstate using)
+    vernac_proof pstate tac using)
 
   | VernacEndProof pe ->
     unsupported_attributes atts;