Slightly rewording the documentation of Theorem, Definition and Fixpoint by herbelin · Pull Request #19766 · rocq-prover/rocq

herbelin · 2024-10-26T15:00:21Z

This PR is preparing the changes of documentation in #19029 and #19301, to split general concerns from specific concerns and so that either of the two PR can be merged independently.

Added / updated documentation.

jfehrle

Wording suggestions.

I hope you can make this more succinct as I suggest. I may well have gotten some of the details wrong--please ignore/adapt those parts.

jfehrle · 2024-10-26T18:22:09Z

+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.


Suggested change

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.

A theorem is a statement with a proof. The statement of the theorem

is a type. The proof derives a term that has that type. References to the

theorem may use its term or type, depending on the context.

IMO this should clearly and succinctly state what a theorem is.

What do you mean by "References to the theorem may use its term or type, depending on the context."? Otherwise ok.

I think it is also worth to insist somewhere that Definition and Theorem are just two different views at the same kind of syntactic object.

What do you mean by "References to the theorem may use its term or type, depending on the context."? Otherwise ok.

What I meant was if you apply the theorem, the type of the theorem is used. Print theorem will show both. Maybe my thinking is still fuzzy, feel free to drop the sentence.

I think it is also worth to insist somewhere that Definition and Theorem are just two different views at the same kind of syntactic object.

Yes, a good point. I tend to forget the case where the user has to provide a proof for the Definition.

I hope you'll at least use the first three sentences I suggest here. IMO short and sweet.

What I meant was if you apply the theorem, the type of the theorem is used.

The proof also is also used, in some sense. If your theorem is, say, {x : nat & x > 1} and you use this statement to eventually compute an actual nat bigger than 1, this nat is found in the proof that you applied (and it can be 2, or 3, etc. depending on the proof you give).

Maybe my thinking is still fuzzy, feel free to drop the sentence.

