Coq Real Numbers and IR isomorphisms

Warning: The Coq real numbers depend on classical logic. Importing this module will give you classical logic, the axioms of Coq's real number structure, plus all the logical consquences of these axioms. To avoid these consequences, use CoRN's real number structure IR instead.

All real number structures are isomorphic. This module uses this isomorphis to create a rewrite database RtoIR for converting many problems over R into problems over IR where constructive methods may be employed.

The isomorphism

Lemma RIR_iso : Isomorphism RReals IR.

Definition RasIR : R -> IR := iso_map_lft _ _ RIR_iso.
Definition IRasR : IR -> R := iso_map_rht _ _ RIR_iso.

Lemma RasIRasR_id : forall (x:R), (IRasR (RasIR x)=x).

Lemma IRasRasIR_id : forall (x:IR), (RasIR (IRasR x)[=]x).

equality

Lemma R_eq_as_IR : forall x y, (x = y -> RasIR x [=] RasIR y).

apartness

Lemma R_eq_as_IR_back : forall x y, (RasIR x [=] RasIR y -> x = y).

Lemma R_ap_as_IR : forall x y, (RasIR x [#] RasIR y -> x <> y).

Lemma R_ap_as_IR_back : forall x y, (x <> y -> RasIR x [#] RasIR y).

Lemma IR_ap_as_R : forall x y, (x <> y -> RasIR x [#] RasIR y).

less-than

Lemma R_lt_as_IR : forall x y, (RasIR x [<] RasIR y -> x < y).

Lemma R_lt_as_IR_back : forall x y, (x [<] y -> IRasR x < IRasR y).

Lemma IR_lt_as_R : forall x y, (x < y -> RasIR x [<] RasIR y).

Lemma IR_lt_as_R_back : forall x y, (IRasR x < IRasR y -> x [<] y).

Lemma R_le_as_IR : forall x y, (RasIR x [<=] RasIR y -> x <= y).

Lemma IR_le_as_R : forall x y, (x <= y -> RasIR x [<=] RasIR y).

Lemma IR_le_as_R_back : forall x y, (IRasR x <= IRasR y -> x [<=] y).

zero

Lemma R_Zero_as_IR : (RasIR R0 [=] 0).

Lemma IR_Zero_as_R : (IRasR 0 = 0).

one

Lemma R_One_as_IR : (RasIR R1 [=] 1).

Lemma IR_One_as_R : (IRasR 1 = R1).

addition

Lemma R_plus_as_IR : forall x y, (RasIR (x+y) [=] RasIR x [+] RasIR y).

Lemma IR_plus_as_R : forall x y, (IRasR (x[+]y) [=] IRasR x + IRasR y).

negation

Lemma R_opp_as_IR : forall x, (RasIR (- x) [=] ([--] (RasIR x))).

subtraction

Lemma R_minus_as_IR : forall x y, (RasIR (x-y) [=] RasIR x [-] RasIR y).

multiplication

Lemma R_mult_as_IR : forall x y, (RasIR (x*y) [=] RasIR x [*] RasIR y).

reciprocal

Lemma R_recip_as_IR : forall y Hy, (RasIR (1 / y) [=] (1 [/] RasIR y [//] Hy)).

division

Lemma R_div_as_IR : forall x y Hy, (RasIR (x/y) [=] (RasIR x [/] RasIR y [//] Hy)).

absolute value

Lemma R_abs_as_IR : forall x, RasIR (Rabs x) [=] AbsIR (RasIR x).

parital sum

Lemma R_sum_as_IR : forall a m,
RasIR (sum_f_R0 a m) [=] (∑ⁿ (fun i : N => RasIR (a i)) (S m)).

infinite sum

Lemma R_infsum_as_IR_convergent : forall (y: R) a,
  infinit_sum a y -> convergent (fun i : N => RasIR (a i)).

Lemma R_infsum_as_IR : forall (y: R) a,
  Rfunctions.infinit_sum a y -> forall prf,
  RasIR y [=] ∑₀^∞ (fun i : N => RasIR (a i)) prf.

Lemma R_infsum_f_as_IR : forall (x y: R) f,
  Rfunctions.infinit_sum (f x) y -> forall prf,
  RasIR y [=] ∑₀^∞ (fun i : N => RasIR (f x i)) prf.

factorial

Lemma fac_fact : forall i, fac i = fact i.

Lemma R_nring_as_IR : forall i, RasIR (nring i) [=] nring i.

exponents

Lemma R_pow_as_IR : forall x i,
RasIR (Rpow_def.pow x i)[=] nexp _ i (RasIR x).

Lemma R_exp_as_IR : forall x, RasIR (exp x) [=] Exp (RasIR x).

trigonometry

Lemma R_cos_as_IR : forall x, RasIR (cos x) [=] Cos (RasIR x).

Lemma R_sin_as_IR : forall x, RasIR (sin x) [=] Sin (RasIR x).

Lemma R_tan_as_IR : forall x dom, RasIR (tan x) [=] Tan (RasIR x) dom.

Add Morphism RasIR with signature (@cs_eq _) ==> (@cs_eq _) as R_as_IR_wd.
Qed.

logarithm

Lemma R_ln_as_IR : forall x prf, RasIR (ln x) [=] Log (RasIR x) prf.

integers

Lemma R_pring_as_IR : forall x, RasIR (pring _ x) [=] pring _ x.

Lemma R_zring_as_IR : forall x, RasIR (zring x) [=] zring x.

Lemma INR_as_nring : forall x, INR x = nring (R:=RRing) x.

Lemma IZR_as_zring : forall x, IZR x = zring (R:=RRing) x.

Lemma R_IZR_as_IR : forall x, RasIR (IZR x) [=] zring x.

Lemma R_pi_as_IR : RasIR (PI) [=] π.

Lemma R_pi_alt_as_IR : RasIR (PI) [=] pi.

rationals

Lemma R_Q2R_as_IR : forall q, RasIR (Q2R q) [=] inj_Q IR q.