# Modules vs. generalized rewrite
**URL:** https://discourse.rocq-prover.org/t/modules-vs-generalized-rewrite/1762
**Category:** Using Rocq
**Created:** [August 18, 2022, 10:50am UTC](https://discourse.rocq-prover.org/t/modules-vs-generalized-rewrite/1762 "2022-08-18T10:50:19Z")
**Posts on this page:** 5
**Page:** 1
### Author:  [@io7m](https://discourse.rocq-prover.org/u/io7m)
#### Post date: [August 18, 2022, 10:50am UTC](https://discourse.rocq-prover.org/t/modules-vs-generalized-rewrite/1762/1 "2022-08-18T10:50:19Z")
Hello!
I have the following file:
```auto
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:
```auto
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:
```auto
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:
```auto
(* 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:
```auto
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 `<:`?
---
### Author:  [@io7m](https://discourse.rocq-prover.org/u/io7m)
#### Post date: [August 18, 2022, 10:57am UTC](https://discourse.rocq-prover.org/t/modules-vs-generalized-rewrite/1762/2 "2022-08-18T10:57:04Z")
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. 🙂
---
### Author:  [@io7m](https://discourse.rocq-prover.org/u/io7m)
#### Post date: [August 18, 2022, 12:08pm UTC](https://discourse.rocq-prover.org/t/modules-vs-generalized-rewrite/1762/3 "2022-08-18T12:08:42Z")
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):
```auto
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.
Add Relation (Maps.E.t) (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.
```
---
### Author:  [@io7m](https://discourse.rocq-prover.org/u/io7m)
#### Post date: [August 18, 2022, 1:40pm UTC](https://discourse.rocq-prover.org/t/modules-vs-generalized-rewrite/1762/4 "2022-08-18T13:40:50Z")
My mistake was that I didn’t realize multiple `with` clauses were valid:
```auto
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.
```
---
### Author:  [@mattam82](https://discourse.rocq-prover.org/u/mattam82)
#### Post date: [September 19, 2022, 8:23pm UTC](https://discourse.rocq-prover.org/t/modules-vs-generalized-rewrite/1762/5 "2022-09-19T20:23:36Z")
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.