Skip to content

Other "standard" libraries

Jump to bottom Edit New page
Bas Spitters edited this page Nov 17, 2018 · 21 revisions

Other "Standard" Libraries for Coq

There is a cottage industry of alternative standard libraries/extensions to the standard library.

  • Coq
    • Grew organically over time, lots of different conventions.
  • coq-ext-lib
    • Type classes
    • Originally minimal use of dependent types (that has changed a little bit).
    • Separation between definitions and proofs, e.g. Monad and MonadLaws.
    • Disciplined use of notations to avoid trivial import problems with libraries that are compatible except for notations.
    • Universe polymorphism and primitive projections everywhere.
    • Module naming convention ExtLib.Data.Nat, ExtLib.Structures.Monad, etc. Generally CamelCase for types and snake_case for definitions.
    • License: MIT
  • coq-haskell
    • Type classes
    • Mostly for smoothing the extraction from Coq to Haskell.
    • Module naming convention Hask.Data.List, names reflect their Haskell names, e.g. Maybe instead of option.
  • coq-prelude
    • "Inspired by Haskell"
    • Mostly focused on Monads
    • Module naming convention Control.Classes, Control.State, etc.
    • camelCase for definitions and CamelCase for types/classes.
    • License: GPL3
  • mathclasses
    • First big library based on Type classes.
    • Proposed the unbundled approach, which is now standard.
    • Pervasive setoids
    • Algebraic hierarchy
    • Category theory
    • Universal algebra
    • Exact real number computation
    • License: Public domain
  • ssreflect
    • Canonical structures
  • stdpp
    • Type classes
    • Mostly data types, not a lot of generic interfaces.
    • Lots of hints and patterns to improve type class resolution and type checking.
    • Module naming convention: stdpp.fin, snake_case for identifiers
  • hott-coq
    • Based on homotopy type theory
    • Very math (e.g. topology) inspired.
    • Possibly more difficult to approach from a programming background.
    • Style file describes various conventions, e.g., around typeclass usage, naming conventions, organization, etc
      • Typeclasses used for trunctation levels are required to form a DAG; in general, when we have A <-> B for A and B both classes, we must pick a canonical flow direction so that typeclass resolution neither loops nor misses things.
    • Within the Categories directory:
      • Every file contains approximately one "main" theorem or construction
      • Related constructions are grouped together in the same directory
      • Every directory Foo/Bar/ has a corresponding module Foo/Bar.v which Requires and Includes the relevant files in Foo/Bar/ so that one can Require Import Foo.Bar and get access to the relevant things both at top level and with absolute name Foo.Bar.*.
      • Automated proofs are considered to be "not yet polished enough" if they contain more manual structure than (optionally) induction followed by repeat match goal with / repeat first.

Last section of https://hal.inria.fr/hal-00816703v1/ provides a comparison between type classes and canonical structures.

"Standard" Libraries for other Languages

Add a custom footer
Add a custom sidebar
Clone this wiki locally