The Coq mailing list

[Meven LENNON-BERTRAND <Meven.Bertrand AT univ-nantes.fr>]

    To add to Adam’s answer, the key tool to packaging structures in the
    Mathematical Components project (or, actually, the Hierarchy
      Builder tool, which is now a standalone project) are record
      types. They are quite similar to modules, but with a somewhat
    different trade-off in the precise functionalities. In particular,
    they are first-class types. The best reference I know of to
    compare the different forms of "packaging" available in Coq is this
      short abstract for the Types conferences, it might be of
    interest to you, although it’s quite short…
Meven LENNON-BERTRAND
Doctorant, Équipe Gallinette – LS2N – Université de Nantes
www.meven.ac

Le 13/03/2022 à 13:43, Adam Chlipala a écrit :

On 3/12/22 11:10 PM, Constantine Plotnikov wrote:

  Module Type AbelianGroup.
    Include Group.
    Axiom comutative : forall a b : T, operation a b = operation b a.
  End AbelianGroup.

  [...]

    Theorem plus_group : AbelianGroup with T := T, operation := plus, identity = zero, inverse = unary_minus).
      (* proof that it exists with specified operators *)
    End plus_group.

As you've discovered here, modules are not first-class in Coq.  There is no way to define a module from within a Gallina term, just to reference module members.  I suppose technically the Coq vernacular language could allow use of the tactic mode to define a complete module (albeit with the complication that the goal is no longer a Gallina term), but I don't think that support exists either.

You may not be aware that the style of definition you are pursuing is already one of the standard uses of Coq, rather than a fully novel experiment.  The Mathematical Components project may be the most extensive work with algebraic hierarchies.  They use canonical structures (a relative of type classes) instead of modules.