ceps
ceps copied to clipboard
coq
Proof modes
In the title of the CEP and in Maxime's talk, this proposal is advertised as "proof modes".
The general idea of having a built-in mechanism to implement various "proof modes" seems to me like a very nice idea. It could be used to make a better behaved declarative mode (if one wanted to do that job); maybe it could be used to avoid the current MProof. of MetaCoq; we can even think that it could be used for Iris.
EDIT: I might not be using the term "proof mode" for what it is supposed to mean, thus the confusion. From the talk, I understood "proof mode" in an intuitive way, without knowledge of this part of the implementation.
But it isn't (as I understand it) what the CEP really discusses. The CEP is just about not loading lexer / parsing rules too early. The problem it tries to solve (in my limited understanding of this part of Coq) is pollution of the proof environment with unwanted tactic notations (when the user did not do Require Import).
Moreover, I fail to see SSReflect (the main application that you have in mind if I understood correctly) as a distinct proof mode. To reuse the terms of Pierre-Marie, SSReflect looks more like a tactic library (i.e. a set of tactics), which can be used in the classic proof mode, in combination with Coq built-in set of tactics.
Thus, instead of talking about proof modes, I would talk about a better behaved module system.
EDIT: this might be wishful thinking and much harder to actually do than what you propose.
To continue talking about the application to SSReflect, one could imagine putting Coq basic tactics into various modules which you need to import to use the tactics. Then you could Require Import SSReflect. and Require Import BasicTacticsAlsoUsefulToSSReflectUsers. Similarly, one could consider being able to do Require Import 86Tactics.
Instead of having to specify in which proof mode you are at the beginning of each proof, you could also consider having a Local Import feature. This would have the advantage over proof modes to be more generic.
EDIT: Emilio told me that this is not realistic in the current state of affairs of the module system.
You could also imagine putting all standard tactics into just one file but adding a feature to selectively import a few of them Require Import Tactics [reflexivity, now, easy, discriminate].
Anyway, this is just food for thought. I still believe that the problems that you describe in this CEP are worth fixing.
See also https://github.com/coq/coq/pull/459 the diff may help to understand more some basic first steps.
In the title of the CEP and in Maxime's talk, this proposal is advertised as "proof modes".
The general idea of having a built-in mechanism to implement various "proof modes" seems to me like a very nice idea. It could be used to make a better behaved declarative mode (if one wanted to do that job); maybe it could be used to avoid the current MProof. of MetaCoq; we can even think that it could be used for Iris.
EDIT: I might not be using the term "proof mode" for what it is supposed to mean, thus the confusion. From the talk, I understood "proof mode" in an intuitive way, without knowledge of this part of the implementation.
Yes, "proof mode" is an already existing terminology. It is used by the declarative mode, and this CEP is about refining (and among other things, implementing correctly) this mechanism.
But it isn't (as I understand it) what the CEP really discusses. The CEP is just about not loading lexer / parsing rules too early. The problem it tries to solve (in my limited understanding of this part of Coq) is pollution of the proof environment with unwanted tactic notations (when the user did not do Require Import).
The CEP is not only about not loading rules too early. It is also about a fine grained mechanism to switch between modes, and the possibility to use libraries (i.e. to Require .vo files) independently of the language (mode) they were written in.
Moreover, I fail to see SSReflect (the main application that you have in mind if I understood correctly) as a distinct proof mode. To reuse the terms of Pierre-Marie, SSReflect looks more like a tactic library (i.e. a set of tactics), which can be used in the classic proof mode, in combination with Coq built-in set of tactics.
I don't understand the distinction you are trying to make. First, I'm very surprised that you don't see SSR as a language. Is it a feeling that you got by using it? In my view, it is a proof language whose atomic blocks are tactics. Can you make more explicit what you would call a proof mode? And a proof language?
For example, the declarative mode does nothing more than importing its own tactics and syntax. Formally, Iris is the same, except that it acts on embedded contexts and domain specific logics (but that's part of the tactics implementation).
Second, Ssreflect is typically not an application of this framework, because it was designed to have no syntactic conflicts with the 8.6 tactics (apart from a few places like rewrite where one can still disambiguate without resorting to proof modes). What this CEP brings is more freedom for others to implement other proof languages when we merge SSR.
Yes, "proof mode" is an already existing terminology. It is used by the declarative mode, and this CEP is about refining (and among other things, implementing correctly) this mechanism.
I was confused indeed, so most of my earlier comments stemmed from this confusion.
I don't understand the distinction you are trying to make. First, I'm very surprised that you don't see SSR as a language. Is it a feeling that you got by using it? In my view, it is a proof language whose atomic blocks are tactics. Can you make more explicit what you would call a proof mode? And a proof language?
Don't get me wrong. I never said SSReflect was not a proof language. I already said that it is a well-thought, consistent set of tactics and as such it can be called a proof language. What I am saying is that it is much less different from the classic proof mode than the declarative mode is. See on this example:
Goal forall n, n + 0 = n.
proof.
let n : nat.
per induction on n.
suppose it is 0.
hence thesis.
suppose it is (S n') and (n' + 0 = n').
have (S n' + 0 = S (n' + 0)).
~= (S n').
hence thesis.
end induction.
end proof.
Qed.
Goal forall n, n + 0 = n.
Proof.
induction n.
- reflexivity.
- now simpl; rewrite IHn.
Qed.
Require Import mathcomp.ssreflect.ssreflect.
Set Bullet Behavior "Strict Subproofs".
Goal forall n, n + 0 = n.
Proof.
elim.
- reflexivity.
- by move => n /= ->.
Qed.
You will excuse me from putting back the default behavior of bullets. I can't stand not having them. By the way, I hope that you plan to take advantage of the SSR 2.0 release to make the standard bullets usable with SSReflect.
For example, the declarative mode does nothing more than importing its own tactics and syntax.
Does it? OK, but it feels like it does more. Indeed, as can be seen by executing the previous example step by step, the "tactic" per induction on n. does not affect the proof term, nor the goal to prove, but it does some focusing and changes some hidden state so that it is expecting tactics of the form suppose it is ...
Second, Ssreflect is typically not an application of this framework, because it was designed to have no syntactic conflicts with the 8.6 tactics (apart from a few places like rewrite where one can still disambiguate without resorting to proof modes). What this CEP brings is more freedom for others to implement other proof languages when we merge SSR.
Thanks for the clarification! This was indeed something that I had not understood so far.
Anyway, do not take any of my comments as criticism. I feel that you are proposing something useful here, although I don't have enough knowledge of the system to judge.
Goal forall n, n + 0 = n. Proof. elim.
- reflexivity.
- by move => n /= ->. Qed.
By the way the correct proof here is
Goal forall n, n + 0 = n.
Proof. by elim. Qed.
if you want to be more explicit you could do by elim=> // n ->.
I hope that you plan to take advantage of the SSR 2.0 release to make the standard bullets usable with SSReflect.
This has been already discussed, indeed the "standard" bullets are non usable in many proofs, unless you want to indent like up to tab 80. Bullets were first done in SSR then copied in an incompatible way to Coq.
Anyways, I am the first to blame wrt leading PRs off the tangent, but all this discussion about tactic/proof languages starts to be IMVHO a bit tiring, specially given that often comments about the SSR tactic language come from people who has barely used it so they are not particularly useful.
Tactic discussion is important, but maybe the right place to keep things organized would be a thread on coqdev. Cheers!
By the way the correct proof here is
Come on, there is no such thing as "the correct proof". Anyways, by elim=> // n ->. is not making things more explicit, it is making things less explicit since elim => //. or even move => //. is actually enough to finish the proof.
This has been already discussed, indeed the "standard" bullets are non usable in many proofs, unless you want to indent like up to tab 80. Bullets were first done in SSR then copied in an incompatible way to Coq.
You're kidding me right? This is not by taking such positions that you are going to convince people to use SSReflect. SSReflect's bullets are decorative (and counter-intuitive when you know Coq's bullets). I don't care about decorating my proofs.
Anyways, I am the first to blame wrt leading PRs off the tangent, but all this discussion about tactic/proof languages starts to be IMVHO a bit tiring, specially given that often comments about the SSR tactic language come from people who has barely used it so they are not particularly useful.
Yes you are, so I don't feel bad replying and feeding the troll. Maxime and Enrico's claim is that SSReflect 2.0 is a general purpose language which could be used by anyone doing proofs with Coq and that by keeping it out of the main codebase, we are driving users away (e.g. CompCert apparently). They also claim that this is a solution to compatibility issues and thus that it could solve the problems that some users have. Given such strong opinions (which I would call expansionist), I am considering opening myself to SSReflect (not the style, but the language) but this kind of reply that you are giving me is clearly pushing me out.
Since we are at the level of troll, what about this thing of not putting spaces between a tactic and =>. You were the one (I recall) telling that more spaces make the reading easier (in OCaml). Why doesn't it apply to proofs as well? Or maybe readability is not a goal...
Tactic discussion is important, but maybe the right place to keep things organized would be a thread on coqdev. Cheers!
Yes, you're right. I would have felt bad if I hadn't answered your comments but really, we are just polluting the discussion on this CEP and I feel bad for Maxime and Enrico. This is not the place to discuss SSReflect. Let's drop the subject, alright? Cheers!
Come on, there is no such thing as "the correct proof".
I am not the best person to comment but indeed in math-comp there is a proof style, and I am pretty sure that by elim would be the correct style here. Indeed, there is a correct style because the authors of the library chose so.
You're kidding me right? This is not by taking such positions that you are going to convince people to use SSReflect. SSReflect's bullets are decorative (and counter-intuitive when you know Coq's bullets). I don't care about decorating my proofs.
I am not kidding you. First, I don't care about what people use and I am not trying to convince anyone, as it is each person work to realize what is best for them. I am just pointing out a very serious problem with the "standard" bullets, you can read the summary here: https://github.com/math-comp/math-comp/issues/102 Secondly, I am complaining about your introduction of a totally unrelated statement here "bullets" that pollutes the discussion, and it seems it is not very informed from the practical or historical perspective. Thirdly, I must apologize because I do that all the time in GH.
I am doubly sorry if you considered my reply aggressive and I apologize if I am pushing you out. My intention was just to correct several statements that were verifiably not correct.
There are quite a few other statements in your reply that are easy to rebuke, but I will refrain from doing so as it don't think it is productive, but on a small ending note, the style between a tactic and => is specified in the ssr manual, page 60 https://hal.inria.fr/inria-00258384v16/document
Ok, so I've updated coq/coq#459 to a point where it is almost ready to handle the proper extends. We can continue the discussion about code there.
I have a question: is this CEP supposed to cover the managing of different versions of a same tactic, like the version of apply which uses w_unify and the version of apply which uses evarconv?
@ejgallego: do you have already some model in mind?
I don't know the exact plans of @mattam82, but typically, we will have
- either an ML function
applywhich at some time queries a flag to decide whether it usesMetaandw_unifyorEvarandevarconv - or to distinct ML functions
apply1andapply2, one usingw_unifyand the other usingevarconv
Now, users will probably have some old files which I guess they would like to compile with the legacy apply and new files for which they would like to take benefit of the stronger apply. How to manage this? What are the different effective models that we have at our disposal to implement this?
@herbelin Enrico's suggestion as explained here https://github.com/coq/coq/pull/539#issuecomment-291877985 was to duplicate the code, move the new code to evarconv, give access to both implementations thanks to two modes and remove completely the old code in an upcoming version. It looks to me like a good suggestion because it will avoid unnecessarily complicating the new code, although it will lead to temporary code duplication. Of course, to avoid paying the price of the duplication, after the release bugs should only be fixed in the new version.
@herbelin my impression is that proof modes as they stand now won't scale well for individual tactics, as you would need one proof mode for each particular tactic variation. One possibility is to use attributes +
an option (which are almost ready due to coq/coq#402 , and have ltac pay attention to them. That should work maybe better. Do we want a version attribute?
@Zimmi48: Factorization of code vs duplicated code is a real question. Both have advantages and drawbacks.
@ejgallego: The possibility to have attributes on any node of a syntax tree (this is my understanding of coq/coq#402) is powerful. For tactics, I suspect we would need attributes only on a very few nodes but why not using a general infrastructure for attributes after all.
@ejgallego @herbelin Indeed I'd also prefer the complete separation of the code between the two versions of e.g. apply. I don't see why the proof-modes wouldn't be enough here, at least with the global Set Default Proof Mode Coq-8.6 / Coq-8.7 and a finer grain tactic level (mode 8.6: apply foo), do you think that the latter is unlikely to happen? Do you suggest this finer grain mode/version switching could be implemented with attributes?
@mattam82 proof modes work, however I am concerned about scalability, in the sense that in the current state, you need to have a different proof mode for each tactic, which could quickly lead to proliferation of proof modes.
Yes you could. But we may really need "tactic modes" and "proof modes", in the sense that people may want to have different tactic language modes (LTAC / LTAC 2) and different selection of tactics, imagine:
(apply H)%v8.7 ; (apply M)%v8.6
and this kind of tactic selection semms really specific to the tactic language syntax.
Honestly, I think it should be bearable if the proof mode can only be set at the sentence level. Especially for the 8.7 vs 8.6 modes as this is only for compatibility during the transition.
@Zimmi48 yup, it would be good anyways to factor the ltac grammars a bit.
@mattam82: What are the steps to arrive to this model? Does the plan start with something like separating the current directory plugins/ltac into plugins/ltac/v8.6, plugins/ltac/v8.7, plugins/tactics/v8.6, plugins/tactics/v8.7? Duplicating tactics.ml towards plugins/tactics/v8.6 and plugins/tactics/v8.7? Moving g_tactics.ml4 to both plugins/tactics/v8.6 and plugins/tactics/v8.7? Etc.
I'm a bit lost in the discussion. What is the status of proof modes? Is it already usable today for one or another purpose?