Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] proving a simple equality

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proving a simple equality


Chronological Thread 
  • From: noam neer <noamneer AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] proving a simple equality
  • Date: Sun, 20 Nov 2016 23:07:52 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=noamneer AT gmail.com; spf=Pass smtp.mailfrom=noamneer AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f44.google.com
  • Ironport-phdr: 9a23:xDxWKx3xiKnMhtcasmDT+DRfVm0co7zxezQtwd8ZsesQLfad9pjvdHbS+e9qxAeQG96KsLQe0aGP7/ioGTRZp83e4DZaKN0EfiRGoPtVtjRoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blItdaymUrLV2s+wzqW5/4DZSwROnju0J71ofzusqgCEsM4fhMNkJ6srgk/PpXJNfelb30tnIFuSm1D34cLmr80ryDhZp/90r50Iaq79ZaltFbE=

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




Archive powered by MHonArc 2.6.18.

Top of Page