The Coq mailing list

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

Dear Coq Team & Users,

 

I tried to separate some of my samples from my infrastructure in order to deliver them to Benjamin and found that the main issue here comes from the module system. I changed many module definitions in the standard library, so that I can live with them. The changes are simple and easy to maintain, but it makes it very hard for me to share samples.

 

The issues I have comes from definitions like:

 

https://coq.inria.fr/library/Coq.ZArith.BinInt.html#

 

Module Z

  <: ZAxiomsSig

  <: UsualOrderedTypeFull

  <: UsualDecidableTypeFull

  <: TotalOrder.

 

The problem here is that it is impossible (afaik – I discussed this on the list a while ago) to define the abstract module type of module Z without literally copying the definition of 3 of the 4 involved module types, because all of them include a type definition named “t”. I tried a lot of things, e.g. defining local modules with the common definitions bound together using “with Definition t:=XYZ.t” and including these, but to no effect.

 

I use a lot of automation and automation frequently works better with abstract definitions. If it is not required for a proof to know how e.g. Z is actually defined, it is obviously easier to find the proof automatically if the proof databases don’t contain these unnecessary details, e.g. the systems doesn’t have the option to destruct a Z. For this reason I do a lot of proofs in modules with the involved types defined as abstractly as possible to get the proof done as module types. Obviously this also results in more flexible results. But this requires either

 

1.)    a lot of module type signature cut and paste

2.)    changing every other module type definition in the standard library to a module type functor getting the involved type- and e.g. operator definitions as module type parameters

3.)    enhance Coq’s module system with a module type merge operator, which gives a module type equivalent to the type of Module Z above without signature cut & paste.

I went with method 2, which makes my samples incompatible with the rest of the Coq world – or too large to be manageable because I have my own copy of the standard library.

 

I wonder how others are handling this? Maybe I am just doing something wrong? Or maybe others prefer type classes or canonical instances over modules?

 

In case there is no solution, what would be the proposed fix? I actually would prefer to have 2.) and 3.). I could help with 2.) and deliver a standard library changed to use module type functors plus compatibility files which create the currently existing module types from the newly defined functors. In my version of the lib I also renamed some module types so that it is more obvious from the name what the difference between various variants is, but I would keep the names of all module types as they exist now in the compatibility files.

 

I find this more elegant and flexible than 3.) - I feel the merging of definitions of t, eq, … in the above definition of Z is a bit of a hack, but having 3.) can still be nice for exploring ideas quickly.

 

Best regards,

 

Michael

 

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