Stream: Coq devs & plugin devs

Topic: Well-bracketing of Proof-Qed blocks


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Guillaume Melquiond (May 18 2022 at 09:21):

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

view this post on Zulip Pierre-Marie Pédrot (May 18 2022 at 09:23):

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

view this post on Zulip Pierre-Marie Pédrot (May 18 2022 at 09:24):

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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (May 18 2022 at 09:30):

what's different about instance?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Guillaume Melquiond (May 18 2022 at 09:32):

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

view this post on Zulip Pierre-Marie Pédrot (May 18 2022 at 09:32):

we're dragged back precisely because of that.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (May 18 2022 at 09:35):

Same issue.

view this post on Zulip Pierre-Marie Pédrot (May 18 2022 at 09:35):

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

view this post on Zulip Guillaume Melquiond (May 18 2022 at 09:35):

But this is statically recognized!

view this post on Zulip Pierre-Marie Pédrot (May 18 2022 at 09:36):

Not if you have the refine mode around.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (May 18 2022 at 09:38):

hmm, the refine instance mode was removed indeed.

view this post on Zulip Pierre-Marie Pédrot (May 18 2022 at 09:39):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (May 18 2022 at 09:44):

obligations need the obligaton commands to open

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Guillaume Melquiond (May 18 2022 at 09:54):

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

view this post on Zulip 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

view this post on Zulip 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..

view this post on Zulip 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.)

view this post on Zulip 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)

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Maxime Dénès (May 18 2022 at 11:07):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Gaëtan Gilbert (May 18 2022 at 11:11):

Fixpoint vs Definition := fix

WDYM?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (May 18 2022 at 11:20):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (May 18 2022 at 11:23):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (May 18 2022 at 11:28):

(A:Type)

view this post on Zulip Maxime Dénès (May 18 2022 at 11:29):

?

view this post on Zulip Maxime Dénès (May 18 2022 at 11:29):

That was called polymorphism when I was young

view this post on Zulip Pierre-Marie Pédrot (May 18 2022 at 11:30):

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

view this post on Zulip Pierre-Marie Pédrot (May 18 2022 at 11:31):

view this post on Zulip 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.

view this post on Zulip Maxime Dénès (May 18 2022 at 11:31):

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

view this post on Zulip Pierre-Marie Pédrot (May 18 2022 at 11:31):

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

view this post on Zulip Maxime Dénès (May 18 2022 at 11:31):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Janno (May 18 2022 at 11:35):

Ah, I see. Thank you very much!

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Maxime Dénès (May 18 2022 at 11:39):

It probably requires to instrument the STM, I guess.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Maxime Dénès (May 18 2022 at 11:44):

Would still be nice to have :)

view this post on Zulip Gaëtan Gilbert (May 18 2022 at 11:45):

Is that consensus?

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (May 21 2022 at 04:31):

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

view this post on Zulip Jason Gross (May 21 2022 at 07:09):

That example is about map, not length

view this post on Zulip Gaëtan Gilbert (May 21 2022 at 08:03):

see also https://github.com/coq/coq/commit/4237fa16d23101bc05ebc9a3dad168be4f3f64d8


Last updated: Feb 06 2023 at 00:03 UTC