diff options
| -rw-r--r-- | theories/Reals/Abstract/ConstructiveAbs.v | 153 | ||||
| -rw-r--r-- | theories/Reals/Abstract/ConstructiveLUB.v | 7 | ||||
| -rw-r--r-- | theories/Reals/Abstract/ConstructiveLimits.v | 71 | ||||
| -rw-r--r-- | theories/Reals/Abstract/ConstructiveReals.v | 107 | ||||
| -rw-r--r-- | theories/Reals/Abstract/ConstructiveRealsMorphisms.v | 133 | ||||
| -rw-r--r-- | theories/Reals/Abstract/ConstructiveSum.v | 4 | ||||
| -rw-r--r-- | theories/Reals/Cauchy/ConstructiveRcomplete.v | 5 |
7 files changed, 229 insertions, 251 deletions
diff --git a/theories/Reals/Abstract/ConstructiveAbs.v b/theories/Reals/Abstract/ConstructiveAbs.v index d357ad2d54..31397cbddd 100644 --- a/theories/Reals/Abstract/ConstructiveAbs.v +++ b/theories/Reals/Abstract/ConstructiveAbs.v @@ -57,11 +57,11 @@ Proof. - pose proof (CRabs_def R x (CRabs R x)) as [_ H1]. apply H1, CRle_refl. - rewrite <- CRabs_def. split. apply CRle_refl. - apply (CRle_trans _ (CRzero R)). 2: exact H. - apply (CRle_trans _ (CRopp R (CRzero R))). + apply (CRle_trans _ 0). 2: exact H. + apply (CRle_trans _ (CRopp R 0)). intro abs. apply CRopp_lt_cancel in abs. contradiction. - apply (CRplus_le_reg_l (CRzero R)). - apply (CRle_trans _ (CRzero R)). apply CRplus_opp_r. + apply (CRplus_le_reg_l 0). + apply (CRle_trans _ 0). apply CRplus_opp_r. apply CRplus_0_r. Qed. @@ -164,8 +164,7 @@ Lemma CR_of_Q_abs : forall {R : ConstructiveReals} (q : Q), Proof. intros. destruct (Qlt_le_dec 0 q). - apply (CReq_trans _ (CR_of_Q R q)). - apply CRabs_right. apply (CRle_trans _ (CR_of_Q R 0)). - apply CR_of_Q_zero. apply CR_of_Q_le. apply Qlt_le_weak, q0. + apply CRabs_right. apply CR_of_Q_le. apply Qlt_le_weak, q0. apply CR_of_Q_morph. symmetry. apply Qabs_pos, Qlt_le_weak, q0. - apply (CReq_trans _ (CR_of_Q R (-q))). apply (CReq_trans _ (CRabs R (CRopp R (CR_of_Q R q)))). @@ -173,8 +172,7 @@ Proof. 2: apply CR_of_Q_morph; symmetry; apply Qabs_neg, q0. apply (CReq_trans _ (CRopp R (CR_of_Q R q))). 2: apply CReq_sym, CR_of_Q_opp. - apply CRabs_right. apply (CRle_trans _ (CR_of_Q R 0)). - apply CR_of_Q_zero. + apply CRabs_right. apply (CRle_trans _ (CR_of_Q R (-q))). apply CR_of_Q_le. apply (Qplus_le_l _ _ q). ring_simplify. exact q0. apply CR_of_Q_opp. @@ -206,14 +204,14 @@ Proof. destruct (CR_Q_dense R _ _ neg) as [q [H0 H1]]. destruct (Qlt_le_dec 0 q). - destruct (s (CR_of_Q R (-q)) x 0). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. + apply CR_of_Q_lt. apply (Qplus_lt_l _ _ q). ring_simplify. exact q0. exfalso. pose proof (CRabs_def R x (CR_of_Q R q)) as [H2 _]. apply H2. clear H2. split. apply CRlt_asym, H0. 2: exact H1. rewrite <- Qopp_involutive, CR_of_Q_opp. apply CRopp_ge_le_contravar, CRlt_asym, c. exact c. - apply (CRlt_le_trans _ _ _ H0). - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. exact q0. + apply CR_of_Q_le. exact q0. Qed. @@ -339,24 +337,23 @@ Proof. left; apply CR_of_Q_pos; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRabs_right. unfold CRminus. rewrite CRopp_plus_distr, CRplus_assoc, <- (CRplus_assoc y). rewrite CRplus_opp_r, CRplus_0_l, CRopp_involutive. reflexivity. apply (CRmult_lt_compat_r (CR_of_Q R 2)) in H. 2: apply CR_of_Q_pos; reflexivity. - rewrite CRmult_assoc, <- CR_of_Q_mult in H. - setoid_replace ((1 # 2) * 2)%Q with 1%Q in H. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r in H. - rewrite CRmult_comm, (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_r, - CRmult_1_l in H. - intro abs. rewrite CRabs_left in H. - unfold CRminus in H. - rewrite CRopp_involutive, CRplus_comm in H. - rewrite CRplus_assoc, <- (CRplus_assoc (-x)), CRplus_opp_l in H. - rewrite CRplus_0_l in H. exact (CRlt_asym _ _ H H). - apply CRlt_asym, abs. + intro abs. contradict H. + apply (CRle_trans _ (x + y - CRabs R (y - x))). + rewrite CRabs_left. 2: apply CRlt_asym, abs. + unfold CRminus. rewrite CRopp_involutive, CRplus_comm. + rewrite CRplus_assoc, <- (CRplus_assoc (-x)), CRplus_opp_l. + rewrite CRplus_0_l, (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. + rewrite CRmult_1_r. apply CRle_refl. + rewrite CRmult_assoc, <- CR_of_Q_mult. + setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. + rewrite CRmult_1_r. apply CRle_refl. Qed. Add Parametric Morphism {R : ConstructiveReals} : CRmin @@ -383,11 +380,11 @@ Lemma CRmin_l : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_le_reg_r (CR_of_Q R 2)). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. unfold CRminus. rewrite CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_r (CRabs _ (y + - x)+ -x)). rewrite CRplus_assoc, <- (CRplus_assoc (-CRabs _ (y + - x))). @@ -401,11 +398,11 @@ Lemma CRmin_r : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_le_reg_r (CR_of_Q R 2)). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite (CRplus_comm x). unfold CRminus. rewrite CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (-x)). @@ -451,15 +448,15 @@ Proof. intros. unfold CRmin. unfold CRminus. setoid_replace (x + z + - (x + y)) with (z-y). apply (CRmult_eq_reg_r (CR_of_Q _ 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_plus_distr_r. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. do 3 rewrite (CRplus_assoc x). apply CRplus_morph. reflexivity. do 2 rewrite <- CRplus_assoc. apply CRplus_morph. 2: reflexivity. rewrite (CRplus_comm x). apply CRplus_assoc. @@ -474,11 +471,11 @@ Lemma CRmin_left : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_eq_reg_r (CR_of_Q R 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRabs_right. unfold CRminus. rewrite CRopp_plus_distr. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. apply CRopp_involutive. @@ -491,11 +488,11 @@ Lemma CRmin_right : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_eq_reg_r (CR_of_Q R 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRabs_left. unfold CRminus. do 2 rewrite CRopp_plus_distr. rewrite (CRplus_comm x y). rewrite CRplus_assoc. apply CRplus_morph. reflexivity. @@ -510,10 +507,10 @@ Lemma CRmin_lt : forall {R : ConstructiveReals} (x y z : CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_lt_reg_r (CR_of_Q R 2)). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. apply (CRplus_lt_reg_l _ (CRabs _ (y - x) - (z*CR_of_Q R 2))). unfold CRminus. rewrite CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_r. rewrite (CRplus_comm (CRabs R (y + - x))). @@ -526,7 +523,7 @@ Proof. apply (CRplus_lt_reg_l R (-x)). rewrite CRopp_mult_distr_l. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_lt_compat. apply CRlt_asym. apply CRopp_gt_lt_contravar, H. @@ -537,7 +534,7 @@ Proof. apply (CRplus_lt_reg_l R (-y)). rewrite CRopp_mult_distr_l. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_lt_compat. apply CRlt_asym. apply CRopp_gt_lt_contravar, H0. @@ -552,12 +549,12 @@ Proof. rewrite (CRabs_morph _ ((x - y + (CRabs _ (a - y) - CRabs _ (a - x))) * CR_of_Q R (1 # 2))). rewrite CRabs_mult, (CRabs_right (CR_of_Q R (1 # 2))). - 2: rewrite <- CR_of_Q_zero; apply CR_of_Q_le; discriminate. + 2: apply CR_of_Q_le; discriminate. apply (CRle_trans _ ((CRabs _ (x - y) * 1 + CRabs _ (x-y) * 1) * CR_of_Q R (1 # 2))). apply CRmult_le_compat_r. - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate. + apply CR_of_Q_le. discriminate. apply (CRle_trans _ (CRabs _ (x - y) + CRabs _ (CRabs _ (a - y) - CRabs _ (a - x)))). apply CRabs_triang. rewrite CRmult_1_r. apply CRplus_le_compat_l. @@ -568,11 +565,11 @@ Proof. rewrite CRplus_comm, CRopp_plus_distr, <- CRplus_assoc. rewrite CRplus_opp_r, CRopp_involutive, CRplus_0_l. reflexivity. - rewrite <- CRmult_plus_distr_l, <- CR_of_Q_one. + rewrite <- CRmult_plus_distr_l. rewrite <- (CR_of_Q_plus R 1 1). rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 + 1) * (1 # 2))%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. apply CRle_refl. + rewrite CRmult_1_r. apply CRle_refl. unfold CRminus. apply CRmult_morph. 2: reflexivity. do 4 rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- CRplus_assoc. rewrite CRplus_comm, CRopp_plus_distr. @@ -587,10 +584,10 @@ Lemma CRmin_glb : forall {R : ConstructiveReals} (x y z:CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_le_reg_r (CR_of_Q R 2)). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. apply (CRplus_le_reg_l (CRabs _ (y-x) - (z*CR_of_Q R 2))). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite (CRplus_comm (CRabs R (y + - x) + - (z * CR_of_Q R 2))). @@ -601,13 +598,13 @@ Proof. rewrite CRopp_involutive, (CRplus_comm y), CRplus_assoc. apply CRplus_le_compat_l, (CRplus_le_reg_l y). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_compat; exact H0. - rewrite (CRplus_comm x), CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (-x)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. rewrite CRopp_mult_distr_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_compat; apply CRopp_ge_le_contravar; exact H. Qed. @@ -673,11 +670,11 @@ Lemma CRmax_lub : forall {R : ConstructiveReals} (x y z:CRcarrier R), x <= z -> y <= z -> CRmax x y <= z. Proof. intros. unfold CRmax. - apply (CRmult_le_reg_r (CR_of_Q _ 2)). rewrite <- CR_of_Q_zero. + apply (CRmult_le_reg_r (CR_of_Q _ 2)). apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. apply (CRplus_le_reg_l (-x-y)). rewrite <- CRplus_assoc. unfold CRminus. rewrite <- CRopp_plus_distr, CRplus_opp_l, CRplus_0_l. @@ -687,14 +684,14 @@ Proof. rewrite (CRplus_comm x), CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (-x)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRopp_plus_distr. apply CRplus_le_compat; apply CRopp_ge_le_contravar; assumption. - rewrite (CRplus_comm y), CRopp_plus_distr, CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l y). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. apply CRplus_le_compat; assumption. Qed. @@ -702,12 +699,12 @@ Lemma CRmax_l : forall {R : ConstructiveReals} (x y : CRcarrier R), x <= CRmax x y. Proof. intros. unfold CRmax. - apply (CRmult_le_reg_r (CR_of_Q R 2)). rewrite <- CR_of_Q_zero. + apply (CRmult_le_reg_r (CR_of_Q R 2)). apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - setoid_replace 2%Q with (1+1)%Q. rewrite CR_of_Q_plus, CR_of_Q_one. + rewrite CRmult_1_r. + setoid_replace 2%Q with (1+1)%Q. rewrite CR_of_Q_plus. rewrite CRmult_plus_distr_l, CRmult_1_r, CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (-y)). @@ -720,12 +717,12 @@ Lemma CRmax_r : forall {R : ConstructiveReals} (x y : CRcarrier R), y <= CRmax x y. Proof. intros. unfold CRmax. - apply (CRmult_le_reg_r (CR_of_Q _ 2)). rewrite <- CR_of_Q_zero. + apply (CRmult_le_reg_r (CR_of_Q _ 2)). apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite (CRplus_comm x). rewrite CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (-x)). @@ -754,14 +751,14 @@ Proof. intros. unfold CRmax. setoid_replace (x + z - (x + y)) with (z-y). apply (CRmult_eq_reg_r (CR_of_Q _ 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_plus_distr_r. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRmult_1_r. do 3 rewrite (CRplus_assoc x). apply CRplus_morph. reflexivity. do 2 rewrite <- CRplus_assoc. apply CRplus_morph. 2: reflexivity. @@ -777,11 +774,11 @@ Lemma CRmax_left : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmax. apply (CRmult_eq_reg_r (CR_of_Q R 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRabs_left. unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive. rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. reflexivity. @@ -793,11 +790,11 @@ Lemma CRmax_right : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmax. apply (CRmult_eq_reg_r (CR_of_Q R 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite (CRplus_comm x y). rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRabs_right. unfold CRminus. rewrite CRplus_comm. @@ -812,12 +809,12 @@ Proof. rewrite (CRabs_morph _ ((x - y + (CRabs _ (a - x) - CRabs _ (a - y))) * CR_of_Q R (1 # 2))). rewrite CRabs_mult, (CRabs_right (CR_of_Q R (1 # 2))). - 2: rewrite <- CR_of_Q_zero; apply CR_of_Q_le; discriminate. + 2: apply CR_of_Q_le; discriminate. apply (CRle_trans _ ((CRabs _ (x - y) * 1 + CRabs _ (x-y) * 1) * CR_of_Q R (1 # 2))). apply CRmult_le_compat_r. - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate. + apply CR_of_Q_le. discriminate. apply (CRle_trans _ (CRabs _ (x - y) + CRabs _ (CRabs _ (a - x) - CRabs _ (a - y)))). apply CRabs_triang. rewrite CRmult_1_r. apply CRplus_le_compat_l. @@ -829,11 +826,11 @@ Proof. rewrite CRplus_comm, CRopp_plus_distr, <- CRplus_assoc. rewrite CRplus_opp_r, CRopp_involutive, CRplus_0_l. reflexivity. - rewrite <- CRmult_plus_distr_l, <- CR_of_Q_one. + rewrite <- CRmult_plus_distr_l. rewrite <- (CR_of_Q_plus R 1 1). rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 + 1) * (1 # 2))%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. apply CRle_refl. + rewrite CRmult_1_r. apply CRle_refl. unfold CRminus. rewrite CRopp_mult_distr_l. rewrite <- CRmult_plus_distr_r. apply CRmult_morph. 2: reflexivity. do 4 rewrite CRplus_assoc. apply CRplus_morph. reflexivity. @@ -849,10 +846,10 @@ Lemma CRmax_lub_lt : forall {R : ConstructiveReals} (x y z : CRcarrier R), Proof. intros. unfold CRmax. apply (CRmult_lt_reg_r (CR_of_Q R 2)). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. apply (CRplus_lt_reg_l _ (-y -x)). unfold CRminus. rewrite CRplus_assoc, <- (CRplus_assoc (-x)), <- (CRplus_assoc (-x)). rewrite CRplus_opp_l, CRplus_0_l, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. @@ -861,14 +858,14 @@ Proof. apply CRplus_lt_compat_l. apply (CRplus_lt_reg_l _ y). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_lt_compat. apply CRlt_asym, H0. exact H0. - rewrite CRopp_plus_distr, CRopp_involutive. rewrite CRplus_assoc. apply CRplus_lt_compat_l. apply (CRplus_lt_reg_l _ x). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_lt_compat. apply CRlt_asym, H. exact H. Qed. diff --git a/theories/Reals/Abstract/ConstructiveLUB.v b/theories/Reals/Abstract/ConstructiveLUB.v index 4ae24de154..1c19c6aa40 100644 --- a/theories/Reals/Abstract/ConstructiveLUB.v +++ b/theories/Reals/Abstract/ConstructiveLUB.v @@ -108,7 +108,7 @@ Proof. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. apply le_S, H0. discriminate. - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate. + apply CR_of_Q_le. discriminate. Qed. Lemma is_upper_bound_dec : @@ -272,7 +272,7 @@ Proof. apply CR_of_Q_pos. reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult, (CR_of_Q_plus R 1 1). setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_plus_distr_l, CRmult_1_r, CRmult_1_r. + rewrite CRmult_plus_distr_l, CRmult_1_r, CRmult_1_r. apply CRplus_lt_compat_r. exact H0. } destruct (CR_cv_open_below _ _ l lcv H1) as [p pmaj]. assert (0 < (l-CR_of_Q R r) * CR_of_Q R (1#2)). @@ -280,7 +280,6 @@ Proof. apply CRplus_lt_compat_r. exact H0. apply CR_of_Q_pos. reflexivity. } destruct (CRup_nat (CRinv R _ (inr H2))) as [i imaj]. destruct i. exfalso. simpl in imaj. - rewrite CR_of_Q_zero in imaj. exact (CRlt_asym _ _ imaj (CRinv_0_lt_compat R _ (inr H2) H2)). specialize (pmaj (max (S i) (S p)) (le_trans p (S p) _ (le_S p p (le_refl p)) (Nat.le_max_r (S i) (S p)))). unfold proj1_sig in pmaj. @@ -309,7 +308,7 @@ Proof. CR_of_Q R (1 # Pos.of_nat (S i)))). apply CRlt_asym, imaj. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((Z.of_nat (S i) # 1) * (1 # Pos.of_nat (S i)))%Q with 1%Q. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. unfold CRminus. rewrite CRmult_plus_distr_r, (CRplus_comm (-CR_of_Q R r)). rewrite (CRplus_comm (CR_of_Q R r)), CRmult_plus_distr_r. rewrite CRplus_assoc. apply CRplus_le_compat_l. diff --git a/theories/Reals/Abstract/ConstructiveLimits.v b/theories/Reals/Abstract/ConstructiveLimits.v index 4a40cc8cb3..64dcd2e1ec 100644 --- a/theories/Reals/Abstract/ConstructiveLimits.v +++ b/theories/Reals/Abstract/ConstructiveLimits.v @@ -89,7 +89,7 @@ Lemma CR_cv_unique : forall {R : ConstructiveReals} (xn : nat -> CRcarrier R) -> CR_cv R xn b -> a == b. Proof. - intros. assert (CR_cv R (fun _ => CRzero R) (CRminus R b a)). + intros. assert (CR_cv R (fun _ => 0) (CRminus R b a)). { apply (CR_cv_extens (fun n => CRminus R (xn n) (xn n))). intro n. unfold CRminus. apply CRplus_opp_r. apply CR_cv_plus. exact H0. apply CR_cv_opp, H. } @@ -111,8 +111,7 @@ Proof. rewrite Qmult_1_r in pmaj. exact pmaj. unfold Qeq, Qnum, Qden; simpl. do 2 rewrite Pos.mul_1_r. reflexivity. apply (Qplus_lt_l _ _ q). ring_simplify. - apply (lt_CR_of_Q R q 0). apply (CRlt_le_trans _ (CRzero R) _ H). - apply CR_of_Q_zero. + apply (lt_CR_of_Q R q 0). exact H. apply (CRlt_le_trans _ (CRopp R z)). apply (CRle_lt_trans _ (CRopp R (CR_of_Q R q))). apply CR_of_Q_opp. apply CRopp_gt_lt_contravar, H0. @@ -131,8 +130,7 @@ Proof. setoid_replace ((Z.pos p # 1) * (1 # p))%Q with 1%Q in pmaj. rewrite Qmult_1_r in pmaj. exact pmaj. unfold Qeq, Qnum, Qden; simpl. do 2 rewrite Pos.mul_1_r. reflexivity. - apply (lt_CR_of_Q R 0 q). apply (CRle_lt_trans _ (CRzero R)). - 2: exact H0. apply CR_of_Q_zero. + apply (lt_CR_of_Q R 0 q). exact H0. apply (CRlt_le_trans _ _ _ H). apply (CRle_trans _ (CRabs R (CRopp R z))). apply (CRle_trans _ (CRabs R z)). @@ -140,10 +138,7 @@ Proof. apply H1. apply CRle_refl. apply CRabs_opp. apply CRabs_morph. unfold CRminus. symmetry. apply CRplus_0_l. - subst z. apply (CRplus_eq_reg_l (CRopp R a)). - apply (CReq_trans _ (CRzero R)). apply CRplus_opp_l. - destruct (CRisRing R). - apply (CReq_trans _ (CRplus R b (CRopp R a))). apply CReq_sym, H. - apply Radd_comm. + rewrite CRplus_opp_l, CRplus_comm. symmetry. exact H. Qed. Lemma CR_cv_eq : forall {R : ConstructiveReals} @@ -196,7 +191,7 @@ Lemma Un_cv_nat_real : forall {R : ConstructiveReals} Proof. intros. destruct (CR_archimedean R (CRinv R eps (inr H0))) as [k kmaj]. assert (0 < CR_of_Q R (Z.pos k # 1)). - { rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. } + { apply CR_of_Q_lt. reflexivity. } specialize (H k) as [p pmaj]. exists p. intros. apply (CRle_lt_trans _ (CR_of_Q R (1 # k))). @@ -204,7 +199,7 @@ Proof. apply (CRmult_lt_reg_l (CR_of_Q R (Z.pos k # 1))). exact H1. rewrite <- CR_of_Q_mult. apply (CRle_lt_trans _ 1). - rewrite <- CR_of_Q_one. apply CR_of_Q_le. + apply CR_of_Q_le. unfold Qle; simpl. do 2 rewrite Pos.mul_1_r. apply Z.le_refl. apply (CRmult_lt_reg_r (CRinv R eps (inr H0))). apply CRinv_0_lt_compat, H0. rewrite CRmult_1_l, CRmult_assoc. @@ -220,7 +215,7 @@ Lemma Un_cv_real_nat : forall {R : ConstructiveReals} Proof. intros. intros n. specialize (H (CR_of_Q R (1#n))) as [p pmaj]. - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. + apply CR_of_Q_lt. reflexivity. exists p. intros. apply CRlt_asym. apply pmaj. apply H. Qed. @@ -288,12 +283,12 @@ Proof. setoid_replace (1 # n * x)%Q with ((1 # n) *(1# x))%Q. 2: reflexivity. rewrite <- (CRmult_1_r (CR_of_Q R (1#n))). rewrite CR_of_Q_mult, CRmult_assoc. - apply CRmult_le_compat_l. rewrite <- CR_of_Q_zero. + apply CRmult_le_compat_l. apply CR_of_Q_le. discriminate. intro abs. apply (CRmult_lt_compat_l (CR_of_Q R (Z.pos x #1))) in abs. rewrite CRmult_1_r, <- CRmult_assoc, <- CR_of_Q_mult in abs. rewrite (CR_of_Q_morph R ((Z.pos x # 1) * (1 # x))%Q 1%Q) in abs. - rewrite CR_of_Q_one, CRmult_1_l in abs. + rewrite CRmult_1_l in abs. apply (CRlt_asym _ _ abs), (CRlt_trans _ (1 + CRabs R a)). 2: exact c. rewrite <- CRplus_0_l, <- CRplus_assoc. apply CRplus_lt_compat_r. rewrite CRplus_0_r. apply CRzero_lt_one. @@ -310,7 +305,7 @@ Lemma CR_cv_const : forall {R : ConstructiveReals} (a : CRcarrier R), Proof. intros a p. exists O. intros. unfold CRminus. rewrite CRplus_opp_r. - rewrite CRabs_right. rewrite <- CR_of_Q_zero. + rewrite CRabs_right. apply CR_of_Q_le. discriminate. apply CRle_refl. Qed. @@ -633,7 +628,7 @@ Lemma CR_double : forall {R : ConstructiveReals} (x:CRcarrier R), CR_of_Q R 2 * x == x + x. Proof. intros R x. rewrite (CR_of_Q_morph R 2 (1+1)). - 2: reflexivity. rewrite CR_of_Q_plus, CR_of_Q_one. + 2: reflexivity. rewrite CR_of_Q_plus. rewrite CRmult_plus_distr_r, CRmult_1_l. reflexivity. Qed. @@ -641,7 +636,7 @@ Lemma GeoCvZero : forall {R : ConstructiveReals}, CR_cv R (fun n:nat => CRpow (CR_of_Q R (1#2)) n) 0. Proof. intro R. assert (forall n:nat, INR n < CRpow (CR_of_Q R 2) n). - { induction n. unfold INR; simpl. rewrite CR_of_Q_zero. + { induction n. unfold INR; simpl. apply CRzero_lt_one. unfold INR. fold (1+n)%nat. rewrite Nat2Z.inj_add. rewrite (CR_of_Q_morph R _ ((Z.of_nat 1 # 1) + (Z.of_nat n #1))). @@ -651,29 +646,29 @@ Proof. with (CR_of_Q R 2 * CRpow (CR_of_Q R 2) n). 2: reflexivity. rewrite CR_double. apply CRplus_le_lt_compat. - 2: exact IHn. simpl. rewrite CR_of_Q_one. - apply pow_R1_Rle. rewrite <- CR_of_Q_one. apply CR_of_Q_le. discriminate. } + 2: exact IHn. simpl. + apply pow_R1_Rle. apply CR_of_Q_le. discriminate. } intros p. exists (Pos.to_nat p). intros. unfold CRminus. rewrite CRopp_0. rewrite CRplus_0_r. rewrite CRabs_right. - 2: apply pow_le; rewrite <- CR_of_Q_zero; apply CR_of_Q_le; discriminate. + 2: apply pow_le; apply CR_of_Q_le; discriminate. apply CRlt_asym. apply (CRmult_lt_reg_l (CR_of_Q R (Z.pos p # 1))). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. rewrite <- CR_of_Q_mult. + apply CR_of_Q_lt. reflexivity. rewrite <- CR_of_Q_mult. rewrite (CR_of_Q_morph R ((Z.pos p # 1) * (1 # p)) 1). 2: unfold Qmult, Qeq, Qnum, Qden; ring_simplify; reflexivity. apply (CRmult_lt_reg_r (CRpow (CR_of_Q R 2) i)). - apply pow_lt. simpl. rewrite <- CR_of_Q_zero. + apply pow_lt. simpl. apply CR_of_Q_lt. reflexivity. rewrite CRmult_assoc. rewrite pow_mult. rewrite (pow_proper (CR_of_Q R (1 # 2) * CR_of_Q R 2) 1), pow_one. - rewrite CRmult_1_r, CR_of_Q_one, CRmult_1_l. + rewrite CRmult_1_r, CRmult_1_l. apply (CRle_lt_trans _ (INR i)). 2: exact (H i). clear H. apply CR_of_Q_le. unfold Qle,Qnum,Qden. do 2 rewrite Z.mul_1_r. rewrite <- positive_nat_Z. apply Nat2Z.inj_le, H0. rewrite <- CR_of_Q_mult. setoid_replace ((1#2)*2)%Q with 1%Q. - apply CR_of_Q_one. reflexivity. + reflexivity. reflexivity. Qed. Lemma GeoFiniteSum : forall {R : ConstructiveReals} (n:nat), @@ -681,9 +676,9 @@ Lemma GeoFiniteSum : forall {R : ConstructiveReals} (n:nat), Proof. induction n. - unfold CRsum, CRpow. simpl (1%ConstructiveReals). - unfold CRminus. rewrite (CR_of_Q_morph R _ (1+1)). - rewrite CR_of_Q_plus, CR_of_Q_one, CRplus_assoc. - rewrite CRplus_opp_r, CRplus_0_r. reflexivity. reflexivity. + unfold CRminus. rewrite (CR_of_Q_plus R 1 1). + rewrite CRplus_assoc. + rewrite CRplus_opp_r, CRplus_0_r. reflexivity. - setoid_replace (CRsum (CRpow (CR_of_Q R (1 # 2))) (S n)) with (CRsum (CRpow (CR_of_Q R (1 # 2))) n + CRpow (CR_of_Q R (1 # 2)) (S n)). 2: reflexivity. @@ -701,7 +696,7 @@ Proof. 2: reflexivity. rewrite <- CRmult_assoc, <- CR_of_Q_mult. setoid_replace (2 * (1 # 2))%Q with 1%Q. - rewrite CR_of_Q_one. apply CRmult_1_l. reflexivity. + apply CRmult_1_l. reflexivity. Qed. Lemma GeoHalfBelowTwo : forall {R : ConstructiveReals} (n:nat), @@ -710,7 +705,7 @@ Proof. intros. rewrite <- (CRplus_0_r (CR_of_Q R 2)), GeoFiniteSum. apply CRplus_lt_compat_l. rewrite <- CRopp_0. apply CRopp_gt_lt_contravar. - apply pow_lt. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. + apply pow_lt. apply CR_of_Q_lt. reflexivity. Qed. Lemma GeoHalfTwo : forall {R : ConstructiveReals}, @@ -720,35 +715,35 @@ Proof. apply (CR_cv_eq _ (fun n => CR_of_Q R 2 - CRpow (CR_of_Q R (1 # 2)) n)). - intro n. rewrite GeoFiniteSum. reflexivity. - assert (forall n:nat, INR n < CRpow (CR_of_Q R 2) n). - { induction n. unfold INR; simpl. rewrite CR_of_Q_zero. + { induction n. unfold INR; simpl. apply CRzero_lt_one. apply (CRlt_le_trans _ (CRpow (CR_of_Q R 2) n + 1)). unfold INR. rewrite Nat2Z.inj_succ, <- Z.add_1_l. rewrite (CR_of_Q_morph R _ (1 + (Z.of_nat n #1))). 2: symmetry; apply Qinv_plus_distr. rewrite CR_of_Q_plus. - rewrite CRplus_comm. rewrite CR_of_Q_one. + rewrite CRplus_comm. apply CRplus_lt_compat_r, IHn. setoid_replace (CRpow (CR_of_Q R 2) (S n)) with (CRpow (CR_of_Q R 2) n + CRpow (CR_of_Q R 2) n). apply CRplus_le_compat. apply CRle_refl. - apply pow_R1_Rle. rewrite <- CR_of_Q_one. apply CR_of_Q_le. discriminate. + apply pow_R1_Rle. apply CR_of_Q_le. discriminate. rewrite <- CR_double. reflexivity. } intros n. exists (Pos.to_nat n). intros. setoid_replace (CR_of_Q R 2 - CRpow (CR_of_Q R (1 # 2)) i - CR_of_Q R 2) with (- CRpow (CR_of_Q R (1 # 2)) i). rewrite CRabs_opp. rewrite CRabs_right. assert (0 < CR_of_Q R 2). - { rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. } + { apply CR_of_Q_lt. reflexivity. } rewrite (pow_proper _ (CRinv R (CR_of_Q R 2) (inr H1))). rewrite pow_inv. apply CRlt_asym. apply (CRmult_lt_reg_l (CRpow (CR_of_Q R 2) i)). apply pow_lt, H1. rewrite CRinv_r. apply (CRmult_lt_reg_r (CR_of_Q R (Z.pos n#1))). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. + apply CR_of_Q_lt. reflexivity. rewrite CRmult_1_l, CRmult_assoc. rewrite <- CR_of_Q_mult. rewrite (CR_of_Q_morph R ((1 # n) * (Z.pos n # 1)) 1). 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. apply (CRle_lt_trans _ (INR i)). + rewrite CRmult_1_r. apply (CRle_lt_trans _ (INR i)). 2: apply H. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. destruct i. exfalso. inversion H0. pose proof (Pos2Nat.is_pos n). @@ -758,8 +753,8 @@ Proof. apply (CRmult_eq_reg_l (CR_of_Q R 2)). right. exact H1. rewrite CRinv_r. rewrite <- CR_of_Q_mult. setoid_replace (2 * (1 # 2))%Q with 1%Q. - apply CR_of_Q_one. reflexivity. - apply CRlt_asym, pow_lt. rewrite <- CR_of_Q_zero. + reflexivity. reflexivity. + apply CRlt_asym, pow_lt. apply CR_of_Q_lt. reflexivity. unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_l. reflexivity. @@ -929,5 +924,5 @@ Proof. intros n. exists (Pos.to_nat n). intros. unfold CRminus. simpl. rewrite CRopp_involutive, CRplus_opp_l. rewrite CRabs_right. - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate. apply CRle_refl. + apply CR_of_Q_le. discriminate. apply CRle_refl. Qed. diff --git a/theories/Reals/Abstract/ConstructiveReals.v b/theories/Reals/Abstract/ConstructiveReals.v index d91fd1183a..019428a5b0 100644 --- a/theories/Reals/Abstract/ConstructiveReals.v +++ b/theories/Reals/Abstract/ConstructiveReals.v @@ -101,9 +101,15 @@ Structure ConstructiveReals : Type := CRltDisjunctEpsilon : forall a b c d : CRcarrier, (CRltProp a b \/ CRltProp c d) -> CRlt a b + CRlt c d; - (* Constants *) - CRzero : CRcarrier; - CRone : CRcarrier; + (* The initial field morphism (in characteristic zero). + The abstract definition by iteration of addition is + probably the slowest. Let each instance implement + a faster (and often simpler) version. *) + CR_of_Q : Q -> CRcarrier; + CR_of_Q_lt : forall q r : Q, + Qlt q r -> CRlt (CR_of_Q q) (CR_of_Q r); + lt_CR_of_Q : forall q r : Q, + CRlt (CR_of_Q q) (CR_of_Q r) -> Qlt q r; (* Addition and multiplication *) CRplus : CRcarrier -> CRcarrier -> CRcarrier; @@ -111,19 +117,22 @@ Structure ConstructiveReals : Type := stronger than Prop-existence of opposite *) CRmult : CRcarrier -> CRcarrier -> CRcarrier; - CRisRing : ring_theory CRzero CRone CRplus CRmult + CR_of_Q_plus : forall q r : Q, CReq (CR_of_Q (q+r)) + (CRplus (CR_of_Q q) (CR_of_Q r)); + CR_of_Q_mult : forall q r : Q, CReq (CR_of_Q (q*r)) + (CRmult (CR_of_Q q) (CR_of_Q r)); + CRisRing : ring_theory (CR_of_Q 0) (CR_of_Q 1) CRplus CRmult (fun x y => CRplus x (CRopp y)) CRopp CReq; CRisRingExt : ring_eq_ext CRplus CRmult CRopp CReq; (* Compatibility with order *) - CRzero_lt_one : CRlt CRzero CRone; (* 0 # 1 would only allow 0 < 1 because - of Fmult_lt_0_compat so request 0 < 1 directly. *) + CRzero_lt_one : CRlt (CR_of_Q 0) (CR_of_Q 1); CRplus_lt_compat_l : forall r r1 r2 : CRcarrier, CRlt r1 r2 -> CRlt (CRplus r r1) (CRplus r r2); CRplus_lt_reg_l : forall r r1 r2 : CRcarrier, CRlt (CRplus r r1) (CRplus r r2) -> CRlt r1 r2; CRmult_lt_0_compat : forall x y : CRcarrier, - CRlt CRzero x -> CRlt CRzero y -> CRlt CRzero (CRmult x y); + CRlt (CR_of_Q 0) x -> CRlt (CR_of_Q 0) y -> CRlt (CR_of_Q 0) (CRmult x y); (* A constructive total inverse function on F would need to be continuous, which is impossible because we cannot connect plus and minus infinities. @@ -132,26 +141,11 @@ Structure ConstructiveReals : Type := To implement Finv by Cauchy sequences we need orderAppart, ~orderEq is not enough. *) - CRinv : forall x : CRcarrier, CRapart x CRzero -> CRcarrier; - CRinv_l : forall (r:CRcarrier) (rnz : CRapart r CRzero), - CReq (CRmult (CRinv r rnz) r) CRone; - CRinv_0_lt_compat : forall (r : CRcarrier) (rnz : CRapart r CRzero), - CRlt CRzero r -> CRlt CRzero (CRinv r rnz); - - (* The initial field morphism (in characteristic zero). - The abstract definition by iteration of addition is - probably the slowest. Let each instance implement - a faster (and often simpler) version. *) - CR_of_Q : Q -> CRcarrier; - CR_of_Q_plus : forall q r : Q, CReq (CR_of_Q (q+r)) - (CRplus (CR_of_Q q) (CR_of_Q r)); - CR_of_Q_mult : forall q r : Q, CReq (CR_of_Q (q*r)) - (CRmult (CR_of_Q q) (CR_of_Q r)); - CR_of_Q_one : CReq (CR_of_Q 1) CRone; - CR_of_Q_lt : forall q r : Q, - Qlt q r -> CRlt (CR_of_Q q) (CR_of_Q r); - lt_CR_of_Q : forall q r : Q, - CRlt (CR_of_Q q) (CR_of_Q r) -> Qlt q r; + CRinv : forall x : CRcarrier, CRapart x (CR_of_Q 0) -> CRcarrier; + CRinv_l : forall (r:CRcarrier) (rnz : CRapart r (CR_of_Q 0)), + CReq (CRmult (CRinv r rnz) r) (CR_of_Q 1); + CRinv_0_lt_compat : forall (r : CRcarrier) (rnz : CRapart r (CR_of_Q 0)), + CRlt (CR_of_Q 0) r -> CRlt (CR_of_Q 0) (CRinv r rnz); (* This function is very fast in both the Cauchy and Dedekind instances, because this rational number q is almost what @@ -213,8 +207,17 @@ Notation "x <= y <= z" := (CRle _ x y /\ CRle _ y z) : ConstructiveReals. Notation "x < y < z" := (prod (CRlt _ x y) (CRlt _ y z)) : ConstructiveReals. Notation "x == y" := (CReq _ x y) : ConstructiveReals. Notation "x ≶ y" := (CRapart _ x y) (at level 70, no associativity) : ConstructiveReals. -Notation "0" := (CRzero _) : ConstructiveReals. -Notation "1" := (CRone _) : ConstructiveReals. +Notation "0" := (CR_of_Q _ 0) : ConstructiveReals. +Notation "1" := (CR_of_Q _ 1) : ConstructiveReals. +Notation "2" := (CR_of_Q _ 2) : ConstructiveReals. +Notation "3" := (CR_of_Q _ 3) : ConstructiveReals. +Notation "4" := (CR_of_Q _ 4) : ConstructiveReals. +Notation "5" := (CR_of_Q _ 5) : ConstructiveReals. +Notation "6" := (CR_of_Q _ 6) : ConstructiveReals. +Notation "7" := (CR_of_Q _ 7) : ConstructiveReals. +Notation "8" := (CR_of_Q _ 8) : ConstructiveReals. +Notation "9" := (CR_of_Q _ 9) : ConstructiveReals. +Notation "10" := (CR_of_Q _ 10) : ConstructiveReals. Notation "x + y" := (CRplus _ x y) : ConstructiveReals. Notation "- x" := (CRopp _ x) : ConstructiveReals. Notation "x - y" := (CRminus _ x y) : ConstructiveReals. @@ -567,7 +570,7 @@ Lemma CRopp_involutive : forall {R : ConstructiveReals} (r : CRcarrier R), - - r == r. Proof. intros. apply (CRplus_eq_reg_l (CRopp R r)). - transitivity (CRzero R). apply CRisRing. + transitivity (CR_of_Q R 0). apply CRisRing. apply CReq_sym. transitivity (r + - r). apply CRisRing. apply CRisRing. Qed. @@ -578,7 +581,7 @@ Lemma CRopp_gt_lt_contravar Proof. intros. apply (CRplus_lt_reg_l R r1). destruct (CRisRing R). - apply (CRle_lt_trans _ (CRzero R)). apply Ropp_def. + apply (CRle_lt_trans _ 0). apply Ropp_def. apply (CRplus_lt_compat_l R (CRopp R r2)) in H. apply (CRle_lt_trans _ (CRplus R (CRopp R r2) r2)). apply (CRle_trans _ (CRplus R r2 (CRopp R r2))). @@ -611,13 +614,13 @@ Lemma CRopp_plus_distr : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R), Proof. intros. destruct (CRisRing R), (CRisRingExt R). apply (CRplus_eq_reg_l (CRplus R r1 r2)). - transitivity (CRzero R). apply Ropp_def. + transitivity (CR_of_Q R 0). apply Ropp_def. transitivity (r2 + r1 + (-r1 + -r2)). transitivity (r2 + (r1 + (-r1 + -r2))). transitivity (r2 + - r2). apply CReq_sym. apply Ropp_def. apply Radd_ext. apply CReq_refl. - transitivity (CRzero R + - r2). + transitivity (0 + - r2). apply CReq_sym, Radd_0_l. transitivity (r1 + - r1 + - r2). apply Radd_ext. 2: apply CReq_refl. apply CReq_sym, Ropp_def. @@ -701,7 +704,7 @@ Lemma CRopp_mult_distr_r : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R), - (r1 * r2) == r1 * (- r2). Proof. intros. apply (CRplus_eq_reg_l (CRmult R r1 r2)). - destruct (CRisRing R). transitivity (CRzero R). apply Ropp_def. + destruct (CRisRing R). transitivity (CR_of_Q R 0). apply Ropp_def. transitivity (r1 * (r2 + - r2)). 2: apply CRmult_plus_distr_l. transitivity (r1 * 0). @@ -725,7 +728,7 @@ Lemma CRmult_lt_compat_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R 0 < r -> r1 < r2 -> r1 * r < r2 * r. Proof. intros. apply (CRplus_lt_reg_r (CRopp R (CRmult R r1 r))). - apply (CRle_lt_trans _ (CRzero R)). + apply (CRle_lt_trans _ 0). apply (Ropp_def (CRisRing R)). apply (CRlt_le_trans _ (CRplus R (CRmult R r2 r) (CRmult R (CRopp R r1) r))). apply (CRlt_le_trans _ (CRmult R (CRplus R r2 (CRopp R r1)) r)). @@ -734,7 +737,7 @@ Proof. apply (CRle_lt_trans _ r1). apply (Radd_0_l (CRisRing R)). apply (CRlt_le_trans _ r2 _ H0). apply (CRle_trans _ (CRplus R r2 (CRplus R (CRopp R r1) r1))). - apply (CRle_trans _ (CRplus R r2 (CRzero R))). + apply (CRle_trans _ (CRplus R r2 0)). destruct (CRplus_0_r r2). exact H1. apply CRplus_le_compat_l. destruct (CRplus_opp_l r1). exact H1. destruct (Radd_assoc (CRisRing R) r2 (CRopp R r1) r1). exact H2. @@ -752,7 +755,7 @@ Proof. Qed. Lemma CRinv_r : forall {R : ConstructiveReals} (r:CRcarrier R) - (rnz : r ≶ (CRzero R)), + (rnz : r ≶ 0), r * (/ r) rnz == 1. Proof. intros. transitivity ((/ r) rnz * r). @@ -765,7 +768,7 @@ Proof. intros. apply (CRmult_lt_compat_r ((/ r) (inr H))) in H0. 2: apply CRinv_0_lt_compat, H. apply (CRle_lt_trans _ ((r1 * r) * ((/ r) (inr H)))). - - clear H0. apply (CRle_trans _ (CRmult R r1 (CRone R))). + - clear H0. apply (CRle_trans _ (CRmult R r1 1)). destruct (CRmult_1_r r1). exact H0. apply (CRle_trans _ (CRmult R r1 (CRmult R r ((/ r) (inr H))))). destruct (Rmul_ext (CRisRingExt R) r1 r1 (CReq_refl r1) @@ -779,7 +782,7 @@ Proof. apply (CRle_trans _ (r2 * (r * ((/ r) (inr H))))). destruct (Rmul_assoc (CRisRing R) r2 r ((/ r) (inr H))). exact H0. destruct (Rmul_ext (CRisRingExt R) r2 r2 (CReq_refl r2) - (r * ((/ r) (inr H))) (CRone R)). + (r * ((/ r) (inr H))) 1). apply CRinv_r. exact H1. Qed. @@ -829,7 +832,7 @@ Proof. apply CRmult_lt_compat_r. 2: exact abs. apply (CRplus_lt_reg_r r). apply (CRle_lt_trans _ r). apply (Radd_0_l (CRisRing R)). - apply (CRlt_le_trans _ (CRzero R) _ c). + apply (CRlt_le_trans _ 0 _ c). apply CRplus_opp_l. + intro abs. apply H0. apply CRopp_lt_cancel. apply (CRle_lt_trans _ (CRmult R r2 (CRopp R r))). @@ -839,7 +842,7 @@ Proof. apply CRmult_lt_compat_r. 2: exact abs. apply (CRplus_lt_reg_r r). apply (CRle_lt_trans _ r). apply (Radd_0_l (CRisRing R)). - apply (CRlt_le_trans _ (CRzero R) _ c). + apply (CRlt_le_trans _ 0 _ c). apply CRplus_opp_l. Qed. @@ -920,31 +923,21 @@ Proof. intros R x y H. apply CR_of_Q_morph; assumption. Qed. -Lemma CR_of_Q_zero : forall {R : ConstructiveReals}, - CR_of_Q R 0 == 0. -Proof. - intros. apply CRzero_double. - transitivity (CR_of_Q R (0+0)). apply CR_of_Q_morph. - reflexivity. apply CR_of_Q_plus. -Qed. - Lemma CR_of_Q_opp : forall {R : ConstructiveReals} (q : Q), CR_of_Q R (-q) == - CR_of_Q R q. Proof. intros. apply (CRplus_eq_reg_l (CR_of_Q R q)). - transitivity (CRzero R). + transitivity (CR_of_Q R 0). transitivity (CR_of_Q R (q-q)). apply CReq_sym, CR_of_Q_plus. - transitivity (CR_of_Q R 0). - apply CR_of_Q_morph. ring. apply CR_of_Q_zero. + apply CR_of_Q_morph. ring. apply CReq_sym. apply (CRisRing R). Qed. Lemma CR_of_Q_pos : forall {R : ConstructiveReals} (q:Q), Qlt 0 q -> 0 < CR_of_Q R q. Proof. - intros. apply (CRle_lt_trans _ (CR_of_Q R 0)). - apply CR_of_Q_zero. apply CR_of_Q_lt. exact H. + intros. apply CR_of_Q_lt. exact H. Qed. Lemma CR_of_Q_inv : forall {R : ConstructiveReals} (q : Q) (qPos : Qlt 0 q), @@ -954,7 +947,7 @@ Proof. intros. apply (CRmult_eq_reg_l (CR_of_Q R q)). right. apply CR_of_Q_pos, qPos. - rewrite CRinv_r, <- CR_of_Q_mult, <- CR_of_Q_one. + rewrite CRinv_r, <- CR_of_Q_mult. apply CR_of_Q_morph. field. intro abs. rewrite abs in qPos. exact (Qlt_irrefl 0 qPos). Qed. @@ -969,7 +962,7 @@ Proof. destruct (CR_archimedean R (b * ((/ -(a*b)) (inr epsPos)))) as [n maj]. assert (0 < CR_of_Q R (Z.pos n #1)) as nPos. - { rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. } + { apply CR_of_Q_lt. reflexivity. } assert (b * (/ CR_of_Q R (Z.pos n #1)) (inr nPos) < -(a*b)). { apply (CRmult_lt_reg_r (CR_of_Q R (Z.pos n #1))). apply nPos. rewrite <- (Rmul_assoc (CRisRing R)), CRinv_l, CRmult_1_r. @@ -1082,7 +1075,7 @@ Definition CRfloor {R : ConstructiveReals} (a : CRcarrier R) Proof. destruct (CR_Q_dense R (a - CR_of_Q R (1#2)) a) as [q qmaj]. - apply (CRlt_le_trans _ (a-0)). apply CRplus_lt_compat_l. - apply CRopp_gt_lt_contravar. rewrite <- CR_of_Q_zero. + apply CRopp_gt_lt_contravar. apply CR_of_Q_lt. reflexivity. unfold CRminus. rewrite CRopp_0, CRplus_0_r. apply CRle_refl. - exists (Qfloor q). destruct qmaj. split. diff --git a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v index bc44668e2f..cf302dc847 100644 --- a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v +++ b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v @@ -163,9 +163,8 @@ Lemma CRmorph_zero : forall {R1 R2 : ConstructiveReals} CRmorph f 0 == 0. Proof. intros. apply (CReq_trans _ (CRmorph f (CR_of_Q R1 0))). - apply CRmorph_proper. apply CReq_sym, CR_of_Q_zero. - apply (CReq_trans _ (CR_of_Q R2 0)). - apply CRmorph_rat. apply CR_of_Q_zero. + apply CRmorph_proper. reflexivity. + apply CRmorph_rat. Qed. Lemma CRmorph_one : forall {R1 R2 : ConstructiveReals} @@ -173,9 +172,8 @@ Lemma CRmorph_one : forall {R1 R2 : ConstructiveReals} CRmorph f 1 == 1. Proof. intros. apply (CReq_trans _ (CRmorph f (CR_of_Q R1 1))). - apply CRmorph_proper. apply CReq_sym, CR_of_Q_one. - apply (CReq_trans _ (CR_of_Q R2 1)). - apply CRmorph_rat. apply CR_of_Q_one. + apply CRmorph_proper. reflexivity. + apply CRmorph_rat. Qed. Lemma CRmorph_opp : forall {R1 R2 : ConstructiveReals} @@ -228,9 +226,9 @@ Lemma CRplus_pos_rat_lt : forall {R : ConstructiveReals} (x : CRcarrier R) (q : Qlt 0 q -> CRlt R x (CRplus R x (CR_of_Q R q)). Proof. intros. - apply (CRle_lt_trans _ (CRplus R x (CRzero R))). apply CRplus_0_r. + apply (CRle_lt_trans _ (CRplus R x 0)). apply CRplus_0_r. apply CRplus_lt_compat_l. - apply (CRle_lt_trans _ (CR_of_Q R 0)). apply CR_of_Q_zero. + apply (CRle_lt_trans _ (CR_of_Q R 0)). apply CRle_refl. apply CR_of_Q_lt. exact H. Defined. @@ -238,10 +236,10 @@ Lemma CRplus_neg_rat_lt : forall {R : ConstructiveReals} (x : CRcarrier R) (q : Qlt q 0 -> CRlt R (CRplus R x (CR_of_Q R q)) x. Proof. intros. - apply (CRlt_le_trans _ (CRplus R x (CRzero R))). 2: apply CRplus_0_r. + apply (CRlt_le_trans _ (CRplus R x 0)). 2: apply CRplus_0_r. apply CRplus_lt_compat_l. apply (CRlt_le_trans _ (CR_of_Q R 0)). - apply CR_of_Q_lt. exact H. apply CR_of_Q_zero. + apply CR_of_Q_lt. exact H. apply CRle_refl. Qed. Lemma CRmorph_plus_rat : forall {R1 R2 : ConstructiveReals} @@ -276,7 +274,7 @@ Proof. destruct (CRisRing R1). apply (CRle_trans _ (CRplus R1 x (CRplus R1 (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))))). - apply (CRle_trans _ (CRplus R1 x (CRzero R1))). + apply (CRle_trans _ (CRplus R1 x 0)). destruct (CRplus_0_r x). exact H. apply CRplus_le_compat_l. destruct (Ropp_def (CR_of_Q R1 q)). exact H. destruct (Radd_assoc x (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))). @@ -294,7 +292,7 @@ Proof. _ (CRplus R1 x (CRplus R1 (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))))). destruct (Radd_assoc x (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))). exact H0. - apply (CRle_trans _ (CRplus R1 x (CRzero R1))). + apply (CRle_trans _ (CRplus R1 x 0)). apply CRplus_le_compat_l. destruct (Ropp_def (CR_of_Q R1 q)). exact H1. destruct (CRplus_0_r x). exact H1. apply (CRlt_le_trans _ (CR_of_Q R1 (r-q))). @@ -379,12 +377,12 @@ Proof. apply CRmorph_proper. destruct (CRisRing R1). apply (CReq_trans _ (CRplus R1 x (CRplus R1 y (CRopp R1 y)))). apply CReq_sym, Radd_assoc. - apply (CReq_trans _ (CRplus R1 x (CRzero R1))). 2: apply CRplus_0_r. + apply (CReq_trans _ (CRplus R1 x 0)). 2: apply CRplus_0_r. destruct (CRisRingExt R1). apply Radd_ext. apply CReq_refl. apply Ropp_def. apply (CRplus_lt_reg_r (CRmorph f y)). apply (CRlt_le_trans _ _ _ abs). clear abs. - apply (CRle_trans _ (CRplus R2 (CRmorph f (CRplus R1 x y)) (CRzero R2))). + apply (CRle_trans _ (CRplus R2 (CRmorph f (CRplus R1 x y)) 0)). destruct (CRplus_0_r (CRmorph f (CRplus R1 x y))). exact H. apply (CRle_trans _ (CRplus R2 (CRmorph f (CRplus R1 x y)) (CRplus R2 (CRmorph f (CRopp R1 y)) (CRmorph f y)))). @@ -407,29 +405,26 @@ Lemma CRmorph_mult_pos : forall {R1 R2 : ConstructiveReals} Proof. induction n. - simpl. destruct (CRisRingExt R1). - apply (CReq_trans _ (CRzero R2)). - + apply (CReq_trans _ (CRmorph f (CRzero R1))). + apply (CReq_trans _ 0). + + apply (CReq_trans _ (CRmorph f 0)). 2: apply CRmorph_zero. apply CRmorph_proper. - apply (CReq_trans _ (CRmult R1 x (CRzero R1))). - 2: apply CRmult_0_r. apply Rmul_ext. apply CReq_refl. apply CR_of_Q_zero. - + apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRzero R2))). + apply (CReq_trans _ (CRmult R1 x 0)). + 2: apply CRmult_0_r. apply Rmul_ext. apply CReq_refl. reflexivity. + + apply (CReq_trans _ (CRmult R2 (CRmorph f x) 0)). apply CReq_sym, CRmult_0_r. destruct (CRisRingExt R2). - apply Rmul_ext0. apply CReq_refl. apply CReq_sym, CR_of_Q_zero. + apply Rmul_ext0. apply CReq_refl. reflexivity. - destruct (CRisRingExt R1), (CRisRingExt R2). - apply (CReq_trans - _ (CRmorph f (CRplus R1 x (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1)))))). + transitivity (CRmorph f (CRplus R1 x (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1))))). apply CRmorph_proper. - apply (CReq_trans - _ (CRmult R1 x (CRplus R1 (CRone R1) (CR_of_Q R1 (Z.of_nat n # 1))))). - apply Rmul_ext. apply CReq_refl. - apply (CReq_trans _ (CR_of_Q R1 (1 + (Z.of_nat n # 1)))). + transitivity (CRmult R1 x (CRplus R1 1 (CR_of_Q R1 (Z.of_nat n # 1)))). + apply Rmul_ext. reflexivity. + transitivity (CR_of_Q R1 (1 + (Z.of_nat n # 1))). apply CR_of_Q_morph. rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite Z.add_comm. rewrite Qinv_plus_distr. reflexivity. - apply (CReq_trans _ (CRplus R1 (CR_of_Q R1 1) (CR_of_Q R1 (Z.of_nat n # 1)))). - apply CR_of_Q_plus. apply Radd_ext. apply CR_of_Q_one. apply CReq_refl. - apply (CReq_trans _ (CRplus R1 (CRmult R1 x (CRone R1)) - (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1))))). - apply CRmult_plus_distr_l. apply Radd_ext. apply CRmult_1_r. apply CReq_refl. + rewrite CR_of_Q_plus. reflexivity. + transitivity (CRplus R1 (CRmult R1 x 1) + (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1)))). + apply CRmult_plus_distr_l. apply Radd_ext. apply CRmult_1_r. reflexivity. apply (CReq_trans _ (CRplus R2 (CRmorph f x) (CRmorph f (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1)))))). @@ -439,16 +434,16 @@ Proof. (CRmult R2 (CRmorph f x) (CR_of_Q R2 (Z.of_nat n # 1))))). apply Radd_ext0. apply CReq_refl. exact IHn. apply (CReq_trans - _ (CRmult R2 (CRmorph f x) (CRplus R2 (CRone R2) (CR_of_Q R2 (Z.of_nat n # 1))))). + _ (CRmult R2 (CRmorph f x) (CRplus R2 1 (CR_of_Q R2 (Z.of_nat n # 1))))). apply (CReq_trans - _ (CRplus R2 (CRmult R2 (CRmorph f x) (CRone R2)) + _ (CRplus R2 (CRmult R2 (CRmorph f x) 1) (CRmult R2 (CRmorph f x) (CR_of_Q R2 (Z.of_nat n # 1))))). apply Radd_ext0. 2: apply CReq_refl. apply CReq_sym, CRmult_1_r. apply CReq_sym, CRmult_plus_distr_l. apply Rmul_ext0. apply CReq_refl. apply (CReq_trans _ (CR_of_Q R2 (1 + (Z.of_nat n # 1)))). apply (CReq_trans _ (CRplus R2 (CR_of_Q R2 1) (CR_of_Q R2 (Z.of_nat n # 1)))). - apply Radd_ext0. apply CReq_sym, CR_of_Q_one. apply CReq_refl. + apply Radd_ext0. reflexivity. reflexivity. apply CReq_sym, CR_of_Q_plus. apply CR_of_Q_morph. rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite Z.add_comm. rewrite Qinv_plus_distr. reflexivity. @@ -501,7 +496,7 @@ Lemma CRmorph_mult_inv : forall {R1 R2 : ConstructiveReals} Proof. intros. apply (CRmult_eq_reg_r (CR_of_Q R2 (Z.pos p # 1))). left. apply (CRle_lt_trans _ (CR_of_Q R2 0)). - apply CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. + apply CRle_refl. apply CR_of_Q_lt. reflexivity. apply (CReq_trans _ (CRmorph f x)). - apply (CReq_trans _ (CRmorph f (CRmult R1 (CRmult R1 x (CR_of_Q R1 (1 # p))) @@ -511,22 +506,22 @@ Proof. _ (CRmult R1 x (CRmult R1 (CR_of_Q R1 (1 # p)) (CR_of_Q R1 (Z.pos p # 1))))). destruct (CRisRing R1). apply CReq_sym, Rmul_assoc. - apply (CReq_trans _ (CRmult R1 x (CRone R1))). + apply (CReq_trans _ (CRmult R1 x 1)). apply (Rmul_ext (CRisRingExt R1)). apply CReq_refl. apply (CReq_trans _ (CR_of_Q R1 ((1#p) * (Z.pos p # 1)))). apply CReq_sym, CR_of_Q_mult. apply (CReq_trans _ (CR_of_Q R1 1)). - apply CR_of_Q_morph. reflexivity. apply CR_of_Q_one. + apply CR_of_Q_morph. reflexivity. reflexivity. apply CRmult_1_r. - apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRmult R2 (CR_of_Q R2 (1 # p)) (CR_of_Q R2 (Z.pos p # 1))))). 2: apply (Rmul_assoc (CRisRing R2)). - apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRone R2))). + apply (CReq_trans _ (CRmult R2 (CRmorph f x) 1)). apply CReq_sym, CRmult_1_r. apply (Rmul_ext (CRisRingExt R2)). apply CReq_refl. apply (CReq_trans _ (CR_of_Q R2 1)). - apply CReq_sym, CR_of_Q_one. + reflexivity. apply (CReq_trans _ (CR_of_Q R2 ((1#p)*(Z.pos p # 1)))). apply CR_of_Q_morph. reflexivity. apply CR_of_Q_mult. Qed. @@ -571,7 +566,7 @@ Qed. Lemma CRmorph_mult_pos_pos_le : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x y : CRcarrier R1), - CRlt R1 (CRzero R1) y + CRlt R1 0 y -> CRmult R2 (CRmorph f x) (CRmorph f y) <= CRmorph f (CRmult R1 x y). Proof. @@ -590,20 +585,20 @@ Proof. apply Qlt_minus_iff in H1. rewrite H4 in H1. inversion H1. } destruct (CR_Q_dense R1 (CRplus R1 x (CR_of_Q R1 ((q-r) * (1#A)))) x) as [s [H4 H5]]. - - apply (CRlt_le_trans _ (CRplus R1 x (CRzero R1))). + - apply (CRlt_le_trans _ (CRplus R1 x 0)). 2: apply CRplus_0_r. apply CRplus_lt_compat_l. apply (CRplus_lt_reg_l R1 (CR_of_Q R1 ((r-q) * (1#A)))). - apply (CRle_lt_trans _ (CRzero R1)). + apply (CRle_lt_trans _ 0). apply (CRle_trans _ (CR_of_Q R1 ((r-q)*(1#A) + (q-r)*(1#A)))). destruct (CR_of_Q_plus R1 ((r-q)*(1#A)) ((q-r)*(1#A))). exact H0. apply (CRle_trans _ (CR_of_Q R1 0)). - 2: destruct (@CR_of_Q_zero R1); exact H4. + 2: apply CRle_refl. intro H4. apply lt_CR_of_Q in H4. ring_simplify in H4. inversion H4. apply (CRlt_le_trans _ (CR_of_Q R1 ((r - q) * (1 # A)))). 2: apply CRplus_0_r. apply (CRle_lt_trans _ (CR_of_Q R1 0)). - apply CR_of_Q_zero. apply CR_of_Q_lt. + apply CRle_refl. apply CR_of_Q_lt. rewrite <- (Qmult_0_r (r-q)). apply Qmult_lt_l. apply Qlt_minus_iff in H1. exact H1. reflexivity. - apply (CRmorph_increasing f) in H4. @@ -637,7 +632,7 @@ Proof. apply (CRlt_le_trans _ (CRmult R2 (CR_of_Q R2 ((q - r) * (1 # A))) (CRmorph f y))). apply (CRmult_lt_reg_l (CR_of_Q R2 (/((r-q)*(1#A))))). - apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CR_of_Q_zero. + apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CRle_refl. apply CR_of_Q_lt, Qinv_lt_0_compat. rewrite <- (Qmult_0_r (r-q)). apply Qmult_lt_l. apply Qlt_minus_iff in H1. exact H1. reflexivity. @@ -655,24 +650,24 @@ Proof. apply (CRlt_le_trans _ (CRmorph f (CR_of_Q R1 (Z.pos A # 1)))). apply CRmorph_increasing. exact Amaj. destruct (CRmorph_rat f (Z.pos A # 1)). exact H4. - apply (CRle_trans _ (CRmult R2 (CRopp R2 (CRone R2)) (CRmorph f y))). - apply (CRle_trans _ (CRopp R2 (CRmult R2 (CRone R2) (CRmorph f y)))). + apply (CRle_trans _ (CRmult R2 (CRopp R2 1) (CRmorph f y))). + apply (CRle_trans _ (CRopp R2 (CRmult R2 1 (CRmorph f y)))). destruct (Ropp_ext (CRisRingExt R2) (CRmorph f y) - (CRmult R2 (CRone R2) (CRmorph f y))). + (CRmult R2 1 (CRmorph f y))). apply CReq_sym, (Rmul_1_l (CRisRing R2)). exact H4. - destruct (CRopp_mult_distr_l (CRone R2) (CRmorph f y)). exact H4. + destruct (CRopp_mult_distr_l 1 (CRmorph f y)). exact H4. apply (CRle_trans _ (CRmult R2 (CRmult R2 (CR_of_Q R2 (/ ((r - q) * (1 # A)))) (CR_of_Q R2 ((q - r) * (1 # A)))) (CRmorph f y))). apply CRmult_le_compat_r_half. - apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. apply (CRle_trans _ (CR_of_Q R2 ((/ ((r - q) * (1 # A))) * ((q - r) * (1 # A))))). apply (CRle_trans _ (CR_of_Q R2 (-1))). apply (CRle_trans _ (CRopp R2 (CR_of_Q R2 1))). - destruct (Ropp_ext (CRisRingExt R2) (CRone R2) (CR_of_Q R2 1)). - apply CReq_sym, CR_of_Q_one. exact H4. + destruct (Ropp_ext (CRisRingExt R2) 1 (CR_of_Q R2 1)). + reflexivity. exact H4. destruct (@CR_of_Q_opp R2 1). exact H0. destruct (CR_of_Q_morph R2 (-1) (/ ((r - q) * (1 # A)) * ((q - r) * (1 # A)))). field. split. @@ -685,7 +680,7 @@ Proof. (CRmorph f y)). exact H0. apply CRmult_le_compat_r_half. - apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. destruct (CRmorph_rat f ((q - r) * (1 # A))). exact H0. + apply (CRle_trans _ (CRmorph f (CRmult R1 y (CR_of_Q R1 s)))). @@ -696,14 +691,14 @@ Proof. destruct (CRmorph_proper f (CRmult R1 y (CR_of_Q R1 s)) (CRmult R1 (CR_of_Q R1 s) y)). apply (Rmul_comm (CRisRing R1)). exact H4. - + apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. Qed. Lemma CRmorph_mult_pos_pos : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x y : CRcarrier R1), - CRlt R1 (CRzero R1) y + CRlt R1 0 y -> CRmorph f (CRmult R1 x y) == CRmult R2 (CRmorph f x) (CRmorph f y). Proof. @@ -718,10 +713,10 @@ Proof. destruct (CR_archimedean R1 y) as [A Amaj]. destruct (CR_Q_dense R1 x (CRplus R1 x (CR_of_Q R1 ((q-r) * (1#A))))) as [s [H4 H5]]. - - apply (CRle_lt_trans _ (CRplus R1 x (CRzero R1))). + - apply (CRle_lt_trans _ (CRplus R1 x 0)). apply CRplus_0_r. apply CRplus_lt_compat_l. apply (CRle_lt_trans _ (CR_of_Q R1 0)). - apply CR_of_Q_zero. apply CR_of_Q_lt. + apply CRle_refl. apply CR_of_Q_lt. rewrite <- (Qmult_0_r (q-r)). apply Qmult_lt_l. apply Qlt_minus_iff in H3. exact H3. reflexivity. - apply (CRmorph_increasing f) in H5. @@ -763,14 +758,14 @@ Proof. (CRmult R2 (CR_of_Q R2 ((q - r) * (1 # A))) (CRmorph f y)))). apply CRplus_le_compat_l, CRmult_le_compat_r_half. - apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. destruct (CRmorph_rat f ((q - r) * (1 # A))). exact H2. apply (CRlt_le_trans _ (CRplus R2 (CR_of_Q R2 r) (CR_of_Q R2 ((q - r))))). apply CRplus_lt_compat_l. * apply (CRmult_lt_reg_l (CR_of_Q R2 (/((q - r) * (1 # A))))). - apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CR_of_Q_zero. + apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CRle_refl. apply CR_of_Q_lt, Qinv_lt_0_compat. rewrite <- (Qmult_0_r (q-r)). apply Qmult_lt_l. apply Qlt_minus_iff in H3. exact H3. reflexivity. @@ -781,9 +776,9 @@ Proof. exact (proj2 (Rmul_assoc (CRisRing R2) (CR_of_Q R2 (/ ((q - r) * (1 # A)))) (CR_of_Q R2 ((q - r) * (1 # A))) (CRmorph f y))). - apply (CRle_trans _ (CRmult R2 (CRone R2) (CRmorph f y))). + apply (CRle_trans _ (CRmult R2 1 (CRmorph f y))). apply CRmult_le_compat_r_half. - apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. apply (CRle_trans _ (CR_of_Q R2 ((/ ((q - r) * (1 # A))) * ((q - r) * (1 # A))))). @@ -793,7 +788,7 @@ Proof. field_simplify. reflexivity. split. intro H5. inversion H5. intro H5. apply Qlt_minus_iff in H3. rewrite H5 in H3. inversion H3. exact H2. - destruct (CR_of_Q_one R2). exact H2. + apply CRle_refl. destruct (Rmul_1_l (CRisRing R2) (CRmorph f y)). intro H5. contradiction. apply (CRlt_le_trans _ (CR_of_Q R2 (Z.pos A # 1))). @@ -809,7 +804,7 @@ Proof. * apply (CRle_trans _ (CR_of_Q R2 (r + (q-r)))). exact (proj1 (CR_of_Q_plus R2 r (q-r))). destruct (CR_of_Q_morph R2 (r + (q-r)) q). ring. exact H2. - + apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. Qed. @@ -867,10 +862,10 @@ Lemma CRmorph_appart_zero : forall {R1 R2 : ConstructiveReals} CRmorph f x ≶ 0. Proof. intros. destruct app. - - left. apply (CRlt_le_trans _ (CRmorph f (CRzero R1))). + - left. apply (CRlt_le_trans _ (CRmorph f 0)). apply CRmorph_increasing. exact c. exact (proj2 (CRmorph_zero f)). - - right. apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + - right. apply (CRle_lt_trans _ (CRmorph f 0)). exact (proj1 (CRmorph_zero f)). apply CRmorph_increasing. exact c. Defined. @@ -885,7 +880,7 @@ Lemma CRmorph_inv : forall {R1 R2 : ConstructiveReals} Proof. intros. apply (CRmult_eq_reg_r (CRmorph f x)). destruct fxnz. right. exact c. left. exact c. - apply (CReq_trans _ (CRone R2)). + apply (CReq_trans _ 1). 2: apply CReq_sym, CRinv_l. apply (CReq_trans _ (CRmorph f (CRmult R1 ((/ x) xnz) x))). apply CReq_sym, CRmorph_mult. @@ -915,11 +910,11 @@ Proof. - simpl. unfold INR. rewrite (CRmorph_proper f _ (1 + CR_of_Q R1 (Z.of_nat n # 1))). rewrite CRmorph_plus. unfold INR in IHn. - rewrite IHn. rewrite CRmorph_one, <- CR_of_Q_one, <- CR_of_Q_plus. + rewrite IHn. rewrite CRmorph_one, <- CR_of_Q_plus. apply CR_of_Q_morph. rewrite Qinv_plus_distr. unfold Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_r. rewrite Nat2Z.inj_succ. rewrite <- Z.add_1_l. reflexivity. - rewrite <- CR_of_Q_one, <- CR_of_Q_plus. + rewrite <- CR_of_Q_plus. apply CR_of_Q_morph. rewrite Qinv_plus_distr. unfold Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_r. rewrite Nat2Z.inj_succ. rewrite <- Z.add_1_l. reflexivity. @@ -1047,7 +1042,7 @@ Proof. apply Pos2Z.pos_le_pos, Pos2Nat.inj_le. rewrite Nat2Pos.id. exact H0. destruct i. inversion H0. pose proof (Pos2Nat.is_pos p). rewrite H2 in H1. inversion H1. discriminate. - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate. + apply CR_of_Q_le. discriminate. rewrite CRplus_0_r. reflexivity. } pose proof (CR_cv_open_above _ _ _ H0 H) as [n nmaj]. apply (CRle_lt_trans _ (CR_of_Q R2 (let (q0, _) := CR_Q_limit x n in diff --git a/theories/Reals/Abstract/ConstructiveSum.v b/theories/Reals/Abstract/ConstructiveSum.v index 11c8e5d8a2..3be03bf615 100644 --- a/theories/Reals/Abstract/ConstructiveSum.v +++ b/theories/Reals/Abstract/ConstructiveSum.v @@ -60,11 +60,11 @@ Lemma sum_const : forall {R : ConstructiveReals} (a : CRcarrier R) (n : nat), CRsum (fun _ => a) n == a * INR (S n). Proof. induction n. - - unfold INR. simpl. rewrite CR_of_Q_one, CRmult_1_r. reflexivity. + - unfold INR. simpl. rewrite CRmult_1_r. reflexivity. - simpl. rewrite IHn. unfold INR. replace (Z.of_nat (S (S n))) with (Z.of_nat (S n) + 1)%Z. rewrite <- Qinv_plus_distr, CR_of_Q_plus, CRmult_plus_distr_l. - apply CRplus_morph. reflexivity. rewrite CR_of_Q_one, CRmult_1_r. reflexivity. + apply CRplus_morph. reflexivity. rewrite CRmult_1_r. reflexivity. replace 1%Z with (Z.of_nat 1). rewrite <- Nat2Z.inj_add. apply f_equal. rewrite Nat.add_comm. reflexivity. reflexivity. Qed. diff --git a/theories/Reals/Cauchy/ConstructiveRcomplete.v b/theories/Reals/Cauchy/ConstructiveRcomplete.v index be844c413a..754f9be5fe 100644 --- a/theories/Reals/Cauchy/ConstructiveRcomplete.v +++ b/theories/Reals/Cauchy/ConstructiveRcomplete.v @@ -309,12 +309,11 @@ Definition CRealConstructive : ConstructiveReals := Build_ConstructiveReals CReal CRealLt CRealLtIsLinear CRealLtProp CRealLtEpsilon CRealLtForget CRealLtDisjunctEpsilon - (inject_Q 0) (inject_Q 1) + inject_Q inject_Q_lt lt_inject_Q CReal_plus CReal_opp CReal_mult + inject_Q_plus inject_Q_mult CReal_isRing CReal_isRingExt CRealLt_0_1 CReal_plus_lt_compat_l CReal_plus_lt_reg_l CReal_mult_lt_0_compat CReal_inv CReal_inv_l CReal_inv_0_lt_compat - inject_Q inject_Q_plus inject_Q_mult - inject_Q_one inject_Q_lt lt_inject_Q CRealQ_dense Rup_pos CReal_abs CRealAbsLUB CRealComplete. |