Ssreflect Users Discussion List

[Assia Mahboubi <>]

Thank you Georges for the clarification!

And many thanks again François for your question: this part of the manual 
should
definitively be improved :-).

Best,

assia

Le 22/02/2016 12:20, Georges Gonthier a écrit :
>   I'm afraid this is not correct: a multirule rewrites the first subterm to 
> which one of the rules applies in a left-to-right traversal of the goal 
> (caveat: literal matches have priority), with the first rule from the 
> multirule tree in left-to-right order. For repeated rewrites the selection 
> process is repeated anew. You can see this in test6 by doing rewrite 
> 2!multi4, which uses eq_adda_b then eq0 on the left-hand side only).
>    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, 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).
>     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?
>>