The Coq mailing list

[Yannick Zakowski <zakowski AT seas.upenn.edu>]

Dear all,

Consider the following self-contained example:

From Coq Require Import
     Setoid
     Morphisms
     RelationClasses.

Section Foo.

  Variable op: nat -> nat.

  Variable rel: nat -> nat -> Prop.

  Context {rel_op_Proper: (Proper (rel ==> rel) op)}.
  Context {rel_trans: Transitive rel}.

  Goal forall (a b: nat) (REL: rel a b),
      rel (op a) (op b).
  Proof.
    intros.
    Typeclasses eauto := debug.
    rewrite REL.
    (* Resolution in 6 steps *)
    Undo.
    Require Import MathClasses.interfaces.abstract_algebra.
    rewrite REL.
    (* Resolution in over 100 steps *)
  Abort.

End Foo.

I am looking for a way to avoid this side-effect of loading this MathClass module.
The problem touches to the overall issues of Hints being aggressively exported, and instances all sharing a single namespace. A general solution would naturally be welcome, but I would already be very happy with a hacky local solution allowing me to get back into my proof. In this specific case, it indeed looks to me like the main culprit that gets applied early and completely derail the proof search is the following External Hint declared in `abstract_algebra.v`:

Hint Extern 4 (?f _ = ?f _) => unshelve eapply (sm_proper (f:=f)).

I have given a shot at `Set Loose Hint Behavior "Strict".` without success. For good conscience I also tried `Remove Hints sm_proper: core_db.`, but as described in the documentation, it does not apply to External Hints.

Any idea as to how to solve this problem would help me a great deal.

For context, in my concrete use-case, I am proving a pass of compilation from an existing language (Helix) to another existing language (Vellvm) using a library (Interaction Trees).
The dependency on MathClass is transitively inherited from Helix, but is essentially irrelevant to the proof itself.
I rewrite non-trivial relations (via the Interaction Tree library) in fairly complex context, so that this overhead seems to become unbearable.
I am therefore ideally really looking for a local way to prevent this behavior, if possible without having to mess with any of the three libraries at play.

Thanks in advance,
Best,
Yannick

P.S. : This intersects with my question on Discourse¹. I am not sure what's the current etiquette on cross posting to try to reach as many users as possible. Let me know if it's any issue.

¹: https://coq.discourse.group/t/preventing-pollution-of-the-instance-context-during-import/942