From 29c3bd75aca1d38a35702f2a923ff32ce958b4f2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 2 Jan 2007 20:05:21 +0000 Subject: [PATCH] There used to be two minimal joins between an ordered_set and an abelian_group: ordered_field_ch0 and riesz_space. To avoid the problem without introducing backtracking in unification I have introduced ordered_abelian_groups. An ordered_field_ch0 is recast as a field that is also an ordered_abelian_group and a cotransitively_ordered_set. I still have to recast riesz_spaces as vector spaces that are also ordered_abelian_groups and lattices. --- .../matita/dama/ordered_fields_ch0.ma | 92 +++++++++---------- helm/software/matita/dama/ordered_groups.ma | 71 ++++++++++++++ 2 files changed, 114 insertions(+), 49 deletions(-) create mode 100644 helm/software/matita/dama/ordered_groups.ma diff --git a/helm/software/matita/dama/ordered_fields_ch0.ma b/helm/software/matita/dama/ordered_fields_ch0.ma index 1c3b0fe7c..191137933 100644 --- a/helm/software/matita/dama/ordered_fields_ch0.ma +++ b/helm/software/matita/dama/ordered_fields_ch0.ma @@ -15,7 +15,7 @@ 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". @@ -23,49 +23,61 @@ alias symbol "plus" = "Abelian group plus". 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 @@ -76,24 +88,6 @@ record ordered_field_ch0 : Type \def 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; diff --git a/helm/software/matita/dama/ordered_groups.ma b/helm/software/matita/dama/ordered_groups.ma new file mode 100644 index 000000000..a9912d43f --- /dev/null +++ b/helm/software/matita/dama/ordered_groups.ma @@ -0,0 +1,71 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/ordered_groups/". + +include "groups.ma". +include "ordered_sets2.ma". + +record pre_ordered_abelian_group : Type ≝ + { og_abelian_group:> abelian_group; + og_ordered_set_: ordered_set; + og_with: os_carrier og_ordered_set_ = og_abelian_group + }. + +lemma og_ordered_set: pre_ordered_abelian_group → ordered_set. + intro G; + apply mk_ordered_set; + [ apply (carrier (og_abelian_group G)) + | apply (eq_rect ? ? (λC:Type.C→C→Prop) ? ? (og_with G)); + apply os_le + | apply + (eq_rect' ? ? + (λa:Type.λH:os_carrier (og_ordered_set_ G) = a. + is_order_relation a + (eq_rect Type (og_ordered_set_ G) (λC:Type.C→C→Prop) + (os_le (og_ordered_set_ G)) a H)) + ? ? (og_with G)); + simplify; + apply (os_order_relation_properties (og_ordered_set_ G)) + ] +qed. + +coercion cic:/matita/ordered_groups/og_ordered_set.con. + +definition is_ordered_abelian_group ≝ + λG:pre_ordered_abelian_group. ∀f,g,h:G. f≤g → f+h≤g+h. + +record ordered_abelian_group : Type ≝ + { og_pre_ordered_abelian_group:> pre_ordered_abelian_group; + og_ordered_abelian_group_properties: + is_ordered_abelian_group og_pre_ordered_abelian_group + }. + +lemma le_zero_x_to_le_opp_x_zero: ∀G:ordered_abelian_group.∀x:G.0 ≤ x → -x ≤ 0. + intros; + generalize in match (og_ordered_abelian_group_properties ? ? ? (-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: ∀G:ordered_abelian_group.∀x:G. x ≤ 0 → 0 ≤ -x. + intros; + generalize in match (og_ordered_abelian_group_properties ? ? ? (-x) H); intro; + rewrite > zero_neutral in H1; + rewrite > plus_comm in H1; + rewrite > opp_inverse in H1; + assumption. +qed. -- 2.39.2