Naming conventions (letter case, underscores, &c) for Coq

Question

Does Coq have an established convention/style for constructors, variables, terms, &c?

An established convention that isn't exceptionless is totally fine. For example, terms should be lowercase like nat unless you're trying to mimic math notation in cases like N or Z is a good convention.

---

The naming convention I've started using for toy Coq code is PascalCase for variables and constructors and snake_case for everything else.

I like being able to visually distinguish variables and nonvariables at a glance, and like naming single-argument constructors after the type of their argument, which is possible in this convention.

However, using the same portion of the namespace for constructors and variables leads to problems.

In this code snippet, MisspelledConstructor is a variable and will unify with anything. This problem is not huge is practice because Coq enforces exhaustiveness in match statements, but distinguishing constructors and variables by convention would lead to more informative error messages and make debugging slightly easier.

match thing with
| MisspelledConstructor => expression
| (* some pattern *) => (* this expression is unreachable because 
   MisspelledConstructor matches everything *)
end

Answer 1

A similar question was recently discussed in the Coq Zulip chat (regular link, no-login-needed link), of which this answer is a summary.

The vstyle project is working on building / collecting Coq style conventions.

Some specific libraries have their own conventions. For example:

• MathComp
• Iris
• HoTT
• Verdi

See also Deep Generation of Coq Lemma Names Using Elaborated Terms and Learning to Format Coq Code Using Language Models for more references.