The Coq mailing list

[Robbert Krebbers <mail AT robbertkrebbers.nl>]

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 @ ? *)