Isomorphism between CR and IR
Because CR and IR are both real number structures, they are isomorphic. This module develops lemmas for translating between expressions over CR and IR. A rewrite database IRtoCR contains rewrite lemmas for converting expressions over IR to expressions over CR.
Lemma CRIR_iso : Isomorphism CRasCReals IR.
Definition CRasIR : CR -> IR := iso_map_lft _ _ CRIR_iso.
Definition IRasCR : IR -> CR := iso_map_rht _ _ CRIR_iso.
Lemma CRasIRasCR_id : forall (x:CR), (IRasCR (CRasIR x)==x)%CR.
Lemma IRasCRasIR_id : forall (x:IR), (CRasIR (IRasCR x)[=]x).
Lemma IRasCR_wd : forall x y, x[=]y -> (IRasCR x == IRasCR y)%CR.
Lemma IR_eq_as_CR : forall x y, x[=]y <-> (IRasCR x == IRasCR y)%CR.
Lemma CRasIR_wd : forall x y, (x==y)%CR -> CRasIR x [=] CRasIR y.
Lemma CR_less_as_IR : forall x y, (IRasCR x < IRasCR y -> x[<]y)%CR.
Lemma CR_ap_as_IR : forall x y, (IRasCR x >< IRasCR y -> x[#]y)%CR.
Lemma IR_leEq_as_CR : forall x y, x[<=]y <-> (IRasCR x <= IRasCR y)%CR.
Lemma IR_Zero_as_CR : (IRasCR 0=='0)%CR.
Lemma CR_ap_zero_as_IR : forall x, (IRasCR x >< '0 -> x[#]0)%CR.
Lemma IR_plus_as_CR : forall x y,
(IRasCR (x[+]y)== IRasCR x + IRasCR y)%CR.
Lemma IR_Sum0_as_CR : forall m x,
(IRasCR (∑0 m x)==Sum0 m (fun n => IRasCR (x n)))%CR.
Lemma IR_opp_as_CR : forall x,
(IRasCR ([--]x)== - IRasCR x)%CR.
Lemma IR_minus_as_CR : forall x y,
(IRasCR (x[-]y)== IRasCR x - IRasCR y)%CR.
Lemma IR_One_as_CR : (IRasCR 1=='1)%CR.
Lemma IR_mult_as_CR : forall x y,
(IRasCR (x[*]y)==(IRasCR x * IRasCR y))%CR.
Lemma IR_div_as_CR : forall x y y_ y__,
(IRasCR (x[/]y[//]y_)==(IRasCR x[/]IRasCR y[//]y__))%CR.
Lemma IR_div_as_CR_1 :forall x y y_,
(IRasCR (x[/]y[//]y_)==(IRasCR x[/]IRasCR y[//](map_pres_ap_zero _ _ (iso_map_rht _ _ CRIR_iso) y y_)))%CR.
Lemma IR_div_as_CR_2 :forall x y y_,
(IRasCR (x[/]y[//](CR_ap_zero_as_IR _ y_))==(IRasCR x[/]IRasCR y[//]y_))%CR.
Lemma IR_recip_as_CR :forall y y_ y__,
(IRasCR (1[/]y[//]y_)==(CRinv (IRasCR y) y__))%CR.
Lemma IR_recip_as_CR_1 :forall y y_,
(IRasCR (1[/]y[//]y_)==(CRinv (IRasCR y) (map_pres_ap_zero _ _ (iso_map_rht _ _ CRIR_iso) y y_)))%CR.
Lemma IR_recip_as_CR_2 :forall y y_,
(IRasCR (1[/]y[//](CR_ap_zero_as_IR _ y_))==(CRinv (IRasCR y) y_))%CR.
Lemma IR_nring_as_CR : forall n,
(IRasCR (nring n)==ms_id (nring n))%CR.
Lemma IR_pring_as_CR : forall p,
(IRasCR (pring _ p)==ms_id (pring _ p))%CR.
Lemma IR_zring_as_CR : forall z,
(IRasCR (zring z)==ms_id (zring z))%CR.
Lemma IR_inj_Q_as_CR : forall (a:Q), (IRasCR (inj_Q IR a)==('a))%CR.
Lemma IR_Cauchy_prop_as_CR : forall (x:CauchySeq IR),
(Cauchy_prop (fun n => (IRasCR (x n)))).
Lemma IR_Lim_as_CR : forall (x:CauchySeq IR),
(IRasCR (Lim x)==Lim (Build_CauchySeq _ _ (IR_Cauchy_prop_as_CR x)))%CR.
Lemma IR_AbsSmall_as_CR : forall (x y:IR),
AbsSmall x y <-> AbsSmall (R:=CRasCOrdField) (IRasCR x) (IRasCR y).
Definition CRasIR : CR -> IR := iso_map_lft _ _ CRIR_iso.
Definition IRasCR : IR -> CR := iso_map_rht _ _ CRIR_iso.
Lemma CRasIRasCR_id : forall (x:CR), (IRasCR (CRasIR x)==x)%CR.
Lemma IRasCRasIR_id : forall (x:IR), (CRasIR (IRasCR x)[=]x).
Lemma IRasCR_wd : forall x y, x[=]y -> (IRasCR x == IRasCR y)%CR.
Lemma IR_eq_as_CR : forall x y, x[=]y <-> (IRasCR x == IRasCR y)%CR.
Lemma CRasIR_wd : forall x y, (x==y)%CR -> CRasIR x [=] CRasIR y.
Lemma CR_less_as_IR : forall x y, (IRasCR x < IRasCR y -> x[<]y)%CR.
Lemma CR_ap_as_IR : forall x y, (IRasCR x >< IRasCR y -> x[#]y)%CR.
Lemma IR_leEq_as_CR : forall x y, x[<=]y <-> (IRasCR x <= IRasCR y)%CR.
Lemma IR_Zero_as_CR : (IRasCR 0=='0)%CR.
Lemma CR_ap_zero_as_IR : forall x, (IRasCR x >< '0 -> x[#]0)%CR.
Lemma IR_plus_as_CR : forall x y,
(IRasCR (x[+]y)== IRasCR x + IRasCR y)%CR.
Lemma IR_Sum0_as_CR : forall m x,
(IRasCR (∑0 m x)==Sum0 m (fun n => IRasCR (x n)))%CR.
Lemma IR_opp_as_CR : forall x,
(IRasCR ([--]x)== - IRasCR x)%CR.
Lemma IR_minus_as_CR : forall x y,
(IRasCR (x[-]y)== IRasCR x - IRasCR y)%CR.
Lemma IR_One_as_CR : (IRasCR 1=='1)%CR.
Lemma IR_mult_as_CR : forall x y,
(IRasCR (x[*]y)==(IRasCR x * IRasCR y))%CR.
Lemma IR_div_as_CR : forall x y y_ y__,
(IRasCR (x[/]y[//]y_)==(IRasCR x[/]IRasCR y[//]y__))%CR.
Lemma IR_div_as_CR_1 :forall x y y_,
(IRasCR (x[/]y[//]y_)==(IRasCR x[/]IRasCR y[//](map_pres_ap_zero _ _ (iso_map_rht _ _ CRIR_iso) y y_)))%CR.
Lemma IR_div_as_CR_2 :forall x y y_,
(IRasCR (x[/]y[//](CR_ap_zero_as_IR _ y_))==(IRasCR x[/]IRasCR y[//]y_))%CR.
Lemma IR_recip_as_CR :forall y y_ y__,
(IRasCR (1[/]y[//]y_)==(CRinv (IRasCR y) y__))%CR.
Lemma IR_recip_as_CR_1 :forall y y_,
(IRasCR (1[/]y[//]y_)==(CRinv (IRasCR y) (map_pres_ap_zero _ _ (iso_map_rht _ _ CRIR_iso) y y_)))%CR.
Lemma IR_recip_as_CR_2 :forall y y_,
(IRasCR (1[/]y[//](CR_ap_zero_as_IR _ y_))==(CRinv (IRasCR y) y_))%CR.
Lemma IR_nring_as_CR : forall n,
(IRasCR (nring n)==ms_id (nring n))%CR.
Lemma IR_pring_as_CR : forall p,
(IRasCR (pring _ p)==ms_id (pring _ p))%CR.
Lemma IR_zring_as_CR : forall z,
(IRasCR (zring z)==ms_id (zring z))%CR.
Lemma IR_inj_Q_as_CR : forall (a:Q), (IRasCR (inj_Q IR a)==('a))%CR.
Lemma IR_Cauchy_prop_as_CR : forall (x:CauchySeq IR),
(Cauchy_prop (fun n => (IRasCR (x n)))).
Lemma IR_Lim_as_CR : forall (x:CauchySeq IR),
(IRasCR (Lim x)==Lim (Build_CauchySeq _ _ (IR_Cauchy_prop_as_CR x)))%CR.
Lemma IR_AbsSmall_as_CR : forall (x y:IR),
AbsSmall x y <-> AbsSmall (R:=CRasCOrdField) (IRasCR x) (IRasCR y).