The Coq mailing list

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

Dear Coq Users,

 

just before I rewrite half of the standard library (I just made variants of Equalities, Orders, GenericMinMax and NZAxioms where all module types get the base type as parameter), can someone confirm that there is no way to combine two module types with a common element (say a type t) into one bigger module type (see the example below)?

 

In case this is not possible: how do you live with the structure module types as defined in the standard library? Is there a good reason why was the standard library is done like this, that is it for some reason a bad idea to give every module type a type parameter (and maybe some others)?

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Soegtrop, Michael
Sent: Thursday, June 30, 2016 6:45 PM
To: coq-club AT inria.fr
Subject: [Coq-Club] How to define a module type for NAxioms.NAxiomsSig + Orders.UsualOrderedTypeFull + ... effectively?

 

Dear Coq Users,

 

the file Coq.NArith.BinNat contains this definition:

 

Module N

<: NAxiomsSig

<: UsualOrderedTypeFull

<: UsualDecidableTypeFull

<: TotalOrder.

 

I wonder if there is an effective way to define a Module Type with the same interface as the 4 module types given above combined? Just chaining them with <+ like this:

 

Module Type NatInt :=

     NAxioms.NAxiomsSig

  <+ Orders.UsualOrderedTypeFull

  <+ Equalities.UsualDecidableTypeFull

  <+ Orders.TotalOrder.

 

fails, because all of them contain a type t. The only way I see is to include e.g. UsualOrderedTypeFull is to include all its components as shown in this image:

 

 

the colored boxes are module type functors, the white ones module types including a type t. Blue are functions, red are specifications, the darker ones contain definitions/lemmas, the light ones contain parameters/axioms.

 

Is there a smart way of doing this without essentially copying the definition of UsualOrderedTypeFull, UsualDecidableTypeFull and TotalOrder?

 

Should I create Module Type functors matching all the white boxes above?

 

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

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