The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

You should probably use [fold] to iterate over the elements in the
[subset] function (better computational behaviour and easier reasoning
on the function after its been defined, than with Program Fixpoint).
Also, using the accumulator in [add] to get rid of the extra [union]
yields the following code:

Module Powerset (M : FSetInterface.S).
  Module MSet := FSetList.Make(M).

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

  Definition powerset (s : M.t) : MSet.t :=
    M.fold add s MSet.empty.
End Powerset.

With the following invariants for the functions:
  Property add_spec :
    forall x m s, MSet.In s (add x m) <->
      (MSet.In s m \/ exists s', MSet.In s' m /\ M.Equal (M.add x s') s).

  Property powerset_spec :
    forall s s', MSet.In s' (powerset s) <-> M.Subset s' s.

Cheers,

Stéphane
-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06