Ssreflect Users Discussion List

[Laurent Thery <>]

On 05/06/2014 10:44 PM, Bas Spitters wrote:

Yesterday over lunch we had a similar discussion whether omega/lia would work for non-standard arithmetic.

In theory it should of course, it is just another model of PA/HA.
However, the backend may not be so flexible.

On Tue, May 6, 2014 at 8:05 PM, Laurent Thery <> wrote:

-------- Original Message -------- Subject: Re: [ssreflect] omega and mathcomp Date: Tue, 06 May 2014 20:04:52 +0200 From: Laurent Thery <> To: Maxime Dénès <>

On 05/06/2014 07:59 PM, Maxime Dénès wrote:
> I've always wondered (because I'm not using these things a lot), is 
> there any reason to prefer omega over romega?
>

The implementation is a matter of taste (reflexive or not) but from what 
I recall they don' t solve
exactly the same goals so you can' t replace blindly one by the other.

The base of omega and lia is Fourier Motzkin. That is clearly largely applicable.
See for example my (old !) toy implementation.

ftp://ftp-sop.inria.fr/marelle/Laurent.Thery/Fourier.zip

Then there are different technique (cut, omega test) that take care of the discrete nature
of things but you may not be interested by those.

--
Laurent