Unifying the syntax of Theorem, Definition, Fixpoint, etc.

[Zimmi48]

Rendered

[SkySkimmer]

I think I would prefer Theorem (and Lemma etc) to be really an alias of Definition, ie when body is provided you get a transparent constant by default and have to use the attribute to get opacity for both Theorem and Definition.

[Zimmi48]

Thanks for this perspective! I hadn't considered it. I'll add it to the "alternatives" section for now.

[gares]

I like this.

Wrt the opaque attribute, you could have a sub attrite, eg opaque(tactics) or better unfold(37) or unfold(never), that is another attribute for the tactic level thing, as one could have simpl(never). In some sense, it may the good occasion to disambiguate, and use opaque only for the kernel notion of opacity

[Zimmi48]

And so aim to deprecate the Opaque / Transparent commands? What about the Hint Opaque / Hint Transparent ones?

[SkySkimmer]

And so aim to deprecate the Opaque / Transparent commands?

No, changing back and forth is still useful.

[JasonGross]

I am strongly in favor of this.
I especially like that I will now finally be able to use reduction expressions with fixpoints.

[JasonGross]

Is this going to cause confusion that we'll regret in the future?

[Zimmi48]

This is the question I'm asking in the "Unresolved questions" section.

[Blaisorblade]

IMVHO, I think qed and defined would be strictly better names in the current scenario.
Otherwise, please pick fresh words that can be used consistently, and make sense if coq/coq#3389 is accepted.

Ideally, technical terms and their meanings would be in a one-to-one mapping, absent strong reasons for a specific case.

[aspiwack]

