Ssreflect Users Discussion List

[Georges Gonthier <>]

   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