Isomorphism between CR and Cauchy_IR

In prove that CR is a real number structure, we must climb the algebraic heirarchy. The easiest way of doing this is to construct an isomorphism between Cauchy_IR and CR because they are similar strucutres. Then we can leverage the proofs that Cauchy_IR is a real number structure.

CR to Cauchy_IR


Definition CRasCauchy_IR_raw (x:CR) (n:nat) := approximate x (1 # P_of_succ_nat n)%Qpos.

Lemma CRasCauchy_IR_raw_is_Cauchy : forall (x:CR),
Cauchy_prop (R:=Q_as_COrdField) (CRasCauchy_IR_raw x).

Definition CRasCauchy_IR (x:CR) : Cauchy_IR :=
Build_CauchySeq _ _ (CRasCauchy_IR_raw_is_Cauchy x).

Lemma CRasCauchy_IR_wd : forall (x y:CR), (x==y)%CR -> CRasCauchy_IR x[=]CRasCauchy_IR y.

Cauchy_IR to CR


Definition Cauchy_IRasCR_raw (x:Cauchy_IR) (e:QposInf) : Q.
Defined.

Lemma Cauchy_IRasCR_is_Regular : forall (x:Cauchy_IR),
is_RegularFunction (Cauchy_IRasCR_raw x).

Definition Cauchy_IRasCR (x:Cauchy_IR) : CR :=
Build_RegularFunction (Cauchy_IRasCR_is_Regular x).

Lemma Cauchy_IRasCR_wd : forall (x y:Cauchy_IR), x[=]y -> (Cauchy_IRasCR x==Cauchy_IRasCR y)%CR.

Composition is the identity
Lemma CRasCR : forall x:CR, (Cauchy_IRasCR (CRasCauchy_IR x)==x)%CR.

Lemma Cauchy_IRasCauchy_IR : forall x:Cauchy_IR, CRasCauchy_IR (Cauchy_IRasCR x)[=]x.

Equalities are well defined.
Lemma Cauchy_IR_eq_as_CR_eq : forall (x y:Cauchy_IR),
((Cauchy_IRasCR x) == (Cauchy_IRasCR y))%CR <-> x[=]y.

Lemma CR_eq_as_Cauchy_IR_eq : forall (x y:CR),
(CRasCauchy_IR x [=] CRasCauchy_IR y) <-> (x==y)%CR.

Functions preserved by isomorphism.

Lemma reverse_iso_wd_fun : forall
(f:Cauchy_IR -> Cauchy_IR)
(g:CR -> CR),
(forall x y, (x==y -> g x == g y)%CR) ->
(forall (x:Cauchy_IR),
(g (Cauchy_IRasCR x) == Cauchy_IRasCR (f x))%CR) ->
forall (x:CR),
(f (CRasCauchy_IR x) [=] CRasCauchy_IR (g x)).

Lemma reverse_iso_uc_fun : forall
(f:Cauchy_IR -> Cauchy_IR)
(g:CR --> CR),
(forall (x:Cauchy_IR),
(g (Cauchy_IRasCR x) == Cauchy_IRasCR (f x))%CR) ->
forall (x:CR),
(f (CRasCauchy_IR x) [=] CRasCauchy_IR (g x)).

Lemma reverse_iso_bin_wd_fun : forall
(f:Cauchy_IR -> Cauchy_IR -> Cauchy_IR)
(g:CR -> CR -> CR),
(forall w x, (w == x)%CR -> forall y z, (y == z -> g w y == g x z)%CR) ->
(forall (x y:Cauchy_IR),
(g (Cauchy_IRasCR x) (Cauchy_IRasCR y) == Cauchy_IRasCR (f x y))%CR) ->
forall (x y:CR),
(f (CRasCauchy_IR x) (CRasCauchy_IR y) [=] CRasCauchy_IR (g x y)).

Lemma reverse_iso_bin_uc_fun : forall
(f:Cauchy_IR -> Cauchy_IR -> Cauchy_IR)
(g:CR --> CR --> CR),
(forall (x y:Cauchy_IR),
(g (Cauchy_IRasCR x) (Cauchy_IRasCR y) == Cauchy_IRasCR (f x y))%CR) ->
forall (x y:CR),
(f (CRasCauchy_IR x) (CRasCauchy_IR y) [=] CRasCauchy_IR (g x y)).

injection of rationals is preserved.
Lemma Cauchy_IR_inject_Q_as_CR_inject_Q : forall x:Q,
(' x == Cauchy_IRasCR (Cauchy_CReals.inject_Q _ x))%CR.


Lemma CR_inject_Q_as_Cauchy_IR_inject_Q : forall x:Q,
Cauchy_CReals.inject_Q _ x [=] CRasCauchy_IR (' x)%CR.

plus is preserved.
Lemma Cauchy_IR_plus_as_CR_plus : forall x y:Cauchy_IR,
(Cauchy_IRasCR x + Cauchy_IRasCR y == Cauchy_IRasCR (x[+]y))%CR.


Lemma CR_plus_as_Cauchy_IR_plus : forall x y:CR,
CRasCauchy_IR x [+] CRasCauchy_IR y [=] CRasCauchy_IR (x+y)%CR.

opp is preserved.
Lemma Cauchy_IR_opp_as_CR_opp : forall x:Cauchy_IR,
(-Cauchy_IRasCR x == Cauchy_IRasCR ([--]x))%CR.


Lemma CR_opp_as_Cauchy_IR_opp : forall x:CR,
[--](CRasCauchy_IR x) [=] CRasCauchy_IR (- x)%CR.

le is preserved.
Lemma Cauchy_IR_le_as_CR_le : forall (x y:Cauchy_IR),
(Cauchy_IRasCR x <= Cauchy_IRasCR y)%CR <-> x[<=]y.


Lemma CR_le_as_Cauchy_IR_le : forall (x y:CR),
CRasCauchy_IR x[<=]CRasCauchy_IR y <-> (x<=y)%CR.

mult is preserved.
Lemma Cauchy_IR_mult_as_CRmult_bounded : forall x y:Cauchy_IR,
forall (z:Qpos) (N:nat), (forall i:nat, (N<=i) -> AbsSmall (z:Q) (CS_seq _ y i)) ->
(ucFun2 (CRmult_bounded z) (Cauchy_IRasCR x) (Cauchy_IRasCR y) == Cauchy_IRasCR (x[*]y))%CR.

Lemma AbsSmall_Qabs : forall x y, (Qabs y <= x)%Q <-> AbsSmall x y.

Lemma Cauchy_IR_mult_as_CR_mult : forall x y:Cauchy_IR,
((Cauchy_IRasCR x)*(Cauchy_IRasCR y) == Cauchy_IRasCR (x[*]y))%CR.


Lemma CR_mult_as_Cauchy_IR_mult : forall x y:CR,
(CRasCauchy_IR x)[*](CRasCauchy_IR y) [=] CRasCauchy_IR (x*y)%CR.

lt is preserved.
Lemma Cauchy_IR_lt_as_CR_lt_1 : forall (x y:Cauchy_IR),
x[<]y -> (Cauchy_IRasCR x < Cauchy_IRasCR y)%CR.

Lemma CR_lt_as_Cauchy_IR_lt_1 : forall (x y:CR),
(x < y)%CR -> (CRasCauchy_IR x)[<](CRasCauchy_IR y).

Lemma Cauchy_IR_lt_as_CR_lt_2 : forall (x y:Cauchy_IR),
((Cauchy_IRasCR x) < (Cauchy_IRasCR y))%CR -> x[<]y.

Lemma CR_lt_as_Cauchy_IR_lt_2 : forall (x y:CR),
(CRasCauchy_IR x)[<](CRasCauchy_IR y) -> (x < y)%CR.

appartness is preserved.
Lemma Cauchy_IR_ap_as_CR_ap_1 : forall (x y:Cauchy_IR),
x[#]y -> (CRapart (Cauchy_IRasCR x) (Cauchy_IRasCR y))%CR.

Lemma CR_ap_as_Cauchy_IR_ap_1 : forall (x y:CR),
CRapart x y -> (CRasCauchy_IR x) [#] (CRasCauchy_IR y).

Lemma Cauchy_IR_ap_as_CR_ap_2 : forall (x y:Cauchy_IR),
(CRapart (Cauchy_IRasCR x) (Cauchy_IRasCR y))%CR -> x[#]y.

Lemma CR_ap_as_Cauchy_IR_ap_2 : forall (x y:CR),
(CRasCauchy_IR x) [#] (CRasCauchy_IR y) -> CRapart x y.

inv is preserved.
Lemma Cauchy_IR_inv_as_CRinv_pos : forall (x:Cauchy_IR) x_,
forall (z:Qpos) (N:nat), (forall i:nat, (N<=i) -> (z <= (CS_seq _ x i))%Q) ->
(CRinv_pos z (Cauchy_IRasCR x) == Cauchy_IRasCR (f_rcpcl x (Cinright _ _ x_)))%CR.

Lemma Cauchy_IR_nonZero_as_CR_nonZero_1 : forall (x:Cauchy_IR),
Dom (f_rcpcl' _) x -> (CRapart (Cauchy_IRasCR x) (inject_Q 0%Q))%CR.

Lemma CR_nonZero_as_Cauchy_IR_nonZero_1 : forall (x:CR),
(CRapart x (inject_Q 0%Q))%CR -> Dom (f_rcpcl' _) (CRasCauchy_IR x).

Lemma Cauchy_IR_inv_as_CR_inv_short : forall (x:Cauchy_IR) x_,
(@CRinv (Cauchy_IRasCR x) (Cauchy_IR_nonZero_as_CR_nonZero_1 _ x_) == Cauchy_IRasCR (f_rcpcl x x_))%CR.


Lemma Cauchy_IR_inv_as_CR_inv : forall (x:Cauchy_IR) x_ H,
(@CRinv (Cauchy_IRasCR x) H == Cauchy_IRasCR (f_rcpcl x x_))%CR.

Lemma CR_inv_as_Cauchy_IR_inv : forall (x:CR) x_ H,
f_rcpcl (CRasCauchy_IR x) H [=] CRasCauchy_IR (@CRinv x x_).

Lemma CR_inv_as_Cauchy_IR_inv_short : forall (x:CR) x_,
f_rcpcl (CRasCauchy_IR x) (CR_nonZero_as_Cauchy_IR_nonZero_1 _ x_) [=] CRasCauchy_IR (@CRinv x x_).