The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Samuel,

I am happy that I could help :-)

Two more notes:

1.) There is an (undocumented) tactic called "is_constructor". This might 
simplify your checks. There is also a tactic to check for ground terms in the 
pipeline. Search for "is_" in 
https://github.com/coq/coq/blob/master/plugins/ltac/extratactics.ml4 for 
other undocumented term classification tactics (I have it on my to do list to 
write the documentation).

2.) In case you are working on large terms, it might be worthwhile to do a 
performance comparison of autorewrite vs. repeat rewrite vs. rewrite_strat 
vs. match context + rewrite. A usage of rewrite_strat for your case would 
look as below, but there are quite a few options one can try:

        [rewrite_strat (bottomup terms ZToReg_morphism.(morph_add) 
ZToReg_morphism.(morph_sub) ZToReg_morphism.(morph_mul))]

In case you look into this, I would be interested in the results. I did test 
this in the past, but I had only rater modest term sizes where it did not 
make much of a difference and didn't bother to create large artificial terms. 
For large term sizes, timing might be substantially different.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928