Ssreflect Users Discussion List

[Assia Mahboubi <>]

Hi Jason,

as Enrico said, the matching and pattern selection mechanisms are described in
the manual, available here : http://hal.inria.fr/inria-00258384/en

Section 7 is dedicated to the rewrite tactic but matching and pattern 
selection
are actually in section 4.2 of the current version, as they are also used for
the (sub)term selection tactic 'set'.

Of course, do not hesitate to send examples if this does not answer your 
problems.

Best,

assia

Le 19/06/2014 21:53, Enrico Tassi a écrit :
> 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,
>