The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 11/19/2016 03:03 AM, noam neer wrote:
>     Require Import Reals.
>     Open Scope R_scope.
>
>     Goal forall a b, (a+b)^2 = a^2 + 2*a*b + b^2.
>     intros.
>     field.
>     Qed.
>
> but then I tried the same thing with the real power operator, i.e.
>
>     Goal forall a b, a>0 -> b>0 -> Rpower (a+b) 2 = (Rpower a 2) + 2*a*b
> + (Rpower b 2).

By default, field for R only works with power that are natural numbers:

Check pow

  pow: R -> nat -> R

your goal instead uses the full power function

Check Rpower.

  Rpower_nat : R -> R -> R.

So if you want to orive it with field you have first to convert your full
power to nat power. A theorem exists:

Search Rpower (_ ^ _).

Rpower_pow:
  forall (n : nat) (x : R) (_ : Rlt R0 x), eq (Rpower x (INR n)) (pow x n)

INR is the convertion fron N -> R. So in order to be able to rewrite
you are left with converting  2 in the real to an INR 2.  As a matter
of fact, these two are convertible: INR 2 computes to 2.

you can see that with

Print INR
INR =
fix INR (n : nat) : R :=
  match n with
  | O => R0
  | S O => R1
  | S (S _ as n0) => Rplus (INR n0) R1
  end

and the fact that in R 2 is encoded as 1 + 1 in R
(to see that, apply for example the tactic set (one := 1) to your goal).

Unfortunately rewrite is not powerful enough to discover this convertion 
so you have to help Coq. This gives:

    Goal forall a b, a>0 -> b>0 -> Rpower (a+b) 2 = (Rpower a 2) + 
2*a*b + (Rpower b 2).
    intros.
Search Rpower (_ ^ _).
    change 2 with (INR 2).
    rewrite !Rpower_pow.
    change (INR 2) with 2.
    field.
    trivial.
    trivial.
Search (0 < _ + _).
    apply Rplus_lt_0_compat.
    trivial.
    trivial.
Qed.

--
Laurent