The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi,

If you are interested in the powerset construction for finite sets as
in 'the powerset construction' or 'subset construction' that converts
NFA to DFA, you might have a look to our ATBR library [1] that
features a decision procedure for Kleene algebras implemented through
construction, determinisation and equivalence checking of finite
automata in Coq, using a lot of FSets and FMaps. In particular, we
have a module that determinise epsilon-free finite autmata.

Alternatively, if you wish to implement the powerset construction that
builds the 2^n subsets of a given set of size n,  here is a piece of
code that should do the job [2]...

thomas
[1] http://sardes.inrialpes.fr/~braibant/atbr
[2]


Require Import FSets FSetInterface.
Require Import Program.Wf.
Module subset ( M : FSetInterface.S).
  Module MSet := FSetList.Make (M). (* or FSetAVL , to represent sets of sets 
*)

  Definition add x (m : MSet.t) : MSet.t :=
    MSet.fold (fun s acc => MSet.add (M.add x s) acc ) m MSet.empty.

  Program Fixpoint subset (s : M.t) {measure (M.cardinal s)}: MSet.t :=
    match M.choose s with
      | None => MSet.empty
      | Some x => let s := subset (M.remove x s) in
        MSet.union (add x s) s
    end.
  Next Obligation. Admitted. (* the size is decreasing *)

End subset.


On Wed, Jul 21, 2010 at 7:35 PM, David Pereira 
<dpereira AT liacc.up.pt>
 wrote:
> Hi all,
>
> Does anyone know about any implementation of the powerset construction for 
> finite sets that is compatible with the FSet library of Coq's standard 
> library?
>
> Thanks in advance.
>
> Best regards,
>  David.
>
>
>
>