Merge PR coq#19092: Better integration of Derive in declare.ml + fix of

coq#18951

Reviewed-by: ppedrot
Ack-by: SkySkimmer
Co-authored-by: ppedrot <[email protected]>

doc/changelog/02-specification-language/19092-master+fix18951-anomaly-derive-admitted.rst

@@ -0,0 +1,5 @@
+- **Fixed:**
+  :cmd:`Derive` now supports :cmd:`Admitted`
+  (`#19092 <https://github.com/coq/coq/pull/19092>`_,
+  fixes `#18951 <https://github.com/coq/coq/issues/18951>`_,
+  by Hugo Herbelin).

plugins/derive/derive.ml

@@ -8,14 +8,18 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Context
 open Context.Named.Declaration
+open Vernacentries.DefAttributes
 
 (** [start_deriving f suchthat lemma] starts a proof of [suchthat]
     (which can contain references to [f]) in the context extended by
     [f:=?x]. When the proof ends, [f] is defined as the value of [?x]
     and [lemma] as the proof. *)
-let start_deriving f suchthat name : Declare.Proof.t =
+let start_deriving ~atts CAst.{v=f;loc} suchthat name : Declare.Proof.t =
+
+  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
+  if program_mode then CErrors.user_err (Pp.str "Program mode not supported.");
 
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -24,22 +28,26 @@ let start_deriving f suchthat name : Declare.Proof.t =
   (* create a sort variable for the type of [f] *)
   (* spiwack: I don't know what the rigidity flag does, picked the one
      that looked the most general. *)
-  let (sigma,f_type_sort) = Evd.new_sort_variable Evd.univ_flexible_alg sigma in
-  let f_type_type = EConstr.mkSort f_type_sort in
+  let sigma, (f_type, f_impargs) =
+    let (sigma,f_type_sort) = Evd.new_sort_variable Evd.univ_flexible_alg sigma in
+    let f_type_type = EConstr.mkSort f_type_sort in
+    let sigma, f_type = Evarutil.new_evar env sigma ~src:(Loc.tag @@ Evar_kinds.GoalEvar) ~typeclass_candidate:false f_type_type in
+    let sigma = Evd.shelve sigma [fst (EConstr.destEvar sigma f_type)] in
+    sigma, (f_type, [])
+  in
+  let (sigma, ef) = Evarutil.new_evar env sigma ~src:(Loc.tag @@ Evar_kinds.GoalEvar) ~typeclass_candidate:false f_type in
+  let env' = EConstr.push_named (LocalDef (EConstr.annotR f, ef, f_type)) env in
+  let impls = Names.Id.Map.add f (Constrintern.compute_internalization_data env sigma f Constrintern.Variable f_type f_impargs) Constrintern.empty_internalization_env in
+  let sigma = Evd.shelve sigma [fst (EConstr.destEvar sigma ef)] in
+  let sigma, (suchthat, impargs) = Constrintern.interp_type_evars_impls env' sigma ~impls suchthat in
   (* create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *)
   let goals =
     let open Proofview in
-    TCons ( env , sigma , f_type_type , (fun sigma f_type ->
-        TCons ( env , sigma , f_type , (fun sigma ef ->
-            let f_type = EConstr.Unsafe.to_constr f_type in
-            let ef = EConstr.Unsafe.to_constr ef in
-            let env' = Environ.push_named (LocalDef (annotR f, ef, f_type)) env in
-            let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in
-            TCons ( env' , sigma , suchthat , (fun sigma _ ->
-                TNil sigma))))))
-  in
-
-  let info = Declare.Info.make ~poly:false ~kind () in
-  let lemma = Declare.Proof.start_derive ~name ~f ~info goals in
+        TCons ( env , sigma , f_type , (fun sigma ef' ->
+            let sigma = Evd.define (fst (EConstr.destEvar sigma ef')) ef sigma in
+            TCons ( env' , sigma , suchthat , (fun sigma _ -> TNil sigma)))) in
+  let info = Declare.Info.make ~poly ~scope ?clearbody ~kind ?typing_flags ?user_warns () in  (* TODO: udecl *)
+  let cinfo = Declare.CInfo.[make ~name:f ~typ:() ~impargs:f_impargs (); make ~name ~typ:() ~impargs ()] in
+  let lemma = Declare.Proof.start_derive ~name ~f ~info ~cinfo goals in
   Declare.Proof.map lemma ~f:(fun p ->
-      Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p)
+      Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 1 shelve) p)

plugins/derive/derive.mli

@@ -13,7 +13,8 @@
     [f:=?x]. When the proof ends, [f] is defined as the value of [?x]
     and [lemma] as the proof. *)
 val start_deriving
-  :  Names.Id.t
+  :  atts:Vernacentries.DefAttributes.t
+  -> Names.Id.t CAst.t
   -> Constrexpr.constr_expr
   -> Names.Id.t
   -> Declare.Proof.t

plugins/derive/g_derive.mlg

@@ -23,6 +23,7 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac
 }
 
 VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } STATE open_proof
