The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 07/04/2016 03:22 AM, Arnaud Spiwack wrote:
> 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.

I did find another spot in the refman - where tactic-in-term is 
introduced - which says about tactic-in-term : "This mechanism is 
comparable to the Declare Implicit Tactic command defined at 8.9.7, 
except that the used tactic is local to each hole instead of being 
declared globally."

That would suggest that Declare Implicit Tactic was expected to share 
the same limitations as tactic-in-term.  One such limitation is that it 
must completely solve its goal (including all of its subgoals) - or 
fail.  It is not permitted to merely attempt a solution, and otherwise 
pass its goal or any surviving unproved subgoals on to wherever it/they 
would otherwise have gone.  Note that shelving a subgoal within a 
tactic-in-term merely causes it to fail, so perhaps the same is expected 
to apply to Declare Implicit Tactic.

If that is going to be the behavior of Declare Implicit Tactic if/when 
it is fixed, then that makes it useless for the case I'm trying to 
solve.  Maybe it makes it so prone to inducing failures that it won't 
get used at all - and perhaps this is its history?

There are those other techniques which I outlined in that other e-mail: 
typeclasses, canonical instances, Program/Obligation Tactic.  But, they 
each have their own limitations.

The question becomes: should there be a way to do automatic unlimited 
general-case attempts at hole filling?  And how would such a mechanism 
interact with all those others?

-- Jonathan

> 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