coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Declare Implicit Tactic bit-rot

From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Declare Implicit Tactic bit-rot
Date: Mon, 4 Jul 2016 09:22:18 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=arnaud.spiwack AT gmail.com; spf=Pass smtp.mailfrom=arnaud.spiwack AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f50.google.com
Ironport-phdr: 9a23:X5CnnxxhgcrqKbLXCy+O+j09IxM/srCxBDY+r6Qd0e0QIJqq85mqBkHD//Il1AaPBtSDragdwLCJ7+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL2PbrnD61zMOABK3bVMzfbWtXNSLxJ7oi6ibwN76W01wnj2zYLd/fl2djD76kY0ou7ZkMbs70RDTo3FFKKx8zGJsIk+PzV6nvp/jtLYqySlbuuog+shcSu26Ov1gFf0LRAghZksy/YXAsQTJBV+E4WJZWWELmDJJBRLE5Vf0RMGinDH9s79Uwi+TIMG+dqg1Rj2p7O8/QQTwiTgOPD0R9GDHzNR3iLNHrRmhoR1m3oOSbpvDZ6k2Rb/UYd5PHTkJZc1WTSEUR9rkN4Y=

To be honest, I doubt it ever worked well. And I'm guessing no one has actually used it. I'd be interested in the history of this feature though.

On 1 July 2016 at 06:04, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 06/30/2016 11:38 PM, Jason Gross wrote:

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...

I just wonder if someone will ever fix it ;-) It looks like it has been broken for a long time - some googling suggests maybe since 8.2? It was put in in 8.1, according to CHANGES.

It would also be nice if/when it works if it didn't require complete solution or shelving - that way it could just transform implicit goals, or decide to do nothing, and leave the goal go wherever it would otherwise normally go - on the shelf, as a focused subgoal, etc. Also, that way "Declare Implicit Tactic idtac" would return behavior to the default.

-- Jonathan

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