Experiment the addition of sealed/defined attributes

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' ->

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

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 <https://github.com/coq/coq/pull/19029>`_,
+  by Hugo Herbelin).

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 (Attributes.Defined Conv_oracle.transparent)) () in
   let info = Declare.Info.make ~poly () in
-  Declare.declare_definition ~info ~cinfo ~opaque:false ~body sigma
+  Declare.declare_definition ~info ~cinfo ~body sigma

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

doc/sphinx/language/core/conversion.rst

@@ -142,8 +142,11 @@ or :term:`constants <constant>` defined in the :term:`global environment` with t
    E[Γ] ⊢ c~\triangleright_δ~t
 
 :term:`Delta-reduction <delta-reduction>` only unfolds :term:`constants <constant>` that are
-marked :gdef:`transparent`.  :gdef:`Opaque <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
 ~~~~~~~~~~~

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 <LocalInterpretationRulesForNotations>` 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`.
@@ -92,30 +106,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`.
+   In this case, the proof should normally be terminated with :cmd:`Defined`. See :ref:`proof-editing-mode`.
 
-   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` as well as the exclusive attributes :attr:`sealed`,
+   :attr:`opaque` and :attr:`transparent`.
 
    .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`.
 
@@ -128,10 +139,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 <tactic>`.
 Assertions cause Rocq to enter :term:`proof mode` (see :ref:`proofhandling`).
 Common tactics are described in the :ref:`writing-proofs` chapter.
@@ -152,20 +163,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 +185,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:
@@ -200,7 +212,14 @@ 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 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 using the :attr:`transparent` attribute or by ending
+the proof with :cmd:`Defined` in place of :cmd:`Qed`. We
+recommend using the attribute.
 
 .. note::
 
@@ -213,13 +232,40 @@ 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.
 
    #. 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, 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
+
+.. attr:: transparent
+
+.. attr:: opaque
+
+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.

doc/sphinx/language/core/inductive.rst

@@ -462,44 +462,47 @@ 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. 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, 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`.
 
    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<example_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

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
 

doc/sphinx/user-extensions/syntax-extensions.rst

@@ -468,6 +468,8 @@ Reserving notations
       the other. See :ref:`factorization <NotationFactorization>` for
       details.
 
+.. _simultaneous-definition-and-notation:
+
 Simultaneous definition of terms and notations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 

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: [

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: [