Should hints/commands inside proofs be supported further or change semantics? For instance
Lemma foo : P 1.
Proof.
...
#[local] Hint ...
..
Qed.
but this includes further constructs like Remove Hints
, Opaque
, (Require) Import
.
I ask because a new Proof General feature would need special handling similar to the STM, and PG devs ( @Pierre Courtieu @Hendrik Tews @Erik Martin-Dorel ) seem uneasy with the idea in https://github.com/ProofGeneral/PG/issues/688, and argue such hints are a bad idea (I disagree) and should probably be scoped to the proof anyway (I agree, but that'd be a large semantic change).
I think Require inside a proof is definitely not something we want.
I think it would be good for Hints inside proofs to revert their mutation of the global state at the end of a proof. That way it would be more compatible with skipping proofs.
If it needs to be global, then it should go outside of the proof.
This would of course require a change to the semantics of adding hints in Coq, but I don't think it would be an unpopular or difficult change. cc @Emilio Jesús Gallego Arias
I'm tempted to think that Opaque and Import should also behave similarly.
There are two ways you may want to change the scoping :
For Opaque
, it depends what you want to do at Qed time in terms of unfolding strategy.
FWIW: today's semantics when the STM skip proofs is to replay those commands. Making them local by default sounds reasonable, but what about migration? The PG issue suggests supporting #[global]
as well (and then #[export]
).
Re Require
, I agree, and that's _almost_ trivial to avoid, except that dropping Require
can change the semantics so this is error-prone (even in manual changes and especially automatically) — From Coq Import Arith.
doesn't exist, and Import Arith
or Import Coq.Arith.Arith.
can pick up _other_ modules.
Thanks @Paolo Giarrusso for raising this discussion upstream.
Actually as proposed by @Pierre Courtieu in https://github.com/ProofGeneral/PG/issues/688#issuecomment-1420601232, there are mostly 3 possible strategies to address Paolo's request:
Hence a few questions:
A. how to "detect such non local side effecting commands" ? is it easy to find a snippet in Coq's codebase that declare them?
B. would strategy 3. be a tractable solution from your viewpoint? (either with a comment, or better, with a #[global]
parsed attribute?)
in which case, an Opaque plus.
command would only impact plus
within the proof, while #[global] Opaque plus.
would also keep it opaque afterwards. (Maybe this approach, removing side-effects from inline Commands by default would also simplify the STM implementation?)
Cc-ing @Enrico Tassi & @Emilio Jesús Gallego Arias as well, in case they would miss this brainstorming discussion…
Maxime Dénès said:
For
Opaque
, it depends what you want to do at Qed time in terms of unfolding strategy.
Is this true? I was under the impression that Qed ignored opaque?
A. how to "detect such non local side effecting commands" ? is it easy to find a snippet in Coq's codebase that declare them?
Coq detects them using the "vernac classifier" https://github.com/coq/coq/blob/master/vernac/vernac_classifier.ml
plugins which add commands register those commands with the classifier (actual data for plugin commands is in vernacextend.ml) when they are declared, this is the CLASSIFIED BY in .mlg files https://github.com/coq/coq/blob/8f1590f7840d0dff71fa9b7a7bbc1ed01d779359/plugins/ltac/extratactics.mlg#L245
the commands which get replayed are the "VtSideff" ones IIRC
some other commands may get treated specially (IIRC Definition gets treated specially for instance)
Is this true? I was under the impression that Qed ignored opaque?
I think he means
Lemma foo : bla.
Proof.
Opaque bar.
some tactic.
Qed. (* when checking the body of foo, bar is opaque *)
(* when checking the body of foo, bar is opaque *)
but that only means that the kernel _prefers_ to not unfold bar
that's what Opaque means isn't it?
just clarifying, since the topic's so confusing and Ali had a question
@Erik Martin-Dorel I'd be happy to add #[local]
, #[export]
or #[global]
as appropriate — and I'll note #[local]
already means something else — but we need a warning
and a warning in proof general wouldn't help when I'm using PG to step proofs from users of other IDEs
I'd personally change the scope of global directives, making them end with Qed. I did propose so ten years ago, but it never got too much traction.
Maybe a #[proof_local] thing is the way to go.
I don't know what omit-proof is exactly, but if you end up facing these problems it probably means it should not be implemented in the UI.
I understand this is a feature that some interfaces may want, but is this discussion really an UI issue?
(or, can I move it to #Coq devs & plugin devs, where I think it belongs, and which has larger audience)
I don't know what omit-proof is exactly, but if you end up facing these problems it probably means it should not be implemented in the UI.
omit-proofs is a poor man's STM without the XML protocol — it simply admits earlier proofs. I agree new UIs should eventually make this unnecessary, but all current PG alternatives have downsides.
This topic was moved here from #User interfaces devs & users > Plans for hints in proofs by Karl Palmskog.
From my point of view I don't care so much what the semantics of such a command is, in the sense that coq-lsp can handle all of them as long as indeed they declare how they update the state correctly.
So indeed, if a hint command will cause an update to the global hint database, then everything that depends on that database must be rebuilt, but it doesn't, then I'm happy too.
So indeed, with my methodology, Paolo request could be implemented by simply having a proof-local copy of the relevant parts of the summary. Unfortunately this requires changes in Coq, I proposed we do something like this a few years ago but we didn't advance much.
It is also fine to skip a proof but have global-updating commands, if the data flow is registered correctly
Part of the motivation is that PG uses simpler tech, and the cleanups are generally desirable anyway; I've seen many Coq users assume that hints in proofs are proof-local, and they were by no means just beginners
Last updated: Nov 29 2023 at 18:01 UTC