I would say that it is the standard usage which is ambiguous. Syntactically, there is no difference between a proof of some statement and a term of some type, that is when you apply a theorem, what you syntactically do is to apply the proof. However, in the case of a pair proof/statement, the focus is on the statement and we usually intend that the exact proof does not matter (and thus use Qed to enforce that), while in the case of a pair term/type, the focus is on the term and the type is intended to be an auxiliary re-derivable information. (Don't know if this explanaton helps.)

Syntactically, there is no difference between a proof of some statement and a term of some type, that is when you apply a theorem, what you syntactically do is to apply the proof.

When you apply a theorem, the theorem name is inserted into the proof term of Show Proof. I expect Qed doesn't later recheck the referenced theorem--right?

jfehrle · 2024-10-26T18:25:40Z

+
+Moreover, definitions can be local (defined with :g:`let`) or global
+(defined at top-level).


Suggested change

Moreover, definitions can be local (defined with :g:`let`) or global

(defined at top-level).

Moved this text to the first paragraph

jfehrle · 2024-10-26T19:24:41Z

+   In its most basic form :g:`Definition @ident := term`, the command
+   binds :n:`@term` to the name :n:`@ident` in the global environment,
+   provided that :n:`@term` is well-typed.
+
+   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`
+   (and similarly when one of `@term` or `@type` is omitted).
+


Suggested change

In its most basic form :g:`Definition @ident := term`, the command

binds :n:`@term` to the name :n:`@ident` in the global environment,

provided that :n:`@term` is well-typed.

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`

(and similarly when one of `@term` or `@type` is omitted).

The command

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 @binder is specified, the definition is equivalent to

:n:`Definition @ident : forall {* @binder }, @type := fun {* @binder } => @term`

(and similarly when one of `@term` or `@type` is omitted).

We prefer describing the behavior of each bit of the syntax separately rather than listing multiple similar forms. It's easier for readers, who don't have to read a lot of very similar text and mentally do a diff to figure out what each bit of the syntax does.

"and registers :n:@ident as being of type :n:@type, and bound to value :n:@term" -- what is this registration? Seems like implementation detail that the user probably doesn't need to know about.

We prefer describing the behavior of each bit of the syntax separately rather than listing multiple similar forms.

My bad, I anticipated too much. In #19301, Definition will take a with clause and we will have to take into account that there are potentially several ident/term pairs in a same Definition.

In the meantime, I reverted this part.

jfehrle · 2024-10-26T19:35:17Z

+   In its most basic form :g:`@thm_token @ident : @type`, the command
+   interprets :n:`@type` as a statement and waits for a
+   proof. Once a proof is given and validated, a theorem bound to
+   :n:`@ident` and stating :n:`@type` is added to the global
+   environment.

-   These commands accept the :attr:`program` attribute.  See :ref:`program_lemma`.
+   The form :n:`@thm_token @ident {* @binder } : @type := @term` is
+   equivalent to :n:`@thm_token @ident : 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


As in the description of Definition, can we describe each syntactic item separately rather than listing multiple similar forms?

I thought that the simpler form was easier to understand than the general uncommon form, but I'm ok to consider the general form from the very beginning.

jfehrle · 2024-10-26T19:40:27Z

+   constraints on a special argument called the decreasing argument. This
+   is needed to ensure that the :cmd:`Fixpoint` definition always terminates.


Shouldn't this remain plural to match "constraints"?

OK, so let's put constraints singular.

jfehrle · 2024-10-26T19:41:50Z

-   :cmd:`Fixpoint` without the :attr:`program` attribute does not support the
-   :n:`wf` or :n:`measure` clauses of :n:`@fixannot`. See :ref:`program_fixpoint`.


This seems like useful info--did you intend to drop it?

It is moved in the attribute paragraph.

jfehrle · 2024-10-26T19:43:53Z

      only through their fully qualified names rather than their
-      unqualified names after an :cmd:`Import`.
+      unqualified names, even after an :cmd:`Import`.


"rather than their unqualified names" seems like overkill if the previous clause says "only through their unqualified names"

…int. Also adding some missing supported attributes.

herbelin

Thanks for the review. I pushed a new version.

Besides the new changes, hoping I don't forget anything, the pending open questions are:

To what a theorem name refers?
How to explain the similarity between Definitions and Theorems?

herbelin · 2024-10-27T05:24:51Z

+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.


What do you mean by "References to the theorem may use its term or type, depending on the context."? Otherwise ok.

I think it is also worth to insist somewhere that Definition and Theorem are just two different views at the same kind of syntactic object.

herbelin · 2024-10-27T05:25:03Z

+
+Moreover, definitions can be local (defined with :g:`let`) or global
+(defined at top-level).


herbelin · 2024-10-27T05:35:45Z

+   In its most basic form :g:`Definition @ident := term`, the command
+   binds :n:`@term` to the name :n:`@ident` in the global environment,
+   provided that :n:`@term` is well-typed.
+
+   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`
+   (and similarly when one of `@term` or `@type` is omitted).
+


We prefer describing the behavior of each bit of the syntax separately rather than listing multiple similar forms.

My bad, I anticipated too much. In #19301, Definition will take a with clause and we will have to take into account that there are potentially several ident/term pairs in a same Definition.

In the meantime, I reverted this part.

herbelin · 2024-10-27T05:46:55Z

+   constraints on a special argument called the decreasing argument. This
+   is needed to ensure that the :cmd:`Fixpoint` definition always terminates.


OK, so let's put constraints singular.

herbelin · 2024-10-27T05:47:23Z

-   :cmd:`Fixpoint` without the :attr:`program` attribute does not support the
-   :n:`wf` or :n:`measure` clauses of :n:`@fixannot`. See :ref:`program_fixpoint`.


It is moved in the attribute paragraph.

herbelin · 2024-10-27T05:47:52Z

      only through their fully qualified names rather than their
-      unqualified names after an :cmd:`Import`.
+      unqualified names, even after an :cmd:`Import`.


herbelin · 2024-10-27T06:12:37Z


-   This command accepts the :attr:`bypass_check(universes)`,
-   :attr:`bypass_check(guard)`, :attr:`deprecated`, :attr:`warn`, and :attr:`using` attributes.
+   The command supports the :attr:`local`, :attr:`universes(polymorphic)`,


I proposed a solution which does not use the word "command".

jfehrle

A few further suggestions. It gets harder to read the changes after the first round of comments.

Hope you'll revise the introductory paragraph on Theorem.

jfehrle · 2024-10-30T19:05:46Z

+
+Definitions associate a specified term with a given name. The name can later
+be replaced with its definition through :term:`δ-reduction <delta-reduction>`.


Suggested change

Definitions associate a specified term with a given name. The name can later

be replaced with its definition through :term:`δ-reduction <delta-reduction>`.

Definitions and theorems are used to define terms that have a specific type.

Definitions most commonly associate a specified term with a given name.

Alternatively, the type may be specified instead of the term, in which case, a proof

must be provided to derive the term just as for theorems. The name can later

be replaced with its definition through :term:`δ-reduction <delta-reduction>`.

The first sentence suggests they are similar. Details of their differences should go later
where Definition syntax is given (e.g. opacity and that specifying both term and type
will verify that they match). N'est-ce pas?

jfehrle · 2024-10-30T19:07:50Z

+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.


I hope you'll at least use the first three sentences I suggest here. IMO short and sweet.

jfehrle · 2024-10-30T19:14:18Z

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


Suggested change

This binds :n:`@term` to the name :n:`@ident` in the global environment,

Binds :n:`@term` to the name :n:`@ident` in the global environment,

jfehrle · 2024-10-30T19:18:03Z

+   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`.


Suggested change

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:`@binder` is specified, :n:`@term` and :n:`@type` are treated as if they had

respectively been given as :n:`fun {* @binder } => @term` and :n:`forall {* @binder }, @type`.

"distributes" suggest to me a reference to a distributive property, which IINM is not the case--it just has its everyday meaning.

jfehrle · 2024-10-30T19:21:22Z

+   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 }`.


Suggested change

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 }`.

If :n:`@binder` is specified, :n:`@type` is used as

:n:`forall {* @binder }, @type` and the proof starts in the context :n:`{* @binder }`.

"behaves" is vague; better just to state the behavior

jfehrle · 2024-10-30T19:24:04Z

+   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`.


