The Coq mailing list

[J�r�mie Koenig <jk AT jk.fr.eu.org>]

On Tue, Jan 17, 2012 at 6:41 PM,  
<td202 AT doc.ic.ac.uk>
 wrote:
> Is there some way that I can get Coq to identify MyB.X and MyC.X?

I don't think so. The "Module X := ..." commands in B and C create two
different modules.

> If not, is there a sensible workaround?

You need to instanciate a unique A module outside B and C, and pass it to 
them.

For instance:

Module Type KO.
Parameter x : Type.
End KO.

Module Type Ah (Import ko : KO).
Parameter foo : Type.
Parameter zeb : x -> foo.
End Ah.

Module A (Import ko : KO).
Inductive foo_ := zeb_ : x -> foo_.
Definition foo := foo_.
Definition zeb := zeb_.
End A.

Module B (ko : KO) (Import X : Ah ko).
Definition flob (f : foo) : foo := f.
End B.

Module C (ko : KO) (Import X : Ah ko).
Definition flip (f : foo) : foo := f.
End C.

Module D (ko : KO).
Module X : Ah ko := A ko.
Module Import MyB := B ko X.
Module Import MyC := C ko X.

Lemma flobflip : forall f, flob (flip f) = f.
admit.
Qed.
End D.

-- 
Jérémie Koenig 
<jk AT jk.fr.eu.org>
http://jk.fr.eu.org/