a tutorial draft about SSReflect tactics

[grianneau]

This is a tutorial draft about SSReflect tactics. Some basic knowledge of Coq is required (interactive session with jsCoq, type system of Coq, Check command, etc) that we should probably need to minimise.
The goal is to introduce the main SSReflect tactics with which one can accomplish most proof steps.
The tutorial can be an opportunity to dissimenate other bits of knowledge, such as basic use of the MathComp library and small scale reflection.
To start with, it is important that the user gets an overview of the main tactics and gets an intuitive understanding of what each tactic does in a basic isolated case (the current examples may seem superficial).

Two technical questions:

1. Is it possible to add some spoiler code in the html page? The idea is to provide some extra-content that is hidden at first. It can be useful to provide solutions to some of the exercices.
2. Is it possible to import Hierarchy Builder wihtin jsCoq? It may be useful to display nicer messages when using MathComp.

[thomas-lamiaux]

Hi @grianneau, thank you very much for contributing, I am very happy to see that people are starting to contribute.

Review

I have read the tutorial in details. It is not bad for a first draft, but I think they are issues with it because the target is not clear:

1. The content oscillate between targeting newcomers to Coq and Vanilla Coq users. Hence, depending on who you are and where you are in the tutorial, it can be either be too slow or too fast. It probably would be best to have two different tutorials, one for each kind of users. This draft could be a base for both modulo different explanations.
2. There is the sentence "The following code is considered bad practice." which illustrate this issue above but also raise the question of what is this tutorial supposed to be about. Is it to teach SSReflect methodology / introduce MathComp and MathComp's writing style ?
3. There are a lot of stuff to explain about SSReflect. It seems complicated to do everything in one tutorial without being a bit fast / superficial about it, or very long. Should some part deserve specific tutorials like "Forward Reasoning with SSReflect" ?

Recommendation

If all goes well with the platform doc project, these tutorials should become the first things people go to when they want to learn a new feature, so as a general rule I think it is good to think first where the community want to go.

This is particularly the case here, as SSReflect is a large and powerful language with its own methodology. Further, as it has a slightly complicated history, and is often viewed wrongfully as unreadable and only usable in MathComp style. I know that they are many people in the community that would like to seize this opportunity to debunk and clarify this point.

Therefore, I think it is very important here to first discuss within its community what and how you want to present SSReflect. In particular, answers to first questions like:

• Do you want general intro tutorials ? Like "SSReflect for newcommers" and "SSReflect for Coq users" ? What would be in there then ? How should it be presented ? What is the goal of such tutorials ?
• Should some part be left out / or developed further in specific tutorials like "Forward Reasoning with SSReflect" ? What would they be ?
• Most users of SSReflect are MathComp people, yet SSReflect and its methodology can be useful to many are used by people that do not deal with MathComp. Hence, should both kind of content be separated ?

Going Further

Consequently, I suggest to:

1. Start a discussion within the community, e.g. on zulip to understand what you want
2. Open issues for each tuto / how, and maybe a project to centralize it all
3. Adapt this first draft to what has been decided

[thomas-lamiaux]

Concerning your questions:

1. Currently, no as we are only using coqdoc but once we switch to Alectryon it should be possible
2. I don't know, as for technical reasons we are currently stuck with Coq 8.17 but in the future I guess it should be possible

[grianneau]

Thank you for your feedback, Thomas!

There are three things: SSReflect tactics, SSR methodology and MathComp. The first one is addressed.

I agree with you, the tutorial should target either newcomers or Vanilla Rocq (Coq) users and the current draft is flawed. Getting feedback from a reader in the target audience can help.
From a pedagogical point of view (for most learners) it is not bad repeating some information across tutorials if the following pieces of info are in spoilers. A tutorial can be the opportunity to plant some seeds in the mind of the readers. That's why I also give some examples that use MathComp, but they should maybe completely be made without MathComp for this tutorial.

From my point of view, the Coq scripts tend to be unreadable (of course this is less true for expert users) . I don't see it as an issue. I consider the scripts are meant to be played step-by-step, not just read. That's why I like to provide a version with one basic step per line, I call this coding style tategaki 縦書き. With Lean in Visual Studio Code it is easy to run step-by-step just by moving the cursor at the end of the next word. This feature is quite friendly.

[thomas-lamiaux]

@grianneau there is now a reviewer team for mathcomp that should be able to help progress on this tutorial