The Coq mailing list

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

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

Maybe then declaring `Typeclasses Opaque equiv` will avoid this unexpected 
unification. Also, it looks like this application 
(`simple apply @sm_proper`) is coming from a regular hint rather than the 
extern hint you mentioned (they are marked with
*external* in the traces).
— Matthieu

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