The Coq mailing list

[Laurent Thery <laurent.thery AT inria.fr>]

Hi,

personally I use lra (Require Import Psatz) but fourier is fine

--Laurent

----- noam neer 
<noamneer AT gmail.com>
 a écrit :
> thanx.
> 
> BTW, what is the simplest way to prove simple goals like "0<=2"?
> "fourier" works but I wonder if it is not an overkill.
> 
> 
> 
> On Mon, Nov 21, 2016 at 3:01 PM, Laurent Thery 
> <Laurent.Thery AT inria.fr>
> wrote:
> 
> >
> >
> > On 11/20/2016 10:07 PM, noam neer wrote:
> >
> >> thanks.
> >>
> >> however I just tried to use the same trick in a different goal and it
> >> didn't work -
> >>
> >>     Goal Rpower 2 3 = 8.
> >>     change 3 with (INR 3).
> >>
> >>     Error: Not convertible.
> >>
> >> why didn't it work here ?
> >>
> >>
> >
> > Numbers are encoded in R with 0 and 1
> >
> > Compare
> >
> > Check (1 + ((1 + 1) * 5)).
> >
> > with
> >
> > Compute (INR 11).
> >
> > So now INR 11 = 11 is not a conversion anymore, you have to prove the
> > replacement. For example:
> >
> > replace (INR 11) with (11%R) by (simpl; ring).
> >
> > --
> > Laurent
> >
> >
> >
> > --
> > Laurent
> >