The Coq mailing list

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

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.
>>