diff options
Diffstat (limited to 'theories/Reals/Rbase.v')
-rw-r--r-- | theories/Reals/Rbase.v | 169 |
1 files changed, 169 insertions, 0 deletions
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index bfbab59bd..b459a3d85 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -224,6 +224,13 @@ Intro;Generalize (H0 r1==R0 r2==R0 (Rmult r1 r2)==R0 Tauto. Save. +(**********) +Lemma Rmult_Rplus_distrl: + (r1,r2,r3:R) ((Rmult (Rplus r1 r2) r3)== + (Rplus (Rmult r1 r3) (Rmult r2 r3))). +Intros; Ring. +Save. + (***********) Definition Rsqr:R->R:=[r:R](Rmult r r). @@ -282,6 +289,13 @@ Tauto. Save. (**********) +Lemma Rminus_distr: + (x,y,z:R) (Rmult x (Rminus y z))== + (Rminus (Rmult x y) (Rmult x z)). +Intros; Ring. +Save. + +(**********) Lemma eq_Ropp:(r1,r2:R)(r1==r2)->((Ropp r1)==(Ropp r2)). Auto with real. Save. @@ -316,6 +330,28 @@ Intros;Red;Intro;Generalize (Rplus_plus_r r (Ropp r) R0 H0);Intro; Save. (*********) +Lemma Rinv_R1:(Rinv R1)==R1. +Apply (r_Rmult_mult R1 (Rinv R1) R1); + [Rewrite (Rinv_r R1 R1_neq_R0); + Rewrite (let (H1,H2)=(Rmult_ne R1) in H1);Trivial| + Red;Intro;Apply R1_neq_R0;Assumption]. +Save. + +(*********) +Lemma Rinv_neq_R0:(r:R)(~r==R0)->~(Rinv r)==R0. +Intros;Red;Intro;Generalize (Rmult_mult_r r (Rinv r) R0 H0); + Clear H0;Intro;Rewrite (Rinv_r r H) in H0;Rewrite (Rmult_Or r) in H0; + Generalize R1_neq_R0;Intro;Auto. +Save. + +(*********) +Lemma Rinv_Rinv:(r:R)(~r==R0)->(Rinv (Rinv r))==r. +Intros;Apply (r_Rmult_mult (Rinv r) (Rinv (Rinv r)) r); + [Rewrite (Rinv_r (Rinv r) (Rinv_neq_R0 r H)); + Rewrite (Rinv_l r H);Trivial |Apply Rinv_neq_R0;Assumption]. +Save. + +(*********) Lemma Rinv_Rmult:(r1,r2:R)(~r1==R0)->(~r2==R0)-> (Rinv (Rmult r1 r2))==(Rmult (Rinv r1) (Rinv r2)). Intros;Cut ~(Rmult r1 r2)==R0. @@ -375,6 +411,13 @@ Elim (imp_not_Req r2 r1);Auto with zarith real. Save. (**********) +Lemma Rlt_ge_not:(r1,r2:R)(Rlt r1 r2)->~(Rge r1 r2). +Intros;Red;Intro;Unfold Rge in H0;Unfold Rgt in H0;Elim H0;Intro. +Apply (Rlt_antisym r1 r2 H H1). +Rewrite H1 in H;Exact (Rlt_antisym r2 r2 H H). +Save. + +(**********) Lemma Rle_le_eq:(r1,r2:R)(Rle r1 r2)/\(Rle r2 r1)<->(r1==r2). Intros; Split; Intro. Elim H; Unfold Rle; Intros. @@ -493,6 +536,18 @@ Apply (Rlt_anti_compatibility r R0 (Ropp r)); Save. (**********) +Lemma Rle_monotony: + (r,r1,r2:R) + (Rle R0 r) + ->(Rle r1 r2)->(Rle (Rmult r r1) (Rmult r r2)). +Intros r r1 r2;Unfold Rle;Intros;Elim H;Elim H0;Intros. +Left;Apply Rlt_monotony;Assumption. +Right;Rewrite H1;Reflexivity. +Right;Rewrite <- H2;Rewrite Rmult_Ol;Rewrite Rmult_Ol;Reflexivity. +Right;Rewrite H1;Reflexivity. +Save. + +(**********) Lemma Rlt_minus:(r1,r2:R)(Rlt r1 r2)->(Rlt (Rminus r1 r2) R0). Intros; Cut (Rlt (Rminus r1 r2) (Rminus r2 r2)). Rewrite -> (eq_Rminus r2); Auto with zarith real. @@ -646,6 +701,37 @@ Rewrite (Rmult_Or r);Intro;Generalize R1_neq_R0;Auto. Apply (imp_not_Req r R0);Left;Assumption. Save. +(*********) +Lemma Rinv_lt:(r1,r2:R)(Rlt R0 (Rmult r1 r2))->(Rlt r1 r2)-> + (Rlt (Rinv r2) (Rinv r1)). +Intros;Generalize (Rlt_monotony (Rinv (Rmult r1 r2)) r1 r2 + (Rlt_Rinv (Rmult r1 r2) H) H0);Intro; + Elim (without_div_O_contr r1 r2 + (sym_not_eqT R R0 (Rmult r1 r2) (imp_not_Req R0 (Rmult r1 r2) + (or_introl (Rlt R0 (Rmult r1 r2)) (Rgt R0 (Rmult r1 r2)) H)))); + Intros;Rewrite Rinv_Rmult in H1;Auto; + Rewrite (Rmult_assoc (Rinv r1) (Rinv r2) r2) in H1; + Rewrite (Rinv_l r2 H3) in H1; + Rewrite (let (H1,H2)=(Rmult_ne (Rinv r1)) in H1) in H1; + Rewrite (Rmult_sym (Rinv r1) (Rinv r2)) in H1; + Rewrite (Rmult_assoc (Rinv r2) (Rinv r1) r1 ) in H1; + Rewrite (Rinv_l r1 H2) in H1; + Rewrite (let (H1,H2)=(Rmult_ne (Rinv r2)) in H1) in H1;Assumption. +Save. + +(**********) +Lemma Rlt_monotony_rev: + (r,r1,r2:R)(Rlt R0 r)->(Rlt (Rmult r r1) (Rmult r r2)) + ->(Rlt r1 r2). +Intros;Cut (s:R) (Rmult (Rinv r) (Rmult r s))==s. +Intros; Rewrite <- (H1 r1); Rewrite <- (H1 r2);Apply Rlt_monotony. +Apply Rlt_Rinv; Assumption. +Assumption. +Intro;Rewrite <- Rmult_assoc;Rewrite Rinv_l. +Ring. +Apply imp_not_Req; Right; Unfold Rgt; Assumption. +Save. + (*********************************************************) (* Greater *) (*********************************************************) @@ -815,6 +901,14 @@ Right; Apply (r_Rplus_plus r r1 r2 H0). Save. (***********) +Lemma Rge_monotony: + (x,y,z:R) (Rge z R0) -> (Rge x y) -> (Rge (Rmult x z) (Rmult y z)). +Intros;Apply Rle_sym1; + Rewrite (Rmult_sym y z); Rewrite (Rmult_sym x z); + Apply Rle_monotony;Apply Rle_sym2; Assumption. +Save. + +(***********) Lemma Rgt_minus:(r1,r2:R)(Rgt r1 r2)->(Rgt (Rminus r1 r2) R0). Intros; Cut (Rgt (Rminus r1 r2) (Rminus r2 r2)). Rewrite -> (eq_Rminus r2 r2); Auto with zarith real. @@ -823,6 +917,16 @@ Unfold Rminus; Rewrite -> (Rplus_sym r1 (Ropp r2)); Apply (Rgt_plus_plus_r (Ropp r2) r1 r2 H). Save. +(*********) +Lemma minus_Rgt:(r1,r2:R)(Rgt (Rminus r1 r2) R0)->(Rgt r1 r2). +Intros;Generalize (Rgt_plus_plus_r r2 (Rminus r1 r2) R0 H); Intro; + Rewrite (Rplus_sym r2 (Rminus r1 r2)) in H0;Unfold Rminus in H0; + Rewrite (Rplus_assoc r1 (Ropp r2) r2) in H0; + Rewrite (Rplus_Ropp_l r2) in H0; + Elim (Rplus_ne r1); Intros a b; Rewrite a in H0; Clear a b; + Elim (Rplus_ne r2); Intros a b; Rewrite a in H0; Clear a b;Exact H0. +Save. + (**********) Lemma Rge_minus:(r1,r2:R)(Rge r1 r2)->(Rge (Rminus r1 r2) R0). Unfold Rge; Intros; Elim H; Intro. @@ -846,6 +950,12 @@ Unfold Rgt;Intros;Generalize (Rlt_monotony r1 R0 r2 H H0);Intro; Rewrite (Rmult_Or r1) in H1;Assumption. Save. +(*********) +Lemma Rmult_lt_pos:(x,y:R)(Rlt R0 x)->(Rlt R0 y)->(Rlt R0 (Rmult x y)). +Generalize Rmult_gt;Unfold Rgt;Auto. +Save. + + (***********) Lemma Rplus_eq_R0:(a,b:R)(Rle R0 a)->(Rle R0 b)->(Rplus a b)==R0-> (a==R0)/\(b==R0). @@ -919,6 +1029,34 @@ Unfold Rminus; Rewrite -> Rplus_sym; Rewrite -> Rplus_assoc; Auto with zarith real. Save. +(*********) +Lemma mult_INR:(n,m:nat)(INR (mult n m))==(Rmult (INR n) (INR m)). +Induction n. +Simpl; Intro;Apply sym_eqT;Apply Rmult_Ol. +Intros;Unfold 1 mult;Cbv Beta Iota;Fold mult; + Rewrite (plus_INR m (mult n0 m));Rewrite (H m); + Pattern 1 (INR m); + Rewrite <-(let (H1,H2)=(Rmult_ne (INR m)) in H1); + Rewrite (Rmult_sym (INR n0) (INR m)); + Rewrite <-(Rmult_Rplus_distr (INR m) R1 (INR n0)); + Rewrite (Rplus_sym R1 (INR n0));Rewrite <-(S_INR n0); + Apply Rmult_sym. +Save. + + +(*********) +Lemma INR_lt_0:(n:nat)(lt O n)->(Rlt R0 (INR n)). +Induction n;Intros. +Absurd (lt (0) (0));[Apply lt_n_n|Assumption]. +Elim (le_lt_or_eq (0) n0 (lt_n_Sm_le (0) n0 H0));Intro. +Generalize (H H1);Clear H H1;Intro;Rewrite (S_INR n0); + Generalize (Rlt_compatibility R1 R0 (INR n0) H);Intro; + Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H1; + Rewrite (Rplus_sym (INR n0) R1); + Apply (Rlt_trans R0 R1 (Rplus R1 (INR n0)) (Rlt_R0_R1) H1). +Rewrite <-H1;Simpl;Apply Rlt_R0_R1. +Save. + (**********) Lemma INR_le:(n:nat)(Rle R0 (INR n)). Induction n. @@ -927,6 +1065,18 @@ Intros;Rewrite (S_INR n0);Apply (Rlt_le R0 (Rplus (INR n0) R1)); Apply (Rlt_r_plus_R1 (INR n0) H). Save. +(*********) +Lemma INR_le_nm:(n,m:nat)(le n m)->(Rle (INR n) (INR m)). +Intros;Elim (le_lt_or_eq n m H);Intro. +Cut (lt (0) (minus m n)). +Intro;Generalize (INR_lt_0 (minus m n) H1); + Intro;Rewrite minus_INR in H2;Auto; + Apply (Rlt_le (INR n) (INR m));Fold (Rgt (INR m) (INR n)); + Apply (minus_Rgt (INR m) (INR n));Unfold Rgt;Assumption. +Omega. +Rewrite H0;Unfold Rle;Right;Trivial. +Save. + (**********) Lemma not_INR_O:(n:nat)~(INR n)==R0->~n=O. Intros;Cut n=(0)->(INR n)==R0. @@ -952,6 +1102,11 @@ Save. Definition INZ:=inject_nat. (**********) +Lemma IZN:(z:Z)(`0<=z`)->(Ex [n:nat] z=(INZ n)). +Unfold INZ;Intros;Apply inject_nat_complete;Assumption. +Save. + +(**********) Lemma INR_IZR_INZ:(n:nat)(INR n)==(IZR (INZ n)). Induction n;Auto with zarith real. Intros;Rewrite S_INR;Simpl;Rewrite bij1;Rewrite <-S_INR;Auto with zarith real. @@ -1077,6 +1232,14 @@ Intros;Generalize (eq_Rminus (IZR z1) (IZR z2) H); Intro;Omega. Save. +(*********) +Lemma le_O_IZR:(z:Z)(Rle R0 (IZR z))->(Zle ZERO z). +Unfold Rle;Intros;Elim H;Clear H;Intro. +Unfold Zle;Red;Intro;Apply (Zlt_le_weak `0` z (lt_O_IZR z H)); + Assumption. +Generalize (eq_IZR_R0 z (sym_eqT R R0 (IZR z) H));Intro;Omega. +Save. + (**********) Lemma le_IZR_R1:(z:Z)(Rle (IZR z) R1)->(Zle z `1`). Induction z; Intros. @@ -1106,6 +1269,12 @@ Intro;Rewrite H1 in H0;Clear H1 H;Apply (eq_IZR (NEG p) `1` H0). Save. (**********) +Lemma IZR_ge: + (m,n:Z) `m>= n` ->(Rge (IZR m) (IZR n)). +Intros;Apply Rlt_not_ge;Red;Intro;Generalize (lt_IZR m n H0);Intro; Omega. +Save. + +(**********) Lemma single_z_r_R1:(r:R)(z,x:Z)(Rlt r (IZR z))->(Rle (IZR z) (Rplus r R1)) ->(Rlt r (IZR x))->(Rle (IZR x) (Rplus r R1))->z=x. Intros;Generalize (Rlt_Ropp r (IZR x) H1);Intro; |