The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

3 is (1 + (1 + 1)) but (INR 3) is ((1 + 1) + 1)

Gaëtan Gilbert

On 20/11/2016 22:07, noam neer wrote:

thanks.

however I just tried to use the same trick in a different goal and it didn't work -

    Goal Rpower 2 3 = 8.

    change 3 with (INR 3).

    Error: Not convertible.

why didn't it work here ?

On Sat, Nov 19, 2016 at 11:43 AM, Laurent Thery <Laurent.Thery AT inria.fr> wrote:


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