Finite Sets over Countalbe Types in Ssreflect

Saarland University Computer Science

We develop a library for finite sets using Ssreflect. In contrast to the "finset" library in Ssreflect, which only allows finite base types, we allow countable types as base types. Finite sets are implemented as a quotient on lists using some canonical duplicate free list as representative. We provide most of the basic theory as well as constructions for least and greatest fixpoints and maximal extensions.

Theory Files (requires mathcomp-ssreflect-1.6)

Theory Files (requires ssreflect-1.5)

Coqdoc Documentation

Used in

Completeness and Decidability Results for CTL in Coq (ITP 2014)

Completeness and Decidability Results for CTL in Coq (Extended Version)


Webmaster, Tue Aug 16 10:42:32 2016