Home

Awesome

Extensional Structures

arthuraa

This package provides Coq data structures that support extensional reasoning, for which the notion of equality coincides with exhibiting the same observable behavior: sets are equal when they contain the same elements; functions are equal when that produce the same outputs; etc.

Features

Axiom independent ─ Unlike the case of built-in functions and predicates, these extensionality principles do not rely on any axioms beyond Coq's theory.

Executable ─ Data structures are implemented as ordered lists and behave reasonably when extracted (as long as you do not have high expectations for performance).

Compatible with Mathematical Components ─ The design is inspired by SSReflect and the Mathematical Components libraries, and attempts to follow their style and philosophy.

Usage

Currently, four data structures are supported:

Here, T ranges over instances of ordType (defined in ord), which are types endowed with a decidable total order relation. (For ffun def, the codomain of def must be an eqType as well.) Basic data types such as nat, bool, option, products, and sums are all pre-declared as instances of ordType. Instances for other types can be transported via subtyping, injective functions, etc., as for other MathComp classes, or derived automatically using Deriving.

The function-like structures coerce into Coq functions, allowing us to write f x to retrieve the value of the map f at x. Similarly, sets coerce to SSReflect collective predicates, allowing us to write x \in A to express that x belongs to the set A.

Extensional reasoning is provided by the following lemmas:

eq_fset  : forall T   (A B : {fset T}),      A =i B <-> A = B
eq_fmap  : forall T S (f g : {fmap T -> S}), f =1 g <-> f = g
eq_ffun  : forall T S (def : T -> S) (f g : ffun def),
                                             f =1 g <-> f = g
eq_fperm : forall T   (f g : {fperm T}),     f =1 g <-> f = g

Documentation for the libraries is currently scarce, but will be progressively added as comments in the headers of the files. Once the package is installed, it can be required using the extructures qualifier.

From extructures Require Import ord fset.

Check the tests/ directory for detailed examples.

Installation

The easiest way to install the package is through the OPAM Coq archive. After installing OPAM and adding the Coq archive, run:

opam install coq-extructures

Alternatively, you can compile the package by hand. You'll need the following dependencies:

To compile the package, simply run

make

After compilation, you can install the package by running

make install

Alternatives

Other packages with similar goals are available out there.