Stream: Coq users

Topic: Beginner best practices


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

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.

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

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

view this post on Zulip 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: Jun 23 2024 at 05:02 UTC