aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Reals/Machin.v36
-rw-r--r--theories/Reals/PSeries_reg.v29
-rw-r--r--theories/Reals/R_sqrt.v20
-rw-r--r--theories/Reals/Ranalysis5.v90
-rw-r--r--theories/Reals/Ratan.v238
-rw-r--r--theories/Reals/Rbasic_fun.v4
-rw-r--r--theories/Reals/Rderiv.v6
-rw-r--r--theories/Reals/Reals.v1
-rw-r--r--theories/Reals/Rlimit.v8
-rw-r--r--theories/Reals/Rpower.v24
-rw-r--r--theories/Reals/Rtrigo.v2
-rw-r--r--theories/Reals/Rtrigo1.v40
-rw-r--r--theories/Reals/Rtrigo_calc.v1
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.