The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

On Sat, 9 May 2020 16:44:23 +0200
Théo Zimmermann 
<theo.zimmi AT gmail.com>
 wrote:

> Hi Jonathan,
> 
> This is actually a FAQ. In a previous Coq-Club thread I referenced the
> abstract I wrote in 2016 explaining this technique (which wasn't novel
> at this time since I was attributing it to an e-mail of Michael
> Soegtrop in a previous Coq-Club thread):
> https://hal.archives-ouvertes.fr/hal-01671994/document
> 
> Théo


Interesting!  This would have been in 2016 or earlier.  Maybe it was
Michael Soegtrop who gave me that advice and not Jason.

> 
> Le sam. 9 mai 2020 à 07:03, 
> jonikelee AT gmail.com
>  
> <jonikelee AT gmail.com>
> a écrit :
> >
> > On Fri, 8 May 2020 21:33:32 -0400
> > Jason Gross 
> > <jasongross9 AT gmail.com>
> >  wrote:
> >  
> > > I believe you can add `shelve` as a hint, and this will allow the
> > > search to succeed with a partial solution.  You can then use
> > > `unshelve eauto` to get back the left-over goals  
> >
> > That sounds familiar, Jason.  Didn't you once advise me to try
> > this?  I recall trying something like "Hint Extern 999 _ => shelve
> > : db".  I don't recall it working out that well, though.
> >
> > Eddy, can you make the rules into rewrites, and use autorewrite
> > with db instead?
> >  
> > >
> > > On Fri, May 8, 2020, 20:06 Eddy Westbrook 
> > > <westbrook AT galois.com>
> > > wrote:
> > >  
> > > > Hey coq-club list-ers,
> > > >
> > > > Is there any way to partially solve a goal using the auto hint
> > > > databases? That is, is there a way to do something like "eauto
> > > > with <my_db>” but for it to make as much progress as it can and
> > > > then leave the remaining sub-goals for me to prove manually?
> > > >
> > > > The use case here is that I have monadic programs I’m trying to
> > > > prove properties of, and I have a set of rules to prove those
> > > > properties modulo properties of the values produced in those
> > > > computations. So, for instance, I have a monadic program that
> > > > manipulates bitvectors, and my rules can reduce (in a rote and
> > > > automatable way) all the properties about my monadic program to
> > > > properties about bitvectors that I have to prove by hand. The
> > > > hope is that I could use the hint databases to define how to
> > > > apply my rules, and then I could apply these hints and end up
> > > > with my goals about bitvectors to prove by hand. The only other
> > > > option is to write a monolithic tactic that pattern-matches on
> > > > the form of the goal to apply my rules, and that isn’t as nice
> > > > and extensible.
> > > >
> > > > Any ideas?
> > > >
> > > > Thanks,
> > > > -Eddy  
> >