CODEWITHSUNDEEP
modulecoq
Joachim Breitner
Joachim Breitner

Reputation: 25763

Default implementations in coq’s Modules

I have an interface that I want to implement several times:

Module Type I.
  Parameter a : A.
  Parameter b : B.
  Parameter c : C.
End I.

(and assume that each of a, b and c are actually many definitions).

An implementation would be

Module Imp1 <: I.
  Definition a : A := bar.
  Definition b : B := foo a.
  Definition c : C := baz a b.
End I.

Now it turns out that many implementations share the definition of b (which require a), but have different definitions of c.

How can I centralize the definition of b? Preferably without changing I or duplicating lots of definitions thereof?

(I imagine writing a module functor BImp expecting a:A as some kind of parameter, and then I can Import (BImp a).)

Upvotes: 0

Views: 278

Answers (2)

user3551663
user3551663

Reputation:

You can instanciate modules inside other modules. This forces you to duplicate part the modules' signatures, but not the proofs the modules contain.

Module Type PreorderSignature.
Parameter Inline type : Type.
Parameter Inline less : type -> type -> Prop.
Parameter Inline reflexivity : forall x1, less x1 x1.
Parameter Inline transitivity : forall x1 x2 x3, less x1 x2 -> less x2 x3 -> less x1 x3.
End PreorderSignature.

Module Preorder (PS : PreorderSignature).
Import PS.
(* Preorder facts. *)
End Preorder.

Module Type EquivalenceRelationSignature.
Parameter Inline type : Type.
Parameter Inline equal : type -> type -> Prop.
Parameter Inline reflexivity : forall x1, equal x1 x1.
Parameter Inline symmetry : forall x1 x2, equal x1 x2 -> equal x2 x1.
Parameter Inline transitivity : forall x1 x2 x3, equal x1 x2 -> equal x2 x3 -> equal x1 x3.
End EquivalenceRelationSignature.

Module EquivalenceRelation (ERS : EquivalenceRelationSignature).
Import ERS.
Module PreorderSignatureInstance <: PreorderSignature.
Definition type := type.
Definition less := equal.
Definition reflexivity := reflexivity.
Definition transitivity := transitivity.
End PreorderSignatureInstance.
Module PreorderInstance := Preorder PreorderSignatureInstance.
Import PreorderInstance.
(* Now your equivalence relations will inherit all the facts about preorders. *)
(* Other equivalence relation facts. *)
End EquivalenceRelation.

Module Type PartialOrderSignature.
Parameter Inline type : Type.
Parameter Inline less : type -> type -> Prop.
Parameter Inline reflexivity : forall x1, less x1 x1.
Parameter Inline antisymmetry : forall x1 x2, less x1 x2 -> less x2 x1 -> x1 = x2.
Parameter Inline transitivity : forall x1 x2 x3, less x1 x2 -> less x2 x3 -> less x1 x3.
End PartialOrderSignature.

Module PartialOrder (POS : PartialOrderSignature).
Import POS.
Module PreorderSignatureInstance <: PreorderSignature.
Definition type := type.
Definition less := less.
Definition reflexivity := reflexivity.
Definition transitivity := transitivity.
End PreorderSignatureInstance.
Module PreorderInstance := Preorder PreorderSignatureInstance.
Import PreorderInstance.
(* Now your partial orders will inherit all the facts about preorders. *)
(* Other partial order facts. *)
End PartialOrder.

And to flatten the module hierarchy a bit you can use the Import and Parameter Inline commands.

Upvotes: 0

Konstantin Weitz
Konstantin Weitz

Reputation: 6422

You can outsource your shared definitions into a global definition (here outsourced) parameterized on the changing parts of your module (here a). I don't know if there is something like Haskell's default implementations.

Module Type I.
  Parameter a : A.
  Parameter b : B.
  Parameter c : C.
End I.

Definition outsourced (a:A) := foo a.

Module Imp1 <: I.
  Definition a : A := bar.
  Definition b : B := outsourced a.
  Definition c : C := baz a b.
End Imp1.

Module Imp2 <: I.
  Definition a : A := bar'.
  Definition b : B := outsourced a.
  Definition c : C := baz' a b.
End Imp2.

Upvotes: 1

Related Questions