The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Dear oh dear, just ignore my previous answer. I dont know why (the
habit of using integers maybe ^^), I read "omega" instead of
"fourier". With reals, the inequality should be true but I dont think
that Fourier can deal with divisions.
To prove it "manually", try multiplying both sides by the big
(positive) denumerator (Rmult_le_reg_l willbe your friend) and
simplify in order to end up with an inequality that  automatic tactics
can handle.
Sorry for my first answer again.

Stéphane L.

On Thu, Mar 12, 2009 at 4:43 PM, Stéphane Lescuyer
<stephane.lescuyer AT inria.fr>
 wrote:
> I'll assume that you're dealing with Z integers (otherwise you wouldnt
> write such bignumbers without crashing Coq anyway :)). Since
> comparison on Z is computable (and defined as a function) and your
> expression is ground, (vm_compute; intro; discriminate) should do the
> trick in principle. Similary, for goals involving strict comparisons,
> you can use reflexivity.
>
> Now, in your case, the inequality is False so there's no way you will
> be able to prove that. Try vm_compute and you will see that the goal
> reduces to Gt=Gt -> False which is not provable. The reason for that
> is that the first operand of the sum is 0 (euclidian division) and the
> second is -1 (which can be surprising but thats the way it is defined
> for negative integers in the standard library). Try the division in
> ZOdiv for a more "intuitive" result maybe.
>
> HTH,
>
> Stéphane L.
>
> On Thu, Mar 12, 2009 at 4:26 PM, Eric Biagioli 
>Â <ericbiagioli AT gmail.com>
>  wrote:
>> Hello everyone,
>>
>> I'm writing to ask a little question. I'm sorry if it's a stupid
>> question. I need to prove (in Coq) that
>>
>> 0 <= 87500000020642221/100000000000000000+ -1/1000
>>
>> The "fourier" tactic didn't work (perhaps I'm doing something wrong?),
>> and I don't know what could I do.
>>
>> Thankyou in advance,
>>
>> Eric
>>
>> --------------------------------------------------------
>> Bug reports: http://logical.saclay.inria.fr/coq-bugs
>> Archives: http://pauillac.inria.fr/pipermail/coq-club
>>          http://pauillac.inria.fr/bin/wilma/coq-club
>> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>>
>
>
>
> --
> I'm the kind of guy that until it happens, I won't worry about it. -
> R.H. RoY05, MVP06
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06