Tutorial, Equations: Basics

[thomas-lamiaux]

A tutorial introducing the basics of the package Equations

[Vanille-N]

Thanks for the review request @thomas-lamiaux .

Speaking from the position of someone who is familiar with Coq but has never used Equations before, I'm probably quite close to the intended audience for this tutorial.
I don't have the knowledge to evaluate the completeness of this tutorial, but at least it seems pedagogically sound.

[thomas-lamiaux]

While writing this tutorial and reviewing with the developers, we have identified a behavior of funelim that was not wanted (described below) which should lead to modification to Equations. Waiting for it to be changed, I'll switch this PR back to draft.

By default, funelim destruct the goal following the pattern of the definition but does not do any simplifications similarly to how Fixpoint definition works with induction.
It is up to the user to call simp by hand. It is particularly annoying in the case of with clauses, as it makes a subclause corresponding to the branch of the with appear, and one has to rewrite it by hand, then simplify again to get the good pattern. As an alternative, you can simplify directly by rewriting by the generated equation Heqcall.
While always solvable by hand in a few lines, it is not a wanted behavior as it introduces an asymmetry in dealing with patterns depending on if they have a with clause or not.

It is like that for Fixpoint definitions because simpl and cbn are not always easy to control, so we do not want simplification to be done automatically. In our case, because we are relying on controlled rewriting, this should actually pose no issues to always rewrite directly by Heqcall. It actually has several advantages:

• It makes proof easier and faster, as we only have to rewrite by one specific equations that we already know, and do not have to do proof search among the different equations as done by simp f1 ... fn
• It solves the issue of with clauses
• Users get exactly what they want, pattern match + replacement by the good equality without simplifying the rest of the goal

Moreover, the cost to change it is low as funelim f; simp f won't break as simp f works even it has nothing left to do, and in the case of with clause, it will actually enable to remove (small) superfluous code.

While changing the behavior, it was further realized that Heqcall was not present in contexts for regular pattern because Equations was wrongfully simplifying opaque terms. Hence, leading to the discovery of an actual bug.

[Zimmi48]

Waiting for it to be changed, I'll switch this PR back to draft.

I suggest a different approach: merge now with a note about the issue and the workaround in the tutorial, and let users know that this workaround is not needed anymore after version X. When version X has been released and available to the users (as part of a Coq Platform release) for a while, then it will be time to obliterate the mention of this issue (and instead specify that this is the minimum version required to follow this tutorial).

BTW, thank you Neven for the review. I was also planning to do one (from the same point of view of a non-Equation user), but it's difficult for me to find the time. It's good that this tutorial has been reviewed. Merging it now doesn't prevent improving it even more later...

[thomas-lamiaux]

@Zimmi48 That is a reasonable position, and I guess it should be the default one once the documentation will be actually indexed on the version of the Coq platform.
There is nothing left to do, so I'll merge for now, and we can update the tutorial, once the modifications to Equations are merged..

[jfehrle]

A few cursory observations. I looked here while reading coq/rfcs#91.

I think hyperlinking will be essential to make the tutorial accessible to the entire community.

[jfehrle]

Why would someone prefer to use Equations instead of Fixpoint? Would be nice to show a comparative example first using Fixpoint, then using Equations.

[thomas-lamiaux]

We thought about that but we already wanted to have a clear tutorial which was not the case before. Maybe be having a how-to "when to use Equations" could be useful ?

[jfehrle]

IMO the first paragraph in any tutorial should state the benefit of reading the tutorial and of using the described feature. Stating the motivation (or goal) makes it much easier to follow/absorb the contents.

Indeed, this is a good idea for all documentation.

[thomas-lamiaux]

It sounds like a good idea, but some packages like Equations will more than one tutorial. In this case, I think it could be interesting to have a first page like that https://coq.inria.fr/doc/V8.19.0/refman/language/core/index.html

[jfehrle]

Sure. That first page should also state the benefit/purpose of the feature. It doesn't need to be an exhaustive statement.

[thomas-lamiaux]

Also a good reason to use a first page, is that Equations is to particularly good to well-founded recursion or dependent functional programming, and it can hardly be explained in 5 minutes in the basic tutorials.
As you mentioned, in the intro it currently sounds weird.