Experiment the addition of sealed/defined attributes by herbelin · Pull Request #19029 · rocq-prover/rocq

herbelin · 2024-05-15T12:28:59Z

The PR experiments the implementation of a proposal related to rocq-prover/rfcs#42. It adds attributes sealed and defined that allow to indicate the opacity of a definition defined non-interactively.

When used in an interactive proof, sealed and defined take precedence over Qedand Defined. Consequently, using an attribute in interactive mode allows to match Definition with Defined and Theorem with Qed without impacting the opacity (since it is the attribute which takes precedence).

In non-interactive mode, a Definition is declared defined in the absence of an atttribute while Theorem mandatorily requires an attribute (however, the syntax Theorem :=itself is eventually provided only in #19301).

The main technical change is that the "opaque" value is now part of the Declare.CInfo.t while it was before passed as a standalone argument or stored in the program obligation state.

Here are some examples:

#[sealed] Definition c := 0.
#[defined] Theorem t : nat. exact 0. Defined.
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.

Added / updated test-suite.
Added changelog.
Added / updated documentation.

Pending questions:

sealed/defined attributes only in front of names (as in Fixpoint #[sealed] foo ...) or also in front of commands (as in #[sealed] Fixpoint foo ...) [but easier to done once Unifying the syntax of Definition, Theorem, Fixpoint and CoFixpoint (CEP #42) #19301 is merged]: now added also in front

Depends on:

proux01 · 2024-05-31T09:09:13Z

Draft PR, removing the milestone.

herbelin

Thanks for the comments

herbelin · 2024-10-22T13:20:17Z

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


Yes, but we are talking here about definitions and Qed is unusual both in mathematical practice and in Coq scripts.

herbelin · 2024-10-22T13:21:18Z

+---------------------------
+
+Definitions and theorems associate terms of some type to a name. In
+the case of a definition (or assimilated, like :cmd:`Fixpoint` or


herbelin · 2024-10-22T13:37:25Z

+Definitions and theorems associate terms of some type to a name. In
+the case of a definition (or assimilated, like :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 (or
+assimilated), the term is the proof and the type is the statement.


I moved the paragraph at the beginning of the section. Tell me what you think about it.

I did not rephrase it though because it is important I think to let open the idea that a definition can be build by tactics and a proof as a term.

herbelin · 2024-10-22T13:41:59Z

+   This attribute tells to prevent the unfoldability of a definition,
+   so that the definition behaves like an abstract definition.


I don't know what happend in my mind when I wrote the comment.

What I want to say is that it is more than preventing unfolding (which Opaque does in some sense). In the absence of a better choice, I reused "prevents the unfoldability of a definition".

herbelin · 2024-10-22T13:43:16Z

   This command accepts the :attr:`program`,
   :attr:`bypass_check(universes)`, and :attr:`bypass_check(guard)` attributes.
+   It also accepts the :attr:`sealed` attribute placed just before the
+   name (or names) defined by the fixpoint.


herbelin · 2024-10-22T13:44:10Z

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


herbelin · 2024-10-22T13:44:13Z

 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
 ]


…in module parameter.

…int. Also adding some missing supported attributes.

…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 rocq-prover#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)

Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com> Co-Authored-By: Zimmi48 <Zimmi48@users.noreply.github.com>

… mode.

…ation.

…sparent.

herbelin · 2024-10-27T09:02:24Z

In answer to your remaining todo, yes, I think it makes sense to support the attribute both before the command itself or before the constant names. In case it is before the command, the same sealedness should apply to all defined constants. If it is in front of the name of the constant, it allows being more fine-grained. Obviously, we should error if these are inconsistent.

Done.

Either, we want to have two separate notions: transparent vs opaque / defined vs sealed. Or we think that this is a continuum worth presenting as such. Then no need for the word defined, the attributes could be named transparent, opaque and sealed.

I added a commit experimenting this (to be eventually squashed if we adopt it).

jfehrle · 2024-10-29T19:06:59Z

+  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


Suggested change

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

Attributes :attr:`sealed` and :attr:`defined` to set

the opacity of a definition or theorem. :attr:`sealed` makes the object

immutably opaque, unlike the :cmd:`Opaque` command, which makes

an object mutably opaque

Some of the wording was not idiomatic
Also "the confusion with the notion of opacity" doesn't tell you what the difference in notions is, so vague

coqbot-app · 2024-11-28T02:30:48Z

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 · 2024-12-30T02:27:44Z

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

herbelin added kind: feature New user-facing feature request or implementation. part: attributes #[attributes] modify the behaviour of vernac sentences. part: gallina The gallina commands labels May 15, 2024

herbelin added this to the 8.20+rc1 milestone May 15, 2024

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 May 15, 2024

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

herbelin force-pushed the master+sealed-attribute branch from b5d663f to e3c91ca Compare May 17, 2024 15:57

coqbot-app Bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label May 17, 2024

herbelin force-pushed the master+sealed-attribute branch from e3c91ca to 3e40fa2 Compare May 17, 2024 16:01

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

herbelin mentioned this pull request May 26, 2024

Better integration of Derive in declare.ml + fix of #18951 #19092

Merged

3 tasks

proux01 removed this from the 8.20+rc1 milestone May 31, 2024

herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 18, 2024

herbelin force-pushed the master+sealed-attribute branch from 3e40fa2 to f881a75 Compare June 18, 2024 19:27

herbelin marked this pull request as ready for review June 18, 2024 19:27

herbelin requested review from a team as code owners June 18, 2024 19:27

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

herbelin force-pushed the master+sealed-attribute branch from f881a75 to 6b63e32 Compare June 22, 2024 10:12

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 Jun 22, 2024

herbelin commented Oct 22, 2024

View reviewed changes

andres-erbsen mentioned this pull request Oct 23, 2024

ZModOffet: theory Z.modulo with range offset to ZArith #19753

Closed

1 task

This was referenced Oct 25, 2024

Refine description of "About" and mention transparency. #19716

Merged

Slightly rewording the documentation of Theorem, Definition and Fixpoint #19766

Closed

herbelin and others added 21 commits October 27, 2024 09:47

Fixes rocq-prover#19767: anomaly when printing functor with Strategy …

6cb44b4

…in module parameter.

Reworking slightly the documentation of Definition, Theorem and Fixpo…

c248044

…int. Also adding some missing supported attributes.

Rewording the structure of the documentation of Definition/Theorem.

ccba976

Is OblState.view still used?

7c379f1

Adding List.map5.

8471db8

Using the word "sealed" in About.

603a7f8

Documenting attributes sealed and defined.

a21cd6a

Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com> Co-Authored-By: Zimmi48 <Zimmi48@users.noreply.github.com>

Assigning kind Theorem rather than Definition to Goal.

aaa4c5a

Using Lemma instead of Definition for opaque structures.

d2411ee

Using #[sealed] for opaque proofs of Compare.

aa4cada

Using #[sealed] for opaque instances.

3cebc64

Using #[sealed] for opaque morally-relevant definitions.

3d16d75

Using #[sealed] for opaque morally-relevant definitions in test-suite.

a35abec

Using #[sealed] for opaque fixpoints.

b4ae67e

Using #[sealed] for opaque Example.

2dda694

Take Theorem/Definition into account to decide opacity in interactive…

99f69d6

… mode.

Change log for rocq-prover#19029

dc4ce6f

Renaming proof ending Opaque->Qed, Transparent->Defined in Vernacexpr.

b23f8e8

Attempt to clarify role of Qed/Defined proof ending in opacity comput…

afb1376

…ation.

Replace binary sealed/defined attribute by ternary sealed/opaque/tran…

3076d12

…sparent.

ppedrot mentioned this pull request Oct 29, 2024

Refine Hint Opaque/Transparent documentation #19761

Merged

1 task

jfehrle reviewed Oct 29, 2024

View reviewed changes

Navigation Menu

Uh oh!

Experiment the addition of sealed/defined attributes - #19029

Experiment the addition of sealed/defined attributes#19029
herbelin wants to merge 21 commits into
rocq-prover:masterfrom
herbelin:master+sealed-attribute

herbelin commented May 15, 2024 •

edited

Loading

Uh oh!

proux01 commented May 31, 2024

Uh oh!

herbelin left a comment

Uh oh!

herbelin Oct 22, 2024

Uh oh!

herbelin Oct 22, 2024

Uh oh!

herbelin Oct 22, 2024

Uh oh!

herbelin Oct 22, 2024

Uh oh!

herbelin Oct 22, 2024

Uh oh!

herbelin Oct 22, 2024

Uh oh!

herbelin Oct 22, 2024

Uh oh!

herbelin commented Oct 27, 2024

Uh oh!

jfehrle Oct 29, 2024

Uh oh!

coqbot-app Bot commented Nov 28, 2024

Uh oh!

coqbot-app Bot commented Dec 30, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

		This attribute tells to prevent the unfoldability of a definition,
		so that the definition behaves like an abstract definition.

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

Uh oh!

Conversation

herbelin commented May 15, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

proux01 commented May 31, 2024

Uh oh!

herbelin left a comment

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!

herbelin commented Oct 27, 2024

Uh oh!

Choose a reason for hiding this comment

Uh oh!

coqbot-app Bot commented Nov 28, 2024

Uh oh!

coqbot-app Bot commented Dec 30, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

herbelin commented May 15, 2024 •

edited

Loading