The Coq mailing list

[Eddy Westbrook <westbrook AT galois.com>]

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