Style Guide for Coq

Published by applied.fm.

Note

This is a work in progress! We welcome feedback and pull requests. Find us on GitHub.

About

• Principles
  • Roles & personas
  • Use cases
  • Desired outcomes
    • Mitigate bike-shedding & reduce cognitive load
    • Style is enforcable by a linter
    • Find & replace work as expected
    • Separate things are separate; dependencies are easy to trace
    • Project is robust against changes to the Coq engine
    • Project is minimally impacted by changes in upstream components
    • Upstream maintainers are not punished for offering to help
    • Project changes have minimal impact on downstream users
• FAQ
  • What is a style guide?
  • Why adopt a style guide?
  • When is the right time to adopt a style guide?
  • Why adopt this style guide?
  • How does this relate to Requirements on the Use of Coq in the Context of Common Criteria Evaluations?
  • What is Alectryon?
  • How can I contribute to this guide?

Code Style

• Formatting
  • Spaces, tabs
  • Line length
  • Indentation
  • Non-ASCII characters
  • Notation
• Naming conventions
  • Files
  • Modules and module types
  • Definitions
  • Lemmas
  • Variables
  • Types
  • Predicates
  • Projections
• Scope management
  • Require, Import, Export
  • local, global, export
  • Module, Module Type
  • Section
    • Context
  • Notation
• Definitions
  • Type inference
  • Definition, Example
  • Fixpoint, CoFixpoint
  • Lemma, Theorem, Fact, Remark, Corollary, Proposition, Property
  • Hypothesis, Hypotheses, Variable, Variables
  • Axiom, Axioms, Conjecture, Conjectures, Parameter, Parameters
  • Attributes
    • Program
    • Arguments
    • Opaque, Transparent
  • Expressions
    • let ... in
    • if ... then ... else
    • match ... with ... end
    • Monads (... ;; ..., >>, >>=, let!)
  • Keeping everything organized
• Types
  • Numeric types
    • Number Notation
    • nat, pos, N, Z, Q
    • Fin.t
    • BigN, BigZ, BigQ
  • String types
    • String Notation
    • ascii (" ... ")
    • string (" ... ")
    • byte
    • ByteVector
  • Primitive objects
    • int
    • float
    • array
  • Sum types
    • Variant
    • Inductive
    • CoInductive
    • sum (+), or (\/)
    • option, sumor (... + { ... })
    • bool, sumbool ({ ... } + { ~ ... })
  • Product types
    • Record, Structure
    • prod (*), sigma ({ ... | ... }), and (/\), ex (exists ... , ...)
  • Containers
    • list ([ ... ])
    • VectorDef.t
    • MSets
  • Typeclasses and canonical structures
    • Class
    • Instance
    • Canonical Structure
  • Inheritance and Coercion
  • Implicit Type, Implicit Types
  • Boxed and unboxed representations
  • Common classes & structures
    • Coq.Classes.DecidableClass
    • Coq.Classes.EquivDec
    • Coq.Classes.RelationClasses
    • Coq.Classes.SetoidClass
    • Coq.Classes.SetoidDec
    • ExtLib.Structures.Monad
  • Universes
    • Universe polymorphism
• Ltac
  • Goal & context management
    • Automatic variable naming
    • Braces and bullets
    • No epic proofs
  • Destruct patterns
  • Defining custom tactics
  • Tactic Notation
  • Guidance on specific tactics
    • intros, revert, rename, clear
    • admit, give_up
    • easy, now, assumption, trivial
    • try
    • lia, nia
    • left, right, exists, constructor
    • reflexivity, symmetry, transitivity, congruence
    • absurd, contradiction, exfalso
    • exact, apply, refine
    • simpl, red, cbv
    • rewrite, subst
    • assert ... as, enough
    • pose proof ... as
    • remember ... as
    • change ... with
    • generalize
    • specialize
    • auto
    • eintros, evar, eauto, erefine, eassumption, eenough, instantiate

Extraction Style

• Extraction to OCaml
• Extraction to Haskell
• Extraction to C

Project Style

• Project structure
  • Documentation
    • Project documentation
    • Source & example documentation
    • Repository documentation
  • Dependencies
  • Source control
  • Continuous Integration
  • Releases
    • Versioning
    • Distribution
    • Documentation
    • Announcements
  • Repo Structure
    • dep/
    • docs/
    • ext/
    • src/
    • examples/
    • theories/
    • .gitignore
    • .readthedocs.yaml
    • _CoqProject
    • coq-myproject.opam
    • Makefile
    • Makefile.configure.example
    • LICENSE.txt
    • CONTRIBUTING.md
    • README.md