Philosophy

With a language as powerful as Coq (full dependent types), there are a lot of possibilities for expressing abstraction. This library is evolving around a core concept for a way to build programs and reason about them.

Split Computation & Reasoning

The core philosophy can best be summed up with the following statement:

Divide computation and reasoning and describe their connection using type classes.

What this means is that when we want to define a structure, for example, a Monad we declare a class for the computational part.

Class Monad (m : Type -> Type) : Type :=
{ bind : forall T, m T -> forall U, (T -> m U) -> m U
; ret  : forall T, T -> m T
}.

and a corresponding class for the reasoning principles admitted by this structure (we elide the use of equivalence relations for expository purposes).

Class MonadLaws (m : Type -> Type) : Type :=
{ ret_of_bind : forall T U (t : T) (f : T -> m U), bind c ret = c
; bind_of_ret : forall T U (t : T) (f : T -> m U), bind (ret x) f = f x
; bind_assoc  : forall c1 c2 c3, bind (bind c1 c2) c3 = bind c1 (fun x => bind (c2 x) c3))
}.

For convenience programming, we use the class, which contains purely computational definition. For reasoning about our programming, we postulate a corresponding instance of monad laws and use custom tactics for rewriting and reducing with respect to the monad laws. This has several benefits:

1. Programs are not hindered by expensive dependent types (since compilation of Coq is not yet a solved problem and the Coq kernel has performance limitations).
2. Verifications can be done with respect to abstract properties that can be proven for numerous implementations of the underlying structure (here a monad).

This means that verifications will normally be predicated on proofs of these abstract properties. For example, rather than saying:

Theorem program_correct : forall x y z, f x y = z.

You will rather say:

Theorem program_correct : MonadLaws m -> forall x y z, f x y = z.

This enables users to use custom implementations and retain all the properties as long as they can verify the laws with their implementation.

Alternatives

There are numerous alternative approaches that could have been used.

1. Modules are the traditional abstraction in Coq, i.e. they are the way that the standard library implements structures like finite maps, sets, etc. They are second-class in Coq meaning that the language used to manipulate them is different than the language used for manipulating normal values (like natural numbers, etc.).
   1. Modules are very nice because they provide isolated name spaces and are convenient to program with because they have signatures that hide internal definitions.
   2. The second class nature makes them difficult to use and less powerful than is necessary in some cases, for example, constructing finite maps where the key type comes from a data structure is not possible. See, for example, Toward a verified relational database management system
   3. It is often desirable to prove properties over the course of several files and keep an abstract type of the type that you are working with. To achieve this, files often need to include boiler plate to use functors which need to be instantiated consistently to ensure getting the appropriate facts about the appropriate types. I believe that the later two of these points make second-class modules a poor abstraction mechanism when compared to first-class alternatives.