diff options
Diffstat (limited to 'theories')
25 files changed, 1420 insertions, 3313 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 7c69350db4..ea4062d9fe 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -1363,7 +1363,8 @@ Lemma elements_aux_cardinal : Proof. simple induction m; simpl; intuition. rewrite <- H; simpl. - rewrite <- H0; omega. + rewrite <- H0, Nat.add_succ_r, (Nat.add_comm (cardinal t)), Nat.add_assoc. + reflexivity. Qed. Lemma elements_cardinal : forall (m:t elt), cardinal m = length (elements m). diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 0ef356b582..fa553d9fce 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -68,7 +68,7 @@ Hint Constructors avl : core. Lemma height_non_negative : forall (s : t elt), avl s -> height s >= 0. Proof. - induction s; simpl; intros; auto with zarith. + induction s; simpl; intros. now apply Z.le_ge. inv avl; intuition; omega_max. Qed. diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index e5133f66b2..342a51b39b 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -476,8 +476,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. unfold elements. intros m; set (p:=1); clearbody p; revert m p. induction m; simpl; auto; intros. - rewrite (IHm1 (append p 2)), (IHm2 (append p 3)); auto. - destruct o; rewrite app_length; simpl; omega. + rewrite (IHm1 (append p 2)), (IHm2 (append p 3)). + destruct o; rewrite app_length; simpl; auto. Qed. End CompcertSpec. diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index da504259f5..1983c6caa1 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -17,7 +17,7 @@ [mem x s=true] instead of [In x s], [equal s s'=true] instead of [Equal s s'], etc. *) -Require Import FSetProperties Zerob Sumbool Omega DecidableTypeEx. +Require Import FSetProperties Zerob Sumbool DecidableTypeEx. Module WEqProperties_fun (Import E:DecidableType)(M:WSfun E). Module Import MP := WProperties_fun E M. @@ -847,11 +847,16 @@ Proof. unfold sum. intros f g Hf Hg. assert (fc : compat_opL (fun x:elt =>plus (f x))). red; auto with fset. -assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros; omega. +assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros x y z. + rewrite !PeanoNat.Nat.add_assoc, (PeanoNat.Nat.add_comm (f x) (f y)); reflexivity. assert (gc : compat_opL (fun x:elt => plus (g x))). red; auto with fset. -assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros; omega. +assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros x y z. + rewrite !PeanoNat.Nat.add_assoc, (PeanoNat.Nat.add_comm (g x) (g y)); reflexivity. assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). repeat red; auto. -assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega. +assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros x y z. + set (u := (f x + g x)); set (v := (f y + g y)). + rewrite !PeanoNat.Nat.add_assoc, (PeanoNat.Nat.add_comm u). + reflexivity. assert (st : Equivalence (@Logic.eq nat)) by (split; congruence). intros s;pattern s; apply set_rec. intros. @@ -859,7 +864,10 @@ rewrite <- (fold_equal _ _ st _ fc ft 0 _ _ H). rewrite <- (fold_equal _ _ st _ gc gt 0 _ _ H). rewrite <- (fold_equal _ _ st _ fgc fgt 0 _ _ H); auto. intros; do 3 (rewrite (fold_add _ _ st);auto). -rewrite H0;simpl;omega. +rewrite H0;simpl. +rewrite <- !(PeanoNat.Nat.add_assoc (f x)); f_equal. +rewrite !PeanoNat.Nat.add_assoc. f_equal. +apply PeanoNat.Nat.add_comm. do 3 rewrite fold_empty;auto. Qed. @@ -872,7 +880,11 @@ assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))). repeat red; intros. rewrite (Hf _ _ H); auto. assert (ct : transposeL (fun x => plus (if f x then 1 else 0))). - red; intros; omega. + red; intros. + set (a := if f x then _ else _). + rewrite PeanoNat.Nat.add_comm. + rewrite <- !PeanoNat.Nat.add_assoc. f_equal. + apply PeanoNat.Nat.add_comm. intros s;pattern s; apply set_rec. intros. change elt with E.t. @@ -921,9 +933,11 @@ Lemma sum_compat : forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g -> forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s. intros. -unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto with *. +unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto with fset. intros x x' Hx y y' Hy. rewrite Hx, Hy; auto. +intros x y z; rewrite !PeanoNat.Nat.add_assoc; f_equal; apply PeanoNat.Nat.add_comm. intros x x' Hx y y' Hy. rewrite Hx, Hy; auto. +intros x y z; rewrite !PeanoNat.Nat.add_assoc; f_equal; apply PeanoNat.Nat.add_comm. Qed. End Sum. diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 2a9e15ab37..8538b54c08 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -29,7 +29,7 @@ Table of contents: 3. Weak classical axioms -3.1. Weak excluded middle +3.1. Weak excluded middle and classical de Morgan law 3.2. Gödel-Dummett axiom and right distributivity of implication over disjunction @@ -514,7 +514,7 @@ End Weak_proof_irrelevance_CCI. (** * Weak classical axioms *) (** We show the following increasing in the strength of axioms: - - weak excluded-middle + - weak excluded-middle and classical De Morgan's law - right distributivity of implication over disjunction and Gödel-Dummett axiom - independence of general premises and drinker's paradox - excluded-middle @@ -523,11 +523,15 @@ End Weak_proof_irrelevance_CCI. (** ** Weak excluded-middle *) (** The weak classical logic based on [~~A \/ ~A] is referred to with - name KC in [[ChagrovZakharyaschev97]] + name KC in [[ChagrovZakharyaschev97]]. See [[SorbiTerwijn11]] for + a short survey. [[ChagrovZakharyaschev97]] Alexander Chagrov and Michael Zakharyaschev, "Modal Logic", Clarendon Press, 1997. -*) + + [[SorbiTerwijn11]] Andrea Sorbi and Sebastiaan A. Terwijn, + "Generalizations of the weak law of the excluded-middle", Notre + Dame J. Formal Logic, vol 56(2), pp 321-331, 2015. *) Definition weak_excluded_middle := forall A:Prop, ~~A \/ ~A. @@ -539,16 +543,21 @@ Definition weak_excluded_middle := Definition weak_generalized_excluded_middle := forall A B:Prop, ((A -> B) -> B) \/ (A -> B). +(** Classical De Morgan's law *) + +Definition classical_de_morgan_law := + forall A B:Prop, ~(A /\ B) -> ~A \/ ~B. + (** ** Gödel-Dummett axiom *) (** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]]. [[Dummett59]] Michael A. E. Dummett. "A Propositional Calculus - with a Denumerable Matrix", In the Journal of Symbolic Logic, Vol - 24 No. 2(1959), pp 97-103. + with a Denumerable Matrix", In the Journal of Symbolic Logic, vol + 24(2), pp 97-103, 1959. [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül", - Ergeb. Math. Koll. 4 (1933), pp. 34-38. + Ergeb. Math. Koll. 4, pp. 34-38, 1933. *) Definition GodelDummett := forall A B:Prop, (A -> B) \/ (B -> A). @@ -590,6 +599,16 @@ Proof. right; intro HA; apply (HAnotA HA HA). Qed. +(** The weak excluded middle is equivalent to the classical De Morgan's law *) + +Lemma weak_excluded_middle_iff_classical_de_morgan_law : + weak_excluded_middle <-> classical_de_morgan_law. +Proof. + split; [intro WEM|intro CDML]; intros A *. + - destruct (WEM A); tauto. + - destruct (CDML A (~A)); tauto. +Qed. + (** ** Independence of general premises and drinker's paradox *) (** Independence of general premises is the unconstrained, non 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 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** The first three levels of homotopy type theory: homotopy propositions, + homotopy sets and homotopy one types. For more information, + https://github.com/HoTT/HoTT + and + https://homotopytypetheory.org/book + + Univalence is not assumed here, and equality is Coq's usual inductive + type eq in sort Prop. This is a little different from HoTT, where + sort Prop does not exist and equality is directly in sort Type. *) + + +(* It is almost impossible to prove that a type is a homotopy proposition + without funext, so we assume it here. *) +Require Import Coq.Logic.FunctionalExtensionality. + +(* A homotopy proposition is a type that has at most one element. + Its unique inhabitant, when it exists, is to be interpreted as the + proof of the homotopy proposition. + Homotopy propositions are therefore an alternative to the sort Prop, + to select which types represent mathematical propositions. *) +Definition IsHProp (P : Type) : Prop + := forall p q : P, p = q. + +(* A homotopy set is a type such as each equality type x = y is a + homotopy proposition. For example, any type which equality is + decidable in sort Prop is a homotopy set, as shown in file + Coq.Logic.Eqdep_dec.v. *) +Definition IsHSet (X : Type) : Prop + := forall (x y : X) (p q : x = y), p = q. + +Definition IsHOneType (X : Type) : Prop + := forall (x y : X) (p q : x = y) (r s : p = q), r = s. + +Lemma forall_hprop : forall (A : Type) (P : A -> 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/QArith/QArith_base.v b/theories/QArith/QArith_base.v index b60feb9256..54d35cded2 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -79,7 +79,7 @@ Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope. Lemma inject_Z_injective (a b: Z): inject_Z a == inject_Z b <-> a = b. Proof. - unfold Qeq. simpl. omega. + unfold Qeq; simpl; rewrite !Z.mul_1_r; reflexivity. Qed. (** Another approach : using Qcompare for defining order relations. *) @@ -599,9 +599,7 @@ Proof. Qed. Lemma Qle_antisym x y : x<=y -> y<=x -> x==y. -Proof. - unfold Qle, Qeq; auto with zarith. -Qed. +Proof. apply Z.le_antisymm. Qed. Lemma Qle_trans : forall x y z, x<=y -> y<=z -> x<=z. Proof. @@ -618,14 +616,10 @@ Qed. Hint Resolve Qle_trans : qarith. Lemma Qlt_irrefl x : ~x<x. -Proof. - unfold Qlt. auto with zarith. -Qed. +Proof. apply Z.lt_irrefl. Qed. Lemma Qlt_not_eq x y : x<y -> ~ x==y. -Proof. - unfold Qlt, Qeq; auto with zarith. -Qed. +Proof. apply Z.lt_neq. Qed. Lemma Zle_Qle (x y: Z): (x <= y)%Z = (inject_Z x <= inject_Z y). Proof. @@ -647,9 +641,7 @@ Proof. Qed. Lemma Qlt_le_weak x y : x<y -> x<=y. -Proof. - unfold Qle, Qlt; auto with zarith. -Qed. +Proof. apply Z.lt_le_incl. Qed. Lemma Qle_lt_trans : forall x y z, x<=y -> y<z -> x<z. Proof. @@ -684,25 +676,17 @@ Qed. (** [x<y] iff [~(y<=x)] *) -Lemma Qnot_lt_le : forall x y, ~ x<y -> y<=x. -Proof. - unfold Qle, Qlt; auto with zarith. -Qed. +Lemma Qnot_lt_le x y : ~ x < y -> y <= x. +Proof. apply Z.nlt_ge. Qed. -Lemma Qnot_le_lt : forall x y, ~ x<=y -> y<x. -Proof. - unfold Qle, Qlt; auto with zarith. -Qed. +Lemma Qnot_le_lt x y : ~ x <= y -> y < x. +Proof. apply Z.nle_gt. Qed. -Lemma Qlt_not_le : forall x y, x<y -> ~ y<=x. -Proof. - unfold Qle, Qlt; auto with zarith. -Qed. +Lemma Qlt_not_le x y : x < y -> ~ y <= x. +Proof. apply Z.lt_nge. Qed. -Lemma Qle_not_lt : forall x y, x<=y -> ~ y<x. -Proof. - unfold Qle, Qlt; auto with zarith. -Qed. +Lemma Qle_not_lt x y : x <= y -> ~ y < x. +Proof. apply Z.le_ngt. Qed. Lemma Qle_lt_or_eq : forall x y, x<=y -> x<y \/ x==y. Proof. @@ -746,21 +730,24 @@ Defined. Lemma Qopp_le_compat : forall p q, p<=q -> -q <= -p. Proof. intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl. - rewrite !Z.mul_opp_l. omega. + now rewrite !Z.mul_opp_l, <- Z.opp_le_mono. Qed. + Hint Resolve Qopp_le_compat : qarith. Lemma Qle_minus_iff : forall p q, p <= q <-> 0 <= q+-p. Proof. intros (x1,x2) (y1,y2); unfold Qle; simpl. - rewrite Z.mul_opp_l. omega. + rewrite Z.mul_1_r, Z.mul_opp_l, <- Z.le_sub_le_add_r, Z.opp_involutive. + reflexivity. Qed. Lemma Qlt_minus_iff : forall p q, p < q <-> 0 < q+-p. Proof. intros (x1,x2) (y1,y2); unfold Qlt; simpl. - rewrite Z.mul_opp_l. omega. + rewrite Z.mul_1_r, Z.mul_opp_l, <- Z.lt_sub_lt_add_r, Z.opp_involutive. + reflexivity. Qed. Lemma Qplus_le_compat : @@ -831,9 +818,11 @@ Lemma Qmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z. Proof. intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl. Open Scope Z_scope. + rewrite Z.mul_1_r. intros; simpl_mult. rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1). - apply Z.mul_le_mono_nonneg_r; auto with zarith. + apply Z.mul_le_mono_nonneg_r; auto. + now apply Z.mul_nonneg_nonneg. Close Scope Z_scope. Qed. @@ -843,9 +832,10 @@ Proof. Open Scope Z_scope. simpl_mult. rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1). + rewrite Z.mul_1_r. intros LT LE. apply Z.mul_le_mono_pos_r in LE; trivial. - apply Z.mul_pos_pos; [omega|easy]. + apply Z.mul_pos_pos; easy. Close Scope Z_scope. Qed. @@ -866,10 +856,11 @@ Lemma Qmult_lt_compat_r : forall x y z, 0 < z -> x < y -> x*z < y*z. Proof. intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl. Open Scope Z_scope. + rewrite Z.mul_1_r. intros; simpl_mult. rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1). apply Z.mul_lt_mono_pos_r; auto with zarith. - apply Z.mul_pos_pos; [omega|reflexivity]. + apply Z.mul_pos_pos; easy. Close Scope Z_scope. Qed. @@ -880,8 +871,9 @@ Proof. unfold Qle, Qlt; simpl. simpl_mult. rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1). + rewrite Z.mul_1_r. intro LT. rewrite <- Z.mul_lt_mono_pos_r. reflexivity. - apply Z.mul_pos_pos; [omega|reflexivity]. + now apply Z.mul_pos_pos. Close Scope Z_scope. Qed. @@ -896,6 +888,7 @@ Proof. intros a b Ha Hb. unfold Qle in *. simpl in *. +rewrite Z.mul_1_r in *. auto with *. Qed. diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 78cd549ce6..e314f64028 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -35,7 +35,7 @@ Proof. rewrite <- Hg in LE; clear Hg. assert (0 <> g) by (intro; subst; discriminate). rewrite Z2Pos.id. ring. - rewrite <- (Z.mul_pos_cancel_l g); [now rewrite <- Hd | omega]. + now rewrite <- (Z.mul_pos_cancel_l g); [ rewrite <- Hd | apply Z.le_neq ]. Close Scope Z_scope. Qed. @@ -60,8 +60,8 @@ Proof. - congruence. - (*rel_prime*) constructor. - * exists aa; auto with zarith. - * exists bb; auto with zarith. + * exists aa; auto using Z.mul_1_r. + * exists bb; auto using Z.mul_1_r. * intros x Ha Hb. destruct Hg1 as (Hg11,Hg12,Hg13). destruct (Hg13 (g*x)) as (x',Hx). @@ -73,8 +73,8 @@ Proof. apply Z.mul_reg_l with g; auto. rewrite Hx at 1; ring. - (* rel_prime *) constructor. - * exists cc; auto with zarith. - * exists dd; auto with zarith. + * exists cc; auto using Z.mul_1_r. + * exists dd; auto using Z.mul_1_r. * intros x Hc Hd. inversion Hg'1 as (Hg'11,Hg'12,Hg'13). destruct (Hg'13 (g'*x)) as (x',Hx). @@ -85,9 +85,9 @@ Proof. exists x'. apply Z.mul_reg_l with g'; auto. rewrite Hx at 1; ring. - apply Z.lt_gt. - rewrite <- (Z.mul_pos_cancel_l g); [now rewrite <- Hg4 | omega]. + rewrite <- (Z.mul_pos_cancel_l g); [ now rewrite <- Hg4 | apply Z.le_neq; intuition ]. - apply Z.lt_gt. - rewrite <- (Z.mul_pos_cancel_l g'); [now rewrite <- Hg'4 | omega]. + rewrite <- (Z.mul_pos_cancel_l g'); [now rewrite <- Hg'4 | apply Z.le_neq; intuition ]. - apply Z.mul_reg_l with (g*g'). * rewrite Z.mul_eq_0. now destruct 1. * rewrite Z.mul_shuffle1, <- Hg3, <- Hg'4. diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index af5c471d5d..8d68038582 100644 --- a/theories/QArith/Qround.v +++ b/theories/QArith/Qround.v @@ -13,7 +13,8 @@ Require Import QArith. Lemma Qopp_lt_compat: forall p q : Q, p < q -> - q < - p. Proof. intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl. -rewrite !Z.mul_opp_l; omega. +rewrite !Z.mul_opp_l. +apply Z.opp_lt_mono. Qed. Hint Resolve Qopp_lt_compat : qarith. @@ -38,7 +39,7 @@ intros z. unfold Qceiling. simpl. rewrite Zdiv_1_r. -auto with *. +apply Z.opp_involutive. Qed. Lemma Qfloor_le : forall x, Qfloor x <= x. @@ -119,7 +120,7 @@ Lemma Qceiling_resp_le : forall x y, x <= y -> (Qceiling x <= Qceiling y)%Z. Proof. intros x y Hxy. unfold Qceiling. -cut (Qfloor (-y) <= Qfloor (-x))%Z; auto with *. +rewrite <- Z.opp_le_mono; auto with qarith. Qed. Hint Resolve Qceiling_resp_le : qarith. 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 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import Coq.Logic.Eqdep_dec. +Require Import Coq.Logic.FunctionalExtensionality. +Require Import Coq.Logic.HLevels. +Require Import QArith. +Require Import Qabs. +Require Import ConstructiveCauchyReals. +Require Import ConstructiveRcomplete. + +(** + Classical Dedekind reals. With the 3 logical axioms funext, + sig_forall_dec and sig_not_dec, the lower cuts defined as + functions Q -> 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 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) -(************************************************************************) - -(*********************************************************) -(** * Basic lemmas for the contructive real numbers *) -(*********************************************************) - -(* Implement interface ConstructiveReals opaquely with - Cauchy reals and prove basic results. - Those are therefore true for any implementation of - ConstructiveReals (for example with Dedekind reals). - - This file is the recommended import for working with - constructive reals, do not use ConstructiveCauchyReals - directly. *) - -Require Import ConstructiveCauchyRealsMult. -Require Import ConstructiveRcomplete. -Require Export ConstructiveReals. -Require Import Zpower. -Require Export ZArithRing. -Require Import Omega. -Require Import QArith_base. -Require Import Qring. - -Declare Scope R_scope_constr. - -Local Open Scope Z_scope. -Local Open Scope R_scope_constr. - -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). 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) with (-(1#p))%Q in abs. - rewrite opp_inject_Q in abs. destruct a. contradiction. - reflexivity. -Defined. - -Definition CR : ConstructiveReals. -Proof. - exact CRealImplem. -Qed. (* Keep it opaque to possibly change the implementation later *) - -Definition R := CRcarrier CR. - -Definition Req := orderEq R (CRlt CR). -Definition Rle (x y : R) := CRlt CR y x -> 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. diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v index a760a0af6a..0df1442f46 100644 --- a/theories/Reals/Rtrigo1.v +++ b/theories/Reals/Rtrigo1.v @@ -18,6 +18,7 @@ Require Export Cos_rel. Require Export Cos_plus. Require Import ZArith_base. Require Import Zcomplements. +Import Omega. Require Import Lra. Require Import Ranalysis1. Require Import Rsqrt_def. diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index a8e6993a63..cc216b21f8 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -12,7 +12,6 @@ Require Import OrderedType. Require Import ZArith. Require Import PeanoNat. Require Import Ascii String. -Require Import Omega. Require Import NArith Ndec. Require Import Compare_dec. @@ -55,7 +54,7 @@ Module Nat_as_OT <: UsualOrderedType. Proof. unfold lt; intros; apply lt_trans with y; auto. Qed. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. - Proof. unfold lt, eq; intros; omega. Qed. + Proof. unfold lt, eq; intros ? ? LT ->; revert LT; apply Nat.lt_irrefl. Qed. Definition compare x y : Compare lt eq x y. Proof. @@ -85,10 +84,10 @@ Module Z_as_OT <: UsualOrderedType. Definition lt (x y:Z) := (x<y). Lemma lt_trans : forall x y z, x<y -> y<z -> x<z. - Proof. intros; omega. Qed. + Proof. exact Z.lt_trans. Qed. Lemma lt_not_eq : forall x y, x<y -> ~ x=y. - Proof. intros; omega. Qed. + Proof. intros x y LT ->; revert LT; apply Z.lt_irrefl. Qed. Definition compare x y : Compare lt eq x y. Proof. diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index b0744caa7b..38f9336f1b 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -18,6 +18,7 @@ Require Export Zpow_def. (** Extra modules using [Omega] or [Ring]. *) +Require Export Omega. Require Export Zcomplements. Require Export Zpower. Require Export Zdiv. diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 73c8ec11c6..0be6f8c8de 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -10,7 +10,6 @@ Require Import ZArithRing. Require Import ZArith_base. -Require Export Omega. Require Import Wf_nat. Local Open Scope Z_scope. @@ -40,10 +39,19 @@ Proof. reflexivity. Qed. Lemma floor_ok : forall p:positive, floor p <= Zpos p < 2 * floor p. Proof. - unfold floor. induction p; simpl. - - rewrite !Pos2Z.inj_xI, (Pos2Z.inj_xO (xO _)), Pos2Z.inj_xO. omega. - - rewrite (Pos2Z.inj_xO (xO _)), (Pos2Z.inj_xO p), Pos2Z.inj_xO. omega. - - omega. + unfold floor. induction p as [p [IH1p IH2p]|p [IH1p IH2]|]; simpl. + - rewrite !Pos2Z.inj_xI, (Pos2Z.inj_xO (xO _)), Pos2Z.inj_xO. + split. + + apply Z.le_trans with (2 * Z.pos p); auto with zarith. + rewrite <- (Z.add_0_r (2 * Z.pos p)) at 1; auto with zarith. + + apply Z.lt_le_trans with (2 * (Z.pos p + 1)). + * rewrite Z.mul_add_distr_l, Z.mul_1_r. + apply Zplus_lt_compat_l; red; auto with zarith. + * apply Z.mul_le_mono_nonneg_l; auto with zarith. + rewrite Z.add_1_r; apply Zlt_le_succ; auto. + - rewrite (Pos2Z.inj_xO (xO _)), (Pos2Z.inj_xO p), Pos2Z.inj_xO. + split; auto with zarith. + - split; auto with zarith; red; auto. Qed. (**********************************************************************) @@ -64,9 +72,10 @@ Proof. - rewrite Z.abs_eq; auto; intros. destruct (H (Z.abs m)); auto with zarith. destruct (Zabs_dec m) as [-> | ->]; trivial. - - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. - destruct (H (Z.abs m)); auto with zarith. - destruct (Zabs_dec m) as [-> | ->]; trivial. + - rewrite Z.abs_neq, Z.opp_involutive; intros. + + destruct (H (Z.abs m)); auto with zarith. + destruct (Zabs_dec m) as [-> | ->]; trivial. + + apply Z.opp_le_mono; rewrite Z.opp_involutive; auto. Qed. Theorem Z_lt_abs_induction : @@ -84,9 +93,10 @@ Proof. - rewrite Z.abs_eq; auto; intros. elim (H (Z.abs m)); intros; auto with zarith. elim (Zabs_dec m); intro eq; rewrite eq; trivial. - - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. - destruct (H (Z.abs m)); auto with zarith. - destruct (Zabs_dec m) as [-> | ->]; trivial. + - rewrite Z.abs_neq, Z.opp_involutive; intros. + + destruct (H (Z.abs m)); auto with zarith. + destruct (Zabs_dec m) as [-> | ->]; trivial. + + apply Z.opp_le_mono; rewrite Z.opp_involutive; auto. Qed. (** To do case analysis over the sign of [z] *) @@ -129,7 +139,7 @@ Section Zlength_properties. clear l. induction l. auto with zarith. intros. simpl length; simpl Zlength_aux. - rewrite IHl, Nat2Z.inj_succ; auto with zarith. + rewrite IHl, Nat2Z.inj_succ, Z.add_succ_comm; auto. unfold Zlength. now rewrite H. Qed. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 78df9941c9..2aaab3e50e 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -14,7 +14,7 @@ (** Initial Contribution by Claude Marché and Xavier Urbain *) Require Export ZArith_base. -Require Import Zbool Omega ZArithRing Zcomplements Setoid Morphisms. +Require Import Zbool ZArithRing Zcomplements Setoid Morphisms. Local Open Scope Z_scope. (** The definition of the division is now in [BinIntDef], the initial @@ -67,7 +67,12 @@ Definition Remainder_alt r b := Z.abs r < Z.abs b /\ Z.sgn r <> - Z.sgn b. Lemma Remainder_equiv : forall r b, Remainder r b <-> Remainder_alt r b. Proof. - intros; unfold Remainder, Remainder_alt; omega with *. + unfold Remainder, Remainder_alt. + intros [ | r | r ] [ | b | b ]; intuition try easy. + - now apply Z.opp_lt_mono. + - right; split. + + now apply Z.opp_lt_mono. + + apply Pos2Z.neg_is_nonpos. Qed. Hint Unfold Remainder : core. @@ -104,7 +109,7 @@ Proof (Z.mod_neg_bound a b). Lemma Z_div_mod_eq a b : b > 0 -> a = b*(a/b) + (a mod b). Proof. - intros Hb; apply Z.div_mod; auto with zarith. + intros Hb; apply Z.div_mod; now intros ->. Qed. Lemma Zmod_eq_full a b : b<>0 -> a mod b = a - (a/b)*b. @@ -224,18 +229,25 @@ Proof Z.div_mul. (* Division of positive numbers is positive. *) Lemma Z_div_pos: forall a b, b > 0 -> 0 <= a -> 0 <= a/b. -Proof. intros. apply Z.div_pos; auto with zarith. Qed. +Proof. intros. apply Z.div_pos; auto using Z.gt_lt. Qed. Lemma Z_div_ge0: forall a b, b > 0 -> a >= 0 -> a/b >=0. Proof. - intros; generalize (Z_div_pos a b H); auto with zarith. + intros; apply Z.le_ge, Z_div_pos; auto using Z.ge_le. Qed. (** As soon as the divisor is greater or equal than 2, the division is strictly decreasing. *) Lemma Z_div_lt : forall a b:Z, b >= 2 -> a > 0 -> a/b < a. -Proof. intros. apply Z.div_lt; auto with zarith. Qed. +Proof. + intros a b b_ge_2 a_gt_0. + apply Z.div_lt. + - apply Z.gt_lt; exact a_gt_0. + - apply (Z.lt_le_trans _ 2). + + reflexivity. + + apply Z.ge_le; exact b_ge_2. +Qed. (** A division of a small number by a bigger one yields zero. *) @@ -250,17 +262,17 @@ Proof Z.mod_small. (** [Z.ge] is compatible with a positive division. *) Lemma Z_div_ge : forall a b c:Z, c > 0 -> a >= b -> a/c >= b/c. -Proof. intros. apply Z.le_ge. apply Z.div_le_mono; auto with zarith. Qed. +Proof. intros. apply Z.le_ge. apply Z.div_le_mono; auto using Z.gt_lt, Z.ge_le. Qed. (** Same, with [Z.le]. *) Lemma Z_div_le : forall a b c:Z, c > 0 -> a <= b -> a/c <= b/c. -Proof. intros. apply Z.div_le_mono; auto with zarith. Qed. +Proof. intros. apply Z.div_le_mono; auto using Z.gt_lt. Qed. (** With our choice of division, rounding of (a/b) is always done toward bottom: *) Lemma Z_mult_div_ge : forall a b:Z, b > 0 -> b*(a/b) <= a. -Proof. intros. apply Z.mul_div_le; auto with zarith. Qed. +Proof. intros. apply Z.mul_div_le; auto using Z.gt_lt. Qed. Lemma Z_mult_div_ge_neg : forall a b:Z, b < 0 -> b*(a/b) >= a. Proof. intros. apply Z.le_ge. apply Z.mul_div_ge; auto with zarith. Qed. @@ -296,14 +308,18 @@ Proof. intros a b q; rewrite Z.mul_comm; apply Z.div_le_lower_bound. Qed. Lemma Zdiv_le_compat_l: forall p q r, 0 <= p -> 0 < q < r -> p / r <= p / q. -Proof. intros; apply Z.div_le_compat_l; auto with zarith. Qed. +Proof. intros; apply Z.div_le_compat_l; intuition auto using Z.lt_le_incl. Qed. Theorem Zdiv_sgn: forall a b, 0 <= Z.sgn (a/b) * Z.sgn a * Z.sgn b. Proof. destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith; generalize (Z.div_pos (Zpos a) (Zpos b)); unfold Z.div, Z.div_eucl; - destruct Z.pos_div_eucl as (q,r); destruct r; omega with *. + destruct Z.pos_div_eucl as (q,r); destruct r; + rewrite ?Z.mul_1_r, <-?Z.opp_eq_mul_m1, ?Z.sgn_opp, ?Z.opp_involutive; + match goal with [|- (_ -> _ -> ?P) -> _] => + intros HH; assert (HH1 : P); auto with zarith + end; apply Z.sgn_nonneg; auto with zarith. Qed. (** * Relations between usual operations and Z.modulo and Z.div *) @@ -346,14 +362,14 @@ Proof. intros. zero_or_not b. apply Z.div_opp_l_z; auto. Qed. Lemma Z_div_nz_opp_full : forall a b:Z, a mod b <> 0 -> (-a)/b = -(a/b)-1. -Proof. intros a b. zero_or_not b. intros; rewrite Z.div_opp_l_nz; auto. Qed. +Proof. intros a b. zero_or_not b. easy. intros; rewrite Z.div_opp_l_nz; auto. Qed. Lemma Z_div_zero_opp_r : forall a b:Z, a mod b = 0 -> a/(-b) = -(a/b). Proof. intros. zero_or_not b. apply Z.div_opp_r_z; auto. Qed. Lemma Z_div_nz_opp_r : forall a b:Z, a mod b <> 0 -> a/(-b) = -(a/b)-1. -Proof. intros a b. zero_or_not b. intros; rewrite Z.div_opp_r_nz; auto. Qed. +Proof. intros a b. zero_or_not b. easy. intros; rewrite Z.div_opp_r_nz; auto. Qed. (** Cancellations. *) @@ -372,14 +388,16 @@ Lemma Zmult_mod_distr_l: forall a b c, (c*a) mod (c*b) = c * (a mod b). Proof. intros. zero_or_not c. rewrite (Z.mul_comm c b); zero_or_not b. - rewrite (Z.mul_comm b c). apply Z.mul_mod_distr_l; auto. + + now rewrite Z.mul_0_r. + + rewrite (Z.mul_comm b c). apply Z.mul_mod_distr_l; auto. Qed. Lemma Zmult_mod_distr_r: forall a b c, (a*c) mod (b*c) = (a mod b) * c. Proof. intros. zero_or_not b. rewrite (Z.mul_comm b c); zero_or_not c. - rewrite (Z.mul_comm c b). apply Z.mul_mod_distr_r; auto. + + now rewrite Z.mul_0_r. + + rewrite (Z.mul_comm c b). apply Z.mul_mod_distr_r; auto. Qed. (** Operations modulo. *) @@ -456,7 +474,7 @@ Proof. unfold eqm; auto. Qed. Lemma eqm_trans : forall a b c, a == b -> b == c -> a == c. -Proof. unfold eqm; eauto with *. Qed. +Proof. now unfold eqm; intros a b c ->. Qed. Instance eqm_setoid : Equivalence eqm. Proof. @@ -501,7 +519,8 @@ End EqualityModulo. Lemma Zdiv_Zdiv : forall a b c, 0<=b -> 0<=c -> (a/b)/c = a/(b*c). Proof. intros. zero_or_not b. rewrite Z.mul_comm. zero_or_not c. - rewrite Z.mul_comm. apply Z.div_div; auto with zarith. + rewrite Z.mul_comm. apply Z.div_div; auto. + apply Z.le_neq; auto. Qed. (** Unfortunately, the previous result isn't always true on negative numbers. @@ -519,7 +538,10 @@ Qed. Theorem Zdiv_mult_le: forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b. Proof. - intros. zero_or_not b. apply Z.div_mul_le; auto with zarith. Qed. + intros. zero_or_not b. now rewrite Z.mul_0_r. + apply Z.div_mul_le; auto. + apply Z.le_neq; auto. +Qed. (** Z.modulo is related to divisibility (see more in Znumtheory) *) @@ -566,17 +588,17 @@ Qed. Lemma Z_div_same : forall a, a > 0 -> a/a = 1. Proof. - intros; apply Z_div_same_full; auto with zarith. + now intros; apply Z_div_same_full; intros ->. Qed. Lemma Z_div_plus : forall a b c:Z, c > 0 -> (a + b * c) / c = a / c + b. Proof. - intros; apply Z_div_plus_full; auto with zarith. + now intros; apply Z_div_plus_full; intros ->. Qed. Lemma Z_div_mult : forall a b:Z, b > 0 -> (a*b)/b = a. Proof. - intros; apply Z_div_mult_full; auto with zarith. + now intros; apply Z_div_mult_full; intros ->. Qed. Lemma Z_mod_plus : forall a b c:Z, c > 0 -> (a + b * c) mod c = a mod c. @@ -591,7 +613,7 @@ Qed. Lemma Z_div_exact_2 : forall a b:Z, b > 0 -> a mod b = 0 -> a = b*(a/b). Proof. - intros; apply Z_div_exact_full_2; auto with zarith. + now intros; apply Z_div_exact_full_2; auto; intros ->. Qed. Lemma Z_mod_zero_opp : forall a b:Z, b > 0 -> a mod b = 0 -> (-a) mod b = 0. @@ -673,14 +695,15 @@ Theorem Zdiv_eucl_extended : Proof. intros b Hb a. destruct (Z_le_gt_dec 0 b) as [Hb'|Hb']. - - assert (Hb'' : b > 0) by omega. + - assert (Hb'' : b > 0) by (apply Z.lt_gt, Z.le_neq; auto). rewrite Z.abs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ]. - - assert (Hb'' : - b > 0) by omega. + - assert (Hb'' : - b > 0). + { now apply Z.lt_gt, Z.opp_lt_mono; rewrite Z.opp_involutive; apply Z.gt_lt. } destruct (Zdiv_eucl_exist Hb'' a) as ((q,r),[]). exists (- q, r). split. + rewrite <- Z.mul_opp_comm; assumption. - + rewrite Z.abs_neq; [ assumption | omega ]. + + rewrite Z.abs_neq; [ assumption | apply Z.lt_le_incl, Z.gt_lt; auto ]. Qed. Arguments Zdiv_eucl_extended : default implicits. diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 5d1a13ff6c..01365135c5 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -117,17 +117,23 @@ Proof. right. now rewrite <- Z.mod_divide. Defined. +Lemma Z_lt_neq {x y: Z} : x < y -> y <> x. +Proof. auto using Z.lt_neq, Z.neq_sym. Qed. + Theorem Zdivide_Zdiv_eq a b : 0 < a -> (a | b) -> b = a * (b / a). Proof. intros Ha H. - rewrite (Z.div_mod b a) at 1; auto with zarith. - rewrite Zdivide_mod; auto with zarith. + rewrite (Z.div_mod b a) at 1. + + rewrite Zdivide_mod; auto with zarith. + + auto using Z_lt_neq. Qed. Theorem Zdivide_Zdiv_eq_2 a b c : 0 < a -> (a | b) -> (c * b) / a = c * (b / a). Proof. - intros. apply Z.divide_div_mul_exact; auto with zarith. + intros. apply Z.divide_div_mul_exact. + + now apply Z_lt_neq. + + auto with zarith. Qed. Theorem Zdivide_le: forall a b : Z, @@ -139,28 +145,30 @@ Qed. Theorem Zdivide_Zdiv_lt_pos a b : 1 < a -> 0 < b -> (a | b) -> 0 < b / a < b . Proof. - intros H1 H2 H3; split. - apply Z.mul_pos_cancel_l with a; auto with zarith. - rewrite <- Zdivide_Zdiv_eq; auto with zarith. - now apply Z.div_lt. + intros H1 H2 H3. + assert (0 < a) by (now transitivity 1). + split. + + apply Z.mul_pos_cancel_l with a; auto. + rewrite <- Zdivide_Zdiv_eq; auto. + + now apply Z.div_lt. Qed. Lemma Zmod_div_mod n m a: 0 < n -> 0 < m -> (n | m) -> a mod n = (a mod m) mod n. -Proof. +Proof with auto using Z_lt_neq. intros H1 H2 (p,Hp). - rewrite (Z.div_mod a m) at 1; auto with zarith. + rewrite (Z.div_mod a m) at 1... rewrite Hp at 1. - rewrite Z.mul_shuffle0, Z.add_comm, Z.mod_add; auto with zarith. + rewrite Z.mul_shuffle0, Z.add_comm, Z.mod_add... Qed. Lemma Zmod_divide_minus a b c: 0 < b -> a mod b = c -> (b | a - c). -Proof. - intros H H1. apply Z.mod_divide; auto with zarith. - rewrite Zminus_mod; auto with zarith. +Proof with auto using Z_lt_neq. + intros H H1. apply Z.mod_divide... + rewrite Zminus_mod. rewrite H1. rewrite <- (Z.mod_small c b) at 1. - rewrite Z.sub_diag, Z.mod_0_l; auto with zarith. + rewrite Z.sub_diag, Z.mod_0_l... subst. now apply Z.mod_pos_bound. Qed. @@ -169,10 +177,11 @@ Lemma Zdivide_mod_minus a b c: Proof. intros (H1, H2) H3. assert (0 < b) by Z.order. - replace a with ((a - c) + c); auto with zarith. - rewrite Z.add_mod; auto with zarith. - rewrite (Zdivide_mod (a-c) b); try rewrite Z.add_0_l; auto with zarith. - rewrite Z.mod_mod; try apply Zmod_small; auto with zarith. + assert (b <> 0) by now apply Z_lt_neq. + replace a with ((a - c) + c) by ring. + rewrite Z.add_mod; auto. + rewrite (Zdivide_mod (a-c) b); try rewrite Z.add_0_l; auto. + rewrite Z.mod_mod; try apply Zmod_small; auto. Qed. (** * Greatest common divisor (gcd). *) @@ -300,8 +309,9 @@ Section extended_euclid_algorithm. set (q := u3 / x) in *. assert (Hq : 0 <= u3 - q * x < x). replace (u3 - q * x) with (u3 mod x). - apply Z_mod_lt; omega. - assert (xpos : x > 0). omega. + apply Z_mod_lt. + apply Z.lt_gt, Z.le_neq; auto. + assert (xpos : x > 0) by (apply Z.lt_gt, Z.le_neq; auto). generalize (Z_div_mod_eq u3 x xpos). unfold q. intro eq; pattern u3 at 2; rewrite eq; ring. @@ -325,11 +335,13 @@ Section extended_euclid_algorithm. intros; apply euclid_rec with (u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := 1) (v3 := b); - auto with zarith; ring. + auto; ring. intros; apply euclid_rec with (u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := -1) (v3 := - b); - auto with zarith; try ring. + auto; try ring. + now apply Z.opp_nonneg_nonpos, Z.lt_le_incl, Z.gt_lt. + auto with zarith. Qed. End extended_euclid_algorithm. @@ -433,22 +445,24 @@ Lemma rel_prime_cross_prod : rel_prime a b -> rel_prime c d -> b > 0 -> d > 0 -> a * d = b * c -> a = c /\ b = d. Proof. - intros a b c d; intros. + intros a b c d; intros H H0 H1 H2 H3. elim (Z.divide_antisym b d). - split; auto with zarith. - rewrite H4 in H3. - rewrite Z.mul_comm in H3. - apply Z.mul_reg_l with d; auto with zarith. - intros; omega. - apply Gauss with a. - rewrite H3. - auto with zarith. - red; auto with zarith. - apply Gauss with c. - rewrite Z.mul_comm. - rewrite <- H3. - auto with zarith. - red; auto with zarith. + - split; auto with zarith. + rewrite H4 in H3. + rewrite Z.mul_comm in H3. + apply Z.mul_reg_l with d; auto. + contradict H2; rewrite H2; discriminate. + - intros H4; contradict H1; rewrite H4. + apply Zgt_asym, Z.lt_gt, Z.opp_lt_mono. + now rewrite Z.opp_involutive; apply Z.gt_lt. + - apply Gauss with a. + + rewrite H3; auto with zarith. + + now apply Zis_gcd_sym. + - apply Gauss with c. + + rewrite Z.mul_comm. + rewrite <- H3. + auto with zarith. + + now apply Zis_gcd_sym. Qed. (** After factorization by a gcd, the original numbers are relatively prime. *) @@ -457,32 +471,35 @@ Lemma Zis_gcd_rel_prime : forall a b g:Z, b > 0 -> g >= 0 -> Zis_gcd a b g -> rel_prime (a / g) (b / g). Proof. - intros a b g; intros. - assert (g <> 0). - intro. - elim H1; intros. - elim H4; intros. - rewrite H2 in H6; subst b; omega. + intros a b g; intros H H0 H1. + assert (H2 : g <> 0) by + (intro; + elim H1; intros; + elim H4; intros; + rewrite H2 in H6; subst b; + contradict H; rewrite Z.mul_0_r; discriminate). + assert (H3 : g > 0) by + (apply Z.lt_gt, Z.le_neq; split; try apply Z.ge_le; auto). unfold rel_prime. - destruct H1. - destruct H1 as (a',H1). - destruct H3 as (b',H3). + destruct H1 as [Ha Hb Hab]. + destruct Ha as [a' Ha']. + destruct Hb as [b' Hb']. replace (a/g) with a'; - [|rewrite H1; rewrite Z_div_mult; auto with zarith]. + [|rewrite Ha'; rewrite Z_div_mult; auto with zarith]. replace (b/g) with b'; - [|rewrite H3; rewrite Z_div_mult; auto with zarith]. + [|rewrite Hb'; rewrite Z_div_mult; auto with zarith]. constructor. - exists a'; auto with zarith. - exists b'; auto with zarith. - intros x (xa,H5) (xb,H6). - destruct (H4 (x*g)) as (x',Hx'). - exists xa; rewrite Z.mul_assoc; rewrite <- H5; auto. - exists xb; rewrite Z.mul_assoc; rewrite <- H6; auto. - replace g with (1*g) in Hx'; auto with zarith. - do 2 rewrite Z.mul_assoc in Hx'. - apply Z.mul_reg_r in Hx'; trivial. - rewrite Z.mul_1_r in Hx'. - exists x'; auto with zarith. + - exists a'; rewrite ?Z.mul_1_r; auto with zarith. + - exists b'; rewrite ?Z.mul_1_r; auto with zarith. + - intros x (xa,H5) (xb,H6). + destruct (Hab (x*g)) as (x',Hx'). + exists xa; rewrite Z.mul_assoc; rewrite <- H5; auto. + exists xb; rewrite Z.mul_assoc; rewrite <- H6; auto. + replace g with (1*g) in Hx'; auto with zarith. + do 2 rewrite Z.mul_assoc in Hx'. + apply Z.mul_reg_r in Hx'; trivial. + rewrite Z.mul_1_r in Hx'. + exists x'; auto with zarith. Qed. Theorem rel_prime_sym: forall a b, rel_prime a b -> rel_prime b a. @@ -504,18 +521,18 @@ Qed. Theorem rel_prime_1: forall n, rel_prime 1 n. Proof. intros n; red; apply Zis_gcd_intro; auto. - exists 1; auto with zarith. - exists n; auto with zarith. + exists 1; reflexivity. + exists n; rewrite Z.mul_1_r; reflexivity. Qed. Theorem not_rel_prime_0: forall n, 1 < n -> ~ rel_prime 0 n. Proof. intros n H H1; absurd (n = 1 \/ n = -1). - intros [H2 | H2]; subst; contradict H; auto with zarith. + intros [H2 | H2]; subst; contradict H; discriminate. case (Zis_gcd_unique 0 n n 1); auto. apply Zis_gcd_intro; auto. - exists 0; auto with zarith. - exists 1; auto with zarith. + exists 0; reflexivity. + exists 1; rewrite Z.mul_1_l; reflexivity. Qed. Theorem rel_prime_mod: forall p q, 0 < q -> @@ -528,15 +545,16 @@ Proof. apply bezout_rel_prime. apply Bezout_intro with q1 (r1 + q1 * (p / q)). rewrite <- H2. - pattern p at 3; rewrite (Z_div_mod_eq p q); try ring; auto with zarith. + pattern p at 3; rewrite (Z_div_mod_eq p q); try ring. + now apply Z.lt_gt. Qed. Theorem rel_prime_mod_rev: forall p q, 0 < q -> rel_prime (p mod q) q -> rel_prime p q. Proof. intros p q H H0. - rewrite (Z_div_mod_eq p q); auto with zarith; red. - apply Zis_gcd_sym; apply Zis_gcd_for_euclid2; auto with zarith. + rewrite (Z_div_mod_eq p q) by now apply Z.lt_gt. red. + apply Zis_gcd_sym; apply Zis_gcd_for_euclid2; auto. Qed. Theorem Zrel_prime_neq_mod_0: forall a b, 1 < b -> rel_prime a b -> a mod b <> 0. @@ -544,7 +562,8 @@ Proof. intros a b H H1 H2. case (not_rel_prime_0 _ H). rewrite <- H2. - apply rel_prime_mod; auto with zarith. + apply rel_prime_mod; auto. + now transitivity 1. Qed. (** * Primality *) @@ -563,25 +582,56 @@ Proof. assert (a = - p \/ - p < a < -1 \/ a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p). { assert (Z.abs a <= Z.abs p) as H2. - apply Zdivide_bounds; [ assumption | omega ]. + apply Zdivide_bounds; [ assumption | now intros -> ]. revert H2. pattern (Z.abs a); apply Zabs_ind; pattern (Z.abs p); apply Zabs_ind; - intros; omega. } + intros H2 H3 H4. + - destruct (Zle_lt_or_eq _ _ H4) as [H5 | H5]; try intuition. + destruct (Zle_lt_or_eq _ _ (Z.ge_le _ _ H3)) as [H6 | H6]; try intuition. + destruct (Zle_lt_or_eq _ _ (Zlt_le_succ _ _ H6)) as [H7 | H7]; intuition. + - contradict H2; apply Zlt_not_le; apply Z.lt_trans with (2 := H); red; auto. + - destruct (Zle_lt_or_eq _ _ H4) as [H5 | H5]. + + destruct (Zle_lt_or_eq _ _ H3) as [H6 | H6]; try intuition. + assert (H7 : a <= Z.pred 0) by (apply Z.lt_le_pred; auto). + destruct (Zle_lt_or_eq _ _ H7) as [H8 | H8]; intuition. + assert (- p < a < -1); try intuition. + now apply Z.opp_lt_mono; rewrite Z.opp_involutive. + + now left; rewrite <- H5, Z.opp_involutive. + - contradict H2. + apply Zlt_not_le; apply Z.lt_trans with (2 := H); red; auto. + } intuition idtac. (* -p < a < -1 *) - - absurd (rel_prime (- a) p); intuition. - inversion H2. - assert (- a | - a) by auto with zarith. - assert (- a | p) by auto with zarith. - apply H7, Z.divide_1_r in H8; intuition. + - absurd (rel_prime (- a) p). + + intros [H1p H2p H3p]. + assert (- a | - a) by auto with zarith. + assert (- a | p) by auto with zarith. + apply H3p, Z.divide_1_r in H5; auto with zarith. + destruct H5. + * contradict H4; rewrite <- (Z.opp_involutive a), H5 . + apply Z.lt_irrefl. + * contradict H4; rewrite <- (Z.opp_involutive a), H5 . + discriminate. + + apply H0; split. + * now apply Z.opp_le_mono; rewrite Z.opp_involutive; apply Z.lt_le_incl. + * now apply Z.opp_lt_mono; rewrite Z.opp_involutive. (* a = 0 *) - - inversion H1. subst a; omega. + - contradict H. + replace p with 0; try discriminate. + now apply sym_equal, Z.divide_0_l; rewrite <-H2. (* 1 < a < p *) - - absurd (rel_prime a p); intuition. - inversion H2. - assert (a | a) by auto with zarith. - assert (a | p) by auto with zarith. - apply H7, Z.divide_1_r in H8; intuition. + - absurd (rel_prime a p). + + intros [H1p H2p H3p]. + assert (a | a) by auto with zarith. + assert (a | p) by auto with zarith. + apply H3p, Z.divide_1_r in H5; auto with zarith. + destruct H5. + * contradict H3; rewrite <- (Z.opp_involutive a), H5 . + apply Z.lt_irrefl. + * contradict H3; rewrite <- (Z.opp_involutive a), H5 . + discriminate. + + apply H0; split; auto. + now apply Z.lt_le_incl. Qed. (** A prime number is relatively prime with any number it does not divide *) @@ -605,12 +655,17 @@ Proof. intros a p Hp [H1 H2]. apply rel_prime_sym; apply prime_rel_prime; auto. intros [q Hq]; subst a. - case (Z.le_gt_cases q 0); intros Hl. - absurd (q * p <= 0 * p); auto with zarith. - absurd (1 * p <= q * p); auto with zarith. + destruct Hp as [H3 H4]. + contradict H2; apply Zle_not_lt. + rewrite <- (Z.mul_1_l p) at 1. + apply Zmult_le_compat_r. + - apply (Zlt_le_succ 0). + apply Zmult_lt_0_reg_r with p. + + apply Z.le_succ_l, Z.lt_le_incl; auto. + + now apply Z.le_succ_l. + - apply Z.lt_le_incl, Z.le_succ_l, Z.lt_le_incl; auto. Qed. - (** If a prime [p] divides [ab] then it divides either [a] or [b] *) Lemma prime_mult : @@ -623,38 +678,44 @@ Qed. Lemma not_prime_0: ~ prime 0. Proof. - intros H1; case (prime_divisors _ H1 2); auto with zarith. + intros H1; case (prime_divisors _ H1 2); auto with zarith; intuition; discriminate. Qed. Lemma not_prime_1: ~ prime 1. Proof. - intros H1; absurd (1 < 1); auto with zarith. + intros H1; absurd (1 < 1). discriminate. inversion H1; auto. Qed. Lemma prime_2: prime 2. Proof. - apply prime_intro; auto with zarith. - intros n (H,H'); Z.le_elim H; auto with zarith. - - contradict H'; auto with zarith. - - subst n. constructor; auto with zarith. + apply prime_intro. + - red; auto. + - intros n (H,H'); Z.le_elim H; auto with zarith. + + contradict H'; auto with zarith. + now apply Zle_not_lt, (Zlt_le_succ 1). + + subst n. constructor; auto with zarith. Qed. Theorem prime_3: prime 3. Proof. apply prime_intro; auto with zarith. - intros n (H,H'); Z.le_elim H; auto with zarith. - - replace n with 2 by omega. - constructor; auto with zarith. - intros x (q,Hq) (q',Hq'). - exists (q' - q). ring_simplify. now rewrite <- Hq, <- Hq'. - - replace n with 1 by trivial. - constructor; auto with zarith. + - red; auto. + - intros n (H,H'); Z.le_elim H; auto with zarith. + + replace n with 2. + * constructor; auto with zarith. + intros x (q,Hq) (q',Hq'). + exists (q' - q). ring_simplify. now rewrite <- Hq, <- Hq'. + * apply Z.le_antisymm. + ++ now apply (Zlt_le_succ 1). + ++ now apply (Z.lt_le_pred _ 3). + + replace n with 1 by trivial. + constructor; auto with zarith. Qed. Theorem prime_ge_2 p : prime p -> 2 <= p. Proof. - intros (Hp,_); auto with zarith. + now intros (Hp,_); apply (Zlt_le_succ 1). Qed. Definition prime' p := 1<p /\ (forall n, 1<n<p -> ~ (n|p)). @@ -675,17 +736,24 @@ Proof. assert (Hx := Z.abs_nonneg x). set (y:=Z.abs x) in *; clearbody y; clear x; rename y into x. destruct (Z_0_1_more x Hx) as [->|[->|Hx']]. - + exfalso. apply Z.divide_0_l in Hxn. omega. + + exfalso. apply Z.divide_0_l in Hxn. + absurd (1 <= n). + * rewrite Hxn; red; auto. + * intuition. + now exists 1. + elim (H x); auto. split; trivial. - apply Z.le_lt_trans with n; auto with zarith. + apply Z.le_lt_trans with n; try intuition. apply Z.divide_pos_le; auto with zarith. + apply Z.lt_le_trans with (2 := H0); red; auto. - (* prime' -> prime *) constructor; trivial. intros n Hn Hnp. - case (Zis_gcd_unique n p n 1); auto with zarith. - constructor; auto with zarith. - apply H; auto with zarith. + case (Zis_gcd_unique n p n 1). + + constructor; auto with zarith. + + apply H; auto with zarith. + now intuition; apply Z.lt_le_incl. + + intros H1; intuition; subst n; discriminate. + + intros H1; intuition; subst n; discriminate. Qed. Theorem square_not_prime: forall a, ~ prime (a * a). @@ -698,7 +766,9 @@ Proof. assert (H' : 1 < a) by now apply (Z.square_lt_simpl_nonneg 1). apply (Ha' a). + split; trivial. - rewrite <- (Z.mul_1_l a) at 1. apply Z.mul_lt_mono_pos_r; omega. + rewrite <- (Z.mul_1_l a) at 1. + apply Z.mul_lt_mono_pos_r; auto. + apply Z.lt_trans with (2 := H'); red; auto. + exists a; auto. Qed. @@ -709,10 +779,11 @@ Proof. assert (Hp: 0 < p); try apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. assert (Hq: 0 < q); try apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. case prime_divisors with (2 := H2); auto. - intros H4; contradict Hp; subst; auto with zarith. - intros [H4| [H4 | H4]]; subst; auto. - contradict H; auto; apply not_prime_1. - contradict Hp; auto with zarith. + - intros H4; contradict Hp; subst; discriminate. + - intros [H4| [H4 | H4]]; subst; auto. + + contradict H; auto; apply not_prime_1. + + contradict Hp; apply Zle_not_lt, (Z.opp_le_mono _ 0). + now rewrite Z.opp_involutive; apply Z.lt_le_incl. Qed. (** we now prove that [Z.gcd] is indeed a gcd in @@ -748,6 +819,9 @@ Proof. apply Zgcd_is_gcd; auto. Z.le_elim H1. - generalize (Z.gcd_nonneg a b); auto with zarith. + intros H3 H4; contradict H3. + rewrite <- (Z.opp_involutive (Z.gcd a b)), <- H4. + now apply Zlt_not_le, Z.opp_lt_mono; rewrite Z.opp_involutive. - subst. now case (Z.gcd a b). Qed. @@ -801,7 +875,8 @@ Proof. case (Zis_gcd_unique a b (Z.gcd a b) 1); auto. apply Zgcd_is_gcd. intros H2; absurd (0 <= Z.gcd a b); auto with zarith. - generalize (Z.gcd_nonneg a b); auto with zarith. + - rewrite H2; red; auto. + - generalize (Z.gcd_nonneg a b); auto with zarith. Qed. Definition rel_prime_dec: forall a b, @@ -819,18 +894,25 @@ Definition prime_dec_aux: Proof. intros p m. case (Z_lt_dec 1 m); intros H1; - [ | left; intros; exfalso; omega ]. + [ | left; intros; exfalso; + contradict H1; apply Z.lt_trans with n; intuition]. pattern m; apply natlike_rec; auto with zarith. - left; intros; exfalso; omega. - intros x Hx IH; destruct IH as [F|E]. - destruct (rel_prime_dec x p) as [Y|N]. - left; intros n [HH1 HH2]. - rewrite Z.lt_succ_r in HH2. - Z.le_elim HH2; subst; auto with zarith. - - case (Z_lt_dec 1 x); intros HH1. - * right; exists x; split; auto with zarith. - * left; intros n [HHH1 HHH2]; contradict HHH1; auto with zarith. - - right; destruct E as (n,((H0,H2),H3)); exists n; auto with zarith. + - left; intros; exfalso. + absurd (1 < 0); try discriminate. + apply Z.lt_trans with n; intuition. + - intros x Hx IH; destruct IH as [F|E]. + + destruct (rel_prime_dec x p) as [Y|N]. + * left; intros n [HH1 HH2]. + rewrite Z.lt_succ_r in HH2. + Z.le_elim HH2; subst; auto with zarith. + * case (Z_lt_dec 1 x); intros HH1. + -- right; exists x; split; auto with zarith. + -- left; intros n [HHH1 HHH2]; contradict HHH1; auto with zarith. + apply Zle_not_lt; apply Z.le_trans with x. + ++ now apply Zlt_succ_le. + ++ now apply Znot_gt_le; contradict HH1; apply Z.gt_lt. + + right; destruct E as (n,((H0,H2),H3)); exists n; auto with zarith. + - apply Z.le_trans with (2 := Z.lt_le_incl _ _ H1); discriminate. Defined. Definition prime_dec: forall p, { prime p }+{ ~ prime p }. @@ -842,6 +924,7 @@ Proof. constructor; auto with zarith. * right; intros H3; inversion_clear H3 as [Hp1 Hp2]. case H2; intros n [Hn1 Hn2]; case Hn2; auto with zarith. + now apply Hp2; intuition; apply Z.lt_le_incl. + right; intros H3; inversion_clear H3 as [Hp1 Hp2]; case H1; auto. Defined. @@ -856,10 +939,15 @@ Proof. subst n; constructor; auto with zarith. - case H1; intros n (Hn1,Hn2). destruct (Z_0_1_more _ (Z.gcd_nonneg n p)) as [H|[H|H]]. - + exfalso. apply Z.gcd_eq_0_l in H. omega. + + exfalso. apply Z.gcd_eq_0_l in H. + absurd (1 < n). + * rewrite H; discriminate. + * now intuition. + elim Hn2. red. rewrite <- H. apply Zgcd_is_gcd. + exists (Z.gcd n p); split; [ split; auto | apply Z.gcd_divide_r ]. apply Z.le_lt_trans with n; auto with zarith. - apply Z.divide_pos_le; auto with zarith. - apply Z.gcd_divide_l. + * apply Z.divide_pos_le; auto with zarith. + -- apply Z.lt_trans with 1; intuition. + -- apply Z.gcd_divide_l. + * intuition. Qed. diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index 66e246616f..e65eb7cdc7 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import ZArith_base ZArithRing Zcomplements Zdiv Znumtheory. +Require Import ZArith_base ZArithRing Omega Zcomplements Zdiv Znumtheory. Require Export Zpower. Local Open Scope Z_scope. diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index f80d075b67..da8a9402dd 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Wf_nat ZArith_base Omega Zcomplements. +Require Import Wf_nat ZArith_base Zcomplements. Require Export Zpow_def. Local Open Scope Z_scope. @@ -220,7 +220,8 @@ Section Powers_of_2. Lemma two_p_pred x : 0 <= x -> two_p (Z.pred x) < two_p x. Proof. - rewrite !two_p_equiv. intros. apply Z.pow_lt_mono_r; auto with zarith. + rewrite !two_p_equiv. intros. apply Z.pow_lt_mono_r; auto using Z.lt_pred_l. + reflexivity. Qed. End Powers_of_2. @@ -265,17 +266,45 @@ Section power_div_with_rest. let '(q,r,d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in x = q * d + r /\ 0 <= r < d. Proof. - apply Pos.iter_invariant; [|omega]. - intros ((q,r),d) (H,H'). unfold Zdiv_rest_aux. - destruct q as [ |[q|q| ]|[q|q| ]]; try omega. + apply Pos.iter_invariant; [|rewrite Z.mul_1_r, Z.add_0_r; repeat split; auto; discriminate]. + intros ((q,r),d) (H,(H1',H2')). unfold Zdiv_rest_aux. + assert (H1 : 0 < d) by now apply Z.le_lt_trans with (1 := H1'). + assert (H2 : 0 <= d + r) by now apply Z.add_nonneg_nonneg; auto; apply Z.lt_le_incl. + assert (H3 : d + r < 2 * d) + by now rewrite <-Z.add_diag; apply Zplus_lt_compat_l. + assert (H4 : r < 2 * d) by now + apply Z.lt_le_trans with (1 * d); [ + rewrite Z.mul_1_l; auto | + apply Zmult_le_compat_r; try discriminate; + now apply Z.lt_le_incl]. + destruct q as [ |[q|q| ]|[q|q| ]]. + - repeat split; auto. - rewrite Pos2Z.inj_xI, Z.mul_add_distr_r in H. - rewrite Z.mul_shuffle3, Z.mul_assoc. omega. + rewrite Z.mul_shuffle3, Z.mul_assoc. + rewrite Z.mul_1_l in H; rewrite Z.add_assoc. + repeat split; auto with zarith. - rewrite Pos2Z.inj_xO in H. - rewrite Z.mul_shuffle3, Z.mul_assoc. omega. + rewrite Z.mul_shuffle3, Z.mul_assoc. + repeat split; auto. + - rewrite Z.mul_1_l in H; repeat split; auto. - rewrite Pos2Z.neg_xI, Z.mul_sub_distr_r in H. - rewrite Z.mul_sub_distr_r, Z.mul_shuffle3, Z.mul_assoc. omega. + rewrite Z.mul_sub_distr_r, Z.mul_shuffle3, Z.mul_assoc. + repeat split; auto. + rewrite !Z.mul_1_l, H, Z.add_assoc. + apply f_equal2 with (f := Z.add); auto. + rewrite <- Z.sub_sub_distr, <- !Z.add_diag, Z.add_simpl_r. + now rewrite Z.mul_1_l. - rewrite Pos2Z.neg_xO in H. - rewrite Z.mul_shuffle3, Z.mul_assoc. omega. + rewrite Z.mul_shuffle3, Z.mul_assoc. + repeat split; auto. + - repeat split; auto. + rewrite H, (Z.mul_opp_l 1), Z.mul_1_l, Z.add_assoc. + apply f_equal2 with (f := Z.add); auto. + rewrite Z.add_comm, <- Z.add_diag. + rewrite Z.mul_add_distr_l. + replace (-1 * d) with (-d). + + now rewrite Z.add_assoc, Z.add_opp_diag_r . + + now rewrite (Z.mul_opp_l 1), <-(Z.mul_opp_l 1). Qed. (** Old-style rich specification by proof of existence *) |