diff options
author | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-30 15:31:47 +0000 |
---|---|---|
committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-30 15:31:47 +0000 |
commit | 83a067cae072132484cfe18a5c7b4e91676deedf (patch) | |
tree | fb4505c094fdf1121c00d8a93c7cd686d4fb443e /theories/Reals/Rbase.v | |
parent | 0b52b95c747f220576468f4e12ab4156499a649f (diff) |
Integration de nouveaux lemmes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2253 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rbase.v')
-rw-r--r-- | theories/Reals/Rbase.v | 98 |
1 files changed, 98 insertions, 0 deletions
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index 3a1d677db..b37b7b1a0 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -1501,3 +1501,101 @@ Intros r z H1 H2 (s, (H3,(H4,H5))). Apply H3; Apply single_z_r_R1 with r; Trivial. Save. +(*****************************************************************) +(* Définitions de nouveaux types *) +(*****************************************************************) + +Record nonnegreal : Type := mknonnegreal { +nonneg :> R; +cond_nonneg : ``0<=nonneg`` }. + +Record posreal : Type := mkposreal { +pos :> R; +cond_pos : ``0<pos`` }. + +Record nonposreal : Type := mknonposreal { +nonpos :> R; +cond_nonpos : ``nonpos<=0`` }. + +Record negreal : Type := mknegreal { +neg :> R; +cond_neg : ``neg<0`` }. + +Record nonzeroreal : Type := mknonzeroreal { +nonzero :> R; +cond_nonzero : ~``nonzero==0`` }. + +(**********) +Lemma prod_neq_R0 : (x,y:R) ~``x==0``->~``y==0``->~``x*y==0``. +Intros; Red; Intro; Generalize (without_div_Od x y H1); Intro; Elim H2; Intro; [Rewrite H3 in H; Elim H | Rewrite H3 in H0; Elim H0]; Reflexivity. +Save. + +(**********) +Lemma regle_signe : (x,y:R) ``0<x`` -> ``0<y`` -> ``0<x*y``. +Intros; Rewrite <- (Rmult_Ol x); Rewrite <- (Rmult_sym x); Apply (Rlt_monotony x R0 y H H0). +Save. + +(*********) +Lemma regle_signe_le : (x,y:R) ``0<=x`` -> ``0<=y`` -> ``0<=x*y``. +Intros; Rewrite <- (Rmult_Ol x); Rewrite <- (Rmult_sym x); Apply (Rle_monotony x R0 y H H0). +Save. + +(**********************************************************) +(* Quelques règles concernant < et <= *) +(**********************************************************) + +Lemma gt0_plus_gt0_is_gt0 : (x,y:R) ``0<x`` -> ``0<y`` -> ``0<x+y``. +Intros; Apply Rlt_trans with x; [Assumption | Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rlt_compatibility; Assumption]. +Save. + +Lemma ge0_plus_gt0_is_gt0 : (x,y:R) ``0<=x`` -> ``0<y`` -> ``0<x+y``. +Intros; Apply Rle_lt_trans with x; [Assumption | Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rlt_compatibility; Assumption]. +Save. + +Lemma gt0_plus_ge0_is_gt0 : (x,y:R) ``0<x`` -> ``0<=y`` -> ``0<x+y``. +Intros; Rewrite <- Rplus_sym; Apply ge0_plus_gt0_is_gt0; Assumption. +Save. + +Lemma ge0_plus_ge0_is_ge0 : (x,y:R) ``0<=x`` -> ``0<=y`` -> ``0<=x+y``. +Intros; Apply Rle_trans with x; [Assumption | Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Assumption]. +Save. + +Lemma ge0_plus_ge0_eq_0 : (x,y:R) ``0<=x`` -> ``0<=y`` -> ``x+y==0`` -> ``x==0``/\``y==0``. +Intros; Split; [Elim H; Intro; [Generalize (gt0_plus_ge0_is_gt0 x y H2 H0); Intro; Rewrite H1 in H3; Elim (Rlt_antirefl ``0`` H3) | Symmetry; Assumption] | Elim H0; Intro; [Generalize (ge0_plus_gt0_is_gt0 x y H H2); Intro; Rewrite H1 in H3; Elim (Rlt_antirefl R0 H3) | Symmetry; Assumption]]. +Save. + +Lemma Rmult_le : (r1,r2,r3,r4:R) ``0<=r1`` -> ``0<=r3`` -> ``r1<=r2`` -> ``r3<=r4`` -> ``r1*r3<=r2*r4``. +Intros; Apply Rle_trans with ``r2*r3``; [Apply Rle_monotony_r; Assumption | Apply Rle_monotony; [ Apply Rle_trans with r1; Assumption | Assumption]]. +Save. + +Lemma plus_le_is_le : (x,y,z:R) ``0<=y`` -> ``x+y<=z`` -> ``x<=z``. +Intros; Apply Rle_trans with ``x+y``; [Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Assumption | Assumption]. +Save. + +Lemma le_plus_lt_is_lt : (x,y,z,t:R) ``x<=y`` -> ``z<t`` -> ``x+z<y+t``. +Intros; Apply Rle_lt_trans with ``y+z``; [Apply Rle_compatibility_r; Assumption | Apply Rlt_compatibility; Assumption]. +Save. + +Lemma plus_lt_is_lt : (x,y,z:R) ``0<=y`` -> ``x+y<z`` -> ``x<z``. +Intros; Apply Rle_lt_trans with ``x+y``; [Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Assumption | Assumption]. +Save. + +Lemma Rmult_lt2 : (r1,r2,r3,r4:R) ``0<=r1`` -> ``0<=r3`` -> ``r1<r2`` -> ``r3<r4`` -> ``r1*r3<r2*r4``. +Intros; Apply Rle_lt_trans with ``r2*r3``; [Apply Rle_monotony_r; [Assumption | Left; Assumption] | Apply Rlt_monotony; [Apply Rle_lt_trans with r1; Assumption | Assumption]]. +Save. + +(*****************************************************) +(* Résultat complémentaire sur la fonction 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]]. +Save.
\ No newline at end of file |