Ssreflect Users Discussion List

[Assia Mahboubi <>]

Hello Georges (and list),

reading your message again:

Le 22/02/2016 12:20, Georges Gonthier a écrit :

>    The grouping of pairs does not affect the selection strategy, but it 
> does make it easier include one rule set in another, revrse the direction 
> of a rule subset, 

I did not understand what "reverse the direction of a rule subset" means? 
Since
multi-rules are nested pairs, how could we reverse one of the components?

> or (universally) quantify over parameters of a subset of rules (there is 
> special code that will omit unnecessary quantifiers for rules that can be 
> syntactically extracted).

neither did I get this part. Is there an example of this feature somewhere in
the libraries?

Thanks in advance for your help,

assia

>     Best,
> Georges
> 
> -----Original Message-----
> From: 
> 
>  
> [mailto:]
>  On Behalf Of Assia Mahboubi
> Sent: 22 February 2016 10:46
> To: 
> 
> Subject: Re: [ssreflect] ssreflect and omega
> 
> Hi François,
> 
>   thank you for spotting this problem in the manual. In the attached file, 
> I have tried to clarify the description of the semantic of rewrite with 
> multi-rules and to illustrate its behaviour.
> 
> Now a multi-rule nested in another multi-rule is treated just like an 
> atomic rule. Hence
> 
>  `rewrite !(eq1, (eq2, eq3))`.
> 
> behaves as:
> 
> repeat (
>   repeat rewrite eq1;
>   repeat (
>      repeat rewrite eq2;
>      repeat rewrite eq3
>           )
>         ).
> 
> Hence nested parentheses can be used to implement a normalization procedure 
> which has to complete a certain sub-normalisation before switching to its 
> next step.
> 
> assia
> 
> Le 22/02/2016 08:54, François Pottier a écrit :
>>
>> Hi Assia,
>>
>> Thanks for lia4mathcomp, this should be very useful.
>>
>>> The "Multi-rule rewriting" paragraph, p. 41, includes an example of 
>>> multi-rule implementing the translation of a signature on nat into 
>>> another one, which illustrates the possibilities of control (by 
>>> nested parentheses) mentioned by Georges.
>>
>> I must say that I find this part of the manual very mysterious. The 
>> manual says "Note that the inner parentheses of trecE guide the 
>> rewrite strategy operated by this tactic." OK, so the parentheses 
>> serve *some* purpose... But what is their exact semantics?
>>