diff options
Diffstat (limited to 'theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v')
| -rw-r--r-- | theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v | 994 |
1 files changed, 462 insertions, 532 deletions
diff --git a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v index fc57fc4056..f3a59b493f 100644 --- a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v +++ b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v @@ -20,7 +20,7 @@ Require CMorphisms. Local Open Scope CReal_scope. -Definition QCauchySeq_bound (qn : nat -> Q) (cvmod : positive -> nat) +Definition QCauchySeq_bound (qn : positive -> Q) (cvmod : positive -> positive) : positive := match Qnum (qn (cvmod 1%positive)) with | Z0 => 1%positive @@ -28,13 +28,13 @@ Definition QCauchySeq_bound (qn : nat -> Q) (cvmod : positive -> nat) | Z.neg p => p + 1 end. -Lemma QCauchySeq_bounded_prop (qn : nat -> Q) (cvmod : positive -> nat) +Lemma QCauchySeq_bounded_prop (qn : positive -> Q) (cvmod : positive -> positive) : QCauchySeq qn cvmod - -> forall n:nat, le (cvmod 1%positive) n - -> Qlt (Qabs (qn n)) (Z.pos (QCauchySeq_bound qn cvmod) # 1). + -> forall n:positive, Pos.le (cvmod 1%positive) n + -> Qlt (Qabs (qn n)) (Z.pos (QCauchySeq_bound qn cvmod) # 1). Proof. intros H n H0. unfold QCauchySeq_bound. - specialize (H 1%positive (cvmod 1%positive) n (le_refl _) H0). + specialize (H 1%positive (cvmod 1%positive) n (Pos.le_refl _) H0). destruct (qn (cvmod 1%positive)) as [a b]. unfold Qnum. rewrite Qabs_Qminus in H. apply (Qplus_lt_l _ _ (-Qabs (a#b))). @@ -56,24 +56,21 @@ Proof. Qed. Lemma CReal_mult_cauchy - : forall (xn yn zn : nat -> Q) (Ay Az : positive) (cvmod : positive -> nat), + : forall (xn yn zn : positive -> Q) (Ay Az : positive) (cvmod : positive -> positive), QSeqEquiv xn yn cvmod - -> QCauchySeq zn Pos.to_nat - -> (forall n:nat, le (cvmod 2%positive) n + -> QCauchySeq zn id + -> (forall n:positive, Pos.le (cvmod 2%positive) n -> Qlt (Qabs (yn n)) (Z.pos Ay # 1)) - -> (forall n:nat, le 1 n + -> (forall n:positive, Pos.le 1 n -> Qlt (Qabs (zn n)) (Z.pos Az # 1)) - -> QSeqEquiv (fun n:nat => xn n * zn n) (fun n:nat => yn n * zn n) - (fun p => max (max (cvmod 2%positive) + -> QSeqEquiv (fun n:positive => xn n * zn n) (fun n:positive => yn n * zn n) + (fun p => Pos.max (Pos.max (cvmod 2%positive) (cvmod (2 * (Pos.max Ay Az) * p)%positive)) - (Pos.to_nat (2 * (Pos.max Ay Az) * p)%positive)). + (2 * (Pos.max Ay Az) * p)%positive). Proof. intros xn yn zn Ay Az cvmod limx limz majy majz. remember (Pos.mul 2 (Pos.max Ay Az)) as z. intros k p q H H0. - assert (Pos.to_nat k <> O) as kPos. - { intro absurd. pose proof (Pos2Nat.is_pos k). - rewrite absurd in H1. inversion H1. } setoid_replace (xn p * zn p - yn q * zn q)%Q with ((xn p - yn q) * zn p + yn q * (zn p - zn q))%Q. 2: ring. @@ -84,12 +81,12 @@ Proof. apply Qplus_lt_le_compat. - apply (Qle_lt_trans _ ((1#z * k) * Qabs (zn p)%nat)). + apply Qmult_le_compat_r. apply Qle_lteq. left. apply limx. - apply (le_trans _ (Init.Nat.max (cvmod (z * k)%positive) (Pos.to_nat (z * k)))). - apply Nat.le_max_l. refine (le_trans _ _ _ _ H). - rewrite <- Nat.max_assoc. apply Nat.le_max_r. - apply (le_trans _ (Init.Nat.max (cvmod (z * k)%positive) (Pos.to_nat (z * k)))). - apply Nat.le_max_l. refine (le_trans _ _ _ _ H0). - rewrite <- Nat.max_assoc. apply Nat.le_max_r. apply Qabs_nonneg. + apply (Pos.le_trans _ (Pos.max (cvmod (z * k)%positive) (z * k))). + apply Pos.le_max_l. refine (Pos.le_trans _ _ _ _ H). + rewrite <- Pos.max_assoc. apply Pos.le_max_r. + apply (Pos.le_trans _ (Pos.max (cvmod (z * k)%positive) (z * k))). + apply Pos.le_max_l. refine (Pos.le_trans _ _ _ _ H0). + rewrite <- Pos.max_assoc. apply Pos.le_max_r. apply Qabs_nonneg. + subst z. rewrite <- (Qmult_1_r (1 # 2 * k)). rewrite <- Pos.mul_assoc. rewrite <- (Pos.mul_comm k). rewrite Pos.mul_assoc. rewrite (factorDenom _ _ (2 * k)). rewrite <- Qmult_assoc. @@ -102,21 +99,20 @@ Proof. rewrite Qmult_comm. apply Qmult_lt_l. reflexivity. setoid_replace (/(1#Az))%Q with (Z.pos Az # 1)%Q. 2: reflexivity. - apply majz. - refine (le_trans _ _ _ _ H). - apply (le_trans _ (Pos.to_nat (2 * Pos.max Ay Az * k))). - apply Pos2Nat.is_pos. apply Nat.le_max_r. + apply majz. refine (Pos.le_trans _ _ _ _ H). + apply (Pos.le_trans _ (2 * Pos.max Ay Az * k)). + discriminate. apply Pos.le_max_r. - apply (Qle_trans _ ((1 # z * k) * Qabs (yn q)%nat)). + rewrite Qmult_comm. apply Qmult_le_compat_r. apply Qle_lteq. left. apply limz. - apply (le_trans _ (max (cvmod (z * k)%positive) - (Pos.to_nat (z * k)%positive))). - apply Nat.le_max_r. refine (le_trans _ _ _ _ H). - rewrite <- Nat.max_assoc. apply Nat.le_max_r. - apply (le_trans _ (max (cvmod (z * k)%positive) - (Pos.to_nat (z * k)%positive))). - apply Nat.le_max_r. refine (le_trans _ _ _ _ H0). - rewrite <- Nat.max_assoc. apply Nat.le_max_r. + apply (Pos.le_trans _ (Pos.max (cvmod (z * k)%positive) + (z * k)%positive)). + apply Pos.le_max_r. refine (Pos.le_trans _ _ _ _ H). + rewrite <- Pos.max_assoc. apply Pos.le_max_r. + apply (Pos.le_trans _ (Pos.max (cvmod (z * k)%positive) + (z * k)%positive)). + apply Pos.le_max_r. refine (Pos.le_trans _ _ _ _ H0). + rewrite <- Pos.max_assoc. apply Pos.le_max_r. apply Qabs_nonneg. + subst z. rewrite <- (Qmult_1_r (1 # 2 * k)). rewrite <- Pos.mul_assoc. rewrite <- (Pos.mul_comm k). rewrite Pos.mul_assoc. @@ -130,38 +126,36 @@ Proof. 2: intro abs; inversion abs. rewrite Qmult_comm. apply Qmult_lt_l. reflexivity. setoid_replace (/(1#Ay))%Q with (Z.pos Ay # 1)%Q. 2: reflexivity. - apply majy. refine (le_trans _ _ _ _ H0). - rewrite <- Nat.max_assoc. apply Nat.le_max_l. + apply majy. refine (Pos.le_trans _ _ _ _ H0). + rewrite <- Pos.max_assoc. apply Pos.le_max_l. - rewrite Qinv_plus_distr. unfold Qeq. reflexivity. Qed. -Lemma linear_max : forall (p Ax Ay : positive) (i : nat), - le (Pos.to_nat p) i - -> (max (max 2 (Pos.to_nat (2 * Pos.max Ax Ay * p))) - (Pos.to_nat (2 * Pos.max Ax Ay * p)) - <= Pos.to_nat (2 * Pos.max Ax Ay) * i)%nat. -Proof. - intros. rewrite max_l. 2: apply Nat.le_max_r. rewrite max_r. - rewrite Pos2Nat.inj_mul. apply Nat.mul_le_mono_nonneg. - apply le_0_n. apply le_refl. apply le_0_n. exact H. - apply (Pos2Nat.inj_le 2). rewrite <- Pos.mul_assoc. - apply (Pos.mul_le_mono_l 2 1). - rewrite <- (Pos.mul_le_mono_l 2 1). +Lemma linear_max : forall (p Ax Ay i : positive), + Pos.le p i + -> (Pos.max (Pos.max 2 (2 * Pos.max Ax Ay * p)) + (2 * Pos.max Ax Ay * p) + <= (2 * Pos.max Ax Ay) * i)%positive. +Proof. + intros. rewrite Pos.max_l. 2: apply Pos.le_max_r. rewrite Pos.max_r. + apply Pos.mul_le_mono_l. exact H. + apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. + rewrite <- Pos.mul_assoc, <- (Pos.mul_le_mono_l 2). destruct (Pos.max Ax Ay * p)%positive; discriminate. Qed. Definition CReal_mult (x y : CReal) : CReal. Proof. destruct x as [xn limx]. destruct y as [yn limy]. - pose (QCauchySeq_bound xn Pos.to_nat) as Ax. - pose (QCauchySeq_bound yn Pos.to_nat) as Ay. - exists (fun n : nat => xn (Pos.to_nat (2 * Pos.max Ax Ay) * n)%nat - * yn (Pos.to_nat (2 * Pos.max Ax Ay) * n)%nat). + pose (QCauchySeq_bound xn id) as Ax. + pose (QCauchySeq_bound yn id) as Ay. + exists (fun n : positive => xn ((2 * Pos.max Ax Ay) * n)%positive + * yn ((2 * Pos.max Ax Ay) * n)%positive). intros p n k H0 H1. - apply (CReal_mult_cauchy xn xn yn Ax Ay Pos.to_nat limx limy). - intros. apply (QCauchySeq_bounded_prop xn Pos.to_nat limx). - apply (le_trans _ (Pos.to_nat 2)). apply le_S, le_refl. exact H. - intros. exact (QCauchySeq_bounded_prop yn Pos.to_nat limy _ H). + apply (CReal_mult_cauchy xn xn yn Ax Ay id limx limy). + intros. apply (QCauchySeq_bounded_prop xn id limx). + apply (Pos.le_trans _ 2). discriminate. exact H. + intros. exact (QCauchySeq_bounded_prop yn id limy _ H). apply linear_max; assumption. apply linear_max; assumption. Defined. @@ -169,45 +163,44 @@ Infix "*" := CReal_mult : CReal_scope. Lemma CReal_mult_unfold : forall x y : CReal, QSeqEquivEx (proj1_sig (CReal_mult x y)) - (fun n : nat => proj1_sig x n * proj1_sig y n)%Q. + (fun n : positive => proj1_sig x n * proj1_sig y n)%Q. Proof. intros [xn limx] [yn limy]. unfold CReal_mult ; simpl. - pose proof (QCauchySeq_bounded_prop xn Pos.to_nat limx) as majx. - pose proof (QCauchySeq_bounded_prop yn Pos.to_nat limy) as majy. - remember (QCauchySeq_bound xn Pos.to_nat) as Ax. - remember (QCauchySeq_bound yn Pos.to_nat) as Ay. + pose proof (QCauchySeq_bounded_prop xn id limx) as majx. + pose proof (QCauchySeq_bounded_prop yn id limy) as majy. + remember (QCauchySeq_bound xn id) as Ax. + remember (QCauchySeq_bound yn id) as Ay. exists (fun p : positive => - Init.Nat.max (Pos.to_nat (2 * Pos.max Ax Ay * p)) - (Pos.to_nat (2 * Pos.max Ax Ay * p))). - intros p n k H0 H1. rewrite max_l in H0, H1. - apply (CReal_mult_cauchy xn xn yn Ax Ay Pos.to_nat limx limy). + Pos.max (2 * Pos.max Ax Ay * p) + (2 * Pos.max Ax Ay * p)). + intros p n k H0 H1. rewrite Pos.max_l in H0, H1. + apply (CReal_mult_cauchy xn xn yn Ax Ay id limx limy). 2: apply majy. intros. apply majx. - refine (le_trans _ _ _ _ H). apply le_S, le_refl. - 3: apply le_refl. 3: apply le_refl. - apply linear_max. refine (le_trans _ _ _ _ H0). - rewrite <- (mult_1_l (Pos.to_nat p)). rewrite Pos2Nat.inj_mul. - apply Nat.mul_le_mono_nonneg. auto. apply Pos2Nat.is_pos. - apply le_0_n. apply le_refl. rewrite max_l. - rewrite Nat.max_r. apply H1. apply Pos2Nat.inj_le. - 2: apply Nat.le_max_r. - apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. + refine (Pos.le_trans _ _ _ _ H). discriminate. + 3: apply Pos.le_refl. 3: apply Pos.le_refl. + apply linear_max. refine (Pos.le_trans _ _ _ _ H0). + apply (Pos.le_trans _ (1*p)). apply Pos.le_refl. + apply Pos.mul_le_mono_r. discriminate. + rewrite Pos.max_l. + rewrite Pos.max_r. apply H1. 2: apply Pos.le_max_r. + apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. unfold id. rewrite <- Pos.mul_assoc, <- (Pos.mul_le_mono_l 2 1). destruct (Pos.max Ax Ay * p)%positive; discriminate. Qed. -Lemma CReal_mult_assoc_bounded_r : forall (xn yn zn : nat -> Q), +Lemma CReal_mult_assoc_bounded_r : forall (xn yn zn : positive -> Q), QSeqEquivEx xn yn (* both are Cauchy with same limit *) - -> QSeqEquiv zn zn Pos.to_nat + -> QSeqEquiv zn zn id -> QSeqEquivEx (fun n => xn n * zn n)%Q (fun n => yn n * zn n)%Q. Proof. intros xn yn zn [cvmod cveq] H0. - exists (fun p => max (max (cvmod 2%positive) (cvmod (2 * (Pos.max (QCauchySeq_bound yn (fun k : positive => cvmod (2 * k)%positive)) (QCauchySeq_bound zn Pos.to_nat)) * p)%positive)) - (Pos.to_nat (2 * (Pos.max (QCauchySeq_bound yn (fun k : positive => cvmod (2 * k)%positive)) (QCauchySeq_bound zn Pos.to_nat)) * p)%positive)). + exists (fun p => Pos.max (Pos.max (cvmod 2%positive) (cvmod (2 * (Pos.max (QCauchySeq_bound yn (fun k : positive => cvmod (2 * k)%positive)) (QCauchySeq_bound zn id)) * p)%positive)) + (2 * (Pos.max (QCauchySeq_bound yn (fun k : positive => cvmod (2 * k)%positive)) (QCauchySeq_bound zn id)) * p)%positive). apply (CReal_mult_cauchy _ _ _ _ _ _ cveq H0). exact (QCauchySeq_bounded_prop yn (fun k => cvmod (2 * k)%positive) (QSeqEquiv_cau_r xn yn cvmod cveq)). - exact (QCauchySeq_bounded_prop zn Pos.to_nat H0). + exact (QCauchySeq_bounded_prop zn id H0). Qed. Lemma CReal_mult_assoc : forall x y z : CReal, (x * y) * z == x * (y * z). @@ -217,74 +210,72 @@ Proof. - apply (QSeqEquivEx_trans _ (fun n => proj1_sig (CReal_mult x y) n * proj1_sig z n)%Q). apply CReal_mult_unfold. destruct x as [xn limx], y as [yn limy], z as [zn limz]; unfold CReal_mult; simpl. - pose proof (QCauchySeq_bounded_prop xn Pos.to_nat limx) as majx. - pose proof (QCauchySeq_bounded_prop yn Pos.to_nat limy) as majy. - pose proof (QCauchySeq_bounded_prop zn Pos.to_nat limz) as majz. - remember (QCauchySeq_bound xn Pos.to_nat) as Ax. - remember (QCauchySeq_bound yn Pos.to_nat) as Ay. - remember (QCauchySeq_bound zn Pos.to_nat) as Az. + pose proof (QCauchySeq_bounded_prop xn id limx) as majx. + pose proof (QCauchySeq_bounded_prop yn id limy) as majy. + pose proof (QCauchySeq_bounded_prop zn id limz) as majz. + remember (QCauchySeq_bound xn id) as Ax. + remember (QCauchySeq_bound yn id) as Ay. + remember (QCauchySeq_bound zn id) as Az. apply CReal_mult_assoc_bounded_r. 2: exact limz. exists (fun p : positive => - Init.Nat.max (Pos.to_nat (2 * Pos.max Ax Ay * p)) - (Pos.to_nat (2 * Pos.max Ax Ay * p))). + Pos.max (2 * Pos.max Ax Ay * p) + (2 * Pos.max Ax Ay * p)). intros p n k H0 H1. - apply (CReal_mult_cauchy xn xn yn Ax Ay Pos.to_nat limx limy). - 2: exact majy. intros. apply majx. refine (le_trans _ _ _ _ H). - apply le_S, le_refl. rewrite max_l in H0, H1. - 2: apply le_refl. 2: apply le_refl. + apply (CReal_mult_cauchy xn xn yn Ax Ay id limx limy). + 2: exact majy. intros. apply majx. refine (Pos.le_trans _ _ _ _ H). + discriminate. rewrite Pos.max_l in H0, H1. + 2: apply Pos.le_refl. 2: apply Pos.le_refl. apply linear_max. - apply (le_trans _ (Pos.to_nat (2 * Pos.max Ax Ay * p))). - rewrite <- (mult_1_l (Pos.to_nat p)). rewrite Pos2Nat.inj_mul. - apply Nat.mul_le_mono_nonneg. auto. apply Pos2Nat.is_pos. - apply le_0_n. apply le_refl. apply H0. rewrite max_l. 2: apply Nat.le_max_r. - rewrite Nat.max_r in H1. 2: apply le_refl. - refine (le_trans _ _ _ _ H1). rewrite Nat.max_r. - apply le_refl. apply Pos2Nat.inj_le. - apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. + apply (Pos.le_trans _ (2 * Pos.max Ax Ay * p)). + apply (Pos.le_trans _ (1*p)). apply Pos.le_refl. + apply Pos.mul_le_mono_r. discriminate. + exact H0. rewrite Pos.max_l. 2: apply Pos.le_max_r. + rewrite Pos.max_r in H1. 2: apply Pos.le_refl. + refine (Pos.le_trans _ _ _ _ H1). rewrite Pos.max_r. + apply Pos.le_refl. apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. + unfold id. rewrite <- Pos.mul_assoc, <- (Pos.mul_le_mono_l 2 1). destruct (Pos.max Ax Ay * p)%positive; discriminate. - apply (QSeqEquivEx_trans _ (fun n => proj1_sig x n * proj1_sig (CReal_mult y z) n)%Q). 2: apply QSeqEquivEx_sym; apply CReal_mult_unfold. destruct x as [xn limx], y as [yn limy], z as [zn limz]; unfold CReal_mult; simpl. - pose proof (QCauchySeq_bounded_prop xn Pos.to_nat limx) as majx. - pose proof (QCauchySeq_bounded_prop yn Pos.to_nat limy) as majy. - pose proof (QCauchySeq_bounded_prop zn Pos.to_nat limz) as majz. - remember (QCauchySeq_bound xn Pos.to_nat) as Ax. - remember (QCauchySeq_bound yn Pos.to_nat) as Ay. - remember (QCauchySeq_bound zn Pos.to_nat) as Az. - pose proof (CReal_mult_assoc_bounded_r (fun n0 : nat => yn n0 * zn n0)%Q (fun n : nat => - yn (Pos.to_nat (Pos.max Ay Az)~0 * n)%nat - * zn (Pos.to_nat (Pos.max Ay Az)~0 * n)%nat)%Q xn) + pose proof (QCauchySeq_bounded_prop xn id limx) as majx. + pose proof (QCauchySeq_bounded_prop yn id limy) as majy. + pose proof (QCauchySeq_bounded_prop zn id limz) as majz. + remember (QCauchySeq_bound xn id) as Ax. + remember (QCauchySeq_bound yn id) as Ay. + remember (QCauchySeq_bound zn id) as Az. + pose proof (CReal_mult_assoc_bounded_r (fun n0 : positive => yn n0 * zn n0)%Q (fun n : positive => + yn ((Pos.max Ay Az)~0 * n)%positive + * zn ((Pos.max Ay Az)~0 * n)%positive)%Q xn) as [cvmod cveq]. + exists (fun p : positive => - max (Pos.to_nat (2 * Pos.max Ay Az * p)) - (Pos.to_nat (2 * Pos.max Ay Az * p))). - intros p n k H0 H1. rewrite max_l in H0, H1. - apply (CReal_mult_cauchy yn yn zn Ay Az Pos.to_nat limy limz). - 2: exact majz. intros. apply majy. refine (le_trans _ _ _ _ H). - apply le_S, le_refl. - 3: apply le_refl. 3: apply le_refl. - rewrite max_l. rewrite max_r. apply H0. - apply Pos2Nat.inj_le. - apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. + Pos.max (2 * Pos.max Ay Az * p) + (2 * Pos.max Ay Az * p)). + intros p n k H0 H1. rewrite Pos.max_l in H0, H1. + apply (CReal_mult_cauchy yn yn zn Ay Az id limy limz). + 2: exact majz. intros. apply majy. refine (Pos.le_trans _ _ _ _ H). + discriminate. + 3: apply Pos.le_refl. 3: apply Pos.le_refl. + rewrite Pos.max_l. rewrite Pos.max_r. apply H0. + apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. unfold id. rewrite <- Pos.mul_assoc, <- (Pos.mul_le_mono_l 2 1). destruct (Pos.max Ay Az * p)%positive; discriminate. - apply Nat.le_max_r. - apply linear_max. refine (le_trans _ _ _ _ H1). - rewrite <- (mult_1_l (Pos.to_nat p)). rewrite Pos2Nat.inj_mul. - apply Nat.mul_le_mono_nonneg. auto. apply Pos2Nat.is_pos. - apply le_0_n. apply le_refl. + apply Pos.le_max_r. + apply linear_max. refine (Pos.le_trans _ _ _ _ H1). + apply (Pos.le_trans _ (1*p)). apply Pos.le_refl. + apply Pos.mul_le_mono_r. discriminate. + exact limx. + exists cvmod. intros p k n H1 H2. specialize (cveq p k n H1 H2). setoid_replace (xn k * yn k * zn k - xn n * - (yn (Pos.to_nat (Pos.max Ay Az)~0 * n)%nat * - zn (Pos.to_nat (Pos.max Ay Az)~0 * n)%nat))%Q - with ((fun n : nat => yn n * zn n * xn n) k - - (fun n : nat => - yn (Pos.to_nat (Pos.max Ay Az)~0 * n)%nat * - zn (Pos.to_nat (Pos.max Ay Az)~0 * n)%nat * + (yn ((Pos.max Ay Az)~0 * n)%positive * + zn ((Pos.max Ay Az)~0 * n)%positive))%Q + with ((fun n : positive => yn n * zn n * xn n) k - + (fun n : positive => + yn ((Pos.max Ay Az)~0 * n)%positive * + zn ((Pos.max Ay Az)~0 * n)%positive * xn n) n)%Q. apply cveq. ring. Qed. @@ -295,30 +286,29 @@ Proof. apply (QSeqEquivEx_trans _ (fun n => proj1_sig y n * proj1_sig x n)%Q). destruct x as [xn limx], y as [yn limy]; simpl. 2: apply QSeqEquivEx_sym; apply CReal_mult_unfold. - pose proof (QCauchySeq_bounded_prop xn Pos.to_nat limx) as majx. - pose proof (QCauchySeq_bounded_prop yn Pos.to_nat limy) as majy. - remember (QCauchySeq_bound xn Pos.to_nat) as Ax. - remember (QCauchySeq_bound yn Pos.to_nat) as Ay. + pose proof (QCauchySeq_bounded_prop xn id limx) as majx. + pose proof (QCauchySeq_bounded_prop yn id limy) as majy. + remember (QCauchySeq_bound xn id) as Ax. + remember (QCauchySeq_bound yn id) as Ay. apply QSeqEquivEx_sym. exists (fun p : positive => - Init.Nat.max (Pos.to_nat (2 * Pos.max Ay Ax * p)) - (Pos.to_nat (2 * Pos.max Ay Ax * p))). - intros p n k H0 H1. rewrite max_l in H0, H1. - 2: apply le_refl. 2: apply le_refl. - rewrite (Qmult_comm (xn (Pos.to_nat (Pos.max Ax Ay)~0 * k)%nat)). - apply (CReal_mult_cauchy yn yn xn Ay Ax Pos.to_nat limy limx). - 2: exact majx. intros. apply majy. refine (le_trans _ _ _ _ H). - apply le_S, le_refl. - rewrite max_l. rewrite max_r. apply H0. - apply Pos2Nat.inj_le. + Pos.max (2 * Pos.max Ay Ax * p) + (2 * Pos.max Ay Ax * p)). + intros p n k H0 H1. rewrite Pos.max_l in H0, H1. + 2: apply Pos.le_refl. 2: apply Pos.le_refl. + rewrite (Qmult_comm (xn ((Pos.max Ax Ay)~0 * k)%positive)). + apply (CReal_mult_cauchy yn yn xn Ay Ax id limy limx). + 2: exact majx. intros. apply majy. refine (Pos.le_trans _ _ _ _ H). + discriminate. + rewrite Pos.max_l. rewrite Pos.max_r. apply H0. + unfold id. apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. rewrite <- Pos.mul_assoc, <- (Pos.mul_le_mono_l 2 1). destruct (Pos.max Ay Ax * p)%positive; discriminate. - apply Nat.le_max_r. rewrite (Pos.max_comm Ax Ay). - apply linear_max. refine (le_trans _ _ _ _ H1). - rewrite <- (mult_1_l (Pos.to_nat p)). rewrite Pos2Nat.inj_mul. - apply Nat.mul_le_mono_nonneg. auto. apply Pos2Nat.is_pos. - apply le_0_n. apply le_refl. + apply Pos.le_max_r. rewrite (Pos.max_comm Ax Ay). + apply linear_max. refine (Pos.le_trans _ _ _ _ H1). + apply (Pos.le_trans _ (1*p)). apply Pos.le_refl. + apply Pos.mul_le_mono_r. discriminate. Qed. Lemma CReal_mult_proper_l : forall x y z : CReal, @@ -333,16 +323,16 @@ Proof. apply CReal_mult_unfold. destruct x as [xn limx], y as [yn limy], z as [zn limz]; simpl. destruct H as [cvmod H]. simpl in H. - pose proof (QCauchySeq_bounded_prop xn Pos.to_nat limx) as majx. + pose proof (QCauchySeq_bounded_prop xn id limx) as majx. pose proof (QCauchySeq_bounded_prop zn (fun k => cvmod (2 * k)%positive) (QSeqEquiv_cau_r yn zn cvmod H)) as majz. - remember (QCauchySeq_bound xn Pos.to_nat) as Ax. + remember (QCauchySeq_bound xn id) as Ax. remember (QCauchySeq_bound zn (fun k => cvmod (2 * k)%positive)) as Az. apply QSeqEquivEx_sym. exists (fun p : positive => - max (max (cvmod (2%positive)) (cvmod (2 * Pos.max Az Ax * p)%positive)) - (Pos.to_nat (2 * Pos.max Az Ax * p))). + Pos.max (Pos.max (cvmod (2%positive)) (cvmod (2 * Pos.max Az Ax * p)%positive)) + (2 * Pos.max Az Ax * p)). intros p n k H1 H2. setoid_replace (xn n * yn n - xn k * zn k)%Q with (yn n * xn n - zn k * xn k)%Q. 2: ring. @@ -359,25 +349,21 @@ Proof. pose proof (CRealLt_aboveSig (inject_Q 0) x x0 H). pose proof (CRealLt_aboveSig (inject_Q 0) y x1 H0). destruct x as [xn limx], y as [yn limy]; simpl in H, H1, H2, H0. - pose proof (QCauchySeq_bounded_prop xn Pos.to_nat limx) as majx. - pose proof (QCauchySeq_bounded_prop yn Pos.to_nat limy) as majy. - destruct (Qarchimedean (/ (xn (Pos.to_nat x0) - 0 - (2 # x0)))). - destruct (Qarchimedean (/ (yn (Pos.to_nat x1) - 0 - (2 # x1)))). + pose proof (QCauchySeq_bounded_prop xn id limx) as majx. + pose proof (QCauchySeq_bounded_prop yn id limy) as majy. + destruct (Qarchimedean (/ (xn x0 - 0 - (2 # x0)))). + destruct (Qarchimedean (/ (yn x1 - 0 - (2 # x1)))). exists (Pos.max x0 x~0 * Pos.max x1 x2~0)%positive. simpl. - remember (QCauchySeq_bound xn Pos.to_nat) as Ax. - remember (QCauchySeq_bound yn Pos.to_nat) as Ay. + remember (QCauchySeq_bound xn id) as Ax. + remember (QCauchySeq_bound yn id) as Ay. unfold Qminus. rewrite Qplus_0_r. - rewrite <- Pos2Nat.inj_mul. unfold Qminus in H1, H2. specialize (H1 ((Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0))%positive). assert (Pos.max x1 x2~0 <= (Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0))%positive. - { apply Pos2Nat.inj_le. - rewrite Pos.mul_assoc. rewrite Pos2Nat.inj_mul. - rewrite <- (mult_1_l (Pos.to_nat (Pos.max x1 x2~0))). - rewrite mult_assoc. apply Nat.mul_le_mono_nonneg. auto. - rewrite mult_1_r. apply Pos2Nat.is_pos. apply le_0_n. - apply le_refl. } + { rewrite Pos.mul_assoc. + rewrite <- (Pos.mul_1_l (Pos.max x1 x2~0)). + rewrite Pos.mul_assoc. apply Pos.mul_le_mono_r. discriminate. } specialize (H2 ((Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0))%positive H3). rewrite Qplus_0_r in H1, H2. apply (Qlt_trans _ ((2 # Pos.max x0 x~0) * (2 # Pos.max x1 x2~0))). @@ -386,7 +372,7 @@ Proof. replace (Z.pos p~0) with (2 * Z.pos p)%Z. apply Z.mul_lt_mono_pos_r. apply Pos2Z.is_pos. reflexivity. reflexivity. apply H4. - apply (Qlt_trans _ ((2 # Pos.max x0 x~0) * (yn (Pos.to_nat ((Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0)))))). + apply (Qlt_trans _ ((2 # Pos.max x0 x~0) * (yn ((Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0))%positive))). apply Qmult_lt_l. reflexivity. apply H2. apply Qmult_lt_r. apply (Qlt_trans 0 (2 # Pos.max x1 x2~0)). reflexivity. apply H2. apply H1. rewrite Pos.mul_comm. apply Pos2Nat.inj_le. @@ -406,140 +392,133 @@ Proof. apply CReal_mult_unfold. apply (QSeqEquivEx_trans _ (fun n => proj1_sig (CReal_mult x y) n + proj1_sig (CReal_mult x z) n))%Q. - 2: apply QSeqEquivEx_sym; exists (fun p => Pos.to_nat (2 * p)) + 2: apply QSeqEquivEx_sym; exists (fun p:positive => 2 * p)%positive ; apply CReal_plus_unfold. apply (QSeqEquivEx_trans _ (fun n => proj1_sig x n * (proj1_sig y n + proj1_sig z n))%Q). - pose proof (CReal_plus_unfold y z). destruct x as [xn limx], y as [yn limy], z as [zn limz]; simpl; simpl in H. - pose proof (QCauchySeq_bounded_prop xn Pos.to_nat) as majx. - pose proof (QCauchySeq_bounded_prop yn Pos.to_nat) as majy. - pose proof (QCauchySeq_bounded_prop zn Pos.to_nat) as majz. - remember (QCauchySeq_bound xn Pos.to_nat) as Ax. - remember (QCauchySeq_bound yn Pos.to_nat) as Ay. - remember (QCauchySeq_bound zn Pos.to_nat) as Az. - pose proof (CReal_mult_cauchy (fun n => yn (n + (n + 0))%nat + zn (n + (n + 0))%nat)%Q + pose proof (QCauchySeq_bounded_prop xn id) as majx. + pose proof (QCauchySeq_bounded_prop yn id) as majy. + pose proof (QCauchySeq_bounded_prop zn id) as majz. + remember (QCauchySeq_bound xn id) as Ax. + remember (QCauchySeq_bound yn id) as Ay. + remember (QCauchySeq_bound zn id) as Az. + pose proof (CReal_mult_cauchy (fun n => yn (n~0)%positive + zn (n~0)%positive)%Q (fun n => yn n + zn n)%Q xn (Ay + Az) Ax - (fun p => Pos.to_nat (2 * p)) H limx). - exists (fun p : positive => (Pos.to_nat (2 * (2 * Pos.max (Ay + Az) Ax * p)))). + (fun p:positive => 2 * p)%positive H limx). + exists (fun p : positive => (2 * (2 * Pos.max (Ay + Az) Ax * p))%positive). intros p n k H1 H2. - setoid_replace (xn n * (yn (n + (n + 0))%nat + zn (n + (n + 0))%nat) - xn k * (yn k + zn k))%Q - with ((yn (n + (n + 0))%nat + zn (n + (n + 0))%nat) * xn n - (yn k + zn k) * xn k)%Q. + setoid_replace (xn n * (yn (n~0)%positive + zn (n~0)%positive) - xn k * (yn k + zn k))%Q + with ((yn (n~0)%positive + zn (n~0)%positive) * xn n - (yn k + zn k) * xn k)%Q. 2: ring. - assert (Pos.to_nat (2 * Pos.max (Ay + Az) Ax * p) <= - Pos.to_nat 2 * Pos.to_nat (2 * Pos.max (Ay + Az) Ax * p))%nat. - { rewrite (Pos2Nat.inj_mul 2). - rewrite <- (mult_1_l (Pos.to_nat (2 * Pos.max (Ay + Az) Ax * p))). - rewrite mult_assoc. apply Nat.mul_le_mono_nonneg. auto. - simpl. auto. apply le_0_n. apply le_refl. } + assert ((2 * Pos.max (Ay + Az) Ax * p) <= + 2 * (2 * Pos.max (Ay + Az) Ax * p))%positive. + { rewrite <- Pos.mul_assoc. + apply Pos.mul_le_mono_l. + apply (Pos.le_trans _ (1*(Pos.max (Ay + Az) Ax * p))). + apply Pos.le_refl. apply Pos.mul_le_mono_r. discriminate. } apply H0. intros n0 H4. apply (Qle_lt_trans _ _ _ (Qabs_triangle _ _)). rewrite Pos2Z.inj_add, <- Qinv_plus_distr. apply Qplus_lt_le_compat. apply majy. exact limy. - refine (le_trans _ _ _ _ H4); apply le_n_S, le_0_n. + refine (Pos.le_trans _ _ _ _ H4); discriminate. apply Qlt_le_weak. apply majz. exact limz. - refine (le_trans _ _ _ _ H4); apply le_n_S, le_0_n. - apply majx. exact limx. refine (le_trans _ _ _ _ H1). - rewrite max_l. rewrite max_r. apply le_refl. - apply Pos2Nat.inj_le. rewrite <- (Pos.mul_le_mono_l 2). + refine (Pos.le_trans _ _ _ _ H4); discriminate. + apply majx. exact limx. refine (Pos.le_trans _ _ _ _ H1). + rewrite Pos.max_l. rewrite Pos.max_r. apply Pos.le_refl. + rewrite <- (Pos.mul_le_mono_l 2). apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l. destruct (Pos.max (Ay + Az) Ax * p)%positive; discriminate. - apply (le_trans _ (Pos.to_nat (2 * (2 * Pos.max (Ay + Az) Ax * p)))). - 2: apply Nat.le_max_r. apply Pos2Nat.inj_le. + apply (Pos.le_trans _ (2 * (2 * Pos.max (Ay + Az) Ax * p))). + 2: apply Pos.le_max_r. rewrite <- Pos.mul_assoc. rewrite (Pos.mul_assoc 2 2). rewrite <- Pos.mul_le_mono_r. discriminate. - refine (le_trans _ _ _ _ H2). rewrite <- Nat.max_comm. - rewrite Nat.max_assoc. rewrite max_r. apply le_refl. - apply Nat.max_lub. - rewrite <- Pos2Nat.inj_mul in H3. apply H3. apply Pos2Nat.inj_le. + refine (Pos.le_trans _ _ _ _ H2). rewrite <- Pos.max_comm. + rewrite Pos.max_assoc. rewrite Pos.max_r. apply Pos.le_refl. + apply Pos.max_lub. apply H3. rewrite <- Pos.mul_le_mono_l. apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l. destruct (Pos.max (Ay + Az) Ax * p)%positive; discriminate. - destruct x as [xn limx], y as [yn limy], z as [zn limz]; simpl. - pose proof (QCauchySeq_bounded_prop xn Pos.to_nat) as majx. - pose proof (QCauchySeq_bounded_prop yn Pos.to_nat) as majy. - pose proof (QCauchySeq_bounded_prop zn Pos.to_nat) as majz. - remember (QCauchySeq_bound xn Pos.to_nat) as Ax. - remember (QCauchySeq_bound yn Pos.to_nat) as Ay. - remember (QCauchySeq_bound zn Pos.to_nat) as Az. - exists (fun p : positive => (Pos.to_nat (2 * (Pos.max (Pos.max Ax Ay) Az) * (2 * p)))). + pose proof (QCauchySeq_bounded_prop xn id) as majx. + pose proof (QCauchySeq_bounded_prop yn id) as majy. + pose proof (QCauchySeq_bounded_prop zn id) as majz. + remember (QCauchySeq_bound xn id) as Ax. + remember (QCauchySeq_bound yn id) as Ay. + remember (QCauchySeq_bound zn id) as Az. + exists (fun p : positive => (2 * (Pos.max (Pos.max Ax Ay) Az) * (2 * p))%positive). intros p n k H H0. setoid_replace (xn n * (yn n + zn n) - - (xn (Pos.to_nat (Pos.max Ax Ay)~0 * k)%nat * - yn (Pos.to_nat (Pos.max Ax Ay)~0 * k)%nat + - xn (Pos.to_nat (Pos.max Ax Az)~0 * k)%nat * - zn (Pos.to_nat (Pos.max Ax Az)~0 * k)%nat))%Q - with (xn n * yn n - (xn (Pos.to_nat (Pos.max Ax Ay)~0 * k)%nat * - yn (Pos.to_nat (Pos.max Ax Ay)~0 * k)%nat) - + (xn n * zn n - xn (Pos.to_nat (Pos.max Ax Az)~0 * k)%nat * - zn (Pos.to_nat (Pos.max Ax Az)~0 * k)%nat))%Q. + (xn ((Pos.max Ax Ay)~0 * k)%positive * + yn ((Pos.max Ax Ay)~0 * k)%positive + + xn ((Pos.max Ax Az)~0 * k)%positive * + zn ((Pos.max Ax Az)~0 * k)%positive))%Q + with (xn n * yn n - (xn ((Pos.max Ax Ay)~0 * k)%positive * + yn ((Pos.max Ax Ay)~0 * k)%positive) + + (xn n * zn n - xn ((Pos.max Ax Az)~0 * k)%positive * + zn ((Pos.max Ax Az)~0 * k)%positive))%Q. 2: ring. - apply (Qle_lt_trans _ (Qabs (xn n * yn n - (xn (Pos.to_nat (Pos.max Ax Ay)~0 * k)%nat * - yn (Pos.to_nat (Pos.max Ax Ay)~0 * k)%nat)) - + Qabs (xn n * zn n - xn (Pos.to_nat (Pos.max Ax Az)~0 * k)%nat * - zn (Pos.to_nat (Pos.max Ax Az)~0 * k)%nat))). + apply (Qle_lt_trans _ (Qabs (xn n * yn n - (xn ((Pos.max Ax Ay)~0 * k)%positive * + yn ((Pos.max Ax Ay)~0 * k)%positive)) + + Qabs (xn n * zn n - xn ((Pos.max Ax Az)~0 * k)%positive * + zn ((Pos.max Ax Az)~0 * k)%positive))). apply Qabs_triangle. setoid_replace (1#p)%Q with ((1#2*p) + (1#2*p))%Q. apply Qplus_lt_le_compat. - + apply (CReal_mult_cauchy xn xn yn Ax Ay Pos.to_nat limx limy). + + apply (CReal_mult_cauchy xn xn yn Ax Ay id limx limy). intros. apply majx. exact limx. - refine (le_trans _ _ _ _ H1). apply le_S, le_refl. + refine (Pos.le_trans _ _ _ _ H1). discriminate. apply majy. exact limy. - rewrite <- Nat.max_assoc. - rewrite (Nat.max_l ((Pos.to_nat (2 * Pos.max Ax Ay * (2 * p))))). - 2: apply le_refl. - refine (le_trans _ _ _ _ H). apply Nat.max_lub. - apply Pos2Nat.inj_le. apply (Pos.le_trans _ (2*1)). + rewrite <- Pos.max_assoc. + rewrite (Pos.max_l ((2 * Pos.max Ax Ay * (2 * p)))). + 2: apply Pos.le_refl. + refine (Pos.le_trans _ _ _ _ H). apply Pos.max_lub. + apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l. destruct (Pos.max (Pos.max Ax Ay) Az * (2 * p))%positive; discriminate. - apply Pos2Nat.inj_le. rewrite <- Pos.mul_assoc, <- Pos.mul_assoc. rewrite <- Pos.mul_le_mono_l, <- Pos.mul_le_mono_r. apply Pos.le_max_l. - rewrite <- Nat.max_assoc. - rewrite (Nat.max_l ((Pos.to_nat (2 * Pos.max Ax Ay * (2 * p))))). - 2: apply le_refl. - rewrite max_r. apply (le_trans _ (1*k)). - rewrite Nat.mul_1_l. refine (le_trans _ _ _ _ H0). - apply Pos2Nat.inj_le. + rewrite <- Pos.max_assoc. + rewrite (Pos.max_l ((2 * Pos.max Ax Ay * (2 * p)))). + 2: apply Pos.le_refl. + rewrite Pos.max_r. apply (Pos.le_trans _ (1*k)). + rewrite Pos.mul_1_l. refine (Pos.le_trans _ _ _ _ H0). rewrite <- Pos.mul_assoc, <- Pos.mul_assoc, <- Pos.mul_le_mono_l. rewrite <- Pos.mul_le_mono_r. - apply Pos.le_max_l. apply Nat.mul_le_mono_nonneg_r. apply le_0_n. - apply Pos2Nat.is_pos. apply Pos2Nat.inj_le. + apply Pos.le_max_l. apply Pos.mul_le_mono_r. discriminate. apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l. destruct (Pos.max Ax Ay * (2 * p))%positive; discriminate. + apply Qlt_le_weak. - apply (CReal_mult_cauchy xn xn zn Ax Az Pos.to_nat limx limz). + apply (CReal_mult_cauchy xn xn zn Ax Az id limx limz). intros. apply majx. exact limx. - refine (le_trans _ _ _ _ H1). apply le_S, le_refl. + refine (Pos.le_trans _ _ _ _ H1). discriminate. intros. apply majz. exact limz. exact H1. - rewrite <- Nat.max_assoc. - rewrite (Nat.max_l ((Pos.to_nat (2 * Pos.max Ax Az * (2 * p))))). - 2: apply le_refl. - refine (le_trans _ _ _ _ H). apply Nat.max_lub. - apply Pos2Nat.inj_le. apply (Pos.le_trans _ (2*1)). + rewrite <- Pos.max_assoc. + rewrite (Pos.max_l ((2 * Pos.max Ax Az * (2 * p)))). + 2: apply Pos.le_refl. + refine (Pos.le_trans _ _ _ _ H). apply Pos.max_lub. + apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l. destruct (Pos.max (Pos.max Ax Ay) Az * (2 * p))%positive; discriminate. - apply Pos2Nat.inj_le. rewrite <- Pos.mul_assoc, <- Pos.mul_assoc. rewrite <- Pos.mul_le_mono_l, <- Pos.mul_le_mono_r. rewrite <- Pos.max_assoc, (Pos.max_comm Ay Az), Pos.max_assoc. apply Pos.le_max_l. - rewrite <- Nat.max_assoc. - rewrite (Nat.max_l ((Pos.to_nat (2 * Pos.max Ax Az * (2 * p))))). - 2: apply le_refl. - rewrite max_r. apply (le_trans _ (1*k)). - rewrite Nat.mul_1_l. refine (le_trans _ _ _ _ H0). - apply Pos2Nat.inj_le. + rewrite <- Pos.max_assoc. + rewrite (Pos.max_l ((2 * Pos.max Ax Az * (2 * p)))). + 2: apply Pos.le_refl. + rewrite Pos.max_r. apply (Pos.le_trans _ (1*k)). + rewrite Pos.mul_1_l. refine (Pos.le_trans _ _ _ _ H0). rewrite <- Pos.mul_assoc, <- Pos.mul_assoc, <- Pos.mul_le_mono_l. rewrite <- Pos.mul_le_mono_r. rewrite <- Pos.max_assoc, (Pos.max_comm Ay Az), Pos.max_assoc. - apply Pos.le_max_l. apply Nat.mul_le_mono_nonneg_r. apply le_0_n. - apply Pos2Nat.is_pos. apply Pos2Nat.inj_le. + apply Pos.le_max_l. apply Pos.mul_le_mono_r. discriminate. apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l. destruct (Pos.max Ax Az * (2 * p))%positive; discriminate. @@ -560,38 +539,37 @@ Proof. intros [rn limr]. split. - intros [m maj]. simpl in maj. rewrite Qmult_1_l in maj. - pose proof (QCauchySeq_bounded_prop (fun _ : nat => 1%Q) Pos.to_nat (ConstCauchy 1)). - pose proof (QCauchySeq_bounded_prop rn Pos.to_nat limr). - remember (QCauchySeq_bound (fun _ : nat => 1%Q) Pos.to_nat) as x. - remember (QCauchySeq_bound rn Pos.to_nat) as x0. + pose proof (QCauchySeq_bounded_prop (fun _ : positive => 1%Q) id (ConstCauchy 1)). + pose proof (QCauchySeq_bounded_prop rn id limr). + remember (QCauchySeq_bound (fun _ : positive => 1%Q) id) as x. + remember (QCauchySeq_bound rn id) as x0. specialize (limr m). apply (Qlt_not_le (2 # m) (1 # m)). - apply (Qlt_trans _ (rn (Pos.to_nat m) - - rn (Pos.to_nat (Pos.max x x0)~0 * Pos.to_nat m)%nat)). + apply (Qlt_trans _ (rn m + - rn ((Pos.max x x0)~0 * m)%positive)). apply maj. - apply (Qle_lt_trans _ (Qabs (rn (Pos.to_nat m) - rn (Pos.to_nat (Pos.max x x0)~0 * Pos.to_nat m)%nat))). - apply Qle_Qabs. apply limr. apply le_refl. - rewrite <- (mult_1_l (Pos.to_nat m)). rewrite mult_assoc. - apply Nat.mul_le_mono_nonneg. auto. rewrite mult_1_r. - apply Pos2Nat.is_pos. apply le_0_n. apply le_refl. + apply (Qle_lt_trans _ (Qabs (rn m - rn ((Pos.max x x0)~0 * m)%positive))). + apply Qle_Qabs. apply limr. apply Pos.le_refl. + rewrite <- (Pos.mul_1_l m). rewrite Pos.mul_assoc. unfold id. + apply Pos.mul_le_mono_r. discriminate. apply Z.mul_le_mono_nonneg. discriminate. discriminate. discriminate. apply Z.le_refl. - intros [m maj]. simpl in maj. - pose proof (QCauchySeq_bounded_prop (fun _ : nat => 1%Q) Pos.to_nat (ConstCauchy 1)). - pose proof (QCauchySeq_bounded_prop rn Pos.to_nat limr). - remember (QCauchySeq_bound (fun _ : nat => 1%Q) Pos.to_nat) as x. - remember (QCauchySeq_bound rn Pos.to_nat) as x0. + pose proof (QCauchySeq_bounded_prop (fun _ : positive => 1%Q) id (ConstCauchy 1)). + pose proof (QCauchySeq_bounded_prop rn id limr). + remember (QCauchySeq_bound (fun _ : positive => 1%Q) id) as x. + remember (QCauchySeq_bound rn id) as x0. simpl in maj. rewrite Qmult_1_l in maj. specialize (limr m). apply (Qlt_not_le (2 # m) (1 # m)). - apply (Qlt_trans _ (rn (Pos.to_nat (Pos.max x x0)~0 * Pos.to_nat m)%nat - rn (Pos.to_nat m))). + apply (Qlt_trans _ (rn ((Pos.max x x0)~0 * m)%positive - rn m)). apply maj. - apply (Qle_lt_trans _ (Qabs (rn (Pos.to_nat (Pos.max x x0)~0 * Pos.to_nat m)%nat - rn (Pos.to_nat m)))). + apply (Qle_lt_trans _ (Qabs (rn ((Pos.max x x0)~0 * m)%positive - rn m))). apply Qle_Qabs. apply limr. - rewrite <- (mult_1_l (Pos.to_nat m)). rewrite mult_assoc. - apply Nat.mul_le_mono_nonneg. auto. rewrite mult_1_r. - apply Pos2Nat.is_pos. apply le_0_n. apply le_refl. - apply le_refl. apply Z.mul_le_mono_nonneg. discriminate. discriminate. + rewrite <- (Pos.mul_1_l m). rewrite Pos.mul_assoc. unfold id. + apply Pos.mul_le_mono_r. discriminate. + apply Pos.le_refl. + apply Z.mul_le_mono_nonneg. discriminate. discriminate. discriminate. apply Z.le_refl. Qed. @@ -748,11 +726,11 @@ Proof. Qed. Lemma CReal_abs_appart_zero : forall (x : CReal) (n : positive), - Qlt (2#n) (Qabs (proj1_sig x (Pos.to_nat n))) + Qlt (2#n) (Qabs (proj1_sig x n)) -> 0 # x. Proof. intros. destruct x as [xn xcau]. simpl in H. - destruct (Qlt_le_dec 0 (xn (Pos.to_nat n))). + destruct (Qlt_le_dec 0 (xn n)). - left. exists n; simpl. rewrite Qabs_pos in H. ring_simplify. exact H. apply Qlt_le_weak. exact q. - right. exists n; simpl. rewrite Qabs_neg in H. @@ -769,39 +747,40 @@ Lemma CRealArchimedean Proof. (* Locate x within 1/4 and pick the first integer above this interval. *) intros [xn limx]. - pose proof (Qlt_floor (xn 4%nat + (1#4))). unfold inject_Z in H. - pose proof (Qfloor_le (xn 4%nat + (1#4))). unfold inject_Z in H0. - remember (Qfloor (xn 4%nat + (1#4)))%Z as n. + pose proof (Qlt_floor (xn 4%positive + (1#4))). unfold inject_Z in H. + pose proof (Qfloor_le (xn 4%positive + (1#4))). unfold inject_Z in H0. + remember (Qfloor (xn 4%positive + (1#4)))%Z as n. exists (n+1)%Z. split. - - assert (Qlt 0 ((n + 1 # 1) - (xn 4%nat + (1 # 4)))) as epsPos. + - assert (Qlt 0 ((n + 1 # 1) - (xn 4%positive + (1 # 4)))) as epsPos. { unfold Qminus. rewrite <- Qlt_minus_iff. exact H. } - destruct (Qarchimedean (/((1#2)*((n + 1 # 1) - (xn 4%nat + (1 # 4)))))) as [k kmaj]. + destruct (Qarchimedean (/((1#2)*((n + 1 # 1) - (xn 4%positive + (1 # 4)))))) as [k kmaj]. exists (Pos.max 4 k). simpl. - apply (Qlt_trans _ ((n + 1 # 1) - (xn 4%nat + (1 # 4)))). + apply (Qlt_trans _ ((n + 1 # 1) - (xn 4%positive + (1 # 4)))). + setoid_replace (Z.pos k # 1)%Q with (/(1#k))%Q in kmaj. 2: reflexivity. rewrite <- Qinv_lt_contravar in kmaj. 2: reflexivity. apply (Qle_lt_trans _ (2#k)). rewrite <- (Qmult_le_l _ _ (1#2)). setoid_replace ((1 # 2) * (2 # k))%Q with (1#k)%Q. 2: reflexivity. - setoid_replace ((1 # 2) * (2 # Pos.max 4 k))%Q with (1#Pos.max 4 k)%Q. 2: reflexivity. + setoid_replace ((1 # 2) * (2 # Pos.max 4 k))%Q with (1#Pos.max 4 k)%Q. + 2: reflexivity. unfold Qle; simpl. apply Pos2Z.pos_le_pos. apply Pos.le_max_r. reflexivity. rewrite <- (Qmult_lt_l _ _ (1#2)). setoid_replace ((1 # 2) * (2 # k))%Q with (1#k)%Q. exact kmaj. reflexivity. reflexivity. rewrite <- (Qmult_0_r (1#2)). rewrite Qmult_lt_l. exact epsPos. reflexivity. - + rewrite <- (Qplus_lt_r _ _ (xn (Pos.to_nat (Pos.max 4 k)) - (n + 1 # 1) + (1#4))). + + rewrite <- (Qplus_lt_r _ _ (xn (Pos.max 4 k) - (n + 1 # 1) + (1#4))). ring_simplify. - apply (Qle_lt_trans _ (Qabs (xn (Pos.to_nat (Pos.max 4 k)) - xn 4%nat))). + apply (Qle_lt_trans _ (Qabs (xn (Pos.max 4 k) - xn 4%positive))). apply Qle_Qabs. apply limx. - rewrite Pos2Nat.inj_max. apply Nat.le_max_l. apply le_refl. + apply Pos.le_max_l. apply Pos.le_refl. - apply (CReal_plus_lt_reg_l (-(2))). ring_simplify. exists 4%positive. simpl. rewrite <- Qinv_plus_distr. rewrite <- (Qplus_lt_r _ _ ((n#1) - (1#2))). ring_simplify. - apply (Qle_lt_trans _ (xn 4%nat + (1 # 4)) _ H0). + apply (Qle_lt_trans _ (xn 4%positive + (1 # 4)) _ H0). unfold Pos.to_nat; simpl. - rewrite <- (Qplus_lt_r _ _ (-xn 4%nat)). ring_simplify. + rewrite <- (Qplus_lt_r _ _ (-xn 4%positive)). ring_simplify. reflexivity. Defined. @@ -821,9 +800,10 @@ Lemma CRealLtDisjunctEpsilon : forall a b c d : CReal, (CRealLtProp a b \/ CRealLtProp c d) -> CRealLt a b + CRealLt c d. Proof. intros. + (* Convert to nat to use indefinite description. *) assert (exists n : nat, n <> O /\ - (Qlt (2 # Pos.of_nat n) (proj1_sig b n - proj1_sig a n) - \/ Qlt (2 # Pos.of_nat n) (proj1_sig d n - proj1_sig c n))). + (Qlt (2 # Pos.of_nat n) (proj1_sig b (Pos.of_nat n) - proj1_sig a (Pos.of_nat n)) + \/ Qlt (2 # Pos.of_nat n) (proj1_sig d (Pos.of_nat n) - proj1_sig c (Pos.of_nat n)))). { destruct H. destruct H as [n maj]. exists (Pos.to_nat n). split. intro abs. destruct (Pos2Nat.is_succ n). rewrite H in abs. inversion abs. left. rewrite Pos2Nat.id. apply maj. @@ -833,72 +813,73 @@ Proof. apply constructive_indefinite_ground_description_nat in H0. - destruct H0 as [n [nPos maj]]. destruct (Qlt_le_dec (2 # Pos.of_nat n) - (proj1_sig b n - proj1_sig a n)). - left. exists (Pos.of_nat n). rewrite Nat2Pos.id. apply q. apply nPos. - assert (2 # Pos.of_nat n < proj1_sig d n - proj1_sig c n)%Q. + (proj1_sig b (Pos.of_nat n) - proj1_sig a (Pos.of_nat n))). + left. exists (Pos.of_nat n). apply q. + assert (2 # Pos.of_nat n < proj1_sig d (Pos.of_nat n) - proj1_sig c (Pos.of_nat n))%Q. destruct maj. exfalso. - apply (Qlt_not_le (2 # Pos.of_nat n) (proj1_sig b n - proj1_sig a n)); assumption. - assumption. clear maj. right. exists (Pos.of_nat n). rewrite Nat2Pos.id. - apply H0. apply nPos. + apply (Qlt_not_le (2 # Pos.of_nat n) (proj1_sig b (Pos.of_nat n) - proj1_sig a (Pos.of_nat n))); assumption. + assumption. clear maj. right. exists (Pos.of_nat n). + apply H0. - clear H0. clear H. intro n. destruct n. right. intros [abs _]. exact (abs (eq_refl O)). - destruct (Qlt_le_dec (2 # Pos.of_nat (S n)) (proj1_sig b (S n) - proj1_sig a (S n))). + destruct (Qlt_le_dec (2 # Pos.of_nat (S n)) (proj1_sig b (Pos.of_nat (S n)) - proj1_sig a (Pos.of_nat (S n)))). left. split. discriminate. left. apply q. - destruct (Qlt_le_dec (2 # Pos.of_nat (S n)) (proj1_sig d (S n) - proj1_sig c (S n))). + destruct (Qlt_le_dec (2 # Pos.of_nat (S n)) (proj1_sig d (Pos.of_nat (S n)) - proj1_sig c (Pos.of_nat (S n)))). left. split. discriminate. right. apply q0. right. intros [_ [abs|abs]]. apply (Qlt_not_le (2 # Pos.of_nat (S n)) - (proj1_sig b (S n) - proj1_sig a (S n))); assumption. + (proj1_sig b (Pos.of_nat (S n)) - proj1_sig a (Pos.of_nat (S n)))); assumption. apply (Qlt_not_le (2 # Pos.of_nat (S n)) - (proj1_sig d (S n) - proj1_sig c (S n))); assumption. + (proj1_sig d (Pos.of_nat (S n)) - proj1_sig c (Pos.of_nat (S n)))); assumption. Qed. -Lemma CRealShiftReal : forall (x : CReal) (k : nat), - QCauchySeq (fun n => proj1_sig x (plus n k)) Pos.to_nat. +Lemma CRealShiftReal : forall (x : CReal) (k : positive), + QCauchySeq (fun n => proj1_sig x (Pos.add n k)) id. Proof. - intros x k n p q H H0. + assert (forall p k : positive, (p <= p + k)%positive). + { intros. apply Pos2Nat.inj_le. rewrite Pos2Nat.inj_add. + apply (le_trans _ (Pos.to_nat p + 0)). + rewrite plus_0_r. apply le_refl. apply Nat.add_le_mono_l. + apply le_0_n. } + intros x k n p q H0 H1. destruct x as [xn cau]; unfold proj1_sig. - destruct k. rewrite plus_0_r. rewrite plus_0_r. apply cau; assumption. - specialize (cau (n + Pos.of_nat (S k))%positive (p + S k)%nat (q + S k)%nat). - apply (Qlt_trans _ (1 # n + Pos.of_nat (S k))). - apply cau. rewrite Pos2Nat.inj_add. rewrite Nat2Pos.id. - apply Nat.add_le_mono_r. apply H. discriminate. - rewrite Pos2Nat.inj_add. rewrite Nat2Pos.id. - apply Nat.add_le_mono_r. apply H0. discriminate. - apply Pos2Nat.inj_lt; simpl. rewrite Pos2Nat.inj_add. - rewrite <- (plus_0_r (Pos.to_nat n)). rewrite <- plus_assoc. - apply Nat.add_lt_mono_l. apply Pos2Nat.is_pos. + apply cau. apply (Pos.le_trans _ _ _ H0). apply H. + apply (Pos.le_trans _ _ _ H1). apply H. Qed. -Lemma CRealShiftEqual : forall (x : CReal) (k : nat), - CRealEq x (exist _ (fun n => proj1_sig x (plus n k)) (CRealShiftReal x k)). +Lemma CRealShiftEqual : forall (x : CReal) (k : positive), + CRealEq x (exist _ (fun n => proj1_sig x (Pos.add n k)) (CRealShiftReal x k)). Proof. intros. split. - intros [n maj]. destruct x as [xn cau]; simpl in maj. - specialize (cau n (Pos.to_nat n + k)%nat (Pos.to_nat n)). + specialize (cau n (n + k)%positive n). apply Qlt_not_le in maj. apply maj. clear maj. - apply (Qle_trans _ (Qabs (xn (Pos.to_nat n + k)%nat - xn (Pos.to_nat n)))). + apply (Qle_trans _ (Qabs (xn (n + k)%positive - xn n))). apply Qle_Qabs. apply (Qle_trans _ (1#n)). apply Zlt_le_weak. - apply cau. rewrite <- (plus_0_r (Pos.to_nat n)). - rewrite <- plus_assoc. apply Nat.add_le_mono_l. apply le_0_n. - apply le_refl. apply Z.mul_le_mono_pos_r. apply Pos2Z.is_pos. - discriminate. + apply cau. unfold id. apply Pos2Nat.inj_le. rewrite Pos2Nat.inj_add. + apply (le_trans _ (Pos.to_nat n + 0)). + rewrite plus_0_r. apply le_refl. apply Nat.add_le_mono_l. + apply le_0_n. apply Pos.le_refl. + apply Z.mul_le_mono_pos_r. apply Pos2Z.is_pos. discriminate. - intros [n maj]. destruct x as [xn cau]; simpl in maj. - specialize (cau n (Pos.to_nat n) (Pos.to_nat n + k)%nat). + specialize (cau n n (n + k)%positive). apply Qlt_not_le in maj. apply maj. clear maj. - apply (Qle_trans _ (Qabs (xn (Pos.to_nat n) - xn (Pos.to_nat n + k)%nat))). + apply (Qle_trans _ (Qabs (xn n - xn (n + k)%positive))). apply Qle_Qabs. apply (Qle_trans _ (1#n)). apply Zlt_le_weak. - apply cau. apply le_refl. rewrite <- (plus_0_r (Pos.to_nat n)). - rewrite <- plus_assoc. apply Nat.add_le_mono_l. apply le_0_n. + apply cau. apply Pos.le_refl. + apply Pos2Nat.inj_le. rewrite Pos2Nat.inj_add. + apply (le_trans _ (Pos.to_nat n + 0)). + rewrite plus_0_r. apply le_refl. apply Nat.add_le_mono_l. + apply le_0_n. apply Z.mul_le_mono_pos_r. apply Pos2Z.is_pos. discriminate. Qed. (* Find an equal negative real number, which rational sequence stays below 0, so that it can be inversed. *) Definition CRealNegShift (x : CReal) - : CRealLt x (inject_Q 0) - -> { y : prod positive CReal | CRealEq x (snd y) - /\ forall n:nat, Qlt (proj1_sig (snd y) n) (-1 # fst y) }. + : x < inject_Q 0 + -> { y : prod positive CReal + | x == (snd y) /\ forall n:positive, Qlt (proj1_sig (snd y) n) (-1 # fst y) }. Proof. intro xNeg. pose proof (CRealLt_aboveSig x (inject_Q 0)). @@ -906,36 +887,26 @@ Proof. pose proof (CRealShiftEqual x). destruct xNeg as [n maj], x as [xn cau]; simpl in maj. specialize (H n maj); simpl in H. - destruct (Qarchimedean (/ (0 - xn (Pos.to_nat n) - (2 # n)))) as [a _]. + destruct (Qarchimedean (/ (0 - xn n - (2 # n)))) as [a _]. remember (Pos.max n a~0) as k. clear Heqk. clear maj. clear n. - exists (pair k - (exist _ (fun n => xn (plus n (Pos.to_nat k))) (H0 (Pos.to_nat k)))). + exists (pair k (exist _ (fun n => xn (Pos.add n k)) (H0 k))). split. apply H1. intro n. simpl. apply Qlt_minus_iff. - destruct n. - - specialize (H k). - unfold Qminus in H. rewrite Qplus_0_l in H. apply Qlt_minus_iff in H. - unfold Qminus. rewrite Qplus_comm. - apply (Qlt_trans _ (- xn (Pos.to_nat k)%nat - (2 #k))). apply H. - unfold Qminus. simpl. apply Qplus_lt_r. - apply Z.mul_lt_mono_pos_r. simpl. apply Pos2Z.is_pos. - reflexivity. apply Pos.le_refl. - - apply (Qlt_trans _ (-(2 # k) - xn (S n + Pos.to_nat k)%nat)). - rewrite <- (Nat2Pos.id (S n)). rewrite <- Pos2Nat.inj_add. - specialize (H (Pos.of_nat (S n) + k)%positive). - unfold Qminus in H. rewrite Qplus_0_l in H. apply Qlt_minus_iff in H. - unfold Qminus. rewrite Qplus_comm. apply H. apply Pos2Nat.inj_le. - rewrite <- (plus_0_l (Pos.to_nat k)). rewrite Pos2Nat.inj_add. - apply Nat.add_le_mono_r. apply le_0_n. discriminate. - apply Qplus_lt_l. - apply Z.mul_lt_mono_pos_r. simpl. apply Pos2Z.is_pos. - reflexivity. + apply (Qlt_trans _ (-(2 # k) - xn (n + k)%positive)). + specialize (H (n + k)%positive). + unfold Qminus in H. rewrite Qplus_0_l in H. apply Qlt_minus_iff in H. + unfold Qminus. rewrite Qplus_comm. apply H. apply Pos2Nat.inj_le. + rewrite <- (plus_0_l (Pos.to_nat k)). rewrite Pos2Nat.inj_add. + apply Nat.add_le_mono_r. apply le_0_n. + apply Qplus_lt_l. + apply Z.mul_lt_mono_pos_r. simpl. apply Pos2Z.is_pos. + reflexivity. Qed. Definition CRealPosShift (x : CReal) : inject_Q 0 < x - -> { y : prod positive CReal | CRealEq x (snd y) - /\ forall n:nat, Qlt (1 # fst y) (proj1_sig (snd y) n) }. + -> { y : prod positive CReal + | x == (snd y) /\ forall n:positive, Qlt (1 # fst y) (proj1_sig (snd y) n) }. Proof. intro xPos. pose proof (CRealLt_aboveSig (inject_Q 0) x). @@ -943,66 +914,57 @@ Proof. pose proof (CRealShiftEqual x). destruct xPos as [n maj], x as [xn cau]; simpl in maj. simpl in H. specialize (H n). - destruct (Qarchimedean (/ (xn (Pos.to_nat n) - 0 - (2 # n)))) as [a _]. + destruct (Qarchimedean (/ (xn n - 0 - (2 # n)))) as [a _]. specialize (H maj); simpl in H. remember (Pos.max n a~0) as k. clear Heqk. clear maj. clear n. - exists (pair k - (exist _ (fun n => xn (plus n (Pos.to_nat k))) (H0 (Pos.to_nat k)))). + exists (pair k (exist _ (fun n => xn (Pos.add n k)) (H0 k))). split. apply H1. intro n. simpl. apply Qlt_minus_iff. - destruct n. - - specialize (H k). - unfold Qminus in H. rewrite Qplus_0_r in H. - simpl. rewrite <- Qlt_minus_iff. - apply (Qlt_trans _ (2 #k)). - apply Z.mul_lt_mono_pos_r. simpl. apply Pos2Z.is_pos. - reflexivity. apply H. apply Pos.le_refl. - - rewrite <- Qlt_minus_iff. apply (Qlt_trans _ (2 # k)). - apply Z.mul_lt_mono_pos_r. simpl. apply Pos2Z.is_pos. - reflexivity. specialize (H (Pos.of_nat (S n) + k)%positive). - unfold Qminus in H. rewrite Qplus_0_r in H. - rewrite Pos2Nat.inj_add in H. rewrite Nat2Pos.id in H. - apply H. apply Pos2Nat.inj_le. - rewrite <- (plus_0_l (Pos.to_nat k)). rewrite Pos2Nat.inj_add. - apply Nat.add_le_mono_r. apply le_0_n. discriminate. + rewrite <- Qlt_minus_iff. apply (Qlt_trans _ (2 # k)). + apply Z.mul_lt_mono_pos_r. simpl. apply Pos2Z.is_pos. + reflexivity. specialize (H (n + k)%positive). + unfold Qminus in H. rewrite Qplus_0_r in H. + apply H. apply Pos2Nat.inj_le. + rewrite <- (plus_0_l (Pos.to_nat k)). rewrite Pos2Nat.inj_add. + apply Nat.add_le_mono_r. apply le_0_n. Qed. -Lemma CReal_inv_neg : forall (yn : nat -> Q) (k : positive), - (QCauchySeq yn Pos.to_nat) - -> (forall n : nat, yn n < -1 # k)%Q - -> QCauchySeq (fun n : nat => / yn (Pos.to_nat k ^ 2 * n)%nat) Pos.to_nat. +Lemma CReal_inv_neg : forall (yn : positive -> Q) (k : positive), + (QCauchySeq yn id) + -> (forall n : positive, yn n < -1 # k)%Q + -> QCauchySeq (fun n : positive => / yn (k ^ 2 * n)%positive) id. Proof. (* Prove the inverse sequence is Cauchy *) intros yn k cau maj n p q H0 H1. - setoid_replace (/ yn (Pos.to_nat k ^ 2 * p)%nat - - / yn (Pos.to_nat k ^ 2 * q)%nat)%Q - with ((yn (Pos.to_nat k ^ 2 * q)%nat - - yn (Pos.to_nat k ^ 2 * p)%nat) - / (yn (Pos.to_nat k ^ 2 * q)%nat * - yn (Pos.to_nat k ^ 2 * p)%nat)). - + apply (Qle_lt_trans _ (Qabs (yn (Pos.to_nat k ^ 2 * q)%nat - - yn (Pos.to_nat k ^ 2 * p)%nat) + setoid_replace (/ yn (k ^ 2 * p)%positive - + / yn (k ^ 2 * q)%positive)%Q + with ((yn (k ^ 2 * q)%positive - + yn (k ^ 2 * p)%positive) + / (yn (k ^ 2 * q)%positive * + yn (k ^ 2 * p)%positive)). + + apply (Qle_lt_trans _ (Qabs (yn (k ^ 2 * q)%positive + - yn (k ^ 2 * p)%positive) / (1 # (k^2)))). assert (1 # k ^ 2 - < Qabs (yn (Pos.to_nat k ^ 2 * q)%nat * yn (Pos.to_nat k ^ 2 * p)%nat))%Q. + < Qabs (yn (k ^ 2 * q)%positive * yn (k ^ 2 * p)%positive))%Q. { rewrite Qabs_Qmult. unfold "^"%positive; simpl. rewrite factorDenom. rewrite Pos.mul_1_r. - apply (Qlt_trans _ ((1#k) * Qabs (yn (Pos.to_nat k * (Pos.to_nat k * 1) * p)%nat))). + apply (Qlt_trans _ ((1#k) * Qabs (yn (k * (k * 1) * p)%positive))). apply Qmult_lt_l. reflexivity. rewrite Qabs_neg. - specialize (maj (Pos.to_nat k * (Pos.to_nat k * 1) * p)%nat). + specialize (maj (k * (k * 1) * p)%positive). apply Qlt_minus_iff in maj. apply Qlt_minus_iff. rewrite Qplus_comm. setoid_replace (-(1#k))%Q with (-1 # k)%Q. apply maj. reflexivity. apply (Qle_trans _ (-1 # k)). apply Zlt_le_weak. - apply maj. discriminate. + apply maj. discriminate. rewrite Pos.mul_1_r. apply Qmult_lt_r. apply (Qlt_trans 0 (1#k)). reflexivity. rewrite Qabs_neg. - specialize (maj (Pos.to_nat k * (Pos.to_nat k * 1) * p)%nat). + specialize (maj (k * k * p)%positive). apply Qlt_minus_iff in maj. apply Qlt_minus_iff. - rewrite Qplus_comm. setoid_replace (-(1#k))%Q with (-1 # k)%Q. apply maj. - reflexivity. apply (Qle_trans _ (-1 # k)). apply Zlt_le_weak. + rewrite Qplus_comm. setoid_replace (-(1#k))%Q with (-1 # k)%Q. + apply maj. reflexivity. apply (Qle_trans _ (-1 # k)). apply Zlt_le_weak. apply maj. discriminate. rewrite Qabs_neg. - specialize (maj (Pos.to_nat k * (Pos.to_nat k * 1) * q)%nat). + specialize (maj (k * k * q)%positive). apply Qlt_minus_iff in maj. apply Qlt_minus_iff. rewrite Qplus_comm. setoid_replace (-(1#k))%Q with (-1 # k)%Q. apply maj. reflexivity. apply (Qle_trans _ (-1 # k)). apply Zlt_le_weak. @@ -1016,66 +978,56 @@ Proof. reflexivity. rewrite Qmult_1_l. apply H. apply Qabs_nonneg. simpl in maj. specialize (cau (n * (k^2))%positive - (Pos.to_nat k ^ 2 * q)%nat - (Pos.to_nat k ^ 2 * p)%nat). + (k ^ 2 * q)%positive + (k ^ 2 * p)%positive). apply Qlt_shift_div_r. reflexivity. apply (Qlt_le_trans _ (1 # n * k ^ 2)). apply cau. - rewrite Pos2Nat.inj_mul. rewrite mult_comm. - unfold "^"%positive. simpl. rewrite Pos2Nat.inj_mul. - rewrite <- mult_assoc. rewrite <- mult_assoc. - apply Nat.mul_le_mono_nonneg_l. apply le_0_n. - rewrite (mult_1_r). rewrite Pos.mul_1_r. - apply Nat.mul_le_mono_nonneg_l. apply le_0_n. - apply (le_trans _ (q+0)). rewrite plus_0_r. assumption. - rewrite plus_0_r. apply le_refl. - rewrite Pos2Nat.inj_mul. rewrite mult_comm. - unfold "^"%positive; simpl. rewrite Pos2Nat.inj_mul. - rewrite <- mult_assoc. rewrite <- mult_assoc. - apply Nat.mul_le_mono_nonneg_l. apply le_0_n. - rewrite (mult_1_r). rewrite Pos.mul_1_r. - apply Nat.mul_le_mono_nonneg_l. apply le_0_n. - apply (le_trans _ (p+0)). rewrite plus_0_r. assumption. - rewrite plus_0_r. apply le_refl. + rewrite Pos.mul_comm. + unfold "^"%positive. simpl. + unfold id. rewrite Pos.mul_1_r. + rewrite <- Pos.mul_le_mono_l. exact H1. + unfold id. rewrite Pos.mul_comm. + apply Pos.mul_le_mono_l. exact H0. rewrite factorDenom. apply Qle_refl. + field. split. intro abs. - specialize (maj (Pos.to_nat k ^ 2 * p)%nat). + specialize (maj (k ^ 2 * p)%positive). rewrite abs in maj. inversion maj. intro abs. - specialize (maj (Pos.to_nat k ^ 2 * q)%nat). + specialize (maj (k ^ 2 * q)%positive). rewrite abs in maj. inversion maj. Qed. -Lemma CReal_inv_pos : forall (yn : nat -> Q) (k : positive), - (QCauchySeq yn Pos.to_nat) - -> (forall n : nat, 1 # k < yn n)%Q - -> QCauchySeq (fun n : nat => / yn (Pos.to_nat k ^ 2 * n)%nat) Pos.to_nat. +Lemma CReal_inv_pos : forall (yn : positive -> Q) (k : positive), + (QCauchySeq yn id) + -> (forall n : positive, 1 # k < yn n)%Q + -> QCauchySeq (fun n : positive => / yn (k ^ 2 * n)%positive) id. Proof. intros yn k cau maj n p q H0 H1. - setoid_replace (/ yn (Pos.to_nat k ^ 2 * p)%nat - - / yn (Pos.to_nat k ^ 2 * q)%nat)%Q - with ((yn (Pos.to_nat k ^ 2 * q)%nat - - yn (Pos.to_nat k ^ 2 * p)%nat) - / (yn (Pos.to_nat k ^ 2 * q)%nat * - yn (Pos.to_nat k ^ 2 * p)%nat)). - + apply (Qle_lt_trans _ (Qabs (yn (Pos.to_nat k ^ 2 * q)%nat - - yn (Pos.to_nat k ^ 2 * p)%nat) + setoid_replace (/ yn (k ^ 2 * p)%positive - + / yn (k ^ 2 * q)%positive)%Q + with ((yn (k ^ 2 * q)%positive - + yn (k ^ 2 * p)%positive) + / (yn (k ^ 2 * q)%positive * + yn (k ^ 2 * p)%positive)). + + apply (Qle_lt_trans _ (Qabs (yn (k ^ 2 * q)%positive + - yn (k ^ 2 * p)%positive) / (1 # (k^2)))). assert (1 # k ^ 2 - < Qabs (yn (Pos.to_nat k ^ 2 * q)%nat * yn (Pos.to_nat k ^ 2 * p)%nat))%Q. + < Qabs (yn (k ^ 2 * q)%positive * yn (k ^ 2 * p)%positive))%Q. { rewrite Qabs_Qmult. unfold "^"%positive; simpl. rewrite factorDenom. rewrite Pos.mul_1_r. - apply (Qlt_trans _ ((1#k) * Qabs (yn (Pos.to_nat k * (Pos.to_nat k * 1) * p)%nat))). + apply (Qlt_trans _ ((1#k) * Qabs (yn (k * k * p)%positive))). apply Qmult_lt_l. reflexivity. rewrite Qabs_pos. - specialize (maj (Pos.to_nat k * (Pos.to_nat k * 1) * p)%nat). + specialize (maj (k * k * p)%positive). apply maj. apply (Qle_trans _ (1 # k)). discriminate. apply Zlt_le_weak. apply maj. apply Qmult_lt_r. apply (Qlt_trans 0 (1#k)). reflexivity. rewrite Qabs_pos. - specialize (maj (Pos.to_nat k * (Pos.to_nat k * 1) * p)%nat). + specialize (maj (k * k * p)%positive). apply maj. apply (Qle_trans _ (1 # k)). discriminate. apply Zlt_le_weak. apply maj. rewrite Qabs_pos. - specialize (maj (Pos.to_nat k * (Pos.to_nat k * 1) * q)%nat). + specialize (maj (k * k * q)%positive). apply maj. apply (Qle_trans _ (1 # k)). discriminate. apply Zlt_le_weak. apply maj. } unfold Qdiv. rewrite Qabs_Qmult. rewrite Qabs_Qinv. @@ -1087,32 +1039,20 @@ Proof. reflexivity. rewrite Qmult_1_l. apply H. apply Qabs_nonneg. simpl in maj. specialize (cau (n * (k^2))%positive - (Pos.to_nat k ^ 2 * q)%nat - (Pos.to_nat k ^ 2 * p)%nat). + (k ^ 2 * q)%positive + (k ^ 2 * p)%positive). apply Qlt_shift_div_r. reflexivity. apply (Qlt_le_trans _ (1 # n * k ^ 2)). apply cau. - rewrite Pos2Nat.inj_mul. rewrite mult_comm. - unfold "^"%positive. simpl. rewrite Pos2Nat.inj_mul. - rewrite <- mult_assoc. rewrite <- mult_assoc. - apply Nat.mul_le_mono_nonneg_l. apply le_0_n. - rewrite (mult_1_r). rewrite Pos.mul_1_r. - apply Nat.mul_le_mono_nonneg_l. apply le_0_n. - apply (le_trans _ (q+0)). rewrite plus_0_r. assumption. - rewrite plus_0_r. apply le_refl. - rewrite Pos2Nat.inj_mul. rewrite mult_comm. - unfold "^"%positive; simpl. rewrite Pos2Nat.inj_mul. - rewrite <- mult_assoc. rewrite <- mult_assoc. - apply Nat.mul_le_mono_nonneg_l. apply le_0_n. - rewrite (mult_1_r). rewrite Pos.mul_1_r. - apply Nat.mul_le_mono_nonneg_l. apply le_0_n. - apply (le_trans _ (p+0)). rewrite plus_0_r. assumption. - rewrite plus_0_r. apply le_refl. + rewrite Pos.mul_comm. unfold id. + apply Pos.mul_le_mono_l. exact H1. + unfold id. rewrite Pos.mul_comm. + apply Pos.mul_le_mono_l. exact H0. rewrite factorDenom. apply Qle_refl. + field. split. intro abs. - specialize (maj (Pos.to_nat k ^ 2 * p)%nat). + specialize (maj (k ^ 2 * p)%positive). rewrite abs in maj. inversion maj. intro abs. - specialize (maj (Pos.to_nat k ^ 2 * q)%nat). + specialize (maj (k ^ 2 * q)%positive). rewrite abs in maj. inversion maj. Qed. @@ -1121,11 +1061,11 @@ Proof. destruct xnz as [xNeg | xPos]. - destruct (CRealNegShift x xNeg) as [[k y] [_ maj]]. destruct y as [yn cau]; unfold proj1_sig, snd, fst in maj. - exists (fun n => Qinv (yn (mult (Pos.to_nat k^2) n))). + exists (fun n:positive => Qinv (yn (Pos.mul (k^2) n)%positive)). apply (CReal_inv_neg yn). apply cau. apply maj. - destruct (CRealPosShift x xPos) as [[k y] [_ maj]]. destruct y as [yn cau]; unfold proj1_sig, snd, fst in maj. - exists (fun n => Qinv (yn (mult (Pos.to_nat k^2) n))). + exists (fun n => Qinv (yn (Pos.mul (k^2) n))). apply (CReal_inv_pos yn). apply cau. apply maj. Defined. @@ -1141,19 +1081,20 @@ Proof. - destruct (CRealPosShift r c) as [[k rpos] [req maj]]. clear req. destruct rpos as [rn cau]; simpl in maj. unfold CRealLt; simpl. - destruct (Qarchimedean (rn 1%nat)) as [A majA]. + destruct (Qarchimedean (rn 1%positive)) as [A majA]. exists (2 * (A + 1))%positive. unfold Qminus. rewrite Qplus_0_r. - rewrite <- (Qmult_1_l (Qinv (rn (Pos.to_nat k * (Pos.to_nat k * 1) * Pos.to_nat (2 * (A + 1)))%nat))). + rewrite <- (Qmult_1_l (Qinv (rn (k * (k * 1) * (2 * (A + 1)))%positive))). apply Qlt_shift_div_l. apply (Qlt_trans 0 (1#k)). reflexivity. apply maj. rewrite <- (Qmult_inv_r (Z.pos A + 1 # 1)). setoid_replace (2 # 2 * (A + 1))%Q with (Qinv (Z.pos A + 1 # 1)). 2: reflexivity. rewrite Qmult_comm. apply Qmult_lt_r. reflexivity. - rewrite mult_1_r. rewrite <- Pos2Nat.inj_mul. rewrite <- Pos2Nat.inj_mul. - rewrite <- (Qplus_lt_l _ _ (- rn 1%nat)). - apply (Qle_lt_trans _ (Qabs (rn (Pos.to_nat (k * k * (2 * (A + 1)))) + - rn 1%nat))). + rewrite Pos.mul_1_r. + rewrite <- (Qplus_lt_l _ _ (- rn 1%positive)). + apply (Qle_lt_trans _ (Qabs (rn (k * k * (2 * (A + 1)))%positive + - rn 1%positive))). apply Qle_Qabs. apply (Qlt_le_trans _ 1). apply cau. - apply Pos2Nat.is_pos. apply le_refl. + destruct (k * k * (2 * (A + 1)))%positive; discriminate. + apply Pos.le_refl. rewrite <- Qinv_plus_distr. rewrite <- (Qplus_comm 1). rewrite <- Qplus_0_r. rewrite <- Qplus_assoc. rewrite <- Qplus_assoc. rewrite Qplus_le_r. rewrite Qplus_0_l. apply Qlt_le_weak. @@ -1161,32 +1102,30 @@ Proof. intro abs. inversion abs. Qed. -Lemma CReal_linear_shift : forall (x : CReal) (k : nat), - le 1 k -> QCauchySeq (fun n => proj1_sig x (k * n)%nat) Pos.to_nat. -Proof. - intros [xn limx] k lek p n m H H0. unfold proj1_sig. - apply limx. apply (le_trans _ n). apply H. - rewrite <- (mult_1_l n). rewrite mult_assoc. - apply Nat.mul_le_mono_nonneg_r. apply le_0_n. - rewrite mult_1_r. apply lek. apply (le_trans _ m). apply H0. - rewrite <- (mult_1_l m). rewrite mult_assoc. - apply Nat.mul_le_mono_nonneg_r. apply le_0_n. - rewrite mult_1_r. apply lek. +Lemma CReal_linear_shift : forall (x : CReal) (k : positive), + QCauchySeq (fun n => proj1_sig x (k * n)%positive) id. +Proof. + intros [xn limx] k p n m H H0. unfold proj1_sig. + apply limx. apply (Pos.le_trans _ n). apply H. + rewrite <- (Pos.mul_1_l n). rewrite Pos.mul_assoc. + apply Pos.mul_le_mono_r. destruct (k*1)%positive; discriminate. + apply (Pos.le_trans _ (1*m)). exact H0. + apply Pos.mul_le_mono_r. destruct k; discriminate. Qed. -Lemma CReal_linear_shift_eq : forall (x : CReal) (k : nat) (kPos : le 1 k), +Lemma CReal_linear_shift_eq : forall (x : CReal) (k : positive), CRealEq x - (exist (fun n : nat -> Q => QCauchySeq n Pos.to_nat) - (fun n : nat => proj1_sig x (k * n)%nat) (CReal_linear_shift x k kPos)). + (exist (fun n : positive -> Q => QCauchySeq n id) + (fun n : positive => proj1_sig x (k * n)%positive) (CReal_linear_shift x k)). Proof. intros. apply CRealEq_diff. intro n. destruct x as [xn limx]; unfold proj1_sig. - specialize (limx n (Pos.to_nat n) (k * Pos.to_nat n)%nat). + specialize (limx n n (k * n)%positive). apply (Qle_trans _ (1 # n)). apply Qlt_le_weak. apply limx. - apply le_refl. rewrite <- (mult_1_l (Pos.to_nat n)). - rewrite mult_assoc. apply Nat.mul_le_mono_nonneg_r. apply le_0_n. - rewrite mult_1_r. apply kPos. apply Z.mul_le_mono_nonneg_r. - discriminate. discriminate. + apply Pos.le_refl. rewrite <- (Pos.mul_1_l n). + rewrite Pos.mul_assoc. apply Pos.mul_le_mono_r. + destruct (k*1)%positive; discriminate. + apply Z.mul_le_mono_nonneg_r. discriminate. discriminate. Qed. Lemma CReal_inv_l : forall (r:CReal) (rnz : r # 0), @@ -1199,57 +1138,55 @@ Proof. apply (QSeqEquivEx_trans _ (proj1_sig (CReal_mult ((let (yn, cau) as s - return ((forall n : nat, proj1_sig s n < -1 # k) -> CReal) := rneg in - fun maj0 : forall n : nat, yn n < -1 # k => - exist (fun x : nat -> Q => QCauchySeq x Pos.to_nat) - (fun n : nat => Qinv (yn (Pos.to_nat k * (Pos.to_nat k * 1) * n))%nat) + return ((forall n : positive, proj1_sig s n < -1 # k) -> CReal) := rneg in + fun maj0 : forall n : positive, yn n < -1 # k => + exist (fun x : positive -> Q => QCauchySeq x id) + (fun n : positive => Qinv (yn (k * (k * 1) * n))%positive) (CReal_inv_neg yn k cau maj0)) maj) rneg)))%Q. + apply CRealEq_modindep. apply CRealEq_diff. apply CReal_mult_proper_l. apply req. - + assert (le 1 (Pos.to_nat k * (Pos.to_nat k * 1))%nat). rewrite mult_1_r. - rewrite <- Pos2Nat.inj_mul. apply Pos2Nat.is_pos. - apply (QSeqEquivEx_trans _ + + apply (QSeqEquivEx_trans _ (proj1_sig (CReal_mult ((let (yn, cau) as s - return ((forall n : nat, proj1_sig s n < -1 # k) -> CReal) := rneg in - fun maj0 : forall n : nat, yn n < -1 # k => - exist (fun x : nat -> Q => QCauchySeq x Pos.to_nat) - (fun n : nat => Qinv (yn (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat)) + return ((forall n : positive, proj1_sig s n < -1 # k) -> CReal) := rneg in + fun maj0 : forall n : positive, yn n < -1 # k => + exist (fun x : positive -> Q => QCauchySeq x id) + (fun n : positive => Qinv (yn (k * (k * 1) * n)%positive)) (CReal_inv_neg yn k cau maj0)) maj) - (exist _ (fun n => proj1_sig rneg (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat) (CReal_linear_shift rneg _ H)))))%Q. + (exist _ (fun n => proj1_sig rneg (k * (k * 1) * n)%positive) (CReal_linear_shift rneg _)))))%Q. apply CRealEq_modindep. apply CRealEq_diff. apply CReal_mult_proper_l. apply CReal_linear_shift_eq. destruct r as [rn limr], rneg as [rnn limneg]; simpl. pose proof (QCauchySeq_bounded_prop - (fun n : nat => Qinv (rnn (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat)) - Pos.to_nat (CReal_inv_neg rnn k limneg maj)). + (fun n : positive => Qinv (rnn (k * (k * 1) * n)%positive)) + id (CReal_inv_neg rnn k limneg maj)). pose proof (QCauchySeq_bounded_prop - (fun n : nat => rnn (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat) - Pos.to_nat + (fun n : positive => rnn (k * (k * 1) * n)%positive) + id (CReal_linear_shift - (exist (fun x0 : nat -> Q => QCauchySeq x0 Pos.to_nat) rnn limneg) - (Pos.to_nat k * (Pos.to_nat k * 1)) H)) ; simpl. + (exist (fun x0 : positive -> Q => QCauchySeq x0 id) rnn limneg) + (k * (k * 1)))) ; simpl. remember (QCauchySeq_bound - (fun n0 : nat => / rnn (Pos.to_nat k * (Pos.to_nat k * 1) * n0)%nat)%Q - Pos.to_nat) as x. + (fun n0 : positive => / rnn (k * (k * 1) * n0)%positive)%Q + id) as x. remember (QCauchySeq_bound - (fun n0 : nat => rnn (Pos.to_nat k * (Pos.to_nat k * 1) * n0)%nat) - Pos.to_nat) as x0. - exists (fun n => 1%nat). intros p n m H2 H3. rewrite Qmult_comm. + (fun n0 : positive => rnn (k * (k * 1) * n0)%positive) + id) as x0. + exists (fun n => 1%positive). intros p n m H2 H3. rewrite Qmult_comm. rewrite Qmult_inv_r. unfold Qminus. rewrite Qplus_opp_r. reflexivity. intro abs. - specialize (maj (Pos.to_nat k * (Pos.to_nat k * 1) - * (Pos.to_nat (Pos.max x x0)~0 * n))%nat). - simpl in maj. rewrite abs in maj. inversion maj. + unfold snd,fst, proj1_sig in maj. + specialize (maj (k * (k * 1) * (Pos.max x x0 * n)~0)%positive). + rewrite abs in maj. inversion maj. - (* r > 0 *) destruct (CRealPosShift r c) as [[k rneg] [req maj]]. simpl in req. apply CRealEq_diff. apply CRealEq_modindep. apply (QSeqEquivEx_trans _ (proj1_sig (CReal_mult ((let (yn, cau) as s - return ((forall n : nat, 1 # k < proj1_sig s n) -> CReal) := rneg in - fun maj0 : forall n : nat, 1 # k < yn n => - exist (fun x : nat -> Q => QCauchySeq x Pos.to_nat) - (fun n : nat => Qinv (yn (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat)) + return ((forall n : positive, 1 # k < proj1_sig s n) -> CReal) := rneg in + fun maj0 : forall n : positive, 1 # k < yn n => + exist (fun x : positive -> Q => QCauchySeq x id) + (fun n : positive => Qinv (yn (k * (k * 1) * n)%positive)) (CReal_inv_pos yn k cau maj0)) maj) rneg)))%Q. + apply CRealEq_modindep. apply CRealEq_diff. apply CReal_mult_proper_l. apply req. @@ -1258,35 +1195,34 @@ Proof. apply (QSeqEquivEx_trans _ (proj1_sig (CReal_mult ((let (yn, cau) as s - return ((forall n : nat, 1 # k < proj1_sig s n) -> CReal) := rneg in - fun maj0 : forall n : nat, 1 # k < yn n => - exist (fun x : nat -> Q => QCauchySeq x Pos.to_nat) - (fun n : nat => Qinv (yn (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat)) + return ((forall n : positive, 1 # k < proj1_sig s n) -> CReal) := rneg in + fun maj0 : forall n : positive, 1 # k < yn n => + exist (fun x : positive -> Q => QCauchySeq x id) + (fun n : positive => Qinv (yn (k * (k * 1) * n)%positive)) (CReal_inv_pos yn k cau maj0)) maj) - (exist _ (fun n => proj1_sig rneg (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat) (CReal_linear_shift rneg _ H)))))%Q. + (exist _ (fun n => proj1_sig rneg (k * (k * 1) * n)%positive) (CReal_linear_shift rneg _)))))%Q. apply CRealEq_modindep. apply CRealEq_diff. apply CReal_mult_proper_l. apply CReal_linear_shift_eq. destruct r as [rn limr], rneg as [rnn limneg]; simpl. pose proof (QCauchySeq_bounded_prop - (fun n : nat => Qinv (rnn (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat)) - Pos.to_nat (CReal_inv_pos rnn k limneg maj)). + (fun n : positive => Qinv (rnn (k * (k * 1) * n)%positive)) + id (CReal_inv_pos rnn k limneg maj)). pose proof (QCauchySeq_bounded_prop - (fun n : nat => rnn (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat) - Pos.to_nat + (fun n : positive => rnn (k * (k * 1) * n)%positive) + id (CReal_linear_shift - (exist (fun x0 : nat -> Q => QCauchySeq x0 Pos.to_nat) rnn limneg) - (Pos.to_nat k * (Pos.to_nat k * 1)) H)) ; simpl. + (exist (fun x0 : positive -> Q => QCauchySeq x0 id) rnn limneg) + (k * (k * 1)))) ; simpl. remember (QCauchySeq_bound - (fun n0 : nat => / rnn (Pos.to_nat k * (Pos.to_nat k * 1) * n0)%nat) - Pos.to_nat)%Q as x. + (fun n0 : positive => / rnn (k * (k * 1) * n0)%positive) + id)%Q as x. remember (QCauchySeq_bound - (fun n0 : nat => rnn (Pos.to_nat k * (Pos.to_nat k * 1) * n0)%nat) - Pos.to_nat) as x0. - exists (fun n => 1%nat). intros p n m H2 H3. rewrite Qmult_comm. + (fun n0 : positive => rnn (k * (k * 1) * n0)%positive) + id) as x0. + exists (fun n => 1%positive). intros p n m H2 H3. rewrite Qmult_comm. rewrite Qmult_inv_r. unfold Qminus. rewrite Qplus_opp_r. reflexivity. intro abs. - specialize (maj (Pos.to_nat k * (Pos.to_nat k * 1) - * (Pos.to_nat (Pos.max x x0)~0 * n))%nat). + specialize (maj ((k * (k * 1) * (Pos.max x x0 * n)~0)%positive)). simpl in maj. rewrite abs in maj. inversion maj. Qed. @@ -1369,12 +1305,13 @@ Proof. apply CRealLt_above in c. destruct c as [i imaj]. simpl in imaj. apply CRealLt_above in c0. destruct c0 as [j jmaj]. simpl in jmaj. pose proof (CReal_abs_appart_zero y). - destruct x as [xn xcau], y as [yn ycau]. simpl in kmaj. - remember (QCauchySeq_bound xn Pos.to_nat) as a. - remember (QCauchySeq_bound yn Pos.to_nat) as b. - simpl in kmaj. simpl in imaj, jmaj. simpl in H0. + destruct x as [xn xcau], y as [yn ycau]. + unfold CReal_mult, proj1_sig in kmaj. + remember (QCauchySeq_bound xn id) as a. + remember (QCauchySeq_bound yn id) as b. + simpl in imaj, jmaj. simpl in H0. specialize (kmaj (Pos.max k (Pos.max i j)) (Pos.le_max_l _ _)). - destruct (H0 ((Pos.max a b)~0 * (Pos.max k (Pos.max i j)))%positive). + destruct (H0 (2*(Pos.max a b) * (Pos.max k (Pos.max i j)))%positive). - apply (Qlt_trans _ (2#k)). + unfold Qlt. rewrite <- Z.mul_lt_mono_pos_l. 2: reflexivity. unfold Qden. apply Pos2Z.pos_lt_pos. @@ -1385,11 +1322,8 @@ Proof. fold (2*Pos.max a b)%positive. rewrite Pos2Nat.inj_mul. apply Nat.lt_1_mul_pos. auto. apply Pos2Nat.is_pos. + apply (Qlt_le_trans _ _ _ kmaj). unfold Qminus. rewrite Qplus_0_r. - rewrite <- (Qmult_1_l (Qabs (yn (Pos.to_nat ((Pos.max a b)~0 * Pos.max k (Pos.max i j)))))). + rewrite <- (Qmult_1_l (Qabs (yn (2*(Pos.max a b) * Pos.max k (Pos.max i j))%positive))). apply (Qle_trans _ _ _ (Qle_Qabs _)). rewrite Qabs_Qmult. - replace (Pos.to_nat (Pos.max a b)~0 * Pos.to_nat (Pos.max k (Pos.max i j)))%nat - with (Pos.to_nat ((Pos.max a b)~0 * Pos.max k (Pos.max i j))). - 2: apply Pos2Nat.inj_mul. apply Qmult_le_compat_r. 2: apply Qabs_nonneg. apply Qabs_Qle_condition. split. apply Qlt_le_weak. apply Qlt_minus_iff, (Qlt_trans _ (2#j)). @@ -1398,18 +1332,14 @@ Proof. rewrite Pos.mul_1_l. apply (Pos.le_trans _ (Pos.max i j) _ (Pos.le_max_r _ _)). apply Pos.le_max_r. - apply Pos2Nat.inj_le. do 2 rewrite Pos2Nat.inj_mul. - rewrite <- Nat.mul_le_mono_pos_r. 2: apply Pos2Nat.is_pos. - apply Pos2Nat.is_pos. + rewrite <- Pos.mul_le_mono_r. discriminate. apply Qlt_le_weak. apply Qlt_minus_iff, (Qlt_trans _ (2#i)). reflexivity. apply imaj. apply (Pos.le_trans _ (1 * Pos.max k (Pos.max i j))). rewrite Pos.mul_1_l. apply (Pos.le_trans _ (Pos.max i j) _ (Pos.le_max_l _ _)). apply Pos.le_max_r. - apply Pos2Nat.inj_le. do 2 rewrite Pos2Nat.inj_mul. - rewrite <- Nat.mul_le_mono_pos_r. 2: apply Pos2Nat.is_pos. - apply Pos2Nat.is_pos. + rewrite <- Pos.mul_le_mono_r. discriminate. - left. apply (CReal_mult_lt_reg_r (exist _ yn ycau) _ _ c). rewrite CReal_mult_0_l. exact H. - right. apply (CReal_mult_lt_reg_r (CReal_opp (exist _ yn ycau))). @@ -1450,11 +1380,11 @@ Proof. (* Locate a and b at the index given by a<b, and pick the middle rational number. *) intros [p pmaj]. - exists ((proj1_sig a (Pos.to_nat p) + proj1_sig b (Pos.to_nat p)) * (1#2))%Q. + exists ((proj1_sig a p + proj1_sig b p) * (1#2))%Q. split. - apply (CReal_le_lt_trans _ _ _ (inject_Q_compare a p)). apply inject_Q_lt. apply (Qmult_lt_l _ _ 2). reflexivity. - apply (Qplus_lt_l _ _ (-2*proj1_sig a (Pos.to_nat p))). + apply (Qplus_lt_l _ _ (-2*proj1_sig a p)). field_simplify. field_simplify in pmaj. setoid_replace (-2#2)%Q with (-1)%Q. 2: reflexivity. setoid_replace (2*(1#p))%Q with (2#p)%Q. 2: reflexivity. @@ -1462,12 +1392,12 @@ Proof. - apply (CReal_plus_lt_reg_l (-b)). rewrite CReal_plus_opp_l. apply (CReal_plus_lt_reg_r - (-inject_Q ((proj1_sig a (Pos.to_nat p) + proj1_sig b (Pos.to_nat p)) * (1 # 2)))). + (-inject_Q ((proj1_sig a p + proj1_sig b p) * (1 # 2)))). rewrite CReal_plus_assoc, CReal_plus_opp_r, CReal_plus_0_r, CReal_plus_0_l. rewrite <- opp_inject_Q. apply (CReal_le_lt_trans _ _ _ (inject_Q_compare (-b) p)). apply inject_Q_lt. apply (Qmult_lt_l _ _ 2). reflexivity. - apply (Qplus_lt_l _ _ (2*proj1_sig b (Pos.to_nat p))). + apply (Qplus_lt_l _ _ (2*proj1_sig b p)). destruct b as [bn bcau]; simpl. simpl in pmaj. field_simplify. field_simplify in pmaj. setoid_replace (-2#2)%Q with (-1)%Q. 2: reflexivity. |