coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Apply without TC inference
- Date: Wed, 27 Jul 2016 09:51:38 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f174.google.com
- Ironport-phdr: 9a23:3wJzyRbZjs3XDjQmTybqCUv/LSx+4OfEezUN459isYplN5qZpc+5bnLW6fgltlLVR4KTs6sC0LuO9f69EjJeqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ3pzxib35pcObSj4LrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyZb1eFjUvdW4vt+PxshyWbwyJ72ccW2NethdJHQXD8FmuXJD3syj3sudw8CafNMzyC7szXGLxvO9QVBb0hXJfZHYC+2bNh5kogQ==
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 @ ? *)
- [Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jason Gross, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jason Gross, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jason Gross, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jason Gross, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Matthieu Sozeau, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Matthieu Sozeau, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
Archive powered by MHonArc 2.6.18.