Skip to content

Other "standard" libraries

Jump to bottom Edit New page
Pierre Roux edited this page Jul 29, 2024 · 21 revisions

Other "Standard" Libraries for Coq

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

  • Libraries offering a release for Coq 8.19
    • 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-HoTT
      • 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.
    • mit-plv coqutil is a minimalistic selection of common bits from various developments at MIT
    • mathclasses
      • First big library based on Type classes.
      • Proposed the unbundled approach, which is now one of the standards (although it can suffer some scaling issues).
      • Pervasive setoids
      • Algebraic hierarchy
      • Category theory
      • Universal algebra
      • Exact real number computation
      • License: Public domain
    • Mathematical Components
      • Along with Analysis, the most complete basis for mathematical developments in Coq
      • bigop, matrices, finite functions,...
      • Extensive hierarchies of algebraic structures
      • Uses Hierarchy-Builder that currently uses canonical structures
    • Stdlib
      • The historical standard library of Coq
      • Grew organically over time, lots of different conventions.
      • Uses old-fashioned modules
    • stdpp
      • Uses type classes for building abstractions.
        • Most general purpose notations in stdpp are overloaded using operational type classes.
        • There is support for overloaded notations for monads (like the "do" notation), but no general purpose theory about them. We found such general purpose theory not too useful in practice, because one mostly uses properties that are very specific to the monad being used (like list, set, option).
        • Type classes are used to describe properties of types: being inhabited, countable, finite, having decidable equality, being infinite, having UIP, etc.
        • Type classes are used for abstractions around orders, finite sets, and finite maps.
        • There are no type classes for abstractions over number types. This is deliberate, because it having such tactics would break tactics like lia that are too useful in practice.
      • Contains a large library of operations/properties about lists.
      • Contains a large library of operations/properties about sets.
        • There are a number of abstractions for different implementations of (finite) sets.
        • Some implementations that are available: 1.) a generic finite set construction based on radix-2 search trees for any countable type, 2.) sets as lists (up to permutation), both a version with and without duplicates 3.) general sets over a carrier A as either A → Prop or A → bool.
        • There is a generic and extensible tactic set_solver that is able to solve goals involving sets. The tactic is generic because it works for any finite set implementation, and modular because it can easily be extended (via type classes) to support additional connectives on sets.
      • Contains a large library of operations/properties about finite maps.
        • Like sets, there are a number of abstractions to support different implementations.
        • The most widely used implementation is based on radix-2 search trees, and supports keys of any countable type. This implementation enjoys m1 = m2 ↔ ∀ i, m1 !! i = m2 !! i where = is the Leibniz equality.
      • Uses Leibniz equality by default, but also has support for setoids on top of that (often in terms of more general lemmas).
      • Has a reasonably powerful general purpose solver called naive_solver that tries to prove goals by means of brute force (with some tricks to make it kind of breadth first to avoid it diverging too often).
      • Lots of hints and patterns to improve type class resolution and type checking.
      • Module naming convention: stdpp.fin, snake_case for identifiers
    • TLC
      • Explicitly aims to be an alternative standard library
      • Relies on classical axioms
  • Libraries without recent release, potentially no longer maintained
    • 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.
      • This project seems to share some goals with the hs-to-coq base library.
    • 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
    • fiat-crypto "Util" directory is standard-ish, in particular it has systematic lemmas and tactics for list and Z. There is also fiat-crypto Algebra which is is designed for reasoning about code that itself does not depent the algebra library.
    • StructTact
      • Tactic and utility lemma library
    • Hahn library

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