From b9b7500136380e2465c13af1fba1019fad0c2ebf Mon Sep 17 00:00:00 2001 From: mayero Date: Mon, 18 Jun 2001 20:23:14 +0000 Subject: Ajouts de lemmes (pour Float) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1791 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Reals/R_Ifp.v | 14 +++ theories/Reals/Rbase.v | 95 ++++++++++++++--- theories/Reals/Rbasic_fun.v | 69 +++++++++++- theories/Reals/Rfunctions.v | 250 ++++++++++++++++++++++++++++++++++++++++++-- theories/Reals/Rtrigo_fun.v | 8 +- 5 files changed, 407 insertions(+), 29 deletions(-) diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index a6ac4c922..240b8c920 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -131,6 +131,20 @@ Generalize (Rgt_plus_plus_r (Ropp R1) (IZR (up r)) r H);Intro; Rewrite a in H2;Clear a b;Auto with zarith real. Save. +(**********) +Lemma Int_part_INR:(n : nat) (Int_part (INR n)) = (inject_nat n). +Intros n; Unfold Int_part. +Cut (up (INR n)) = (Zplus (inject_nat n) (inject_nat (1))). +Intros H'; Rewrite H'; Simpl; Ring. +Apply sym_equal; Apply tech_up; Auto. +Replace (Zplus (inject_nat n) (inject_nat (1))) with (INZ (S n)). +Repeat Rewrite <- INR_IZR_INZ. +Apply lt_INR; Auto. +Rewrite Zplus_sym; Rewrite <- inj_plus; Simpl; Auto. +Rewrite plus_IZR; Simpl; Auto with real. +Repeat Rewrite <- INR_IZR_INZ; Auto with real. +Save. + (**********) Lemma fp_nat:(r:R)(frac_part r)==R0->(Ex [c:Z](r==(IZR c))). Unfold frac_part;Intros;Split with (Int_part r);Apply Rminus_eq; Auto with zarith real. diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index 23fb79c5c..f2603ca67 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -1208,18 +1208,18 @@ Save. Hints Resolve plus_INR minus_INR mult_INR : real. (*********) -Lemma INR_lt_0:(n:nat)(lt O n)->``0 < (INR n)``. +Lemma lt_INR_0:(n:nat)(lt O n)->``0 < (INR n)``. Induction 1; Intros; Auto with real. Rewrite S_INR; Auto with real. Save. -Hints Resolve INR_lt_0: real. +Hints Resolve lt_INR_0: real. -Lemma INR_lt_nm:(n,m:nat)(lt n m)->``(INR n) < (INR m)``. +Lemma lt_INR:(n,m:nat)(lt n m)->``(INR n) < (INR m)``. Induction 1; Intros; Auto with real. Rewrite S_INR; Auto with real. Rewrite S_INR; Apply Rlt_trans with (INR m0); Auto with real. Save. -Hints Resolve INR_lt_nm: real. +Hints Resolve lt_INR: real. Lemma INR_lt_1:(n:nat)(lt (S O) n)->``1 < (INR n)``. Intros;Replace ``1`` with (INR (S O));Auto with real. @@ -1228,27 +1228,42 @@ Hints Resolve INR_lt_1: real. (**********) Lemma INR_pos : (p:positive)``0<(INR (convert p))``. -Intro; Apply INR_lt_0. +Intro; Apply lt_INR_0. Simpl; Auto with real. Apply compare_convert_O. Save. Hints Resolve INR_pos : real. (**********) -Lemma INR_le:(n:nat)``0 <= (INR n)``. +Lemma pos_INR:(n:nat)``0 <= (INR n)``. Intro n; Case n. Simpl; Auto with real. Auto with arith real. Save. -Hints Resolve INR_le: real. +Hints Resolve pos_INR: real. + +Lemma INR_lt:(n,m:nat)``(INR n) < (INR m)``->(lt n m). +Double Induction 1 2;Intros. +Simpl;ElimType False;Apply (Rlt_antirefl R0);Auto. +Auto with arith. +Generalize (pos_INR (S n0));Intro;Cut (INR O)==R0; + [Intro H2;Rewrite H2 in H0;Idtac|Simpl;Trivial]. +Generalize (Rle_lt_trans ``0`` (INR (S n0)) ``0`` H1 H0);Intro; + ElimType False;Apply (Rlt_antirefl R0);Auto. +Do 2 Rewrite S_INR in H1;Cut ``(INR n1) < (INR n0)``. +Intro H2;Generalize (H0 n0 H2);Intro;Auto with arith. +Apply (Rlt_anti_compatibility ``1`` (INR n1) (INR n0)). +Rewrite Rplus_sym;Rewrite (Rplus_sym ``1`` (INR n0));Trivial. +Save. +Hints Resolve INR_lt: real. (*********) -Lemma INR_le_nm:(n,m:nat)(le n m)->``(INR n)<=(INR m)``. +Lemma le_INR:(n,m:nat)(le n m)->``(INR n)<=(INR m)``. Induction 1; Intros; Auto with real. Rewrite S_INR. Apply Rle_trans with (INR m0); Auto with real. Save. -Hints Resolve INR_le_nm: real. +Hints Resolve le_INR: real. (**********) Lemma not_INR_O:(n:nat)``(INR n)<>0``->~n=O. @@ -1276,6 +1291,27 @@ Apply sym_not_eqT; Apply imp_not_Req; Auto with real. Save. Hints Resolve not_nm_INR : real. +Lemma INR_eq: (n,m:nat)(INR n)==(INR m)->n=m. +Intros;Case (le_or_lt n m); Intros H1. +Case (le_lt_or_eq ? ? H1); Intros H2;Auto. +Cut ~n=m. +Intro H3;Generalize (not_nm_INR n m H3);Intro H4; + ElimType False;Auto. +Omega. +Symmetry;Cut ~m=n. +Intro H3;Generalize (not_nm_INR m n H3);Intro H4; + ElimType False;Auto. +Omega. +Save. +Hints Resolve INR_eq : real. + +Lemma INR_le: (n, m : nat) (Rle (INR n) (INR m)) -> (le n m). +Intros;Elim H;Intro. +Generalize (INR_lt n m H0);Intro;Auto with arith. +Generalize (INR_eq n m H0);Intro;Rewrite H1;Auto. +Save. +Hints Resolve INR_le : real. + Lemma not_1_INR:(n:nat)~n=(S O)->``(INR n)<>1``. Replace ``1`` with (INR (S O)); Auto with real. Save. @@ -1299,8 +1335,8 @@ Induction n; Auto with real. Intros; Simpl; Rewrite bij1; Auto with real. Save. -Lemma plus_IZR_NEG_POS : - (p,q:positive)(IZR `(POS p)+(NEG q)`)==``(IZR (POS p))+(IZR (NEG q))``. +Lemma plus_IZR_NEG_POS : + (p,q:positive)(IZR `(POS p)+(NEG q)`)==``(IZR (POS p))+(IZR (NEG q))``. Intros. Case (lt_eq_lt_dec (convert p) (convert q)). Intros [H | H]; Simpl. @@ -1326,6 +1362,20 @@ Rewrite Zplus_sym; Rewrite Rplus_sym; Apply plus_IZR_NEG_POS. Simpl; Intros; Rewrite convert_add; Rewrite plus_INR; Auto with real. Save. +(**********) +Lemma mult_IZR:(z,t:Z)(IZR `z*t`)==``(IZR z)*(IZR t)``. +Intros z t; Case z; Case t; Simpl; Auto with real. +Intros t1 z1; Rewrite times_convert; Auto with real. +Intros t1 z1; Rewrite times_convert; Auto with real. +Rewrite Rmult_sym. +Rewrite Ropp_mul1; Auto with real. +Apply eq_Ropp; Rewrite mult_sym; Auto with real. +Intros t1 z1; Rewrite times_convert; Auto with real. +Rewrite Ropp_mul1; Auto with real. +Intros t1 z1; Rewrite times_convert; Auto with real. +Rewrite Ropp_mul2; Auto with real. +Save. + (**********) Lemma Ropp_Ropp_IZR:(z:Z)(IZR (`-z`))==``-(IZR z)``. Intro z; Case z; Simpl; Auto with real. @@ -1368,6 +1418,12 @@ Intros;Generalize (eq_Rminus (IZR z1) (IZR z2) H); Intro;Omega. Save. +(**********) +Lemma not_O_IZR:(z:Z)`z<>0`->``(IZR z)<>0``. +Intros z H; Red; Intros H0; Case H. +Apply eq_IZR; Auto. +Save. + (*********) Lemma le_O_IZR:(z:Z)``0<= (IZR z)``->`0<=z`. Unfold Rle; Intros z [H|H]. @@ -1395,6 +1451,17 @@ Intros;Apply Rlt_not_ge;Red;Intro. Generalize (lt_IZR m n H0); Intro; Omega. Save. +Lemma IZR_le: (m,n:Z) `m<= n` -> ``(IZR m)<=(IZR n)``. +Intros;Apply Rgt_not_le;Red;Intro. +Unfold Rgt in H0;Generalize (lt_IZR n m H0); Intro; Omega. +Save. + +Lemma IZR_lt: (m,n:Z) `m< n` -> ``(IZR m)<(IZR n)``. +Intros;Cut `m<=n`. +Intro H0;Elim (IZR_le m n H0);Intro;Auto. +Generalize (eq_IZR m n H1);Intro;ElimType False;Omega. +Omega. + Lemma one_IZR_lt1 : (z:Z)``-1<(IZR z)<1``->`z=0`. Intros z (H1,H2). Apply Zle_antisym. @@ -1419,9 +1486,9 @@ Save. (**********) -Lemma single_z_r_R1 - : (r:R)(z,x:Z)``r<(IZR z)``->``(IZR z)<=r+1``->``r<(IZR x)``->``(IZR x)<=r+1`` - ->z=x. +Lemma single_z_r_R1: + (r:R)(z,x:Z)``r<(IZR z)``->``(IZR z)<=r+1``->``r<(IZR x)``-> + ``(IZR x)<=r+1``->z=x. Intros; Apply one_IZR_r_R1 with r; Auto. Save. diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 1079323dc..34bb1f790 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -76,6 +76,35 @@ Generalize (not_Rle r1 r2 n);Clear n;Intro;Unfold Rgt in H0; Apply (Rlt_le r r1 (Rle_lt_trans r r2 r1 H H0)). Save. +Lemma RmaxLess1: (r1, r2 : R) (Rle r1 (Rmax r1 r2)). +Intros r1 r2; Unfold Rmax; Case (total_order_Rle r1 r2); Auto with real. +Save. + +Lemma RmaxLess2: (r1, r2 : R) (Rle r2 (Rmax r1 r2)). +Intros r1 r2; Unfold Rmax; Case (total_order_Rle r1 r2); Auto with real. +Save. + +Lemma RmaxSym: (p, q : R) (Rmax p q) == (Rmax q p). +Intros p q; Unfold Rmax; + Case (total_order_Rle p q); Case (total_order_Rle q p); Auto; Intros H1 H2; + Apply Rle_antisym; Auto with real. +Save. + +Lemma RmaxRmult: + (p, q, r : R) + (Rle R0 r) -> (Rmax (Rmult r p) (Rmult r q)) == (Rmult r (Rmax p q)). +Intros p q r H; Unfold Rmax. +Case (total_order_Rle p q); Case (total_order_Rle (Rmult r p) (Rmult r q)); + Auto; Intros H1 H2; Auto. +Case H; Intros E1. +Case H1; Auto with real. +Rewrite <- E1; Repeat Rewrite Rmult_Ol; Auto. +Case H; Intros E1. +Case H2; Auto with real. +Apply Rle_monotony_contra with z := r; Auto. +Rewrite <- E1; Repeat Rewrite Rmult_Ol; Auto. +Save. + (*******************************) (* Rabsolu *) (*******************************) @@ -127,6 +156,12 @@ Assumption. Trivial. Save. +Lemma Rabsolu_left1: (a : R) (Rle a R0) -> (Rabsolu a) == (Ropp a). +Intros a H; Case H; Intros H1. +Apply Rabsolu_left; Auto. +Rewrite H1; Simpl; Rewrite Rabsolu_right; Auto with real. +Save. + (*********) Lemma Rabsolu_pos:(x:R)(Rle R0 (Rabsolu x)). Intros;Unfold Rabsolu;Case (case_Rabsolu x);Intro. @@ -262,7 +297,6 @@ Intro;Generalize (Rle_not R1 R0 Rlt_R0_R1);Intro; Ring. Save. - (*********) Lemma Rabsolu_triang:(a,b:R)(Rle (Rabsolu (Rplus a b)) (Rplus (Rabsolu a) (Rabsolu b))). @@ -366,3 +400,36 @@ Fold (Rgt a x) in H;Generalize (Rgt_ge_trans a x R0 H r);Intro; Assumption. Save. +Lemma RmaxAbs: + (p, q, r : R) + (Rle p q) -> (Rle q r) -> (Rle (Rabsolu q) (Rmax (Rabsolu p) (Rabsolu r))). +Intros p q r H' H'0; Case (Rle_or_lt R0 p); Intros H'1. +Repeat Rewrite Rabsolu_right; Auto with real. +Apply Rle_trans with r; Auto with real. +Apply RmaxLess2; Auto. +Apply Rge_trans with p; Auto with real; Apply Rge_trans with q; Auto with real. +Apply Rge_trans with p; Auto with real. +Rewrite (Rabsolu_left p); Auto. +Case (Rle_or_lt R0 q); Intros H'2. +Repeat Rewrite Rabsolu_right; Auto with real. +Apply Rle_trans with r; Auto. +Apply RmaxLess2; Auto. +Apply Rge_trans with q; Auto with real. +Rewrite (Rabsolu_left q); Auto. +Case (Rle_or_lt R0 r); Intros H'3. +Repeat Rewrite Rabsolu_right; Auto with real. +Apply Rle_trans with (Ropp p); Auto with real. +Apply RmaxLess1; Auto. +Rewrite (Rabsolu_left r); Auto. +Apply Rle_trans with (Ropp p); Auto with real. +Apply RmaxLess1; Auto. +Save. + +Lemma Rabsolu_Zabs: (z : Z) (Rabsolu (IZR z)) == (IZR (Zabs z)). +Intros z; Case z; Simpl; Auto with real. +Apply Rabsolu_right; Auto with real. +Intros p0; Apply Rabsolu_right; Auto with real zarith. +Intros p0; Rewrite Rabsolu_Ropp. +Apply Rabsolu_right; Auto with real zarith. +Save. + diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 857969b74..3885ce173 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -9,6 +9,7 @@ (*i $Id$ i*) (*i Some properties about pow and sum have been made with John Harrison i*) +(*i Some Lemmas (about pow and powerRZ) have been done by Laurent Thery i*) (*********************************************************) (* Definition of the some functions *) (* *) @@ -16,6 +17,7 @@ Require Export Rlimit. Require Omega. +Require Import Zpower. (*******************************) (* Factorial *) @@ -70,6 +72,81 @@ Fixpoint pow [r:R;n:nat]:R:= |(S n) => (Rmult r (pow r n)) end. +Theorem pow_O: (e : R) (pow e O) == R1. +Simpl; Auto with real. +Qed. + +Theorem pow_1: (e : R) (pow e (1)) == e. +Simpl; Auto with real. +Qed. + +Theorem pow_add: + (e : R) (n, m : nat) (pow e (plus n m)) == (Rmult (pow e n) (pow e m)). +Intros e n; Elim n; Simpl; Auto with real. +Intros n0 H' m; Rewrite H'; Auto with real. +Qed. + +Lemma pow_nonzero: + (x:R) (n:nat) ~(x==R0) -> ~((pow x n)==R0). +Intro; Induction n; Simpl. +Intro; Red;Intro;Apply R1_neq_R0;Assumption. +Intros;Red; Intro;Elim (without_div_Od x (pow x n0) H1). +Intro; Auto. +Apply H;Assumption. +Save. + +Hints Resolve pow_O pow_1 pow_add pow_nonzero:real. + +Theorem pow_RN_plus: + (e : R) + (n, m : nat) + ~ e == R0 -> (pow e n) == (Rmult (pow e (plus n m)) (Rinv (pow e m))). +Intros e n; Elim n; Simpl; Auto with real. +Intros n0 H' m H'0. +Rewrite Rmult_assoc; Rewrite <- H'; Auto. +Qed. + +Theorem pow_lt: (e : R) (n : nat) (Rlt R0 e) -> (Rlt R0 (pow e n)). +Intros e n; Elim n; Simpl; Auto with real. +Intros n0 H' H'0; Replace R0 with (Rmult e R0); Auto with real. +Qed. +Hints Resolve pow_lt :real. + +Theorem Rlt_pow_R1: + (e : R) (n : nat) (Rlt R1 e) -> (lt O n) -> (Rlt R1 (pow e n)). +Intros e n; Elim n; Simpl; Auto with real. +Intros H' H'0; ElimType False; Omega. +Intros n0; Case n0. +Simpl; Rewrite Rmult_1r; Auto. +Intros n1 H' H'0 H'1. +Replace R1 with (Rmult R1 R1); Auto with real. +Apply Rlt_trans with r2 := (Rmult e R1); Auto with real. +Apply Rlt_monotony; Auto with real. +Apply Rlt_trans with r2 := R1; Auto with real. +Apply H'; Auto with arith. +Qed. +Hints Resolve Rlt_pow_R1 :real. + +Theorem Rlt_pow: + (e : R) (n, m : nat) (Rlt R1 e) -> (lt n m) -> (Rlt (pow e n) (pow e m)). +Intros e n m H' H'0; Replace m with (plus (minus m n) n). +Rewrite pow_add. +Pattern 1 (pow e n); Replace (pow e n) with (Rmult R1 (pow e n)); + Auto with real. +Apply Rminus_lt. +Repeat Rewrite [x : R] (Rmult_sym x (pow e n)); Rewrite <- Rminus_distr. +Replace R0 with (Rmult (pow e n) R0); Auto with real. +Apply Rlt_monotony; Auto with real. +Apply pow_lt; Auto with real. +Apply Rlt_trans with r2 := R1; Auto with real. +Apply Rlt_minus; Auto with real. +Apply Rlt_pow_R1; Auto with arith. +Apply simpl_lt_plus_l with p := n; Auto with arith. +Rewrite le_plus_minus_r; Auto with arith; Rewrite <- plus_n_O; Auto. +Rewrite plus_sym; Auto with arith. +Qed. +Hints Resolve Rlt_pow :real. + (*********) Lemma tech_pow_Rmult:(x:R)(n:nat)(Rmult x (pow x n))==(pow x (S n)). Induction n; Simpl; Trivial. @@ -107,7 +184,7 @@ Intro;Rewrite H1;Pattern 1 (Rplus R1 (Rmult (INR (S n0)) e)); Simpl;Rewrite Rmult_Ol;Unfold Rle;Right;Auto. Unfold Rle;Left;Generalize Rmult_gt;Unfold Rgt;Intro; Fold (Rsqr e);Apply (H3 (INR (S n1)) (Rsqr e) - (INR_lt_0 (S n1) (lt_O_Sn n1)));Fold (Rgt e R0) in H; + (lt_INR_0 (S n1) (lt_O_Sn n1)));Fold (Rgt e R0) in H; Apply (pos_Rsqr1 e (imp_not_Req e R0 (or_intror (Rlt e R0) (Rgt e R0) H))). Rewrite (S_INR n0);Ring. @@ -213,15 +290,6 @@ Intros;Elim H;Reflexivity. Intros; Simpl;Apply Rmult_Ol. Save. -Lemma pow_nonzero: - (x:R) (n:nat) ~(x==R0) -> ~((pow x n)==R0). -Intro; Induction n; Simpl. -Intro; Red;Intro;Apply R1_neq_R0;Assumption. -Intros;Red; Intro;Elim (without_div_Od x (pow x n0) H1). -Intro; Auto. -Apply H;Assumption. -Save. - Lemma Rinv_pow: (x:R) (n:nat) ~(x==R0) -> (Rinv (pow x n))==(pow (Rinv x) n). Intros; Elim n; Simpl. @@ -286,6 +354,168 @@ Assumption. Red;Intro; Apply R1_neq_R0;Assumption. Save. +Theorem pow_R1: + (r : R) (n : nat) (pow r n) == R1 -> (Rabsolu r) == R1 \/ n = O. +Intros r n H'. +Case (Req_EM (Rabsolu r) R1); Auto; Intros H'1. +Case (not_Req ? ? H'1); Intros H'2. +Generalize H'; Case n; Auto. +Intros n0 H'0. +Cut ~ r == R0; [Intros Eq1 | Idtac]. +Cut ~ (Rabsolu r) == R0; [Intros Eq2 | Apply Rabsolu_no_R0]; Auto. +Absurd (Rlt (pow (Rabsolu (Rinv r)) O) (pow (Rabsolu (Rinv r)) (S n0))); Auto. +Replace (pow (Rabsolu (Rinv r)) (S n0)) with R1. +Simpl; Apply Rlt_antirefl; Auto. +Rewrite Rabsolu_Rinv; Auto. +Rewrite <- Rinv_pow; Auto. +Rewrite Power_Rabsolu; Auto. +Rewrite H'0; Rewrite Rabsolu_right; Auto with real. +Apply Rle_ge; Auto with real. +Apply Rlt_pow; Auto with arith. +Rewrite Rabsolu_Rinv; Auto. +Apply Rlt_monotony_contra with z := (Rabsolu r). +Case (Rabsolu_pos r); Auto. +Intros H'3; Case Eq2; Auto. +Rewrite Rmult_1r; Rewrite Rinv_r; Auto with real. +Red;Intro;Absurd ``(pow r (S n0)) == 1``;Auto. +Simpl; Rewrite H; Rewrite Rmult_Ol; Auto with real. +Generalize H'; Case n; Auto. +Intros n0 H'0. +Cut ~ r == R0; [Intros Eq1 | Auto with real]. +Cut ~ (Rabsolu r) == R0; [Intros Eq2 | Apply Rabsolu_no_R0]; Auto. +Absurd (Rlt (pow (Rabsolu r) O) (pow (Rabsolu r) (S n0))); + Auto with real arith. +Repeat Rewrite Power_Rabsolu; Rewrite H'0; Simpl; Auto with real. +Red;Intro;Absurd ``(pow r (S n0)) == 1``;Auto. +Simpl; Rewrite H; Rewrite Rmult_Ol; Auto with real. +Qed. + +(*******************************) +(* PowerRZ *) +(*******************************) +(*i Due to L.Thery i*) + +Tactic Definition CaseEqk name := +Generalize (refl_equal ? name); Pattern -1 name; Case name. + +Definition powerRZ := + [e : R] [n : Z] Cases n of + ZERO => R1 + | (POS p) => (pow e (convert p)) + | (NEG p) => (Rinv (pow e (convert p))) + end. + +Theorem Zpower_NR0: + (e : Z) (n : nat) (Zle ZERO e) -> (Zle ZERO (Zpower_nat e n)). +Intros e n; Elim n; Unfold Zpower_nat; Simpl; Auto with zarith. +Qed. + +Theorem powerRZ_O: (e : R) (powerRZ e ZERO) == R1. +Simpl; Auto. +Qed. + +Theorem powerRZ_1: (e : R) (powerRZ e (Zs ZERO)) == e. +Simpl; Auto with real. +Qed. + +Theorem powerRZ_NOR: (e : R) (z : Z) ~ e == R0 -> ~ (powerRZ e z) == R0. +Intros e z; Case z; Simpl; Auto with real. +Qed. +Hints Resolve powerRZ_O powerRZ_1 powerRZ_NOR :real. + +Theorem powerRZ_add: + (e : R) + (n, m : Z) + ~ e == R0 -> (powerRZ e (Zplus n m)) == (Rmult (powerRZ e n) (powerRZ e m)). +Intros e n m; Case n; Case m; Simpl; Auto with real. +Intros n1 m1; Rewrite convert_add; Auto with real. +Intros n1 m1; (CaseEqk '(compare m1 n1 EGAL)); Simpl; Auto with real. +Intros H' H'0; Rewrite compare_convert_EGAL with 1 := H'; Auto with real. +Intros H' H'0; Rewrite (true_sub_convert n1 m1); Auto with real. +Rewrite (pow_RN_plus e (minus (convert n1) (convert m1)) (convert m1)); + Auto with real. +Rewrite plus_sym; Rewrite le_plus_minus_r; Auto with real. +Rewrite Rinv_Rmult; Auto with real. +Rewrite Rinv_Rinv; Auto with real. +Apply lt_le_weak. +Apply compare_convert_INFERIEUR; Auto. +Apply ZC2; Auto. +Intros H' H'0; Rewrite (true_sub_convert m1 n1); Auto with real. +Rewrite (pow_RN_plus e (minus (convert m1) (convert n1)) (convert n1)); + Auto with real. +Rewrite plus_sym; Rewrite le_plus_minus_r; Auto with real. +Apply lt_le_weak. +Change (gt (convert m1) (convert n1)). +Apply compare_convert_SUPERIEUR; Auto. +Intros n1 m1; (CaseEqk '(compare m1 n1 EGAL)); Simpl; Auto with real. +Intros H' H'0; Rewrite compare_convert_EGAL with 1 := H'; Auto with real. +Intros H' H'0; Rewrite (true_sub_convert n1 m1); Auto with real. +Rewrite (pow_RN_plus e (minus (convert n1) (convert m1)) (convert m1)); + Auto with real. +Rewrite plus_sym; Rewrite le_plus_minus_r; Auto with real. +Apply lt_le_weak. +Apply compare_convert_INFERIEUR; Auto. +Apply ZC2; Auto. +Intros H' H'0; Rewrite (true_sub_convert m1 n1); Auto with real. +Rewrite (pow_RN_plus e (minus (convert m1) (convert n1)) (convert n1)); + Auto with real. +Rewrite plus_sym; Rewrite le_plus_minus_r; Auto with real. +Rewrite Rinv_Rmult; Auto with real. +Apply lt_le_weak. +Change (gt (convert m1) (convert n1)). +Apply compare_convert_SUPERIEUR; Auto. +Intros n1 m1; Rewrite convert_add; Auto with real. +Intros H'; Rewrite pow_add; Auto with real. +Apply Rinv_Rmult; Auto. +Apply pow_nonzero; Auto. +Apply pow_nonzero; Auto. +Qed. +Hints Resolve powerRZ_O powerRZ_1 powerRZ_NOR powerRZ_add :real. + +Theorem Zpower_nat_powerRZ: + (n, m : nat) + (IZR (Zpower_nat (inject_nat n) m)) == (powerRZ (INR n) (inject_nat m)). +Intros n m; Elim m; Simpl; Auto with real. +Intros m1 H'; Rewrite bij1; Simpl. +Replace (Zpower_nat (inject_nat n) (S m1)) + with (Zmult (inject_nat n) (Zpower_nat (inject_nat n) m1)). +Rewrite mult_IZR; Auto with real. +Repeat Rewrite <- INR_IZR_INZ; Simpl. +Rewrite H'; Simpl. +Case m1; Simpl; Auto with real. +Intros m2; Rewrite bij1; Auto. +Unfold Zpower_nat; Auto. +Qed. + +Theorem powerRZ_lt: (e : R) (z : Z) (Rlt R0 e) -> (Rlt R0 (powerRZ e z)). +Intros e z; Case z; Simpl; Auto with real. +Qed. +Hints Resolve powerRZ_lt :real. + +Theorem powerRZ_le: (e : R) (z : Z) (Rlt R0 e) -> (Rle R0 (powerRZ e z)). +Intros e z H'; Apply Rlt_le; Auto with real. +Qed. +Hints Resolve powerRZ_le :real. + +Theorem Zpower_nat_powerRZ_absolu: + (n, m : Z) + (Zle ZERO m) -> (IZR (Zpower_nat n (absolu m))) == (powerRZ (IZR n) m). +Intros n m; Case m; Simpl; Auto with zarith. +Intros p H'; Elim (convert p); Simpl; Auto with zarith. +Intros n0 H'0; Rewrite <- H'0; Simpl; Auto with zarith. +Rewrite <- mult_IZR; Auto. +Intros p H'; Absurd `0 <= (NEG p)`;Auto with zarith. +Qed. + +Theorem powerRZ_R1: (n : Z) (powerRZ R1 n) == R1. +Intros n; Case n; Simpl; Auto. +Intros p; Elim (convert p); Simpl; Auto; Intros n0 H'; Rewrite H'; Ring. +Intros p; Elim (convert p); Simpl. +Exact Rinv_R1. +Intros n1 H'; Rewrite Rinv_Rmult; Try Rewrite Rinv_R1; Try Rewrite H'; + Auto with real. +Qed. + (*******************************) (* Sum of n first naturals *) (*******************************) diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v index 1d59a71e3..2bc5063eb 100644 --- a/theories/Reals/Rtrigo_fun.v +++ b/theories/Reals/Rtrigo_fun.v @@ -31,7 +31,7 @@ Split with O;Intros;Rewrite (simpl_fact n);Unfold R_dist; Intro; Rewrite (Rabsolu_pos_eq (Rinv (INR (S n)))). Cut (Rlt (Rminus (Rinv eps) R1) R0). Intro;Generalize (Rlt_le_trans (Rminus (Rinv eps) R1) R0 (INR n) H2 - (INR_le n));Clear H2;Intro; + (pos_INR n));Clear H2;Intro; Unfold Rminus in H2;Generalize (Rlt_compatibility R1 (Rplus (Rinv eps) (Ropp R1)) (INR n) H2); Replace (Rplus R1 (Rplus (Rinv eps) (Ropp R1))) with (Rinv eps); @@ -54,7 +54,7 @@ Apply Rlt_minus;Unfold Rgt in a;Rewrite <- Rinv_R1; Apply (Rinv_lt R1 eps);Auto; Rewrite (let (H1,H2)=(Rmult_ne eps) in H2);Unfold Rgt in H;Assumption. Unfold Rgt in H1;Apply Rlt_le;Assumption. -Unfold Rgt;Apply Rlt_Rinv; Apply INR_lt_0;Apply lt_O_Sn. +Unfold Rgt;Apply Rlt_Rinv; Apply lt_INR_0;Apply lt_O_Sn. (**) Cut `0<=(up (Rminus (Rinv eps) R1))`. Intro;Elim (IZN (up (Rminus (Rinv eps) R1)) H0);Intros; @@ -65,7 +65,7 @@ Intro;Elim (IZN (up (Rminus (Rinv eps) R1)) H0);Intros; Intro; Rewrite (Rabsolu_pos_eq (Rinv (INR (S n)))). Cut (Rlt (Rminus (Rinv eps) R1) (INR x)). Intro;Generalize (Rlt_le_trans (Rminus (Rinv eps) R1) (INR x) (INR n) - H4 (INR_le_nm x n ([n,m:nat; H:(ge m n)]H x n H2))); + H4 (le_INR x n ([n,m:nat; H:(ge m n)]H x n H2))); Clear H4;Intro;Unfold Rminus in H4;Generalize (Rlt_compatibility R1 (Rplus (Rinv eps) (Ropp R1)) (INR n) H4); Replace (Rplus R1 (Rplus (Rinv eps) (Ropp R1))) with (Rinv eps); @@ -89,7 +89,7 @@ Cut (IZR (up (Rminus (Rinv eps) R1)))==(IZR (INZ x)); Elim (archimed (Rminus (Rinv eps) R1));Intros;Clear H6; Unfold Rgt in H5;Rewrite H4 in H5;Rewrite INR_IZR_INZ;Assumption. Unfold Rgt in H1;Apply Rlt_le;Assumption. -Unfold Rgt;Apply Rlt_Rinv; Apply INR_lt_0;Apply lt_O_Sn. +Unfold Rgt;Apply Rlt_Rinv; Apply lt_INR_0;Apply lt_O_Sn. Apply (le_O_IZR (up (Rminus (Rinv eps) R1))); Apply (Rle_trans R0 (Rminus (Rinv eps) R1) (IZR (up (Rminus (Rinv eps) R1)))). -- cgit v1.2.3