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.
@Hugo Herbelin your question is offtopic for the thread
It is very hard to understand why that kind of discussion is randomly inserted
on unrelated topics,
The discussion has already happened many times
If you want it to happen again let's do in the proper channel
but I don't see why the outcome should be different from the last time
In my very humble opinion, inserting this kind of questions in places unrelated drives away / scares contributors, devs, and users
I think Hugo's question is completely fine. This is why we can move topics in Zulip
I've split the have vs assert and this thread from the main one
@Théo Zimmermann can you move this topic to coq devs? Or give me moving powers too
@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).
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.
And common direction requires that every interesting feature, every interesting syntax is worth to be valued.
Shall I add this as a topic to the call? I think it would be good to discuss it face to face
This topic was moved here from #Coq users > How to better document tactics? by Ali Caglayan
I've added some talking points to the coq call @Hugo Herbelin https://github.com/coq/coq/wiki/Coq-Call-2022-01-26
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.
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.
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.
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.
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.
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.
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.
In this case, we could for example show that forward proofs are possible in coq but are harder to write and reason about.
I don't think that forward vs. backwards has anything to do with Curry-Howard
I've translated proof scripts manually line by line between HOL systems and Coq (in both directions), and it works fine.
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.
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
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.
I write my ML programs with a lot of let-bindings, and I'd do that in Haskell as well
if anything it's rather a bias of the meta-language of Coq, that dates back to the LCF approach
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
There is also a large bias towards automation (perhaps with good reason). Automating forward reasoning is very difficult compared to backwards reasoning.
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: May 31 2023 at 15:01 UTC