Hugo Herbelin (Jan 26 2022 at 12:49): Hugo Herbelin (Jan 26 2022 at 12:49):In any case, I did not want to start a flame. My question is not about quarelling about this or that feature of have and assert. My question is about why not to work altogether at proposing to users a clear picture of how to use Coq, and to possibly implement what is needed for that since at the end it is mostly a question of decision to take. Then, once we decide to work together at providing a clear and unified picture, we can discuss the details.
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:52):@Hugo Herbelin your question is offtopic for the thread
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:52):It is very hard to understand why that kind of discussion is randomly inserted
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:52):on unrelated topics,
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:53):The discussion has already happened many times
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:53):If you want it to happen again let's do in the proper channel
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:53):but I don't see why the outcome should be different from the last time
Emilio Jesús Gallego Arias (Jan 26 2022 at 12:54):In my very humble opinion, inserting this kind of questions in places unrelated drives away / scares contributors, devs, and users
Ali Caglayan (Jan 26 2022 at 12:55):I think Hugo's question is completely fine. This is why we can move topics in Zulip
Ali Caglayan (Jan 26 2022 at 12:56):I've split the have vs assert and this thread from the main one
Ali Caglayan (Jan 26 2022 at 12:58):@Théo Zimmermann can you move this topic to coq devs? Or give me moving powers too
Hugo Herbelin (Jan 26 2022 at 13:02):@Emilio Jesús Gallego Arias, you're missing the point. There is a question of features, there is a question of syntax, but before all, you are a developer, and you know that, if we want, we can change assert or have to make them like we want them to be. For instance, nothing really prevents per se that assert do generalization over unresolved terms, or that assert supports a f x := t syntax, etc. It is a question of decision. But we cannot take any kind of concrete decision if, from the very beginning, we decide that we don't want to propose a unified and consensual view of Coq, taking into consideration all aspects (including e.g. efficiency).
Hugo Herbelin (Jan 26 2022 at 13:09):In particular the quarrels that this or that tactic does this or that that another does not do is a trap. For instance, I have pending works for years to make tactics more powerful that cannot simply make its way because of an absence of consensus on the directions we want to go. Not working together is simply leading to paralysis while there are so many interesting things to do about tactics which we could do by deciding to go in a common direction.
Hugo Herbelin (Jan 26 2022 at 13:11):And common direction requires that every interesting feature, every interesting syntax is worth to be valued.
Ali Caglayan (Jan 26 2022 at 13:17):Shall I add this as a topic to the call? I think it would be good to discuss it face to face
Notification Bot (Jan 26 2022 at 13:18):This topic was moved here from #Coq users > How to better document tactics? by Ali Caglayan
Ali Caglayan (Jan 26 2022 at 13:23):I've added some talking points to the coq call @Hugo Herbelin https://github.com/coq/coq/wiki/Coq-Call-2022-01-26
Hugo Herbelin (Jan 26 2022 at 13:31):Ali Caglayan said:
Shall I add this as a topic to the call? I think it would be good to discuss it face to face
It is a kind of discussion which may need a lot of time. For the call, I would not do more than making a plan or setting objectives for a discussion. For instance, I think it is important to compare features so that we know what we want (and that can take hours) but I don't think we'll go anywhere if there is no clear objective in advance about where we want to go and where we want to put our energy.
Ali Caglayan (Jan 26 2022 at 13:33):OK I put it at the end anyway. It might be a starting point for getting a more regulated serious discussion about what to do.
Ali Caglayan (Jan 26 2022 at 13:35):To be clear it is not there to advocate any style of tactics over another. I have also thought about similar ideas in the past.
Before I have been helping some users with learning tactics. One of the most off-putting things was the shear amount of tactics and little documentation. I've tried to write cheat-sheets in the past to help people, but somebody will always come along with a tactic that I've never even seen before and ask about it.
Ali Caglayan (Jan 26 2022 at 13:36):ssreflect is very good in the regard that practically everything is documented. It has other issues such as the learning curve being somewhat steep, but that is to be expected when doing serious formalization.
Ali Caglayan (Jan 26 2022 at 13:37):On the other hand for the past 20 years the ltac tactic cheat sheets have not even changed slightly. I see many users that are confused about old tactics etc.
Ali Caglayan (Jan 26 2022 at 13:38):But with all this stuff there ought to be some abstract notion of "how to do a proof". If we can nail down what exactly that entails, then that might help structure all tactic documentation in the future.
Ali Caglayan (Jan 26 2022 at 13:41):In mathematical circles, the fact that coq is heavily geared towards proofs starting from the conclusion is already quite controversial. I don't think telling users that "coq is based on PUICIC which is a type theory/programming language so it makes sense to write proofs this way" is the best explanation.
Ali Caglayan (Jan 26 2022 at 13:41):In this case, we could for example show that forward proofs are possible in coq but are harder to write and reason about.
Pierre-Marie Pédrot (Jan 26 2022 at 13:45):I don't think that forward vs. backwards has anything to do with Curry-Howard
Karl Palmskog (Jan 26 2022 at 13:46):I've translated proof scripts manually line by line between HOL systems and Coq (in both directions), and it works fine.
Ali Caglayan (Jan 26 2022 at 13:47):Right maybe not exactly due to Curry-Howards, but type theory does push natural deduction/sequent style proofs quite far which is almost always backwards reasoning.
Karl Palmskog (Jan 26 2022 at 13:47):one key surface-level difference in dependent type theory over simple types for regular users is arguably that -> is primitive and preferred over / \ in many cases, whereas the HOLs don't care
Hugo Herbelin (Jan 26 2022 at 13:48):It is the Call-by-name bias: forward reasoning is the let-in of programming language, which theoricians of type theory indeed tend to omit.
Pierre-Marie Pédrot (Jan 26 2022 at 13:56):I write my ML programs with a lot of let-bindings, and I'd do that in Haskell as well
Pierre-Marie Pédrot (Jan 26 2022 at 13:57):if anything it's rather a bias of the meta-language of Coq, that dates back to the LCF approach
Hugo Herbelin (Jan 26 2022 at 14:04):If about Coq, it is a bias in the documentation of Coq, because forward reasoning and let-in exist in Coq for more almost 20 years now
Ali Caglayan (Jan 26 2022 at 14:07):There is also a large bias towards automation (perhaps with good reason). Automating forward reasoning is very difficult compared to backwards reasoning.
Ali Caglayan (Jan 26 2022 at 16:47):So in summary:
These can all have major effects on the style of tactics used. If we wish to document tactics better we need to address these points in a somewhat generic manner.
Last updated: Nov 29 2023 at 18:01 UTC