The Coq mailing list

[Robbert Krebbers <mail AT robbertkrebbers.nl>]

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.

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