The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Dear All,

The issue I am trying to solve is the following. I have a part of my
development where basically everything depends of a parameter. Let us
say S: Set. The part that depends on this parameter is, say, 5 files.
The most straightforward way to handle this would be to start every
definition and theorem with 'forall S: Set,'. As such that is possible
but it becomes really irritative when one realizes that all the things
one defines in this development also need to be passed this parameter
S. The code would basically be littered with S-es all over the place.
One possible way to solve this would be to turn S into an implicit
parameter in most places. This would help a bit, but I do not really
like the result of this too much because still quite a few S-es are
left and now one has to omit some parameters somewhere but not
everywhere. It is not that convenient.

So, I thought, let us use the module system to solve this. I put the
parameter S in a 'Module Type', and all of the code in a module that
depends on this Module Type. The problem is with the 5 files that
depend on one another. These 5 files each get a module that depends on
the Module Type and some of these modules need to Import some of the
other modules. What I am now running into is that when I import a
module it seems to basically copy the module contents. So, if module_1
contains and inductive definition D and module_2 imports module_1
there are now two inductive definitions module_1.D and module_2.D and
where it expects a parameter of type module_1.D it is not possible to
pass a parameter of type module_2.D. See example-1 below.

I think I can solve this by kind of linearly chaining these modules.
See example-2 below. After this I could just use the outer module
(Module5) and only mention things in de modules by going through
Module5 to avoid the confusion of the multiply defined objects.
Problem here are that the Imports get pretty ugly and that
conceptually these modules do not depend linearly on each other. It
may be that logically speaking one would like to use only Module1,
Module2 and Module4 and not import the rest of them because as such
they would not apply at certain place.

Anyone any ideas about this? Am I misusing the module system terribly?

Kind Regards,
Chris


Example-1:

Module Type Thing.
   Parameter S: Set.
End Thing.

Module Module1 (T: Thing).
   Inductive flups: Set := flups1 | flups2.
End Module1.

Module Module2 (T: Thing).
   Module mod1 := Module1 T.
   Import mod1.
End Module2.

Module SpecificThing <: Thing.
   Definition S: Set := nat.
End SpecificThing.

Module SpecificModule1 := Module1 SpecificThing.
Module SpecificModule2 := Module2 SpecificThing.

Parameter p: SpecificModule1.flups.
Goal SpecificModule2.mod1.flups.
exact p.
Error: The term "p" has type "SpecificModule1.flups"
while it is expected to have type "SpecificModule2.mod1.flups".

Example-2:

Module Type Thing.
   Parameter S: Set.
End Thing.

Module Module1 (T: Thing).
   Inductive flups: Set := flups1 | flups2.
End Module1.

Module Module2 (T: Thing).
   Module mod1 := Module1 T.
   Export mod1.
End Module2.

Module Module3 (T: Thing).
   Module mod2 := Module2 T.
   Export mod2.
End Module3.

Module Module4 (T: Thing).
   Module mod3 := Module3 T.
   Export mod3.
End Module4.

Module Module5 (T: Thing).
   Module mod4 := Module4 T.
   Export mod4.
End Module5.

Module SpecificThing <: Thing.
   Definition S: Set := nat.
End SpecificThing.

Module SpecificModule5 := Module5 SpecificThing.
Import SpecificModule5.
Import SpecificModule5.mod4.
Import SpecificModule5.mod4.mod3.
Import SpecificModule5.mod4.mod3.mod2.
Import SpecificModule5.mod4.mod3.mod2.mod1.

Check flups. (* flups: Set *)