The Coq mailing list

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

Just to extend on Xavier's answer, if you are only using Program for
the non-structural induction but not for programming with dependent
types, you should rather try using Function instead. The difference is
that Function will create a handy "unfolding" equation which makes it
easy to reason about your function after it has been defined.

Also, beware of using Xp.In_dec instead of X.mem in your functions.

S.

On Tue, Nov 9, 2010 at 10:49 AM, Xavier Leroy 
<Xavier.Leroy AT inria.fr>
 wrote:
> 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
>



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