The Standard Library should not be adding transitivity and symmetry hints to core

[JasonGross]

Description of the problem

https://github.com/coq/coq/blob/cb296e38848656025f68527e017e22d1e781f716/theories/Structures/Equalities.v#L57-L60

This means that any time I extend a module with this type via <+, core gets permanently polluted with this endlessly looping instances. For example:

Require Import Coq.Structures.Equalities.

Module Foo (E : EqualityTypeOrig).
  Module E' := E (* possibly to add extra things to E with <+ *).
End Foo.

Module Bar <: EqualityTypeOrig.
  Definition t := nat.
  Definition eq := @eq nat.
  Definition eq_refl := @eq_refl nat.
  Definition eq_sym := @eq_sym nat.
  Definition eq_trans := @eq_trans nat.
End Bar.

Module F := Foo Bar.
Print HintDb core.
(* For F.E'.eq ->   simple apply F.E'.eq_refl(level 0, pattern
                 F.E'.eq ?META535 ?META535, id 0)
                 simple apply F.E'.eq_sym ; trivial(level 1, pattern
                 F.E'.eq ?META530 ?META529, id 0)
                 simple eapply F.E'.eq_trans(level 3, pattern
                 F.E'.eq ?META536 ?META538, id 0)
*)

These should not be in core, and any code that relies on them being in core can be fixed in a backwards compatible way by locally adding the hints to core.

Coq Version

8.15

[Alizter]

This is very tricky to do unfortunately. Even manually adding the hints to core is not so straightforward. The FSets library requires a lot of work since it relies mostly on these hints being in core. As there are several sets of such instances around it will take some work to find out which ones are needed.

[JasonGross]

It should not be so hard. Simply create a new db structures or fsets or something, add these hints to that db, and replace every invocation of intuition, firstorder, auto, and eauto with the corresponding invocation that uses both core and strucutres. Or make the hints #[export] rather than #[global], stick them in a Module Export Hints inside IsEqOrig, and then import all of the Hints modules before any proof that breaks.

[Alizter]

I'll try your second suggestion later.