The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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

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