Slightly rewording the documentation of Theorem, Definition and Fixpoint

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 <delta-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,26 @@ 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`.
+   In this case, the proof should normally be terminated with :cmd:`Defined`. 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`.
 
@@ -128,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 <tactic>`.
 Assertions cause Rocq to enter :term:`proof mode` (see :ref:`proofhandling`).
 Common tactics are described in the :ref:`writing-proofs` chapter.
@@ -152,20 +162,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 +184,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 +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::
 
@@ -213,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.
 

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