Suggested change

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`.

The form :n:`Fixpoint @ident {* @binder} { struct @ident } : @type := @term.

declares :n:`@ident` as a recursive function with arguments

:n:`{* @binder}` and body :n:`@term` of type :n:`type`.

jfehrle · 2024-10-30T19:27:11Z

+   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.


And fails if none of the arguments satisfy the condition.

jfehrle · 2024-10-30T19:31:18Z

+   If :n:`@decl_notation` is present, a notation is defined at the same time
+   (see :ref:`simultaneous-definition-and-notation`).


I don't understand why defining a notation is useful enough to be included in Fixpoint syntax. IINM is could also be done with a separate command. Perhaps a very short example would help.

Villetaneuse · 2025-06-07T08:44:38Z

@herbelin @jfehrle Where are we with this PR?

coqbot-app · 2025-08-27T02:31:47Z

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

coqbot-app · 2025-09-29T02:32:39Z

This PR was not rebased after 30 days despite the warning, it is now closed.

herbelin added the kind: documentation Additions or improvement to documentation. label Oct 26, 2024

herbelin added this to the 9.0+rc1 milestone Oct 26, 2024

herbelin requested a review from a team as a code owner October 26, 2024 15:00

coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Oct 26, 2024

herbelin mentioned this pull request Oct 26, 2024

Experiment the addition of sealed/defined attributes #19029

Closed

4 tasks

jfehrle reviewed Oct 26, 2024

View reviewed changes

Reworking slightly the documentation of Definition, Theorem and Fixpo…

e8f4978

…int. Also adding some missing supported attributes.

herbelin force-pushed the master+rewording-doc-theorem-definition branch from 10d1810 to 9584899 Compare October 27, 2024 08:39

herbelin commented Oct 27, 2024

View reviewed changes

herbelin mentioned this pull request Oct 27, 2024

Unifying the syntax of Definition, Theorem, Fixpoint and CoFixpoint (CEP #42) #19301

Closed

4 tasks

Rewording the structure of the documentation of Definition/Theorem.

697d347

herbelin force-pushed the master+rewording-doc-theorem-definition branch from 9584899 to 697d347 Compare October 28, 2024 10:12

herbelin removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Oct 28, 2024

jfehrle reviewed Oct 30, 2024

View reviewed changes

ppedrot modified the milestones: 9.0+rc1, 9.1+rc1 Dec 26, 2024

SkySkimmer added the needs: fixing The proposed code change is broken. label Jan 23, 2025

github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Apr 2, 2025

SkySkimmer removed this from the 9.1+rc1 milestone Jun 6, 2025

coqbot-app Bot added the stale This PR will be closed unless it is rebased. label Aug 27, 2025

coqbot-app Bot closed this Sep 29, 2025


		Moreover, definitions can be local (defined with :g:`let`) or global
		(defined at top-level).

		constraints on a special argument called the decreasing argument. This
		is needed to ensure that the :cmd:`Fixpoint` definition always terminates.

		:cmd:`Fixpoint` without the :attr:`program` attribute does not support the
		:n:`wf` or :n:`measure` clauses of :n:`@fixannot`. See :ref:`program_fixpoint`.


		Definitions associate a specified term with a given name. The name can later
		be replaced with its definition through :term:`δ-reduction <delta-reduction>`.

-Definitions associate a specified term with a given name. The name can later
-be replaced with its definition through :term:`δ-reduction <delta-reduction>`.
+Definitions and theorems are used to define terms that have a specific type.
+Definitions most commonly associate a specified term with a given name.
+Alternatively, the type may be specified instead of the term, in which case, a proof
+must be provided to derive the term just as for theorems. The name can later
+be replaced with its definition through :term:`δ-reduction <delta-reduction>`.

	This binds :n:`@term` to the name :n:`@ident` in the global environment,
	Binds :n:`@term` to the name :n:`@ident` in the global environment,

		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:`@binder` is specified, this behaves as if :n:`@type` had been
		:n:`forall {* @binder }, @type` and the proof starts in the context :n:`{* @binder }`.

		If :n:`@decl_notation` is present, a notation is defined at the same time
		(see :ref:`simultaneous-definition-and-notation`).

Uh oh!

Conversation

herbelin commented Oct 26, 2024

Uh oh!

jfehrle left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

herbelin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jfehrle left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jfehrle Oct 30, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jfehrle left a comment •

edited

Loading

jfehrle Oct 30, 2024 •

edited

Loading

jfehrle Oct 30, 2024 •

edited

Loading

jfehrle Oct 30, 2024 •

edited

Loading