-| [ "Derive" identref(f) "SuchThat" constr(suchthat) "As" identref(lemma) ] ->
-  { Derive.start_deriving f.CAst.v suchthat lemma.CAst.v }
+| #[ atts = Vernacentries.DefAttributes.def_attributes; ]
+  [ "Derive" identref(f) "SuchThat" constr(suchthat) "As" identref(lemma) ] ->
+  { Derive.start_deriving ~atts f suchthat lemma.CAst.v }
 END

test-suite/bugs/bug_19234.v

@@ -0,0 +1,7 @@
+Require Import Derive.
+Derive b SuchThat b As spec.
+Unshelve.
+2:exact Type.
+unfold b.
+exact Type.
+Defined.

test-suite/success/Derive.v

@@ -0,0 +1,10 @@
+Require Import Derive.
+
+(* Tests when x is refined by typechecking *)
+Derive x SuchThat (eq_refl x = eq_refl 0) As x_ok.
+reflexivity.
+Qed.
+
+Derive s SuchThat (forall z, eq_refl (s z) = eq_refl (S z)) As s_ok.
+reflexivity.
+Qed.

vernac/declare.ml

@@ -1641,11 +1641,10 @@ let start_core ~info ~cinfo ?proof_ending ?using sigma =
 
 let start = start_core ?proof_ending:None
 
-let start_dependent ~info ~name ~proof_ending goals =
+let start_dependent ~info ~cinfo ~name ~proof_ending goals =
   let { Info.poly; typing_flags; _ } = info in
   let proof = Proof.dependent_start ~name ~poly ?typing_flags goals in
   let initial_euctx = Evd.ustate Proof.((data proof).sigma) in
-  let cinfo = [] in
   let pinfo = Proof_info.make ~info ~cinfo ~proof_ending () in
   { proof
   ; endline_tactic = None
@@ -1654,13 +1653,13 @@ let start_dependent ~info ~name ~proof_ending goals =
   ; pinfo
   }
 
-let start_derive ~f ~name ~info goals =
+let start_derive ~f ~name ~info ~cinfo goals =
   let proof_ending = Proof_ending.End_derive {f; name} in
-  start_dependent ~info ~name ~proof_ending goals
+  start_dependent ~info ~cinfo ~name ~proof_ending goals
 
 let start_equations ~name ~info ~hook ~types sigma goals =
   let proof_ending = Proof_ending.End_equations {hook; i=name; types; sigma} in
-  start_dependent ~name ~info ~proof_ending goals
+  start_dependent ~name ~cinfo:[] ~info ~proof_ending goals
 
 let start_definition ~info ~cinfo ?using sigma =
   let { CInfo.name; typ; args } = cinfo in
@@ -2239,6 +2238,7 @@ let finish_admitted ~pm ~pinfo ~uctx ~sec_vars typs =
 let save_admitted ~pm ~proof =
   let Proof.{ entry; sigma } = Proof.data (get proof) in
   let typs = List.map pi3 (Proofview.initial_goals entry) in
+  List.iter (check_type_evars_solved (Global.env()) sigma) typs;
   let iproof = get proof in
   List.iter (check_type_evars_solved (Global.env()) sigma) typs;
   let sec_vars = compute_proof_using_for_admitted proof.pinfo proof typs iproof in
