Ssreflect Users Discussion List

[Enrico Tassi <>]

On Thu, Jun 19, 2014 at 08:40:18PM +0100, Jason Gross wrote:
> I have run into a number of cases where ssreflect's rewrite will loop
> forever (or at least for a number of minutes), while Coq's rewrite
> (accessed by doing [Ltac coq_rewrite H := rewrite H.] before I've imported
> ssr) will succeed instantly.  I'll set my scripts on generating a minimal
> example, but I was wondering if anyone else has encountered this problem,
> and if anyone could enlighten me as to why this might be happening, or at
> least to the differences between Coq's rewrite and ssr's rewrite.

They are completely different, and the one of ssr is well documented in
the user manual.  

In a few words ssr's rewrite performs an initial filtering phase using
the head symbol of the say LHS of the equation to identify the instance
of the rule (i.e. fix its quantified variables) but then performs full
conversion to identify all the occurrences of such instance.  Especially
this last phase may be costly if you have huge (proof) terms hanging
around and you have mainly 2 mechanisms to drive it: the patterns and the
occurrence numbers.

Best,
-- 
Enrico Tassi