From c690a68ba0b78b913cbcb60f7508d431071d4c79 Mon Sep 17 00:00:00 2001 From: Vincent Semeria Date: Fri, 4 Oct 2019 18:29:58 +0200 Subject: Replace classical reals quotient axioms by functional extensionality. Define homotopy propositions and homotopy sets. Rename local variable R in test Nsatz, to avoid a name collision with the type of real numbers. --- .../10-standard-library/10827-dedekind-reals.rst | 11 + doc/stdlib/index-list.html.template | 3 +- plugins/syntax/r_syntax.ml | 2 +- test-suite/success/Nsatz.v | 10 +- theories/Logic/HLevels.v | 146 + theories/Reals/ClassicalDedekindReals.v | 465 ++++ theories/Reals/ConstructiveCauchyReals.v | 40 +- theories/Reals/ConstructiveRIneq.v | 2817 -------------------- theories/Reals/ConstructiveRcomplete.v | 33 + theories/Reals/ConstructiveRealsMorphisms.v | 2 +- theories/Reals/RIneq.v | 237 +- theories/Reals/Raxioms.v | 248 +- theories/Reals/Rdefinitions.v | 88 +- 13 files changed, 1021 insertions(+), 3081 deletions(-) create mode 100644 doc/changelog/10-standard-library/10827-dedekind-reals.rst create mode 100644 theories/Logic/HLevels.v create mode 100644 theories/Reals/ClassicalDedekindReals.v delete mode 100644 theories/Reals/ConstructiveRIneq.v diff --git a/doc/changelog/10-standard-library/10827-dedekind-reals.rst b/doc/changelog/10-standard-library/10827-dedekind-reals.rst new file mode 100644 index 0000000000..5d8467025b --- /dev/null +++ b/doc/changelog/10-standard-library/10827-dedekind-reals.rst @@ -0,0 +1,11 @@ +- New module `Reals.ClassicalDedekindReals` defines Dedekind real numbers + as boolean-values functions along with 3 logical axioms: limited principle + of omniscience, excluded middle of negations and functional extensionality. + The exposed type :g:`R` in module :g:`Reals.Rdefinitions` is those + Dedekind reals, hidden behind an opaque module. + Classical Dedekind reals are a quotient of constructive reals, which allows + to transport many constructive proofs to the classical case. + + See `#10827 `_, by Vincent Semeria, + based on discussions with Guillaume Melquiond, Bas Spitters and Hugo Herbelin, + code review by Hugo Herbelin. diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index d1b98b94a3..df7cda9aad 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -68,6 +68,7 @@ through the Require Import command.

theories/Logic/WKL.v theories/Logic/FinFun.v theories/Logic/PropFacts.v + theories/Logic/HLevels.v
Structures: @@ -518,8 +519,8 @@ through the Require Import command.

