From 624a7c13a2ed22ed2535690074c7a08e18de7f13 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 14 Nov 2007 13:17:07 +0000
Subject: [PATCH] ogroups almost finished

---
 helm/software/matita/dama/excedence.ma      | 18 +++++
 helm/software/matita/dama/ordered_groups.ma | 83 ++++++++++++---------
 2 files changed, 65 insertions(+), 36 deletions(-)

diff --git a/helm/software/matita/dama/excedence.ma b/helm/software/matita/dama/excedence.ma
index 6d1fc4dd7..59b8baa4e 100644
--- a/helm/software/matita/dama/excedence.ma
+++ b/helm/software/matita/dama/excedence.ma
@@ -119,3 +119,21 @@ theorem lt_to_excede: ∀E:excedence.∀a,b:E. (a < b) → (b ≰ a).
 intros (E a b Lab); cases Lab (LEab Aab);
 cases Aab (H H); [cases (LEab H)] fold normalize (b ≰ a); assumption; (* BUG *)  
 qed.
+
+theorem le_le_to_eq: ∀E:excedence.∀x,y:E. x ≤ y → y ≤ x → x ≈ y.
+intros 6 (E x y L1 L2 H); cases H; [apply (L1 H1)|apply (L2 H1)]
+qed.
+
+lemma unfold_apart: ∀E:excedence. ∀x,y:E. x ≰ y ∨ y ≰ x → x # y.
+unfold apart_of_excedence; unfold apart; simplify; intros; assumption;
+qed.
+
+lemma le_rewl: ∀E:excedence.∀z,y,x:E. x ≈ y → x ≤ z → y ≤ z.
+intros (E z y x Exy Lxz); apply (le_transitive ???? ? Lxz);
+intro Xyz; apply Exy; apply unfold_apart; right; assumption;
+qed.
+
+lemma le_rewr: ∀E:excedence.∀z,y,x:E. x ≈ y → z ≤ x → z ≤ y.
+intros (E z y x Exy Lxz); apply (le_transitive ???? Lxz);
+intro Xyz; apply Exy; apply unfold_apart; left; assumption;
+qed.
diff --git a/helm/software/matita/dama/ordered_groups.ma b/helm/software/matita/dama/ordered_groups.ma
index 11ac6a216..fb4b29f0d 100644
--- a/helm/software/matita/dama/ordered_groups.ma
+++ b/helm/software/matita/dama/ordered_groups.ma
@@ -17,50 +17,29 @@ set "baseuri" "cic:/matita/ordered_groups/".
 include "ordered_sets.ma".
 include "groups.ma".
 
-record pre_ordered_abelian_group : Type ≝
- { og_abelian_group_: abelian_group;
-   og_tordered_set:> tordered_set;
-   og_with: carr og_abelian_group_ = og_tordered_set
- }.
+record pre_ogroup : Type ≝ { 
+  og_abelian_group_: abelian_group;
+  og_tordered_set:> tordered_set;
+  og_with: carr og_abelian_group_ = og_tordered_set
+}.
 
-lemma og_abelian_group: pre_ordered_abelian_group → abelian_group.
+lemma og_abelian_group: pre_ogroup → abelian_group.
 intro G; apply (mk_abelian_group G); [1,2,3: rewrite < (og_with G)]
 [apply (plus (og_abelian_group_ G));|apply zero;|apply opp]
-unfold apartness_OF_pre_ordered_abelian_group; cases (og_with G); simplify;
+unfold apartness_OF_pre_ogroup; cases (og_with G); simplify;
 [apply plus_assoc|apply plus_comm|apply zero_neutral|apply opp_inverse|apply plus_strong_ext]
 qed.
 
 coercion cic:/matita/ordered_groups/og_abelian_group.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_le_eq: ∀E:excedence.∀x,y:E. x ≤ y → y ≤ x → x ≈ y.
-intros 6 (E x y L1 L2 H); cases H; [apply (L1 H1)|apply (L2 H1)]
-qed.
-
-lemma unfold_apart: ∀E:excedence. ∀x,y:E. x ≰ y ∨ y ≰ x → x # y.
-unfold apart_of_excedence; unfold apart; simplify; intros; assumption;
-qed.
-
-lemma le_rewl: ∀E:excedence.∀z,y,x:E. x ≈ y → x ≤ z → y ≤ z.
-intros (E z y x Exy Lxz); apply (le_transitive ???? ? Lxz);
-intro Xyz; apply Exy; apply unfold_apart; right; assumption;
-qed.
-
-lemma le_rewr: ∀E:excedence.∀z,y,x:E. x ≈ y → z ≤ x → z ≤ y.
-intros (E z y x Exy Lxz); apply (le_transitive ???? Lxz);
-intro Xyz; apply Exy; apply unfold_apart; left; assumption;
-qed.
+record ogroup : Type ≝ { 
+  og_carr:> pre_ogroup;
+  fle_plusr: ∀f,g,h:og_carr. f≤g → f+h≤g+h
+}.
 
 lemma plus_cancr_le: 
