# Use a submodule of OrderedType in FSets
**URL:** https://discourse.rocq-prover.org/t/use-a-submodule-of-orderedtype-in-fsets/383
**Category:** Using Rocq
**Created:** [August 6, 2019, 7:20am UTC](https://discourse.rocq-prover.org/t/use-a-submodule-of-orderedtype-in-fsets/383 "2019-08-06T07:20:07Z")
**Posts on this page:** 5
**Page:** 1
### Author:  [@mht208](https://discourse.rocq-prover.org/u/mht208)
#### Post date: [August 6, 2019, 7:20am UTC](https://discourse.rocq-prover.org/t/use-a-submodule-of-orderedtype-in-fsets/383/1 "2019-08-06T07:20:07Z")
I’d like to make a submodule of OrderedType and then use the submodule in FSets with the following code.
```
From Coq Require Import OrderedType FSets.
Module Type NewOT <: OrderedType.OrderedType.
Include OrderedType.OrderedType.
Parameter foo : t -> t -> bool.
End NewOT.
Module Type NewSet <: FSetInterface.S.
Declare Module E : NewOT.
Include Sfun E.
End NewSet.
Module Make (O : NewOT) := FSetList.Make O.
Module Make' (O : NewOT) <: NewSet with Module E := O := FSetList.Make O.
```
Unfortunately, Coq (version 8.9.1) reported “Error: The field foo is missing in Top.Make’.E.”. How can I solve this problem?
---
### Author:  [@herbelin](https://discourse.rocq-prover.org/u/herbelin)
#### Post date: [August 7, 2019, 7:32pm UTC](https://discourse.rocq-prover.org/t/use-a-submodule-of-orderedtype-in-fsets/383/2 "2019-08-07T19:32:09Z")
The following seems to work:
```auto
From Coq Require Import OrderedType FSets.
Module Type NewOT <: OrderedType.OrderedType.
Include OrderedType.OrderedType.
Parameter foo : t -> t -> bool.
End NewOT.
Module Type NewSet <: FSetInterface.S.
Declare Module E' : NewOT.
Module E : OrderedType.OrderedType := E'.
Include Sfun E.
End NewSet.
Module Make (O : NewOT) := FSetList.Make O.
Module Make' (O : NewOT) <: NewSet with Module E' := O.
Module E' := O.
Include FSetList.Make O.
End Make'.
```
The module `E` inherited from `FSetList.Make O` has only type `OrderedType` so keeping a copy of `E` that includes `foo` seems necessary.
---
### Author:  [@mht208](https://discourse.rocq-prover.org/u/mht208)
#### Post date: [August 10, 2019, 2:05pm UTC](https://discourse.rocq-prover.org/t/use-a-submodule-of-orderedtype-in-fsets/383/3 "2019-08-10T14:05:20Z")
Thank you. But then I have another problem in using foo together with functions in FSetInterface.S.
In the following code, the lemma test cannot be defined.
The error message is: The term “x” has type “S.elt” while it is expected to have type “S.E’.t”.
```
Module Lemmas (S : NewSet).
Lemma test :
forall (x y : S.elt) (s : S.t),
S.mem x s = S.mem y s -> S.E'.foo x y = true.
Proof.
Admitted.
End Lemmas.
```
In the following code, the lemma test cannot be defined.
The error message is: The term “x” has type “S.E’.t” while it is expected to have type “S.elt”.
```
Module Lemmas (S : NewSet).
Lemma test :
forall (x y : S.E'.t) (s : S.t),
S.mem x s = S.mem y s -> S.E'.foo x y = true.
Proof.
Admitted.
End Lemmas.
```
In the following code, lemma test cannot be defined.
The error message is: The term “x” has type “O.t” while it is expected to have type “S.elt”.
```
Module Lemmas (O : NewOT) (S : NewSet with Module E' := O).
Lemma test :
forall (x y : O.t) (s : S.t),
S.mem x s = S.mem y s -> O.foo x y = true.
Proof.
Admitted.
End Lemmas.
```
In the following code, NewNatLemmas cannot be defined.
The error message is: Error: The field foo is missing in Top.NewNatSet.E.
```
Module Lemmas (O : NewOT) (S : NewSet with Module E' := O with Module E := O).
Lemma test :
forall (x y : O.t) (s : S.t),
S.mem x s = S.mem y s -> O.foo x y = true.
Proof.
Admitted.
End Lemmas.
From Coq Require Import OrderedTypeEx.
Module NewNatOT <: NewOT.
Include Nat_as_OT.
Definition foo := Nat.eqb.
End NewNatOT.
Module NewNatSet := Make' NewNatOT.
Module NewNatLemmas := Lemmas NewNatOT NewNatSet.
```
My current solution is to re-define Backport\_Sets and use it instead of FSetList.Make.
But I wonder if there is more elegant way to solve the problem.
---
### Author:  [@herbelin](https://discourse.rocq-prover.org/u/herbelin)
#### Post date: [August 10, 2019, 6:22pm UTC](https://discourse.rocq-prover.org/t/use-a-submodule-of-orderedtype-in-fsets/383/4 "2019-08-10T18:22:53Z")
Hi, sharing `t` in the type of `E` in `NewSet` seems to be useful to make the three first example working:
```auto
From Coq Require Import OrderedType FSets.
Module Type NewOT <: OrderedType.OrderedType.
Include OrderedType.OrderedType.
Parameter foo : t -> t -> bool.
End NewOT.
Module Type NewSet <: FSetInterface.S.
Declare Module E' : NewOT.
Module E : OrderedType.OrderedType with Definition t := E'.t := E'.
Include Sfun E.
End NewSet.
Module Make (O : NewOT) := FSetList.Make O.
Module Make' (O : NewOT) <: NewSet with Module E' := O.
Module E' := O.
Include FSetList.Make O.
End Make'.
```
---
### Author:  [@mht208](https://discourse.rocq-prover.org/u/mht208)
#### Post date: [August 11, 2019, 3:54pm UTC](https://discourse.rocq-prover.org/t/use-a-submodule-of-orderedtype-in-fsets/383/5 "2019-08-11T15:54:57Z")
Wow! That really solves my problem nicely. Thank you so much.