The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

On Mon, Feb 14, 2011 at 9:20 PM, Tom Prince 
<tom.prince AT ualberta.net>
 wrote:
> I don't know whether this behaviour is expected, but the typeclass
> mechanism still has kinks and oddities in it. It would probably help if
> you gave a small self contained example of this behavior (and the
> behviour of auto) occurring.

I've given an example below of the behaviors I was describing
regarding apply, auto, and type classes.  As I said, I'm not sure if
they are "bugs," but I want to wrap my head around what is going on so
that I can use the proper work-arounds.

 - Aaron

<coq>

Require Import SetoidClass.

Parameter A B C: Type.
Parameter P: A -> A -> Prop.
Parameter F: A -> A.

Class K (X: Type) {S: Setoid X} := {
  Q: A -> X -> X -> Prop;

  Q_F:
    forall a x1 x2,
    Q a x1 x2 ->
    Q (F a) x1 x2;

  Q_sym:
    forall a1 a2 x1 x2,
    P a1 a2 ->
    Q a1 x1 x2 ->
    Q a2 x2 x1
}.

Instance B_Setoid: Setoid B.

Instance B_K: K B.
Admitted.

Instance C_Setoid: Setoid C.

Instance C_K: K C.
Admitted.

Tactic Notation "foo" constr(e) constr(ea) :=
  apply e with (1 := ea).

Lemma example_foo:
  forall a1 a2 (x1 x2: C),
  P a1 a2 ->
  Q a1 x1 x2 ->
  Q a2 x2 x1.
Proof.
  intros * H1 H2.
  (* foo Q_sym H1.*) (* FAILS *)
  apply Q_sym with (1 := H1). (* SUCCEEDS *)
Admitted.

Create HintDb db1.
Create HintDb db2.
Create HintDb db3.
Hint Resolve Q_F: db1.
Hint Resolve @Q_F: db2.
Hint Extern 1 => apply Q_F: db3.

Lemma example_auto:
  forall a (x1 x2: C),
  Q a x1 x2 ->
  Q (F a) x1 x2.
Proof.
  intros * H.
  (* auto with db1. *) (* FAILS TO SOLVE GOAL *)
  (* auto with db2. *) (* SOLVES GOAL *)
  (* auto with db3. *) (* SOLVES GOAL *)
Admitted.

</coq>