The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Thu, Dec 13, 2012 at 11:12:27AM +0100, Thomas Braibant wrote:
> I did some quick instrumentation of the "strategies" code in the
> latter file, and one odd thing is that it seems that subterms that are
> partial applications are not considered as candidates for rewriting
> (e.g., f is a candidate, x is a candidate, f x x is a candidate, but f
> x is not). It makes sense from an efficiency point of view: trying all
> possible partial applications as candidates for rewriting ought to be
> expensive.

For the records, if the shape of the rewrite rule is (f _), ssreflect happily
rewrites inside (f x x).
All in all applications are binary. The fact that the constr data type works
on  n-ary applications is an implementation detail. From this angle,
a subterm of ((f x) x) has to be matched by the pattern (f _).

According to my experience this does not make things slow per se.
Indeed you don't need to try all possible partial applications if you
are guided by the presence of the head symbol f. You just need to align
the pattern with the application's head.

If you are not driven by the head constant then you are right, all
partial application may unify with your pattern.

Cheers
-- 
Enrico Tassi