CoRN.reals.fast.CRArith
Require Import Ring_theory.
Require Import Setoid.
Require Import QArith.
Require Import Qabs.
Require Import Qround.
Require Export CRreal.
Require Import Complete.
Require Export CRFieldOps.
Require Import Qring.
Require Import CRing_Homomorphisms.
Require Import Qmetric.
Require Import CornTac.
Require Import Stability.
Require Import ConstructiveEpsilon.
Require Import Qdlog.
Require Import abstract_algebra.
Require Import interfaces.orders.
Open Local Scope CR_scope.
Operations on rational numbers over CR are the same as the operations
on rational numbers.
Lemma CReq_Qeq : ∀ (x y:Q), inject_Q_CR x == inject_Q_CR y ↔ (x == y)%Q.
Proof.
intros x y.
apply Cunit_eq.
Qed.
Lemma CRle_Qle : ∀ (x y:Q), inject_Q_CR x ≤ inject_Q_CR y ↔ (x ≤ y)%Q.
Proof.
split.
intros H.
destruct (Qlt_le_dec y x) as [X|X];[|assumption].
destruct (Qpos_lt_plus X) as [c Hc].
assert (Y:=(H ((1#2)*c)%Qpos)).
simpl in Y.
unfold Cap_raw in Y; simpl in Y.
rewrite → Qle_minus_iff in Y.
rewrite → Hc in Y.
autorewrite with QposElim in Y.
ring_simplify in Y.
elim (Qle_not_lt _ _ Y).
rewrite → Qlt_minus_iff.
ring_simplify.
apply Q.Qmult_lt_0_compat; auto with ×.
intros H e.
simpl.
unfold Cap_raw; simpl.
rewrite → Qle_minus_iff in H.
apply Qle_trans with (0%Q);[|assumption].
rewrite → Qle_minus_iff; ring_simplify.
apply Qpos_nonneg.
Qed.
Lemma CRplus_Qplus : ∀ (x y:Q), inject_Q_CR x + inject_Q_CR y == inject_Q_CR (x + y)%Q.
Proof.
intros x y e1 e2; apply ball_refl.
Qed.
Hint Rewrite <- CRplus_Qplus : toCRring.
Lemma CRopp_Qopp : ∀ (x:Q), - inject_Q_CR x == inject_Q_CR (- x)%Q.
Proof.
intros x e1 e2; apply ball_refl.
Qed.
Lemma CRminus_Qminus : ∀ (x y:Q), inject_Q_CR x - inject_Q_CR y == inject_Q_CR (x - y)%Q.
Proof.
intros x y e1 e2; apply ball_refl.
Qed.
Lemma CRmult_Qmult : ∀ (x y:Q), inject_Q_CR x × inject_Q_CR y == inject_Q_CR (x × y)%Q.
Proof.
intros x y.
rewrite → CRmult_scale.
intros e1 e2; apply ball_refl.
Qed.
Lemma Qap_CRap : ∀ (x y:Q), (~(x==y))%Q → (' x)><(' y).
Proof.
intros x y Hxy.
destruct (Q_dec x y) as [[H|H]|H]; try contradiction;
destruct (Qpos_lt_plus H) as [c Hc];[left|right]; ∃ c; abstract (rewrite → CRminus_Qminus;
rewrite → CRle_Qle; rewrite → Hc; ring_simplify; apply Qle_refl).
Defined.
Lemma CRinv_Qinv : ∀ (x:Q) x_, CRinvT (inject_Q_CR x) x_ == inject_Q_CR (/x)%Q.
Proof.
intros x [[c x_]|[c x_]];
[change (' c ≤ 0 + - 'x)%CR in x_|change (' c ≤ ' x + - 0)%CR in x_]; unfold CRinvT;
rewrite → CRopp_Qopp, CRplus_Qplus, CRle_Qle in x_; try rewrite → CRopp_Qopp;
rewrite → (@CRinv_pos_Qinv c).
rewrite → CRopp_Qopp.
rewrite → CReq_Qeq.
assert (¬x==0)%Q.
intros H.
rewrite → H in x_.
apply (Qle_not_lt _ _ x_).
apply Qpos_prf.
field.
intros X; apply H.
assumption.
rewrite → Qplus_0_l in x_.
assumption.
reflexivity.
rewrite → Qplus_0_r in x_.
assumption.
Qed.
Lemma inject_Q_product (l: list Q): (' cr_Product l) [=] cr_Product (map inject_Q_CR l).
Proof.
induction l.
reflexivity.
change (' (a × cr_Product l)%Q[=]cr_Product (map inject_Q_CR (a :: l))).
rewrite <- CRmult_Qmult.
rewrite IHl.
reflexivity.
Qed.
Lemma inject_Qred_ap (x y: Q): Qred x ≠ Qred y → ' x [#] ' y.
Proof with auto.
intro.
apply Qap_CRap.
intro.
apply H.
apply Qred_complete...
Qed.
Proof.
intros x y.
apply Cunit_eq.
Qed.
Lemma CRle_Qle : ∀ (x y:Q), inject_Q_CR x ≤ inject_Q_CR y ↔ (x ≤ y)%Q.
Proof.
split.
intros H.
destruct (Qlt_le_dec y x) as [X|X];[|assumption].
destruct (Qpos_lt_plus X) as [c Hc].
assert (Y:=(H ((1#2)*c)%Qpos)).
simpl in Y.
unfold Cap_raw in Y; simpl in Y.
rewrite → Qle_minus_iff in Y.
rewrite → Hc in Y.
autorewrite with QposElim in Y.
ring_simplify in Y.
elim (Qle_not_lt _ _ Y).
rewrite → Qlt_minus_iff.
ring_simplify.
apply Q.Qmult_lt_0_compat; auto with ×.
intros H e.
simpl.
unfold Cap_raw; simpl.
rewrite → Qle_minus_iff in H.
apply Qle_trans with (0%Q);[|assumption].
rewrite → Qle_minus_iff; ring_simplify.
apply Qpos_nonneg.
Qed.
Lemma CRplus_Qplus : ∀ (x y:Q), inject_Q_CR x + inject_Q_CR y == inject_Q_CR (x + y)%Q.
Proof.
intros x y e1 e2; apply ball_refl.
Qed.
Hint Rewrite <- CRplus_Qplus : toCRring.
Lemma CRopp_Qopp : ∀ (x:Q), - inject_Q_CR x == inject_Q_CR (- x)%Q.
Proof.
intros x e1 e2; apply ball_refl.
Qed.
Lemma CRminus_Qminus : ∀ (x y:Q), inject_Q_CR x - inject_Q_CR y == inject_Q_CR (x - y)%Q.
Proof.
intros x y e1 e2; apply ball_refl.
Qed.
Lemma CRmult_Qmult : ∀ (x y:Q), inject_Q_CR x × inject_Q_CR y == inject_Q_CR (x × y)%Q.
Proof.
intros x y.
rewrite → CRmult_scale.
intros e1 e2; apply ball_refl.
Qed.
Lemma Qap_CRap : ∀ (x y:Q), (~(x==y))%Q → (' x)><(' y).
Proof.
intros x y Hxy.
destruct (Q_dec x y) as [[H|H]|H]; try contradiction;
destruct (Qpos_lt_plus H) as [c Hc];[left|right]; ∃ c; abstract (rewrite → CRminus_Qminus;
rewrite → CRle_Qle; rewrite → Hc; ring_simplify; apply Qle_refl).
Defined.
Lemma CRinv_Qinv : ∀ (x:Q) x_, CRinvT (inject_Q_CR x) x_ == inject_Q_CR (/x)%Q.
Proof.
intros x [[c x_]|[c x_]];
[change (' c ≤ 0 + - 'x)%CR in x_|change (' c ≤ ' x + - 0)%CR in x_]; unfold CRinvT;
rewrite → CRopp_Qopp, CRplus_Qplus, CRle_Qle in x_; try rewrite → CRopp_Qopp;
rewrite → (@CRinv_pos_Qinv c).
rewrite → CRopp_Qopp.
rewrite → CReq_Qeq.
assert (¬x==0)%Q.
intros H.
rewrite → H in x_.
apply (Qle_not_lt _ _ x_).
apply Qpos_prf.
field.
intros X; apply H.
assumption.
rewrite → Qplus_0_l in x_.
assumption.
reflexivity.
rewrite → Qplus_0_r in x_.
assumption.
Qed.
Lemma inject_Q_product (l: list Q): (' cr_Product l) [=] cr_Product (map inject_Q_CR l).
Proof.
induction l.
reflexivity.
change (' (a × cr_Product l)%Q[=]cr_Product (map inject_Q_CR (a :: l))).
rewrite <- CRmult_Qmult.
rewrite IHl.
reflexivity.
Qed.
Lemma inject_Qred_ap (x y: Q): Qred x ≠ Qred y → ' x [#] ' y.
Proof with auto.
intro.
apply Qap_CRap.
intro.
apply H.
apply Qred_complete...
Qed.
Lemma CR_ring_theory :
@ring_theory CR 0 1 (ucFun2 CRplus_uc) CRmult
(fun (x y:CR) ⇒ (x + - y)) CRopp (@st_eq CR).
Proof.
split.
apply: cm_lft_unit_unfolded.
apply: cag_commutes_unfolded.
apply: plus_assoc_unfolded.
apply: one_mult.
apply: mult_commut_unfolded.
apply: mult_assoc_unfolded.
intros x y z;generalize z x y;apply: ring_distl_unfolded.
reflexivity.
apply: cg_minus_correct.
Qed.
Lemma inject_Q_strext : fun_strext inject_Q_CR.
Proof.
intros x y [Hxy|Hxy].
apply: Qlt_not_eq.
apply Qnot_le_lt.
intros H.
absurd ('y[<=]'x).
rewrite → leEq_def.
auto with ×.
rewrite → CRle_Qle.
auto.
apply ap_symmetric.
apply: Qlt_not_eq.
apply Qnot_le_lt.
intros H.
absurd ('x[<=]'y).
rewrite → leEq_def.
auto with ×.
rewrite → CRle_Qle.
auto.
Qed.
Definition inject_Q_csf := Build_CSetoid_fun _ _ _ inject_Q_strext.
Lemma inject_Q_hom : RingHom Q_as_CRing CRasCRing.
Proof.
∃ (inject_Q_csf).
apply: CRplus_Qplus.
intros x y.
apply eq_symmetric.
apply CRmult_Qmult.
apply eq_reflexive.
Defined.
Lemma CR_Q_ring_morphism :
ring_morph 0%CR 1%CR (ucFun2 CRplus_uc) CRmult
(fun x y ⇒ (x + - y)) CRopp (@st_eq CR)
(0%Q) (1%Q) Qplus Qmult Qminus Qopp Qeq_bool (inject_Q_CR).
Proof.
split; try reflexivity.
apply CRplus_Qplus.
apply CRminus_Qminus.
intros x y; rewrite → CRmult_Qmult; reflexivity.
apply CRopp_Qopp.
intros x y H.
rewrite → CReq_Qeq.
apply Qeq_bool_eq.
assumption.
Qed.
Ltac CRcst t :=
match t with
| (inject_Q_CR ?z) ⇒ Qcst z
| _ ⇒ NotConstant
end.
Ltac CRring_pre := autorewrite with toCRring.
Lemma CR_ring_eq_ext : ring_eq_ext (ucFun2 CRplus_uc) CRmult CRopp (@st_eq CR).
Proof.
split.
rapply ucFun2_wd.
rapply CRmult_wd.
rapply uc_wd.
Qed.
Add Ring CR_ring : CR_ring_theory (morphism CR_Q_ring_morphism, setoid (@st_isSetoid (@msp_is_setoid CR)) CR_ring_eq_ext, constants [CRcst], preprocess [CRring_pre]).
@ring_theory CR 0 1 (ucFun2 CRplus_uc) CRmult
(fun (x y:CR) ⇒ (x + - y)) CRopp (@st_eq CR).
Proof.
split.
apply: cm_lft_unit_unfolded.
apply: cag_commutes_unfolded.
apply: plus_assoc_unfolded.
apply: one_mult.
apply: mult_commut_unfolded.
apply: mult_assoc_unfolded.
intros x y z;generalize z x y;apply: ring_distl_unfolded.
reflexivity.
apply: cg_minus_correct.
Qed.
Lemma inject_Q_strext : fun_strext inject_Q_CR.
Proof.
intros x y [Hxy|Hxy].
apply: Qlt_not_eq.
apply Qnot_le_lt.
intros H.
absurd ('y[<=]'x).
rewrite → leEq_def.
auto with ×.
rewrite → CRle_Qle.
auto.
apply ap_symmetric.
apply: Qlt_not_eq.
apply Qnot_le_lt.
intros H.
absurd ('x[<=]'y).
rewrite → leEq_def.
auto with ×.
rewrite → CRle_Qle.
auto.
Qed.
Definition inject_Q_csf := Build_CSetoid_fun _ _ _ inject_Q_strext.
Lemma inject_Q_hom : RingHom Q_as_CRing CRasCRing.
Proof.
∃ (inject_Q_csf).
apply: CRplus_Qplus.
intros x y.
apply eq_symmetric.
apply CRmult_Qmult.
apply eq_reflexive.
Defined.
Lemma CR_Q_ring_morphism :
ring_morph 0%CR 1%CR (ucFun2 CRplus_uc) CRmult
(fun x y ⇒ (x + - y)) CRopp (@st_eq CR)
(0%Q) (1%Q) Qplus Qmult Qminus Qopp Qeq_bool (inject_Q_CR).
Proof.
split; try reflexivity.
apply CRplus_Qplus.
apply CRminus_Qminus.
intros x y; rewrite → CRmult_Qmult; reflexivity.
apply CRopp_Qopp.
intros x y H.
rewrite → CReq_Qeq.
apply Qeq_bool_eq.
assumption.
Qed.
Ltac CRcst t :=
match t with
| (inject_Q_CR ?z) ⇒ Qcst z
| _ ⇒ NotConstant
end.
Ltac CRring_pre := autorewrite with toCRring.
Lemma CR_ring_eq_ext : ring_eq_ext (ucFun2 CRplus_uc) CRmult CRopp (@st_eq CR).
Proof.
split.
rapply ucFun2_wd.
rapply CRmult_wd.
rapply uc_wd.
Qed.
Add Ring CR_ring : CR_ring_theory (morphism CR_Q_ring_morphism, setoid (@st_isSetoid (@msp_is_setoid CR)) CR_ring_eq_ext, constants [CRcst], preprocess [CRring_pre]).
Relationship between strict and nonstrict positivity
Lemma CRpos_nonNeg : ∀ x, CRpos x → CRnonNeg x.
Proof.
intros x [c Hx].
cut (0 ≤ x)%CR.
unfold CRle.
intros H.
assert (x == x - 0)%CR. ring. rewrite → H0.
assumption.
apply CRle_trans with (' c)%CR; auto with ×.
rewrite → CRle_Qle; auto with ×.
Qed.
Lemma CRneg_nonPos : ∀ x, CRneg x → CRnonPos x.
Proof.
intros x [c Hx].
cut (x ≤ 0)%CR.
unfold CRle.
intros H.
assert (0 - x == -x)%CR. ring. rewrite → H0 in H.
intros e.
rewrite <- (Qopp_involutive e).
rewrite <- (Qopp_involutive (approximate x e)).
apply Qopp_le_compat.
apply H.
apply CRle_trans with ('(-c)%Q)%CR; auto with ×.
rewrite → CRle_Qle; auto with ×.
Qed.
Proof.
intros x [c Hx].
cut (0 ≤ x)%CR.
unfold CRle.
intros H.
assert (x == x - 0)%CR. ring. rewrite → H0.
assumption.
apply CRle_trans with (' c)%CR; auto with ×.
rewrite → CRle_Qle; auto with ×.
Qed.
Lemma CRneg_nonPos : ∀ x, CRneg x → CRnonPos x.
Proof.
intros x [c Hx].
cut (x ≤ 0)%CR.
unfold CRle.
intros H.
assert (0 - x == -x)%CR. ring. rewrite → H0 in H.
intros e.
rewrite <- (Qopp_involutive e).
rewrite <- (Qopp_involutive (approximate x e)).
apply Qopp_le_compat.
apply H.
apply CRle_trans with ('(-c)%Q)%CR; auto with ×.
rewrite → CRle_Qle; auto with ×.
Qed.
Now that we have ring-ness, we can easily prove some auxiliary utility lemmas about operations on CR.
Ltac CRring_replace x y :=
assert (x == y) as CRring_replace_temp by ring;
rewrite CRring_replace_temp;
clear CRring_replace_temp.
Lemma CRle_opp (x y: CR): x ≤ y ↔ - y ≤ - x.
Proof.
unfold CRle. intros.
assert (- x - - y == y - x)%CR as E by ring.
rewrite E.
intuition.
Qed.
Lemma CRopp_opp (x: CR): (--x == x)%CR.
Proof. intros. ring. Qed.
Lemma CRplus_opp (x: CR): (x + - x == 0)%CR.
Proof. intros. ring. Qed.
Lemma CRopp_0: (-0 == 0)%CR.
Proof. intros. ring. Qed.
Lemma CRplus_0_l (x: CR): (0 + x == x)%CR.
Proof. intros. ring. Qed.
Lemma CRplus_0_r (x: CR): (x + 0 == x)%CR.
Proof. intros. ring. Qed.
Lemma approximate_CRplus (x y: CR) (e: Qpos):
approximate (x + y)%CR e = (approximate x ((1#2) × e)%Qpos + approximate y ((1#2) × e)%Qpos)%Q.
Proof. reflexivity. Qed.
Lemma CRnonNeg_CRplus (x y: CR): CRnonNeg x → CRnonNeg y → CRnonNeg (x + y)%CR.
Proof.
unfold CRnonNeg. intros. rewrite approximate_CRplus.
setoid_replace (- e)%Q with (- ((1#2)*e)%Qpos + - ((1#2)*e)%Qpos)%Q by (simpl; ring).
apply Qplus_le_compat; auto.
Qed.
Lemma CRplus_comm (x y: CR): x + y == y + x.
Proof. intros. ring. Qed.
Lemma CRplus_assoc (x y z: CR): x + (y + z) == (x + y) + z.
Proof. intros. ring. Qed.
Lemma CRplus_eq_l (z x y: CR): x == y ↔ x + z == y + z.
Proof with ring.
split; intro E. rewrite E...
rewrite <- (CRplus_0_r x), <- (CRplus_opp z), CRplus_assoc, E...
Qed.
Lemma CRplus_eq_r (z x y: CR): x == y ↔ z + x == z + y.
Proof. intros. do 2 rewrite (CRplus_comm z). apply CRplus_eq_l. Qed.
Lemma CRplus_le_r (x y z: CR): x ≤ y ↔ x+z ≤ y+z.
Proof.
unfold CRle. intros.
assert (y + z - (x + z) == y - x)%CR as E by ring. rewrite E.
intuition.
Qed.
Lemma CRplus_le_l x: ∀ y z : CR, x ≤ y ↔ z + x ≤ z + y.
Proof.
intros. rewrite (CRplus_le_r x y z), (CRplus_comm x), (CRplus_comm y). reflexivity.
Qed.
Lemma CRplus_le_compat (x x' y y': CR): x ≤ x' → y ≤ y' → x+y ≤ x'+y'.
Proof.
unfold CRle. intros.
assert (x' + y' - (x + y) == (x' - x) + (y' - y)) as E by ring. rewrite E.
apply CRnonNeg_CRplus; assumption.
Qed.
Lemma CRlt_irrefl (x: CR): x < x → False.
Proof with auto.
unfold CRltT.
intro.
assert (x - x == 0)%CR by ring.
intros.
generalize (CRpos_wd H0 H).
unfold CRpos.
intros.
destruct H1.
destruct x0.
simpl in c.
assert (x0 ≤ 0)%Q.
rewrite <- CRle_Qle...
apply Qlt_irrefl with 0%Q.
apply Qlt_le_trans with x0...
Qed.
Lemma in_CRball (r: Qpos) (x y : CR): x - ' r ≤ y ∧ y ≤ x + ' r ↔ ball r x y.
Proof with intuition.
intros.
cut (AbsSmall (' r) (x - y) ↔ (x - ' r ≤ y ∧ y ≤ x + ' r)).
pose proof (CRAbsSmall_ball x y r)...
unfold AbsSmall.
simpl.
setoid_replace (x - y ≤ ' r) with (x - ' r ≤ y).
setoid_replace (- ' r ≤ x - y) with (y ≤ x + ' r).
intuition.
rewrite (CRplus_le_r (- ' r) (x - y) ('r + y)).
assert (- ' r + (' r + y) == y) as E by ring. rewrite E.
assert (x - y + (' r + y) == x + ' r)%CR as F by ring. rewrite F...
rewrite (CRplus_le_r (x - y) (' r) (y - 'r)).
assert (x - y + (y - ' r) == x - ' r) as E by ring. rewrite E.
assert (' r + (y - ' r) == y) as F by ring. rewrite F...
Qed.
Lemma in_CRgball (r: Q) (x y: CR): x - ' r ≤ y ∧ y ≤ x + ' r ↔ gball r x y.
Proof with intuition.
unfold gball.
destruct Qdec_sign as [[?|?]|?].
intuition.
generalize (CRle_trans H0 H1).
rewrite <- CRplus_le_l.
rewrite CRopp_Qopp.
rewrite CRle_Qle.
clear H0 H1.
intros.
apply Qlt_irrefl with 0%Q.
apply Qlt_le_trans with (-r)%Q.
change (- 0 < - r)%Q.
apply Qopp_lt_compat...
apply Qle_trans with r...
rewrite <- in_CRball...
rewrite q, CRopp_Qopp, ?CRplus_0_r, CRle_def...
Qed.
Lemma CRgball_plus (x x' y y': CR) e1 e2:
gball e1 x x' → gball e2 y y' → gball (e1 + e2) (x + y)%CR (x' + y')%CR.
Proof with auto.
do 3 rewrite <- in_CRgball.
intros [A B] [C D].
CRring_replace (x + y - ' (e1 + e2)%Q) (x - ' e1 + (y - ' e2)).
CRring_replace (x + y + ' (e1 + e2)%Q) (x + ' e1 + (y + ' e2)).
split; apply CRplus_le_compat...
Qed.
Lemma Qlt_from_CRlt (a b: Q): (' a < ' b)%CR → (a < b)%Q.
Proof with auto.
unfold CRltT.
unfold CRpos.
intros [[e p] H].
revert H.
simpl.
rewrite CRminus_Qminus.
rewrite CRle_Qle.
intros.
apply Qlt_le_trans with (a + e)%Q.
rewrite <-(Qplus_0_r a) at 1.
apply Qplus_lt_r...
apply Q.Qplus_le_l with (-a)%Q.
ring_simplify.
rewrite Qplus_comm...
Qed.
Lemma CRlt_trans (x y z: CR): x < y → y < z → x < z.
Proof.
destruct CRisCOrdField.
destruct ax_less_strorder.
apply so_trans.
Qed.
Lemma CRle_lt_trans (x y z: CR): x ≤ y → y < z → x < z.
Proof with auto.
intros ? [e ?]. ∃ e.
apply CRle_trans with (z - y)%CR...
assert (z - x - (z - y) == y - x)%CR as E by ring.
unfold CRle.
rewrite E...
Qed.
Lemma CRlt_le_trans (x y z: CR): x < y → y ≤ z → x < z.
Proof with auto.
intros [e ?] ?. ∃ e.
apply CRle_trans with (y - x)%CR...
assert (z - x - (y - x) == z - y)%CR as E by ring.
unfold CRle.
rewrite E...
Qed.
Lemma CRlt_le_weak (x y: CR): (x < y → x ≤ y)%CR.
Proof. intros. apply CRpos_nonNeg. assumption. Qed.
Lemma lower_CRapproximation (x: CR) (e: Qpos): ' (approximate x e - e)%Q ≤ x.
Proof.
intros. rewrite <- CRminus_Qminus.
apply CRplus_le_r with ('e)%CR.
ring_simplify. rewrite CRplus_comm.
apply in_CRball, ball_approx_r.
Qed.
Lemma upper_CRapproximation (x: CR) (e: Qpos): x ≤ ' (approximate x e + e)%Q.
Proof.
intros. rewrite <- CRplus_Qplus.
apply CRplus_le_r with (-'e)%CR.
assert (' approximate x e + 'e - 'e == ' approximate x e)%CR as E by ring. rewrite E.
apply (in_CRball e x ('approximate x e)), ball_approx_r.
Qed.
Hint Immediate lower_CRapproximation upper_CRapproximation.
Lemma CRlt_Qmid (x y: CR): x < y → sigT (λ q: Q, x < 'q and 'q < y).
Proof with auto.
intros [q E].
set (quarter := ((1#4)*q)%Qpos).
∃ (quarter + (approximate x quarter + quarter))%Q.
split.
apply CRle_lt_trans with (' (0 + (approximate x quarter + quarter))%Q)%CR...
rewrite Qplus_0_l...
apply CRlt_Qlt.
apply Qplus_lt_l...
apply CRlt_le_trans with (x + 'q)%CR.
apply CRlt_le_trans with (' (approximate x quarter - quarter + q)%Q)%CR.
apply CRlt_Qlt.
setoid_replace (QposAsQ q) with (quarter + quarter + quarter + quarter)%Q.
ring_simplify.
apply Qplus_lt_l.
apply Qmult_lt_compat_r...
reflexivity.
simpl. ring.
rewrite <- CRplus_Qplus.
apply CRplus_le_compat...
apply CRle_refl.
apply CRplus_le_r with (-x)%CR.
CRring_replace (x + 'q - x) ('q)...
Qed.
Lemma CRle_not_lt (x y: CR): (x ≤ y)%CR ↔ Not (y < x)%CR.
Proof.
destruct CRisCOrdField.
simpl in def_leEq.
apply def_leEq.
Qed.
Lemma CRnonNeg_le_0 x: CRnonNeg x ↔ 0 ≤ x.
Proof.
unfold CRle.
assert (x - 0 == x)%CR as E by ring.
rewrite E.
intuition.
Qed.
Lemma CRnonNeg_0: CRnonNeg (0)%CR.
Proof.
unfold CRnonNeg. simpl. intros.
rewrite <- (Qopp_opp 0).
apply Qopp_le_compat.
change (0 ≤ e)%Q. auto.
Qed.
Hint Immediate CRnonNeg_0.
Definition CRle_lt_dec: ∀ x y, DN ((x ≤ y)%CR + (y < x)%CR).
Proof with auto.
intros.
apply (DN_fmap (@DN_decisionT (y < x)%CR)).
intros [A | B]...
left.
apply (leEq_def CRasCOrdField x y)...
Qed.
Definition CRle_dec: ∀ (x y: CR), DN ((x≤y)%CR + (y≤x)%CR).
Proof with auto.
intros. apply (DN_fmap (CRle_lt_dec x y)).
intros [A | B]...
right.
apply CRlt_le_weak...
Qed.
Lemma approximate_CRminus (x y: CR) (e: QposInf):
approximate (x - y)%CR e =
(approximate x (Qpos2QposInf (1 # 2) × e)%QposInf - approximate y (Qpos2QposInf (1 # 2) × e)%QposInf)%Q.
Proof. destruct e; reflexivity. Qed.
Lemma CRnonNeg_criterion (x: CR): (∀ q, (x ≤ ' q)%CR → 0 ≤ q)%Q → CRnonNeg x.
Proof with auto with qarith.
unfold CRle.
unfold CRnonNeg.
intros.
apply Q.Qplus_le_l with e.
ring_simplify.
apply H.
intros.
rewrite approximate_CRminus.
simpl.
cut (approximate x ((1 # 2) × e0)%Qpos - approximate x e ≤ e0 + e)%Q.
intros.
apply Q.Qplus_le_l with (e0 + approximate x ((1#2)*e0)%Qpos - approximate x e)%Q.
ring_simplify...
apply Qle_trans with (Qabs (approximate x ((1 # 2) × e0)%Qpos - approximate x e))%Q.
apply Qle_Qabs.
apply Qle_trans with (((1#2)*e0)%Qpos + e)%Q...
pose proof (regFun_prf x ((1#2)*e0)%Qpos e).
apply Qball_Qabs in H0...
apply Qplus_le_compat.
simpl.
rewrite <- (Qmult_1_r e0) at 2.
rewrite (Qmult_comm e0).
apply Qmult_le_compat_r...
apply Qle_refl.
Qed.
Lemma Qle_CRle_r (x y: CR): (∀ y', y ≤ ' y' → x ≤ ' y') ↔ x ≤ y.
Proof with auto.
split; intros. 2: apply CRle_trans with y...
apply from_DN.
apply (DN_bind (CRle_lt_dec x y)).
intros [?|W]. apply DN_return...
exfalso.
destruct (CRlt_Qmid _ _ W) as [w [A B]].
pose proof (H w (CRlt_le_weak _ _ A)).
apply (CRle_not_lt x ('w)%CR)...
Qed.
Lemma Qle_CRle_l (x y: CR): (∀ x', ' x' ≤ x → ' x' ≤ y) ↔ x ≤ y.
Proof with auto.
intros.
rewrite CRle_opp.
rewrite <- Qle_CRle_r.
split; intros.
rewrite CRle_opp, CRopp_opp, CRopp_Qopp.
apply H.
rewrite CRle_opp, CRopp_Qopp, Qopp_opp...
rewrite CRle_opp, CRopp_Qopp.
apply H.
rewrite CRle_opp, CRopp_Qopp, CRopp_opp, Qopp_opp...
Qed.
Lemma Qle_CRle (x y: CR): (∀ x' y', ' x' ≤ x → y ≤ ' y' → (x' ≤ y')%Q) ↔ x ≤ y.
Proof with auto.
split; intros.
apply (proj1 (Qle_CRle_l _ _)). intros.
apply (proj1 (Qle_CRle_r _ _)). intros.
apply CRle_Qle...
apply CRle_Qle.
apply CRle_trans with x...
apply CRle_trans with y...
Qed.
Lemma CRnonNegQpos : ∀ e : Qpos, CRnonNeg (' ` e).
Proof.
intros [e e_pos]; apply CRnonNeg_criterion; simpl.
intros q A; apply Qlt_le_weak, Qlt_le_trans with (y := e); trivial.
now apply CRle_Qle.
Qed.
Lemma scale_0 x: scale 0 x == 0.
Proof. rewrite <- CRmult_scale. ring. Qed.
Lemma scale_CRplus (q: Q) (x y: CR): scale q (x + y) == scale q x + scale q y.
Proof. intros. do 3 rewrite <- CRmult_scale. ring. Qed.
Lemma scale_CRopp (q: Q) (x: CR): scale q (-x) == - scale q x.
Proof. intros. do 2 rewrite <- CRmult_scale. ring. Qed.
This returs GT if x is clearly greater than e, returns LT if x
is clearly less than (-e), and returns Eq otherwise.
Definition CR_epsilon_sign_dec (e:Qpos) (x:CR) : comparison :=
let z := approximate x e in
match Q.Qle_dec ((2#1) × e) z with
| left p ⇒ Gt
| right _ ⇒
match Q.Qle_dec z (-(2#1) × e)%Q with
| left p ⇒ Datatypes.Lt
| right _ ⇒ Eq
end
end.
let z := approximate x e in
match Q.Qle_dec ((2#1) × e) z with
| left p ⇒ Gt
| right _ ⇒
match Q.Qle_dec z (-(2#1) × e)%Q with
| left p ⇒ Datatypes.Lt
| right _ ⇒ Eq
end
end.
This helper lemma reduces a CRpos problem to a sigma type with
a simple equality proposition.
Lemma CR_epsilon_sign_dec_pos : ∀ x,
{e:Qpos | CR_epsilon_sign_dec e x ≡ Gt} → CRpos x.
Proof.
intros x [e H].
apply (@CRpos_char e).
abstract (unfold CR_epsilon_sign_dec in H; destruct (Q.Qle_dec ((2#1) × e) (approximate x e)) as [A|A];
[assumption | destruct (Q.Qle_dec (approximate x e) (- (2#1) × e)) as [B|B]; discriminate H]).
Defined.
Lemma CR_epsilon_sign_dec_Gt (e:Qpos) (x:CR) :
((2#1) × e ≤ approximate x e)%Q → CR_epsilon_sign_dec e x ≡ Gt.
Proof.
intros.
unfold CR_epsilon_sign_dec.
destruct Q.Qle_dec; intuition.
Qed.
Lemma CR_epsilon_sign_dec_pos_rev (x : CR) (e : Qpos) :
('e ≤ x)%CR → CR_epsilon_sign_dec ((1#4) × e) x ≡ Gt.
Proof.
intros E.
apply CR_epsilon_sign_dec_Gt.
apply Qplus_le_l with (-e)%Q.
simpl. setoid_replace ((2#1) × ((1 # 4) × e) + - e)%Q with (-((1#2) × e))%Q by QposRing.
replace ((1#4) × e)%Qpos with ((1#2) × ((1#2) × e))%Qpos.
now apply (E ((1#2) × e))%Qpos.
apply Qpos_PI.
now destruct e as [[[ | | ] ?] ?].
Qed.
Close Scope CR_scope.
Local Opaque CR.
Instance: Ring CR.
Proof. apply (rings.from_stdlib_ring_theory CR_ring_theory). Qed.
Instance CRlt: Lt CR := λ x y,
∃ n : nat, CR_epsilon_sign_dec ((1#4) × (2#1) ^ -cast nat Z n) (y - x) ≡ Gt.
Lemma CR_lt_ltT x y : x < y IFF CRltT x y.
Proof.
split.
intros E.
apply CR_epsilon_sign_dec_pos.
apply constructive_indefinite_description_nat in E.
destruct E as [n En].
now ∃ ((1#4) × (2#1) ^ -cast nat Z n)%Qpos.
intros. now apply comparison_eq_dec.
intros [ε Eε].
∃ (Z.nat_of_Z (-Qdlog2 ('ε))).
apply CR_epsilon_sign_dec_pos_rev.
apply CRle_trans with ('(ε : Q)); auto.
apply CRle_Qle. simpl.
destruct (decide ((ε : Q) ≤ 1)).
rewrite Z.nat_of_Z_nonneg.
rewrite Zopp_involutive.
apply Qdlog2_spec.
now destruct ε.
apply Z.opp_nonneg_nonpos.
now apply Qdlog2_nonpos.
rewrite Z.nat_of_Z_nonpos.
now apply Qlt_le_weak, Qnot_le_lt.
apply Z.opp_nonpos_nonneg.
apply Qdlog2_nonneg.
now apply Qlt_le_weak, Qnot_le_lt.
Qed.
Instance CRapart: Apart CR := λ x y, x < y ∨ y < x.
Lemma CR_apart_apartT x y : x ≶ y IFF CRapartT x y.
Proof.
split.
intros E.
set (f (n : nat) := CR_epsilon_sign_dec ((1#4) × (2#1) ^ -cast nat Z n)).
assert (∃ n, f n (y - x) ≡ Gt ∨ f n (x - y) ≡ Gt) as E2.
now destruct E as [[n En] | [n En]]; ∃ n; [left | right].
apply constructive_indefinite_description_nat in E2.
destruct E2 as [n E2].
destruct (comparison_eq_dec (f n (y - x)) Gt) as [En|En].
left. apply CR_epsilon_sign_dec_pos.
now ∃ ((1#4) × (2#1) ^ -cast nat Z n)%Qpos.
right. apply CR_epsilon_sign_dec_pos.
∃ ((1#4) × (2#1) ^ -cast nat Z n)%Qpos.
destruct E2; tauto.
intros n.
destruct (comparison_eq_dec (f n (y - x)) Gt); auto.
destruct (comparison_eq_dec (f n (x - y)) Gt); tauto.
intros [E|E].
left. now apply CR_lt_ltT.
right. now apply CR_lt_ltT.
Qed.
Instance: StrongSetoid CR.
Proof with auto; try solve [now apply CR_apart_apartT].
split.
intros x E.
destruct (ap_irreflexive _ x)...
intros x y E.
apply CR_apart_apartT.
apply: ap_symmetric...
intros x y E z.
destruct (ap_cotransitive _ x y) with z; [|left|right]...
intros x y; split; intros E.
apply ap_tight. intros E2. destruct E...
intros E2. destruct (proj2 (ap_tight _ x y))...
Qed.
Instance: StrongSetoid_BinaryMorphism CRmult.
Proof with auto; try solve [now apply CR_apart_apartT].
split; try apply _.
intros x₁ y₁ x₂ y₂ E.
destruct (CRmult_strext x₁ x₂ y₁ y₂); [|left|right]...
Qed.
Instance: FullPseudoOrder CRle CRlt.
Proof with eauto; try solve [eapply CR_lt_ltT; eauto].
split.
split; try apply _.
intros x y [E1 E2].
destruct (less_antisymmetric_unfolded _ x y)...
intros x y E z.
edestruct (less_cotransitive _ x y); [| left | right]...
reflexivity.
intros x y; split.
intros E1 E2.
apply (leEq_def _ x y)...
intros E1. apply (leEq_def _ x y).
intros E2. destruct E1...
Qed.
Instance: FullPseudoSemiRingOrder CRle CRlt.
Proof with eauto; try solve [eapply CR_lt_ltT; eauto].
apply rings.from_full_pseudo_ring_order.
repeat (split; try apply _).
intros x y E.
apply CR_lt_ltT, (plus_resp_less_lft _ x y z)...
apply _.
intros x y E1 E2.
apply CR_lt_ltT, (mult_resp_pos _ x y)...
Qed.
Program Instance CRinv: Recip CR := λ x, CRinvT x _.
Next Obligation. apply CR_apart_apartT. now destruct x. Qed.
Instance: Field CR.
Proof.
split; try apply _.
apply CR_apart_apartT.
now apply: ring_non_triv.
split; try apply _.
intros [x Px] [y Py] E.
now apply: CRinvT_wd.
intros x.
now apply: field_mult_inv.
Qed.
Instance: StrongSetoid_Morphism inject_Q_CR.
Proof.
apply strong_setoids.dec_strong_morphism.
split; try apply _.
Qed.
Instance: StrongSemiRing_Morphism inject_Q_CR.
Proof.
repeat (split; try apply _); intros; try reflexivity; symmetry.
now apply CRplus_Qplus.
now apply CRmult_Qmult.
Qed.
Instance: StrongInjective inject_Q_CR.
Proof.
repeat (split; try apply _); intros.
apply CR_apart_apartT.
now apply: Qap_CRap.
Qed.
Instance: OrderEmbedding inject_Q_CR.
Proof. repeat (split; try apply _); now apply CRle_Qle. Qed.
Instance: StrictOrderEmbedding inject_Q_CR.
Proof. split; apply _. Qed.
{e:Qpos | CR_epsilon_sign_dec e x ≡ Gt} → CRpos x.
Proof.
intros x [e H].
apply (@CRpos_char e).
abstract (unfold CR_epsilon_sign_dec in H; destruct (Q.Qle_dec ((2#1) × e) (approximate x e)) as [A|A];
[assumption | destruct (Q.Qle_dec (approximate x e) (- (2#1) × e)) as [B|B]; discriminate H]).
Defined.
Lemma CR_epsilon_sign_dec_Gt (e:Qpos) (x:CR) :
((2#1) × e ≤ approximate x e)%Q → CR_epsilon_sign_dec e x ≡ Gt.
Proof.
intros.
unfold CR_epsilon_sign_dec.
destruct Q.Qle_dec; intuition.
Qed.
Lemma CR_epsilon_sign_dec_pos_rev (x : CR) (e : Qpos) :
('e ≤ x)%CR → CR_epsilon_sign_dec ((1#4) × e) x ≡ Gt.
Proof.
intros E.
apply CR_epsilon_sign_dec_Gt.
apply Qplus_le_l with (-e)%Q.
simpl. setoid_replace ((2#1) × ((1 # 4) × e) + - e)%Q with (-((1#2) × e))%Q by QposRing.
replace ((1#4) × e)%Qpos with ((1#2) × ((1#2) × e))%Qpos.
now apply (E ((1#2) × e))%Qpos.
apply Qpos_PI.
now destruct e as [[[ | | ] ?] ?].
Qed.
Close Scope CR_scope.
Local Opaque CR.
Instance: Ring CR.
Proof. apply (rings.from_stdlib_ring_theory CR_ring_theory). Qed.
Instance CRlt: Lt CR := λ x y,
∃ n : nat, CR_epsilon_sign_dec ((1#4) × (2#1) ^ -cast nat Z n) (y - x) ≡ Gt.
Lemma CR_lt_ltT x y : x < y IFF CRltT x y.
Proof.
split.
intros E.
apply CR_epsilon_sign_dec_pos.
apply constructive_indefinite_description_nat in E.
destruct E as [n En].
now ∃ ((1#4) × (2#1) ^ -cast nat Z n)%Qpos.
intros. now apply comparison_eq_dec.
intros [ε Eε].
∃ (Z.nat_of_Z (-Qdlog2 ('ε))).
apply CR_epsilon_sign_dec_pos_rev.
apply CRle_trans with ('(ε : Q)); auto.
apply CRle_Qle. simpl.
destruct (decide ((ε : Q) ≤ 1)).
rewrite Z.nat_of_Z_nonneg.
rewrite Zopp_involutive.
apply Qdlog2_spec.
now destruct ε.
apply Z.opp_nonneg_nonpos.
now apply Qdlog2_nonpos.
rewrite Z.nat_of_Z_nonpos.
now apply Qlt_le_weak, Qnot_le_lt.
apply Z.opp_nonpos_nonneg.
apply Qdlog2_nonneg.
now apply Qlt_le_weak, Qnot_le_lt.
Qed.
Instance CRapart: Apart CR := λ x y, x < y ∨ y < x.
Lemma CR_apart_apartT x y : x ≶ y IFF CRapartT x y.
Proof.
split.
intros E.
set (f (n : nat) := CR_epsilon_sign_dec ((1#4) × (2#1) ^ -cast nat Z n)).
assert (∃ n, f n (y - x) ≡ Gt ∨ f n (x - y) ≡ Gt) as E2.
now destruct E as [[n En] | [n En]]; ∃ n; [left | right].
apply constructive_indefinite_description_nat in E2.
destruct E2 as [n E2].
destruct (comparison_eq_dec (f n (y - x)) Gt) as [En|En].
left. apply CR_epsilon_sign_dec_pos.
now ∃ ((1#4) × (2#1) ^ -cast nat Z n)%Qpos.
right. apply CR_epsilon_sign_dec_pos.
∃ ((1#4) × (2#1) ^ -cast nat Z n)%Qpos.
destruct E2; tauto.
intros n.
destruct (comparison_eq_dec (f n (y - x)) Gt); auto.
destruct (comparison_eq_dec (f n (x - y)) Gt); tauto.
intros [E|E].
left. now apply CR_lt_ltT.
right. now apply CR_lt_ltT.
Qed.
Instance: StrongSetoid CR.
Proof with auto; try solve [now apply CR_apart_apartT].
split.
intros x E.
destruct (ap_irreflexive _ x)...
intros x y E.
apply CR_apart_apartT.
apply: ap_symmetric...
intros x y E z.
destruct (ap_cotransitive _ x y) with z; [|left|right]...
intros x y; split; intros E.
apply ap_tight. intros E2. destruct E...
intros E2. destruct (proj2 (ap_tight _ x y))...
Qed.
Instance: StrongSetoid_BinaryMorphism CRmult.
Proof with auto; try solve [now apply CR_apart_apartT].
split; try apply _.
intros x₁ y₁ x₂ y₂ E.
destruct (CRmult_strext x₁ x₂ y₁ y₂); [|left|right]...
Qed.
Instance: FullPseudoOrder CRle CRlt.
Proof with eauto; try solve [eapply CR_lt_ltT; eauto].
split.
split; try apply _.
intros x y [E1 E2].
destruct (less_antisymmetric_unfolded _ x y)...
intros x y E z.
edestruct (less_cotransitive _ x y); [| left | right]...
reflexivity.
intros x y; split.
intros E1 E2.
apply (leEq_def _ x y)...
intros E1. apply (leEq_def _ x y).
intros E2. destruct E1...
Qed.
Instance: FullPseudoSemiRingOrder CRle CRlt.
Proof with eauto; try solve [eapply CR_lt_ltT; eauto].
apply rings.from_full_pseudo_ring_order.
repeat (split; try apply _).
intros x y E.
apply CR_lt_ltT, (plus_resp_less_lft _ x y z)...
apply _.
intros x y E1 E2.
apply CR_lt_ltT, (mult_resp_pos _ x y)...
Qed.
Program Instance CRinv: Recip CR := λ x, CRinvT x _.
Next Obligation. apply CR_apart_apartT. now destruct x. Qed.
Instance: Field CR.
Proof.
split; try apply _.
apply CR_apart_apartT.
now apply: ring_non_triv.
split; try apply _.
intros [x Px] [y Py] E.
now apply: CRinvT_wd.
intros x.
now apply: field_mult_inv.
Qed.
Instance: StrongSetoid_Morphism inject_Q_CR.
Proof.
apply strong_setoids.dec_strong_morphism.
split; try apply _.
Qed.
Instance: StrongSemiRing_Morphism inject_Q_CR.
Proof.
repeat (split; try apply _); intros; try reflexivity; symmetry.
now apply CRplus_Qplus.
now apply CRmult_Qmult.
Qed.
Instance: StrongInjective inject_Q_CR.
Proof.
repeat (split; try apply _); intros.
apply CR_apart_apartT.
now apply: Qap_CRap.
Qed.
Instance: OrderEmbedding inject_Q_CR.
Proof. repeat (split; try apply _); now apply CRle_Qle. Qed.
Instance: StrictOrderEmbedding inject_Q_CR.
Proof. split; apply _. Qed.