The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

> 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  
>