The Coq mailing list

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

A few hints that should enable you to complete your proof in both cases :

* a goal like 1000000000000 <> 0 can be proved with discrR.
* a goal like 0 < 100000000000 can be proved with prove_sup, and in
particular, if the inequality is large, just apply left first
(remember, <= on reals is defined as < \/ =)
* to simplify an expression like 100000000000000000 *
(87400000020642221000 / 100000000000000000) in 87400000020642221000,
you can either use Rinv_r_simpl_m (use associativity of multiplication
as well), or use field.

More generally, you should try to understand exactly what kind of
goals customized tactics can prove in order to know when to apply
them, and you should also get accustomed to the lemmas available in
the library in order to manually use them when no tactic can help. For
the second part, SearchAbout/SearchRewrite/SearchPattern are very
useful.

Stéphane L.

On Fri, Mar 13, 2009 at 5:52 PM, Eric Biagioli 
<ericbiagioli AT gmail.com>
 wrote:
> 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.
>>
>>
>



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