The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Hi Guillaume,

There's a non-implicit argument (f) to your lemma before the maximal
implicit typeclass argument (P f).
If you make this argument implicit as well, everything works fine:

Implicit Arguments l [[f] [p']].

Not sure if that's intuitive behaviour or not, but as a rule of thumb,
if you expect (P f) to be determined automatically from context, then
f as well should be inferrable from context. Except in some cases (the
typeclass-based type of finite sets "set A" is one such
counterexample), I always make sure that in lemmas and functions which
expect implicit instances, these instance's parameters are also
implicit. Incidentally, I would have defined the class outside the
section and then introduce both the function f and its instance using
Context:

Class p (f : nat -> nat) :=  { ... }.

Section pLemmas.
  Context `{p' : P f}.

  ...
End pLemmas.

Cheers,

Stéphane

On Thu, Mar 10, 2011 at 6:30 PM, Guillaume Melquiond
<guillaume.melquiond AT inria.fr>
 wrote:
> 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".
> *)
>
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06