The Coq mailing list

[Laurent Th�ry <Laurent.Thery AT inria.fr>]

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.