From 6cb44b4e71185e9c428889fdb18b5a386950ac35 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 26 Oct 2024 22:40:10 +0200 Subject: [PATCH 01/21] Fixes #19767: anomaly when printing functor with Strategy in module parameter. --- tactics/redexpr.ml | 22 ++++++++++++---------- test-suite/bugs/bug_19767.v | 11 +++++++++++ 2 files changed, 23 insertions(+), 10 deletions(-) create mode 100644 test-suite/bugs/bug_19767.v diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index d5d5edf78fb7..260ef21a1497 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -56,16 +56,7 @@ let { Goptions.get = simplIsCbn } = () let set_strategy_one ref l = - Global.set_strategy (Evaluable.to_kevaluable ref) l; - match ref, l with - | Evaluable.EvalConstRef sp, Conv_oracle.Opaque -> () - | Evaluable.EvalConstRef sp, _ -> - if Declareops.is_opaque (Global.lookup_constant sp) then - user_err - (str "Cannot make" ++ spc () ++ - Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef sp) ++ - spc () ++ str "transparent because it was declared opaque.") - | _ -> () + Global.set_strategy (Evaluable.to_kevaluable ref) l let cache_strategy (_,str) = List.iter @@ -119,8 +110,19 @@ let inStrategy : strategy_obj -> obj = classify_function = classify_strategy; } +let check_not_fully_opaque l ref = + match ref, l with + | Evaluable.EvalConstRef sp, Conv_oracle.Opaque -> () + | Evaluable.EvalConstRef sp, _ -> + if Declareops.is_opaque (Global.lookup_constant sp) then + user_err + (str "Cannot make" ++ spc () ++ + Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef sp) ++ + spc () ++ str "transparent because it was declared opaque.") + | _ -> () let set_strategy local str = + List.iter (fun (l,refs) -> List.iter (check_not_fully_opaque l) refs) str; Lib.add_leaf (inStrategy (local,str)) (* Generic reduction: reduction functions used in reduction tactics *) diff --git a/test-suite/bugs/bug_19767.v b/test-suite/bugs/bug_19767.v new file mode 100644 index 000000000000..cdc712a5db8b --- /dev/null +++ b/test-suite/bugs/bug_19767.v @@ -0,0 +1,11 @@ +Module A. + Module Type T. Definition c := 0. #[global] Strategy expand [c]. End T. + Module F (M:T). End F. + Print F. +End A. + +Module B. + Module Type T. Definition c := 0. #[global] Transparent c. End T. + Module F (M:T). End F. + Print F. +End B. From c248044a5b3f8f74789b14feb9069128fbd53726 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 26 Oct 2024 16:00:03 +0200 Subject: [PATCH 02/21] Reworking slightly the documentation of Definition, Theorem and Fixpoint. Also adding some missing supported attributes. --- doc/sphinx/language/core/definitions.rst | 48 +++++++++---------- doc/sphinx/language/core/inductive.rst | 42 ++++++++-------- doc/sphinx/language/core/modules.rst | 3 +- .../user-extensions/syntax-extensions.rst | 2 + 4 files changed, 48 insertions(+), 47 deletions(-) diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index d2efbff24e07..c0b6dfdd2d43 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -92,30 +92,27 @@ Section :ref:`typing-rules`. | {* @binder } : @type reduce ::= Eval @red_expr in - These commands bind :n:`@term` to the name :n:`@ident` in the global environment, - provided that :n:`@term` is well-typed. They can take the :attr:`local` :term:`attribute`, - which makes the defined :n:`@ident` accessible only through their fully - qualified names, even if :cmd:`Import` or its variants has been used on the - current :cmd:`Module`. + This binds :n:`@term` to the name :n:`@ident` in the global environment, + provided that :n:`@term` is well-typed. + + If :n:`@type` is specified, the command checks that the type of :n:`@term` + is definitionally equal to :n:`@type`. + + If :n:`@binder` is specified, it distributes over :n:`@term` and :n:`@type` as if they had + respectively been :n:`fun {* @binder } => @term` and :n:`forall {* @binder }, @type`. + If :n:`@reduce` is present then :n:`@ident` is bound to the result of the specified computation on :n:`@term`. - These commands also support the :attr:`universes(polymorphic)`, - :attr:`program` (see :ref:`program_definition`), :attr:`canonical`, - :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, :attr:`deprecated`, - :attr:`warn` and :attr:`using` attributes. - If :n:`@term` is omitted, :n:`@type` is required and Rocq enters proof mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a :term:`constant` for which the computational behavior is relevant. See :ref:`proof-editing-mode`. - The form :n:`Definition @ident : @type := @term` checks that the type of :n:`@term` - is definitionally equal to :n:`@type`, and registers :n:`@ident` as being of type - :n:`@type`, and bound to value :n:`@term`. - - The form :n:`Definition @ident {* @binder } : @type := @term` is equivalent to - :n:`Definition @ident : forall {* @binder }, @type := fun {* @binder } => @term`. + The attributes :attr:`local`, :attr:`universes(polymorphic)`, + :attr:`program` (see :ref:`program_definition`), :attr:`canonical`, + :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, :attr:`deprecated`, + :attr:`warn` and :attr:`using` are accepted. .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. @@ -152,20 +149,19 @@ The basic assertion command is: | Property After the statement is asserted, Rocq needs a proof. Once a proof of - :n:`@type` under the assumptions represented by :n:`@binder`\s is given and - validated, the proof is generalized into a proof of :n:`forall {* @binder }, @type` and + :n:`@type` is given, the theorem is bound to the name :n:`@ident` in the global environment. - These commands accept the :attr:`program` attribute. See :ref:`program_lemma`. + If :n:`@binder` is specified, this behaves as if :n:`@type` had been + :n:`forall {* @binder }, @type` and the proof starts in the context :n:`{* @binder }`. Forms using the :n:`with` clause are useful for theorems that are proved by simultaneous induction - over a mutually inductive assumption, or that assert mutually dependent - statements in some mutual coinductive type. It is equivalent to + over a mutually inductive assumption, or that assert mutually dependent coinductive + statements. It is equivalent to :cmd:`Fixpoint` or :cmd:`CoFixpoint` but using tactics to build the proof of the statements (or the :term:`body` of the specification, depending on the point of view). The inductive or coinductive types on which the induction or - coinduction has to be done is assumed to be unambiguous and is guessed by - the system. + coinduction has to be done is guessed by the system. Like in a :cmd:`Fixpoint` or :cmd:`CoFixpoint` definition, the induction hypotheses have to be used on *structurally smaller* arguments (for a :cmd:`Fixpoint`) or @@ -175,8 +171,10 @@ The basic assertion command is: correct at some time of the interactive development of a proof, use the command :cmd:`Guarded`. - This command accepts the :attr:`bypass_check(universes)`, - :attr:`bypass_check(guard)`, :attr:`deprecated`, :attr:`warn`, and :attr:`using` attributes. + The attributes :attr:`local`, :attr:`universes(polymorphic)`, + :attr:`program` (see :ref:`program_lemma`), + :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, :attr:`deprecated`, + :attr:`warn` and :attr:`using` are accepted. .. exn:: The term @term has type @type which should be Set, Prop or Type. :undocumented: diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 1dd04df214be..72b81e0fa5e7 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -465,41 +465,43 @@ constructions. fix_definition ::= @ident_decl {* @binder } {? @fixannot } {? : @type } {? := @term } {? @decl_notations } Allows defining functions by pattern matching over inductive - objects using a fixed point construction. The meaning of this declaration is - to define :n:`@ident` as a recursive function with arguments specified by - the :n:`@binder`\s such that :n:`@ident` applied to arguments - corresponding to these :n:`@binder`\s has type :n:`@type`, and is - equivalent to the expression :n:`@term`. The type of :n:`@ident` is - consequently :n:`forall {* @binder }, @type` and its value is equivalent - to :n:`fun {* @binder } => @term`. - - This command accepts the :attr:`program`, - :attr:`bypass_check(universes)`, and :attr:`bypass_check(guard)` attributes. - - To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical - constraints on a special argument called the decreasing argument. They - are needed to ensure that the :cmd:`Fixpoint` definition always terminates. + objects using a fixed point construction. + + The basic form :n:`Fixpoint @ident {* @binder} { struct @ident } : @type := @term. + declares :n:`@ident` to be the recursive function with arguments + :n:`{* @binder}` and body :n:`@term` of type :n:`type`. + + To be accepted, a :cmd:`Fixpoint` definition has to satisfy a syntactical + constraint on a special argument called the decreasing argument. This + is needed to ensure that the :cmd:`Fixpoint` definition always terminates. The point of the :n:`{struct @ident}` annotation (see :n:`@fixannot`) is to let the user tell the system which argument decreases along the recursive calls. - The :n:`{struct @ident}` annotation may be left implicit, in which case the - system successively tries arguments from left to right until it finds one + The :n:`{struct @ident}` annotation may be left implicit, in which case + Rocq successively tries arguments from left to right until it finds one that satisfies the decreasing condition. - :cmd:`Fixpoint` without the :attr:`program` attribute does not support the - :n:`wf` or :n:`measure` clauses of :n:`@fixannot`. See :ref:`program_fixpoint`. + The :n:`@type` annotation may be left implicit, in which case Rocq + attempts to infer it. + + This command accepts the :attr:`local`, :attr:`universes(polymorphic)`, :attr:`program`, + :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, :attr:`deprecated`, + :attr:`warn` and :attr:`using` attributes. The :attr:`program` attribute is needed + so that the :n:`wf` or :n:`measure` clauses of :n:`@fixannot` are + supported. See :ref:`program_fixpoint`. The :n:`with` clause allows simultaneously defining several mutual fixpoints. It is especially useful when defining functions over mutually defined inductive types. Example: :ref:`Mutual Fixpoints`. + If :n:`@decl_notation` is present, a notation is defined at the same time + (see :ref:`simultaneous-definition-and-notation`). + If :n:`@term` is omitted, :n:`@type` is required and Rocq enters proof mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a :term:`constant` for which the computational behavior is relevant. See :ref:`proof-editing-mode`. - This command accepts the :attr:`using` attribute. - .. note:: + Some fixpoints may have several arguments that fit as decreasing diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index f5d9bc99ac2d..21b905cfb489 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -644,8 +644,7 @@ while noting a few exceptional commands for which :attr:`local` and **Exception:** when :attr:`local` is applied to :cmd:`Definition`, :cmd:`Theorem` or their variants, its semantics are different: it makes the defined objects available - only through their fully qualified names rather than their - unqualified names after an :cmd:`Import`. + only through their fully qualified names, even after an :cmd:`Import`. .. attr:: export diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index ebb156d896f6..b8e693287540 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -468,6 +468,8 @@ Reserving notations the other. See :ref:`factorization ` for details. +.. _simultaneous-definition-and-notation: + Simultaneous definition of terms and notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ From ccba976be4b58e3ef3df013e689c9131c9e86060 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 26 Oct 2024 16:06:38 +0200 Subject: [PATCH 03/21] Rewording the structure of the documentation of Definition/Theorem. --- doc/sphinx/language/core/definitions.rst | 47 +++++++++++++++--------- 1 file changed, 30 insertions(+), 17 deletions(-) diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index c0b6dfdd2d43..de25bdb7cf4c 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -1,5 +1,22 @@ -Definitions -=========== +Definitions and theorems +======================== + +Definitions associate a specified term with a given name. The name can later +be replaced with its definition through :term:`δ-reduction`. Definitions can +be local (defined with :g:`let`) or global +(e.g. defined with :cmd:`Definition` and related forms such as :cmd:`Fixpoint` +and :cmd:`CoFixpoint`). + +On its side, a theorem is a statement with a proof. One can view +the name of a theorem as a way to abbreviate the given proof, in the +same way as the name of a definition abbreviates a term. That is, in +the case of definitions (and related forms such as :cmd:`Fixpoint` or +:cmd:`CoFixpoint`), the term is the body of the definition and the +type is the type of the body. In the case of a theorem, lemma, +corollary, etc. the term is the proof and the type is the statement. + +Moreover, definitions can be local (defined with :g:`let`) or global +(defined at top-level). .. index:: let ... := ... (term) @@ -66,10 +83,7 @@ If a scope is :ref:`bound ` to Top-level definitions --------------------- -Definitions extend the global environment by associating names to terms. -A definition can be seen as a way to give a meaning to a name or as a -way to abbreviate a term. In any case, the name can later be replaced at -any time by its definition. +Top-level definitions extend the global environment by associating names with terms. The operation of unfolding a name into its definition is called :term:`delta-reduction`. @@ -106,8 +120,7 @@ Section :ref:`typing-rules`. If :n:`@term` is omitted, :n:`@type` is required and Rocq enters proof mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. - In this case, the proof should be terminated with :cmd:`Defined` in order to define a :term:`constant` - for which the computational behavior is relevant. See :ref:`proof-editing-mode`. + In this case, the proof should normally be terminated with :cmd:`Defined`. See :ref:`proof-editing-mode`. The attributes :attr:`local`, :attr:`universes(polymorphic)`, :attr:`program` (see :ref:`program_definition`), :attr:`canonical`, @@ -125,10 +138,10 @@ Section :ref:`typing-rules`. .. _Assertions: -Assertions and proofs ---------------------- +Theorems and proofs +------------------- -An assertion states a proposition (or a type) for which the proof (or an +Assertions, such as :cmd:`Theorem`s, state a proposition (or a type) for which the proof (or an inhabitant of the type) is interactively built using :term:`tactics `. Assertions cause Rocq to enter :term:`proof mode` (see :ref:`proofhandling`). Common tactics are described in the :ref:`writing-proofs` chapter. @@ -198,7 +211,12 @@ tactics (see :ref:`writing-proofs`). The user may also enter commands to manage the proof mode (see :ref:`proofhandling`). When the proof is complete, use the :cmd:`Qed` command so the kernel verifies -the proof and adds it to the global environment. +the proof and adds it to the global environment. By default, proofs +that end with :cmd:`Qed` are :term:`opaque`, that is that their content cannot +be unfolded (see :ref:`applyingconversionrules`), thus realizing +*proof irrelevance*, that is that only provability matters, +and not the exact proof. Proofs can be made unfoldable, as +definitions are, by ending the proof with :cmd:`Defined` in place of :cmd:`Qed`. .. note:: @@ -211,11 +229,6 @@ the proof and adds it to the global environment. statements still to be proved. Nonetheless, this practice is discouraged and may stop working in future versions. - #. Proofs ended by :cmd:`Qed` are declared :term:`opaque`. Their content cannot be - unfolded (see :ref:`applyingconversionrules`), thus - realizing some form of *proof-irrelevance*. - Proofs that end with :cmd:`Defined` can be unfolded. - #. :cmd:`Proof` is recommended but can currently be omitted. On the opposite side, :cmd:`Qed` (or :cmd:`Defined`) is mandatory to validate a proof. From 7c379f1509d42ba8b44ff4db51c2838a26131276 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 15 May 2024 13:59:13 +0200 Subject: [PATCH 04/21] Is OblState.view still used? --- vernac/declare.ml | 35 ----------------------------------- vernac/declare.mli | 19 ------------------- 2 files changed, 54 deletions(-) diff --git a/vernac/declare.ml b/vernac/declare.ml index 7a6a62084627..2e601bb75c8c 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1394,41 +1394,6 @@ module State = struct let all pm = ProgMap.bindings pm |> List.map (fun (_,v) -> CEphemeron.get v) let find m t = ProgMap.find_opt t m |> Option.map CEphemeron.get - module View = struct - module Obl = struct - type t = - { name : Id.t - ; loc : Loc.t option - ; status : bool * Evar_kinds.obligation_definition_status - ; solved : bool - } - - let make (o : Obligation.t) = - let { obl_name; obl_location; obl_status; obl_body; _ } = o in - { name = obl_name - ; loc = fst obl_location - ; status = obl_status - ; solved = Option.has_some obl_body - } - end - - type t = - { opaque : bool - ; remaining : int - ; obligations : Obl.t array - } - - let make { prg_opaque; prg_obligations; _ } = - { opaque = prg_opaque - ; remaining = prg_obligations.remaining - ; obligations = Array.map Obl.make prg_obligations.obls - } - - let make eph = CEphemeron.get eph |> make - end - - let view s = Id.Map.map View.make s - end (* In all cases, the use of the map is read-only so we don't expose the ref *) diff --git a/vernac/declare.mli b/vernac/declare.mli index 7be840250ab9..782c40d7705d 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -151,25 +151,6 @@ module OblState : sig type t val empty : t - module View : sig - module Obl : sig - type t = private - { name : Id.t - ; loc : Loc.t option - ; status : bool * Evar_kinds.obligation_definition_status - ; solved : bool - } - end - - type t = private - { opaque : bool - ; remaining : int - ; obligations : Obl.t array - } - end - - val view : t -> View.t Id.Map.t - end (** [Declare.Proof.t] Construction of constants using interactive proofs. *) From 8471db8f476fb2e1cf2742d677c123c530f19210 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 18 Jun 2024 19:33:03 +0200 Subject: [PATCH 05/21] Adding List.map5. --- clib/cList.ml | 16 ++++++++++++++++ clib/cList.mli | 4 ++++ 2 files changed, 20 insertions(+) diff --git a/clib/cList.ml b/clib/cList.ml index 73c5111258c8..05e397031751 100644 --- a/clib/cList.ml +++ b/clib/cList.ml @@ -395,6 +395,22 @@ let map4 f l1 l2 l3 l4 = match l1, l2, l3, l4 with cast c | _ -> invalid_arg "List.map4" +let rec map5_loop f p l1 l2 l3 l4 l5 = match l1, l2, l3, l4, l5 with + | [], [], [], [], [] -> () + | x :: l1, y :: l2, z :: l3, t :: l4, u :: l5 -> + let c = { head = f x y z t u; tail = [] } in + p.tail <- cast c; + map5_loop f c l1 l2 l3 l4 l5 + | _ -> invalid_arg "List.map5" + +let map5 f l1 l2 l3 l4 l5 = match l1, l2, l3, l4, l5 with + | [], [], [], [], [] -> [] + | x :: l1, y :: l2, z :: l3, t :: l4, u :: l5 -> + let c = { head = f x y z t u; tail = [] } in + map5_loop f c l1 l2 l3 l4 l5; + cast c + | _ -> invalid_arg "List.map5" + let rec map_until_loop f p = function | [] -> [] | x :: l as l' -> diff --git a/clib/cList.mli b/clib/cList.mli index 0b2a23b1dbdc..ca8dbc9449d7 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -132,6 +132,10 @@ val map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list (** Like [map] but for 4 lists. *) +val map5 : ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> 'a list -> 'b list -> 'c list -> + 'd list -> 'e list -> 'f list +(** Like [map] but for 5 lists. *) + val map_until : ('a -> 'b option) -> 'a list -> 'b list * 'a list (** [map_until f l] applies f to the elements of l until one returns None, then returns the list of elements where f was applied From 9e63d70a5ff61cf760c8ff30629e8385714c0228 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 18 Jun 2024 19:32:53 +0200 Subject: [PATCH 06/21] Adding sealed/defined attributes to make a declaration kernel-opaque/transparent. The main changes are: - "opaque" is now part of the Declare.CInfo.t (one per component of the proof) - at Qed/Defined time, a check is done to determine if there is an attribute which takes precedence over the Qed/Defined keyword; - for non-interactive declaration, Definition is transparent by default and (assuming the syntax provided as in #19301) Theorem requires an explicit attribute. - the attribute can be set both globally (before the command name) and locally (just before the names declared by the command) --- .../tuto1/src/simple_declare.ml | 4 +- doc/sphinx/language/core/coinductive.rst | 2 +- doc/sphinx/language/core/inductive.rst | 2 +- doc/tools/docgram/common.edit_mlg | 8 +- doc/tools/docgram/fullGrammar | 4 +- doc/tools/docgram/orderedGrammar | 4 +- plugins/derive/derive.ml | 8 +- .../funind/functional_principles_proofs.ml | 2 +- plugins/funind/gen_principle.ml | 14 +- plugins/funind/recdef.ml | 6 +- plugins/ltac/comRewrite.ml | 19 +-- plugins/ltac/extratactics.mlg | 24 ++-- plugins/ltac/leminv.ml | 11 +- plugins/ltac/leminv.mli | 2 +- test-suite/success/sealed.v | 37 +++++ vernac/attributes.ml | 7 + vernac/attributes.mli | 1 + vernac/classes.ml | 43 +++--- vernac/classes.mli | 3 + vernac/comDefinition.ml | 16 +-- vernac/comDefinition.mli | 3 + vernac/comFixpoint.ml | 39 ++--- vernac/comFixpoint.mli | 2 + vernac/declare.ml | 133 ++++++++++-------- vernac/declare.mli | 6 +- vernac/g_vernac.mlg | 8 +- vernac/ppvernac.mli | 2 + vernac/vernacentries.ml | 67 ++++----- vernac/vernacentries.mli | 1 + vernac/vernacexpr.mli | 1 + 30 files changed, 281 insertions(+), 198 deletions(-) create mode 100644 test-suite/success/sealed.v diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 2f8735a1094e..8d961fba847e 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,4 +1,4 @@ let declare_definition ~poly name sigma body = - let cinfo = Declare.CInfo.make ~name ~typ:None () in + let cinfo = Declare.CInfo.make ~name ~typ:None ~opaque:(Some false) () in let info = Declare.Info.make ~poly () in - Declare.declare_definition ~info ~cinfo ~opaque:false ~body sigma + Declare.declare_definition ~info ~cinfo ~body sigma diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index a0e9eefca23e..4d29e72d2d6e 100644 --- a/doc/sphinx/language/core/coinductive.rst +++ b/doc/sphinx/language/core/coinductive.rst @@ -154,7 +154,7 @@ Top-level definitions of corecursive functions .. insertprodn cofix_definition cofix_definition .. prodn:: - cofix_definition ::= @ident_decl {* @binder } {? : @type } {? := @term } {? @decl_notations } + cofix_definition ::= {* #[ {+, @attribute } ] } @ident_decl {* @binder } {? : @type } {? := @term } {? @decl_notations } This command introduces a method for constructing an infinite object of a coinductive type. For example, the stream containing all natural numbers can diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 72b81e0fa5e7..f174a1f89516 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -462,7 +462,7 @@ constructions. .. insertprodn fix_definition fix_definition .. prodn:: - fix_definition ::= @ident_decl {* @binder } {? @fixannot } {? : @type } {? := @term } {? @decl_notations } + fix_definition ::= {* #[ {+, @attribute } ] } @ident_decl {* @binder } {? @fixannot } {? : @type } {? := @term } {? @decl_notations } Allows defining functions by pattern matching over inductive objects using a fixed point construction. diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index ed8be8ab5b71..19f5ca46473d 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1507,13 +1507,13 @@ legacy_attr: [ sentence: [ ] (* productions defined below *) fix_definition: [ -| REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations -| WITH ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations +| REPLACE quoted_attributes ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations +| WITH quoted_attributes ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations ] cofix_definition: [ -| REPLACE ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations -| WITH ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations +| REPLACE quoted_attributes ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations +| WITH quoted_attributes ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations ] type_cstr: [ diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 3b1872763908..a09e9f37dc3e 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1058,11 +1058,11 @@ opt_coercion: [ ] fix_definition: [ -| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations +| quoted_attributes ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations ] cofix_definition: [ -| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations +| quoted_attributes ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations ] rw_pattern: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 7dcd8c5a78a5..5c8135e89bd3 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -462,7 +462,7 @@ pattern0: [ ] fix_definition: [ -| ident_decl LIST0 binder OPT fixannot OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations +| LIST0 [ "#[" LIST1 attribute SEP "," "]" ] ident_decl LIST0 binder OPT fixannot OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations ] thm_token: [ @@ -571,7 +571,7 @@ filtered_import: [ ] cofix_definition: [ -| ident_decl LIST0 binder OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations +| LIST0 [ "#[" LIST1 attribute SEP "," "]" ] ident_decl LIST0 binder OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations ] rw_pattern: [ diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index b95cd865dc27..43ca2ae44e54 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -40,8 +40,8 @@ let rec fill_assumptions env sigma = function and [lemma] as the proof. *) let start_deriving ~atts bl 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 + let scope, _local, poly, program_mode, user_warns, typing_flags, using, clearbody, opaque = + atts.scope, atts.locality, atts.polymorphic, atts.program, atts.user_warns, atts.typing_flags, atts.using, atts.clearbody, atts.opacity in if program_mode then CErrors.user_err (Pp.str "Program mode not supported."); let env = Global.env () in @@ -71,8 +71,8 @@ let start_deriving ~atts bl suchthat name : Declare.Proof.t = let name = get_id d in let impargs = Constrintern.implicits_of_decl_in_internalization_env name impls_env in let impargs = List.map CAst.make (List.map extract_manual impargs) in - make ~name ~typ:() ~impargs ()) ctx' @ - [make ~name ~typ:() ~impargs ()] in + make ~name ~typ:() ~impargs ~opaque:(Some false) ()) ctx' @ + [make ~name ~typ:() ~impargs ~opaque ()] in let lemma = Declare.Proof.start_derive ~name ~info ~cinfo goals in Declare.Proof.map lemma ~f:(fun p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 1 shelve) p) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index f99d90b61ae8..116f47b28fbf 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -884,7 +884,7 @@ let generate_equation_lemma env evd fnames f fun_num nb_params nb_args rec_args_ constructing the lemma Ensures by: obvious i*) let info = Declare.Info.make () in let cinfo = - Declare.CInfo.make ~name:(mk_equation_id f_id) ~typ:lemma_type () + Declare.CInfo.make ~name:(mk_equation_id f_id) ~typ:lemma_type ~opaque:(Some false) () in let lemma = Declare.Proof.start ~cinfo ~info evd in let lemma, _ = Declare.Proof.by prove_replacement lemma in diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 6545c0285d7f..45e5c92d37d9 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -386,7 +386,7 @@ let register_struct is_rec (rec_order, fixpoint_exprl) = CErrors.user_err Pp.(str "Body of Function must be given.") in - ComDefinition.do_definition ~name:fname.CAst.v ~poly:false + ComDefinition.do_definition ~name:fname.CAst.v ~opaque:(Some false) ~poly:false ~kind:Decls.Definition univs binders None body (Some rtype); let evd, rev_pconstants = List.fold_left @@ -1484,7 +1484,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) let lem_id = mk_correct_id f_id in let typ, _ = lemmas_types_infos.(i) in let info = Declare.Info.make () in - let cinfo = Declare.CInfo.make ~name:lem_id ~typ () in + let cinfo = Declare.CInfo.make ~name:lem_id ~typ ~opaque:(Some false) () in let lemma = Declare.Proof.start ~cinfo ~info !evd in let lemma = fst @@ Declare.Proof.by (proving_tac i) lemma in let (_ : _ list) = @@ -1548,9 +1548,9 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) Ensures by: obvious i*) let lem_id = mk_complete_id f_id in - let info = Declare.Info.make () in + let info = Declare.Info.make() in let cinfo = - Declare.CInfo.make ~name:lem_id ~typ:(fst lemmas_types_infos.(i)) () + Declare.CInfo.make ~name:lem_id ~typ:(fst lemmas_types_infos.(i)) ~opaque:(Some false) () in let lemma = Declare.Proof.start ~cinfo sigma ~info in let lemma = @@ -2091,7 +2091,8 @@ let make_graph (f_ref : GlobRef.t) = ; binders = nal_tas @ bl ; rtype = t ; body_def = Some b' - ; notations = [] }) + ; notations = [] + ; fix_attrs = [] }) fixexprl in l @@ -2102,7 +2103,8 @@ let make_graph (f_ref : GlobRef.t) = ; binders = nal_tas ; rtype = t ; body_def = Some b - ; notations = [] } ] + ; notations = [] + ; fix_attrs = [] } ] in let mp = Constant.modpath c in let expr_list = List.split expr_list in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 17df2fa47b46..4d23cc428809 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1463,7 +1463,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name () in let info = Declare.Info.make ~hook:(Declare.Hook.make hook) () in - let cinfo = Declare.CInfo.make ~name:na ~typ:gls_type () in + let cinfo = Declare.CInfo.make ~name:na ~typ:gls_type ~opaque:(Some false (* as in "defined" *)) () in let lemma = Declare.Proof.start ~cinfo ~info sigma in let lemma = if Indfun_common.is_strict_tcc () then @@ -1496,7 +1496,7 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes let cinfo = Declare.CInfo.make ~name:thm_name ~typ:(EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) - () + ~opaque:(Some false) () in let info = Declare.Info.make ~hook () in let lemma = Declare.Proof.start ~cinfo ~info ctx in @@ -1568,7 +1568,7 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref let cinfo = Declare.CInfo.make ~name:eq_name ~typ:(EConstr.of_constr equation_lemma_type) - () + ~opaque:(Some (opacity == Opaque)) () in let lemma = Declare.Proof.start ~cinfo evd ~info in let lemma = diff --git a/plugins/ltac/comRewrite.ml b/plugins/ltac/comRewrite.ml index 0948779ec313..fe46358c4571 100644 --- a/plugins/ltac/comRewrite.ml +++ b/plugins/ltac/comRewrite.ml @@ -35,15 +35,16 @@ let init_setoid () = type rewrite_attributes = { polymorphic : bool; locality : Hints.hint_locality; + opaque : bool option; } let rewrite_attributes = let open Attributes.Notations in - Attributes.(polymorphic ++ locality) >>= fun (polymorphic, locality) -> + Attributes.(polymorphic ++ locality ++ opacity) >>= fun ((polymorphic, locality), opaque) -> let locality = if Locality.make_section_locality locality then Hints.Local else SuperGlobal in - Attributes.Notations.return { polymorphic; locality } + Attributes.Notations.return { polymorphic; locality; opaque } (** Utility functions *) @@ -70,7 +71,7 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance atts binders (name,t) fields = - let _id = Classes.new_instance ~poly:atts.polymorphic + let _id : Id.t = Classes.new_instance ~poly:atts.polymorphic ~opaque:atts.opaque name binders t (true, CAst.make @@ CRecord (fields)) ~locality:atts.locality Hints.empty_hint_info in @@ -172,10 +173,10 @@ let declare_projection name instance_id r = let types = Some (it_mkProd_or_LetIn typ ctx) in let kind = Decls.(IsDefinition Definition) in let impargs, udecl = [], UState.default_univ_decl in - let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in + let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ~opaque:(Some false) () in let info = Declare.Info.make ~kind ~udecl ~poly () in let _r : GlobRef.t = - Declare.declare_definition ~cinfo ~info ~opaque:false ~body sigma + Declare.declare_definition ~cinfo ~info ~body sigma in () let add_setoid atts binders a aeq t n = @@ -195,7 +196,7 @@ let add_morphism_as_parameter atts m n : unit = let instance_id = add_suffix n "_Proper" in let env = Global.env () in let evd = Evd.from_env env in - let poly = atts.polymorphic in + let poly, opaque = atts.polymorphic, atts.opaque in let kind = Decls.(IsAssumption Logical) in let impargs, udecl = [], UState.default_univ_decl in let evd, types = Rewrite.Internal.build_morphism_signature env evd m in @@ -212,7 +213,7 @@ let add_morphism_interactive atts ~tactic m n : Declare.Proof.t = let env = Global.env () in let evd = Evd.from_env env in let evd, morph = Rewrite.Internal.build_morphism_signature env evd m in - let poly = atts.polymorphic in + let poly, opaque = atts.polymorphic, atts.opaque in let kind = Decls.(IsDefinition Instance) in let hook { Declare.Hook.S.dref; _ } = dref |> function | GlobRef.ConstRef cst -> @@ -224,7 +225,7 @@ let add_morphism_interactive atts ~tactic m n : Declare.Proof.t = let hook = Declare.Hook.make hook in Flags.silently (fun () -> - let cinfo = Declare.CInfo.make ~name:instance_id ~typ:morph () in + let cinfo = Declare.CInfo.make ~name:instance_id ~typ:morph ~opaque () in let info = Declare.Info.make ~poly ~hook ~kind () in let lemma = Declare.Proof.start ~cinfo ~info evd in fst (Declare.Proof.by tactic lemma)) () @@ -239,7 +240,7 @@ let add_morphism atts ~tactic binders m s n = [cHole; s; m]) in let _id, lemma = Classes.new_instance_interactive - ~locality:atts.locality ~poly:atts.polymorphic + ~locality:atts.locality ~poly:atts.polymorphic ~opaque:atts.opaque instance_name binders instance_t ~tac:tactic ~hook:(declare_projection n instance_id) Hints.empty_hint_info None diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 00681a922a8d..94d777c5eee6 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -303,39 +303,39 @@ let seff id = VtSideff ([id], VtLater) END*) VERNAC COMMAND EXTEND DeriveInversionClear -| #[ polymorphic; ] [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] +| #[ polymorphic; opacity ] [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] => { seff na } -> { - add_inversion_lemma_exn ~poly:polymorphic na c s false inv_clear_tac } + add_inversion_lemma_exn ~poly:polymorphic ~opaque:opacity na c s false inv_clear_tac } -| #[ polymorphic; ] [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na } +| #[ polymorphic; opacity ] [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na } -> { - add_inversion_lemma_exn ~poly:polymorphic na c Sorts.InProp false inv_clear_tac } + add_inversion_lemma_exn ~poly:polymorphic ~opaque:opacity na c Sorts.InProp false inv_clear_tac } END VERNAC COMMAND EXTEND DeriveInversion -| #[ polymorphic; ] [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] +| #[ polymorphic; opacity ] [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] => { seff na } -> { - add_inversion_lemma_exn ~poly:polymorphic na c s false inv_tac } + add_inversion_lemma_exn ~poly:polymorphic ~opaque:opacity na c s false inv_tac } -| #[ polymorphic; ] [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na } +| #[ polymorphic; opacity ] [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na } -> { - add_inversion_lemma_exn ~poly:polymorphic na c Sorts.InProp false inv_tac } + add_inversion_lemma_exn ~poly:polymorphic ~opaque:opacity na c Sorts.InProp false inv_tac } END VERNAC COMMAND EXTEND DeriveDependentInversion -| #[ polymorphic; ] [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] +| #[ polymorphic; opacity ] [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] => { seff na } -> { - add_inversion_lemma_exn ~poly:polymorphic na c s true dinv_tac } + add_inversion_lemma_exn ~poly:polymorphic ~opaque:opacity na c s true dinv_tac } END VERNAC COMMAND EXTEND DeriveDependentInversionClear -| #[ polymorphic; ] [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] +| #[ polymorphic; opacity ] [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] => { seff na } -> { - add_inversion_lemma_exn ~poly:polymorphic na c s true dinv_clear_tac } + add_inversion_lemma_exn ~poly:polymorphic ~opaque:opacity na c s true dinv_clear_tac } END (**********************************************************************) diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml index 54145c841c2b..6aba27bd6abb 100644 --- a/plugins/ltac/leminv.ml +++ b/plugins/ltac/leminv.ml @@ -229,25 +229,26 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = let invProof = it_mkNamedLambda_or_LetIn sigma c !ownSign in invProof, sigma -let add_inversion_lemma ~poly name env sigma t sort dep inv_op = +let add_inversion_lemma ~poly ~opaque name env sigma t sort dep inv_op = let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in - let cinfo = Declare.CInfo.make ~name ~typ:None () in + let opaque = Some (Option.default false opaque) in + let cinfo = Declare.CInfo.make ~name ~typ:None ~opaque () in let info = Declare.Info.make ~poly ~kind:Decls.(IsProof Lemma) () in let _ : Names.GlobRef.t = - Declare.declare_definition ~cinfo ~info ~opaque:false ~body:invProof sigma + Declare.declare_definition ~cinfo ~info ~body:invProof sigma in () (* inv_op = Inv (derives de complete inv. lemma) * inv_op = InvNoThining (derives de semi inversion lemma) *) -let add_inversion_lemma_exn ~poly na com comsort bool tac = +let add_inversion_lemma_exn ~poly ~opaque na com comsort bool tac = let env = Global.env () in let sigma = Evd.from_env env in let c, uctx = Constrintern.interp_type env sigma com in let sigma = Evd.from_ctx uctx in let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in - add_inversion_lemma ~poly na env sigma c sort bool tac + add_inversion_lemma ~poly ~opaque na env sigma c sort bool tac (* ================================= *) (* Applying a given inversion lemma *) diff --git a/plugins/ltac/leminv.mli b/plugins/ltac/leminv.mli index f835587c4328..ac4f5b544922 100644 --- a/plugins/ltac/leminv.mli +++ b/plugins/ltac/leminv.mli @@ -16,6 +16,6 @@ open Tactypes val lemInv_clause : quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic -val add_inversion_lemma_exn : poly:bool -> +val add_inversion_lemma_exn : poly:bool -> opaque:bool option -> Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) -> unit diff --git a/test-suite/success/sealed.v b/test-suite/success/sealed.v new file mode 100644 index 000000000000..83a21a94ef5c --- /dev/null +++ b/test-suite/success/sealed.v @@ -0,0 +1,37 @@ +(* Opacity per name *) +Fixpoint #[sealed] f n := match n with 0 => 0 | S n => g n end +with #[defined] g n := match n with 0 => 0 | S n => f n end. + +Fail Check eq_refl : f 0 = 0. +Check eq_refl : g 0 = 0. + +(* Opacity globally *) +#[sealed] +Fixpoint f' n := match n with 0 => 0 | S n => g' n end +with g' n := match n with 0 => 0 | S n => f' n end. + +Fail Check eq_refl : f' 0 = 0. +Fail Check eq_refl : g' 0 = 0. + +(* Don't mix the global and local attribute *) +Fail #[sealed] +Fixpoint #[sealed] f' n := match n with 0 => 0 | S n => g' n end +with g' n := match n with 0 => 0 | S n => f' n end. + +(* Other tests *) + +#[sealed] Definition c := 0. + +Fail Check eq_refl : c = 0. + +#[defined] Theorem u : nat. exact 0. Qed. (* ok *) +#[sealed] Definition v : nat. exact 0. Defined. (* ok *) + +Check eq_refl : u = 0. +Fail Check eq_refl : v = 0. + +#[sealed] Theorem w : nat. exact 0. Defined. +#[defined] Definition x : nat. exact 0. Qed. + +Fail Check eq_refl : w = 0. +Check eq_refl : x = 0. diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 93404d8a89a0..ba7ace2d7b46 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -265,6 +265,13 @@ let locality = ("global", single_key_parser ~name ~key:"global" false); ] +let opacity = + let name = "Opacity" in + attribute_of_list [ + ("sealed", single_key_parser ~name ~key:"sealed" true); + ("defined", single_key_parser ~name ~key:"defined" false); + ] + let ukey = "universes" let universe_polymorphism_option_name = ["Universe"; "Polymorphism"] diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 2ad19f75b8df..d58308bacd87 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -57,6 +57,7 @@ val template : bool option attribute val unfold_fix : bool attribute val locality : bool option attribute val option_locality : Goptions.option_locality attribute +val opacity : bool option attribute val reversible : bool option attribute val canonical_field : bool attribute val canonical_instance : bool attribute diff --git a/vernac/classes.ml b/vernac/classes.ml index fa1fb02f2d03..e9ec7d8a87e4 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -311,11 +311,11 @@ let instance_hook info global ?hook cst = declare_instance env sigma (Some info) global cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant iinfo global impargs ?hook name udecl poly sigma term termtype = +let declare_instance_constant iinfo global impargs ?hook name udecl opaque poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in - let cinfo = Declare.CInfo.make ~name ~impargs ~typ:(Some termtype) () in + let cinfo = Declare.CInfo.make ~name ~impargs ~typ:(Some termtype) ~opaque () in let info = Declare.Info.make ~kind ~poly ~udecl () in - let kn = Declare.declare_definition ~cinfo ~info ~opaque:false ~body:term sigma in + let kn = Declare.declare_definition ~cinfo ~info ~body:term sigma in instance_hook iinfo global ?hook kn let do_declare_instance sigma ~locality ~poly k u ctx ctx' pri udecl impargs subst name = @@ -332,7 +332,7 @@ let do_declare_instance sigma ~locality ~poly k u ctx ctx' pri udecl impargs sub Impargs.maybe_declare_manual_implicits false cst impargs; instance_hook pri locality cst -let declare_instance_program pm env sigma ~locality ~poly name pri impargs udecl term termtype = +let declare_instance_program pm env sigma ~locality ~opaque ~poly name pri impargs udecl term termtype = let hook { Declare.Hook.S.scope; dref; _ } = let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in let pri = intern_info pri in @@ -344,13 +344,12 @@ let declare_instance_program pm env sigma ~locality ~poly name pri impargs udecl let hook = Declare.Hook.make hook in let uctx = Evd.ustate sigma in let kind = Decls.IsDefinition Decls.Instance in - let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in - let info = Declare.Info.make ~udecl ~poly ~kind ~hook () in - let pm, _ = - Declare.Obls.add_definition ~pm ~info ~cinfo ~opaque:false ~uctx ~body obls - in pm + let cinfo = Declare.CInfo.make ~name ~typ ~impargs ~opaque () in + let info = Declare.Info.make ~udecl ~poly ~kind ~hook () in + let pm, _ = Declare.Obls.add_definition ~pm ~info ~cinfo ~uctx ~body obls in + pm -let declare_instance_open sigma ?hook ~tac ~locality ~poly id pri impargs udecl ids term termtype = +let declare_instance_open sigma ?hook ~tac ~locality ~opaque ~poly id pri impargs udecl ids term termtype = (* spiwack: it is hard to reorder the actions to do the pretyping after the proof has opened. As a consequence, we use the low-level primitives to code @@ -364,7 +363,7 @@ let declare_instance_open sigma ?hook ~tac ~locality ~poly id pri impargs udecl (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails! This is due to a bug in proof_global :( *) let termtype = Evarutil.nf_evar sigma termtype in - let cinfo = Declare.CInfo.make ~name:id ~impargs ~typ:termtype () in + let cinfo = Declare.CInfo.make ~name:id ~impargs ~typ:termtype ~opaque () in let lemma = Declare.Proof.start ~cinfo ~info sigma in (* spiwack: I don't know what to do with the status here. *) let lemma = @@ -483,15 +482,15 @@ let do_instance_interactive env env' sigma ?hook ~tac ~locality ~poly cty k u ct id pri imps decl (List.map RelDecl.get_name ctx) term termtype) () -let do_instance env env' sigma ?hook ~locality ~poly cty k u ctx ctx' pri decl imps subst id props = +let do_instance env env' sigma ?hook ~locality ~opaque ~poly cty k u ctx ctx' pri decl imps subst id props = let term, termtype, sigma = interp_props ~program_mode:false env' cty k u ctx ctx' subst sigma props in let termtype, sigma = do_instance_resolve_TC termtype sigma env in Pretyping.check_evars_are_solved ~program_mode:false env sigma; - declare_instance_constant pri locality imps ?hook id decl poly sigma term termtype + declare_instance_constant pri locality imps ?hook id decl opaque poly sigma term termtype -let do_instance_program ~pm env env' sigma ?hook ~locality ~poly cty k u ctx ctx' pri decl imps subst id opt_props = +let do_instance_program ~pm env env' sigma ?hook ~locality ~opaque ~poly cty k u ctx ctx' pri decl imps subst id opt_props = let term, termtype, sigma = match opt_props with | Some props -> @@ -504,10 +503,10 @@ let do_instance_program ~pm env env' sigma ?hook ~locality ~poly cty k u ctx ctx term, termtype, sigma in let termtype, sigma = do_instance_resolve_TC termtype sigma env in if not (Evd.has_undefined sigma) && not (Option.is_empty opt_props) then - let () = declare_instance_constant pri locality imps ?hook id decl poly sigma term termtype in + let () = declare_instance_constant pri locality imps ?hook id decl opaque poly sigma term termtype in pm else - declare_instance_program pm env sigma ~locality ~poly id pri imps decl term termtype + declare_instance_program pm env sigma ~locality ~opaque ~poly id pri imps decl term termtype let interp_instance_context ~program_mode env ctx pl tclass = let sigma, decl = interp_univ_decl_opt env pl in @@ -549,29 +548,29 @@ let new_instance_common ~program_mode env instid ctx cl = let env' = push_rel_context ctx env in id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl -let new_instance_interactive ~locality ~poly instid ctx cl +let new_instance_interactive ~locality ~opaque ~poly instid ctx cl ?(tac:unit Proofview.tactic option) ?hook pri opt_props = let env = Global.env() in let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = new_instance_common ~program_mode:false env instid ctx cl in - id, do_instance_interactive env env' sigma ?hook ~tac ~locality ~poly + id, do_instance_interactive env env' sigma ?hook ~tac ~locality ~opaque ~poly cty k u ctx ctx' pri decl imps subst id opt_props -let new_instance_program ~locality ~pm ~poly instid ctx cl opt_props ?hook pri = +let new_instance_program ~locality ~pm ~opaque ~poly instid ctx cl opt_props ?hook pri = let env = Global.env() in let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = new_instance_common ~program_mode:true env instid ctx cl in let pm = - do_instance_program ~pm env env' sigma ?hook ~locality ~poly + do_instance_program ~pm env env' sigma ?hook ~locality ~opaque ~poly cty k u ctx ctx' pri decl imps subst id opt_props in pm, id -let new_instance ~locality ~poly instid ctx cl props ?hook pri = +let new_instance ~locality ~opaque ~poly instid ctx cl props ?hook pri = let env = Global.env() in let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = new_instance_common ~program_mode:false env instid ctx cl in - do_instance env env' sigma ?hook ~locality ~poly + do_instance env env' sigma ?hook ~locality ~opaque ~poly cty k u ctx ctx' pri decl imps subst id props; id diff --git a/vernac/classes.mli b/vernac/classes.mli index b0760c641277..785abdbe1cc9 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -26,6 +26,7 @@ val existing_instance : ?loc:Loc.t -> Hints.hint_locality -> GlobRef.t -> Vernac val new_instance_interactive : locality:Hints.hint_locality + -> opaque:bool option -> poly:bool -> name_decl -> local_binder_expr list @@ -38,6 +39,7 @@ val new_instance_interactive val new_instance : locality:Hints.hint_locality + -> opaque:bool option -> poly:bool -> name_decl -> local_binder_expr list @@ -50,6 +52,7 @@ val new_instance val new_instance_program : locality:Hints.hint_locality -> pm:Declare.OblState.t + -> opaque:bool option -> poly:bool -> name_decl -> local_binder_expr list diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index dc1b66b53db0..d6e29fdcd231 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -117,7 +117,7 @@ let interp_statement ~program_mode env evd ~flags ~scope name bl typ = let ids = List.map Context.Rel.Declaration.get_name ctx in evd, ids, EConstr.it_mkProd_or_LetIn t' ctx, imps @ imps' -let do_definition ?hook ~name ?scope ?clearbody ~poly ?typing_flags ~kind ?using ?user_warns udecl bl red_option c ctypopt = +let do_definition ?hook ~name ?scope ~opaque ?clearbody ~poly ?typing_flags ~kind ?using ?user_warns udecl bl red_option c ctypopt = let program_mode = false in let env = Global.env() in let env = Environ.update_typing_flags ?typing_flags env in @@ -127,13 +127,13 @@ let do_definition ?hook ~name ?scope ?clearbody ~poly ?typing_flags ~kind ?using interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt in let kind = Decls.IsDefinition kind in - let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in + let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ~opaque () in let info = Declare.Info.make ?scope ?clearbody ~kind ?hook ~udecl ~poly ?typing_flags ?user_warns () in let _ : Names.GlobRef.t = - Declare.declare_definition ~info ~cinfo ~opaque:false ~body ?using evd + Declare.declare_definition ~info ~cinfo ~body ?using evd in () -let do_definition_program ?hook ~pm ~name ~scope ?clearbody ~poly ?typing_flags ~kind ?using ?user_warns udecl bl red_option c ctypopt = +let do_definition_program ?hook ~pm ~name ~scope ~opaque ?clearbody ~poly ?typing_flags ~kind ?using ?user_warns udecl bl red_option c ctypopt = let env = Global.env() in let env = Environ.update_typing_flags ?typing_flags env in (* Explicitly bound universes and constraints *) @@ -144,12 +144,12 @@ let do_definition_program ?hook ~pm ~name ~scope ?clearbody ~poly ?typing_flags let body, typ, uctx, _, obls = Declare.Obls.prepare_obligations ~name ~body ?types env evd in Evd.check_univ_decl_early ~poly ~with_obls:true evd udecl [body; typ]; let pm, _ = - let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in + let cinfo = Declare.CInfo.make ~name ~typ ~impargs ~opaque () in let info = Declare.Info.make ~udecl ~scope ?clearbody ~poly ~kind ?hook ?typing_flags ?user_warns () in - Declare.Obls.add_definition ~pm ~info ~cinfo ~opaque:false ~body ~uctx ?using obls + Declare.Obls.add_definition ~pm ~info ~cinfo ~body ~uctx ?using obls in pm -let do_definition_interactive ~program_mode ?hook ~name ~scope ?clearbody ~poly ~typing_flags ~kind ?using ?user_warns udecl bl t = +let do_definition_interactive ~program_mode ?hook ~name ~scope ~opaque ?clearbody ~poly ~typing_flags ~kind ?using ?user_warns udecl bl t = let env = Global.env () in let env = Environ.update_typing_flags ?typing_flags env in let flags = Pretyping.{ all_no_fail_flags with program_mode } in @@ -162,7 +162,7 @@ let do_definition_interactive ~program_mode ?hook ~name ~scope ?clearbody ~poly Pretyping.check_evars_are_solved ~program_mode env evd; let typ = EConstr.to_constr evd typ in let info = Declare.Info.make ?hook ~poly ~scope ?clearbody ~kind ~udecl ?typing_flags ?user_warns () in - let cinfo = Declare.CInfo.make ~name ~typ ~args ~impargs () in + let cinfo = Declare.CInfo.make ~name ~typ ~args ~impargs ~opaque () 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 Declare.Proof.start_definition ~info ~cinfo ?using evd diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 082073c049b5..91629b47ca75 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -29,6 +29,7 @@ val do_definition : ?hook:Declare.Hook.t -> name:Id.t -> ?scope:Locality.definition_scope + -> opaque:bool option -> ?clearbody:bool -> poly:bool -> ?typing_flags:Declarations.typing_flags @@ -47,6 +48,7 @@ val do_definition_program -> pm:Declare.OblState.t -> name:Id.t -> scope:Locality.definition_scope + -> opaque:bool option -> ?clearbody:bool -> poly:bool -> ?typing_flags:Declarations.typing_flags @@ -65,6 +67,7 @@ val do_definition_interactive -> ?hook:Declare.Hook.t -> name:Id.t -> scope:Locality.definition_scope + -> opaque:bool option -> ?clearbody:bool -> poly:bool -> typing_flags:Declarations.typing_flags option diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 0e3e49be5f85..55fe6b540539 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -385,6 +385,7 @@ type ('constr, 'relevance) fix_data = { fiximps : (Names.Name.t * bool) option CAst.t list list; fixntns : Metasyntax.notation_interpretation_decl list; fixwfs : (rel_declaration * EConstr.t * EConstr.t * EConstr.t) option list; + fixopaques : bool option list; } let interp_wf ~program_mode env sigma recname ctx ccl = function @@ -413,7 +414,7 @@ let interp_wf ~program_mode env sigma recname ctx ccl = function in sigma, ((after, [extradecl]), Some (extradecl, rel, relargty, measure), [impl]) -let interp_mutual_definition env ~program_mode ~function_mode rec_order fixl = +let interp_mutual_definition env ~program_mode ~function_mode ?opaque rec_order fixl = let open Context.Named.Declaration in let open EConstr in let fixnames = List.map (fun fix -> fix.Vernacexpr.fname.CAst.v) fixl in @@ -461,9 +462,13 @@ let interp_mutual_definition env ~program_mode ~function_mode rec_order fixl = (* Instantiate evars and check all are resolved *) let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in let sigma = Evd.minimize_universes sigma in + let fixopaques = List.map (fun { Vernacexpr.fix_attrs } -> Attributes.(parse opacity fix_attrs)) fixl in + if List.exists Option.has_some fixopaques && Option.has_some opaque then + CErrors.user_err Pp.(str "Opacity attribute given both globally for the declaration and locally on the names of the declaration."); + let fixopaques = List.map (function None -> (* use global opacity *) opaque | Some _ as o -> o) fixopaques in (* Build the fix declaration block *) - let fix = {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs} in + let fix = {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs;fixopaques} in (env, rec_sign, sigma), (fix, possible_guard, decl) let check_recursive ~kind env evd {fixnames;fixdefs;fixwfs} = @@ -473,12 +478,12 @@ let check_recursive ~kind env evd {fixnames;fixdefs;fixwfs} = check_true_recursivity env evd ~kind (List.combine fixnames fixdefs) end -let ground_fixpoint env evd {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs} = +let ground_fixpoint env evd {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs;fixopaques} = Pretyping.check_evars_are_solved ~program_mode:false env evd; let fixrs = List.map (fun r -> EConstr.ERelevance.kind evd r) fixrs in let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in let fixtypes = List.map EConstr.(to_constr evd) fixtypes in - {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs} + {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs;fixopaques} (** For Funind *) @@ -489,11 +494,11 @@ let interp_fixpoint_short rec_order fixpoint_exprl = let typel = (ground_fixpoint env sigma fix).fixtypes in typel, sigma -let build_recthms {fixnames;fixtypes;fixctxs;fiximps} = - List.map4 (fun name typ ctx impargs -> +let build_recthms {fixnames;fixtypes;fixctxs;fiximps;fixopaques} = + List.map5 (fun name typ ctx impargs opaque -> let args = List.map Context.Rel.Declaration.get_name ctx in - Declare.CInfo.make ~name ~typ ~args ~impargs () - ) fixnames fixtypes fixctxs fiximps + Declare.CInfo.make ~name ~typ ~args ~impargs ~opaque () + ) fixnames fixtypes fixctxs fiximps fixopaques let collect_evars_of_term evd c ty = Evar.Set.union (Evd.evars_of_term evd c) (Evd.evars_of_term evd ty) @@ -528,26 +533,26 @@ let build_program_fixpoint env sigma rec_sign possible_guard fixnames fixrs fixd List.split3 (List.map3 (collect_evars env sigma rec_sign) fixnames fixdefs fixtypes) let finish_obligations env sigma rec_sign possible_guard poly udecl = function - | {fixnames=[recname];fixrs;fixdefs=[body];fixtypes=[ccl];fixctxs=[ctx];fiximps=[imps];fixntns;fixwfs=[Some wf]} -> + | {fixnames=[recname];fixrs;fixdefs=[body];fixtypes=[ccl];fixctxs=[ctx];fiximps=[imps];fixntns;fixwfs=[Some wf];fixopaques} -> let sigma = Evarutil.nf_evar_map sigma in (* use nf_evar_map_undefined?? *) let sigma, recname, body, ccl, impls, obls, hook = build_wellfounded env sigma poly udecl recname ctx (Option.get body) ccl imps wf in let fixrs = List.map (EConstr.ERelevance.kind sigma) fixrs in - sigma, {fixnames=[recname];fixrs;fixdefs=[Some body];fixtypes=[ccl];fixctxs=[ctx];fiximps=[impls];fixntns;fixwfs=[Some wf]}, [obls], hook - | {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs} -> + sigma, {fixnames=[recname];fixrs;fixdefs=[Some body];fixtypes=[ccl];fixctxs=[ctx];fiximps=[impls];fixntns;fixwfs=[Some wf];fixopaques}, [obls], hook + | {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs;fixopaques} -> let fixdefs, fixtypes, obls = build_program_fixpoint env sigma rec_sign possible_guard fixnames fixrs fixdefs fixtypes fixwfs in let fixrs = List.map (EConstr.ERelevance.kind sigma) fixrs in - sigma, {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs}, obls, None + sigma, {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs;fixopaques}, obls, None 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 ~program_mode ?(use_inference_hook=false) ?scope ?clearbody ~kind ~poly ?typing_flags ?user_warns ?using (rec_order, fixl) +let do_mutually_recursive ?pm ~program_mode ?(use_inference_hook=false) ?scope ?opaque ?clearbody ~kind ~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,possible_guard,udecl) = interp_mutual_definition env ~program_mode ~function_mode:false rec_order fixl in + let (env,rec_sign,sigma),(fix,possible_guard,udecl) = interp_mutual_definition env ~program_mode ~function_mode:false ?opaque rec_order fixl in check_recursive ~kind env sigma fix; let sigma, ({fixdefs=bodies;fixrs;fixtypes;fixwfs} as fix), obls, hook = match pm with @@ -565,11 +570,11 @@ let do_mutually_recursive ?pm ~program_mode ?(use_inference_hook=false) ?scope ? (match fixwfs, bodies, cinfo, obls with | [Some _], [body], [cinfo], [obls] -> (* Program Fixpoint wf/measure *) - let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~opaque:false ~body ~uctx ?using obls in + let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~body ~uctx ?using obls in Some pm, None | _ -> let possible_guard = (possible_guard, fixrs) in - Some (Declare.Obls.add_mutual_definitions ~pm ~cinfo ~info ~opaque:false ~uctx ~bodies ~possible_guard ?using obls), None) + Some (Declare.Obls.add_mutual_definitions ~pm ~cinfo ~info ~uctx ~bodies ~possible_guard ?using obls), None) | None -> try let bodies = List.map Option.get bodies in @@ -577,7 +582,7 @@ let do_mutually_recursive ?pm ~program_mode ?(use_inference_hook=false) ?scope ? (* All bodies are defined *) let possible_guard = (possible_guard, fixrs) in let _ : GlobRef.t list = - Declare.declare_mutual_definitions ~cinfo ~info ~opaque:false ~uctx ~possible_guard ~bodies ?using () + Declare.declare_mutual_definitions ~cinfo ~info ~uctx ~possible_guard ~bodies ?using () in None, None with Option.IsNone -> diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index ccf66982dc8a..bb896ebaeeba 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -27,6 +27,8 @@ val do_mutually_recursive (* Tell to try the obligation tactic to solve evars *) -> ?scope:Locality.definition_scope (* Local or Global visibility *) + -> ?opaque:bool + (* Global opacity attribute if any *) -> ?clearbody:bool (* Hide body if in sections *) -> kind:Decls.logical_kind diff --git a/vernac/declare.ml b/vernac/declare.ml index 2e601bb75c8c..ce3e4f3430c6 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -57,11 +57,12 @@ module CInfo = struct (** Names to pre-introduce *) ; impargs : Impargs.manual_implicits (** Explicitily declared implicit arguments *) + ; opaque : bool option } - let make ~name ~typ ?(args=[]) ?(impargs=[]) () = - { name; typ; args; impargs } + let make ~name ~typ ?(args=[]) ?(impargs=[]) ~opaque () = + { name; typ; args; impargs; opaque } let to_constr sigma thm = { thm with typ = EConstr.to_constr sigma thm.typ } @@ -87,8 +88,6 @@ module Info = struct ; ntns : Metasyntax.notation_interpretation_decl list } - (** Note that [opaque] doesn't appear here as it is not known at the - start of the proof in the interactive case. *) let make ?(poly=false) ?(inline=false) ?(kind=Decls.(IsDefinition Definition)) ?(udecl=UState.default_univ_decl) ?(scope=Locality.default_scope) ?(clearbody=false) ?hook ?typing_flags ?user_warns ?(ntns=[]) () = @@ -511,6 +510,19 @@ type ('a, 'b) effect_entry = | DeferredEffectEntry : (private_constants Entries.proof_output Future.computation, unit) effect_entry | PureEntry : (Constr.constr, Constr.constr) effect_entry +let get_opaque_proof (type a b) env (entry : (a, b) effect_entry) (body : a) : Environ.env * Constr.constr = + (* To be called only if we know that there is a proof (e.g. not in vos mode) *) + match entry with + | PureEntry -> env, body + | ImmediateEffectEntry -> + let (pf, _), eff = body in + let env = Safe_typing.push_private_constants env eff in + env, pf + | DeferredEffectEntry -> + let (pf, _), eff = Future.force body in + let env = Safe_typing.push_private_constants env eff in + env, pf + let section_context_of_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (body : a) typ = let open Environ in let env = Global.env () in @@ -518,18 +530,8 @@ let section_context_of_opaque_proof_entry (type a b) (entry : (a, b) effect_entr if List.is_empty (Environ.named_context env) then Id.Set.empty, Id.Set.empty else + let env, pf = get_opaque_proof env entry body in let ids_typ = global_vars_set env typ in - let (pf : Constr.constr), env = match entry with - | PureEntry -> body, env - | ImmediateEffectEntry -> - let (pf, _), eff = body in - let env = Safe_typing.push_private_constants env eff in - pf, env - | DeferredEffectEntry -> - let (pf, _), eff = Future.force body in - let env = Safe_typing.push_private_constants env eff in - pf, env - in let vars = global_vars_set env pf in ids_typ, vars in @@ -537,8 +539,12 @@ let section_context_of_opaque_proof_entry (type a b) (entry : (a, b) effect_entr Environ.really_needed env (Id.Set.union hyp_typ hyp_def) let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a pproof_entry) : b Entries.opaque_entry * _ = + let env = Global.env () in let typ = match e.proof_entry_type with - | None -> assert false + | None -> + let env, pf = get_opaque_proof env entry e.proof_entry_body in + let evd = Evd.from_env env in + EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr pf)) | Some typ -> typ in let secctx = match e.proof_entry_secctx with @@ -844,26 +850,22 @@ type proof_object = ; initial_euctx : UState.t } +let check_opacity opaque sealed = + match sealed with + | Some sealed -> (* Attribute takes precedence *) sealed + | None -> opaque + let future_map2_pair_list_distribute p l f = List.map_i (fun i c -> f (Future.chain p (fun (a, b) -> (List.nth a i, b))) c) 0 l -let process_proof ~info:Info.({ udecl; poly }) ?(is_telescope=false) = function +let process_proof ~info:Info.({ udecl; poly; kind }) ~cinfo = function | DefaultProof { proof = (entries, uctx); opaque; using; keep_body_ucst_separate } -> (* Force transparency for Derive-like dependent statements *) - let opaques = - let n = List.length entries in - List.init n (fun i -> - if i < n-1 && is_telescope then (* waiting for addition of cinfo-based opacity in #19029 *) false - else opaque) in - (* Multiple entries mean either a recursive block of definitions - (as in Co/Fixpoint) or a sequence of dependent definitions (as - in "Derive"). In the second case, the dependency in the - previous entries requires to accumulate the universes from the - previous definitions *) - snd (List.fold_left2_map (fun used_univs ((body, eff), typ) opaque -> + snd (List.fold_left2_map (fun used_univs ((body, eff), typ) CInfo.{ opaque = sealed } -> + let opaque = check_opacity opaque sealed in let uctx, univs, used_univs, body = make_univs_immediate ~poly ?keep_body_ucst_separate ~opaque ~uctx ~udecl ~eff ~used_univs body typ in - (used_univs, (definition_entry_core ?using ~univs ?types:typ body, uctx))) Univ.Level.Set.empty entries opaques) + (used_univs, (definition_entry_core ?using ~univs ?types:typ body, uctx))) Univ.Level.Set.empty entries cinfo) | DeferredOpaqueProof { deferred_proof = bodies; using; initial_proof_data; feedback_id; initial_euctx } -> let { Proof.poly; entry; sigma } = initial_proof_data in (* Deferred multiple entries currently assume either a mutual @@ -966,7 +968,7 @@ let interp_mutual_using env cinfo bodies_types using = using let declare_possibly_mutual_definitions ~info ~cinfo ~obls obj = - let entries = process_proof ~info obj in + let entries = process_proof ~info ~cinfo obj in let { Info.hook; scope; clearbody; kind; typing_flags; user_warns; ntns; _ } = info in let refs = List.map2 (fun CInfo.{name; impargs} (entry, uctx) -> declare_entry ~name ~scope ~clearbody ~kind ?hook ~impargs ~typing_flags ~user_warns ~obls ~uctx entry) cinfo entries in @@ -1019,9 +1021,24 @@ let prepare_recursive_edeclaration sigma cinfo fixtypes fixrs fixdefs = let defs = List.map (EConstr.Vars.subst_vars sigma (List.rev fixnames)) fixdefs in (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) -let declare_mutual_definitions ~info ~cinfo ~opaque ~uctx ~bodies ~possible_guard ?using () = +let default_kind_opacity_immediate = function + | Decls.IsPrimitive | IsSymbol | IsAssumption _ -> true (* Irrelevant *) + | IsDefinition _ -> false + | IsProof _ -> true + +let set_immediate_opacity kind cinfo = + if List.exists (fun CInfo.{opaque} -> Option.is_empty opaque) cinfo then + begin + match kind with + | Decls.IsProof p -> CErrors.user_err (str (Ppvernac.string_of_theorem_kind p) ++ str " declared with \":=\" requires sealed/defined attributes.") + + | _ -> () + end; + default_kind_opacity_immediate kind + +let declare_mutual_definitions ~info ~cinfo ~uctx ~bodies ~possible_guard ?using () = (* Note: uctx is supposed to be already minimized *) - let { Info.typing_flags; _ } = info in + let { Info.typing_flags; kind; _ } = info in let env = Global.env() in let possible_guard, fixrelevances = possible_guard in let fixtypes = List.map (fun CInfo.{typ} -> typ) cinfo in @@ -1030,6 +1047,7 @@ let declare_mutual_definitions ~info ~cinfo ~opaque ~uctx ~bodies ~possible_guar let entries = List.map (fun (body, typ) -> ((body, Evd.empty_side_effects), Some typ)) bodies_types in let entries_for_using = List.map (fun (body, typ) -> (body, Some typ)) bodies_types in let using = interp_mutual_using env cinfo entries_for_using using in + let opaque = set_immediate_opacity kind cinfo in let obj = DefaultProof { proof = (entries, uctx); opaque; using; keep_body_ucst_separate = None } in let refs = declare_possibly_mutual_definitions ~info ~cinfo ~obls:[] obj in let fixnames = List.map (fun { CInfo.name } -> name) cinfo in @@ -1054,8 +1072,8 @@ let check_evars_are_solved env sigma t = let evars = Evarutil.undefined_evars_of_term sigma t in if not (Evar.Set.is_empty evars) then error_unresolved_evars env sigma t evars -let declare_definition ~info ~cinfo ~opaque ~obls ~body ?using sigma = - let { CInfo.name; typ; _ } = cinfo in +let declare_definition ~info ~cinfo ~obls ~body ?using sigma = + let { CInfo.name; typ; opaque; _ } = cinfo in let env = Global.env () in Option.iter (check_evars_are_solved env sigma) typ; check_evars_are_solved env sigma body; @@ -1063,6 +1081,7 @@ let declare_definition ~info ~cinfo ~opaque ~obls ~body ?using sigma = let body = EConstr.to_constr sigma body in let typ = Option.map (EConstr.to_constr sigma) typ in let uctx = Evd.ustate sigma in + let opaque = set_immediate_opacity info.Info.kind [cinfo] in let using = interp_mutual_using env [cinfo] [body,typ] using in let obj = DefaultProof { proof = ([((body,Evd.empty_side_effects),typ)], uctx); opaque; using; keep_body_ucst_separate = None } in let gref = List.hd (declare_possibly_mutual_definitions ~info ~cinfo:[cinfo] ~obls obj) in @@ -1128,7 +1147,6 @@ module ProgramDecl = struct { prg_cinfo : constr CInfo.t ; prg_info : Info.t ; prg_using : Vernacexpr.section_subset_expr option - ; prg_opaque : bool ; prg_hook : 'a option ; prg_body : constr ; prg_uctx : UState.t @@ -1140,7 +1158,7 @@ module ProgramDecl = struct open Obligation - let make ~info ~cinfo ~opaque ~reduce ~deps ~uctx ~body ~possible_guard ?obl_hook ?using obls = + let make ~info ~cinfo ~reduce ~deps ~uctx ~body ~possible_guard ?obl_hook ?using obls = let obls', body = match body with | None -> @@ -1172,7 +1190,6 @@ module ProgramDecl = struct ; prg_info = info ; prg_using = using ; prg_hook = obl_hook - ; prg_opaque = opaque ; prg_body = body ; prg_uctx ; prg_obligations = {obls = obls'; remaining = Array.length obls'} @@ -1463,10 +1480,10 @@ let declare_definition ~pm prg = let body, types = subst_prog varsubst prg in let body, types = EConstr.(of_constr body, of_constr types) in let cinfo = { prg.prg_cinfo with CInfo.typ = Some types } in - let name, info, opaque, using = prg.prg_cinfo.CInfo.name, prg.prg_info, prg.prg_opaque, prg.prg_using in + let name, info, using = prg.prg_cinfo.CInfo.name, prg.prg_info, prg.prg_using in let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in (* XXX: This is doing normalization twice *) - let kn, uctx = declare_definition ~cinfo ~info ~obls ~body ~opaque ?using sigma in + let kn, uctx = declare_definition ~cinfo ~info ~obls ~body ?using sigma in (* XXX: We call the obligation hook here, by consistency with the previous imperative behaviour, however I'm not sure this is right *) let pm = State.call_prg_hook prg @@ -1484,19 +1501,19 @@ let declare_mutual_definitions ~pm l = let typ = EConstr.of_constr typ in let term = EConstr.to_constr sigma term in let typ = EConstr.to_constr sigma typ in - let def = (x.prg_reduce term, x.prg_reduce typ, x.prg_cinfo.CInfo.impargs) in + let def = (x.prg_reduce term, x.prg_reduce typ, (x.prg_cinfo.CInfo.impargs, x.prg_cinfo.CInfo.opaque)) in let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in (def, oblsubst) in let defs, obls = List.split (List.map defobl l) in let obls = List.flatten obls in - let fixitems = List.map2 (fun (d, typ, impargs) name -> CInfo.make ~name ~typ ~impargs ()) defs first.prg_deps in + let fixitems = List.map2 (fun (d, typ, (impargs, opaque)) name -> CInfo.make ~name ~typ ~impargs ~opaque ()) defs first.prg_deps in let fixdefs, fixtypes, _ = List.split3 defs in let possible_guard = Option.get first.prg_possible_guard in (* Declare the recursive definitions *) let kns = declare_mutual_definitions ~info:first.prg_info - ~uctx:first.prg_uctx ~bodies:fixdefs ~possible_guard ~opaque:first.prg_opaque + ~uctx:first.prg_uctx ~bodies:fixdefs ~possible_guard ~cinfo:fixitems ?using:first.prg_using () in (* Only for the first constant *) @@ -2044,6 +2061,8 @@ let control_only_guard { proof; pinfo } = raise (NotGuarded (env, sigma, cofix_error, fix_errors, rec_declaration)) with Exit -> () + (* Ignoring Qed/Defined keyword *) + let return_proof p = (prepare_proof p : closed_proof_output) let close_proof ?warn_incomplete ~opaque ~keep_body_ucst_separate (proof : t) : Proof_object.t = @@ -2075,13 +2094,13 @@ let next = let n = ref 0 in fun () -> incr n; !n let by tac = map_fold ~f:(Proof.solve (Goal_select.SelectNth 1) None tac) let build_constant_by_tactic ~name ?warn_incomplete ~sigma ~sign ~poly (typ : EConstr.t) tac = - let cinfo = [CInfo.make ~name ~typ:() ()] in + let cinfo = [CInfo.make ~name ~typ:() ~opaque:None ()] in let info = Info.make ~poly () in let pinfo = Proof_info.make ~cinfo ~info () in let pf = start_proof_core ~name ~pinfo sigma [Some sign, typ] in let pf, status = by tac pf in let proof = close_proof ?warn_incomplete ~keep_body_ucst_separate:false ~opaque:Vernacexpr.Transparent pf in - let entries = process_proof ~info proof.proof_object in + let entries = process_proof ~info ~cinfo proof.proof_object in let { Proof.sigma } = Proof.data pf.proof in let sigma = Evd.set_universe_context sigma (ustate_of_proof proof.proof_object) in match entries with @@ -2284,15 +2303,15 @@ let finish_proof ~pm proof_obj proof_info = | Regular -> pm, declare_possibly_mutual_definitions ~info ~cinfo ~obls:[] proof_obj | End_obligation oinfo -> - let entries = process_proof ~info proof_obj in + let entries = process_proof ~info ~cinfo proof_obj in let entry, uctx = check_single_entry entries "Obligation.save" in Obls_.obligation_terminator ~pm ~entry ~uctx ~oinfo | End_derive -> - let entries = process_proof ~info ~is_telescope:true proof_obj in + let entries = process_proof ~info ~cinfo proof_obj in pm, finish_derived proof_info entries | End_equations { hook; i; types; sigma } -> let kind = info.Info.kind in - let entries = process_proof ~info proof_obj in + let entries = process_proof ~info ~cinfo proof_obj in let entries = List.map fst entries in finish_proved_equations ~pm ~kind ~hook i entries types sigma @@ -2331,7 +2350,7 @@ let save_regular ~(proof : t) ~opaque ~idopt = (***********************************************************************) let save_lemma_admitted_delayed ~pm ~proof = let { Proof_object.proof_object; pinfo } = proof in - let entries = process_proof ~info:pinfo.info proof_object in + let entries = process_proof ~info:pinfo.info ~cinfo:pinfo.cinfo proof_object in let typs = List.map (function { proof_entry_type }, uctx -> Option.get proof_entry_type, uctx) entries in (* Note: an alternative would be to compute sec_vars of the partial proof as a Future computation, as in compute_proof_using_for_admitted *) @@ -2539,7 +2558,7 @@ let solve_obligation ?check_final prg num tac = let name = Internal.get_name prg in Proof_ending.End_obligation {name; num; auto; check_final} in - let cinfo = CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) () in + let cinfo = CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) ~opaque:None () in let using = let using = Internal.get_using prg in let env = Global.env () in @@ -2633,11 +2652,11 @@ let msg_generating_obl name obls = info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) -let add_definition ~pm ~info ~cinfo ~opaque ~uctx ?body +let add_definition ~pm ~info ~cinfo ~uctx ?body ?tactic ?(reduce = reduce) ?using ?obl_hook obls = let obl_hook = Option.map (fun h -> State.PrgHook h) obl_hook in let prg = - ProgramDecl.make ~info ~cinfo ~body ~opaque ~uctx ~reduce ~deps:[] ~possible_guard:None ?obl_hook ?using obls + ProgramDecl.make ~info ~cinfo ~body ~uctx ~reduce ~deps:[] ~possible_guard:None ?obl_hook ?using obls in let name = CInfo.get_name cinfo in let {obls;_} = Internal.get_obligations prg in @@ -2655,7 +2674,7 @@ let add_definition ~pm ~info ~cinfo ~opaque ~uctx ?body pm, res | _ -> pm, res -let add_mutual_definitions ~pm ~info ~cinfo ~opaque ~uctx ~bodies ~possible_guard +let add_mutual_definitions ~pm ~info ~cinfo ~uctx ~bodies ~possible_guard ?tactic ?(reduce = reduce) ?using ?obl_hook obls = let obl_hook = Option.map (fun h -> State.PrgHook h) obl_hook in let deps = List.map CInfo.get_name cinfo in @@ -2663,7 +2682,7 @@ let add_mutual_definitions ~pm ~info ~cinfo ~opaque ~uctx ~bodies ~possible_guar List.fold_left3 (fun pm cinfo body obls -> let prg = - ProgramDecl.make ~info ~cinfo ~opaque ~body:(Some body) ~uctx ~deps + ProgramDecl.make ~info ~cinfo ~body:(Some body) ~uctx ~deps ~possible_guard:(Some possible_guard) ~reduce ?obl_hook ?using obls in State.add pm (CInfo.get_name cinfo) prg) @@ -2791,9 +2810,9 @@ let declare_constant ?local ~name ~kind ?typing_flags = let declare_entry ~name ?scope ~kind ?user_warns ?hook ~impargs ~uctx entry = declare_entry ~name ?scope ~kind ~typing_flags:None ?clearbody:None ~user_warns ?hook ~impargs ~uctx entry -let declare_definition_full ~info ~cinfo ~opaque ~body ?using sigma = - let c, uctx = declare_definition ~obls:[] ~info ~cinfo ~opaque ~body ?using sigma in +let declare_definition_full ~info ~cinfo ~body ?using sigma = + let c, uctx = declare_definition ~obls:[] ~info ~cinfo ~body ?using sigma in c, if info.poly then Univ.ContextSet.empty else UState.context_set uctx -let declare_definition ~info ~cinfo ~opaque ~body ?using sigma = - declare_definition ~obls:[] ~info ~cinfo ~opaque ~body ?using sigma |> fst +let declare_definition ~info ~cinfo ~body ?using sigma = + declare_definition ~obls:[] ~info ~cinfo ~body ?using sigma |> fst diff --git a/vernac/declare.mli b/vernac/declare.mli index 782c40d7705d..128ce63a3d15 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -79,6 +79,7 @@ module CInfo : sig -> typ:'constr -> ?args:Name.t list -> ?impargs:Impargs.manual_implicits + -> opaque : bool option -> unit -> 'constr t @@ -125,7 +126,6 @@ end val declare_definition : info:Info.t -> cinfo:EConstr.t option CInfo.t - -> opaque:bool -> body:EConstr.t -> ?using:Vernacexpr.section_subset_expr -> Evd.evar_map @@ -134,7 +134,6 @@ val declare_definition val declare_mutual_definitions : info:Info.t -> cinfo: Constr.t CInfo.t list - -> opaque:bool -> uctx:UState.t -> bodies:Constr.t list -> possible_guard:Pretyping.possible_guard * Sorts.relevance list @@ -431,7 +430,6 @@ val declare_constant val declare_definition_full : info:Info.t -> cinfo:EConstr.t option CInfo.t - -> opaque:bool -> body:EConstr.t -> ?using:Vernacexpr.section_subset_expr -> Evd.evar_map @@ -538,7 +536,6 @@ val add_definition : pm:OblState.t -> info:Info.t -> cinfo:Constr.types CInfo.t - -> opaque:bool -> uctx:UState.t -> ?body:Constr.t -> ?tactic:unit Proofview.tactic @@ -556,7 +553,6 @@ val add_mutual_definitions : pm:OblState.t -> info:Info.t -> cinfo:Constr.types CInfo.t list - -> opaque:bool -> uctx:UState.t -> bodies:Constr.t list -> possible_guard:(Pretyping.possible_guard * Sorts.relevance list) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 550a3e5d3412..8820ac988b45 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -500,18 +500,18 @@ GRAMMAR EXTEND Gram ; (* (co)-fixpoints *) fix_definition: - [ [ id_decl = ident_decl; + [ [ fix_attrs = quoted_attributes; id_decl = ident_decl; bl = binders_fixannot; rtype = type_cstr; body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notations -> { let binders, rec_order = bl in - ((rec_order : Constrexpr.fixpoint_order_expr option), {fname = fst id_decl; univs = snd id_decl; binders; rtype; body_def; notations}) + ((rec_order : Constrexpr.fixpoint_order_expr option), {fname = fst id_decl; univs = snd id_decl; binders; rtype; body_def; notations; fix_attrs}) } ] ] ; cofix_definition: - [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr; + [ [ fix_attrs = quoted_attributes; id_decl = ident_decl; binders = binders; rtype = type_cstr; body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notations -> - { {fname = fst id_decl; univs = snd id_decl; binders; rtype; body_def; notations} + { {fname = fst id_decl; univs = snd id_decl; binders; rtype; body_def; notations; fix_attrs} } ]] ; (* Rewrite Rules *) diff --git a/vernac/ppvernac.mli b/vernac/ppvernac.mli index f13b4ea8f675..5f360ec7a6f7 100644 --- a/vernac/ppvernac.mli +++ b/vernac/ppvernac.mli @@ -29,3 +29,5 @@ val pr_using : Vernacexpr.section_subset_expr -> Pp.t (** Prints a vernac expression and closes it with a dot. *) val pr_vernac : Vernacexpr.vernac_control -> Pp.t + +val string_of_theorem_kind : Decls.theorem_kind -> string diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 83d09f05178d..111636aaf08b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -60,6 +60,7 @@ module DefAttributes = struct using : Vernacexpr.section_subset_expr option; reversible : bool; clearbody: bool option; + opacity: bool option; } (* [locality] is used for [vernac_definition_hook], the raw Local/Global attribute is also used to generate [scope]. @@ -109,16 +110,16 @@ module DefAttributes = struct let clearbody = match discharge with DoDischarge -> clearbody | NoDischarge -> return None in (locality ++ user_warns_with_use_globref_instead ++ polymorphic ++ program ++ canonical_instance ++ typing_flags ++ using ++ - reversible ++ clearbody) >>= fun ((((((((locality, user_warns), polymorphic), program), + reversible ++ clearbody ++ opacity) >>= fun (((((((((locality, user_warns), polymorphic), program), canonical_instance), typing_flags), using), - reversible), clearbody) -> + reversible), clearbody), opacity) -> 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 } + return { scope; locality; polymorphic; program; user_warns; canonical_instance; typing_flags; using; reversible; clearbody; opacity } let parse ?coercion ?discharge f = Attributes.parse (def_attributes_gen ?coercion ?discharge ()) f @@ -835,18 +836,18 @@ let vernac_definition_name lid local = let vernac_definition_interactive ~atts (discharge, kind) (lid, udecl) bl t = let open DefAttributes 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 + let scope, local, poly, program_mode, user_warns, typing_flags, using, clearbody, opaque = + atts.scope, atts.locality, atts.polymorphic, atts.program, atts.user_warns, atts.typing_flags, atts.using, atts.clearbody, atts.opacity in let canonical_instance, reversible = atts.canonical_instance, atts.reversible in let hook = vernac_definition_hook ~canonical_instance ~local ~poly ~reversible kind in let name = vernac_definition_name lid scope in - ComDefinition.do_definition_interactive ~typing_flags ~program_mode ~name ~poly ~scope ?clearbody:atts.clearbody + ComDefinition.do_definition_interactive ~typing_flags ~program_mode ~name ~poly ~scope ~opaque ?clearbody:atts.clearbody ~kind:(Decls.IsDefinition kind) ?user_warns ?using:atts.using ?hook udecl bl t let vernac_definition ~atts ~pm (discharge, kind) (lid, udecl) bl red_option c typ_opt = let open DefAttributes 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 + let scope, local, poly, program_mode, user_warns, typing_flags, using, clearbody, opaque = + atts.scope, atts.locality, atts.polymorphic, atts.program, atts.user_warns, atts.typing_flags, atts.using, atts.clearbody, atts.opacity in let canonical_instance, reversible = atts.canonical_instance, atts.reversible in let hook = vernac_definition_hook ~canonical_instance ~local ~poly kind ~reversible in let name = vernac_definition_name lid scope in @@ -858,12 +859,12 @@ let vernac_definition ~atts ~pm (discharge, kind) (lid, udecl) bl red_option c t Some (snd (Redexpr.interp_redexp_no_ltac env sigma r)) in if program_mode then let kind = Decls.IsDefinition kind in - ComDefinition.do_definition_program ~pm ~name + ComDefinition.do_definition_program ~pm ~name ~opaque ?clearbody ~poly ?typing_flags ~scope ~kind ?user_warns ?using udecl bl red_option c typ_opt ?hook else let () = - ComDefinition.do_definition ~name + ComDefinition.do_definition ~name ~opaque ?clearbody ~poly ?typing_flags ~scope ~kind ?user_warns ?using udecl bl red_option c typ_opt ?hook in pm @@ -873,21 +874,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, 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 + let scope, local, poly, program_mode, user_warns, typing_flags, using, clearbody, opaque = + atts.scope, atts.locality, atts.polymorphic, atts.program, atts.user_warns, atts.typing_flags, atts.using, atts.clearbody, atts.opacity in List.iter (fun ((id, _), _) -> check_name_freshness scope id) l; match l with | [] -> assert false | [({v=name},udecl),(bl,typ)] -> ComDefinition.do_definition_interactive - ~typing_flags ~program_mode ~name ~poly ?clearbody ~scope + ~typing_flags ~program_mode ~name ~poly ?clearbody ~scope ~opaque ~kind:(Decls.IsProof kind) ?user_warns ?using udecl bl typ | _ -> let fix = List.map (fun ((fname, univs), (binders, rtype)) -> - { fname; binders; rtype; body_def = None; univs; notations = []}) l in + { fname; binders; rtype; body_def = None; univs; notations = []; fix_attrs = [] }) l in let pm, proof = ComFixpoint.do_mutually_recursive ~program_mode ~use_inference_hook:program_mode - ~scope ?clearbody ~kind:(Decls.IsProof kind) ~poly ?typing_flags + ~scope ?opaque ?clearbody ~kind:(Decls.IsProof kind) ~poly ?typing_flags ?user_warns ?using (CUnknownRecOrder, fix) in assert (Option.is_empty pm); Option.get proof @@ -911,10 +912,12 @@ let vernac_exact_proof ~lemma ~pm c = let vernac_assumption ~atts kind l inline = let open DefAttributes in - let scope, poly, program_mode, using, user_warns = - atts.scope, atts.polymorphic, atts.program, atts.using, atts.user_warns in + let scope, poly, program_mode, using, user_warns, opaque = + atts.scope, atts.polymorphic, atts.program, atts.using, atts.user_warns, atts.opacity in if Option.has_some using then Attributes.unsupported_attributes [CAst.make ("using",VernacFlagEmpty)]; + if Option.has_some opaque then + Attributes.unsupported_attributes [CAst.make ("sealed",VernacFlagEmpty); CAst.make ("unsealed",VernacFlagEmpty)]; ComAssumption.do_assumptions ~poly ~program_mode ~scope ~kind ?user_warns ~inline l let { Goptions.get = is_polymorphic_inductive_cumulativity } = @@ -1245,15 +1248,15 @@ let with_obligations program_mode f pm = let vernac_fixpoint ~atts ~pm (rec_order,fixl) = let open DefAttributes in let scope = vernac_fixpoint_common ~atts fixl in - let poly, typing_flags, program_mode, clearbody, using, user_warns = - atts.polymorphic, atts.typing_flags, atts.program, atts.clearbody, atts.using, atts.user_warns in + let poly, typing_flags, program_mode, clearbody, using, user_warns, opaque = + atts.polymorphic, atts.typing_flags, atts.program, atts.clearbody, atts.using, atts.user_warns, atts.opacity in let () = if program_mode then (* XXX: Switch to the attribute system and match on ~atts *) let opens = List.exists (fun { body_def } -> Option.is_empty body_def) fixl in if opens then CErrors.user_err Pp.(str"Program Fixpoint requires a body.") in with_obligations program_mode - (fun pm -> ComFixpoint.do_mutually_recursive ?pm ~scope ?clearbody ~kind:(IsDefinition Fixpoint) ~poly ?typing_flags ?user_warns ?using (CFixRecOrder rec_order, fixl)) + (fun pm -> ComFixpoint.do_mutually_recursive ?pm ~scope ?opaque ?clearbody ~kind:(IsDefinition Fixpoint) ~poly ?typing_flags ?user_warns ?using (CFixRecOrder rec_order, fixl)) pm let vernac_cofixpoint_common ~atts l = @@ -1266,15 +1269,15 @@ let vernac_cofixpoint_common ~atts l = let vernac_cofixpoint ~pm ~atts cofixl = let open DefAttributes in let scope = vernac_cofixpoint_common ~atts cofixl in - let poly, typing_flags, program_mode, clearbody, using, user_warns = - atts.polymorphic, atts.typing_flags, atts.program, atts.clearbody, atts.using, atts.user_warns in + let poly, typing_flags, program_mode, clearbody, using, user_warns, opaque = + atts.polymorphic, atts.typing_flags, atts.program, atts.clearbody, atts.using, atts.user_warns, atts.opacity in let () = if program_mode then let opens = List.exists (fun { body_def } -> Option.is_empty body_def) cofixl in if opens then CErrors.user_err Pp.(str"Program CoFixpoint requires a body.") in with_obligations program_mode - (fun pm -> ComFixpoint.do_mutually_recursive ?pm ~scope ?clearbody ~kind:(IsDefinition CoFixpoint) ~poly ?typing_flags ?user_warns ?using (CCoFixRecOrder, cofixl)) + (fun pm -> ComFixpoint.do_mutually_recursive ?pm ~scope ?opaque ?clearbody ~kind:(IsDefinition CoFixpoint) ~poly ?typing_flags ?user_warns ?using (CCoFixRecOrder, cofixl)) pm let vernac_scheme l = @@ -1631,28 +1634,28 @@ let vernac_identity_coercion ~atts id qids qidt = let vernac_instance_program ~atts ~pm name bl t props info = Dumpglob.dump_constraint (fst name) false "inst"; - let locality, poly = - Attributes.(parse (Notations.(hint_locality ++ polymorphic))) atts + let (locality, poly), opaque = + Attributes.(parse (Notations.(hint_locality ++ polymorphic ++ opacity))) atts in - let pm, _id = Classes.new_instance_program ~pm ~locality ~poly name bl t props info in + let pm, _id = Classes.new_instance_program ~pm ~locality ~opaque ~poly name bl t props info in pm let vernac_instance_interactive ~atts name bl t info props = Dumpglob.dump_constraint (fst name) false "inst"; - let locality, poly = - Attributes.(parse (Notations.(hint_locality ++ polymorphic))) atts + let (locality, poly), opaque = + Attributes.(parse (Notations.(hint_locality ++ polymorphic ++ opacity))) atts in let _id, pstate = - Classes.new_instance_interactive ~locality ~poly name bl t info props in + Classes.new_instance_interactive ~locality ~opaque ~poly name bl t info props in pstate let vernac_instance ~atts name bl t props info = Dumpglob.dump_constraint (fst name) false "inst"; - let locality, poly = - Attributes.(parse (Notations.(hint_locality ++ polymorphic))) atts + let (locality, poly), opaque = + Attributes.(parse (Notations.(hint_locality ++ polymorphic ++ opacity))) atts in let _id : Id.t = - Classes.new_instance ~locality ~poly name bl t props info in + Classes.new_instance ~locality ~opaque ~poly name bl t props info in () let vernac_declare_instance ~atts id bl inst pri = diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index ccf578e0a7fb..a9e2e11d1a0c 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -85,6 +85,7 @@ type t = { using : Vernacexpr.section_subset_expr option; reversible : bool; clearbody: bool option; + opacity: bool option; } val def_attributes : t Attributes.attribute diff --git a/vernac/vernacexpr.mli b/vernac/vernacexpr.mli index c08980ad8288..0595978a11e6 100644 --- a/vernac/vernacexpr.mli +++ b/vernac/vernacexpr.mli @@ -192,6 +192,7 @@ type recursive_expr_gen = ; rtype : constr_expr ; body_def : constr_expr option ; notations : notation_declaration list + ; fix_attrs : Attributes.vernac_flags } type fixpoint_expr = fixpoint_order_expr option * recursive_expr_gen From 603a7f80a4e4b00d9612b499282e3a4d7b1ba07e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 1 Oct 2024 18:51:52 +0200 Subject: [PATCH 07/21] Using the word "sealed" in About. --- test-suite/output/PrintInfos.out | 2 +- vernac/prettyp.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index a99f17f8e9e0..3ae846cfcca6 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -47,7 +47,7 @@ plus_n_O : forall n : nat, n = n + 0 plus_n_O is not universe polymorphic Arguments plus_n_O n%nat_scope -plus_n_O is opaque +plus_n_O is sealed Expands to: Constant Stdlib.Init.Peano.plus_n_O Inductive le (n : nat) : nat -> Prop := le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m. diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 2a9ab4e31fee..153bd1eb0ded 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -172,7 +172,7 @@ let print_opacity env ref = | Some s -> [pr_global ref ++ str " is " ++ match s with - | FullyOpaque -> str "opaque" + | FullyOpaque -> str "sealed" | TransparentMaybeOpacified Conv_oracle.Opaque -> str "basically transparent but considered opaque for reduction" | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev -> From a21cd6a28cb59234c5838e12f6d321c548f90e65 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 2 Oct 2024 16:15:27 +0200 Subject: [PATCH 08/21] Documenting attributes sealed and defined. Co-Authored-By: Jim Fehrle Co-Authored-By: Zimmi48 --- doc/sphinx/language/core/conversion.rst | 7 +++++-- doc/sphinx/language/core/definitions.rst | 25 +++++++++++++++++++++--- doc/sphinx/language/core/inductive.rst | 3 ++- 3 files changed, 29 insertions(+), 6 deletions(-) diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst index 71d857526e30..fbd66e66c27c 100644 --- a/doc/sphinx/language/core/conversion.rst +++ b/doc/sphinx/language/core/conversion.rst @@ -142,8 +142,11 @@ or :term:`constants ` defined in the :term:`global environment` with t E[Γ] ⊢ c~\triangleright_δ~t :term:`Delta-reduction ` only unfolds :term:`constants ` that are -marked :gdef:`transparent`. :gdef:`Opaque ` is the opposite of -transparent; :term:`delta-reduction` doesn't unfold opaque constants. +marked :gdef:`transparent`. A constant that is not transparent is +either :gdef:`sealed`, meaning that it is never unfolded, or +:gdef:`opaque` meaning that it is transparent for the purpose +of validating the correctness of proofs and types but non-unfoldable +for the purpose of tactics and unification. ι-reduction ~~~~~~~~~~~ diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index de25bdb7cf4c..7d6b3057cfde 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -125,7 +125,8 @@ Section :ref:`typing-rules`. The attributes :attr:`local`, :attr:`universes(polymorphic)`, :attr:`program` (see :ref:`program_definition`), :attr:`canonical`, :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, :attr:`deprecated`, - :attr:`warn` and :attr:`using` are accepted. + :attr:`warn` and :attr:`using`, as well as the exclusive attributes :attr:`sealed` and + :attr:`defined` are accepted. .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. @@ -212,11 +213,13 @@ commands to manage the proof mode (see :ref:`proofhandling`). When the proof is complete, use the :cmd:`Qed` command so the kernel verifies the proof and adds it to the global environment. By default, proofs -that end with :cmd:`Qed` are :term:`opaque`, that is that their content cannot +that end with :cmd:`Qed` are sealed, that is that their content cannot be unfolded (see :ref:`applyingconversionrules`), thus realizing *proof irrelevance*, that is that only provability matters, and not the exact proof. Proofs can be made unfoldable, as -definitions are, by ending the proof with :cmd:`Defined` in place of :cmd:`Qed`. +definitions are, with the :attr:`defined` attribute or by ending +the proof with :cmd:`Defined` in place of :cmd:`Qed`. We +recommend using the attribute. .. note:: @@ -234,3 +237,19 @@ definitions are, by ending the proof with :cmd:`Defined` in place of :cmd:`Qed`. #. One can also use :cmd:`Admitted` in place of :cmd:`Qed` to turn the current asserted statement into an axiom and exit proof mode. + +Sealing and transparency +------------------------ + +By default, definitions are unfoldable while the proofs of theorems are +not. You can change this using these attributes: + +.. attr:: sealed + + Prevents the unfoldability of the definition, so it behaves like an abstract definition. + +.. attr:: defined + + Makes the proof of a theorem unfoldable, as if it were a definition. + + .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index f174a1f89516..da459ec4142c 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -486,7 +486,8 @@ constructions. This command accepts the :attr:`local`, :attr:`universes(polymorphic)`, :attr:`program`, :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, :attr:`deprecated`, - :attr:`warn` and :attr:`using` attributes. The :attr:`program` attribute is needed + :attr:`warn` and :attr:`using` attributes, as well as the exclusive attributes :attr:`sealed` + and :attr:`defined`. The :attr:`program` attribute is needed so that the :n:`wf` or :n:`measure` clauses of :n:`@fixannot` are supported. See :ref:`program_fixpoint`. From aaa4c5a5933e1d66181089eb66ed814f9873978b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 2 Oct 2024 16:14:55 +0200 Subject: [PATCH 09/21] Assigning kind Theorem rather than Definition to Goal. --- vernac/vernacentries.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 111636aaf08b..aa15997d787f 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -841,8 +841,9 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, udecl) bl t = let canonical_instance, reversible = atts.canonical_instance, atts.reversible in let hook = vernac_definition_hook ~canonical_instance ~local ~poly ~reversible kind in let name = vernac_definition_name lid scope in + let kind = Decls.(match lid.v with Anonymous -> (* Goal *) IsProof Theorem | _ -> IsDefinition kind) in ComDefinition.do_definition_interactive ~typing_flags ~program_mode ~name ~poly ~scope ~opaque ?clearbody:atts.clearbody - ~kind:(Decls.IsDefinition kind) ?user_warns ?using:atts.using ?hook udecl bl t + ~kind ?user_warns ?using:atts.using ?hook udecl bl t let vernac_definition ~atts ~pm (discharge, kind) (lid, udecl) bl red_option c typ_opt = let open DefAttributes in From d2411ee6a52de66744d89d07f7c21b43638e2e3b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 2 Oct 2024 02:35:16 +0200 Subject: [PATCH 10/21] Using Lemma instead of Definition for opaque structures. --- theories/QArith/Qcanon.v | 4 ++-- theories/QArith/Qfield.v | 4 ++-- theories/Setoids/Setoid.v | 2 +- theories/micromega/RMicromega.v | 2 +- theories/setoid_ring/Ring_theory.v | 2 +- 5 files changed, 7 insertions(+), 7 deletions(-) diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 78712a7845b5..05afc3bbe04e 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -510,7 +510,7 @@ Proof. intros _ H; inversion H. Qed. -Definition Qcrt : ring_theory 0 1 Qcplus Qcmult Qcminus Qcopp (eq(A:=Qc)). +Lemma Qcrt : ring_theory 0 1 Qcplus Qcmult Qcminus Qcopp (eq(A:=Qc)). Proof. constructor. - exact Qcplus_0_l. @@ -524,7 +524,7 @@ Proof. - exact Qcplus_opp_r. Qed. -Definition Qcft : +Lemma Qcft : field_theory 0%Qc 1%Qc Qcplus Qcmult Qcminus Qcopp Qcdiv Qcinv (eq(A:=Qc)). Proof. constructor. diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v index f438d3ae3f7a..3dfd8d71673b 100644 --- a/theories/QArith/Qfield.v +++ b/theories/QArith/Qfield.v @@ -14,7 +14,7 @@ Require Import NArithRing. (** * field and ring tactics for rational numbers *) -Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq. +Lemma Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq. Proof. constructor. - exact Qplus_0_l. @@ -28,7 +28,7 @@ Proof. - exact Qplus_opp_r. Qed. -Definition Qsft : field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq. +Lemma Qsft : field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq. Proof. constructor. - exact Qsrt. diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index 4d2d7662e71f..d49ac80c328b 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -63,7 +63,7 @@ Ltac refl_st := apply (Seq_refl _ _ H); auto end. -Definition gen_st : forall A : Set, Setoid_Theory _ (@eq A). +Lemma gen_st : forall A : Set, Setoid_Theory _ (@eq A). Proof. constructor; congruence. Qed. diff --git a/theories/micromega/RMicromega.v b/theories/micromega/RMicromega.v index a432aeb79288..906a1aff388e 100644 --- a/theories/micromega/RMicromega.v +++ b/theories/micromega/RMicromega.v @@ -25,7 +25,7 @@ Require Import DeclConstant. Require Setoid. -Definition Rsrt : ring_theory R0 R1 Rplus Rmult Rminus Ropp (@eq R). +Lemma Rsrt : ring_theory R0 R1 Rplus Rmult Rminus Ropp (@eq R). Proof. constructor. - exact Rplus_0_l. diff --git a/theories/setoid_ring/Ring_theory.v b/theories/setoid_ring/Ring_theory.v index 9ca9341a7e1e..975067c0f55c 100644 --- a/theories/setoid_ring/Ring_theory.v +++ b/theories/setoid_ring/Ring_theory.v @@ -302,7 +302,7 @@ Section ALMOST_RING. Hypothesis morph_req : forall x y, (reqb x y) = true -> x == y. - Definition SRIDmorph : ring_morph 0 1 radd rmul SRsub SRopp req + Lemma SRIDmorph : ring_morph 0 1 radd rmul SRsub SRopp req 0 1 radd rmul SRsub SRopp reqb (@IDphi R). Proof. now apply mkmorph. From aa4cada322fc9e0fbdc9f6c83c7d0989ece736e5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 2 Oct 2024 02:27:03 +0200 Subject: [PATCH 11/21] Using #[sealed] for opaque proofs of Compare. --- theories/FSets/FMapList.v | 3 ++- theories/Structures/OrderedTypeEx.v | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index 1f40c09e0654..ed9562f45021 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -1278,6 +1278,7 @@ Qed. Ltac cmp_solve := unfold eq, lt; simpl; try Raw.MX.elim_comp; auto with ordered_type. +#[sealed] Definition compare : forall m1 m2, Compare lt eq m1 m2. Proof. intros (m1,Hm1); induction m1; @@ -1294,6 +1295,6 @@ Proof. { inversion_clear Hm2; auto. } destruct (IHm1 Hm11 (Build_slist Hm22)); [ apply LT | apply EQ | apply GT ]; cmp_solve. -Qed. +Defined. End Make_ord. diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index 228f62b068c8..b332eac8e2cf 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -277,6 +277,7 @@ Module PositiveOrderedTypeBits <: UsualOrderedType. exact (bits_lt_antirefl x H). Qed. + #[sealed] Definition compare : forall x y : t, Compare lt eq x y. Proof. induction x; destruct y. @@ -304,7 +305,7 @@ Module PositiveOrderedTypeBits <: UsualOrderedType. apply GT; simpl; auto. + (* H H *) apply EQ; red; auto. - Qed. + Defined. Lemma eq_dec (x y: positive): {x = y} + {x <> y}. Proof. From 3cebc642db461e503b0522d6d44dd2cbae81a470 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 2 Oct 2024 02:27:40 +0200 Subject: [PATCH 12/21] Using #[sealed] for opaque instances. --- theories/Classes/CRelationClasses.v | 5 ++++- theories/Classes/RelationClasses.v | 4 ++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index b5c927dd310b..efbbc3bf035e 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -82,6 +82,7 @@ Section Defs. #[global] StrictOrder_Transitive :: Transitive R }. (** By definition, a strict order is also asymmetric *) + #[sealed] Global Instance StrictOrder_Asymmetric `(StrictOrder R) : Asymmetric R. Proof. firstorder. Qed. @@ -348,7 +349,8 @@ Section Binary. - firstorder. - intros x y z X X0 x0 y0. specialize (X x0 y0). specialize (X0 x0 y0). firstorder. Qed. - + + #[sealed] Global Instance relation_implication_preorder : PreOrder (@subrelation A). Proof. firstorder. Qed. @@ -364,6 +366,7 @@ Section Binary. morphism for equivalence (see Morphisms). It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *) + #[sealed] Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric eqA R. Proof with auto. reduce_goal. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index e46f9a14778c..1adc2ad2a6f6 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -70,6 +70,7 @@ Section Defs. #[global] StrictOrder_Transitive :: Transitive R }. (** By definition, a strict order is also asymmetric *) + #[sealed] Global Instance StrictOrder_Asymmetric `(StrictOrder R) : Asymmetric R. Proof. firstorder. Qed. @@ -481,10 +482,12 @@ Section Binary. (** Relation equivalence is an equivalence, and subrelation defines a partial order. *) + #[sealed] Global Instance relation_equivalence_equivalence : Equivalence relation_equivalence. Proof. exact (@predicate_equivalence_equivalence (A::A::Tnil)). Qed. + #[sealed] Global Instance relation_implication_preorder : PreOrder (@subrelation A). Proof. exact (@predicate_implication_preorder (A::A::Tnil)). Qed. @@ -500,6 +503,7 @@ Section Binary. morphism for equivalence (see Morphisms). It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *) + #[sealed] Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric A eqA R. Proof with auto. reduce_goal. From 3d16d75d0397273d931d08f29fc9e330484468e7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 2 Oct 2024 02:28:19 +0200 Subject: [PATCH 13/21] Using #[sealed] for opaque morally-relevant definitions. --- theories/FSets/FSetBridge.v | 60 ++++++++++++------- theories/Reals/Abstract/ConstructiveLUB.v | 2 +- theories/Reals/Abstract/ConstructiveReals.v | 6 +- .../Abstract/ConstructiveRealsMorphisms.v | 3 +- theories/Reals/Abstract/ConstructiveSum.v | 3 +- .../Cauchy/ConstructiveCauchyRealsMult.v | 6 +- theories/Reals/Cauchy/ConstructiveRcomplete.v | 3 +- theories/Reals/ClassicalDedekindReals.v | 8 ++- theories/Reals/PSeries_reg.v | 6 +- theories/Reals/Ranalysis_reg.v | 1 + theories/Reals/Ratan.v | 12 ++-- theories/Reals/Rtrigo1.v | 3 +- theories/Strings/PString.v | 3 +- 13 files changed, 77 insertions(+), 39 deletions(-) diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index cb228580f619..47a6bf735cd8 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -23,27 +23,31 @@ Set Firstorder Depth 2. Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. Local Ltac Tauto.intuition_solver ::= auto with bool set. + #[sealed] Definition empty : {s : t | Empty s}. Proof. exists empty; auto with set. - Qed. + Defined. + #[sealed] Definition is_empty : forall s : t, {Empty s} + {~ Empty s}. Proof. intros; generalize (is_empty_1 (s:=s)) (is_empty_2 (s:=s)). case (is_empty s); intuition. - Qed. + Defined. + #[sealed] Definition mem : forall (x : elt) (s : t), {In x s} + {~ In x s}. Proof. intros; generalize (mem_1 (s:=s) (x:=x)) (mem_2 (s:=s) (x:=x)). case (mem x s); intuition. - Qed. + Defined. Definition Add (x : elt) (s s' : t) := forall y : elt, In y s' <-> E.eq x y \/ In y s. + #[sealed] Definition add : forall (x : elt) (s : t), {s' : t | Add x s s'}. Proof. intros; exists (add x s); auto. @@ -51,14 +55,16 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. elim (E.eq_dec x y); auto. intros; right. eapply add_3; eauto. - Qed. + Defined. + #[sealed] Definition singleton : forall x : elt, {s : t | forall y : elt, In y s <-> E.eq x y}. Proof. intros; exists (singleton x); intuition. - Qed. + Defined. + #[sealed] Definition remove : forall (x : elt) (s : t), {s' : t | forall y : elt, In y s' <-> ~ E.eq x y /\ In y s}. @@ -70,40 +76,45 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. + absurd (In x (remove x s)); auto with set ordered_type. apply In_1 with y; auto with ordered_type. + eauto with set. - Qed. + Defined. + #[sealed] Definition union : forall s s' : t, {s'' : t | forall x : elt, In x s'' <-> In x s \/ In x s'}. Proof. intros; exists (union s s'); intuition. - Qed. + Defined. + #[sealed] Definition inter : forall s s' : t, {s'' : t | forall x : elt, In x s'' <-> In x s /\ In x s'}. Proof. intros; exists (inter s s'); intuition; eauto with set. - Qed. + Defined. + #[sealed] Definition diff : forall s s' : t, {s'' : t | forall x : elt, In x s'' <-> In x s /\ ~ In x s'}. Proof. intros; exists (diff s s'); intuition; eauto with set. absurd (In x s'); eauto with set. - Qed. + Defined. + #[sealed] Definition equal : forall s s' : t, {Equal s s'} + {~ Equal s s'}. Proof. intros. generalize (equal_1 (s:=s) (s':=s')) (equal_2 (s:=s) (s':=s')). case (equal s s'); intuition. - Qed. + Defined. + #[sealed] Definition subset : forall s s' : t, {Subset s s'} + {~Subset s s'}. Proof. intros. generalize (subset_1 (s:=s) (s':=s')) (subset_2 (s:=s) (s':=s')). case (subset s s'); intuition. - Qed. + Defined. Definition elements : forall s : t, @@ -112,20 +123,22 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. intros; exists (elements s); intuition. Defined. + #[sealed] Definition fold : forall (A : Type) (f : elt -> A -> A) (s : t) (i : A), {r : A | let (l,_) := elements s in r = fold_left (fun a e => f e a) l i}. Proof. intros; exists (fold (A:=A) f s i); exact (fold_1 s i f). - Qed. + Defined. + #[sealed] Definition cardinal : forall s : t, {r : nat | let (l,_) := elements s in r = length l }. Proof. intros; exists (cardinal s); exact (cardinal_1 s). - Qed. + Defined. Definition fdec (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}) (x : elt) := if Pdec x then true else false. @@ -141,6 +154,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. #[global] Hint Resolve compat_P_aux : core. + #[sealed] Definition filter : forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}) (s : t), {s' : t | compat_P E.eq P -> forall x : elt, In x s' <-> In x s /\ P x}. @@ -157,8 +171,9 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. - apply filter_3; auto. unfold fdec; simpl. case (Pdec x); intuition. - Qed. + Defined. + #[sealed] Definition for_all : forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}) (s : t), {compat_P E.eq P -> For_all P s} + {compat_P E.eq P -> ~ For_all P s}. @@ -178,8 +193,9 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. intro. unfold fdec. case (Pdec x); intuition. - Qed. + Defined. + #[sealed] Definition exists_ : forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}) (s : t), {compat_P E.eq P -> Exists P s} + {compat_P E.eq P -> ~ Exists P s}. @@ -201,8 +217,9 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. exists x; intuition. unfold fdec. case (Pdec x); intuition. - Qed. + Defined. + #[sealed] Definition partition : forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}) (s : t), {partition : t * t | @@ -245,15 +262,16 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. - eapply (filter_1 (s:=s) (x:=x) H2); elim (H4 x); intros B _; apply B; auto. - eapply (filter_1 (s:=s) (x:=x) H3); elim (H x); intros B _; apply B; auto. - Qed. + Defined. + #[sealed] Definition choose_aux: forall s : t, { x : elt | M.choose s = Some x } + { M.choose s = None }. Proof. intros. destruct (M.choose s); [left | right]; auto. exists e; auto. - Qed. + Defined. Definition choose : forall s : t, {x : elt | In x s} + {Empty s}. Proof. @@ -306,6 +324,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. - apply Hx with x'; unfold Equal in H; rewrite H; auto. Qed. + #[sealed] Definition min_elt : forall s : t, {x : elt | In x s /\ For_all (fun y => ~ E.lt y x) s} + {Empty s}. @@ -314,8 +333,9 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. generalize (min_elt_1 (s:=s)) (min_elt_2 (s:=s)) (min_elt_3 (s:=s)). case (min_elt s); [ left | right ]; auto. exists e; unfold For_all; eauto. - Qed. + Defined. + #[sealed] Definition max_elt : forall s : t, {x : elt | In x s /\ For_all (fun y => ~ E.lt x y) s} + {Empty s}. @@ -324,7 +344,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. generalize (max_elt_1 (s:=s)) (max_elt_2 (s:=s)) (max_elt_3 (s:=s)). case (max_elt s); [ left | right ]; auto. exists e; unfold For_all; eauto. - Qed. + Defined. Definition elt := elt. Definition t := t. diff --git a/theories/Reals/Abstract/ConstructiveLUB.v b/theories/Reals/Abstract/ConstructiveLUB.v index 0d8597e27524..48ea2ed6a47a 100644 --- a/theories/Reals/Abstract/ConstructiveLUB.v +++ b/theories/Reals/Abstract/ConstructiveLUB.v @@ -204,7 +204,7 @@ Proof. + exact H. Qed. -Fixpoint DDcut_limit_fix (upcut : DedekindDecCut) (r : Q) (n : nat) : +Fixpoint #[sealed] DDcut_limit_fix (upcut : DedekindDecCut) (r : Q) (n : nat) : Qlt 0 r -> (DDupcut upcut (DDlow upcut + (Z.of_nat n#1) * r)) -> { q : Q | DDupcut upcut q /\ ~DDupcut upcut (q - r) }. diff --git a/theories/Reals/Abstract/ConstructiveReals.v b/theories/Reals/Abstract/ConstructiveReals.v index 839cfbc02ba0..bfb957cb14f7 100644 --- a/theories/Reals/Abstract/ConstructiveReals.v +++ b/theories/Reals/Abstract/ConstructiveReals.v @@ -1152,13 +1152,15 @@ Proof. - exact H. Qed. +#[sealed] Definition CRup_nat {R : ConstructiveReals} (x : CRcarrier R) : { n : nat & x < CR_of_Q R (Z.of_nat n #1) }. Proof. destruct (CR_archimedean R x). exists (Pos.to_nat x0). rewrite positive_nat_Z. exact c. -Qed. +Defined. +#[sealed] Definition CRfloor {R : ConstructiveReals} (a : CRcarrier R) : { p : Z & prod (CR_of_Q R (p#1) < a) (a < CR_of_Q R (p#1) + CR_of_Q R 2) }. @@ -1180,7 +1182,7 @@ Proof. -- apply CR_of_Q_le. rewrite Qinv_plus_distr. apply Qlt_le_weak, Qlt_floor. -- apply CR_of_Q_le. discriminate. -Qed. +Defined. Lemma CRplus_appart_reg_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R), (r + r1) ≶ (r + r2) -> r1 ≶ r2. diff --git a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v index e1521aa6e7de..dc14ae5e6263 100644 --- a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v +++ b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v @@ -984,6 +984,7 @@ Proof. - rewrite q. apply Qle_refl. Qed. +#[sealed] Definition CR_Q_limit {R : ConstructiveReals} (x : CRcarrier R) (n:nat) : { q:Q & x < CR_of_Q R q < x + CR_of_Q R (1 # Pos.of_nat n) }. Proof. @@ -991,7 +992,7 @@ Proof. rewrite <- (CRplus_0_r x). rewrite CRplus_assoc. apply CRplus_lt_compat_l. rewrite CRplus_0_l. apply CR_of_Q_pos. reflexivity. -Qed. +Defined. Lemma CR_Q_limit_cv : forall {R : ConstructiveReals} (x : CRcarrier R), CR_cv R (fun n => CR_of_Q R (let (q,_) := CR_Q_limit x n in q)) x. diff --git a/theories/Reals/Abstract/ConstructiveSum.v b/theories/Reals/Abstract/ConstructiveSum.v index 41e9403d72bd..73ce26c40e82 100644 --- a/theories/Reals/Abstract/ConstructiveSum.v +++ b/theories/Reals/Abstract/ConstructiveSum.v @@ -400,6 +400,7 @@ Proof. + apply H1. Qed. +#[sealed] Definition series_cv_abs {R : ConstructiveReals} (u : nat -> CRcarrier R) : CR_cauchy R (CRsum (fun n => CRabs R (u n))) -> { l : CRcarrier R & series_cv u l }. @@ -409,7 +410,7 @@ Proof. - intro n. apply CRle_refl. - assumption. - exists x0. apply p. -Qed. +Defined. Lemma series_cv_unique : forall {R : ConstructiveReals} (Un:nat -> CRcarrier R) (l1 l2:CRcarrier R), diff --git a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v index 7b4462d4cdb0..37782e15ba77 100644 --- a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v +++ b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v @@ -996,6 +996,7 @@ Proof. pose proof Qpower_pos 2 n ltac:(lra). rewrite Z.abs_0, Qreduce_zero. lra. Qed. +#[sealed] Definition CRealQ_dense (a b : CReal) : a < b -> { q : Q & a < inject_Q q < b }. Proof. @@ -1016,7 +1017,7 @@ Proof. destruct b as [bseq]; simpl in pmaj |- *. unfold CReal_opp_seq; rewrite CReal_red_seq. lra. -Qed. +Defined. Lemma inject_Q_mult : forall q r : Q, inject_Q (q * r) == inject_Q q * inject_Q r. @@ -1030,6 +1031,7 @@ Proof. pose proof Qpower_0_lt 2 n; lra. Qed. +#[sealed] Definition Rup_nat (x : CReal) : { n : nat & x < inject_Q (Z.of_nat n #1) }. Proof. @@ -1040,7 +1042,7 @@ Proof. - exists O. apply (CReal_lt_trans _ (inject_Q (Z.neg p # 1))). + apply maj. + apply inject_Q_lt. reflexivity. -Qed. +Defined. Lemma CReal_mult_le_0_compat : forall (a b : CReal), 0 <= a -> 0 <= b -> 0 <= a * b. diff --git a/theories/Reals/Cauchy/ConstructiveRcomplete.v b/theories/Reals/Cauchy/ConstructiveRcomplete.v index 87e710ac3cc9..97f580646e78 100644 --- a/theories/Reals/Cauchy/ConstructiveRcomplete.v +++ b/theories/Reals/Cauchy/ConstructiveRcomplete.v @@ -67,6 +67,7 @@ Qed. (* Sharpen the archimedean property : constructive versions of the usual floor and ceiling functions. *) +#[sealed] Definition Rfloor (a : CReal) : { p : Z & inject_Q (p#1) < a < inject_Q (p#1) + 2 }. Proof. @@ -81,7 +82,7 @@ Proof. + rewrite inject_Q_plus, (opp_inject_Q 2). ring_simplify. exact H. + rewrite Qinv_plus_distr. reflexivity. -Qed. +Defined. (* ToDo: Move to ConstructiveCauchyAbs.v *) Lemma Qabs_Rabs : forall q : Q, diff --git a/theories/Reals/ClassicalDedekindReals.v b/theories/Reals/ClassicalDedekindReals.v index b0b36f6a2c71..843a56eeb4be 100644 --- a/theories/Reals/ClassicalDedekindReals.v +++ b/theories/Reals/ClassicalDedekindReals.v @@ -215,7 +215,7 @@ Definition DReal : Set (** ** Induction principle *) -Fixpoint DRealQlim_rec (f : Q -> bool) (low : isLowerCut f) (n p : nat) { struct p } +Fixpoint #[sealed] DRealQlim_rec (f : Q -> bool) (low : isLowerCut f) (n p : nat) { struct p } : f (proj1_sig (lowerCutBelow f low) + (Z.of_nat p # Pos.of_nat (S n)))%Q = false -> { q : Q | f q = true /\ f (q + (1 # Pos.of_nat (S n)))%Q = false }. Proof. @@ -345,6 +345,7 @@ Defined. (** *** Conversion from DReal to CReal *) +#[sealed] Definition DRealQlim (x : DReal) (n : nat) : { q : Q | proj1_sig x q = true /\ proj1_sig x (q + (1# Pos.of_nat (S n)))%Q = false }. Proof. @@ -369,8 +370,9 @@ Proof. -- apply f_equal. apply Pos.succ_of_nat. discriminate. - exact des. -Qed. +Defined. +#[sealed] Definition DRealQlimExp2 (x : DReal) (n : nat) : { q : Q | proj1_sig x q = true /\ proj1_sig x (q + (1#(Pos.of_nat (2^n)%nat)))%Q = false }. Proof. @@ -379,7 +381,7 @@ Proof. rewrite Nat.succ_pred_pos in qmaj. 2: apply Nat.neq_0_lt_0, Nat.pow_nonzero; intros contra; inversion contra. exact qmaj. -Qed. +Defined. Definition CReal_of_DReal_seq (x : DReal) (n : Z) := proj1_sig (DRealQlimExp2 x (Z.to_nat (-n))). diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v index 040804ee5ca1..1557fc6dc208 100644 --- a/theories/Reals/PSeries_reg.v +++ b/theories/Reals/PSeries_reg.v @@ -32,6 +32,7 @@ apply Rabs_def2 in b_y; apply Rabs_def1; apply Rlt_le_trans with (x - c);[|apply Rplus_le_compat_r]];tauto. Qed. +#[sealed] Definition boule_of_interval x y (h : x < y) : {c :R & {r : posreal | c - r = x /\ c + r = y}}. Proof. @@ -42,8 +43,9 @@ assert (radius : 0 < (y - x)/2). + now apply Rinv_0_lt_compat, Rlt_0_2. - exists (mkposreal _ radius). simpl; split; unfold Rdiv; field. -Qed. +Defined. +#[sealed] Definition boule_in_interval x y z (h : x < z < y) : {c : R & {r | Boule c r z /\ x < c - r /\ c + r < y}}. Proof. @@ -69,7 +71,7 @@ exists c, r; split. apply Rplus_lt_compat_l, Rmult_lt_compat_r;assumption. + replace y with (y * / 2 + y * /2) by field; rewrite P2. apply Rplus_lt_compat_r, Rmult_lt_compat_r;assumption. -Qed. +Defined. Lemma Ball_in_inter : forall c1 c2 r1 r2 x, Boule c1 r1 x -> Boule c2 r2 x -> diff --git a/theories/Reals/Ranalysis_reg.v b/theories/Reals/Ranalysis_reg.v index 7e01efaebb66..5d37f7930c0c 100644 --- a/theories/Reals/Ranalysis_reg.v +++ b/theories/Reals/Ranalysis_reg.v @@ -29,6 +29,7 @@ Require Export Ranalysis4. Require Export Rpower. Local Open Scope R_scope. +#[sealed] Definition AppVar : R. Proof. exact R0. diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v index f65f7934a777..f4e19dbafbce 100644 --- a/theories/Reals/Ratan.v +++ b/theories/Reals/Ratan.v @@ -451,6 +451,7 @@ Proof. lra. Qed. +#[sealed] Definition frame_tan y : {x | 0 < x < PI/2 /\ Rabs y < tan x}. Proof. destruct (total_order_T (Rabs y) 1) as [Hs|Hgt]. @@ -519,7 +520,7 @@ apply Rlt_trans with (/2 * / cos(PI / 2 - u)). + assert (t := PI2_1); lra. + lra. + assumption. -Qed. +Defined. Lemma ub_opp : forall x, x < PI/2 -> -PI/2 < -x. Proof. @@ -534,6 +535,7 @@ Proof. intros; rewrite tan_neg; assumption. Qed. +#[sealed] Definition pre_atan (y : R) : {x : R | -PI/2 < x < PI/2 /\ tan x = y}. Proof. destruct (frame_tan y) as [ub [[ub0 ubpi2] Ptan_ub]]. @@ -543,7 +545,7 @@ destruct (exists_atan_in_frame (-ub) ub y (pos_opp_lt _ ub0) (ub_opp _ ubpi2) ubpi2 pr) as [v [[vl vu] vq]]. exists v; clear pr. split;[rewrite Rdiv_opp_l; split; lra | assumption]. -Qed. +Defined. Definition atan x := let (v, _) := pre_atan x in v. @@ -910,6 +912,7 @@ rewrite scal_sum; apply sum_eq; intros i _; unfold tg_alt. rewrite Ratan_seq_opp; ring. Qed. +#[sealed] Definition ps_atan_exists_1 (x : R) (Hx : -1 <= x <= 1) : {l : R | Un_cv (fun N : nat => sum_f_R0 (tg_alt (Ratan_seq x)) N) l}. Proof. @@ -924,8 +927,9 @@ apply (Un_cv_ext (fun n => (- 1) * sum_f_R0 (tg_alt (Ratan_seq (- x))) n)). replace (-v) with (-1 * v) by ring. apply CV_mult;[ | assumption]. solve[intros; exists 0%nat; intros; rewrite Rdist_eq; auto]. -Qed. +Defined. +#[sealed] Definition in_int (x : R) : {-1 <= x <= 1}+{~ -1 <= x <= 1}. Proof. destruct (Rle_lt_dec x 1). @@ -933,7 +937,7 @@ destruct (Rle_lt_dec x 1). - left;split; auto. - right;intros [a1 a2]; lra. - right;intros [a1 a2]; lra. -Qed. +Defined. Definition ps_atan (x : R) : R := match in_int x with diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v index dd04ff2dc4f4..2ad1a0e33814 100644 --- a/theories/Reals/Rtrigo1.v +++ b/theories/Reals/Rtrigo1.v @@ -191,6 +191,7 @@ rewrite <- !mult_IZR. apply IZR_lt; reflexivity. Qed. +#[sealed] Definition PI_2_aux : {z | 7/8 <= z <= 7/4 /\ -cos z = 0}. assert (cc : continuity (fun r =>- cos r)). { apply continuity_opp, continuity_cos. @@ -212,7 +213,7 @@ assert (cun : cos (7/4) < 0). { - apply Rlt_le; apply Rlt_trans with (1 := cvp); exact sin_gt_cos_7_8. } apply IVT; auto; lra. -Qed. +Defined. Definition PI2 := proj1_sig PI_2_aux. diff --git a/theories/Strings/PString.v b/theories/Strings/PString.v index 9d779b2eec3c..37821a3fea2f 100644 --- a/theories/Strings/PString.v +++ b/theories/Strings/PString.v @@ -648,6 +648,7 @@ Module OT <: OrderedType.OrderedType with Definition t := string. Hint Immediate eq_sym : core. Hint Resolve eq_refl eq_trans lt_not_eq lt_trans : core. + #[sealed] Definition eq_dec (s1 s2 : t) : {eq s1 s2} + {~ eq s1 s2}. Proof. unfold eq. @@ -655,5 +656,5 @@ Module OT <: OrderedType.OrderedType with Definition t := string. - left. reflexivity. - right. discriminate. - right. discriminate. - Qed. + Defined. End OT. From a35abec292a2c19684354eeb23d2f97483413742 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 2 Oct 2024 16:24:22 +0200 Subject: [PATCH 14/21] Using #[sealed] for opaque morally-relevant definitions in test-suite. --- test-suite/output/SuggestProofUsing.v | 1 + test-suite/output/bug_11608.v | 1 + 2 files changed, 2 insertions(+) diff --git a/test-suite/output/SuggestProofUsing.v b/test-suite/output/SuggestProofUsing.v index 449cf38039bf..8a1e714a1f23 100644 --- a/test-suite/output/SuggestProofUsing.v +++ b/test-suite/output/SuggestProofUsing.v @@ -30,6 +30,7 @@ Section Sec. Qed. (* Having a [Proof using] disables the suggestion message. *) + #[sealed] Definition bar : Type. Proof using A. exact A. diff --git a/test-suite/output/bug_11608.v b/test-suite/output/bug_11608.v index 39290829137e..b58d66c700ab 100644 --- a/test-suite/output/bug_11608.v +++ b/test-suite/output/bug_11608.v @@ -4,6 +4,7 @@ Set Default Proof Using "Type". Section foo. Context (A:Type). + #[sealed] Definition x : option A. (* this can get printed with -vos since without "Proof." there's no Proof using, even with a default annotation. *) From b4ae67e11eb8bdac884eb3b59577a497de77b6d5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 2 Oct 2024 02:31:04 +0200 Subject: [PATCH 15/21] Using #[sealed] for opaque fixpoints. --- theories/Strings/BinaryString.v | 2 +- theories/Strings/HexString.v | 2 +- theories/Strings/OctalString.v | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/Strings/BinaryString.v b/theories/Strings/BinaryString.v index 94fb82216bee..0ca23dad0f64 100644 --- a/theories/Strings/BinaryString.v +++ b/theories/Strings/BinaryString.v @@ -50,7 +50,7 @@ Module Raw. end end. - Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) {struct p} + Fixpoint #[sealed] to_N_of_pos (p : positive) (rest : string) (base : N) {struct p} : to_N (of_pos p rest) base = to_N rest match base with | N0 => N.pos p diff --git a/theories/Strings/HexString.v b/theories/Strings/HexString.v index 4dbab23d58cf..e0a4625d0c92 100644 --- a/theories/Strings/HexString.v +++ b/theories/Strings/HexString.v @@ -122,7 +122,7 @@ Module Raw. end end. - Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) {struct p} + Fixpoint #[sealed] to_N_of_pos (p : positive) (rest : string) (base : N) {struct p} : to_N (of_pos p rest) base = to_N rest match base with | N0 => N.pos p diff --git a/theories/Strings/OctalString.v b/theories/Strings/OctalString.v index 9118555f8817..032ecd44e815 100644 --- a/theories/Strings/OctalString.v +++ b/theories/Strings/OctalString.v @@ -80,7 +80,7 @@ Module Raw. end end. - Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) {struct p} + Fixpoint #[sealed] to_N_of_pos (p : positive) (rest : string) (base : N) {struct p} : to_N (of_pos p rest) base = to_N rest match base with | N0 => N.pos p From 2dda69422628af448fef8ab60216865b33ca9b4d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 2 Oct 2024 02:31:37 +0200 Subject: [PATCH 16/21] Using #[sealed] for opaque Example. --- theories/Logic/ClassicalFacts.v | 1 + theories/QArith/Qcanon.v | 1 + theories/Sorting/CPermutation.v | 1 + 3 files changed, 3 insertions(+) diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 9c27ebb8ab45..bbe8dde9458b 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -826,6 +826,7 @@ Section Example_of_undecidable_predicate_with_the_minimization_property. Let P n := exists k, n<=k /\ s k = true. + #[sealed] Example undecidable_predicate_with_the_minimization_property : Minimization_Property P. Proof. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 05afc3bbe04e..92633db8af62 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -538,6 +538,7 @@ Add Field Qcfield : Qcft. (** A field tactic for rational numbers *) +#[sealed] Example test_field : (forall x y : Qc, y<>0 -> (x/y)*y = x)%Qc. Proof. intros. diff --git a/theories/Sorting/CPermutation.v b/theories/Sorting/CPermutation.v index 710ad7dc6730..9fc8cf284fbb 100644 --- a/theories/Sorting/CPermutation.v +++ b/theories/Sorting/CPermutation.v @@ -282,6 +282,7 @@ Qed. (** As an equivalence relation compatible with some operations, [CPermutation] can be used through [rewrite]. *) +#[sealed] Example CPermutation_rewrite_rev A (l1 l2 l3: list A) : CPermutation l1 l2 -> CPermutation (rev l1) l3 -> CPermutation l3 (rev l2). From 99f69d641306cc0f972ddfc8219d6658d183d9f7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 2 Oct 2024 02:14:33 +0200 Subject: [PATCH 17/21] Take Theorem/Definition into account to decide opacity in interactive mode. --- vernac/declare.ml | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/vernac/declare.ml b/vernac/declare.ml index ce3e4f3430c6..50bc7831f20b 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -2061,15 +2061,31 @@ let control_only_guard { proof; pinfo } = raise (NotGuarded (env, sigma, cofix_error, fix_errors, rec_declaration)) with Exit -> () - (* Ignoring Qed/Defined keyword *) +let warn_use_sealed = + CWarnings.create ~name:"sealed" ~category:CWarnings.CoreCategories.vernacular + (function + | (id, true) -> Pp.strbrk "Use attribute \"sealed\" rather than \"Qed\" proof terminator to declare " ++ Id.print id ++ strbrk " sealed." + | (id, false) -> Pp.strbrk "Use attribute \"defined\" to declare " ++ Id.print id ++ strbrk " transparent.") + +let set_proof_opacity ending kind cinfo opaque_ending = + let idl = List.filter_map (function CInfo.{ name; opaque = None } -> Some name | _ -> None) cinfo in + let ending = CEphemeron.default ending Proof_ending.Regular in + match kind, opaque_ending with + | Decls.IsDefinition d, Vernacexpr.Opaque -> + (* A definition ended with Qed: warn if there is no attribute *) + (match d, ending, idl with + | (Definition | Fixpoint | CoFixpoint), Proof_ending.Regular, id::_ -> warn_use_sealed (id, true) + | _ -> ()); true + | IsDefinition _, Vernacexpr.Transparent -> false + | IsProof _, Vernacexpr.Opaque -> true + | IsProof _, Vernacexpr.Transparent -> false + | (Decls.IsPrimitive | IsSymbol | IsAssumption _), _ -> false (* Irrelevant *) let return_proof p = (prepare_proof p : closed_proof_output) let close_proof ?warn_incomplete ~opaque ~keep_body_ucst_separate (proof : t) : Proof_object.t = NewProfile.profile "close_proof" (fun () -> - let opaque = match opaque with - | Vernacexpr.Opaque -> true - | Vernacexpr.Transparent -> false in + let opaque = set_proof_opacity proof.pinfo.proof_ending proof.pinfo.info.kind proof.pinfo.cinfo opaque in let keep_body_ucst_separate = if keep_body_ucst_separate then Some proof.initial_euctx else None in { Proof_object.proof_object = DefaultProof { proof = prepare_proof ?warn_incomplete proof; opaque; using = proof.using; keep_body_ucst_separate } From dc4ce6f50a4f75cf0b322b1340e14f6eb3f85475 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 2 Oct 2024 18:22:15 +0200 Subject: [PATCH 18/21] Change log for #19029 --- .../19029-master+sealed-attribute.rst | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 doc/changelog/02-specification-language/19029-master+sealed-attribute.rst diff --git a/doc/changelog/02-specification-language/19029-master+sealed-attribute.rst b/doc/changelog/02-specification-language/19029-master+sealed-attribute.rst new file mode 100644 index 000000000000..22cad70b0d8e --- /dev/null +++ b/doc/changelog/02-specification-language/19029-master+sealed-attribute.rst @@ -0,0 +1,8 @@ + +- **Added:** + New attributes :attr:`sealed` and :attr:`defined` allow to change + the default opacity (now called sealing to prevent the confusion + with the notion of opacity implemented by the command :cmd:`Opaque`) + of a definition or theorem + (`#19029 `_, + by Hugo Herbelin). From b23f8e8062b1b04512c12c4553794beda5501adc Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 26 Oct 2024 19:36:54 +0200 Subject: [PATCH 19/21] Renaming proof ending Opaque->Qed, Transparent->Defined in Vernacexpr. --- plugins/funind/functional_principles_proofs.ml | 2 +- plugins/funind/gen_principle.ml | 12 ++++++------ plugins/funind/recdef.ml | 14 +++++++------- stm/stm.ml | 6 +++--- vernac/declare.ml | 10 +++++----- vernac/declare.mli | 6 +++--- vernac/g_proofs.mlg | 8 ++++---- vernac/ppvernac.ml | 6 +++--- vernac/vernac_classifier.ml | 4 ++-- vernac/vernacentries.ml | 2 +- vernac/vernacexpr.mli | 6 +++--- vernac/vernacstate.mli | 2 +- 12 files changed, 39 insertions(+), 39 deletions(-) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 116f47b28fbf..ec9569749e83 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -889,7 +889,7 @@ let generate_equation_lemma env evd fnames f fun_num nb_params nb_args rec_args_ let lemma = Declare.Proof.start ~cinfo ~info evd in let lemma, _ = Declare.Proof.by prove_replacement lemma in let (_ : _ list) = - Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent + Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Defined ~idopt:None in evd diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 45e5c92d37d9..c4b20b8e5e1b 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1335,11 +1335,11 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list = | Some finfos -> finfos in match finfos.equation_lemma with - | None -> Vernacexpr.Transparent (* non recursive definition *) + | None -> Vernacexpr.Defined (* non recursive definition *) | Some equation -> if Declareops.is_opaque (Global.lookup_constant equation) then - Vernacexpr.Opaque - else Vernacexpr.Transparent + Vernacexpr.Qed + else Vernacexpr.Defined in let body, typ, univs, _hook, sigma0 = try @@ -1489,7 +1489,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) let lemma = fst @@ Declare.Proof.by (proving_tac i) lemma in let (_ : _ list) = Declare.Proof.save_regular ~proof:lemma - ~opaque:Vernacexpr.Transparent ~idopt:None + ~opaque:Vernacexpr.Defined ~idopt:None in let finfo = match find_Function_infos (fst f_as_constant) with @@ -1563,7 +1563,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) in let (_ : _ list) = Declare.Proof.save_regular ~proof:lemma - ~opaque:Vernacexpr.Transparent ~idopt:None + ~opaque:Vernacexpr.Defined ~idopt:None in let finfo = match find_Function_infos (fst f_as_constant) with @@ -2166,7 +2166,7 @@ let build_scheme fas = List.iter2 (fun (princ_id, _, _) (body, types, univs, opaque) -> let (_ : Constant.t) = - let opaque = if opaque = Vernacexpr.Opaque then true else false in + let opaque = if opaque = Vernacexpr.Qed then true else false in let def_entry = Declare.definition_entry ~univs ~opaque ?types body in Declare.declare_constant ~name:princ_id ~kind:Decls.(IsProof Theorem) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 4d23cc428809..4954ff5da1ba 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -54,7 +54,7 @@ let declare_fun name kind ?univs value = let defined lemma = let (_ : _ list) = - Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent + Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Defined ~idopt:None in () @@ -1382,11 +1382,11 @@ let is_opaque_constant c = let cb = Global.lookup_constant c in let open Vernacexpr in match cb.Declarations.const_body with - | Declarations.OpaqueDef _ -> Opaque - | Declarations.Undef _ -> Opaque - | Declarations.Def _ -> Transparent - | Declarations.Primitive _ -> Opaque - | Declarations.Symbol _ -> Opaque + | Declarations.OpaqueDef _ -> Vernacexpr.Qed + | Declarations.Undef _ -> Vernacexpr.Qed + | Declarations.Def _ -> Defined + | Declarations.Primitive _ -> Vernacexpr.Qed + | Declarations.Symbol _ -> Vernacexpr.Qed let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type, decompose_and_tac, nb_goal) = @@ -1568,7 +1568,7 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref let cinfo = Declare.CInfo.make ~name:eq_name ~typ:(EConstr.of_constr equation_lemma_type) - ~opaque:(Some (opacity == Opaque)) () + ~opaque:(Some (opacity == Qed)) () in let lemma = Declare.Proof.start ~cinfo evd ~info in let lemma = diff --git a/stm/stm.ml b/stm/stm.ml index aea31e01b58d..eab9bf6875c7 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1487,7 +1487,7 @@ end = struct (* {{{ *) PG_compat.close_future_proof ~feedback_id:stop (Future.from_val proof) in let st = Vernacstate.freeze_full_state () in - let opaque = Opaque in + let opaque = Vernacexpr.Qed in try let _pstate = stm_qed_delay_proof ~st ~id:stop @@ -1774,7 +1774,7 @@ let collect_proof keep cur hd brkind id = | id :: _ -> Names.Id.to_string id in let loc = (snd cur).expr.CAst.loc in let is_defined_expr = function - | VernacSynPure (VernacEndProof (Proved (Transparent,_))) -> true + | VernacSynPure (VernacEndProof (Proved (Defined,_))) -> true | _ -> false in let is_defined = function | _, { expr = e } -> is_defined_expr e.CAst.v.expr @@ -2141,7 +2141,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = qed.fproof <- Some (None, ref false); None | VtKeep opaque -> let opaque = match opaque with - | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent + | VtKeepOpaque -> Vernacexpr.Qed | VtKeepDefined -> Defined | VtKeepAxiom -> assert false in let control, pe = extract_pe x in diff --git a/vernac/declare.ml b/vernac/declare.ml index 50bc7831f20b..e0a5371292e8 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -2071,14 +2071,14 @@ let set_proof_opacity ending kind cinfo opaque_ending = let idl = List.filter_map (function CInfo.{ name; opaque = None } -> Some name | _ -> None) cinfo in let ending = CEphemeron.default ending Proof_ending.Regular in match kind, opaque_ending with - | Decls.IsDefinition d, Vernacexpr.Opaque -> + | Decls.IsDefinition d, Vernacexpr.Qed -> (* A definition ended with Qed: warn if there is no attribute *) (match d, ending, idl with | (Definition | Fixpoint | CoFixpoint), Proof_ending.Regular, id::_ -> warn_use_sealed (id, true) | _ -> ()); true - | IsDefinition _, Vernacexpr.Transparent -> false - | IsProof _, Vernacexpr.Opaque -> true - | IsProof _, Vernacexpr.Transparent -> false + | IsDefinition _, Vernacexpr.Defined -> false + | IsProof _, Vernacexpr.Qed -> true + | IsProof _, Vernacexpr.Defined -> false | (Decls.IsPrimitive | IsSymbol | IsAssumption _), _ -> false (* Irrelevant *) let return_proof p = (prepare_proof p : closed_proof_output) @@ -2115,7 +2115,7 @@ let build_constant_by_tactic ~name ?warn_incomplete ~sigma ~sign ~poly (typ : EC let pinfo = Proof_info.make ~cinfo ~info () in let pf = start_proof_core ~name ~pinfo sigma [Some sign, typ] in let pf, status = by tac pf in - let proof = close_proof ?warn_incomplete ~keep_body_ucst_separate:false ~opaque:Vernacexpr.Transparent pf in + let proof = close_proof ?warn_incomplete ~keep_body_ucst_separate:false ~opaque:Vernacexpr.Defined pf in let entries = process_proof ~info ~cinfo proof.proof_object in let { Proof.sigma } = Proof.data pf.proof in let sigma = Evd.set_universe_context sigma (ustate_of_proof proof.proof_object) in diff --git a/vernac/declare.mli b/vernac/declare.mli index 128ce63a3d15..c2ffdde620d1 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -206,14 +206,14 @@ module Proof : sig val save : pm:OblState.t -> proof:t - -> opaque:Vernacexpr.opacity_flag + -> opaque:Vernacexpr.proof_opacity -> idopt:Names.lident option -> OblState.t * GlobRef.t list (** For proofs known to have [Regular] ending, no need to touch program state. *) val save_regular : proof:t - -> opaque:Vernacexpr.opacity_flag + -> opaque:Vernacexpr.proof_opacity -> idopt:Names.lident option -> GlobRef.t list @@ -291,7 +291,7 @@ module Proof : sig instead *) type proof_object - val close_proof : ?warn_incomplete:bool -> opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> t -> proof_object + val close_proof : ?warn_incomplete:bool -> opaque:Vernacexpr.proof_opacity -> keep_body_ucst_separate:bool -> t -> proof_object val close_future_proof : feedback_id:Stateid.t -> t -> closed_proof_output Future.computation -> proof_object (** Special cases for delayed proofs, in this case we must provide the diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 1f20d9aaa41e..4eacb1e77ca8 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -65,12 +65,12 @@ GRAMMAR EXTEND Gram | IDENT "Abort" -> { VernacSynPure VernacAbort } | IDENT "Abort"; IDENT "All" -> { VernacSynPure VernacAbortAll } | IDENT "Admitted" -> { VernacSynPure (VernacEndProof Admitted) } - | IDENT "Qed" -> { VernacSynPure (VernacEndProof (Proved (Opaque,None))) } + | IDENT "Qed" -> { VernacSynPure (VernacEndProof (Proved (Qed,None))) } | IDENT "Save"; id = identref -> - { VernacSynPure (VernacEndProof (Proved (Opaque, Some id))) } - | IDENT "Defined" -> { VernacSynPure (VernacEndProof (Proved (Transparent,None))) } + { VernacSynPure (VernacEndProof (Proved (Qed, Some id))) } + | IDENT "Defined" -> { VernacSynPure (VernacEndProof (Proved (Defined,None))) } | IDENT "Defined"; id=identref -> - { VernacSynPure (VernacEndProof (Proved (Transparent,Some id))) } + { VernacSynPure (VernacEndProof (Proved (Defined,Some id))) } | IDENT "Restart" -> { VernacSynPure VernacRestart } | IDENT "Undo" -> { VernacSynPure (VernacUndo 1) } | IDENT "Undo"; n = natural -> { VernacSynPure (VernacUndo n) } diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 10ea5068e878..6d3541fa203c 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -876,9 +876,9 @@ let pr_synpure_vernac_expr v = | VernacEndProof (Proved (opac,o)) -> return ( match o with | None -> (match opac with - | Transparent -> keyword "Defined" - | Opaque -> keyword "Qed") - | Some id -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id + | Defined -> keyword "Defined" + | Qed -> keyword "Qed") + | Some id -> (if opac <> Defined then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id ) | VernacExactProof c -> return (hov 2 (keyword "Proof" ++ pr_lconstrarg c)) diff --git a/vernac/vernac_classifier.ml b/vernac/vernac_classifier.ml index a1b9b2f06f51..1fe06e19839e 100644 --- a/vernac/vernac_classifier.ml +++ b/vernac/vernac_classifier.ml @@ -32,8 +32,8 @@ let string_of_vernac_classification = function | VtProofMode _ -> "Proof Mode" let vtkeep_of_opaque = function - | Opaque -> VtKeepOpaque - | Transparent -> VtKeepDefined + | Qed -> VtKeepOpaque + | Defined -> VtKeepDefined let idents_of_name : Names.Name.t -> Names.Id.t list = function diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index aa15997d787f..7866a52ff002 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -907,7 +907,7 @@ let vernac_exact_proof ~lemma ~pm c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the beginning of a proof. *) let lemma, status = Declare.Proof.by (Tactics.exact_proof c) lemma in - let pm, _ = Declare.Proof.save ~pm ~proof:lemma ~opaque:Opaque ~idopt:None in + let pm, _ = Declare.Proof.save ~pm ~proof:lemma ~opaque:Qed ~idopt:None in if not status then Feedback.feedback Feedback.AddedAxiom; pm diff --git a/vernac/vernacexpr.mli b/vernac/vernacexpr.mli index 0595978a11e6..ae792b0573fa 100644 --- a/vernac/vernacexpr.mli +++ b/vernac/vernacexpr.mli @@ -245,15 +245,15 @@ type one_inductive_expr = type typeclass_constraint = name_decl * Glob_term.binding_kind * constr_expr and typeclass_context = typeclass_constraint list +type proof_opacity = Qed | Defined + type proof_expr = ident_decl * (local_binder_expr list * constr_expr) -type opacity_flag = Opaque | Transparent - type proof_end = | Admitted (* name in `Save ident` when closing goal *) - | Proved of opacity_flag * lident option + | Proved of proof_opacity * lident option type scheme_type = | SchemeInduction diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index ca2228bdffdb..1b7aaf88652a 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -119,7 +119,7 @@ module Declare : sig -> Declare.Proof.proof_object val close_proof - : opaque:Vernacexpr.opacity_flag + : opaque:Vernacexpr.proof_opacity -> keep_body_ucst_separate:bool -> Declare.Proof.proof_object From afb13765f3347f754237a2e0a08372b73751710d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 26 Oct 2024 20:57:15 +0200 Subject: [PATCH 20/21] Attempt to clarify role of Qed/Defined proof ending in opacity computation. --- vernac/declare.ml | 55 ++++++++++++++++++++++++++--------------------- 1 file changed, 30 insertions(+), 25 deletions(-) diff --git a/vernac/declare.ml b/vernac/declare.ml index e0a5371292e8..0ebb60ccc4a9 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -838,7 +838,7 @@ type closed_proof_output = ((Constr.t * Evd.side_effects) * Constr.t option) lis type proof_object = | DefaultProof of { proof : closed_proof_output - ; opaque : bool + ; default_proof_opacity : Vernacexpr.proof_opacity ; using : Names.Id.Set.t option ; keep_body_ucst_separate : UState.t option } @@ -850,19 +850,19 @@ type proof_object = ; initial_euctx : UState.t } -let check_opacity opaque sealed = +let set_opacity default_proof_opacity sealed = match sealed with - | Some sealed -> (* Attribute takes precedence *) sealed - | None -> opaque + | Some sealed -> (* Attribute takes precedence on proof ending *) sealed + | None -> Vernacexpr.(match default_proof_opacity with Qed -> true | Defined -> false) let future_map2_pair_list_distribute p l f = List.map_i (fun i c -> f (Future.chain p (fun (a, b) -> (List.nth a i, b))) c) 0 l let process_proof ~info:Info.({ udecl; poly; kind }) ~cinfo = function - | DefaultProof { proof = (entries, uctx); opaque; using; keep_body_ucst_separate } -> + | DefaultProof { proof = (entries, uctx); default_proof_opacity; using; keep_body_ucst_separate } -> (* Force transparency for Derive-like dependent statements *) snd (List.fold_left2_map (fun used_univs ((body, eff), typ) CInfo.{ opaque = sealed } -> - let opaque = check_opacity opaque sealed in + let opaque = set_opacity default_proof_opacity sealed in let uctx, univs, used_univs, body = make_univs_immediate ~poly ?keep_body_ucst_separate ~opaque ~uctx ~udecl ~eff ~used_univs body typ in (used_univs, (definition_entry_core ?using ~univs ?types:typ body, uctx))) Univ.Level.Set.empty entries cinfo) @@ -1022,18 +1022,21 @@ let prepare_recursive_edeclaration sigma cinfo fixtypes fixrs fixdefs = (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) let default_kind_opacity_immediate = function - | Decls.IsPrimitive | IsSymbol | IsAssumption _ -> true (* Irrelevant *) - | IsDefinition _ -> false - | IsProof _ -> true + | Decls.IsPrimitive | IsSymbol | IsAssumption _ -> assert false (* not built interactively *) + | IsDefinition _ -> Vernacexpr.Defined + | IsProof _ -> Vernacexpr.Qed -let set_immediate_opacity kind cinfo = +let check_immediate_theorem kind cinfo = if List.exists (fun CInfo.{opaque} -> Option.is_empty opaque) cinfo then begin match kind with | Decls.IsProof p -> CErrors.user_err (str (Ppvernac.string_of_theorem_kind p) ++ str " declared with \":=\" requires sealed/defined attributes.") | _ -> () - end; + end + +let set_default_proof_opacity_immediate kind cinfo = + check_immediate_theorem kind cinfo; default_kind_opacity_immediate kind let declare_mutual_definitions ~info ~cinfo ~uctx ~bodies ~possible_guard ?using () = @@ -1047,8 +1050,8 @@ let declare_mutual_definitions ~info ~cinfo ~uctx ~bodies ~possible_guard ?using let entries = List.map (fun (body, typ) -> ((body, Evd.empty_side_effects), Some typ)) bodies_types in let entries_for_using = List.map (fun (body, typ) -> (body, Some typ)) bodies_types in let using = interp_mutual_using env cinfo entries_for_using using in - let opaque = set_immediate_opacity kind cinfo in - let obj = DefaultProof { proof = (entries, uctx); opaque; using; keep_body_ucst_separate = None } in + let default_proof_opacity = set_default_proof_opacity_immediate kind cinfo in + let obj = DefaultProof { proof = (entries, uctx); default_proof_opacity; using; keep_body_ucst_separate = None } in let refs = declare_possibly_mutual_definitions ~info ~cinfo ~obls:[] obj in let fixnames = List.map (fun { CInfo.name } -> name) cinfo in recursive_message indexes fixnames; @@ -1081,9 +1084,9 @@ let declare_definition ~info ~cinfo ~obls ~body ?using sigma = let body = EConstr.to_constr sigma body in let typ = Option.map (EConstr.to_constr sigma) typ in let uctx = Evd.ustate sigma in - let opaque = set_immediate_opacity info.Info.kind [cinfo] in + let default_proof_opacity = set_default_proof_opacity_immediate info.Info.kind [cinfo] in let using = interp_mutual_using env [cinfo] [body,typ] using in - let obj = DefaultProof { proof = ([((body,Evd.empty_side_effects),typ)], uctx); opaque; using; keep_body_ucst_separate = None } in + let obj = DefaultProof { proof = ([((body,Evd.empty_side_effects),typ)], uctx); default_proof_opacity; using; keep_body_ucst_separate = None } in let gref = List.hd (declare_possibly_mutual_definitions ~info ~cinfo:[cinfo] ~obls obj) in gref, uctx @@ -2067,28 +2070,30 @@ let warn_use_sealed = | (id, true) -> Pp.strbrk "Use attribute \"sealed\" rather than \"Qed\" proof terminator to declare " ++ Id.print id ++ strbrk " sealed." | (id, false) -> Pp.strbrk "Use attribute \"defined\" to declare " ++ Id.print id ++ strbrk " transparent.") -let set_proof_opacity ending kind cinfo opaque_ending = - let idl = List.filter_map (function CInfo.{ name; opaque = None } -> Some name | _ -> None) cinfo in - let ending = CEphemeron.default ending Proof_ending.Regular in +let check_proof_opacity_compatibility ending kind cinfo opaque_ending = match kind, opaque_ending with | Decls.IsDefinition d, Vernacexpr.Qed -> (* A definition ended with Qed: warn if there is no attribute *) + let ending = CEphemeron.default ending Proof_ending.Regular in + let idl = List.filter_map (function CInfo.{ name; opaque = None } -> Some name | _ -> None) cinfo in (match d, ending, idl with | (Definition | Fixpoint | CoFixpoint), Proof_ending.Regular, id::_ -> warn_use_sealed (id, true) - | _ -> ()); true - | IsDefinition _, Vernacexpr.Defined -> false - | IsProof _, Vernacexpr.Qed -> true - | IsProof _, Vernacexpr.Defined -> false - | (Decls.IsPrimitive | IsSymbol | IsAssumption _), _ -> false (* Irrelevant *) + | _ -> ()) + | (IsDefinition _ | IsProof _), _ -> () + | (Decls.IsPrimitive | IsSymbol | IsAssumption _), _ -> assert false (* not built interactively *) + +let set_proof_opacity ending kind cinfo opaque_ending = + check_proof_opacity_compatibility ending kind cinfo opaque_ending; + opaque_ending let return_proof p = (prepare_proof p : closed_proof_output) let close_proof ?warn_incomplete ~opaque ~keep_body_ucst_separate (proof : t) : Proof_object.t = NewProfile.profile "close_proof" (fun () -> - let opaque = set_proof_opacity proof.pinfo.proof_ending proof.pinfo.info.kind proof.pinfo.cinfo opaque in + let default_proof_opacity = set_proof_opacity proof.pinfo.proof_ending proof.pinfo.info.kind proof.pinfo.cinfo opaque in let keep_body_ucst_separate = if keep_body_ucst_separate then Some proof.initial_euctx else None in { Proof_object.proof_object = - DefaultProof { proof = prepare_proof ?warn_incomplete proof; opaque; using = proof.using; keep_body_ucst_separate } + DefaultProof { proof = prepare_proof ?warn_incomplete proof; default_proof_opacity; using = proof.using; keep_body_ucst_separate } ; pinfo = proof.pinfo }) () From 3076d12eceebf42edfdaee47953d91b59d6be29a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 26 Oct 2024 21:00:01 +0200 Subject: [PATCH 21/21] Replace binary sealed/defined attribute by ternary sealed/opaque/transparent. --- .../tuto1/src/simple_declare.ml | 2 +- doc/sphinx/language/core/definitions.rst | 42 +++++++++++----- doc/sphinx/language/core/inductive.rst | 4 +- plugins/derive/derive.ml | 2 +- .../funind/functional_principles_proofs.ml | 2 +- plugins/funind/gen_principle.ml | 6 +-- plugins/funind/recdef.ml | 6 +-- plugins/ltac/comRewrite.ml | 4 +- plugins/ltac/leminv.ml | 2 +- plugins/ltac/leminv.mli | 2 +- test-suite/success/sealed.v | 6 +-- vernac/attributes.ml | 9 +++- vernac/attributes.mli | 6 ++- vernac/classes.mli | 6 +-- vernac/comDefinition.mli | 6 +-- vernac/comFixpoint.ml | 2 +- vernac/comFixpoint.mli | 2 +- vernac/declare.ml | 49 ++++++++++--------- vernac/declare.mli | 2 +- vernac/vernacentries.ml | 2 +- vernac/vernacentries.mli | 2 +- 21 files changed, 95 insertions(+), 69 deletions(-) diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 8d961fba847e..d9b0581e1a7d 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,4 +1,4 @@ let declare_definition ~poly name sigma body = - let cinfo = Declare.CInfo.make ~name ~typ:None ~opaque:(Some false) () in + let cinfo = Declare.CInfo.make ~name ~typ:None ~opaque:(Some (Attributes.Defined Conv_oracle.transparent)) () in let info = Declare.Info.make ~poly () in Declare.declare_definition ~info ~cinfo ~body sigma diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 7d6b3057cfde..f674fe90776e 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -125,8 +125,8 @@ Section :ref:`typing-rules`. The attributes :attr:`local`, :attr:`universes(polymorphic)`, :attr:`program` (see :ref:`program_definition`), :attr:`canonical`, :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, :attr:`deprecated`, - :attr:`warn` and :attr:`using`, as well as the exclusive attributes :attr:`sealed` and - :attr:`defined` are accepted. + :attr:`warn` and :attr:`using` as well as the exclusive attributes :attr:`sealed`, + :attr:`opaque` and :attr:`transparent`. .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. @@ -217,7 +217,7 @@ that end with :cmd:`Qed` are sealed, that is that their content cannot be unfolded (see :ref:`applyingconversionrules`), thus realizing *proof irrelevance*, that is that only provability matters, and not the exact proof. Proofs can be made unfoldable, as -definitions are, with the :attr:`defined` attribute or by ending +definitions are, by using the :attr:`transparent` attribute or by ending the proof with :cmd:`Defined` in place of :cmd:`Qed`. We recommend using the attribute. @@ -238,18 +238,34 @@ recommend using the attribute. #. One can also use :cmd:`Admitted` in place of :cmd:`Qed` to turn the current asserted statement into an axiom and exit proof mode. -Sealing and transparency ------------------------- - -By default, definitions are unfoldable while the proofs of theorems are -not. You can change this using these attributes: +Sealing, transparency and opacity +--------------------------------- + +Definitions and theorems can be sealed, transparent or opaque. Sealed +means that the body of the definition or the proof of the theorem are +abstract and cannot be unfolded. Transparent means that it can be +freely unfolded. Opaque means that it is unfoldable for type-checking +but kept abstract for reduction (see +e.g. :tacn:`unfold`). Transparency and opacity can be changed at any +time using the commands :cmd:`Transparent` and :cmd:`Opaque`. On the +other side, a sealed constant cannot be changed later to transparent +or opaque, nor a transparent or opaque constant be changed to sealed. + +By default, definitions not built by tactics are +transparent. Definitions built interactively and ended with +:n:`Defined` are transparent. Theorems built interactively and ended +with :n:`Qed` are sealed. In the other cases, one of the following +attribute is expected: .. attr:: sealed - Prevents the unfoldability of the definition, so it behaves like an abstract definition. - -.. attr:: defined +.. attr:: transparent - Makes the proof of a theorem unfoldable, as if it were a definition. +.. attr:: opaque - .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. +Note that these attributes can be added either before the declaration +(e.g. :n:`#[sealed] Definition @ident := @term`) or before the name of +the constant (e.g. :n:`Definition #[sealed] @ident := @term`). When +several constants are declared at once (using :n:`with`), the +attribute given before the declaration is used as the default for all +names not themselves prefixed by an attribute. diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index da459ec4142c..11cb135458ba 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -486,8 +486,8 @@ constructions. This command accepts the :attr:`local`, :attr:`universes(polymorphic)`, :attr:`program`, :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, :attr:`deprecated`, - :attr:`warn` and :attr:`using` attributes, as well as the exclusive attributes :attr:`sealed` - and :attr:`defined`. The :attr:`program` attribute is needed + :attr:`warn` and :attr:`using` attributes, as well as the exclusive attributes :attr:`sealed`, + :attr:`opaque` and :attr:`transparent`. The :attr:`program` attribute is needed so that the :n:`wf` or :n:`measure` clauses of :n:`@fixannot` are supported. See :ref:`program_fixpoint`. diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 43ca2ae44e54..254557f477c3 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -71,7 +71,7 @@ let start_deriving ~atts bl suchthat name : Declare.Proof.t = let name = get_id d in let impargs = Constrintern.implicits_of_decl_in_internalization_env name impls_env in let impargs = List.map CAst.make (List.map extract_manual impargs) in - make ~name ~typ:() ~impargs ~opaque:(Some false) ()) ctx' @ + make ~name ~typ:() ~impargs ~opaque:(Some (Attributes.Defined Conv_oracle.transparent)) ()) ctx' @ [make ~name ~typ:() ~impargs ~opaque ()] in let lemma = Declare.Proof.start_derive ~name ~info ~cinfo goals in Declare.Proof.map lemma ~f:(fun p -> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ec9569749e83..d2c4c24077bf 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -884,7 +884,7 @@ let generate_equation_lemma env evd fnames f fun_num nb_params nb_args rec_args_ constructing the lemma Ensures by: obvious i*) let info = Declare.Info.make () in let cinfo = - Declare.CInfo.make ~name:(mk_equation_id f_id) ~typ:lemma_type ~opaque:(Some false) () + Declare.CInfo.make ~name:(mk_equation_id f_id) ~typ:lemma_type ~opaque:(Some (Attributes.Defined Conv_oracle.transparent)) () in let lemma = Declare.Proof.start ~cinfo ~info evd in let lemma, _ = Declare.Proof.by prove_replacement lemma in diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index c4b20b8e5e1b..c80e1a070af0 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -386,7 +386,7 @@ let register_struct is_rec (rec_order, fixpoint_exprl) = CErrors.user_err Pp.(str "Body of Function must be given.") in - ComDefinition.do_definition ~name:fname.CAst.v ~opaque:(Some false) ~poly:false + ComDefinition.do_definition ~name:fname.CAst.v ~opaque:(Some (Attributes.Defined Conv_oracle.transparent)) ~poly:false ~kind:Decls.Definition univs binders None body (Some rtype); let evd, rev_pconstants = List.fold_left @@ -1484,7 +1484,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) let lem_id = mk_correct_id f_id in let typ, _ = lemmas_types_infos.(i) in let info = Declare.Info.make () in - let cinfo = Declare.CInfo.make ~name:lem_id ~typ ~opaque:(Some false) () in + let cinfo = Declare.CInfo.make ~name:lem_id ~typ ~opaque:(Some (Attributes.Defined Conv_oracle.transparent)) () in let lemma = Declare.Proof.start ~cinfo ~info !evd in let lemma = fst @@ Declare.Proof.by (proving_tac i) lemma in let (_ : _ list) = @@ -1550,7 +1550,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) let lem_id = mk_complete_id f_id in let info = Declare.Info.make() in let cinfo = - Declare.CInfo.make ~name:lem_id ~typ:(fst lemmas_types_infos.(i)) ~opaque:(Some false) () + Declare.CInfo.make ~name:lem_id ~typ:(fst lemmas_types_infos.(i)) ~opaque:(Some (Attributes.Defined Conv_oracle.transparent)) () in let lemma = Declare.Proof.start ~cinfo sigma ~info in let lemma = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 4954ff5da1ba..8833569c5728 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1463,7 +1463,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name () in let info = Declare.Info.make ~hook:(Declare.Hook.make hook) () in - let cinfo = Declare.CInfo.make ~name:na ~typ:gls_type ~opaque:(Some false (* as in "defined" *)) () in + let cinfo = Declare.CInfo.make ~name:na ~typ:gls_type ~opaque:(Some (Attributes.Defined Conv_oracle.transparent) (* as in "defined" *)) () in let lemma = Declare.Proof.start ~cinfo ~info sigma in let lemma = if Indfun_common.is_strict_tcc () then @@ -1496,7 +1496,7 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes let cinfo = Declare.CInfo.make ~name:thm_name ~typ:(EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) - ~opaque:(Some false) () + ~opaque:(Some (Attributes.Defined Conv_oracle.transparent)) () in let info = Declare.Info.make ~hook () in let lemma = Declare.Proof.start ~cinfo ~info ctx in @@ -1568,7 +1568,7 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref let cinfo = Declare.CInfo.make ~name:eq_name ~typ:(EConstr.of_constr equation_lemma_type) - ~opaque:(Some (opacity == Qed)) () + ~opaque:(Some (match opacity with Vernacexpr.Qed -> Attributes.Sealed | Vernacexpr.Defined -> Attributes.Defined Conv_oracle.transparent)) () in let lemma = Declare.Proof.start ~cinfo evd ~info in let lemma = diff --git a/plugins/ltac/comRewrite.ml b/plugins/ltac/comRewrite.ml index fe46358c4571..76e9c4b8f0b9 100644 --- a/plugins/ltac/comRewrite.ml +++ b/plugins/ltac/comRewrite.ml @@ -35,7 +35,7 @@ let init_setoid () = type rewrite_attributes = { polymorphic : bool; locality : Hints.hint_locality; - opaque : bool option; + opaque : Attributes.opacity option; } let rewrite_attributes = @@ -173,7 +173,7 @@ let declare_projection name instance_id r = let types = Some (it_mkProd_or_LetIn typ ctx) in let kind = Decls.(IsDefinition Definition) in let impargs, udecl = [], UState.default_univ_decl in - let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ~opaque:(Some false) () in + let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ~opaque:(Some (Attributes.Defined Conv_oracle.transparent)) () in let info = Declare.Info.make ~kind ~udecl ~poly () in let _r : GlobRef.t = Declare.declare_definition ~cinfo ~info ~body sigma diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml index 6aba27bd6abb..1ea838457945 100644 --- a/plugins/ltac/leminv.ml +++ b/plugins/ltac/leminv.ml @@ -231,7 +231,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = let add_inversion_lemma ~poly ~opaque name env sigma t sort dep inv_op = let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in - let opaque = Some (Option.default false opaque) in + let opaque = Some (Option.default (Attributes.Defined Conv_oracle.transparent) opaque) in let cinfo = Declare.CInfo.make ~name ~typ:None ~opaque () in let info = Declare.Info.make ~poly ~kind:Decls.(IsProof Lemma) () in let _ : Names.GlobRef.t = diff --git a/plugins/ltac/leminv.mli b/plugins/ltac/leminv.mli index ac4f5b544922..8b8c49d586cd 100644 --- a/plugins/ltac/leminv.mli +++ b/plugins/ltac/leminv.mli @@ -16,6 +16,6 @@ open Tactypes val lemInv_clause : quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic -val add_inversion_lemma_exn : poly:bool -> opaque:bool option -> +val add_inversion_lemma_exn : poly:bool -> opaque:Attributes.opacity option -> Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) -> unit diff --git a/test-suite/success/sealed.v b/test-suite/success/sealed.v index 83a21a94ef5c..fad1ed28dde7 100644 --- a/test-suite/success/sealed.v +++ b/test-suite/success/sealed.v @@ -1,6 +1,6 @@ (* Opacity per name *) Fixpoint #[sealed] f n := match n with 0 => 0 | S n => g n end -with #[defined] g n := match n with 0 => 0 | S n => f n end. +with #[transparent] g n := match n with 0 => 0 | S n => f n end. Fail Check eq_refl : f 0 = 0. Check eq_refl : g 0 = 0. @@ -24,14 +24,14 @@ with g' n := match n with 0 => 0 | S n => f' n end. Fail Check eq_refl : c = 0. -#[defined] Theorem u : nat. exact 0. Qed. (* ok *) +#[transparent] Theorem u : nat. exact 0. Qed. (* ok *) #[sealed] Definition v : nat. exact 0. Defined. (* ok *) Check eq_refl : u = 0. Fail Check eq_refl : v = 0. #[sealed] Theorem w : nat. exact 0. Defined. -#[defined] Definition x : nat. exact 0. Qed. +#[transparent] Definition x : nat. exact 0. Qed. Fail Check eq_refl : w = 0. Check eq_refl : x = 0. diff --git a/vernac/attributes.ml b/vernac/attributes.ml index ba7ace2d7b46..2ce209206819 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -265,11 +265,16 @@ let locality = ("global", single_key_parser ~name ~key:"global" false); ] +type opacity = + | Sealed + | Defined of Conv_oracle.level + let opacity = let name = "Opacity" in attribute_of_list [ - ("sealed", single_key_parser ~name ~key:"sealed" true); - ("defined", single_key_parser ~name ~key:"defined" false); + ("sealed", single_key_parser ~name ~key:"sealed" Sealed); + ("opaque", single_key_parser ~name ~key:"opaque" (Defined Conv_oracle.Opaque)); + ("transparent", single_key_parser ~name ~key:"transparent" (Defined Conv_oracle.transparent)); ] let ukey = "universes" diff --git a/vernac/attributes.mli b/vernac/attributes.mli index d58308bacd87..5ff8103e8409 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -49,6 +49,10 @@ end (** Definitions for some standard attributes. *) +type opacity = + | Sealed + | Defined of Conv_oracle.level + val raw_attributes : vernac_flags attribute val polymorphic : bool attribute @@ -57,7 +61,7 @@ val template : bool option attribute val unfold_fix : bool attribute val locality : bool option attribute val option_locality : Goptions.option_locality attribute -val opacity : bool option attribute +val opacity : opacity option attribute val reversible : bool option attribute val canonical_field : bool attribute val canonical_instance : bool attribute diff --git a/vernac/classes.mli b/vernac/classes.mli index 785abdbe1cc9..3b542ac374e5 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -26,7 +26,7 @@ val existing_instance : ?loc:Loc.t -> Hints.hint_locality -> GlobRef.t -> Vernac val new_instance_interactive : locality:Hints.hint_locality - -> opaque:bool option + -> opaque:Attributes.opacity option -> poly:bool -> name_decl -> local_binder_expr list @@ -39,7 +39,7 @@ val new_instance_interactive val new_instance : locality:Hints.hint_locality - -> opaque:bool option + -> opaque:Attributes.opacity option -> poly:bool -> name_decl -> local_binder_expr list @@ -52,7 +52,7 @@ val new_instance val new_instance_program : locality:Hints.hint_locality -> pm:Declare.OblState.t - -> opaque:bool option + -> opaque:Attributes.opacity option -> poly:bool -> name_decl -> local_binder_expr list diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 91629b47ca75..a2341b79ece5 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -29,7 +29,7 @@ val do_definition : ?hook:Declare.Hook.t -> name:Id.t -> ?scope:Locality.definition_scope - -> opaque:bool option + -> opaque:Attributes.opacity option -> ?clearbody:bool -> poly:bool -> ?typing_flags:Declarations.typing_flags @@ -48,7 +48,7 @@ val do_definition_program -> pm:Declare.OblState.t -> name:Id.t -> scope:Locality.definition_scope - -> opaque:bool option + -> opaque:Attributes.opacity option -> ?clearbody:bool -> poly:bool -> ?typing_flags:Declarations.typing_flags @@ -67,7 +67,7 @@ val do_definition_interactive -> ?hook:Declare.Hook.t -> name:Id.t -> scope:Locality.definition_scope - -> opaque:bool option + -> opaque:Attributes.opacity option -> ?clearbody:bool -> poly:bool -> typing_flags:Declarations.typing_flags option diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 55fe6b540539..8f15d0285ab9 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -385,7 +385,7 @@ type ('constr, 'relevance) fix_data = { fiximps : (Names.Name.t * bool) option CAst.t list list; fixntns : Metasyntax.notation_interpretation_decl list; fixwfs : (rel_declaration * EConstr.t * EConstr.t * EConstr.t) option list; - fixopaques : bool option list; + fixopaques : Attributes.opacity option list; } let interp_wf ~program_mode env sigma recname ctx ccl = function diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index bb896ebaeeba..457bb447f792 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -27,7 +27,7 @@ val do_mutually_recursive (* Tell to try the obligation tactic to solve evars *) -> ?scope:Locality.definition_scope (* Local or Global visibility *) - -> ?opaque:bool + -> ?opaque:Attributes.opacity (* Global opacity attribute if any *) -> ?clearbody:bool (* Hide body if in sections *) diff --git a/vernac/declare.ml b/vernac/declare.ml index 0ebb60ccc4a9..830888003b31 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -57,7 +57,7 @@ module CInfo = struct (** Names to pre-introduce *) ; impargs : Impargs.manual_implicits (** Explicitily declared implicit arguments *) - ; opaque : bool option + ; opaque : Attributes.opacity option } @@ -106,7 +106,7 @@ type 'eff deferred_opaque_proof_body = { (* Opacity of default proofs, possibly with private universes *) type default_body_opacity = - | Transparent + | Transparent of Conv_oracle.level (* udecl is for body+type; all universes are in proof_entry_universes *) | Opaque of Univ.ContextSet.t (* if poly, the private uctx, udecl excludes the private uctx *) @@ -250,7 +250,7 @@ let make_univs_immediate_default ~poly ~opaque ~uctx ~udecl ~eff ~used_univs bod when monomorphic it shouldn't really matter. *) Monomorphic_entry (Univ.ContextSet.union uctx (Safe_typing.universes_of_private eff.Evd.seff_private)), snd utyp in - uctx, utyp, used_univs, Default { body = (body, eff); opaque = if opaque then Opaque Univ.ContextSet.empty else Transparent } + uctx, utyp, used_univs, Default { body = (body, eff); opaque = Attributes.(match opaque with Sealed -> Opaque Univ.ContextSet.empty | Defined tr -> Transparent tr)} let make_univs_immediate ~poly ?keep_body_ucst_separate ~opaque ~uctx ~udecl ~eff ~used_univs body typ = (* allow_deferred case *) @@ -258,7 +258,7 @@ let make_univs_immediate ~poly ?keep_body_ucst_separate ~opaque ~uctx ~udecl ~ef | Some initial_euctx when not poly -> make_univs_immediate_private_mono ~initial_euctx ~uctx ~udecl ~eff ~used_univs body typ | _ -> (* private_poly_univs case *) - if poly && opaque && private_poly_univs () + if poly && opaque == Attributes.Sealed && private_poly_univs () then make_univs_immediate_private_poly ~uctx ~udecl ~eff ~used_univs body typ else make_univs_immediate_default ~poly ~opaque ~uctx ~udecl ~eff ~used_univs body typ @@ -272,11 +272,11 @@ let definition_entry_core ?using ?(inline=false) ?types proof_entry_universes = univs; proof_entry_inline_code = inline} -let pure_definition_entry ?(opaque=Transparent) ?using ?inline ?types ?univs body = +let pure_definition_entry ?(opaque=Transparent Conv_oracle.transparent) ?using ?inline ?types ?univs body = definition_entry_core ?using ?inline ?types ?univs body let definition_entry ?(opaque=false) ?using ?inline ?types ?univs body = - let opaque = if opaque then Opaque Univ.ContextSet.empty else Transparent in + let opaque = if opaque then Opaque Univ.ContextSet.empty else Transparent Conv_oracle.transparent in definition_entry_core ?using ?inline ?types ?univs (Default { body = (body, Evd.empty_side_effects); opaque }) let delayed_definition_entry ?feedback_id ?using ~univs ?types body = @@ -322,7 +322,7 @@ module ProofEntry = struct let get_opacity entry = match entry.proof_entry_body with - | Default { body; opaque = Transparent } -> false + | Default { body; opaque = Transparent _ } -> false | Default { body; opaque = Opaque _ } -> true | DeferredOpaque _ -> true @@ -336,7 +336,7 @@ module ProofEntry = struct let force_extract_body entry = match entry.proof_entry_body with - | Default { body = (body, eff); opaque = Transparent } -> ((body, Univ.ContextSet.empty), eff), false, None + | Default { body = (body, eff); opaque = Transparent _ } -> ((body, Univ.ContextSet.empty), eff), false, None | Default { body = (body, eff); opaque = Opaque uctx } -> ((body, uctx), eff), true, None | DeferredOpaque { body; feedback_id } -> Future.force body, true, feedback_id @@ -344,17 +344,17 @@ module ProofEntry = struct let (body, eff), opaque = force_entry_body entry in let uctx = match opaque with | Opaque uctx -> uctx - | Transparent -> Univ.ContextSet.empty + | Transparent _ -> Univ.ContextSet.empty in (body, uctx), eff let set_transparent_for_derived entry = let body, opaque = force_entry_body entry in match opaque with - | Transparent -> { entry with proof_entry_body = Default { body; opaque } } + | Transparent _ -> { entry with proof_entry_body = Default { body; opaque } } | Opaque uctx -> { entry with - proof_entry_body = Default { body; opaque = Transparent }; + proof_entry_body = Default { body; opaque = Transparent Conv_oracle.transparent }; proof_entry_universes = add_mono_univ_uctx_for_derived uctx entry.proof_entry_universes } let rec shrink ctx sign c t accu = @@ -451,14 +451,15 @@ let (objConstant : (Id.t * constant_obj) Libobject.Dyn.tag) = let inConstant v = Libobject.Dyn.Easy.inj v objConstant (* Register the libobjects attached to the constants *) -let register_constant cst kind ?user_warns local = +let register_constant cst kind ?user_warns ?transparency local = (* Register the declaration *) let id = Label.to_id (Constant.label cst) in let o = inConstant (id, { cst_kind = kind; cst_locl = local; cst_warn = user_warns }) in let () = Lib.add_leaf o in (* Register associated data *) Impargs.declare_constant_implicits cst; - Notation.declare_ref_arguments_scope (GlobRef.ConstRef cst) + Notation.declare_ref_arguments_scope (GlobRef.ConstRef cst); + Option.iter (fun b -> Redexpr.set_strategy false [b,[Evaluable.EvalConstRef cst]]) transparency let register_side_effect (c, body, role) = (* Register the body in the opaque table *) @@ -578,7 +579,7 @@ let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind ~typi | DefinitionEntry de -> (* We deal with side effects *) (match de.proof_entry_body with - | Default { body = (body, eff); opaque = Transparent } -> + | Default { body = (body, eff); opaque = Transparent transparency } -> (* This globally defines the side-effects in the environment and registers their libobjects. *) let () = export_side_effects eff in @@ -588,14 +589,14 @@ let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind ~typi (* We register the global universes after exporting side-effects, since the latter depend on the former. *) let () = Global.push_context_set ctx in - Entries.DefinitionEntry e, false, ubinders, None, ctx + Entries.DefinitionEntry e, false, ubinders, None, ctx, Some transparency | Default { body = (body, eff); opaque = Opaque body_uctx } -> let body = ((body, body_uctx), eff.Evd.seff_private) in let de = { de with proof_entry_body = body } in let cd, ctx = cast_opaque_proof_entry ImmediateEffectEntry de in let ubinders = make_ubinders ctx de.proof_entry_universes in let () = Global.push_context_set ctx in - Entries.OpaqueEntry cd, false, ubinders, Some (Future.from_val body, None), ctx + Entries.OpaqueEntry cd, false, ubinders, Some (Future.from_val body, None), ctx, None | DeferredOpaque { body; feedback_id } -> let map (body, eff) = body, eff.Evd.seff_private in let body = Future.chain body map in @@ -603,7 +604,7 @@ let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind ~typi let cd, ctx = cast_opaque_proof_entry DeferredEffectEntry de in let ubinders = make_ubinders ctx de.proof_entry_universes in let () = Global.push_context_set ctx in - Entries.OpaqueEntry cd, false, ubinders, Some (body, feedback_id), ctx) + Entries.OpaqueEntry cd, false, ubinders, Some (body, feedback_id), ctx, None) | ParameterEntry e -> let univ_entry, ctx = extract_monomorphic (fst e.parameter_entry_universes) in let ubinders = make_ubinders ctx e.parameter_entry_universes in @@ -614,7 +615,7 @@ let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind ~typi Entries.parameter_entry_universes = univ_entry; Entries.parameter_entry_inline_code = e.parameter_entry_inline_code; } in - Entries.ParameterEntry e, not (Lib.is_modtype_strict()), ubinders, None, ctx + Entries.ParameterEntry e, not (Lib.is_modtype_strict()), ubinders, None, ctx, None | PrimitiveEntry e -> let typ, univ_entry, ctx = match e.prim_entry_type with | None -> @@ -629,7 +630,7 @@ let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind ~typi Entries.prim_entry_content = e.prim_entry_content; } in let ubinders = make_ubinders ctx univ_entry in - Entries.PrimitiveEntry e, false, ubinders, None, ctx + Entries.PrimitiveEntry e, false, ubinders, None, ctx, None | SymbolEntry { symb_entry_type=typ; symb_entry_unfold_fix=un_fix; symb_entry_universes=entry_univs } -> let univ_entry, ctx = extract_monomorphic (fst entry_univs) in let () = Global.push_context_set ctx in @@ -639,7 +640,7 @@ let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind ~typi Entries.symb_entry_universes = univ_entry; } in let ubinders = make_ubinders ctx entry_univs in - Entries.SymbolEntry e, false, ubinders, None, ctx + Entries.SymbolEntry e, false, ubinders, None, ctx, None in let declare_opaque kn = function | None -> () @@ -652,7 +653,7 @@ let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind ~typi | Def _ | Undef _ | Primitive _ | Symbol _ -> assert false in let () = check_exists name in - let decl, unsafe, ubinders, delayed, ctx = make_constant cd in + let decl, unsafe, ubinders, delayed, ctx, transparency = make_constant cd in let kn = Global.add_constant ?typing_flags name decl in let () = let is_new_constraint (u,_,v as c) = @@ -665,7 +666,7 @@ let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind ~typi in let () = DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) ubinders in let () = declare_opaque kn delayed in - let () = register_constant kn kind local ?user_warns in + let () = register_constant kn kind ?transparency local ?user_warns in if unsafe || is_unsafe_typing_flags typing_flags then feedback_axiom(); kn @@ -853,7 +854,7 @@ type proof_object = let set_opacity default_proof_opacity sealed = match sealed with | Some sealed -> (* Attribute takes precedence on proof ending *) sealed - | None -> Vernacexpr.(match default_proof_opacity with Qed -> true | Defined -> false) + | None -> match default_proof_opacity with Vernacexpr.Qed -> Attributes.Sealed | Defined -> Attributes.Defined Conv_oracle.transparent let future_map2_pair_list_distribute p l f = List.map_i (fun i c -> f (Future.chain p (fun (a, b) -> (List.nth a i, b))) c) 0 l @@ -2125,7 +2126,7 @@ let build_constant_by_tactic ~name ?warn_incomplete ~sigma ~sign ~poly (typ : EC let { Proof.sigma } = Proof.data pf.proof in let sigma = Evd.set_universe_context sigma (ustate_of_proof proof.proof_object) in match entries with - | [ { proof_entry_body = Default { body; opaque = Transparent } } as entry, _] -> + | [ { proof_entry_body = Default { body; opaque = Transparent _ } } as entry, _] -> { entry with proof_entry_body = body }, status, sigma | _ -> CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term, or a non transparent one.") diff --git a/vernac/declare.mli b/vernac/declare.mli index c2ffdde620d1..3472e145d7c5 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -79,7 +79,7 @@ module CInfo : sig -> typ:'constr -> ?args:Name.t list -> ?impargs:Impargs.manual_implicits - -> opaque : bool option + -> opaque : Attributes.opacity option -> unit -> 'constr t diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7866a52ff002..9d19a99673a8 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -60,7 +60,7 @@ module DefAttributes = struct using : Vernacexpr.section_subset_expr option; reversible : bool; clearbody: bool option; - opacity: bool option; + opacity: Attributes.opacity option; } (* [locality] is used for [vernac_definition_hook], the raw Local/Global attribute is also used to generate [scope]. diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index a9e2e11d1a0c..0a3ee8438e44 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -85,7 +85,7 @@ type t = { using : Vernacexpr.section_subset_expr option; reversible : bool; clearbody: bool option; - opacity: bool option; + opacity: Attributes.opacity option; } val def_attributes : t Attributes.attribute