From ab6530c5a05cebc23dd677e251ac524bec6e8aee Mon Sep 17 00:00:00 2001
From: desmettr
Date: Tue, 21 Jan 2003 14:03:27 +0000
Subject: 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
---
 theories/Reals/RIneq.v       | 20 --------------------
 theories/Reals/Rtrigo.v      | 15 ++++-----------
 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 09dadee90e..f707081df6 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 f1763a6d2c..631757abee 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 3c87d0d509..004cbda0ce 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.
-- 
cgit v1.2.3