Stream: Coq users

Topic: Beginner best practices

Hugo Musso Gualandi (Mar 04 2024 at 13:47):

Hi,
I have dabbled with Coq for a bunch of years, but never got to the point where I would stop calling myself a Coq "beginner". One small thing that I notice is that there are a bunch of trivial decisions that come up, that I don't know what is the right one to pick by default and thus it wastes brain cycles that could have been used more productively elsewhere. For example:

• When I use intros, should I name the variables or let Coq pick the names?
• When I name things, what is a good naming convention?
• When I do induction, should I simpl all the cases with ";" or should I simplify each sub-case on demand?
• Do I call simpl before or after introducing the hypotheses? Doing it before might require calling intros twice instead of once.

Do you know if anyone has ever written about this sort of stuff? I find myself wishing for something along the lines of that Code Complete book, but for Coq.

Karl Palmskog (Mar 04 2024 at 13:52):

if you're looking for strong conventions for Coq code, probably the most developed ones are for the Mathematical Components library with the SSReflect proof language. For a good starting point, see the MathComp book.

The official MathComp coding conventions: https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md#proof-style

Pierre Roux (Mar 04 2024 at 14:37):

Otherwise, your only other question that I'd consider has a relatively consensual answer is the first one: never use intros., or at least never let it remain in a finished proof. We now have option -mangle-names to test that you didn't accidentally used an automatically generated name. ssreflect is better than ltac here, with move=> ? that prevents accidentally using an automatically generated name explicitly.

Gaëtan Gilbert (Mar 04 2024 at 14:40):

you can use intros. if you don't use the names though, eg intros. assumption.

Last updated: Oct 13 2024 at 01:02 UTC