Well-bracketing of Proof-Qed blocks · Coq devs & plugin devs

Stream: Coq devs & plugin devs

Topic: Well-bracketing of Proof-Qed blocks

Pierre-Marie Pédrot (May 18 2022 at 09:17):

I remember this being discussed somewhere but I can't find it: weren't we supposed at some point to enforce that people start their proofs with the Proof command?

Pierre-Marie Pédrot (May 18 2022 at 09:18):

At the very least we should have a warning, but AFAICT it doesn't exist yet.

Guillaume Melquiond (May 18 2022 at 09:21):

Pierre-Marie Pédrot said:

I remember this being discussed somewhere but I can't find it: weren't we supposed at some point to enforce that people start their proofs with the Proof command?

That does not ring a bell. What would be the point? Not putting Proof (especially after Definition) is not an indication that the user is likely to have made a mistake and thus is worth warning about.

Guillaume Melquiond (May 18 2022 at 09:21):

I am against warning messages whose sole purpose is to aggravate users.

Pierre-Marie Pédrot (May 18 2022 at 09:23):

it's a mistake in so far as it makes proof scripts brittle

Pierre-Marie Pédrot (May 18 2022 at 09:24):

Coq can't decide if a proof is opened there a priori

Guillaume Melquiond (May 18 2022 at 09:29):

Are you talking about Instance or are you talking about something else? If you want to make Proof mandtory after Instance, then fine with me.

Gaëtan Gilbert (May 18 2022 at 09:30):

what's different about instance?

Pierre-Marie Pédrot (May 18 2022 at 09:31):

Proof should be mandatory every time we enter the proof mode, to statically check this. This is important for UIs.

Pierre-Marie Pédrot (May 18 2022 at 09:31):

(and not only UIs if one day we manage to make coqc itself more parallel)

Pierre-Marie Pédrot (May 18 2022 at 09:32):

it's explicitly recommended in the doc that one should start their proofs with the Proof keyword.

Guillaume Melquiond (May 18 2022 at 09:32):

No, this is not important. The current syntax of Lemma and the like is unambiguous.

Pierre-Marie Pédrot (May 18 2022 at 09:32):

we're dragged back precisely because of that.

Pierre-Marie Pédrot (May 18 2022 at 09:33):

Are you seriously claiming that you don't wrap your proofs with Proof - Qed already?

Pierre-Marie Pédrot (May 18 2022 at 09:34):

even if this were only about style, there are decent languages that are more authoritarian about style

Guillaume Melquiond (May 18 2022 at 09:34):

No, read carefully my first reply. I am claiming that I do not wrap my definitions with Proof. Defined.

Pierre-Marie Pédrot (May 18 2022 at 09:35):

Same issue.

Pierre-Marie Pédrot (May 18 2022 at 09:35):

You're entering proof mode, this should be statically recognized.

Guillaume Melquiond (May 18 2022 at 09:35):

But this is statically recognized!

Pierre-Marie Pédrot (May 18 2022 at 09:36):

Not if you have the refine mode around.

Guillaume Melquiond (May 18 2022 at 09:36):

I do not know what you are talking about. Please show me an example that currently cannot be statically recognized.

Pierre-Marie Pédrot (May 18 2022 at 09:38):

hmm, the refine instance mode was removed indeed.

Pierre-Marie Pédrot (May 18 2022 at 09:39):

ok, maybe this was solved since then, but there is still the style issue.

Pierre-Marie Pédrot (May 18 2022 at 09:39):

(not mentioning making the parsing harder, but not sure what @Maxime Dénès is up to these days)

Guillaume Melquiond (May 18 2022 at 09:41):

Gaëtan Gilbert said:

what's different about instance?

I was under the impression that Instance could silently create proof obligations. But perhaps I am misremembering.

Gaëtan Gilbert (May 18 2022 at 09:44):

obligations need the obligaton commands to open

Guillaume Melquiond (May 18 2022 at 09:49):

I did not mean this kind of obligations; I was just talking about missing proof terms. It seemed to me that you could provide a half-baked instance and Coq would query for the missing parts. But it seems like the attribute #[refine] is now needed to enable this behavior.

Pierre-Marie Pédrot (May 18 2022 at 09:52):

I'm not sure why you're insisting that Proof. Defined. should be treated any different from Proof. Qed. though...

Pierre-Marie Pédrot (May 18 2022 at 09:53):

if we follow the static classification argument we could even get rid of Proof altogether.

Guillaume Melquiond (May 18 2022 at 09:54):

Sure, I am fine with keeping only Proof using and Proof with.

Gaëtan Gilbert (May 18 2022 at 10:21):

Proof is useful for scripts which operate on scripts, eg "go back to the last Proof and add using" because then they don't have to know which commands (including from plugins) may open proofs

Karl Palmskog (May 18 2022 at 10:22):

