# Modules vs. generalized rewrite

Hello!

I have the following file:

``````Require Coq.FSets.FMaps.
Require Coq.FSets.FMapAVL.

Require Coq.Strings.String.
Require Coq.Structures.OrderedTypeEx.

Module Maps : FMapInterface.S with Definition E.t := String.string :=
FMapAVL.Make OrderedTypeEx.String_as_OT.

(* Maps.E.t = String.string *)
Print Maps.E.t.
(* eq = Logic.eq *)
Print OrderedTypeEx.String_as_OT.eq.
(* eq = ??? *)
Print Maps.E.eq.

Lemma k : forall m n, Maps.E.eq m n -> m = n.
Proof.
intros m n Heq.
(* setoid rewrite failed *)
rewrite Heq.
``````

I’m trying to work backwards to determine why exactly the rewrite fails with a pretty obnoxious looking rewrite failure:

``````Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints:
UNDEFINED EVARS:
?X9==[m n Heq |- Relation_Definitions.relation Maps.E.t] (internal placeholder) {?r}
?X10==[m n Heq (do_subrelation:=Morphisms.do_subrelation)
|- Morphisms.Proper (Morphisms.respectful Maps.E.eq (Morphisms.respectful ?r (Basics.flip Basics.impl)))
eq] (internal placeholder) {?p}
?X11==[m n Heq |- Morphisms.ProperProxy ?r n] (internal placeholder) {?p0}
TYPECLASSES:?X9 ?X10 ?X11
SHELF:||
FUTURE GOALS STACK:?X11 ?X10 ?X9||?X3 ?X2 ?X1
.
``````

Firstly:

``````Module Maps : FMapInterface.S with Definition E.t := String.string :=
``````

I’m using `: FMapInterface.S` because I want the internals of `Maps` to be abstracted away as much as possible; I don’t want proofs over `Maps.t` to descend into the guts of the AVL tree; I want to work solely from the exposed `Maps` and `FMapFacts` theorems. However, I think this causes an issue because:

``````(* Maps.E.t = String.string *)
Print Maps.E.t.
(* eq = Logic.eq *)
Print OrderedTypeEx.String_as_OT.eq.
(* eq = ??? *)
Print Maps.E.eq.
``````

… Although `Maps.E.t` is exposed as `string` thanks to the `with` clause, and `OrderedTypeEx.String_as_OT.eq` is visible as Leibniz equality, the `Maps.E.eq` definition appears to Coq to be an arbitrary `t -> t -> Prop` function. The failed proof of `k` would seem to confirm this. If I instead use:

``````Module Maps <: FMapInterface.S with Definition E.t := String.string :=
``````

The rewrite works as the concrete definition of `eq` is exposed, but then proofs involving `Maps.t` are exposed to the fact that it’s an AVL tree because the concrete details of everything else in the module are exposed too.

I feel like this is a case of needing generalized rewriting, which I (unfortunately) don’t know how to use yet and I’m still struggling through the documentation for it.

Is there a pleasant way to get `Maps.E.eq` to work in rewrites without using `<:`?

Er, to be clear, I’m not asking to be able to prove `Maps.E.eq m n -> m = n` in all cases; I just used that as an example of something that fails. In other words, I think this question is about being able to make `m` and `n` interchangeable in some sense (presumably with generalized rewriting) rather than about forcing `Maps.E.eq` to be Leibniz equality.

Adding a relation outside of the module helps (but isn’t really the solution, I don’t think - I have Leibniz equality, I just can’t seem to expose it):

``````Require Coq.FSets.FMaps.
Require Coq.FSets.FMapAVL.

Require Coq.Strings.String.
Require Coq.Structures.OrderedTypeEx.

Module Maps : FMapInterface.S with Definition E.t := String.string :=
FMapAVL.Make OrderedTypeEx.String_as_OT.

(* Maps.E.t = String.string *)
Print Maps.E.t.
(* eq = Logic.eq *)
Print OrderedTypeEx.String_as_OT.eq.
(* eq = ??? *)
Print Maps.E.eq.

reflexivity  proved by (Maps.E.eq_refl)
symmetry     proved by (Maps.E.eq_sym)
transitivity proved by (Maps.E.eq_trans)
as MapsEqRelation.

Lemma k : forall m n p, Maps.E.eq m n -> Maps.E.eq n p -> Maps.E.eq m p.
Proof.
intros m n p Heq0 Heq1.
rewrite Heq0.
exact Heq1.
Qed.
``````

My mistake was that I didn’t realize multiple `with` clauses were valid:

``````Require Coq.FSets.FMaps.
Require Coq.FSets.FMapAVL.

Require Coq.Strings.String.
Require Coq.Structures.OrderedTypeEx.

Module Ord : OrderedTypeEx.UsualOrderedType
with Definition t  := String.string
with Definition eq := @Logic.eq String.string.
Include OrderedTypeEx.String_as_OT.
End Ord.

Module Maps : FMapInterface.S
with Definition E.t := String.string
with Definition E.eq := Ord.eq
:= FMapAVL.Make Ord.

(* Maps.E.t = String.string *)
Print Maps.E.t.
(* eq = Logic.eq *)
Print OrderedTypeEx.String_as_OT.eq.
(* eq = Ord.eq = Logic.eq *)
Print Maps.E.eq.
(* eq = Logic.eq *)
Print Ord.eq.
``````

Only with Leibniz equality you can change m with n “under” Leibniz equality, as Leibniz equality is the coarsest relation you can define in Coq.