The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

Hi,

I'm wanting to develop a Coq tactic that, given a database of rewrite rules, 
will perform a search of all possible ways the current goal can be rewritten. 
I'm wanting to experiment with the use of heuristics to guide the search.

Specifically, if I had the rewrite rules "a=b", "b=c" and the goal "a+a=b", 
the first stage in the search would be to use each rewrite only once on the 
goal in all possible ways to produce the new goals "b+a=b", "a+b=b" 
and "a+a=c". I would then repeat this for the new goals, using heuristics to 
guide which goals to explore.

I would rather use Ltac for this if I could, but it doesn't appear to give 
enough control in terms of using a database of rules, caching explored nodes 
etc. My only other option is to use OCaml but I'm having a lot of trouble 
getting going because I can't find any good documentation. 

I looked at modifying "auto" but this doesn't appear to use rewrite rules in 
the sense of Coq's "rewrite" tactic which I want. I had a look at 
the "autorewrite" tactic; this looks more like what I need but it doesn't 
appear to exhaustively apply rewrites and only explores one path. Are there 
other tactics that work more like my description?

What OCaml (or Coq) commands can I make use of to generate the next set of 
goals to search? Coq's "rewrite X" tactic seems to rewrite with X as many 
times as it can when I need to find all the ways X can be used only once. Is 
there a simple way to generate all these possibilities?

Also, I noticed an OCaml file involving discrimination nets, which auto 
appears to use. As I would like this tactic to be scalable, is there some way 
I can make use of this?

Any pointers would be greatly appreciated.

Regards,

Sean