The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I asked about something like this recently on coqdev (subject was: 
simple refine vs. typeclass hole filling vs. goal number 
predictability), but did not get any replies.  But, I didn't know about 
class_apply (is there a class_refine, too?).

Since class_apply exists, then in your case it may just be that what is 
needed is a tactical way to "@"-ify a symbol.  Right now, "@silly" and 
"silly" act as two distinct symbols with two distinct types - and 
"silly" gets typeclass inference run on it as a symbol (hence why 
class_apply can't prevent that).  One could write a tactic that takes 
something like "silly" and completely generalizes it before applying it 
- but it may generalize it more than was intended.

-- Jonathan


On 07/26/2016 06:41 PM, 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 @ ? *)