diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index d2efbff24e07..ed495f8a302b 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`. @@ -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 `. 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. 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 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~