The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Hi,

I'm a beginner with respect to typeclasses and I'm experimenting to see
whether my Coq developments would benefit from using them. And in some
simple cases, they don't seem to help at all. See below for a simplified
example.

Lemma l has an implicit hypothesis that I expect the typeclass mechanism
to fill automatically. The hypothesis is explicitly filled by "auto with
typeclass_instances", so I suppose my instances are correctly defined.
In fact, the refine tactic fills the extra hypothesis implicitly, so it
seems like everything works just fine. But the apply tactic just leaves
me with a goal to prove.

Am I'm expecting too much from typeclasses? Did I miss some vernacular
command that would force apply to fill the blanks? Or is it simply a bug
in apply? I am using Coq 8.3pl1.

Best regards,

Guillaume


Section A.
Variable f : nat -> nat.
Class P := p : forall x, f x = 0.
Context {p' : P}.
Lemma l : forall x, f x = f x.
intros x.
now rewrite p.
Qed.
End A.

Section B.
Axiom g : nat -> nat.
Global Instance Pg : P g.
Admitted.
End B.

Section C.
Goal forall x, g x = g x.
apply l.
(*
Why do I have to prove "P g" here?
Note that "refine (l g)" properly discharges
the extra goal, contrarily to "apply l".
*)