The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi Yannick,

Sorry, it didn't go further than what is written there, and I don't
think I really put together a prototype demonstrating these ideas.

Best,
Théo

Le lun. 11 mai 2020 à 03:13, Yannick Zakowski
<zakowski AT seas.upenn.edu>
 a écrit :
>
> Hi Théo,
>
> The paper you linked describes a work in progress. Did it end up being
> fleshed out in some form or another? Or alternatively, is the prototype
> implementation of `apply` that it refers to available somewhere to toy
> around with the technique?
>
> Best,
> Yannick
>
> On 5/9/20 10:44 AM, Théo Zimmermann 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
> >
> > 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