coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] proving a simple equality, noam neer, 11/19/2016
- Re: [Coq-Club] proving a simple equality, Laurent Thery, 11/19/2016
- Re: [Coq-Club] proving a simple equality, noam neer, 11/20/2016
- Re: [Coq-Club] proving a simple equality, Gaetan Gilbert, 11/21/2016
- Re: [Coq-Club] proving a simple equality, Laurent Thery, 11/21/2016
- Re: [Coq-Club] proving a simple equality, noam neer, 11/22/2016
- [Coq-Club] Re : Re: proving a simple equality, Laurent Thery, 11/22/2016
- Re: [Coq-Club] proving a simple equality, Guillaume Melquiond, 11/22/2016
- Re: [Coq-Club] proving a simple equality, noam neer, 11/22/2016
- Re: [Coq-Club] proving a simple equality, noam neer, 11/20/2016
- Re: [Coq-Club] proving a simple equality, Laurent Thery, 11/19/2016
Archive powered by MHonArc 2.6.18.