theories/Reals/ConstructiveRealsMorphisms.v theories/Reals/ConstructiveCauchyReals.v theories/Reals/ConstructiveCauchyRealsMult.v + theories/Reals/ClassicalDedekindReals.v theories/Reals/Raxioms.v - theories/Reals/ConstructiveRIneq.v theories/Reals/ConstructiveRealsLUB.v theories/Reals/RIneq.v theories/Reals/DiscrR.v diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 66db924051..70c1077106 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -102,7 +102,7 @@ let bigint_of_z c = match DAst.get c with let rdefinitions = ["Coq";"Reals";"Rdefinitions"] let r_modpath = MPfile (make_dir rdefinitions) let r_base_modpath = MPdot (r_modpath, Label.make "RbaseSymbolsImpl") -let r_path = make_path rdefinitions "R" +let r_path = make_path ["Coq";"Reals";"Rdefinitions";"RbaseSymbolsImpl"] "R" let glob_IZR = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "IZR") let glob_Rmult = GlobRef.ConstRef (Constant.make2 r_base_modpath @@ Label.make "Rmult") diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v index 381fbabe72..998f3f7dd1 100644 --- a/test-suite/success/Nsatz.v +++ b/test-suite/success/Nsatz.v @@ -419,13 +419,13 @@ Qed. -Lemma Desargues: forall A B C A1 B1 C1 P Q R S:point, +Lemma Desargues: forall A B C A1 B1 C1 P Q T S:point, X S = 0 -> Y S = 0 -> Y A = 0 -> collinear A S A1 -> collinear B S B1 -> collinear C S C1 -> collinear B1 C1 P -> collinear B C P -> collinear A1 C1 Q -> collinear A C Q -> - collinear A1 B1 R -> collinear A B R -> - collinear P Q R + collinear A1 B1 T -> collinear A B T -> + collinear P Q T \/ X A = X B \/ X A = X C \/ X B = X C \/ X A = 0 \/ Y B = 0 \/ Y C = 0 \/ collinear S B C \/ parallel A C A1 C1 \/ parallel A B A1 B1. Proof. @@ -440,8 +440,8 @@ let lv := rev (X A :: Y A1 :: X A1 :: Y B1 :: Y C1 - :: X R - :: Y R + :: X T + :: Y T :: X Q :: Y Q :: X P :: Y P :: X C1 :: X B1 :: nil) in nsatz with radicalmax :=1%N strategy:=0%Z diff --git a/theories/Logic/HLevels.v b/theories/Logic/HLevels.v new file mode 100644 index 0000000000..010c4aad6f --- /dev/null +++ b/theories/Logic/HLevels.v @@ -0,0 +1,146 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* Prop), + (forall x:A, IsHProp (P x)) + -> IsHProp (forall x:A, P x). +Proof. + intros A P H p q. apply functional_extensionality_dep. + intro x. apply H. +Qed. + +(* Homotopy propositions are stable by conjunction, but not by disjunction, + which can have a proof by the left and another proof by the right. *) +Lemma and_hprop : forall P Q : Prop, + IsHProp P -> IsHProp Q -> IsHProp (P /\ Q). +Proof. + intros. intros p q. destruct p,q. + replace p0 with p. replace q0 with q. reflexivity. + apply H0. apply H. +Qed. + +Lemma impl_hprop : forall P Q : Prop, + IsHProp Q -> IsHProp (P -> Q). +Proof. + intros P Q H p q. apply functional_extensionality. + intros. apply H. +Qed. + +Lemma false_hprop : IsHProp False. +Proof. + intros p q. contradiction. +Qed. + +Lemma true_hprop : IsHProp True. +Proof. + intros p q. destruct p,q. reflexivity. +Qed. + +(* All negations are homotopy propositions. *) +Lemma not_hprop : forall P : Type, IsHProp (P -> False). +Proof. + intros P p q. apply functional_extensionality. + intros. contradiction. +Qed. + +(* Homotopy propositions are included in homotopy sets. + They are the first 2 levels of a cumulative hierarchy of types + indexed by the natural numbers. In homotopy type theory, + homotopy propositions are call (-1)-types and homotopy + sets 0-types. *) +Lemma hset_hprop : forall X : Type, + IsHProp X -> IsHSet X. +Proof. + intros X H. + assert (forall (x y z:X) (p : y = z), eq_trans (H x y) p = H x z). + { intros. unfold eq_trans, eq_ind. destruct p. reflexivity. } + assert (forall (x y z:X) (p : y = z), + p = eq_trans (eq_sym (H x y)) (H x z)). + { intros. rewrite <- (H0 x y z p). unfold eq_trans, eq_sym, eq_ind. + destruct p, (H x y). reflexivity. } + intros x y p q. + rewrite (H1 x x y p), (H1 x x y q). reflexivity. +Qed. + +Lemma eq_trans_cancel : forall {X : Type} {x y z : X} (p : x = y) (q r : y = z), + (eq_trans p q = eq_trans p r) -> q = r. +Proof. + intros. destruct p. simpl in H. destruct r. + simpl in H. rewrite eq_trans_refl_l in H. exact H. +Qed. + +Lemma hset_hOneType : forall X : Type, + IsHSet X -> IsHOneType X. +Proof. + intros X f x y p q. + pose (fun a => f x y p a) as g. + assert (forall a (r : q = a), eq_trans (g q) r = g a). + { intros. destruct a. subst q. reflexivity. } + intros r s. pose proof (H p (eq_sym r)). + pose proof (H p (eq_sym s)). + rewrite <- H1 in H0. apply eq_trans_cancel in H0. + rewrite <- eq_sym_involutive. rewrite <- (eq_sym_involutive r). + rewrite H0. reflexivity. +Qed. + +(* "IsHProp X" sounds like a proposition, because it asserts + a property of the type X. And indeed: *) +Lemma hprop_hprop : forall X : Type, + IsHProp (IsHProp X). +Proof. + intros X p q. + apply forall_hprop. intro x. + apply forall_hprop. intro y. intros f g. + apply (hset_hprop X p). +Qed. + +Lemma hprop_hset : forall X : Type, + IsHProp (IsHSet X). +Proof. + intros X f g. + apply functional_extensionality_dep. intro x. + apply functional_extensionality_dep. intro y. + apply functional_extensionality_dep. intro a. + apply functional_extensionality_dep. intro b. + apply (hset_hOneType). exact f. +Qed. diff --git a/theories/Reals/ClassicalDedekindReals.v b/theories/Reals/ClassicalDedekindReals.v new file mode 100644 index 0000000000..e32def29b8 --- /dev/null +++ b/theories/Reals/ClassicalDedekindReals.v @@ -0,0 +1,465 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* bool have all the classical properties of the + real numbers. + + We could prove operations and theorems about them directly, + but instead we notice that they are a quotient of the + constructive Cauchy reals, from which they inherit many properties. +*) + +(* The limited principle of omniscience *) +Axiom sig_forall_dec + : forall (P : nat -> Prop), + (forall n, {P n} + {~P n}) + -> {n | ~P n} + {forall n, P n}. + +Axiom sig_not_dec : forall P : Prop, { ~~P } + { ~P }. + +(* Try to find a surjection CReal -> lower cuts. *) +Definition isLowerCut (f : Q -> bool) : Prop + := (forall q r:Q, Qle q r -> f r = true -> f q = true) (* interval *) + /\ ~(forall q:Q, f q = true) (* avoid positive infinity *) + /\ ~(forall q:Q, f q = false) (* avoid negative infinity *) + (* openness, the cut contains rational numbers + strictly lower than a real number. *) + /\ (forall q:Q, f q = true -> ~(forall r:Q, Qle r q \/ f r = false)). + +Lemma isLowerCut_hprop : forall (f : Q -> bool), + IsHProp (isLowerCut f). +Proof. + intro f. apply and_hprop. + 2: apply and_hprop. 2: apply not_hprop. + 2: apply and_hprop. 2: apply not_hprop. + - apply forall_hprop. intro x. + apply forall_hprop. intro y. + apply impl_hprop. apply impl_hprop. + intros p q. apply eq_proofs_unicity_on. + intro b. destruct (f x), b. + left. reflexivity. right. discriminate. + right. discriminate. left. reflexivity. + - apply forall_hprop. intro q. apply impl_hprop. apply not_hprop. +Qed. + +Lemma lowerCutBelow : forall f : Q -> bool, + isLowerCut f -> { q : Q | f q = true }. +Proof. + intros. + destruct (sig_forall_dec (fun n:nat => f (-(Z.of_nat n # 1))%Q = false)). + - intro n. destruct (f (-(Z.of_nat n # 1))%Q). + right. discriminate. left. reflexivity. + - destruct s. exists (-(Z.of_nat x # 1))%Q. + destruct (f (-(Z.of_nat x # 1))%Q). + reflexivity. exfalso. apply n. reflexivity. + - exfalso. destruct H, H0, H1. apply H1. intro q. + destruct (f q) eqn:des. 2: reflexivity. exfalso. + destruct (Qarchimedean (-q)) as [p pmaj]. + rewrite <- (Qplus_lt_l _ _ (q-(Z.pos p # 1))) in pmaj. + ring_simplify in pmaj. + specialize (H (- (Z.pos p#1))%Q q). + specialize (e (Pos.to_nat p)). + rewrite positive_nat_Z in e. rewrite H in e. discriminate. + 2: exact des. ring_simplify. apply Qlt_le_weak, pmaj. +Qed. + +Lemma lowerCutAbove : forall f : Q -> bool, + isLowerCut f -> { q : Q | f q = false }. +Proof. + intros. + destruct (sig_forall_dec (fun n => f (Z.of_nat n # 1)%Q = true)). + - intro n. destruct (f (Z.of_nat n # 1)%Q). + left. reflexivity. right. discriminate. + - destruct s. exists (Z.of_nat x # 1)%Q. destruct (f (Z.of_nat x # 1)%Q). + exfalso. apply n. reflexivity. reflexivity. + - exfalso. destruct H, H0, H1. apply H0. intro q. + destruct (Qarchimedean q) as [p pmaj]. + apply (H q (Z.of_nat (Pos.to_nat p) # 1)%Q). + rewrite positive_nat_Z. apply Qlt_le_weak, pmaj. apply e. +Qed. + +Definition DReal : Set + := { f : Q -> bool | isLowerCut f }. + +Fixpoint DRealQlim_rec (f : Q -> bool) (low : isLowerCut f) (n p : nat) { struct p } + : f (proj1_sig (lowerCutBelow f low) + (Z.of_nat p # Pos.of_nat (S n)))%Q = false + -> { q : Q | f q = true /\ f (q + (1 # Pos.of_nat (S n)))%Q = false }. +Proof. + intros. destruct p. + - exfalso. destruct (lowerCutBelow f low); unfold proj1_sig in H. + destruct low. rewrite (H0 _ x) in H. discriminate. simpl. + apply (Qplus_le_l _ _ (-x)). ring_simplify. discriminate. exact e. + - destruct (f (proj1_sig (lowerCutBelow f low) + (Z.of_nat p # Pos.of_nat (S n)))%Q) eqn:des. + + exists (proj1_sig (lowerCutBelow f low) + (Z.of_nat p # Pos.of_nat (S n)))%Q. + split. exact des. + destruct (f (proj1_sig (lowerCutBelow f low) + + (Z.of_nat p # Pos.of_nat (S n)) + (1 # Pos.of_nat (S n)))%Q) eqn:d. + 2: reflexivity. exfalso. + destruct low. + rewrite (e _ (proj1_sig (lowerCutBelow f (conj e a)) + (Z.of_nat p # Pos.of_nat (S n)) + (1 # Pos.of_nat (S n))))%Q in H. + discriminate. 2: exact d. rewrite <- Qplus_assoc, Qplus_le_r. + rewrite Qinv_plus_distr. + replace (Z.of_nat p + 1)%Z with (Z.of_nat (S p))%Z. apply Qle_refl. + replace 1%Z with (Z.of_nat 1). rewrite <- (Nat2Z.inj_add p 1). + apply f_equal. rewrite Nat.add_comm. reflexivity. reflexivity. + + destruct (DRealQlim_rec f low n p des) as [q qmaj]. + exists q. exact qmaj. +Qed. + +Definition DRealQlim (x : DReal) (n : nat) + : { q : Q | proj1_sig x q = true /\ proj1_sig x (q + (1# Pos.of_nat (S n)))%Q = false }. +Proof. + destruct x as [f low]. + destruct (lowerCutAbove f low). + destruct (Qarchimedean (x - proj1_sig (lowerCutBelow f low))) as [p pmaj]. + apply (DRealQlim_rec f low n ((S n) * Pos.to_nat p)). + destruct (lowerCutBelow f low); unfold proj1_sig; unfold proj1_sig in pmaj. + destruct (f (x0 + (Z.of_nat (S n * Pos.to_nat p) # Pos.of_nat (S n)))%Q) eqn:des. + 2: reflexivity. exfalso. destruct low. + rewrite (H _ (x0 + (Z.of_nat (S n * Pos.to_nat p) # Pos.of_nat (S n)))%Q) in e. + discriminate. 2: exact des. + setoid_replace (Z.of_nat (S n * Pos.to_nat p) # Pos.of_nat (S n))%Q with (Z.pos p # 1)%Q. + apply (Qplus_lt_l _ _ x0) in pmaj. ring_simplify in pmaj. + apply Qlt_le_weak, pmaj. rewrite Nat2Z.inj_mul, positive_nat_Z. + unfold Qeq, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_comm. + replace (Z.of_nat (S n)) with (Z.pos (Pos.of_nat (S n))). reflexivity. + simpl. destruct n. reflexivity. apply f_equal. + apply Pos.succ_of_nat. discriminate. +Qed. + +Definition DRealAbstr : CReal -> DReal. +Proof. + intro x. + assert (forall (q : Q) (n : nat), + {(fun n0 : nat => (proj1_sig x (S n0) <= q + (1 # Pos.of_nat (S n0)))%Q) n} + + {~ (fun n0 : nat => (proj1_sig x (S n0) <= q + (1 # Pos.of_nat (S n0)))%Q) n}). + { intros. destruct (Qlt_le_dec (q + (1 # Pos.of_nat (S n))) (proj1_sig x (S n))). + right. apply (Qlt_not_le _ _ q0). left. exact q0. } + + exists (fun q:Q => if sig_forall_dec (fun n:nat => Qle (proj1_sig x (S n)) (q + (1#Pos.of_nat (S n)))) (H q) + then true else false). + repeat split. + - intros. + destruct (sig_forall_dec (fun n : nat => (proj1_sig x (S n) <= q + (1 # Pos.of_nat (S n)))%Q) + (H q)). + reflexivity. exfalso. + destruct (sig_forall_dec (fun n : nat => (proj1_sig x (S n) <= r + (1 # Pos.of_nat (S n)))%Q) + (H r)). + destruct s. apply n. + apply (Qle_trans _ _ _ (q0 x0)). + apply Qplus_le_l. exact H0. discriminate. + - intro abs. destruct (Rfloor x) as [z [_ zmaj]]. + specialize (abs (z+3 # 1)%Q). + destruct (sig_forall_dec (fun n : nat => (proj1_sig x (S n) <= (z+3 # 1) + (1 # Pos.of_nat (S n)))%Q) + (H (z+3 # 1)%Q)). + 2: exfalso; discriminate. clear abs. destruct s as [n nmaj]. apply nmaj. + rewrite <- (inject_Q_plus (z#1) 2) in zmaj. + apply CRealLt_asym in zmaj. rewrite <- CRealLe_not_lt in zmaj. + specialize (zmaj (Pos.of_nat (S n))). unfold inject_Q, proj1_sig in zmaj. + rewrite Nat2Pos.id in zmaj. 2: discriminate. + destruct x as [xn xcau]; unfold proj1_sig. + rewrite Qinv_plus_distr in zmaj. + apply (Qplus_le_l _ _ (-(z + 2 # 1))). apply (Qle_trans _ _ _ zmaj). + apply (Qplus_le_l _ _ (-(1 # Pos.of_nat (S n)))). apply (Qle_trans _ 1). + unfold Qopp, Qnum, Qden. rewrite Qinv_plus_distr. + unfold Qle, Qnum, Qden. apply Z2Nat.inj_le. discriminate. discriminate. + do 2 rewrite Z.mul_1_l. unfold Z.to_nat. rewrite Nat2Pos.id. 2: discriminate. + apply le_n_S, le_0_n. setoid_replace (- (z + 2 # 1))%Q with (-(z+2) #1)%Q. + 2: reflexivity. ring_simplify. rewrite Qinv_plus_distr. + replace (z + 3 + - (z + 2))%Z with 1%Z. apply Qle_refl. ring. + - intro abs. destruct (Rfloor x) as [z [zmaj _]]. + specialize (abs (z-4 # 1)%Q). + destruct (sig_forall_dec (fun n : nat => (proj1_sig x (S n) <= (z-4 # 1) + (1 # Pos.of_nat (S n)))%Q) + (H (z-4 # 1)%Q)). + exfalso; discriminate. clear abs. + apply CRealLt_asym in zmaj. apply zmaj. clear zmaj. + exists 1%positive. unfold inject_Q, proj1_sig. + specialize (q O). + destruct x as [xn xcau]; unfold proj1_sig; unfold proj1_sig in q. + unfold Pos.of_nat in q. rewrite Qinv_plus_distr in q. + unfold Pos.to_nat; simpl. apply (Qplus_lt_l _ _ (xn 1%nat - 2)). + ring_simplify. rewrite Qinv_plus_distr. + apply (Qle_lt_trans _ _ _ q). apply Qlt_minus_iff. + unfold Qopp, Qnum, Qden. rewrite Qinv_plus_distr. + replace (z + -2 + - (z - 4 + 1))%Z with 1%Z. 2: ring. reflexivity. + - intros q H0 abs. + destruct (sig_forall_dec (fun n : nat => (proj1_sig x (S n) <= q + (1 # Pos.of_nat (S n)))%Q) (H q)). + 2: exfalso; discriminate. clear H0. + destruct x as [xn xcau]; unfold proj1_sig in abs, s. + destruct s as [n nmaj]. + (* We have that q < x as real numbers. The middle + (q + xSn - 1/Sn)/2 is also lower than x, witnessed by the same index n. *) + specialize (abs ((q + xn (S n) - (1 # Pos.of_nat (S n))%Q)/2)%Q). + destruct abs. + + apply (Qmult_le_r _ _ 2) in H0. field_simplify in H0. + apply (Qplus_le_r _ _ ((1 # Pos.of_nat (S n)) - q)) in H0. + ring_simplify in H0. apply nmaj. rewrite Qplus_comm. exact H0. reflexivity. + + destruct (sig_forall_dec + (fun n0 : nat => + (xn (S n0) <= (q + xn (S n) - (1 # Pos.of_nat (S n))) / 2 + (1 # Pos.of_nat (S n0)))%Q) + (H ((q + xn (S n) - (1 # Pos.of_nat (S n))) / 2)%Q)). + discriminate. clear H0. specialize (q0 n). + apply (Qmult_le_l _ _ 2) in q0. field_simplify in q0. + apply (Qplus_le_l _ _ (-xn (S n))) in q0. ring_simplify in q0. + contradiction. reflexivity. +Defined. + +Lemma UpperAboveLower : forall (f : Q -> bool) (q r : Q), + isLowerCut f + -> f q = true + -> f r = false + -> Qlt q r. +Proof. + intros. destruct H. apply Qnot_le_lt. intro abs. + rewrite (H r q abs) in H1. discriminate. exact H0. +Qed. + +Definition DRealRepr : DReal -> CReal. +Proof. + intro x. exists (fun n => proj1_sig (DRealQlim x n)). + intros n p q H H0. + destruct (DRealQlim x p), (DRealQlim x q); unfold proj1_sig. + destruct x as [f low]; unfold proj1_sig in a0, a. + apply Qabs_case. + - intros. apply (Qlt_le_trans _ (1 # Pos.of_nat (S q))). + apply (Qplus_lt_l _ _ x1). ring_simplify. apply (UpperAboveLower f). + exact low. apply a. apply a0. unfold Qle, Qnum, Qden. + do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos. + apply Pos2Nat.inj_le. rewrite Nat2Pos.id. apply (le_trans _ _ _ H0), le_S, le_refl. + discriminate. + - intros. apply (Qlt_le_trans _ (1 # Pos.of_nat (S p))). + apply (Qplus_lt_l _ _ x0). ring_simplify. apply (UpperAboveLower f). + exact low. apply a0. apply a. unfold Qle, Qnum, Qden. + do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos. + apply Pos2Nat.inj_le. rewrite Nat2Pos.id. apply (le_trans _ _ _ H), le_S, le_refl. + discriminate. +Defined. + +Definition Rle (x y : DReal) + := forall q:Q, proj1_sig x q = true -> proj1_sig y q = true. + +Lemma Rle_antisym : forall x y : DReal, + Rle x y + -> Rle y x + -> x = y. +Proof. + intros [f cf] [g cg] H H0. unfold Rle in H,H0; simpl in H, H0. + assert (f = g). + { apply functional_extensionality. intro q. + specialize (H q). specialize (H0 q). + destruct (f q), (g q). reflexivity. + exfalso. specialize (H (eq_refl _)). discriminate. + exfalso. specialize (H0 (eq_refl _)). discriminate. + reflexivity. } + subst g. replace cg with cf. reflexivity. + apply isLowerCut_hprop. +Qed. + +Lemma lowerUpper : forall (f : Q -> bool) (q r : Q), + isLowerCut f -> Qle q r -> f q = false -> f r = false. +Proof. + intros. destruct H. specialize (H q r H0). destruct (f r) eqn:desR. + 2: reflexivity. exfalso. specialize (H (eq_refl _)). + rewrite H in H1. discriminate. +Qed. + +Lemma DRealOpen : forall (x : DReal) (q : Q), + proj1_sig x q = true + -> { r : Q | Qlt q r /\ proj1_sig x r = true }. +Proof. + intros. + destruct (sig_forall_dec (fun n => Qle (proj1_sig (DRealQlim x n)) q)). + - intro n. destruct (DRealQlim x n); unfold proj1_sig. + destruct (Qlt_le_dec q x0). right. exact (Qlt_not_le _ _ q0). + left. exact q0. + - destruct s. apply Qnot_le_lt in n. + destruct (DRealQlim x x0); unfold proj1_sig in n. + exists x1. split. exact n. apply a. + - exfalso. destruct x as [f low]. unfold proj1_sig in H, q0. + destruct low, a, a. apply (n1 q H). intros. + destruct (Qlt_le_dec q r). 2: left; exact q1. right. + destruct (Qarchimedean (/(r - q))) as [p pmaj]. + specialize (q0 (Pos.to_nat p)). + destruct (DRealQlim (exist _ f (conj e (conj n (conj n0 n1)))) (Pos.to_nat p)) + as [s smaj]. + unfold proj1_sig in smaj. + apply (lowerUpper f (s + (1 # Pos.of_nat (S (Pos.to_nat p))))). + exact (conj e (conj n (conj n0 n1))). + 2: apply smaj. apply (Qle_trans _ (s + (r-q))). + apply Qplus_le_r. apply (Qle_trans _ (1 # p)). + unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. + apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. + rewrite Nat2Pos.id. apply le_S, le_refl. discriminate. + apply (Qmult_le_l _ _ ( (Z.pos p # 1) / (r-q))). + rewrite <- (Qmult_0_r (Z.pos p #1)). apply Qmult_lt_l. + reflexivity. apply Qinv_lt_0_compat. + unfold Qminus. rewrite <- Qlt_minus_iff. exact q1. + unfold Qdiv. rewrite Qmult_comm, <- Qmult_assoc. + rewrite (Qmult_comm (/(r-q))), Qmult_inv_r, Qmult_assoc. + setoid_replace ((1 # p) * (Z.pos p # 1))%Q with 1%Q. + 2: reflexivity. rewrite Qmult_1_l, Qmult_1_r. + apply Qlt_le_weak, pmaj. intro abs. apply Qlt_minus_iff in q1. + rewrite abs in q1. apply (Qlt_not_le _ _ q1), Qle_refl. + apply (Qplus_le_l _ _ (q-r)). ring_simplify. exact q0. +Qed. + +Lemma DRealReprQ : forall (x : DReal) (q : Q), + proj1_sig x q = true + -> CRealLt (inject_Q q) (DRealRepr x). +Proof. + intros. + destruct (DRealOpen x q H) as [r rmaj]. + destruct (Qarchimedean (4/(r - q))) as [p pmaj]. + exists p. + destruct x as [f low]; unfold DRealRepr, inject_Q, proj1_sig. + destruct (DRealQlim (exist _ f low) (Pos.to_nat p)) as [s smaj]. + unfold proj1_sig in smaj, rmaj. + apply (Qplus_lt_l _ _ (q+ (1 # Pos.of_nat (S (Pos.to_nat p))))). + ring_simplify. rewrite <- (Qplus_comm s). + apply (UpperAboveLower f _ _ low). 2: apply smaj. + destruct low. apply (e _ r). 2: apply rmaj. + rewrite <- (Qplus_comm q). + apply (Qle_trans _ (q + (4#p))). + - rewrite <- Qplus_assoc. apply Qplus_le_r. + apply (Qle_trans _ ((2#p) + (1#p))). + apply Qplus_le_r. + unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. + apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. + rewrite Nat2Pos.id. apply le_S, le_refl. discriminate. + rewrite Qinv_plus_distr. unfold Qle, Qnum, Qden. + apply Z.mul_le_mono_nonneg_r. discriminate. discriminate. + - apply (Qle_trans _ (q + (r-q))). 2: ring_simplify; apply Qle_refl. + apply Qplus_le_r. + apply (Qmult_le_l _ _ ( (Z.pos p # 1) / (r-q))). + rewrite <- (Qmult_0_r (Z.pos p #1)). apply Qmult_lt_l. + reflexivity. apply Qinv_lt_0_compat. + unfold Qminus. rewrite <- Qlt_minus_iff. apply rmaj. + unfold Qdiv. rewrite Qmult_comm, <- Qmult_assoc. + rewrite (Qmult_comm (/(r-q))), Qmult_inv_r, Qmult_assoc. + setoid_replace ((4 # p) * (Z.pos p # 1))%Q with 4%Q. + 2: reflexivity. rewrite Qmult_1_r. + apply Qlt_le_weak, pmaj. intro abs. destruct rmaj. + apply Qlt_minus_iff in H0. + rewrite abs in H0. apply (Qlt_not_le _ _ H0), Qle_refl. +Qed. + +Lemma DRealReprQup : forall (x : DReal) (q : Q), + proj1_sig x q = false + -> CRealLe (DRealRepr x) (inject_Q q). +Proof. + intros x q H [p pmaj]. + unfold inject_Q, DRealRepr, proj1_sig in pmaj. + destruct (DRealQlim x (Pos.to_nat p)) as [r rmaj], rmaj. + clear H1. destruct x as [f low], low; unfold proj1_sig in H, H0. + apply (Qplus_lt_l _ _ q) in pmaj. ring_simplify in pmaj. + rewrite (e _ r) in H. discriminate. 2: exact H0. + apply Qlt_le_weak. apply (Qlt_trans _ ((2#p)+q)). 2: exact pmaj. + apply (Qplus_lt_l _ _ (-q)). ring_simplify. reflexivity. +Qed. + +Lemma DRealQuot1 : forall x y:DReal, CRealEq (DRealRepr x) (DRealRepr y) -> x = y. +Proof. + intros. destruct H. apply Rle_antisym. + - clear H. intros q H1. destruct (proj1_sig y q) eqn:des. + reflexivity. exfalso. apply H0. + apply (CReal_le_lt_trans _ (inject_Q q)). apply DRealReprQup. + exact des. apply DRealReprQ. exact H1. + - clear H0. intros q H1. destruct (proj1_sig x q) eqn:des. + reflexivity. exfalso. apply H. + apply (CReal_le_lt_trans _ (inject_Q q)). apply DRealReprQup. + exact des. apply DRealReprQ. exact H1. +Qed. + +Lemma DRealAbstrFalse : forall (x : CReal) (q : Q) (n : nat), + proj1_sig (DRealAbstr x) q = false + -> (proj1_sig x (S n) <= q + (1 # Pos.of_nat (S n)))%Q. +Proof. + intros. destruct x as [xn xcau]. + unfold DRealAbstr, proj1_sig in H. + destruct ( + sig_forall_dec (fun n : nat => (xn (S n) <= q + (1 # Pos.of_nat (S n)))%Q) + (fun n : nat => + match Qlt_le_dec (q + (1 # Pos.of_nat (S n))) (xn (S n)) with + | left q0 => right (Qlt_not_le (q + (1 # Pos.of_nat (S n))) (xn (S n)) q0) + | right q0 => left q0 + end)). + discriminate. apply q0. +Qed. + +Lemma DRealQuot2 : forall x:CReal, CRealEq (DRealRepr (DRealAbstr x)) x. +Proof. + split. + - intros [p pmaj]. unfold DRealRepr, proj1_sig in pmaj. + destruct x as [xn xcau]. + destruct (DRealQlim (DRealAbstr (exist _ xn xcau)) (Pos.to_nat p)) + as [q [_ qmaj]]. + (* By pmaj, q + 1/p < x as real numbers. + But by qmaj x <= q + 1/(p+1), contradiction. *) + apply (DRealAbstrFalse _ _ (pred (Pos.to_nat p))) in qmaj. + unfold proj1_sig in qmaj. + rewrite Nat.succ_pred in qmaj. + apply (Qlt_not_le _ _ pmaj), (Qplus_le_l _ _ q). + ring_simplify. apply (Qle_trans _ _ _ qmaj). + rewrite <- Qplus_assoc. apply Qplus_le_r. + rewrite Pos2Nat.id. apply (Qle_trans _ ((1#p)+(1#p))). + apply Qplus_le_l. unfold Qle, Qnum, Qden. + do 2 rewrite Z.mul_1_l. + apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. + rewrite Nat2Pos.id. apply le_S, le_refl. discriminate. + rewrite Qinv_plus_distr. apply Qle_refl. + intro abs. pose proof (Pos2Nat.is_pos p). + rewrite abs in H. inversion H. + - intros [p pmaj]. unfold DRealRepr, proj1_sig in pmaj. + destruct x as [xn xcau]. + destruct (DRealQlim (DRealAbstr (exist _ xn xcau)) (Pos.to_nat p)) + as [q [qmaj _]]. + (* By pmaj, x < q - 1/p *) + unfold DRealAbstr, proj1_sig in qmaj. + destruct ( + sig_forall_dec (fun n : nat => (xn (S n) <= q + (1 # Pos.of_nat (S n)))%Q) + (fun n : nat => + match Qlt_le_dec (q + (1 # Pos.of_nat (S n))) (xn (S n)) with + | left q0 => + right (Qlt_not_le (q + (1 # Pos.of_nat (S n))) (xn (S n)) q0) + | right q0 => left q0 + end)). + 2: discriminate. clear qmaj. + destruct s as [n nmaj]. apply nmaj. + apply (Qplus_lt_l _ _ (xn (Pos.to_nat p) + (1#Pos.of_nat (S n)))) in pmaj. + ring_simplify in pmaj. apply Qlt_le_weak. rewrite Qplus_comm. + apply (Qlt_trans _ ((2 # p) + xn (Pos.to_nat p) + (1 # Pos.of_nat (S n)))). + 2: exact pmaj. + apply (Qplus_lt_l _ _ (-xn (Pos.to_nat p))). + apply (Qle_lt_trans _ _ _ (Qle_Qabs _)). + destruct (le_lt_dec (S n) (Pos.to_nat p)). + + specialize (xcau (Pos.of_nat (S n)) (S n) (Pos.to_nat p)). + apply (Qlt_trans _ (1# Pos.of_nat (S n))). apply xcau. + rewrite Nat2Pos.id. apply le_refl. discriminate. + rewrite Nat2Pos.id. exact l. discriminate. + apply (Qplus_lt_l _ _ (-(1#Pos.of_nat (S n)))). + ring_simplify. reflexivity. + + apply (Qlt_trans _ (1#p)). apply xcau. + apply le_S_n in l. apply le_S, l. apply le_refl. + ring_simplify. apply (Qlt_trans _ (2#p)). + unfold Qlt, Qnum, Qden. + apply Z.mul_lt_mono_pos_r. reflexivity. reflexivity. + apply (Qplus_lt_l _ _ (-(2#p))). ring_simplify. reflexivity. +Qed. diff --git a/theories/Reals/ConstructiveCauchyReals.v b/theories/Reals/ConstructiveCauchyReals.v index 965d31d403..b83f8581d0 100644 --- a/theories/Reals/ConstructiveCauchyReals.v +++ b/theories/Reals/ConstructiveCauchyReals.v @@ -16,15 +16,7 @@ Require Import Logic.ConstructiveEpsilon. Require CMorphisms. (** The constructive Cauchy real numbers, ie the Cauchy sequences - of rational numbers. This file is not supposed to be imported, - except in Rdefinitions.v, Raxioms.v, Rcomplete_constr.v - and ConstructiveRIneq.v. - - Constructive real numbers should be considered abstractly, - forgetting the fact that they are implemented as rational sequences. - All useful lemmas of this file are exposed in ConstructiveRIneq.v, - under more abstract names, like Rlt_asym instead of CRealLt_asym. - + of rational numbers. Cauchy reals are Cauchy sequences of rational numbers, equipped with explicit moduli of convergence and @@ -705,6 +697,17 @@ Proof. right. rewrite H0, H. exact c. Qed. +Add Parametric Morphism : CRealLtProp + with signature CRealEq ==> CRealEq ==> iff + as CRealLtProp_morph. +Proof. + intros x y H x0 y0 H0. split. + - intro. apply CRealLtForget. apply CRealLtEpsilon in H1. + rewrite <- H, <- H0. exact H1. + - intro. apply CRealLtForget. apply CRealLtEpsilon in H1. + rewrite H, H0. exact H1. +Qed. + Add Parametric Morphism : CRealLe with signature CRealEq ==> CRealEq ==> iff as CRealLe_morph. @@ -772,6 +775,9 @@ Proof. intro q. exists (fun n => q). apply ConstCauchy. Defined. +Definition inject_Z : Z -> CReal + := fun n => inject_Q (n # 1). + Notation "0" := (inject_Q 0) : CReal_scope. Notation "1" := (inject_Q 1) : CReal_scope. Notation "2" := (inject_Q 2) : CReal_scope. @@ -1324,3 +1330,19 @@ Proof. apply (Qlt_not_le _ _ maj). apply (Qle_trans _ 0). apply (Qplus_le_l _ _ r). ring_simplify. exact H. discriminate. Qed. + +Lemma inject_Z_plus : forall q r : Z, + inject_Z (q + r) == inject_Z q + inject_Z r. +Proof. + intros. unfold inject_Z. + setoid_replace (q + r # 1)%Q with ((q#1) + (r#1))%Q. + apply inject_Q_plus. rewrite Qinv_plus_distr. reflexivity. +Qed. + +Lemma opp_inject_Z : forall n : Z, + inject_Z (-n) == - inject_Z n. +Proof. + intros. unfold inject_Z. + setoid_replace (-n # 1)%Q with (-(n#1))%Q. + rewrite opp_inject_Q. reflexivity. reflexivity. +Qed. diff --git a/theories/Reals/ConstructiveRIneq.v b/theories/Reals/ConstructiveRIneq.v deleted file mode 100644 index e0f08d2fbe..0000000000 --- a/theories/Reals/ConstructiveRIneq.v +++ /dev/null @@ -1,2817 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* 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). - -Infix "==" := Req : R_scope_constr. -Infix "#" := Rappart : R_scope_constr. -Infix "<" := Rlt : R_scope_constr. -Infix ">" := Rgt : R_scope_constr. -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" := (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), p. - exact (f x x abs abs). -Qed. -Hint Immediate Rle_refl: rorders. - -Lemma Req_refl : forall x : R, x == x. -Proof. - intros. split; apply Rle_refl. -Qed. - -Lemma Req_sym : forall x y : R, x == y -> y == x. -Proof. - intros. destruct H. split; intro abs; contradiction. -Qed. - -Lemma Req_trans : forall x y z : R, x == y -> y == z -> x == z. -Proof. - intros. destruct H,H0. destruct (CRltLinear CR), p. split. - - intro abs. destruct (s _ y _ abs); contradiction. - - intro abs. destruct (s _ y _ abs); contradiction. -Qed. - -Add Parametric Relation : R Req - reflexivity proved by Req_refl - symmetry proved by Req_sym - 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). -Proof. - intros. destruct (CRltLinear CR). apply s. exact H. -Qed. - -Instance Rlt_morph - : CMorphisms.Proper - (CMorphisms.respectful Req (CMorphisms.respectful Req CRelationClasses.iffT)) Rlt. -Proof. - 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. - - intro. destruct (linear_order_T y x y0). assumption. - contradiction. destruct (linear_order_T x x0 y0). - assumption. assumption. contradiction. -Qed. - -Instance RltProp_morph - : Morphisms.Proper - (Morphisms.respectful Req (Morphisms.respectful Req iff)) RltProp. -Proof. - 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. - -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 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 - with signature Req ==> Req ==> iff - as Rle_morph. -Proof. - intros. split. - - intros H1 H2. unfold CRealLe in H1. - rewrite <- H0 in H2. rewrite <- H in H2. contradiction. - - intros H1 H2. unfold CRealLe in H1. - rewrite H0 in H2. rewrite H in H2. contradiction. -Qed. - -Add Parametric Morphism : Rge - with signature Req ==> Req ==> iff - as Rge_morph. -Proof. - intros. unfold Rge. apply Rle_morph; assumption. -Qed. - - -Definition Rplus := CRplus CR. -Definition Rmult := CRmult CR. -Definition Rinv := CRinv CR. -Definition Ropp := CRopp CR. - -Add Parametric Morphism : Rplus - with signature Req ==> Req ==> Req - as Rplus_morph. -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. -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 CRisRingExt. -Qed. - -Instance Ropp_morph_T - : CMorphisms.Proper - (CMorphisms.respectful Req Req) Ropp. -Proof. - 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. - -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 - Rminus Ropp - Req. -Proof. - exact (CRisRing CR). -Qed. - -Add Ring CRealRing : RisRing. - -Lemma Rplus_comm : forall x y:R, x + y == y + x. -Proof. intros. ring. Qed. - -Lemma Rplus_assoc : forall x y z:R, (x + y) + z == x + (y + z). -Proof. intros. ring. Qed. - -Lemma Rplus_opp_r : forall x:R, x + -x == 0. -Proof. intros. ring. Qed. - -Lemma Rplus_0_l : forall x:R, 0 + x == x. -Proof. intros. ring. Qed. - -Lemma Rmult_0_l : forall x:R, 0 * x == 0. -Proof. intros. ring. Qed. - -Lemma Rmult_1_l : forall x:R, 1 * x == x. -Proof. intros. ring. Qed. - -Lemma Rmult_comm : forall x y:R, x * y == y * x. -Proof. intros. ring. Qed. - -Lemma Rmult_assoc : forall x y z:R, (x * y) * z == x * (y * z). -Proof. intros. ring. Qed. - -Definition Rinv_l := CRinv_l CR. - -Lemma Rmult_plus_distr_l : forall r1 r2 r3 : R, - r1 * (r2 + r3) == (r1 * r2) + (r1 * r3). -Proof. intros. ring. Qed. - -Definition Rlt_0_1 := CRzero_lt_one CR. - -Lemma Rlt_asym : forall x y :R, x < y -> y < x -> False. -Proof. - 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), p. - apply (c x y); assumption. -Qed. - -Lemma Rplus_lt_compat_l : forall x y z : R, - y < z -> x + y < x + z. -Proof. - intros. apply CRplus_lt_compat_l. exact H. -Qed. - -Lemma Ropp_mult_distr_l - : forall r1 r2 : R, -(r1 * r2) == (- r1) * r2. -Proof. - intros. ring. -Qed. - -Lemma Rplus_lt_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2. -Proof. - 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. 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. - rewrite <- Rmult_plus_distr_l. - apply CRmult_lt_0_compat. exact H. - apply (Rplus_lt_reg_l y). - rewrite Rplus_comm, Rplus_0_l. - rewrite <- Rplus_assoc, H1, Rplus_0_l. exact H0. -Qed. - -Hint Resolve Rplus_comm Rplus_assoc Rplus_opp_r Rplus_0_l - Rmult_comm Rmult_assoc Rinv_l Rmult_1_l Rmult_plus_distr_l - Rlt_0_1 Rlt_asym Rlt_trans Rplus_lt_compat_l Rmult_lt_compat_l - Rmult_0_l : creal. - -Fixpoint INR (n:nat) : R := - match n with - | O => 0 - | S O => 1 - | S n => INR n + 1 - end. -Arguments INR n%nat. - -(* compact representation for 2*p *) -Fixpoint IPR_2 (p:positive) : R := - match p with - | xH => 1 + 1 - | xO p => (1 + 1) * IPR_2 p - | xI p => (1 + 1) * (1 + IPR_2 p) - end. - -Definition IPR (p:positive) : R := - match p with - | xH => 1 - | xO p => IPR_2 p - | xI p => 1 + IPR_2 p - end. -Arguments IPR p%positive : simpl never. - -(**********) -Definition IZR (z:Z) : R := - match z with - | Z0 => 0 - | Zpos n => IPR n - | Zneg n => - IPR n - end. -Arguments IZR z%Z : simpl never. - -Notation "2" := (IZR 2) : R_scope_constr. - - -(*********************************************************) -(** ** Relation between orders and equality *) -(*********************************************************) - -Lemma Rge_refl : forall r, r <= r. -Proof. exact Rle_refl. Qed. -Hint Immediate Rge_refl: rorders. - -(** Irreflexivity of the strict order *) - -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 -> False. -Proof. exact Rlt_irrefl. Qed. - -Lemma Rlt_not_eq : forall r1 r2, r1 < r2 -> r1 <> r2. -Proof. - intros. intro abs. subst r2. exact (Rlt_irrefl r1 H). -Qed. - -Lemma Rgt_not_eq : forall r1 r2, r1 > r2 -> r1 <> r2. -Proof. - intros; apply not_eq_sym; apply Rlt_not_eq; auto with creal. -Qed. - -(**********) -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 r). - - intro abs. subst r2. exact (Rlt_irrefl r1 r). -Qed. -Hint Resolve Rlt_dichotomy_converse: creal. - -(** Reasoning by case on equality and order *) - - -(*********************************************************) -(** ** Relating [<], [>], [<=] and [>=] *) -(*********************************************************) - -(*********************************************************) -(** ** Order *) -(*********************************************************) - -(** *** Relating strict and large orders *) - -Lemma Rlt_le : forall r1 r2, r1 < r2 -> r1 <= r2. -Proof. - intros. intro abs. apply (Rlt_asym r1 r2); assumption. -Qed. -Hint Resolve Rlt_le: creal. - -Lemma Rgt_ge : forall r1 r2, r1 > r2 -> r1 >= r2. -Proof. - intros. intro abs. apply (Rlt_asym r1 r2); assumption. -Qed. - -(**********) -Lemma Rle_ge : forall r1 r2, r1 <= r2 -> r2 >= r1. -Proof. - intros. intros abs. contradiction. -Qed. -Hint Immediate Rle_ge: creal. -Hint Resolve Rle_ge: rorders. - -Lemma Rge_le : forall r1 r2, r1 >= r2 -> r2 <= r1. -Proof. - intros. intro abs. contradiction. -Qed. -Hint Resolve Rge_le: creal. -Hint Immediate Rge_le: rorders. - -(**********) -Lemma Rlt_gt : forall r1 r2, r1 < r2 -> r2 > r1. -Proof. - trivial. -Qed. -Hint Resolve Rlt_gt: rorders. - -Lemma Rgt_lt : forall r1 r2, r1 > r2 -> r2 < r1. -Proof. - trivial. -Qed. -Hint Immediate Rgt_lt: rorders. - -(**********) - -Lemma Rnot_lt_le : forall r1 r2, (r1 < r2 -> False) -> r2 <= r1. -Proof. - intros. exact H. -Qed. - -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 -> False) -> r2 >= r1. -Proof. - intros. intro abs. contradiction. -Qed. - -Lemma Rnot_lt_ge : forall r1 r2, (r1 < r2 -> False) -> r1 >= r2. -Proof. - intros. intro abs. contradiction. -Qed. - -(**********) -Lemma Rlt_not_le : forall r1 r2, r2 < r1 -> ~ r1 <= r2. -Proof. - generalize Rlt_asym Rlt_dichotomy_converse; unfold CRealLe. - unfold not; intuition eauto 3. -Qed. -Hint Immediate Rlt_not_le: creal. - -Lemma Rgt_not_le : forall r1 r2, r1 > r2 -> ~ r1 <= r2. -Proof. exact Rlt_not_le. Qed. - -Lemma Rlt_not_ge : forall r1 r2, r1 < r2 -> ~ r1 >= r2. -Proof. red; intros; eapply Rlt_not_le; eauto with creal. Qed. -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 -> 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 -> False. -Proof. intros; apply (Rle_not_lt r1 r2); auto with creal. Qed. - -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 -> False. -Proof. do 2 intro; apply Rge_not_lt. Qed. - -(**********) -Lemma Req_le : forall r1 r2, r1 = r2 -> r1 <= r2. -Proof. - intros. intro abs. subst r2. exact (Rlt_irrefl r1 abs). -Qed. -Hint Immediate Req_le: creal. - -Lemma Req_ge : forall r1 r2, r1 = r2 -> r1 >= r2. -Proof. - intros. intro abs. subst r2. exact (Rlt_irrefl r1 abs). -Qed. -Hint Immediate Req_ge: creal. - -Lemma Req_le_sym : forall r1 r2, r2 = r1 -> r1 <= r2. -Proof. - intros. intro abs. subst r2. exact (Rlt_irrefl r1 abs). -Qed. -Hint Immediate Req_le_sym: creal. - -Lemma Req_ge_sym : forall r1 r2, r2 = r1 -> r1 >= r2. -Proof. - intros. intro abs. subst r2. exact (Rlt_irrefl r1 abs). -Qed. -Hint Immediate Req_ge_sym: creal. - -(** *** Asymmetry *) - -(** Remark: [Rlt_asym] is an axiom *) - -Lemma Rgt_asym : forall r1 r2, r1 > r2 -> r2 > r1 -> False. -Proof. do 2 intro; apply Rlt_asym. Qed. - - -(** *** Compatibility with equality *) - -Lemma Rlt_eq_compat : - forall r1 r2 r3 r4, r1 = r2 -> r2 < r4 -> r4 = r3 -> r1 < r3. -Proof. - intros x x' y y'; intros; replace x with x'; replace y with y'; assumption. -Qed. - -Lemma Rgt_eq_compat : - forall r1 r2 r3 r4, r1 = r2 -> r2 > r4 -> r4 = r3 -> r1 > r3. -Proof. intros; red; apply Rlt_eq_compat with (r2:=r4) (r4:=r2); auto. Qed. - -(** *** Transitivity *) - -Lemma Rle_trans : forall r1 r2 r3, r1 <= r2 -> r2 <= r3 -> r1 <= r3. -Proof. - intros. intro abs. - destruct (linear_order_T r3 r2 r1 abs); contradiction. -Qed. - -Lemma Rge_trans : forall r1 r2 r3, r1 >= r2 -> r2 >= r3 -> r1 >= r3. -Proof. - intros. apply (Rle_trans _ r2); assumption. -Qed. - -Lemma Rgt_trans : forall r1 r2 r3, r1 > r2 -> r2 > r3 -> r1 > r3. -Proof. - intros. apply (Rlt_trans _ r2); assumption. -Qed. - -(**********) -Lemma Rle_lt_trans : forall r1 r2 r3, r1 <= r2 -> r2 < r3 -> r1 < r3. -Proof. - intros. - destruct (linear_order_T r2 r1 r3 H0). contradiction. apply r. -Qed. - -Lemma Rlt_le_trans : forall r1 r2 r3, r1 < r2 -> r2 <= r3 -> r1 < r3. -Proof. - intros. - destruct (linear_order_T r1 r3 r2 H). apply r. contradiction. -Qed. - -Lemma Rge_gt_trans : forall r1 r2 r3, r1 >= r2 -> r2 > r3 -> r1 > r3. -Proof. - intros. apply (Rlt_le_trans _ r2); assumption. -Qed. - -Lemma Rgt_ge_trans : forall r1 r2 r3, r1 > r2 -> r2 >= r3 -> r1 > r3. -Proof. - intros. apply (Rle_lt_trans _ r2); assumption. -Qed. - - -(*********************************************************) -(** ** Addition *) -(*********************************************************) - -(** Remark: [Rplus_0_l] is an axiom *) - -Lemma Rplus_0_r : forall r, r + 0 == r. -Proof. - intros. rewrite Rplus_comm. rewrite Rplus_0_l. reflexivity. -Qed. -Hint Resolve Rplus_0_r: creal. - -Lemma Rplus_ne : forall r, r + 0 == r /\ 0 + r == r. -Proof. - split. apply Rplus_0_r. apply Rplus_0_l. -Qed. -Hint Resolve Rplus_ne: creal. - -(**********) - -(** Remark: [Rplus_opp_r] is an axiom *) - -Lemma Rplus_opp_l : forall r, - r + r == 0. -Proof. - intros. rewrite Rplus_comm. apply Rplus_opp_r. -Qed. -Hint Resolve Rplus_opp_l: creal. - -(**********) -Lemma Rplus_opp_r_uniq : forall r1 r2, r1 + r2 == 0 -> r2 == - r1. -Proof. - intros x y H. rewrite <- (Rplus_0_l y). - rewrite <- (Rplus_opp_l x). rewrite Rplus_assoc. - rewrite H. rewrite Rplus_0_r. reflexivity. -Qed. - -Lemma Rplus_eq_compat_l : forall r r1 r2, r1 == r2 -> r + r1 == r + r2. -Proof. - intros. rewrite H. reflexivity. -Qed. - -Lemma Rplus_eq_compat_r : forall r r1 r2, r1 == r2 -> r1 + r == r2 + r. -Proof. - intros. rewrite H. reflexivity. -Qed. - - -(**********) -Lemma Rplus_eq_reg_l : forall r r1 r2, r + r1 == r + r2 -> r1 == r2. -Proof. - intros; transitivity (- r + r + r1). - rewrite Rplus_opp_l. rewrite Rplus_0_l. reflexivity. - transitivity (- r + r + r2). - repeat rewrite Rplus_assoc; rewrite <- H; reflexivity. - rewrite Rplus_opp_l. rewrite Rplus_0_l. reflexivity. -Qed. -Hint Resolve Rplus_eq_reg_l: creal. - -Lemma Rplus_eq_reg_r : forall r r1 r2, r1 + r == r2 + r -> r1 == r2. -Proof. - intros r r1 r2 H. - apply Rplus_eq_reg_l with r. - now rewrite 2!(Rplus_comm r). -Qed. - -(**********) -Lemma Rplus_0_r_uniq : forall r r1, r + r1 == r -> r1 == 0. -Proof. - intros. apply (Rplus_eq_reg_l r). rewrite Rplus_0_r. exact H. -Qed. - - -(*********************************************************) -(** ** Multiplication *) -(*********************************************************) - -(**********) -Lemma Rinv_r : forall r (rnz : r # 0), - r # 0 -> r * ((/ r) rnz) == 1. -Proof. - intros. rewrite Rmult_comm. rewrite Rinv_l. - reflexivity. -Qed. -Hint Resolve Rinv_r: creal. - -Lemma Rinv_l_sym : forall r (rnz: r # 0), 1 == (/ r) rnz * r. -Proof. - intros. symmetry. apply Rinv_l. -Qed. -Hint Resolve Rinv_l_sym: creal. - -Lemma Rinv_r_sym : forall r (rnz : r # 0), 1 == r * (/ r) rnz. -Proof. - intros. symmetry. apply Rinv_r. apply rnz. -Qed. -Hint Resolve Rinv_r_sym: creal. - -(**********) -Lemma Rmult_0_r : forall r, r * 0 == 0. -Proof. - intro; ring. -Qed. -Hint Resolve Rmult_0_r: creal. - -(**********) -Lemma Rmult_ne : forall r, r * 1 == r /\ 1 * r == r. -Proof. - intro; split; ring. -Qed. -Hint Resolve Rmult_ne: creal. - -(**********) -Lemma Rmult_1_r : forall r, r * 1 == r. -Proof. - intro; ring. -Qed. -Hint Resolve Rmult_1_r: creal. - -(**********) -Lemma Rmult_eq_compat_l : forall r r1 r2, r1 == r2 -> r * r1 == r * r2. -Proof. - intros. rewrite H. reflexivity. -Qed. - -Lemma Rmult_eq_compat_r : forall r r1 r2, r1 == r2 -> r1 * r == r2 * r. -Proof. - intros. rewrite H. reflexivity. -Qed. - -(**********) -Lemma Rmult_eq_reg_l : forall r r1 r2, r * r1 == r * r2 -> r # 0 -> r1 == r2. -Proof. - intros. transitivity ((/ r) H0 * r * r1). - rewrite Rinv_l. ring. - transitivity ((/ r) H0 * r * r2). - repeat rewrite Rmult_assoc; rewrite H; reflexivity. - rewrite Rinv_l. ring. -Qed. - -Lemma Rmult_eq_reg_r : forall r r1 r2, r1 * r == r2 * r -> r # 0 -> r1 == r2. -Proof. - intros. - apply Rmult_eq_reg_l with (2 := H0). - now rewrite 2!(Rmult_comm r). -Qed. - -(**********) -Lemma Rmult_eq_0_compat : forall r1 r2, r1 == 0 \/ r2 == 0 -> r1 * r2 == 0. -Proof. - intros r1 r2 [H| H]; rewrite H; auto with creal. -Qed. - -Hint Resolve Rmult_eq_0_compat: creal. - -(**********) -Lemma Rmult_eq_0_compat_r : forall r1 r2, r1 == 0 -> r1 * r2 == 0. -Proof. - auto with creal. -Qed. - -(**********) -Lemma Rmult_eq_0_compat_l : forall r1 r2, r2 == 0 -> r1 * r2 == 0. -Proof. - auto with creal. -Qed. - -(**********) -Lemma Rmult_integral_contrapositive : - 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, 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 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. - -Lemma Rmult_integral_contrapositive_currified : - forall r1 r2, r1 # 0 -> r2 # 0 -> (r1 * r2) # 0. -Proof. - intros. apply Rmult_integral_contrapositive. - split; assumption. -Qed. - -(**********) -Lemma Rmult_plus_distr_r : - forall r1 r2 r3, (r1 + r2) * r3 == r1 * r3 + r2 * r3. -Proof. - intros; ring. -Qed. - -(*********************************************************) -(** ** Square function *) -(*********************************************************) - -(***********) -Definition Rsqr (r : R) := r * r. - -Notation "r ²" := (Rsqr r) (at level 1, format "r ²") : R_scope_constr. - -(***********) -Lemma Rsqr_0 : Rsqr 0 == 0. - unfold Rsqr; auto with creal. -Qed. - -(*********************************************************) -(** ** Opposite *) -(*********************************************************) - -(**********) -Lemma Ropp_eq_compat : forall r1 r2, r1 == r2 -> - r1 == - r2. -Proof. - intros. rewrite H. reflexivity. -Qed. -Hint Resolve Ropp_eq_compat: creal. - -(**********) -Lemma Ropp_0 : -0 == 0. -Proof. - ring. -Qed. -Hint Resolve Ropp_0: creal. - -(**********) -Lemma Ropp_eq_0_compat : forall r, r == 0 -> - r == 0. -Proof. - intros; rewrite H; auto with creal. -Qed. -Hint Resolve Ropp_eq_0_compat: creal. - -(**********) -Lemma Ropp_involutive : forall r, - - r == r. -Proof. - intro; ring. -Qed. -Hint Resolve Ropp_involutive: creal. - -(**********) -Lemma Ropp_plus_distr : forall r1 r2, - (r1 + r2) == - r1 + - r2. -Proof. - intros; ring. -Qed. -Hint Resolve Ropp_plus_distr: creal. - -(*********************************************************) -(** ** Opposite and multiplication *) -(*********************************************************) - -Lemma Ropp_mult_distr_l_reverse : forall r1 r2, - r1 * r2 == - (r1 * r2). -Proof. - intros; ring. -Qed. -Hint Resolve Ropp_mult_distr_l_reverse: creal. - -(**********) -Lemma Rmult_opp_opp : forall r1 r2, - r1 * - r2 == r1 * r2. -Proof. - intros; ring. -Qed. -Hint Resolve Rmult_opp_opp: creal. - -Lemma Ropp_mult_distr_r : forall r1 r2, - (r1 * r2) == r1 * - r2. -Proof. - intros; ring. -Qed. - -Lemma Ropp_mult_distr_r_reverse : forall r1 r2, r1 * - r2 == - (r1 * r2). -Proof. - intros; ring. -Qed. - -(*********************************************************) -(** ** Subtraction *) -(*********************************************************) - -Lemma Rminus_0_r : forall r, r - 0 == r. -Proof. - intro r. unfold Rminus. ring. -Qed. -Hint Resolve Rminus_0_r: creal. - -Lemma Rminus_0_l : forall r, 0 - r == - r. -Proof. - intro r. unfold Rminus. ring. -Qed. -Hint Resolve Rminus_0_l: creal. - -(**********) -Lemma Ropp_minus_distr : forall r1 r2, - (r1 - r2) == r2 - r1. -Proof. - intros; ring. -Qed. -Hint Resolve Ropp_minus_distr: creal. - -Lemma Ropp_minus_distr' : forall r1 r2, - (r2 - r1) == r1 - r2. -Proof. - intros; ring. -Qed. - -(**********) -Lemma Rminus_diag_eq : forall r1 r2, r1 == r2 -> r1 - r2 == 0. -Proof. - intros; rewrite H; unfold Rminus; ring. -Qed. -Hint Resolve Rminus_diag_eq: creal. - -(**********) -Lemma Rminus_diag_uniq : forall r1 r2, r1 - r2 == 0 -> r1 == r2. -Proof. - intros r1 r2. unfold Rminus,CRminus; rewrite Rplus_comm; intro. - rewrite <- (Ropp_involutive r2); apply (Rplus_opp_r_uniq (- r2) r1 H). -Qed. -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; reflexivity. -Qed. -Hint Immediate Rminus_diag_uniq_sym: creal. - -Lemma Rplus_minus : forall r1 r2, r1 + (r2 - r1) == r2. -Proof. - intros; ring. -Qed. -Hint Resolve Rplus_minus: creal. - -(**********) -Lemma Rmult_minus_distr_l : - forall r1 r2 r3, r1 * (r2 - r3) == r1 * r2 - r1 * r3. -Proof. - intros; ring. -Qed. - - -(*********************************************************) -(** ** Order and addition *) -(*********************************************************) - -(** *** Compatibility *) - -(** Remark: [Rplus_lt_compat_l] is an axiom *) - -Lemma Rplus_gt_compat_l : forall r r1 r2, r1 > r2 -> r + r1 > r + r2. -Proof. - intros. apply Rplus_lt_compat_l. apply H. -Qed. -Hint Resolve Rplus_gt_compat_l: creal. - -(**********) -Lemma Rplus_lt_compat_r : forall r r1 r2, r1 < r2 -> r1 + r < r2 + r. -Proof. - intros. - rewrite (Rplus_comm r1 r); rewrite (Rplus_comm r2 r). - apply Rplus_lt_compat_l. exact H. -Qed. -Hint Resolve Rplus_lt_compat_r: creal. - -Lemma Rplus_gt_compat_r : forall r r1 r2, r1 > r2 -> r1 + r > r2 + r. -Proof. do 3 intro; apply Rplus_lt_compat_r. Qed. - -(**********) - -Lemma Rplus_lt_reg_r : forall r r1 r2, r1 + r < r2 + r -> r1 < r2. -Proof. - intros. - apply (Rplus_lt_reg_l r). - now rewrite 2!(Rplus_comm r). -Qed. - -Lemma Rplus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2. -Proof. - intros. intro abs. apply Rplus_lt_reg_l in abs. contradiction. -Qed. - -Lemma Rplus_ge_compat_l : forall r r1 r2, r1 >= r2 -> r + r1 >= r + r2. -Proof. - intros. apply Rplus_le_compat_l. apply H. -Qed. -Hint Resolve Rplus_ge_compat_l: creal. - -(**********) -Lemma Rplus_le_compat_r : forall r r1 r2, r1 <= r2 -> r1 + r <= r2 + r. -Proof. - intros. intro abs. apply Rplus_lt_reg_r in abs. contradiction. -Qed. - -Hint Resolve Rplus_le_compat_l Rplus_le_compat_r: creal. - -Lemma Rplus_ge_compat_r : forall r r1 r2, r1 >= r2 -> r1 + r >= r2 + r. -Proof. - intros. apply Rplus_le_compat_r. apply H. -Qed. - -(*********) -Lemma Rplus_lt_compat : - forall r1 r2 r3 r4, r1 < r2 -> r3 < r4 -> r1 + r3 < r2 + r4. -Proof. - intros; apply Rlt_trans with (r2 + r3); auto with creal. -Qed. -Hint Immediate Rplus_lt_compat: creal. - -Lemma Rplus_le_compat : - forall r1 r2 r3 r4, r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4. -Proof. - intros; apply Rle_trans with (r2 + r3); auto with creal. -Qed. -Hint Immediate Rplus_le_compat: creal. - -Lemma Rplus_gt_compat : - forall r1 r2 r3 r4, r1 > r2 -> r3 > r4 -> r1 + r3 > r2 + r4. -Proof. - intros. apply Rplus_lt_compat; assumption. -Qed. - -Lemma Rplus_ge_compat : - forall r1 r2 r3 r4, r1 >= r2 -> r3 >= r4 -> r1 + r3 >= r2 + r4. -Proof. - intros. apply Rplus_le_compat; assumption. -Qed. - -(*********) -Lemma Rplus_lt_le_compat : - forall r1 r2 r3 r4, r1 < r2 -> r3 <= r4 -> r1 + r3 < r2 + r4. -Proof. - intros; apply Rlt_le_trans with (r2 + r3); auto with creal. -Qed. - -Lemma Rplus_le_lt_compat : - forall r1 r2 r3 r4, r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4. -Proof. - intros; apply Rle_lt_trans with (r2 + r3); auto with creal. -Qed. - -Hint Immediate Rplus_lt_le_compat Rplus_le_lt_compat: creal. - -Lemma Rplus_gt_ge_compat : - forall r1 r2 r3 r4, r1 > r2 -> r3 >= r4 -> r1 + r3 > r2 + r4. -Proof. - intros. apply Rplus_lt_le_compat; assumption. -Qed. - -Lemma Rplus_ge_gt_compat : - forall r1 r2 r3 r4, r1 >= r2 -> r3 > r4 -> r1 + r3 > r2 + r4. -Proof. - intros. apply Rplus_le_lt_compat; assumption. -Qed. - -(**********) -Lemma Rplus_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 + r2. -Proof. - intros. apply (Rlt_trans _ (r1+0)). rewrite Rplus_0_r. exact H. - apply Rplus_lt_compat_l. exact H0. -Qed. - -Lemma Rplus_le_lt_0_compat : forall r1 r2, 0 <= r1 -> 0 < r2 -> 0 < r1 + r2. -Proof. - intros. apply (Rle_lt_trans _ (r1+0)). rewrite Rplus_0_r. exact H. - apply Rplus_lt_compat_l. exact H0. -Qed. - -Lemma Rplus_lt_le_0_compat : forall r1 r2, 0 < r1 -> 0 <= r2 -> 0 < r1 + r2. -Proof. - intros x y; intros; rewrite <- Rplus_comm; apply Rplus_le_lt_0_compat; - assumption. -Qed. - -Lemma Rplus_le_le_0_compat : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2. -Proof. - intros. apply (Rle_trans _ (r1+0)). rewrite Rplus_0_r. exact H. - apply Rplus_le_compat_l. exact H0. -Qed. - -(**********) -Lemma sum_inequa_Rle_lt : - forall a x b c y d, - a <= x -> x < b -> c < y -> y <= d -> a + c < x + y < b + d. -Proof. - intros; split. - apply Rlt_le_trans with (a + y); auto with creal. - apply Rlt_le_trans with (b + y); auto with creal. -Qed. - -(** *** Cancellation *) - -Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2. -Proof. - intros. intro abs. apply (Rplus_lt_compat_l r) in abs. contradiction. -Qed. - -Lemma Rplus_le_reg_r : forall r r1 r2, r1 + r <= r2 + r -> r1 <= r2. -Proof. - intros. - apply (Rplus_le_reg_l r). - now rewrite 2!(Rplus_comm r). -Qed. - -Lemma Rplus_gt_reg_l : forall r r1 r2, r + r1 > r + r2 -> r1 > r2. -Proof. - unfold CRealGt; intros; apply (Rplus_lt_reg_l r r2 r1 H). -Qed. - -Lemma Rplus_ge_reg_l : forall r r1 r2, r + r1 >= r + r2 -> r1 >= r2. -Proof. - intros; apply Rle_ge; apply Rplus_le_reg_l with r; auto with creal. -Qed. - -(**********) -Lemma Rplus_le_reg_pos_r : - forall r1 r2 r3, 0 <= r2 -> r1 + r2 <= r3 -> r1 <= r3. -Proof. - intros. apply (Rle_trans _ (r1+r2)). 2: exact H0. - rewrite <- (Rplus_0_r r1), Rplus_assoc. - apply Rplus_le_compat_l. rewrite Rplus_0_l. exact H. -Qed. - -Lemma Rplus_lt_reg_pos_r : forall r1 r2 r3, 0 <= r2 -> r1 + r2 < r3 -> r1 < r3. -Proof. - intros. apply (Rle_lt_trans _ (r1+r2)). 2: exact H0. - rewrite <- (Rplus_0_r r1), Rplus_assoc. - apply Rplus_le_compat_l. rewrite Rplus_0_l. exact H. -Qed. - -Lemma Rplus_ge_reg_neg_r : - forall r1 r2 r3, 0 >= r2 -> r1 + r2 >= r3 -> r1 >= r3. -Proof. - intros. apply (Rge_trans _ (r1+r2)). 2: exact H0. - apply Rle_ge. rewrite <- (Rplus_0_r r1), Rplus_assoc. - apply Rplus_le_compat_l. rewrite Rplus_0_l. exact H. -Qed. - -Lemma Rplus_gt_reg_neg_r : forall r1 r2 r3, 0 >= r2 -> r1 + r2 > r3 -> r1 > r3. -Proof. - intros. apply (Rlt_le_trans _ (r1+r2)). exact H0. - rewrite <- (Rplus_0_r r1), Rplus_assoc. - apply Rplus_le_compat_l. rewrite Rplus_0_l. exact H. -Qed. - -(***********) -Lemma Rplus_eq_0_l : - forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 == 0 -> r1 == 0. -Proof. - intros. split. - - intro abs. rewrite <- (Rplus_opp_r r1) in H1. - apply Rplus_eq_reg_l in H1. rewrite H1 in H0. clear H1. - apply (Rplus_le_compat_l r1) in H0. - rewrite Rplus_opp_r in H0. rewrite Rplus_0_r in H0. - contradiction. - - intro abs. clear H. rewrite <- (Rplus_opp_r r1) in H1. - apply Rplus_eq_reg_l in H1. rewrite H1 in H0. clear H1. - apply (Rplus_le_compat_l r1) in H0. - rewrite Rplus_opp_r in H0. rewrite Rplus_0_r in H0. - contradiction. -Qed. - -Lemma Rplus_eq_R0 : - forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 == 0 -> r1 == 0 /\ r2 == 0. -Proof. - intros a b; split. - apply Rplus_eq_0_l with b; auto with creal. - apply Rplus_eq_0_l with a; auto with creal. - rewrite Rplus_comm; auto with creal. -Qed. - - -(*********************************************************) -(** ** Order and opposite *) -(*********************************************************) - -(** *** Contravariant compatibility *) - -Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2. -Proof. - unfold CRealGt; intros. - apply (Rplus_lt_reg_l (r2 + r1)). - setoid_replace (r2 + r1 + - r1) with r2 by ring. - setoid_replace (r2 + r1 + - r2) with r1 by ring. - exact H. -Qed. -Hint Resolve Ropp_gt_lt_contravar : creal. - -Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2. -Proof. - intros. apply Ropp_gt_lt_contravar. exact H. -Qed. -Hint Resolve Ropp_lt_gt_contravar: creal. - -(**********) -Lemma Ropp_lt_contravar : forall r1 r2, r2 < r1 -> - r1 < - r2. -Proof. - auto with creal. -Qed. -Hint Resolve Ropp_lt_contravar: creal. - -Lemma Ropp_gt_contravar : forall r1 r2, r2 > r1 -> - r1 > - r2. -Proof. auto with creal. Qed. - -(**********) - -Lemma Ropp_lt_cancel : forall r1 r2, - r2 < - r1 -> r1 < r2. -Proof. - intros x y H'. - rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y); - auto with creal. -Qed. -Hint Immediate Ropp_lt_cancel: creal. - -Lemma Ropp_gt_cancel : forall r1 r2, - r2 > - r1 -> r1 > r2. -Proof. - intros. apply Ropp_lt_cancel. apply H. -Qed. - -Lemma Ropp_le_ge_contravar : forall r1 r2, r1 <= r2 -> - r1 >= - r2. -Proof. - intros. intro abs. apply Ropp_lt_cancel in abs. contradiction. -Qed. -Hint Resolve Ropp_le_ge_contravar: creal. - -Lemma Ropp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2. -Proof. - intros. intro abs. apply Ropp_lt_cancel in abs. contradiction. -Qed. -Hint Resolve Ropp_ge_le_contravar: creal. - -(**********) -Lemma Ropp_le_contravar : forall r1 r2, r2 <= r1 -> - r1 <= - r2. -Proof. - intros. intro abs. apply Ropp_lt_cancel in abs. contradiction. -Qed. -Hint Resolve Ropp_le_contravar: creal. - -Lemma Ropp_ge_contravar : forall r1 r2, r2 >= r1 -> - r1 >= - r2. -Proof. - intros. apply Ropp_le_contravar. apply H. -Qed. - -(**********) -Lemma Ropp_0_lt_gt_contravar : forall r, 0 < r -> 0 > - r. -Proof. - intros; setoid_replace 0 with (-0); auto with creal. ring. -Qed. -Hint Resolve Ropp_0_lt_gt_contravar: creal. - -Lemma Ropp_0_gt_lt_contravar : forall r, 0 > r -> 0 < - r. -Proof. - intros; setoid_replace 0 with (-0); auto with creal. ring. -Qed. -Hint Resolve Ropp_0_gt_lt_contravar: creal. - -(**********) -Lemma Ropp_lt_gt_0_contravar : forall r, r > 0 -> - r < 0. -Proof. - intros; rewrite <- Ropp_0; auto with creal. -Qed. -Hint Resolve Ropp_lt_gt_0_contravar: creal. - -Lemma Ropp_gt_lt_0_contravar : forall r, r < 0 -> - r > 0. -Proof. - intros; rewrite <- Ropp_0; auto with creal. -Qed. -Hint Resolve Ropp_gt_lt_0_contravar: creal. - -(**********) -Lemma Ropp_0_le_ge_contravar : forall r, 0 <= r -> 0 >= - r. -Proof. - intros; setoid_replace 0 with (-0); auto with creal. ring. -Qed. -Hint Resolve Ropp_0_le_ge_contravar: creal. - -Lemma Ropp_0_ge_le_contravar : forall r, 0 >= r -> 0 <= - r. -Proof. - intros; setoid_replace 0 with (-0); auto with creal. ring. -Qed. -Hint Resolve Ropp_0_ge_le_contravar: creal. - -(** *** Cancellation *) - -Lemma Ropp_le_cancel : forall r1 r2, - r2 <= - r1 -> r1 <= r2. -Proof. - intros. intro abs. apply Ropp_lt_gt_contravar in abs. contradiction. -Qed. -Hint Immediate Ropp_le_cancel: creal. - -Lemma Ropp_ge_cancel : forall r1 r2, - r2 >= - r1 -> r1 >= r2. -Proof. - intros. apply Ropp_le_cancel. apply H. -Qed. - -(*********************************************************) -(** ** Order and multiplication *) -(*********************************************************) - -(** Remark: [Rmult_lt_compat_l] is an axiom *) - -(** *** Covariant compatibility *) - -Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r. -Proof. - intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with creal. -Qed. -Hint Resolve Rmult_lt_compat_r : core. - -Lemma Rmult_gt_compat_r : forall r r1 r2, r > 0 -> r1 > r2 -> r1 * r > r2 * r. -Proof. - intros. apply Rmult_lt_compat_r; assumption. -Qed. - -Lemma Rmult_gt_compat_l : forall r r1 r2, r > 0 -> r1 > r2 -> r * r1 > r * r2. -Proof. - intros. apply Rmult_lt_compat_l; assumption. -Qed. - -Lemma Rmult_gt_0_lt_compat : - forall r1 r2 r3 r4, - r3 > 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. -Proof. - intros; apply Rlt_trans with (r2 * r3); auto with creal. -Qed. - -(*********) -Lemma Rmult_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 * r2. -Proof. - intros; setoid_replace 0 with (0 * r2); auto with creal. - rewrite Rmult_0_l. reflexivity. -Qed. - -Lemma Rmult_gt_0_compat : forall r1 r2, r1 > 0 -> r2 > 0 -> r1 * r2 > 0. -Proof. - apply Rmult_lt_0_compat. -Qed. - -(** *** Contravariant compatibility *) - -Lemma Rmult_lt_gt_compat_neg_l : - forall r r1 r2, r < 0 -> r1 < r2 -> r * r1 > r * r2. -Proof. - intros; setoid_replace r with (- - r); auto with creal. - rewrite (Ropp_mult_distr_l_reverse (- r)); - rewrite (Ropp_mult_distr_l_reverse (- r)). - apply Ropp_lt_gt_contravar; auto with creal. - rewrite Ropp_involutive. reflexivity. -Qed. - -(** *** Cancellation *) - -Lemma Rinv_0_lt_compat : forall r (rpos : 0 < r), 0 < (/ r) (inr rpos). -Proof. - intros. apply CRinv_0_lt_compat. exact rpos. -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) (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. -Qed. - -Lemma Rmult_lt_reg_r : forall r r1 r2, 0 < r -> r1 * r < r2 * r -> r1 < r2. -Proof. - intros. - apply Rmult_lt_reg_l with r. - exact H. - now rewrite 2!(Rmult_comm r). -Qed. - -Lemma Rmult_gt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2. -Proof. - intros. apply Rmult_lt_reg_l in H0; assumption. -Qed. - -Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2. -Proof. - intros. intro abs. apply (Rmult_lt_compat_l r) in abs. - contradiction. apply H. -Qed. - -Lemma Rmult_le_reg_r : forall r r1 r2, 0 < r -> r1 * r <= r2 * r -> r1 <= r2. -Proof. - intros. - apply Rmult_le_reg_l with r. - exact H. - now rewrite 2!(Rmult_comm r). -Qed. - -(*********************************************************) -(** ** Order and substraction *) -(*********************************************************) - -Lemma Rlt_minus : forall r1 r2, r1 < r2 -> r1 - r2 < 0. -Proof. - intros; apply (Rplus_lt_reg_l r2). - setoid_replace (r2 + (r1 - r2)) with r1 by ring. - now rewrite Rplus_0_r. -Qed. -Hint Resolve Rlt_minus: creal. - -Lemma Rgt_minus : forall r1 r2, r1 > r2 -> r1 - r2 > 0. -Proof. - intros; apply (Rplus_lt_reg_l r2). - setoid_replace (r2 + (r1 - r2)) with r1 by ring. - now rewrite Rplus_0_r. -Qed. - -Lemma Rlt_Rminus : forall a b, a < b -> 0 < b - a. -Proof. - intros a b; apply Rgt_minus. -Qed. - -(**********) -Lemma Rle_minus : forall r1 r2, r1 <= r2 -> r1 - r2 <= 0. -Proof. - intros. intro abs. apply (Rplus_lt_compat_l r2) in abs. - 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. - unfold Rminus in abs. - rewrite Rplus_0_r, Rplus_comm, Rplus_assoc, Rplus_opp_l, Rplus_0_r in abs. - contradiction. -Qed. - -(**********) -Lemma Rminus_lt : forall r1 r2, r1 - r2 < 0 -> r1 < r2. -Proof. - intros. rewrite <- (Rplus_opp_r r2) in H. - apply Rplus_lt_reg_r in H. exact H. -Qed. - -Lemma Rminus_gt : forall r1 r2, r1 - r2 > 0 -> r1 > r2. -Proof. - intros. rewrite <- (Rplus_opp_r r2) in H. - apply Rplus_lt_reg_r in H. exact H. -Qed. - -Lemma Rminus_gt_0_lt : forall a b, 0 < b - a -> a < b. -Proof. intro; intro; apply Rminus_gt. Qed. - -(**********) -Lemma Rminus_le : forall r1 r2, r1 - r2 <= 0 -> r1 <= r2. -Proof. - intros. rewrite <- (Rplus_opp_r r2) in H. - apply Rplus_le_reg_r in H. exact H. -Qed. - -Lemma Rminus_ge : forall r1 r2, r1 - r2 >= 0 -> r1 >= r2. -Proof. - intros. rewrite <- (Rplus_opp_r r2) in H. - apply Rplus_le_reg_r in H. exact H. -Qed. - -(**********) -Lemma tech_Rplus : forall r s, 0 <= r -> 0 < s -> r + s <> 0. -Proof. - intros; apply not_eq_sym; apply Rlt_not_eq. - rewrite Rplus_comm; setoid_replace 0 with (0 + 0); auto with creal. ring. -Qed. -Hint Immediate tech_Rplus: creal. - -(*********************************************************) -(** ** Zero is less than one *) -(*********************************************************) - -Lemma Rle_0_1 : 0 <= 1. -Proof. - intro abs. apply (Rlt_asym 0 1). - apply Rlt_0_1. apply abs. -Qed. - - -(*********************************************************) -(** ** Inverse *) -(*********************************************************) - -Lemma Rinv_1 : forall nz : 1 # 0, (/ 1) nz == 1. -Proof. - intros. rewrite <- (Rmult_1_l ((/1) nz)). rewrite Rinv_r. - reflexivity. right. apply Rlt_0_1. -Qed. -Hint Resolve Rinv_1: creal. - -(*********) -Lemma Ropp_inv_permute : forall r (rnz : r # 0) (ronz : (-r) # 0), - - (/ r) rnz == (/ - r) ronz. -Proof. - intros. - apply (Rmult_eq_reg_l (-r)). rewrite Rinv_r. - rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_r. - rewrite Ropp_involutive. rewrite Rinv_r. reflexivity. - exact rnz. exact ronz. exact ronz. -Qed. - -(*********) -Lemma Rinv_neq_0_compat : forall r (rnz : r # 0), ((/ r) rnz) # 0. -Proof. - intros. destruct rnz. left. - assert (0 < (/-r) (inr (Ropp_0_gt_lt_contravar _ c))). - { apply Rinv_0_lt_compat. } - rewrite <- (Ropp_inv_permute _ (inl c)) in H. - apply Ropp_lt_cancel. rewrite Ropp_0. exact H. - right. apply Rinv_0_lt_compat. -Qed. -Hint Resolve Rinv_neq_0_compat: creal. - -(*********) -Lemma Rinv_involutive : forall r (rnz : r # 0) (rinz : ((/ r) rnz) # 0), - (/ ((/ r) rnz)) rinz == r. -Proof. - intros. apply (Rmult_eq_reg_l ((/r) rnz)). rewrite Rinv_r. - rewrite Rinv_l. reflexivity. exact rinz. exact rinz. -Qed. -Hint Resolve Rinv_involutive: creal. - -(*********) -Lemma Rinv_mult_distr : - forall r1 r2 (r1nz : r1 # 0) (r2nz : r2 # 0) (rmnz : (r1*r2) # 0), - (/ (r1 * r2)) rmnz == (/ r1) r1nz * (/ r2) r2nz. -Proof. - intros. apply (Rmult_eq_reg_l r1). 2: exact r1nz. - rewrite <- Rmult_assoc. rewrite Rinv_r. rewrite Rmult_1_l. - apply (Rmult_eq_reg_l r2). 2: exact r2nz. - rewrite Rinv_r. rewrite <- Rmult_assoc. - rewrite (Rmult_comm r2 r1). rewrite Rinv_r. - reflexivity. exact rmnz. exact r2nz. exact r1nz. -Qed. - -Lemma Rinv_r_simpl_r : forall r1 r2 (rnz : r1 # 0), r1 * (/ r1) rnz * r2 == r2. -Proof. - intros; transitivity (1 * r2); auto with creal. - rewrite Rinv_r; auto with creal. rewrite Rmult_1_l. reflexivity. -Qed. - -Lemma Rinv_r_simpl_l : forall r1 r2 (rnz : r1 # 0), - r2 * r1 * (/ r1) rnz == r2. -Proof. - intros. rewrite Rmult_assoc. rewrite Rinv_r, Rmult_1_r. - reflexivity. exact rnz. -Qed. - -Lemma Rinv_r_simpl_m : forall r1 r2 (rnz : r1 # 0), - r1 * r2 * (/ r1) rnz == r2. -Proof. - intros. rewrite Rmult_comm, <- Rmult_assoc, Rinv_l, Rmult_1_l. - reflexivity. -Qed. -Hint Resolve Rinv_r_simpl_l Rinv_r_simpl_r Rinv_r_simpl_m: creal. - -(*********) -Lemma Rinv_mult_simpl : - forall r1 r2 r3 (r1nz : r1 # 0) (r2nz : r2 # 0), - r1 * (/ r2) r2nz * (r3 * (/ r1) r1nz) == r3 * (/ r2) r2nz. -Proof. - intros a b c; intros. - transitivity (a * (/ a) r1nz * (c * (/ b) r2nz)); auto with creal. - ring. -Qed. - -Lemma Rinv_eq_compat : forall x y (rxnz : x # 0) (rynz : y # 0), - x == y - -> (/ x) rxnz == (/ y) rynz. -Proof. - intros. apply (Rmult_eq_reg_l x). rewrite Rinv_r. - rewrite H. rewrite Rinv_r. reflexivity. - exact rynz. exact rxnz. exact rxnz. -Qed. - - -(*********************************************************) -(** ** Order and inverse *) -(*********************************************************) - -Lemma Rinv_lt_0_compat : forall r (rneg : r < 0), (/ r) (inl rneg) < 0. -Proof. - 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. -Qed. -Hint Resolve Rinv_lt_0_compat: creal. - - - -(*********************************************************) -(** ** Miscellaneous *) -(*********************************************************) - -(**********) -Lemma Rle_lt_0_plus_1 : forall r, 0 <= r -> 0 < r + 1. -Proof. - intros. apply (Rle_lt_trans _ (r+0)). rewrite Rplus_0_r. - exact H. apply Rplus_lt_compat_l. apply Rlt_0_1. -Qed. -Hint Resolve Rle_lt_0_plus_1: creal. - -(**********) -Lemma Rlt_plus_1 : forall r, r < r + 1. -Proof. - intro r. rewrite <- Rplus_0_r. rewrite Rplus_assoc. - apply Rplus_lt_compat_l. rewrite Rplus_0_l. exact Rlt_0_1. -Qed. -Hint Resolve Rlt_plus_1: creal. - -(**********) -Lemma tech_Rgt_minus : forall r1 r2, 0 < r2 -> r1 > r1 - r2. -Proof. - intros. apply (Rplus_lt_reg_r r2). - unfold Rminus, CRminus; rewrite Rplus_assoc, Rplus_opp_l. - apply Rplus_lt_compat_l. exact H. -Qed. - -(*********************************************************) -(** ** Injection from [N] to [R] *) -(*********************************************************) - -(**********) -Lemma S_INR : forall n:nat, INR (S n) == INR n + 1. -Proof. - intro; destruct n. rewrite Rplus_0_l. reflexivity. reflexivity. -Qed. - -(**********) -Lemma IZN : forall n:Z, (0 <= n)%Z -> { m : nat | n = Z.of_nat m }. -Proof. - intros. exists (Z.to_nat n). rewrite Z2Nat.id. reflexivity. assumption. -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. exfalso. inversion H. - - intros. unfold lt in H. apply le_S_n in H. destruct m. - 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 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. - apply Rplus_lt_compat_l. rewrite Rplus_0_l. - exact Rlt_0_1. -Qed. - -(**********) -Lemma S_O_plus_INR : forall n:nat, INR (1 + n) == INR 1 + INR n. -Proof. - intros; destruct n. - - rewrite Rplus_comm, Rplus_0_l. reflexivity. - - rewrite Rplus_comm. reflexivity. -Qed. - -(**********) -Lemma plus_INR : forall n m:nat, INR (n + m) == INR n + INR m. -Proof. - intros n m; induction n as [| n Hrecn]. - - rewrite Rplus_0_l. reflexivity. - - replace (S n + m)%nat with (S (n + m)); auto with arith. - repeat rewrite S_INR. - rewrite Hrecn; ring. -Qed. - -(**********) -Lemma minus_INR : forall n m:nat, (m <= n)%nat -> INR (n - m) == INR n - INR m. -Proof. - intros n m le; pattern m, n; apply le_elim_rel. - intros. rewrite <- minus_n_O. simpl. - unfold Rminus, CRminus. rewrite Ropp_0, Rplus_0_r. reflexivity. - intros; repeat rewrite S_INR; simpl. - rewrite H0. unfold Rminus. ring. exact le. -Qed. - -(*********) -Lemma mult_INR : forall n m:nat, INR (n * m) == INR n * INR m. -Proof. - intros n m; induction n as [| n Hrecn]. - - rewrite Rmult_0_l. reflexivity. - - intros; repeat rewrite S_INR; simpl. - rewrite plus_INR. rewrite Hrecn; ring. -Qed. - -Lemma INR_IPR : forall p, INR (Pos.to_nat p) == IPR p. -Proof. - assert (H: forall p, 2 * INR (Pos.to_nat p) == IPR_2 p). - { induction p as [p|p|]. - - unfold IPR_2; rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- IHp. - rewrite Rplus_comm. reflexivity. - - unfold IPR_2; now rewrite Pos2Nat.inj_xO, mult_INR, <- IHp. - - apply Rmult_1_r. } - intros [p|p|] ; unfold IPR. - rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- H. - apply Rplus_comm. - now rewrite Pos2Nat.inj_xO, mult_INR, <- H. - easy. -Qed. - -Fixpoint pow (r:R) (n:nat) : R := - match n with - | O => 1 - | S n => r * (pow r n) - end. - -Lemma Rpow_eq_compat : forall (x y : R) (n : nat), - x == y -> pow x n == pow y n. -Proof. - intro x. induction n. - - reflexivity. - - intros. simpl. rewrite IHn, H. reflexivity. exact H. -Qed. - -Lemma pow_INR (m n: nat) : INR (m ^ n) == pow (INR m) n. -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. - intros. apply (lt_INR 0). exact H. -Qed. -Hint Resolve lt_0_INR: creal. - -Lemma lt_1_INR : forall n:nat, (1 < n)%nat -> 1 < INR n. -Proof. - apply lt_INR. -Qed. -Hint Resolve lt_1_INR: creal. - -(**********) -Lemma pos_INR_nat_of_P : forall p:positive, 0 < INR (Pos.to_nat p). -Proof. - intro; apply lt_0_INR. - simpl; auto with creal. - apply Pos2Nat.is_pos. -Qed. -Hint Resolve pos_INR_nat_of_P: creal. - -(**********) -Lemma pos_INR : forall n:nat, 0 <= INR n. -Proof. - intro n; case n. - simpl; auto with creal. - auto with arith creal. -Qed. -Hint Resolve pos_INR: creal. - -Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat. -Proof. - intros n m. revert n. - induction m ; intros n H. - - elim (Rlt_irrefl 0). - apply Rle_lt_trans with (2 := H). - apply pos_INR. - - destruct n as [|n]. - apply Nat.lt_0_succ. - apply lt_n_S, IHm. - rewrite 2!S_INR in H. - apply Rplus_lt_reg_r with (1 := H). -Qed. -Hint Resolve INR_lt: creal. - -(*********) -Lemma le_INR : forall n m:nat, (n <= m)%nat -> INR n <= INR m. -Proof. - simple induction 1; intros; auto with creal. - rewrite S_INR. - apply Rle_trans with (INR m0); auto with creal. -Qed. -Hint Resolve le_INR: creal. - -(**********) -Lemma INR_not_0 : forall n:nat, INR n <> 0 -> n <> 0%nat. -Proof. - red; intros n H H1. - apply H. - rewrite H1; trivial. -Qed. -Hint Immediate INR_not_0: creal. - -(**********) -Lemma not_0_INR : forall n:nat, n <> 0%nat -> 0 < INR n. -Proof. - intro n; case n. - intro; absurd (0%nat = 0%nat); trivial. - intros; rewrite S_INR. - apply (Rlt_le_trans _ (0 + 1)). rewrite Rplus_0_l. apply Rlt_0_1. - apply Rplus_le_compat_r. apply pos_INR. -Qed. -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_lt_dec n m); intros H1. - left. apply lt_INR. - case (le_lt_or_eq _ _ H1); intros H2. - exact H2. contradiction. - right. apply lt_INR. exact H1. -Qed. -Hint Resolve not_INR: creal. - -Lemma INR_eq : forall n m:nat, INR n == INR m -> n = m. -Proof. - intros n m HR. - destruct (dec_eq_nat n m) as [H|H]. - exact H. exfalso. - apply not_INR in H. destruct HR,H; contradiction. -Qed. -Hint Resolve INR_eq: creal. - -Lemma INR_le : forall n m:nat, INR n <= INR m -> (n <= m)%nat. -Proof. - intros n m. revert n. - induction m ; intros n H. - - destruct n. apply le_refl. exfalso. - rewrite S_INR in H. - assert (0 + 1 <= 0). apply (Rle_trans _ (INR n + 1)). - apply Rplus_le_compat_r. apply pos_INR. apply H. - rewrite Rplus_0_l in H0. apply H0. apply Rlt_0_1. - - destruct n as [|n]. apply le_0_n. - apply le_n_S, IHm. - rewrite 2!S_INR in H. - apply Rplus_le_reg_r in H. apply H. -Qed. -Hint Resolve INR_le: creal. - -Lemma not_1_INR : forall n:nat, n <> 1%nat -> INR n # 1. -Proof. - intros n. - apply not_INR. -Qed. -Hint Resolve not_1_INR: creal. - -(*********************************************************) -(** ** Injection from [Z] to [R] *) -(*********************************************************) - -Lemma IPR_pos : forall p:positive, 0 < IPR p. -Proof. - intro p. rewrite <- INR_IPR. apply (lt_INR 0), Pos2Nat.is_pos. -Qed. - -Lemma IPR_double : forall p:positive, IPR (2*p) == 2 * IPR p. -Proof. - intro p. destruct p; try reflexivity. - rewrite Rmult_1_r. reflexivity. -Qed. - -Lemma INR_IZR_INZ : forall n:nat, INR n == IZR (Z.of_nat n). -Proof. - intros [|n]. - easy. - simpl Z.of_nat. unfold IZR. - now rewrite <- INR_IPR, SuccNat2Pos.id_succ. -Qed. - -Lemma plus_IZR_NEG_POS : - forall p q:positive, IZR (Zpos p + Zneg q) == IZR (Zpos p) + IZR (Zneg q). -Proof. - intros p q; simpl. rewrite Z.pos_sub_spec. - case Pos.compare_spec; intros H; unfold IZR. - subst. ring. - rewrite <- 3!INR_IPR, Pos2Nat.inj_sub. - rewrite minus_INR. - 2: (now apply lt_le_weak, Pos2Nat.inj_lt). - ring. - trivial. - rewrite <- 3!INR_IPR, Pos2Nat.inj_sub. - rewrite minus_INR. - 2: (now apply lt_le_weak, Pos2Nat.inj_lt). - unfold Rminus. ring. trivial. -Qed. - -Lemma plus_IPR : forall n m:positive, IPR (n + m) == IPR n + IPR m. -Proof. - intros. repeat rewrite <- INR_IPR. - rewrite Pos2Nat.inj_add. apply plus_INR. -Qed. - -(**********) -Lemma plus_IZR : forall n m:Z, IZR (n + m) == IZR n + IZR m. -Proof. - intro z; destruct z; intro t; destruct t; intros. - - rewrite Rplus_0_l. reflexivity. - - rewrite Rplus_0_l. rewrite Z.add_0_l. reflexivity. - - rewrite Rplus_0_l. reflexivity. - - rewrite Rplus_comm,Rplus_0_l. reflexivity. - - rewrite <- Pos2Z.inj_add. unfold IZR. apply plus_IPR. - - apply plus_IZR_NEG_POS. - - rewrite Rplus_comm,Rplus_0_l, Z.add_0_r. reflexivity. - - rewrite Z.add_comm; rewrite Rplus_comm; apply plus_IZR_NEG_POS. - - simpl. unfold IZR. rewrite <- 3!INR_IPR, Pos2Nat.inj_add, plus_INR. - ring. -Qed. - -Lemma mult_IPR : forall n m:positive, IPR (n * m) == IPR n * IPR m. -Proof. - intros. repeat rewrite <- INR_IPR. - rewrite Pos2Nat.inj_mul. apply mult_INR. -Qed. - -(**********) -Lemma mult_IZR : forall n m:Z, IZR (n * m) == IZR n * IZR m. -Proof. - intros n m. destruct n. - - rewrite Rmult_0_l. rewrite Z.mul_0_l. reflexivity. - - destruct m. rewrite Z.mul_0_r, Rmult_0_r. reflexivity. - simpl; unfold IZR. apply mult_IPR. - simpl. unfold IZR. rewrite mult_IPR. ring. - - destruct m. rewrite Z.mul_0_r, Rmult_0_r. reflexivity. - simpl. unfold IZR. rewrite mult_IPR. ring. - simpl. unfold IZR. rewrite mult_IPR. ring. -Qed. - -Lemma pow_IZR : forall z n, pow (IZR z) n == IZR (Z.pow z (Z.of_nat n)). -Proof. - intros z [|n];simpl; trivial. reflexivity. - rewrite Zpower_pos_nat. - rewrite SuccNat2Pos.id_succ. unfold Zpower_nat;simpl. - rewrite mult_IZR. - induction n;simpl;trivial. reflexivity. - rewrite mult_IZR;ring[IHn]. -Qed. - -(**********) -Lemma succ_IZR : forall n:Z, IZR (Z.succ n) == IZR n + 1. -Proof. - intro; unfold Z.succ; apply plus_IZR. -Qed. - -(**********) -Lemma opp_IZR : forall n:Z, IZR (- n) == - IZR n. -Proof. - intros [|z|z]; unfold IZR; simpl; auto with creal. - ring. - reflexivity. rewrite Ropp_involutive. reflexivity. -Qed. - -Definition Ropp_Ropp_IZR := opp_IZR. - -Lemma minus_IZR : forall n m:Z, IZR (n - m) == IZR n - IZR m. -Proof. - intros; unfold Z.sub, Rminus,CRminus. - rewrite <- opp_IZR. - apply plus_IZR. -Qed. - -(**********) -Lemma Z_R_minus : forall n m:Z, IZR n - IZR m == IZR (n - m). -Proof. - intros z1 z2; unfold Rminus,CRminus; unfold Z.sub. - rewrite <- (Ropp_Ropp_IZR z2); symmetry; apply plus_IZR. -Qed. - -(**********) -Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z. -Proof. - intro z; case z; simpl; intros. - elim (Rlt_irrefl _ H). - easy. - elim (Rlt_not_le _ _ H). - unfold IZR. - rewrite <- INR_IPR. - auto with creal. -Qed. - -(**********) -Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z. -Proof. - intros z1 z2 H; apply Z.lt_0_sub. - apply lt_0_IZR. - rewrite <- Z_R_minus. - exact (Rgt_minus (IZR z2) (IZR z1) H). -Qed. - -(**********) -Lemma eq_IZR_R0 : forall n:Z, IZR n == 0 -> n = 0%Z. -Proof. - intro z; destruct z; simpl; intros; auto with zarith. - unfold IZR in H. rewrite <- INR_IPR in H. - apply (INR_eq _ 0) in H. - exfalso. pose proof (Pos2Nat.is_pos p). - rewrite H in H0. inversion H0. - unfold IZR in H. rewrite <- INR_IPR in H. - apply (Rplus_eq_compat_r (INR (Pos.to_nat p))) in H. - rewrite Rplus_opp_l, Rplus_0_l in H. symmetry in H. - apply (INR_eq _ 0) in H. - exfalso. pose proof (Pos2Nat.is_pos p). - rewrite H in H0. inversion H0. -Qed. - -(**********) -Lemma eq_IZR : forall n m:Z, IZR n == IZR m -> n = m. -Proof. - intros z1 z2 H; generalize (Rminus_diag_eq (IZR z1) (IZR z2) H); - rewrite (Z_R_minus z1 z2); intro; generalize (eq_IZR_R0 (z1 - z2) H0); - intro; omega. -Qed. - -Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m. -Proof. - assert (forall n:Z, Z.lt 0 n -> 0 < IZR n) as posCase. - { intros. destruct (IZN n). apply Z.lt_le_incl. apply H. - subst n. rewrite <- INR_IZR_INZ. apply (lt_INR 0). - apply Nat2Z.inj_lt. apply H. } - intros. apply (Rplus_lt_reg_r (-(IZR n))). - pose proof minus_IZR. unfold Rminus,CRminus in H0. - repeat rewrite <- H0. unfold Zminus. - rewrite Z.add_opp_diag_r. apply posCase. - rewrite (Z.add_lt_mono_l _ _ n). ring_simplify. apply H. -Qed. - -(**********) -Lemma not_0_IZR : forall n:Z, n <> 0%Z -> IZR n # 0. -Proof. - intros. destruct n. exfalso. apply H. reflexivity. - right. apply (IZR_lt 0). reflexivity. - left. apply (IZR_lt _ 0). reflexivity. -Qed. - -(*********) -Lemma le_0_IZR : forall n:Z, 0 <= IZR n -> (0 <= n)%Z. -Proof. - intros. destruct n. discriminate. discriminate. - exfalso. rewrite <- Ropp_0 in H. unfold IZR in H. apply H. - apply Ropp_gt_lt_contravar. rewrite <- INR_IPR. - apply (lt_INR 0). apply Pos2Nat.is_pos. -Qed. - -(**********) -Lemma le_IZR : forall n m:Z, IZR n <= IZR m -> (n <= m)%Z. -Proof. - intros. apply (Rplus_le_compat_r (-(IZR n))) in H. - pose proof minus_IZR. unfold Rminus,CRminus in H0. - repeat rewrite <- H0 in H. unfold Zminus in H. - rewrite Z.add_opp_diag_r in H. - apply (Z.add_le_mono_l _ _ (-n)). ring_simplify. - rewrite Z.add_comm. apply le_0_IZR. apply H. -Qed. - -(**********) -Lemma le_IZR_R1 : forall n:Z, IZR n <= 1 -> (n <= 1)%Z. -Proof. - intros. apply (le_IZR n 1). apply H. -Qed. - -(**********) -Lemma IZR_ge : forall n m:Z, (n >= m)%Z -> IZR n >= IZR m. -Proof. - 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_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 (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. -Hint Extern 0 (IZR _ >= IZR _) => apply Rle_ge, IZR_le, Zle_bool_imp_le, eq_refl : creal. -Hint Extern 0 (IZR _ < IZR _) => apply IZR_lt, eq_refl : creal. -Hint Extern 0 (IZR _ > IZR _) => apply IZR_lt, eq_refl : creal. -Hint Extern 0 (IZR _ <> IZR _) => apply IZR_neq, Zeq_bool_neq, eq_refl : creal. - -Lemma one_IZR_lt1 : forall n:Z, -(1) < IZR n < 1 -> n = 0%Z. -Proof. - intros z [H1 H2]. - apply Z.le_antisymm. - apply Z.lt_succ_r; apply lt_IZR; trivial. - change 0%Z with (Z.succ (-1)). - apply Z.le_succ_l; apply lt_IZR; trivial. -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 r z x [H1 H2] [H3 H4]. - cut ((z - x)%Z = 0%Z); auto with zarith. - apply one_IZR_lt1. - split; rewrite <- Z_R_minus. - setoid_replace (-(1)) with (r - (r + 1)). - unfold CReal_minus; apply Rplus_lt_le_compat; auto with creal. - ring. - setoid_replace 1 with (r + 1 - r). - unfold CReal_minus; apply Rplus_le_lt_compat; auto with creal. - ring. -Qed. - - -(**********) -Lemma single_z_r_R1 : - forall r (n m:Z), - r < IZR n -> IZR n <= r + 1 -> r < IZR m -> IZR m <= r + 1 -> n = m. -Proof. - intros; apply one_IZR_r_R1 with r; auto. -Qed. - -(**********) -Lemma tech_single_z_r_R1 : - forall r (n:Z), - r < IZR n -> - IZR n <= r + 1 -> - { 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. -Qed. - - -Lemma Rmult_le_compat_l_half : forall r r1 r2, - 0 < r -> r1 <= r2 -> r * r1 <= r * r2. -Proof. - intros. intro abs. apply (Rmult_lt_reg_l) in abs. - contradiction. apply H. -Qed. - -Lemma INR_CR_of_Q : forall (n : nat), - CR_of_Q CR (Z.of_nat n # 1) == INR n. -Proof. - induction n. - - apply CR_of_Q_zero. - - transitivity (CR_of_Q CR (1 + (Z.of_nat n # 1))). - replace (S n) with (1 + n)%nat. 2: reflexivity. - rewrite (Nat2Z.inj_add 1 n). - apply CR_of_Q_proper. - rewrite <- (Qinv_plus_distr (Z.of_nat 1) (Z.of_nat n) 1). reflexivity. - rewrite CR_of_Q_plus. rewrite IHn. clear IHn. - setoid_replace (INR (S n)) with (1 + INR n). - rewrite CR_of_Q_one. reflexivity. - simpl. destruct n. rewrite Rplus_0_r. reflexivity. - rewrite Rplus_comm. reflexivity. -Qed. - -Definition Rup_nat (x : R) - : { n : nat & x < INR n }. -Proof. - intros. destruct (CR_archimedean CR x) as [p maj]. - exists (Pos.to_nat p). - rewrite <- INR_CR_of_Q, positive_nat_Z. exact maj. -Qed. - -Fixpoint Rarchimedean_ind (x:R) (n : Z) (p:nat) { struct p } - : (x < IZR n < x + 2 + (INR p)) - -> { n:Z & x < IZR n < x+2 }. -Proof. - destruct p. - - 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. - split; rewrite plus_IZR, opp_IZR. - setoid_replace (IZR 1) with 1. 2: reflexivity. - 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 }. -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). - split; rewrite <- INR_IZR_INZ. exact nmaj. - rewrite Rplus_comm in pmaj. exact pmaj. -Qed. - -Lemma Rmult_le_0_compat : forall a b, - 0 <= a -> 0 <= b -> 0 <= a * b. -Proof. - (* Limit of (a + 1/n)*b when n -> infty. *) - 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))) (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. - rewrite Rmult_0_l in maj. - rewrite Rmult_assoc in maj. rewrite Rinv_l in maj. - rewrite Rmult_1_r in maj. contradiction. - apply epsPos. - - (* 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))) (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))) (inr nPos)) - 0 b). - 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))) (inr nPos))). - apply H1. -Qed. - -Lemma Rmult_le_compat_l : forall r r1 r2, - 0 <= r -> r1 <= r2 -> r * r1 <= r * r2. -Proof. - intros. apply Rminus_ge. apply Rge_minus in H0. - unfold Rminus,CRminus. rewrite Ropp_mult_distr_r. - rewrite <- Rmult_plus_distr_l. - apply Rmult_le_0_compat; assumption. -Qed. -Hint Resolve Rmult_le_compat_l: creal. - -Lemma Rmult_le_compat_r : forall r r1 r2, - 0 <= r -> r1 <= r2 -> r1 * r <= r2 * r. -Proof. - intros. rewrite <- (Rmult_comm r). rewrite <- (Rmult_comm r). - apply Rmult_le_compat_l; assumption. -Qed. -Hint Resolve Rmult_le_compat_r: creal. - -(*********) -Lemma Rmult_le_0_lt_compat : - forall r1 r2 r3 r4, - 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. 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. - -Lemma Rmult_le_compat_neg_l : - forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r2 <= r * r1. -Proof. - intros. apply Ropp_le_cancel. - do 2 rewrite Ropp_mult_distr_l. apply Rmult_le_compat_l. - 2: exact H0. apply Ropp_0_ge_le_contravar. exact H. -Qed. -Hint Resolve Rmult_le_compat_neg_l: creal. - -Lemma Rmult_le_ge_compat_neg_l : - forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r1 >= r * r2. -Proof. - intros; apply Rle_ge; auto with creal. -Qed. -Hint Resolve Rmult_le_ge_compat_neg_l: creal. - - -(**********) -Lemma Rmult_ge_compat_l : - forall r r1 r2, r >= 0 -> r1 >= r2 -> r * r1 >= r * r2. -Proof. - intros. apply Rmult_le_compat_l; assumption. -Qed. - -Lemma Rmult_ge_compat_r : - forall r r1 r2, r >= 0 -> r1 >= r2 -> r1 * r >= r2 * r. -Proof. - intros. apply Rmult_le_compat_r; assumption. -Qed. - - -(**********) -Lemma Rmult_le_compat : - forall r1 r2 r3 r4, - 0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4. -Proof. - intros x y z t H' H'0 H'1 H'2. - apply Rle_trans with (r2 := x * t); auto with creal. - repeat rewrite (fun x => Rmult_comm x t). - apply Rmult_le_compat_l; auto. - apply Rle_trans with z; auto. -Qed. -Hint Resolve Rmult_le_compat: creal. - -Lemma Rmult_ge_compat : - forall r1 r2 r3 r4, - r2 >= 0 -> r4 >= 0 -> r1 >= r2 -> r3 >= r4 -> r1 * r3 >= r2 * r4. -Proof. auto with creal rorders. Qed. - -Lemma mult_IPR_IZR : forall (n:positive) (m:Z), IZR (Z.pos n * m) == IPR n * IZR m. -Proof. - intros. rewrite mult_IZR. apply Rmult_eq_compat_r. reflexivity. -Qed. - -Definition IQR (q:Q) : R := - match q with - | Qmake a b => IZR a * (/ (IPR b)) (inr (IPR_pos b)) - end. -Arguments IQR q%Q : simpl never. - -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)) (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) (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 - _ _ _ _ (inr (Rmult_lt_0_compat _ _ (IPR_pos _) (IPR_pos _)))). - apply Rinv_eq_compat. apply mult_IPR. -Qed. - -Lemma IQR_pos : forall q:Q, Qlt 0 q -> 0 < IQR q. -Proof. - intros. destruct q; unfold IQR. - apply Rmult_lt_0_compat. apply (IZR_lt 0). - unfold Qlt in H; simpl in H. - rewrite Z.mul_1_r in H. apply H. - apply Rinv_0_lt_compat. -Qed. - -Lemma opp_IQR : forall q:Q, IQR (- q) == - IQR q. -Proof. - intros [a b]; unfold IQR; simpl. - rewrite Ropp_mult_distr_l. - rewrite opp_IZR. reflexivity. -Qed. - -Lemma lt_IQR : forall n m:Q, IQR n < IQR m -> (n < m)%Q. -Proof. - intros. destruct n,m; unfold IQR in H. - unfold Qlt; simpl. apply (Rmult_lt_compat_r (IPR Qden)) in H. - rewrite Rmult_assoc in H. rewrite Rinv_l in H. - rewrite Rmult_1_r in H. rewrite (Rmult_comm (IZR Qnum0)) in H. - apply (Rmult_lt_compat_l (IPR Qden0)) in H. - do 2 rewrite <- Rmult_assoc in H. rewrite Rinv_r in H. - rewrite Rmult_1_l in H. - rewrite (Rmult_comm (IZR Qnum0)) in H. - do 2 rewrite <- mult_IPR_IZR in H. apply lt_IZR in H. - rewrite Z.mul_comm. rewrite (Z.mul_comm Qnum0). - apply H. - right. rewrite <- INR_IPR. apply (lt_INR 0). apply Pos2Nat.is_pos. - rewrite <- INR_IPR. apply (lt_INR 0). apply Pos2Nat.is_pos. - apply IPR_pos. -Qed. - -Lemma IQR_lt : forall n m:Q, Qlt n m -> IQR n < IQR m. -Proof. - intros. apply (Rplus_lt_reg_r (-IQR n)). - rewrite Rplus_opp_r. rewrite <- opp_IQR. rewrite <- plus_IQR. - apply IQR_pos. apply (Qplus_lt_l _ _ n). - ring_simplify. apply H. -Qed. - -Lemma IQR_nonneg : forall q:Q, Qle 0 q -> 0 <= (IQR q). -Proof. - intros [a b] H. unfold IQR;simpl. - apply (Rle_trans _ (IZR a * 0)). rewrite Rmult_0_r. apply Rle_refl. - 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. - 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. -Proof. - intros. apply (Rplus_le_reg_r (-IQR n)). - rewrite Rplus_opp_r. rewrite <- opp_IQR. rewrite <- plus_IQR. - apply IQR_nonneg. apply (Qplus_le_l _ _ n). - ring_simplify. apply H. -Qed. - -Add Parametric Morphism : IQR - with signature Qeq ==> Req - as IQR_morph. -Proof. - intros. destruct x,y; unfold IQR; simpl. - unfold Qeq in H; simpl in H. - apply (Rmult_eq_reg_r (IZR (Z.pos Qden))). - rewrite Rmult_assoc. rewrite Rinv_l. rewrite Rmult_1_r. - rewrite (Rmult_comm (IZR Qnum0)). - apply (Rmult_eq_reg_l (IZR (Z.pos Qden0))). - rewrite <- Rmult_assoc. rewrite <- Rmult_assoc. rewrite Rinv_r. - rewrite Rmult_1_l. - repeat rewrite <- mult_IZR. - rewrite <- H. rewrite Zmult_comm. reflexivity. - right. apply IPR_pos. - right. apply (IZR_lt 0). apply Pos2Z.is_pos. - 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 }. -Proof. - (* Decreasing loop on n, until it is the first integer above a. *) - intros H H0. destruct n. - - exfalso. apply (Rlt_asym 0 a); assumption. - - destruct n as [|p] eqn:des. - + (* n = 1 *) exists O. split. - apply H. rewrite Rplus_0_l. apply (Rlt_trans a (1+0)). - rewrite Rplus_comm, Rplus_0_l. apply H0. - apply Rplus_le_lt_compat. - apply Rle_refl. apply Rlt_0_1. - + (* n > 1 *) - destruct (linear_order_T (INR p) a (INR (S p))). - * rewrite <- Rplus_0_l, S_INR, Rplus_comm. apply Rplus_lt_compat_l. - apply Rlt_0_1. - * exists p. split. exact r. - rewrite S_INR, S_INR, Rplus_assoc in H0. exact H0. - * apply (Rfloor_pos a n H). rewrite des. apply r. -Qed. - -Definition Rfloor (a : R) - : { 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). 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. split; rewrite opp_IZR, plus_IZR. - + rewrite <- (Ropp_involutive a). apply Ropp_gt_lt_contravar. - destruct p as [_ a0]. apply (Rplus_lt_reg_r 1). - rewrite Rplus_comm, Rplus_assoc. rewrite <- INR_IZR_INZ. apply a0. - + 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. - -(* A point in an archimedean field is the limit of a - sequence of rational numbers (n maps to the q between - a and a+1/n). This is how real numbers compute, - and they are measured by exact rational numbers. *) -Definition RQ_dense (a b : R) - : a < b -> { q : Q & a < IQR q < b }. -Proof. - intros 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)) (inr epsPos))) - as [n maj]. - destruct n as [|k]. - - exfalso. - apply (Rmult_lt_compat_l (b-a)) in maj. 2: apply epsPos. - rewrite Rmult_0_r in maj. rewrite Rinv_r in maj. - apply (Rlt_asym 0 1). apply Rlt_0_1. apply maj. - right. apply epsPos. - - (* 0 < n *) - pose (Pos.of_nat (S k)) as n. - destruct (Rfloor (IZR (2 * Z.pos n) * b)) as [p maj2]. - exists (p # (2*n))%Q. split. - + apply (Rlt_trans a (b - IQR (1 # n))). - apply (Rplus_lt_reg_r (IQR (1#n))). - unfold Rminus,CRminus. rewrite Rplus_assoc. rewrite Rplus_opp_l. - rewrite Rplus_0_r. apply (Rplus_lt_reg_l (-a)). - rewrite <- Rplus_assoc, Rplus_opp_l, Rplus_0_l. - rewrite Rplus_comm. unfold IQR. - rewrite Rmult_1_l. apply (Rmult_lt_reg_l (IPR n)). - apply IPR_pos. rewrite Rinv_r. - apply (Rmult_lt_compat_l (b-a)) in maj. - rewrite Rinv_r, Rmult_comm in maj. - rewrite <- INR_IPR. unfold n. rewrite Nat2Pos.id. - apply maj. discriminate. right. exact epsPos. exact epsPos. - right. apply IPR_pos. - apply (Rplus_lt_reg_r (IQR (1 # n))). - unfold Rminus,CRminus. rewrite Rplus_assoc, Rplus_opp_l. - rewrite Rplus_0_r. rewrite <- plus_IQR. - destruct maj2 as [_ maj2]. - setoid_replace ((p # 2 * n) + (1 # n))%Q - with ((p + 2 # 2 * n))%Q. unfold IQR. - apply (Rmult_lt_reg_r (IZR (Z.pos (2 * n)))). - apply (IZR_lt 0). reflexivity. rewrite Rmult_assoc. - rewrite Rinv_l. rewrite Rmult_1_r. rewrite Rmult_comm. - rewrite plus_IZR. apply maj2. - setoid_replace (1#n)%Q with (2#2*n)%Q. 2: reflexivity. - apply Qinv_plus_distr. - + destruct maj2 as [maj2 _]. unfold IQR. - apply (Rmult_lt_reg_r (IZR (Z.pos (2 * n)))). - apply (IZR_lt 0). apply Pos2Z.is_pos. rewrite Rmult_assoc, Rinv_l. - rewrite Rmult_1_r, Rmult_comm. apply maj2. -Qed. - -Definition RQ_limit : forall (x : R) (n:nat), - { 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. - apply Rplus_lt_compat_l. rewrite Rplus_0_l. apply IQR_pos. - 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) + (y <= x). -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 Rlt_lpo_floor : forall x : R, - (forall (P : nat -> Prop), (forall n, {P n} + {~P n}) - -> {n | ~P n} + {forall n, P n}) - -> { p : Z & IZR p <= x < IZR p + 1 }. -Proof. - intros x lpo. destruct (Rfloor x) as [n [H H0]]. - destruct (Rlt_lpo_dec x (IZR n + 1) lpo). - - exists n. split. unfold Rle. apply Rlt_asym. exact H. exact r. - - exists (n+1)%Z. split. rewrite plus_IZR. exact r. - rewrite plus_IZR, Rplus_assoc. exact H0. -Qed. - - -(*********) -Lemma Rmult_le_pos : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2. -Proof. - intros x y H H0; rewrite <- (Rmult_0_l x); rewrite <- (Rmult_comm x); - apply (Rmult_le_compat_l x 0 y H H0). -Qed. - -Lemma Rinv_le_contravar : - forall x y (xpos : 0 < x) (ynz : y # 0), - 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. - apply (Rmult_lt_compat_r y) in abs. - rewrite Rmult_assoc in abs. rewrite Rinv_l in abs. - rewrite Rmult_1_r in abs. rewrite Rmult_1_l in abs. contradiction. - exact (Rlt_le_trans _ x _ xpos H). - right. exact xpos. -Qed. - -Lemma Rle_Rinv : forall x y (xpos : 0 < x) (ypos : 0 < y), - x <= y -> (/ y) (inr ypos) <= (/ x) (inr xpos). -Proof. - intros. - apply Rinv_le_contravar with (1 := H). -Qed. - -Lemma Ropp_div : forall x y (ynz : y # 0), - -x * (/y) ynz == - (x * (/ y) ynz). -Proof. - intros; ring. -Qed. - -Lemma double : forall r1, 2 * r1 == r1 + r1. -Proof. - intros. rewrite (Rmult_plus_distr_r 1 1 r1), Rmult_1_l. reflexivity. -Qed. - -Lemma Rlt_0_2 : 0 < 2. -Proof. - apply (Rlt_trans 0 (0+1)). rewrite Rplus_0_l. exact Rlt_0_1. - apply Rplus_lt_le_compat. exact Rlt_0_1. apply Rle_refl. -Qed. - -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. -Qed. - -(* IZR : Z -> R is a ring morphism *) -Lemma R_rm : ring_morph - 0 1 Rplus Rmult Rminus Ropp Req - 0%Z 1%Z Zplus Zmult Zminus Z.opp Zeq_bool IZR. -Proof. -constructor ; try easy. -exact plus_IZR. -exact minus_IZR. -exact mult_IZR. -exact opp_IZR. -intros x y H. -replace y with x. reflexivity. -now apply Zeq_bool_eq. -Qed. - -Lemma Zeq_bool_IZR x y : - IZR x == IZR y -> Zeq_bool x y = true. -Proof. -intros H. -apply Zeq_is_eq_bool. -now apply eq_IZR. -Qed. - - -(*********************************************************) -(** ** Other rules about < and <= *) -(*********************************************************) - -Lemma Rmult_ge_0_gt_0_lt_compat : - forall r1 r2 r3 r4, - 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. unfold Rle. apply Rlt_asym. apply H1. - apply Rmult_lt_compat_l. apply H0. apply H2. -Qed. - -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) (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) (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. - rewrite (Rmult_comm (x-y)), <- Rmult_assoc, Rinv_r, Rmult_1_l, - (Rmult_plus_distr_r 1 1), (Rmult_plus_distr_r 1 1) - in H. - ring_simplify in H; contradiction. - 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) (inr bpos). -Proof. -intros; apply Rmult_lt_0_compat;[|apply Rinv_0_lt_compat]; assumption. -Qed. - -Lemma Rdiv_plus_distr : forall a b c (cnz : c # 0), - (a + b)* (/c) cnz == a* (/c) cnz + b* (/c) cnz. -Proof. - intros. apply Rmult_plus_distr_r. -Qed. - -Lemma Rdiv_minus_distr : forall a b c (cnz : c # 0), - (a - b)* (/c) cnz == a* (/c) cnz - b* (/c) cnz. -Proof. - intros; unfold Rminus,CRminus; rewrite Rmult_plus_distr_r. - apply Rplus_morph. reflexivity. - rewrite Ropp_mult_distr_l. reflexivity. -Qed. - - -(*********************************************************) -(** * Definitions of new types *) -(*********************************************************) - -Record nonnegreal : Type := mknonnegreal - {nonneg :> R; cond_nonneg : 0 <= nonneg}. - -Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}. - -Record nonposreal : Type := mknonposreal - {nonpos :> R; cond_nonpos : nonpos <= 0}. - -Record negreal : Type := mknegreal {neg :> R; cond_neg : neg < 0}. - -Record nonzeroreal : Type := mknonzeroreal - {nonzero :> R; cond_nonzero : nonzero <> 0}. diff --git a/theories/Reals/ConstructiveRcomplete.v b/theories/Reals/ConstructiveRcomplete.v index 0a515672f2..b575c17961 100644 --- a/theories/Reals/ConstructiveRcomplete.v +++ b/theories/Reals/ConstructiveRcomplete.v @@ -11,6 +11,7 @@ Require Import QArith_base. Require Import Qabs. +Require Import ConstructiveReals. Require Import ConstructiveCauchyRealsMult. Require Import Logic.ConstructiveEpsilon. @@ -347,3 +348,35 @@ Proof. apply Qplus_le_r. discriminate. rewrite Qinv_plus_distr. reflexivity. Qed. + +Definition CRealImplem : ConstructiveReals. +Proof. + assert (isLinearOrder CReal CRealLt) as lin. + { repeat split. exact CRealLt_asym. + exact CReal_lt_trans. + intros. destruct (CRealLt_dec x z y H). + left. exact c. right. exact c. } + apply (Build_ConstructiveReals + 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 + 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 + inject_Q inject_Q_plus inject_Q_mult + inject_Q_one inject_Q_lt lt_inject_Q + CRealQ_dense Rup_pos). + - intros. destruct (Rcauchy_complete xn) as [l cv]. + intro n. destruct (H n). exists x. intros. + specialize (a i j H0 H1) as [a b]. split. 2: exact b. + rewrite <- opp_inject_Q. + setoid_replace (-(1#n))%Q with (-1#n)%Q. exact a. reflexivity. + exists l. intros p. destruct (cv p). + exists x. intros. specialize (a i H0). split. 2: apply a. + unfold orderLe. + intro abs. setoid_replace (-1#p)%Q with (-(1#p))%Q in abs. + rewrite opp_inject_Q in abs. destruct a. contradiction. + reflexivity. +Defined. diff --git a/theories/Reals/ConstructiveRealsMorphisms.v b/theories/Reals/ConstructiveRealsMorphisms.v index 0d3027d475..7954e9a96c 100644 --- a/theories/Reals/ConstructiveRealsMorphisms.v +++ b/theories/Reals/ConstructiveRealsMorphisms.v @@ -29,7 +29,7 @@ Require Import QArith. Require Import Qabs. Require Import ConstructiveReals. Require Import ConstructiveCauchyRealsMult. -Require Import ConstructiveRIneq. +Require Import ConstructiveRcomplete. Record ConstructiveRealsMorphism (R1 R2 : ConstructiveReals) : Set := diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 3b108b485a..7813c7b975 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -13,7 +13,8 @@ (** * Basic lemmas for the classical real numbers *) (*********************************************************) -Require Import ConstructiveRIneq. +Require Import ConstructiveCauchyReals. +Require Import ConstructiveCauchyRealsMult. Require Export Raxioms. Require Import Rpow_def. Require Import Zpower. @@ -457,11 +458,13 @@ Qed. Lemma Rplus_eq_0_l : forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0. Proof. - intros. apply Rquot1. rewrite Rrepr_0. - apply (Rplus_eq_0_l (Rrepr r1) (Rrepr r2)). - rewrite Rrepr_le, Rrepr_0 in H. exact H. - rewrite Rrepr_le, Rrepr_0 in H0. exact H0. - rewrite <- Rrepr_plus, H1, Rrepr_0. reflexivity. + intros a b H [H0| H0] H1; auto with real. + absurd (0 < a + b). + rewrite H1; auto with real. + apply Rle_lt_trans with (a + 0). + rewrite Rplus_0_r; assumption. + auto using Rplus_lt_compat_l with real. + rewrite <- H0, Rplus_0_r in H1; assumption. Qed. Lemma Rplus_eq_R0 : @@ -541,9 +544,10 @@ Qed. (**********) 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. + intros. apply Rquot1. apply (CReal_mult_eq_reg_l (Rrepr r)). apply Rrepr_appart in H0. rewrite Rrepr_0 in H0. exact H0. + apply Rrepr_appart in H0. + rewrite <- Rrepr_mult, <- Rrepr_mult, H. reflexivity. Qed. Lemma Rmult_eq_reg_r : forall r r1 r2, r1 * r = r2 * r -> r <> 0 -> r1 = r2. @@ -996,16 +1000,16 @@ Qed. Lemma Rplus_lt_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2. Proof. - intros. rewrite Rlt_def. apply Rlt_forget. apply (Rplus_lt_reg_l (Rrepr r)). + intros. rewrite Rlt_def. apply CRealLtForget. apply (CReal_plus_lt_reg_l (Rrepr r)). rewrite <- Rrepr_plus, <- Rrepr_plus. - rewrite Rlt_def in H. apply Rlt_epsilon. exact H. + rewrite Rlt_def in H. apply CRealLtEpsilon. exact H. Qed. Lemma Rplus_lt_reg_r : forall r r1 r2, r1 + r < r2 + r -> r1 < r2. Proof. - intros. rewrite Rlt_def. apply Rlt_forget. apply (Rplus_lt_reg_r (Rrepr r)). + intros. rewrite Rlt_def. apply CRealLtForget. apply (CReal_plus_lt_reg_r (Rrepr r)). rewrite <- Rrepr_plus, <- Rrepr_plus. rewrite Rlt_def in H. - apply Rlt_epsilon. exact H. + apply CRealLtEpsilon. exact H. Qed. Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2. @@ -1076,18 +1080,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. apply Rlt_epsilon. exact H. + apply CRealLtForget. + apply CReal_opp_gt_lt_contravar. unfold Rgt in H. + rewrite Rlt_def in H. apply CRealLtEpsilon. 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 Rlt_forget. - apply Ropp_lt_gt_contravar. rewrite Rlt_def in H. - apply Rlt_epsilon. exact H. + apply CRealLtForget. + apply CReal_opp_gt_lt_contravar. rewrite Rlt_def in H. + apply CRealLtEpsilon. exact H. Qed. Hint Resolve Ropp_lt_gt_contravar: real. @@ -1239,10 +1243,11 @@ Lemma Rmult_le_compat : forall r1 r2 r3 r4, 0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4. Proof. - intros. rewrite Rrepr_le, Rrepr_mult, Rrepr_mult. - apply Rmult_le_compat. rewrite <- Rrepr_0, <- Rrepr_le. exact H. - rewrite <- Rrepr_0, <- Rrepr_le. exact H0. - rewrite <- Rrepr_le. exact H1. rewrite <- Rrepr_le. exact H2. + intros x y z t H' H'0 H'1 H'2. + apply Rle_trans with (r2 := x * t); auto with real. + repeat rewrite (fun x => Rmult_comm x t). + apply Rmult_le_compat_l; auto. + apply Rle_trans with z; auto. Qed. Hint Resolve Rmult_le_compat: real. @@ -1307,18 +1312,20 @@ 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. apply Rlt_forget. - apply (Rmult_lt_reg_l (Rrepr r)). - rewrite <- Rrepr_0. apply Rlt_epsilon. exact H. - rewrite <- Rrepr_mult, <- Rrepr_mult. apply Rlt_epsilon. exact H0. + intros z x y H H0. + case (Rtotal_order x y); intros Eq0; auto; elim Eq0; clear Eq0; intros Eq0. + rewrite Eq0 in H0; exfalso; apply (Rlt_irrefl (z * y)); auto. + generalize (Rmult_lt_compat_l z y x H Eq0); intro; exfalso; + generalize (Rlt_trans (z * x) (z * y) (z * x) H0 H1); + intro; apply (Rlt_irrefl (z * x)); auto. 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 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. + intros. + apply Rmult_lt_reg_l with r. + exact H. + now rewrite 2!(Rmult_comm r). Qed. Lemma Rmult_gt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2. @@ -1326,10 +1333,14 @@ 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. apply Rlt_epsilon. exact H. - rewrite <- Rrepr_mult, <- Rrepr_mult. - rewrite <- Rrepr_le. exact H0. + intros z x y H H0; case H0; auto with real. + intros H1; apply Rlt_le. + apply Rmult_lt_reg_l with (r := z); auto. + intros H1; replace x with (/ z * (z * x)); auto with real. + replace y with (/ z * (z * y)). + rewrite H1; auto with real. + rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real. + rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real. Qed. Lemma Rmult_le_reg_r : forall r r1 r2, 0 < r -> r1 * r <= r2 * r -> r1 <= r2. @@ -1574,9 +1585,11 @@ Qed. (**********) Lemma plus_INR : forall n m:nat, INR (n + m) = INR n + INR m. Proof. - intros. apply Rquot1. - rewrite Rrepr_INR, Rrepr_plus, plus_INR, - <- Rrepr_INR, <- Rrepr_INR. reflexivity. + intros n m; induction n as [| n Hrecn]. + simpl; auto with real. + replace (S n + m)%nat with (S (n + m)); auto with arith. + repeat rewrite S_INR. + rewrite Hrecn; ring. Qed. Hint Resolve plus_INR: real. @@ -1645,8 +1658,16 @@ 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. apply Rlt_epsilon. exact H. + intros n m. revert n. + induction m ; intros n H. + - elim (Rlt_irrefl 0). + apply Rle_lt_trans with (2 := H). + apply pos_INR. + - destruct n as [|n]. + apply Nat.lt_0_succ. + apply lt_n_S, IHm. + rewrite 2!S_INR in H. + apply Rplus_lt_reg_r with (1 := H). Qed. Hint Resolve INR_lt: real. @@ -1680,8 +1701,11 @@ Hint Resolve not_0_INR: real. Lemma not_INR : forall n m:nat, n <> m -> INR n <> INR m. Proof. - intros. apply Rappart_repr. rewrite Rrepr_INR, Rrepr_INR. - apply not_INR. exact H. + intros n m H; case (le_or_lt n m); intros H1. + case (le_lt_or_eq _ _ H1); intros H2. + apply Rlt_dichotomy_converse; auto with real. + exfalso; auto. + apply not_eq_sym; apply Rlt_dichotomy_converse; auto with real. Qed. Hint Resolve not_INR: real. @@ -1721,8 +1745,17 @@ Qed. Lemma INR_IPR : forall p, INR (Pos.to_nat p) = IPR p. Proof. - intros. apply Rquot1. rewrite Rrepr_INR, Rrepr_IPR. - apply INR_IPR. + assert (H: forall p, 2 * INR (Pos.to_nat p) = IPR_2 p). + induction p as [p|p|] ; simpl IPR_2. + rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- IHp. + now rewrite (Rplus_comm (2 * _)). + now rewrite Pos2Nat.inj_xO, mult_INR, <- IHp. + apply Rmult_1_r. + intros [p|p|] ; unfold IPR. + rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- H. + apply Rplus_comm. + now rewrite Pos2Nat.inj_xO, mult_INR, <- H. + easy. Qed. (**********) @@ -1737,15 +1770,26 @@ Qed. Lemma plus_IZR_NEG_POS : forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q). Proof. - intros. apply Rquot1. rewrite Rrepr_plus. - do 3 rewrite Rrepr_IZR. apply plus_IZR_NEG_POS. + intros p q; simpl. rewrite Z.pos_sub_spec. + case Pos.compare_spec; intros H; unfold IZR. + subst. ring. + rewrite <- 3!INR_IPR, Pos2Nat.inj_sub by trivial. + rewrite minus_INR by (now apply lt_le_weak, Pos2Nat.inj_lt). + ring. + rewrite <- 3!INR_IPR, Pos2Nat.inj_sub by trivial. + rewrite minus_INR by (now apply lt_le_weak, Pos2Nat.inj_lt). + ring. Qed. (**********) Lemma plus_IZR : forall n m:Z, IZR (n + m) = IZR n + IZR m. Proof. - intros. apply Rquot1. - rewrite Rrepr_plus. do 3 rewrite Rrepr_IZR. apply plus_IZR. + intro z; destruct z; intro t; destruct t; intros; auto with real. + simpl. unfold IZR. rewrite <- 3!INR_IPR, Pos2Nat.inj_add. apply plus_INR. + apply plus_IZR_NEG_POS. + rewrite Z.add_comm; rewrite Rplus_comm; apply plus_IZR_NEG_POS. + simpl. unfold IZR. rewrite <- 3!INR_IPR, Pos2Nat.inj_add, plus_INR. + apply Ropp_plus_distr. Qed. (**********) @@ -1755,21 +1799,14 @@ Proof. unfold IZR; intros m n; rewrite <- 3!INR_IPR, Pos2Nat.inj_mul, mult_INR; ring. Qed. -Lemma Rrepr_pow : forall (x : R) (n : nat), - (ConstructiveRIneq.Req (Rrepr (pow x n)) - (ConstructiveRIneq.pow (Rrepr x) n)). -Proof. - intro x. induction n. - - apply Rrepr_1. - - simpl. rewrite Rrepr_mult, <- IHn. reflexivity. -Qed. - Lemma pow_IZR : forall z n, pow (IZR z) n = IZR (Z.pow z (Z.of_nat n)). Proof. - intros. apply Rquot1. - rewrite Rrepr_IZR, Rrepr_pow. - rewrite (Rpow_eq_compat _ _ n (Rrepr_IZR z)). - apply pow_IZR. + intros z [|n];simpl;trivial. + rewrite Zpower_pos_nat. + rewrite SuccNat2Pos.id_succ. unfold Zpower_nat;simpl. + rewrite mult_IZR. + induction n;simpl;trivial. + rewrite mult_IZR;ring[IHn]. Qed. (**********) @@ -1803,23 +1840,34 @@ 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. apply Rlt_epsilon. exact H. + intro z; case z; simpl; intros. + elim (Rlt_irrefl _ H). + easy. + elim (Rlt_not_le _ _ H). + unfold IZR. + rewrite <- INR_IPR. + auto with real. 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. - apply Rlt_epsilon. exact H. + intros z1 z2 H; apply Z.lt_0_sub. + apply lt_0_IZR. + rewrite <- Z_R_minus. + exact (Rgt_minus (IZR z2) (IZR z1) H). Qed. (**********) Lemma eq_IZR_R0 : forall n:Z, IZR n = 0 -> n = 0%Z. Proof. - intros. apply eq_IZR_R0. - rewrite <- Rrepr_0, <- Rrepr_IZR, H. reflexivity. + intro z; destruct z; simpl; intros; auto with zarith. + elim Rgt_not_eq with (2 := H). + unfold IZR. rewrite <- INR_IPR. + apply lt_0_INR, Pos2Nat.is_pos. + elim Rlt_not_eq with (2 := H). + unfold IZR. rewrite <- INR_IPR. + apply Ropp_lt_gt_0_contravar, lt_0_INR, Pos2Nat.is_pos. Qed. (**********) @@ -1895,21 +1943,26 @@ 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 Rlt_epsilon. apply H. - rewrite <- Rrepr_IZR, <- Rrepr_1. apply Rlt_epsilon. apply H. + intros z [H1 H2]. + apply Z.le_antisymm. + apply Z.lt_succ_r; apply lt_IZR; trivial. + change 0%Z with (Z.succ (-1)). + apply Z.le_succ_l; apply lt_IZR; trivial. 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 Rlt_epsilon. apply H. - rewrite <- Rrepr_IZR, <- Rrepr_1, <- Rrepr_plus, <- Rrepr_le. - apply H. rewrite <- Rrepr_IZR. apply Rlt_epsilon. apply H0. - rewrite <- Rrepr_IZR, <- Rrepr_1, <- Rrepr_plus, <- Rrepr_le. - apply H0. + 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. + replace (-1) with (r - (r + 1)). + unfold Rminus; apply Rplus_lt_le_compat; auto with real. + ring. + replace 1 with (r + 1 - r). + unfold Rminus; apply Rplus_le_lt_compat; auto with real. + ring. Qed. @@ -1942,13 +1995,13 @@ Qed. Lemma Rinv_le_contravar : forall x y, 0 < x -> x <= y -> / y <= / x. 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). - 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. + intros x y H1 [H2|H2]. + apply Rlt_le. + apply Rinv_lt_contravar with (2 := H2). + apply Rmult_lt_0_compat with (1 := H1). + now apply Rlt_trans with x. + rewrite H2. + apply Rle_refl. Qed. Lemma Rle_Rinv : forall x y:R, 0 < x -> 0 < y -> x <= y -> / y <= / x. @@ -2012,10 +2065,18 @@ Qed. Lemma le_epsilon : forall r1 r2, (forall eps:R, 0 < eps -> r1 <= r2 + eps) -> r1 <= r2. 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. apply Rlt_forget. exact H0. + intros x y H. + destruct (Rle_or_lt x y) as [H1|H1]. + exact H1. + apply Rplus_le_reg_r with x. + replace (y + x) with (2 * (y + (x - y) * / 2)) by field. + replace (x + x) with (2 * x) by ring. + apply Rmult_le_compat_l. + now apply (IZR_le 0 2). + apply H. + apply Rmult_lt_0_compat. + now apply Rgt_minus. + apply Rinv_0_lt_compat, Rlt_0_2. Qed. (**********) diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index d856d1c7fe..be283fb7cf 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -20,10 +20,12 @@ (*********************************************************) Require Export ZArith_base. -Require Import ConstructiveRIneq. +Require Import ClassicalDedekindReals. +Require Import ConstructiveCauchyReals. +Require Import ConstructiveCauchyRealsMult. +Require Import ConstructiveRcomplete. Require Import ConstructiveRealsLUB. Require Export Rdefinitions. -Declare Scope R_scope. Local Open Scope R_scope. (*********************************************************) @@ -34,7 +36,7 @@ Local Open Scope R_scope. (** ** Addition *) (*********************************************************) -Open Scope R_scope_constr. +Open Scope CReal_scope. Lemma Rrepr_0 : Rrepr 0 == 0. Proof. @@ -58,7 +60,7 @@ Qed. Lemma Rrepr_minus : forall x y:R, Rrepr (x - y) == Rrepr x - Rrepr y. Proof. - intros. unfold Rminus, CRminus. + intros. unfold Rminus, CReal_minus. rewrite Rrepr_plus, Rrepr_opp. reflexivity. Qed. @@ -72,10 +74,10 @@ 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 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. + rewrite Rrepr_0 in c. exact (CRealLt_irrefl 0 c). + rewrite Rrepr_0 in c. exact (CRealLt_irrefl 0 c). + - rewrite Rquot2. apply (CReal_mult_eq_reg_l (Rrepr x)). exact xnz. + rewrite CReal_mult_comm, (CReal_mult_comm (Rrepr x)), CReal_inv_l, CReal_inv_l. reflexivity. Qed. @@ -83,12 +85,12 @@ 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). + apply CRealLtEpsilon in H. + exact (CRealLt_asym (Rrepr x) (Rrepr y) H abs). + destruct H. exact (CRealLt_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. apply Rlt_epsilon in r. contradiction. + rewrite RbaseSymbolsImpl.Rlt_def in r. apply CRealLtEpsilon in r. contradiction. Qed. Lemma Rrepr_appart : forall x y:R, @@ -96,26 +98,26 @@ Lemma Rrepr_appart : forall x y:R, Proof. intros. destruct (total_order_T x y). destruct s. left. rewrite RbaseSymbolsImpl.Rlt_def in r. - apply Rlt_epsilon. exact r. contradiction. + apply CRealLtEpsilon. exact r. contradiction. right. rewrite RbaseSymbolsImpl.Rlt_def in r. - apply Rlt_epsilon. exact r. + apply CRealLtEpsilon. 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). + destruct abs. exact (CRealLt_asym (Rrepr x) (Rrepr x) H H). + destruct abs. exact (CRealLt_asym (Rrepr x) (Rrepr x) H H). Qed. -Close Scope R_scope_constr. +Close Scope CReal_scope. (**********) Lemma Rplus_comm : forall r1 r2:R, r1 + r2 = r2 + r1. Proof. - intros. apply Rquot1. do 2 rewrite Rrepr_plus. apply Rplus_comm. + intros. apply Rquot1. do 2 rewrite Rrepr_plus. apply CReal_plus_comm. Qed. Hint Resolve Rplus_comm: real. @@ -123,7 +125,7 @@ Hint Resolve Rplus_comm: real. Lemma Rplus_assoc : forall r1 r2 r3:R, r1 + r2 + r3 = r1 + (r2 + r3). Proof. intros. apply Rquot1. repeat rewrite Rrepr_plus. - apply Rplus_assoc. + apply CReal_plus_assoc. Qed. Hint Resolve Rplus_assoc: real. @@ -131,7 +133,7 @@ Hint Resolve Rplus_assoc: real. Lemma Rplus_opp_r : forall r:R, r + - r = 0. Proof. intros. apply Rquot1. rewrite Rrepr_plus, Rrepr_opp, Rrepr_0. - apply Rplus_opp_r. + apply CReal_plus_opp_r. Qed. Hint Resolve Rplus_opp_r: real. @@ -139,7 +141,7 @@ Hint Resolve Rplus_opp_r: real. Lemma Rplus_0_l : forall r:R, 0 + r = r. Proof. intros. apply Rquot1. rewrite Rrepr_plus, Rrepr_0. - apply Rplus_0_l. + apply CReal_plus_0_l. Qed. Hint Resolve Rplus_0_l: real. @@ -150,7 +152,7 @@ Hint Resolve Rplus_0_l: real. (**********) Lemma Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1. Proof. - intros. apply Rquot1. do 2 rewrite Rrepr_mult. apply Rmult_comm. + intros. apply Rquot1. do 2 rewrite Rrepr_mult. apply CReal_mult_comm. Qed. Hint Resolve Rmult_comm: real. @@ -158,7 +160,7 @@ Hint Resolve Rmult_comm: real. Lemma Rmult_assoc : forall r1 r2 r3:R, r1 * r2 * r3 = r1 * (r2 * r3). Proof. intros. apply Rquot1. repeat rewrite Rrepr_mult. - apply Rmult_assoc. + apply CReal_mult_assoc. Qed. Hint Resolve Rmult_assoc: real. @@ -167,7 +169,7 @@ Lemma Rinv_l : forall r:R, r <> 0 -> / r * r = 1. Proof. intros. rewrite RinvImpl.Rinv_def; destruct (Req_appart_dec r R0). - contradiction. - - apply Rquot1. rewrite Rrepr_mult, Rquot2, Rrepr_1. apply Rinv_l. + - apply Rquot1. rewrite Rrepr_mult, Rquot2, Rrepr_1. apply CReal_inv_l. Qed. Hint Resolve Rinv_l: real. @@ -175,7 +177,7 @@ Hint Resolve Rinv_l: real. Lemma Rmult_1_l : forall r:R, 1 * r = r. Proof. intros. apply Rquot1. rewrite Rrepr_mult, Rrepr_1. - apply Rmult_1_l. + apply CReal_mult_1_l. Qed. Hint Resolve Rmult_1_l: real. @@ -183,17 +185,17 @@ Hint Resolve Rmult_1_l: real. Lemma R1_neq_R0 : 1 <> 0. Proof. intro abs. - assert (Req (CRone CR) (CRzero CR)). + assert (CRealEq 1%CReal 0%CReal). { transitivity (Rrepr 1). symmetry. - replace 1%R with (Rabst (CRone CR)). + replace 1%R with (Rabst 1%CReal). 2: unfold IZR,IPR; rewrite RbaseSymbolsImpl.R1_def; reflexivity. rewrite Rquot2. reflexivity. transitivity (Rrepr 0). rewrite abs. reflexivity. - replace 0%R with (Rabst (CRzero CR)). + replace 0%R with (Rabst 0%CReal). 2: unfold IZR; rewrite RbaseSymbolsImpl.R0_def; reflexivity. rewrite Rquot2. reflexivity. } - pose proof (Rlt_morph (CRzero CR) (CRzero CR) (Req_refl _) (CRone CR) (CRzero CR) H). - apply (Rlt_irrefl (CRzero CR)). apply H0. apply Rlt_0_1. + pose proof (CRealLt_morph 0%CReal 0%CReal (CRealEq_refl _) 1%CReal 0%CReal H). + apply (CRealLt_irrefl 0%CReal). apply H0. apply CRealLt_0_1. Qed. Hint Resolve R1_neq_R0: real. @@ -207,7 +209,7 @@ Lemma Proof. intros. apply Rquot1. rewrite Rrepr_mult, Rrepr_plus, Rrepr_plus, Rrepr_mult, Rrepr_mult. - apply Rmult_plus_distr_l. + apply CReal_mult_plus_distr_l. Qed. Hint Resolve Rmult_plus_distr_l: real. @@ -223,35 +225,35 @@ 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. + apply CRealLtEpsilon in H. apply CRealLtEpsilon in abs. + apply (CRealLt_asym (Rrepr r1) (Rrepr r2)); assumption. 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. + apply CRealLtEpsilon in H. apply CRealLtEpsilon in H0. + apply CRealLtForget. + apply (CReal_lt_trans (Rrepr r1) (Rrepr r2) (Rrepr r3)); assumption. 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 Rlt_forget. - apply Rplus_lt_compat_l. apply Rlt_epsilon. exact H. + do 2 rewrite Rrepr_plus. apply CRealLtForget. + apply CReal_plus_lt_compat_l. apply CRealLtEpsilon. 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 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. + do 2 rewrite Rrepr_mult. apply CRealLtForget. apply CReal_mult_lt_compat_l. + rewrite <- (Rquot2 0%CReal). unfold IZR in H. + rewrite RbaseSymbolsImpl.R0_def in H. apply CRealLtEpsilon. exact H. + rewrite RbaseSymbolsImpl.Rlt_def in H0. apply CRealLtEpsilon. exact H0. Qed. Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real. @@ -274,119 +276,133 @@ Arguments INR n%nat. (**********************************************************) Lemma Rrepr_INR : forall n : nat, - Req (Rrepr (INR n)) (ConstructiveRIneq.INR n). + CRealEq (Rrepr (INR n)) (inject_Z (Z.of_nat n)). Proof. induction n. - apply Rrepr_0. - - simpl. destruct n. apply Rrepr_1. - rewrite Rrepr_plus, <- IHn, Rrepr_1. reflexivity. + - replace (Z.of_nat (S n)) with (Z.of_nat n + 1)%Z. + simpl. destruct n. apply Rrepr_1. + rewrite Rrepr_plus,inject_Z_plus, <- IHn, Rrepr_1. reflexivity. + replace 1%Z with (Z.of_nat 1). rewrite <- (Nat2Z.inj_add n 1). + apply f_equal. rewrite Nat.add_comm. reflexivity. reflexivity. Qed. Lemma Rrepr_IPR2 : forall n : positive, - Req (Rrepr (IPR_2 n)) (ConstructiveRIneq.IPR_2 n). + CRealEq (Rrepr (IPR_2 n)) (inject_Z (Z.pos (n~0))). Proof. induction n. - - unfold IPR_2, ConstructiveRIneq.IPR_2. - rewrite RbaseSymbolsImpl.R1_def, Rrepr_mult, Rrepr_plus, Rrepr_plus, <- IHn. - unfold IPR_2. - rewrite Rquot2. rewrite RbaseSymbolsImpl.R1_def. reflexivity. - - unfold IPR_2, ConstructiveRIneq.IPR_2. - rewrite Rrepr_mult, Rrepr_plus, <- IHn. - rewrite RbaseSymbolsImpl.R1_def. rewrite Rquot2. - unfold IPR_2. rewrite RbaseSymbolsImpl.R1_def. reflexivity. - - unfold IPR_2, ConstructiveRIneq.IPR_2. - rewrite RbaseSymbolsImpl.R1_def. - rewrite Rrepr_plus, Rquot2. reflexivity. + - simpl. replace (Z.pos n~1~0) with ((Z.pos n~0 + 1) + (Z.pos n~0 + 1))%Z. + rewrite RbaseSymbolsImpl.R1_def, Rrepr_mult, inject_Z_plus, inject_Z_plus. + rewrite Rrepr_plus, Rrepr_plus, <- IHn. + rewrite Rquot2, CReal_mult_plus_distr_r, CReal_mult_1_l. + rewrite (CReal_plus_comm 1%CReal). repeat rewrite CReal_plus_assoc. + apply CReal_plus_morph. reflexivity. + reflexivity. + repeat rewrite <- Pos2Z.inj_add. apply f_equal. + rewrite Pos.add_diag. apply f_equal. + rewrite Pos.add_1_r. reflexivity. + - simpl. replace (Z.pos n~0~0) with ((Z.pos n~0) + (Z.pos n~0))%Z. + rewrite RbaseSymbolsImpl.R1_def, Rrepr_mult, inject_Z_plus. + rewrite Rrepr_plus, <- IHn. + rewrite Rquot2, CReal_mult_plus_distr_r, CReal_mult_1_l. reflexivity. + rewrite <- Pos2Z.inj_add. apply f_equal. + rewrite Pos.add_diag. reflexivity. + - simpl. rewrite Rrepr_plus, RbaseSymbolsImpl.R1_def, Rquot2. + replace 2%Z with (1 + 1)%Z. rewrite inject_Z_plus. reflexivity. + reflexivity. Qed. Lemma Rrepr_IPR : forall n : positive, - Req (Rrepr (IPR n)) (ConstructiveRIneq.IPR n). + CRealEq (Rrepr (IPR n)) (inject_Z (Z.pos n)). Proof. intro n. destruct n. - - unfold IPR, ConstructiveRIneq.IPR. - rewrite Rrepr_plus, <- Rrepr_IPR2. - rewrite RbaseSymbolsImpl.R1_def. rewrite Rquot2. reflexivity. - - unfold IPR, ConstructiveRIneq.IPR. - apply Rrepr_IPR2. + - unfold IPR. rewrite Rrepr_plus. + replace (n~1)%positive with (n~0 + 1)%positive. + rewrite Pos2Z.inj_add, inject_Z_plus, <- Rrepr_IPR2, CReal_plus_comm. + rewrite RbaseSymbolsImpl.R1_def, Rquot2. reflexivity. + rewrite Pos.add_1_r. reflexivity. + - apply Rrepr_IPR2. - unfold IPR. rewrite RbaseSymbolsImpl.R1_def. apply Rquot2. Qed. Lemma Rrepr_IZR : forall n : Z, - Req (Rrepr (IZR n)) (ConstructiveRIneq.IZR n). + CRealEq (Rrepr (IZR n)) (inject_Z n). Proof. intros [|p|n]. - unfold IZR. rewrite RbaseSymbolsImpl.R0_def. apply Rquot2. - apply Rrepr_IPR. - - unfold IZR, ConstructiveRIneq.IZR. - rewrite <- Rrepr_IPR, Rrepr_opp. reflexivity. + - unfold IZR. rewrite Rrepr_opp, Rrepr_IPR. rewrite <- opp_inject_Z. + replace (- Z.pos n)%Z with (Z.neg n). reflexivity. reflexivity. Qed. (**********) Lemma archimed : forall r:R, IZR (up r) > r /\ IZR (up r) - r <= 1. Proof. intro r. unfold up. - destruct (Rarchimedean (Rrepr r)) as [n nmaj], (total_order_T (IZR n - r) R1). + destruct (CRealArchimedean (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 Rlt_forget. apply nmaj. + apply CRealLtForget. apply nmaj. unfold Rle. left. exact r0. - split. unfold Rgt. rewrite RbaseSymbolsImpl.Rlt_def. - rewrite Rrepr_IZR. apply Rlt_forget. apply nmaj. right. exact e. + rewrite Rrepr_IZR. apply CRealLtForget. apply nmaj. right. exact e. - split. + unfold Rgt, Z.pred. rewrite RbaseSymbolsImpl.Rlt_def. - rewrite Rrepr_IZR, plus_IZR. + rewrite Rrepr_IZR, inject_Z_plus. rewrite RbaseSymbolsImpl.Rlt_def in r0. rewrite Rrepr_minus in r0. rewrite <- (Rrepr_IZR n). - unfold ConstructiveRIneq.IZR, ConstructiveRIneq.IPR. - 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)))) + apply CRealLtForget. apply CRealLtEpsilon in r0. + unfold CReal_minus in r0. + apply (CReal_plus_lt_compat_l + (CReal_plus (Rrepr r) (CReal_opp (Rrepr R1)))) in r0. - rewrite ConstructiveRIneq.Rplus_assoc, - ConstructiveRIneq.Rplus_opp_l, - ConstructiveRIneq.Rplus_0_r, + rewrite CReal_plus_assoc, + CReal_plus_opp_l, + CReal_plus_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 + CReal_plus_comm, + CReal_plus_assoc, + <- (CReal_plus_assoc (CReal_opp (Rrepr r))), + CReal_plus_opp_l, + CReal_plus_0_l in r0. - exact r0. + rewrite (opp_inject_Z 1). exact r0. + destruct (total_order_T (IZR (Z.pred n) - r) 1). destruct s. left. exact r1. right. exact e. - exfalso. destruct nmaj as [_ nmaj]. rewrite <- Rrepr_IZR in nmaj. + exfalso. destruct nmaj as [_ nmaj]. + pose proof Rrepr_IZR as iz. unfold inject_Z in iz. + rewrite <- iz 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. - unfold IZR, IPR. rewrite RbaseSymbolsImpl.R1_def, Rquot2. apply Rle_refl. + apply CRealLtForget. + apply (CReal_lt_le_trans _ _ _ nmaj). + unfold IZR, IPR. rewrite RbaseSymbolsImpl.R1_def, Rquot2. + rewrite <- (inject_Z_plus 1 1). apply CRealLe_refl. clear nmaj. unfold Z.pred in r1. rewrite RbaseSymbolsImpl.Rlt_def in r1. - rewrite Rrepr_minus, (Rrepr_IZR (n + -1)), plus_IZR, - <- (Rrepr_IZR n) - in r1. - unfold ConstructiveRIneq.IZR, ConstructiveRIneq.IPR in r1. + rewrite Rrepr_minus, (Rrepr_IZR (n + -1)) in r1. + rewrite inject_Z_plus, <- (Rrepr_IZR n) 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. - apply Rlt_forget. - apply (ConstructiveRIneq.Rle_lt_trans - _ (ConstructiveRIneq.Rplus (ConstructiveRIneq.Rplus (Rrepr r) (Rrepr 1)) (CRone CR))). + apply CRealLtEpsilon in r1. + apply (CReal_plus_lt_compat_l + (CReal_plus (Rrepr r) 1%CReal)) in r1. + apply CRealLtForget. + apply (CReal_le_lt_trans + _ (CReal_plus (CReal_plus (Rrepr r) (Rrepr 1)) 1%CReal)). 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)) + rewrite RbaseSymbolsImpl.R1_def, (Rquot2 1%CReal), <- CReal_plus_assoc. + apply CRealLe_refl. + rewrite <- (CReal_plus_comm (Rrepr 1)), + <- CReal_plus_assoc, + (CReal_plus_comm (Rrepr 1)) in r1. - apply (ConstructiveRIneq.Rlt_le_trans _ _ _ r1). - unfold ConstructiveRIneq.Rminus. - ring_simplify. apply ConstructiveRIneq.Rle_refl. + apply (CReal_lt_le_trans _ _ _ r1). + unfold CReal_minus. rewrite (opp_inject_Z 1). + rewrite (CReal_plus_comm (Rrepr (IZR n))), CReal_plus_assoc, + <- (CReal_plus_assoc 1), <- (CReal_plus_assoc 1), CReal_plus_opp_r. + rewrite CReal_plus_0_l, CReal_plus_comm, CReal_plus_assoc, + CReal_plus_opp_l, CReal_plus_0_r. + apply CRealLe_refl. Qed. (**********************************************************) @@ -408,29 +424,29 @@ Lemma completeness : forall E:R -> Prop, bound E -> (exists x : R, E x) -> { m:R | is_lub E m }. Proof. - intros. pose (fun x:ConstructiveRIneq.R => E (Rabst x)) as Er. - assert (forall x y : CRcarrier CR, orderEq (CRcarrier CR) (CRlt CR) x y -> Er x <-> Er y) + intros. pose (fun x:CReal => E (Rabst x)) as Er. + assert (forall x y : CReal, CRealEq x y -> Er x <-> Er y) as Erproper. { intros. unfold Er. replace (Rabst x) with (Rabst y). reflexivity. apply Rquot1. do 2 rewrite Rquot2. split; apply H1. } - assert (exists x : ConstructiveRIneq.R, Er x) as Einhab. + assert (exists x : CReal, Er x) as Einhab. { destruct H0. exists (Rrepr x). unfold Er. replace (Rabst (Rrepr x)) with x. exact H0. apply Rquot1. rewrite Rquot2. reflexivity. } - assert (exists x : ConstructiveRIneq.R, - (forall y:ConstructiveRIneq.R, Er y -> ConstructiveRIneq.Rle y x)) + assert (exists x : CReal, + (forall y:CReal, Er y -> CRealLe y x)) as Ebound. { destruct H. exists (Rrepr x). intros y Ey. rewrite <- (Rquot2 y). apply Rrepr_le. apply H. exact Ey. } - destruct (CR_sig_lub CR + destruct (CR_sig_lub CRealImplem Er Erproper sig_forall_dec sig_not_dec Einhab Ebound). exists (Rabst x). split. intros y Ey. apply Rrepr_le. rewrite Rquot2. - unfold ConstructiveRIneq.Rle. apply a. + unfold CRealLe. 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. - unfold ConstructiveRIneq.Rle. apply H3. intros y Ey. + unfold CRealLe. apply H3. intros y Ey. intros. rewrite <- (Rquot2 y) in H4. apply Rrepr_le in H4. exact H4. apply H1, Ey. diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index b1ce8109ca..35025ba9bc 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -8,17 +8,18 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(* Classical quotient of the constructive Cauchy real numbers. - This file contains the definition of the classical real numbers - type R, its algebraic operations, its order and the proof that - it is total, and the proof that R is archimedean (up). - It also defines IZR, the ring morphism from Z to R. *) +(* Abstraction of classical Dedekind reals behind an opaque module, + for backward compatibility. + + This file also contains the proof that classical reals are a + quotient of constructive Cauchy reals. *) Require Export ZArith_base. Require Import QArith_base. -Require Import ConstructiveRIneq. +Require Import ConstructiveCauchyReals. +Require Import ConstructiveCauchyRealsMult. +Require Import ClassicalDedekindReals. -Parameter R : Set. (* Declare primitive numeral notations for Scope R_scope *) Declare Scope R_scope. @@ -27,26 +28,18 @@ Declare ML Module "r_syntax_plugin". (* Declare Scope R_scope with Key R *) Delimit Scope R_scope with R. -(* Automatically open scope R_scope for arguments of type R *) -Bind Scope R_scope with R. - Local Open Scope R_scope. -(* The limited principle of omniscience *) -Axiom sig_forall_dec - : forall (P : nat -> Prop), - (forall n, {P n} + {~P n}) - -> {n | ~P n} + {forall n, P n}. - -Axiom sig_not_dec : forall P : Prop, { ~~P } + { ~P }. - -Axiom Rabst : ConstructiveRIneq.R -> R. -Axiom Rrepr : R -> ConstructiveRIneq.R. -Axiom Rquot1 : forall x y:R, Req (Rrepr x) (Rrepr y) -> x = y. -Axiom Rquot2 : forall x:ConstructiveRIneq.R, Req (Rrepr (Rabst x)) x. (* Those symbols must be kept opaque, for backward compatibility. *) Module Type RbaseSymbolsSig. + Parameter R : Set. + Bind Scope R_scope with R. + Axiom Rabst : CReal -> R. + Axiom Rrepr : R -> CReal. + Axiom Rquot1 : forall x y:R, CRealEq (Rrepr x) (Rrepr y) -> x = y. + Axiom Rquot2 : forall x:CReal, CRealEq (Rrepr (Rabst x)) x. + Parameter R0 : R. Parameter R1 : R. Parameter Rplus : R -> R -> R. @@ -54,29 +47,34 @@ Module Type RbaseSymbolsSig. Parameter Ropp : R -> R. Parameter Rlt : R -> R -> Prop. - Parameter R0_def : R0 = Rabst (CRzero CR). - Parameter R1_def : R1 = Rabst (CRone CR). + Parameter R0_def : R0 = Rabst (inject_Q 0). + Parameter R1_def : R1 = Rabst (inject_Q 1). Parameter Rplus_def : forall x y : R, - Rplus x y = Rabst (ConstructiveRIneq.Rplus (Rrepr x) (Rrepr y)). + Rplus x y = Rabst (CReal_plus (Rrepr x) (Rrepr y)). Parameter Rmult_def : forall x y : R, - Rmult x y = Rabst (ConstructiveRIneq.Rmult (Rrepr x) (Rrepr y)). + Rmult x y = Rabst (CReal_mult (Rrepr x) (Rrepr y)). Parameter Ropp_def : forall x : R, - Ropp x = Rabst (ConstructiveRIneq.Ropp (Rrepr x)). + Ropp x = Rabst (CReal_opp (Rrepr x)). Parameter Rlt_def : forall x y : R, - Rlt x y = ConstructiveRIneq.RltProp (Rrepr x) (Rrepr y). + Rlt x y = CRealLtProp (Rrepr x) (Rrepr y). End RbaseSymbolsSig. Module RbaseSymbolsImpl : RbaseSymbolsSig. - Definition R0 : R := Rabst (CRzero CR). - Definition R1 : R := Rabst (CRone CR). + Definition R := DReal. + Definition Rabst := DRealAbstr. + Definition Rrepr := DRealRepr. + Definition Rquot1 := DRealQuot1. + Definition Rquot2 := DRealQuot2. + Definition R0 : R := Rabst (inject_Q 0). + Definition R1 : R := Rabst (inject_Q 1). Definition Rplus : R -> R -> R - := fun x y : R => Rabst (ConstructiveRIneq.Rplus (Rrepr x) (Rrepr y)). + := fun x y : R => Rabst (CReal_plus (Rrepr x) (Rrepr y)). Definition Rmult : R -> R -> R - := fun x y : R => Rabst (ConstructiveRIneq.Rmult (Rrepr x) (Rrepr y)). + := fun x y : R => Rabst (CReal_mult (Rrepr x) (Rrepr y)). Definition Ropp : R -> R - := fun x : R => Rabst (ConstructiveRIneq.Ropp (Rrepr x)). + := fun x : R => Rabst (CReal_opp (Rrepr x)). Definition Rlt : R -> R -> Prop - := fun x y : R => ConstructiveRIneq.RltProp (Rrepr x) (Rrepr y). + := fun x y : R => CRealLtProp (Rrepr x) (Rrepr y). Definition R0_def := eq_refl R0. Definition R1_def := eq_refl R1. @@ -88,6 +86,7 @@ End RbaseSymbolsImpl. Export RbaseSymbolsImpl. (* Keep the same names as before *) +Notation R := RbaseSymbolsImpl.R (only parsing). Notation R0 := RbaseSymbolsImpl.R0 (only parsing). Notation R1 := RbaseSymbolsImpl.R1 (only parsing). Notation Rplus := RbaseSymbolsImpl.Rplus (only parsing). @@ -95,6 +94,9 @@ Notation Rmult := RbaseSymbolsImpl.Rmult (only parsing). Notation Ropp := RbaseSymbolsImpl.Ropp (only parsing). Notation Rlt := RbaseSymbolsImpl.Rlt (only parsing). +(* Automatically open scope R_scope for arguments of type R *) +Bind Scope R_scope with R. + Infix "+" := Rplus : R_scope. Infix "*" := Rmult : R_scope. Notation "- x" := (Ropp x) : R_scope. @@ -160,11 +162,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 (Rlt_lpo_dec (Rrepr r1) (Rrepr r2) sig_forall_dec). + intros. destruct (CRealLt_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 r0. + apply CRealLtForget. exact c. + - destruct (CRealLt_lpo_dec (Rrepr r2) (Rrepr r1) sig_forall_dec). + + right. rewrite RbaseSymbolsImpl.Rlt_def. apply CRealLtForget. exact c. + left. right. apply Rquot1. split; assumption. Qed. @@ -178,9 +180,9 @@ Proof. Qed. Lemma Rrepr_appart_0 : forall x:R, - (x < R0 \/ R0 < x) -> Rappart (Rrepr x) (CRzero CR). + (x < R0 \/ R0 < x) -> CReal_appart (Rrepr x) (inject_Q 0). Proof. - intros. apply CRltDisjunctEpsilon. destruct H. + intros. apply CRealLtDisjunctEpsilon. 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. @@ -192,7 +194,7 @@ Module Type RinvSig. Parameter Rinv_def : forall x : R, Rinv x = match Req_appart_dec x R0 with | left _ => R0 (* / 0 is undefined, we take 0 arbitrarily *) - | right r => Rabst ((ConstructiveRIneq.Rinv (Rrepr x) (Rrepr_appart_0 x r))) + | right r => Rabst ((CReal_inv (Rrepr x) (Rrepr_appart_0 x r))) end. End RinvSig. @@ -200,7 +202,7 @@ Module RinvImpl : RinvSig. Definition Rinv : R -> R := fun x => match Req_appart_dec x R0 with | left _ => R0 (* / 0 is undefined, we take 0 arbitrarily *) - | right r => Rabst ((ConstructiveRIneq.Rinv (Rrepr x) (Rrepr_appart_0 x r))) + | right r => Rabst ((CReal_inv (Rrepr x) (Rrepr_appart_0 x r))) end. Definition Rinv_def := fun x => eq_refl (Rinv x). End RinvImpl. @@ -215,7 +217,7 @@ Infix "/" := Rdiv : R_scope. (* First integer strictly above x *) Definition up (x : R) : Z. Proof. - destruct (Rarchimedean (Rrepr x)) as [n nmaj], (total_order_T (IZR n - x) R1). + destruct (CRealArchimedean (Rrepr x)) as [n nmaj], (total_order_T (IZR n - x) R1). destruct s. - exact n. - (* x = n-1 *) exact n. -- cgit v1.2.3