The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

Dear Yannick,

> Le 15 juil. 2020 à 16:32, Yannick Zakowski <zakowski AT seas.upenn.edu> a 
> écrit :
> 
> 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.

I don’t see a way to avoid the import of instances from math-classes if you 
have to Require Import. 
However, the shape of the hint here might leave some hope for finding a 
workaround, because generalized
rewriting itself does not generate `(_ = _)` subgoals to be solved by type 
class resolution, only
`Proper R f`, `ProperProxy R f` and `subrelation R R’` goals. So you might 
have more luck disabling
the hint that produces the `(_ = _)` subgoal?

Best,
— Matthieu