The Coq mailing list

["Andrew McCreight" <continuation AT gmail.com>]

My goal was simply to avoid the warning messages.  I don't actually use the setoid equalities of FSetFacts, so I don't need to include them in the signature.  Instead, I prove extensional equality for list sets, and use "real" equality.

-Andrew

On Fri, Jun 6, 2008 at 7:51 AM, Aaron Bohannon <bohannon AT cis.upenn.edu> wrote:

I tried something like that, but I don't understand how it can be made
to work.  Is there a way to write a signature for FSetFacts that
declares information about the setoid it defines?  Otherwise, the
client functor G will not be able to use rewriting in the setoid.  To
give a concrete example, how can I design G so that the rewriting
tactic in the proof will work, other than uncommenting the third line?

Require Import FSets.
Module G (MyFSet : FSetInterface.S).
 (* Module MyFacts := FSetFacts.Facts MyFSet. *)
 Lemma foo : forall x y s,
   MyFSet.E.eq x y -> MyFSet.In x s -> MyFSet.In y s.
 Proof.
   intros x y s Heq H. rewrite -> Heq in H. assumption.
 Qed.
End G.

 - Aaron

On Thu, Jun 5, 2008 at 5:58 PM, Andrew McCreight <continuation AT gmail.com> wrote:
> I had this exact same problem.  I think my solution was to define a
> signature for sets + (some subset of) FSetFacts and use that as a functor
> argument instead of the raw set.  It is a little ugly, especially given that
> you can't really unpack a module inside of another module, so there is
> always an extra level of indirection (unless you import the outer module,
> which is not something you usually want to do, because you'll usually have
> more than one kind of set sitting around).
>
> -Andrew
>
> On Thu, Jun 5, 2008 at 2:21 PM, Aaron Bohannon <bohannon AT cis.upenn.edu>
> wrote:
>>
>> I've noticed a bad interaction between setoids and the module system.
>> If a setoid is defined in a functor (let's call it F), then apparently
>> that functor must only be instantiated exactly once (otherwise, you
>> will see a long warning and rewriting in the setoid will stop
>> working).  This doesn't sound like a huge problem (why would you
>> instantiate a functor twice?), until you try to write another functor
>> G (in its own file) with proofs that require rewriting in the setoid
>> defined in F.  In order for the file containing G to compile, G must
>> instantiate F internally.  Thus, one must be sure to never instantiate
>> F outside of G.  OK, now that's already a software engineering
>> nightmare, but worse, imagine two functors G1 and G2 that both require
>> access to rewriting in the setoid defined in F.  Now you're completely
>> stuck.
>>
>> I'm not sure if I can call this a bug, because there is no simple,
>> obvious solution.  The only thing that comes to mind would be to allow
>> abstraction over setoid and morphism declarations by including them in
>> module types.  Is anybody working on this issue?  Does anybody know of
>> good work-arounds?  For a specific example of such a functor F, see
>> the FSetFacts file from the standard library.
>>
>>  - Aaron
>>
>> --------------------------------------------------------
>> Bug reports: http://logical.futurs.inria.fr/coq-bugs
>> Archives: http://pauillac.inria.fr/pipermail/coq-club
>>          http://pauillac.inria.fr/bin/wilma/coq-club
>> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
>