diff options
| author | Maxime Dénès | 2017-03-22 22:37:27 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-22 22:37:27 +0100 |
| commit | 7050ab7a246d5614e6d16f546bc8197e689e4bd7 (patch) | |
| tree | 09194e01667b08833bac60d2be5d9979cedb08ce | |
| parent | 947d93a8b7ff0fc7ba23633fcd44820427e29326 (diff) | |
| parent | 4f4b9d04bc59dc1f3b6962b0b077ba274638efc7 (diff) | |
Merge PR#415: Use a compact representation for real literals
37 files changed, 446 insertions, 985 deletions
@@ -7,7 +7,7 @@ Tactics functional extensionality in H supposed to be a quantified equality until giving a bare equality. -Libraries +Standard Library - New file PropExtensionality.v to explicitly work in the axiomatic context of propositional extensionality. @@ -16,6 +16,12 @@ Libraries Various proof-theoretic characterizations of choice over setoids in file ChoiceFacts.v. +- IZR (Reals) has been changed to produce a compact representation of + integers. As a consequence, IZR is no longer convertible to INR and + lemmas such as INR_IZR_INZ should be used instead. +- Real constants are now represented using IZR rather than R0 and R1; + this might cause rewriting rules to fail to apply to constants. + Changes from V8.6beta1 to V8.6 ============================== diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex index 0664bf9095..77d5928345 100644 --- a/doc/refman/Polynom.tex +++ b/doc/refman/Polynom.tex @@ -342,16 +342,16 @@ describes their syntax and effects: By default the tactic does not recognize power expressions as ring expressions. \item[sign {\term}] allows {\tt ring\_simplify} to use a minus operation - when outputing its normal form, i.e writing $x - y$ instead of $x + (-y)$. + when outputting its normal form, i.e writing $x - y$ instead of $x + (-y)$. The term {\term} is a proof that a given sign function indicates expressions that are signed ({\term} has to be a - proof of {\tt Ring\_theory.get\_sign}). See {\tt plugins/setoid\_ring/IntialRing.v} for examples of sign function. -\item[div {\term}] allows {\tt ring} and {\tt ring\_simplify} to use moniomals + proof of {\tt Ring\_theory.get\_sign}). See {\tt plugins/setoid\_ring/InitialRing.v} for examples of sign function. +\item[div {\term}] allows {\tt ring} and {\tt ring\_simplify} to use monomials with coefficient other than 1 in the rewriting. The term {\term} is a proof that a given division function satisfies the specification of an euclidean division function ({\term} has to be a proof of {\tt Ring\_theory.div\_theory}). For example, this function is called when trying to rewrite $7x$ by $2x = z$ to tell that $7 = 3 * 2 + 1$. - See {\tt plugins/setoid\_ring/IntialRing.v} for examples of div function. + See {\tt plugins/setoid\_ring/InitialRing.v} for examples of div function. \end{description} diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v index 1d7ee93ea3..a962547131 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/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index 2352d78d63..30e475b710 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -18,7 +18,7 @@ Require Import Refl. Require Import Raxioms RIneq Rpow_def DiscrR. Require Import QArith. Require Import Qfield. - +Require Import Qreals. Require Setoid. (*Declare ML Module "micromega_plugin".*) @@ -38,15 +38,8 @@ Proof. exact Rplus_opp_r. Qed. -Add Ring Rring : Rsrt. Open Scope R_scope. -Lemma Rmult_neutral : forall x:R , 0 * x = 0. -Proof. - intro ; ring. -Qed. - - Lemma Rsor : SOR R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle Rlt. Proof. constructor; intros ; subst ; try (intuition (subst; try ring ; auto with real)). @@ -59,142 +52,41 @@ Proof. apply (Rlt_irrefl m) ; auto. apply Rnot_le_lt. auto with real. destruct (total_order_T n m) as [ [H1 | H1] | H1] ; auto. - intros. - rewrite <- (Rmult_neutral m). - apply (Rmult_lt_compat_r) ; auto. -Qed. - -Definition IQR := fun x : Q => (IZR (Qnum x) * / IZR (' Qden x))%R. - - -Lemma Rinv_elim : forall x y z, - y <> 0 -> (z * y = x <-> x * / y = z). -Proof. - intros. - split ; intros. - subst. - rewrite Rmult_assoc. - rewrite Rinv_r; auto. - ring. - subst. - rewrite Rmult_assoc. - rewrite (Rmult_comm (/ y)). - rewrite Rinv_r ; auto. - ring. -Qed. - -Ltac INR_nat_of_P := - match goal with - | H : context[INR (Pos.to_nat ?X)] |- _ => - revert H ; - let HH := fresh in - assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (Pos.to_nat X)) - | |- context[INR (Pos.to_nat ?X)] => - let HH := fresh in - assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (Pos.to_nat X)) - end. - -Ltac add_eq expr val := set (temp := expr) ; - generalize (eq_refl temp) ; - unfold temp at 1 ; generalize temp ; intro val ; clear temp. - -Ltac Rinv_elim := - match goal with - | |- context[?x * / ?y] => - let z := fresh "v" in - add_eq (x * / y) z ; - let H := fresh in intro H ; rewrite <- Rinv_elim in H - end. - -Lemma Rlt_neq : forall r , 0 < r -> r <> 0. -Proof. - red. intros. - subst. - apply (Rlt_irrefl 0 H). + now apply Rmult_lt_0_compat. Qed. +Notation IQR := Q2R (only parsing). Lemma Rinv_1 : forall x, x * / 1 = x. Proof. intro. - Rinv_elim. - subst ; ring. - apply R1_neq_R0. + rewrite Rinv_1. + apply Rmult_1_r. Qed. -Lemma Qeq_true : forall x y, - Qeq_bool x y = true -> - IQR x = IQR y. +Lemma Qeq_true : forall x y, Qeq_bool x y = true -> IQR x = IQR y. Proof. - unfold IQR. - simpl. - intros. - apply Qeq_bool_eq in H. - unfold Qeq in H. - assert (IZR (Qnum x * ' Qden y) = IZR (Qnum y * ' Qden x))%Z. - rewrite H. reflexivity. - repeat rewrite mult_IZR in H0. - simpl in H0. - revert H0. - repeat INR_nat_of_P. intros. - apply Rinv_elim in H2 ; [| apply Rlt_neq ; auto]. - rewrite <- H2. - field. - split ; apply Rlt_neq ; auto. + now apply Qeq_eqR, Qeq_bool_eq. Qed. Lemma Qeq_false : forall x y, Qeq_bool x y = false -> IQR x <> IQR y. Proof. intros. - apply Qeq_bool_neq in H. - intro. apply H. clear H. - unfold Qeq,IQR in *. - simpl in *. - revert H0. - repeat Rinv_elim. - intros. - subst. - assert (IZR (Qnum x * ' Qden y)%Z = IZR (Qnum y * ' Qden x)%Z). - repeat rewrite mult_IZR. - simpl. - rewrite <- H0. rewrite <- H. - ring. - apply eq_IZR ; auto. - INR_nat_of_P; intros; apply Rlt_neq ; auto. - INR_nat_of_P; intros ; apply Rlt_neq ; auto. + apply Qeq_bool_neq in H. + contradict H. + now apply eqR_Qeq. Qed. - - Lemma Qle_true : forall x y : Q, Qle_bool x y = true -> IQR x <= IQR y. Proof. intros. - apply Qle_bool_imp_le in H. - unfold Qle in H. - unfold IQR. - simpl in *. - apply IZR_le in H. - repeat rewrite mult_IZR in H. - simpl in H. - repeat INR_nat_of_P; intros. - assert (Hr := Rlt_neq r H). - assert (Hr0 := Rlt_neq r0 H0). - replace (IZR (Qnum x) * / r) with ((IZR (Qnum x) * r0) * (/r * /r0)). - replace (IZR (Qnum y) * / r0) with ((IZR (Qnum y) * r) * (/r * /r0)). - apply Rmult_le_compat_r ; auto. - apply Rmult_le_pos. - unfold Rle. left. apply Rinv_0_lt_compat ; auto. - unfold Rle. left. apply Rinv_0_lt_compat ; auto. - field ; intuition. - field ; intuition. + now apply Qle_Rle, Qle_bool_imp_le. Qed. - - Lemma IQR_0 : IQR 0 = 0. Proof. - compute. apply Rinv_1. + apply Rmult_0_l. Qed. Lemma IQR_1 : IQR 1 = 1. @@ -202,160 +94,6 @@ Proof. compute. apply Rinv_1. Qed. -Lemma IQR_plus : forall x y, IQR (x + y) = IQR x + IQR y. -Proof. - intros. - unfold IQR. - simpl in *. - rewrite plus_IZR in *. - rewrite mult_IZR in *. - simpl. - rewrite Pos2Nat.inj_mul. - rewrite mult_INR. - rewrite mult_IZR. - simpl. - repeat INR_nat_of_P. - intros. field. - split ; apply Rlt_neq ; auto. -Qed. - -Lemma IQR_opp : forall x, IQR (- x) = - IQR x. -Proof. - intros. - unfold IQR. - simpl. - rewrite opp_IZR. - ring. -Qed. - -Lemma IQR_minus : forall x y, IQR (x - y) = IQR x - IQR y. -Proof. - intros. - unfold Qminus. - rewrite IQR_plus. - rewrite IQR_opp. - ring. -Qed. - - -Lemma IQR_mult : forall x y, IQR (x * y) = IQR x * IQR y. -Proof. - unfold IQR ; intros. - simpl. - repeat rewrite mult_IZR. - rewrite Pos2Nat.inj_mul. - rewrite mult_INR. - repeat INR_nat_of_P. - intros. field ; split ; apply Rlt_neq ; auto. -Qed. - -Lemma IQR_inv_lt : forall x, (0 < x)%Q -> - IQR (/ x) = / IQR x. -Proof. - unfold IQR ; simpl. - intros. - unfold Qlt in H. - revert H. - simpl. - intros. - unfold Qinv. - destruct x. - destruct Qnum ; simpl in *. - exfalso. auto with zarith. - clear H. - repeat INR_nat_of_P. - intros. - assert (HH := Rlt_neq _ H). - assert (HH0 := Rlt_neq _ H0). - rewrite Rinv_mult_distr ; auto. - rewrite Rinv_involutive ; auto. - ring. - apply Rinv_0_lt_compat in H0. - apply Rlt_neq ; auto. - simpl in H. - exfalso. - rewrite Pos.mul_comm in H. - compute in H. - discriminate. -Qed. - -Lemma Qinv_opp : forall x, (- (/ x) = / ( -x))%Q. -Proof. - destruct x ; destruct Qnum ; reflexivity. -Qed. - -Lemma Qopp_involutive_strong : forall x, (- - x = x)%Q. -Proof. - intros. - destruct x. - unfold Qopp. - simpl. - rewrite Z.opp_involutive. - reflexivity. -Qed. - -Lemma Ropp_0 : forall r , - r = 0 -> r = 0. -Proof. - intros. - rewrite <- (Ropp_involutive r). - apply Ropp_eq_0_compat ; auto. -Qed. - -Lemma IQR_x_0 : forall x, IQR x = 0 -> x == 0%Q. -Proof. - destruct x ; simpl. - unfold IQR. - simpl. - INR_nat_of_P. - intros. - apply Rmult_integral in H0. - destruct H0. - apply eq_IZR_R0 in H0. - subst. - reflexivity. - exfalso. - apply Rinv_0_lt_compat in H. - rewrite <- H0 in H. - apply Rlt_irrefl in H. auto. -Qed. - - -Lemma IQR_inv_gt : forall x, (0 > x)%Q -> - IQR (/ x) = / IQR x. -Proof. - intros. - rewrite <- (Qopp_involutive_strong x). - rewrite <- Qinv_opp. - rewrite IQR_opp. - rewrite IQR_inv_lt. - repeat rewrite IQR_opp. - rewrite Ropp_inv_permute. - auto. - intro. - apply Ropp_0 in H0. - apply IQR_x_0 in H0. - rewrite H0 in H. - compute in H. discriminate. - unfold Qlt in *. - destruct x ; simpl in *. - auto with zarith. -Qed. - -Lemma IQR_inv : forall x, ~ x == 0 -> - IQR (/ x) = / IQR x. -Proof. - intros. - assert ( 0 > x \/ 0 < x)%Q. - destruct x ; unfold Qlt, Qeq in * ; simpl in *. - rewrite Z.mul_1_r in *. - destruct Qnum ; simpl in * ; intuition auto. - right. reflexivity. - left ; reflexivity. - destruct H0. - apply IQR_inv_gt ; auto. - apply IQR_inv_lt ; auto. -Qed. - Lemma IQR_inv_ext : forall x, IQR (/ x) = (if Qeq_bool x 0 then 0 else / IQR x). Proof. @@ -366,18 +104,13 @@ Proof. destruct x ; simpl. unfold Qeq in H. simpl in H. - replace Qnum with 0%Z. - compute. rewrite Rinv_1. - reflexivity. - rewrite <- H. ring. + rewrite Zmult_1_r in H. + rewrite H. + apply Rmult_0_l. intros. - apply IQR_inv. - intro. - rewrite <- Qeq_bool_iff in H0. - congruence. + now apply Q2R_inv, Qeq_bool_neq. Qed. - Notation to_nat := N.to_nat. Lemma QSORaddon : @@ -391,10 +124,10 @@ Proof. constructor ; intros ; try reflexivity. apply IQR_0. apply IQR_1. - apply IQR_plus. - apply IQR_minus. - apply IQR_mult. - apply IQR_opp. + apply Q2R_plus. + apply Q2R_minus. + apply Q2R_mult. + apply Q2R_opp. apply Qeq_true ; auto. apply R_power_theory. apply Qeq_false. @@ -453,13 +186,13 @@ Proof. apply IQR_1. reflexivity. unfold IQR. simpl. rewrite Rinv_1. reflexivity. - apply IQR_plus. - apply IQR_minus. - apply IQR_mult. + apply Q2R_plus. + apply Q2R_minus. + apply Q2R_mult. rewrite <- IHc. apply IQR_inv_ext. rewrite <- IHc. - apply IQR_opp. + apply Q2R_opp. Qed. Require Import EnvRing. diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 97f29df823..6051cb3d3c 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -364,6 +364,7 @@ struct [["Coq";"Reals" ; "Rdefinitions"]; ["Coq";"Reals" ; "Rpow_def"] ; ["Coq";"Reals" ; "Raxioms"] ; + ["Coq";"QArith"; "Qreals"] ; ] let z_modules = [["Coq";"ZArith";"BinInt"]] @@ -479,7 +480,7 @@ struct let coq_Rinv = lazy (r_constant "Rinv") let coq_Rpower = lazy (r_constant "pow") let coq_IZR = lazy (r_constant "IZR") - let coq_IQR = lazy (constant "IQR") + let coq_IQR = lazy (r_constant "Q2R") let coq_PEX = lazy (constant "PEX" ) diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v index 293722125b..facd2e0625 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/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index eb35d3f806..87ee666605 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -323,14 +323,16 @@ let _ = add_map "ring" (map_with_eq [coq_cons,(function -1->Eval|2->Rec|_->Prot); coq_nil, (function -1->Eval|_ -> Prot); + my_reference "IDphi", (function _->Eval); + my_reference "gen_phiZ", (function _->Eval); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); pol_cst "Pphi_pow", - (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); + (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot); (* PEeval: evaluate morphism and polynomial, protect ring operations and make recursive call on the var map *) - pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot)]) + pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot)]) (****************************************************************************) (* Ring database *) @@ -756,12 +758,14 @@ let _ = add_map "field" (map_with_eq [coq_cons,(function -1->Eval|2->Rec|_->Prot); coq_nil, (function -1->Eval|_ -> Prot); + my_reference "IDphi", (function _->Eval); + my_reference "gen_phiZ", (function _->Eval); (* display_linear: evaluate polynomials and coef operations, protect field operations and make recursive call on the var map *) my_reference "display_linear", (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot); my_reference "display_pow_linear", - (function -1|9|10|11|12|13|14|16|18|19->Eval|17->Rec|_->Prot); + (function -1|9|10|11|14|16|18|19->Eval|12|17->Rec|_->Prot); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); @@ -769,19 +773,20 @@ let _ = add_map "field" (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); (* PEeval: evaluate morphism and polynomial, protect ring operations and make recursive call on the var map *) - pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot); + pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot); (* FEeval: evaluate morphism, protect field operations and make recursive call on the var map *) - my_reference "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);; + my_reference "FEeval", (function -1|10|12|15->Eval|14->Rec|_->Prot)]);; let _ = add_map "field_cond" (map_without_eq [coq_cons,(function -1->Eval|2->Rec|_->Prot); coq_nil, (function -1->Eval|_ -> Prot); - (* PCond: evaluate morphism and denum list, protect ring + my_reference "IDphi", (function _->Eval); + my_reference "gen_phiZ", (function _->Eval); + (* PCond: evaluate denum list, protect ring operations and make recursive call on the var map *) - my_reference "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);; -(* (function -1|9|11->Eval|10->Rec|_->Prot)]);;*) + my_reference "PCond", (function -1|11|14->Eval|9|13->Rec|_->Prot)]);; let _ = Redexpr.declare_reduction "simpl_field_expr" diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 3ae2d45f32..8f065f5282 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/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v index 58f79d45ec..e569bcb49f 100644 --- a/test-suite/success/decl_mode.v +++ b/test-suite/success/decl_mode.v @@ -153,7 +153,7 @@ proof. thus ~= (IZR (Zneg z) * IZR (Zneg z)). end cases. end proof. -Qed. +Admitted. Definition irrational (x:R):Prop := forall (p:Z) (q:nat),q<>0%nat -> x<> (IZR p/INR q). diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index a98d529fa0..0e1608a32f 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 6fca9c8ad6..67584f7759 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -143,7 +143,7 @@ Proof. 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 4e2a7c3c6e..05911cd539 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 569518f7b8..e9de24898e 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 19db476fde..2d2385703b 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 379fee6f49..dd2108159f 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1743,24 +1743,40 @@ Proof. intros z; idtac; apply Z_of_nat_complete; assumption. Qed. +Lemma INR_IPR : forall p, INR (Pos.to_nat p) = IPR p. +Proof. + assert (H: forall p, 2 * INR (Pos.to_nat p) = IPR_2 p). + induction p as [p|p|] ; simpl IPR_2. + rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- IHp. + now rewrite (Rplus_comm (2 * _)). + now rewrite Pos2Nat.inj_xO, mult_INR, <- IHp. + apply Rmult_1_r. + intros [p|p|] ; unfold IPR. + rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- H. + apply Rplus_comm. + now rewrite Pos2Nat.inj_xO, mult_INR, <- H. + easy. +Qed. + (**********) Lemma INR_IZR_INZ : forall n:nat, INR n = IZR (Z.of_nat n). Proof. - simple induction n; auto with real. - intros; simpl; rewrite SuccNat2Pos.id_succ; - auto with real. + intros [|n]. + easy. + simpl Z.of_nat. unfold IZR. + now rewrite <- INR_IPR, SuccNat2Pos.id_succ. Qed. Lemma plus_IZR_NEG_POS : forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q). Proof. intros p q; simpl. rewrite Z.pos_sub_spec. - case Pos.compare_spec; intros H; simpl. + case Pos.compare_spec; intros H; unfold IZR. subst. ring. - rewrite Pos2Nat.inj_sub by trivial. + rewrite <- 3!INR_IPR, Pos2Nat.inj_sub by trivial. rewrite minus_INR by (now apply lt_le_weak, Pos2Nat.inj_lt). ring. - rewrite Pos2Nat.inj_sub by trivial. + rewrite <- 3!INR_IPR, Pos2Nat.inj_sub by trivial. rewrite minus_INR by (now apply lt_le_weak, Pos2Nat.inj_lt). ring. Qed. @@ -1769,26 +1785,18 @@ Qed. Lemma plus_IZR : forall n m:Z, IZR (n + m) = IZR n + IZR m. Proof. intro z; destruct z; intro t; destruct t; intros; auto with real. - simpl; intros; rewrite Pos2Nat.inj_add; auto with real. + simpl. unfold IZR. rewrite <- 3!INR_IPR, Pos2Nat.inj_add. apply plus_INR. apply plus_IZR_NEG_POS. rewrite Z.add_comm; rewrite Rplus_comm; apply plus_IZR_NEG_POS. - simpl; intros; rewrite Pos2Nat.inj_add; rewrite plus_INR; - auto with real. + simpl. unfold IZR. rewrite <- 3!INR_IPR, Pos2Nat.inj_add, plus_INR. + apply Ropp_plus_distr. Qed. (**********) Lemma mult_IZR : forall n m:Z, IZR (n * m) = IZR n * IZR m. Proof. - intros z t; case z; case t; simpl; auto with real. - intros t1 z1; rewrite Pos2Nat.inj_mul; auto with real. - intros t1 z1; rewrite Pos2Nat.inj_mul; auto with real. - rewrite Rmult_comm. - rewrite Ropp_mult_distr_l_reverse; auto with real. - apply Ropp_eq_compat; rewrite mult_comm; auto with real. - intros t1 z1; rewrite Pos2Nat.inj_mul; auto with real. - rewrite Ropp_mult_distr_l_reverse; auto with real. - intros t1 z1; rewrite Pos2Nat.inj_mul; auto with real. - rewrite Rmult_opp_opp; auto with real. + intros z t; case z; case t; simpl; auto with real; + unfold IZR; intros m n; rewrite <- 3!INR_IPR, Pos2Nat.inj_mul, mult_INR; ring. Qed. Lemma pow_IZR : forall z n, pow (IZR z) n = IZR (Z.pow z (Z.of_nat n)). @@ -1804,13 +1812,13 @@ 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. (**********) Lemma opp_IZR : forall n:Z, IZR (- n) = - IZR n. Proof. - intro z; case z; simpl; auto with real. + intros [|z|z]; unfold IZR; simpl; auto with real. Qed. Definition Ropp_Ropp_IZR := opp_IZR. @@ -1833,10 +1841,12 @@ Qed. Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z. Proof. intro z; case z; simpl; intros. - absurd (0 < 0); auto with real. - unfold Z.lt; simpl; trivial. - case Rlt_not_le with (1 := H). - replace 0 with (-0); auto with real. + elim (Rlt_irrefl _ H). + easy. + elim (Rlt_not_le _ _ H). + unfold IZR. + rewrite <- INR_IPR. + auto with real. Qed. (**********) @@ -1852,9 +1862,12 @@ Qed. Lemma eq_IZR_R0 : forall n:Z, IZR n = 0 -> n = 0%Z. Proof. intro z; destruct z; simpl; intros; auto with zarith. - case (Rlt_not_eq 0 (INR (Pos.to_nat p))); auto with real. - case (Rlt_not_eq (- INR (Pos.to_nat p)) 0); auto with real. - apply Ropp_lt_gt_0_contravar. unfold Rgt; apply pos_INR_nat_of_P. + elim Rgt_not_eq with (2 := H). + unfold IZR. rewrite <- INR_IPR. + apply lt_0_INR, Pos2Nat.is_pos. + elim Rlt_not_eq with (2 := H). + unfold IZR. rewrite <- INR_IPR. + apply Ropp_lt_gt_0_contravar, lt_0_INR, Pos2Nat.is_pos. Qed. (**********) @@ -2003,6 +2016,31 @@ Proof. [ apply not_0_INR; discriminate | unfold INR; ring ]. Qed. +Lemma R_rm : ring_morph + R0 R1 Rplus Rmult Rminus Ropp eq + 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool IZR. +Proof. +constructor ; try easy. +exact plus_IZR. +exact minus_IZR. +exact mult_IZR. +exact opp_IZR. +intros x y H. +apply f_equal. +now apply Zeq_bool_eq. +Qed. + +Lemma Zeq_bool_IZR x y : + IZR x = IZR y -> Zeq_bool x y = true. +Proof. +intros H. +apply Zeq_is_eq_bool. +now apply eq_IZR. +Qed. + +Add Field RField : Rfield + (completeness Zeq_bool_IZR, morphism R_rm, constants [IZR_tac], power_tac R_power_theory [Rpow_tac]). + (*********************************************************) (** ** Other rules about < and <= *) (*********************************************************) @@ -2017,42 +2055,18 @@ Qed. Lemma le_epsilon : forall r1 r2, (forall eps:R, 0 < eps -> r1 <= r2 + eps) -> r1 <= r2. Proof. - intros x y; intros; elim (Rtotal_order x y); intro. - left; assumption. - elim H0; intro. - right; assumption. - clear H0; generalize (Rgt_minus x y H1); intro H2; change (0 < x - y) in H2. - cut (0 < 2). - intro. - generalize (Rmult_lt_0_compat (x - y) (/ 2) H2 (Rinv_0_lt_compat 2 H0)); - intro H3; generalize (H ((x - y) * / 2) H3); - replace (y + (x - y) * / 2) with ((y + x) * / 2). - intro H4; - generalize (Rmult_le_compat_l 2 x ((y + x) * / 2) (Rlt_le 0 2 H0) H4); - rewrite <- (Rmult_comm ((y + x) * / 2)); rewrite Rmult_assoc; - rewrite <- Rinv_l_sym. - rewrite Rmult_1_r; replace (2 * x) with (x + x). - rewrite (Rplus_comm y); intro H5; apply Rplus_le_reg_l with x; assumption. - ring. - replace 2 with (INR 2); [ apply not_0_INR; discriminate | reflexivity ]. - pattern y at 2; replace y with (y / 2 + y / 2). - unfold Rminus, Rdiv. - repeat rewrite Rmult_plus_distr_r. - ring. - cut (forall z:R, 2 * z = z + z). - intro. - rewrite <- (H4 (y / 2)). - unfold Rdiv. - rewrite <- Rmult_assoc; apply Rinv_r_simpl_m. - replace 2 with (INR 2). - apply not_0_INR. - discriminate. - unfold INR; reflexivity. - intro; ring. - cut (0%nat <> 2%nat); - [ intro H0; generalize (lt_0_INR 2 (neq_O_lt 2 H0)); unfold INR; - intro; assumption - | discriminate ]. + intros x y H. + destruct (Rle_or_lt x y) as [H1|H1]. + exact H1. + apply Rplus_le_reg_r with x. + replace (y + x) with (2 * (y + (x - y) * / 2)) by field. + replace (x + x) with (2 * x) by ring. + apply Rmult_le_compat_l. + now apply (IZR_le 0 2). + apply H. + apply Rmult_lt_0_compat. + now apply Rgt_minus. + apply Rinv_0_lt_compat, Rlt_0_2. Qed. (**********) diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index b6d0728371..e9b1762af8 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -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; @@ -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_sqr.v b/theories/Reals/R_sqr.v index 445ffcb21b..a8937e36fd 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -296,56 +296,9 @@ Lemma canonical_Rsqr : a * Rsqr (x + b / (2 * a)) + (4 * a * c - Rsqr b) / (4 * a). Proof. intros. - rewrite Rsqr_plus. - repeat rewrite Rmult_plus_distr_l. - repeat rewrite Rplus_assoc. - apply Rplus_eq_compat_l. - unfold Rdiv, Rminus. - replace (2 * 1 + 2 * 1) with 4; [ idtac | ring ]. - rewrite (Rmult_plus_distr_r (4 * a * c) (- Rsqr b) (/ (4 * a))). - rewrite Rsqr_mult. - repeat rewrite Rinv_mult_distr. - repeat rewrite (Rmult_comm a). - repeat rewrite Rmult_assoc. - rewrite <- Rinv_l_sym. - rewrite Rmult_1_r. - rewrite (Rmult_comm 2). - repeat rewrite Rmult_assoc. - rewrite <- Rinv_l_sym. - rewrite Rmult_1_r. - rewrite (Rmult_comm (/ 2)). - rewrite (Rmult_comm 2). - repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym. - rewrite Rmult_1_r. - rewrite (Rmult_comm a). - repeat rewrite Rmult_assoc. - rewrite <- Rinv_l_sym. - rewrite Rmult_1_r. - rewrite (Rmult_comm 2). - repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym. - rewrite Rmult_1_r. - repeat rewrite Rplus_assoc. - rewrite (Rplus_comm (Rsqr b * (Rsqr (/ a * / 2) * a))). - repeat rewrite Rplus_assoc. - rewrite (Rmult_comm x). - apply Rplus_eq_compat_l. - rewrite (Rmult_comm (/ a)). - unfold Rsqr; repeat rewrite Rmult_assoc. - rewrite <- Rinv_l_sym. - rewrite Rmult_1_r. - ring. - apply (cond_nonzero a). - discrR. - apply (cond_nonzero a). - discrR. - discrR. - apply (cond_nonzero a). - discrR. - discrR. - discrR. - apply (cond_nonzero a). - discrR. - apply (cond_nonzero a). + unfold Rsqr. + field. + apply a. Qed. Lemma Rsqr_eq : forall x y:R, Rsqr x = Rsqr y -> x = y \/ x = - y. diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index a6b1a26e03..0c1e0b7e86 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -359,107 +359,22 @@ Lemma Rsqr_sol_eq_0_1 : x = sol_x1 a b c \/ x = sol_x2 a b c -> a * Rsqr x + b * x + c = 0. Proof. intros; elim H0; intro. - unfold sol_x1 in H1; unfold Delta in H1; rewrite H1; unfold Rdiv; - repeat rewrite Rsqr_mult; rewrite Rsqr_plus; rewrite <- Rsqr_neg; - rewrite Rsqr_sqrt. - rewrite Rsqr_inv. - unfold Rsqr; repeat rewrite Rinv_mult_distr. - repeat rewrite Rmult_assoc; rewrite (Rmult_comm a). - repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym. - rewrite Rmult_1_r; rewrite Rmult_plus_distr_r. - repeat rewrite Rmult_assoc. - pattern 2 at 2; rewrite (Rmult_comm 2). - repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym. - rewrite Rmult_1_r. - rewrite - (Rmult_plus_distr_r (- b) (sqrt (b * b - 2 * (2 * (a * c)))) (/ 2 * / a)) - . - rewrite Rmult_plus_distr_l; repeat rewrite Rplus_assoc. - replace - (- b * (sqrt (b * b - 2 * (2 * (a * c))) * (/ 2 * / a)) + - (b * (- b * (/ 2 * / a)) + - (b * (sqrt (b * b - 2 * (2 * (a * c))) * (/ 2 * / a)) + c))) with - (b * (- b * (/ 2 * / a)) + c). - unfold Rminus; repeat rewrite <- Rplus_assoc. - replace (b * b + b * b) with (2 * (b * b)). - rewrite Rmult_plus_distr_r; repeat rewrite Rmult_assoc. - rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc. - rewrite <- Rinv_l_sym. - rewrite Rmult_1_r. - rewrite Ropp_mult_distr_l_reverse; repeat rewrite Rmult_assoc; - rewrite (Rmult_comm 2). - repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym. - rewrite Rmult_1_r; rewrite (Rmult_comm (/ 2)); repeat rewrite Rmult_assoc; - rewrite (Rmult_comm 2). - repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym. - rewrite Rmult_1_r; repeat rewrite Rmult_assoc. - rewrite (Rmult_comm a); rewrite Rmult_assoc. - rewrite <- Rinv_l_sym. - rewrite Rmult_1_r; rewrite <- Rmult_opp_opp. - ring. - apply (cond_nonzero a). - discrR. - discrR. - discrR. - ring. - ring. - discrR. - apply (cond_nonzero a). - discrR. - apply (cond_nonzero a). - apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ]. - apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ]. - apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ]. - assumption. - unfold sol_x2 in H1; unfold Delta in H1; rewrite H1; unfold Rdiv; - repeat rewrite Rsqr_mult; rewrite Rsqr_minus; rewrite <- Rsqr_neg; - rewrite Rsqr_sqrt. - rewrite Rsqr_inv. - unfold Rsqr; repeat rewrite Rinv_mult_distr; - repeat rewrite Rmult_assoc. - rewrite (Rmult_comm a); repeat rewrite Rmult_assoc. - rewrite <- Rinv_l_sym. - rewrite Rmult_1_r; unfold Rminus; rewrite Rmult_plus_distr_r. - rewrite Ropp_mult_distr_l_reverse; repeat rewrite Rmult_assoc; - pattern 2 at 2; rewrite (Rmult_comm 2). - repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym. - rewrite Rmult_1_r; - rewrite - (Rmult_plus_distr_r (- b) (- sqrt (b * b + - (2 * (2 * (a * c))))) - (/ 2 * / a)). - rewrite Rmult_plus_distr_l; repeat rewrite Rplus_assoc. - rewrite Ropp_mult_distr_l_reverse; rewrite Ropp_involutive. - replace - (b * (sqrt (b * b + - (2 * (2 * (a * c)))) * (/ 2 * / a)) + - (b * (- b * (/ 2 * / a)) + - (b * (- sqrt (b * b + - (2 * (2 * (a * c)))) * (/ 2 * / a)) + c))) with - (b * (- b * (/ 2 * / a)) + c). - repeat rewrite <- Rplus_assoc; replace (b * b + b * b) with (2 * (b * b)). - rewrite Rmult_plus_distr_r; repeat rewrite Rmult_assoc; - rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; - rewrite <- Rinv_l_sym. - rewrite Ropp_mult_distr_l_reverse; repeat rewrite Rmult_assoc. - rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym. - rewrite Rmult_1_r; rewrite (Rmult_comm (/ 2)); repeat rewrite Rmult_assoc. - rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym. - rewrite Rmult_1_r; repeat rewrite Rmult_assoc; rewrite (Rmult_comm a); - rewrite Rmult_assoc; rewrite <- Rinv_l_sym. - rewrite Rmult_1_r; rewrite <- Rmult_opp_opp; ring. - apply (cond_nonzero a). - discrR. - discrR. - discrR. - ring. - ring. - discrR. - apply (cond_nonzero a). - discrR. - discrR. - apply (cond_nonzero a). - apply prod_neq_R0; discrR || apply (cond_nonzero a). - apply prod_neq_R0; discrR || apply (cond_nonzero a). - apply prod_neq_R0; discrR || apply (cond_nonzero a). - assumption. + rewrite H1. + unfold sol_x1, Delta, Rsqr. + field_simplify. + rewrite <- (Rsqr_pow2 (sqrt _)), Rsqr_sqrt. + field. + apply a. + apply H. + apply a. + rewrite H1. + unfold sol_x2, Delta, Rsqr. + field_simplify. + rewrite <- (Rsqr_pow2 (sqrt _)), Rsqr_sqrt. + field. + apply a. + apply H. + apply a. Qed. Lemma Rsqr_sol_eq_0_0 : @@ -505,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 0254218c44..27cb356a09 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 4e88714d61..d4597aebaf 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/Ranalysis4.v b/theories/Reals/Ranalysis4.v index 661bc8c76b..23daedb8ba 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -130,15 +130,8 @@ Proof. intro; exists (mkposreal (- x) H1); intros. rewrite (Rabs_left x). rewrite (Rabs_left (x + h)). - rewrite Rplus_comm. - rewrite Ropp_plus_distr. - unfold Rminus; rewrite Ropp_involutive; rewrite Rplus_assoc; - rewrite Rplus_opp_l. - rewrite Rplus_0_r; unfold Rdiv. - rewrite Ropp_mult_distr_l_reverse. - rewrite <- Rinv_r_sym. - rewrite Ropp_involutive; rewrite Rplus_opp_l; rewrite Rabs_R0; apply H0. - apply H2. + replace ((-(x + h) - - x) / h - -1) with 0 by now field. + rewrite Rabs_R0; apply H0. destruct (Rcase_abs h) as [Hlt|Hgt]. apply Ropp_lt_cancel. rewrite Ropp_0; rewrite Ropp_plus_distr; apply Rplus_lt_0_compat. diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index d172139f56..f9da88aad4 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 e13ef1f2ca..e438750df0 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; replace 3 with (IZR 3) by (simpl; ring); - replace 2 with (IZR 2) by (simpl; ring); 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. +rewrite !INR_IZR_INZ. +simpl. +field_simplify. +unfold Rdiv. +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). @@ -853,6 +833,8 @@ intros x Hx eps Heps. apply Rlt_trans with (2 := H). apply Rinv_0_lt_compat. exact Heps. + unfold N. + rewrite INR_IZR_INZ, positive_nat_Z. exact HN. apply lt_INR. omega. @@ -1076,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. @@ -1165,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 9fbda92a2f..7f9db3b18f 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -115,19 +115,6 @@ Arguments INR n%nat. (**********************************************************) -(** * Injection from [Z] to [R] *) -(**********************************************************) - -(**********) -Definition IZR (z:Z) : R := - match z with - | Z0 => 0 - | Zpos n => INR (Pos.to_nat n) - | Zneg n => - INR (Pos.to_nat n) - end. -Arguments IZR z%Z. - -(**********************************************************) (** * [R] Archimedean *) (**********************************************************) diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index c889d73473..df16624976 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. (*********) @@ -613,11 +609,12 @@ Qed. Lemma Rabs_Zabs : forall z:Z, Rabs (IZR z) = IZR (Z.abs z). Proof. - intros z; case z; simpl; auto with real. - apply Rabs_right; auto with real. - intros p0; apply Rabs_right; auto with real zarith. + intros z; case z; unfold Zabs. + apply Rabs_R0. + now intros p0; apply Rabs_pos_eq, (IZR_le 0). + unfold IZR at 1. intros p0; rewrite Rabs_Ropp. - apply Rabs_right; auto with real zarith. + now apply Rabs_pos_eq, (IZR_le 0). Qed. Lemma abs_IZR : forall z, IZR (Z.abs z) = Rabs (IZR z). diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index f3f8f74098..cb5dea93ad 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/Rderiv.v b/theories/Reals/Rderiv.v index bd330ac9b9..5fb6bd2b71 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -296,14 +296,10 @@ Proof. intros; generalize (H0 eps H1); clear H0; intro; elim H0; clear H0; intros; elim H0; clear H0; simpl; intros; split with x; split; auto. - intros; generalize (H2 x1 H3); clear H2; intro; - rewrite Ropp_mult_distr_l_reverse in H2; - rewrite Ropp_mult_distr_l_reverse in H2; - rewrite Ropp_mult_distr_l_reverse in H2; - rewrite (let (H1, H2) := Rmult_ne (f x1) in H2) in H2; - rewrite (let (H1, H2) := Rmult_ne (f x0) in H2) in H2; - rewrite (let (H1, H2) := Rmult_ne (df x0) in H2) in H2; - assumption. + intros; generalize (H2 x1 H3); clear H2; intro. + replace (- f x1 - - f x0) with (-1 * f x1 - -1 * f x0) by ring. + replace (- df x0) with (-1 * df x0) by ring. + exact H2. Qed. (*********) diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 0a49d49831..99acdd0a1c 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/Rlimit.v b/theories/Reals/Rlimit.v index e424a732ac..f071407521 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -407,8 +407,7 @@ Proof. generalize (Rplus_lt_compat (R_dist (f x2) l) eps (R_dist (f x2) l') eps H H0); unfold R_dist; intros; rewrite (Rabs_minus_sym (f x2) l) in H1; - rewrite (Rmult_comm 2 eps); rewrite (Rmult_plus_distr_l eps 1 1); - elim (Rmult_ne eps); intros a b; rewrite a; clear a b; + rewrite (Rmult_comm 2 eps); replace (eps *2) with (eps + eps) by ring; generalize (R_dist_tri l l' (f x2)); unfold R_dist; intros; apply diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v index 791718a450..f331bb2039 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 b3ce6fa338..f62ed2a6c1 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -55,25 +55,8 @@ Proof. simpl in H0. replace (/ 3) with (1 * / 1 + -1 * 1 * / 1 + -1 * (-1 * 1) * / 2 + - -1 * (-1 * (-1 * 1)) * / (2 + 1 + 1 + 1 + 1)). + -1 * (-1 * (-1 * 1)) * / (2 + 1 + 1 + 1 + 1)) by field. apply H0. - repeat rewrite Rinv_1; repeat rewrite Rmult_1_r; - rewrite Ropp_mult_distr_l_reverse; rewrite Rmult_1_l; - rewrite Ropp_involutive; rewrite Rplus_opp_r; rewrite Rmult_1_r; - rewrite Rplus_0_l; rewrite Rmult_1_l; apply Rmult_eq_reg_l with 6. - rewrite Rmult_plus_distr_l; replace (2 + 1 + 1 + 1 + 1) with 6. - rewrite <- (Rmult_comm (/ 6)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym. - rewrite Rmult_1_l; replace 6 with 6. - do 2 rewrite Rmult_assoc; rewrite <- Rinv_r_sym. - rewrite Rmult_1_r; rewrite (Rmult_comm 3); rewrite <- Rmult_assoc; - rewrite <- Rinv_r_sym. - ring. - discrR. - discrR. - ring. - discrR. - ring. - discrR. apply H. unfold Un_decreasing; intros; apply Rmult_le_reg_l with (INR (fact n)). @@ -505,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. @@ -732,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 744fd66416..c6b0c3f37a 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 4d24186396..17b9677eff 100644 --- a/theories/Reals/Rtrigo1.v +++ b/theories/Reals/Rtrigo1.v @@ -182,13 +182,10 @@ 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; replace 7 with (IZR 7) by (simpl; field). -replace 8 with (IZR 8) by (simpl; field). +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. match goal with |- IZR ?a / ?b < ?c / ?d => apply Rmult_lt_reg_r with d;[apply (IZR_lt 0); reflexivity | @@ -198,7 +195,7 @@ match goal with end. unfold Rdiv; rewrite !Rmult_assoc, Rinv_l, Rmult_1_r; [ | apply not_eq_sym, Rlt_not_eq, (IZR_lt 0); reflexivity]. -repeat (rewrite <- !plus_IZR || rewrite <- !mult_IZR). +rewrite <- !mult_IZR. apply IZR_lt; reflexivity. Qed. @@ -323,6 +320,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 +531,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 +590,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 +600,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 +608,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 +710,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 +764,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. @@ -1260,44 +1257,22 @@ Proof. intros x y H1 H2 H3 H4; rewrite <- (cos_neg x); rewrite <- (cos_neg y); rewrite <- (cos_period (- x) 1); rewrite <- (cos_period (- y) 1); unfold INR in |- *; - replace (- x + 2 * 1 * PI) with (PI / 2 - (x - 3 * (PI / 2))). - replace (- y + 2 * 1 * PI) with (PI / 2 - (y - 3 * (PI / 2))). + replace (- x + 2 * 1 * PI) with (PI / 2 - (x - 3 * (PI / 2))) by field. + replace (- y + 2 * 1 * PI) with (PI / 2 - (y - 3 * (PI / 2))) by field. repeat rewrite cos_shift; intro H5; generalize (Rplus_le_compat_l (-3 * (PI / 2)) PI x H1); generalize (Rplus_le_compat_l (-3 * (PI / 2)) x (2 * PI) H2); generalize (Rplus_le_compat_l (-3 * (PI / 2)) PI y H3); generalize (Rplus_le_compat_l (-3 * (PI / 2)) y (2 * PI) H4). - replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)). - replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)). - replace (-3 * (PI / 2) + 2 * PI) with (PI / 2). - replace (-3 * (PI / 2) + PI) with (- (PI / 2)). + replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)) by ring. + replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)) by ring. + replace (-3 * (PI / 2) + 2 * PI) with (PI / 2) by field. + replace (-3 * (PI / 2) + PI) with (- (PI / 2)) by field. clear H1 H2 H3 H4; intros H1 H2 H3 H4; apply Rplus_lt_reg_l with (-3 * (PI / 2)); - replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)). - replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)). + replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)) by ring. + replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)) by ring. apply (sin_increasing_0 (x - 3 * (PI / 2)) (y - 3 * (PI / 2)) H4 H3 H2 H1 H5). - unfold Rminus in |- *. - rewrite Ropp_mult_distr_l_reverse. - apply Rplus_comm. - unfold Rminus in |- *. - rewrite Ropp_mult_distr_l_reverse. - apply Rplus_comm. - pattern PI at 3 in |- *; rewrite double_var. - ring. - rewrite double; pattern PI at 3 4 in |- *; rewrite double_var. - ring. - unfold Rminus in |- *. - rewrite Ropp_mult_distr_l_reverse. - apply Rplus_comm. - unfold Rminus in |- *. - rewrite Ropp_mult_distr_l_reverse. - apply Rplus_comm. - rewrite Rmult_1_r. - rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var. - ring. - rewrite Rmult_1_r. - rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var. - ring. Qed. Lemma cos_increasing_1 : @@ -1737,7 +1712,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. @@ -1747,7 +1722,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. @@ -1769,7 +1744,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. @@ -1779,7 +1754,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. @@ -1858,7 +1833,7 @@ Proof. - right; left; auto. - left. clear Hi. subst. - replace 0 with (IZR 0 * PI) by (simpl; ring). f_equal. f_equal. + replace 0 with (IZR 0 * PI) by apply Rmult_0_l. f_equal. f_equal. apply one_IZR_lt1. split. + apply Rlt_le_trans with 0; diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index a5092d22dc..092bc30d07 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_calc.v b/theories/Reals/Rtrigo_calc.v index 9ba14ee734..53056cabdf 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -32,48 +32,22 @@ Proof. Qed. Lemma sin_cos_PI4 : sin (PI / 4) = cos (PI / 4). -Proof with trivial. - rewrite cos_sin... - replace (PI / 2 + PI / 4) with (- (PI / 4) + PI)... - rewrite neg_sin; rewrite sin_neg; ring... - cut (PI = PI / 2 + PI / 2); [ intro | apply double_var ]... - pattern PI at 2 3; rewrite H; pattern PI at 2 3; rewrite H... - assert (H0 : 2 <> 0); - [ discrR | unfold Rdiv; rewrite Rinv_mult_distr; try ring ]... +Proof. + rewrite cos_sin. + replace (PI / 2 + PI / 4) with (- (PI / 4) + PI) by field. + rewrite neg_sin, sin_neg; ring. Qed. Lemma sin_PI3_cos_PI6 : sin (PI / 3) = cos (PI / 6). -Proof with trivial. - replace (PI / 6) with (PI / 2 - PI / 3)... - rewrite cos_shift... - assert (H0 : 6 <> 0); [ discrR | idtac ]... - assert (H1 : 3 <> 0); [ discrR | idtac ]... - assert (H2 : 2 <> 0); [ discrR | idtac ]... - apply Rmult_eq_reg_l with 6... - rewrite Rmult_minus_distr_l; repeat rewrite (Rmult_comm 6)... - unfold Rdiv; repeat rewrite Rmult_assoc... - rewrite <- Rinv_l_sym... - rewrite (Rmult_comm (/ 3)); repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym... - rewrite (Rmult_comm PI); repeat rewrite Rmult_1_r; - repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym... - ring... +Proof. + replace (PI / 6) with (PI / 2 - PI / 3) by field. + now rewrite cos_shift. Qed. Lemma sin_PI6_cos_PI3 : cos (PI / 3) = sin (PI / 6). -Proof with trivial. - replace (PI / 6) with (PI / 2 - PI / 3)... - rewrite sin_shift... - assert (H0 : 6 <> 0); [ discrR | idtac ]... - assert (H1 : 3 <> 0); [ discrR | idtac ]... - assert (H2 : 2 <> 0); [ discrR | idtac ]... - apply Rmult_eq_reg_l with 6... - rewrite Rmult_minus_distr_l; repeat rewrite (Rmult_comm 6)... - unfold Rdiv; repeat rewrite Rmult_assoc... - rewrite <- Rinv_l_sym... - rewrite (Rmult_comm (/ 3)); repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym... - rewrite (Rmult_comm PI); repeat rewrite Rmult_1_r; - repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym... - ring... +Proof. + replace (PI / 6) with (PI / 2 - PI / 3) by field. + now rewrite sin_shift. Qed. Lemma PI6_RGT_0 : 0 < PI / 6. @@ -90,29 +64,20 @@ Proof. Qed. Lemma sin_PI6 : sin (PI / 6) = 1 / 2. -Proof with trivial. - assert (H : 2 <> 0); [ discrR | idtac ]... - apply Rmult_eq_reg_l with (2 * cos (PI / 6))... +Proof. + apply Rmult_eq_reg_l with (2 * cos (PI / 6)). replace (2 * cos (PI / 6) * sin (PI / 6)) with - (2 * sin (PI / 6) * cos (PI / 6))... - rewrite <- sin_2a; replace (2 * (PI / 6)) with (PI / 3)... - rewrite sin_PI3_cos_PI6... - unfold Rdiv; rewrite Rmult_1_l; rewrite Rmult_assoc; - pattern 2 at 2; rewrite (Rmult_comm 2); rewrite Rmult_assoc; - rewrite <- Rinv_l_sym... - rewrite Rmult_1_r... - unfold Rdiv; rewrite Rinv_mult_distr... - rewrite (Rmult_comm (/ 2)); rewrite (Rmult_comm 2); - repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym... - rewrite Rmult_1_r... - discrR... - ring... - apply prod_neq_R0... + (2 * sin (PI / 6) * cos (PI / 6)) by ring. + rewrite <- sin_2a; replace (2 * (PI / 6)) with (PI / 3) by field. + rewrite sin_PI3_cos_PI6. + field. + apply prod_neq_R0. + discrR. cut (0 < cos (PI / 6)); [ intro H1; auto with real | apply cos_gt_0; [ apply (Rlt_trans (- (PI / 2)) 0 (PI / 6) _PI2_RLT_0 PI6_RGT_0) - | apply PI6_RLT_PI2 ] ]... + | apply PI6_RLT_PI2 ] ]. Qed. Lemma sqrt2_neq_0 : sqrt 2 <> 0. @@ -188,20 +153,13 @@ Proof with trivial. apply Rinv_0_lt_compat; apply Rlt_sqrt2_0... rewrite Rsqr_div... rewrite Rsqr_1; rewrite Rsqr_sqrt... - assert (H : 2 <> 0); [ discrR | idtac ]... unfold Rsqr; pattern (cos (PI / 4)) at 1; rewrite <- sin_cos_PI4; replace (sin (PI / 4) * cos (PI / 4)) with - (1 / 2 * (2 * sin (PI / 4) * cos (PI / 4)))... - rewrite <- sin_2a; replace (2 * (PI / 4)) with (PI / 2)... + (1 / 2 * (2 * sin (PI / 4) * cos (PI / 4))) by field. + rewrite <- sin_2a; replace (2 * (PI / 4)) with (PI / 2) by field. rewrite sin_PI2... - apply Rmult_1_r... - unfold Rdiv; rewrite (Rmult_comm 2); rewrite Rinv_mult_distr... - repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym... - rewrite Rmult_1_r... - unfold Rdiv; rewrite Rmult_1_l; repeat rewrite <- Rmult_assoc... - rewrite <- Rinv_l_sym... - rewrite Rmult_1_l... + field. left; prove_sup... apply sqrt2_neq_0... Qed. @@ -219,24 +177,17 @@ Proof. Qed. Lemma cos3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2. -Proof with trivial. - replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4))... - rewrite cos_shift; rewrite sin_neg; rewrite sin_PI4... - unfold Rdiv; rewrite Ropp_mult_distr_l_reverse... - unfold Rminus; rewrite Ropp_involutive; pattern PI at 1; - rewrite double_var; unfold Rdiv; rewrite Rmult_plus_distr_r; - repeat rewrite Rmult_assoc; rewrite <- Rinv_mult_distr; - [ ring | discrR | discrR ]... +Proof. + replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field. + rewrite cos_shift; rewrite sin_neg; rewrite sin_PI4. + unfold Rdiv. + ring. Qed. Lemma sin3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2. -Proof with trivial. - replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4))... - rewrite sin_shift; rewrite cos_neg; rewrite cos_PI4... - unfold Rminus; rewrite Ropp_involutive; pattern PI at 1; - rewrite double_var; unfold Rdiv; rewrite Rmult_plus_distr_r; - repeat rewrite Rmult_assoc; rewrite <- Rinv_mult_distr; - [ ring | discrR | discrR ]... +Proof. + replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field. + now rewrite sin_shift, cos_neg, cos_PI4. Qed. Lemma cos_PI6 : cos (PI / 6) = sqrt 3 / 2. @@ -248,19 +199,11 @@ Proof with trivial. left; apply (Rmult_lt_0_compat (sqrt 3) (/ 2))... apply Rlt_sqrt3_0... apply Rinv_0_lt_compat; prove_sup0... - assert (H : 2 <> 0); [ discrR | idtac ]... - assert (H1 : 4 <> 0); [ apply prod_neq_R0 | idtac ]... rewrite Rsqr_div... rewrite cos2; unfold Rsqr; rewrite sin_PI6; rewrite sqrt_def... - unfold Rdiv; rewrite Rmult_1_l; apply Rmult_eq_reg_l with 4... - rewrite Rmult_minus_distr_l; rewrite (Rmult_comm 3); - repeat rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym... - rewrite Rmult_1_l; rewrite Rmult_1_r... - rewrite <- (Rmult_comm (/ 2)); repeat rewrite <- Rmult_assoc... - rewrite <- Rinv_l_sym... - rewrite Rmult_1_l; rewrite <- Rinv_r_sym... - ring... - left; prove_sup0... + field. + left ; prove_sup0. + discrR. Qed. Lemma tan_PI6 : tan (PI / 6) = 1 / sqrt 3. @@ -306,56 +249,32 @@ Proof. Qed. Lemma cos_2PI3 : cos (2 * (PI / 3)) = -1 / 2. -Proof with trivial. - assert (H : 2 <> 0); [ discrR | idtac ]... - assert (H0 : 4 <> 0); [ apply prod_neq_R0 | idtac ]... - rewrite double; rewrite cos_plus; rewrite sin_PI3; rewrite cos_PI3; - unfold Rdiv; rewrite Rmult_1_l; apply Rmult_eq_reg_l with 4... - rewrite Rmult_minus_distr_l; repeat rewrite Rmult_assoc; - rewrite (Rmult_comm 2)... - repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym... - rewrite Rmult_1_r; rewrite <- Rinv_r_sym... - pattern 2 at 4; rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; - rewrite <- Rinv_l_sym... - rewrite Rmult_1_r; rewrite Ropp_mult_distr_r_reverse; rewrite Rmult_1_r... - rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym... - rewrite Rmult_1_r; rewrite (Rmult_comm 2); rewrite (Rmult_comm (/ 2))... - repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym... - rewrite Rmult_1_r; rewrite sqrt_def... - ring... - left; prove_sup... +Proof. + rewrite cos_2a, sin_PI3, cos_PI3. + replace (sqrt 3 / 2 * (sqrt 3 / 2)) with ((sqrt 3 * sqrt 3) / 4) by field. + rewrite sqrt_sqrt. + field. + left ; prove_sup0. Qed. Lemma tan_2PI3 : tan (2 * (PI / 3)) = - sqrt 3. -Proof with trivial. - assert (H : 2 <> 0); [ discrR | idtac ]... - unfold tan; rewrite sin_2PI3; rewrite cos_2PI3; unfold Rdiv; - rewrite Ropp_mult_distr_l_reverse; rewrite Rmult_1_l; - rewrite <- Ropp_inv_permute... - rewrite Rinv_involutive... - rewrite Rmult_assoc; rewrite Ropp_mult_distr_r_reverse; rewrite <- Rinv_l_sym... - ring... - apply Rinv_neq_0_compat... +Proof. + unfold tan; rewrite sin_2PI3, cos_2PI3. + field. Qed. Lemma cos_5PI4 : cos (5 * (PI / 4)) = -1 / sqrt 2. -Proof with trivial. - replace (5 * (PI / 4)) with (PI / 4 + PI)... - rewrite neg_cos; rewrite cos_PI4; unfold Rdiv; - rewrite Ropp_mult_distr_l_reverse... - pattern PI at 2; rewrite double_var; pattern PI at 2 3; - rewrite double_var; assert (H : 2 <> 0); - [ discrR | unfold Rdiv; repeat rewrite Rinv_mult_distr; try ring ]... +Proof. + replace (5 * (PI / 4)) with (PI / 4 + PI) by field. + rewrite neg_cos; rewrite cos_PI4; unfold Rdiv. + ring. Qed. Lemma sin_5PI4 : sin (5 * (PI / 4)) = -1 / sqrt 2. -Proof with trivial. - replace (5 * (PI / 4)) with (PI / 4 + PI)... - rewrite neg_sin; rewrite sin_PI4; unfold Rdiv; - rewrite Ropp_mult_distr_l_reverse... - pattern PI at 2; rewrite double_var; pattern PI at 2 3; - rewrite double_var; assert (H : 2 <> 0); - [ discrR | unfold Rdiv; repeat rewrite Rinv_mult_distr; try ring ]... +Proof. + replace (5 * (PI / 4)) with (PI / 4 + PI) by field. + rewrite neg_sin; rewrite sin_PI4; unfold Rdiv. + ring. Qed. Lemma sin_cos5PI4 : cos (5 * (PI / 4)) = sin (5 * (PI / 4)). diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index eed612d94b..d9c18d3587 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. @@ -395,15 +396,8 @@ Proof. apply Rlt_le_trans with alp. apply H7. unfold alp; apply Rmin_l. - rewrite sin_plus; unfold Rminus, Rdiv; - repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l; - repeat rewrite Rmult_assoc; repeat rewrite Rplus_assoc; - apply Rplus_eq_compat_l. - rewrite (Rplus_comm (sin x * (-1 * / h))); repeat rewrite Rplus_assoc; - apply Rplus_eq_compat_l. - rewrite Ropp_mult_distr_r_reverse; rewrite Ropp_mult_distr_l_reverse; - rewrite Rmult_1_r; rewrite Rmult_1_l; rewrite Ropp_mult_distr_r_reverse; - rewrite <- Ropp_mult_distr_l_reverse; apply Rplus_comm. + rewrite sin_plus. + now field. unfold alp; unfold Rmin; case (Rle_dec alp1 alp2); intro. apply (cond_pos alp1). apply (cond_pos alp2). diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index d43baee8cd..12d5cbbf0f 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. |