Proof. is used by several documentation tools to indicate that something can be folded (people don't usually care about proof scripts, but they want the option to view on command). It also makes .v files more readable, when there is a clear demarcation between statement/type and body/script. Please keep the possibility to have Proof..

Pierre-Marie Pédrot (May 18 2022 at 10:25):

(In case this is not clear, I am still advocating for a mandatory Proof statement.)

Karl Palmskog (May 18 2022 at 10:35):

I would personally like to see Proof mandated or warned about during absence. But even adding a manually activated way to get a warning would also be great (compare to mangling of names)

Maxime Dénès (May 18 2022 at 11:03):

Yes, the refine instance mode was removed, so that deciding whether a command opens a proof or not no longer depends on typing and unification...

Maxime Dénès (May 18 2022 at 11:05):

One bias I often see in these discussions is we tend to discuss whether making things simpler is really necessary, or if we'd be capable of dealing with the complexity. IMHO we should turn the table. Simplicity should be the default.

Ali Caglayan (May 18 2022 at 11:06):

Nobody should have to care which commands open proofs IMO. A proof should sit between a Proof. and a Defined. or Qed. making life simpler for everybody who isn't a Coq expert.

Maxime Dénès (May 18 2022 at 11:06):

Now the real question is probably how we manage the change w.r.t. our users. It could be a better experience for them to be given a whole new version of the vernac language based on a simple approach, rather than having to deal with incremental changes, one warning at a time.

Maxime Dénès (May 18 2022 at 11:07):

But I'm afraid it would require some technical coordination and planning :)

Pierre-Marie Pédrot (May 18 2022 at 11:08):

I'm not sure there is any change in making Proof mandatory. That's already the implicit norm.

Maxime Dénès (May 18 2022 at 11:09):

It should be noted that we are not just talking about minor cosmetic aspect of the language. It seems pretty clear that vernac was not designed to be as simple and lean as possible. On the contrary, it was made to look close to natural languages, providing a lot of synonyms or closely related concepts, etc.

Maxime Dénès (May 18 2022 at 11:10):

I'm not sure what would be the point of making Proof mandatory in isolation from a more global redesign of the language. Like the treatment of keywords, Fixpoint vs Definition := fix, etc etc

Maxime Dénès (May 18 2022 at 11:11):

In particular, it does not sound crazy to have two flavors of the language. One which is closer to a programming language and another which is closer to a natural language (if it is still an active line of research).

Gaëtan Gilbert (May 18 2022 at 11:11):

Fixpoint vs Definition := fix

WDYM?

Maxime Dénès (May 18 2022 at 11:13):

Separating the two aims would help us avoid the current situation where almost every construction of the language is sitting somewhere between incompatible constraints, with a clear lack of uniformity of the whole.

Karl Palmskog (May 18 2022 at 11:14):

from user and Platform side, I think we'd rather see piecewise changes to the vernacular language than big redesigns

Maxime Dénès (May 18 2022 at 11:15):

Interesting. I was expecting people to want to have control on when they switch, rather than having to port and fix warnings when a new Coq version is released. But from the developer side, it is of course easier to do it incrementally.

Maxime Dénès (May 18 2022 at 11:17):

Gaëtan Gilbert said:

Fixpoint vs Definition := fix

WDYM?

I mean that when I study the Rust documentation and then look at basic constructions, I don't find stuff like this: https://github.com/coq/coq/blob/master/theories/Init/Datatypes.v#L327 :)

Pierre-Marie Pédrot (May 18 2022 at 11:19):

I'm pretty sure length is written that way to work around the guard condition

Pierre-Marie Pédrot (May 18 2022 at 11:20):

for nested inductive types it's important that parameters are outside of the fixpoint

Pierre-Marie Pédrot (May 18 2022 at 11:21):

dependent types are hard and I don't think it's reasonable to merge Fixpoint and Definition + fix

Pierre-Marie Pédrot (May 18 2022 at 11:22):

remember the (currently still unfolding under our eyes) fiasco of the "compatibility" layer for primitive projections? Yet another instance where trying to hide real complexity under the rug resulted in sever headaches.

Gaëtan Gilbert (May 18 2022 at 11:23):

does rust really not have some funky stuff to deal with lifetimes somewhere?

Maxime Dénès (May 18 2022 at 11:27):

They do, of course, it's also not simple, that's why I took this example. But it feels more progressive.

Maxime Dénès (May 18 2022 at 11:28):

Pierre-Marie Pédrot said:

dependent types are hard and I don't think it's reasonable to merge Fixpoint and Definition + fix

There's no dependent types in list and length, is there?

Gaëtan Gilbert (May 18 2022 at 11:28):

(A:Type)

Maxime Dénès (May 18 2022 at 11:29):

That was called polymorphism when I was young

Pierre-Marie Pédrot (May 18 2022 at 11:30):

@Maxime Dénès there are dependent types everywhere in a statement using length

Pierre-Marie Pédrot (May 18 2022 at 11:31):

if you take into account the fact that basically the spec of a library for tactics is the literal syntax (not even quotienting by α-conversion!) we're pretty much screwed

Maxime Dénès (May 18 2022 at 11:31):

Ah yes, in statements. But I don't see why we could not have the Fixpoint vernac do the right thing on the length example.

Maxime Dénès (May 18 2022 at 11:31):

The primitive proj layer is very different: it displays terms as other terms.

Pierre-Marie Pédrot (May 18 2022 at 11:31):

there is a nifty comment in the patch that introduced the length def

Maxime Dénès (May 18 2022 at 11:31):

It is the difference between a lie and a macro :)

