Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Using hint databases to partially solve a goal?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Using hint databases to partially solve a goal?


Chronological Thread 
  • From: Théo Zimmermann <theo.zimmi AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Cc: Jason Gross <jasongross9 AT gmail.com>
  • Subject: Re: [Coq-Club] Using hint databases to partially solve a goal?
  • Date: Sat, 9 May 2020 16:44:23 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-lj1-f172.google.com
  • Ironport-phdr: 9a23:rKTrjhE7UsbRW0Jg0pb+XJ1GYnF86YWxBRYc798ds5kLTJ7ypsuwAkXT6L1XgUPTWs2DsrQY0reQ4/2rBjxIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLN/IA+1oAjRucUbg4hvIbstxxXUpXdFZ/5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnMVhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1kyoMKSI3/3/LhcxxlKJboQyupxpjw47PfYqZMONycr7Bcd8GQGZMWNtaWS5cDYOmd4YAAOQBMuRYoYfzpFUAsAWwChWjCu701j9In2X70bEm3+g9EwzL2hErEdIUsHTTqdX4LLkcUeCvy6nP1TrMbPJW2TL46IfWaBAhpOuDXbR2ccHMzkQvCwPFgUuXqYD/PjKV1+ENs22a7+d7WuKvjnQoqwB1ojS12sgsjYzJi5sTx1vZ+ip33Jw7KsekSE5nf9GkCp1QujmUOoZ1Xs8vXmBltSI6x7MGpJK1cykHxZUnyhLCZPGKbouF7xH9WeueLjl0mWxodbKxihi98Uauyu3xW8qq3VhEqCdOj9fCtncI1xPJ68iHTONw8V272TmT1wDT6/9ELl4vlabCLJ4h36AwmYQJsUTfACD2g1/6jKGMdkgi5+Om6Pznb634qpOAM4J4kALzP6Q0lsChHeg1MRICU3WZ9Oii0rDo4Ff3T69QjvIsl6nUqJDaKtofpq6+GwJV15ws6xe7Dzu/1NQYn2QLIEtLeB6ajYXlJUvCIP//Dfe4jFSslClky+raMb3mB5XBNnnDkLH/crZh80NQ1hY/wNRF659XCrwNOuz/VlPyudDCExM0MRK4z/7iCNpn14MeXWyPArWeMKPXqVKI+uIvLPeLZIMPuTf9Kv0l5/vvjXIill8deLOm3ZoTaHyiAvtmJECZbWL2gtgdCWcKohY+TOvyhVKeVj5Tfm++UL445jEmE42rFpzDR4CogLyZxii3BJxWZmZcClCNC3jkbYuEW+1fIB6Vd+Rmi3QvUaWrA9sq0gjrvwvnwZJmKPDV82sWr8Sw+sJy4rjvlZA1wg51CsGQyWSESWc8yn8ISjhwzqF6pE1VxVKK0Kw+iPtdQ48Ar8hVWxs3YMaPh9dxDMr/D0eYJo/QFQSWB+6+CDR0deofht8DZ0EnRYenhxHHmi6oWvobzuPRQpMz9a3Y0j76IMMvky+XhplktEEvR450DUPjg6d+8wbJAIuQyheWkq+rceIX2yufrT7fn1rLh1lRVUtLaYuARWoWPxKEotHw50eERLirW+wq

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
>



Archive powered by MHonArc 2.6.18.

Top of Page