The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

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

Turns out the library already has an Ltac isZcst:

https://github.com/coq/coq/blob/629fbc743f8b5e7623a6834f19885b2e379cb782/plugins/setoid_ring/InitialRing.v#L883


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

For ring preprocessing, I didn't have any large terms so far, but I did for
expressions involving Z.testbit. There, switching from "repeat rewrite" to
rewrite_strat yielded a ~10x speedup:
https://github.com/mit-plv/riscv-coq/commit/4d83bc164c