Ssreflect Users Discussion List

[Assia Mahboubi <>]

Hi François,

for the sake of completeness, the possibility of rewriting with sets of 
rewrite
rules Georges is talking about is documented in section 7.2 of the manual of
ssreflect (https://hal.inria.fr/inria-00258384v16).

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.

Best,

assia

Le 18/02/2016 12:21, Georges Gonthier a écrit :
>    For nat instances this is mostly a matter of unfolding, because the 
> mathcomp constants addn, subn, and muln functions are convertible to plus, 
> minus and mult, respectively. The separate constants were introduced to 
> improve the behaviour of simpl; this could now be mostly achieved via the 
> Arguments : simpl never directive (unfortunately, with some 
> incompatibilities tied to the inclusion of part of the simpl refolding 
> functionality in basic reduction).
>    This still leaves the issue of recognizing mathcomp inequalities, in 
> goals and assumptions. For int and other numeric types, changes are deeper 
> as mathcomp uses different representations, so a combination of views, 
> injectivity lemmas and rewriting will be necessary to work with omega "as 
> is" - perhaps in the long run it might be better to parametrize omega with 
> the theories it can work with.
>   Finally, indeed mathcomp does not use autorewrite at all, mostly because 
> the internalization of rule sets using pairs gives us more flexibility and 
> control - at some cost in efficiency, which hasn't been a real issue in 
> practice. Note that canonical structures (or type classes) can provide a 
> very efficient alternative to repeated rewriting for morphic transport; see 
> Cyril's generic_quotient.v development for an instance of this.
>    Best,
> Georges
> 
> -----Original Message-----
> From: 
> 
>  
> [mailto:]
>  On Behalf Of François Pottier
> Sent: 18 February 2016 10:42
> To: Benjamin Werner 
> <>
> Cc: 
> 
> Subject: Re: [ssreflect] ssreflect and omega
> 
> Le 02/18/2016 11:30 AM, Benjamin Werner a écrit :
>> If I recall correctly, the idea is to have a bunch of simple equality 
>> lemmas of the form forall x y, x+y = (x+y)%nat to apply them, and then 
>> call omega.
> 
> Thanks for this example. By the way, is autorewrite still used/useful under 
> ssreflect? In standard Coq it would be the preferred way of applying a 
> large set of rewriting rules until a normal form is reached.
> 
> --
> François Pottier
> 
> https://na01.safelinks.protection.outlook.com/?url=http:%2f%2fgallium.inria.fr%2f~fpottier%2f&data=01%7C01%7Cgonthier%40064d.mgd.microsoft.com%7Cfe6b8c5fe0704dc6f2f808d33850244b%7C72f988bf86f141af91ab2d7cd011db47%7C1&sdata=%2bS37O9z%2f3jnadGeV5hrv3KQaLs3TgvL9hSQnirE4B5U%3d
>