The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

A bigger issue seems to be that Coq provides (at least) three ways to
deal with this kind of kind of modularity: classes, structures and
modules.

This makes it difficult to organize the stdlib.

I know there are thoughts on merging some of these. I don't recall
having seen a CEP, though.

On Sun, Jul 30, 2017 at 4:01 PM, Elvis M. Detty 
<beque AT protonmail.com>
 wrote:
> № 3 sounds lovely! I just spent the last week or so fighting my "module
> merger" scripts*, so Michael's mail hit a nerve :).
>
> I dream about a "lax Include", where the definitions are only included if
> the module itself does not provide its own.
>
> ElMa
>
> *: In my project I use scripts to do № 1: copy base module verbatim over to
> the bottom of the git repo, then git rebase over it to adapt the derived
> module to the parent
>
> This is of course fragile, and invalidates all git references in the
> process, so cannot really recommend.
>
>
> Sent with ProtonMail Secure Email.
>
> -------- Original Message --------
> Subject: [Coq-Club] Issues with the module system
> Local Time: July 30, 2017 2:05 AM
> UTC Time: July 30, 2017 9:05 AM
> From: 
> michael.soegtrop AT intel.com
> To: 
> coq-club AT inria.fr
>  
> <coq-club AT inria.fr>
>
>
> 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
>
>