diff options
Diffstat (limited to 'theories/Reals/ConstructiveReals.v')
| -rw-r--r-- | theories/Reals/ConstructiveReals.v | 835 |
1 files changed, 0 insertions, 835 deletions
diff --git a/theories/Reals/ConstructiveReals.v b/theories/Reals/ConstructiveReals.v deleted file mode 100644 index d6eee518d3..0000000000 --- a/theories/Reals/ConstructiveReals.v +++ /dev/null @@ -1,835 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) -(************************************************************************) - -(** An interface for constructive and computable real numbers. - All of its instances are isomorphic (see file ConstructiveRealsMorphisms). - For example it contains the Cauchy reals implemented in file - ConstructivecauchyReals and the sumbool-based Dedekind reals defined by - -Structure R := { - (* The cuts are represented as propositional functions, rather than subsets, - as there are no subsets in type theory. *) - lower : Q -> Prop; - upper : Q -> Prop; - (* The cuts respect equality on Q. *) - lower_proper : Proper (Qeq ==> iff) lower; - upper_proper : Proper (Qeq ==> iff) upper; - (* The cuts are inhabited. *) - lower_bound : { q : Q | lower q }; - upper_bound : { r : Q | upper r }; - (* The lower cut is a lower set. *) - lower_lower : forall q r, q < r -> lower r -> lower q; - (* The lower cut is open. *) - lower_open : forall q, lower q -> exists r, q < r /\ lower r; - (* The upper cut is an upper set. *) - upper_upper : forall q r, q < r -> upper q -> upper r; - (* The upper cut is open. *) - upper_open : forall r, upper r -> exists q, q < r /\ upper q; - (* The cuts are disjoint. *) - disjoint : forall q, ~ (lower q /\ upper q); - (* There is no gap between the cuts. *) - located : forall q r, q < r -> { lower q } + { upper r } -}. - - see github.com/andrejbauer/dedekind-reals for the Prop-based - version of those Dedekind reals (although Prop fails to make - them an instance of ConstructiveReals). - - Any computation about constructive reals, can be worked - in the fastest instance for it; we then transport the results - to all other instances by the isomorphisms. This way of working - is different from the usual interfaces, where we would rather - prove things abstractly, by quantifying universally on the instance. - - The functions of ConstructiveReals do not have a direct impact - on performance, because algorithms will be extracted from instances, - and because fast ConstructiveReals morphisms should be coded - manually. However, since instances are forced to implement - those functions, it is probable that they will also use them - in their algorithms. So those functions hint at what we think - will yield fast and small extracted programs. *) - - -Require Import QArith. - -Definition isLinearOrder (X : Set) (Xlt : X -> X -> Set) : Set - := (forall x y:X, Xlt x y -> Xlt y x -> False) - * (forall x y z : X, Xlt x y -> Xlt y z -> Xlt x z) - * (forall x y z : X, Xlt x z -> Xlt x y + Xlt y z). - -Definition orderEq (X : Set) (Xlt : X -> X -> Set) (x y : X) : Prop - := (Xlt x y -> False) /\ (Xlt y x -> False). - -Definition orderAppart (X : Set) (Xlt : X -> X -> Set) (x y : X) : Set - := Xlt x y + Xlt y x. - -Definition orderLe (X : Set) (Xlt : X -> X -> Set) (x y : X) : Prop - := Xlt y x -> False. - -Definition sig_forall_dec_T : Type - := forall (P : nat -> Prop), (forall n, {P n} + {~P n}) - -> {n | ~P n} + {forall n, P n}. - -Definition sig_not_dec_T : Type := forall P : Prop, { ~~P } + { ~P }. - -Record ConstructiveReals : Type := - { - CRcarrier : Set; - - (* Put this order relation in sort Set rather than Prop, - to allow the definition of fast ConstructiveReals morphisms. - For example, the Cauchy reals do store information in - the proofs of CRlt, which is used in algorithms in sort Set. *) - CRlt : CRcarrier -> CRcarrier -> Set; - CRltLinear : isLinearOrder CRcarrier CRlt; - - (* The propositional truncation of CRlt. It facilitates proofs - when computations are not considered important, for example in - classical reals with extra logical axioms. *) - CRltProp : CRcarrier -> CRcarrier -> Prop; - (* This choice algorithm can be slow, keep it for the classical - quotient of the reals, where computations are blocked by - axioms like LPO. *) - CRltEpsilon : forall x y : CRcarrier, CRltProp x y -> CRlt x y; - CRltForget : forall x y : CRcarrier, CRlt x y -> CRltProp x y; - CRltDisjunctEpsilon : forall a b c d : CRcarrier, - (CRltProp a b \/ CRltProp c d) -> CRlt a b + CRlt c d; - - (* Constants *) - CRzero : CRcarrier; - CRone : CRcarrier; - - (* Addition and multiplication *) - CRplus : CRcarrier -> CRcarrier -> CRcarrier; - CRopp : CRcarrier -> CRcarrier; (* Computable opposite, - stronger than Prop-existence of opposite *) - CRmult : CRcarrier -> CRcarrier -> CRcarrier; - - CRisRing : ring_theory CRzero CRone CRplus CRmult - (fun x y => CRplus x (CRopp y)) CRopp (orderEq CRcarrier CRlt); - CRisRingExt : ring_eq_ext CRplus CRmult CRopp (orderEq CRcarrier CRlt); - - (* Compatibility with order *) - CRzero_lt_one : CRlt CRzero CRone; (* 0 # 1 would only allow 0 < 1 because - of Fmult_lt_0_compat so request 0 < 1 directly. *) - CRplus_lt_compat_l : forall r r1 r2 : CRcarrier, - CRlt r1 r2 -> CRlt (CRplus r r1) (CRplus r r2); - CRplus_lt_reg_l : forall r r1 r2 : CRcarrier, - CRlt (CRplus r r1) (CRplus r r2) -> CRlt r1 r2; - CRmult_lt_0_compat : forall x y : CRcarrier, - CRlt CRzero x -> CRlt CRzero y -> CRlt CRzero (CRmult x y); - - (* A constructive total inverse function on F would need to be continuous, - which is impossible because we cannot connect plus and minus infinities. - Therefore it has to be a partial function, defined on non zero elements. - For this reason we cannot use Coq's field_theory and field tactic. - - To implement Finv by Cauchy sequences we need orderAppart, - ~orderEq is not enough. *) - CRinv : forall x : CRcarrier, orderAppart _ CRlt x CRzero -> CRcarrier; - CRinv_l : forall (r:CRcarrier) (rnz : orderAppart _ CRlt r CRzero), - orderEq _ CRlt (CRmult (CRinv r rnz) r) CRone; - CRinv_0_lt_compat : forall (r : CRcarrier) (rnz : orderAppart _ CRlt r CRzero), - CRlt CRzero r -> CRlt CRzero (CRinv r rnz); - - (* The initial field morphism (in characteristic zero). - The abstract definition by iteration of addition is - probably the slowest. Let each instance implement - a faster (and often simpler) version. *) - CR_of_Q : Q -> CRcarrier; - CR_of_Q_plus : forall q r : Q, orderEq _ CRlt (CR_of_Q (q+r)) - (CRplus (CR_of_Q q) (CR_of_Q r)); - CR_of_Q_mult : forall q r : Q, orderEq _ CRlt (CR_of_Q (q*r)) - (CRmult (CR_of_Q q) (CR_of_Q r)); - CR_of_Q_one : orderEq _ CRlt (CR_of_Q 1) CRone; - CR_of_Q_lt : forall q r : Q, - Qlt q r -> CRlt (CR_of_Q q) (CR_of_Q r); - lt_CR_of_Q : forall q r : Q, - CRlt (CR_of_Q q) (CR_of_Q r) -> Qlt q r; - - (* This function is very fast in both the Cauchy and Dedekind - instances, because this rational number q is almost what - the proof of CRlt x y contains. - This function is also the heart of the computation of - constructive real numbers : it approximates x to any - requested precision y. *) - CR_Q_dense : forall x y : CRcarrier, CRlt x y -> - { q : Q & prod (CRlt x (CR_of_Q q)) - (CRlt (CR_of_Q q) y) }; - CR_archimedean : forall x : CRcarrier, - { n : positive & CRlt x (CR_of_Q (Z.pos n # 1)) }; - - CRminus (x y : CRcarrier) : CRcarrier - := CRplus x (CRopp y); - - (* Definitions of convergence and Cauchy-ness. The formulas - with orderLe or CRlt are logically equivalent, the choice of - orderLe in sort Prop is a question of performance. - It is very rare to turn back to the strict order to - define functions in sort Set, so we prefer to discard - those proofs during extraction. And even in those rare cases, - it is easy to divide epsilon by 2 for example. *) - CR_cv (un : nat -> CRcarrier) (l : CRcarrier) : Set - := forall p:positive, - { n : nat | forall i:nat, le n i - -> orderLe _ CRlt (CR_of_Q (-1#p)) (CRminus (un i) l) - /\ orderLe _ CRlt (CRminus (un i) l) (CR_of_Q (1#p)) }; - CR_cauchy (un : nat -> CRcarrier) : Set - := forall p : positive, - { n : nat | forall i j:nat, le n i -> le n j - -> orderLe _ CRlt (CR_of_Q (-1#p)) (CRminus (un i) (un j)) - /\ orderLe _ CRlt (CRminus (un i) (un j)) (CR_of_Q (1#p)) }; - - (* For the Cauchy reals, this algorithm consists in building - a Cauchy sequence of rationals un : nat -> Q that has - the same limit as xn. For each n:nat, un n is a 1/n - rational approximation of a point of xn that has converged - within 1/n. *) - CR_complete : - forall xn : (nat -> CRcarrier), - CR_cauchy xn -> { l : CRcarrier & CR_cv xn l }; - }. - -Lemma CRlt_asym : forall (R : ConstructiveReals) (x y : CRcarrier R), - CRlt R x y -> CRlt R y x -> False. -Proof. - intros. destruct (CRltLinear R), p. - apply (f x y); assumption. -Qed. - -Lemma CRlt_proper - : forall R : ConstructiveReals, - CMorphisms.Proper - (CMorphisms.respectful (orderEq _ (CRlt R)) - (CMorphisms.respectful (orderEq _ (CRlt R)) CRelationClasses.iffT)) (CRlt R). -Proof. - intros R x y H x0 y0 H0. destruct H, H0. - destruct (CRltLinear R). split. - - intro. destruct (s x y x0). assumption. - contradiction. destruct (s y y0 x0). - assumption. assumption. contradiction. - - intro. destruct (s y x y0). assumption. - contradiction. destruct (s x x0 y0). - assumption. assumption. contradiction. -Qed. - -Lemma CRle_refl : forall (R : ConstructiveReals) (x : CRcarrier R), - CRlt R x x -> False. -Proof. - intros. destruct (CRltLinear R), p. - exact (f x x H H). -Qed. - -Lemma CRle_lt_trans : forall (R : ConstructiveReals) (r1 r2 r3 : CRcarrier R), - (CRlt R r2 r1 -> False) -> CRlt R r2 r3 -> CRlt R r1 r3. -Proof. - intros. destruct (CRltLinear R). - destruct (s r2 r1 r3 H0). contradiction. apply c. -Qed. - -Lemma CRlt_le_trans : forall (R : ConstructiveReals) (r1 r2 r3 : CRcarrier R), - CRlt R r1 r2 -> (CRlt R r3 r2 -> False) -> CRlt R r1 r3. -Proof. - intros. destruct (CRltLinear R). - destruct (s r1 r3 r2 H). apply c. contradiction. -Qed. - -Lemma CRle_trans : forall (R : ConstructiveReals) (x y z : CRcarrier R), - orderLe _ (CRlt R) x y -> orderLe _ (CRlt R) y z -> orderLe _ (CRlt R) x z. -Proof. - intros. intro abs. apply H0. - apply (CRlt_le_trans _ _ x); assumption. -Qed. - -Lemma CRlt_trans : forall (R : ConstructiveReals) (x y z : CRcarrier R), - CRlt R x y -> CRlt R y z -> CRlt R x z. -Proof. - intros. apply (CRlt_le_trans R _ y _ H). - apply CRlt_asym. exact H0. -Defined. - -Lemma CRlt_trans_flip : forall (R : ConstructiveReals) (x y z : CRcarrier R), - CRlt R y z -> CRlt R x y -> CRlt R x z. -Proof. - intros. apply (CRlt_le_trans R _ y). exact H0. - apply CRlt_asym. exact H. -Defined. - -Lemma CReq_refl : forall (R : ConstructiveReals) (x : CRcarrier R), - orderEq _ (CRlt R) x x. -Proof. - split; apply CRle_refl. -Qed. - -Lemma CReq_sym : forall (R : ConstructiveReals) (x y : CRcarrier R), - orderEq _ (CRlt R) x y - -> orderEq _ (CRlt R) y x. -Proof. - intros. destruct H. split; intro abs; contradiction. -Qed. - -Lemma CReq_trans : forall (R : ConstructiveReals) (x y z : CRcarrier R), - orderEq _ (CRlt R) x y - -> orderEq _ (CRlt R) y z - -> orderEq _ (CRlt R) x z. -Proof. - intros. destruct H,H0. destruct (CRltLinear R), p. split. - - intro abs. destruct (s _ y _ abs); contradiction. - - intro abs. destruct (s _ y _ abs); contradiction. -Qed. - -Lemma CR_setoid : forall R : ConstructiveReals, - Setoid_Theory (CRcarrier R) (orderEq _ (CRlt R)). -Proof. - split. intro x. apply CReq_refl. - intros x y. apply CReq_sym. - intros x y z. apply CReq_trans. -Qed. - -Lemma CRplus_0_r : forall (R : ConstructiveReals) (x : CRcarrier R), - orderEq _ (CRlt R) (CRplus R x (CRzero R)) x. -Proof. - intros. destruct (CRisRing R). - apply (CReq_trans R _ (CRplus R (CRzero R) x)). - apply Radd_comm. apply Radd_0_l. -Qed. - -Lemma CRmult_1_r : forall (R : ConstructiveReals) (x : CRcarrier R), - orderEq _ (CRlt R) (CRmult R x (CRone R)) x. -Proof. - intros. destruct (CRisRing R). - apply (CReq_trans R _ (CRmult R (CRone R) x)). - apply Rmul_comm. apply Rmul_1_l. -Qed. - -Lemma CRplus_opp_l : forall (R : ConstructiveReals) (x : CRcarrier R), - orderEq _ (CRlt R) (CRplus R (CRopp R x) x) (CRzero R). -Proof. - intros. destruct (CRisRing R). - apply (CReq_trans R _ (CRplus R x (CRopp R x))). - apply Radd_comm. apply Ropp_def. -Qed. - -Lemma CRplus_lt_compat_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R), - CRlt R r1 r2 -> CRlt R (CRplus R r1 r) (CRplus R r2 r). -Proof. - intros. destruct (CRisRing R). - apply (CRlt_proper R (CRplus R r r1) (CRplus R r1 r) (Radd_comm _ _) - (CRplus R r2 r) (CRplus R r2 r)). - apply CReq_refl. - apply (CRlt_proper R _ _ (CReq_refl _ _) _ (CRplus R r r2)). - apply Radd_comm. apply CRplus_lt_compat_l. exact H. -Qed. - -Lemma CRplus_lt_reg_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R), - CRlt R (CRplus R r1 r) (CRplus R r2 r) -> CRlt R r1 r2. -Proof. - intros. destruct (CRisRing R). - apply (CRlt_proper R (CRplus R r r1) (CRplus R r1 r) (Radd_comm _ _) - (CRplus R r2 r) (CRplus R r2 r)) in H. - 2: apply CReq_refl. - apply (CRlt_proper R _ _ (CReq_refl _ _) _ (CRplus R r r2)) in H. - apply CRplus_lt_reg_l in H. exact H. - apply Radd_comm. -Qed. - -Lemma CRplus_le_compat_l : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R), - orderLe _ (CRlt R) r1 r2 - -> orderLe _ (CRlt R) (CRplus R r r1) (CRplus R r r2). -Proof. - intros. intros abs. apply CRplus_lt_reg_l in abs. apply H. exact abs. -Qed. - -Lemma CRplus_le_compat_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R), - orderLe _ (CRlt R) r1 r2 - -> orderLe _ (CRlt R) (CRplus R r1 r) (CRplus R r2 r). -Proof. - intros. intros abs. apply CRplus_lt_reg_r in abs. apply H. exact abs. -Qed. - -Lemma CRplus_le_reg_l : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R), - orderLe _ (CRlt R) (CRplus R r r1) (CRplus R r r2) - -> orderLe _ (CRlt R) r1 r2. -Proof. - intros. intro abs. apply H. clear H. - apply CRplus_lt_compat_l. exact abs. -Qed. - -Lemma CRplus_le_reg_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R), - orderLe _ (CRlt R) (CRplus R r1 r) (CRplus R r2 r) - -> orderLe _ (CRlt R) r1 r2. -Proof. - intros. intro abs. apply H. clear H. - apply CRplus_lt_compat_r. exact abs. -Qed. - -Lemma CRplus_lt_le_compat : - forall (R : ConstructiveReals) (r1 r2 r3 r4 : CRcarrier R), - CRlt R r1 r2 - -> (CRlt R r4 r3 -> False) - -> CRlt R (CRplus R r1 r3) (CRplus R r2 r4). -Proof. - intros. apply (CRlt_le_trans R _ (CRplus R r2 r3)). - apply CRplus_lt_compat_r. exact H. intro abs. - apply CRplus_lt_reg_l in abs. contradiction. -Qed. - -Lemma CRplus_eq_reg_l : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R), - orderEq _ (CRlt R) (CRplus R r r1) (CRplus R r r2) - -> orderEq _ (CRlt R) r1 r2. -Proof. - intros. - destruct (CRisRingExt R). clear Rmul_ext Ropp_ext. - pose proof (Radd_ext - (CRopp R r) (CRopp R r) (CReq_refl _ _) - _ _ H). - destruct (CRisRing R). - apply (CReq_trans _ r1) in H0. - apply (CReq_trans R _ _ _ H0). - apply (CReq_trans R _ (CRplus R (CRplus R (CRopp R r) r) r2)). - apply Radd_assoc. - apply (CReq_trans R _ (CRplus R (CRzero R) r2)). - apply Radd_ext. apply CRplus_opp_l. apply CReq_refl. - apply Radd_0_l. apply CReq_sym. - apply (CReq_trans R _ (CRplus R (CRplus R (CRopp R r) r) r1)). - apply Radd_assoc. - apply (CReq_trans R _ (CRplus R (CRzero R) r1)). - apply Radd_ext. apply CRplus_opp_l. apply CReq_refl. - apply Radd_0_l. -Qed. - -Lemma CRplus_eq_reg_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R), - orderEq _ (CRlt R) (CRplus R r1 r) (CRplus R r2 r) - -> orderEq _ (CRlt R) r1 r2. -Proof. - intros. apply (CRplus_eq_reg_l R r). - apply (CReq_trans R _ (CRplus R r1 r)). apply (Radd_comm (CRisRing R)). - apply (CReq_trans R _ (CRplus R r2 r)). - exact H. apply (Radd_comm (CRisRing R)). -Qed. - -Lemma CRopp_involutive : forall (R : ConstructiveReals) (r : CRcarrier R), - orderEq _ (CRlt R) (CRopp R (CRopp R r)) r. -Proof. - intros. apply (CRplus_eq_reg_l R (CRopp R r)). - apply (CReq_trans R _ (CRzero R)). apply CRisRing. - apply CReq_sym, (CReq_trans R _ (CRplus R r (CRopp R r))). - apply CRisRing. apply CRisRing. -Qed. - -Lemma CRopp_gt_lt_contravar - : forall (R : ConstructiveReals) (r1 r2 : CRcarrier R), - CRlt R r2 r1 -> CRlt R (CRopp R r1) (CRopp R r2). -Proof. - intros. apply (CRplus_lt_reg_l R r1). - destruct (CRisRing R). - apply (CRle_lt_trans R _ (CRzero R)). apply Ropp_def. - apply (CRplus_lt_compat_l R (CRopp R r2)) in H. - apply (CRle_lt_trans R _ (CRplus R (CRopp R r2) r2)). - apply (CRle_trans R _ (CRplus R r2 (CRopp R r2))). - destruct (Ropp_def r2). exact H0. - destruct (Radd_comm r2 (CRopp R r2)). exact H1. - apply (CRlt_le_trans R _ _ _ H). - destruct (Radd_comm r1 (CRopp R r2)). exact H0. -Qed. - -Lemma CRopp_lt_cancel : forall (R : ConstructiveReals) (r1 r2 : CRcarrier R), - CRlt R (CRopp R r2) (CRopp R r1) -> CRlt R r1 r2. -Proof. - intros. apply (CRplus_lt_compat_r R r1) in H. - destruct (CRplus_opp_l R r1) as [_ H1]. - apply (CRlt_le_trans R _ _ _ H) in H1. clear H. - apply (CRplus_lt_compat_l R r2) in H1. - destruct (CRplus_0_r R r2) as [_ H0]. - apply (CRlt_le_trans R _ _ _ H1) in H0. clear H1. - destruct (Radd_assoc (CRisRing R) r2 (CRopp R r2) r1) as [H _]. - apply (CRle_lt_trans R _ _ _ H) in H0. clear H. - apply (CRle_lt_trans R _ (CRplus R (CRzero R) r1)). - apply (Radd_0_l (CRisRing R)). - apply (CRle_lt_trans R _ (CRplus R (CRplus R r2 (CRopp R r2)) r1)). - 2: exact H0. apply CRplus_le_compat_r. - destruct (Ropp_def (CRisRing R) r2). exact H. -Qed. - -Lemma CRopp_plus_distr : forall (R : ConstructiveReals) (r1 r2 : CRcarrier R), - orderEq _ (CRlt R) (CRopp R (CRplus R r1 r2)) (CRplus R (CRopp R r1) (CRopp R r2)). -Proof. - intros. destruct (CRisRing R), (CRisRingExt R). - apply (CRplus_eq_reg_l R (CRplus R r1 r2)). - apply (CReq_trans R _ (CRzero R)). apply Ropp_def. - apply (CReq_trans R _ (CRplus R (CRplus R r2 r1) (CRplus R (CRopp R r1) (CRopp R r2)))). - apply (CReq_trans R _ (CRplus R r2 (CRplus R r1 (CRplus R (CRopp R r1) (CRopp R r2))))). - apply (CReq_trans R _ (CRplus R r2 (CRopp R r2))). - apply CReq_sym. apply Ropp_def. apply Radd_ext. - apply CReq_refl. - apply (CReq_trans R _ (CRplus R (CRzero R) (CRopp R r2))). - apply CReq_sym, Radd_0_l. - apply (CReq_trans R _ (CRplus R (CRplus R r1 (CRopp R r1)) (CRopp R r2))). - apply Radd_ext. 2: apply CReq_refl. apply CReq_sym, Ropp_def. - apply CReq_sym, Radd_assoc. apply Radd_assoc. - apply Radd_ext. 2: apply CReq_refl. apply Radd_comm. -Qed. - -Lemma CRmult_plus_distr_l : forall (R : ConstructiveReals) (r1 r2 r3 : CRcarrier R), - orderEq _ (CRlt R) (CRmult R r1 (CRplus R r2 r3)) - (CRplus R (CRmult R r1 r2) (CRmult R r1 r3)). -Proof. - intros. destruct (CRisRing R). - apply (CReq_trans R _ (CRmult R (CRplus R r2 r3) r1)). - apply Rmul_comm. - apply (CReq_trans R _ (CRplus R (CRmult R r2 r1) (CRmult R r3 r1))). - apply Rdistr_l. - apply (CReq_trans R _ (CRplus R (CRmult R r1 r2) (CRmult R r3 r1))). - destruct (CRisRingExt R). apply Radd_ext. - apply Rmul_comm. apply CReq_refl. - destruct (CRisRingExt R). apply Radd_ext. - apply CReq_refl. apply Rmul_comm. -Qed. - -(* x == x+x -> x == 0 *) -Lemma CRzero_double : forall (R : ConstructiveReals) (x : CRcarrier R), - orderEq _ (CRlt R) x (CRplus R x x) - -> orderEq _ (CRlt R) x (CRzero R). -Proof. - intros. - apply (CRplus_eq_reg_l R x), CReq_sym, (CReq_trans R _ x). - apply CRplus_0_r. exact H. -Qed. - -Lemma CRmult_0_r : forall (R : ConstructiveReals) (x : CRcarrier R), - orderEq _ (CRlt R) (CRmult R x (CRzero R)) (CRzero R). -Proof. - intros. apply CRzero_double. - apply (CReq_trans R _ (CRmult R x (CRplus R (CRzero R) (CRzero R)))). - destruct (CRisRingExt R). apply Rmul_ext. apply CReq_refl. - apply CReq_sym, CRplus_0_r. - destruct (CRisRing R). apply CRmult_plus_distr_l. -Qed. - -Lemma CRopp_mult_distr_r : forall (R : ConstructiveReals) (r1 r2 : CRcarrier R), - orderEq _ (CRlt R) (CRopp R (CRmult R r1 r2)) - (CRmult R r1 (CRopp R r2)). -Proof. - intros. apply (CRplus_eq_reg_l R (CRmult R r1 r2)). - destruct (CRisRing R). - apply (CReq_trans R _ (CRzero R)). apply Ropp_def. - apply (CReq_trans R _ (CRmult R r1 (CRplus R r2 (CRopp R r2)))). - 2: apply CRmult_plus_distr_l. - apply (CReq_trans R _ (CRmult R r1 (CRzero R))). - apply CReq_sym, CRmult_0_r. - destruct (CRisRingExt R). apply Rmul_ext. apply CReq_refl. - apply CReq_sym, Ropp_def. -Qed. - -Lemma CRopp_mult_distr_l : forall (R : ConstructiveReals) (r1 r2 : CRcarrier R), - orderEq _ (CRlt R) (CRopp R (CRmult R r1 r2)) - (CRmult R (CRopp R r1) r2). -Proof. - intros. apply (CReq_trans R _ (CRmult R r2 (CRopp R r1))). - apply (CReq_trans R _ (CRopp R (CRmult R r2 r1))). - apply (Ropp_ext (CRisRingExt R)). - apply CReq_sym, (Rmul_comm (CRisRing R)). - apply CRopp_mult_distr_r. - apply CReq_sym, (Rmul_comm (CRisRing R)). -Qed. - -Lemma CRmult_lt_compat_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R), - CRlt R (CRzero R) r - -> CRlt R r1 r2 - -> CRlt R (CRmult R r1 r) (CRmult R r2 r). -Proof. - intros. apply (CRplus_lt_reg_r R (CRopp R (CRmult R r1 r))). - apply (CRle_lt_trans R _ (CRzero R)). - apply (Ropp_def (CRisRing R)). - apply (CRlt_le_trans R _ (CRplus R (CRmult R r2 r) (CRmult R (CRopp R r1) r))). - apply (CRlt_le_trans R _ (CRmult R (CRplus R r2 (CRopp R r1)) r)). - apply CRmult_lt_0_compat. 2: exact H. - apply (CRplus_lt_reg_r R r1). - apply (CRle_lt_trans R _ r1). apply (Radd_0_l (CRisRing R)). - apply (CRlt_le_trans R _ r2 _ H0). - apply (CRle_trans R _ (CRplus R r2 (CRplus R (CRopp R r1) r1))). - apply (CRle_trans R _ (CRplus R r2 (CRzero R))). - destruct (CRplus_0_r R r2). exact H1. - apply CRplus_le_compat_l. destruct (CRplus_opp_l R r1). exact H1. - destruct (Radd_assoc (CRisRing R) r2 (CRopp R r1) r1). exact H2. - destruct (CRisRing R). - destruct (Rdistr_l r2 (CRopp R r1) r). exact H2. - apply CRplus_le_compat_l. destruct (CRopp_mult_distr_l R r1 r). - exact H1. -Qed. - -Lemma CRinv_r : forall (R : ConstructiveReals) (r:CRcarrier R) - (rnz : orderAppart _ (CRlt R) r (CRzero R)), - orderEq _ (CRlt R) (CRmult R r (CRinv R r rnz)) (CRone R). -Proof. - intros. apply (CReq_trans R _ (CRmult R (CRinv R r rnz) r)). - apply (CRisRing R). apply CRinv_l. -Qed. - -Lemma CRmult_lt_reg_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R), - CRlt R (CRzero R) r - -> CRlt R (CRmult R r1 r) (CRmult R r2 r) - -> CRlt R r1 r2. -Proof. - intros. apply (CRmult_lt_compat_r R (CRinv R r (inr H))) in H0. - 2: apply CRinv_0_lt_compat, H. - apply (CRle_lt_trans R _ (CRmult R (CRmult R r1 r) (CRinv R r (inr H)))). - - clear H0. apply (CRle_trans R _ (CRmult R r1 (CRone R))). - destruct (CRmult_1_r R r1). exact H0. - apply (CRle_trans R _ (CRmult R r1 (CRmult R r (CRinv R r (inr H))))). - destruct (Rmul_ext (CRisRingExt R) r1 r1 (CReq_refl R r1) - (CRmult R r (CRinv R r (inr H))) (CRone R)). - apply CRinv_r. exact H0. - destruct (Rmul_assoc (CRisRing R) r1 r (CRinv R r (inr H))). exact H1. - - apply (CRlt_le_trans R _ (CRmult R (CRmult R r2 r) (CRinv R r (inr H)))). - exact H0. clear H0. - apply (CRle_trans R _ (CRmult R r2 (CRone R))). - 2: destruct (CRmult_1_r R r2); exact H1. - apply (CRle_trans R _ (CRmult R r2 (CRmult R r (CRinv R r (inr H))))). - destruct (Rmul_assoc (CRisRing R) r2 r (CRinv R r (inr H))). exact H0. - destruct (Rmul_ext (CRisRingExt R) r2 r2 (CReq_refl R r2) - (CRmult R r (CRinv R r (inr H))) (CRone R)). - apply CRinv_r. exact H1. -Qed. - -Lemma CRmult_lt_reg_l : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R), - CRlt R (CRzero R) r - -> CRlt R (CRmult R r r1) (CRmult R r r2) - -> CRlt R r1 r2. -Proof. - intros. - destruct (Rmul_comm (CRisRing R) r r1) as [H1 _]. - apply (CRle_lt_trans R _ _ _ H1) in H0. clear H1. - destruct (Rmul_comm (CRisRing R) r r2) as [_ H1]. - apply (CRlt_le_trans R _ _ _ H0) in H1. clear H0. - apply CRmult_lt_reg_r in H1. - exact H1. exact H. -Qed. - -Lemma CRmult_le_compat_l : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R), - CRlt R (CRzero R) r - -> orderLe _ (CRlt R) r1 r2 - -> orderLe _ (CRlt R) (CRmult R r r1) (CRmult R r r2). -Proof. - intros. intro abs. apply CRmult_lt_reg_l in abs. - contradiction. exact H. -Qed. - -Lemma CRmult_le_compat_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R), - CRlt R (CRzero R) r - -> orderLe _ (CRlt R) r1 r2 - -> orderLe _ (CRlt R) (CRmult R r1 r) (CRmult R r2 r). -Proof. - intros. intro abs. apply CRmult_lt_reg_r in abs. - contradiction. exact H. -Qed. - -Lemma CRmult_eq_reg_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R), - orderAppart _ (CRlt R) (CRzero R) r - -> orderEq _ (CRlt R) (CRmult R r1 r) (CRmult R r2 r) - -> orderEq _ (CRlt R) r1 r2. -Proof. - intros. destruct H0,H. - - split. - + intro abs. apply H0. apply CRmult_lt_compat_r. - exact c. exact abs. - + intro abs. apply H1. apply CRmult_lt_compat_r. - exact c. exact abs. - - split. - + intro abs. apply H1. apply CRopp_lt_cancel. - apply (CRle_lt_trans R _ (CRmult R r1 (CRopp R r))). - apply CRopp_mult_distr_r. - apply (CRlt_le_trans R _ (CRmult R r2 (CRopp R r))). - 2: apply CRopp_mult_distr_r. - apply CRmult_lt_compat_r. 2: exact abs. - apply (CRplus_lt_reg_r R r). apply (CRle_lt_trans R _ r). - apply (Radd_0_l (CRisRing R)). - apply (CRlt_le_trans R _ (CRzero R) _ c). - apply CRplus_opp_l. - + intro abs. apply H0. apply CRopp_lt_cancel. - apply (CRle_lt_trans R _ (CRmult R r2 (CRopp R r))). - apply CRopp_mult_distr_r. - apply (CRlt_le_trans R _ (CRmult R r1 (CRopp R r))). - 2: apply CRopp_mult_distr_r. - apply CRmult_lt_compat_r. 2: exact abs. - apply (CRplus_lt_reg_r R r). apply (CRle_lt_trans R _ r). - apply (Radd_0_l (CRisRing R)). - apply (CRlt_le_trans R _ (CRzero R) _ c). - apply CRplus_opp_l. -Qed. - -Lemma CR_of_Q_proper : forall (R : ConstructiveReals) (q r : Q), - q == r -> orderEq _ (CRlt R) (CR_of_Q R q) (CR_of_Q R r). -Proof. - split. - - intro abs. apply lt_CR_of_Q in abs. rewrite H in abs. - exact (Qlt_not_le r r abs (Qle_refl r)). - - intro abs. apply lt_CR_of_Q in abs. rewrite H in abs. - exact (Qlt_not_le r r abs (Qle_refl r)). -Qed. - -Lemma CR_of_Q_zero : forall (R : ConstructiveReals), - orderEq _ (CRlt R) (CR_of_Q R 0) (CRzero R). -Proof. - intros. apply CRzero_double. - apply (CReq_trans R _ (CR_of_Q R (0+0))). apply CR_of_Q_proper. - reflexivity. apply CR_of_Q_plus. -Qed. - -Lemma CR_of_Q_opp : forall (R : ConstructiveReals) (q : Q), - orderEq _ (CRlt R) (CR_of_Q R (-q)) (CRopp R (CR_of_Q R q)). -Proof. - intros. apply (CRplus_eq_reg_l R (CR_of_Q R q)). - apply (CReq_trans R _ (CRzero R)). - apply (CReq_trans R _ (CR_of_Q R (q-q))). - apply CReq_sym, CR_of_Q_plus. - apply (CReq_trans R _ (CR_of_Q R 0)). - apply CR_of_Q_proper. ring. apply CR_of_Q_zero. - apply CReq_sym. apply (CRisRing R). -Qed. - -Lemma CR_of_Q_le : forall (R : ConstructiveReals) (r q : Q), - Qle r q - -> orderLe _ (CRlt R) (CR_of_Q R r) (CR_of_Q R q). -Proof. - intros. intro abs. apply lt_CR_of_Q in abs. - exact (Qlt_not_le _ _ abs H). -Qed. - -Lemma CR_of_Q_pos : forall (R : ConstructiveReals) (q:Q), - Qlt 0 q -> CRlt R (CRzero R) (CR_of_Q R q). -Proof. - intros. apply (CRle_lt_trans R _ (CR_of_Q R 0)). - apply CR_of_Q_zero. apply CR_of_Q_lt. exact H. -Qed. - -Lemma CR_cv_above_rat - : forall (R : ConstructiveReals) (xn : nat -> Q) (x : CRcarrier R) (q : Q), - CR_cv R (fun n : nat => CR_of_Q R (xn n)) x - -> CRlt R (CR_of_Q R q) x - -> { n : nat | forall p:nat, le n p -> Qlt q (xn p) }. -Proof. - intros. - destruct (CR_Q_dense R _ _ H0) as [r [H1 H2]]. - apply lt_CR_of_Q in H1. clear H0. - destruct (Qarchimedean (/(r-q))) as [p pmaj]. - destruct (H p) as [n nmaj]. - exists n. intros k lenk. specialize (nmaj k lenk) as [H3 _]. - apply (lt_CR_of_Q R), (CRlt_le_trans R _ (CRplus R x (CR_of_Q R (-1#p)))). - apply (CRlt_trans R _ (CRplus R (CR_of_Q R r) (CR_of_Q R (-1#p)))). - 2: apply CRplus_lt_compat_r, H2. - apply (CRlt_le_trans R _ (CR_of_Q R (r+(-1#p)))). - - apply CR_of_Q_lt. - apply (Qplus_lt_l _ _ (-(-1#p)-q)). field_simplify. - setoid_replace (-1*(-1#p)) with (1#p). 2: reflexivity. - apply (Qmult_lt_l _ _ (r-q)) in pmaj. - rewrite Qmult_inv_r in pmaj. apply Qlt_shift_div_r in pmaj. - 2: reflexivity. setoid_replace (-1*q + r) with (r-q). exact pmaj. - ring. intro abs. apply Qlt_minus_iff in H1. - rewrite abs in H1. inversion H1. - apply Qlt_minus_iff in H1. exact H1. - - apply CR_of_Q_plus. - - apply (CRplus_le_reg_r R (CRopp R x)). - apply (CRle_trans R _ (CR_of_Q R (-1#p))). 2: exact H3. clear H3. - apply (CRle_trans R _ (CRplus R (CRopp R x) (CRplus R x (CR_of_Q R (-1 # p))))). - exact (proj1 (Radd_comm (CRisRing R) _ _)). - apply (CRle_trans R _ (CRplus R (CRplus R (CRopp R x) x) (CR_of_Q R (-1 # p)))). - exact (proj2 (Radd_assoc (CRisRing R) _ _ _)). - apply (CRle_trans R _ (CRplus R (CRzero R) (CR_of_Q R (-1 # p)))). - apply CRplus_le_compat_r. exact (proj2 (CRplus_opp_l R _)). - exact (proj2 (Radd_0_l (CRisRing R) _)). -Qed. - -Lemma CR_cv_below_rat - : forall (R : ConstructiveReals) (xn : nat -> Q) (x : CRcarrier R) (q : Q), - CR_cv R (fun n : nat => CR_of_Q R (xn n)) x - -> CRlt R x (CR_of_Q R q) - -> { n : nat | forall p:nat, le n p -> Qlt (xn p) q }. -Proof. - intros. - destruct (CR_Q_dense R _ _ H0) as [r [H1 H2]]. - apply lt_CR_of_Q in H2. clear H0. - destruct (Qarchimedean (/(q-r))) as [p pmaj]. - destruct (H p) as [n nmaj]. - exists n. intros k lenk. specialize (nmaj k lenk) as [_ H4]. - apply (lt_CR_of_Q R), (CRle_lt_trans R _ (CRplus R x (CR_of_Q R (1#p)))). - - apply (CRplus_le_reg_r R (CRopp R x)). - apply (CRle_trans R _ (CR_of_Q R (1#p))). exact H4. clear H4. - apply (CRle_trans R _ (CRplus R (CRopp R x) (CRplus R x (CR_of_Q R (1 # p))))). - 2: exact (proj1 (Radd_comm (CRisRing R) _ _)). - apply (CRle_trans R _ (CRplus R (CRplus R (CRopp R x) x) (CR_of_Q R (1 # p)))). - 2: exact (proj1 (Radd_assoc (CRisRing R) _ _ _)). - apply (CRle_trans R _ (CRplus R (CRzero R) (CR_of_Q R (1 # p)))). - exact (proj1 (Radd_0_l (CRisRing R) _)). - apply CRplus_le_compat_r. exact (proj1 (CRplus_opp_l R _)). - - apply (CRlt_trans R _ (CRplus R (CR_of_Q R r) (CR_of_Q R (1 # p)))). - apply CRplus_lt_compat_r. exact H1. - apply (CRle_lt_trans R _ (CR_of_Q R (r + (1#p)))). - apply CR_of_Q_plus. apply CR_of_Q_lt. - apply (Qmult_lt_l _ _ (q-r)) in pmaj. - rewrite Qmult_inv_r in pmaj. apply Qlt_shift_div_r in pmaj. - apply (Qplus_lt_l _ _ (-r)). field_simplify. - setoid_replace (-1*r + q) with (q-r). exact pmaj. - ring. reflexivity. intro abs. apply Qlt_minus_iff in H2. - rewrite abs in H2. inversion H2. - apply Qlt_minus_iff in H2. exact H2. -Qed. - -Lemma CR_cv_const : forall (R : ConstructiveReals) (x y : CRcarrier R), - CR_cv R (fun _ => x) y -> orderEq _ (CRlt R) x y. -Proof. - intros. destruct (CRisRing R). split. - - intro abs. - destruct (CR_Q_dense R x y abs) as [q [H0 H1]]. - destruct (CR_Q_dense R _ _ H1) as [r [H2 H3]]. - apply lt_CR_of_Q in H2. - destruct (Qarchimedean (/(r-q))) as [p pmaj]. - destruct (H p) as [n nmaj]. specialize (nmaj n (le_refl n)) as [nmaj _]. - apply nmaj. clear nmaj. - apply (CRlt_trans R _ (CR_of_Q R (q-r))). - apply (CRlt_le_trans R _ (CRplus R (CR_of_Q R q) (CRopp R (CR_of_Q R r)))). - + apply CRplus_lt_le_compat. exact H0. - intro H4. apply CRopp_lt_cancel in H4. exact (CRlt_asym R _ _ H4 H3). - + apply (CRle_trans R _ (CRplus R (CR_of_Q R q) (CR_of_Q R (-r)))). - apply CRplus_le_compat_l. exact (proj1 (CR_of_Q_opp R r)). - exact (proj1 (CR_of_Q_plus R _ _)). - + apply CR_of_Q_lt. - apply (Qplus_lt_l _ _ (-(-1#p)+r-q)). field_simplify. - setoid_replace (-1*(-1#p)) with (1#p). 2: reflexivity. - apply (Qmult_lt_l _ _ (r-q)) in pmaj. - rewrite Qmult_inv_r in pmaj. apply Qlt_shift_div_r in pmaj. - 2: reflexivity. setoid_replace (-1*q + r) with (r-q). exact pmaj. - ring. intro H4. apply Qlt_minus_iff in H2. - rewrite H4 in H2. inversion H2. - apply Qlt_minus_iff in H2. exact H2. - - intro abs. - destruct (CR_Q_dense R _ _ abs) as [q [H0 H1]]. - destruct (CR_Q_dense R _ _ H0) as [r [H2 H3]]. - apply lt_CR_of_Q in H3. - destruct (Qarchimedean (/(q-r))) as [p pmaj]. - destruct (H p) as [n nmaj]. specialize (nmaj n (le_refl n)) as [_ nmaj]. - apply nmaj. clear nmaj. - apply (CRlt_trans R _ (CR_of_Q R (q-r))). - + apply CR_of_Q_lt. - apply (Qmult_lt_l _ _ (q-r)) in pmaj. - rewrite Qmult_inv_r in pmaj. apply Qlt_shift_div_r in pmaj. - exact pmaj. reflexivity. - intro H4. apply Qlt_minus_iff in H3. - rewrite H4 in H3. inversion H3. - apply Qlt_minus_iff in H3. exact H3. - + apply (CRle_lt_trans R _ (CRplus R (CR_of_Q R q) (CR_of_Q R (-r)))). - apply CR_of_Q_plus. - apply (CRle_lt_trans R _ (CRplus R (CR_of_Q R q) (CRopp R (CR_of_Q R r)))). - apply CRplus_le_compat_l. exact (proj2 (CR_of_Q_opp R r)). - apply CRplus_lt_le_compat. exact H1. - intro H4. apply CRopp_lt_cancel in H4. - exact (CRlt_asym R _ _ H4 H2). -Qed. |