The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

David Pereira wrote:

> I am experimenting with Program Fixpoint feature of Coq for building
> functions on finite sets. [...] Is there any standard tricks for
> reasoning about terms built using the Program Fixpoint construction?

In the case of "measured" or well-founded functions, none that I know of :-(

As far as I know, the idiomatic way to use Program Fixpoint {measure}
is to return an "informative" type {x | P x} where P captures
everything you'd ever want to know later about the result of the function.
E.g. in your case,

Program Fixpoint add_to_set_not_in (S:X.t)(H:X.t) { measure X.cardinal S} :
    { R : X.t | forall x, X.In x R <-> X.In x S /\ ~X.In x H } :=
  ... (* same code as before *)

Program Fixpoint then generates the appropriate proof obligations to
show both termination and satisfaction of the spec.

Two more remarks.  First, I may very well be wrong, but your function
looks like set difference, in which case it is already available as X.diff.

Second, the "fold" operator over sets is a very good way to define
functions that need to enumerate all elements of a set.  It comes with
a nifty induction principle in FSetProperties that allows you to prove
properties in a fairly natural way.

Hope this helps,

- Xavier Leroy