Modules vs. generalized rewrite

Using Rocq
1

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 <:?

2

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. :slightly_smiling_face:

3

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.

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.
4

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

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.