The Coq mailing list

[Fr�d�ric Besson <frederic.besson AT inria.fr>]

On 1 janv. 2012, at 19:56, Ramon Snir wrote:

> Any reason to prefer one over the other?
For this particular goal, both tactics are kind of overkill but I am not 
aware of alternatives...
- As explained by Laurent, field solves equalities over fields.
- lra solves goals involving linear equalities and inequalities.

Your goal is an equality between constants thus in the scope of both...
If the context  contains (many) hypotheses that are linear, 
lra can take time figuring out that those hypotheses are irrelevant...

> Also - when will 8.4 be released?
8.4beta is out! 


> 
> On 01/01/2012 20:11, Frédéric Besson wrote:
>> Using Coq 8.4, the linear real arithmetic tactic (lra) also does the job.
>> 
>> Require Import Reals.
>> Require Import Psatz.
>> Open Scope R_scope.
>> 
>> Goal 7 / 2 * 3 = 21 / 2.
>> Proof.
>>   lra.
>> Qed.
>> 
>>      
>> 
>> On 1 janv. 2012, at 16:36, Ramon Snir wrote:
>> 
>>> Hurrah!
>>> Works like a charm!
>>> 
>>> On 01/01/2012 17:29, Laurent Théry wrote:
>>>> On 12/31/2011 05:27 PM, Ramon Snir wrote:
>>>>> Hello!
>>>>> 
>>>>> I am trying to automate proving multiple equalities over R (would be a 
>>>>> shame if I'd have to manually prove everything), but Rcompute seems to 
>>>>> fail on many cases.
>>>>> 
>>>>> This code:
>>>>> 
>>>>> Goal 7 / 2 * 3 = 21 / 2.
>>>>> Proof.
>>>>> Rcompute.
>>>>> Qed.
>>>>> 
>>>>> Generates:
>>>>> 
>>>>> Toplevel input, characters 0-8:
>>>>> In nested Ltac calls to "Rcompute" and "apply IZR_eq" (expanded to
>>>>> "apply IZR_eq"), last call failed.
>>>>> Error: Impossible to unify "IZR ?6656 = IZR ?6657" with
>>>>> "IZR (1 + 2 * (1 + 2)) / IZR 2 * IZR (1 + 2) =
>>>>>  IZR (1 + 2 * (2 * (1 + 2 * 2))) / IZR 2".
>>>>> 
>>>>> What other way is there to prove almost trivial R equalities?
>>>>> 
>>>> You can use the field tactic that proves all equalities that are true 
>>>> modulo associativity,
>>>> commutativity and distributivity
>>>> 
>>>> 
>>>> Require Import Reals.
>>>> Require Import Field.
>>>> 
>>>> Open Scope R_scope.
>>>> 
>>>> Goal 7 / 2 * 3 = 21 / 2.
>>>> Proof.
>>>> field.
>>>> Qed.
>>>>