The Coq mailing list

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

Thanks Matthieu. 

Surprisingly, it does not seems to scale to more 

complex example.

Set Typeclasses Dependency Order.

Notation "x .1" := (projT1 x) (at level 3).

Parameter myType: Type. 

Class Foo (a:myType) := {}.

Class Bar (a:myType) := {}.

Class Qux (a:myType) := {}.

Parameter fooTobar : forall a (H : Foo a), {b: myType & Bar b}.

Parameter barToqux : forall a (H : Bar a), {b: myType & Qux b}.

Hint Extern 5 (Bar ?D.1) =>

    destruct D; simpl : typeclass_instances.

Hint Extern 5 (Qux ?D.1) =>

    destruct D; simpl : typeclass_instances.

Hint Extern 1 myType => simple refine (fooTobar _ _).1.

Hint Extern 1 myType => simple refine (barToqux _ _).1.

Typeclasses eauto := debug.

Definition trivial a (H : Foo a) : {b : myType & Qux b}. 

Proof.

  Fail typeclasses eauto with core typeclass_instances.

Abort.

On Mon, Mar 7, 2016 at 10:37 PM, Matthieu Sozeau <mattam AT mattam.org> wrote:

Hi,

   Set Typeclasses Dependency Order. is what you need here,

it will correctly backtrack on exact a, and actually try to solve the

?g1 : myType goal before the ?g2 : Bar ?g1 goal. The reason it is 

an option is that many libraries rely on the old behavior, which can

be a huge performance gain depending on the situation.

  Beware that your Hint Extern's actually do some resolution before

producing goals on which typeclasses eauto can backtrack, e.g. in

the successful trace:

Debug: 1: eapply existT on {b : myType & Bar b}

Debug: 1.1.1: exact a on myType

Debug: 1.2: no match for (Bar a) , 1 possibilities

Debug: Backtracking after exact a

Debug: 1.1: exact H on (Foo ?m)

Debug: 1.1.2: (*external*) simple refine (fooTobar _ _) .1 on myType

Debug: 1.2.1: (*external*) destruct D; simpl on (Bar (fooTobar a H) .1)

Debug: 1.2.1.1.1: exact b on (Bar x)

The Debug: 1.1 line is an internal call to resolution due to the 1.1.2 

extern call, the rest will not backtrack on this choice. Moving 

typeclasses eauto (along with auto ...) to the new engine is part of

my current plans. This should bring Hint Externs with multiple

successes as well.

Best,

-- Matthieu

On Mon, Mar 7, 2016 at 10:12 PM nicolas tabareau <nicolas.tabareau AT inria.fr> 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 ? 

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

--

Nicolas Tabareau
Researcher at Inria
Ascola Group, Nantes