Formalization of a finite sets library in Coq

This page presents the formalization in the Coq proof assistant of a finite sets library. It actually contains three different implementations of finite sets: using ordered lists, red-black trees and AVLs. This formalization heavily uses modules and functors, a novelty in Coq 7.4, demonstrating their power in the context of proof, as well as in the context of programming.

LRI Research report: Functors for Proofs and Programs (PostScript file). To be presented at ESOP 2004

Original Ocaml code

• Red-black trees: rbset.mli / rbset.ml / rbset.ps
• AVL from the Ocaml standard library: set.mli / set.ml

Ocaml code obtained by extraction

• Red-black trees: rbt.mli / rbt.ml
• AVL: avl.mli / avl.ml

Coq sources

• Browse the Coq sources:
  • Global index
  • Table of contents
  • FSetInterface : signatures for ordered type (OrderedType) and finite sets (S and Sdep)
  • FSetBridge bridges (as functors) from dependent to/from non-dependent set signature
  • FSetProperties additional properties that can be derived
  • FSetList : implementation using sorted lists
  • FSetRBT : implementation using red-black trees
  • FSetAVL : implementation using AVLs
  • FSet load everything
• Download the sources: FSets.tar.gz / FSets for Coq V8.0
• PostScript file