The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

And just to add to Stéphane's answer, indeed I'd recommend also to 
directly prove an unfolding lemma after the definition to simplify 
reasoning on the function. In 8.3, it would look like that:

 Import WfExtensionality. (* (In Program/Wf) Assumes extensionality to get 
the general 
                        fixpoint unfolding lemma without conditions *)

 Lemma add_to_set_not_in_unfold (S:X.t)(H:X.t) :
   add_to_set_not_in S H = 
   match X.choose S with
     | None => X.empty
     | Some x => if Xp.In_dec x H then add_to_set_not_in (X.remove x S) H
                 else X.add x (add_to_set_not_in (X.remove x S) H)
   end.
 Proof.
   unfold add_to_set_not_in at 1.
   unfold_sub add_to_set_not_in_func (add_to_set_not_in_func (existT (fun _ : 
t => t) S H)). simpl.
   now destruct (choose S); [destruct Xp.In_dec|].
 Qed.

 Lemma teste : X.Equal (add_to_set_not_in X.empty X.empty) X.empty.
 Proof.
   rewrite add_to_set_not_in_unfold. 
   case_eq (choose empty). intros. admit (* invert choose empty = Some e *).
   intros. reflexivity.
 Qed.

-- Matthieu

Le 9 nov. 2010 à 11:33, Stéphane Lescuyer a écrit :

> 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
> 

-- Matthieu