diff options
| -rw-r--r-- | theories/QArith/QArith_base.v | 30 | ||||
| -rw-r--r-- | theories/Reals/ConstructiveCauchyReals.v | 634 | ||||
| -rw-r--r-- | theories/Reals/ConstructiveRIneq.v | 190 | ||||
| -rw-r--r-- | theories/Reals/ConstructiveRcomplete.v | 576 | ||||
| -rw-r--r-- | theories/Reals/Raxioms.v | 30 | ||||
| -rw-r--r-- | theories/Reals/Rdefinitions.v | 25 |
6 files changed, 982 insertions, 503 deletions
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 21bea6c315..1401f06986 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -726,6 +726,21 @@ Proof. exact (Z_lt_le_dec (Qnum x * QDen y) (Qnum y * QDen x)). Defined. +Lemma Qarchimedean : forall q : Q, { p : positive | Qlt q (Z.pos p # 1) }. +Proof. + intros. destruct q as [a b]. unfold Qlt. simpl. + rewrite Zmult_1_r. destruct a. + - exists xH. reflexivity. + - exists (p+1)%positive. apply (Z.lt_le_trans _ (Z.pos (p+1))). + apply Z.lt_succ_diag_r. rewrite Pos2Z.inj_mul. + rewrite <- (Zmult_1_r (Z.pos (p+1))). apply Z.mul_le_mono_nonneg. + discriminate. rewrite Zmult_1_r. apply Z.le_refl. discriminate. + apply Z2Nat.inj_le. discriminate. apply Pos2Z.is_nonneg. + apply Nat.le_succ_l. apply Nat2Z.inj_lt. + rewrite Z2Nat.id. apply Pos2Z.is_pos. apply Pos2Z.is_nonneg. + - exists xH. reflexivity. +Qed. + (** Compatibility of operations with respect to order. *) Lemma Qopp_le_compat : forall p q, p<=q -> -q <= -p. @@ -980,6 +995,21 @@ change (1/b < c). apply Qlt_shift_div_r; assumption. Qed. +Lemma Qinv_lt_contravar : forall a b : Q, + Qlt 0 a -> Qlt 0 b -> (Qlt a b <-> Qlt (/b) (/a)). +Proof. + intros. split. + - intro. rewrite <- Qmult_1_l. apply Qlt_shift_div_r. apply H0. + rewrite <- (Qmult_inv_r a). rewrite Qmult_comm. + apply Qmult_lt_l. apply Qinv_lt_0_compat. apply H. + apply H1. intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H). + - intro. rewrite <- (Qinv_involutive b). rewrite <- (Qmult_1_l (// b)). + apply Qlt_shift_div_l. apply Qinv_lt_0_compat. apply H0. + rewrite <- (Qmult_inv_r a). apply Qmult_lt_l. apply H. + apply H1. intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H). +Qed. + + (** * Rational to the n-th power *) Definition Qpower_positive : Q -> positive -> Q := diff --git a/theories/Reals/ConstructiveCauchyReals.v b/theories/Reals/ConstructiveCauchyReals.v index 3ca9248600..5de3c69e29 100644 --- a/theories/Reals/ConstructiveCauchyReals.v +++ b/theories/Reals/ConstructiveCauchyReals.v @@ -24,95 +24,9 @@ Open Scope Q. Constructive real numbers should be considered abstractly, forgetting the fact that they are implemented as rational sequences. All useful lemmas of this file are exposed in ConstructiveRIneq.v, - under more abstract names, like Rlt_asym instead of CRealLt_asym. *) + under more abstract names, like Rlt_asym instead of CRealLt_asym. -(* First some limit results about Q *) -Lemma Qarchimedean : forall q : Q, { p : positive | Qlt q (Z.pos p # 1) }. -Proof. - intros. destruct q. unfold Qlt. simpl. - rewrite Zmult_1_r. destruct Qnum. - - exists xH. reflexivity. - - exists (p+1)%positive. apply (Z.lt_le_trans _ (Z.pos (p+1))). - apply Z.lt_succ_diag_r. rewrite Pos2Z.inj_mul. - rewrite <- (Zmult_1_r (Z.pos (p+1))). apply Z.mul_le_mono_nonneg. - discriminate. rewrite Zmult_1_r. apply Z.le_refl. discriminate. - apply Z2Nat.inj_le. discriminate. apply Pos2Z.is_nonneg. - apply Nat.le_succ_l. apply Nat2Z.inj_lt. - rewrite Z2Nat.id. apply Pos2Z.is_pos. apply Pos2Z.is_nonneg. - - exists xH. reflexivity. -Qed. - -Lemma Qinv_lt_contravar : forall a b : Q, - Qlt 0 a -> Qlt 0 b -> (Qlt a b <-> Qlt (/b) (/a)). -Proof. - intros. split. - - intro. rewrite <- Qmult_1_l. apply Qlt_shift_div_r. apply H0. - rewrite <- (Qmult_inv_r a). rewrite Qmult_comm. - apply Qmult_lt_l. apply Qinv_lt_0_compat. apply H. - apply H1. intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H). - - intro. rewrite <- (Qinv_involutive b). rewrite <- (Qmult_1_l (// b)). - apply Qlt_shift_div_l. apply Qinv_lt_0_compat. apply H0. - rewrite <- (Qmult_inv_r a). apply Qmult_lt_l. apply H. - apply H1. intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H). -Qed. - -Lemma Qabs_separation : forall q : Q, - (forall k:positive, Qlt (Qabs q) (1 # k)) - -> q == 0. -Proof. - intros. destruct (Qle_lt_or_eq 0 (Qabs q)). apply Qabs_nonneg. - - exfalso. destruct (Qarchimedean (Qinv (Qabs q))) as [p maj]. - specialize (H p). apply (Qlt_not_le (/ Qabs q) (Z.pos p # 1)). - apply maj. apply Qlt_le_weak. - setoid_replace (Z.pos p # 1) with (/(1#p)). 2: reflexivity. - rewrite <- Qinv_lt_contravar. apply H. apply H0. - reflexivity. - - destruct q. unfold Qeq in H0. simpl in H0. - rewrite Zmult_1_r in H0. replace Qnum with 0%Z. reflexivity. - destruct (Zabs_dec Qnum). rewrite e. rewrite H0. reflexivity. - rewrite e. rewrite <- H0. ring. -Qed. - -Lemma Qle_limit : forall (a b : Q), - (forall eps:Q, Qlt 0 eps -> Qlt a (b + eps)) - -> Qle a b. -Proof. - intros. destruct (Q_dec a b). destruct s. - apply Qlt_le_weak. assumption. exfalso. - assert (0 < a - b). unfold Qminus. apply (Qlt_minus_iff b a). - assumption. specialize (H (a-b) H0). - apply (Qlt_irrefl a). ring_simplify in H. assumption. - rewrite q. apply Qle_refl. -Qed. - -Lemma Qopp_lt_compat : forall p q, p<q -> -q < -p. -Proof. - intros (a1,a2) (b1,b2); unfold Qlt; simpl. - rewrite !Z.mul_opp_l. omega. -Qed. - -Lemma Qmult_minus_one : forall q : Q, inject_Z (-1) * q == - q. -Proof. - intros. field. -Qed. - -Lemma Qsub_comm : forall a b : Q, - a + b == b - a. -Proof. - intros. unfold Qeq. simpl. rewrite Pos.mul_comm. ring. -Qed. - -Lemma PosLt_le_total : forall p q, Pos.lt p q \/ Pos.le q p. -Proof. - intros. destruct (Pos.lt_total p q). left. assumption. - right. destruct H. subst q. apply Pos.le_refl. unfold Pos.lt in H. - unfold Pos.le. rewrite H. discriminate. -Qed. - - - - -(* Cauchy reals are Cauchy sequences of rational numbers, equipped with explicit moduli of convergence and an equivalence relation (the difference converges to zero). @@ -301,77 +215,6 @@ Bind Scope R_scope_constr with CReal. Open Scope R_scope_constr. - - -(* The equality on Cauchy reals is just QSeqEquiv, - which is independant of the convergence modulus. *) -Lemma CRealEq_modindep : forall (x y : CReal), - QSeqEquivEx (proj1_sig x) (proj1_sig y) - <-> forall n:positive, Qle (Qabs (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n))) - (2 # n). -Proof. - intros [xn limx] [yn limy]. unfold proj1_sig. split. - - intros [cvmod H] n. unfold proj1_sig in H. - apply Qle_limit. intros. - destruct (Qarchimedean (/eps)) as [k maj]. - remember (max (cvmod k) (Pos.to_nat n)) as p. - assert (le (cvmod k) p). - { rewrite Heqp. apply Nat.le_max_l. } - assert (Pos.to_nat n <= p)%nat. - { rewrite Heqp. apply Nat.le_max_r. } - specialize (H k p p H1 H1). - setoid_replace (xn (Pos.to_nat n) - yn (Pos.to_nat n)) - with (xn (Pos.to_nat n) - xn p + (xn p - yn p + (yn p - yn (Pos.to_nat n)))). - apply (Qle_lt_trans _ (Qabs (xn (Pos.to_nat n) - xn p) - + Qabs (xn p - yn p + (yn p - yn (Pos.to_nat n))))). - apply Qabs_triangle. - setoid_replace (2 # n) with ((1 # n) + (1#n)). rewrite <- Qplus_assoc. - apply Qplus_lt_le_compat. - apply limx. apply le_refl. assumption. - apply (Qle_trans _ (Qabs (xn p - yn p) + Qabs (yn p - yn (Pos.to_nat n)))). - apply Qabs_triangle. rewrite (Qplus_comm (1#n)). apply Qplus_le_compat. - apply Qle_lteq. left. apply (Qlt_trans _ (1 # k)). - assumption. - setoid_replace (Z.pos k #1) with (/ (1#k)) in maj. 2: reflexivity. - apply Qinv_lt_contravar. reflexivity. apply H0. apply maj. - apply Qle_lteq. left. - apply limy. assumption. apply le_refl. - ring_simplify. reflexivity. field. - - intros. exists (fun q => Pos.to_nat (2 * (3 * q))). intros k p q H0 H1. - unfold proj1_sig. specialize (H (2 * (3 * k))%positive). - assert ((Pos.to_nat (3 * k) <= Pos.to_nat (2 * (3 * k)))%nat). - { generalize (3 * k)%positive. intros. rewrite Pos2Nat.inj_mul. - rewrite <- (mult_1_l (Pos.to_nat p0)). apply Nat.mul_le_mono_nonneg. - auto. unfold Pos.to_nat. simpl. auto. - apply (le_trans 0 1). auto. apply Pos2Nat.is_pos. rewrite mult_1_l. - apply le_refl. } - setoid_replace (xn p - yn q) - with (xn p - xn (Pos.to_nat (2 * (3 * k))) - + (xn (Pos.to_nat (2 * (3 * k))) - yn (Pos.to_nat (2 * (3 * k))) - + (yn (Pos.to_nat (2 * (3 * k))) - yn q))). - setoid_replace (1 # k) with ((1 # 3 * k) + ((1 # 3 * k) + (1 # 3 * k))). - apply (Qle_lt_trans - _ (Qabs (xn p - xn (Pos.to_nat (2 * (3 * k)))) - + (Qabs (xn (Pos.to_nat (2 * (3 * k))) - yn (Pos.to_nat (2 * (3 * k))) - + (yn (Pos.to_nat (2 * (3 * k))) - yn q))))). - apply Qabs_triangle. apply Qplus_lt_le_compat. - apply limx. apply (le_trans _ (Pos.to_nat (2 * (3 * k)))). assumption. assumption. - assumption. - apply (Qle_trans - _ (Qabs (xn (Pos.to_nat (2 * (3 * k))) - yn (Pos.to_nat (2 * (3 * k)))) - + Qabs (yn (Pos.to_nat (2 * (3 * k))) - yn q))). - apply Qabs_triangle. apply Qplus_le_compat. - setoid_replace (1 # 3 * k) with (2 # 2 * (3 * k)). apply H. - rewrite (factorDenom _ _ 3). rewrite (factorDenom _ _ 2). rewrite (factorDenom _ _ 3). - rewrite Qmult_assoc. rewrite (Qmult_comm (1#2)). - rewrite <- Qmult_assoc. apply Qmult_comp. reflexivity. - unfold Qeq. reflexivity. - apply Qle_lteq. left. apply limy. assumption. - apply (le_trans _ (Pos.to_nat (2 * (3 * k)))). assumption. assumption. - rewrite (factorDenom _ _ 3). ring_simplify. reflexivity. field. -Qed. - - (* So QSeqEquiv is the equivalence relation of this constructive pre-order *) Definition CRealLt (x y : CReal) : Prop := exists n : positive, Qlt (2 # n) @@ -409,6 +252,30 @@ Proof. (proj1_sig y (S n) - proj1_sig x (S n))); assumption. Qed. +(* CRealLt is decided by the LPO in Type, + which is a non-constructive oracle. *) +Lemma CRealLt_lpo_dec : forall x y : CReal, + (forall (P : nat -> Prop), (forall n, {P n} + {~P n}) + -> {n | ~P n} + {forall n, P n}) + -> { CRealLt x y } + { ~CRealLt x y }. +Proof. + intros x y lpo. + destruct (lpo (fun n:nat => Qle (proj1_sig y (S n) - proj1_sig x (S n)) + (2 # Pos.of_nat (S n)))). + - intro n. destruct (Qlt_le_dec (2 # Pos.of_nat (S n)) + (proj1_sig y (S n) - proj1_sig x (S n))). + right. apply Qlt_not_le. exact q. left. exact q. + - left. destruct s as [n nmaj]. exists (Pos.of_nat (S n)). + rewrite Nat2Pos.id. apply Qnot_le_lt. exact nmaj. discriminate. + - right. intro abs. destruct abs as [n majn]. + specialize (q (pred (Pos.to_nat n))). + replace (S (pred (Pos.to_nat n))) with (Pos.to_nat n) in q. + rewrite Pos2Nat.id in q. + pose proof (Qle_not_lt _ _ q). contradiction. + symmetry. apply Nat.succ_pred. intro abs. + pose proof (Pos2Nat.is_pos n). rewrite abs in H. inversion H. +Qed. + (* Alias the quotient order equality *) Definition CRealEq (x y : CReal) : Prop := ~CRealLt x y /\ ~CRealLt y x. @@ -465,6 +332,79 @@ Proof. apply Qle_Qabs. apply H. Qed. +(* The equality on Cauchy reals is just QSeqEquiv, + which is independant of the convergence modulus. *) +Lemma CRealEq_modindep : forall (x y : CReal), + QSeqEquivEx (proj1_sig x) (proj1_sig y) + <-> forall n:positive, + Qle (Qabs (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n))) (2 # n). +Proof. + assert (forall x y: CReal, QSeqEquivEx (proj1_sig x) (proj1_sig y) -> x <= y ). + { intros [xn limx] [yn limy] [cvmod H] [n abs]. simpl in abs, H. + pose (xn (Pos.to_nat n) - yn (Pos.to_nat n) - (2#n)) as eps. + destruct (Qarchimedean (/eps)) as [k maj]. + remember (max (cvmod k) (Pos.to_nat n)) as p. + assert (le (cvmod k) p). + { rewrite Heqp. apply Nat.le_max_l. } + assert (Pos.to_nat n <= p)%nat. + { rewrite Heqp. apply Nat.le_max_r. } + specialize (H k p p H0 H0). + setoid_replace (Z.pos k #1)%Q with (/ (1#k)) in maj. 2: reflexivity. + apply Qinv_lt_contravar in maj. 2: reflexivity. unfold eps in maj. + clear abs. (* less precise majoration *) + apply (Qplus_lt_r _ _ (2#n)) in maj. ring_simplify in maj. + apply (Qlt_not_le _ _ maj). clear maj. + setoid_replace (xn (Pos.to_nat n) + -1 * yn (Pos.to_nat n)) + with (xn (Pos.to_nat n) - xn p + (xn p - yn p + (yn p - yn (Pos.to_nat n)))). + 2: ring. + setoid_replace (2 # n)%Q with ((1 # n) + (1#n)). + rewrite <- Qplus_assoc. + apply Qplus_le_compat. apply (Qle_trans _ _ _ (Qle_Qabs _)). + apply Qlt_le_weak. apply limx. apply le_refl. assumption. + rewrite (Qplus_comm (1#n)). + apply Qplus_le_compat. apply (Qle_trans _ _ _ (Qle_Qabs _)). + apply Qlt_le_weak. exact H. + apply (Qle_trans _ _ _ (Qle_Qabs _)). apply Qlt_le_weak. apply limy. + assumption. apply le_refl. ring_simplify. reflexivity. + unfold eps. unfold Qminus. rewrite <- Qlt_minus_iff. exact abs. } + split. + - rewrite <- CRealEq_diff. intros. split. + apply H, QSeqEquivEx_sym. exact H0. apply H. exact H0. + - clear H. intros. destruct x as [xn limx], y as [yn limy]. + exists (fun q => Pos.to_nat (2 * (3 * q))). intros k p q H0 H1. + unfold proj1_sig. specialize (H (2 * (3 * k))%positive). + assert ((Pos.to_nat (3 * k) <= Pos.to_nat (2 * (3 * k)))%nat). + { generalize (3 * k)%positive. intros. rewrite Pos2Nat.inj_mul. + rewrite <- (mult_1_l (Pos.to_nat p0)). apply Nat.mul_le_mono_nonneg. + auto. unfold Pos.to_nat. simpl. auto. + apply (le_trans 0 1). auto. apply Pos2Nat.is_pos. rewrite mult_1_l. + apply le_refl. } + setoid_replace (xn p - yn q) + with (xn p - xn (Pos.to_nat (2 * (3 * k))) + + (xn (Pos.to_nat (2 * (3 * k))) - yn (Pos.to_nat (2 * (3 * k))) + + (yn (Pos.to_nat (2 * (3 * k))) - yn q))). + setoid_replace (1 # k)%Q with ((1 # 3 * k) + ((1 # 3 * k) + (1 # 3 * k))). + apply (Qle_lt_trans + _ (Qabs (xn p - xn (Pos.to_nat (2 * (3 * k)))) + + (Qabs (xn (Pos.to_nat (2 * (3 * k))) - yn (Pos.to_nat (2 * (3 * k))) + + (yn (Pos.to_nat (2 * (3 * k))) - yn q))))). + apply Qabs_triangle. apply Qplus_lt_le_compat. + apply limx. apply (le_trans _ (Pos.to_nat (2 * (3 * k)))). assumption. assumption. + assumption. + apply (Qle_trans + _ (Qabs (xn (Pos.to_nat (2 * (3 * k))) - yn (Pos.to_nat (2 * (3 * k)))) + + Qabs (yn (Pos.to_nat (2 * (3 * k))) - yn q))). + apply Qabs_triangle. apply Qplus_le_compat. + setoid_replace (1 # 3 * k)%Q with (2 # 2 * (3 * k))%Q. apply H. + rewrite (factorDenom _ _ 3). rewrite (factorDenom _ _ 2). rewrite (factorDenom _ _ 3). + rewrite Qmult_assoc. rewrite (Qmult_comm (1#2)). + rewrite <- Qmult_assoc. apply Qmult_comp. reflexivity. + unfold Qeq. reflexivity. + apply Qle_lteq. left. apply limy. assumption. + apply (le_trans _ (Pos.to_nat (2 * (3 * k)))). assumption. assumption. + rewrite (factorDenom _ _ 3). ring_simplify. reflexivity. field. +Qed. + (* Extend separation to all indices above *) Lemma CRealLt_aboveSig : forall (x y : CReal) (n : positive), (Qlt (2 # n) @@ -565,17 +505,12 @@ Proof. intros x y H [n q]. apply CRealLt_above in H. destruct H as [p H]. pose proof (CRealLt_above_same y x n q). - destruct (PosLt_le_total n p). - - apply (Qlt_not_le (proj1_sig y (Pos.to_nat p)) (proj1_sig x (Pos.to_nat p))). - apply H0. unfold Pos.le. unfold Pos.lt in H1. rewrite H1. discriminate. - apply Qlt_le_weak. apply (Qplus_lt_l _ _ (-proj1_sig x (Pos.to_nat p))). - rewrite Qplus_opp_r. apply (Qlt_trans _ (2#p)). - unfold Qlt. simpl. unfold Z.lt. auto. apply H. apply Pos.le_refl. - - apply (Qlt_not_le (proj1_sig y (Pos.to_nat n)) (proj1_sig x (Pos.to_nat n))). - apply H0. apply Pos.le_refl. apply Qlt_le_weak. - apply (Qplus_lt_l _ _ (-proj1_sig x (Pos.to_nat n))). - rewrite Qplus_opp_r. apply (Qlt_trans _ (2#p)). - unfold Qlt. simpl. unfold Z.lt. auto. apply H. assumption. + apply (Qlt_not_le (proj1_sig y (Pos.to_nat (Pos.max n p))) + (proj1_sig x (Pos.to_nat (Pos.max n p)))). + apply H0. apply Pos.le_max_l. + apply Qlt_le_weak. apply (Qplus_lt_l _ _ (-proj1_sig x (Pos.to_nat (Pos.max n p)))). + rewrite Qplus_opp_r. apply (Qlt_trans _ (2#p)). + unfold Qlt. simpl. unfold Z.lt. auto. apply H. apply Pos.le_max_r. Qed. Lemma CRealLt_irrefl : forall x:CReal, ~(x < x). @@ -656,9 +591,10 @@ Proof. rewrite <- Qplus_assoc. rewrite <- Qplus_0_l. rewrite <- (Qplus_opp_r (1#n)). rewrite (Qplus_comm (1#n)). rewrite <- Qplus_assoc. apply Qplus_lt_le_compat. - + apply (Qplus_lt_l _ _ (1#n)). rewrite Qplus_opp_r. - apply (Qplus_lt_r _ _ (yn (Pos.to_nat n) - yn (Pos.to_nat (Pos.max n (4 * k))))). - ring_simplify. rewrite Qmult_minus_one. + + apply (Qplus_lt_r _ _ (yn (Pos.to_nat n) - yn (Pos.to_nat (Pos.max n (4 * k))) + (1#n))) + ; ring_simplify. + setoid_replace (-1 * yn (Pos.to_nat (Pos.max n (4 * k)))) + with (- yn (Pos.to_nat (Pos.max n (4 * k)))). 2: ring. apply (Qle_lt_trans _ (Qabs (yn (Pos.to_nat n) - yn (Pos.to_nat (Pos.max n (4 * k)))))). apply Qle_Qabs. apply limy. apply le_refl. apply H. @@ -692,13 +628,19 @@ Proof. Qed. Lemma CRealLt_Le_trans : forall x y z : CReal, - CRealLt x y - -> CRealLe y z -> CRealLt x z. + x < y -> y <= z -> x < z. Proof. intros. destruct (linear_order_T x z y H). apply c. contradiction. Qed. +Lemma CRealLe_trans : forall x y z : CReal, + x <= y -> y <= z -> x <= z. +Proof. + intros. intro abs. apply H0. + apply (CRealLt_Le_trans _ x); assumption. +Qed. + Lemma CRealLt_trans : forall x y z : CReal, x < y -> y < z -> x < z. Proof. @@ -981,7 +923,7 @@ Proof. destruct x as [xn limx]. exists (fun n : nat => - xn n). intros k p q H H0. unfold Qminus. rewrite Qopp_involutive. - rewrite Qsub_comm. apply limx; assumption. + rewrite Qplus_comm. apply limx; assumption. Defined. Notation "- x" := (CReal_opp x) : R_scope_constr. @@ -1060,6 +1002,12 @@ Proof. apply H. Qed. +Lemma CReal_plus_0_r : forall r : CReal, + r + 0 == r. +Proof. + intro r. rewrite CReal_plus_comm. apply CReal_plus_0_l. +Qed. + Lemma CReal_plus_lt_compat_l : forall x y z : CReal, CRealLt y z @@ -1080,9 +1028,7 @@ Proof. Qed. Lemma CReal_plus_lt_reg_l : - forall x y z : CReal, - CRealLt (CReal_plus x y) (CReal_plus x z) - -> CRealLt y z. + forall x y z : CReal, x + y < x + z -> y < z. Proof. intros. destruct H as [n maj]. exists (2*n)%positive. setoid_replace (proj1_sig z (Pos.to_nat (2 * n)) - proj1_sig y (Pos.to_nat (2 * n)))%Q @@ -1095,6 +1041,27 @@ Proof. simpl; ring. Qed. +Lemma CReal_plus_lt_reg_r : + forall x y z : CReal, y + x < z + x -> y < z. +Proof. + intros x y z H. rewrite (CReal_plus_comm y), (CReal_plus_comm z) in H. + apply CReal_plus_lt_reg_l in H. exact H. +Qed. + +Lemma CReal_plus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2. +Proof. + intros. intro abs. apply CReal_plus_lt_reg_l in abs. contradiction. +Qed. + +Lemma CReal_plus_le_lt_compat : + forall r1 r2 r3 r4 : CReal, r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4. +Proof. + intros; apply CRealLe_Lt_trans with (r2 + r3). + intro abs. rewrite CReal_plus_comm, (CReal_plus_comm r1) in abs. + apply CReal_plus_lt_reg_l in abs. contradiction. + apply CReal_plus_lt_compat_l; exact H0. +Qed. + Lemma CReal_plus_opp_r : forall x : CReal, x + - x == 0. Proof. @@ -1105,6 +1072,12 @@ Proof. unfold Qle. simpl. unfold Z.le. intro absurd. inversion absurd. field. Qed. +Lemma CReal_plus_opp_l : forall x : CReal, + - x + x == 0. +Proof. + intro x. rewrite CReal_plus_comm. apply CReal_plus_opp_r. +Qed. + Lemma CReal_plus_proper_r : forall x y z : CReal, CRealEq x y -> CRealEq (CReal_plus x z) (CReal_plus y z). Proof. @@ -1144,7 +1117,7 @@ Proof. - intro abs. apply (CReal_plus_lt_compat_l r) in abs. contradiction. Qed. -Fixpoint BoundFromZero (qn : nat -> Q) (k : nat) (A : positive) {struct k} +Fixpoint BoundFromZero (qn : nat -> Q) (k : nat) (A : positive) { struct k } : (forall n:nat, le k n -> Qlt (Qabs (qn n)) (Z.pos A # 1)) -> { B : positive | forall n:nat, Qlt (Qabs (qn n)) (Z.pos B # 1) }. Proof. @@ -1492,8 +1465,7 @@ Proof. Qed. Lemma CReal_mult_plus_distr_l : forall r1 r2 r3 : CReal, - CRealEq (CReal_mult r1 (CReal_plus r2 r3)) - (CReal_plus (CReal_mult r1 r2) (CReal_mult r1 r3)). + r1 * (r2 + r3) == (r1 * r2) + (r1 * r3). Proof. intros x y z. apply CRealEq_diff. apply CRealEq_modindep. apply (QSeqEquivEx_trans _ (fun n => proj1_sig x n @@ -1613,6 +1585,15 @@ Proof. + rewrite Qinv_plus_distr. unfold Qeq. reflexivity. Qed. +Lemma CReal_mult_plus_distr_r : forall r1 r2 r3 : CReal, + (r2 + r3) * r1 == (r2 * r1) + (r3 * r1). +Proof. + intros. + rewrite CReal_mult_comm, CReal_mult_plus_distr_l, + <- (CReal_mult_comm r1), <- (CReal_mult_comm r1). + reflexivity. +Qed. + Lemma CReal_mult_1_l : forall r: CReal, 1 * r == r. Proof. intros [rn limr]. split. @@ -1708,12 +1689,41 @@ Qed. Add Ring CRealRing : CReal_isRing. +Lemma CReal_opp_0 : -0 == 0. +Proof. + ring. +Qed. + +Lemma CReal_opp_plus_distr : forall r1 r2, - (r1 + r2) == - r1 + - r2. +Proof. + intros; ring. +Qed. + +Lemma CReal_opp_involutive : forall x:CReal, --x == x. +Proof. + intro x. ring. +Qed. + +Lemma CReal_opp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2. +Proof. + unfold CRealGt; intros. + apply (CReal_plus_lt_reg_l (r2 + r1)). + setoid_replace (r2 + r1 + - r1) with r2 by ring. + setoid_replace (r2 + r1 + - r2) with r1 by ring. + exact H. +Qed. + (**********) Lemma CReal_mult_0_l : forall r, 0 * r == 0. Proof. intro; ring. Qed. +Lemma CReal_mult_0_r : forall r, r * 0 == 0. +Proof. + intro; ring. +Qed. + (**********) Lemma CReal_mult_1_r : forall r, r * 1 == r. Proof. @@ -1728,9 +1738,7 @@ Proof. Qed. Lemma CReal_mult_lt_compat_l : forall x y z : CReal, - CRealLt (inject_Q 0) x - -> CRealLt y z - -> CRealLt (CReal_mult x y) (CReal_mult x z). + 0 < x -> y < z -> x*y < x*z. Proof. intros. apply (CReal_plus_lt_reg_l (CReal_opp (CReal_mult x y))). @@ -1744,6 +1752,13 @@ Proof. rewrite <- CReal_plus_assoc, H1, CReal_plus_0_l. exact H0. Qed. +Lemma CReal_mult_lt_compat_r : forall x y z : CReal, + 0 < x -> y < z -> y*x < z*x. +Proof. + intros. rewrite <- (CReal_mult_comm x), <- (CReal_mult_comm x). + apply (CReal_mult_lt_compat_l x); assumption. +Qed. + Lemma CReal_mult_eq_reg_l : forall (r r1 r2 : CReal), r # 0 -> CRealEq (CReal_mult r r1) (CReal_mult r r2) @@ -1891,6 +1906,12 @@ Proof. intro p. rewrite <- INR_IPR. apply (lt_INR 0), Pos2Nat.is_pos. Qed. +Lemma IPR_double : forall p:positive, IPR (2*p) == 2 * IPR p. +Proof. + intro p. destruct p; try reflexivity. + rewrite CReal_mult_1_r. reflexivity. +Qed. + (**********) Lemma INR_IZR_INZ : forall n:nat, INR n == IZR (Z.of_nat n). Proof. @@ -1939,6 +1960,77 @@ Proof. ring. Qed. +Lemma mult_IPR : forall n m:positive, IPR (n * m) == IPR n * IPR m. +Proof. + intros. repeat rewrite <- INR_IPR. + rewrite Pos2Nat.inj_mul. apply mult_INR. +Qed. + +Lemma mult_IZR : forall n m:Z, IZR (n * m) == IZR n * IZR m. +Proof. + intros n m. destruct n. + - rewrite CReal_mult_0_l. rewrite Z.mul_0_l. reflexivity. + - destruct m. rewrite Z.mul_0_r, CReal_mult_0_r. reflexivity. + simpl; unfold IZR. apply mult_IPR. + simpl. unfold IZR. rewrite mult_IPR. ring. + - destruct m. rewrite Z.mul_0_r, CReal_mult_0_r. reflexivity. + simpl. unfold IZR. rewrite mult_IPR. ring. + simpl. unfold IZR. rewrite mult_IPR. ring. +Qed. + +Lemma opp_IZR : forall n:Z, IZR (- n) == - IZR n. +Proof. + intros [|z|z]; unfold IZR. rewrite CReal_opp_0. reflexivity. + reflexivity. rewrite CReal_opp_involutive. reflexivity. +Qed. + +Lemma minus_IZR : forall n m:Z, IZR (n - m) == IZR n - IZR m. +Proof. + intros; unfold Z.sub, CReal_minus. + rewrite <- opp_IZR. + apply plus_IZR. +Qed. + +Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m. +Proof. + assert (forall n:Z, Z.lt 0 n -> 0 < IZR n) as posCase. + { intros. destruct (IZN n). apply Z.lt_le_incl. apply H. + subst n. rewrite <- INR_IZR_INZ. apply (lt_INR 0). + apply Nat2Z.inj_lt. apply H. } + intros. apply (CReal_plus_lt_reg_r (-(IZR n))). + pose proof minus_IZR. unfold CReal_minus in H0. + repeat rewrite <- H0. unfold Zminus. + rewrite Z.add_opp_diag_r. apply posCase. + rewrite (Z.add_lt_mono_l _ _ n). ring_simplify. apply H. +Qed. + +Lemma Z_R_minus : forall n m:Z, IZR n - IZR m == IZR (n - m). +Proof. + intros z1 z2; unfold CReal_minus; unfold Z.sub. + rewrite plus_IZR, opp_IZR. reflexivity. +Qed. + +Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z. +Proof. + intro z; case z; simpl; intros. + elim (CRealLt_irrefl _ H). + easy. exfalso. + apply (CRealLt_asym 0 (IZR (Z.neg p))). exact H. + apply (IZR_lt (Z.neg p) 0). reflexivity. +Qed. + +Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z. +Proof. + intros z1 z2 H; apply Z.lt_0_sub. + apply lt_0_IZR. + rewrite <- Z_R_minus. apply (CReal_plus_lt_reg_l (IZR z1)). + ring_simplify. exact H. +Qed. + +Lemma IZR_le : forall n m:Z, (n <= m)%Z -> IZR n <= IZR m. +Proof. + intros m n H. intro abs. apply (lt_IZR n m) in abs. omega. +Qed. Lemma CReal_iterate_one : forall (n : nat), IZR (Z.of_nat n) == inject_Q (Z.of_nat n # 1). @@ -2478,6 +2570,72 @@ Proof. simpl in maj. rewrite abs in maj. inversion maj. Qed. +Lemma CReal_inv_r : forall (r:CReal) (rnz : r # 0), + r * ((/ r) rnz) == 1. +Proof. + intros. rewrite CReal_mult_comm, CReal_inv_l. + reflexivity. +Qed. + +Lemma CReal_inv_1 : forall nz : 1 # 0, (/ 1) nz == 1. +Proof. + intros. rewrite <- (CReal_mult_1_l ((/1) nz)). rewrite CReal_inv_r. + reflexivity. +Qed. + +Lemma CReal_inv_mult_distr : + forall r1 r2 (r1nz : r1 # 0) (r2nz : r2 # 0) (rmnz : (r1*r2) # 0), + (/ (r1 * r2)) rmnz == (/ r1) r1nz * (/ r2) r2nz. +Proof. + intros. apply (CReal_mult_eq_reg_l r1). exact r1nz. + rewrite <- CReal_mult_assoc. rewrite CReal_inv_r. rewrite CReal_mult_1_l. + apply (CReal_mult_eq_reg_l r2). exact r2nz. + rewrite CReal_inv_r. rewrite <- CReal_mult_assoc. + rewrite (CReal_mult_comm r2 r1). rewrite CReal_inv_r. + reflexivity. +Qed. + +Lemma Rinv_eq_compat : forall x y (rxnz : x # 0) (rynz : y # 0), + x == y + -> (/ x) rxnz == (/ y) rynz. +Proof. + intros. apply (CReal_mult_eq_reg_l x). exact rxnz. + rewrite CReal_inv_r, H, CReal_inv_r. reflexivity. +Qed. + +Lemma CReal_mult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2. +Proof. + intros z x y H H0. + apply (CReal_mult_lt_compat_l ((/z) (or_intror H))) in H0. + repeat rewrite <- CReal_mult_assoc in H0. rewrite CReal_inv_l in H0. + repeat rewrite CReal_mult_1_l in H0. apply H0. + apply CReal_inv_0_lt_compat. exact H. +Qed. + +Lemma CReal_mult_lt_reg_r : forall r r1 r2, 0 < r -> r1 * r < r2 * r -> r1 < r2. +Proof. + intros. + apply CReal_mult_lt_reg_l with r. + exact H. + now rewrite 2!(CReal_mult_comm r). +Qed. + +Lemma CReal_mult_eq_reg_r : forall r r1 r2, r1 * r == r2 * r -> r # 0 -> r1 == r2. +Proof. + intros. apply (CReal_mult_eq_reg_l r). exact H0. + now rewrite 2!(CReal_mult_comm r). +Qed. + +Lemma CReal_mult_eq_compat_l : forall r r1 r2, r1 == r2 -> r * r1 == r * r2. +Proof. + intros. rewrite H. reflexivity. +Qed. + +Lemma CReal_mult_eq_compat_r : forall r r1 r2, r1 == r2 -> r1 * r == r2 * r. +Proof. + intros. rewrite H. reflexivity. +Qed. + Fixpoint pow (r:CReal) (n:nat) : CReal := match n with | O => 1 @@ -2492,6 +2650,113 @@ Definition IQR (q:Q) : CReal := end. Arguments IQR q%Q : simpl never. +Lemma mult_IPR_IZR : forall (n:positive) (m:Z), IZR (Z.pos n * m) == IPR n * IZR m. +Proof. + intros. rewrite mult_IZR. apply CReal_mult_eq_compat_r. reflexivity. +Qed. + +Lemma plus_IQR : forall n m:Q, IQR (n + m) == IQR n + IQR m. +Proof. + intros. destruct n,m; unfold Qplus,IQR; simpl. + rewrite plus_IZR. repeat rewrite mult_IZR. + setoid_replace ((/ IPR (Qden * Qden0)) (or_intror (IPR_pos (Qden * Qden0)))) + with ((/ IPR Qden) (or_intror (IPR_pos Qden)) + * (/ IPR Qden0) (or_intror (IPR_pos Qden0))). + rewrite CReal_mult_plus_distr_r. + repeat rewrite CReal_mult_assoc. rewrite <- (CReal_mult_assoc (IZR (Z.pos Qden))). + rewrite CReal_inv_r, CReal_mult_1_l. + rewrite (CReal_mult_comm ((/IPR Qden) (or_intror (IPR_pos Qden)))). + rewrite <- (CReal_mult_assoc (IZR (Z.pos Qden0))). + rewrite CReal_inv_r, CReal_mult_1_l. reflexivity. unfold IZR. + rewrite <- (CReal_inv_mult_distr + _ _ _ _ (or_intror (CReal_mult_lt_0_compat _ _ (IPR_pos _) (IPR_pos _)))). + apply Rinv_eq_compat. apply mult_IPR. +Qed. + +Lemma IQR_pos : forall q:Q, Qlt 0 q -> 0 < IQR q. +Proof. + intros. destruct q; unfold IQR. + apply CReal_mult_lt_0_compat. apply (IZR_lt 0). + unfold Qlt in H; simpl in H. + rewrite Z.mul_1_r in H. apply H. + apply CReal_inv_0_lt_compat. apply IPR_pos. +Qed. + +Lemma opp_IQR : forall q:Q, IQR (- q) == - IQR q. +Proof. + intros [a b]; unfold IQR; simpl. + rewrite CReal_opp_mult_distr_l. + rewrite opp_IZR. reflexivity. +Qed. + +Lemma lt_IQR : forall n m:Q, IQR n < IQR m -> (n < m)%Q. +Proof. + intros. destruct n,m; unfold IQR in H. + unfold Qlt; simpl. apply (CReal_mult_lt_compat_r (IPR Qden)) in H. + rewrite CReal_mult_assoc in H. rewrite CReal_inv_l in H. + rewrite CReal_mult_1_r in H. rewrite (CReal_mult_comm (IZR Qnum0)) in H. + apply (CReal_mult_lt_compat_l (IPR Qden0)) in H. + do 2 rewrite <- CReal_mult_assoc in H. rewrite CReal_inv_r in H. + rewrite CReal_mult_1_l in H. + rewrite (CReal_mult_comm (IZR Qnum0)) in H. + do 2 rewrite <- mult_IPR_IZR in H. apply lt_IZR in H. + rewrite Z.mul_comm. rewrite (Z.mul_comm Qnum0). + apply H. apply IPR_pos. apply IPR_pos. +Qed. + +Lemma CReal_mult_le_compat_l_half : forall r r1 r2, + 0 < r -> r1 <= r2 -> r * r1 <= r * r2. +Proof. + intros. intro abs. apply (CReal_mult_lt_reg_l) in abs. + contradiction. apply H. +Qed. + +Lemma IQR_lt : forall n m:Q, Qlt n m -> IQR n < IQR m. +Proof. + intros. apply (CReal_plus_lt_reg_r (-IQR n)). + rewrite CReal_plus_opp_r. rewrite <- opp_IQR. rewrite <- plus_IQR. + apply IQR_pos. apply (Qplus_lt_l _ _ n). + ring_simplify. apply H. +Qed. + +Lemma IQR_nonneg : forall q:Q, Qle 0 q -> 0 <= (IQR q). +Proof. + intros [a b] H. unfold IQR;simpl. + apply (CRealLe_trans _ ((/ IPR b) (or_intror (IPR_pos b)) * 0)). + rewrite CReal_mult_0_r. apply CRealLe_refl. + rewrite (CReal_mult_comm (IZR a)). apply CReal_mult_le_compat_l_half. + apply CReal_inv_0_lt_compat. apply IPR_pos. + apply (IZR_le 0 a). unfold Qle in H; simpl in H. + rewrite Z.mul_1_r in H. apply H. +Qed. + +Lemma IQR_le : forall n m:Q, Qle n m -> IQR n <= IQR m. +Proof. + intros. intro abs. apply (CReal_plus_lt_compat_l (-IQR n)) in abs. + rewrite CReal_plus_opp_l, <- opp_IQR, <- plus_IQR in abs. + apply IQR_nonneg in abs. contradiction. apply (Qplus_le_l _ _ n). + ring_simplify. apply H. +Qed. + +Add Parametric Morphism : IQR + with signature Qeq ==> CRealEq + as IQR_morph. +Proof. + intros. destruct x,y; unfold IQR; simpl. + unfold Qeq in H; simpl in H. + apply (CReal_mult_eq_reg_r (IZR (Z.pos Qden))). + 2: right; apply IPR_pos. + rewrite CReal_mult_assoc. rewrite CReal_inv_l. rewrite CReal_mult_1_r. + rewrite (CReal_mult_comm (IZR Qnum0)). + apply (CReal_mult_eq_reg_l (IZR (Z.pos Qden0))). + right; apply IPR_pos. + rewrite <- CReal_mult_assoc, <- CReal_mult_assoc, CReal_inv_r. + rewrite CReal_mult_1_l. + repeat rewrite <- mult_IZR. + rewrite <- H. rewrite Zmult_comm. reflexivity. +Qed. + + Lemma CReal_invQ : forall (b : positive) (pos : Qlt 0 (Z.pos b # 1)), CRealEq (CReal_inv (inject_Q (Z.pos b # 1)) (or_intror (CReal_injectQPos (Z.pos b # 1) pos))) (inject_Q (1 # b)). @@ -2530,6 +2795,7 @@ Proof. discriminate. Qed. + Close Scope R_scope_constr. Close Scope Q. diff --git a/theories/Reals/ConstructiveRIneq.v b/theories/Reals/ConstructiveRIneq.v index adffa9b719..e497b7d9bb 100644 --- a/theories/Reals/ConstructiveRIneq.v +++ b/theories/Reals/ConstructiveRIneq.v @@ -25,6 +25,8 @@ Local Open Scope R_scope_constr. (* Export all axioms *) +Notation R := CReal (only parsing). +Notation Req := CRealEq (only parsing). Notation Rplus_comm := CReal_plus_comm (only parsing). Notation Rplus_assoc := CReal_plus_assoc (only parsing). Notation Rplus_opp_r := CReal_plus_opp_r (only parsing). @@ -40,12 +42,39 @@ Notation Rlt_trans := CRealLt_trans (only parsing). Notation Rplus_lt_compat_l := CReal_plus_lt_compat_l (only parsing). Notation Rmult_lt_compat_l := CReal_mult_lt_compat_l (only parsing). Notation Rmult_0_l := CReal_mult_0_l (only parsing). +Notation INR := INR (only parsing). +Notation IZR := IZR (only parsing). +Notation IQR := IQR (only parsing). Hint Resolve Rplus_comm Rplus_assoc Rplus_opp_r Rplus_0_l Rmult_comm Rmult_assoc Rinv_l Rmult_1_l Rmult_plus_distr_l Rlt_0_1 Rlt_asym Rlt_trans Rplus_lt_compat_l Rmult_lt_compat_l Rmult_0_l : creal. +Infix "==" := CRealEq : R_scope_constr. +Infix "#" := CReal_appart : R_scope_constr. +Infix "<" := CRealLt : R_scope_constr. +Infix ">" := CRealGt : R_scope_constr. +Infix "<=" := CRealLe : R_scope_constr. +Infix ">=" := CRealGe : R_scope_constr. + +Notation "x <= y <= z" := (x <= y /\ y <= z) : R_scope_constr. +Notation "x <= y < z" := (x <= y /\ y < z) : R_scope_constr. +Notation "x < y < z" := (x < y /\ y < z) : R_scope_constr. +Notation "x < y <= z" := (x < y /\ y <= z) : R_scope_constr. + +Infix "+" := CReal_plus : R_scope_constr. +Notation "- x" := (CReal_opp x) : R_scope_constr. +Infix "-" := CReal_minus : R_scope_constr. +Infix "*" := CReal_mult : R_scope_constr. +Notation "/ x" := (CReal_inv x) (at level 35, right associativity) : R_scope_constr. + +Notation "0" := (inject_Q 0) : R_scope_constr. +Notation "1" := (inject_Q 1) : R_scope_constr. +Notation "2" := (IZR 2) : R_scope_constr. + +Add Ring CRealRing : CReal_isRing. + (*********************************************************) (** ** Relation between orders and equality *) @@ -1928,167 +1957,6 @@ Proof. right. apply IPR_pos. Qed. -Definition Rup_nat (x : CReal) - : { n : nat | x < INR n }. -Proof. - intros. destruct (Rarchimedean x) as [p [maj _]]. - destruct p. - - exists O. apply maj. - - exists (Pos.to_nat p). rewrite INR_IPR. apply maj. - - exists O. apply (CRealLt_trans _ (IZR (Z.neg p)) _ maj). - apply (IZR_lt _ 0). reflexivity. -Qed. - -(* Sharpen the archimedean property : constructive versions of - the usual floor and ceiling functions. - - n is a temporary parameter used for the recursion, - look at Ffloor below. *) -Fixpoint Rfloor_pos (a : CReal) (n : nat) { struct n } - : 0 < a - -> a < INR n - -> { p : nat | INR p < a < INR p + 2 }. -Proof. - (* Decreasing loop on n, until it is the first integer above a. *) - intros H H0. destruct n. - - exfalso. apply (CRealLt_asym 0 a); assumption. - - destruct n as [|p] eqn:des. - + (* n = 1 *) exists O. split. - apply H. rewrite Rplus_0_l. apply (CRealLt_trans a (1+0)). - rewrite Rplus_0_r. apply H0. apply Rplus_le_lt_compat. - apply Rle_refl. apply Rlt_0_1. - + (* n > 1 *) - destruct (linear_order_T (INR p) a (INR (S p))). - * rewrite <- Rplus_0_r, S_INR. apply Rplus_lt_compat_l. - apply Rlt_0_1. - * exists p. split. exact c. - rewrite S_INR, S_INR, Rplus_assoc in H0. exact H0. - * apply (Rfloor_pos a n H). rewrite des. apply c. -Qed. - -Definition Rfloor (a : CReal) - : { p : Z | IZR p < a < IZR p + 2 }. -Proof. - assert (forall x:CReal, 0 < x -> { n : nat | x < INR n }). - { intros. pose proof (Rarchimedean x) as [n [maj _]]. - destruct n. - + exfalso. apply (CRealLt_asym 0 x); assumption. - + exists (Pos.to_nat p). rewrite INR_IPR. apply maj. - + exfalso. apply (CRealLt_asym 0 x). apply H. - apply (CRealLt_trans x (IZR (Z.neg p))). apply maj. - apply (Rplus_lt_reg_r (-IZR (Z.neg p))). - rewrite Rplus_opp_r. rewrite <- opp_IZR. - rewrite Rplus_0_l. apply (IZR_lt 0). reflexivity. } - destruct (linear_order_T 0 a 1 Rlt_0_1). - - destruct (H a c). destruct (Rfloor_pos a x c c0). - exists (Z.of_nat x0). rewrite <- INR_IZR_INZ. apply a0. - - apply (Rplus_lt_compat_r (-a)) in c. - rewrite Rplus_opp_r in c. destruct (H (1-a) c). - destruct (Rfloor_pos (1-a) x c c0). - exists (-(Z.of_nat x0 + 1))%Z. rewrite opp_IZR. - rewrite plus_IZR. simpl. split. - + rewrite <- (Ropp_involutive a). apply Ropp_gt_lt_contravar. - destruct a0 as [_ a0]. apply (Rplus_lt_reg_r 1). - rewrite Rplus_comm, Rplus_assoc. rewrite <- INR_IZR_INZ. apply a0. - + destruct a0 as [a0 _]. apply (Rplus_lt_compat_l a) in a0. - ring_simplify in a0. rewrite <- INR_IZR_INZ. - apply (Rplus_lt_reg_r (INR x0)). unfold IZR, IPR, IPR_2. - ring_simplify. exact a0. -Qed. - -Lemma Qplus_same_denom : forall a b c, ((a # c) + (b # c) == (a+b) # c)%Q. -Proof. - intros. unfold Qeq. simpl. rewrite Pos2Z.inj_mul. ring. -Qed. - -(* A point in an archimedean field is the limit of a - sequence of rational numbers (n maps to the q between - a and a+1/n). This will yield a maximum - archimedean field, which is the field of real numbers. *) -Definition FQ_dense_pos (a b : CReal) - : 0 < b - -> a < b -> { q : Q | a < IQR q < b }. -Proof. - intros H H0. - assert (0 < b - a) as epsPos. - { apply (Rplus_lt_compat_r (-a)) in H0. - rewrite Rplus_opp_r in H0. apply H0. } - pose proof (Rarchimedean ((/(b-a)) (or_intror epsPos))) - as [n [maj _]]. - destruct n as [|n|n]. - - exfalso. - apply (Rmult_lt_compat_l (b-a)) in maj. 2: apply epsPos. - rewrite Rmult_0_r in maj. rewrite Rinv_r in maj. - apply (CRealLt_asym 0 1). apply Rlt_0_1. apply maj. - right. exact epsPos. - - (* 0 < n *) - destruct (Rfloor (IZR (2 * Z.pos n) * b)) as [p maj2]. - exists (p # (2*n))%Q. split. - + apply (CRealLt_trans a (b - IQR (1 # n))). - apply (Rplus_lt_reg_r (IQR (1#n))). - unfold CReal_minus. rewrite Rplus_assoc. rewrite Rplus_opp_l. - rewrite Rplus_0_r. apply (Rplus_lt_reg_l (-a)). - rewrite <- Rplus_assoc. rewrite Rplus_opp_l. rewrite Rplus_0_l. - rewrite Rplus_comm. unfold IQR. - rewrite Rmult_1_l. apply (Rmult_lt_reg_l (IZR (Z.pos n))). - apply (IZR_lt 0). reflexivity. rewrite Rinv_r. - apply (Rmult_lt_compat_r (b-a)) in maj. rewrite Rinv_l in maj. - apply maj. exact epsPos. - right. apply IPR_pos. - apply (Rplus_lt_reg_r (IQR (1 # n))). - unfold CReal_minus. rewrite Rplus_assoc. rewrite Rplus_opp_l. - rewrite Rplus_0_r. rewrite <- plus_IQR. - destruct maj2 as [_ maj2]. - setoid_replace ((p # 2 * n) + (1 # n))%Q - with ((p + 2 # 2 * n))%Q. unfold IQR. - apply (Rmult_lt_reg_r (IZR (Z.pos (2 * n)))). - apply (IZR_lt 0). reflexivity. rewrite Rmult_assoc. - rewrite Rinv_l. rewrite Rmult_1_r. rewrite Rmult_comm. - rewrite plus_IZR. apply maj2. - setoid_replace (1#n)%Q with (2#2*n)%Q. 2: reflexivity. - apply Qplus_same_denom. - + destruct maj2 as [maj2 _]. unfold IQR. - apply (Rmult_lt_reg_r (IZR (Z.pos (2 * n)))). - apply (IZR_lt 0). apply Pos2Z.is_pos. rewrite Rmult_assoc. rewrite Rinv_l. - rewrite Rmult_1_r. rewrite Rmult_comm. apply maj2. - - exfalso. - apply (Rmult_lt_compat_l (b-a)) in maj. 2: apply epsPos. - rewrite Rinv_r in maj. apply (CRealLt_asym 0 1). apply Rlt_0_1. - apply (CRealLt_trans 1 ((b - a) * IZR (Z.neg n)) _ maj). - rewrite <- (Rmult_0_r (b-a)). - apply Rmult_lt_compat_l. apply epsPos. apply (IZR_lt _ 0). reflexivity. - right. apply epsPos. -Qed. - -Definition FQ_dense (a b : CReal) - : a < b - -> { q : Q | a < IQR q < b }. -Proof. - intros H. destruct (linear_order_T a 0 b). apply H. - - destruct (FQ_dense_pos (-b) (-a)) as [q maj]. - apply (Rplus_lt_compat_l (-a)) in c. rewrite Rplus_opp_l in c. - rewrite Rplus_0_r in c. apply c. - apply (Rplus_lt_compat_r (-a)) in H. - rewrite Rplus_opp_r in H. - apply (Rplus_lt_compat_l (-b)) in H. rewrite <- Rplus_assoc in H. - rewrite Rplus_opp_l in H. rewrite Rplus_0_l in H. - rewrite Rplus_0_r in H. apply H. - exists (-q)%Q. split. - + destruct maj as [_ maj]. - apply (Rplus_lt_compat_r (-IQR q)) in maj. - rewrite Rplus_opp_r in maj. rewrite <- opp_IQR in maj. - apply (Rplus_lt_compat_l a) in maj. rewrite <- Rplus_assoc in maj. - rewrite Rplus_opp_r in maj. rewrite Rplus_0_l in maj. - rewrite Rplus_0_r in maj. apply maj. - + destruct maj as [maj _]. - apply (Rplus_lt_compat_r (-IQR q)) in maj. - rewrite Rplus_opp_r in maj. rewrite <- opp_IQR in maj. - apply (Rplus_lt_compat_l b) in maj. rewrite <- Rplus_assoc in maj. - rewrite Rplus_opp_r in maj. rewrite Rplus_0_l in maj. - rewrite Rplus_0_r in maj. apply maj. - - apply FQ_dense_pos. apply c. apply H. -Qed. - (*********) Lemma Rmult_le_pos : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2. diff --git a/theories/Reals/ConstructiveRcomplete.v b/theories/Reals/ConstructiveRcomplete.v index 9fb98a528b..06deff1bc1 100644 --- a/theories/Reals/ConstructiveRcomplete.v +++ b/theories/Reals/ConstructiveRcomplete.v @@ -12,13 +12,13 @@ Require Import QArith_base. Require Import Qabs. Require Import ConstructiveCauchyReals. -Require Import ConstructiveRIneq. +Require Import Logic.ConstructiveEpsilon. Local Open Scope R_scope_constr. Lemma CReal_absSmall : forall x y : CReal, (exists n : positive, Qlt (2 # n) - (proj1_sig x (Pos.to_nat n) - Qabs (proj1_sig y (Pos.to_nat n)))) + (proj1_sig x (Pos.to_nat n) - Qabs (proj1_sig y (Pos.to_nat n)))) -> (CRealLt (CReal_opp x) y /\ CRealLt y x). Proof. intros. destruct H as [n maj]. split. @@ -35,120 +35,181 @@ Proof. apply maj. apply Qplus_le_r. apply Qopp_le_compat. apply Qle_Qabs. Qed. +Definition absSmall (a b : CReal) : Prop + := -b < a < b. + Definition Un_cv_mod (un : nat -> CReal) (l : CReal) : Set := forall n : positive, - { p : nat | forall i:nat, le p i - -> -IQR (1#n) < un i - l < IQR (1#n) }. + { p : nat | forall i:nat, le p i -> absSmall (un i - l) (IQR (1#n)) }. Lemma Un_cv_mod_eq : forall (v u : nat -> CReal) (s : CReal), (forall n:nat, u n == v n) -> Un_cv_mod u s -> Un_cv_mod v s. Proof. intros v u s seq H1 p. specialize (H1 p) as [N H0]. - exists N. intros. rewrite <- seq. apply H0. apply H. + exists N. intros. unfold absSmall. rewrite <- seq. apply H0. apply H. Qed. -Lemma IQR_double_inv : forall n : positive, - IQR (1 # 2*n) + IQR (1 # 2*n) == IQR (1 # n). +Definition Un_cauchy_mod (un : nat -> CReal) : Set + := forall n : positive, + { p : nat | forall i j:nat, le p i + -> le p j + -> -IQR (1#n) < un i - un j < IQR (1#n) }. + + +(* Sharpen the archimedean property : constructive versions of + the usual floor and ceiling functions. + + n is a temporary parameter used for the recursion, + look at Ffloor below. *) +Fixpoint Rfloor_pos (a : CReal) (n : nat) { struct n } + : 0 < a + -> a < INR n + -> { p : nat | INR p < a < INR p + 2 }. Proof. - intros. apply (Rmult_eq_reg_l (IPR (2*n))). - unfold IQR. do 2 rewrite Rmult_1_l. - rewrite Rmult_plus_distr_l, Rinv_r, IPR_double, Rmult_assoc, Rinv_r. - rewrite (Rmult_plus_distr_r 1 1). ring. - right. apply IPR_pos. - right. apply IPR_pos. - right. apply IPR_pos. + (* Decreasing loop on n, until it is the first integer above a. *) + intros H H0. destruct n. + - exfalso. apply (CRealLt_asym 0 a); assumption. + - destruct n as [|p] eqn:des. + + (* n = 1 *) exists O. split. + apply H. rewrite CReal_plus_0_l. apply (CRealLt_trans a (1+0)). + rewrite CReal_plus_comm, CReal_plus_0_l. apply H0. + apply CReal_plus_le_lt_compat. + apply CRealLe_refl. apply CRealLt_0_1. + + (* n > 1 *) + destruct (linear_order_T (INR p) a (INR (S p))). + * rewrite <- CReal_plus_0_l, S_INR, CReal_plus_comm. apply CReal_plus_lt_compat_l. + apply CRealLt_0_1. + * exists p. split. exact c. + rewrite S_INR, S_INR, CReal_plus_assoc in H0. exact H0. + * apply (Rfloor_pos a n H). rewrite des. apply c. Qed. -Lemma CV_mod_plus : - forall (An Bn:nat -> CReal) (l1 l2:CReal), - Un_cv_mod An l1 -> Un_cv_mod Bn l2 - -> Un_cv_mod (fun i:nat => An i + Bn i) (l1 + l2). +Definition Rfloor (a : CReal) + : { p : Z | IZR p < a < IZR p + 2 }. Proof. - assert (forall x:CReal, x + x == 2*x) as double. - { intro. rewrite (Rmult_plus_distr_r 1 1), Rmult_1_l. reflexivity. } - intros. intros n. - destruct (H (2*n)%positive). - destruct (H0 (2*n)%positive). - exists (Nat.max x x0). intros. - setoid_replace (An i + Bn i - (l1 + l2)) - with (An i - l1 + (Bn i - l2)). 2: ring. - rewrite <- IQR_double_inv. split. - - rewrite Ropp_plus_distr. - apply Rplus_lt_compat. apply a. apply (le_trans _ (max x x0)). - apply Nat.le_max_l. apply H1. - apply a0. apply (le_trans _ (max x x0)). - apply Nat.le_max_r. apply H1. - - apply Rplus_lt_compat. apply a. apply (le_trans _ (max x x0)). - apply Nat.le_max_l. apply H1. - apply a0. apply (le_trans _ (max x x0)). - apply Nat.le_max_r. apply H1. + assert (forall x:CReal, 0 < x -> { n : nat | x < INR n }). + { intros. pose proof (Rarchimedean x) as [n [maj _]]. + destruct n. + + exfalso. apply (CRealLt_asym 0 x); assumption. + + exists (Pos.to_nat p). rewrite INR_IPR. apply maj. + + exfalso. apply (CRealLt_asym 0 x). apply H. + apply (CRealLt_trans x (IZR (Z.neg p))). apply maj. + apply (CReal_plus_lt_reg_l (-IZR (Z.neg p))). + rewrite CReal_plus_comm, CReal_plus_opp_r. rewrite <- opp_IZR. + rewrite CReal_plus_comm, CReal_plus_0_l. + apply (IZR_lt 0). reflexivity. } + destruct (linear_order_T 0 a 1 CRealLt_0_1). + - destruct (H a c). destruct (Rfloor_pos a x c c0). + exists (Z.of_nat x0). rewrite <- INR_IZR_INZ. apply a0. + - apply (CReal_plus_lt_compat_l (-a)) in c. + rewrite CReal_plus_comm, CReal_plus_opp_r, CReal_plus_comm in c. + destruct (H (1-a) c). + destruct (Rfloor_pos (1-a) x c c0). + exists (-(Z.of_nat x0 + 1))%Z. rewrite opp_IZR. + rewrite plus_IZR. simpl. split. + + rewrite <- (CReal_opp_involutive a). apply CReal_opp_gt_lt_contravar. + destruct a0 as [_ a0]. apply (CReal_plus_lt_reg_r 1). + rewrite CReal_plus_comm, CReal_plus_assoc. rewrite <- INR_IZR_INZ. apply a0. + + destruct a0 as [a0 _]. apply (CReal_plus_lt_compat_l a) in a0. + ring_simplify in a0. rewrite <- INR_IZR_INZ. + apply (CReal_plus_lt_reg_r (INR x0)). unfold IZR, IPR, IPR_2. + ring_simplify. exact a0. Qed. -Lemma Un_cv_mod_const : forall x : CReal, - Un_cv_mod (fun _ => x) x. +(* A point in an archimedean field is the limit of a + sequence of rational numbers (n maps to the q between + a and a+1/n). This will yield a maximum + archimedean field, which is the field of real numbers. *) +Definition FQ_dense_pos (a b : CReal) + : 0 < b + -> a < b -> { q : Q | a < IQR q < b }. Proof. - intros. intro p. exists O. intros. - unfold CReal_minus. rewrite Rplus_opp_r. - split. rewrite <- Ropp_0. - apply Ropp_gt_lt_contravar. unfold IQR. rewrite Rmult_1_l. - apply Rinv_0_lt_compat. unfold IQR. rewrite Rmult_1_l. - apply Rinv_0_lt_compat. + intros H H0. + assert (0 < b - a) as epsPos. + { apply (CReal_plus_lt_compat_l (-a)) in H0. + rewrite CReal_plus_opp_l, CReal_plus_comm in H0. + apply H0. } + pose proof (Rarchimedean ((/(b-a)) (or_intror epsPos))) + as [n [maj _]]. + destruct n as [|n|n]. + - exfalso. + apply (CReal_mult_lt_compat_l (b-a)) in maj. 2: apply epsPos. + rewrite CReal_mult_0_r in maj. rewrite CReal_inv_r in maj. + apply (CRealLt_asym 0 1). apply CRealLt_0_1. apply maj. + - (* 0 < n *) + destruct (Rfloor (IZR (2 * Z.pos n) * b)) as [p maj2]. + exists (p # (2*n))%Q. split. + + apply (CRealLt_trans a (b - IQR (1 # n))). + apply (CReal_plus_lt_reg_r (IQR (1#n))). + unfold CReal_minus. rewrite CReal_plus_assoc. rewrite CReal_plus_opp_l. + rewrite CReal_plus_0_r. apply (CReal_plus_lt_reg_l (-a)). + rewrite <- CReal_plus_assoc, CReal_plus_opp_l, CReal_plus_0_l. + rewrite CReal_plus_comm. unfold IQR. + rewrite CReal_mult_1_l. apply (CReal_mult_lt_reg_l (IZR (Z.pos n))). + apply (IZR_lt 0). reflexivity. rewrite CReal_inv_r. + apply (CReal_mult_lt_compat_l (b-a)) in maj. + rewrite CReal_inv_r, CReal_mult_comm in maj. + apply maj. exact epsPos. + apply (CReal_plus_lt_reg_r (IQR (1 # n))). + unfold CReal_minus. rewrite CReal_plus_assoc, CReal_plus_opp_l. + rewrite CReal_plus_0_r. rewrite <- plus_IQR. + destruct maj2 as [_ maj2]. + setoid_replace ((p # 2 * n) + (1 # n))%Q + with ((p + 2 # 2 * n))%Q. unfold IQR. + apply (CReal_mult_lt_reg_r (IZR (Z.pos (2 * n)))). + apply (IZR_lt 0). reflexivity. rewrite CReal_mult_assoc. + rewrite CReal_inv_l. rewrite CReal_mult_1_r. rewrite CReal_mult_comm. + rewrite plus_IZR. apply maj2. + setoid_replace (1#n)%Q with (2#2*n)%Q. 2: reflexivity. + apply Qinv_plus_distr. + + destruct maj2 as [maj2 _]. unfold IQR. + apply (CReal_mult_lt_reg_r (IZR (Z.pos (2 * n)))). + apply (IZR_lt 0). apply Pos2Z.is_pos. rewrite CReal_mult_assoc, CReal_inv_l. + rewrite CReal_mult_1_r, CReal_mult_comm. apply maj2. + - exfalso. + apply (CReal_mult_lt_compat_l (b-a)) in maj. 2: apply epsPos. + rewrite CReal_inv_r in maj. apply (CRealLt_asym 0 1). apply CRealLt_0_1. + apply (CRealLt_trans 1 ((b - a) * IZR (Z.neg n)) _ maj). + rewrite <- (CReal_mult_0_r (b-a)). + apply CReal_mult_lt_compat_l. apply epsPos. apply (IZR_lt _ 0). reflexivity. Qed. -(** Unicity of limit for convergent sequences *) -Lemma UL_sequence_mod : - forall (Un:nat -> CReal) (l1 l2:CReal), - Un_cv_mod Un l1 -> Un_cv_mod Un l2 -> l1 == l2. +Definition FQ_dense (a b : CReal) + : a < b + -> { q : Q | a < IQR q < b }. Proof. - assert (forall (Un:nat -> CReal) (l1 l2:CReal), - Un_cv_mod Un l1 -> Un_cv_mod Un l2 - -> l1 <= l2). - - intros Un l1 l2; unfold Un_cv_mod; intros. intro abs. - assert (0 < l1 - l2) as epsPos. - { apply Rgt_minus. apply abs. } - destruct (Rup_nat ((/(l1-l2)) (or_intror epsPos))) as [n nmaj]. - assert (lt 0 n) as nPos. - { apply (INR_lt 0). apply (Rlt_trans _ ((/ (l1 - l2)) (or_intror epsPos))). - 2: apply nmaj. apply Rinv_0_lt_compat. } - specialize (H (2*Pos.of_nat n)%positive) as [i imaj]. - specialize (H0 (2*Pos.of_nat n))%positive as [j jmaj]. - specialize (imaj (max i j) (Nat.le_max_l _ _)) as [imaj _]. - specialize (jmaj (max i j) (Nat.le_max_r _ _)) as [_ jmaj]. - apply Ropp_gt_lt_contravar in imaj. rewrite Ropp_involutive in imaj. - unfold CReal_minus in imaj. rewrite Ropp_plus_distr in imaj. - rewrite Ropp_involutive in imaj. rewrite Rplus_comm in imaj. - apply (Rplus_lt_compat _ _ _ _ imaj) in jmaj. - clear imaj. - rewrite Rplus_assoc in jmaj. unfold CReal_minus in jmaj. - rewrite <- (Rplus_assoc (- Un (Init.Nat.max i j))) in jmaj. - rewrite Rplus_opp_l in jmaj. - rewrite <- double in jmaj. rewrite Rplus_0_l in jmaj. - rewrite (Rmult_plus_distr_r 1 1), Rmult_1_l, IQR_double_inv in jmaj. - unfold IQR in jmaj. rewrite Rmult_1_l in jmaj. - apply (Rmult_lt_compat_l (IPR (Pos.of_nat n))) in jmaj. - rewrite Rinv_r, <- INR_IPR, Nat2Pos.id in jmaj. - apply (Rmult_lt_compat_l (l1-l2)) in nmaj. - rewrite Rinv_r in nmaj. rewrite Rmult_comm in jmaj. - apply (CRealLt_asym 1 ((l1-l2)*INR n)); assumption. - right. apply epsPos. apply epsPos. - intro abss. subst n. inversion nPos. - right. apply IPR_pos. apply IPR_pos. - - intros. split; apply (H Un); assumption. + intros H. destruct (linear_order_T a 0 b). apply H. + - destruct (FQ_dense_pos (-b) (-a)) as [q maj]. + apply (CReal_plus_lt_compat_l (-a)) in c. rewrite CReal_plus_opp_l in c. + rewrite CReal_plus_0_r in c. apply c. + apply (CReal_plus_lt_compat_l (-a)) in H. + rewrite CReal_plus_opp_l, CReal_plus_comm in H. + apply (CReal_plus_lt_compat_l (-b)) in H. rewrite <- CReal_plus_assoc in H. + rewrite CReal_plus_opp_l in H. rewrite CReal_plus_0_l in H. + rewrite CReal_plus_0_r in H. apply H. + exists (-q)%Q. split. + + destruct maj as [_ maj]. + apply (CReal_plus_lt_compat_l (-IQR q)) in maj. + rewrite CReal_plus_opp_l, <- opp_IQR, CReal_plus_comm in maj. + apply (CReal_plus_lt_compat_l a) in maj. rewrite <- CReal_plus_assoc in maj. + rewrite CReal_plus_opp_r, CReal_plus_0_l in maj. + rewrite CReal_plus_0_r in maj. apply maj. + + destruct maj as [maj _]. + apply (CReal_plus_lt_compat_l (-IQR q)) in maj. + rewrite CReal_plus_opp_l, <- opp_IQR, CReal_plus_comm in maj. + apply (CReal_plus_lt_compat_l b) in maj. rewrite <- CReal_plus_assoc in maj. + rewrite CReal_plus_opp_r in maj. rewrite CReal_plus_0_l in maj. + rewrite CReal_plus_0_r in maj. apply maj. + - apply FQ_dense_pos. apply c. apply H. Qed. -Definition Un_cauchy_mod (un : nat -> CReal) : Set - := forall n : positive, - { p : nat | forall i j:nat, le p i - -> le p j - -> -IQR (1#n) < un i - un j < IQR (1#n) }. - Definition RQ_limit : forall (x : CReal) (n:nat), { q:Q | x < IQR q < x + IQR (1 # Pos.of_nat n) }. Proof. intros x n. apply (FQ_dense x (x + IQR (1 # Pos.of_nat n))). - rewrite <- (Rplus_0_r x). rewrite Rplus_assoc. - apply Rplus_lt_compat_l. rewrite Rplus_0_l. apply IQR_pos. + rewrite <- (CReal_plus_0_r x). rewrite CReal_plus_assoc. + apply CReal_plus_lt_compat_l. rewrite CReal_plus_0_l. apply IQR_pos. reflexivity. Qed. @@ -171,23 +232,24 @@ Proof. apply Nat.le_max_l. apply H0. split. - apply lt_IQR. unfold Qminus. - apply (Rlt_trans _ (xn p0 - (xn q + IQR (1 # 2 * p)))). - + unfold CReal_minus. rewrite Ropp_plus_distr. unfold CReal_minus. - rewrite <- Rplus_assoc. - apply (Rplus_lt_reg_r (IQR (1 # 2 * p))). - rewrite Rplus_assoc. rewrite Rplus_opp_l. rewrite Rplus_0_r. + apply (CRealLt_trans _ (xn p0 - (xn q + IQR (1 # 2 * p)))). + + unfold CReal_minus. rewrite CReal_opp_plus_distr. unfold CReal_minus. + rewrite <- CReal_plus_assoc. + apply (CReal_plus_lt_reg_r (IQR (1 # 2 * p))). + rewrite CReal_plus_assoc. rewrite CReal_plus_opp_l. rewrite CReal_plus_0_r. rewrite <- plus_IQR. setoid_replace (- (1 # p) + (1 # 2 * p))%Q with (- (1 # 2 * p))%Q. rewrite opp_IQR. exact H1. rewrite Qplus_comm. setoid_replace (1#p)%Q with (2 # 2 *p)%Q. rewrite Qinv_minus_distr. reflexivity. reflexivity. - + rewrite plus_IQR. apply Rplus_lt_compat. + + rewrite plus_IQR. apply CReal_plus_le_lt_compat. + apply CRealLt_asym. destruct (RQ_limit (xn p0) p0); simpl. apply a. destruct (RQ_limit (xn q) q); unfold proj1_sig. - rewrite opp_IQR. apply Ropp_gt_lt_contravar. - apply (Rlt_le_trans _ (xn q + IQR (1 # Pos.of_nat q))). - apply a. apply Rplus_le_compat_l. apply IQR_le. + rewrite opp_IQR. apply CReal_opp_gt_lt_contravar. + apply (CRealLt_Le_trans _ (xn q + IQR (1 # Pos.of_nat q))). + apply a. apply CReal_plus_le_compat_l. apply IQR_le. apply Z2Nat.inj_le. discriminate. discriminate. simpl. assert ((Pos.to_nat p~0 <= q)%nat). { apply (le_trans _ (Init.Nat.max k (2 * Pos.to_nat p))). @@ -198,11 +260,12 @@ Proof. inversion H3. pose proof (Pos2Nat.is_pos (p~0)). rewrite H5 in H4. inversion H4. - apply lt_IQR. unfold Qminus. - apply (Rlt_trans _ (xn p0 + IQR (1 # 2 * p) - xn q)). - + rewrite plus_IQR. apply Rplus_lt_compat. + apply (CRealLt_trans _ (xn p0 + IQR (1 # 2 * p) - xn q)). + + rewrite plus_IQR. apply CReal_plus_le_lt_compat. + apply CRealLt_asym. destruct (RQ_limit (xn p0) p0); unfold proj1_sig. - apply (Rlt_le_trans _ (xn p0 + IQR (1 # Pos.of_nat p0))). - apply a. apply Rplus_le_compat_l. apply IQR_le. + apply (CRealLt_Le_trans _ (xn p0 + IQR (1 # Pos.of_nat p0))). + apply a. apply CReal_plus_le_compat_l. apply IQR_le. apply Z2Nat.inj_le. discriminate. discriminate. simpl. assert ((Pos.to_nat p~0 <= p0)%nat). { apply (le_trans _ (Init.Nat.max k (2 * Pos.to_nat p))). @@ -212,12 +275,12 @@ Proof. rewrite Nat2Pos.id. apply H3. intro abs. subst p0. inversion H3. pose proof (Pos2Nat.is_pos (p~0)). rewrite H5 in H4. inversion H4. - rewrite opp_IQR. apply Ropp_gt_lt_contravar. + rewrite opp_IQR. apply CReal_opp_gt_lt_contravar. destruct (RQ_limit (xn q) q); simpl. apply a. - + unfold CReal_minus. rewrite (Rplus_comm (xn p0)). - rewrite Rplus_assoc. - apply (Rplus_lt_reg_l (- IQR (1 # 2 * p))). - rewrite <- Rplus_assoc. rewrite Rplus_opp_l. rewrite Rplus_0_l. + + unfold CReal_minus. rewrite (CReal_plus_comm (xn p0)). + rewrite CReal_plus_assoc. + apply (CReal_plus_lt_reg_l (- IQR (1 # 2 * p))). + rewrite <- CReal_plus_assoc. rewrite CReal_plus_opp_l. rewrite CReal_plus_0_l. rewrite <- opp_IQR. rewrite <- plus_IQR. setoid_replace (- (1 # 2 * p) + (1 # p))%Q with (1 # 2 * p)%Q. exact H2. rewrite Qplus_comm. @@ -233,7 +296,7 @@ Lemma CReal_cv_self : forall (qn : nat -> Q) (x : CReal) (cvmod : positive -> na Proof. intros qn x cvmod H p. specialize (H (2*p)%positive). exists (cvmod (2*p)%positive). - intros p0 H0. unfold CReal_minus. rewrite FinjectQ_CReal. + intros p0 H0. unfold absSmall, CReal_minus. rewrite FinjectQ_CReal. setoid_replace (IQR (qn p0)) with (inject_Q (qn p0)). 2: apply FinjectQ_CReal. apply CReal_absSmall. @@ -246,12 +309,15 @@ Proof. 2: destruct x; reflexivity. apply (Qle_lt_trans _ (1 # 2 * p)). unfold Qle; simpl. rewrite Pos2Z.inj_max. apply Z.le_max_l. - rewrite <- (Qplus_lt_r _ _ (-(1#p))). unfold Qminus. rewrite Qplus_assoc. - rewrite (Qplus_comm _ (1#p)). rewrite Qplus_opp_r. rewrite Qplus_0_l. - setoid_replace (- (1 # p) + (1 # 2 * p))%Q with (-(1 # 2 * p))%Q. - apply Qopp_lt_compat. apply H. apply H0. - - rewrite Pos2Nat.inj_max. + rewrite <- (Qplus_lt_r + _ _ (Qabs + (qn p0 - + proj1_sig x + (2 * Pos.to_nat (Pos.max (4 * p) (Pos.of_nat (cvmod (2 * p)%positive))))%nat) + -(1#2*p))). + ring_simplify. + setoid_replace (-1 * (1 # 2 * p) + (1 # p))%Q with (1 # 2 * p)%Q. + apply H. apply H0. rewrite Pos2Nat.inj_max. apply (le_trans _ (1 * Nat.max (Pos.to_nat (4 * p)) (Pos.to_nat (Pos.of_nat (cvmod (2 * p)%positive))))). destruct (cvmod (2*p)%positive). apply le_0_n. rewrite mult_1_l. rewrite Nat2Pos.id. 2: discriminate. apply Nat.le_max_r. @@ -267,7 +333,7 @@ Lemma Un_cv_extens : forall (xn yn : nat -> CReal) (l : CReal), -> Un_cv_mod yn l. Proof. intros. intro p. destruct (H p) as [n cv]. exists n. - intros. unfold CReal_minus. rewrite <- (H0 i). apply cv. apply H1. + intros. unfold absSmall, CReal_minus. rewrite <- (H0 i). apply cv. apply H1. Qed. (* Q is dense in Archimedean fields, so all real numbers @@ -284,8 +350,8 @@ Proof. - intros p n k H0 H1. destruct (H p); simpl in H0,H1. specialize (a n k H0 H1). apply Qabs_case. intros _. apply a. intros _. - rewrite <- (Qopp_involutive (1#p)). apply Qopp_lt_compat. - apply a. + apply (Qplus_lt_r _ _ (qn n -qn k-(1#p))). ring_simplify. + destruct a. ring_simplify in H2. exact H2. - exists (exist _ (fun n : nat => qn (increasing_modulus (fun p : positive => proj1_sig (H p)) n)) H0). apply (Un_cv_extens (fun n : nat => IQR (qn n))). @@ -309,19 +375,20 @@ Proof. apply Nat.le_max_l. apply H. destruct (RQ_limit (xn p0) p0) as [q maj]; unfold proj1_sig in H0,H1. split. - - apply (Rlt_trans _ (IQR q - IQR (1 # 2 * p) - l)). - + unfold CReal_minus. rewrite (Rplus_comm (IQR q)). - apply (Rplus_lt_reg_l (IQR (1 # 2 * p))). + - apply (CRealLt_trans _ (IQR q - IQR (1 # 2 * p) - l)). + + unfold CReal_minus. rewrite (CReal_plus_comm (IQR q)). + apply (CReal_plus_lt_reg_l (IQR (1 # 2 * p))). ring_simplify. unfold CReal_minus. rewrite <- opp_IQR. rewrite <- plus_IQR. setoid_replace ((1 # 2 * p) + - (1 # p))%Q with (-(1#2*p))%Q. rewrite opp_IQR. apply H0. setoid_replace (1#p)%Q with (2 # 2*p)%Q. rewrite Qinv_minus_distr. reflexivity. reflexivity. - + unfold CReal_minus. apply Rplus_lt_compat_r. - apply (Rplus_lt_reg_r (IQR (1 # 2 * p))). - ring_simplify. rewrite Rplus_comm. - apply (Rlt_le_trans _ (xn p0 + IQR (1 # Pos.of_nat p0))). - apply maj. apply Rplus_le_compat_l. + + unfold CReal_minus. + do 2 rewrite <- (CReal_plus_comm (-l)). apply CReal_plus_lt_compat_l. + apply (CReal_plus_lt_reg_r (IQR (1 # 2 * p))). + ring_simplify. rewrite CReal_plus_comm. + apply (CRealLt_Le_trans _ (xn p0 + IQR (1 # Pos.of_nat p0))). + apply maj. apply CReal_plus_le_compat_l. apply IQR_le. apply Z2Nat.inj_le. discriminate. discriminate. simpl. assert ((Pos.to_nat p~0 <= p0)%nat). @@ -332,12 +399,261 @@ Proof. rewrite Nat2Pos.id. apply H2. intro abs. subst p0. inversion H2. pose proof (Pos2Nat.is_pos (p~0)). rewrite H4 in H3. inversion H3. - - apply (Rlt_trans _ (IQR q - l)). - + apply Rplus_lt_compat_r. apply maj. - + apply (Rlt_trans _ (IQR (1 # 2 * p))). + - apply (CRealLt_trans _ (IQR q - l)). + + unfold CReal_minus. do 2 rewrite <- (CReal_plus_comm (-l)). + apply CReal_plus_lt_compat_l. apply maj. + + apply (CRealLt_trans _ (IQR (1 # 2 * p))). apply H1. apply IQR_lt. rewrite <- Qplus_0_r. setoid_replace (1#p)%Q with ((1#2*p)+(1#2*p))%Q. apply Qplus_lt_r. reflexivity. - rewrite Qplus_same_denom. reflexivity. + rewrite Qinv_plus_distr. reflexivity. +Qed. + +Definition sig_forall_dec_T : Type + := forall (P : nat -> Prop), (forall n, {P n} + {~P n}) + -> {n | ~P n} + {forall n, P n}. + +Definition sig_not_dec_T : Type := forall P : Prop, {not (not P)} + {not P}. + +Definition is_upper_bound (E:CReal -> Prop) (m:CReal) + := forall x:CReal, E x -> x <= m. + +Definition is_lub (E:CReal -> Prop) (m:CReal) := + is_upper_bound E m /\ (forall b:CReal, is_upper_bound E b -> m <= b). + +Lemma is_upper_bound_dec : + forall (E:CReal -> Prop) (x:CReal), + sig_forall_dec_T + -> sig_not_dec_T + -> { is_upper_bound E x } + { ~is_upper_bound E x }. +Proof. + intros. destruct (X0 (~exists y:CReal, E y /\ x < y)). + - left. intros y H. + destruct (CRealLt_lpo_dec x y X). 2: exact n0. + exfalso. apply n. intro abs. apply abs. + exists y. split. exact H. exact c. + - right. intro abs. apply n. intros [y [H H0]]. + specialize (abs y H). contradiction. +Qed. + +Definition Rup_nat (x : CReal) + : { n : nat | x < INR n }. +Proof. + intros. destruct (Rarchimedean x) as [p [maj _]]. + destruct p. + - exists O. apply maj. + - exists (Pos.to_nat p). rewrite INR_IPR. apply maj. + - exists O. apply (CRealLt_trans _ (IZR (Z.neg p)) _ maj). + apply (IZR_lt _ 0). reflexivity. +Qed. + +Lemma is_upper_bound_epsilon : + forall (E:CReal -> Prop), + sig_forall_dec_T + -> sig_not_dec_T + -> (exists x:CReal, is_upper_bound E x) + -> { n:nat | is_upper_bound E (INR n) }. +Proof. + intros. apply constructive_indefinite_ground_description_nat. + - intro n. apply is_upper_bound_dec. exact X. exact X0. + - destruct H as [x H]. destruct (Rup_nat x). exists x0. + intros y ey. specialize (H y ey). + apply CRealLt_asym. apply (CRealLe_Lt_trans _ x); assumption. +Qed. + +Lemma is_upper_bound_not_epsilon : + forall E:CReal -> Prop, + sig_forall_dec_T + -> sig_not_dec_T + -> (exists x : CReal, E x) + -> { m:nat | ~is_upper_bound E (-INR m) }. +Proof. + intros E lpo sig_not_dec H. + apply constructive_indefinite_ground_description_nat. + - intro n. destruct (is_upper_bound_dec E (-INR n) lpo sig_not_dec). + right. intro abs. contradiction. left. exact n0. + - destruct H as [x H]. destruct (Rup_nat (-x)) as [n H0]. + exists n. intro abs. specialize (abs x H). + apply abs. apply (CReal_plus_lt_reg_l (INR n-x)). + ring_simplify. exact H0. +Qed. + +(* Decidable Dedekind cuts are Cauchy reals. *) +Record DedekindDecCut : Type := + { + DDupcut : Q -> Prop; + DDproper : forall q r : Q, (q == r -> DDupcut q -> DDupcut r)%Q; + DDlow : Q; + DDhigh : Q; + DDdec : forall q:Q, { DDupcut q } + { ~DDupcut q }; + DDinterval : forall q r : Q, Qle q r -> DDupcut q -> DDupcut r; + DDhighProp : DDupcut DDhigh; + DDlowProp : ~DDupcut DDlow; + }. + +Lemma DDlow_below_up : forall (upcut : DedekindDecCut) (a b : Q), + DDupcut upcut a -> ~DDupcut upcut b -> Qlt b a. +Proof. + intros. destruct (Qlt_le_dec b a). exact q. + exfalso. apply H0. apply (DDinterval upcut a). + exact q. exact H. +Qed. + +Fixpoint DDcut_limit_fix (upcut : DedekindDecCut) (r : Q) (n : nat) : + Qlt 0 r + -> (DDupcut upcut (DDlow upcut + (Z.of_nat n#1) * r)) + -> { q : Q | DDupcut upcut q /\ ~DDupcut upcut (q - r) }. +Proof. + destruct n. + - intros. exfalso. simpl in H0. + apply (DDproper upcut _ (DDlow upcut)) in H0. 2: ring. + exact (DDlowProp upcut H0). + - intros. destruct (DDdec upcut (DDlow upcut + (Z.of_nat n # 1) * r)). + + exact (DDcut_limit_fix upcut r n H d). + + exists (DDlow upcut + (Z.of_nat (S n) # 1) * r)%Q. split. + exact H0. intro abs. + apply (DDproper upcut _ (DDlow upcut + (Z.of_nat n # 1) * r)) in abs. + contradiction. + rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite <- Qinv_plus_distr. + ring. +Qed. + +Lemma DDcut_limit : forall (upcut : DedekindDecCut) (r : Q), + Qlt 0 r + -> { q : Q | DDupcut upcut q /\ ~DDupcut upcut (q - r) }. +Proof. + intros. + destruct (Qarchimedean ((DDhigh upcut - DDlow upcut)/r)) as [n nmaj]. + apply (DDcut_limit_fix upcut r (Pos.to_nat n) H). + apply (Qmult_lt_r _ _ r) in nmaj. 2: exact H. + unfold Qdiv in nmaj. + rewrite <- Qmult_assoc, (Qmult_comm (/r)), Qmult_inv_r, Qmult_1_r in nmaj. + apply (DDinterval upcut (DDhigh upcut)). 2: exact (DDhighProp upcut). + apply Qlt_le_weak. apply (Qplus_lt_r _ _ (-DDlow upcut)). + rewrite Qplus_assoc, <- (Qplus_comm (DDlow upcut)), Qplus_opp_r, + Qplus_0_l, Qplus_comm. + rewrite positive_nat_Z. exact nmaj. + intros abs. rewrite abs in H. exact (Qlt_irrefl 0 H). +Qed. + +Lemma glb_dec_Q : forall upcut : DedekindDecCut, + { x : CReal | forall r:Q, (x < IQR r -> DDupcut upcut r) + /\ (IQR r < x -> ~DDupcut upcut r) }. +Proof. + intros. + assert (forall a b : Q, Qle a b -> Qle (-b) (-a)). + { intros. apply (Qplus_le_l _ _ (a+b)). ring_simplify. exact H. } + assert (QCauchySeq (fun n:nat => proj1_sig (DDcut_limit + upcut (1#Pos.of_nat n) (eq_refl _))) + Pos.to_nat). + { intros p i j pi pj. + destruct (DDcut_limit upcut (1 # Pos.of_nat i) eq_refl), + (DDcut_limit upcut (1 # Pos.of_nat j) eq_refl); unfold proj1_sig. + apply Qabs_case. intros. + apply (Qplus_lt_l _ _ (x0- (1#p))). ring_simplify. + setoid_replace (x + -1 * (1 # p))%Q with (x - (1 # p))%Q. + 2: ring. apply (Qle_lt_trans _ (x- (1#Pos.of_nat i))). + apply Qplus_le_r. apply H. + apply Z2Nat.inj_le. discriminate. discriminate. simpl. + rewrite Nat2Pos.id. exact pi. intro abs. + subst i. inversion pi. pose proof (Pos2Nat.is_pos p). + rewrite H2 in H1. inversion H1. + apply (DDlow_below_up upcut). apply a0. apply a. + intros. + apply (Qplus_lt_l _ _ (x- (1#p))). ring_simplify. + setoid_replace (x0 + -1 * (1 # p))%Q with (x0 - (1 # p))%Q. + 2: ring. apply (Qle_lt_trans _ (x0- (1#Pos.of_nat j))). + apply Qplus_le_r. apply H. + apply Z2Nat.inj_le. discriminate. discriminate. simpl. + rewrite Nat2Pos.id. exact pj. intro abs. + subst j. inversion pj. pose proof (Pos2Nat.is_pos p). + rewrite H2 in H1. inversion H1. + apply (DDlow_below_up upcut). apply a. apply a0. } + pose (exist (fun qn => QSeqEquiv qn qn Pos.to_nat) _ H0) as l. + exists l. split. + - intros. (* find an upper point between the limit and r *) + rewrite FinjectQ_CReal in H1. destruct H1 as [p pmaj]. + unfold l,proj1_sig in pmaj. + destruct (DDcut_limit upcut (1 # Pos.of_nat (Pos.to_nat p)) eq_refl) as [q qmaj] + ; simpl in pmaj. + apply (DDinterval upcut q). 2: apply qmaj. + apply (Qplus_lt_l _ _ q) in pmaj. ring_simplify in pmaj. + apply (Qle_trans _ ((2#p) + q)). + apply (Qplus_le_l _ _ (-q)). ring_simplify. discriminate. + apply Qlt_le_weak. exact pmaj. + - intros H1 abs. + rewrite FinjectQ_CReal in H1. destruct H1 as [p pmaj]. + unfold l,proj1_sig in pmaj. + destruct (DDcut_limit upcut (1 # Pos.of_nat (Pos.to_nat p)) eq_refl) as [q qmaj] + ; simpl in pmaj. + rewrite Pos2Nat.id in qmaj. + apply (Qplus_lt_r _ _ (r - (2#p))) in pmaj. ring_simplify in pmaj. + destruct qmaj. apply H2. + apply (DDinterval upcut r). 2: exact abs. + apply Qlt_le_weak, (Qlt_trans _ (-1*(2#p) + q) _ pmaj). + apply (Qplus_lt_l _ _ ((2#p) -q)). ring_simplify. + setoid_replace (-1 * (1 # p))%Q with (-(1#p))%Q. + 2: ring. rewrite Qinv_minus_distr. reflexivity. +Qed. + +Lemma is_upper_bound_glb : + forall (E:CReal -> Prop), + sig_not_dec_T + -> sig_forall_dec_T + -> (exists x : CReal, E x) + -> (exists x : CReal, is_upper_bound E x) + -> { x : CReal | forall r:Q, (x < IQR r -> is_upper_bound E (IQR r)) + /\ (IQR r < x -> ~is_upper_bound E (IQR r)) }. +Proof. + intros. + destruct (is_upper_bound_epsilon E X0 X H0) as [a luba]. + destruct (is_upper_bound_not_epsilon E X0 X H) as [b glbb]. + pose (fun q => is_upper_bound E (IQR q)) as upcut. + assert (forall q:Q, { upcut q } + { ~upcut q } ). + { intro q. apply is_upper_bound_dec. exact X0. exact X. } + assert (forall q r : Q, (q <= r)%Q -> upcut q -> upcut r). + { intros. intros x Ex. specialize (H3 x Ex). intro abs. + apply H3. apply (CRealLe_Lt_trans _ (IQR r)). 2: exact abs. + apply IQR_le. exact H2. } + assert (upcut (Z.of_nat a # 1)%Q). + { intros x Ex. unfold IQR. rewrite CReal_inv_1, CReal_mult_1_r. + specialize (luba x Ex). rewrite <- INR_IZR_INZ. exact luba. } + assert (~upcut (- Z.of_nat b # 1)%Q). + { intros abs. apply glbb. intros x Ex. + specialize (abs x Ex). unfold IQR in abs. + rewrite CReal_inv_1, CReal_mult_1_r, opp_IZR, <- INR_IZR_INZ in abs. + exact abs. } + assert (forall q r : Q, (q == r)%Q -> upcut q -> upcut r). + { intros. intros x Ex. specialize (H6 x Ex). rewrite <- H5. exact H6. } + destruct (glb_dec_Q (Build_DedekindDecCut + upcut H5 (-Z.of_nat b # 1)%Q (Z.of_nat a # 1) + H1 H2 H3 H4)). + simpl in a0. exists x. intro r. split. + - intros. apply a0. exact H6. + - intros H6 abs. specialize (a0 r) as [_ a0]. apply a0. + exact H6. exact abs. +Qed. + +Lemma is_upper_bound_closed : + forall (E:CReal -> Prop) (sig_forall_dec : sig_forall_dec_T) + (sig_not_dec : sig_not_dec_T) + (Einhab : exists x : CReal, E x) + (Ebound : exists x : CReal, is_upper_bound E x), + is_lub + E (proj1_sig (is_upper_bound_glb + E sig_not_dec sig_forall_dec Einhab Ebound)). +Proof. + intros. split. + - intros x Ex. + destruct (is_upper_bound_glb E sig_not_dec sig_forall_dec Einhab Ebound); simpl. + intro abs. destruct (FQ_dense x0 x abs) as [q [qmaj H]]. + specialize (a q) as [a _]. specialize (a qmaj x Ex). + contradiction. + - intros. + destruct (is_upper_bound_glb E sig_not_dec sig_forall_dec Einhab Ebound); simpl. + intro abs. destruct (FQ_dense b x abs) as [q [qmaj H0]]. + specialize (a q) as [_ a]. apply a. exact H0. + intros y Ey. specialize (H y Ey). intro abs2. + apply H. exact (CRealLt_trans _ (IQR q) _ qmaj abs2). Qed. diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 8379829037..fd375e67be 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -14,6 +14,7 @@ Require Export ZArith_base. Require Import ConstructiveCauchyReals. +Require Import ConstructiveRcomplete. Require Export Rdefinitions. Declare Scope R_scope. Local Open Scope R_scope. @@ -349,12 +350,27 @@ Definition is_lub (E:R -> Prop) (m:R) := is_upper_bound E m /\ (forall b:R, is_upper_bound E b -> m <= b). (**********) -(* This axiom can be proved by excluded middle in sort Set. - For this, define a sequence by dichotomy, using excluded middle - to know whether the current point majorates E or not. - Then conclude by the Cauchy-completeness of R, which is proved - constructively. *) -Axiom - completeness : +Lemma completeness : forall E:R -> Prop, bound E -> (exists x : R, E x) -> { m:R | is_lub E m }. +Proof. + intros. pose (fun x:CReal => E (Rabst x)) as Er. + assert (exists x : CReal, Er x) as Einhab. + { destruct H0. exists (Rrepr x). unfold Er. + replace (Rabst (Rrepr x)) with x. exact H0. + apply Rquot1. rewrite Rquot2. reflexivity. } + assert (exists x : CReal, ConstructiveRcomplete.is_upper_bound Er x) as Ebound. + { destruct H. exists (Rrepr x). intros y Ey. rewrite <- (Rquot2 y). + apply Rrepr_le. apply H. exact Ey. } + pose proof (is_upper_bound_closed Er sig_forall_dec sig_not_dec + Einhab Ebound). + destruct (is_upper_bound_glb + Er sig_not_dec sig_forall_dec Einhab Ebound); simpl in H1. + exists (Rabst x). split. + intros y Ey. apply Rrepr_le. rewrite Rquot2. apply H1. + unfold Er. replace (Rabst (Rrepr y)) with y. exact Ey. + apply Rquot1. rewrite Rquot2. reflexivity. + intros. destruct H1. apply Rrepr_le. rewrite Rquot2. + apply H3. intros y Ey. rewrite <- Rquot2. + apply Rrepr_le, H2, Ey. +Qed. diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 03eb6c8b44..025192203e 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -33,6 +33,8 @@ Axiom sig_forall_dec : forall (P : nat -> Prop), (forall n, {P n} + {~P n}) -> {n | ~P n} + {forall n, P n}. +Axiom sig_not_dec : forall P : Prop, {not (not P)} + {not P}. + Axiom Rabst : CReal -> R. Axiom Rrepr : R -> CReal. Axiom Rquot1 : forall x y:R, CRealEq (Rrepr x) (Rrepr y) -> x = y. @@ -151,30 +153,11 @@ Definition IZR (z:Z) : R := end. Arguments IZR z%Z : simpl never. -Lemma CRealLt_dec : forall x y : CReal, { CRealLt x y } + { ~CRealLt x y }. -Proof. - intros. - destruct (sig_forall_dec - (fun n:nat => Qle (proj1_sig y (S n) - proj1_sig x (S n)) (2 # Pos.of_nat (S n)))). - - intro n. destruct (Qlt_le_dec (2 # Pos.of_nat (S n)) - (proj1_sig y (S n) - proj1_sig x (S n))). - right. apply Qlt_not_le. exact q. left. exact q. - - left. destruct s as [n nmaj]. exists (Pos.of_nat (S n)). - rewrite Nat2Pos.id. apply Qnot_le_lt. exact nmaj. discriminate. - - right. intro abs. destruct abs as [n majn]. - specialize (q (pred (Pos.to_nat n))). - replace (S (pred (Pos.to_nat n))) with (Pos.to_nat n) in q. - rewrite Pos2Nat.id in q. - pose proof (Qle_not_lt _ _ q). contradiction. - symmetry. apply Nat.succ_pred. intro abs. - pose proof (Pos2Nat.is_pos n). rewrite abs in H. inversion H. -Qed. - Lemma total_order_T : forall r1 r2:R, {Rlt r1 r2} + {r1 = r2} + {Rlt r2 r1}. Proof. - intros. destruct (CRealLt_dec (Rrepr r1) (Rrepr r2)). + intros. destruct (CRealLt_lpo_dec (Rrepr r1) (Rrepr r2) sig_forall_dec). - left. left. rewrite RbaseSymbolsImpl.Rlt_def. exact c. - - destruct (CRealLt_dec (Rrepr r2) (Rrepr r1)). + - destruct (CRealLt_lpo_dec (Rrepr r2) (Rrepr r1) sig_forall_dec). + right. rewrite RbaseSymbolsImpl.Rlt_def. exact c. + left. right. apply Rquot1. split; assumption. Qed. |