1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/ordered_fields_ch0/".
18 include "ordered_sets2.ma".
20 (*CSC: non capisco questi alias! Una volta non servivano*)
21 alias id "plus" = "cic:/matita/groups/plus.con".
22 alias symbol "plus" = "Abelian group plus".
24 record pre_ordered_field_ch0: Type ≝
26 of_cotransitively_ordered_set_: cotransitively_ordered_set;
27 of_with: os_carrier of_cotransitively_ordered_set_ = carrier of_field
30 (*CSC: the following lemma (that is also a coercion) should be automatically
32 lemma of_cotransitively_ordered_set : pre_ordered_field_ch0 → cotransitively_ordered_set.
34 apply mk_cotransitively_ordered_set;
35 [ apply mk_ordered_set;
38 (eq_rect ? ? (λC:Type.C→C→Prop) (os_le (of_cotransitively_ordered_set_ F)) ? (of_with F))
40 (eq_rect' Type (os_carrier (of_cotransitively_ordered_set_ F))
41 (λa:Type.λH:os_carrier (of_cotransitively_ordered_set_ F)=a.
42 is_order_relation a (eq_rect Type (os_carrier (of_cotransitively_ordered_set_ F)) (λC:Type.C→C→Prop) (os_le (of_cotransitively_ordered_set_ F)) a H))
43 ? (Type_OF_pre_ordered_field_ch0 F) (of_with F));
45 apply (os_order_relation_properties (of_cotransitively_ordered_set_ F))
50 (λa:Type.λH:os_carrier (of_cotransitively_ordered_set_ F)=a.
54 λa2:Type.λH1:os_carrier (of_cotransitively_ordered_set_ F)=a2.
57 [refl_eq ⇒ os_le (of_cotransitively_ordered_set_ F)])
60 apply cos_cotransitive
64 coercion cic:/matita/ordered_fields_ch0/of_cotransitively_ordered_set.con.
66 record is_ordered_field_ch0 (F:pre_ordered_field_ch0) : Type \def
67 { of_mult_compat: ∀a,b:F. 0≤a → 0≤b → 0≤a*b;
68 of_plus_compat: ∀a,b,c:F. a≤b → a+c≤b+c;
69 of_weak_tricotomy : ∀a,b:F. a≠b → a≤b ∨ b≤a;
70 (* 0 characteristics *)
71 of_char0: ∀n. n > O → sum ? (plus F) 0 1 n ≠ 0
74 record ordered_field_ch0 : Type \def
75 { of_pre_ordered_field_ch0:> pre_ordered_field_ch0;
76 of_ordered_field_properties:> is_ordered_field_ch0 of_pre_ordered_field_ch0
79 lemma le_zero_x_to_le_opp_x_zero: ∀F:ordered_field_ch0.∀x:F.0 ≤ x → -x ≤ 0.
81 generalize in match (of_plus_compat ? F ? ? (-x) H); intro;
82 rewrite > zero_neutral in H1;
83 rewrite > plus_comm in H1;
84 rewrite > opp_inverse in H1;
88 lemma le_x_zero_to_le_zero_opp_x: ∀F:ordered_field_ch0.∀x:F. x ≤ 0 → 0 ≤ -x.
90 generalize in match (of_plus_compat ? F ? ? (-x) H); intro;
91 rewrite > zero_neutral in H1;
92 rewrite > plus_comm in H1;
93 rewrite > opp_inverse in H1;
98 lemma eq_opp_x_times_opp_one_x: ∀F:ordered_field_ch0.∀x:F.-x = -1*x.
101 lemma not_eq_x_zero_to_lt_zero_mult_x_x:
102 ∀F:ordered_field_ch0.∀x:F. x ≠ 0 → 0 < x * x.
104 elim (of_weak_tricotomy ? ? ? ? ? ? ? ? F ? ? H);
105 [ generalize in match (le_x_zero_to_le_zero_opp_x F ? H1); intro;
106 generalize in match (of_mult_compat ? ? ? ? ? ? ? ? F ? ? H2 H2); intro;
109 axiom lt_zero_to_lt_inv_zero:
110 ∀F:ordered_field_ch0.∀x:F.∀p:x≠0. lt F 0 x → lt F 0 (inv ? x p).
112 alias symbol "lt" = "natural 'less than'".
114 (* The ordering is not necessary. *)
115 axiom not_eq_sum_field_zero: ∀F:ordered_field_ch0.∀n. O<n → sum_field F n ≠ 0.
116 axiom le_zero_sum_field: ∀F:ordered_field_ch0.∀n. O<n → lt F 0 (sum_field F n).
118 axiom lt_zero_to_le_inv_zero:
119 ∀F:ordered_field_ch0.∀n:nat.∀p:sum_field F n ≠ 0. 0 ≤ inv ? (sum_field ? n) p.
121 definition tends_to : ∀F:ordered_field_ch0.∀f:nat→F.∀l:F.Prop.
123 (λF:ordered_field_ch0.λf:nat → F.λl:F.
124 ∀n:nat.∃m:nat.∀j:nat. le m j →
125 l - (inv F (sum_field ? (S n)) ?) ≤ f j ∧
126 f j ≤ l + (inv F (sum_field ? (S n)) ?));
127 apply not_eq_sum_field_zero;
133 definition is_cauchy_seq ≝
134 λF:ordered_field_ch0.λf:nat→F.
137 -eps ≤ f M - f n ∧ f M - f n ≤ eps.
142 definition is_cauchy_seq : ∀F:ordered_field_ch0.∀f:nat→F.Prop.
144 (λF:ordered_field_ch0.λf:nat→F.
147 -(inv ? (sum_field F (S m)) ?) ≤ f N - f n ∧
148 f N - f n ≤ inv ? (sum_field F (S m)) ?);
149 apply not_eq_sum_field_zero;
154 definition is_complete ≝
155 λF:ordered_field_ch0.
156 ∀f:nat→F. is_cauchy_seq ? f →
157 ex F (λl:F. tends_to ? f l).