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: Eddy Westbrook <westbrook AT galois.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Using hint databases to partially solve a goal?
  • Date: Mon, 11 May 2020 14:39:35 -0700
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=westbrook AT galois.com; spf=PermError smtp.mailfrom=westbrook AT galois.com; spf=None smtp.helo=postmaster AT mail-pj1-f41.google.com
  • Ironport-phdr: 9a23:j+CpEhElWWsIbKHM+0Kh4J1GYnF86YWxBRYc798ds5kLTJ7zpcWwAkXT6L1XgUPTWs2DsrQY0reQ4virADFdqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5yIRmsqQjdqsYajZZiJ6sx1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrhK9qBJwzIHafY+bNPRgcKzfft0UQnFMXtpIVyxEHo+8b5cDAugHMO1Fr4f9vVwOrR6mCAejGezg1z9JjWL20qIkyOQhDRrJ3BYnH9IJs3TfsdL4NakMXuCu0KnH1i/Db/RR2Tf+84XIfQouofWLXbJxasrd01UgFwTAjliJr4HuIjya2PgXvWeB8+pgSfygi3QhqwxpvzWix8Qhh4vKi4wbxV3J8SV3zYk6KNGkR0N3f8KpHZVOuiyEOYV4Tc0vTmVntisky7AIuYO3cSwIxZkp2RLSd/qKeJWL7BL7TOudPyt0iXZ/dL+8hxu+61asxvD9W8Wu31tGszJJn9vCu3wXyRDe6tKLRuZ980qlwzqC0w7e5+dZKk4uj6XbMYQuwrsom5oTr0vDGij2lV3zjKCMd0Uk/vGk6/zlYrn7v5OcOYB5hhzkPqQhncy/Bus4MgwQUGSB5eu807jj8VX4QLVMkPI2jrHUvI7GKckfvKK0AA9Y3pw95xqiDjqqytsVkWQfIFJAYh2HjozpO1/UIPD/CPeym1qtnylwx/DaJbLhGJLNLn/AkLr6crZy8UpcyA0yzdBE/Z5bFrYBIPfrVk/rqNPYFgM5MxCzw+v/FNp90ZoeVXuTDa+dLaPdqkSF5vkvIumJfI8aoizxK/kj5/70jH82g0URfaez3chfVHftFfN/Zk6dfHDEg9EbEG5MsBBtYvbtjQivXTJCL0m/RL42/DY8C8ryEorYWoq3h7uC9CiyGppXfSZNDVXaQiSgTJmNR/pZMHHaGcRmiDFRDeHwGb9k7gmnsUrB85QiK+PV/iMCspe6jop67unUlAp0/jtxXZrEjzO9Clpsl2ZNfAcYmbhlqBUnmFiK1a95mLpTEtkBv6oUADd/DobVyqlBM/63Wg/FeY3UGlOvQ9HjGTNoC9xtmpkBZEFyH9jkhRfGjXKn
Hi all,

I somehow have not been getting any of your responses, but luckily I can see
them on the archives… Not sure what to do about that. Maybe include me in the
CC list? Again, not sure.

The shelving and unshelving solution makes sense to me, especially as I think
my rules are pretty deterministic, and so I shouldn’t need to backtrack.
Thanks to Jason for the suggestion and Théo for the write-up about this
approach.

Jonathan, your suggestion about using autorewrite makes sense, and it
actually would be nice to use rewriting anyway. However, I always find that
autorewrite is very slow. Do you have any suggestions for making it faster? I
only really need to apply rewrites at the top level, so maybe I could get it
to not traverse the term by using rewrite_strat?

Thanks,
-Eddy

> On May 8, 2020, at 5:05 PM, 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