Ssreflect Users Discussion List

[Bas Spitters <>]

I tried to get Fourier to work for the constructive reals at some point.

However, the implementation seemed not very modular requiring a lot of reimplementation.

You seemed to be saying that it should not be so difficult.

On Wed, May 7, 2014 at 10:50 AM, Laurent Thery <> wrote:

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