The Coq mailing list

[Adam Koprowski <koper AT astercity.net>]

  I'm working on a big project in Coq 8.0 and I really appreciate all its new
features, including module system (which is not new to Coq 8.0 but is new for 
me). But I have ran kind of too many times into problems with them. I hope 
that's just because I'm not experienced with modules and some more experienced 
users can help me figure out what I'm doing wrong. Below are my 3 module-related 
problems. If anyone can help me with any of them (especially 1st one) I'll be 
really grateful! And although the examples are very artificial (to make them 
short and readable) in case of every presented problem I run into it in course 
of my development and it caused my some trouble.

(1) Below is a structure of my modules simplified and without a content. My 
problem is to make Coq unify between modules H.T and Comp.T (which are clearly 
the same) in module HorpoWF. Basically I won't to get rid of an error message 
that appears when trying to enter definition for HorpoWF.x. Note that in case 
Term is just a definition (not an inductive one) everything works fine.

> Module Type Signature.
>   Parameter A: Set.
> End Signature.
>
> Module Terms (S: Signature).
>   Inductive Term: Set :=
>   | blah: Term.
> End Terms.
>
> Module Horpo (S: Signature).
>   Module T := Terms S.
> End Horpo.
>
> Module Computability (S: Signature).
>   Module T := Terms S.
> End Computability.
>
> Module HorpoWF (S: Signature).
>   Module H := Horpo S.
>   Module Comp := Computability S.
>
>   Variable a: H.T.Term.
>   Variable b: Comp.T.Term.
>   Definition x := a = b. (* ERROR! *)
>    (* The term "b" has type "Comp.T.Term" while it is *)
>    (* expected to have type "H.T.Term" *)
> End HorpoWF.


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

  For second one imagine that we want a functor with order over given set as 
argument.
> Module Type X.
>   Parameter A: Set.
> End X.

 As Coq doesn't allow even on syntax level to write:
> Module Test (S: X) (O: Order' with Definition R.A := S.A).

 The only solution I can see is to write:
> Module Test (S: X)(R: Relation' with Definition A := S.A)
>                   (O: Order' with Module R := R).
 As the chain of modules leading to Order' gets longer it is obviously getting 
very inconvenient.


(3) It's not rare to have situation where some definitions are interleaved with 
parameters over which we want to abstract. So we have:

Parameters_1
Definitions_1
Parameters_2
Definitions_2
...

  of course everything can depend on what was above. As putting definitions in 
module type is not very convenient because then when giving implementation one 
has to repeat them, for me an obvious solution was to split it into modules and 
module types as below:

> Module Type MA.
>   (* Parameters_1 *)
> End MA.
>
> Module MB (A: MA).
>   (* Definitions_1 *)
> End MB.
>
> Module Type MC.
>   Declare Module A : MA.
>   Declare Module B := MB A.
>   (* Parameters_2 *)
> End MC.

 but the declaration of module B inside MC is rejected by Coq with a message: 
"Only simple modules allowed in module declarations".

  Any suggestions?
   Kind regards,
    Adam Koprowski

--
----------------------------------------------------
-         
akoprow AT cs.vu.nl,
 ICQ: 3204612           -
-  The difference between impossible and possible  -
-      lies in determination (Tommy Lasorda)       -
----------------------------------------------------