Pierre-Marie Pédrot (May 18 2022 at 11:32):

Datatypes.length and app defined back via fun+fix instead of Fixpoint
Since length and app were defined inside a Section in List.v, their type argument A wasn't inside the fixpoint. Restoring the initial definition repairs (at least) Cachan/IntMap.

Janno (May 18 2022 at 11:32):

Could somebody explain why length cannot be a Fixpoint? I feel like I've written the same function as Fixpoint and I don't remember any issues with that.

Maxime Dénès (May 18 2022 at 11:32):

Pierre-Marie Pédrot said:

Datatypes.length and app defined back via fun+fix instead of Fixpoint
Since length and app were defined inside a Section in List.v, their type argument A wasn't inside the fixpoint. Restoring the initial definition repairs (at least) Cachan/IntMap.

Putting the comment in the code would already be an improvement :)

Maxime Dénès (May 18 2022 at 11:33):

Janno said:

Could somebody explain why length cannot be a Fixpoint? I feel like I've written the same function as Fixpoint and I don't remember any issues with that.

The problem is not immediate. It appears when you want to reason by recursion, with some recursive calls involving length themselves.

Maxime Dénès (May 18 2022 at 11:35):

The reduction behavior is not the same if you put the parameter below the fix, which is what Fixpoint does.

Maxime Dénès (May 18 2022 at 11:35):

And in particular sometimes it prevents the guard condition from being able to reason on the nested fix as much as you would like.

Janno (May 18 2022 at 11:35):

Ah, I see. Thank you very much!

Maxime Dénès (May 18 2022 at 11:36):

The fact that expert users like you are not aware of these very subtle details that appear in such a basic construct as the length function on lists is a strong message IMHO. Our learning curve is not reasonable.

Ali Caglayan (May 18 2022 at 11:36):

@Pierre-Marie Pédrot How easy is it to warn about a lack of Proof.? I feel like it would have to be quite invasive. (Implementation wise)

Maxime Dénès (May 18 2022 at 11:39):

It probably requires to instrument the STM, I guess.

Gaëtan Gilbert (May 18 2022 at 11:41):

Maxime Dénès said:

Ah yes, in statements. But I don't see why we could not have the Fixpoint vernac do the right thing on the length example.

what is the right thing? the way length is currently defined reduces more / has nicer interactions with the guard but AFAIK it sometimes interacts badly with fixpoint refolding
see also https://github.com/coq/coq/pull/6632 (there were some CI failures)

Maxime Dénès (May 18 2022 at 11:43):

Ah right, I forgot that the consensus on the "right" fix was more like a kernel extension to recognize these parameters

Maxime Dénès (May 18 2022 at 11:44):

Would still be nice to have :)

Gaëtan Gilbert (May 18 2022 at 11:45):

Is that consensus?

Maxime Dénès (May 18 2022 at 11:46):

If @Pierre-Marie Pédrot agreed that the change should be in the kernel, of course it means consensus :)

Paolo Giarrusso (May 18 2022 at 17:31):

Karl Palmskog said:

from user and Platform side, I think we'd rather see piecewise changes to the vernacular language than big redesigns

That depends. For instance, the ongoing switch away from "default #[global] has clearly been annoying because it was too incremental, and we've had to start using #[global]` in some places when it's (still today) illegal in others.

Paolo Giarrusso (May 18 2022 at 17:33):

For a more interesting example, Unifall seems to still lacks an ETA precisely because it tries to be backward compatible, instead of providing "Coq 9.0 typeclasses" (the alternative would have other problems but could help for new code)

Paolo Giarrusso (May 18 2022 at 17:35):

on the original topic of Proof., today Proof. isn't a no-op with Set Default Proof Using (which you want to combine vos and sections), and an attempt to change that caused coq to deadlock with itself... so IMHO either Set Default Proof Using. starts acting without Proof. or Proof. should be mandatory.

Jason Gross (May 21 2022 at 00:17):

I'm a bit confused by the length example. I see why List.map needs to be Definition + fix to satisfy the guard condition, but I cannot think of an example where having the type argument to length would interfere with the guard checker (because A is not called on a subterm of the list)

Paolo Giarrusso (May 21 2022 at 04:31):

PMP already provided an example: https://github.com/coq/coq/issues/16040

Jason Gross (May 21 2022 at 07:09):

That example is about map, not length

Gaëtan Gilbert (May 21 2022 at 08:03):

Last updated: Oct 12 2024 at 11:01 UTC