diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Reals/Machin.v | 36 | ||||
| -rw-r--r-- | theories/Reals/PSeries_reg.v | 29 | ||||
| -rw-r--r-- | theories/Reals/R_sqrt.v | 20 | ||||
| -rw-r--r-- | theories/Reals/Ranalysis5.v | 90 | ||||
| -rw-r--r-- | theories/Reals/Ratan.v | 238 | ||||
| -rw-r--r-- | theories/Reals/Rbasic_fun.v | 4 | ||||
| -rw-r--r-- | theories/Reals/Rderiv.v | 6 | ||||
| -rw-r--r-- | theories/Reals/Reals.v | 1 | ||||
| -rw-r--r-- | theories/Reals/Rlimit.v | 8 | ||||
| -rw-r--r-- | theories/Reals/Rpower.v | 24 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo.v | 2 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo1.v | 40 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo_calc.v | 1 |
13 files changed, 257 insertions, 242 deletions
diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v index cdf98cbde..8f7e07ac4 100644 --- a/theories/Reals/Machin.v +++ b/theories/Reals/Machin.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Fourier. +Require Import Lra. Require Import Rbase. Require Import Rtrigo1. Require Import Ranalysis_reg. @@ -67,7 +67,7 @@ assert (atan x <= PI/4). assert (atan y < PI/4). rewrite <- atan_1; apply atan_increasing. assumption. -rewrite Ropp_div; split; fourier. +rewrite Ropp_div; split; lra. Qed. (* A simple formula, reasonably efficient. *) @@ -77,8 +77,8 @@ assert (utility : 0 < PI/2) by (apply PI2_RGT_0). rewrite <- atan_1. rewrite (atan_sub_correct 1 (/2)). apply f_equal, f_equal; unfold atan_sub; field. - apply Rgt_not_eq; fourier. - apply tech; try split; try fourier. + apply Rgt_not_eq; lra. + apply tech; try split; try lra. apply atan_bound. Qed. @@ -86,7 +86,7 @@ Lemma Machin_4_5_239 : PI/4 = 4 * atan (/5) - atan(/239). Proof. rewrite <- atan_1. rewrite (atan_sub_correct 1 (/5)); - [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [ | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. replace (4 * atan (/5) - atan (/239)) with (atan (/5) + (atan (/5) + (atan (/5) + (atan (/5) + - @@ -95,17 +95,17 @@ apply f_equal. replace (atan_sub 1 (/5)) with (2/3) by (unfold atan_sub; field). rewrite (atan_sub_correct (2/3) (/5)); - [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. replace (atan_sub (2/3) (/5)) with (7/17) by (unfold atan_sub; field). rewrite (atan_sub_correct (7/17) (/5)); - [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. replace (atan_sub (7/17) (/5)) with (9/46) by (unfold atan_sub; field). rewrite (atan_sub_correct (9/46) (/5)); - [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. rewrite <- atan_opp; apply f_equal. unfold atan_sub; field. @@ -115,7 +115,7 @@ Lemma Machin_2_3_7 : PI/4 = 2 * atan(/3) + (atan (/7)). Proof. rewrite <- atan_1. rewrite (atan_sub_correct 1 (/3)); - [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [ | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. replace (2 * atan (/3) + atan (/7)) with (atan (/3) + (atan (/3) + atan (/7))) by ring. @@ -123,7 +123,7 @@ apply f_equal. replace (atan_sub 1 (/3)) with (/2) by (unfold atan_sub; field). rewrite (atan_sub_correct (/2) (/3)); - [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. apply f_equal; unfold atan_sub; field. Qed. @@ -138,19 +138,19 @@ Lemma PI_2_3_7_ineq : sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <= PI / 4 <= sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N). Proof. -assert (dec3 : 0 <= /3 <= 1) by (split; fourier). -assert (dec7 : 0 <= /7 <= 1) by (split; fourier). +assert (dec3 : 0 <= /3 <= 1) by (split; lra). +assert (dec7 : 0 <= /7 <= 1) by (split; lra). assert (decr : Un_decreasing PI_2_3_7_tg). apply Ratan_seq_decreasing in dec3. apply Ratan_seq_decreasing in dec7. intros n; apply Rplus_le_compat. - apply Rmult_le_compat_l; [ fourier | exact (dec3 n)]. + apply Rmult_le_compat_l; [ lra | exact (dec3 n)]. exact (dec7 n). assert (cv : Un_cv PI_2_3_7_tg 0). apply Ratan_seq_converging in dec3. apply Ratan_seq_converging in dec7. intros eps ep. - assert (ep' : 0 < eps /3) by fourier. + assert (ep' : 0 < eps /3) by lra. destruct (dec3 _ ep') as [N1 Pn1]; destruct (dec7 _ ep') as [N2 Pn2]. exists (N1 + N2)%nat; intros n Nn. unfold PI_2_3_7_tg. @@ -161,14 +161,14 @@ assert (cv : Un_cv PI_2_3_7_tg 0). apply Rplus_lt_compat. unfold R_dist, Rminus, Rdiv. rewrite <- (Rmult_0_r 2), <- Ropp_mult_distr_r_reverse. - rewrite <- Rmult_plus_distr_l, Rabs_mult, (Rabs_pos_eq 2);[|fourier]. - rewrite Rmult_assoc; apply Rmult_lt_compat_l;[fourier | ]. + rewrite <- Rmult_plus_distr_l, Rabs_mult, (Rabs_pos_eq 2);[|lra]. + rewrite Rmult_assoc; apply Rmult_lt_compat_l;[lra | ]. apply (Pn1 n); omega. apply (Pn2 n); omega. rewrite Machin_2_3_7. -rewrite !atan_eq_ps_atan; try (split; fourier). +rewrite !atan_eq_ps_atan; try (split; lra). unfold ps_atan; destruct (in_int (/3)); destruct (in_int (/7)); - try match goal with id : ~ _ |- _ => case id; split; fourier end. + try match goal with id : ~ _ |- _ => case id; split; lra end. destruct (ps_atan_exists_1 (/3)) as [v3 Pv3]. destruct (ps_atan_exists_1 (/7)) as [v7 Pv7]. assert (main : Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg)) (2 * v3 + v7)). diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v index 61d1b5afe..146d69101 100644 --- a/theories/Reals/PSeries_reg.v +++ b/theories/Reals/PSeries_reg.v @@ -15,7 +15,7 @@ Require Import Ranalysis1. Require Import MVT. Require Import Max. Require Import Even. -Require Import Fourier. +Require Import Lra. Local Open Scope R_scope. (* Boule is French for Ball *) @@ -431,7 +431,7 @@ assert (ctrho : forall n z, Boule c d z -> continuity_pt (rho_ n) z). intros y dyz; unfold rho_; destruct (Req_EM_T y x) as [xy | xny]. rewrite xy in dyz. destruct (Rle_dec delta (Rabs (z - x))). - rewrite Rmin_left, R_dist_sym in dyz; unfold R_dist in dyz; fourier. + rewrite Rmin_left, R_dist_sym in dyz; unfold R_dist in dyz; lra. rewrite Rmin_right, R_dist_sym in dyz; unfold R_dist in dyz; [case (Rlt_irrefl _ dyz) |apply Rlt_le, Rnot_le_gt; assumption]. reflexivity. @@ -449,7 +449,7 @@ assert (ctrho : forall n z, Boule c d z -> continuity_pt (rho_ n) z). assert (CVU rho_ rho c d ). intros eps ep. assert (ep8 : 0 < eps/8). - fourier. + lra. destruct (cvu _ ep8) as [N Pn1]. assert (cauchy1 : forall n p, (N <= n)%nat -> (N <= p)%nat -> forall z, Boule c d z -> Rabs (f' n z - f' p z) < eps/4). @@ -537,7 +537,7 @@ assert (CVU rho_ rho c d ). simpl; unfold R_dist. unfold Rminus; rewrite (Rplus_comm y), Rplus_assoc, Rplus_opp_r, Rplus_0_r. rewrite Rabs_pos_eq;[ |apply Rlt_le; assumption ]. - apply Rlt_le_trans with (Rmin (Rmin d' d2) delta);[fourier | ]. + apply Rlt_le_trans with (Rmin (Rmin d' d2) delta);[lra | ]. apply Rle_trans with (Rmin d' d2); apply Rmin_l. apply Rle_trans with (1 := R_dist_tri _ _ (rho_ p (y + Rmin (Rmin d' d2) delta/2))). apply Rplus_le_compat. @@ -548,33 +548,32 @@ assert (CVU rho_ rho c d ). replace (rho_ p (y + Rmin (Rmin d' d2) delta / 2)) with ((f p (y + Rmin (Rmin d' d2) delta / 2) - f p x)/ ((y + Rmin (Rmin d' d2) delta / 2) - x)). - apply step_2; auto; try fourier. + apply step_2; auto; try lra. assert (0 < pos delta) by (apply cond_pos). apply Boule_convex with y (y + delta/2). assumption. destruct (Pdelta (y + delta/2)); auto. - rewrite xy; unfold Boule; rewrite Rabs_pos_eq; try fourier; auto. - split; try fourier. + rewrite xy; unfold Boule; rewrite Rabs_pos_eq; try lra; auto. + split; try lra. apply Rplus_le_compat_l, Rmult_le_compat_r;[ | apply Rmin_r]. now apply Rlt_le, Rinv_0_lt_compat, Rlt_0_2. - apply Rminus_not_eq_right; rewrite xy; apply Rgt_not_eq; fourier. unfold rho_. destruct (Req_EM_T (y + Rmin (Rmin d' d2) delta/2) x) as [ymx | ymnx]. - case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); fourier. + case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); lra. reflexivity. unfold rho_. destruct (Req_EM_T (y + Rmin (Rmin d' d2) delta / 2) x) as [ymx | ymnx]. - case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); fourier. + case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); lra. reflexivity. - apply Rlt_le, Pd2; split;[split;[exact I | apply Rlt_not_eq; fourier] | ]. + apply Rlt_le, Pd2; split;[split;[exact I | apply Rlt_not_eq; lra] | ]. simpl; unfold R_dist. unfold Rminus; rewrite (Rplus_comm y), Rplus_assoc, Rplus_opp_r, Rplus_0_r. - rewrite Rabs_pos_eq;[ | fourier]. - apply Rlt_le_trans with (Rmin (Rmin d' d2) delta); [fourier |]. + rewrite Rabs_pos_eq;[ | lra]. + apply Rlt_le_trans with (Rmin (Rmin d' d2) delta); [lra |]. apply Rle_trans with (Rmin d' d2). solve[apply Rmin_l]. solve[apply Rmin_r]. - apply Rlt_le, Rlt_le_trans with (eps/4);[ | fourier]. + apply Rlt_le, Rlt_le_trans with (eps/4);[ | lra]. unfold rho_; destruct (Req_EM_T y x); solve[auto]. assert (unif_ac' : forall p, (N <= p)%nat -> forall y, Boule c d y -> Rabs (rho y - rho_ p y) < eps). @@ -589,7 +588,7 @@ assert (CVU rho_ rho c d ). intros eps' ep'; simpl; exists 0%nat; intros; rewrite R_dist_eq; assumption. intros p pN y b_y. replace eps with (eps/2 + eps/2) by field. - assert (ep2 : 0 < eps/2) by fourier. + assert (ep2 : 0 < eps/2) by lra. destruct (cvrho y b_y _ ep2) as [N2 Pn2]. apply Rle_lt_trans with (1 := R_dist_tri _ _ (rho_ (max N N2) y)). apply Rplus_lt_le_compat. diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index d4035fad6..6991923b1 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -155,6 +155,22 @@ Proof. | apply (sqrt_positivity x (Rlt_le 0 x H1)) ]. Qed. +Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y. +intros x y H H0; try assumption. +replace 0 with (x * 0). +apply Rmult_lt_compat_l; auto with real. +ring. +Qed. + +Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y. +intros x y H H0; try assumption. +case H; intros. +red; left. +apply Rlt_mult_inv_pos; auto with real. +rewrite <- H1. +red; right; ring. +Qed. + Lemma sqrt_div_alt : forall x y : R, 0 < y -> sqrt (x / y) = sqrt x / sqrt y. Proof. @@ -176,14 +192,14 @@ Proof. clearbody Hx'. clear Hx. apply Rsqr_inj. apply sqrt_pos. - apply Fourier_util.Rle_mult_inv_pos. + apply Rle_mult_inv_pos. apply Rsqrt_positivity. now apply sqrt_lt_R0. rewrite Rsqr_div, 2!Rsqr_sqrt. unfold Rsqr. now rewrite Rsqrt_Rsqrt. now apply Rlt_le. - now apply Fourier_util.Rle_mult_inv_pos. + now apply Rle_mult_inv_pos. apply Rgt_not_eq. now apply sqrt_lt_R0. Qed. diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index afb78e1c8..e66130b34 100644 --- a/theories/Reals/Ranalysis5.v +++ b/theories/Reals/Ranalysis5.v @@ -12,7 +12,7 @@ Require Import Rbase. Require Import Ranalysis_reg. Require Import Rfunctions. Require Import Rseries. -Require Import Fourier. +Require Import Lra. Require Import RiemannInt. Require Import SeqProp. Require Import Max. @@ -56,7 +56,7 @@ Proof. } rewrite f_eq_g in Htemp by easy. unfold id in Htemp. - fourier. + lra. Qed. Lemma derivable_pt_id_interv : forall (lb ub x:R), @@ -99,7 +99,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs apply Req_le ; apply Rabs_right ; apply Rgt_ge ; assumption. split. assert (Sublemma : forall x y z, -z < y - x -> x < y + z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Sublemma2. rewrite Rabs_Ropp. apply Rlt_le_trans with (r2:=a-lb) ; [| apply RRle_abs] ; @@ -108,7 +108,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_r] ; apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption. assert (Sublemma : forall x y z, y < z - x -> x + y < z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Sublemma2. apply Rlt_le_trans with (r2:=ub-a) ; [| apply RRle_abs] ; @@ -137,7 +137,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs apply Req_le ; apply Rabs_right ; apply Rgt_ge ; assumption. split. assert (Sublemma : forall x y z, -z < y - x -> x < y + z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Sublemma2. rewrite Rabs_Ropp. apply Rlt_le_trans with (r2:=a-lb) ; [| apply RRle_abs] ; @@ -146,7 +146,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_r] ; apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption. assert (Sublemma : forall x y z, y < z - x -> x + y < z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Sublemma2. apply Rlt_le_trans with (r2:=ub-a) ; [| apply RRle_abs] ; @@ -415,7 +415,7 @@ Ltac case_le H := let h' := fresh in match t with ?x <= ?y => case (total_order_T x y); [intros h'; case h'; clear h' | - intros h'; clear -H h'; elimtype False; fourier ] end. + intros h'; clear -H h'; elimtype False; lra ] end. (* end hide *) @@ -539,37 +539,37 @@ intros f g lb ub lb_lt_ub f_incr_interv f_eq_g f_cont_interv b b_encad. assert (x1_encad : lb <= x1 <= ub). split. apply RmaxLess2. apply Rlt_le. rewrite Hx1. rewrite Sublemma. - split. apply Rlt_trans with (r2:=x) ; fourier. + split. apply Rlt_trans with (r2:=x) ; lra. assumption. assert (x2_encad : lb <= x2 <= ub). split. apply Rlt_le ; rewrite Hx2 ; apply Rgt_lt ; rewrite Sublemma2. - split. apply Rgt_trans with (r2:=x) ; fourier. + split. apply Rgt_trans with (r2:=x) ; lra. assumption. apply Rmin_r. assert (x_lt_x2 : x < x2). rewrite Hx2. apply Rgt_lt. rewrite Sublemma2. - split ; fourier. + split ; lra. assert (x1_lt_x : x1 < x). rewrite Hx1. rewrite Sublemma. - split ; fourier. + split ; lra. exists (Rmin (f x - f x1) (f x2 - f x)). - split. apply Rmin_pos ; apply Rgt_minus. apply f_incr_interv ; [apply RmaxLess2 | | ] ; fourier. + split. apply Rmin_pos ; apply Rgt_minus. apply f_incr_interv ; [apply RmaxLess2 | | ] ; lra. apply f_incr_interv ; intuition. intros y Temp. destruct Temp as (_,y_cond). rewrite <- f_x_b in y_cond. assert (Temp : forall x y d1 d2, d1 > 0 -> d2 > 0 -> Rabs (y - x) < Rmin d1 d2 -> x - d1 <= y <= x + d2). intros. - split. assert (H10 : forall x y z, x - y <= z -> x - z <= y). intuition. fourier. + split. assert (H10 : forall x y z, x - y <= z -> x - z <= y). intuition. lra. apply H10. apply Rle_trans with (r2:=Rabs (y0 - x0)). replace (Rabs (y0 - x0)) with (Rabs (x0 - y0)). apply RRle_abs. rewrite <- Rabs_Ropp. unfold Rminus ; rewrite Ropp_plus_distr. rewrite Ropp_involutive. intuition. apply Rle_trans with (r2:= Rmin d1 d2). apply Rlt_le ; assumption. apply Rmin_l. - assert (H10 : forall x y z, x - y <= z -> x <= y + z). intuition. fourier. + assert (H10 : forall x y z, x - y <= z -> x <= y + z). intuition. lra. apply H10. apply Rle_trans with (r2:=Rabs (y0 - x0)). apply RRle_abs. apply Rle_trans with (r2:= Rmin d1 d2). apply Rlt_le ; assumption. apply Rmin_r. @@ -602,12 +602,12 @@ intros f g lb ub lb_lt_ub f_incr_interv f_eq_g f_cont_interv b b_encad. assert (x1_neq_x' : x1 <> x'). intro Hfalse. rewrite Hfalse, f_x'_y in y_cond. assert (Hf : Rabs (y - f x) < f x - y). - apply Rlt_le_trans with (r2:=Rmin (f x - y) (f x2 - f x)). fourier. + apply Rlt_le_trans with (r2:=Rmin (f x - y) (f x2 - f x)). lra. apply Rmin_l. assert(Hfin : f x - y < f x - y). apply Rle_lt_trans with (r2:=Rabs (y - f x)). replace (Rabs (y - f x)) with (Rabs (f x - y)). apply RRle_abs. - rewrite <- Rabs_Ropp. replace (- (f x - y)) with (y - f x) by field ; reflexivity. fourier. + rewrite <- Rabs_Ropp. replace (- (f x - y)) with (y - f x) by field ; reflexivity. lra. apply (Rlt_irrefl (f x - y)) ; assumption. split ; intuition. assert (x'_lb : x - eps < x'). @@ -619,17 +619,17 @@ intros f g lb ub lb_lt_ub f_incr_interv f_eq_g f_cont_interv b b_encad. assert (x1_neq_x' : x' <> x2). intro Hfalse. rewrite <- Hfalse, f_x'_y in y_cond. assert (Hf : Rabs (y - f x) < y - f x). - apply Rlt_le_trans with (r2:=Rmin (f x - f x1) (y - f x)). fourier. + apply Rlt_le_trans with (r2:=Rmin (f x - f x1) (y - f x)). lra. apply Rmin_r. assert(Hfin : y - f x < y - f x). - apply Rle_lt_trans with (r2:=Rabs (y - f x)). apply RRle_abs. fourier. + apply Rle_lt_trans with (r2:=Rabs (y - f x)). apply RRle_abs. lra. apply (Rlt_irrefl (y - f x)) ; assumption. split ; intuition. assert (x'_ub : x' < x + eps). apply Sublemma3. split. intuition. apply Rlt_not_eq. apply Rlt_le_trans with (r2:=x2) ; [ |rewrite Hx2 ; apply Rmin_l] ; intuition. - apply Rabs_def1 ; fourier. + apply Rabs_def1 ; lra. assumption. split. apply Rle_trans with (r2:=x1) ; intuition. apply Rle_trans with (r2:=x2) ; intuition. @@ -742,7 +742,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq. assert (lb <= x + h <= ub). split. assert (Sublemma : forall x y z, -z <= y - x -> x <= y + z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Rlt_le ; apply Sublemma2. rewrite Rabs_Ropp. apply Rlt_le_trans with (r2:=x-lb) ; [| apply RRle_abs] ; @@ -751,7 +751,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq. apply Rlt_le_trans with (r2:=delta''). assumption. intuition. apply Rmin_r. apply Rgt_minus. intuition. assert (Sublemma : forall x y z, y <= z - x -> x + y <= z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Rlt_le ; apply Sublemma2. apply Rlt_le_trans with (r2:=ub-x) ; [| apply RRle_abs] ; @@ -767,7 +767,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq. assumption. split ; [|intuition]. assert (Sublemma : forall x y z, - z <= y - x -> x <= y + z). - intros ; fourier. + intros ; lra. apply Sublemma ; apply Rlt_le ; apply Sublemma2. rewrite Rabs_Ropp. apply Rlt_le_trans with (r2:=x-lb) ; [| apply RRle_abs] ; apply Rlt_le_trans with (r2:=Rmin (x - lb) (ub - x)) ; [| apply Rmin_l] ; @@ -1031,7 +1031,7 @@ Lemma derivable_pt_lim_CVU : forall (fn fn':nat -> R -> R) (f g:R->R) derivable_pt_lim f x (g x). Proof. intros fn fn' f g x c' r xinb Dfn_eq_fn' fn_CV_f fn'_CVU_g g_cont eps eps_pos. -assert (eps_8_pos : 0 < eps / 8) by fourier. +assert (eps_8_pos : 0 < eps / 8) by lra. elim (g_cont x xinb _ eps_8_pos) ; clear g_cont ; intros delta1 (delta1_pos, g_cont). destruct (Ball_in_inter _ _ _ _ _ xinb @@ -1041,11 +1041,11 @@ exists delta; intros h hpos hinbdelta. assert (eps'_pos : 0 < (Rabs h) * eps / 4). unfold Rdiv ; rewrite Rmult_assoc ; apply Rmult_lt_0_compat. apply Rabs_pos_lt ; assumption. -fourier. +lra. destruct (fn_CV_f x xinb ((Rabs h) * eps / 4) eps'_pos) as [N2 fnx_CV_fx]. assert (xhinbxdelta : Boule x delta (x + h)). clear -hinbdelta; apply Rabs_def2 in hinbdelta; unfold Boule; simpl. - destruct hinbdelta; apply Rabs_def1; fourier. + destruct hinbdelta; apply Rabs_def1; lra. assert (t : Boule c' r (x + h)). apply Pdelta in xhinbxdelta; tauto. destruct (fn_CV_f (x+h) t ((Rabs h) * eps / 4) eps'_pos) as [N1 fnxh_CV_fxh]. @@ -1064,17 +1064,17 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn exists (fn' N c) ; apply Dfn_eq_fn'. assert (t : Boule x delta c). apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta; destruct c_encad. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (pr2 : forall c : R, x + h < c < x -> derivable_pt id c). solve[intros; apply derivable_id]. - assert (xh_x : x+h < x) by fourier. + assert (xh_x : x+h < x) by lra. assert (pr3 : forall c : R, x + h <= c <= x -> continuity_pt (fn N) c). intros c c_encad ; apply derivable_continuous_pt. exists (fn' N c) ; apply Dfn_eq_fn' ; intuition. assert (t : Boule x delta c). apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (pr4 : forall c : R, x + h <= c <= x -> continuity_pt id c). solve[intros; apply derivable_continuous ; apply derivable_id]. @@ -1117,7 +1117,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn assert (t : Boule x delta c). destruct P. apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * (eps / 8) + Rabs h * (eps / 8)). @@ -1131,27 +1131,27 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn apply Rlt_trans with (Rabs h). apply Rabs_def1. apply Rlt_trans with 0. - destruct P; fourier. + destruct P; lra. apply Rabs_pos_lt ; assumption. - rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_involutive;[ | fourier]. - destruct P; fourier. + rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_involutive;[ | lra]. + destruct P; lra. clear -Pdelta xhinbxdelta. apply Pdelta in xhinbxdelta; destruct xhinbxdelta as [_ P']. apply Rabs_def2 in P'; simpl in P'; destruct P'; - apply Rabs_def1; fourier. + apply Rabs_def1; lra. rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite <- Rmult_plus_distr_l. replace (Rabs h * eps / 4 + (Rabs h * eps / 4 + Rabs h * (eps / 8 + eps / 8))) with (Rabs h * (eps / 4 + eps / 4 + eps / 8 + eps / 8)) by field. apply Rmult_lt_compat_l. apply Rabs_pos_lt ; assumption. - fourier. + lra. assert (H := pr1 c P) ; elim H ; clear H ; intros l Hl. assert (Temp : l = fn' N c). assert (bc'rc : Boule c' r c). assert (t : Boule x delta c). clear - xhinbxdelta P. destruct P; apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def1; fourier. + apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (Hl' := Dfn_eq_fn' c N bc'rc). unfold derivable_pt_abs in Hl; clear -Hl Hl'. @@ -1175,17 +1175,17 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn exists (fn' N c) ; apply Dfn_eq_fn'. assert (t : Boule x delta c). apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta; destruct c_encad. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (pr2 : forall c : R, x < c < x + h -> derivable_pt id c). solve[intros; apply derivable_id]. - assert (xh_x : x < x + h) by fourier. + assert (xh_x : x < x + h) by lra. assert (pr3 : forall c : R, x <= c <= x + h -> continuity_pt (fn N) c). intros c c_encad ; apply derivable_continuous_pt. exists (fn' N c) ; apply Dfn_eq_fn' ; intuition. assert (t : Boule x delta c). apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (pr4 : forall c : R, x <= c <= x + h -> continuity_pt id c). solve[intros; apply derivable_continuous ; apply derivable_id]. @@ -1223,7 +1223,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn assert (t : Boule x delta c). destruct P. apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * (eps / 8) + Rabs h * (eps / 8)). @@ -1236,27 +1236,27 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn apply Rlt_not_eq ; exact (proj1 P). apply Rlt_trans with (Rabs h). apply Rabs_def1. - destruct P; rewrite Rabs_pos_eq;fourier. + destruct P; rewrite Rabs_pos_eq;lra. apply Rle_lt_trans with 0. - assert (t := Rabs_pos h); clear -t; fourier. - clear -P; destruct P; fourier. + assert (t := Rabs_pos h); clear -t; lra. + clear -P; destruct P; lra. clear -Pdelta xhinbxdelta. apply Pdelta in xhinbxdelta; destruct xhinbxdelta as [_ P']. apply Rabs_def2 in P'; simpl in P'; destruct P'; - apply Rabs_def1; fourier. + apply Rabs_def1; lra. rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite <- Rmult_plus_distr_l. replace (Rabs h * eps / 4 + (Rabs h * eps / 4 + Rabs h * (eps / 8 + eps / 8))) with (Rabs h * (eps / 4 + eps / 4 + eps / 8 + eps / 8)) by field. apply Rmult_lt_compat_l. apply Rabs_pos_lt ; assumption. - fourier. + lra. assert (H := pr1 c P) ; elim H ; clear H ; intros l Hl. assert (Temp : l = fn' N c). assert (bc'rc : Boule c' r c). assert (t : Boule x delta c). clear - xhinbxdelta P. destruct P; apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def1; fourier. + apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (Hl' := Dfn_eq_fn' c N bc'rc). unfold derivable_pt_abs in Hl; clear -Hl Hl'. diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v index ce39d5ffe..03e6ff61a 100644 --- a/theories/Reals/Ratan.v +++ b/theories/Reals/Ratan.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Fourier. +Require Import Lra. Require Import Rbase. Require Import PSeries_reg. Require Import Rtrigo1. @@ -32,7 +32,7 @@ intros x y; unfold Rdiv; rewrite <-Ropp_mult_distr_l_reverse; reflexivity. Qed. Definition pos_half_prf : 0 < /2. -Proof. fourier. Qed. +Proof. lra. Qed. Definition pos_half := mkposreal (/2) pos_half_prf. @@ -40,15 +40,15 @@ Lemma Boule_half_to_interval : forall x , Boule (/2) pos_half x -> 0 <= x <= 1. Proof. unfold Boule, pos_half; simpl. -intros x b; apply Rabs_def2 in b; destruct b; split; fourier. +intros x b; apply Rabs_def2 in b; destruct b; split; lra. Qed. Lemma Boule_lt : forall c r x, Boule c r x -> Rabs x < Rabs c + r. Proof. unfold Boule; intros c r x h. apply Rabs_def2 in h; destruct h; apply Rabs_def1; - (destruct (Rle_lt_dec 0 c);[rewrite Rabs_pos_eq; fourier | - rewrite <- Rabs_Ropp, Rabs_pos_eq; fourier]). + (destruct (Rle_lt_dec 0 c);[rewrite Rabs_pos_eq; lra | + rewrite <- Rabs_Ropp, Rabs_pos_eq; lra]). Qed. (* The following lemma does not belong here. *) @@ -117,53 +117,53 @@ intros [ | N] Npos n decr to0 cv nN. case (even_odd_cor n) as [p' [neven | nodd]]. rewrite neven. destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. - unfold R_dist; rewrite Rabs_pos_eq;[ | fourier]. + unfold R_dist; rewrite Rabs_pos_eq;[ | lra]. assert (dist : (p <= p')%nat) by omega. assert (t := decreasing_prop _ _ _ (CV_ALT_step1 f decr) dist). apply Rle_trans with (sum_f_R0 (tg_alt f) (2 * p) - l). unfold Rminus; apply Rplus_le_compat_r; exact t. match goal with _ : ?a <= l, _ : l <= ?b |- _ => replace (f (S (2 * p))) with (b - a) by - (rewrite tech5; unfold tg_alt; rewrite pow_1_odd; ring); fourier + (rewrite tech5; unfold tg_alt; rewrite pow_1_odd; ring); lra end. rewrite nodd; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. unfold R_dist; rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_minus_distr; - [ | fourier]. + [ | lra]. assert (dist : (p <= p')%nat) by omega. apply Rle_trans with (l - sum_f_R0 (tg_alt f) (S (2 * p))). unfold Rminus; apply Rplus_le_compat_l, Ropp_le_contravar. solve[apply Rge_le, (growing_prop _ _ _ (CV_ALT_step0 f decr) dist)]. unfold Rminus; rewrite tech5, Ropp_plus_distr, <- Rplus_assoc. - unfold tg_alt at 2; rewrite pow_1_odd; fourier. + unfold tg_alt at 2; rewrite pow_1_odd; lra. rewrite Nodd; destruct (alternated_series_ineq _ _ p decr to0 cv) as [B _]. destruct (alternated_series_ineq _ _ (S p) decr to0 cv) as [_ C]. assert (keep : (2 * S p = S (S ( 2 * p)))%nat) by ring. case (even_odd_cor n) as [p' [neven | nodd]]. rewrite neven; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. - unfold R_dist; rewrite Rabs_pos_eq;[ | fourier]. + unfold R_dist; rewrite Rabs_pos_eq;[ | lra]. assert (dist : (S p < S p')%nat) by omega. apply Rle_trans with (sum_f_R0 (tg_alt f) (2 * S p) - l). unfold Rminus; apply Rplus_le_compat_r, (decreasing_prop _ _ _ (CV_ALT_step1 f decr)). omega. rewrite keep, tech5; unfold tg_alt at 2; rewrite <- keep, pow_1_even. - fourier. + lra. rewrite nodd; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. - unfold R_dist; rewrite <- Rabs_Ropp, Rabs_pos_eq;[ | fourier]. + unfold R_dist; rewrite <- Rabs_Ropp, Rabs_pos_eq;[ | lra]. rewrite Ropp_minus_distr. apply Rle_trans with (l - sum_f_R0 (tg_alt f) (S (2 * p))). unfold Rminus; apply Rplus_le_compat_l, Ropp_le_contravar, Rge_le, (growing_prop _ _ _ (CV_ALT_step0 f decr)); omega. generalize C; rewrite keep, tech5; unfold tg_alt. rewrite <- keep, pow_1_even. - assert (t : forall a b c, a <= b + 1 * c -> a - b <= c) by (intros; fourier). + assert (t : forall a b c, a <= b + 1 * c -> a - b <= c) by (intros; lra). solve[apply t]. clear WLOG; intros Hyp [ | n] decr to0 cv _. generalize (alternated_series_ineq f l 0 decr to0 cv). unfold R_dist, tg_alt; simpl; rewrite !Rmult_1_l, !Rmult_1_r. assert (f 1%nat <= f 0%nat) by apply decr. - intros [A B]; rewrite Rabs_pos_eq; fourier. + intros [A B]; rewrite Rabs_pos_eq; lra. apply Rle_trans with (f 1%nat). apply (Hyp 1%nat (le_n 1) (S n) decr to0 cv). omega. @@ -180,7 +180,7 @@ Lemma Alt_CVU : forall (f : nat -> R -> R) g h c r, CVU (fun N x => sum_f_R0 (tg_alt (fun i => f i x)) N) g c r. Proof. intros f g h c r decr to0 to_g bound bound0 eps ep. -assert (ep' : 0 <eps/2) by fourier. +assert (ep' : 0 <eps/2) by lra. destruct (bound0 _ ep) as [N Pn]; exists N. intros n y nN dy. rewrite <- Rabs_Ropp, Ropp_minus_distr; apply Rle_lt_trans with (f n y). @@ -201,14 +201,14 @@ intros x; destruct (Rle_lt_dec 0 x). replace (x ^ 2) with (x * x) by field. apply Rmult_le_pos; assumption. replace (x ^ 2) with ((-x) * (-x)) by field. -apply Rmult_le_pos; fourier. +apply Rmult_le_pos; lra. Qed. Lemma pow2_abs : forall x, Rabs x ^ 2 = x ^ 2. Proof. intros x; destruct (Rle_lt_dec 0 x). rewrite Rabs_pos_eq;[field | assumption]. -rewrite <- Rabs_Ropp, Rabs_pos_eq;[field | fourier]. +rewrite <- Rabs_Ropp, Rabs_pos_eq;[field | lra]. Qed. (** * Properties of tangent *) @@ -307,18 +307,18 @@ destruct (MVT_cor1 cos (PI/2) x derivable_cos xgtpi2) as [c [Pc [cint1 cint2]]]. revert Pc; rewrite cos_PI2, Rminus_0_r. rewrite <- (pr_nu cos c (derivable_pt_cos c)), derive_pt_cos. -assert (0 < c < 2) by (split; assert (t := PI2_RGT_0); fourier). +assert (0 < c < 2) by (split; assert (t := PI2_RGT_0); lra). assert (0 < sin c) by now apply sin_pos_tech. intros Pc. case (Rlt_not_le _ _ cx). rewrite <- (Rplus_0_l (cos x)), Pc, Ropp_mult_distr_l_reverse. -apply Rle_minus, Rmult_le_pos;[apply Rlt_le; assumption | fourier ]. +apply Rle_minus, Rmult_le_pos;[apply Rlt_le; assumption | lra ]. Qed. Lemma PI2_3_2 : 3/2 < PI/2. Proof. -apply PI2_lower_bound;[split; fourier | ]. -destruct (pre_cos_bound (3/2) 1) as [t _]; [fourier | fourier | ]. +apply PI2_lower_bound;[split; lra | ]. +destruct (pre_cos_bound (3/2) 1) as [t _]; [lra | lra | ]. apply Rlt_le_trans with (2 := t); clear t. unfold cos_approx; simpl; unfold cos_term. rewrite !INR_IZR_INZ. @@ -330,7 +330,7 @@ apply Rdiv_lt_0_compat ; now apply IZR_lt. Qed. Lemma PI2_1 : 1 < PI/2. -Proof. assert (t := PI2_3_2); fourier. Qed. +Proof. assert (t := PI2_3_2); lra. Qed. Lemma tan_increasing : forall x y:R, @@ -347,7 +347,7 @@ intros x y Z_le_x x_lt_y y_le_1. derivable_pt tan x). intros ; apply derivable_pt_tan ; intuition. apply derive_increasing_interv with (a:=-PI/2) (b:=PI/2) (pr:=local_derivable_pt_tan) ; intuition. - fourier. + lra. assert (Temp := pr_nu tan t (derivable_pt_tan t t_encad) (local_derivable_pt_tan t t_encad)) ; rewrite <- Temp ; clear Temp. assert (Temp := derive_pt_tan t t_encad) ; rewrite Temp ; clear Temp. @@ -414,49 +414,49 @@ Qed. (** * Definition of arctangent as the reciprocal function of tangent and proof of this status *) Lemma tan_1_gt_1 : tan 1 > 1. Proof. -assert (0 < cos 1) by (apply cos_gt_0; assert (t:=PI2_1); fourier). +assert (0 < cos 1) by (apply cos_gt_0; assert (t:=PI2_1); lra). assert (t1 : cos 1 <= 1 - 1/2 + 1/24). - destruct (pre_cos_bound 1 0) as [_ t]; try fourier; revert t. + destruct (pre_cos_bound 1 0) as [_ t]; try lra; revert t. unfold cos_approx, cos_term; simpl; intros t; apply Rle_trans with (1:=t). clear t; apply Req_le; field. assert (t2 : 1 - 1/6 <= sin 1). - destruct (pre_sin_bound 1 0) as [t _]; try fourier; revert t. + destruct (pre_sin_bound 1 0) as [t _]; try lra; revert t. unfold sin_approx, sin_term; simpl; intros t; apply Rle_trans with (2:=t). clear t; apply Req_le; field. pattern 1 at 2; replace 1 with - (cos 1 / cos 1) by (field; apply Rgt_not_eq; fourier). + (cos 1 / cos 1) by (field; apply Rgt_not_eq; lra). apply Rlt_gt; apply (Rmult_lt_compat_r (/ cos 1) (cos 1) (sin 1)). apply Rinv_0_lt_compat; assumption. apply Rle_lt_trans with (1 := t1); apply Rlt_le_trans with (2 := t2). -fourier. +lra. Qed. Definition frame_tan y : {x | 0 < x < PI/2 /\ Rabs y < tan x}. Proof. destruct (total_order_T (Rabs y) 1) as [Hs|Hgt]. - assert (yle1 : Rabs y <= 1) by (destruct Hs; fourier). + assert (yle1 : Rabs y <= 1) by (destruct Hs; lra). clear Hs; exists 1; split;[split; [exact Rlt_0_1 | exact PI2_1] | ]. apply Rle_lt_trans with (1 := yle1); exact tan_1_gt_1. assert (0 < / (Rabs y + 1)). - apply Rinv_0_lt_compat; fourier. + apply Rinv_0_lt_compat; lra. set (u := /2 * / (Rabs y + 1)). assert (0 < u). - apply Rmult_lt_0_compat; [fourier | assumption]. + apply Rmult_lt_0_compat; [lra | assumption]. assert (vlt1 : / (Rabs y + 1) < 1). apply Rmult_lt_reg_r with (Rabs y + 1). - assert (t := Rabs_pos y); fourier. - rewrite Rinv_l; [rewrite Rmult_1_l | apply Rgt_not_eq]; fourier. + assert (t := Rabs_pos y); lra. + rewrite Rinv_l; [rewrite Rmult_1_l | apply Rgt_not_eq]; lra. assert (vlt2 : u < 1). apply Rlt_trans with (/ (Rabs y + 1)). rewrite double_var. - assert (t : forall x, 0 < x -> x < x + x) by (clear; intros; fourier). + assert (t : forall x, 0 < x -> x < x + x) by (clear; intros; lra). unfold u; rewrite Rmult_comm; apply t. unfold Rdiv; rewrite Rmult_comm; assumption. assumption. assert(int : 0 < PI / 2 - u < PI / 2). split. assert (t := PI2_1); apply Rlt_Rminus, Rlt_trans with (2 := t); assumption. - assert (dumb : forall x y, 0 < y -> x - y < x) by (clear; intros; fourier). + assert (dumb : forall x y, 0 < y -> x - y < x) by (clear; intros; lra). apply dumb; clear dumb; assumption. exists (PI/2 - u). assert (tmp : forall x y, 0 < x -> y < 1 -> x * y < x). @@ -473,7 +473,7 @@ split. assert (sin u < u). assert (t1 : 0 <= u) by (apply Rlt_le; assumption). assert (t2 : u <= 4) by - (apply Rle_trans with 1;[apply Rlt_le | fourier]; assumption). + (apply Rle_trans with 1;[apply Rlt_le | lra]; assumption). destruct (pre_sin_bound u 0 t1 t2) as [_ t]. apply Rle_lt_trans with (1 := t); clear t1 t2 t. unfold sin_approx; simpl; unfold sin_term; simpl ((-1) ^ 0); @@ -503,17 +503,17 @@ split. solve[apply Rinv_0_lt_compat, INR_fact_lt_0]. apply Rlt_trans with (2 := vlt2). simpl; unfold u; apply tmp; auto; rewrite Rmult_1_r; assumption. - apply Rlt_trans with (Rabs y + 1);[fourier | ]. + apply Rlt_trans with (Rabs y + 1);[lra | ]. pattern (Rabs y + 1) at 1; rewrite <- (Rinv_involutive (Rabs y + 1)); - [ | apply Rgt_not_eq; fourier]. + [ | apply Rgt_not_eq; lra]. rewrite <- Rinv_mult_distr. apply Rinv_lt_contravar. apply Rmult_lt_0_compat. - apply Rmult_lt_0_compat;[fourier | assumption]. + apply Rmult_lt_0_compat;[lra | assumption]. assumption. replace (/(Rabs y + 1)) with (2 * u). - fourier. - unfold u; field; apply Rgt_not_eq; clear -Hgt; fourier. + lra. + unfold u; field; apply Rgt_not_eq; clear -Hgt; lra. solve[discrR]. apply Rgt_not_eq; assumption. unfold tan. @@ -522,22 +522,22 @@ set (u' := PI / 2); unfold Rdiv; apply Rmult_lt_compat_r; unfold u'. rewrite cos_shift; assumption. assert (vlt3 : u < /4). replace (/4) with (/2 * /2) by field. - unfold u; apply Rmult_lt_compat_l;[fourier | ]. + unfold u; apply Rmult_lt_compat_l;[lra | ]. apply Rinv_lt_contravar. - apply Rmult_lt_0_compat; fourier. - fourier. -assert (1 < PI / 2 - u) by (assert (t := PI2_3_2); fourier). + apply Rmult_lt_0_compat; lra. + lra. +assert (1 < PI / 2 - u) by (assert (t := PI2_3_2); lra). apply Rlt_trans with (sin 1). - assert (t' : 1 <= 4) by fourier. + assert (t' : 1 <= 4) by lra. destruct (pre_sin_bound 1 0 (Rlt_le _ _ Rlt_0_1) t') as [t _]. apply Rlt_le_trans with (2 := t); clear t. - simpl plus; replace (sin_approx 1 1) with (5/6);[fourier | ]. + simpl plus; replace (sin_approx 1 1) with (5/6);[lra | ]. unfold sin_approx, sin_term; simpl; field. apply sin_increasing_1. - assert (t := PI2_1); fourier. + assert (t := PI2_1); lra. apply Rlt_le, PI2_1. - assert (t := PI2_1); fourier. - fourier. + assert (t := PI2_1); lra. + lra. assumption. Qed. @@ -547,7 +547,7 @@ intros x h; rewrite Ropp_div; apply Ropp_lt_contravar; assumption. Qed. Lemma pos_opp_lt : forall x, 0 < x -> -x < x. -Proof. intros; fourier. Qed. +Proof. intros; lra. Qed. Lemma tech_opp_tan : forall x y, -tan x < y -> tan (-x) < y. Proof. @@ -562,7 +562,7 @@ set (pr := (conj (tech_opp_tan _ _ (proj2 (Rabs_def2 _ _ Ptan_ub))) destruct (exists_atan_in_frame (-ub) ub y (pos_opp_lt _ ub0) (ub_opp _ ubpi2) ubpi2 pr) as [v [[vl vu] vq]]. exists v; clear pr. -split;[rewrite Ropp_div; split; fourier | assumption]. +split;[rewrite Ropp_div; split; lra | assumption]. Qed. Definition atan x := let (v, _) := pre_atan x in v. @@ -581,7 +581,7 @@ Lemma atan_opp : forall x, atan (- x) = - atan x. Proof. intros x; generalize (atan_bound (-x)); rewrite Ropp_div;intros [a b]. generalize (atan_bound x); rewrite Ropp_div; intros [c d]. -apply tan_is_inj; try rewrite Ropp_div; try split; try fourier. +apply tan_is_inj; try rewrite Ropp_div; try split; try lra. rewrite tan_neg, !atan_right_inv; reflexivity. Qed. @@ -604,23 +604,23 @@ assert (int_tan : forall y, tan (- ub) <= y -> y <= tan ub -> rewrite <- (atan_right_inv y); apply tan_increasing. destruct (atan_bound y); assumption. assumption. - fourier. - fourier. + lra. + lra. destruct (Rle_lt_dec (atan y) ub) as [h | abs]; auto. assert (tan ub < y). rewrite <- (atan_right_inv y); apply tan_increasing. - rewrite Ropp_div; fourier. + rewrite Ropp_div; lra. assumption. destruct (atan_bound y); assumption. - fourier. + lra. assert (incr : forall x y, -ub <= x -> x < y -> y <= ub -> tan x < tan y). intros y z l yz u; apply tan_increasing. - rewrite Ropp_div; fourier. + rewrite Ropp_div; lra. assumption. - fourier. + lra. assert (der : forall a, -ub <= a <= ub -> derivable_pt tan a). intros a [la ua]; apply derivable_pt_tan. - rewrite Ropp_div; split; fourier. + rewrite Ropp_div; split; lra. assert (df_neq : derive_pt tan (atan x) (derivable_pt_recip_interv_prelim1 tan atan (- ub) ub x lb_lt_ub xint inv_p int_tan incr der) <> 0). @@ -651,7 +651,7 @@ Qed. Lemma atan_0 : atan 0 = 0. Proof. apply tan_is_inj; try (apply atan_bound). - assert (t := PI_RGT_0); rewrite Ropp_div; split; fourier. + assert (t := PI_RGT_0); rewrite Ropp_div; split; lra. rewrite atan_right_inv, tan_0. reflexivity. Qed. @@ -659,7 +659,7 @@ Qed. Lemma atan_1 : atan 1 = PI/4. Proof. assert (ut := PI_RGT_0). -assert (-PI/2 < PI/4 < PI/2) by (rewrite Ropp_div; split; fourier). +assert (-PI/2 < PI/4 < PI/2) by (rewrite Ropp_div; split; lra). assert (t := atan_bound 1). apply tan_is_inj; auto. rewrite tan_PI4, atan_right_inv; reflexivity. @@ -688,23 +688,23 @@ assert (int_tan : forall y, tan (- ub) <= y -> y <= tan ub -> rewrite <- (atan_right_inv y); apply tan_increasing. destruct (atan_bound y); assumption. assumption. - fourier. - fourier. + lra. + lra. destruct (Rle_lt_dec (atan y) ub) as [h | abs]; auto. assert (tan ub < y). rewrite <- (atan_right_inv y); apply tan_increasing. - rewrite Ropp_div; fourier. + rewrite Ropp_div; lra. assumption. destruct (atan_bound y); assumption. - fourier. + lra. assert (incr : forall x y, -ub <= x -> x < y -> y <= ub -> tan x < tan y). intros y z l yz u; apply tan_increasing. - rewrite Ropp_div; fourier. + rewrite Ropp_div; lra. assumption. - fourier. + lra. assert (der : forall a, -ub <= a <= ub -> derivable_pt tan a). intros a [la ua]; apply derivable_pt_tan. - rewrite Ropp_div; split; fourier. + rewrite Ropp_div; split; lra. assert (df_neq : derive_pt tan (atan x) (derivable_pt_recip_interv_prelim1 tan atan (- ub) ub x lb_lt_ub xint inv_p int_tan incr der) <> 0). @@ -883,7 +883,7 @@ Proof. destruct (Rle_lt_dec 0 x). assert (pr : 0 <= x <= 1) by tauto. exact (ps_atan_exists_01 x pr). -assert (pr : 0 <= -x <= 1) by (destruct Hx; split; fourier). +assert (pr : 0 <= -x <= 1) by (destruct Hx; split; lra). destruct (ps_atan_exists_01 _ pr) as [v Pv]. exists (-v). apply (Un_cv_ext (fun n => (- 1) * sum_f_R0 (tg_alt (Ratan_seq (- x))) n)). @@ -898,8 +898,8 @@ Proof. destruct (Rle_lt_dec x 1). destruct (Rle_lt_dec (-1) x). left;split; auto. - right;intros [a1 a2]; fourier. -right;intros [a1 a2]; fourier. + right;intros [a1 a2]; lra. +right;intros [a1 a2]; lra. Qed. Definition ps_atan (x : R) : R := @@ -922,7 +922,7 @@ unfold ps_atan. unfold Rdiv; rewrite !Rmult_0_l, Rmult_0_r; reflexivity. intros eps ep; exists 0%nat; intros n _; unfold R_dist. rewrite Rminus_0_r, Rabs_pos_eq; auto with real. -case h2; split; fourier. +case h2; split; lra. Qed. Lemma ps_atan_exists_1_opp : @@ -948,9 +948,9 @@ destruct (in_int (- x)) as [inside | outside]. destruct (in_int x) as [ins' | outs']. generalize (ps_atan_exists_1_opp x inside ins'). intros h; exact h. - destruct inside; case outs'; split; fourier. + destruct inside; case outs'; split; lra. destruct (in_int x) as [ins' | outs']. - destruct outside; case ins'; split; fourier. + destruct outside; case ins'; split; lra. apply atan_opp. Qed. @@ -1057,7 +1057,7 @@ Proof. intros x n. assert (dif : - x ^ 2 <> 1). apply Rlt_not_eq; apply Rle_lt_trans with 0;[ | apply Rlt_0_1]. -assert (t := pow2_ge_0 x); fourier. +assert (t := pow2_ge_0 x); lra. replace (1 + x ^ 2) with (1 - - (x ^ 2)) by ring; rewrite <- (tech3 _ n dif). apply sum_eq; unfold tg_alt, Datan_seq; intros i _. rewrite pow_mult, <- Rpow_mult_distr. @@ -1073,7 +1073,7 @@ intros x y n n_lb x_encad ; assert (x_pos : x >= 0) by intuition. apply False_ind ; intuition. clear -x_encad x_pos y_pos ; induction n ; unfold Datan_seq. case x_pos ; clear x_pos ; intro x_pos. - simpl ; apply Rmult_gt_0_lt_compat ; intuition. fourier. + simpl ; apply Rmult_gt_0_lt_compat ; intuition. lra. rewrite x_pos ; rewrite pow_i. replace (y ^ (2*1)) with (y*y). apply Rmult_gt_0_compat ; assumption. simpl ; field. @@ -1084,7 +1084,7 @@ intros x y n n_lb x_encad ; assert (x_pos : x >= 0) by intuition. case x_pos ; clear x_pos ; intro x_pos. rewrite Hrew ; rewrite Hrew. apply Rmult_gt_0_lt_compat ; intuition. - apply Rmult_gt_0_lt_compat ; intuition ; fourier. + apply Rmult_gt_0_lt_compat ; intuition ; lra. rewrite x_pos. rewrite pow_i ; intuition. Qed. @@ -1141,7 +1141,7 @@ elim (pow_lt_1_zero _ x_ub2 _ eps'_pos) ; intros N HN ; exists N. intros n Hn. assert (H1 : - x^2 <> 1). apply Rlt_not_eq; apply Rle_lt_trans with (2 := Rlt_0_1). -assert (t := pow2_ge_0 x); fourier. +assert (t := pow2_ge_0 x); lra. rewrite Datan_sum_eq. unfold R_dist. assert (tool : forall a b, a / b - /b = (-1 + a) /b). @@ -1179,13 +1179,13 @@ apply (Alt_CVU (fun x n => Datan_seq n x) (Datan_seq (Rabs c + r)) c r). intros x inb; apply Datan_seq_decreasing; try (apply Boule_lt in inb; apply Rabs_def2 in inb; - destruct inb; fourier). + destruct inb; lra). intros x inb; apply Datan_seq_CV_0; try (apply Boule_lt in inb; apply Rabs_def2 in inb; - destruct inb; fourier). + destruct inb; lra). intros x inb; apply (Datan_lim x); try (apply Boule_lt in inb; apply Rabs_def2 in inb; - destruct inb; fourier). + destruct inb; lra). intros x [ | n] inb. solve[unfold Datan_seq; apply Rle_refl]. rewrite <- (Datan_seq_Rabs x); apply Rlt_le, Datan_seq_increasing. @@ -1193,7 +1193,7 @@ apply (Alt_CVU (fun x n => Datan_seq n x) apply Boule_lt in inb; intuition. solve[apply Rabs_pos]. apply Datan_seq_CV_0. - apply Rlt_trans with 0;[fourier | ]. + apply Rlt_trans with 0;[lra | ]. apply Rplus_le_lt_0_compat. solve[apply Rabs_pos]. destruct r; assumption. @@ -1226,7 +1226,7 @@ intros N x x_lb x_ub. apply Hdelta ; assumption. unfold id ; field ; assumption. intros eps eps_pos. - assert (eps_3_pos : (eps/3) > 0) by fourier. + assert (eps_3_pos : (eps/3) > 0) by lra. elim (IHN (eps/3) eps_3_pos) ; intros delta1 Hdelta1. assert (Main : derivable_pt_lim (fun x : R =>tg_alt (Ratan_seq x) (S N)) x ((tg_alt (Datan_seq x)) (S N))). clear -Tool ; intros eps' eps'_pos. @@ -1297,7 +1297,7 @@ intros N x x_lb x_ub. intuition ; apply Rlt_le_trans with (r2:=delta) ; intuition unfold delta, mydelta. apply Rmin_l. apply Rmin_r. - fourier. + lra. Qed. Lemma Ratan_CVU' : @@ -1310,7 +1310,7 @@ apply (Alt_CVU (fun i r => Ratan_seq r i) ps_atan PI_tg (/2) pos_half); now intros; apply Ratan_seq_converging, Boule_half_to_interval. intros x b; apply Boule_half_to_interval in b. unfold ps_atan; destruct (in_int x) as [inside | outside]; - [ | destruct b; case outside; split; fourier]. + [ | destruct b; case outside; split; lra]. destruct (ps_atan_exists_1 x inside) as [v Pv]. apply Un_cv_ext with (2 := Pv);[reflexivity]. intros x n b; apply Boule_half_to_interval in b. @@ -1330,7 +1330,7 @@ exists N; intros n x nN b_y. case (Rtotal_order 0 x) as [xgt0 | [x0 | x0]]. assert (Boule (/2) {| pos := / 2; cond_pos := pos_half_prf|} x). revert b_y; unfold Boule; simpl; intros b_y; apply Rabs_def2 in b_y. - destruct b_y; unfold Boule; simpl; apply Rabs_def1; fourier. + destruct b_y; unfold Boule; simpl; apply Rabs_def1; lra. apply Pn; assumption. rewrite <- x0, ps_atan0_0. rewrite <- (sum_eq (fun _ => 0)), sum_cte, Rmult_0_l, Rminus_0_r, Rabs_pos_eq. @@ -1343,7 +1343,7 @@ replace (ps_atan x - sum_f_R0 (tg_alt (Ratan_seq x)) n) with rewrite Rabs_Ropp. assert (Boule (/2) {| pos := / 2; cond_pos := pos_half_prf|} (-x)). revert b_y; unfold Boule; simpl; intros b_y; apply Rabs_def2 in b_y. - destruct b_y; unfold Boule; simpl; apply Rabs_def1; fourier. + destruct b_y; unfold Boule; simpl; apply Rabs_def1; lra. apply Pn; assumption. unfold Rminus; rewrite ps_atan_opp, Ropp_plus_distr, sum_Ratan_seq_opp. rewrite !Ropp_involutive; reflexivity. @@ -1372,7 +1372,7 @@ apply continuity_inv. apply continuity_plus. apply continuity_const ; unfold constant ; intuition. apply derivable_continuous ; apply derivable_pow. -intro x ; apply Rgt_not_eq ; apply Rge_gt_trans with (1+0) ; [|fourier] ; +intro x ; apply Rgt_not_eq ; apply Rge_gt_trans with (1+0) ; [|lra] ; apply Rplus_ge_compat_l. replace (x^2) with (x²). apply Rle_ge ; apply Rle_0_sqr. @@ -1393,11 +1393,11 @@ apply derivable_pt_lim_CVU with assumption. intros y N inb; apply Rabs_def2 in inb; destruct inb. apply Datan_is_datan. - fourier. - fourier. + lra. + lra. intros y inb; apply Rabs_def2 in inb; destruct inb. - assert (y_gt_0 : -1 < y) by fourier. - assert (y_lt_1 : y < 1) by fourier. + assert (y_gt_0 : -1 < y) by lra. + assert (y_lt_1 : y < 1) by lra. intros eps eps_pos ; elim (Ratan_is_ps_atan eps eps_pos). intros N HN ; exists N; intros n n_lb ; apply HN ; tauto. apply Datan_CVU_prelim. @@ -1406,8 +1406,8 @@ apply derivable_pt_lim_CVU with replace ((c + r - (c - r)) / 2) with (r :R) by field. assert (Rabs c < 1 - r). unfold Boule in Pcr1; destruct r; simpl in *; apply Rabs_def1; - apply Rabs_def2 in Pcr1; destruct Pcr1; fourier. - fourier. + apply Rabs_def2 in Pcr1; destruct Pcr1; lra. + lra. intros; apply Datan_continuity. Qed. @@ -1426,7 +1426,7 @@ Lemma ps_atan_continuity_pt_1 : forall eps : R, dist R_met (ps_atan x) (Alt_PI/4) < eps). Proof. intros eps eps_pos. -assert (eps_3_pos : eps / 3 > 0) by fourier. +assert (eps_3_pos : eps / 3 > 0) by lra. elim (Ratan_is_ps_atan (eps / 3) eps_3_pos) ; intros N1 HN1. unfold Alt_PI. destruct exist_PI as [v Pv]; replace ((4 * v)/4) with v by field. @@ -1461,10 +1461,10 @@ rewrite Rplus_assoc ; apply Rabs_triang. unfold D_x, no_cond ; split ; [ | apply Rgt_not_eq ] ; intuition. intuition. apply HN2; unfold N; omega. - fourier. + lra. rewrite <- Rabs_Ropp, Ropp_minus_distr; apply HN1. unfold N; omega. - fourier. + lra. assumption. field. ring. @@ -1486,11 +1486,11 @@ intros x x_encad Pratan Prmymeta. rewrite Hrew1. replace (Rsqr x) with (x ^ 2) by (unfold Rsqr; ring). unfold Rdiv; rewrite Rmult_1_l; reflexivity. - fourier. + lra. assumption. intros; reflexivity. - fourier. - assert (t := tan_1_gt_1); split;destruct x_encad; fourier. + lra. + assert (t := tan_1_gt_1); split;destruct x_encad; lra. intros; reflexivity. Qed. @@ -1503,46 +1503,46 @@ assert (pr1 : forall c : R, 0 < c < x -> derivable_pt (atan - ps_atan) c). apply derivable_pt_minus. exact (derivable_pt_atan c). apply derivable_pt_ps_atan. - destruct x_encad; destruct c_encad; split; fourier. + destruct x_encad; destruct c_encad; split; lra. assert (pr2 : forall c : R, 0 < c < x -> derivable_pt id c). - intros ; apply derivable_pt_id; fourier. + intros ; apply derivable_pt_id; lra. assert (delta_cont : forall c : R, 0 <= c <= x -> continuity_pt (atan - ps_atan) c). intros c [[c_encad1 | c_encad1 ] [c_encad2 | c_encad2]]; apply continuity_pt_minus. apply derivable_continuous_pt ; apply derivable_pt_atan. apply derivable_continuous_pt ; apply derivable_pt_ps_atan. - split; destruct x_encad; fourier. + split; destruct x_encad; lra. apply derivable_continuous_pt, derivable_pt_atan. apply derivable_continuous_pt, derivable_pt_ps_atan. - subst c; destruct x_encad; split; fourier. + subst c; destruct x_encad; split; lra. apply derivable_continuous_pt, derivable_pt_atan. apply derivable_continuous_pt, derivable_pt_ps_atan. - subst c; split; fourier. + subst c; split; lra. apply derivable_continuous_pt, derivable_pt_atan. apply derivable_continuous_pt, derivable_pt_ps_atan. - subst c; destruct x_encad; split; fourier. + subst c; destruct x_encad; split; lra. assert (id_cont : forall c : R, 0 <= c <= x -> continuity_pt id c). intros ; apply derivable_continuous ; apply derivable_id. -assert (x_lb : 0 < x) by (destruct x_encad; fourier). +assert (x_lb : 0 < x) by (destruct x_encad; lra). elim (MVT (atan - ps_atan)%F id 0 x pr1 pr2 x_lb delta_cont id_cont) ; intros d Temp ; elim Temp ; intros d_encad Main. clear - Main x_encad. assert (Temp : forall (pr: derivable_pt (atan - ps_atan) d), derive_pt (atan - ps_atan) d pr = 0). intro pr. assert (d_encad3 : -1 < d < 1). - destruct d_encad; destruct x_encad; split; fourier. + destruct d_encad; destruct x_encad; split; lra. pose (pr3 := derivable_pt_minus atan ps_atan d (derivable_pt_atan d) (derivable_pt_ps_atan d d_encad3)). rewrite <- pr_nu_var2_interv with (f:=(atan - ps_atan)%F) (g:=(atan - ps_atan)%F) (lb:=0) (ub:=x) (pr1:=pr3) (pr2:=pr). unfold pr3. rewrite derive_pt_minus. rewrite Datan_eq_DatanSeq_interv with (Prmymeta := derivable_pt_atan d). intuition. assumption. - destruct d_encad; fourier. + destruct d_encad; lra. assumption. reflexivity. assert (iatan0 : atan 0 = 0). apply tan_is_inj. apply atan_bound. - rewrite Ropp_div; assert (t := PI2_RGT_0); split; fourier. + rewrite Ropp_div; assert (t := PI2_RGT_0); split; lra. rewrite tan_0, atan_right_inv; reflexivity. generalize Main; rewrite Temp, Rmult_0_r. replace ((atan - ps_atan)%F x) with (atan x - ps_atan x) by intuition. @@ -1560,19 +1560,19 @@ Qed. Theorem Alt_PI_eq : Alt_PI = PI. Proof. apply Rmult_eq_reg_r with (/4); fold (Alt_PI/4); fold (PI/4); - [ | apply Rgt_not_eq; fourier]. + [ | apply Rgt_not_eq; lra]. assert (0 < PI/6) by (apply PI6_RGT_0). assert (t1:= PI2_1). assert (t2 := PI_4). assert (m := Alt_PI_RGT_0). -assert (-PI/2 < 1 < PI/2) by (rewrite Ropp_div; split; fourier). +assert (-PI/2 < 1 < PI/2) by (rewrite Ropp_div; split; lra). apply cond_eq; intros eps ep. change (R_dist (Alt_PI/4) (PI/4) < eps). assert (ca : continuity_pt atan 1). apply derivable_continuous_pt, derivable_pt_atan. assert (Xe : exists eps', exists eps'', eps' + eps'' <= eps /\ 0 < eps' /\ 0 < eps''). - exists (eps/2); exists (eps/2); repeat apply conj; fourier. + exists (eps/2); exists (eps/2); repeat apply conj; lra. destruct Xe as [eps' [eps'' [eps_ineq [ep' ep'']]]]. destruct (ps_atan_continuity_pt_1 _ ep') as [alpha [a0 Palpha]]. destruct (ca _ ep'') as [beta [b0 Pbeta]]. @@ -1585,14 +1585,14 @@ assert (Xa : exists a, 0 < a < 1 /\ R_dist a 1 < alpha /\ assert ((1 - alpha /2) <= Rmax (1 - alpha /2) (1 - beta /2)) by apply Rmax_l. assert ((1 - beta /2) <= Rmax (1 - alpha /2) (1 - beta /2)) by apply Rmax_r. assert (Rmax (1 - alpha /2) (1 - beta /2) < 1) - by (apply Rmax_lub_lt; fourier). - split;[split;[ | apply Rmax_lub_lt]; fourier | ]. + by (apply Rmax_lub_lt; lra). + split;[split;[ | apply Rmax_lub_lt]; lra | ]. assert (0 <= 1 - Rmax (/ 2) (Rmax (1 - alpha / 2) (1 - beta / 2))). assert (Rmax (/2) (Rmax (1 - alpha / 2) - (1 - beta /2)) <= 1) by (apply Rmax_lub; fourier). - fourier. + (1 - beta /2)) <= 1) by (apply Rmax_lub; lra). + lra. split; unfold R_dist; rewrite <-Rabs_Ropp, Ropp_minus_distr, - Rabs_pos_eq;fourier. + Rabs_pos_eq;lra. destruct Xa as [a [[Pa0 Pa1] [P1 P2]]]. apply Rle_lt_trans with (1 := R_dist_tri _ _ (ps_atan a)). apply Rlt_le_trans with (2 := eps_ineq). diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index aa886cee0..59e014862 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -15,7 +15,7 @@ Require Import Rbase. Require Import R_Ifp. -Require Import Fourier. +Require Import Lra. Local Open Scope R_scope. Implicit Type r : R. @@ -357,7 +357,7 @@ Qed. Lemma Rle_abs : forall x:R, x <= Rabs x. Proof. - intro; unfold Rabs; case (Rcase_abs x); intros; fourier. + intro; unfold Rabs; case (Rcase_abs x); intros; lra. Qed. Definition RRle_abs := Rle_abs. diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index dfa5c7104..aaf691ed1 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -16,7 +16,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Rlimit. -Require Import Fourier. +Require Import Lra. Require Import Omega. Local Open Scope R_scope. @@ -77,7 +77,7 @@ Proof. elim (Rmin_Rgt (/ 2) x 0); intros a b; cut (0 < 2). intro; generalize (Rinv_0_lt_compat 2 H3); intro; fold (/ 2 > 0) in H4; apply (b (conj H4 H)). - fourier. + lra. intros; elim H3; clear H3; intros; generalize (let (H1, H2) := @@ -167,7 +167,7 @@ Proof. unfold Rabs; destruct (Rcase_abs 2) as [Hlt|Hge]; auto. cut (0 < 2). intro H7; elim (Rlt_asym 0 2 H7 Hlt). - fourier. + lra. apply Rabs_no_R0. discrR. Qed. diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v index b249b519f..3ef368bb4 100644 --- a/theories/Reals/Reals.v +++ b/theories/Reals/Reals.v @@ -30,3 +30,4 @@ Require Export SeqSeries. Require Export Rtrigo. Require Export Ranalysis. Require Export Integration. +Require Import Fourier. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index b14fcc4d3..e3e995d20 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -15,7 +15,7 @@ Require Import Rbase. Require Import Rfunctions. -Require Import Fourier. +Require Import Lra. Local Open Scope R_scope. (*******************************) @@ -24,7 +24,7 @@ Local Open Scope R_scope. (*********) Lemma eps2_Rgt_R0 : forall eps:R, eps > 0 -> eps * / 2 > 0. Proof. - intros; fourier. + intros; lra. Qed. (*********) @@ -45,14 +45,14 @@ Qed. Lemma Rlt_eps2_eps : forall eps:R, eps > 0 -> eps * / 2 < eps. Proof. intros. - fourier. + lra. Qed. (*********) Lemma Rlt_eps4_eps : forall eps:R, eps > 0 -> eps * / (2 + 2) < eps. Proof. intros. - fourier. + lra. Qed. (*********) diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index c6fac951b..d465523a7 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -25,7 +25,7 @@ Require Import R_sqrt. Require Import Sqrt_reg. Require Import MVT. Require Import Ranalysis4. -Require Import Fourier. +Require Import Lra. Local Open Scope R_scope. Lemma P_Rmin : forall (P:R -> Prop) (x y:R), P x -> P y -> P (Rmin x y). @@ -714,7 +714,7 @@ Qed. Lemma Rlt_Rpower_l a b c: 0 < c -> 0 < a < b -> a ^R c < b ^R c. Proof. intros c0 [a0 ab]; apply exp_increasing. -now apply Rmult_lt_compat_l; auto; apply ln_increasing; fourier. +now apply Rmult_lt_compat_l; auto; apply ln_increasing; lra. Qed. Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> a ^R c <= b ^R c. @@ -722,7 +722,7 @@ Proof. intros [c0 | c0]; [ | intros; rewrite <- c0, !Rpower_O; [apply Rle_refl | |] ]. intros [a0 [ab|ab]]. - now apply Rlt_le, Rlt_Rpower_l;[ | split]; fourier. + now apply Rlt_le, Rlt_Rpower_l;[ | split]; lra. rewrite ab; apply Rle_refl. apply Rlt_le_trans with a; tauto. tauto. @@ -754,10 +754,10 @@ assert (cmp : 0 < x + sqrt (x ^ 2 + 1)). replace (x ^ 2) with ((-x) ^ 2) by ring. assert (sqrt ((- x) ^ 2) < sqrt ((-x)^2+1)). apply sqrt_lt_1_alt. - split;[apply pow_le | ]; fourier. + split;[apply pow_le | ]; lra. pattern x at 1; replace x with (- (sqrt ((- x) ^ 2))). - assert (t:= sqrt_pos ((-x)^2)); fourier. - simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive;[reflexivity | fourier]. + assert (t:= sqrt_pos ((-x)^2)); lra. + simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive;[reflexivity | lra]. apply Rplus_lt_le_0_compat;[apply Rnot_le_gt; assumption | apply sqrt_pos]. rewrite exp_ln;[ | assumption]. rewrite exp_Ropp, exp_ln;[ | assumption]. @@ -770,7 +770,7 @@ apply Rmult_eq_reg_l with (2 * (x + sqrt (x ^ 2 + 1)));[ | apply Rgt_not_eq, Rmult_lt_0_compat;[apply Rlt_0_2 | assumption]]. assert (pow2_sqrt : forall x, 0 <= x -> sqrt x ^ 2 = x) by (intros; simpl; rewrite Rmult_1_r, sqrt_sqrt; auto). -field_simplify;[rewrite pow2_sqrt;[field | ] | apply Rgt_not_eq; fourier]. +field_simplify;[rewrite pow2_sqrt;[field | ] | apply Rgt_not_eq; lra]. apply Rplus_le_le_0_compat;[simpl; rewrite Rmult_1_r; apply (Rle_0_sqr x)|apply Rlt_le, Rlt_0_1]. Qed. @@ -784,12 +784,12 @@ assert (0 < x + sqrt (x ^ 2 + 1)). replace (x ^ 2) with ((-x) ^ 2) by ring. assert (sqrt ((- x) ^ 2) < sqrt ((-x)^2+1)). apply sqrt_lt_1_alt. - split;[apply pow_le|]; fourier. + split;[apply pow_le|]; lra. pattern x at 1; replace x with (- (sqrt ((- x) ^ 2))). - assert (t:= sqrt_pos ((-x)^2)); fourier. - simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive; auto; fourier. + assert (t:= sqrt_pos ((-x)^2)); lra. + simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive; auto; lra. assert (0 < x ^ 2 + 1). - apply Rplus_le_lt_0_compat;[simpl; rewrite Rmult_1_r; apply Rle_0_sqr|fourier]. + apply Rplus_le_lt_0_compat;[simpl; rewrite Rmult_1_r; apply Rle_0_sqr|lra]. replace (/sqrt (x ^ 2 + 1)) with (/(x + sqrt (x ^ 2 + 1)) * (1 + (/(2 * sqrt (x ^ 2 + 1)) * (INR 2 * x ^ 1 + 0)))). @@ -817,7 +817,7 @@ intros x y xy. case (Rle_dec (arcsinh y) (arcsinh x));[ | apply Rnot_le_lt ]. intros abs; case (Rlt_not_le _ _ xy). rewrite <- (sinh_arcsinh y), <- (sinh_arcsinh x). -destruct abs as [lt | q];[| rewrite q; fourier]. +destruct abs as [lt | q];[| rewrite q; lra]. apply Rlt_le, sinh_lt; assumption. Qed. diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index ffc0adf50..ddd8722e1 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -18,7 +18,7 @@ Require Export Cos_rel. Require Export Cos_plus. Require Import ZArith_base. Require Import Zcomplements. -Require Import Fourier. +Require Import Lra. Require Import Ranalysis1. Require Import Rsqrt_def. Require Import PSeries_reg. diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v index bf00f736f..a75fd2dde 100644 --- a/theories/Reals/Rtrigo1.v +++ b/theories/Reals/Rtrigo1.v @@ -18,7 +18,7 @@ Require Export Cos_rel. Require Export Cos_plus. Require Import ZArith_base. Require Import Zcomplements. -Require Import Fourier. +Require Import Lra. Require Import Ranalysis1. Require Import Rsqrt_def. Require Import PSeries_reg. @@ -175,10 +175,10 @@ Qed. Lemma sin_gt_cos_7_8 : sin (7 / 8) > cos (7 / 8). Proof. -assert (lo1 : 0 <= 7/8) by fourier. -assert (up1 : 7/8 <= 4) by fourier. -assert (lo : -2 <= 7/8) by fourier. -assert (up : 7/8 <= 2) by fourier. +assert (lo1 : 0 <= 7/8) by lra. +assert (up1 : 7/8 <= 4) by lra. +assert (lo : -2 <= 7/8) by lra. +assert (up : 7/8 <= 2) by lra. destruct (pre_sin_bound _ 0 lo1 up1) as [lower _ ]. destruct (pre_cos_bound _ 0 lo up) as [_ upper]. apply Rle_lt_trans with (1 := upper). @@ -205,12 +205,12 @@ Definition PI_2_aux : {z | 7/8 <= z <= 7/4 /\ -cos z = 0}. assert (cc : continuity (fun r =>- cos r)). apply continuity_opp, continuity_cos. assert (cvp : 0 < cos (7/8)). - assert (int78 : -2 <= 7/8 <= 2) by (split; fourier). + assert (int78 : -2 <= 7/8 <= 2) by (split; lra). destruct int78 as [lower upper]. case (pre_cos_bound _ 0 lower upper). unfold cos_approx; simpl sum_f_R0; unfold cos_term. intros cl _; apply Rlt_le_trans with (2 := cl); simpl. - fourier. + lra. assert (cun : cos (7/4) < 0). replace (7/4) with (7/8 + 7/8) by field. rewrite cos_plus. @@ -218,7 +218,7 @@ assert (cun : cos (7/4) < 0). exact sin_gt_cos_7_8. apply Rlt_le; assumption. apply Rlt_le; apply Rlt_trans with (1 := cvp); exact sin_gt_cos_7_8. -apply IVT; auto; fourier. +apply IVT; auto; lra. Qed. Definition PI2 := proj1_sig PI_2_aux. @@ -270,7 +270,7 @@ Qed. Lemma sin_pos_tech : forall x, 0 < x < 2 -> 0 < sin x. intros x [int1 int2]. assert (lo : 0 <= x) by (apply Rlt_le; assumption). -assert (up : x <= 4) by (apply Rlt_le, Rlt_trans with (1:=int2); fourier). +assert (up : x <= 4) by (apply Rlt_le, Rlt_trans with (1:=int2); lra). destruct (pre_sin_bound _ 0 lo up) as [t _]; clear lo up. apply Rlt_le_trans with (2:= t); clear t. unfold sin_approx; simpl sum_f_R0; unfold sin_term; simpl. @@ -280,13 +280,13 @@ end. assert (t' : x ^ 2 <= 4). replace 4 with (2 ^ 2) by field. apply (pow_incr x 2); split; apply Rlt_le; assumption. -apply Rmult_lt_0_compat;[assumption | fourier ]. +apply Rmult_lt_0_compat;[assumption | lra ]. Qed. Lemma sin_PI2 : sin (PI / 2) = 1. replace (PI / 2) with PI2 by (unfold PI; field). assert (int' : 0 < PI2 < 2). - destruct pi2_int; split; fourier. + destruct pi2_int; split; lra. assert (lo2 := sin_pos_tech PI2 int'). assert (t2 : Rabs (sin PI2) = 1). rewrite <- Rabs_R1; apply Rsqr_eq_abs_0. @@ -295,10 +295,10 @@ revert t2; rewrite Rabs_pos_eq;[| apply Rlt_le]; tauto. Qed. Lemma PI_RGT_0 : PI > 0. -Proof. unfold PI; destruct pi2_int; fourier. Qed. +Proof. unfold PI; destruct pi2_int; lra. Qed. Lemma PI_4 : PI <= 4. -Proof. unfold PI; destruct pi2_int; fourier. Qed. +Proof. unfold PI; destruct pi2_int; lra. Qed. (**********) Lemma PI_neq0 : PI <> 0. @@ -344,13 +344,13 @@ Lemma cos_bound : forall (a : R) (n : nat), - PI / 2 <= a -> a <= PI / 2 -> Proof. intros a n lower upper; apply pre_cos_bound. apply Rle_trans with (2 := lower). - apply Rmult_le_reg_r with 2; [fourier |]. + apply Rmult_le_reg_r with 2; [lra |]. replace ((-PI/2) * 2) with (-PI) by field. - assert (t := PI_4); fourier. + assert (t := PI_4); lra. apply Rle_trans with (1 := upper). -apply Rmult_le_reg_r with 2; [fourier | ]. +apply Rmult_le_reg_r with 2; [lra | ]. replace ((PI/2) * 2) with PI by field. -generalize PI_4; intros; fourier. +generalize PI_4; intros; lra. Qed. (**********) Lemma neg_cos : forall x:R, cos (x + PI) = - cos x. @@ -749,19 +749,19 @@ Qed. Lemma _PI2_RLT_0 : - (PI / 2) < 0. Proof. assert (H := PI_RGT_0). - fourier. + lra. Qed. Lemma PI4_RLT_PI2 : PI / 4 < PI / 2. Proof. assert (H := PI_RGT_0). - fourier. + lra. Qed. Lemma PI2_Rlt_PI : PI / 2 < PI. Proof. assert (H := PI_RGT_0). - fourier. + lra. Qed. (***************************************************) diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 7cbfc6303..78797c87c 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -205,7 +205,6 @@ Proof with trivial. rewrite cos2; unfold Rsqr; rewrite sin_PI6; rewrite sqrt_def... field. left ; prove_sup0. - discrR. Qed. Lemma tan_PI6 : tan (PI / 6) = 1 / sqrt 3. |