The Coq mailing list

[Frederic Blanqui <blanqui AT loria.fr>]

On Wed, 19 May 2004, Adam Koprowski wrote:

> (2) Let's say we have a hierarchy of modules one being refinement of 
> another.
> For instance modules describing order with more and more assumptions about 
> it.
> Below I'll restrict to two modules but in principle there can be much more.
>    I can see two methods (at least) of such definition.
>
>  > Module Type Relation.
>  >   Parameter A: Set.
>  >   Parameter R: A -> A -> Prop.
>  > End Relation.
>  >
>  > Module Type Order.
>  >   Parameter A: Set.
>  >   Declare Module R: Relation with Definition A := A.
>  >   Parameter R_irr: forall (a: A), ~R.R a a.
>  > End Order.
>
>    or
>
>  > Module Type Relation'.
>  >   Parameter A: Set.
>  >   Parameter R: A -> A -> Prop.
>  > End Relation'.
>  >
>  > Module Type Order'.
>  >   Declare Module R: Relation.
>  >   Parameter R_irr: forall (a: R.A), ~R.R a a.
>  > End Order'.
>
>    Both approaches have disadvantages. It is possible to avoid them?
>
>    For the first one let's imagine a functor that takes as argument a module
> representing relation and another one representing it's extension to an 
> order.
> One would like to write:
>  > Module Test (R: Relation)(O: Order with Module R := R).
>    which of course is not accepted by Coq (Signature components for label A 
> do
> not match)


write O: Order with Definition A := R.A with Module R := R instead!