diff options
Diffstat (limited to 'theories/Reals/Cauchy/ConstructiveCauchyReals.v')
| -rw-r--r-- | theories/Reals/Cauchy/ConstructiveCauchyReals.v | 596 |
1 files changed, 255 insertions, 341 deletions
diff --git a/theories/Reals/Cauchy/ConstructiveCauchyReals.v b/theories/Reals/Cauchy/ConstructiveCauchyReals.v index 167f8d41c9..1a5335a573 100644 --- a/theories/Reals/Cauchy/ConstructiveCauchyReals.v +++ b/theories/Reals/Cauchy/ConstructiveCauchyReals.v @@ -33,20 +33,23 @@ Require CMorphisms. The double quantification on p q is needed to avoid forall un, QSeqEquiv un (fun _ => un O) (fun q => O) which says nothing about the limit of un. + + We define sequences as positive -> Q instead of nat -> Q, + so that we can compute arguments like 2^n fast. *) -Definition QSeqEquiv (un vn : nat -> Q) (cvmod : positive -> nat) +Definition QSeqEquiv (un vn : positive -> Q) (cvmod : positive -> positive) : Prop - := forall (k : positive) (p q : nat), - le (cvmod k) p - -> le (cvmod k) q + := forall (k : positive) (p q : positive), + Pos.le (cvmod k) p + -> Pos.le (cvmod k) q -> Qlt (Qabs (un p - vn q)) (1 # k). (* A Cauchy sequence is a sequence equivalent to itself. If sequences are equivalent, they are both Cauchy and have the same limit. *) -Definition QCauchySeq (un : nat -> Q) (cvmod : positive -> nat) : Prop +Definition QCauchySeq (un : positive -> Q) (cvmod : positive -> positive) : Prop := QSeqEquiv un un cvmod. -Lemma QSeqEquiv_sym : forall (un vn : nat -> Q) (cvmod : positive -> nat), +Lemma QSeqEquiv_sym : forall (un vn : positive -> Q) (cvmod : positive -> positive), QSeqEquiv un vn cvmod -> QSeqEquiv vn un cvmod. Proof. @@ -59,11 +62,12 @@ Proof. intros. unfold Qeq. simpl. destruct a; reflexivity. Qed. -Lemma QSeqEquiv_trans : forall (un vn wn : nat -> Q) - (cvmod cvmodw : positive -> nat), +Lemma QSeqEquiv_trans : forall (un vn wn : positive -> Q) + (cvmod cvmodw : positive -> positive), QSeqEquiv un vn cvmod -> QSeqEquiv vn wn cvmodw - -> QSeqEquiv un wn (fun q => max (cvmod (2 * q)%positive) (cvmodw (2 * q)%positive)). + -> QSeqEquiv un wn (fun q => Pos.max (cvmod (2 * q)%positive) + (cvmodw (2 * q)%positive)). Proof. intros. intros k p q H1 H2. setoid_replace (un p - wn q) with (un p - vn p + (vn p - wn q)). @@ -71,38 +75,42 @@ Proof. _ (Qabs (un p - vn p) + Qabs (vn p - wn q))). apply Qabs_triangle. apply (Qlt_le_trans _ ((1 # (2*k)) + (1 # (2*k)))). apply Qplus_lt_le_compat. - - assert ((cvmod (2 * k)%positive <= p)%nat). - { apply (le_trans _ (max (cvmod (2 * k)%positive) (cvmodw (2 * k)%positive))). - apply Nat.le_max_l. assumption. } + - assert ((cvmod (2 * k)%positive <= p)%positive). + { apply (Pos.le_trans _ (Pos.max (cvmod (2 * k)%positive) + (cvmodw (2 * k)%positive))). + apply Pos.le_max_l. assumption. } apply H. assumption. assumption. - apply Qle_lteq. left. apply H0. - apply (le_trans _ (max (cvmod (2 * k)%positive) (cvmodw (2 * k)%positive))). - apply Nat.le_max_r. assumption. - apply (le_trans _ (max (cvmod (2 * k)%positive) (cvmodw (2 * k)%positive))). - apply Nat.le_max_r. assumption. + apply (Pos.le_trans _ (Pos.max (cvmod (2 * k)%positive) + (cvmodw (2 * k)%positive))). + apply Pos.le_max_r. assumption. + apply (Pos.le_trans _ (Pos.max (cvmod (2 * k)%positive) + (cvmodw (2 * k)%positive))). + apply Pos.le_max_r. assumption. - rewrite (factorDenom _ _ 2). ring_simplify. apply Qle_refl. - ring. Qed. -Definition QSeqEquivEx (un vn : nat -> Q) : Prop - := exists (cvmod : positive -> nat), QSeqEquiv un vn cvmod. +Definition QSeqEquivEx (un vn : positive -> Q) : Prop + := exists (cvmod : positive -> positive), QSeqEquiv un vn cvmod. -Lemma QSeqEquivEx_sym : forall (un vn : nat -> Q), QSeqEquivEx un vn -> QSeqEquivEx vn un. +Lemma QSeqEquivEx_sym : forall (un vn : positive -> Q), + QSeqEquivEx un vn -> QSeqEquivEx vn un. Proof. intros. destruct H. exists x. apply QSeqEquiv_sym. apply H. Qed. -Lemma QSeqEquivEx_trans : forall un vn wn : nat -> Q, +Lemma QSeqEquivEx_trans : forall un vn wn : positive -> Q, QSeqEquivEx un vn -> QSeqEquivEx vn wn -> QSeqEquivEx un wn. Proof. intros. destruct H,H0. - exists (fun q => max (x (2 * q)%positive) (x0 (2 * q)%positive)). + exists (fun q => Pos.max (x (2 * q)%positive) (x0 (2 * q)%positive)). apply (QSeqEquiv_trans un vn wn); assumption. Qed. -Lemma QSeqEquiv_cau_r : forall (un vn : nat -> Q) (cvmod : positive -> nat), +Lemma QSeqEquiv_cau_r : forall (un vn : positive -> Q) (cvmod : positive -> positive), QSeqEquiv un vn cvmod -> QCauchySeq vn (fun k => cvmod (2 * k)%positive). Proof. @@ -118,82 +126,15 @@ Proof. apply Qabs_triangle. apply (Qlt_le_trans _ ((1 # (2 * k)) + (1 # (2 * k)))). apply Qplus_lt_le_compat. - + rewrite Qabs_Qminus. apply H. apply le_refl. assumption. - + apply Qle_lteq. left. apply H. apply le_refl. assumption. + + rewrite Qabs_Qminus. apply H. apply Pos.le_refl. assumption. + + apply Qle_lteq. left. apply H. apply Pos.le_refl. assumption. + rewrite (factorDenom _ _ 2). ring_simplify. apply Qle_refl. - ring. Qed. -Fixpoint increasing_modulus (modulus : positive -> nat) (n : nat) - := match n with - | O => modulus xH - | S p => max (modulus (Pos.of_nat n)) (increasing_modulus modulus p) - end. - -Lemma increasing_modulus_inc : forall (modulus : positive -> nat) (n p : nat), - le (increasing_modulus modulus n) - (increasing_modulus modulus (p + n)). -Proof. - induction p. - - apply le_refl. - - apply (le_trans _ (increasing_modulus modulus (p + n))). - apply IHp. simpl. destruct (plus p n). apply Nat.le_max_r. apply Nat.le_max_r. -Qed. - -Lemma increasing_modulus_max : forall (modulus : positive -> nat) (p n : nat), - le n p -> le (modulus (Pos.of_nat n)) - (increasing_modulus modulus p). -Proof. - induction p. - - intros. inversion H. subst n. apply le_refl. - - intros. simpl. destruct p. simpl. - + destruct n. apply Nat.le_max_l. apply le_S_n in H. - inversion H. apply Nat.le_max_l. - + apply Nat.le_succ_r in H. destruct H. - apply (le_trans _ (increasing_modulus modulus (S p))). - 2: apply Nat.le_max_r. apply IHp. apply H. - subst n. apply (le_trans _ (modulus (Pos.succ (Pos.of_nat (S p))))). - apply le_refl. apply Nat.le_max_l. -Qed. - -(* Choice of a standard element in each QSeqEquiv class. *) -Lemma standard_modulus : forall (un : nat -> Q) (cvmod : positive -> nat), - QCauchySeq un cvmod - -> (QCauchySeq (fun n => un (increasing_modulus cvmod n)) Pos.to_nat - /\ QSeqEquiv un (fun n => un (increasing_modulus cvmod n)) - (fun p => max (cvmod p) (Pos.to_nat p))). -Proof. - intros. split. - - intros k p q H0 H1. apply H. - + apply (le_trans _ (increasing_modulus cvmod (Pos.to_nat k))). - apply (le_trans _ (cvmod (Pos.of_nat (Pos.to_nat k)))). - rewrite Pos2Nat.id. apply le_refl. - destruct (Pos.to_nat k). apply le_refl. apply Nat.le_max_l. - destruct (Nat.le_exists_sub (Pos.to_nat k) p H0) as [i [H2 H3]]. subst p. - apply increasing_modulus_inc. - + apply (le_trans _ (increasing_modulus cvmod (Pos.to_nat k))). - apply (le_trans _ (cvmod (Pos.of_nat (Pos.to_nat k)))). - rewrite Pos2Nat.id. apply le_refl. - destruct (Pos.to_nat k). apply le_refl. apply Nat.le_max_l. - destruct (Nat.le_exists_sub (Pos.to_nat k) q H1) as [i [H2 H3]]. subst q. - apply increasing_modulus_inc. - - intros k p q H0 H1. apply H. - + apply (le_trans _ (Init.Nat.max (cvmod k) (Pos.to_nat k))). - apply Nat.le_max_l. assumption. - + apply (le_trans _ (increasing_modulus cvmod (Pos.to_nat k))). - apply (le_trans _ (cvmod (Pos.of_nat (Pos.to_nat k)))). - rewrite Pos2Nat.id. apply le_refl. - destruct (Pos.to_nat k). apply le_refl. apply Nat.le_max_l. - assert (le (Pos.to_nat k) q). - { apply (le_trans _ (Init.Nat.max (cvmod k) (Pos.to_nat k))). - apply Nat.le_max_r. assumption. } - destruct (Nat.le_exists_sub (Pos.to_nat k) q H2) as [i [H3 H4]]. subst q. - apply increasing_modulus_inc. -Qed. - (* A Cauchy real is a Cauchy sequence with the standard modulus *) Definition CReal : Set - := { x : (nat -> Q) | QCauchySeq x Pos.to_nat }. + := { x : (positive -> Q) | QCauchySeq x id }. Declare Scope CReal_scope. @@ -208,12 +149,10 @@ Local Open Scope CReal_scope. (* So QSeqEquiv is the equivalence relation of this constructive pre-order *) Definition CRealLt (x y : CReal) : Set - := { n : positive | Qlt (2 # n) - (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n)) }. + := { n : positive | Qlt (2 # n) (proj1_sig y n - proj1_sig x n) }. Definition CRealLtProp (x y : CReal) : Prop - := exists n : positive, Qlt (2 # n) - (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n)). + := exists n : positive, Qlt (2 # n) (proj1_sig y n - proj1_sig x n). Definition CRealGt (x y : CReal) := CRealLt y x. Definition CReal_appart (x y : CReal) := sum (CRealLt x y) (CRealLt y x). @@ -226,23 +165,23 @@ Infix "#" := CReal_appart : CReal_scope. Lemma CRealLtEpsilon : forall x y : CReal, CRealLtProp x y -> x < y. Proof. - intros. - assert (exists n : nat, n <> O - /\ Qlt (2 # Pos.of_nat n) (proj1_sig y n - proj1_sig x n)). - { destruct H as [n maj]. exists (Pos.to_nat n). split. - intro abs. destruct (Pos2Nat.is_succ n). rewrite H in abs. - inversion abs. rewrite Pos2Nat.id. apply maj. } + intros. unfold CRealLtProp in H. + (* Convert to nat to use indefinite description. *) + assert (exists n : nat, lt O n /\ Qlt (2 # Pos.of_nat n) + (proj1_sig y (Pos.of_nat n) - proj1_sig x (Pos.of_nat n))). + { destruct H as [n maj]. exists (Pos.to_nat n). split. apply Pos2Nat.is_pos. + rewrite Pos2Nat.id. exact maj. } + clear H. apply constructive_indefinite_ground_description_nat in H0. - destruct H0 as [n maj]. exists (Pos.of_nat n). - rewrite Nat2Pos.id. apply maj. apply maj. + destruct H0 as [n maj]. exists (Pos.of_nat n). exact (proj2 maj). intro n. destruct n. right. - intros [abs _]. exact (abs (eq_refl O)). + intros [abs _]. inversion abs. destruct (Qlt_le_dec (2 # Pos.of_nat (S n)) - (proj1_sig y (S n) - proj1_sig x (S n))). - left. split. discriminate. apply q. + (proj1_sig y (Pos.of_nat (S n)) - proj1_sig x (Pos.of_nat (S n)))). + left. split. apply le_n_S, le_0_n. apply q. right. intros [_ abs]. apply (Qlt_not_le (2 # Pos.of_nat (S n)) - (proj1_sig y (S n) - proj1_sig x (S n))); assumption. + (proj1_sig y (Pos.of_nat (S n)) - proj1_sig x (Pos.of_nat (S n)))); assumption. Qed. Lemma CRealLtForget : forall x y : CReal, @@ -254,18 +193,18 @@ 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}) + (forall (P : nat -> Prop), (forall n:nat, {P n} + {~P n}) -> {n | ~P n} + {forall n, P n}) -> CRealLt x y + (CRealLt x y -> False). Proof. intros x y lpo. - destruct (lpo (fun n:nat => Qle (proj1_sig y (S n) - proj1_sig x (S n)) + destruct (lpo (fun n:nat => Qle (proj1_sig y (Pos.of_nat (S n)) - proj1_sig x (Pos.of_nat (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))). + (proj1_sig y (Pos.of_nat (S n)) - proj1_sig x (Pos.of_nat (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. + apply Qnot_le_lt. exact nmaj. - 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. @@ -296,41 +235,37 @@ Definition CRealEq (x y : CReal) : Prop Infix "==" := CRealEq : CReal_scope. Lemma CRealLe_not_lt : forall x y : CReal, - (forall n:positive, Qle (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n)) - (2 # n)) + (forall n:positive, Qle (proj1_sig x n - proj1_sig y n) (2 # n)) <-> x <= y. Proof. intros. split. - intros. intro H0. destruct H0 as [n H0]. specialize (H n). apply (Qle_not_lt (2 # n) (2 # n)). apply Qle_refl. - apply (Qlt_le_trans _ (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n))). + apply (Qlt_le_trans _ (proj1_sig x n - proj1_sig y n)). assumption. assumption. - intros. - destruct (Qlt_le_dec (2 # n) (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n))). + destruct (Qlt_le_dec (2 # n) (proj1_sig x n - proj1_sig y n)). exfalso. apply H. exists n. assumption. assumption. Qed. Lemma CRealEq_diff : forall (x y : CReal), CRealEq x y - <-> forall n:positive, Qle (Qabs (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n))) - (2 # n). + <-> forall n:positive, Qle (Qabs (proj1_sig x n - proj1_sig y n)) (2 # n). Proof. intros. split. - intros. destruct H. apply Qabs_case. intro. pose proof (CRealLe_not_lt x y) as [_ H2]. apply H2. assumption. intro. pose proof (CRealLe_not_lt y x) as [_ H2]. - setoid_replace (- (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n))) - with (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n)). + setoid_replace (- (proj1_sig x n - proj1_sig y n)) + with (proj1_sig y n - proj1_sig x n). apply H2. assumption. ring. - intros. split. + apply CRealLe_not_lt. intro n. specialize (H n). rewrite Qabs_Qminus in H. - apply (Qle_trans _ (Qabs (proj1_sig y (Pos.to_nat n) - - proj1_sig x (Pos.to_nat n)))). + apply (Qle_trans _ (Qabs (proj1_sig y n - proj1_sig x n))). apply Qle_Qabs. apply H. + apply CRealLe_not_lt. intro n. specialize (H n). - apply (Qle_trans _ (Qabs (proj1_sig x (Pos.to_nat n) - - proj1_sig y (Pos.to_nat n)))). + apply (Qle_trans _ (Qabs (proj1_sig x n - proj1_sig y n))). apply Qle_Qabs. apply H. Qed. @@ -339,111 +274,106 @@ Qed. 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). + Qle (Qabs (proj1_sig x n - proj1_sig y 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. + pose (xn n - yn 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. } + remember (Pos.max (cvmod k) n) as p. + assert (Pos.le (cvmod k) p). + { rewrite Heqp. apply Pos.le_max_l. } + assert (n <= p)%positive. + { rewrite Heqp. apply Pos.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)))). + setoid_replace (xn n + -1 * yn n) + with (xn n - xn p + (xn p - yn p + (yn p - yn 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. + apply Qlt_le_weak. apply limx. apply Pos.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. + assumption. apply Pos.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. + exists (fun q:positive => 2 * (3 * q))%positive. 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. } + assert (3 * k <= 2 * (3 * k))%positive. + { generalize (3 * k)%positive. intros. apply (Pos.le_trans _ (1 * p0)). + apply Pos.le_refl. rewrite <- Pos.mul_le_mono_r. discriminate. } 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))). + with (xn p - xn (2 * (3 * k))%positive + + (xn (2 * (3 * k))%positive - yn (2 * (3 * k))%positive + + (yn (2 * (3 * k))%positive - yn q))). + 2: ring. 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))))). + _ (Qabs (xn p - xn (2 * (3 * k))%positive) + + (Qabs (xn (2 * (3 * k))%positive - yn (2 * (3 * k))%positive + + (yn (2 * (3 * k))%positive - yn q))))). apply Qabs_triangle. apply Qplus_lt_le_compat. - apply limx. apply (le_trans _ (Pos.to_nat (2 * (3 * k)))). assumption. assumption. + apply limx. apply (Pos.le_trans _ (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))). + _ (Qabs (xn (2 * (3 * k))%positive - yn (2 * (3 * k))%positive) + + Qabs (yn (2 * (3 * k))%positive - 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 (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. + apply (Pos.le_trans _ (2 * (3 * k))). assumption. assumption. + rewrite (factorDenom _ _ 3). ring_simplify. reflexivity. Qed. (* Extend separation to all indices above *) Lemma CRealLt_aboveSig : forall (x y : CReal) (n : positive), (Qlt (2 # n) - (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n))) - -> let (k, _) := Qarchimedean (/(proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n) - (2#n))) + (proj1_sig y n - proj1_sig x n)) + -> let (k, _) := Qarchimedean (/(proj1_sig y n - proj1_sig x n - (2#n))) in forall p:positive, Pos.le (Pos.max n (2*k)) p -> Qlt (2 # (Pos.max n (2*k))) - (proj1_sig y (Pos.to_nat p) - proj1_sig x (Pos.to_nat p)). + (proj1_sig y p - proj1_sig x p). Proof. intros [xn limx] [yn limy] n maj. unfold proj1_sig; unfold proj1_sig in maj. - pose (yn (Pos.to_nat n) - xn (Pos.to_nat n)) as dn. - destruct (Qarchimedean (/(yn (Pos.to_nat n) - xn (Pos.to_nat n) - (2#n)))) as [k kmaj]. - assert (0 < yn (Pos.to_nat n) - xn (Pos.to_nat n) - (2 # n))%Q as H0. + pose (yn n - xn n) as dn. + destruct (Qarchimedean (/(yn n - xn n - (2#n)))) as [k kmaj]. + assert (0 < yn n - xn n - (2 # n))%Q as H0. { rewrite <- (Qplus_opp_r (2#n)). apply Qplus_lt_l. assumption. } - intros. - remember (yn (Pos.to_nat p) - xn (Pos.to_nat p)) as dp. - + intros. remember (yn p - xn p) as dp. rewrite <- (Qplus_0_r dp). rewrite <- (Qplus_opp_r dn). rewrite (Qplus_comm dn). rewrite Qplus_assoc. assert (Qlt (Qabs (dp - dn)) (2#n)). { rewrite Heqdp. unfold dn. - setoid_replace (yn (Pos.to_nat p) - xn (Pos.to_nat p) - (yn (Pos.to_nat n) - xn (Pos.to_nat n))) - with (yn (Pos.to_nat p) - yn (Pos.to_nat n) - + (xn (Pos.to_nat n) - xn (Pos.to_nat p))). - apply (Qle_lt_trans _ (Qabs (yn (Pos.to_nat p) - yn (Pos.to_nat n)) - + Qabs (xn (Pos.to_nat n) - xn (Pos.to_nat p)))). + setoid_replace (yn p - xn p - (yn n - xn n)) + with (yn p - yn n + (xn n - xn p)). + apply (Qle_lt_trans _ (Qabs (yn p - yn n) + Qabs (xn n - xn p))). apply Qabs_triangle. setoid_replace (2#n)%Q with ((1#n) + (1#n))%Q. apply Qplus_lt_le_compat. apply limy. - apply Pos2Nat.inj_le. apply (Pos.le_trans _ (Pos.max n (2 * k))). + apply (Pos.le_trans _ (Pos.max n (2 * k))). apply Pos.le_max_l. assumption. - apply le_refl. apply Qlt_le_weak. apply limx. apply le_refl. - apply Pos2Nat.inj_le. apply (Pos.le_trans _ (Pos.max n (2 * k))). + apply Pos.le_refl. apply Qlt_le_weak. apply limx. apply Pos.le_refl. + apply (Pos.le_trans _ (Pos.max n (2 * k))). apply Pos.le_max_l. assumption. - rewrite Qinv_plus_distr. reflexivity. field. } + rewrite Qinv_plus_distr. reflexivity. ring. } apply (Qle_lt_trans _ (-(2#n) + dn)). rewrite Qplus_comm. unfold dn. apply Qlt_le_weak. apply (Qle_lt_trans _ (2 # (2 * k))). apply Pos.le_max_r. @@ -463,12 +393,11 @@ Qed. Lemma CRealLt_above : forall (x y : CReal), CRealLt x y -> { k : positive | forall p:positive, - Pos.le k p -> Qlt (2 # k) (proj1_sig y (Pos.to_nat p) - - proj1_sig x (Pos.to_nat p)) }. + Pos.le k p -> Qlt (2 # k) (proj1_sig y p - proj1_sig x p) }. Proof. intros x y [n maj]. pose proof (CRealLt_aboveSig x y n maj). - destruct (Qarchimedean (/ (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n) - (2 # n)))) + destruct (Qarchimedean (/ (proj1_sig y n - proj1_sig x n - (2 # n)))) as [k kmaj]. exists (Pos.max n (2*k)). apply H. Qed. @@ -476,28 +405,26 @@ Qed. (* The CRealLt index separates the Cauchy sequences *) Lemma CRealLt_above_same : forall (x y : CReal) (n : positive), Qlt (2 # n) - (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n)) - -> forall p:positive, Pos.le n p - -> Qlt (proj1_sig x (Pos.to_nat p)) (proj1_sig y (Pos.to_nat p)). + (proj1_sig y n - proj1_sig x n) + -> forall p:positive, Pos.le n p -> Qlt (proj1_sig x p) (proj1_sig y p). Proof. intros [xn limx] [yn limy] n inf p H. simpl. simpl in inf. - apply (Qplus_lt_l _ _ (- xn (Pos.to_nat n))). - apply (Qle_lt_trans _ (Qabs (xn (Pos.to_nat p) + - xn (Pos.to_nat n)))). + apply (Qplus_lt_l _ _ (- xn n)). + apply (Qle_lt_trans _ (Qabs (xn p + - xn n))). apply Qle_Qabs. apply (Qlt_trans _ (1#n)). - apply limx. apply Pos2Nat.inj_le. assumption. apply le_refl. - rewrite <- (Qplus_0_r (yn (Pos.to_nat p))). - rewrite <- (Qplus_opp_r (yn (Pos.to_nat n))). - rewrite (Qplus_comm (yn (Pos.to_nat n))). rewrite Qplus_assoc. + apply limx. exact H. apply Pos.le_refl. + rewrite <- (Qplus_0_r (yn p)). + rewrite <- (Qplus_opp_r (yn n)). + rewrite (Qplus_comm (yn n)). rewrite Qplus_assoc. rewrite <- Qplus_assoc. setoid_replace (1#n)%Q with (-(1#n) + (2#n))%Q. 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 p))). + apply (Qplus_lt_r _ _ (yn n + - yn p)). ring_simplify. - setoid_replace (yn (Pos.to_nat n) + (-1 # 1) * yn (Pos.to_nat p)) - with (yn (Pos.to_nat n) - yn (Pos.to_nat p)). - apply (Qle_lt_trans _ (Qabs (yn (Pos.to_nat n) - yn (Pos.to_nat p)))). - apply Qle_Qabs. apply limy. apply le_refl. apply Pos2Nat.inj_le. assumption. + setoid_replace (yn n + (-1 # 1) * yn p) with (yn n - yn p). + apply (Qle_lt_trans _ (Qabs (yn n - yn p))). + apply Qle_Qabs. apply limy. apply Pos.le_refl. assumption. field. apply Qle_lteq. left. assumption. rewrite Qplus_comm. rewrite Qinv_minus_distr. reflexivity. @@ -508,10 +435,10 @@ 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). - 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 (Qlt_not_le (proj1_sig y (Pos.max n p)) + (proj1_sig x (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)))). + apply Qlt_le_weak. apply (Qplus_lt_l _ _ (-proj1_sig x (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. @@ -542,31 +469,24 @@ Lemma CRealLt_dec : forall x y z : CReal, Proof. intros [xn limx] [yn limy] [zn limz] [n inf]. unfold proj1_sig in inf. - remember (yn (Pos.to_nat n) - xn (Pos.to_nat n) - (2 # n)) as eps. + remember (yn n - xn n - (2 # n)) as eps. assert (Qlt 0 eps) as epsPos. { subst eps. unfold Qminus. apply (Qlt_minus_iff (2#n)). assumption. } - assert (forall n p, Pos.to_nat n <= Pos.to_nat (Pos.max n p))%nat. - { intros. apply Pos2Nat.inj_le. unfold Pos.max. unfold Pos.le. - destruct (n0 ?= p)%positive eqn:des. - rewrite des. discriminate. rewrite des. discriminate. - unfold Pos.compare. rewrite Pos.compare_cont_refl. discriminate. } destruct (Qarchimedean (/eps)) as [k kmaj]. - destruct (Qlt_le_dec ((yn (Pos.to_nat n) + xn (Pos.to_nat n)) / (2#1)) - (zn (Pos.to_nat (Pos.max n (4 * k))))) + destruct (Qlt_le_dec ((yn n + xn n) / (2#1)) + (zn (Pos.max n (4 * k)))) as [decMiddle|decMiddle]. - left. exists (Pos.max n (4 * k)). unfold proj1_sig. unfold Qminus. - rewrite <- (Qplus_0_r (zn (Pos.to_nat (Pos.max n (4 * k))))). - rewrite <- (Qplus_opp_r (xn (Pos.to_nat n))). - rewrite (Qplus_comm (xn (Pos.to_nat n))). rewrite Qplus_assoc. + rewrite <- (Qplus_0_r (zn (Pos.max n (4 * k)))). + rewrite <- (Qplus_opp_r (xn n)). + rewrite (Qplus_comm (xn n)). rewrite Qplus_assoc. rewrite <- Qplus_assoc. rewrite <- Qplus_0_r. rewrite <- (Qplus_opp_r (1#n)). rewrite Qplus_assoc. apply Qplus_lt_le_compat. - + apply (Qplus_lt_l _ _ (- xn (Pos.to_nat n))) in decMiddle. - apply (Qlt_trans _ ((yn (Pos.to_nat n) + xn (Pos.to_nat n)) / (2 # 1) - + - xn (Pos.to_nat n))). - setoid_replace ((yn (Pos.to_nat n) + xn (Pos.to_nat n)) / (2 # 1) - - xn (Pos.to_nat n)) - with ((yn (Pos.to_nat n) - xn (Pos.to_nat n)) / (2 # 1)). + + apply (Qplus_lt_l _ _ (- xn n)) in decMiddle. + apply (Qlt_trans _ ((yn n + xn n) / (2 # 1) + - xn n)). + setoid_replace ((yn n + xn n) / (2 # 1) - xn n) + with ((yn n - xn n) / (2 # 1)). apply Qlt_shift_div_l. unfold Qlt. simpl. unfold Z.lt. auto. rewrite Qmult_plus_distr_l. setoid_replace ((1 # n) * (2 # 1))%Q with (2#n)%Q. @@ -580,31 +500,30 @@ Proof. apply Qinv_lt_contravar. reflexivity. apply epsPos. apply kmaj. unfold Qeq. simpl. rewrite Pos.mul_1_r. reflexivity. field. assumption. - + setoid_replace (xn (Pos.to_nat n) + - xn (Pos.to_nat (Pos.max n (4 * k)))) - with (-(xn (Pos.to_nat (Pos.max n (4 * k))) - xn (Pos.to_nat n))). + + setoid_replace (xn n + - xn (Pos.max n (4 * k))) + with (-(xn (Pos.max n (4 * k)) - xn n)). apply Qopp_le_compat. - apply (Qle_trans _ (Qabs (xn (Pos.to_nat (Pos.max n (4 * k))) - xn (Pos.to_nat n)))). - apply Qle_Qabs. apply Qle_lteq. left. apply limx. apply H. - apply le_refl. field. + apply (Qle_trans _ (Qabs (xn (Pos.max n (4 * k)) - xn n))). + apply Qle_Qabs. apply Qle_lteq. left. apply limx. apply Pos.le_max_l. + apply Pos.le_refl. ring. - right. exists (Pos.max n (4 * k)). unfold proj1_sig. unfold Qminus. - rewrite <- (Qplus_0_r (yn (Pos.to_nat (Pos.max n (4 * k))))). - rewrite <- (Qplus_opp_r (yn (Pos.to_nat n))). - rewrite (Qplus_comm (yn (Pos.to_nat n))). rewrite Qplus_assoc. + rewrite <- (Qplus_0_r (yn (Pos.max n (4 * k)))). + rewrite <- (Qplus_opp_r (yn n)). + rewrite (Qplus_comm (yn n)). rewrite Qplus_assoc. 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_r _ _ (yn (Pos.to_nat n) - yn (Pos.to_nat (Pos.max n (4 * k))) + (1#n))) + + apply (Qplus_lt_r _ _ (yn n - yn (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. + setoid_replace (-1 * yn (Pos.max n (4 * k))) + with (- yn (Pos.max n (4 * k))). 2: ring. + apply (Qle_lt_trans _ (Qabs (yn n - yn (Pos.max n (4 * k))))). + apply Qle_Qabs. apply limy. apply Pos.le_refl. apply Pos.le_max_l. + apply Qopp_le_compat in decMiddle. - apply (Qplus_le_r _ _ (yn (Pos.to_nat n))) in decMiddle. - apply (Qle_trans _ (yn (Pos.to_nat n) + - ((yn (Pos.to_nat n) + xn (Pos.to_nat n)) / (2 # 1)))). - setoid_replace (yn (Pos.to_nat n) + - ((yn (Pos.to_nat n) + xn (Pos.to_nat n)) / (2 # 1))) - with ((yn (Pos.to_nat n) - xn (Pos.to_nat n)) / (2 # 1)). + apply (Qplus_le_r _ _ (yn n)) in decMiddle. + apply (Qle_trans _ (yn n + - ((yn n + xn n) / (2 # 1)))). + setoid_replace (yn n + - ((yn n + xn n) / (2 # 1))) + with ((yn n - xn n) / (2 # 1)). apply Qle_shift_div_l. unfold Qlt. simpl. unfold Z.lt. auto. rewrite Qmult_plus_distr_l. setoid_replace ((1 # n) * (2 # 1))%Q with (2#n)%Q. @@ -766,7 +685,7 @@ Qed. (* Injection of Q into CReal *) Lemma ConstCauchy : forall q : Q, - QCauchySeq (fun _ => q) Pos.to_nat. + QCauchySeq (fun _ => q) id. Proof. intros. intros k p r H H0. unfold Qminus. rewrite Qplus_opp_r. unfold Qlt. simpl. @@ -811,64 +730,64 @@ Qed. by a factor 2. *) Lemma CRealLtQ : forall (x : CReal) (q : Q), CRealLt x (inject_Q q) - -> forall p:positive, Qlt (proj1_sig x (Pos.to_nat p)) (q + (1#p)). + -> forall p:positive, Qlt (proj1_sig x p) (q + (1#p)). Proof. intros [xn cau] q maj p. simpl. - destruct (Qlt_le_dec (xn (Pos.to_nat p)) (q + (1 # p))). assumption. + destruct (Qlt_le_dec (xn p) (q + (1 # p))). assumption. exfalso. apply CRealLt_above in maj. destruct maj as [k maj]; simpl in maj. specialize (maj (Pos.max k p) (Pos.le_max_l _ _)). - specialize (cau p (Pos.to_nat p) (Pos.to_nat (Pos.max k p)) (le_refl _)). - pose proof (Qplus_lt_le_compat (2#k) (q - xn (Pos.to_nat (Pos.max k p))) - (q + (1 # p)) (xn (Pos.to_nat p)) maj q0). + specialize (cau p p (Pos.max k p) (Pos.le_refl _)). + pose proof (Qplus_lt_le_compat (2#k) (q - xn (Pos.max k p)) + (q + (1 # p)) (xn p) maj q0). rewrite Qplus_comm in H. unfold Qminus in H. rewrite <- Qplus_assoc in H. rewrite <- Qplus_assoc in H. apply Qplus_lt_r in H. - rewrite <- (Qplus_lt_r _ _ (xn (Pos.to_nat p))) in maj. + rewrite <- (Qplus_lt_r _ _ (xn p)) in maj. apply (Qlt_not_le (1#p) ((1 # p) + (2 # k))). rewrite <- (Qplus_0_r (1#p)). rewrite <- Qplus_assoc. apply Qplus_lt_r. reflexivity. apply Qlt_le_weak. - apply (Qlt_trans _ (- xn (Pos.to_nat (Pos.max k p)) + xn (Pos.to_nat p)) _ H). + apply (Qlt_trans _ (- xn (Pos.max k p) + xn p) _ H). rewrite Qplus_comm. - apply (Qle_lt_trans _ (Qabs (xn (Pos.to_nat p) - xn (Pos.to_nat (Pos.max k p))))). - apply Qle_Qabs. apply cau. apply Pos2Nat.inj_le. apply Pos.le_max_r. + apply (Qle_lt_trans _ (Qabs (xn p - xn (Pos.max k p)))). + apply Qle_Qabs. apply cau. apply Pos.le_max_r. Qed. Lemma CRealLtQopp : forall (x : CReal) (q : Q), CRealLt (inject_Q q) x - -> forall p:positive, Qlt (q - (1#p)) (proj1_sig x (Pos.to_nat p)). + -> forall p:positive, Qlt (q - (1#p)) (proj1_sig x p). Proof. intros [xn cau] q maj p. simpl. - destruct (Qlt_le_dec (q - (1 # p)) (xn (Pos.to_nat p))). assumption. + destruct (Qlt_le_dec (q - (1 # p)) (xn p)). assumption. exfalso. apply CRealLt_above in maj. destruct maj as [k maj]; simpl in maj. specialize (maj (Pos.max k p) (Pos.le_max_l _ _)). - specialize (cau p (Pos.to_nat (Pos.max k p)) (Pos.to_nat p)). - pose proof (Qplus_lt_le_compat (2#k) (xn (Pos.to_nat (Pos.max k p)) - q) - (xn (Pos.to_nat p)) (q - (1 # p)) maj q0). + specialize (cau p (Pos.max k p) p). + pose proof (Qplus_lt_le_compat (2#k) (xn (Pos.max k p) - q) + (xn p) (q - (1 # p)) maj q0). unfold Qminus in H. rewrite <- Qplus_assoc in H. rewrite (Qplus_assoc (-q)) in H. rewrite (Qplus_comm (-q)) in H. rewrite Qplus_opp_r in H. rewrite Qplus_0_l in H. apply (Qplus_lt_l _ _ (1#p)) in H. - rewrite <- (Qplus_assoc (xn (Pos.to_nat (Pos.max k p)))) in H. + rewrite <- (Qplus_assoc (xn (Pos.max k p))) in H. rewrite (Qplus_comm (-(1#p))) in H. rewrite Qplus_opp_r in H. rewrite Qplus_0_r in H. rewrite Qplus_comm in H. - rewrite Qplus_assoc in H. apply (Qplus_lt_l _ _ (- xn (Pos.to_nat p))) in H. + rewrite Qplus_assoc in H. apply (Qplus_lt_l _ _ (- xn p)) in H. rewrite <- Qplus_assoc in H. rewrite Qplus_opp_r in H. rewrite Qplus_0_r in H. apply (Qlt_not_le (1#p) ((1 # p) + (2 # k))). rewrite <- (Qplus_0_r (1#p)). rewrite <- Qplus_assoc. apply Qplus_lt_r. reflexivity. apply Qlt_le_weak. - apply (Qlt_trans _ (xn (Pos.to_nat (Pos.max k p)) - xn (Pos.to_nat p)) _ H). - apply (Qle_lt_trans _ (Qabs (xn (Pos.to_nat (Pos.max k p)) - xn (Pos.to_nat p)))). - apply Qle_Qabs. apply cau. apply Pos2Nat.inj_le. - apply Pos.le_max_r. apply le_refl. + apply (Qlt_trans _ (xn (Pos.max k p) - xn p) _ H). + apply (Qle_lt_trans _ (Qabs (xn (Pos.max k p) - xn p))). + apply Qle_Qabs. apply cau. + apply Pos.le_max_r. apply Pos.le_refl. Qed. Lemma inject_Q_compare : forall (x : CReal) (p : positive), - x <= inject_Q (proj1_sig x (Pos.to_nat p) + (1#p)). + x <= inject_Q (proj1_sig x p + (1#p)). Proof. intros. intros [n nmaj]. destruct x as [xn xcau]; simpl in nmaj. @@ -876,18 +795,17 @@ Proof. ring_simplify in nmaj. destruct (Pos.max_dec p n). - apply Pos.max_l_iff in e. - apply Pos2Nat.inj_le in e. - specialize (xcau n (Pos.to_nat n) (Pos.to_nat p) (le_refl _) e). - apply (Qlt_le_trans _ _ (Qabs (xn (Pos.to_nat n) + -1 * xn (Pos.to_nat p)))) in nmaj. + specialize (xcau n n p (Pos.le_refl _) e). + apply (Qlt_le_trans _ _ (Qabs (xn n + -1 * xn p))) in nmaj. 2: apply Qle_Qabs. apply (Qlt_trans _ _ _ nmaj) in xcau. apply (Qplus_lt_l _ _ (-(1#n)-(1#p))) in xcau. ring_simplify in xcau. setoid_replace ((2 # n) + -1 * (1 # n)) with (1#n)%Q in xcau. discriminate xcau. setoid_replace (-1 * (1 # n)) with (-1#n)%Q. 2: reflexivity. rewrite Qinv_plus_distr. reflexivity. - - apply Pos.max_r_iff, Pos2Nat.inj_le in e. - specialize (xcau p (Pos.to_nat n) (Pos.to_nat p) e (le_refl _)). - apply (Qlt_le_trans _ _ (Qabs (xn (Pos.to_nat n) + -1 * xn (Pos.to_nat p)))) in nmaj. + - apply Pos.max_r_iff in e. + specialize (xcau p n p e (Pos.le_refl _)). + apply (Qlt_le_trans _ _ (Qabs (xn n + -1 * xn p))) in nmaj. 2: apply Qle_Qabs. apply (Qlt_trans _ _ _ nmaj) in xcau. apply (Qplus_lt_l _ _ (-(1#p))) in xcau. ring_simplify in xcau. discriminate. @@ -921,12 +839,12 @@ Qed. (* Algebraic operations *) Lemma CReal_plus_cauchy - : forall (xn yn zn : nat -> Q) (cvmod : positive -> nat), + : forall (xn yn zn : positive -> Q) (cvmod : positive -> positive), QSeqEquiv xn yn cvmod - -> QCauchySeq zn Pos.to_nat - -> QSeqEquiv (fun n:nat => xn n + zn n) (fun n:nat => yn n + zn n) - (fun p => max (cvmod (2 * p)%positive) - (Pos.to_nat (2 * p)%positive)). + -> QCauchySeq zn id + -> QSeqEquiv (fun n:positive => xn n + zn n) (fun n:positive => yn n + zn n) + (fun p => Pos.max (cvmod (2 * p)%positive) + (2 * p)%positive). Proof. intros. intros p n k H1 H2. setoid_replace (xn n + zn n - (yn k + zn k)) @@ -936,70 +854,67 @@ Proof. apply Qabs_triangle. setoid_replace (1#p)%Q with ((1#2*p) + (1#2*p))%Q. apply Qplus_lt_le_compat. - - apply H. apply (le_trans _ (Init.Nat.max (cvmod (2 * p)%positive) (Pos.to_nat (2 * p)))). - apply Nat.le_max_l. apply H1. - apply (le_trans _ (Init.Nat.max (cvmod (2 * p)%positive) (Pos.to_nat (2 * p)))). - apply Nat.le_max_l. apply H2. + - apply H. apply (Pos.le_trans _ (Pos.max (cvmod (2 * p)%positive) (2 * p))). + apply Pos.le_max_l. apply H1. + apply (Pos.le_trans _ (Pos.max (cvmod (2 * p)%positive) (2 * p))). + apply Pos.le_max_l. apply H2. - apply Qle_lteq. left. apply H0. - apply (le_trans _ (Init.Nat.max (cvmod (2 * p)%positive) (Pos.to_nat (2 * p)))). - apply Nat.le_max_r. apply H1. - apply (le_trans _ (Init.Nat.max (cvmod (2 * p)%positive) (Pos.to_nat (2 * p)))). - apply Nat.le_max_r. apply H2. + apply (Pos.le_trans _ (Pos.max (cvmod (2 * p)%positive) (2 * p))). + apply Pos.le_max_r. apply H1. + apply (Pos.le_trans _ (Pos.max (cvmod (2 * p)%positive) (2 * p))). + apply Pos.le_max_r. apply H2. - rewrite Qinv_plus_distr. unfold Qeq. reflexivity. Qed. Definition CReal_plus (x y : CReal) : CReal. Proof. destruct x as [xn limx], y as [yn limy]. - pose proof (CReal_plus_cauchy xn xn yn Pos.to_nat limx limy). - exists (fun n : nat => xn (2 * n)%nat + yn (2 * n)%nat). + pose proof (CReal_plus_cauchy xn xn yn id limx limy). + exists (fun n : positive => xn (2 * n)%positive + yn (2 * n)%positive). intros p k n H0 H1. apply H. - - rewrite max_l. rewrite Pos2Nat.inj_mul. - apply Nat.mul_le_mono_nonneg. apply le_0_n. apply le_refl. - apply le_0_n. apply H0. apply le_refl. - - rewrite Pos2Nat.inj_mul. rewrite max_l. - apply Nat.mul_le_mono_nonneg. apply le_0_n. apply le_refl. - apply le_0_n. apply H1. apply le_refl. + - rewrite Pos.max_l. unfold id. rewrite <- Pos.mul_le_mono_l. + exact H0. apply Pos.le_refl. + - rewrite Pos.max_l. unfold id. + apply Pos.mul_le_mono_l. exact H1. apply Pos.le_refl. Defined. Infix "+" := CReal_plus : CReal_scope. -Lemma CReal_plus_nth : forall (x y : CReal) (n : nat), - proj1_sig (x + y) n = Qplus (proj1_sig x (2*n)%nat) (proj1_sig y (2*n)%nat). +Lemma CReal_plus_nth : forall (x y : CReal) (n : positive), + proj1_sig (x + y) n = Qplus (proj1_sig x (2*n)%positive) + (proj1_sig y (2*n)%positive). Proof. intros. destruct x,y; reflexivity. Qed. Lemma CReal_plus_unfold : forall (x y : CReal), QSeqEquiv (proj1_sig (CReal_plus x y)) - (fun n : nat => proj1_sig x n + proj1_sig y n)%Q - (fun p => Pos.to_nat (2 * p)). + (fun n : positive => proj1_sig x n + proj1_sig y n)%Q + (fun p => 2 * p)%positive. Proof. intros [xn limx] [yn limy]. unfold CReal_plus; simpl. intros p n k H H0. - setoid_replace (xn (2 * n)%nat + yn (2 * n)%nat - (xn k + yn k))%Q - with (xn (2 * n)%nat - xn k + (yn (2 * n)%nat - yn k))%Q. + setoid_replace (xn (2 * n)%positive + yn (2 * n)%positive - (xn k + yn k))%Q + with (xn (2 * n)%positive - xn k + (yn (2 * n)%positive - yn k))%Q. 2: field. - apply (Qle_lt_trans _ (Qabs (xn (2 * n)%nat - xn k) + Qabs (yn (2 * n)%nat - yn k))). + apply (Qle_lt_trans _ (Qabs (xn (2 * n)%positive - xn k) + Qabs (yn (2 * n)%positive - yn k))). apply Qabs_triangle. setoid_replace (1#p)%Q with ((1#2*p) + (1#2*p))%Q. apply Qplus_lt_le_compat. - - apply limx. apply (le_trans _ n). apply H. - rewrite <- (mult_1_l n). rewrite mult_assoc. - apply Nat.mul_le_mono_nonneg. auto. simpl. auto. - apply le_0_n. apply le_refl. apply H0. - - apply Qlt_le_weak. apply limy. apply (le_trans _ n). apply H. - rewrite <- (mult_1_l n). rewrite mult_assoc. - apply Nat.mul_le_mono_nonneg. auto. simpl. auto. - apply le_0_n. apply le_refl. apply H0. + - apply limx. apply (Pos.le_trans _ n). apply H. + apply (Pos.le_trans _ (1 * n)). apply Pos.le_refl. + apply Pos.mul_le_mono_r. discriminate. exact H0. + - apply Qlt_le_weak. apply limy. apply (Pos.le_trans _ n). apply H. + apply (Pos.le_trans _ (1 * n)). apply Pos.le_refl. + apply Pos.mul_le_mono_r. discriminate. exact H0. - rewrite Qinv_plus_distr. unfold Qeq. reflexivity. Qed. Definition CReal_opp (x : CReal) : CReal. Proof. destruct x as [xn limx]. - exists (fun n : nat => - xn n). + exists (fun n : positive => - xn n). intros k p q H H0. unfold Qminus. rewrite Qopp_involutive. rewrite Qplus_comm. apply limx; assumption. Defined. @@ -1011,10 +926,10 @@ Definition CReal_minus (x y : CReal) : CReal Infix "-" := CReal_minus : CReal_scope. -Lemma belowMultiple : forall n p : nat, lt 0 p -> le n (p * n). +Lemma belowMultiple : forall n p : positive, Pos.le n (p * n). Proof. - intros. rewrite <- (mult_1_l n). apply Nat.mul_le_mono_nonneg. - auto. assumption. apply le_0_n. rewrite mult_1_l. apply le_refl. + intros. apply (Pos.le_trans _ (1*n)). apply Pos.le_refl. + apply Pos.mul_le_mono_r. destruct p; discriminate. Qed. Lemma CReal_plus_assoc : forall (x y z : CReal), @@ -1024,20 +939,20 @@ Proof. intros. apply CRealEq_diff. intro n. destruct x as [xn limx], y as [yn limy], z as [zn limz]. unfold CReal_plus; unfold proj1_sig. - setoid_replace (xn (2 * (2 * Pos.to_nat n))%nat + yn (2 * (2 * Pos.to_nat n))%nat - + zn (2 * Pos.to_nat n)%nat - - (xn (2 * Pos.to_nat n)%nat + (yn (2 * (2 * Pos.to_nat n))%nat - + zn (2 * (2 * Pos.to_nat n))%nat)))%Q - with (xn (2 * (2 * Pos.to_nat n))%nat - xn (2 * Pos.to_nat n)%nat - + (zn (2 * Pos.to_nat n)%nat - zn (2 * (2 * Pos.to_nat n))%nat))%Q. - apply (Qle_trans _ (Qabs (xn (2 * (2 * Pos.to_nat n))%nat - xn (2 * Pos.to_nat n)%nat) - + Qabs (zn (2 * Pos.to_nat n)%nat - zn (2 * (2 * Pos.to_nat n))%nat))). + setoid_replace (xn (2 * (2 * n))%positive + yn (2 * (2 * n))%positive + + zn (2 * n)%positive + - (xn (2 * n)%positive + (yn (2 * (2 * n))%positive + + zn (2 * (2 * n))%positive)))%Q + with (xn (2 * (2 * n))%positive - xn (2 * n)%positive + + (zn (2 * n)%positive - zn (2 * (2 * n))%positive))%Q. + apply (Qle_trans _ (Qabs (xn (2 * (2 * n))%positive - xn (2 * n)%positive) + + Qabs (zn (2 * n)%positive - zn (2 * (2 * n))%positive))). apply Qabs_triangle. rewrite <- (Qinv_plus_distr 1 1 n). apply Qplus_le_compat. - apply Qle_lteq. left. apply limx. rewrite mult_assoc. - apply belowMultiple. simpl. auto. apply belowMultiple. auto. - apply Qle_lteq. left. apply limz. apply belowMultiple. auto. - rewrite mult_assoc. apply belowMultiple. simpl. auto. field. + apply Qle_lteq. left. apply limx. rewrite Pos.mul_assoc. + apply belowMultiple. apply belowMultiple. + apply Qle_lteq. left. apply limz. apply belowMultiple. + rewrite Pos.mul_assoc. apply belowMultiple. simpl. field. Qed. Lemma CReal_plus_comm : forall x y : CReal, @@ -1045,39 +960,40 @@ Lemma CReal_plus_comm : forall x y : CReal, Proof. intros [xn limx] [yn limy]. apply CRealEq_diff. intros. unfold CReal_plus, proj1_sig. - setoid_replace (xn (2 * Pos.to_nat n)%nat + yn (2 * Pos.to_nat n)%nat - - (yn (2 * Pos.to_nat n)%nat + xn (2 * Pos.to_nat n)%nat))%Q + setoid_replace (xn (2 * n)%positive + yn (2 * n)%positive + - (yn (2 * n)%positive + xn (2 * n)%positive))%Q with 0%Q. unfold Qle. simpl. unfold Z.le. intro absurd. inversion absurd. field. Qed. Lemma CReal_plus_0_l : forall r : CReal, - CRealEq (CReal_plus (inject_Q 0) r) r. + inject_Q 0 + r == r. Proof. - intro r. assert (forall n:nat, le n (2 * n)). - { intro n. simpl. rewrite <- (plus_0_r n). rewrite <- plus_assoc. - apply Nat.add_le_mono_l. apply le_0_n. } - split. - - intros [n maj]. destruct r as [xn q]; unfold CReal_plus, proj1_sig, inject_Q in maj. + intro r. split. + - intros [n maj]. + destruct r as [xn q]; unfold CReal_plus, proj1_sig, inject_Q in maj. rewrite Qplus_0_l in maj. - specialize (q n (Pos.to_nat n) (mult 2 (Pos.to_nat n)) (le_refl _)). - apply (Qlt_not_le (2#n) (xn (Pos.to_nat n) - xn (2 * Pos.to_nat n)%nat)). + specialize (q n n (Pos.mul 2 n) (Pos.le_refl _)). + apply (Qlt_not_le (2#n) (xn n - xn (2 * n)%positive)). assumption. - apply (Qle_trans _ (Qabs (xn (Pos.to_nat n) - xn (2 * Pos.to_nat n)%nat))). + apply (Qle_trans _ (Qabs (xn n - xn (2 * n)%positive))). apply Qle_Qabs. apply (Qle_trans _ (1#n)). apply Qlt_le_weak. apply q. - apply H. unfold Qle, Z.le; simpl. apply Pos2Nat.inj_le. rewrite Pos2Nat.inj_xO. - apply H. - - intros [n maj]. destruct r as [xn q]; unfold CReal_plus, proj1_sig, inject_Q in maj. + apply belowMultiple. + unfold Qle, Qnum, Qden. apply Z.mul_le_mono_nonneg_r. + discriminate. discriminate. + - intros [n maj]. + destruct r as [xn q]; unfold CReal_plus, proj1_sig, inject_Q in maj. rewrite Qplus_0_l in maj. - specialize (q n (Pos.to_nat n) (mult 2 (Pos.to_nat n)) (le_refl _)). + specialize (q n n (Pos.mul 2 n) (Pos.le_refl _)). rewrite Qabs_Qminus in q. - apply (Qlt_not_le (2#n) (xn (mult 2 (Pos.to_nat n)) - xn (Pos.to_nat n))). + apply (Qlt_not_le (2#n) (xn (Pos.mul 2 n) - xn n)). assumption. - apply (Qle_trans _ (Qabs (xn (mult 2 (Pos.to_nat n)) - xn (Pos.to_nat n)))). + apply (Qle_trans _ (Qabs (xn (Pos.mul 2 n) - xn n))). apply Qle_Qabs. apply (Qle_trans _ (1#n)). apply Qlt_le_weak. apply q. - apply H. unfold Qle, Z.le; simpl. apply Pos2Nat.inj_le. rewrite Pos2Nat.inj_xO. - apply H. + apply belowMultiple. + unfold Qle, Qnum, Qden. apply Z.mul_le_mono_nonneg_r. + discriminate. discriminate. Qed. Lemma CReal_plus_0_r : forall r : CReal, @@ -1091,14 +1007,11 @@ Lemma CReal_plus_lt_compat_l : Proof. intros. apply CRealLt_above in H. destruct H as [n maj]. - exists n. specialize (maj (xO n)). - rewrite Pos2Nat.inj_xO in maj. - setoid_replace (proj1_sig (CReal_plus x z) (Pos.to_nat n) - - proj1_sig (CReal_plus x y) (Pos.to_nat n))%Q - with (proj1_sig z (2 * Pos.to_nat n)%nat - proj1_sig y (2 * Pos.to_nat n)%nat)%Q. - apply maj. apply Pos2Nat.inj_le. - rewrite <- (plus_0_r (Pos.to_nat n)). rewrite Pos2Nat.inj_xO. - simpl. apply Nat.add_le_mono_l. apply le_0_n. + exists n. specialize (maj (2 * n)%positive). + setoid_replace (proj1_sig (CReal_plus x z) n + - proj1_sig (CReal_plus x y) n)%Q + with (proj1_sig z (2 * n)%positive - proj1_sig y (2 * n)%positive)%Q. + apply maj. apply belowMultiple. simpl. destruct x as [xn limx], y as [yn limy], z as [zn limz]. simpl; ring. Qed. @@ -1114,12 +1027,13 @@ Lemma CReal_plus_lt_reg_l : 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 - with (proj1_sig (CReal_plus x z) (Pos.to_nat n) - proj1_sig (CReal_plus x y) (Pos.to_nat n))%Q. - apply (Qle_lt_trans _ (2#n)). unfold Qle, Z.le; simpl. apply Pos2Nat.inj_le. - rewrite <- (plus_0_r (Pos.to_nat n~0)). rewrite (Pos2Nat.inj_xO (n~0)). - simpl. apply Nat.add_le_mono_l. apply le_0_n. - apply maj. rewrite Pos2Nat.inj_xO. + setoid_replace (proj1_sig z (2 * n)%positive - proj1_sig y (2 * n)%positive)%Q + with (proj1_sig (CReal_plus x z) n - proj1_sig (CReal_plus x y) n)%Q. + apply (Qle_lt_trans _ (2#n)). + setoid_replace (2 # 2 * n)%Q with (1 # n)%Q. 2: reflexivity. + unfold Qle, Qnum, Qden. apply Z.mul_le_mono_nonneg_r. + discriminate. discriminate. + apply maj. destruct x as [xn limx], y as [yn limy], z as [zn limz]. simpl; ring. Qed. @@ -1173,7 +1087,7 @@ Lemma CReal_plus_opp_r : forall x : CReal, Proof. intros [xn limx]. apply CRealEq_diff. intros. unfold CReal_plus, CReal_opp, inject_Q, proj1_sig. - setoid_replace (xn (2 * Pos.to_nat n)%nat + - xn (2 * Pos.to_nat n)%nat - 0)%Q + setoid_replace (xn (2 * n)%positive + - xn (2 * n)%positive - 0)%Q with 0%Q. unfold Qle. simpl. unfold Z.le. intro absurd. inversion absurd. field. Qed. |