diff options
27 files changed, 229 insertions, 274 deletions
diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v index 1d7ee93ea..a96254713 100644 --- a/plugins/fourier/Fourier.v +++ b/plugins/fourier/Fourier.v @@ -13,6 +13,6 @@ Require Export DiscrR. Require Export Fourier_util. Declare ML Module "fourier_plugin". -Ltac fourier := abstract (fourierz; field; discrR). +Ltac fourier := abstract (compute [IZR IPR IPR_2] in *; fourierz; field; discrR). Ltac fourier_eq := apply Rge_antisym; fourier. diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v index 293722125..facd2e062 100644 --- a/plugins/setoid_ring/RealField.v +++ b/plugins/setoid_ring/RealField.v @@ -59,11 +59,12 @@ Notation Rset := (Eqsth R). Notation Rext := (Eq_ext Rplus Rmult Ropp). Lemma Rlt_0_2 : 0 < 2. +Proof. apply Rlt_trans with (0 + 1). apply Rlt_n_Sn. rewrite Rplus_comm. apply Rplus_lt_compat_l. - replace 1 with (0 + 1). + replace R1 with (0 + 1). apply Rlt_n_Sn. apply Rplus_0_l. Qed. @@ -126,9 +127,17 @@ Ltac Rpow_tac t := | _ => constr:(N.of_nat t) end. -Add Field RField : Rfield - (completeness Zeq_bool_complete, power_tac R_power_theory [Rpow_tac]). - - - +Ltac IZR_tac t := + match t with + | R0 => constr:(0%Z) + | R1 => constr:(1%Z) + | IZR ?u => + match isZcst u with + | true => u + | _ => constr:(InitialRing.NotConstant) + end + | _ => constr:(InitialRing.NotConstant) + end. +Add Field RField : Rfield + (completeness Zeq_bool_complete, constants [IZR_tac], power_tac R_power_theory [Rpow_tac]). diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 3ae2d45f3..8f065f528 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -9,6 +9,8 @@ open Util open Names open Globnames +open Glob_term +open Bigint (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "r_syntax_plugin" @@ -17,95 +19,105 @@ let () = Mltop.add_known_module __coq_plugin_name exception Non_closed_number (**********************************************************************) -(* Parsing R via scopes *) +(* Parsing positive via scopes *) (**********************************************************************) -open Glob_term -open Bigint +let binnums = ["Coq";"Numbers";"BinNums"] let make_dir l = DirPath.make (List.rev_map Id.of_string l) -let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"] -let make_path dir id = Libnames.make_path dir (Id.of_string id) +let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) + +let positive_path = make_path binnums "positive" + +(* TODO: temporary hack *) +let make_kn dir id = Globnames.encode_mind dir id + +let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive") +let glob_positive = IndRef (positive_kn,0) +let path_of_xI = ((positive_kn,0),1) +let path_of_xO = ((positive_kn,0),2) +let path_of_xH = ((positive_kn,0),3) +let glob_xI = ConstructRef path_of_xI +let glob_xO = ConstructRef path_of_xO +let glob_xH = ConstructRef path_of_xH + +let pos_of_bignat dloc x = + let ref_xI = GRef (dloc, glob_xI, None) in + let ref_xH = GRef (dloc, glob_xH, None) in + let ref_xO = GRef (dloc, glob_xO, None) in + let rec pos_of x = + match div2_with_rest x with + | (q,false) -> GApp (dloc, ref_xO,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> GApp (dloc,ref_xI,[pos_of q]) + | (q,true) -> ref_xH + in + pos_of x + +(**********************************************************************) +(* Printing positive via scopes *) +(**********************************************************************) + +let rec bignat_of_pos = function + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) + | GRef (_, a, _) when Globnames.eq_gr a glob_xH -> Bigint.one + | _ -> raise Non_closed_number + +(**********************************************************************) +(* Parsing Z via scopes *) +(**********************************************************************) +let z_path = make_path binnums "Z" +let z_kn = make_kn (make_dir binnums) (Id.of_string "Z") +let glob_z = IndRef (z_kn,0) +let path_of_ZERO = ((z_kn,0),1) +let path_of_POS = ((z_kn,0),2) +let path_of_NEG = ((z_kn,0),3) +let glob_ZERO = ConstructRef path_of_ZERO +let glob_POS = ConstructRef path_of_POS +let glob_NEG = ConstructRef path_of_NEG + +let z_of_int dloc n = + if not (Bigint.equal n zero) then + let sgn, n = + if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in + GApp(dloc, GRef (dloc,sgn,None), [pos_of_bignat dloc n]) + else + GRef (dloc, glob_ZERO, None) + +(**********************************************************************) +(* Printing Z via scopes *) +(**********************************************************************) + +let bigint_of_z = function + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) + | GRef (_, a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero + | _ -> raise Non_closed_number + +(**********************************************************************) +(* Parsing R via scopes *) +(**********************************************************************) + +let rdefinitions = ["Coq";"Reals";"Rdefinitions"] let r_path = make_path rdefinitions "R" (* TODO: temporary hack *) let make_path dir id = Globnames.encode_con dir (Id.of_string id) -let r_kn = make_path rdefinitions "R" -let glob_R = ConstRef r_kn -let glob_R1 = ConstRef (make_path rdefinitions "R1") -let glob_R0 = ConstRef (make_path rdefinitions "R0") -let glob_Ropp = ConstRef (make_path rdefinitions "Ropp") -let glob_Rplus = ConstRef (make_path rdefinitions "Rplus") -let glob_Rmult = ConstRef (make_path rdefinitions "Rmult") - -let two = mult_2 one -let three = add_1 two -let four = mult_2 two - -(* Unary representation of strictly positive numbers *) -let rec small_r dloc n = - if equal one n then GRef (dloc, glob_R1, None) - else GApp(dloc,GRef (dloc,glob_Rplus, None), - [GRef (dloc, glob_R1, None);small_r dloc (sub_1 n)]) - -let r_of_posint dloc n = - let r1 = GRef (dloc, glob_R1, None) in - let r2 = small_r dloc two in - let rec r_of_pos n = - if less_than n four then small_r dloc n - else - let (q,r) = div2_with_rest n in - let b = GApp(dloc,GRef(dloc,glob_Rmult,None),[r2;r_of_pos q]) in - if r then GApp(dloc,GRef(dloc,glob_Rplus,None),[r1;b]) else b in - if not (Bigint.equal n zero) then r_of_pos n else GRef(dloc,glob_R0,None) +let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR") let r_of_int dloc z = - if is_strictly_neg z then - GApp (dloc, GRef(dloc,glob_Ropp,None), [r_of_posint dloc (neg z)]) - else - r_of_posint dloc z + GApp (dloc, GRef(dloc,glob_IZR,None), [z_of_int dloc z]) (**********************************************************************) (* Printing R via scopes *) (**********************************************************************) -let bignat_of_r = -(* for numbers > 1 *) -let rec bignat_of_pos = function - (* 1+1 *) - | GApp (_,GRef (_,p,_), [GRef (_,o1,_); GRef (_,o2,_)]) - when Globnames.eq_gr p glob_Rplus && Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 -> two - (* 1+(1+1) *) - | GApp (_,GRef (_,p1,_), [GRef (_,o1,_); - GApp(_,GRef (_,p2,_),[GRef(_,o2,_);GRef(_,o3,_)])]) - when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rplus && - Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 && Globnames.eq_gr o3 glob_R1 -> three - (* (1+1)*b *) - | GApp (_,GRef (_,p,_), [a; b]) when Globnames.eq_gr p glob_Rmult -> - if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number; - mult_2 (bignat_of_pos b) - (* 1+(1+1)*b *) - | GApp (_,GRef (_,p1,_), [GRef (_,o,_); GApp (_,GRef (_,p2,_),[a;b])]) - when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rmult && Globnames.eq_gr o glob_R1 -> - if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number; - add_1 (mult_2 (bignat_of_pos b)) - | _ -> raise Non_closed_number -in -let bignat_of_r = function - | GRef (_,a,_) when Globnames.eq_gr a glob_R0 -> zero - | GRef (_,a,_) when Globnames.eq_gr a glob_R1 -> one - | r -> bignat_of_pos r -in -bignat_of_r - let bigint_of_r = function - | GApp (_,GRef (_,o,_), [a]) when Globnames.eq_gr o glob_Ropp -> - let n = bignat_of_r a in - if Bigint.equal n zero then raise Non_closed_number; - neg n - | a -> bignat_of_r a + | GApp (_,GRef (_,o,_), [a]) when Globnames.eq_gr o glob_IZR -> + bigint_of_z a + | _ -> raise Non_closed_number let uninterp_r p = try @@ -113,12 +125,9 @@ let uninterp_r p = with Non_closed_number -> None -let mkGRef gr = GRef (Loc.ghost,gr,None) - let _ = Notation.declare_numeral_interpreter "R_scope" (r_path,["Coq";"Reals";"Rdefinitions"]) r_of_int - (List.map mkGRef - [glob_Ropp;glob_R0;glob_Rplus;glob_Rmult;glob_R1], + ([GRef (Loc.ghost,glob_IZR,None)], uninterp_r, false) diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index a98d529fa..0e1608a32 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -78,7 +78,7 @@ Proof. ring. discrR. discrR. - pattern 1 at 3; replace 1 with (/ 1); + replace 1 with (/ 1); [ apply tech7; discrR | apply Rinv_1 ]. replace (An (S x)) with (An (S x + 0)%nat). apply (tech6 (fun i:nat => An (S x + i)%nat) (/ 2)). diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index 7d9fff276..67584f775 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -106,7 +106,7 @@ Proof. split. ring. unfold k0; case (Rcase_abs y) as [Hlt|Hge]. - assert (H0 := archimed (x / - y)); rewrite <- Z_R_minus; change (IZR 1) with 1; + assert (H0 := archimed (x / - y)); rewrite <- Z_R_minus; simpl; unfold Rminus. replace (- ((1 + - IZR (up (x / - y))) * y)) with ((IZR (up (x / - y)) - 1) * y); [ idtac | ring ]. @@ -140,10 +140,10 @@ Proof. rewrite <- Ropp_mult_distr_r_reverse; rewrite (Ropp_inv_permute _ H); elim H0; unfold Rdiv; intros H1 _; exact H1. apply Ropp_neq_0_compat; assumption. - assert (H0 := archimed (x / y)); rewrite <- Z_R_minus; change (IZR 1) with 1; + assert (H0 := archimed (x / y)); rewrite <- Z_R_minus; simpl; cut (0 < y). intro; unfold Rminus; - replace (- ((IZR (up (x / y)) + -1) * y)) with ((1 - IZR (up (x / y))) * y); + replace (- ((IZR (up (x / y)) + -(1)) * y)) with ((1 - IZR (up (x / y))) * y); [ idtac | ring ]. split. apply Rmult_le_reg_l with (/ y). diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index 4e2a7c3c6..05911cd53 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -31,9 +31,6 @@ Ltac discrR := try match goal with | |- (?X1 <> ?X2) => - change 2 with (IZR 2); - change 1 with (IZR 1); - change 0 with (IZR 0); repeat rewrite <- plus_IZR || rewrite <- mult_IZR || @@ -52,9 +49,6 @@ Ltac prove_sup0 := end. Ltac omega_sup := - change 2 with (IZR 2); - change 1 with (IZR 1); - change 0 with (IZR 0); repeat rewrite <- plus_IZR || rewrite <- mult_IZR || rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus; @@ -72,9 +66,6 @@ Ltac prove_sup := end. Ltac Rcompute := - change 2 with (IZR 2); - change 1 with (IZR 1); - change 0 with (IZR 0); repeat rewrite <- plus_IZR || rewrite <- mult_IZR || rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus; diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index 569518f7b..e9de24898 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -439,20 +439,16 @@ Proof. repeat rewrite <- Rmult_assoc. rewrite <- Rinv_r_sym. rewrite Rmult_1_l. - replace (INR N * INR N) with (Rsqr (INR N)); [ idtac | reflexivity ]. - rewrite Rmult_assoc. - rewrite Rmult_comm. - replace 4 with (Rsqr 2); [ idtac | ring_Rsqr ]. + change 4 with (Rsqr 2). rewrite <- Rsqr_mult. apply Rsqr_incr_1. - replace 2 with (INR 2). - rewrite <- mult_INR; apply H1. - reflexivity. + change 2 with (INR 2). + rewrite Rmult_comm, <- mult_INR; apply H1. left; apply lt_INR_0; apply H. left; apply Rmult_lt_0_compat. - prove_sup0. apply lt_INR_0; apply div2_not_R0. apply lt_n_S; apply H. + now apply IZR_lt. cut (1 < S N)%nat. intro; unfold Rsqr; apply prod_neq_R0; apply not_O_INR; intro; assert (H4 := div2_not_R0 _ H2); rewrite H3 in H4; diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v index 19db476fd..2d2385703 100644 --- a/theories/Reals/Machin.v +++ b/theories/Reals/Machin.v @@ -53,7 +53,7 @@ assert (-(PI/4) <= atan x). destruct xm1 as [xm1 | xm1]. rewrite <- atan_1, <- atan_opp; apply Rlt_le, atan_increasing. assumption. - solve[rewrite <- xm1, atan_opp, atan_1; apply Rle_refl]. + solve[rewrite <- xm1; change (-1) with (-(1)); rewrite atan_opp, atan_1; apply Rle_refl]. assert (-(PI/4) < atan y). rewrite <- atan_1, <- atan_opp; apply atan_increasing. assumption. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 686077327..7cd4c00c7 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1812,7 +1812,7 @@ Qed. (**********) Lemma succ_IZR : forall n:Z, IZR (Z.succ n) = IZR n + 1. Proof. - intro; change 1 with (IZR 1); unfold Z.succ; apply plus_IZR. + intro; unfold Z.succ; apply plus_IZR. Qed. (**********) diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index d0f9aea28..e9b1762af 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -92,7 +92,7 @@ Proof. auto with zarith real. (*inf a 1*) cut (r - IZR (up r) < 0). - rewrite <- Z_R_minus; change (IZR 1) with 1; intro; unfold Rminus; + rewrite <- Z_R_minus; simpl; intro; unfold Rminus; rewrite Ropp_plus_distr; rewrite <- Rplus_assoc; fold (r - IZR (up r)); rewrite Ropp_involutive; elim (Rplus_ne 1); intros a b; pattern 1 at 2; @@ -112,21 +112,12 @@ Lemma base_Int_part : Proof. intro; unfold Int_part; elim (archimed r); intros. split; rewrite <- (Z_R_minus (up r) 1); simpl. - generalize (Rle_minus (IZR (up r) - r) 1 H0); intro; unfold Rminus in H1; - rewrite (Rplus_assoc (IZR (up r)) (- r) (-1)) in H1; - rewrite (Rplus_comm (- r) (-1)) in H1; - rewrite <- (Rplus_assoc (IZR (up r)) (-1) (- r)) in H1; - fold (IZR (up r) - 1) in H1; fold (IZR (up r) - 1 - r) in H1; - apply Rminus_le; auto with zarith real. - generalize (Rplus_gt_compat_l (-1) (IZR (up r)) r H); intro; - rewrite (Rplus_comm (-1) (IZR (up r))) in H1; - generalize (Rplus_gt_compat_l (- r) (IZR (up r) + -1) (-1 + r) H1); - intro; clear H H0 H1; rewrite (Rplus_comm (- r) (IZR (up r) + -1)) in H2; - fold (IZR (up r) - 1) in H2; fold (IZR (up r) - 1 - r) in H2; - rewrite (Rplus_comm (- r) (-1 + r)) in H2; - rewrite (Rplus_assoc (-1) r (- r)) in H2; rewrite (Rplus_opp_r r) in H2; - elim (Rplus_ne (-1)); intros a b; rewrite a in H2; - clear a b; auto with zarith real. + apply Rminus_le. + replace (IZR (up r) - 1 - r) with (IZR (up r) - r - 1) by ring. + now apply Rle_minus. + apply Rminus_gt. + replace (IZR (up r) - 1 - r - -1) with (IZR (up r) - r) by ring. + now apply Rgt_minus. Qed. (**********) @@ -240,7 +231,6 @@ Proof. clear a b; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H; cut (1 = IZR 1); auto with zarith real. - intro; rewrite H1 in H; clear H1; rewrite <- (plus_IZR (Int_part r1 - Int_part r2) 1) in H; generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2) H0 H); intros; clear H H0; unfold Int_part at 1; @@ -324,12 +314,12 @@ Proof. rewrite (Rplus_opp_r (IZR (Int_part r1) - IZR (Int_part r2))) in H0; elim (Rplus_ne (r1 - r2)); intros a b; rewrite b in H0; clear a b; rewrite <- (Rplus_opp_l 1) in H0; - rewrite <- (Rplus_assoc (IZR (Int_part r1) - IZR (Int_part r2)) (-1) 1) + rewrite <- (Rplus_assoc (IZR (Int_part r1) - IZR (Int_part r2)) (-(1)) 1) in H0; fold (IZR (Int_part r1) - IZR (Int_part r2) - 1) in H0; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H; - cut (1 = IZR 1); auto with zarith real. - intro; rewrite H1 in H; rewrite H1 in H0; clear H1; + auto with zarith real. + change (_ + -1) with (IZR (Int_part r1 - Int_part r2) - 1) in H; rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H; rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H0; rewrite <- (plus_IZR (Int_part r1 - Int_part r2 - 1) 1) in H0; @@ -376,7 +366,7 @@ Proof. rewrite (Ropp_involutive (IZR 1)); rewrite (Ropp_involutive (IZR (Int_part r2))); rewrite (Ropp_plus_distr (IZR (Int_part r1))); - rewrite (Ropp_involutive (IZR (Int_part r2))); change (IZR 1) with 1; + rewrite (Ropp_involutive (IZR (Int_part r2))); simpl; rewrite <- (Rplus_assoc (r1 + - r2) (- IZR (Int_part r1) + IZR (Int_part r2)) 1) ; rewrite (Rplus_assoc r1 (- r2) (- IZR (Int_part r1) + IZR (Int_part r2))); @@ -442,9 +432,9 @@ Proof. in H0; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H0; elim (Rplus_ne (r1 + r2)); intros a b; rewrite b in H0; clear a b; + change 2 with (1 + 1) in H0; rewrite <- (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2)) 1 1) in H0; - cut (1 = IZR 1); auto with zarith real. - intro; rewrite H1 in H0; rewrite H1 in H; clear H1; + auto with zarith real. rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H; rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0; rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H; @@ -509,7 +499,6 @@ Proof. intros a b; rewrite a in H0; clear a b; elim (Rplus_ne (r1 + r2)); intros a b; rewrite b in H0; clear a b; cut (1 = IZR 1); auto with zarith real. - intro; rewrite H in H1; clear H; rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0; rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H1; rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H1; @@ -536,7 +525,7 @@ Proof. rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2))); unfold Rminus; rewrite - (Rplus_assoc (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))) (-1)) + (Rplus_assoc (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))) (-(1))) ; rewrite <- (Ropp_plus_distr (IZR (Int_part r1) + IZR (Int_part r2)) 1); trivial with zarith real. Qed. diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index 5c975c3f5..0c1e0b7e8 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -420,10 +420,10 @@ Proof. rewrite (Rmult_comm (/ a)). rewrite Rmult_assoc. rewrite <- Rinv_mult_distr. - replace (2 * (2 * a) * a) with (Rsqr (2 * a)). + replace (4 * a * a) with (Rsqr (2 * a)). reflexivity. ring_Rsqr. - rewrite <- Rmult_assoc; apply prod_neq_R0; + apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ]. apply (cond_nonzero a). assumption. diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 0254218c4..27cb356a0 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -88,17 +88,11 @@ Proof. right; unfold Rdiv. repeat rewrite Rabs_mult. rewrite Rabs_Rinv; discrR. - replace (Rabs 8) with 8. - replace 8 with 8; [ idtac | ring ]. - rewrite Rinv_mult_distr; [ idtac | discrR | discrR ]. - replace (2 * / Rabs (f2 x) * (Rabs eps * Rabs (f2 x) * (/ 2 * / 4))) with - (Rabs eps * / 4 * (2 * / 2) * (Rabs (f2 x) * / Rabs (f2 x))); - [ idtac | ring ]. - replace (Rabs eps) with eps. - repeat rewrite <- Rinv_r_sym; try discrR || (apply Rabs_no_R0; assumption). - ring. - symmetry ; apply Rabs_right; left; assumption. - symmetry ; apply Rabs_right; left; prove_sup. + rewrite (Rabs_pos_eq 8) by now apply IZR_le. + rewrite (Rabs_pos_eq eps). + field. + now apply Rabs_no_R0. + now apply Rlt_le. Qed. Lemma maj_term2 : diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v index 4e88714d6..d4597aeba 100644 --- a/theories/Reals/Ranalysis3.v +++ b/theories/Reals/Ranalysis3.v @@ -201,8 +201,8 @@ Proof. apply Rabs_pos_lt. unfold Rdiv, Rsqr; repeat rewrite Rmult_assoc. repeat apply prod_neq_R0; try assumption. - red; intro; rewrite H15 in H6; elim (Rlt_irrefl _ H6). - apply Rinv_neq_0_compat; repeat apply prod_neq_R0; discrR || assumption. + now apply Rgt_not_eq. + apply Rinv_neq_0_compat; apply prod_neq_R0; [discrR | assumption]. apply H13. split. apply D_x_no_cond; assumption. @@ -213,8 +213,7 @@ Proof. red; intro; rewrite H11 in H6; elim (Rlt_irrefl _ H6). assumption. assumption. - apply Rinv_neq_0_compat; repeat apply prod_neq_R0; - [ discrR | discrR | discrR | assumption ]. + apply Rinv_neq_0_compat; apply prod_neq_R0; [discrR | assumption]. (***********************************) (* Third case *) (* (f1 x)<>0 l1=0 l2=0 *) @@ -224,11 +223,11 @@ Proof. elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x)))); [ idtac | apply Rabs_pos_lt; unfold Rdiv, Rsqr; repeat rewrite Rmult_assoc; - repeat apply prod_neq_R0; + repeat apply prod_neq_R0 ; [ assumption | assumption - | red; intro; rewrite H11 in H6; elim (Rlt_irrefl _ H6) - | apply Rinv_neq_0_compat; repeat apply prod_neq_R0; discrR || assumption ] ]. + | now apply Rgt_not_eq + | apply Rinv_neq_0_compat; apply prod_neq_R0; discrR || assumption ] ]. intros alp_f2d H12. cut (0 < Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d alp_f2d)). intro. @@ -295,8 +294,10 @@ Proof. elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x)))); [ idtac | apply Rabs_pos_lt; unfold Rsqr, Rdiv; - repeat rewrite Rinv_mult_distr; repeat apply prod_neq_R0; - try assumption || discrR ]. + repeat apply prod_neq_R0 ; + [ assumption.. + | now apply Rgt_not_eq + | apply Rinv_neq_0_compat; apply prod_neq_R0; discrR || assumption ] ]. intros alp_f2d H11. assert (H12 := derivable_continuous_pt _ _ X). unfold continuity_pt in H12. @@ -380,15 +381,9 @@ Proof. repeat apply prod_neq_R0; try assumption. red; intro H18; rewrite H18 in H6; elim (Rlt_irrefl _ H6). apply Rinv_neq_0_compat; discrR. - apply Rinv_neq_0_compat; discrR. - apply Rinv_neq_0_compat; discrR. apply Rinv_neq_0_compat; assumption. apply Rinv_neq_0_compat; assumption. discrR. - discrR. - discrR. - discrR. - discrR. apply prod_neq_R0; [ discrR | assumption ]. elim H13; intros. apply H19. @@ -408,16 +403,9 @@ Proof. repeat apply prod_neq_R0; try assumption. red; intro H13; rewrite H13 in H6; elim (Rlt_irrefl _ H6). apply Rinv_neq_0_compat; discrR. - apply Rinv_neq_0_compat; discrR. - apply Rinv_neq_0_compat; discrR. apply Rinv_neq_0_compat; assumption. apply Rinv_neq_0_compat; assumption. apply prod_neq_R0; [ discrR | assumption ]. - red; intro H11; rewrite H11 in H6; elim (Rlt_irrefl _ H6). - apply Rinv_neq_0_compat; discrR. - apply Rinv_neq_0_compat; discrR. - apply Rinv_neq_0_compat; discrR. - apply Rinv_neq_0_compat; assumption. (***********************************) (* Fifth case *) (* (f1 x)<>0 l1<>0 l2=0 *) diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index d172139f5..f9da88aad 100644 --- a/theories/Reals/Ranalysis5.v +++ b/theories/Reals/Ranalysis5.v @@ -249,8 +249,10 @@ assert (Sublemma : forall x y lb ub, lb <= x <= ub /\ lb <= y <= ub -> lb <= (x+ split. replace lb with ((lb + lb) * /2) by field. unfold Rdiv ; apply Rmult_le_compat_r ; intuition. + now apply Rlt_le, Rinv_0_lt_compat, IZR_lt. replace ub with ((ub + ub) * /2) by field. unfold Rdiv ; apply Rmult_le_compat_r ; intuition. + now apply Rlt_le, Rinv_0_lt_compat, IZR_lt. intros x y P N x_lt_y. induction N. simpl ; intuition. @@ -1030,6 +1032,7 @@ intros x ub lb lb_lt_x x_lt_ub. assert (T : 0 < ub - lb). fourier. unfold Rdiv ; apply Rlt_mult_inv_pos ; intuition. +now apply IZR_lt. Qed. Definition mkposreal_lb_ub (x lb ub:R) (lb_lt_x:lb<x) (x_lt_ub:x<ub) : posreal. @@ -1102,7 +1105,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn rewrite <- Rmult_1_r ; replace 1 with (derive_pt id c (pr2 c P)) by reg. replace (- (fn N (x + h) - fn N x)) with (fn N x - fn N (x + h)) by field. assumption. - solve[apply Rlt_not_eq ; intuition]. + now apply Rlt_not_eq, IZR_lt. rewrite <- Hc'; clear Hc Hc'. replace (derive_pt (fn N) c (pr1 c P)) with (fn' N c). replace (h * fn' N c - h * g x) with (h * (fn' N c - g x)) by field. diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v index d9aa6b859..3e5362efe 100644 --- a/theories/Reals/Ratan.v +++ b/theories/Reals/Ratan.v @@ -132,7 +132,7 @@ intros [ | N] Npos n decr to0 cv nN. 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, Ropp_mult_distr_l_reverse; fourier. + unfold tg_alt at 2; rewrite pow_1_odd; fourier. 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. @@ -161,7 +161,6 @@ 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. - rewrite Ropp_mult_distr_l_reverse. intros [A B]; rewrite Rabs_pos_eq; fourier. apply Rle_trans with (f 1%nat). apply (Hyp 1%nat (le_n 1) (S n) decr to0 cv). @@ -320,31 +319,12 @@ apply PI2_lower_bound;[split; fourier | ]. destruct (pre_cos_bound (3/2) 1) as [t _]; [fourier | fourier | ]. apply Rlt_le_trans with (2 := t); clear t. unfold cos_approx; simpl; unfold cos_term. -simpl mult; replace ((-1)^ 0) with 1 by ring; replace ((-1)^2) with 1 by ring; - replace ((-1)^4) with 1 by ring; replace ((-1)^1) with (-1) by ring; - replace ((-1)^3) with (-1) by ring; change 3 with (IZR 3); - change 2 with (IZR 2); simpl Z.of_nat; - rewrite !INR_IZR_INZ, Ropp_mult_distr_l_reverse, Rmult_1_l. -match goal with |- _ < ?a => -replace a with ((- IZR 3 ^ 6 * IZR (Z.of_nat (fact 0)) * IZR (Z.of_nat (fact 2)) * - IZR (Z.of_nat (fact 4)) + - IZR 3 ^ 4 * IZR 2 ^ 2 * IZR (Z.of_nat (fact 0)) * IZR (Z.of_nat (fact 2)) * - IZR (Z.of_nat (fact 6)) - - IZR 3 ^ 2 * IZR 2 ^ 4 * IZR (Z.of_nat (fact 0)) * IZR (Z.of_nat (fact 4)) * - IZR (Z.of_nat (fact 6)) + - IZR 2 ^ 6 * IZR (Z.of_nat (fact 2)) * IZR (Z.of_nat (fact 4)) * - IZR (Z.of_nat (fact 6))) / - (IZR 2 ^ 6 * IZR (Z.of_nat (fact 0)) * IZR (Z.of_nat (fact 2)) * - IZR (Z.of_nat (fact 4)) * IZR (Z.of_nat (fact 6))));[ | field; - repeat apply conj;((rewrite <- INR_IZR_INZ; apply INR_fact_neq_0) || - (apply Rgt_not_eq; apply (IZR_lt 0); reflexivity)) ] -end. -rewrite !fact_simpl, !Nat2Z.inj_mul; simpl Z.of_nat. -unfold Rdiv; apply Rmult_lt_0_compat. -unfold Rminus; rewrite !pow_IZR, <- !opp_IZR, <- !mult_IZR, <- !opp_IZR, - <- !plus_IZR; apply (IZR_lt 0); reflexivity. -apply Rinv_0_lt_compat; rewrite !pow_IZR, <- !mult_IZR; apply (IZR_lt 0). -reflexivity. +unfold INR. +simpl. +field_simplify. +change (0 */ 1 < 9925632 / 141557760). +rewrite Rmult_0_l. +apply Rdiv_lt_0_compat ; now apply IZR_lt. Qed. Lemma PI2_1 : 1 < PI/2. @@ -502,11 +482,11 @@ split. rewrite (Rmult_comm (-1)); simpl ((/(Rabs y + 1)) ^ 0). unfold Rdiv; rewrite Rinv_1, !Rmult_assoc, <- !Rmult_plus_distr_l. apply tmp;[assumption | ]. - rewrite Rplus_assoc, Rmult_1_l; pattern 1 at 3; rewrite <- Rplus_0_r. + rewrite Rplus_assoc, Rmult_1_l; pattern 1 at 2; rewrite <- Rplus_0_r. apply Rplus_lt_compat_l. rewrite <- Rmult_assoc. match goal with |- (?a * (-1)) + _ < 0 => - rewrite <- (Rplus_opp_l a), Ropp_mult_distr_r_reverse, Rmult_1_r + rewrite <- (Rplus_opp_l a); change (-1) with (-(1)); rewrite Ropp_mult_distr_r_reverse, Rmult_1_r end. apply Rplus_lt_compat_l. assert (0 < u ^ 2) by (apply pow_lt; assumption). @@ -1078,8 +1058,9 @@ apply Rlt_not_eq; apply Rle_lt_trans with 0;[ | apply Rlt_0_1]. assert (t := pow2_ge_0 x); fourier. 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, Ropp_mult_distr_l_reverse, Rmult_1_l. -reflexivity. +rewrite pow_mult, <- Rpow_mult_distr. +f_equal. +ring. Qed. Lemma Datan_seq_increasing : forall x y n, (n > 0)%nat -> 0 <= x < y -> Datan_seq x n < Datan_seq y n. @@ -1167,6 +1148,7 @@ assert (tool : forall a b, a / b - /b = (-1 + a) /b). reflexivity. set (u := 1 + x ^ 2); rewrite tool; unfold Rminus; rewrite <- Rplus_assoc. unfold Rdiv, u. +change (-1) with (-(1)). rewrite Rplus_opp_l, Rplus_0_l, Ropp_mult_distr_l_reverse, Rabs_Ropp. rewrite Rabs_mult; clear tool u. assert (tool : forall k, Rabs ((-x ^ 2) ^ k) = Rabs ((x ^ 2) ^ k)). diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index e9098104c..7f9db3b18 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -115,35 +115,6 @@ Arguments INR n%nat. (**********************************************************) -(** * Injection from [Z] to [R] *) -(**********************************************************) - -(* compact representation for 2*p *) -Fixpoint IPR_2 (p:positive) : R := - match p with - | xH => 1 + 1 - | xO p => (1 + 1) * IPR_2 p - | xI p => (1 + 1) * (1 + IPR_2 p) - end. - -Definition IPR (p:positive) : R := - match p with - | xH => 1 - | xO p => IPR_2 p - | xI p => 1 + IPR_2 p - end. -Arguments IPR p%positive : simpl never. - -(**********) -Definition IZR (z:Z) : R := - match z with - | Z0 => 0 - | Zpos n => IPR n - | Zneg n => - IPR n - end. -Arguments IZR z%Z : simpl never. - -(**********************************************************) (** * [R] Archimedean *) (**********************************************************) diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index fe5402e6e..df1662497 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -451,20 +451,16 @@ Qed. Lemma Rabs_Ropp : forall x:R, Rabs (- x) = Rabs x. Proof. - intro; cut (- x = -1 * x). - intros; rewrite H. + intro; replace (-x) with (-1 * x) by ring. rewrite Rabs_mult. - cut (Rabs (-1) = 1). - intros; rewrite H0. - ring. + replace (Rabs (-1)) with 1. + apply Rmult_1_l. unfold Rabs; case (Rcase_abs (-1)). intro; ring. - intro H0; generalize (Rge_le (-1) 0 H0); intros. - generalize (Ropp_le_ge_contravar 0 (-1) H1). - rewrite Ropp_involutive; rewrite Ropp_0. - intro; generalize (Rgt_not_le 1 0 Rlt_0_1); intro; generalize (Rge_le 0 1 H2); - intro; exfalso; auto. - ring. + rewrite <- Ropp_0. + intro H0; apply Ropp_ge_cancel in H0. + elim (Rge_not_lt _ _ H0). + apply Rlt_0_1. Qed. (*********) diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index f3f8f7409..cb5dea93a 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -69,3 +69,32 @@ Notation "x <= y <= z" := (x <= y /\ y <= z) : R_scope. Notation "x <= y < z" := (x <= y /\ y < z) : R_scope. Notation "x < y < z" := (x < y /\ y < z) : R_scope. Notation "x < y <= z" := (x < y /\ y <= z) : R_scope. + +(**********************************************************) +(** * Injection from [Z] to [R] *) +(**********************************************************) + +(* compact representation for 2*p *) +Fixpoint IPR_2 (p:positive) : R := + match p with + | xH => R1 + R1 + | xO p => (R1 + R1) * IPR_2 p + | xI p => (R1 + R1) * (R1 + IPR_2 p) + end. + +Definition IPR (p:positive) : R := + match p with + | xH => R1 + | xO p => IPR_2 p + | xI p => R1 + IPR_2 p + end. +Arguments IPR p%positive : simpl never. + +(**********) +Definition IZR (z:Z) : R := + match z with + | Z0 => R0 + | Zpos n => IPR n + | Zneg n => - IPR n + end. +Arguments IZR z%Z : simpl never. diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 0a49d4983..99acdd0a1 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -416,8 +416,9 @@ Proof. simpl; apply Rabs_R1. replace (S n) with (n + 1)%nat; [ rewrite pow_add | ring ]. rewrite Rabs_mult. - rewrite Hrecn; rewrite Rmult_1_l; simpl; rewrite Rmult_1_r; - rewrite Rabs_Ropp; apply Rabs_R1. + rewrite Hrecn; rewrite Rmult_1_l; simpl; rewrite Rmult_1_r. + change (-1) with (-(1)). + rewrite Rabs_Ropp; apply Rabs_R1. Qed. Lemma pow_mult : forall (x:R) (n1 n2:nat), x ^ (n1 * n2) = (x ^ n1) ^ n2. diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v index 7bd6c916d..b9a9458c8 100644 --- a/theories/Reals/Rlogic.v +++ b/theories/Reals/Rlogic.v @@ -82,7 +82,7 @@ assert (HN: (INR N + 1 = IZR (up (/ l)) - 1)%R). apply Rle_lt_trans with (1 := H1l). apply archimed. rewrite minus_IZR. - change (IZR 2) with 2%R. + simpl. ring. assert (Hl': (/ (INR (S N) + 1) < l)%R). rewrite <- (Rinv_involutive l) by now apply Rgt_not_eq. diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v index 791718a45..f331bb203 100644 --- a/theories/Reals/Rpow_def.v +++ b/theories/Reals/Rpow_def.v @@ -10,6 +10,6 @@ Require Import Rdefinitions. Fixpoint pow (r:R) (n:nat) : R := match n with - | O => R1 + | O => 1 | S n => Rmult r (pow r n) end. diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index a053c349e..f62ed2a6c 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -488,12 +488,9 @@ Proof. rewrite Rinv_r. apply exp_lt_inv. apply Rle_lt_trans with (1 := exp_le_3). - change (3 < 2 ^R 2). + change (3 < 2 ^R (1 + 1)). repeat rewrite Rpower_plus; repeat rewrite Rpower_1. - repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l; - repeat rewrite Rmult_1_l. - pattern 3 at 1; rewrite <- Rplus_0_r; replace (2 + 2) with (3 + 1); - [ apply Rplus_lt_compat_l; apply Rlt_0_1 | ring ]. + now apply (IZR_lt 3 4). prove_sup0. discrR. Qed. @@ -715,7 +712,7 @@ Definition arcsinh x := ln (x + sqrt (x ^ 2 + 1)). Lemma arcsinh_sinh : forall x, arcsinh (sinh x) = x. intros x; unfold sinh, arcsinh. assert (Rminus_eq_0 : forall r, r - r = 0) by (intros; ring). -pattern 1 at 5; rewrite <- exp_0, <- (Rminus_eq_0 x); unfold Rminus. +rewrite <- exp_0, <- (Rminus_eq_0 x); unfold Rminus. rewrite exp_plus. match goal with |- context[sqrt ?a] => replace a with (((exp x + exp(-x))/2)^2) by field diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 744fd6641..c6b0c3f37 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -207,7 +207,7 @@ Section sequence. assert (Rabs (/2) < 1). rewrite Rabs_pos_eq. - rewrite <- Rinv_1 at 3. + rewrite <- Rinv_1. apply Rinv_lt_contravar. rewrite Rmult_1_l. now apply (IZR_lt 0 2). diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v index 6b1754021..48dbd1944 100644 --- a/theories/Reals/Rtrigo1.v +++ b/theories/Reals/Rtrigo1.v @@ -182,13 +182,11 @@ destruct (pre_cos_bound _ 0 lo up) as [_ upper]. apply Rle_lt_trans with (1 := upper). apply Rlt_le_trans with (2 := lower). unfold cos_approx, sin_approx. -simpl sum_f_R0; change 7 with (IZR 7). -change 8 with (IZR 8). +simpl sum_f_R0. unfold cos_term, sin_term; simpl fact; rewrite !INR_IZR_INZ. -simpl plus; simpl mult. -field_simplify; - try (repeat apply conj; apply not_eq_sym, Rlt_not_eq, (IZR_lt 0); reflexivity). -unfold Rminus; rewrite !pow_IZR, <- !mult_IZR, <- !opp_IZR, <- ?plus_IZR. +simpl plus; simpl mult; simpl Z_of_nat. +field_simplify. +change (8073344 / 12582912 < 18760 / 24576). match goal with |- IZR ?a / ?b < ?c / ?d => apply Rmult_lt_reg_r with d;[apply (IZR_lt 0); reflexivity | @@ -323,6 +321,7 @@ Lemma sin_PI : sin PI = 0. Proof. assert (H := sin2_cos2 PI). rewrite cos_PI in H. + change (-1) with (-(1)) in H. rewrite <- Rsqr_neg in H. rewrite Rsqr_1 in H. cut (Rsqr (sin PI) = 0). @@ -533,9 +532,8 @@ Qed. Lemma sin_PI_x : forall x:R, sin (PI - x) = sin x. Proof. - intro x; rewrite sin_minus; rewrite sin_PI; rewrite cos_PI; rewrite Rmult_0_l; - unfold Rminus in |- *; rewrite Rplus_0_l; rewrite Ropp_mult_distr_l_reverse; - rewrite Ropp_involutive; apply Rmult_1_l. + intro x; rewrite sin_minus; rewrite sin_PI; rewrite cos_PI. + ring. Qed. Lemma sin_period : forall (x:R) (k:nat), sin (x + 2 * INR k * PI) = sin x. @@ -593,9 +591,9 @@ Proof. generalize (Rsqr_incrst_1 1 (sin x) H (Rlt_le 0 1 Rlt_0_1) (Rlt_le 0 (sin x) (Rlt_trans 0 1 (sin x) Rlt_0_1 H))); - rewrite Rsqr_1; intro; rewrite sin2 in H0; unfold Rminus in H0; + rewrite Rsqr_1; intro; rewrite sin2 in H0; unfold Rminus in H0. generalize (Rplus_lt_compat_l (-1) 1 (1 + - Rsqr (cos x)) H0); - repeat rewrite <- Rplus_assoc; repeat rewrite Rplus_opp_l; + repeat rewrite <- Rplus_assoc; change (-1) with (-(1)); rewrite Rplus_opp_l; rewrite Rplus_0_l; intro; rewrite <- Ropp_0 in H1; generalize (Ropp_lt_gt_contravar (-0) (- Rsqr (cos x)) H1); repeat rewrite Ropp_involutive; intro; generalize (Rle_0_sqr (cos x)); @@ -603,6 +601,7 @@ Proof. auto with real. cut (sin x < -1). intro; generalize (Ropp_lt_gt_contravar (sin x) (-1) H); + change (-1) with (-(1)); rewrite Ropp_involutive; clear H; intro; generalize (Rsqr_incrst_1 1 (- sin x) H (Rlt_le 0 1 Rlt_0_1) @@ -610,7 +609,7 @@ Proof. rewrite Rsqr_1; intro; rewrite <- Rsqr_neg in H0; rewrite sin2 in H0; unfold Rminus in H0; generalize (Rplus_lt_compat_l (-1) 1 (1 + - Rsqr (cos x)) H0); - repeat rewrite <- Rplus_assoc; repeat rewrite Rplus_opp_l; + rewrite <- Rplus_assoc; change (-1) with (-(1)); rewrite Rplus_opp_l; rewrite Rplus_0_l; intro; rewrite <- Ropp_0 in H1; generalize (Ropp_lt_gt_contravar (-0) (- Rsqr (cos x)) H1); repeat rewrite Ropp_involutive; intro; generalize (Rle_0_sqr (cos x)); @@ -712,17 +711,16 @@ Proof. do 2 rewrite fact_simpl; do 2 rewrite mult_INR. repeat rewrite <- Rmult_assoc. rewrite <- (Rmult_comm (INR (fact (2 * n + 1)))). - rewrite Rmult_assoc. apply Rmult_lt_compat_l. apply lt_INR_0; apply neq_O_lt. assert (H2 := fact_neq_0 (2 * n + 1)). red in |- *; intro; elim H2; symmetry in |- *; assumption. do 2 rewrite S_INR; rewrite plus_INR; rewrite mult_INR; set (x := INR n); unfold INR in |- *. - replace ((2 * x + 1 + 1 + 1) * (2 * x + 1 + 1)) with (4 * x * x + 10 * x + 6); + replace (((1 + 1) * x + 1 + 1 + 1) * ((1 + 1) * x + 1 + 1)) with (4 * x * x + 10 * x + 6); [ idtac | ring ]. - apply Rplus_lt_reg_l with (-4); rewrite Rplus_opp_l; - replace (-4 + (4 * x * x + 10 * x + 6)) with (4 * x * x + 10 * x + 2); + apply Rplus_lt_reg_l with (-(4)); rewrite Rplus_opp_l; + replace (-(4) + (4 * x * x + 10 * x + 6)) with (4 * x * x + 10 * x + 2); [ idtac | ring ]. apply Rplus_le_lt_0_compat. cut (0 <= x). @@ -767,7 +765,7 @@ Proof. unfold Rdiv in |- *; pattern PI at 2 in |- *; rewrite <- Rmult_1_r. apply Rmult_lt_compat_l. apply PI_RGT_0. - pattern 1 at 3 in |- *; rewrite <- Rinv_1; apply Rinv_lt_contravar. + rewrite <- Rinv_1; apply Rinv_lt_contravar. rewrite Rmult_1_l; prove_sup0. pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; apply Rlt_0_1. @@ -1715,7 +1713,7 @@ Proof. rewrite H5. rewrite mult_INR. simpl in |- *. - rewrite <- (Rplus_0_l (2 * INR x2 * PI)). + rewrite <- (Rplus_0_l ((1 + 1) * INR x2 * PI)). rewrite sin_period. apply sin_0. rewrite H5. @@ -1725,7 +1723,7 @@ Proof. rewrite Rmult_1_l; rewrite sin_plus. rewrite sin_PI. rewrite Rmult_0_r. - rewrite <- (Rplus_0_l (2 * INR x2 * PI)). + rewrite <- (Rplus_0_l ((1 + 1) * INR x2 * PI)). rewrite sin_period. rewrite sin_0; ring. apply le_IZR. @@ -1747,7 +1745,7 @@ Proof. rewrite H5. rewrite mult_INR. simpl in |- *. - rewrite <- (Rplus_0_l (2 * INR x2 * PI)). + rewrite <- (Rplus_0_l ((1 + 1) * INR x2 * PI)). rewrite sin_period. rewrite sin_0; ring. rewrite H5. @@ -1757,7 +1755,7 @@ Proof. rewrite Rmult_1_l; rewrite sin_plus. rewrite sin_PI. rewrite Rmult_0_r. - rewrite <- (Rplus_0_l (2 * INR x2 * PI)). + rewrite <- (Rplus_0_l ((1 + 1) * INR x2 * PI)). rewrite sin_period. rewrite sin_0; ring. apply le_IZR. @@ -1798,7 +1796,7 @@ Lemma cos_eq_0_0 (x:R) : Proof. rewrite cos_sin. intros Hx. destruct (sin_eq_0_0 (PI/2 + x) Hx) as (k,Hk). clear Hx. - exists (k-1)%Z. rewrite <- Z_R_minus; change (IZR 1) with 1. + exists (k-1)%Z. rewrite <- Z_R_minus; simpl. symmetry in Hk. field_simplify [Hk]. field. Qed. diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index a5092d22d..092bc30d0 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -320,7 +320,7 @@ Proof. (1 - sum_f_R0 (fun i:nat => cos_n i * Rsqr a0 ^ i) (S n1)). unfold Rminus; rewrite Ropp_plus_distr; rewrite Ropp_involutive; repeat rewrite Rplus_assoc; rewrite (Rplus_comm 1); - rewrite (Rplus_comm (-1)); repeat rewrite Rplus_assoc; + rewrite (Rplus_comm (-(1))); repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; rewrite <- Rabs_Ropp; rewrite Ropp_plus_distr; rewrite Ropp_involutive; unfold Rminus in H6; apply H6. @@ -367,10 +367,10 @@ Proof. reflexivity. ring. intro; elim H2; intros; split. - apply Rplus_le_reg_l with (-1). + apply Rplus_le_reg_l with (-(1)). rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; rewrite (Rplus_comm (-1)); apply H3. - apply Rplus_le_reg_l with (-1). + apply Rplus_le_reg_l with (-(1)). rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; rewrite (Rplus_comm (-1)); apply H4. unfold cos_term; simpl; unfold Rdiv; rewrite Rinv_1; diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index 4a1e3179c..d9c18d358 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -251,6 +251,7 @@ Proof. exists delta; intros. rewrite Rplus_0_l; replace (cos h - cos 0) with (-2 * Rsqr (sin (h / 2))). unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r. + change (-2) with (-(2)). unfold Rdiv; do 2 rewrite Ropp_mult_distr_l_reverse. rewrite Rabs_Ropp. replace (2 * Rsqr (sin (h * / 2)) * / h) with @@ -266,7 +267,7 @@ Proof. apply Rabs_pos. assert (H9 := SIN_bound (h / 2)). unfold Rabs; case (Rcase_abs (sin (h / 2))); intro. - pattern 1 at 3; rewrite <- (Ropp_involutive 1). + rewrite <- (Ropp_involutive 1). apply Ropp_le_contravar. elim H9; intros; assumption. elim H9; intros; assumption. diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index d43baee8c..12d5cbbf0 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -21,6 +21,7 @@ Proof. destruct (total_order_T h 0) as [[Hlt|Heq]|Hgt]. repeat rewrite Rabs_left. unfold Rminus; do 2 rewrite <- (Rplus_comm (-1)). + change (-1) with (-(1)). do 2 rewrite Ropp_plus_distr; rewrite Ropp_involutive; apply Rplus_le_compat_l. apply Ropp_le_contravar; apply sqrt_le_1. |