diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /theories/Reals/Machin.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'theories/Reals/Machin.v')
-rw-r--r-- | theories/Reals/Machin.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v index 40a857e3..1a94f6a8 100644 --- a/theories/Reals/Machin.v +++ b/theories/Reals/Machin.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,6 +16,7 @@ Require Import Rseries. Require Import SeqProp. Require Import PartSum. Require Import Ratan. +Require Import Omega. Local Open Scope R_scope. @@ -27,6 +28,7 @@ Lemma atan_sub_correct : forall u v, 1 + u * v <> 0 -> -PI/2 < atan u - atan v < PI/2 -> -PI/2 < atan (atan_sub u v) < PI/2 -> atan u = atan v + atan (atan_sub u v). +Proof. intros u v pn0 uvint aint. assert (cos (atan u) <> 0). destruct (atan_bound u); apply Rgt_not_eq, cos_gt_0; auto. @@ -44,6 +46,7 @@ Qed. Lemma tech : forall x y , -1 <= x <= 1 -> -1 < y < 1 -> -PI/2 < atan x - atan y < PI/2. +Proof. assert (ut := PI_RGT_0). intros x y [xm1 x1] [ym1 y1]. assert (-(PI/4) <= atan x). @@ -67,6 +70,7 @@ Qed. (* A simple formula, reasonably efficient. *) Lemma Machin_2_3 : PI/4 = atan(/2) + atan(/3). +Proof. assert (utility : 0 < PI/2) by (apply PI2_RGT_0). rewrite <- atan_1. rewrite (atan_sub_correct 1 (/2)). @@ -77,6 +81,7 @@ apply atan_bound. Qed. Lemma Machin_4_5_239 : PI/4 = 4 * atan (/5) - atan(/239). +Proof. rewrite <- atan_1. rewrite (atan_sub_correct 1 (/5)); [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier | @@ -105,6 +110,7 @@ unfold atan_sub; field. Qed. Lemma Machin_2_3_7 : PI/4 = 2 * atan(/3) + (atan (/7)). +Proof. rewrite <- atan_1. rewrite (atan_sub_correct 1 (/3)); [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier | |