Ssreflect Users Discussion List

[Assia Mahboubi <>]

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?
>

Attachment: multi_rw.v
Description: application/save-to-disk