The Coq mailing list

[Eric Biagioli <ericbiagioli AT gmail.com>]

Hello again,

Thank you for the responses. I'm writing again because I tried all the
posibilities and it didn't work. Perhaps I'm doing something wrong?

One of the problems that I am having is when I use the Rmult_le_reg_l.
I get two new goals and I don't know how to proof them.

In one of the many ways that I tried, after some simplifications the
only thing that I get was exactly the same inequality that I had at
the beggining. I was wondering if it could be possible to use the
existent lemma Rle_0_1, that says "0 <= 1". Could be possible to
convert the goal  0 <= 87400000020642221000 / 100000000000000000 into
the goal 0 <= 1 by multiplying and dividing both sides of the
inequality? I tried but I couldn't.

The following are two examples of what I did.  I didn't complete the
proof even in the case in which I added the two hypothesis "0 <
100000000000000000" and "0 < 87400000020642221000"

So, any suggestion?

Thankyou in advance,

Eric


-----Example 1.
Require Import QArith.
Require Import Reals.
Require Import Fourier.

Open Scope R_scope.

Ltac field_simplify_right :=
 match goal with
 |- _ <= ?x => field_simplify (x)
 end.

Section TEST.
 Goal 0 <= 87500000020642221 / 100000000000000000 + -1 / 1000.
 field_simplify_right.
                (*
                        At this point the goal is
                        0 <= 87400000020642221000 / 100000000000000000
                *)
 apply (Rmult_le_reg_l 100000000000000000).

At this point I have two goals.
                (*
                        1) 0 <= 100000000000000000
                        2) 100000000000000000 * 0 <= 100000000000000000 *
(87400000020642221000 / 100000000000000000)
                        
                        I don't know how to prove neither (1) nor (2).
                *)
...
...
-----------------------------------------------------------------------




-----Example 2 (Adding the Hypothesis h0: 0 < 100000000000000000).
Require Import QArith.
Require Import Reals.
Require Import Fourier.

Open Scope R_scope.

Ltac field_simplify_right :=
 match goal with
 |- _ <= ?x => field_simplify (x)
 end.

Theorem aux : forall a b c, c <> 0 -> a * (b / c) = a * b / c.
intros.
field.
assumption.
Qed.

Section TEST.
 Hypothesis h0: 0 < 100000000000000000.

 Goal 0 <= 87500000020642221 / 100000000000000000 + -1 / 1000.
 field_simplify_right.
 apply (Rmult_le_reg_l 100000000000000000).
 assumption.
 rewrite Rmult_0_r.
 rewrite aux.
(* I don't know how to continue ....
At this point I have 2 goals:
1) 0 <= 100000000000000000 * 87400000020642221000 / 100000000000000000
2) 100000000000000000 <> 0
*)

End TEST.
-----------------------------------------------------------------------




On Thu, Mar 12, 2009 at 1:47 PM, Bruno Barras 
<bruno.barras AT inria.fr>
 wrote:
> Stéphane Lescuyer a écrit :
>>
>> 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.
>
> Such simplification can be done by field_simplify. Try e.g.
> field_simplifiy (87500000020642221 / 100000000000000000 + -1 / 1000).
> Then use lemma Rmult_le_reg_l, field_simplify again and then fourier should
> apply (last hint: prove x/1=x with field).
>
> Not as automated as one would expect indeed. Feedback on common situations
> where using field is painful (like this one) is welcome, as it will help us
> improve field.
>
> In the meantime, crafting a small Ltac script that does it automatically is
> a good exercise and will improve your proof script. (I guess Adam Chlipala
> will agree.)
>
> Bruno Barras.
>
>