diff options
| author | Vincent Semeria | 2019-08-09 23:50:19 +0200 |
|---|---|---|
| committer | Vincent Semeria | 2019-08-09 23:50:19 +0200 |
| commit | 0ea914c66097f04784a67999457bf3a6273dff1e (patch) | |
| tree | 4dc49b0d4aac4fe19f156feaf7108f2d054714c0 | |
| parent | bf35f5534f21c084921b5fc3a0830d4a1d9ebd87 (diff) | |
Switch constructive Rlt to sort Type, to make it compute later
| -rw-r--r-- | theories/QArith/QArith_base.v | 8 | ||||
| -rw-r--r-- | theories/Reals/ConstructiveCauchyReals.v | 198 | ||||
| -rw-r--r-- | theories/Reals/ConstructiveRIneq.v | 429 | ||||
| -rw-r--r-- | theories/Reals/ConstructiveRcomplete.v | 110 | ||||
| -rw-r--r-- | theories/Reals/ConstructiveReals.v | 50 | ||||
| -rw-r--r-- | theories/Reals/RIneq.v | 58 | ||||
| -rw-r--r-- | theories/Reals/Raxioms.v | 95 | ||||
| -rw-r--r-- | theories/Reals/Rdefinitions.v | 20 |
8 files changed, 627 insertions, 341 deletions
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index a5ea5cc6e5..b60feb9256 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -728,18 +728,18 @@ Defined. Lemma Qarchimedean : forall q : Q, { p : positive | q < Z.pos p # 1 }. Proof. - intros. destruct q as [a b]. unfold Qlt. simpl. - rewrite Zmult_1_r. destruct a. + intros. destruct q as [a b]. destruct a. - exists xH. reflexivity. - exists (p+1)%positive. apply (Z.lt_le_trans _ (Z.pos (p+1))). - apply Z.lt_succ_diag_r. rewrite Pos2Z.inj_mul. + simpl. rewrite Pos.mul_1_r. + apply Z.lt_succ_diag_r. simpl. rewrite Pos2Z.inj_mul. rewrite <- (Zmult_1_r (Z.pos (p+1))). apply Z.mul_le_mono_nonneg. discriminate. rewrite Zmult_1_r. apply Z.le_refl. discriminate. apply Z2Nat.inj_le. discriminate. apply Pos2Z.is_nonneg. apply Nat.le_succ_l. apply Nat2Z.inj_lt. rewrite Z2Nat.id. apply Pos2Z.is_pos. apply Pos2Z.is_nonneg. - exists xH. reflexivity. -Qed. +Defined. (** Compatibility of operations with respect to order. *) diff --git a/theories/Reals/ConstructiveCauchyReals.v b/theories/Reals/ConstructiveCauchyReals.v index 701fabd974..2b592ea21a 100644 --- a/theories/Reals/ConstructiveCauchyReals.v +++ b/theories/Reals/ConstructiveCauchyReals.v @@ -13,6 +13,7 @@ Require Import QArith. Require Import Qabs. Require Import Qround. Require Import Logic.ConstructiveEpsilon. +Require CMorphisms. Open Scope Q. @@ -216,12 +217,16 @@ Open Scope CReal_scope. (* So QSeqEquiv is the equivalence relation of this constructive pre-order *) -Definition CRealLt (x y : CReal) : Prop +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)) }. + +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)). Definition CRealGt (x y : CReal) := CRealLt y x. -Definition CReal_appart (x y : CReal) := CRealLt x y \/ CRealLt y x. +Definition CReal_appart (x y : CReal) := sum (CRealLt x y) (CRealLt y x). Infix "<" := CRealLt : CReal_scope. Infix ">" := CRealGt : CReal_scope. @@ -229,9 +234,7 @@ Infix "#" := CReal_appart : CReal_scope. (* This Prop can be extracted as a sigma type *) Lemma CRealLtEpsilon : forall x y : CReal, - x < y - -> { n : positive | Qlt (2 # n) - (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n)) }. + CRealLtProp x y -> x < y. Proof. intros. assert (exists n : nat, n <> O @@ -252,12 +255,18 @@ Proof. (proj1_sig y (S n) - proj1_sig x (S n))); assumption. Qed. +Lemma CRealLtForget : forall x y : CReal, + x < y -> CRealLtProp x y. +Proof. + intros. destruct H. exists x0. exact q. +Qed. + (* CRealLt is decided by the LPO in Type, which is a non-constructive oracle. *) Lemma CRealLt_lpo_dec : forall x y : CReal, (forall (P : nat -> Prop), (forall n, {P n} + {~P n}) -> {n | ~P n} + {forall n, P n}) - -> { CRealLt x y } + { ~CRealLt x y }. + -> 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)) @@ -278,13 +287,13 @@ Qed. (* Alias the quotient order equality *) Definition CRealEq (x y : CReal) : Prop - := ~CRealLt x y /\ ~CRealLt y x. + := (CRealLt x y -> False) /\ (CRealLt y x -> False). Infix "==" := CRealEq : CReal_scope. (* Alias the large order *) Definition CRealLe (x y : CReal) : Prop - := ~CRealLt y x. + := CRealLt y x -> False. Definition CRealGe (x y : CReal) := CRealLe y x. @@ -292,9 +301,9 @@ Infix "<=" := CRealLe : CReal_scope. Infix ">=" := CRealGe : CReal_scope. Notation "x <= y <= z" := (x <= y /\ y <= z) : CReal_scope. -Notation "x <= y < z" := (x <= y /\ y < z) : CReal_scope. -Notation "x < y < z" := (x < y /\ y < z) : CReal_scope. -Notation "x < y <= z" := (x < y /\ y <= z) : CReal_scope. +Notation "x <= y < z" := (prod (x <= y) (y < z)) : CReal_scope. +Notation "x < y < z" := (prod (x < y) (y < z)) : CReal_scope. +Notation "x < y <= z" := (prod (x < y) (y <= z)) : 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)) @@ -460,8 +469,8 @@ Qed. Lemma CRealLt_above : forall (x y : CReal), CRealLt x y - -> exists 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)). + -> { 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)) }. Proof. intros x y [n maj]. pose proof (CRealLt_aboveSig x y n maj). @@ -513,7 +522,7 @@ Proof. unfold Qlt. simpl. unfold Z.lt. auto. apply H. apply Pos.le_max_r. Qed. -Lemma CRealLt_irrefl : forall x:CReal, ~(x < x). +Lemma CRealLt_irrefl : forall x:CReal, x < x -> False. Proof. intros x abs. exact (CRealLt_asym x x abs abs). Qed. @@ -535,10 +544,10 @@ Proof. Qed. Lemma CRealLt_dec : forall x y z : CReal, - CRealLt x y -> { CRealLt x z } + { CRealLt z y }. + CRealLt x y -> CRealLt x z + CRealLt z y. Proof. intros [xn limx] [yn limy] [zn limz] clt. - destruct (CRealLtEpsilon _ _ clt) as [n inf]. + destruct clt as [n inf]. unfold proj1_sig in inf. remember (yn (Pos.to_nat n) - xn (Pos.to_nat n) - (2 # n)) as eps. assert (Qlt 0 eps) as epsPos. @@ -662,11 +671,16 @@ Add Parametric Relation : CReal CRealEq transitivity proved by CRealEq_trans as CRealEq_rel. -Add Parametric Morphism : CRealLt - with signature CRealEq ==> CRealEq ==> iff - as CRealLt_morph. +Instance CRealEq_relT : CRelationClasses.Equivalence CRealEq. +Proof. + split. exact CRealEq_refl. exact CRealEq_sym. exact CRealEq_trans. +Qed. + +Instance CRealLt_morph + : CMorphisms.Proper + (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CRealLt. Proof. - intros. destruct H, H0. split. + intros x y H x0 y0 H0. destruct H, H0. split. - intro. destruct (CRealLt_dec x x0 y). assumption. contradiction. destruct (CRealLt_dec y x0 y0). assumption. assumption. contradiction. @@ -675,22 +689,22 @@ Proof. assumption. assumption. contradiction. Qed. -Add Parametric Morphism : CRealGt - with signature CRealEq ==> CRealEq ==> iff - as CRealGt_morph. +Instance CRealGt_morph + : CMorphisms.Proper + (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CRealGt. Proof. - intros. unfold CRealGt. apply CRealLt_morph; assumption. + intros x y H x0 y0 H0. apply CRealLt_morph; assumption. Qed. -Add Parametric Morphism : CReal_appart - with signature CRealEq ==> CRealEq ==> iff - as CReal_appart_morph. +Instance CReal_appart_morph + : CMorphisms.Proper + (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CReal_appart. Proof. split. - - intros. destruct H1. left. rewrite <- H0, <- H. exact H1. - right. rewrite <- H0, <- H. exact H1. - - intros. destruct H1. left. rewrite H0, H. exact H1. - right. rewrite H0, H. exact H1. + - intros. destruct H1. left. rewrite <- H0, <- H. exact c. + right. rewrite <- H0, <- H. exact c. + - intros. destruct H1. left. rewrite H0, H. exact c. + right. rewrite H0, H. exact c. Qed. Add Parametric Morphism : CRealLe @@ -1108,6 +1122,17 @@ Proof. - apply CReal_plus_proper_r. apply H. Qed. +Instance CReal_plus_morph_T + : CMorphisms.Proper + (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRealEq)) CReal_plus. +Proof. + intros x y H z t H0. apply (CRealEq_trans _ (CReal_plus x t)). + - destruct H0. + split. intro abs. apply CReal_plus_lt_reg_l in abs. contradiction. + intro abs. apply CReal_plus_lt_reg_l in abs. contradiction. + - apply CReal_plus_proper_r. apply H. +Qed. + Lemma CReal_plus_eq_reg_l : forall (r r1 r2 : CReal), CRealEq (CReal_plus r r1) (CReal_plus r r2) -> CRealEq r1 r2. @@ -1424,7 +1449,7 @@ Lemma CReal_mult_lt_0_compat : forall x y : CReal, -> CRealLt (inject_Q 0) y -> CRealLt (inject_Q 0) (CReal_mult x y). Proof. - intros. destruct H, H0. + intros. destruct H as [x0 H], H0 as [x1 H0]. 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]. @@ -1673,6 +1698,13 @@ Proof. apply CReal_isRingExt. Qed. +Instance CReal_mult_morph_T + : CMorphisms.Proper + (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRealEq)) CReal_mult. +Proof. + apply CReal_isRingExt. +Qed. + Add Parametric Morphism : CReal_opp with signature CRealEq ==> CRealEq as CReal_opp_morph. @@ -1680,6 +1712,13 @@ Proof. apply (Ropp_ext CReal_isRingExt). Qed. +Instance CReal_opp_morph_T + : CMorphisms.Proper + (CMorphisms.respectful CRealEq CRealEq) CReal_opp. +Proof. + apply CReal_isRingExt. +Qed. + Add Parametric Morphism : CReal_minus with signature CRealEq ==> CRealEq ==> CRealEq as CReal_minus_morph. @@ -1687,6 +1726,13 @@ Proof. intros. unfold CReal_minus. rewrite H,H0. reflexivity. Qed. +Instance CReal_minus_morph_T + : CMorphisms.Proper + (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRealEq)) CReal_minus. +Proof. + intros x y exy z t ezt. unfold CReal_minus. rewrite exy,ezt. reflexivity. +Qed. + Add Ring CRealRing : CReal_isRing. Lemma CReal_opp_0 : -0 == 0. @@ -1768,15 +1814,15 @@ Proof. - intro abs. apply (CReal_mult_lt_compat_l (-r)) in abs. rewrite <- CReal_opp_mult_distr_l, <- CReal_opp_mult_distr_l, H0 in abs. exact (CRealLt_irrefl _ abs). apply (CReal_plus_lt_reg_l r). - rewrite CReal_plus_opp_r, CReal_plus_comm, CReal_plus_0_l. exact H. + rewrite CReal_plus_opp_r, CReal_plus_comm, CReal_plus_0_l. exact c. - intro abs. apply (CReal_mult_lt_compat_l (-r)) in abs. rewrite <- CReal_opp_mult_distr_l, <- CReal_opp_mult_distr_l, H0 in abs. exact (CRealLt_irrefl _ abs). apply (CReal_plus_lt_reg_l r). - rewrite CReal_plus_opp_r, CReal_plus_comm, CReal_plus_0_l. exact H. + rewrite CReal_plus_opp_r, CReal_plus_comm, CReal_plus_0_l. exact c. - intro abs. apply (CReal_mult_lt_compat_l r) in abs. rewrite H0 in abs. - exact (CRealLt_irrefl _ abs). exact H. + exact (CRealLt_irrefl _ abs). exact c. - intro abs. apply (CReal_mult_lt_compat_l r) in abs. rewrite H0 in abs. - exact (CRealLt_irrefl _ abs). exact H. + exact (CRealLt_irrefl _ abs). exact c. Qed. @@ -1827,15 +1873,24 @@ Proof. intro; destruct n. rewrite CReal_plus_0_l. reflexivity. reflexivity. Qed. +Lemma le_succ_r_T : forall n m : nat, (n <= S m)%nat -> {(n <= m)%nat} + {n = S m}. +Proof. + intros. destruct (le_lt_dec n m). left. exact l. + right. apply Nat.le_succ_r in H. destruct H. + exfalso. apply (le_not_lt n m); assumption. exact H. +Qed. + Lemma lt_INR : forall n m:nat, (n < m)%nat -> INR n < INR m. Proof. induction m. - - intros. inversion H. + - intros. exfalso. inversion H. - intros. unfold lt in H. apply le_S_n in H. destruct m. - inversion H. apply CRealLt_0_1. apply Nat.le_succ_r in H. destruct H. + assert (n = 0)%nat. + { inversion H. reflexivity. } + subst n. apply CRealLt_0_1. apply le_succ_r_T in H. destruct H. rewrite S_INR. apply (CRealLt_trans _ (INR (S m) + 0)). rewrite CReal_plus_comm, CReal_plus_0_l. apply IHm. - apply le_n_S. exact H. + apply le_n_S. exact l. apply CReal_plus_lt_compat_l. exact CRealLt_0_1. subst n. rewrite (S_INR (S m)). rewrite <- (CReal_plus_0_l). rewrite (CReal_plus_comm 0), CReal_plus_assoc. @@ -1881,9 +1936,9 @@ Proof. Qed. (**********) -Lemma IZN : forall n:Z, (0 <= n)%Z -> exists m : nat, n = Z.of_nat m. +Lemma IZN : forall n:Z, (0 <= n)%Z -> { m : nat | n = Z.of_nat m }. Proof. - intros z; idtac; apply Z_of_nat_complete; assumption. + intros. exists (Z.to_nat n). rewrite Z2Nat.id. reflexivity. assumption. Qed. Lemma INR_IPR : forall p, INR (Pos.to_nat p) == IPR p. @@ -2067,7 +2122,7 @@ Qed. (* Axiom Rarchimed_constr *) Lemma Rarchimedean : forall x:CReal, - { n:Z | x < IZR n /\ IZR n < x+2 }. + { n:Z & x < IZR n < x+2 }. Proof. (* Locate x within 1/4 and pick the first integer above this interval. *) intros [xn limx]. @@ -2110,7 +2165,7 @@ Proof. Qed. Lemma CRealLtDisjunctEpsilon : forall a b c d : CReal, - (CRealLt a b \/ CRealLt c d) -> { CRealLt a b } + { CRealLt c d }. + (CRealLtProp a b \/ CRealLtProp c d) -> CRealLt a b + CRealLt c d. Proof. intros. assert (exists n : nat, n <> O /\ @@ -2192,7 +2247,7 @@ Definition CRealNegShift (x : CReal) -> { y : prod positive CReal | CRealEq x (snd y) /\ forall n:nat, Qlt (proj1_sig (snd y) n) (-1 # fst y) }. Proof. - intro xNeg. apply CRealLtEpsilon in xNeg. + intro xNeg. pose proof (CRealLt_aboveSig x (inject_Q 0)). pose proof (CRealShiftReal x). pose proof (CRealShiftEqual x). @@ -2229,7 +2284,7 @@ Definition CRealPosShift (x : CReal) -> { y : prod positive CReal | CRealEq x (snd y) /\ forall n:nat, Qlt (1 # fst y) (proj1_sig (snd y) n) }. Proof. - intro xPos. apply CRealLtEpsilon in xPos. + intro xPos. pose proof (CRealLt_aboveSig (inject_Q 0) x). pose proof (CRealShiftReal x). pose proof (CRealShiftEqual x). @@ -2410,7 +2465,7 @@ Qed. Definition CReal_inv (x : CReal) (xnz : x # 0) : CReal. Proof. - apply CRealLtDisjunctEpsilon in xnz. destruct xnz as [xNeg | xPos]. + 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))). @@ -2428,10 +2483,10 @@ Lemma CReal_inv_0_lt_compat 0 < r -> 0 < ((/ r) rnz). Proof. intros. unfold CReal_inv. simpl. - destruct (CRealLtDisjunctEpsilon r (inject_Q 0) (inject_Q 0) r rnz). + destruct rnz. - exfalso. apply CRealLt_asym in H. contradiction. - destruct (CRealPosShift r c) as [[k rpos] [req maj]]. - clear req. clear rnz. destruct rpos as [rn cau]; simpl in maj. + clear req. destruct rpos as [rn cau]; simpl in maj. unfold CRealLt; simpl. destruct (Qarchimedean (rn 1%nat)) as [A majA]. exists (2 * (A + 1))%positive. unfold Qminus. rewrite Qplus_0_r. @@ -2485,7 +2540,7 @@ Lemma CReal_inv_l : forall (r:CReal) (rnz : r # 0), ((/ r) rnz) * r == 1. Proof. intros. unfold CReal_inv; simpl. - destruct (CRealLtDisjunctEpsilon r (inject_Q 0) (inject_Q 0) r rnz). + destruct rnz. - (* r < 0 *) destruct (CRealNegShift r c) as [[k rneg] [req maj]]. simpl in req. apply CRealEq_diff. apply CRealEq_modindep. apply (QSeqEquivEx_trans _ @@ -2606,7 +2661,7 @@ Qed. Lemma CReal_mult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2. Proof. intros z x y H H0. - apply (CReal_mult_lt_compat_l ((/z) (or_intror H))) in H0. + apply (CReal_mult_lt_compat_l ((/z) (inr H))) in H0. repeat rewrite <- CReal_mult_assoc in H0. rewrite CReal_inv_l in H0. repeat rewrite CReal_mult_1_l in H0. apply H0. apply CReal_inv_0_lt_compat. exact H. @@ -2646,7 +2701,7 @@ Fixpoint pow (r:CReal) (n:nat) : CReal := (**********) Definition IQR (q:Q) : CReal := match q with - | Qmake a b => IZR a * (CReal_inv (IPR b)) (or_intror (IPR_pos b)) + | Qmake a b => IZR a * (CReal_inv (IPR b)) (inr (IPR_pos b)) end. Arguments IQR q%Q : simpl never. @@ -2659,17 +2714,17 @@ Lemma plus_IQR : forall n m:Q, IQR (n + m) == IQR n + IQR m. Proof. intros. destruct n,m; unfold Qplus,IQR; simpl. rewrite plus_IZR. repeat rewrite mult_IZR. - setoid_replace ((/ IPR (Qden * Qden0)) (or_intror (IPR_pos (Qden * Qden0)))) - with ((/ IPR Qden) (or_intror (IPR_pos Qden)) - * (/ IPR Qden0) (or_intror (IPR_pos Qden0))). + setoid_replace ((/ IPR (Qden * Qden0)) (inr (IPR_pos (Qden * Qden0)))) + with ((/ IPR Qden) (inr (IPR_pos Qden)) + * (/ IPR Qden0) (inr (IPR_pos Qden0))). rewrite CReal_mult_plus_distr_r. repeat rewrite CReal_mult_assoc. rewrite <- (CReal_mult_assoc (IZR (Z.pos Qden))). rewrite CReal_inv_r, CReal_mult_1_l. - rewrite (CReal_mult_comm ((/IPR Qden) (or_intror (IPR_pos Qden)))). + rewrite (CReal_mult_comm ((/IPR Qden) (inr (IPR_pos Qden)))). rewrite <- (CReal_mult_assoc (IZR (Z.pos Qden0))). rewrite CReal_inv_r, CReal_mult_1_l. reflexivity. unfold IZR. rewrite <- (CReal_inv_mult_distr - _ _ _ _ (or_intror (CReal_mult_lt_0_compat _ _ (IPR_pos _) (IPR_pos _)))). + _ _ _ _ (inr (CReal_mult_lt_0_compat _ _ (IPR_pos _) (IPR_pos _)))). apply Rinv_eq_compat. apply mult_IPR. Qed. @@ -2721,8 +2776,8 @@ Qed. Lemma IQR_nonneg : forall q:Q, Qle 0 q -> 0 <= (IQR q). Proof. - intros [a b] H. unfold IQR;simpl. - apply (CRealLe_trans _ ((/ IPR b) (or_intror (IPR_pos b)) * 0)). + intros [a b] H. unfold IQR. + apply (CRealLe_trans _ ((/ IPR b) (inr (IPR_pos b)) * 0)). rewrite CReal_mult_0_r. apply CRealLe_refl. rewrite (CReal_mult_comm (IZR a)). apply CReal_mult_le_compat_l_half. apply CReal_inv_0_lt_compat. apply IPR_pos. @@ -2742,7 +2797,7 @@ Add Parametric Morphism : IQR with signature Qeq ==> CRealEq as IQR_morph. Proof. - intros. destruct x,y; unfold IQR; simpl. + intros. destruct x,y; unfold IQR. unfold Qeq in H; simpl in H. apply (CReal_mult_eq_reg_r (IZR (Z.pos Qden))). 2: right; apply IPR_pos. @@ -2756,9 +2811,26 @@ Proof. rewrite <- H. rewrite Zmult_comm. reflexivity. Qed. +Instance IQR_morph_T + : CMorphisms.Proper + (CMorphisms.respectful Qeq CRealEq) IQR. +Proof. + intros x y H. destruct x,y; unfold IQR. + unfold Qeq in H; simpl in H. + apply (CReal_mult_eq_reg_r (IZR (Z.pos Qden))). + 2: right; apply IPR_pos. + rewrite CReal_mult_assoc. rewrite CReal_inv_l. rewrite CReal_mult_1_r. + rewrite (CReal_mult_comm (IZR Qnum0)). + apply (CReal_mult_eq_reg_l (IZR (Z.pos Qden0))). + right; apply IPR_pos. + rewrite <- CReal_mult_assoc, <- CReal_mult_assoc, CReal_inv_r. + rewrite CReal_mult_1_l. + repeat rewrite <- mult_IZR. + rewrite <- H. rewrite Zmult_comm. reflexivity. +Qed. Lemma CReal_invQ : forall (b : positive) (pos : Qlt 0 (Z.pos b # 1)), - CRealEq (CReal_inv (inject_Q (Z.pos b # 1)) (or_intror (CReal_injectQPos (Z.pos b # 1) pos))) + CRealEq (CReal_inv (inject_Q (Z.pos b # 1)) (inr (CReal_injectQPos (Z.pos b # 1) pos))) (inject_Q (1 # b)). Proof. intros. @@ -2776,12 +2848,12 @@ Qed. Lemma FinjectQ_CReal : forall q : Q, IQR q == inject_Q q. Proof. - intros [a b]. unfold IQR; simpl. + intros [a b]. unfold IQR. pose proof (CReal_iterate_one (Pos.to_nat b)). rewrite positive_nat_Z in H. simpl in H. assert (0 < Z.pos b # 1)%Q as pos. reflexivity. apply (CRealEq_trans _ (CReal_mult (IZR a) - (CReal_inv (inject_Q (Z.pos b # 1)) (or_intror (CReal_injectQPos (Z.pos b # 1) pos))))). + (CReal_inv (inject_Q (Z.pos b # 1)) (inr (CReal_injectQPos (Z.pos b # 1) pos))))). - apply CReal_mult_proper_l. apply (CReal_mult_eq_reg_l (IPR b)). right. apply IPR_pos. @@ -2812,7 +2884,7 @@ Proof. Qed. Lemma CRealArchimedean - : forall x:CReal, { n:Z | CRealLt x (gen_phiZ (inject_Q 0) (inject_Q 1) CReal_plus + : forall x:CReal, { n:Z & CRealLt x (gen_phiZ (inject_Q 0) (inject_Q 1) CReal_plus CReal_mult CReal_opp n) }. Proof. intros [xn limx]. destruct (Qarchimedean (xn 1%nat)) as [k kmaj]. diff --git a/theories/Reals/ConstructiveRIneq.v b/theories/Reals/ConstructiveRIneq.v index e96808db2a..95fb991ffe 100644 --- a/theories/Reals/ConstructiveRIneq.v +++ b/theories/Reals/ConstructiveRIneq.v @@ -39,22 +39,20 @@ Proof. exact CRealLt_trans. intros. destruct (CRealLt_dec x z y H). left. exact c. right. exact c. } - assert (forall r r1 r2 : CReal, CRealLt r1 r2 <-> CRealLt (r + r1) (r + r2)) - as plusLtCompat. - { split. intros. apply CReal_plus_lt_compat_l. exact H. - intros. apply CReal_plus_lt_reg_l in H. exact H. } apply (Build_ConstructiveReals - CReal CRealLt lin + CReal CRealLt lin CRealLtProp + CRealLtEpsilon CRealLtForget CRealLtDisjunctEpsilon (inject_Q 0) (inject_Q 1) CReal_plus CReal_opp CReal_mult CReal_isRing CReal_isRingExt CRealLt_0_1 - plusLtCompat CReal_mult_lt_0_compat + CReal_plus_lt_compat_l CReal_plus_lt_reg_l + CReal_mult_lt_0_compat CReal_inv CReal_inv_l CReal_inv_0_lt_compat CRealArchimedean). - intros. destruct (Rcauchy_complete xn) as [l cv]. intro n. apply (H (IQR (1#n))). apply IQR_pos. reflexivity. exists l. intros eps epsPos. - destruct (Rup_nat ((/eps) (or_intror epsPos))) as [n nmaj]. + destruct (Rup_nat ((/eps) (inr epsPos))) as [n nmaj]. specialize (cv (Pos.of_nat (S n))) as [p pmaj]. exists p. intros. specialize (pmaj i H0). unfold absSmall in pmaj. apply (CReal_mult_lt_compat_l eps) in nmaj. @@ -73,16 +71,16 @@ Proof. apply IPR_pos. rewrite CReal_inv_r, <- INR_IPR, Nat2Pos.id. 2: discriminate. apply (CRealLt_trans _ (INR n * eps) _ nmaj). apply CReal_mult_lt_compat_r. exact epsPos. apply lt_INR, le_refl. - - exact CRealLt_lpo_dec. - exact sig_lub. Qed. (* Keep it opaque to possibly change the implementation later *) Definition R := CRcarrier CR. Definition Req := orderEq R (CRlt CR). -Definition Rle (x y : R) := ~CRlt CR y x. -Definition Rge (x y : R) := ~CRlt CR x y. +Definition Rle (x y : R) := CRlt CR y x -> False. +Definition Rge (x y : R) := CRlt CR x y -> False. Definition Rlt := CRlt CR. +Definition RltProp := CRltProp CR. Definition Rgt (x y : R) := CRlt CR y x. Definition Rappart := orderAppart R (CRlt CR). @@ -94,15 +92,25 @@ Infix "<=" := Rle : R_scope_constr. Infix ">=" := Rge : R_scope_constr. Notation "x <= y <= z" := (x <= y /\ y <= z) : R_scope_constr. -Notation "x <= y < z" := (x <= y /\ y < z) : R_scope_constr. -Notation "x < y < z" := (x < y /\ y < z) : R_scope_constr. -Notation "x < y <= z" := (x < y /\ y <= z) : R_scope_constr. +Notation "x <= y < z" := (prod (x <= y) (y < z)) : R_scope_constr. +Notation "x < y < z" := (prod (x < y) (y < z)) : R_scope_constr. +Notation "x < y <= z" := (prod (x < y) (y <= z)) : R_scope_constr. + +Lemma Rlt_epsilon : forall x y : R, RltProp x y -> x < y. +Proof. + exact (CRltEpsilon CR). +Qed. + +Lemma Rlt_forget : forall x y : R, x < y -> RltProp x y. +Proof. + exact (CRltForget CR). +Qed. Lemma Rle_refl : forall x : R, x <= x. Proof. intros. intro abs. - destruct (CRltLinear CR), a. - specialize (H x x abs). contradiction. + destruct (CRltLinear CR), p. + exact (f x x abs abs). Qed. Hint Immediate Rle_refl: rorders. @@ -118,7 +126,7 @@ Qed. Lemma Req_trans : forall x y z : R, x == y -> y == z -> x == z. Proof. - intros. destruct H,H0. destruct (CRltLinear CR), a. split. + intros. destruct H,H0. destruct (CRltLinear CR), p. split. - intro abs. destruct (s _ y _ abs); contradiction. - intro abs. destruct (s _ y _ abs); contradiction. Qed. @@ -129,17 +137,22 @@ Add Parametric Relation : R Req transitivity proved by Req_trans as Req_rel. +Instance Req_relT : CRelationClasses.Equivalence Req. +Proof. + split. exact Req_refl. exact Req_sym. exact Req_trans. +Qed. + Lemma linear_order_T : forall x y z : R, - x < z -> {x < y} + {y < z}. + x < z -> (x < y) + (y < z). Proof. intros. destruct (CRltLinear CR). apply s. exact H. Qed. -Add Parametric Morphism : Rlt - with signature Req ==> Req ==> iff - as Rlt_morph. +Instance Rlt_morph + : CMorphisms.Proper + (CMorphisms.respectful Req (CMorphisms.respectful Req CRelationClasses.iffT)) Rlt. Proof. - intros. destruct H, H0. split. + intros x y H x0 y0 H0. destruct H, H0. split. - intro. destruct (linear_order_T x y x0). assumption. contradiction. destruct (linear_order_T y y0 x0). assumption. assumption. contradiction. @@ -148,22 +161,37 @@ Proof. assumption. assumption. contradiction. Qed. -Add Parametric Morphism : Rgt - with signature Req ==> Req ==> iff - as Rgt_morph. +Instance RltProp_morph + : Morphisms.Proper + (Morphisms.respectful Req (Morphisms.respectful Req iff)) RltProp. Proof. - intros. unfold Rgt. apply Rlt_morph; assumption. + intros x y H x0 y0 H0. destruct H, H0. split. + - intro. destruct (linear_order_T x y x0). + apply Rlt_epsilon. assumption. + contradiction. destruct (linear_order_T y y0 x0). + assumption. apply Rlt_forget. assumption. contradiction. + - intro. destruct (linear_order_T y x y0). + apply Rlt_epsilon. assumption. + contradiction. destruct (linear_order_T x x0 y0). + assumption. apply Rlt_forget. assumption. contradiction. Qed. -Add Parametric Morphism : Rappart - with signature Req ==> Req ==> iff - as Rappart_morph. +Instance Rgt_morph + : CMorphisms.Proper + (CMorphisms.respectful Req (CMorphisms.respectful Req CRelationClasses.iffT)) Rgt. +Proof. + intros x y H x0 y0 H0. unfold Rgt. apply Rlt_morph; assumption. +Qed. + +Instance Rappart_morph + : CMorphisms.Proper + (CMorphisms.respectful Req (CMorphisms.respectful Req CRelationClasses.iffT)) Rappart. Proof. split. - - intros. destruct H1. left. rewrite <- H0, <- H. exact H1. - right. rewrite <- H0, <- H. exact H1. - - intros. destruct H1. left. rewrite H0, H. exact H1. - right. rewrite H0, H. exact H1. + - intros. destruct H1. left. rewrite <- H0, <- H. exact c. + right. rewrite <- H0, <- H. exact c. + - intros. destruct H1. left. rewrite H0, H. exact c. + right. rewrite H0, H. exact c. Qed. Add Parametric Morphism : Rle @@ -189,7 +217,6 @@ Definition Rplus := CRplus CR. Definition Rmult := CRmult CR. Definition Rinv := CRinv CR. Definition Ropp := CRopp CR. -Definition Rminus := CRminus CR. Add Parametric Morphism : Rplus with signature Req ==> Req ==> Req @@ -198,6 +225,13 @@ Proof. apply CRisRingExt. Qed. +Instance Rplus_morph_T + : CMorphisms.Proper + (CMorphisms.respectful Req (CMorphisms.respectful Req Req)) Rplus. +Proof. + apply CRisRingExt. +Qed. + Add Parametric Morphism : Rmult with signature Req ==> Req ==> Req as Rmult_morph. @@ -205,22 +239,30 @@ Proof. apply CRisRingExt. Qed. +Instance Rmult_morph_T + : CMorphisms.Proper + (CMorphisms.respectful Req (CMorphisms.respectful Req Req)) Rmult. +Proof. + apply CRisRingExt. +Qed. + Add Parametric Morphism : Ropp with signature Req ==> Req as Ropp_morph. Proof. - apply (Ropp_ext (CRisRingExt CR)). + apply CRisRingExt. Qed. -Add Parametric Morphism : Rminus - with signature Req ==> Req ==> Req - as Rminus_morph. +Instance Ropp_morph_T + : CMorphisms.Proper + (CMorphisms.respectful Req Req) Ropp. Proof. - intros. unfold Rminus, CRminus. rewrite H,H0. reflexivity. + apply CRisRingExt. Qed. Infix "+" := Rplus : R_scope_constr. Notation "- x" := (Ropp x) : R_scope_constr. +Definition Rminus (r1 r2:R) : R := r1 + - r2. Infix "-" := Rminus : R_scope_constr. Infix "*" := Rmult : R_scope_constr. Notation "/ x" := (CRinv CR x) (at level 35, right associativity) : R_scope_constr. @@ -228,6 +270,14 @@ Notation "/ x" := (CRinv CR x) (at level 35, right associativity) : R_scope_cons Notation "0" := (CRzero CR) : R_scope_constr. Notation "1" := (CRone CR) : R_scope_constr. +Add Parametric Morphism : Rminus + with signature Req ==> Req ==> Req + as Rminus_morph. +Proof. + intros. unfold Rminus, CRminus. rewrite H,H0. reflexivity. +Qed. + + (* Help Add Ring to find the correct equality *) Lemma RisRing : ring_theory 0 1 Rplus Rmult @@ -271,16 +321,16 @@ Proof. intros. ring. Qed. Definition Rlt_0_1 := CRzero_lt_one CR. -Lemma Rlt_asym : forall x y :R, x < y -> ~(y < x). +Lemma Rlt_asym : forall x y :R, x < y -> y < x -> False. Proof. - intros. intro abs. destruct (CRltLinear CR), a. - apply (H0 x y); assumption. + intros. destruct (CRltLinear CR), p. + apply (f x y); assumption. Qed. Lemma Rlt_trans : forall x y z : R, x < y -> y < z -> x < z. Proof. - intros. destruct (CRltLinear CR), a. - apply (H2 x y); assumption. + intros. destruct (CRltLinear CR), p. + apply (c x y); assumption. Qed. Lemma Rplus_lt_compat_l : forall x y z : R, @@ -297,13 +347,13 @@ Qed. Lemma Rplus_lt_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2. Proof. - intros. apply CRplus_lt_compat_l in H. exact H. + intros. apply CRplus_lt_reg_l in H. exact H. Qed. Lemma Rmult_lt_compat_l : forall x y z : R, 0 < x -> y < z -> x * y < x * z. Proof. - intros. rewrite (CRplus_lt_compat_l CR (- (x * y))). + intros. apply (CRplus_lt_reg_l CR (- (x * y))). rewrite Rplus_comm. pose proof Rplus_opp_r. rewrite H1. rewrite Rmult_comm, Ropp_mult_distr_l, Rmult_comm. @@ -365,13 +415,13 @@ Hint Immediate Rge_refl: rorders. (** Irreflexivity of the strict order *) -Lemma Rlt_irrefl : forall r, ~ r < r. +Lemma Rlt_irrefl : forall r, r < r -> False. Proof. intros r H; eapply Rlt_asym; eauto. Qed. Hint Resolve Rlt_irrefl: creal. -Lemma Rgt_irrefl : forall r, ~ r > r. +Lemma Rgt_irrefl : forall r, r > r -> False. Proof. exact Rlt_irrefl. Qed. Lemma Rlt_not_eq : forall r1 r2, r1 < r2 -> r1 <> r2. @@ -385,11 +435,11 @@ Proof. Qed. (**********) -Lemma Rlt_dichotomy_converse : forall r1 r2, r1 < r2 \/ r1 > r2 -> r1 <> r2. +Lemma Rlt_dichotomy_converse : forall r1 r2, ((r1 < r2) + (r1 > r2)) -> r1 <> r2. Proof. intros. destruct H. - - intro abs. subst r2. exact (Rlt_irrefl r1 H). - - intro abs. subst r2. exact (Rlt_irrefl r1 H). + - intro abs. subst r2. exact (Rlt_irrefl r1 r). + - intro abs. subst r2. exact (Rlt_irrefl r1 r). Qed. Hint Resolve Rlt_dichotomy_converse: creal. @@ -447,22 +497,22 @@ Hint Immediate Rgt_lt: rorders. (**********) -Lemma Rnot_lt_le : forall r1 r2, ~ r1 < r2 -> r2 <= r1. +Lemma Rnot_lt_le : forall r1 r2, (r1 < r2 -> False) -> r2 <= r1. Proof. - intros. intro abs. contradiction. + intros. exact H. Qed. -Lemma Rnot_gt_le : forall r1 r2, ~ r1 > r2 -> r1 <= r2. +Lemma Rnot_gt_le : forall r1 r2, (r1 > r2 -> False) -> r1 <= r2. Proof. intros. intro abs. contradiction. Qed. -Lemma Rnot_gt_ge : forall r1 r2, ~ r1 > r2 -> r2 >= r1. +Lemma Rnot_gt_ge : forall r1 r2, (r1 > r2 -> False) -> r2 >= r1. Proof. intros. intro abs. contradiction. Qed. -Lemma Rnot_lt_ge : forall r1 r2, ~ r1 < r2 -> r1 >= r2. +Lemma Rnot_lt_ge : forall r1 r2, (r1 < r2 -> False) -> r1 >= r2. Proof. intros. intro abs. contradiction. Qed. @@ -485,19 +535,19 @@ Hint Immediate Rlt_not_ge: creal. Lemma Rgt_not_ge : forall r1 r2, r2 > r1 -> ~ r1 >= r2. Proof. exact Rlt_not_ge. Qed. -Lemma Rle_not_lt : forall r1 r2, r2 <= r1 -> ~ r1 < r2. +Lemma Rle_not_lt : forall r1 r2, r2 <= r1 -> r1 < r2 -> False. Proof. intros r1 r2. generalize (Rlt_asym r1 r2) (Rlt_dichotomy_converse r1 r2). unfold CRealLe; intuition. Qed. -Lemma Rge_not_lt : forall r1 r2, r1 >= r2 -> ~ r1 < r2. -Proof. intros; apply Rle_not_lt; auto with creal. Qed. +Lemma Rge_not_lt : forall r1 r2, r1 >= r2 -> r1 < r2 -> False. +Proof. intros; apply (Rle_not_lt r1 r2); auto with creal. Qed. -Lemma Rle_not_gt : forall r1 r2, r1 <= r2 -> ~ r1 > r2. +Lemma Rle_not_gt : forall r1 r2, r1 <= r2 -> r1 > r2 -> False. Proof. do 2 intro; apply Rle_not_lt. Qed. -Lemma Rge_not_gt : forall r1 r2, r2 >= r1 -> ~ r1 > r2. +Lemma Rge_not_gt : forall r1 r2, r2 >= r1 -> r1 > r2 -> False. Proof. do 2 intro; apply Rge_not_lt. Qed. (**********) @@ -529,7 +579,7 @@ Hint Immediate Req_ge_sym: creal. (** Remark: [Rlt_asym] is an axiom *) -Lemma Rgt_asym : forall r1 r2, r1 > r2 -> ~ r2 > r1. +Lemma Rgt_asym : forall r1 r2, r1 > r2 -> r2 > r1 -> False. Proof. do 2 intro; apply Rlt_asym. Qed. @@ -755,17 +805,17 @@ Qed. (**********) Lemma Rmult_integral_contrapositive : - forall r1 r2, r1 # 0 /\ r2 # 0 -> (r1 * r2) # 0. + forall r1 r2, (prod (r1 # 0) (r2 # 0)) -> (r1 * r2) # 0. Proof. assert (forall r, 0 > r -> 0 < - r). { intros. rewrite <- (Rplus_opp_l r), <- (Rplus_0_r (-r)), Rplus_assoc. apply Rplus_lt_compat_l. rewrite Rplus_0_l. apply H. } - intros. destruct H0, H0, H1. + intros. destruct H0, r, r0. - right. setoid_replace (r1*r2) with (-r1 * -r2). 2: ring. rewrite <- (Rmult_0_r (-r1)). apply Rmult_lt_compat_l; apply H; assumption. - left. rewrite <- (Rmult_0_r r2). - rewrite Rmult_comm. apply (Rmult_lt_compat_l). apply H1. apply H0. - - left. rewrite <- (Rmult_0_r r1). apply (Rmult_lt_compat_l). apply H0. apply H1. + rewrite Rmult_comm. apply (Rmult_lt_compat_l). apply c0. apply c. + - left. rewrite <- (Rmult_0_r r1). apply (Rmult_lt_compat_l). apply c. apply c0. - right. rewrite <- (Rmult_0_r r1). apply Rmult_lt_compat_l; assumption. Qed. Hint Resolve Rmult_integral_contrapositive: creal. @@ -870,13 +920,13 @@ Qed. Lemma Rminus_0_r : forall r, r - 0 == r. Proof. - intro; ring. + intro r. unfold Rminus. ring. Qed. Hint Resolve Rminus_0_r: creal. Lemma Rminus_0_l : forall r, 0 - r == - r. Proof. - intro; ring. + intro r. unfold Rminus. ring. Qed. Hint Resolve Rminus_0_l: creal. @@ -895,7 +945,7 @@ Qed. (**********) Lemma Rminus_diag_eq : forall r1 r2, r1 == r2 -> r1 - r2 == 0. Proof. - intros; rewrite H; ring. + intros; rewrite H; unfold Rminus; ring. Qed. Hint Resolve Rminus_diag_eq: creal. @@ -909,8 +959,8 @@ Hint Immediate Rminus_diag_uniq: creal. Lemma Rminus_diag_uniq_sym : forall r1 r2, r2 - r1 == 0 -> r1 == r2. Proof. - intros; generalize (Rminus_diag_uniq r2 r1 H); clear H; intro H; rewrite H; - ring. + intros; generalize (Rminus_diag_uniq r2 r1 H); clear H; + intro H; rewrite H; reflexivity. Qed. Hint Immediate Rminus_diag_uniq_sym: creal. @@ -1338,7 +1388,7 @@ Qed. (** *** Cancellation *) -Lemma Rinv_0_lt_compat : forall r (rpos : 0 < r), 0 < (/ r) (or_intror rpos). +Lemma Rinv_0_lt_compat : forall r (rpos : 0 < r), 0 < (/ r) (inr rpos). Proof. intros. apply CRinv_0_lt_compat. exact rpos. Qed. @@ -1346,7 +1396,7 @@ Qed. Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2. Proof. intros z x y H H0. - apply (Rmult_lt_compat_l ((/z) (or_intror H))) in H0. + apply (Rmult_lt_compat_l ((/z) (inr H))) in H0. repeat rewrite <- Rmult_assoc in H0. rewrite Rinv_l in H0. repeat rewrite Rmult_1_l in H0. apply H0. apply Rinv_0_lt_compat. @@ -1407,13 +1457,17 @@ Qed. Lemma Rle_minus : forall r1 r2, r1 <= r2 -> r1 - r2 <= 0. Proof. intros. intro abs. apply (Rplus_lt_compat_l r2) in abs. - ring_simplify in abs. contradiction. + unfold Rminus in abs. + rewrite Rplus_0_r, Rplus_comm, Rplus_assoc, Rplus_opp_l, Rplus_0_r in abs. + contradiction. Qed. Lemma Rge_minus : forall r1 r2, r1 >= r2 -> r1 - r2 >= 0. Proof. intros. intro abs. apply (Rplus_lt_compat_l r2) in abs. - ring_simplify in abs. contradiction. + unfold Rminus in abs. + rewrite Rplus_0_r, Rplus_comm, Rplus_assoc, Rplus_opp_l, Rplus_0_r in abs. + contradiction. Qed. (**********) @@ -1490,9 +1544,9 @@ Qed. Lemma Rinv_neq_0_compat : forall r (rnz : r # 0), ((/ r) rnz) # 0. Proof. intros. destruct rnz. left. - assert (0 < (/-r) (or_intror (Ropp_0_gt_lt_contravar _ c))). + assert (0 < (/-r) (inr (Ropp_0_gt_lt_contravar _ c))). { apply Rinv_0_lt_compat. } - rewrite <- (Ropp_inv_permute _ (or_introl c)) in H. + rewrite <- (Ropp_inv_permute _ (inl c)) in H. apply Ropp_lt_cancel. rewrite Ropp_0. exact H. right. apply Rinv_0_lt_compat. Qed. @@ -1565,9 +1619,9 @@ Qed. (** ** Order and inverse *) (*********************************************************) -Lemma Rinv_lt_0_compat : forall r (rneg : r < 0), (/ r) (or_introl rneg) < 0. +Lemma Rinv_lt_0_compat : forall r (rneg : r < 0), (/ r) (inl rneg) < 0. Proof. - intros. assert (0 < (/-r) (or_intror (Ropp_0_gt_lt_contravar r rneg))). + intros. assert (0 < (/-r) (inr (Ropp_0_gt_lt_contravar r rneg))). { apply Rinv_0_lt_compat. } rewrite <- Ropp_inv_permute in H. rewrite <- Ropp_0 in H. apply Ropp_lt_cancel in H. apply H. @@ -1617,12 +1671,14 @@ Qed. Lemma lt_INR : forall n m:nat, (n < m)%nat -> INR n < INR m. Proof. induction m. - - intros. inversion H. + - intros. exfalso. inversion H. - intros. unfold lt in H. apply le_S_n in H. destruct m. - inversion H. apply Rlt_0_1. apply Nat.le_succ_r in H. destruct H. + assert (n = 0)%nat. + { inversion H. reflexivity. } + subst n. apply Rlt_0_1. apply le_succ_r_T in H. destruct H. rewrite S_INR. apply (Rlt_trans _ (INR (S m) + 0)). rewrite Rplus_comm, Rplus_0_l. apply IHm. - apply le_n_S. exact H. + apply le_n_S. exact l. apply Rplus_lt_compat_l. exact Rlt_0_1. subst n. rewrite (S_INR (S m)). rewrite <- (Rplus_0_l). rewrite (Rplus_comm 0), Rplus_assoc. @@ -1655,7 +1711,7 @@ Proof. intros. rewrite <- minus_n_O. simpl. unfold Rminus, CRminus. rewrite Ropp_0, Rplus_0_r. reflexivity. intros; repeat rewrite S_INR; simpl. - unfold CReal_minus. rewrite H0. ring. exact le. + rewrite H0. unfold Rminus. ring. exact le. Qed. (*********) @@ -1702,8 +1758,7 @@ Proof. now induction n as [|n IHn];[ | simpl; rewrite mult_INR, IHn]. Qed. (*********) Lemma lt_0_INR : forall n:nat, (0 < n)%nat -> 0 < INR n. Proof. - simple induction 1; intros. apply Rlt_0_1. - rewrite S_INR. apply (Rlt_trans _ (INR m)). apply H1. apply Rlt_plus_1. + intros. apply (lt_INR 0). exact H. Qed. Hint Resolve lt_0_INR: creal. @@ -1777,9 +1832,10 @@ Hint Resolve not_0_INR: creal. Lemma not_INR : forall n m:nat, n <> m -> INR n # INR m. Proof. - intros n m H; case (le_or_lt n m); intros H1. + intros n m H; case (le_lt_dec n m); intros H1. + left. apply lt_INR. case (le_lt_or_eq _ _ H1); intros H2. - left. apply lt_INR. exact H2. contradiction. + exact H2. contradiction. right. apply lt_INR. exact H1. Qed. Hint Resolve not_INR: creal. @@ -1853,7 +1909,7 @@ Proof. rewrite <- 3!INR_IPR, Pos2Nat.inj_sub. rewrite minus_INR. 2: (now apply lt_le_weak, Pos2Nat.inj_lt). - ring. trivial. + unfold Rminus. ring. trivial. Qed. Lemma plus_IPR : forall n m:positive, IPR (n + m) == IPR n + IPR m. @@ -1998,10 +2054,9 @@ Qed. (**********) Lemma not_0_IZR : forall n:Z, n <> 0%Z -> IZR n # 0. Proof. - intros. destruct (Z.lt_trichotomy n 0). - left. apply (IZR_lt n 0). exact H0. - destruct H0. contradiction. - right. apply (IZR_lt 0 n). exact H0. + intros. destruct n. exfalso. apply H. reflexivity. + right. apply (IZR_lt 0). reflexivity. + left. apply (IZR_lt _ 0). reflexivity. Qed. (*********) @@ -2033,22 +2088,27 @@ Qed. (**********) Lemma IZR_ge : forall n m:Z, (n >= m)%Z -> IZR n >= IZR m. Proof. - intros m n H; apply Rnot_lt_ge; red; intro. - generalize (lt_IZR m n H0); intro; omega. + intros m n H; apply Rnot_lt_ge. intro abs. + apply lt_IZR in abs. omega. Qed. Lemma IZR_le : forall n m:Z, (n <= m)%Z -> IZR n <= IZR m. Proof. - intros m n H; apply Rnot_gt_le; red; intro. - unfold CRealGt in H0; generalize (lt_IZR n m H0); intro; omega. + intros m n H; apply Rnot_lt_ge. intro abs. + apply lt_IZR in abs. omega. Qed. Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 # IZR z2. Proof. - intros. destruct (Z.lt_trichotomy z1 z2). - left. apply IZR_lt. exact H0. - destruct H0. contradiction. - right. apply IZR_lt. exact H0. + intros. destruct (not_0_IZR (z1-z2)). + intro abs. apply H. rewrite <- (Z.add_cancel_r _ _ (-z2)). + ring_simplify. exact abs. + left. apply IZR_lt. apply (lt_IZR _ 0) in c. + rewrite (Z.add_lt_mono_r _ _ (-z2)). + ring_simplify. exact c. + right. apply IZR_lt. apply (lt_IZR 0) in c. + rewrite (Z.add_lt_mono_l _ _ (-z2)). + ring_simplify. rewrite Z.add_comm. exact c. Qed. Hint Extern 0 (IZR _ <= IZR _) => apply IZR_le, Zle_bool_imp_le, eq_refl : creal. @@ -2072,7 +2132,7 @@ Proof. intros r z x [H1 H2] [H3 H4]. cut ((z - x)%Z = 0%Z); auto with zarith. apply one_IZR_lt1. - rewrite <- Z_R_minus; split. + split; rewrite <- Z_R_minus. setoid_replace (-(1)) with (r - (r + 1)). unfold CReal_minus; apply Rplus_lt_le_compat; auto with creal. ring. @@ -2095,7 +2155,7 @@ Lemma tech_single_z_r_R1 : forall r (n:Z), r < IZR n -> IZR n <= r + 1 -> - (exists s : Z, s <> n /\ r < IZR s /\ IZR s <= r + 1) -> False. + { s : Z & prod (s <> n) (r < IZR s <= r + 1) } -> False. Proof. intros r z H1 H2 [s [H3 [H4 H5]]]. apply H3; apply single_z_r_R1 with r; trivial. @@ -2123,7 +2183,7 @@ Proof. Qed. Definition Rup_nat (x : R) - : { n : nat | x < INR n }. + : { n : nat & x < INR n }. Proof. intros. destruct (CRarchimedean CR x) as [p maj]. destruct p. @@ -2142,36 +2202,36 @@ Qed. Fixpoint Rarchimedean_ind (x:R) (n : Z) (p:nat) { struct p } : (x < IZR n < x + 2 + (INR p)) - -> { n:Z | x < IZR n /\ IZR n < x+2 }. + -> { n:Z & x < IZR n < x+2 }. Proof. destruct p. - - exists n. rewrite Rplus_0_r in H. exact H. + - exists n. destruct H. split. exact r. rewrite Rplus_0_r in r0; exact r0. - intros. destruct (linear_order_T (x+1+INR p) (IZR n) (x+2+INR p)). do 2 rewrite Rplus_assoc. apply Rplus_lt_compat_l, Rplus_lt_compat_r. rewrite <- (Rplus_0_r 1). apply Rplus_lt_compat_l. apply Rlt_0_1. + apply (Rarchimedean_ind x (n-1)%Z p). unfold Zminus. - rewrite plus_IZR, opp_IZR. + split; rewrite plus_IZR, opp_IZR. setoid_replace (IZR 1) with 1. 2: reflexivity. - split. apply (Rplus_lt_reg_l 1). ring_simplify. apply (Rle_lt_trans _ (x + 1 + INR p)). 2: exact r. rewrite Rplus_assoc. apply Rplus_le_compat_l. rewrite <- (Rplus_0_r 1), Rplus_assoc. apply Rplus_le_compat_l. rewrite Rplus_0_l. apply (le_INR 0), le_0_n. + setoid_replace (IZR 1) with 1. 2: reflexivity. apply (Rplus_lt_reg_l 1). ring_simplify. setoid_replace (x + 2 + INR p + 1) with (x + 2 + INR (S p)). apply H. rewrite S_INR. ring. + apply (Rarchimedean_ind x n p). split. apply H. exact r. Qed. -Lemma Rarchimedean (x:R) : { n : Z | x < IZR n < x + 2 }. +Lemma Rarchimedean (x:R) : { n : Z & x < IZR n < x + 2 }. Proof. destruct (Rup_nat x) as [n nmaj]. destruct (Rup_nat (INR n + - (x + 2))) as [p pmaj]. apply (Rplus_lt_compat_r (x+2)) in pmaj. rewrite Rplus_assoc, Rplus_opp_l, Rplus_0_r in pmaj. apply (Rarchimedean_ind x (Z.of_nat n) p). - rewrite <- INR_IZR_INZ. split. exact nmaj. + split; rewrite <- INR_IZR_INZ. exact nmaj. rewrite Rplus_comm in pmaj. exact pmaj. Qed. @@ -2182,7 +2242,7 @@ Proof. intros. intro abs. assert (0 < -(a*b)) as epsPos. { rewrite <- Ropp_0. apply Ropp_gt_lt_contravar. apply abs. } - pose proof (Rup_nat (b * (/ (-(a*b))) (or_intror (Ropp_0_gt_lt_contravar _ abs)))) + pose proof (Rup_nat (b * (/ (-(a*b))) (inr (Ropp_0_gt_lt_contravar _ abs)))) as [n maj]. destruct n as [|n]. - simpl in maj. apply (Rmult_lt_compat_r (-(a*b))) in maj. @@ -2193,23 +2253,23 @@ Proof. - (* n > 0 *) assert (0 < INR (S n)) as nPos. { apply (lt_INR 0). apply le_n_S, le_0_n. } - assert (b * (/ (INR (S n))) (or_intror nPos) < -(a*b)). + assert (b * (/ (INR (S n))) (inr nPos) < -(a*b)). { apply (Rmult_lt_reg_r (INR (S n))). apply nPos. rewrite Rmult_assoc. rewrite Rinv_l. rewrite Rmult_1_r. apply (Rmult_lt_compat_r (-(a*b))) in maj. rewrite Rmult_assoc in maj. rewrite Rinv_l in maj. rewrite Rmult_1_r in maj. rewrite Rmult_comm. apply maj. exact epsPos. } - pose proof (Rmult_le_compat_l_half (a + (/ (INR (S n))) (or_intror nPos)) + pose proof (Rmult_le_compat_l_half (a + (/ (INR (S n))) (inr nPos)) 0 b). - assert (a + (/ (INR (S n))) (or_intror nPos) > 0 + 0). + assert (a + (/ (INR (S n))) (inr nPos) > 0 + 0). apply Rplus_le_lt_compat. apply H. apply Rinv_0_lt_compat. rewrite Rplus_0_l in H3. specialize (H2 H3 H0). clear H3. rewrite Rmult_0_r in H2. apply H2. clear H2. rewrite Rmult_plus_distr_r. apply (Rplus_lt_compat_l (a*b)) in H1. rewrite Rplus_opp_r in H1. - rewrite (Rmult_comm ((/ (INR (S n))) (or_intror nPos))). + rewrite (Rmult_comm ((/ (INR (S n))) (inr nPos))). apply H1. Qed. @@ -2237,8 +2297,8 @@ Lemma Rmult_le_0_lt_compat : 0 <= r1 -> 0 <= r3 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. Proof. intros. apply (Rle_lt_trans _ (r2 * r3)). - apply Rmult_le_compat_r. apply H0. apply Rlt_asym. - apply H1. apply Rmult_lt_compat_l. exact (Rle_lt_trans 0 r1 r2 H H1). + apply Rmult_le_compat_r. apply H0. intro abs. apply (Rlt_asym r1 r2 H1). + apply abs. apply Rmult_lt_compat_l. exact (Rle_lt_trans 0 r1 r2 H H1). exact H2. Qed. @@ -2298,7 +2358,7 @@ Qed. Definition IQR (q:Q) : R := match q with - | Qmake a b => IZR a * (/ (IPR b)) (or_intror (IPR_pos b)) + | Qmake a b => IZR a * (/ (IPR b)) (inr (IPR_pos b)) end. Arguments IQR q%Q : simpl never. @@ -2306,19 +2366,19 @@ Lemma plus_IQR : forall n m:Q, IQR (n + m) == IQR n + IQR m. Proof. intros. destruct n,m; unfold Qplus,IQR; simpl. rewrite plus_IZR. repeat rewrite mult_IZR. - setoid_replace ((/ IPR (Qden * Qden0)) (or_intror (IPR_pos (Qden * Qden0)))) - with ((/ IPR Qden) (or_intror (IPR_pos Qden)) - * (/ IPR Qden0) (or_intror (IPR_pos Qden0))). + setoid_replace ((/ IPR (Qden * Qden0)) (inr (IPR_pos (Qden * Qden0)))) + with ((/ IPR Qden) (inr (IPR_pos Qden)) + * (/ IPR Qden0) (inr (IPR_pos Qden0))). rewrite Rmult_plus_distr_r. repeat rewrite Rmult_assoc. rewrite <- (Rmult_assoc (IZR (Z.pos Qden))). rewrite Rinv_r. rewrite Rmult_1_l. - rewrite (Rmult_comm ((/IPR Qden) (or_intror (IPR_pos Qden)))). + rewrite (Rmult_comm ((/IPR Qden) (inr (IPR_pos Qden)))). rewrite <- (Rmult_assoc (IZR (Z.pos Qden0))). rewrite Rinv_r. rewrite Rmult_1_l. reflexivity. unfold IZR. right. apply IPR_pos. right. apply IPR_pos. rewrite <- (Rinv_mult_distr - _ _ _ _ (or_intror (Rmult_lt_0_compat _ _ (IPR_pos _) (IPR_pos _)))). + _ _ _ _ (inr (Rmult_lt_0_compat _ _ (IPR_pos _) (IPR_pos _)))). apply Rinv_eq_compat. apply mult_IPR. Qed. @@ -2371,7 +2431,7 @@ Proof. apply Rmult_le_compat_l. apply (IZR_le 0 a). unfold Qle in H; simpl in H. rewrite Z.mul_1_r in H. apply H. - apply Rlt_asym. apply Rinv_0_lt_compat. + unfold Rle. apply Rlt_asym. apply Rinv_0_lt_compat. Qed. Lemma IQR_le : forall n m:Q, Qle n m -> IQR n <= IQR m. @@ -2401,10 +2461,29 @@ Proof. right. apply IPR_pos. Qed. +Instance IQR_morph_T + : CMorphisms.Proper + (CMorphisms.respectful Qeq Req) IQR. +Proof. + intros x y H. destruct x,y; unfold IQR. + unfold Qeq in H; simpl in H. + apply (Rmult_eq_reg_r (IZR (Z.pos Qden))). + 2: right; apply IPR_pos. + rewrite Rmult_assoc, Rinv_l, Rmult_1_r. + rewrite (Rmult_comm (IZR Qnum0)). + apply (Rmult_eq_reg_l (IZR (Z.pos Qden0))). + 2: right; apply IPR_pos. + rewrite <- Rmult_assoc, <- Rmult_assoc, Rinv_r. + rewrite Rmult_1_l. + repeat rewrite <- mult_IZR. + rewrite <- H. rewrite Zmult_comm. reflexivity. + right; apply IPR_pos. +Qed. + Fixpoint Rfloor_pos (a : R) (n : nat) { struct n } : 0 < a -> a < INR n - -> { p : nat | INR p < a < INR p + 2 }. + -> { p : nat & INR p < a < INR p + 2 }. Proof. (* Decreasing loop on n, until it is the first integer above a. *) intros H H0. destruct n. @@ -2425,22 +2504,23 @@ Proof. Qed. Definition Rfloor (a : R) - : { p : Z | IZR p < a < IZR p + 2 }. + : { p : Z & IZR p < a < IZR p + 2 }. Proof. destruct (linear_order_T 0 a 1 Rlt_0_1). - destruct (Rup_nat a). destruct (Rfloor_pos a x r r0). - exists (Z.of_nat x0). rewrite <- INR_IZR_INZ. apply a0. + exists (Z.of_nat x0). split; rewrite <- INR_IZR_INZ; apply p. - apply (Rplus_lt_compat_l (-a)) in r. rewrite Rplus_comm, Rplus_opp_r, Rplus_comm in r. destruct (Rup_nat (1-a)). destruct (Rfloor_pos (1-a) x r r0). - exists (-(Z.of_nat x0 + 1))%Z. rewrite opp_IZR. - rewrite plus_IZR. simpl. split. + exists (-(Z.of_nat x0 + 1))%Z. split; rewrite opp_IZR, plus_IZR. + rewrite <- (Ropp_involutive a). apply Ropp_gt_lt_contravar. - destruct a0 as [_ a0]. apply (Rplus_lt_reg_r 1). + destruct p as [_ a0]. apply (Rplus_lt_reg_r 1). rewrite Rplus_comm, Rplus_assoc. rewrite <- INR_IZR_INZ. apply a0. - + destruct a0 as [a0 _]. apply (Rplus_lt_compat_l a) in a0. - ring_simplify in a0. rewrite <- INR_IZR_INZ. + + destruct p as [a0 _]. apply (Rplus_lt_compat_l a) in a0. + unfold Rminus in a0. + rewrite <- (Rplus_comm (1+-a)), Rplus_assoc, Rplus_opp_l, Rplus_0_r in a0. + rewrite <- INR_IZR_INZ. apply (Rplus_lt_reg_r (INR x0)). unfold IZR, IPR, IPR_2. ring_simplify. exact a0. Qed. @@ -2451,13 +2531,13 @@ Qed. and they are measured by exact rational numbers. *) Definition RQ_dense_pos (a b : R) : 0 < b - -> a < b -> { q : Q | a < IQR q < b }. + -> a < b -> { q : Q & a < IQR q < b }. Proof. intros H H0. assert (0 < b - a) as epsPos. { apply (Rplus_lt_compat_r (-a)) in H0. rewrite Rplus_opp_r in H0. apply H0. } - pose proof (Rup_nat ((/(b-a)) (or_intror epsPos))) + pose proof (Rup_nat ((/(b-a)) (inr epsPos))) as [n maj]. destruct n as [|k]. - exfalso. @@ -2502,7 +2582,7 @@ Qed. Definition RQ_dense (a b : R) : a < b - -> { q : Q | a < IQR q < b }. + -> { q : Q & a < IQR q < b }. Proof. intros H. destruct (linear_order_T a 0 b). apply H. - destruct (RQ_dense_pos (-b) (-a)) as [q maj]. @@ -2530,7 +2610,7 @@ Proof. Qed. Definition RQ_limit : forall (x : R) (n:nat), - { q:Q | x < IQR q < x + IQR (1 # Pos.of_nat n) }. + { q:Q & x < IQR q < x + IQR (1 # Pos.of_nat n) }. Proof. intros x n. apply (RQ_dense x (x + IQR (1 # Pos.of_nat n))). rewrite <- (Rplus_0_r x). rewrite Rplus_assoc. @@ -2538,6 +2618,69 @@ Proof. reflexivity. Qed. +(* Rlt is decided by the LPO in Type, + which is a non-constructive oracle. *) +Lemma Rlt_lpo_dec : forall x y : R, + (forall (P : nat -> Prop), (forall n, {P n} + {~P n}) + -> {n | ~P n} + {forall n, P n}) + -> (x < y) + (x < y -> False). +Proof. + intros x y lpo. + pose (fun n => let (l,_) := RQ_limit x n in l) as xn. + pose (fun n => let (l,_) := RQ_limit y n in l) as yn. + destruct (lpo (fun n:nat => Qle (yn n - xn n) (1 # Pos.of_nat n))). + - intro n. destruct (Qlt_le_dec (1 # Pos.of_nat n) (yn n - xn n)). + right. apply Qlt_not_le. exact q. left. exact q. + - left. destruct s as [n nmaj]. unfold xn,yn in nmaj. + destruct (RQ_limit x n), (RQ_limit y n); unfold proj1_sig in nmaj. + apply Qnot_le_lt in nmaj. + apply (Rlt_le_trans x (IQR x0)). apply p. + apply (Rle_trans _ (IQR (x1 - (1# Pos.of_nat n)))). + apply IQR_le. apply (Qplus_le_l _ _ ((1#Pos.of_nat n) - x0)). + ring_simplify. ring_simplify in nmaj. rewrite Qplus_comm. + apply Qlt_le_weak. exact nmaj. + unfold Qminus. rewrite plus_IQR,opp_IQR. + apply (Rplus_le_reg_r (IQR (1#Pos.of_nat n))). + ring_simplify. unfold Rle. apply Rlt_asym. rewrite Rplus_comm. apply p0. + - right. intro abs. + pose ((y - x) * IQR (1#2)) as eps. + assert (0 < eps) as epsPos. + { apply Rmult_lt_0_compat. apply Rgt_minus. exact abs. + apply IQR_pos. reflexivity. } + destruct (Rup_nat ((/eps) (inr epsPos))) as [n nmaj]. + specialize (q (S n)). unfold xn, yn in q. + destruct (RQ_limit x (S n)) as [a amaj], (RQ_limit y (S n)) as [b bmaj]; + unfold proj1_sig in q. + assert (IQR (1 # Pos.of_nat (S n)) < eps). + { unfold IQR. rewrite Rmult_1_l. + apply (Rmult_lt_reg_l (IPR (Pos.of_nat (S n)))). apply IPR_pos. + rewrite Rinv_r, <- INR_IPR, Nat2Pos.id. 2: discriminate. + apply (Rlt_trans _ _ (INR (S n))) in nmaj. + apply (Rmult_lt_compat_l eps) in nmaj. + rewrite Rinv_r, Rmult_comm in nmaj. exact nmaj. + right. exact epsPos. exact epsPos. apply lt_INR. apply le_n_S, le_refl. + right. apply IPR_pos. } + unfold eps in H. apply (Rlt_asym y (IQR b)). + + apply bmaj. + + apply (Rlt_le_trans _ (IQR a + (y - x) * IQR (1 # 2))). + apply IQR_le in q. + apply (Rle_lt_trans _ _ _ q) in H. + apply (Rplus_lt_reg_l (-IQR a)). + rewrite <- Rplus_assoc, Rplus_opp_l, Rplus_0_l, Rplus_comm, + <- opp_IQR, <- plus_IQR. exact H. + apply (Rplus_lt_compat_l x) in H. + destruct amaj. apply (Rlt_trans _ _ _ r0) in H. + apply (Rplus_lt_compat_r ((y - x) * IQR (1 # 2))) in H. + unfold Rle. apply Rlt_asym. + setoid_replace (x + (y - x) * IQR (1 # 2) + (y - x) * IQR (1 # 2)) with y in H. + exact H. + rewrite Rplus_assoc, <- Rmult_plus_distr_r. + setoid_replace (y - x + (y - x)) with ((y-x)*2). + unfold IQR. rewrite Rmult_1_l, Rmult_assoc, Rinv_r. ring. + right. apply (IZR_lt 0). reflexivity. + unfold IZR, IPR, IPR_2. ring. +Qed. + (*********) Lemma Rmult_le_pos : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2. @@ -2548,7 +2691,7 @@ Qed. Lemma Rinv_le_contravar : forall x y (xpos : 0 < x) (ynz : y # 0), - x <= y -> (/ y) ynz <= (/ x) (or_intror xpos). + x <= y -> (/ y) ynz <= (/ x) (inr xpos). Proof. intros. intro abs. apply (Rmult_lt_compat_l x) in abs. 2: apply xpos. rewrite Rinv_r in abs. @@ -2560,7 +2703,7 @@ Proof. Qed. Lemma Rle_Rinv : forall x y (xpos : 0 < x) (ypos : 0 < y), - x <= y -> (/ y) (or_intror ypos) <= (/ x) (or_intror xpos). + x <= y -> (/ y) (inr ypos) <= (/ x) (inr xpos). Proof. intros. apply Rinv_le_contravar with (1 := H). @@ -2583,8 +2726,8 @@ Proof. apply Rplus_lt_le_compat. exact Rlt_0_1. apply Rle_refl. Qed. -Lemma double_var : forall r1, r1 == r1 * (/ 2) (or_intror Rlt_0_2) - + r1 * (/ 2) (or_intror Rlt_0_2). +Lemma double_var : forall r1, r1 == r1 * (/ 2) (inr Rlt_0_2) + + r1 * (/ 2) (inr Rlt_0_2). Proof. intro; rewrite <- double; rewrite <- Rmult_assoc; symmetry ; apply Rinv_r_simpl_m. @@ -2623,7 +2766,7 @@ Lemma Rmult_ge_0_gt_0_lt_compat : r3 >= 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. Proof. intros. apply (Rle_lt_trans _ (r2 * r3)). - apply Rmult_le_compat_r. apply H. apply Rlt_asym. apply H1. + apply Rmult_le_compat_r. apply H. unfold Rle. apply Rlt_asym. apply H1. apply Rmult_lt_compat_l. apply H0. apply H2. Qed. @@ -2631,11 +2774,11 @@ Lemma le_epsilon : forall r1 r2, (forall eps, 0 < eps -> r1 <= r2 + eps) -> r1 <= r2. Proof. intros x y H. intro abs. - assert (0 < (x - y) * (/ 2) (or_intror Rlt_0_2)). + assert (0 < (x - y) * (/ 2) (inr Rlt_0_2)). { apply (Rplus_lt_compat_r (-y)) in abs. rewrite Rplus_opp_r in abs. apply Rmult_lt_0_compat. exact abs. apply Rinv_0_lt_compat. } - specialize (H ((x - y) * (/ 2) (or_intror Rlt_0_2)) H0). + specialize (H ((x - y) * (/ 2) (inr Rlt_0_2)) H0). apply (Rmult_le_compat_l 2) in H. rewrite Rmult_plus_distr_l in H. apply (Rplus_le_compat_l (-x)) in H. @@ -2643,12 +2786,12 @@ Proof. (Rmult_plus_distr_r 1 1), (Rmult_plus_distr_r 1 1) in H. ring_simplify in H; contradiction. - right. apply Rlt_0_2. apply Rlt_asym. apply Rlt_0_2. + right. apply Rlt_0_2. unfold Rle. apply Rlt_asym. apply Rlt_0_2. Qed. (**********) Lemma Rdiv_lt_0_compat : forall a b (bpos : 0 < b), - 0 < a -> 0 < a * (/b) (or_intror bpos). + 0 < a -> 0 < a * (/b) (inr bpos). Proof. intros; apply Rmult_lt_0_compat;[|apply Rinv_0_lt_compat]; assumption. Qed. diff --git a/theories/Reals/ConstructiveRcomplete.v b/theories/Reals/ConstructiveRcomplete.v index 241eca0fb2..929fa03051 100644 --- a/theories/Reals/ConstructiveRcomplete.v +++ b/theories/Reals/ConstructiveRcomplete.v @@ -16,12 +16,12 @@ Require Import Logic.ConstructiveEpsilon. Local Open Scope CReal_scope. -Lemma CReal_absSmall : forall x y : CReal, - (exists n : positive, Qlt (2 # n) - (proj1_sig x (Pos.to_nat n) - Qabs (proj1_sig y (Pos.to_nat n)))) - -> (CRealLt (CReal_opp x) y /\ CRealLt y x). +Lemma CReal_absSmall : forall (x y : CReal) (n : positive), + (Qlt (2 # n) + (proj1_sig x (Pos.to_nat n) - Qabs (proj1_sig y (Pos.to_nat n)))) + -> (CRealLt (CReal_opp x) y * CRealLt y x). Proof. - intros. destruct H as [n maj]. split. + intros x y n maj. split. - exists n. destruct x as [xn caux], y as [yn cauy]; simpl. simpl in maj. unfold Qminus. rewrite Qopp_involutive. rewrite Qplus_comm. @@ -35,24 +35,26 @@ Proof. apply maj. apply Qplus_le_r. apply Qopp_le_compat. apply Qle_Qabs. Qed. -Definition absSmall (a b : CReal) : Prop +Definition absSmall (a b : CReal) : Set := -b < a < b. Definition Un_cv_mod (un : nat -> CReal) (l : CReal) : Set := forall n : positive, - { p : nat | forall i:nat, le p i -> absSmall (un i - l) (IQR (1#n)) }. + { p : nat & forall i:nat, le p i -> absSmall (un i - l) (IQR (1#n)) }. Lemma Un_cv_mod_eq : forall (v u : nat -> CReal) (s : CReal), (forall n:nat, u n == v n) -> Un_cv_mod u s -> Un_cv_mod v s. Proof. intros v u s seq H1 p. specialize (H1 p) as [N H0]. - exists N. intros. unfold absSmall. rewrite <- seq. apply H0. apply H. + exists N. intros. unfold absSmall. split. + rewrite <- seq. apply H0. apply H. + rewrite <- seq. apply H0. apply H. Qed. Definition Un_cauchy_mod (un : nat -> CReal) : Set := forall n : positive, - { p : nat | forall i j:nat, le p i + { p : nat & forall i j:nat, le p i -> le p j -> -IQR (1#n) < un i - un j < IQR (1#n) }. @@ -65,7 +67,7 @@ Definition Un_cauchy_mod (un : nat -> CReal) : Set Fixpoint Rfloor_pos (a : CReal) (n : nat) { struct n } : 0 < a -> a < INR n - -> { p : nat | INR p < a < INR p + 2 }. + -> { p : nat & INR p < a < INR p + 2 }. Proof. (* Decreasing loop on n, until it is the first integer above a. *) intros H H0. destruct n. @@ -86,9 +88,9 @@ Proof. Qed. Definition Rfloor (a : CReal) - : { p : Z | IZR p < a < IZR p + 2 }. + : { p : Z & IZR p < a < IZR p + 2 }. Proof. - assert (forall x:CReal, 0 < x -> { n : nat | x < INR n }). + assert (forall x:CReal, 0 < x -> { n : nat & x < INR n }). { intros. pose proof (Rarchimedean x) as [n [maj _]]. destruct n. + exfalso. apply (CRealLt_asym 0 x); assumption. @@ -101,24 +103,25 @@ Proof. apply (IZR_lt 0). reflexivity. } destruct (linear_order_T 0 a 1 CRealLt_0_1). - destruct (H a c). destruct (Rfloor_pos a x c c0). - exists (Z.of_nat x0). rewrite <- INR_IZR_INZ. apply a0. + exists (Z.of_nat x0). split; rewrite <- INR_IZR_INZ; apply p. - apply (CReal_plus_lt_compat_l (-a)) in c. rewrite CReal_plus_comm, CReal_plus_opp_r, CReal_plus_comm in c. destruct (H (1-a) c). destruct (Rfloor_pos (1-a) x c c0). - exists (-(Z.of_nat x0 + 1))%Z. rewrite opp_IZR. - rewrite plus_IZR. simpl. split. + exists (-(Z.of_nat x0 + 1))%Z. split; rewrite opp_IZR, plus_IZR. + rewrite <- (CReal_opp_involutive a). apply CReal_opp_gt_lt_contravar. - destruct a0 as [_ a0]. apply (CReal_plus_lt_reg_r 1). + destruct p as [_ a0]. apply (CReal_plus_lt_reg_r 1). rewrite CReal_plus_comm, CReal_plus_assoc. rewrite <- INR_IZR_INZ. apply a0. - + destruct a0 as [a0 _]. apply (CReal_plus_lt_compat_l a) in a0. - ring_simplify in a0. rewrite <- INR_IZR_INZ. + + destruct p as [a0 _]. apply (CReal_plus_lt_compat_l a) in a0. + unfold CReal_minus in a0. + rewrite <- (CReal_plus_comm (1+-a)), CReal_plus_assoc, CReal_plus_opp_l, CReal_plus_0_r in a0. + rewrite <- INR_IZR_INZ. apply (CReal_plus_lt_reg_r (INR x0)). unfold IZR, IPR, IPR_2. ring_simplify. exact a0. Qed. Definition Rup_nat (x : CReal) - : { n : nat | x < INR n }. + : { n : nat & x < INR n }. Proof. intros. destruct (Rarchimedean x) as [p [maj _]]. destruct p. @@ -134,14 +137,14 @@ Qed. archimedean field, which is the field of real numbers. *) Definition FQ_dense_pos (a b : CReal) : 0 < b - -> a < b -> { q : Q | a < IQR q < b }. + -> a < b -> { q : Q & a < IQR q < b }. Proof. intros H H0. assert (0 < b - a) as epsPos. { apply (CReal_plus_lt_compat_l (-a)) in H0. rewrite CReal_plus_opp_l, CReal_plus_comm in H0. apply H0. } - pose proof (Rup_nat ((/(b-a)) (or_intror epsPos))) + pose proof (Rup_nat ((/(b-a)) (inr epsPos))) as [n maj]. destruct n as [|k]. - exfalso. @@ -184,7 +187,7 @@ Qed. Definition FQ_dense (a b : CReal) : a < b - -> { q : Q | a < IQR q < b }. + -> { q : Q & a < IQR q < b }. Proof. intros H. destruct (linear_order_T a 0 b). apply H. - destruct (FQ_dense_pos (-b) (-a)) as [q maj]. @@ -212,7 +215,7 @@ Proof. Qed. Definition RQ_limit : forall (x : CReal) (n:nat), - { q:Q | x < IQR q < x + IQR (1 # Pos.of_nat n) }. + { q:Q & x < IQR q < x + IQR (1 # Pos.of_nat n) }. Proof. intros x n. apply (FQ_dense x (x + IQR (1 # Pos.of_nat n))). rewrite <- (CReal_plus_0_r x). rewrite CReal_plus_assoc. @@ -228,7 +231,7 @@ Definition Un_cauchy_Q (xn : nat -> Q) : Set Lemma Rdiag_cauchy_sequence : forall (xn : nat -> CReal), Un_cauchy_mod xn - -> Un_cauchy_Q (fun n => proj1_sig (RQ_limit (xn n) n)). + -> Un_cauchy_Q (fun n => let (l,_) := RQ_limit (xn n) n in l). Proof. intros xn H p. specialize (H (2 * p)%positive) as [k cv]. exists (max k (2 * Pos.to_nat p)). intros. @@ -246,55 +249,64 @@ Proof. rewrite CReal_plus_assoc. rewrite CReal_plus_opp_l. rewrite CReal_plus_0_r. rewrite <- plus_IQR. setoid_replace (- (1 # p) + (1 # 2 * p))%Q with (- (1 # 2 * p))%Q. - rewrite opp_IQR. exact H1. + rewrite opp_IQR. exact c. rewrite Qplus_comm. setoid_replace (1#p)%Q with (2 # 2 *p)%Q. rewrite Qinv_minus_distr. reflexivity. reflexivity. + rewrite plus_IQR. apply CReal_plus_le_lt_compat. apply CRealLt_asym. - destruct (RQ_limit (xn p0) p0); simpl. apply a. + destruct (RQ_limit (xn p0) p0); simpl. apply p1. destruct (RQ_limit (xn q) q); unfold proj1_sig. rewrite opp_IQR. apply CReal_opp_gt_lt_contravar. apply (CRealLt_Le_trans _ (xn q + IQR (1 # Pos.of_nat q))). - apply a. apply CReal_plus_le_compat_l. apply IQR_le. + apply p1. apply CReal_plus_le_compat_l. apply IQR_le. apply Z2Nat.inj_le. discriminate. discriminate. simpl. assert ((Pos.to_nat p~0 <= q)%nat). { apply (le_trans _ (Init.Nat.max k (2 * Pos.to_nat p))). 2: apply H0. replace (p~0)%positive with (2*p)%positive. 2: reflexivity. rewrite Pos2Nat.inj_mul. apply Nat.le_max_r. } - rewrite Nat2Pos.id. apply H3. intro abs. subst q. - inversion H3. pose proof (Pos2Nat.is_pos (p~0)). - rewrite H5 in H4. inversion H4. + rewrite Nat2Pos.id. apply H1. intro abs. subst q. + inversion H1. pose proof (Pos2Nat.is_pos (p~0)). + rewrite H3 in H2. inversion H2. - apply lt_IQR. unfold Qminus. apply (CRealLt_trans _ (xn p0 + IQR (1 # 2 * p) - xn q)). + rewrite plus_IQR. apply CReal_plus_le_lt_compat. apply CRealLt_asym. destruct (RQ_limit (xn p0) p0); unfold proj1_sig. apply (CRealLt_Le_trans _ (xn p0 + IQR (1 # Pos.of_nat p0))). - apply a. apply CReal_plus_le_compat_l. apply IQR_le. + apply p1. apply CReal_plus_le_compat_l. apply IQR_le. apply Z2Nat.inj_le. discriminate. discriminate. simpl. assert ((Pos.to_nat p~0 <= p0)%nat). { apply (le_trans _ (Init.Nat.max k (2 * Pos.to_nat p))). 2: apply H. replace (p~0)%positive with (2*p)%positive. 2: reflexivity. rewrite Pos2Nat.inj_mul. apply Nat.le_max_r. } - rewrite Nat2Pos.id. apply H3. intro abs. subst p0. - inversion H3. pose proof (Pos2Nat.is_pos (p~0)). - rewrite H5 in H4. inversion H4. + rewrite Nat2Pos.id. apply H1. intro abs. subst p0. + inversion H1. pose proof (Pos2Nat.is_pos (p~0)). + rewrite H3 in H2. inversion H2. rewrite opp_IQR. apply CReal_opp_gt_lt_contravar. - destruct (RQ_limit (xn q) q); simpl. apply a. + destruct (RQ_limit (xn q) q); simpl. apply p1. + unfold CReal_minus. rewrite (CReal_plus_comm (xn p0)). rewrite CReal_plus_assoc. apply (CReal_plus_lt_reg_l (- IQR (1 # 2 * p))). rewrite <- CReal_plus_assoc. rewrite CReal_plus_opp_l. rewrite CReal_plus_0_l. rewrite <- opp_IQR. rewrite <- plus_IQR. setoid_replace (- (1 # 2 * p) + (1 # p))%Q with (1 # 2 * p)%Q. - exact H2. rewrite Qplus_comm. + exact c0. rewrite Qplus_comm. setoid_replace (1#p)%Q with (2 # 2*p)%Q. rewrite Qinv_minus_distr. reflexivity. reflexivity. Qed. +Lemma doubleLtCovariant : forall a b c d e f : CReal, + a == b -> c == d -> e == f + -> (a < c < e) + -> (b < d < f). +Proof. + split. rewrite <- H. rewrite <- H0. apply H2. + rewrite <- H0. rewrite <- H1. apply H2. +Qed. + (* An element of CReal is a Cauchy sequence of rational numbers, show that it converges to itself in CReal. *) Lemma CReal_cv_self : forall (qn : nat -> Q) (x : CReal) (cvmod : positive -> nat), @@ -303,11 +315,12 @@ Lemma CReal_cv_self : forall (qn : nat -> Q) (x : CReal) (cvmod : positive -> na Proof. intros qn x cvmod H p. specialize (H (2*p)%positive). exists (cvmod (2*p)%positive). - intros p0 H0. unfold absSmall, CReal_minus. rewrite FinjectQ_CReal. - setoid_replace (IQR (qn p0)) with (inject_Q (qn p0)). - 2: apply FinjectQ_CReal. - apply CReal_absSmall. - exists (Pos.max (4 * p)%positive (Pos.of_nat (cvmod (2 * p)%positive))). + intros p0 H0. unfold absSmall, CReal_minus. + apply (doubleLtCovariant (-inject_Q (1#p)) _ (inject_Q (qn p0) - x) _ (inject_Q (1#p))). + rewrite FinjectQ_CReal. reflexivity. + rewrite FinjectQ_CReal. reflexivity. + rewrite FinjectQ_CReal. reflexivity. + apply (CReal_absSmall _ _ (Pos.max (4 * p)%positive (Pos.of_nat (cvmod (2 * p)%positive)))). setoid_replace (proj1_sig (inject_Q (1 # p)) (Pos.to_nat (Pos.max (4 * p) (Pos.of_nat (cvmod (2 * p)%positive))))) with (1 # p)%Q. 2: reflexivity. @@ -340,7 +353,8 @@ Lemma Un_cv_extens : forall (xn yn : nat -> CReal) (l : CReal), -> Un_cv_mod yn l. Proof. intros. intro p. destruct (H p) as [n cv]. exists n. - intros. unfold absSmall, CReal_minus. rewrite <- (H0 i). apply cv. apply H1. + intros. unfold absSmall, CReal_minus. + split; rewrite <- (H0 i); apply cv; apply H1. Qed. (* Q is dense in Archimedean fields, so all real numbers @@ -373,12 +387,12 @@ Lemma Rcauchy_complete : forall (xn : nat -> CReal), -> { l : CReal & Un_cv_mod xn l }. Proof. intros xn cau. - destruct (R_has_all_rational_limits (fun n => proj1_sig (RQ_limit (xn n) n)) + destruct (R_has_all_rational_limits (fun n => let (l,_) := RQ_limit (xn n) n in l) (Rdiag_cauchy_sequence xn cau)) as [l cv]. exists l. intro p. specialize (cv (2*p)%positive) as [k cv]. exists (max k (2 * Pos.to_nat p)). intros p0 H. specialize (cv p0). - destruct cv. apply (le_trans _ (max k (2 * Pos.to_nat p))). + destruct cv as [H0 H1]. apply (le_trans _ (max k (2 * Pos.to_nat p))). apply Nat.le_max_l. apply H. destruct (RQ_limit (xn p0) p0) as [q maj]; unfold proj1_sig in H0,H1. split. @@ -436,13 +450,13 @@ Lemma is_upper_bound_dec : -> { is_upper_bound E x } + { ~is_upper_bound E x }. Proof. intros E x lpo sig_not_dec. - destruct (sig_not_dec (~exists y:CReal, E y /\ x < y)). + destruct (sig_not_dec (~exists y:CReal, E y /\ CRealLtProp x y)). - left. intros y H. - destruct (CRealLt_lpo_dec x y lpo). 2: exact n0. + destruct (CRealLt_lpo_dec x y lpo). 2: exact f. exfalso. apply n. intro abs. apply abs. - exists y. split. exact H. exact c. + exists y. split. exact H. destruct c. exists x0. exact q. - right. intro abs. apply n. intros [y [H H0]]. - specialize (abs y H). contradiction. + specialize (abs y H). apply CRealLtEpsilon in H0. contradiction. Qed. Lemma is_upper_bound_epsilon : diff --git a/theories/Reals/ConstructiveReals.v b/theories/Reals/ConstructiveReals.v index 7311b5953f..97876d129a 100644 --- a/theories/Reals/ConstructiveReals.v +++ b/theories/Reals/ConstructiveReals.v @@ -15,16 +15,16 @@ Require Import QArith. -Definition isLinearOrder (X : Set) (Xlt : X -> X -> Prop) : Set - := prod ((forall x y:X, Xlt x y -> ~Xlt y x) - /\ (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 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 -> Prop) (x y : X) : Prop - := ~Xlt x y /\ ~Xlt y x. +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 -> Prop) (x y : X) : Prop - := Xlt x y \/ Xlt y x. +Definition orderAppart (X : Set) (Xlt : X -> X -> Set) (x y : X) : Set + := Xlt x y + Xlt y x. Definition sig_forall_dec_T : Type := forall (P : nat -> Prop), (forall n, {P n} + {~P n}) @@ -35,9 +35,18 @@ Definition sig_not_dec_T : Type := forall P : Prop, { ~~P } + { ~P }. Record ConstructiveReals : Type := { CRcarrier : Set; - CRlt : CRcarrier -> CRcarrier -> Prop; + CRlt : CRcarrier -> CRcarrier -> Set; CRltLinear : isLinearOrder CRcarrier CRlt; + 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; @@ -56,7 +65,9 @@ Record ConstructiveReals : Type := 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); + 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); @@ -74,32 +85,28 @@ Record ConstructiveReals : Type := CRlt CRzero r -> CRlt CRzero (CRinv r rnz); CRarchimedean : forall x : CRcarrier, - { k : Z | CRlt x (gen_phiZ CRzero CRone CRplus CRmult CRopp k) }; + { k : Z & CRlt x (gen_phiZ CRzero CRone CRplus CRmult CRopp k) }; CRminus (x y : CRcarrier) : CRcarrier := CRplus x (CRopp y); CR_cv (un : nat -> CRcarrier) (l : CRcarrier) : Set := forall eps:CRcarrier, CRlt CRzero eps - -> { p : nat | forall i:nat, le p i -> CRlt (CRopp eps) (CRminus (un i) l) - /\ CRlt (CRminus (un i) l) eps }; + -> { p : nat & forall i:nat, le p i -> CRlt (CRopp eps) (CRminus (un i) l) + * CRlt (CRminus (un i) l) eps }; CR_cauchy (un : nat -> CRcarrier) : Set := forall eps:CRcarrier, CRlt CRzero eps - -> { p : nat | forall i j:nat, le p i -> le p j -> + -> { p : nat & forall i j:nat, le p i -> le p j -> CRlt (CRopp eps) (CRminus (un i) (un j)) - /\ CRlt (CRminus (un i) (un j)) eps }; + * CRlt (CRminus (un i) (un j)) eps }; CR_complete : forall xn : nat -> CRcarrier, CR_cauchy xn -> { l : CRcarrier & CR_cv xn l }; (* Those are redundant, they could be proved from the previous hypotheses *) - CRlt_lpo_dec : forall x y : CRcarrier, - sig_forall_dec_T - -> { CRlt x y } + { ~CRlt x y }; - CRis_upper_bound (E:CRcarrier -> Prop) (m:CRcarrier) - := forall x:CRcarrier, E x -> ~(CRlt m x); + := forall x:CRcarrier, E x -> CRlt m x -> False; CR_sig_lub : forall (E:CRcarrier -> Prop), @@ -108,6 +115,5 @@ Record ConstructiveReals : Type := -> (exists x : CRcarrier, E x) -> (exists x : CRcarrier, CRis_upper_bound E x) -> { u : CRcarrier | CRis_upper_bound E u /\ - forall y:CRcarrier, CRis_upper_bound E y -> ~CRlt y u }; - + forall y:CRcarrier, CRis_upper_bound E y -> CRlt y u -> False }; }. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 1b1bfcec3e..75298855b2 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -543,7 +543,7 @@ Lemma Rmult_eq_reg_l : forall r r1 r2, r * r1 = r * r2 -> r <> 0 -> r1 = r2. Proof. intros. apply Rquot1. apply (Rmult_eq_reg_l (Rrepr r)). rewrite <- Rrepr_mult, <- Rrepr_mult, H. reflexivity. - rewrite Rrepr_appart, Rrepr_0 in H0. exact H0. + apply Rrepr_appart in H0. rewrite Rrepr_0 in H0. exact H0. Qed. Lemma Rmult_eq_reg_r : forall r r1 r2, r1 * r = r2 * r -> r <> 0 -> r1 = r2. @@ -996,15 +996,16 @@ Qed. Lemma Rplus_lt_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2. Proof. - intros. rewrite Rlt_def. apply (Rplus_lt_reg_l (Rrepr r)). + intros. rewrite Rlt_def. apply Rlt_forget. apply (Rplus_lt_reg_l (Rrepr r)). rewrite <- Rrepr_plus, <- Rrepr_plus. - rewrite Rlt_def in H. exact H. + rewrite Rlt_def in H. apply Rlt_epsilon. exact H. Qed. Lemma Rplus_lt_reg_r : forall r r1 r2, r1 + r < r2 + r -> r1 < r2. Proof. - intros. rewrite Rlt_def. apply (Rplus_lt_reg_r (Rrepr r)). - rewrite <- Rrepr_plus, <- Rrepr_plus. rewrite Rlt_def in H. exact H. + intros. rewrite Rlt_def. apply Rlt_forget. apply (Rplus_lt_reg_r (Rrepr r)). + rewrite <- Rrepr_plus, <- Rrepr_plus. rewrite Rlt_def in H. + apply Rlt_epsilon. exact H. Qed. Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2. @@ -1075,15 +1076,18 @@ Qed. Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2. Proof. intros. rewrite Rlt_def. rewrite Rrepr_opp, Rrepr_opp. + apply Rlt_forget. apply Ropp_gt_lt_contravar. unfold Rgt in H. - rewrite Rlt_def in H. exact H. + rewrite Rlt_def in H. apply Rlt_epsilon. exact H. Qed. Hint Resolve Ropp_gt_lt_contravar : core. Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2. Proof. intros. unfold Rgt. rewrite Rlt_def. rewrite Rrepr_opp, Rrepr_opp. - apply Ropp_lt_gt_contravar. rewrite Rlt_def in H. exact H. + apply Rlt_forget. + apply Ropp_lt_gt_contravar. rewrite Rlt_def in H. + apply Rlt_epsilon. exact H. Qed. Hint Resolve Ropp_lt_gt_contravar: real. @@ -1303,18 +1307,18 @@ Qed. Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2. Proof. - intros. rewrite Rlt_def in H,H0. rewrite Rlt_def. + intros. rewrite Rlt_def in H,H0. rewrite Rlt_def. apply Rlt_forget. apply (Rmult_lt_reg_l (Rrepr r)). - rewrite <- Rrepr_0. exact H. - rewrite <- Rrepr_mult, <- Rrepr_mult. exact H0. + rewrite <- Rrepr_0. apply Rlt_epsilon. exact H. + rewrite <- Rrepr_mult, <- Rrepr_mult. apply Rlt_epsilon. exact H0. Qed. Lemma Rmult_lt_reg_r : forall r r1 r2 : R, 0 < r -> r1 * r < r2 * r -> r1 < r2. Proof. intros. rewrite Rlt_def. rewrite Rlt_def in H, H0. - apply (Rmult_lt_reg_r (Rrepr r)). - rewrite <- Rrepr_0. exact H. - rewrite <- Rrepr_mult, <- Rrepr_mult. exact H0. + apply Rlt_forget. apply (Rmult_lt_reg_r (Rrepr r)). + rewrite <- Rrepr_0. apply Rlt_epsilon. exact H. + rewrite <- Rrepr_mult, <- Rrepr_mult. apply Rlt_epsilon. exact H0. Qed. Lemma Rmult_gt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2. @@ -1323,7 +1327,7 @@ Proof. eauto using Rmult_lt_reg_l with rorders. Qed. Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2. Proof. intros. rewrite Rrepr_le. rewrite Rlt_def in H. apply (Rmult_le_reg_l (Rrepr r)). - rewrite <- Rrepr_0. exact H. + rewrite <- Rrepr_0. apply Rlt_epsilon. exact H. rewrite <- Rrepr_mult, <- Rrepr_mult. rewrite <- Rrepr_le. exact H0. Qed. @@ -1642,7 +1646,7 @@ Hint Resolve pos_INR: real. Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat. Proof. intros. apply INR_lt. rewrite Rlt_def in H. - rewrite Rrepr_INR, Rrepr_INR in H. exact H. + rewrite Rrepr_INR, Rrepr_INR in H. apply Rlt_epsilon. exact H. Qed. Hint Resolve INR_lt: real. @@ -1676,7 +1680,7 @@ Hint Resolve not_0_INR: real. Lemma not_INR : forall n m:nat, n <> m -> INR n <> INR m. Proof. - intros. rewrite Rrepr_appart, Rrepr_INR, Rrepr_INR. + intros. apply Rappart_repr. rewrite Rrepr_INR, Rrepr_INR. apply not_INR. exact H. Qed. Hint Resolve not_INR: real. @@ -1801,14 +1805,15 @@ Qed. Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z. Proof. intros. apply lt_0_IZR. rewrite <- Rrepr_0, <- Rrepr_IZR. - rewrite Rlt_def in H. exact H. + rewrite Rlt_def in H. apply Rlt_epsilon. exact H. Qed. (**********) Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z. Proof. intros. apply lt_IZR. - rewrite <- Rrepr_IZR, <- Rrepr_IZR. rewrite Rlt_def in H. exact H. + rewrite <- Rrepr_IZR, <- Rrepr_IZR. rewrite Rlt_def in H. + apply Rlt_epsilon. exact H. Qed. (**********) @@ -1892,17 +1897,18 @@ Hint Extern 0 (IZR _ <> IZR _) => apply IZR_neq, Zeq_bool_neq, eq_refl : real. Lemma one_IZR_lt1 : forall n:Z, -1 < IZR n < 1 -> n = 0%Z. Proof. intros. apply one_IZR_lt1. do 2 rewrite Rlt_def in H. split. - rewrite <- Rrepr_IZR, <- Rrepr_1, <- Rrepr_opp. apply H. - rewrite <- Rrepr_IZR, <- Rrepr_1. apply H. + rewrite <- Rrepr_IZR, <- Rrepr_1, <- Rrepr_opp. + apply Rlt_epsilon. apply H. + rewrite <- Rrepr_IZR, <- Rrepr_1. apply Rlt_epsilon. apply H. Qed. Lemma one_IZR_r_R1 : forall r (n m:Z), r < IZR n <= r + 1 -> r < IZR m <= r + 1 -> n = m. Proof. intros. rewrite Rlt_def in H, H0. apply (one_IZR_r_R1 (Rrepr r)); split. - rewrite <- Rrepr_IZR. apply H. + rewrite <- Rrepr_IZR. apply Rlt_epsilon. apply H. rewrite <- Rrepr_IZR, <- Rrepr_1, <- Rrepr_plus, <- Rrepr_le. - apply H. rewrite <- Rrepr_IZR. apply H0. + apply H. rewrite <- Rrepr_IZR. apply Rlt_epsilon. apply H0. rewrite <- Rrepr_IZR, <- Rrepr_1, <- Rrepr_plus, <- Rrepr_le. apply H0. Qed. @@ -1939,8 +1945,10 @@ Lemma Rinv_le_contravar : Proof. intros. apply Rrepr_le. assert (y <> 0). intro abs. subst y. apply (Rlt_irrefl 0). exact (Rlt_le_trans 0 x 0 H H0). - rewrite Rrepr_appart, Rrepr_0 in H1. rewrite Rlt_def in H. rewrite Rrepr_0 in H. - rewrite (Rrepr_inv y H1), (Rrepr_inv x (or_intror H)). + apply Rrepr_appart in H1. + rewrite Rrepr_0 in H1. rewrite Rlt_def in H. rewrite Rrepr_0 in H. + apply Rlt_epsilon in H. + rewrite (Rrepr_inv y H1), (Rrepr_inv x (inr H)). apply Rinv_le_contravar. rewrite <- Rrepr_le. exact H0. Qed. @@ -2008,7 +2016,7 @@ Proof. intros. rewrite Rrepr_le. apply le_epsilon. intros. rewrite <- (Rquot2 eps), <- Rrepr_plus. rewrite <- Rrepr_le. apply H. rewrite Rlt_def. - rewrite Rquot2, Rrepr_0. exact H0. + rewrite Rquot2, Rrepr_0. apply Rlt_forget. exact H0. Qed. (**********) diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 1b45d28040..f734b47fb5 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -64,8 +64,8 @@ Lemma Rrepr_inv : forall (x:R) (xnz : Rrepr x # 0), Proof. intros. rewrite RinvImpl.Rinv_def. destruct (Req_appart_dec x R0). - exfalso. subst x. destruct xnz. - rewrite Rrepr_0 in H. exact (Rlt_irrefl 0 H). - rewrite Rrepr_0 in H. exact (Rlt_irrefl 0 H). + rewrite Rrepr_0 in c. exact (Rlt_irrefl 0 c). + rewrite Rrepr_0 in c. exact (Rlt_irrefl 0 c). - rewrite Rquot2. apply (Rmult_eq_reg_l (Rrepr x)). 2: exact xnz. rewrite Rmult_comm, (Rmult_comm (Rrepr x)), Rinv_l, Rinv_l. reflexivity. @@ -75,21 +75,30 @@ Lemma Rrepr_le : forall x y:R, (x <= y)%R <-> Rrepr x <= Rrepr y. Proof. split. - intros [H|H] abs. rewrite RbaseSymbolsImpl.Rlt_def in H. + apply Rlt_epsilon in H. exact (Rlt_asym (Rrepr x) (Rrepr y) H abs). destruct H. exact (Rlt_asym (Rrepr x) (Rrepr x) abs abs). - intros. destruct (total_order_T x y). destruct s. - left. exact r. right. exact e. rewrite RbaseSymbolsImpl.Rlt_def in r. contradiction. + left. exact r. right. exact e. + rewrite RbaseSymbolsImpl.Rlt_def in r. apply Rlt_epsilon in r. contradiction. Qed. -Lemma Rrepr_appart : forall x y:R, (x <> y)%R <-> Rrepr x # Rrepr y. +Lemma Rrepr_appart : forall x y:R, + (x <> y)%R -> Rrepr x # Rrepr y. Proof. - split. - - intros. destruct (total_order_T x y). destruct s. - left. rewrite RbaseSymbolsImpl.Rlt_def in r. exact r. contradiction. - right. rewrite RbaseSymbolsImpl.Rlt_def in r. exact r. - - intros [H|H] abs. - destruct abs. exact (Rlt_asym (Rrepr x) (Rrepr x) H H). - destruct abs. exact (Rlt_asym (Rrepr x) (Rrepr x) H H). + intros. destruct (total_order_T x y). destruct s. + left. rewrite RbaseSymbolsImpl.Rlt_def in r. + apply Rlt_epsilon. exact r. contradiction. + right. rewrite RbaseSymbolsImpl.Rlt_def in r. + apply Rlt_epsilon. exact r. +Qed. + +Lemma Rappart_repr : forall x y:R, + Rrepr x # Rrepr y -> (x <> y)%R. +Proof. + intros x y [H|H] abs. + destruct abs. exact (Rlt_asym (Rrepr x) (Rrepr x) H H). + destruct abs. exact (Rlt_asym (Rrepr x) (Rrepr x) H H). Qed. Close Scope R_scope_constr. @@ -206,6 +215,7 @@ Hint Resolve Rmult_plus_distr_l: real. Lemma Rlt_asym : forall r1 r2:R, r1 < r2 -> ~ r2 < r1. Proof. intros. intro abs. rewrite RbaseSymbolsImpl.Rlt_def in H, abs. + apply Rlt_epsilon in H. apply Rlt_epsilon in abs. apply (Rlt_asym (Rrepr r1) (Rrepr r2)); assumption. Qed. @@ -213,6 +223,8 @@ Qed. Lemma Rlt_trans : forall r1 r2 r3:R, r1 < r2 -> r2 < r3 -> r1 < r3. Proof. intros. rewrite RbaseSymbolsImpl.Rlt_def. rewrite RbaseSymbolsImpl.Rlt_def in H, H0. + apply Rlt_epsilon in H. apply Rlt_epsilon in H0. + apply Rlt_forget. apply (Rlt_trans (Rrepr r1) (Rrepr r2) (Rrepr r3)); assumption. Qed. @@ -220,16 +232,18 @@ Qed. Lemma Rplus_lt_compat_l : forall r r1 r2:R, r1 < r2 -> r + r1 < r + r2. Proof. intros. rewrite RbaseSymbolsImpl.Rlt_def. rewrite RbaseSymbolsImpl.Rlt_def in H. - do 2 rewrite Rrepr_plus. apply Rplus_lt_compat_l. exact H. + do 2 rewrite Rrepr_plus. apply Rlt_forget. + apply Rplus_lt_compat_l. apply Rlt_epsilon. exact H. Qed. (**********) Lemma Rmult_lt_compat_l : forall r r1 r2:R, 0 < r -> r1 < r2 -> r * r1 < r * r2. Proof. intros. rewrite RbaseSymbolsImpl.Rlt_def. rewrite RbaseSymbolsImpl.Rlt_def in H. - do 2 rewrite Rrepr_mult. apply Rmult_lt_compat_l. - rewrite <- (Rquot2 (CRzero CR)). unfold IZR in H. rewrite RbaseSymbolsImpl.R0_def in H. exact H. - rewrite RbaseSymbolsImpl.Rlt_def in H0. exact H0. + do 2 rewrite Rrepr_mult. apply Rlt_forget. apply Rmult_lt_compat_l. + rewrite <- (Rquot2 (CRzero CR)). unfold IZR in H. + rewrite RbaseSymbolsImpl.R0_def in H. apply Rlt_epsilon. exact H. + rewrite RbaseSymbolsImpl.Rlt_def in H0. apply Rlt_epsilon. exact H0. Qed. Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real. @@ -305,24 +319,39 @@ Proof. intro r. unfold up. destruct (Rarchimedean (Rrepr r)) as [n nmaj], (total_order_T (IZR n - r) R1). destruct s. - - split. unfold Rgt. rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_IZR. apply nmaj. + - split. unfold Rgt. rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_IZR. + apply Rlt_forget. apply nmaj. unfold Rle. left. exact r0. - - split. unfold Rgt. rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_IZR. apply nmaj. - right. exact e. + - split. unfold Rgt. rewrite RbaseSymbolsImpl.Rlt_def. + rewrite Rrepr_IZR. apply Rlt_forget. apply nmaj. right. exact e. - split. - + unfold Rgt, Z.pred. rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_IZR, plus_IZR. + + unfold Rgt, Z.pred. rewrite RbaseSymbolsImpl.Rlt_def. + rewrite Rrepr_IZR, plus_IZR. rewrite RbaseSymbolsImpl.Rlt_def in r0. rewrite Rrepr_minus in r0. rewrite <- (Rrepr_IZR n). unfold ConstructiveRIneq.IZR, ConstructiveRIneq.IPR. - apply (ConstructiveRIneq.Rplus_lt_compat_l (ConstructiveRIneq.Rminus (Rrepr r) (Rrepr R1))) + apply Rlt_forget. apply Rlt_epsilon in r0. + unfold ConstructiveRIneq.Rminus in r0. + apply (ConstructiveRIneq.Rplus_lt_compat_l + (ConstructiveRIneq.Rplus (Rrepr r) (ConstructiveRIneq.Ropp (Rrepr R1)))) in r0. - ring_simplify in r0. rewrite RbaseSymbolsImpl.R1_def in r0. rewrite Rquot2 in r0. - rewrite ConstructiveRIneq.Rplus_comm. exact r0. + rewrite ConstructiveRIneq.Rplus_assoc, + ConstructiveRIneq.Rplus_opp_l, + ConstructiveRIneq.Rplus_0_r, + RbaseSymbolsImpl.R1_def, Rquot2, + ConstructiveRIneq.Rplus_comm, + ConstructiveRIneq.Rplus_assoc, + <- (ConstructiveRIneq.Rplus_assoc (ConstructiveRIneq.Ropp (Rrepr r))), + ConstructiveRIneq.Rplus_opp_l, + ConstructiveRIneq.Rplus_0_l + in r0. + exact r0. + destruct (total_order_T (IZR (Z.pred n) - r) 1). destruct s. left. exact r1. right. exact e. - exfalso. rewrite <- Rrepr_IZR in nmaj. + exfalso. destruct nmaj as [_ nmaj]. rewrite <- Rrepr_IZR in nmaj. apply (Rlt_asym (IZR n) (r + 2)). rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_plus. rewrite (Rrepr_plus 1 1). + apply Rlt_forget. apply (ConstructiveRIneq.Rlt_le_trans _ (ConstructiveRIneq.Rplus (Rrepr r) (ConstructiveRIneq.IZR 2))). apply nmaj. @@ -334,15 +363,22 @@ Proof. in r1. unfold ConstructiveRIneq.IZR, ConstructiveRIneq.IPR in r1. rewrite RbaseSymbolsImpl.Rlt_def, Rrepr_plus. + apply Rlt_epsilon in r1. apply (ConstructiveRIneq.Rplus_lt_compat_l (ConstructiveRIneq.Rplus (Rrepr r) (CRone CR))) in r1. - ring_simplify in r1. + apply Rlt_forget. apply (ConstructiveRIneq.Rle_lt_trans _ (ConstructiveRIneq.Rplus (ConstructiveRIneq.Rplus (Rrepr r) (Rrepr 1)) (CRone CR))). - 2: apply r1. rewrite (Rrepr_plus 1 1). unfold IZR, IPR. rewrite RbaseSymbolsImpl.R1_def, (Rquot2 (CRone CR)), <- ConstructiveRIneq.Rplus_assoc. apply Rle_refl. + rewrite <- (ConstructiveRIneq.Rplus_comm (Rrepr 1)), + <- ConstructiveRIneq.Rplus_assoc, + (ConstructiveRIneq.Rplus_comm (Rrepr 1)) + in r1. + apply (ConstructiveRIneq.Rlt_le_trans _ _ _ r1). + unfold ConstructiveRIneq.Rminus. + ring_simplify. apply ConstructiveRIneq.Rle_refl. Qed. (**********************************************************) @@ -377,10 +413,13 @@ Proof. destruct (CR_sig_lub CR Er sig_forall_dec sig_not_dec Einhab Ebound). exists (Rabst x). split. - intros y Ey. apply Rrepr_le. rewrite Rquot2. apply a. + intros y Ey. apply Rrepr_le. rewrite Rquot2. + unfold ConstructiveRIneq.Rle. apply a. unfold Er. replace (Rabst (Rrepr y)) with y. exact Ey. apply Rquot1. rewrite Rquot2. reflexivity. intros. destruct a. apply Rrepr_le. rewrite Rquot2. - apply H3. intros y Ey. rewrite <- (Rquot2 y). - apply Rrepr_le, H1, Ey. + unfold ConstructiveRIneq.Rle. apply H3. intros y Ey. + intros. rewrite <- (Rquot2 y) in H4. + apply Rrepr_le in H4. exact H4. + apply H1, Ey. Qed. diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 6e0eef0974..c71baf42f5 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -59,7 +59,7 @@ Module Type RbaseSymbolsSig. Parameter Ropp_def : forall x : R, Ropp x = Rabst (ConstructiveRIneq.Ropp (Rrepr x)). Parameter Rlt_def : forall x y : R, - Rlt x y = ConstructiveRIneq.Rlt (Rrepr x) (Rrepr y). + Rlt x y = ConstructiveRIneq.RltProp (Rrepr x) (Rrepr y). End RbaseSymbolsSig. Module RbaseSymbolsImpl : RbaseSymbolsSig. @@ -72,7 +72,7 @@ Module RbaseSymbolsImpl : RbaseSymbolsSig. Definition Ropp : R -> R := fun x : R => Rabst (ConstructiveRIneq.Ropp (Rrepr x)). Definition Rlt : R -> R -> Prop - := fun x y : R => ConstructiveRIneq.Rlt (Rrepr x) (Rrepr y). + := fun x y : R => ConstructiveRIneq.RltProp (Rrepr x) (Rrepr y). Definition R0_def := eq_refl R0. Definition R1_def := eq_refl R1. @@ -156,10 +156,11 @@ Arguments IZR z%Z : simpl never. Lemma total_order_T : forall r1 r2:R, {Rlt r1 r2} + {r1 = r2} + {Rlt r2 r1}. Proof. - intros. destruct (CRlt_lpo_dec CR (Rrepr r1) (Rrepr r2) sig_forall_dec). - - left. left. rewrite RbaseSymbolsImpl.Rlt_def. exact c. - - destruct (CRlt_lpo_dec CR (Rrepr r2) (Rrepr r1) sig_forall_dec). - + right. rewrite RbaseSymbolsImpl.Rlt_def. exact c. + intros. destruct (Rlt_lpo_dec (Rrepr r1) (Rrepr r2) sig_forall_dec). + - left. left. rewrite RbaseSymbolsImpl.Rlt_def. + apply Rlt_forget. exact r. + - destruct (Rlt_lpo_dec (Rrepr r2) (Rrepr r1) sig_forall_dec). + + right. rewrite RbaseSymbolsImpl.Rlt_def. apply Rlt_forget. exact r. + left. right. apply Rquot1. split; assumption. Qed. @@ -175,8 +176,11 @@ Qed. Lemma Rrepr_appart_0 : forall x:R, (x < R0 \/ R0 < x) -> Rappart (Rrepr x) (CRzero CR). Proof. - intros. destruct H. left. rewrite RbaseSymbolsImpl.Rlt_def, RbaseSymbolsImpl.R0_def, Rquot2 in H. exact H. - right. rewrite RbaseSymbolsImpl.Rlt_def, RbaseSymbolsImpl.R0_def, Rquot2 in H. exact H. + intros. apply CRltDisjunctEpsilon. destruct H. + left. rewrite RbaseSymbolsImpl.Rlt_def, RbaseSymbolsImpl.R0_def, Rquot2 in H. + exact H. + right. rewrite RbaseSymbolsImpl.Rlt_def, RbaseSymbolsImpl.R0_def, Rquot2 in H. + exact H. Qed. Module Type RinvSig. |