"Correct" way to structure modules

Using Coq
1

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. :slightly_smiling_face:

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:

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:

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 Imports it. This seems pretty unpleasant, and having rewritten the above code to use something like it, seems to result in increasingly more redundant declarations:

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:

Module NatEquatableOrdered <: EquatableOrdered.
  ...
End NatEquatableOrdered.

… Without manually restating every definition in NatOrdered and NatEquatable?

1 Like
2

I am not an expert at module design but you can use ˋImport`, even in module types. So restating is no big deal generally.

3

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.