The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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