The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Have you tried using Tactic Notation and ident, if I recall correctly?  There should be a way to interpret a symbol as a name rather than as a constr.

I think that the extra typeclass resolution is related to a bug I ran into in 8.4 a while back, where if you have an implicit argument which is an unresolable typeclass, and the argument doesn't appear in the type, and you [eapply] the lemma, then just about every subsequent tactic (reflexivity, destruct, etc, but not refine) will fail with a typeclass resolution error.

On Wed, Jul 27, 2016 at 6:52 AM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 07/26/2016 07:27 PM, Robbert Krebbers wrote:
> Something fishy seems to be going on. When writing:
>
>   class_apply @silly; [reflexivity|]
>
> with:
>
>   Lemma silly {A} `{C A} : 0 = 0 -> c = c -> True.
>
> Then reflexivity invokes TC inference on the shelved goal while its
> own goal 0 = 0 does not even involve the type class.

Even though class_apply is not documented, IMHO this is a bug. There
shouldn't be a way for reflexivity in the "0=0" subgoal to alter the
other subgoal.

Note that, if one replaces reflexivity by exact eq_refl, then typeclass
inference isn't induced in that other subgoal.  However, apply eq_refl
does induce the inference.   And class_apply @eq_refl doesn't.

-- Jonathan

>
> See below for an example.
>
> ============================
>
> Require Import Classes.Init.
>
> Class C A := c : A.
> Instance nat_C : C nat := 0.
> Instance bool_C : C bool := true.
> Lemma silly {A} `{C A} : 0 = 0 -> c = c -> True.
> Proof. auto. Qed.
>
> Goal True.
> class_apply @silly; [reflexivity|].
> (* BAD: @eq bool (@c bool bool_C) (@c bool bool_C) *)
> (* Why does reflexivity invoke TC inference? *)
> Restart.
> class_apply @silly. reflexivity.
> (* @eq ?A (@c ?A ?H) (@c ?A ?H) *)
> (* Now it no longer happens, why is class_apply @silly. reflexivity. *)
> (* any different from class_apply @silly; [reflexivity|]. *)
>
> On 07/27/2016 12:41 AM, Robbert Krebbers wrote:
>> Hi,
>>
>> is there a variant of apply that does not invoke type class inference on
>> the arguments of the applied lemma, but instead turns type class
>> constraints into shelved subgoals so that these can be solved later.
>>
>> The (undocumented) tactic "class_apply" seems to be doing somewhat what
>> I like, but not entirely: it only turns type class constraints into
>> shelved subgoals when the applied lemma is prefixed with an @. This is
>> insufficient when used as part of the implementation of some Ltac tactic
>> because I do not want the users of my tactic having to prefix their
>> lemmas with an @.
>>
>> I have included an example below.
>>
>> Robbert
>>
>> =========
>>
>> Require Import Classes.Init.
>>
>> Class C A := c : A.
>> Instance nat_C : C nat := 0.
>> Instance bool_C : C bool := true.
>> Lemma silly {A} `{C A} : c = c -> True.
>> Proof. auto. Qed.
>>
>> Goal True.
>> apply silly. (* BAD: @eq bool (@c bool bool_C) (@c bool bool_C) *)
>> (* I only want TC inference to be invoked later,
>>     for example when doing: *)
>> Fail apply (@eq_refl nat).
>> Restart.
>> eapply silly. (* BAD: @eq bool (@c bool bool_C) (@c bool bool_C) *)
>> Restart.
>> eapply @silly. (* BAD: @eq bool (@c bool bool_C) (@c bool bool_C) *)
>> Restart.
>> class_apply silly. (* BAD: @eq bool (@c bool bool_C) (@c bool bool_C) *)
>> Restart.
>> class_apply @silly. (* GOOD: @eq ?A (@c ?A ?H) (@c ?A ?H) *)
>> apply (@eq_refl nat). (* works *)
>>
>> (* But can we also do it without the @ ? *)
>>
>>