Coq Real Numbers
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.
Here we show that the real numbers from the Coq standard library form a real number structure. This is done in the usual way by building up the algebraic heirarchy.
Lemma R_is_CSetoid: is_CSetoid R (@eq R) (fun x y : R => x <> y).
Definition RCSetoid : CSetoid := Build_CSetoid R (@eq R) (fun x y => x <> y) R_is_CSetoid.
Canonical Structure RCSetoid.
Canonical Structure RSetoid := cs_crr RCSetoid.
addition
Lemma RPlus_is_setoid_bin_fun: bin_fun_strext RCSetoid RCSetoid RCSetoid Rplus.
Definition RPlus_sbinfun : CSetoid_bin_op RCSetoid := Build_CSetoid_bin_op RCSetoid Rplus RPlus_is_setoid_bin_fun.
Lemma R_is_CSemiGroup : is_CSemiGroup RCSetoid RPlus_sbinfun.
Definition RSemiGroup : CSemiGroup := Build_CSemiGroup RCSetoid RPlus_sbinfun R_is_CSemiGroup.
Canonical Structure RSemiGroup.
Lemma R_is_CMonoid : is_CMonoid RSemiGroup (0%R).
Definition RMonoid : CMonoid := Build_CMonoid _ _ R_is_CMonoid.
Canonical Structure RMonoid.
negation
Lemma RNeg_sunop : fun_strext (S1:=RCSetoid) (S2:=RCSetoid) Ropp.
Definition RNeg_op : CSetoid_un_op RMonoid := Build_CSetoid_un_op RCSetoid Ropp RNeg_sunop.
Lemma R_is_Group : is_CGroup RMonoid RNeg_op.
Definition RGroup := Build_CGroup _ _ R_is_Group.
Canonical Structure RGroup.
Lemma R_is_AbGroup : is_CAbGroup RGroup.
Definition RAbGroup := Build_CAbGroup _ R_is_AbGroup.
Canonical Structure RAbGroup.
multiplication
Lemma RMul_is_csbinop : bin_fun_strext RCSetoid RCSetoid RCSetoid Rmult.
Definition RMul_op : CSetoid_bin_op RMonoid := Build_CSetoid_bin_op RCSetoid Rmult RMul_is_csbinop.
Lemma RMul_assoc : associative (S:=RAbGroup) RMul_op.
Lemma R_is_Ring : is_CRing RAbGroup (1%R) RMul_op.
Definition RRing := Build_CRing _ _ _ R_is_Ring.
Canonical Structure RRing.
reciprocal
Definition Rrecip : forall x : RRing, x [#] 0 -> RRing := fun x _ => Rinv x.
Lemma R_is_Field : is_CField RRing Rrecip.
Lemma R_is_Field2: forall (x y : RRing) (x_ : x[#]0) (y_ : y[#]0),
Rrecip x x_[#]Rrecip y y_ -> x[#]y.
Definition RField : CField := Build_CField _ _ R_is_Field R_is_Field2.
Canonical Structure RField.
less-than
Lemma Rlt_strext : Crel_strext RField Rlt.
Definition Rless_rel : CCSetoid_relation RField := Build_CCSetoid_relation RField Rlt Rlt_strext.
greater-than
Lemma Rgt_strext : Crel_strext RField Rgt.
Definition Rgt_rel : CCSetoid_relation RField := Build_CCSetoid_relation RField Rgt Rgt_strext.
Lemma R_is_OrdField : is_COrdField RField Rless_rel Rle Rgt_rel Rge.
Definition ROrdField : COrdField := Build_COrdField _ _ _ _ _ R_is_OrdField.
Canonical Structure ROrdField.
Lemma cauchy_prop_cauchy_crit : (CauchySeq ROrdField) ->
forall s : (N -> ROrdField), (Cauchy_prop (R:=ROrdField) s) -> (Rseries.Cauchy_crit s).
limit
INR is isomorphic to nring