Use a submodule of OrderedType in FSets

Using Coq
1

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?

2

The following seems to work:

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.

3

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.

4

Hi, sharing t in the type of E in NewSet seems to be useful to make the three first example working:

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'.
5

Wow! That really solves my problem nicely. Thank you so much.