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.

diff --git a/helm/software/matita/dama/ordered_fields_ch0.ma b/helm/software/matita/dama/ordered_fields_ch0.ma
index 1c3b0fe7c14fb00ebf72563fe4b4b6f2fdffaab2..1911379333608b2fdb1d28f80f40fd0b27ca5db2 100644 (file)
--- 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 (file)
index 0000000..a9912d4
--- /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.