Stream: Coq devs & plugin devs

Topic: How to better document tactics?


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

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:52):

@Hugo Herbelin your question is offtopic for the thread

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

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:52):

on unrelated topics,

view this post on Zulip Emilio Jesús Gallego Arias (Jan 26 2022 at 12:53):

The discussion has already happened many times

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

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

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

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

view this post on Zulip Ali Caglayan (Jan 26 2022 at 12:56):

I've split the have vs assert and this thread from the main one

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

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

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

view this post on Zulip Hugo Herbelin (Jan 26 2022 at 13:11):

And common direction requires that every interesting feature, every interesting syntax is worth to be valued.

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

view this post on Zulip Notification Bot (Jan 26 2022 at 13:18):

This topic was moved here from #Coq users > How to better document tactics? by Ali Caglayan

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

view this post on Zulip 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: May 31 2023 at 15:01 UTC