The Coq mailing list

[Eddy Westbrook <westbrook AT galois.com>]

Nope, spoke too soon. typeclasses eauto says in the documentation that it is 
supposed to allow unsolved goals to remain, but I did in fact need the "Hint 
Extern 999 _ => shelve : db” trick from an earlier response.

With this trick, though, it does seem to be working.

Thanks,
-Eddy

> On May 13, 2020, at 12:26 PM, Eddy Westbrook 
> <westbrook AT galois.com>
>  wrote:
> 
> Thanks for your help, everyone.
> 
> I ended up figuring out another way to do this that seems to work for me: 
> typeclasses eauto, which allows unsolved goals to remain in the proof state.
> 
> -Eddy
> 
>> On May 11, 2020, at 4:15 PM, 
>> jonikelee AT gmail.com
>>  wrote:
>> 
>> 
>>> 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
>> 
>> Maybe.  I have a similar case where the rewrites only need to be
>> applied at top level, and I have not tried rewrite_strat to see if it
>> gives a performance improvement because it was already pretty fast.
>> 
>> Also, with Ltac2, it may be easy to use mutable structures to build a
>> tactic to apply an incrementally constructed collection of rules.
>> 
>>> 
>>>> 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  
>>> 
>> 
>