The Coq mailing list

[Kevin Hamlen <hamlen AT utdallas.edu>]

Dear Coq users,

What do Coq programmers consider the "right way" to organize large 
projects containing functors?  In particular, how do authors of large 
projects define collections of modules that all build upon some shared 
functor without getting duplicate name-conflicts? Here's an example:

(* Input parameters and axioms are declared as a module type: *)
Module Type FOO_TYPE.
  Parameter foo: Type.
End FOO_TYPE.

(* Another module builds definitions from the inputs: *)
Module FooDefs (Foo: FOO_TYPE).
  Inductive bar := Bar (f:Foo.foo).
  (* ... hundreds more definitions ... *)
End FooDefs.

(* Now we wish to create myriad modules that prove various things about 
FooDefs given a Foo.  Here's one way that doesn't work well: *)
Module FooTheory1 (Foo: FOO_TYPE).
  Module F := FooDefs Foo.
  Import F.
  Ltac silly1 := match goal with |- Bar _ = Bar _ => reflexivity end.
  (* ... more theorems, proofs, and ltacs ... *)
End FooTheory1.

(* This doesn't work well because each module defined in this way has 
its own copy of FooDefs, which Coq doesn't always recognize as equal. *)
Module Foo:FOO_TYPE.
  Definition foo:=nat.
End Foo.
Module FD := FooDefs Foo.
Module FT1 := FooTheory1 Foo.
Import FD.
Import FT1.
Theorem silly: forall (x:bar), x=x.
Proof.
  destruct x.
  Fail silly1. (* fails because FD.Bar is not the same as FT1.F.Bar. *)
Abort.


Here are two alternative options that also don't seem to work well:

(2) Using "Export F" in FooTheory1 instead of creating a separate FD 
module fixes the problem above, but then all FooTheory modules must be 
arranged in a linear hierarchy to avoid duplicating the definition of 
F.  They can't be created independently, lest they export two distinctly 
named versions of F.

(3) We could make a FOO_DEFS module type (whose content is a verbatim 
copy of FooDefs) and then parameterize all the FooTheory modules with 
FOO_DEFS instead of FOO_TYPE modules.  But that leads to a rather 
tortuous development regimen: Every new FooTheory module must also 
define a FOO_THEORY type that duplicates all its definitions, and 
instantiating the new FooTheory requires first laboriously instantiating 
all the modules it depends upon, just so that they can all import the 
shared definition of FooDefs.

What is the "right" way to do this sort of thing?

Thanks,
Kevin