-  ∀G:ordered_abelian_group.∀x,y,z:G.x+z ≤ y + z → x ≤ y.
+  ∀G:ogroup.∀x,y,z:G.x+z ≤ y + z → x ≤ y.
 intros 5 (G x y z L);
 apply (le_rewl ??? (0+x) (zero_neutral ??));
 apply (le_rewl ??? (x+0) (plus_comm ???));
@@ -72,12 +51,44 @@ apply (le_rewr ??? (y+0) (plus_comm ???));
 apply (le_rewr ??? (y+(-z+z))); [apply feq_plusl;apply opp_inverse;]
 apply (le_rewr ??? (y+(z+ -z))); [apply feq_plusl;apply plus_comm;]
 apply (le_rewr ??? (y+z+ -z)); [apply eq_symmetric; apply plus_assoc;]
-apply (og_ordered_abelian_group_properties ??? (-z));
+apply (fle_plusr ??? (-z));
+assumption;
+qed.
+
+lemma fle_plusl: ∀G:ogroup. ∀f,g,h:G. f≤g → h+f≤h+g.
+intros (G f g h);
+apply (plus_cancr_le ??? (-h));
+apply (le_rewl ??? (f+h+ -h)); [apply feq_plusr;apply plus_comm;]
+apply (le_rewl ??? (f+(h+ -h)) (plus_assoc ????));
+apply (le_rewl ??? (f+(-h+h))); [apply feq_plusl;apply plus_comm;]
+apply (le_rewl ??? (f+0)); [apply feq_plusl; apply eq_symmetric; apply opp_inverse]
+apply (le_rewl ??? (0+f) (plus_comm ???));
+apply (le_rewl ??? (f) (eq_symmetric ??? (zero_neutral ??)));
+apply (le_rewr ??? (g+h+ -h)); [apply feq_plusr;apply plus_comm;]
+apply (le_rewr ??? (g+(h+ -h)) (plus_assoc ????));
+apply (le_rewr ??? (g+(-h+h))); [apply feq_plusl;apply plus_comm;]
+apply (le_rewr ??? (g+0)); [apply feq_plusl; apply eq_symmetric; apply opp_inverse]
+apply (le_rewr ??? (0+g) (plus_comm ???));
+apply (le_rewr ??? (g) (eq_symmetric ??? (zero_neutral ??)));
 assumption;
 qed.
 
+lemma plus_cancl_le: 
+  ∀G:ogroup.∀x,y,z:G.z+x ≤ z+y → x ≤ y.
+intros 5 (G x y z L);
+apply (le_rewl ??? (0+x) (zero_neutral ??));
+apply (le_rewl ??? ((-z+z)+x)); [apply feq_plusr;apply opp_inverse;]
+apply (le_rewl ??? (-z+(z+x)) (plus_assoc ????));
+apply (le_rewr ??? (0+y) (zero_neutral ??));
+apply (le_rewr ??? ((-z+z)+y)); [apply feq_plusr;apply opp_inverse;]
+apply (le_rewr ??? (-z+(z+y)) (plus_assoc ????));
+apply (fle_plusl ??? (-z));
+assumption;
+qed.
+
+
 lemma le_zero_x_to_le_opp_x_zero: 
-  ∀G:ordered_abelian_group.∀x:G.0 ≤ x → -x ≤ 0.
+  ∀G:ogroup.∀x:G.0 ≤ x → -x ≤ 0.
 intros (G x Px); apply (plus_cancr_le ??? x);
 apply (le_rewl ??? 0 (eq_symmetric ??? (opp_inverse ??)));
 apply (le_rewr ??? x (eq_symmetric ??? (zero_neutral ??)));
@@ -85,7 +96,7 @@ assumption;
 qed.
 
 lemma le_x_zero_to_le_zero_opp_x: 
-  ∀G:ordered_abelian_group.∀x:G. x ≤ 0 → 0 ≤ -x.
+  ∀G:ogroup.∀x:G. x ≤ 0 → 0 ≤ -x.
 intros (G x Lx0); apply (plus_cancr_le ??? x);
 apply (le_rewr ??? 0 (eq_symmetric ??? (opp_inverse ??)));
 apply (le_rewl ??? x (eq_symmetric ??? (zero_neutral ??)));
-- 
2.39.2