@@ -2256,42 +2256,28 @@ let save_admitted ~pm ~proof =
 (* Saving a lemma-like constant                                         *)
 (************************************************************************)
 
-let finish_derived ~f ~name ~entries =
+let finish_derived ~f ~name {entries; pinfo; uctx} =
   (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *)
 
-  let f_def, lemma_def =
-    match entries with
-    | [_;f_def;lemma_def] ->
-      f_def, lemma_def
-    | _ -> assert false
-  in
-  (* The opacity of [f_def] is adjusted to be [false], as it
-     must. Then [f] is declared in the global environment. *)
-  let f_def = ProofEntry.set_transparent_for_derived f_def in
-  let f_kind = Decls.(IsDefinition Definition) in
-  let f_def = DefinitionEntry f_def in
-  let f_kn = declare_constant ~name:f ~kind:f_kind f_def ~typing_flags:None in
-  (* Derive does not support univ poly *)
-  let () = assert (not (Global.is_polymorphic (ConstRef f_kn))) in
-  let f_kn_term = Constr.UnsafeMonomorphic.mkConst f_kn in
-  (* In the type and body of the proof of [suchthat] there can be
-     references to the variable [f]. It needs to be replaced by
-     references to the constant [f] declared above. This substitution
-     performs this precise action. *)
-  let substf c = Vars.replace_vars [f,f_kn_term] c in
-  (* Extracts the type of the proof of [suchthat]. *)
-  let lemma_pretype typ =
-    match typ with
-    | Some t -> Some (substf t)
-    | None -> assert false (* Declare always sets type here. *)
-  in
-  (* The references of [f] are subsituted appropriately. *)
-  let lemma_def = ProofEntry.map_entry_type lemma_def ~f:lemma_pretype in
-  (* The same is done in the body of the proof. *)
-  let lemma_def = ProofEntry.map_proof_entry lemma_def ~f:(fun (b,fx) -> (substf b, fx)) in
-  let lemma_def = DefinitionEntry lemma_def in
-  let ct = declare_constant ~name ~typing_flags:None ~kind:Decls.(IsProof Proposition) lemma_def in
-  [GlobRef.ConstRef f_kn; GlobRef.ConstRef ct]
+  let { Proof_info.info = { Info.hook; scope; clearbody; kind; typing_flags; user_warns; poly; udecl; _ } } = pinfo in
+  let _, _, refs, _ =
+    List.fold_left2 (fun (i, subst, refs, used_univs) CInfo.{name; impargs} entry ->
+      (* The opacity of the specification is adjusted to be [false], as it must.*)
+      let entry = if i = 0 then ProofEntry.set_transparent_for_derived entry else entry in
+      let f c = UState.nf_universes uctx (Vars.replace_vars subst c) in
+      let entry = ProofEntry.map_entry_type entry ~f:(Option.map f) in
+      let entry = ProofEntry.map_proof_entry entry ~f:(fun (b,fx) -> (f b, fx)) in
+      let used_univs_body = Vars.universes_of_constr (fst (fst (ProofEntry.get_entry_body entry))) (* Currently assume not delayed *) in
+      let used_univs_typ = Option.cata Vars.universes_of_constr Univ.Level.Set.empty entry.proof_entry_type in
+      let used_univs = Univ.Level.Set.union used_univs (Univ.Level.Set.union used_univs_body used_univs_typ) in
+      let uctx' = UState.restrict uctx used_univs in
+      let entry = { entry with proof_entry_universes = UState.check_univ_decl ~poly uctx' udecl } in
+      let gref = declare_entry ~name ~scope ~clearbody ~kind ?hook ~impargs ~typing_flags ~user_warns ~uctx entry in
+      let cst = match gref with ConstRef cst -> cst | _ -> assert false in
+      let inst = instance_of_univs entry.proof_entry_universes in
+      (i+1, (name, Constr.mkConstU (cst,inst))::subst, gref::refs, used_univs))
+      (0, [], [], Univ.Level.Set.empty) pinfo.Proof_info.cinfo entries in
+  refs
 
 let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 =
 
@@ -2331,7 +2317,7 @@ let finish_proof ~pm proof_obj proof_info =
     let entry, uctx = check_single_entry proof_obj "Obligation.save" in
     Obls_.obligation_terminator ~pm ~entry ~uctx ~oinfo
   | End_derive { f ; name } ->
-    pm, finish_derived ~f ~name ~entries:proof_obj.entries
+    pm, finish_derived ~f ~name proof_obj
   | End_equations { hook; i; types; sigma } ->
     let kind = proof_info.Proof_info.info.Info.kind in
     finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma

vernac/declare.mli

@@ -193,7 +193,7 @@ module Proof : sig
      both of them. Please, get in touch with the developers if you
      would like to experiment with multi-goal dependent proofs so we
      can use your input on the design of the new API. *)
