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.
  rewriteQle_minus_iff in Y.
  rewriteHc in Y.
  autorewrite with QposElim in Y.
  ring_simplify in Y.
  elim (Qle_not_lt _ _ Y).
  rewriteQlt_minus_iff.
  ring_simplify.
  apply Q.Qmult_lt_0_compat; auto with ×.
 intros H e.
 simpl.
 unfold Cap_raw; simpl.
 rewriteQle_minus_iff in H.
 apply Qle_trans with (0%Q);[|assumption].
 rewriteQle_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.
 rewriteCRmult_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 (rewriteCRminus_Qminus;
     rewriteCRle_Qle; rewriteHc; 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;
     rewriteCRopp_Qopp, CRplus_Qplus, CRle_Qle in x_; try rewriteCRopp_Qopp;
       rewrite → (@CRinv_pos_Qinv c).
    rewriteCRopp_Qopp.
    rewriteCReq_Qeq.
    assert (¬x==0)%Q.
     intros H.
     rewriteH in x_.
     apply (Qle_not_lt _ _ x_).
     apply Qpos_prf.
    field.
    intros X; apply H.
    assumption.
   rewriteQplus_0_l in x_.
   assumption.
  reflexivity.
 rewriteQplus_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.

Ring

CR forms a ring for the ring tactic.
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).
   rewriteleEq_def.
   auto with ×.
  rewriteCRle_Qle.
  auto.
 apply ap_symmetric.
 apply: Qlt_not_eq.
 apply Qnot_le_lt.
 intros H.
 absurd ('x[<=]'y).
  rewriteleEq_def.
  auto with ×.
 rewriteCRle_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; rewriteCRmult_Qmult; reflexivity.
  apply CRopp_Qopp.
 intros x y H.
 rewriteCReq_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 xCRnonNeg x.
Proof.
 intros x [c Hx].
 cut (0 x)%CR.
  unfold CRle.
  intros H.
  assert (x == x - 0)%CR. ring. rewriteH0.
  assumption.
 apply CRle_trans with (' c)%CR; auto with ×.
 rewriteCRle_Qle; auto with ×.
Qed.

Lemma CRneg_nonPos : x, CRneg xCRnonPos x.
Proof.
 intros x [c Hx].
 cut (x 0)%CR.
  unfold CRle.
  intros H.
  assert (0 - x == -x)%CR. ring. rewriteH0 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 ×.
 rewriteCRle_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 xCRnonNeg yCRnonNeg (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 < xFalse.
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 < yy < zx < z.
Proof.
 destruct CRisCOrdField.
 destruct ax_less_strorder.
 apply so_trans.
Qed.

Lemma CRle_lt_trans (x y z: CR): x yy < zx < 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 < yy zx < 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 < yx 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 < ysigT (λ 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 ((xy)%CR + (yx)%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)%QCRnonNeg 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' xy ' 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 pGt
 | right _
  match Q.Qle_dec z (-(2#1) × e)%Q with
  | left pDatatypes.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)%QCR_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)%CRCR_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 [ε ].
   (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.