Ssreflect Users Discussion List

[Georges Gonthier <>]

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