-  val start_derive : f:Id.t -> name:Id.t -> info:Info.t -> Proofview.telescope -> t
+  val start_derive : f:Id.t -> name:Id.t -> info:Info.t -> cinfo:unit CInfo.t list -> Proofview.telescope -> t
 
   val start_equations :
        name:Id.t

vernac/vernacentries.ml

@@ -104,24 +104,27 @@ module DefAttributes = struct
   let clearbody = bool_attribute ~name:"clearbody"
 
   (* [XXX] EJGA: coercion is unused here *)
-  let parse ?(coercion=false) ?(discharge=NoDischarge,"","") f =
+  let def_attributes_gen ?(coercion=false) ?(discharge=NoDischarge,"","") () =
     let discharge, deprecated_thing, replacement = discharge in
     let clearbody = match discharge with DoDischarge -> clearbody | NoDischarge -> return None in
-    let (((((((locality, user_warns), polymorphic), program),
-         canonical_instance), typing_flags), using),
-         reversible), clearbody =
-      parse (locality ++ user_warns_with_use_globref_instead ++ polymorphic ++ program ++
-             canonical_instance ++ typing_flags ++ using ++
-             reversible ++ clearbody)
-        f
-    in
-    let using = Option.map Proof_using.using_from_string using in
-    let reversible = Option.default false reversible in
-    let () = if Option.has_some clearbody && not (Lib.sections_are_opened())
-      then CErrors.user_err Pp.(str "Cannot use attribute clearbody outside sections.")
-    in
-    let scope = scope_of_locality locality discharge deprecated_thing replacement in
-    { scope; locality; polymorphic; program; user_warns; canonical_instance; typing_flags; using; reversible; clearbody }
+    (locality ++ user_warns_with_use_globref_instead ++ polymorphic ++ program ++
+               canonical_instance ++ typing_flags ++ using ++
+               reversible ++ clearbody) >>= fun ((((((((locality, user_warns), polymorphic), program),
+           canonical_instance), typing_flags), using),
+           reversible), clearbody) ->
+      let using = Option.map Proof_using.using_from_string using in
+      let reversible = Option.default false reversible in
+      let () = if Option.has_some clearbody && not (Lib.sections_are_opened())
+        then CErrors.user_err Pp.(str "Cannot use attribute clearbody outside sections.")
+      in
+      let scope = scope_of_locality locality discharge deprecated_thing replacement in
+      return { scope; locality; polymorphic; program; user_warns; canonical_instance; typing_flags; using; reversible; clearbody }
+
+  let parse ?coercion ?discharge f =
+    Attributes.parse (def_attributes_gen ?coercion ?discharge ()) f
+
+  let def_attributes = def_attributes_gen ()
+
 end
 
 let with_def_attributes ?coercion ?discharge ~atts f =

vernac/vernacentries.mli

@@ -71,3 +71,22 @@ val preprocess_inductive_decl
   -> Vernacexpr.inductive_kind
   -> (Vernacexpr.inductive_expr * Vernacexpr.notation_declaration list) list
   -> Preprocessed_Mind_decl.t
+
+module DefAttributes : sig
+
+type t = {
+  scope : Locality.definition_scope;
+  locality : bool option;
+  polymorphic : bool;
+  program : bool;
+  user_warns : Globnames.extended_global_reference UserWarn.with_qf option;
+  canonical_instance : bool;
+  typing_flags : Declarations.typing_flags option;
+  using : Vernacexpr.section_subset_expr option;
+  reversible : bool;
+  clearbody: bool option;
+}
+
+val def_attributes : t Attributes.attribute
+
+end