The Coq mailing list

[Randy Pollack <rap AT inf.ed.ac.uk>]

Hello,

I'm playing with modules for the first time.  Here are some questions.

Is it possible to have a hypothetical module?  For example, consider a
signature of "identifiers"

 Module Type Id.
  Parameter X: Set.
  Axiom Xdec: (x,y:X){x=y}+{~x=y}.
 End Id.

It is obvious that this signature can be instantiated, e.g. by taking
X:=nat.  But I only want an abstract module satisfying Id, so I'd like
to say  (at the toplevel):

 Declare Module Variables : Id.

Is there some way to do this?

Since I don't see how to do that, I instantiated the signature with a
ground module:

 Module Var: Id.
  Definition X := nat.
  ...
 End Var.

Now I also want another module for parameters, Par:Id.  I can write

 Module Par: Id.
  Definition X := nat.
  ...
 End Par.

and since Var and Par are abstract, Var.X <> Par.X, as desired.

However, I was surprised to see that I can also write

 Module Par: Id := Var

and still have Var.X <> Par.X.  Since modules have strengthening, this
is against my intuition.  What is the explanation?

Best,
Randy