The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Kevin,

I would say go with option 3) and use the <+ operator to combine modules and 
module types into larger ones in order to avoid the "tortuous development 
regimen with laboriously instantiating all the modules". I show below how 
this would look for your example and also show a little appendix D stuff.

In general this gets easier when you work more abstract. It is strange that 
most of your modules are living on their own without implementing any module 
type. If your developments look like this, it might be that you are using the 
module system just as a namespace system. The idea behind the module system 
is that you implement modules using only abstract definitions (what is in a 
module type) of other modules. If you generally depend on concrete 
implementations of other modules in module definitions, you end up with a lot 
of trouble of the kind you describe. If you mostly depend on what is in the 
module type in the definition of a module, things are much more natural. I 
usually work as abstract as possible, because this makes automation more 
efficient. If you have a lot of concrete details in the context you don't 
really need, automation will try to make use of it anyway rather than 
applying higher level abstract results, which should be sufficient. 
Especially simplification is not your friend if you work to concrete. Of 
cause this can get tricky, like working with abstract numbers, but things are 
improving. An important point with modules when going the abstract way is 
looking into opaque and transparent ascription and using "with x := y" in 
opaque ascriptions properly.

I agree that in complex developments there are corner cases between what 
should be a module type and what should be a module. In such cases I 
typically have both and use the Empty <+ trick shown below to make a module 
from a module type. Also building sensible collections of modules and module 
types using the <+ operator is a useful approach to simplify things.

I am generally interested in large scale maintainable proof engineering and 
try to understand what issues people end up with. If your project is open 
source, I would like to have a look at it (please send me a private mail in 
case).
 
Best regards,

Michael

Some ideas:

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

(* This might be used as both, a module and a module type, so define both *)
Module Type FOO_DEFS (Foo: FOO_TYPE).
   Inductive bar := Bar (f:Foo.foo).
End FOO_DEFS.

(* Make a module from a module type *)
Module FooDefs (Foo: FOO_TYPE).
  Include FOO_DEFS Foo.
End FooDefs.

(* There is an abbreviation for this.
   Use an Empty module to trick the <+ include operator in accepting a module 
type.
   The first operand of <+ must be a module in a module definition, but all 
others can be module tpes. *)

Module Empty.
End Empty.

Module FooDefs' (Foo: FOO_TYPE) := Empty <+ FOO_DEFS Foo.

(* Compare Print FooDefs and FooDefs' *)

(* Sometimes it is also useful to combine module types into one *)
Module Type FOO_WITH_DEFS := FOO_TYPE <+ FOO_DEFS.

(* Theory getting everything separately *)
Module FooTheory1 (Foo: FOO_TYPE) (F: FOO_DEFS Foo).
  Import F.
   Ltac silly1 := match goal with |- Bar _ = Bar _ => reflexivity end.
   (* ... more theorems, proofs, and ltacs ... *)
End FooTheory1.

(* Theory getting all in one *)
Module FooTheory2 (F: FOO_WITH_DEFS).
  Import F.
   Ltac silly2 := match goal with |- Bar _ = Bar _ => reflexivity end.
   (* ... more theorems, proofs, and ltacs ... *)
End FooTheory2.

(* 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 FD.
(* The all in one argument for FooTheory2 is easily created *)
Module FDX := Foo <+ FD.
Module FT2 := FooTheory2 FDX.
Import FD.
Import FT1.
Import FT2.

(* Both theories work fine *)

Theorem silly1: forall (x:bar), x=x.
Proof.
   destruct x.
   silly1.
Qed.

Theorem silly2: forall (x:bar), x=x.
Proof.
   destruct x.
   silly2.
Qed.

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928