set "baseuri" "cic:/matita/ordered_fields_ch0/".
include "fields.ma".
-include "ordered_sets2.ma".
+include "ordered_groups.ma".
(*CSC: non capisco questi alias! Una volta non servivano*)
alias id "plus" = "cic:/matita/groups/plus.con".
record pre_ordered_field_ch0: Type ≝
{ of_field:> field;
+ of_ordered_abelian_group_: ordered_abelian_group;
of_cotransitively_ordered_set_: cotransitively_ordered_set;
- of_with: os_carrier of_cotransitively_ordered_set_ = carrier of_field
+ of_with1_:
+ cos_ordered_set of_cotransitively_ordered_set_ =
+ og_ordered_set of_ordered_abelian_group_;
+ of_with2:
+ og_abelian_group of_ordered_abelian_group_ = r_abelian_group of_field
}.
-(*CSC: the following lemma (that is also a coercion) should be automatically
- generated *)
+lemma of_ordered_abelian_group: pre_ordered_field_ch0 → ordered_abelian_group.
+ intro F;
+ apply mk_ordered_abelian_group;
+ [ apply mk_pre_ordered_abelian_group;
+ [ apply (r_abelian_group F)
+ | apply (og_ordered_set (of_ordered_abelian_group_ F))
+ | apply (eq_f ? ? carrier);
+ apply (of_with2 F)
+ ]
+ |
+ apply
+ (eq_rect' ? ?
+ (λG:abelian_group.λH:og_abelian_group (of_ordered_abelian_group_ F)=G.
+ is_ordered_abelian_group
+ (mk_pre_ordered_abelian_group G (of_ordered_abelian_group_ F)
+ (eq_f abelian_group Type carrier (of_ordered_abelian_group_ F) G
+ H)))
+ ? ? (of_with2 F));
+ simplify;
+ apply (og_ordered_abelian_group_properties (of_ordered_abelian_group_ F))
+ ]
+qed.
+
+coercion cic:/matita/ordered_fields_ch0/of_ordered_abelian_group.con.
+
+(*CSC: I am not able to prove this since unfold is undone by coercion composition*)
+axiom of_with1:
+ ∀G:pre_ordered_field_ch0.
+ cos_ordered_set (of_cotransitively_ordered_set_ G) =
+ og_ordered_set (of_ordered_abelian_group G).
+
lemma of_cotransitively_ordered_set : pre_ordered_field_ch0 → cotransitively_ordered_set.
intro F;
apply mk_cotransitively_ordered_set;
- [ apply mk_ordered_set;
- [ apply (carrier F)
- | apply
- (eq_rect ? ? (λC:Type.C→C→Prop) (os_le (of_cotransitively_ordered_set_ F)) ? (of_with F))
- | apply
- (eq_rect' Type (os_carrier (of_cotransitively_ordered_set_ F))
- (λa:Type.λH:os_carrier (of_cotransitively_ordered_set_ F)=a.
- 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))
- ? (Type_OF_pre_ordered_field_ch0 F) (of_with F));
- simplify;
- apply (os_order_relation_properties (of_cotransitively_ordered_set_ F))
- ]
- | simplify;
- apply
- (eq_rect' ? ?
- (λa:Type.λH:os_carrier (of_cotransitively_ordered_set_ F)=a.
- cotransitive a
- match H in eq
- return
- λa2:Type.λH1:os_carrier (of_cotransitively_ordered_set_ F)=a2.
- a2→a2→Prop
- with
- [refl_eq ⇒ os_le (of_cotransitively_ordered_set_ F)])
- ? ? (of_with F));
- simplify;
+ [ apply (og_ordered_set F)
+ | apply
+ (eq_rect ? ? (λa:ordered_set.cotransitive (os_carrier a) (os_le a))
+ ? ? (of_with1 F));
apply cos_cotransitive
- ].
+ ]
qed.
coercion cic:/matita/ordered_fields_ch0/of_cotransitively_ordered_set.con.
record is_ordered_field_ch0 (F:pre_ordered_field_ch0) : Type \def
{ of_mult_compat: ∀a,b:F. 0≤a → 0≤b → 0≤a*b;
- of_plus_compat: ∀a,b,c:F. a≤b → a+c≤b+c;
of_weak_tricotomy : ∀a,b:F. a≠b → a≤b ∨ b≤a;
(* 0 characteristics *)
of_char0: ∀n. n > O → sum ? (plus F) 0 1 n ≠ 0
of_ordered_field_properties:> is_ordered_field_ch0 of_pre_ordered_field_ch0
}.
-lemma le_zero_x_to_le_opp_x_zero: ∀F:ordered_field_ch0.∀x:F.0 ≤ x → -x ≤ 0.
- intros;
- generalize in match (of_plus_compat ? F ? ? (-x) H); intro;
- rewrite > zero_neutral in H1;
- rewrite > plus_comm in H1;
- rewrite > opp_inverse in H1;
- assumption.
-qed.
-
-lemma le_x_zero_to_le_zero_opp_x: ∀F:ordered_field_ch0.∀x:F. x ≤ 0 → 0 ≤ -x.
- intros;
- generalize in match (of_plus_compat ? F ? ? (-x) H); intro;
- rewrite > zero_neutral in H1;
- rewrite > plus_comm in H1;
- rewrite > opp_inverse in H1;
- assumption.
-qed.
-
(*
lemma eq_opp_x_times_opp_one_x: ∀F:ordered_field_ch0.∀x:F.-x = -1*x.
intros;
f j ≤ l + (inv F (sum_field ? (S n)) ?));
apply not_eq_sum_field_zero;
unfold;
- auto new.
+ autobatch.
qed.
(*
f N - f n ≤ inv ? (sum_field F (S m)) ?);
apply not_eq_sum_field_zero;
unfold;
- auto.
+ autobatch.
qed.
definition is_complete ≝