The Coq mailing list

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

On 7/16/20 12:16 PM, Matthieu Sozeau wrote:

> 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

`Typeclasses Opaque equiv` does not change the behavior.

You are however absolutely right, raising the level of debug to 2 shows something that makes more sense: there is a file "MathClasses.misc.workarounds.v" that actually contains the real culprit this time I think:

Instance equivalence_proper `{Equivalence A R} : Proper (R ==> R ==> iff) R | 0 := _.

So that any search for a Proper instance gets hijacked into an Equivalence one!

I gave a naive shot at

Existing Instance equivalence_proper | 50.

and:

Remove Hints equivalence_proper : typeclasses_instances.

to try to stop it from triggering first, but to no success in both cases.
Would you have a suggestion to kill such an instance?

Thanks,
Yannick

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