aspiwack/finset

A Coq library for extensional finite sets and comprehension
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.
Lib
Quotients
.gitignore
FinMap.v
FinSet.v
LICENCE
_CoqProject

Finite sets of countable types in Coq

Finite objects on countable types can often be represented in a extensional way in Coq (that is, such that the native equality of Coq validates the appropriate extensionality principles). This library is an attempt at implementing such objects. The resulting data types are quite inefficient and are not appropriate in an implementation, but can be very helpful as implementation tools.

For now the only implemented structure are finite subsets. Potential extensions are finite multisets and functions with finite support.

Licence

Cosa and all of its files are distributed under the CeCILL v2.1 licence. It is a licence in the spirit of Gnu's GPL maintained by three French academic institutes. See the `LICENCE` file for details.

Principles

The main ingredient is that quotients of countable types by decidable equivalence relations can be defined extensionally in Coq. This concept has been described and exploited in Cyril Cohen's PhD thesis (see in particular Chapter 6).

This rests on two pillars. One is a consequence of Hedberg's theorem that types with decidable equality have uniqueness of identity proofs: `{ x:A | P x }` is extensionally a subset of `A` when `P` is decidable. The second is that countable types support indefinite description, i.e. `(∃x,P x) → {x | P x}`, for `P` decidable.

Finite sets, then, are expressed as such a quotient of the type of lists (lists of countable types are themselves countable).

Design

Decidable propositions

This library uses a type of strongly decidable propositions rather than booleans. The type is as follows

``````Record DProp := {
Holds :> Prop;
Denies : Prop;
dec :> { Holds } + { Denies };
contradictory : Holds -> Denies -> False
}.
``````

The reason to prefer this type to booleans is essentially what Bob Harper explains in his blog post Boolean blindness.

Countable types

Since the encodings as natural numbers, that the countable types in this library enjoy, are not particularly efficient. It was found preferable to use a type class to define countability, so that instances can be inferred automatically.

Finite sets

One advantage of the definition of finite set given in this library is that they are defined simultaneously on all the countable types. As a result, syntax for defining sets by comprehension can be given. Because finite sets of countable types are themselves countable, comprehension primitives form, conveniently, a monad.

Documentation

A `coqdoc` generated documentation is available.

The sources are organised as follows:

• `FinSet` is the file containing the interface for finite sets
• The `Lib` directory contains general purpose libraries: `DProp` defines the decidable propositions, `CEExt` contains extension to the `Coq.Logic.ConstructiveEpsilon` library from Coq's standard library, `LibSet` contains extension to Coq's list library mostly pertaining to lists viewed as sets.
• The `Quotients` directory contains libraries used to define quotients: `Retract` contains a theory of retraction, `Countable` defines countable types and `Quotient` define extensional quotients of countable types by decidable equivalence relations.

Installation

The library needs a recent version of Coq development version to compile. When version 8.5 is released, it will be the reference version.

To compile use the following command:

``````coq_makefile -f _CoqProject -o Makefile && make
``````

Then install (probably as root) with:

``````make install
``````
You can’t perform that action at this time.