The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/07/2016 04:11 PM, nicolas tabareau wrote:
> 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 ?

Unfortunately, none that involve typeclasses, and none that have the 
"auto-like" ability to make use of hint dbs.

One could write an auto-like tactic that uses hint dbs and fully 
backtracks by using "+" and multimatch, in combination with Gregory 
Malecha's coq-ltac-iter plugin 
(https://github.com/gmalecha/coq-ltac-iter) to iterate over a hint db.  
Unfortunately, I don't think his plugin handles Extern hints yet.

-- Jonathan

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