The Coq mailing list

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

Hello,

That's a sensible suggestion, unfortunately I do not quite understand why this hint gets applied. In the minimal example from my original message, the beginning of the debug trace goes as follows:

Debug: 1: looking for (Proper (rel ==> ?r) op) with backtracking
Debug: 1.1: exact rel_op_Proper on (Proper (rel ==> ?r) op), 0 subgoal(s)
Debug: 2: looking for (Proper (rel ==> ?r ==> flip impl) rel) with backtracking
Debug: 2.1: simple apply @sm_proper on (Proper (rel ==> ?r ==> flip impl) rel), 1 subgoal(s)
Debug: 2.1-1 : (Setoid_Morphism rel)

We are looking for a Proper instance as expected, nothing in this goal explicitly refers to equiv (i.e. "=" from MathClasses perspective), and yet `sm_proper` gets applied.

Yannick

On 7/16/20 6:23 AM, Matthieu Sozeau wrote:

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