The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Fri, Jun 06, 2008 at 10:51:33AM -0400, Aaron Bohannon 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
> 


Hi Aaron, Hi Andrew,

For the moment, I haven't managed yet to reproduce the issue you're
mentioning. For instance, if I take the above code and duplicate the
line about MyFacts into a MyFacts2 line, nothing strange happen on my
machine, not even any warning. Could you please give me some code
triggering the bug, as well as the exact coq version you're using (svn
revision...)?

In the meanwhile, I've killed in FSets one duplication of
FSetFacts.WFacts instances that Aaron mentionned to my privately: in
FSetProperties.WProperties, there's no need to create a new WFacts
instance FM, since this module contains an instance Dec of
FSetDecide.WDecide that itself contains an instance F of WFacts. So a
simple FM:=Dec.F can replace the earlier FM:=WFacts E M (see svn
commit 11064). 

This small change is far from ending this discussion, but it indicates
at least that in many situations the duplication can be suppressed
easily, especially if dependencies are linear (here WFacts --> WDecide
--> WProperties). Of course, the duplication issue may remain in more
complex situations (diamond dependencies, for instance). That's why we
should investigate this problem with setoid rewrite and fix it. As
far as I know, the earlier implementation of setoid rewrite was
working in this situation (although it was generating tons of warning)
and I don't see why the new version would not be able to do it as
well.

A last comment about your idea of using restrictive module types: it
may be interesting as a quick workaround, but I doubt it can provide
you more than that. Anyway, if you're looking for a way to declare a
setoid relation and morphisms in a module type, you can have a look at
theories/Numbers/NatInt/NZAxioms.v in a recent coq svn archive.

Best regards,
Pierre Letouzey