# "Correct" way to structure modules
**URL:** https://discourse.rocq-prover.org/t/correct-way-to-structure-modules/1751
**Category:** Using Rocq
**Created:** [August 9, 2022, 12:10pm UTC](https://discourse.rocq-prover.org/t/correct-way-to-structure-modules/1751 "2022-08-09T12:10:05Z")
**Posts on this page:** 3
**Page:** 1
### Author:  [@io7m](https://discourse.rocq-prover.org/u/io7m)
#### Post date: [August 9, 2022, 12:10pm UTC](https://discourse.rocq-prover.org/t/correct-way-to-structure-modules/1751/1 "2022-08-09T12:10:05Z")
Hello. I’m going through what I assume is the normal rite of passage for Coq users, which I assume usually ends in a vow never to use the module system for anything ever again. 🙂
I’m trying to work out the “correct” way to structure something. This isn’t a real project, I’m just trying to work out what the best practices are. Here’s a trivial example:
```auto
Require Import Coq.Arith.PeanoNat.
Module Type Equatable.
Parameter t : Type.
Parameter eq : t -> t -> Prop.
Parameter eq_reflexive : forall x, eq x x.
Parameter eq_symmetric : forall x y, eq x y -> eq y x.
Parameter eq_transitive : forall x y z, eq x y -> eq y z -> eq x z.
End Equatable.
Module Type Ordered.
Parameter t : Type.
Parameter lt : t -> t -> Prop.
Parameter lt_irreflexive : forall x, ~lt x x.
Parameter lt_transitive : forall x y z, lt x y -> lt y z -> lt x z.
End Ordered.
Module NatEquatable <: Equatable.
Definition t := nat.
Definition eq : t -> t -> Prop := Logic.eq.
Definition eq_reflexive : forall x, eq x x.
Proof. intro x. apply eq_refl. Qed.
Definition eq_symmetric : forall x y, eq x y -> eq y x.
Proof. intros x y H. symmetry. exact H. Qed.
Definition eq_transitive : forall x y z, eq x y -> eq y z -> eq x z.
Proof.
intros x y z Hxy Hyz.
rewrite Hxy.
exact Hyz.
Qed.
End NatEquatable.
Module NatOrdered <: Ordered.
Definition t := nat.
Definition lt := Peano.lt.
Definition lt_irreflexive : forall x, ~lt x x.
Proof. apply Nat.lt_irrefl. Qed.
Definition lt_transitive : forall x y z, lt x y -> lt y z -> lt x z.
Proof. apply Nat.lt_trans. Qed.
End NatOrdered.
```
This is all fine, and works the way I would expect. However, now if I want to express the type of modules that abstract over types that are both `Equatable` and `Ordered`, I can’t do it with the above definitions:
```auto
Module Type EquatableOrdered := Equatable <+ Ordered.
```
_The label t is already declared._
I had a somewhat-more-than-brief look at `Coq.Structures.*`, and I see that it seems to use a pattern where `t` is included in its own module type that includes `t` and no other definitions, and every other module type `Import`s it. This seems pretty unpleasant, and having rewritten the above code to use something like it, seems to result in increasingly more redundant declarations:
```auto
Require Import Coq.Arith.PeanoNat.
Module Type T.
Parameter t : Type.
End T.
Module Type Equatable (Import T : T).
Parameter eq : t -> t -> Prop.
Parameter eq_reflexive : forall x, eq x x.
Parameter eq_symmetric : forall x y, eq x y -> eq y x.
Parameter eq_transitive : forall x y z, eq x y -> eq y z -> eq x z.
End Equatable.
Module Type Ordered (Import T : T).
Parameter lt : t -> t -> Prop.
Parameter lt_irreflexive : forall x, ~lt x x.
Parameter lt_transitive : forall x y z, lt x y -> lt y z -> lt x z.
End Ordered.
Module NatT <: T.
Definition t := nat.
End NatT.
Module NatEquatable <: Equatable NatT.
Definition t := nat.
Definition eq : t -> t -> Prop := Logic.eq.
Definition eq_reflexive : forall x, eq x x.
Proof. intro x. apply eq_refl. Qed.
Definition eq_symmetric : forall x y, eq x y -> eq y x.
Proof. intros x y H. symmetry. exact H. Qed.
Definition eq_transitive : forall x y z, eq x y -> eq y z -> eq x z.
Proof.
intros x y z Hxy Hyz.
rewrite Hxy.
exact Hyz.
Qed.
End NatEquatable.
Module NatOrdered <: Ordered NatT.
Definition t := nat.
Definition lt := Peano.lt.
Definition lt_irreflexive : forall x, ~lt x x.
Proof. apply Nat.lt_irrefl. Qed.
Definition lt_transitive : forall x y z, lt x y -> lt y z -> lt x z.
Proof. apply Nat.lt_trans. Qed.
End NatOrdered.
Module Type EquatableOrdered := T <+ Equatable <+ Ordered.
```
Is this the “expected” way the module system is supposed to behave? Is there a better way to express the above? In fact, having already written `NatEquatable` and `NatOrdered`, is there a way to have:
```auto
Module NatEquatableOrdered <: EquatableOrdered.
...
End NatEquatableOrdered.
```
… Without manually restating every definition in `NatOrdered` and `NatEquatable`?
---
### Author:  [@Matafou](https://discourse.rocq-prover.org/u/Matafou)
#### Post date: [August 9, 2022, 6:42pm UTC](https://discourse.rocq-prover.org/t/correct-way-to-structure-modules/1751/2 "2022-08-09T18:42:21Z")
I am not an expert at module design but you can use ˋImport`, even in module types. So restating is no big deal generally.
---
### Author:  [@io7m](https://discourse.rocq-prover.org/u/io7m)
#### Post date: [August 9, 2022, 7:07pm UTC](https://discourse.rocq-prover.org/t/correct-way-to-structure-modules/1751/3 "2022-08-09T19:07:15Z")
Unfortunately, frequently (and in the case above), using `Import` isn’t possible due to the same “_The label t is already declared._” class of error.