The Coq mailing list

[nicolas tabareau <nicolas.tabareau AT inria.fr>]

Thanks for the trick but that is indeed not what I was looking for. 

Have you a typical example of auto-like tactics on your github ? 

On Mon, Mar 7, 2016 at 10:00 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

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.

--

Nicolas Tabareau
Researcher at Inria
Ascola Group, Nantes