diff options
author | 2003-01-21 14:03:27 +0000 | |
---|---|---|
committer | 2003-01-21 14:03:27 +0000 | |
commit | ab6530c5a05cebc23dd677e251ac524bec6e8aee (patch) | |
tree | 5c8e18d9e7cfc2debaac6f9ee4bb4c536c8f4da2 /theories/Reals | |
parent | fb5304d62446fb2b054a6320e5368459f95b731f (diff) |
Suppression de INR2 / Conséquence logique de la nouvelle représentation des constantes entières
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3555 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals')
-rw-r--r-- | theories/Reals/RIneq.v | 20 | ||||
-rw-r--r-- | theories/Reals/Rtrigo.v | 15 | ||||
-rw-r--r-- | theories/Reals/Rtrigo_calc.v | 3 |
3 files changed, 5 insertions, 33 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 09dadee90..f707081df 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1574,26 +1574,6 @@ Intro; Ring. Cut ~(O=(2)); [Intro H0; Generalize (lt_INR_0 (2) (neq_O_lt (2) H0)); Unfold INR; Intro; Assumption | Discriminate]. Qed. -(*****************************************************) -(** Complementary results about [INR] *) -(*****************************************************) - -Fixpoint INR2 [n:nat] : R := Cases n of -O => ``0`` -| (S n0) => Cases n0 of -O => ``1`` -| (S _) => ``1+(INR2 n0)`` -end -end. - -Theorem INR_eq_INR2 : (n:nat) (INR n)==(INR2 n). -Induction n; [Unfold INR INR2; Reflexivity | Intros; Unfold INR INR2; Fold INR INR2; Rewrite H; Case n0; [Reflexivity | Intros; Ring]]. -Qed. - -Lemma add_auto : (p,q:nat) ``(INR2 (S p))+(INR2 q)==(INR2 p)+(INR2 (S q))``. -Intros; Repeat Rewrite <- INR_eq_INR2; Repeat Rewrite S_INR; Ring. -Qed. - (**********) Lemma complet_weak : (E:R->Prop) (bound E) -> (ExT [x:R] (E x)) -> (ExT [m:R] (is_lub E m)). Intros; Elim (complet E H H0); Intros; Split with x; Assumption. diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index f1763a6d2..631757abe 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -225,7 +225,7 @@ Intro x; Rewrite -> sin_plus; Rewrite -> sin_PI2; Rewrite -> cos_PI2; Ring. Qed. Lemma PI2_RGT_0 : ``0<PI/2``. -Cut ~(O=(2)); [Intro H; Generalize (lt_INR_0 (2) (neq_O_lt (2) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H1; Generalize (Rmult_lt_pos PI (Rinv ``2``) PI_RGT_0 (Rlt_Rinv ``2`` H1)); Intro H2; Assumption | Discriminate]. +Unfold Rdiv; Apply Rmult_lt_pos; [Apply PI_RGT_0 | Apply Rlt_Rinv; Sup]. Qed. Lemma SIN_bound : (x:R) ``-1<=(sin x)<=1``. @@ -303,20 +303,13 @@ Apply Rlt_monotony. Apply lt_INR_0; Apply neq_O_lt. Assert H2 := (fact_neq_0 (plus (mult (2) n) (1))). Red; Intro; Elim H2; Symmetry; Assumption. -Do 2 Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite INR_eq_INR2; Unfold INR2; Fold INR2; Pose x := (INR2 n). +Do 2 Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Pose x := (INR n); Unfold INR. Replace ``(2*x+1+1+1)*(2*x+1+1)`` with ``4*x*x+10*x+6``; [Idtac | Ring]. Apply Rlt_anti_compatibility with ``-4``; Rewrite Rplus_Ropp_l; Replace ``-4+(4*x*x+10*x+6)`` with ``(4*x*x+10*x)+2``; [Idtac | Ring]. Apply ge0_plus_gt0_is_gt0. Cut ``0<=x``. -Intro; Apply ge0_plus_ge0_is_ge0; Repeat Apply Rmult_le_pos. -Left; Sup0. -Left; Sup0. -Assumption. -Assumption. -Left; Sup0. -Left; Sup0. -Assumption. -Unfold x; Replace R0 with (INR O); [Rewrite <- INR_eq_INR2; Apply le_INR; Apply le_O_n | Reflexivity]. +Intro; Apply ge0_plus_ge0_is_ge0; Repeat Apply Rmult_le_pos; Assumption Orelse Left; Sup. +Unfold x; Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity]. Sup0. Apply INR_eq; Do 2 Rewrite S_INR; Do 3 Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Ring. Apply INR_fact_neq_0. diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 3c87d0d50..004cbda0c 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -386,8 +386,7 @@ Rewrite sqrt_def. Ring. Replace ``3`` with ``(INR (S (S (S O))))`` . Apply pos_INR. -Rewrite INR_eq_INR2. -Reflexivity. +Unfold INR; Rewrite Rplus_sym; Reflexivity. DiscrR. DiscrR. DiscrR. |