To be entirely fair to @Zimmi48 , this confusion already exists. Qed makes things opaque, Defined makes thing transparent (that's all over the documentation, etc…). On the other hand Opaque makes things “sort-of opaque, somehow, a little, you know…” And this is where the confusion stems from.

And, frankly, #[qed] Definition is super esoteric.

I wonder what the cost would be to change Opaque and Transparent into more honest names instead?

[gares]

FTR at the coq call I heard seal and unseal, for flipping the "Qed opaque" status. We could then keep opacity(number) for the "other opacity".

[JasonGross]

Let me repeat again my call from six years ago to have more notions of opacity: coq/coq#3389
This is probably beyond the scope of this PR

[Zimmi48]

That's interesting and also echoes the comment of Enrico above. But yes, this is out of scope.

[Zimmi48]

It seems like the main questions to resolve will be about the opacity attribute(s).

Considering the suggestions by Enrico and Jason to extend the available opacity options, it would be great to ensure that whatever is decided is compatible with these views for the future of opacity.

Regarding the question of the default opacity (no attribute), is there any opposition to Gaëtan's suggestion for the default to always be transparent when a body is provided (even with the Theorem family)? I am starting to lean in this direction as well since it makes things even simpler to explain and remember.

[gares]

default to always be transparen

Are you saying that Theorem x : T. exact t. Qed is opaque but Theorem x : T := t. is transparent? Please no.

Theorems are opaque, Definitions are transparent. How can it be simpler than that?
And I'd take the occasion to disallow Defined to end a Theorem and Qed to end a Definition, making the opacity statically and consistently known at the beginning of the command (that is also where the attribute to alter the default would be).

[SkySkimmer]

This is dependent types, proof relevant theorems are normal.

[gares]

How does you proposal help wrt this?

[Zimmi48]

And I'd take the occasion to disallow Defined to end a Theorem and Qed to end a Definition, making the opacity statically and consistently known at the beginning of the command (that is also where the attribute to alter the default would be).

IIUC, in your proposal, the transparent or defined attribute would be required to end a Theorem with Defined (and conversely the opaque or qed attribute would be required to end a Definition with Qed). That would be a consistent choice with making the Theorem command with a body opaque by default. It would also mean not having to scroll to the end of the proof to check the opacity, which could be an advantage. However, I bet that this wouldn't please the HoTT people. A lesser version of this would be to create a warning (of the pedantic category) in case one ends a Theorem—without the opaque / qed attribute—with Defined. Then HoTT users could choose to disable this warning. This would be more consistent with the current flexibility of the language.

[gares]

No, I meant that Theorem ends with Qed and Definition with Defined. By default the first is opaque, the latter transparent. If you give #[opaque] to Definition you still have to end it with Defined (the attribute is supported by the command that begins the thing, not the terminator).

[gares]

Wrt HoTT-like users, I don't see how this CEP or the proposal of Gaetan helps.
They want things to be transparent, not a different syntax to make things transparent.
Am I missing something?

[tchajed]

I like this, too! In particular it adds a new feature of opaque theorems with explicit bodies using tactics-in-terms (last I checked Proof with ltac:(foo). doesn't work, and it's clunky regardless). This allows really concise theorems when they're generated systematically by automation, particularly when the statement itself can be generated by the automation.

I don't have a strong opinion on what to do about the various combinations, but I would like at least a recommendation on what sane developments should do to reduce the many options Coq gives. I sort of agree with @gares that Theorem foo := t being transparent is confusing. To me it's the difference between the explanation "theorems are opaque and definitions are transparent", as opposed to "explicit bodies are transparent and proof mode constructions are opaque unless terminated with Defined" (but with the caveat that Theorem and Definition are now truly synonymous).

[JasonGross]

Perhaps there should be options Set Default Theorem With Body Opaque (perhaps with a better name), and a similar option for Definition. And then we can document then uniformly (each kind of definition either looks to the theorem or to the definition setting), and differences are only a matter of default settings?

[JasonGross]

No, I meant that Theorem ends with Qed and Definition with Defined. By default the first is opaque, the latter transparent. If you give #[opaque] to Definition you still have to end it with Defined (the attribute is supported by the command that begins the thing, not the terminator).

@gares what should end Fixpoint? And what about Let?

[SkySkimmer]

proof mode constructions are opaque unless terminated with Defined

There's no default unlike what your phrasing implies.

I would just say "Theorem is the same as Definition, you can make the := form opaque with an attribute, proof mode opacity is according to how you end it"

[gares]

I'd say Defined since it is the most common case AFAIK.

[Zimmi48]

No, I meant that Theorem ends with Qed and Definition with Defined.

If we imposed this new view, this would be a pretty big change: everything in HoTT is currently Theorem + Defined. It would need to be changed to #[ transparent ] Theorem + Qed. That would also be confusing to everyone who was used to the meaning of Qed. While this could make sense for a new language, I feel like this is too radical for an evolution of an existing one. OTOH the proposal in #42 (comment) still makes things closer to your idealized view, while being less disruptive.

[Zimmi48]

More precisely @gares, here is a possible path to arrive to what you have in mind:

1. Provide new transparent / opaque attributes and Set Transparent Theorems flag. Deprecate the use of Defined for a theorem without the attribute nor the flag.

2. Turn the deprecation into a hard error. Now all Coq projects have either set the flag on, or are using the transparent attribute whenever they use Defined.

3. Make Qed and Defined synonyms. Opacity is controlled only by the attribute or the flag. Encourage the use of Qed for theorems and Defined for definitions. We never have to go beyond this step. Keeping the two things synonyms is in line with the philosophy of Coq (similar to having Parameter and Axiom synonyms but encouraging their usage in different cases).

Leaving several versions (but at the very least one) between each step should give people plenty of time to adapt. Providing a flag would ensure that HoTT people do not have a hard time because of this change.

[gares]

I like your plan. Somehow I recall I've seen hott files with Definition/Defined. I ve just checked a few and they look like that. Where did you see Theorem/Defined used extensively?

[Zimmi48]

Where did you see Theorem/Defined used extensively?

At least in UniMath there is a mix of Theorem + Qed and Theorem + Defined. I just assumed this was the same thing for HoTT.

[Zimmi48]

I've added the topic to today's call.

Regarding transparency attributes, one option that would be compatible with separating the transparency question from the Qed / Defined keywords and a larger spectrum of transparency levels would be:

• sealed for the current meaning of Qed
• transparent for the current meaning of Defined with the possibility of adding later sub-attributes to specify the precise level of transparency.

[Zimmi48]

The conclusion of the Coq Call is to go with the plan at #42 (comment) but with attributes sealed / unsealed to avoid any kind of confusion with the current Opaque / Transparent commands and the planned meaning of Qed / Defined (just a way to close a theorem / a definition regardless of its transparency). I'll integrate this plan in the CEP and then it will have to be largely advertised (Coq-Club, Discourse, Twitter?) before being definitely approved.

[ejgallego]

Sorry for missing the call today; it seems to me that removing the current mechanism will have a huge impact in terms of compat; on the other hand I don't see any technical advantage on knowing that a proof is opaque / transparent at proof opening time.

Thus IMO we may weight the cost/benefit ratio here.

[Zimmi48]

My own estimation of the cost of porting is "pretty small". Indeed, there will be the option of using the attribute selectively or the flag if all theorems in a file / project must be transparent. As for replacing Defined with Qed, this will never be forced upon the users since in the end they will become synonyms.

This is why I suggested this plan following Enrico's remarks. I wouldn't have proposed any plan that was strongly disruptive for little gain.

[ejgallego]

My own estimation of the cost of porting is "pretty small".

Well, just the amount of documentation / tutorials, stuff like SF that needs to be adapted seems to be more than "pretty small" to me; but my question really is "why"?

Changing the semantics of current code does not help with any problem I can see, on the contrary, that seems to me like a hack in order to workaround bugs in upper layers. As with the other interpretation restrictions I must stay on the technical view that lower layers should not add workarounds for problems in their clients.

[gares]

Note that the design does not require to change existing scripts. It happens that having consistent syntax and attributes one can make documents more coherent in their syntax. Should it become an error, a warning, or nothing, to have Definition end with Qed, is orthogonal to the core of this CEP.

I agree knowing early if a proof is opaque or not brings no advantage to Coq, as well as supporting := in Theorem is not going to change a users life. Having a uniform syntax and a uniform way to control opacity is just making things easier to explain.

[SkySkimmer]

Note that the design does not require to change existing scripts.

I don't see how that's possible, if Qed/Defined don't determine opacity you have to replace them somehow no?

[herbelin]

What about already implementing sealed and unsealed attributes? That does not look like a big deal and would provide an immediate gain.

(And if we want to go to massive renamings or deprecations, I don't realistically see how to avoid doing it using an automatic tool. As an example, there are already many warnings in the CI which are not addressed and I don't see how they could reasonably be all addressed manually.)

[SkySkimmer]

The idea of choosing sealedness based on if Theorem or Definition was used still feels quite bad to me. Maybe I'm too used to the current system but I do have 1 argument: currently to understand if something is sealed I need to remember the meaning of exactly 2 commands (Qed/Defined) but with this change I would need to know the sealedness of all of Theorem Definition Lemma Example etc

[ppedrot]

I agree with Gaëtan that we're spreading state around, and it's always annoying to have to reconciliate disagreeing states.

EDIT: and also, since we believe in Curry-Howard, this is making an artificial distinction between two identical concepts.

[silene]

As far as I am concerned, I do disagree. I think the head keyword should also be used to set the default sealing state, especially since there is no Qed/Defined tail keyword when the proof term is directly provided. Having Definition foo := ... and Theorem foo := ... be perfectly synonymous is a pointless feature for users like me.

[ppedrot]

But then how do we know about the ocean of weird "natural-language" keywords that we have in the implementation? And it becomes non-uniform w.r.t. other proof-starting commands like Instance.

[herbelin]

As a reference, I copy how About reports about sealedness/opacity:

let print_opacity env ref =
  match opacity env ref with
    | None -> []
    | Some s ->
       [pr_global ref ++ str " is " ++
        match s with
          | FullyOpaque -> str "opaque"
          | TransparentMaybeOpacified Conv_oracle.Opaque ->
              str "basically transparent but considered opaque for reduction"
          | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev ->
              str "transparent"
          | TransparentMaybeOpacified (Conv_oracle.Level n) ->
              str "transparent (with expansion weight " ++ int n ++ str ")"
          | TransparentMaybeOpacified Conv_oracle.Expand ->
              str "transparent (with minimal expansion weight)"]

This suggests that a less breaking alternative to sealed/unsealed could be fully_opaque/transparent, even more that Opaque/Transparent are attributes only of unsealed, so that, morally, there are not 4 but 3 statuses: fully opaque, opaque only for reduction, fully transparent. If we then accept to mix the kernel opacity and the reduction opacity in the attribute, it could also be, say:

• fully_opaque/reduction_opaque/transparent??
• opacity=full/opacity=reduction/opacity=transparent??
• opacity=sealed/opacity=opaque/opacity=transparent??
• opacity=sealed)/opacity=reduction)/opacity=transparent)??
• opacity(sealed)/opacity(reduction(level="1",expand,...)/opacity(transparent)??
• etc.

Also, for reference, there are options Set Transparent Obligations and Set Extraction AccessOpaque. which would have to be renamed accordingly.

[ppedrot]

I'm pretty much against this naming scheme because it mixes concepts at the kernel level (sealed vs. unsealed) that are part of the typing rules and heuristic concepts from the upper layers.

[ppedrot]

@silene to support our point, here is a list of definition tokens from the grammar. What are their expected sealedness? No cheating.

• Axiom
• Axioms
• Conjecture
• Conjectures
• Corollary
• Definition
• Example
• Fact
• Hypotheses
• Hypothesis
• Lemma
• Parameter
• Parameters
• Property
• Proposition
• Remark
• SubClass
• Theorem
• Variable
• Variables

[herbelin]

Sorry, there are parallel discussions and I'm replying here on "mixing two views": it is worrying me also but we also need to take care of common terminological usages in place (including in our own practice). We may try to change the About message and the options referring to opacity/transparency in the sealed sense but maybe there are less disruptive solutions that would contribute to cause neither a confusion between the concepts nor a confusion with the existing usages.

[herbelin]

Re: default sealedness. @SkySkimmer, @ppedrot: is your proposal that declarations using := (rather than some interactive proof) are unsealed by default, whatever keyword is used?

[SkySkimmer]

yes

[Zimmi48]

I'm not opposed to what Gaëtan and Pierre-Marie are arguing for, but here is a proposal for a compromise:

• We don't change the meaning of Qed / Defined with respect to opacity / sealedness. If a user uses Qed with a command that was expecting a Defined or conversely, Coq could accept it, but warn "overriding the default sealed / unsealed status for XXX command" or something like this. Maybe it could give an error instead of a warning if an explicit sealed / unsealed attribute has been used.
• In the case of the := form, we change the message that is printed to the user, so that the user doesn't have to know by heart which command does what. Currently, it says "Foo is defined", it would become "Foo is defined as unsealed / transparent" / "Foo is defined as sealed".

[SkySkimmer]

In the case of the := form, we change the message that is printed to the user, so that the user doesn't have to know by heart which command does what. Currently, it says "Foo is defined", it would become "Foo is defined as unsealed / transparent" / "Foo is defined as sealed".

I'd prefer being able to read the code without running it.

[ejgallego]

It seems to me that just adding general support for := for those commands that have bodies is good. I guess things should work like:

Default modalities:

• $logical_kind $name := $body.: by default not sealed, errors if $logical_kind doesn't accept a body.
• $logical_kind $name. Proof. $body_tac. Defined: Similar as above.
• $logical_kind $name. Proof. $body_tac. Qed: $name will be sealed, $body is put in opaquebodies and thanks to typing commands cannot read it.

If the command has an attribute, there are 3 cases:

• the command is of the shape Proof. ... {Qed,Defined}.: in this case, if the attribute agrees with the terminator, there is a warning (redundant attribute), if the attribute disagrees, error.
• the command is of the shape := $body: if the attributed is sealed, seal the definition (put in opaquebodies), otherwise warn for redundancy.

I am not sure how this would work, IMHO it is hard to predict more without going and implementing a proposal, and playing with it a bit. The good news is that I think declare.ml is in pretty good shape and doing something like the above shouldn't be a huge amount of work.

[ejgallego]

I share @silene 's pain point about Theorem $name := $body. not being sealed by default. As a user, I would like to have this syntax. Now that I remember, it was in fact the main motivation I think, to have a syntax of the := form that is sealed by default.

[ejgallego]

I just read the proposal again (congrats @Zimmi48 , great writing!), I am thinking that maybe we are trying to do too much.

IIRC the main motivation was to have Theorem foo := .... So maybe there are a couple of things to remove from the CEP:

• attributes: indeed, I'm not sure why they are useful here. Coq has inherit the non-uniformity of the syntax Definition / Theorem since a long time, so attributes would be only useful if we removed that distinction, but then what's the point of having so many synonyms?
• ability to override the defaults: that can be very confusing for others reading code! Do we have a real case for this customization to be needed?

[ejgallego]

I'm not sure if it was mentioned, but it would be nice if we could set what the default opacity for the Definition, Theorem, etc. keywords were. Currently in the HoTT library, we use Theorem, Definition etc. interchangeably with transparent bodies. They essentially serve as documentation.

But you cannot use Theorem foo := ... yet, so are you forced to emulate it?

I don't mind the default behaviour of Theorem being "sealed", as long as we can change it.

Yeah, that's one of the disadvantages of this approach :(

But at least, the proposed change wouldn't break your current code.

[Zimmi48]

Feature-wise, having the sealed attribute, combined with the existing Definition := syntax would be enough to achieve the initial proposal from this CEP.

However, another point of this CEP was to create more uniformity in the syntax. It is my opinion that Coq has too much "accidental" variability and we should strive to remove some. That's one of the motivations for the CEP. I'm also of the opinion that (real) synonyms are fine and consistent with the current "culture" of Coq (without the drawbacks of the accidental variability). That being said, the proposal of Pierre-Marie and Gaëtan is fully compatible with this vision, and therefore I'm also OK with their proposal.

I have no opinion about the value of knowing the transparency of a constant without executing the code. The proposal was indeed that Coq would only provide a default transparency for various commands, but that this could be tweaked. It is my impression that the same is currently true with other properties of definitions (if you don't know what options are activated, you won't fully know how the constant is defined)...

[herbelin]

PR coq/coq#19029 experiments adding sealed/unsealed attributes. Fully renouncing to the role of Qed/Defined for deciding opacity (as was sometimes discussed) would be quite disruptive. A simple possible rule is the following:

• #[sealed]/#[unsealed] take precedence over the presence of Qed/Defined or the presence of :=;
• in the absence of #[sealed]/#[unsealed], opacity is determined by the use Qed/Defined for interactive constants;
• in the absence of #[sealed]/#[unsealed], opacity is transparent for all non-interactive declarations currently using := (e.g. Definition/Fixpoint/CoFixpoint/Coercion/Instance ...).

It seems that the only real pending question is the default opacity to give to a future support of := for Theorem/Lemma/Proposition/Fact/Remark/Corollary/Property. I'm not worrying about remembering the default status if ever the default is opacity when using := with these 6 keywords, as this would be only and exactly for these 6 predefined "theorem-like" keywords, no more. Adopting that := implies transparency by default (even with those 6 keywords) makes also sense though.

[herbelin]

I don't know if it was mentioned in the discussion. To unify the syntax, we would also need a way to tell that a non-mutual Theorem is co/recursive without giving a struct (which is anyway not available if intended to be a cofixpoint). E.g. with:

#[recursive] Theorem f binders : type := body.

or

Recursive Theorem f binders : type := body.

This would then be applicable also to Instance (as in #7913), Coercion, Canonical Structure, ...

(Or maybe also adding #[recursive(fix)], #[recursive(cofix)] to be more specific.)

Added: another way would be to add a new variant of struct that tells it is corecursive (e.g. CoFixpoint f ctx := c would be expressed by Definition f ctx {cofix} := c).

[herbelin]

To satisfy the three needs given in the motivation of the CEP:

• to be able to define an opaque object without giving the type
• to be able to use Theorem with with only one recursive declaration
• to be able to use Theorem with Qed even for transparent theorems such as eq_sym (for pedagogy (**))

I propose to respectively eventually implement in coq/coq#19029 the following new attributes:

• #[sealed] Definition c := b
• #[recursive] Theorem c : t. ... (***)
• #[defined] Theorem c : t. ... Qed. (*)

The question of what would be the default opacity of Theorem c := b, if provided, did not lead to a consensus (some people primarily see the word "Theorem" and see it as opaque by default while other people primarily see the symbol ":=" and see it as transparent by default). The best solution is thus probably to renounce to provide this syntax.

(*) in the CEP, the keyword unsealed was proposed. The idea to use defined instead is somehow a new proposition I'm doing that looks less disruptive compared to the current status (that is: #[defined] tells to behave as a definition).

(**) pedagogy is also flexible: if really needed we can also explain why Coq does not follow the standard conventions.

(***) somehow, something is still missing to tell that a theorem which is guarded both inductively and coinductively should be considered as a cofixpoint; for that purpose, a fixannot {productive} could e.g. be provided.

Would someone be unhappy with this proposal?

[herbelin]

The part of the previous comment about sealed and defined is implemented in coq/coq#19029.
The syntax unification supporting Theorem c : T := t is in coq/coq#19301.