The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

You have to inline the mytype hint into the sigT hint, like so:

Hint Extern 5 {b: myType & Bar b} =>
  simple refine (existT Bar (_:myType) _); [simple refine (fooTobar _ 
_).1 |].

Yes, it's ugly.  I think the problem is that typeclasses eauto, as well 
as auto and eauto, all to varying degrees don't fully backtrack - even 
in 8.5.  Interestingly, the best of the bunch is auto.

Hopefully, someone will make the auto tactics all fully backtrack at 
some point.  In the mean time, I have given up on the auto tactics - and 
instead write my own backtracking routines using 8.5's "+" operator, the 
new multimatch tactical, and some other tricks.

-- Jonathan

On 03/07/2016 03:31 PM, nicolas tabareau wrote:
> Dear All,
>
> It seems that when typeclasses eauto manages
> to finish a subgoal with exact, it does not backtrack
> on it when the other subgoals fail (below a not too
> long example that exhibits the issue).
>
> Do I understand the problem correctly ?
>
> Can it be solved without the seely alias trick
> I use ?
>
> Best,
>
> -- Nicolas
>
> Notation "x .1" := (projT1 x) (at level 3).
>
> Parameter myType: Type.
>
> Class Foo (a:myType) := {}.
>
> Class Bar (a:myType) := {}.
>
> Parameter fooTobar : forall a (H : Foo a), {b: myType & Bar b}.
>
> Hint Extern 5 (Bar ?D.1) =>
>      destruct D; simpl : typeclass_instances.
>
> Hint Extern 1 myType => simple refine (fooTobar _ _).1.
>
> Hint Extern 5 {b: myType & Bar b} =>
>    simple refine (existT Bar (_:myType) _).
>
> Definition trivial a (H : Foo a) : {b : myType & Bar b}.
> Proof.
>    (* does not try to do simple refine (fooTobar _ _).1. *)
>    Fail typeclasses eauto with core typeclass_instances.
> Abort.
>
> (* just using an alias, to prevent exact to succeed *)
>
> Definition myType2:= myType.
>
> Hint Extern 1 myType2 => simple refine (fooTobar _ _).1.
>
> Hint Extern 5 {b: myType2 & Bar b} =>
>    simple refine (existT Bar (_:myType2) _).
>
> Definition trivial a (H : Foo a) : {b : myType2 & Bar b}.
> Proof.
>    typeclasses eauto with core typeclass_instances.
> Defined.