coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Declare Implicit Tactic bit-rot (was: question about Existing Class)

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Declare Implicit Tactic bit-rot (was: question about Existing Class)
Date: Fri, 01 Jul 2016 03:38:12 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f53.google.com
Ironport-phdr: 9a23:kYf83RGXg2ThxVCJxVkYyZ1GYnF86YWxBRYc798ds5kLTJ75pMywAkXT6L1XgUPTWs2DsrQf2rKQ6vCrBjFIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWD14Luh6vtptX6WEZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq4QTLpCDT1gPXpmytfssEzhRBCI4DMzSGINiVIcAQHe6xf1RJDqqXrSue902S3cNsrzG+NnEQ++5rtmHUe7wBwMMCQ0pTna

It wasn't previously in my toolbox, but now it's on my radar.

I wonder what happens if you use [abstract] in the implicit tactic... I wonder if you can make it loop by getting it to be called recursively from inside the implicit tactic... I wonder what happens if you're in universe polymorphic mode and you generate new universes that show up only in constraints and not in the proof term...

On Thu, Jun 30, 2016, 7:29 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 06/30/2016 04:00 PM, Jonathan Leivent wrote:
> ...
>
> Hint Extern 0 (eq _ _) => typeclasses eauto : tcinit_db.
>
> Declare Implicit Tactic (eauto with nocore tcinit_db; shelve).
>
> Yes, that could be a winner.
>
> Although now it looks like Declare Implicit Tactic has some bugs. The
> declared tactic doesn't get called in all the cases it claims: "It is
> used every time the term argument of a tactic has one of its holes not
> fully resolved.". For instance, "refine _" doesn't call it.
>
> And in one case, it is giving me: "Anomaly: Evar ?X96 was not
> declared. Please report."
>

On second thought - it seems easier to get Declare Implicit Tactic to
fail than to succeed. I guess nobody uses it.

-- Jonathan

Re: [Coq-Club] Declare Implicit Tactic bit-rot (was: question about Existing Class), Jonathan Leivent, 07/01/2016
- Re: [Coq-Club] Declare Implicit Tactic bit-rot (was: question about Existing Class), Jason Gross, 07/01/2016
  - Re: [Coq-Club] Declare Implicit Tactic bit-rot, Jonathan Leivent, 07/01/2016
    - Re: [Coq-Club] Declare Implicit Tactic bit-rot, Arnaud Spiwack, 07/04/2016
      - Re: [Coq-Club] Declare Implicit Tactic bit-rot, Jonathan Leivent, 07/04/2016