(* $Id: Spec_CReals.v,v 1.26 2000/11/10 11:27:34 freek Exp $ *) (* file "CSetoids.v", line 6-14 *) Require Export Relations. (* file "CSetoids.v", line 21-95 *) Syntactic Definition Symmetric := (symmetric ?). Syntactic Definition Transitive := (transitive ?). Implicit Arguments On. Section Properties_of_relations. Variable A: Set. Definition irreflexive [R:(relation A)] : Prop := (x:A)(not(R x x)). Definition cotransitive [R:(relation A)] : Prop := (x,y:A)(R x y) -> (z:A)(R x z) \/ (R z y). Definition tight_apart [eq,R:(relation A)]: Prop := (x,y:A)(not(R x y)) <-> (eq x y). Definition antisymmetric [R:(relation A)] : Prop := (x,y: A)(R x y) -> (not(R y x)). End Properties_of_relations. Implicit Arguments Off. Record is_CSetoid [A:Set; eq,ap:(relation A)] : Prop := { ax_ap_irreflexive : (irreflexive ap); ax_ap_symmetric : (Symmetric ap); ax_ap_cotransitive : (cotransitive ap); ax_ap_tight : (tight_apart eq ap) }. Record CSetoid : Type := { cs_crr :> Set; cs_eq : (relation cs_crr); cs_ap : (relation cs_crr); cs_proof : (is_CSetoid cs_crr cs_eq cs_ap) }. Syntactic Definition Cs_eq := (cs_eq ?). Infix NONA 8 "[=]" Cs_eq. Syntax constr level 8: cs_eq_infix [<<(cs_eq $_ $e1 $e2)>>] -> [[ $e1:L [0 1] " [=] " $e2:L]]. (* file "CSetoids.v", line 114-120 *) Syntactic Definition Cs_ap := (cs_ap ?). Infix NONA 8 "[#]" Cs_ap. Syntax constr level 8: cs_ap_infix [<<(cs_ap $_ $e1 $e2)>>] -> [[ $e1:L [0 1] " [#] " $e2:L]]. (* file "CSetoids.v", line 139-181 *) Section CSetoid_axioms. Variable S : CSetoid. Lemma CSetoid_is_CSetoid : (is_CSetoid S (cs_eq S) (cs_ap S)). Proof (cs_proof S). Lemma ap_irreflexive : (irreflexive (cs_ap S)). Elim CSetoid_is_CSetoid. Intros. Assumption. Qed. Lemma ap_symmetric : (Symmetric (cs_ap S)). Elim CSetoid_is_CSetoid. Intros. Assumption. Qed. Lemma ap_cotransitive : (cotransitive (cs_ap S)). Elim CSetoid_is_CSetoid. Intros. Assumption. Qed. Lemma ap_tight : (tight_apart (cs_eq S) (cs_ap S)). Elim CSetoid_is_CSetoid. Intros. Assumption. Qed. End CSetoid_axioms. (* file "CSetoids.v", line 192-195 *) Section CSetoid_basics. Variable S : CSetoid. (* file "CSetoids.v", line 269-274 *) Lemma ap_irreflexive_unfolded : (x:S)(~(x[#]x)). Proof (ap_irreflexive S). (* file "CSetoids.v", line 368-370 *) End CSetoid_basics. (* file "CSetoids.v", line 385-405 *) Section CSetoid_relations_and_predicates. Variable S : CSetoid. (* file "CSetoids.v", line 438-456 *) Section CsetoidRelations. Variable R: S -> S -> Prop. Definition rel_well_def_rht: Prop := (x,y,z: S)(R x y) -> (y [=] z) -> (R x z). Definition rel_well_def_lft: Prop := (x,y,z: S)(R x y) -> (x [=] z) -> (R z y). Definition rel_strong_ext : Prop := (x1,x2,y1,y2 : S)(R x1 y1) -> (R x2 y2) \/ (x1 [#] x2) \/ (y1 [#] y2). (* file "CSetoids.v", line 517-535 *) End CsetoidRelations. Record CSetoid_relation : Type := { csr_rel :> S -> S -> Prop; csr_wdr : (rel_well_def_rht csr_rel); csr_wdl : (rel_well_def_lft csr_rel); csr_strext : (rel_strong_ext csr_rel) }. (* file "CSetoids.v", line 606-608 *) End CSetoid_relations_and_predicates. (* file "CSetoids.v", line 625-643 *) Section CSetoid_functions. Variables S1, S2, S3 : CSetoid. Section unary_functions. Variable f : S1 -> S2. Definition fun_well_def : Prop := (x, y: S1)(x [=] y) -> (f x) [=] (f y). Definition fun_strong_ext : Prop := (x, y: S1)((f x) [#] (f y)) -> x [#] y. (* file "CSetoids.v", line 660-670 *) End unary_functions. Record CSetoid_fun : Set := { csf_fun :> S1 -> S2; csf_wd : (fun_well_def csf_fun); csf_strext : (fun_strong_ext csf_fun) }. (* file "CSetoids.v", line 684-703 *) Section binary_functions. Variable f : S1 -> S2 -> S3. Definition bin_fun_well_def : Prop := (x1, x2: S1)(y1, y2: S2) (x1 [=] x2) -> (y1 [=] y2) -> (f x1 y1) [=] (f x2 y2). Definition bin_fun_strong_ext : Prop := (x1, x2: S1)(y1, y2: S2) ((f x1 y1) [#] (f x2 y2)) -> (x1 [#] x2) \/ (y1 [#] y2). (* file "CSetoids.v", line 723-736 *) End binary_functions. Record CSetoid_bin_fun : Set := { csbf_fun :> S1 -> S2 -> S3; csbf_wd : (bin_fun_well_def csbf_fun); csbf_strext : (bin_fun_strong_ext csbf_fun) }. End CSetoid_functions. (* file "CSetoids.v", line 769-807 *) Section csetoid_inner_ops. Variable S : CSetoid. Definition commutes [f:S->S->S] : Prop := (x,y: S)(f x y) [=] (f y x). Definition associative [f:S->S->S]: Prop := (x,y,z:S)(f x (f y z)) [=] (f (f x y) z). Definition un_op_well_def := (fun_well_def S S). Definition un_op_strong_ext := (fun_strong_ext S S). Definition CSetoid_un_op : Set := (CSetoid_fun S S). Definition Build_CSetoid_un_op := (Build_CSetoid_fun S S). (* file "CSetoids.v", line 834-838 *) Definition un_op_strext := (csf_strext S S). (* file "CSetoids.v", line 863-868 *) Definition CSetoid_bin_op : Set := (CSetoid_bin_fun S S S). Definition Build_CSetoid_bin_op := (Build_CSetoid_bin_fun S S S). (* file "CSetoids.v", line 877-879 *) Identity Coercion bin_op_bin_fun: CSetoid_bin_op >-> CSetoid_bin_fun. (* file "CSetoids.v", line 954-956 *) End csetoid_inner_ops. (* file "CSetoids.v", line 962-964 *) Syntactic Definition Associative := (associative ?). (* file "CSetoids.v", line 1044-1079 *) Section SubCSetoids. Variable S : CSetoid. Variable P : S -> Prop. Record subcsetoid_crr : Set := { scs_elem :> S; scs_prf : (P scs_elem) }. Definition restrict_relation [R:(relation S)]: (relation subcsetoid_crr) := [a, b: subcsetoid_crr] Cases a b of (Build_subcsetoid_crr x _) (Build_subcsetoid_crr y _) => (R x y) end. Definition subcsetoid_eq: (relation subcsetoid_crr) := (restrict_relation (cs_eq S)). Definition subcsetoid_ap: (relation subcsetoid_crr) := (restrict_relation (cs_ap S)). (* file "CSetoids.v", line 1106-1130 *) Lemma subcsetoid_is_CSetoid : (is_CSetoid ? subcsetoid_eq subcsetoid_ap). Apply (Build_is_CSetoid ? subcsetoid_eq subcsetoid_ap). (* irreflexive *) Red; Intros. Case x. Unfold not; Intros. Exact (ap_irreflexive_unfolded S ? H). (* symmetric *) Red; Intros x y. Case x. Case y. Intros. Exact (ap_symmetric S ? ? H). (* cotransitive *) Red; Intros x y. Case x. Case y. Intros; Case z. Intros. Exact (ap_cotransitive S ?? H scs_elem2). (* tight *) Red; Intros. Case x. Case y. Intros. Exact (ap_tight S scs_elem1 scs_elem0). Qed. Definition Build_SubCSetoid : CSetoid := (Build_CSetoid subcsetoid_crr subcsetoid_eq subcsetoid_ap subcsetoid_is_CSetoid). (* file "CSetoids.v", line 1243-1245 *) End SubCSetoids. (* file "CSemiGroups.v", line 28-77 *) Definition is_CSemi_grp [A:CSetoid; unit: A; op:(CSetoid_bin_op A)] := (Associative op). Record CSemi_grp : Type := { csg_crr :> CSetoid; csg_unit : csg_crr; (* non-empty *) csg_op : (CSetoid_bin_op csg_crr); csg_proof : (is_CSemi_grp csg_crr csg_unit csg_op) }. Syntactic Definition Zero := (csg_unit ?). Syntax constr level 1: csg_unit_constant [<<(csg_unit $e0)>>] -> ["Zero"]. Syntactic Definition Csg_op := (csg_op ?). Infix 7 "[+]" Csg_op. Syntax constr level 7: csg_op_infix [<<(csbf_fun $_ $_ $_ (csg_op $_) $e1 $e2)>>] -> [[ $e1:E [0 1] "[+]" $e2:L]]. (* file "CSemiGroups.v", line 106-115 *) Section CSemi_grp_basics. Variable G : CSemi_grp. (* file "CSemiGroups.v", line 126-139 *) Definition nonZeroP [x:G] : Prop := (x [#] Zero). End CSemi_grp_basics. Syntactic Definition NonZeroP := (nonZeroP ?). (* file "CMonoids.v", line 6-21 *) Definition is_rht_unit [S: CSetoid; op: (CSetoid_bin_op S); one: S] : Prop := (x: S)((op x one) [=] x). (* file "CMonoids.v", line 34-47 *) Record is_CMonoid [G: CSemi_grp]: Prop := { runit : (is_rht_unit G Csg_op Zero); commut: (commutes G Csg_op) }. Record CMonoid : Type := { cm_crr :> CSemi_grp; cm_proof : (is_CMonoid cm_crr) }. (* file "CMonoids.v", line 150-166 *) Lemma is_CMonoid_proof_irr : (S:CSetoid)(one:S)(mult:(CSetoid_bin_op S))(p,q:(Associative mult)) (is_CMonoid (Build_CSemi_grp S one mult p)) -> (is_CMonoid (Build_CSemi_grp S one mult q)). Intros. Elim H; Intros. Simpl in runit0. Simpl in commut0. Apply Build_is_CMonoid; Simpl; Assumption. Qed. (* file "CGroups.v", line 6-33 *) Definition is_inverse [S:CSetoid; op:(CSetoid_bin_op S); one:S; x:S; x_inv:S] : Prop := ((op x x_inv) [=] one). Syntactic Definition Is_inverse := (is_inverse ?). Definition is_CGroup [G: CMonoid; inv: (CSetoid_un_op G)] := (x: G)(Is_inverse Csg_op Zero x (inv x)). Record CGroup : Type := { cg_crr :> CMonoid; cg_inv : (CSetoid_un_op cg_crr); cg_proof : (is_CGroup cg_crr cg_inv) }. (* file "CGroups.v", line 37-69 *) Syntactic Definition Cg_inv := (cg_inv ?). Grammar command command1 := Cg_inv_prefix [ "[--]" command1($c) ] -> [<<(Cg_inv $c)>>]. Syntax constr level 1: cg_inv_prefix [<<(csf_fun $_ $_ (cg_inv $_) $e1)>>] -> [[ "[--]" $e1:L]]. Definition cg_minus := [G: CGroup][x, y: G](x [+] [--]y). Syntactic Definition Cg_minus := (cg_minus ?). Infix NONA 7 "[-]" Cg_minus. Syntax constr level 7: cg_minus_infix [<<(cg_minus $_ $e1 $e2)>>] -> [[ $e1:E [0 1] "[-]" $e2:L]]. (* file "CRings.v", line 11-64 *) (* Constructive RINGS *) Definition distributive := [S:CSetoid; mult,plus:(CSetoid_bin_op S)] (x,y,z:S) (mult x (plus y z)) [=] (plus (mult x y) (mult x z)). Syntactic Definition Distributive := (distributive ?). Record is_CRing [G : CGroup; one : G; mult : (CSetoid_bin_op G)] : Prop := { ax_mult_assoc : (Associative mult); ax_mult_mon : (is_CMonoid (Build_CSemi_grp G one mult ax_mult_assoc)); ax_dist : (Distributive mult (csg_op G)); ax_non_triv : (one [#] Zero) }. Record CRing : Type := { cr_crr :> CGroup; cr_one : cr_crr; cr_mult : (CSetoid_bin_op cr_crr); cr_proof : (is_CRing cr_crr cr_one cr_mult) }. Definition cr_plus := csg_op. Definition cr_inv := cg_inv. Definition cr_minus := cg_minus. Syntactic Definition Cr_mult := (cr_mult ?). Syntactic Definition One := (cr_one ?). Syntax constr level 1: cr_one_constant [<<(cr_one $e0)>>] -> ["One"]. (* file "CRings.v", line 70-117 *) Infix 6 "[*]" Cr_mult. Syntax constr level 6: cr_mult_infix [<<(csbf_fun $_ $_ $_ (cr_mult $_) $e1 $e2)>>] -> [[ $e1:E [0 1] "[*]" $e2:L]]. Section CRing_axioms. Variable R : CRing. Lemma CRing_is_CRing : (is_CRing R One Cr_mult). Elim R; Intros. Exact cr_proof0. Qed. Lemma mult_assoc : (Associative (cr_mult R)). Elim CRing_is_CRing; Intros. Assumption. Qed. Lemma mult_mon : (is_CMonoid (Build_CSemi_grp R One Cr_mult mult_assoc)). Elim (cr_proof R). Intros. Apply is_CMonoid_proof_irr with ax_mult_assoc0. Assumption. Qed. (* file "CRings.v", line 162-188 *) End CRing_axioms. Section Ring_constructions. Variable R : CRing. Definition Build_multCMonoid : CMonoid := (Build_CMonoid ? (mult_mon R)). Definition NonZeros : CSetoid := (Build_SubCSetoid R NonZeroP). Definition nzinj : NonZeros -> R := (scs_elem R NonZeroP). (* file "CRings.v", line 273-275 *) End Ring_constructions. (* file "CRings.v", line 281-283 *) Syntactic Definition NZinj := (nzinj ?). (* file "CRings.v", line 495-510 *) Section exponentiation. Variable R: CRing. (* file "CRings.v", line 544-546 *) End exponentiation. (* file "CRings.v", line 564-582 *) Section nat_injection. Variable R: CRing. Fixpoint nring [m:nat]: R := Cases m of O => Zero | (S n) => ((nring n) [+] One) end. (* file "CRings.v", line 611-613 *) End nat_injection. (* file "CRings.v", line 626-628 *) Syntactic Definition Nring := (nring ?). (* file "CFields.v", line 48-67 *) (* FIELDS *) Definition is_CField [R: CRing; cf_rcpcl: (CSetoid_un_op (NonZeros R))] : Prop := (x: (NonZeros R))(Is_inverse (cr_mult R) One (NZinj x) (NZinj (cf_rcpcl x))). Record CField : Type := { cf_crr :> CRing; cf_rcpcl : (CSetoid_un_op (NonZeros cf_crr)); cf_proof : (is_CField cf_crr cf_rcpcl) }. (* file "COrdFields.v", line 16-73 *) Implicit Arguments On. Record strictorder [A:Set; R: A->A->Prop] : Prop := { so_trans : (Transitive R); so_asym : (antisymmetric R) }. Implicit Arguments Off. Record is_COrdField [F: CField; less : (CSetoid_relation F)] : Prop := {ax_less_strorder : (strictorder less); ax_plus_resp_less: (x,y:F)(less x y) -> (z:F)(less (x[+]z) (y[+]z)); ax_mult_resp_pos : (x,y:F)(less Zero x)->(less Zero y)->(less Zero (x[*]y)); ax_less_conf_ap : (x,y:F)(x [#] y) <-> ((less x y) \/ (less y x)) }. Record COrdField : Type := {cof_crr :> CField; cof_less : (CSetoid_relation cof_crr); cof_proof : (is_COrdField cof_crr cof_less) }. Syntactic Definition Less := (cof_less ?). Infix NONA 8 "[:<]" Less. Syntax constr level 8: less_infix [<<(csr_rel $_ (cof_less $_) $e1 $e2)>>] -> [[ $e1:L [0 1] " [:<] " $e2:L]]. Definition greater := [F:COrdField; x,y : F] y[:<]x. Syntactic Definition Greater := (greater ?). Infix NONA 8 "[:>]" Greater. Syntax constr level 8: greater_infix [<<(greater $_ $e1 $e2)>>] -> [[ $e1:L [0 1] " [:>] " $e2:L]]. (* file "COrdFields.v", line 2156-2162 *) Definition absSmall [R:COrdField;e,x:R]: Prop := ([--]e [:<] x) /\ (x [:<] e). Syntactic Definition AbsSmall := (absSmall ?). (* file "COrdFields.v", line 2718-2759 *) Section OrdField_Cauchy. Variable R : COrdField. Implicit Arguments On. Definition Cauchy_prop [g:nat -> R]: Prop := (e:R)(Zero [:<] e) -> (Ex [N:nat](m:nat)(le N m) -> (AbsSmall e ((g m)[-](g N)))). Implicit Arguments Off. (* Def. CauchyP, Build_CauchyP *) (* Should be defined in terms of CauchyP *) (* Implicit arguments turned off, because Coq makes a mess of it in combination with the coercions *) Record CauchySeq : Set := {CS_seq :> nat -> R; CS_proof: (Cauchy_prop CS_seq) }. Definition seqLimit [seq:nat->R; lim:R]: Prop := (e:R)(Zero [:<] e) -> (Ex [N:nat](m:nat)(le N m) -> (AbsSmall e ((seq m)[-]lim))). End OrdField_Cauchy. Syntactic Definition SeqLimit := (seqLimit ?). (* file "CReals.v", line 11-26 *) Record is_CReals [R: COrdField; lim : (CauchySeq R) -> R] : Prop := {ax_Lim : (s:(CauchySeq R))(SeqLimit s (lim s)); ax_Arch : (x:R)(Ex [n:nat](x [:<] (Nring n))) }. Record CReals : Type := {crl_crr :> COrdField; crl_lim : (CauchySeq crl_crr) -> crl_crr; crl_proof : (is_CReals crl_crr crl_lim) }.