helm/software/matita/dama/ordered_group.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/ordered_group/".
  16
  17 include "group.ma".
  18
  19 record pogroup_ : Type ≝ {
  20   og_abelian_group_: abelian_group;
  21   og_excedence:> excedence;
  22   og_with: carr og_abelian_group_ = apart_of_excedence og_excedence
  23 }.
  24
  25 lemma og_abelian_group: pogroup_ → abelian_group.
  26 intro G; apply (mk_abelian_group G); [1,2,3: rewrite < (og_with G)]
  27 [apply (plus (og_abelian_group_ G));|apply zero;|apply opp]
  28 unfold apartness_OF_pogroup_; cases (og_with G); simplify;
  29 [apply plus_assoc|apply plus_comm|apply zero_neutral|apply opp_inverse|apply plus_strong_ext]
  30 qed.
  31
  32 coercion cic:/matita/ordered_group/og_abelian_group.con.
  33
  34 record pogroup : Type ≝ {
  35   og_carr:> pogroup_;
  36   plus_cancr_exc: ∀f,g,h:og_carr. f+h ≰ g+h → f ≰ g
  37 }.
  38
  39 lemma fexc_plusr:
  40   ∀G:pogroup.∀x,y,z:G. x ≰ y → x+z ≰ y + z.
  41 intros 5 (G x y z L); apply (plus_cancr_exc ??? (-z));
  42 apply (Ex≪  (x + (z + -z)) (plus_assoc ????));
  43 apply (Ex≪  (x + (-z + z)) (plus_comm ??z));
  44 apply (Ex≪  (x+0) (opp_inverse ??));
  45 apply (Ex≪  (0+x) (plus_comm ???));
  46 apply (Ex≪  x (zero_neutral ??));
  47 apply (Ex≫ (y + (z + -z)) (plus_assoc ????));
  48 apply (Ex≫  (y + (-z + z)) (plus_comm ??z));
  49 apply (Ex≫  (y+0) (opp_inverse ??));
  50 apply (Ex≫  (0+y) (plus_comm ???));
  51 apply (Ex≫  y (zero_neutral ??) L);
  52 qed.
  53
  54 coercion cic:/matita/ordered_group/fexc_plusr.con nocomposites.
  55
  56 lemma plus_cancl_exc: ∀G:pogroup.∀f,g,h:G. h+f ≰ h+g → f ≰ g.
  57 intros 5 (G x y z L); apply (plus_cancr_exc ??? z);
  58 apply (exc_rewl ??? (z+x) (plus_comm ???));
  59 apply (exc_rewr ??? (z+y) (plus_comm ???) L);
  60 qed.
  61
  62 lemma fexc_plusl:
  63   ∀G:pogroup.∀x,y,z:G. x ≰ y → z+x ≰ z+y.
  64 intros 5 (G x y z L); apply (plus_cancl_exc ??? (-z));
  65 apply (exc_rewl ???? (plus_assoc ??z x));
  66 apply (exc_rewr ???? (plus_assoc ??z y));
  67 apply (exc_rewl ??? (0+x) (opp_inverse ??));
  68 apply (exc_rewr ??? (0+y) (opp_inverse ??));
  69 apply (exc_rewl ???? (zero_neutral ??));
  70 apply (exc_rewr ???? (zero_neutral ??) L);
  71 qed.
  72
  73 coercion cic:/matita/ordered_group/fexc_plusl.con nocomposites.
  74
  75 lemma plus_cancr_le:
  76   ∀G:pogroup.∀x,y,z:G.x+z ≤ y + z → x ≤ y.
  77 intros 5 (G x y z L);
  78 apply (le_rewl ??? (0+x) (zero_neutral ??));
  79 apply (le_rewl ??? (x+0) (plus_comm ???));
  80 apply (le_rewl ??? (x+(-z+z)) (opp_inverse ??));
  81 apply (le_rewl ??? (x+(z+ -z)) (plus_comm ??z));
  82 apply (le_rewl ??? (x+z+ -z) (plus_assoc ????));
  83 apply (le_rewr ??? (0+y) (zero_neutral ??));
  84 apply (le_rewr ??? (y+0) (plus_comm ???));
  85 apply (le_rewr ??? (y+(-z+z)) (opp_inverse ??));
  86 apply (le_rewr ??? (y+(z+ -z)) (plus_comm ??z));
  87 apply (le_rewr ??? (y+z+ -z) (plus_assoc ????));
  88 intro H; apply L; clear L; apply (plus_cancr_exc ??? (-z) H);
  89 qed.
  90
  91 lemma fle_plusl: ∀G:pogroup. ∀f,g,h:G. f≤g → h+f≤h+g.
  92 intros (G f g h);
  93 apply (plus_cancr_le ??? (-h));
  94 apply (le_rewl ??? (f+h+ -h) (plus_comm ? f h));
  95 apply (le_rewl ??? (f+(h+ -h)) (plus_assoc ????));
  96 apply (le_rewl ??? (f+(-h+h)) (plus_comm ? h (-h)));
  97 apply (le_rewl ??? (f+0) (opp_inverse ??));
  98 apply (le_rewl ??? (0+f) (plus_comm ???));
  99 apply (le_rewl ??? (f) (zero_neutral ??));
 100 apply (le_rewr ??? (g+h+ -h) (plus_comm ? h ?));
 101 apply (le_rewr ??? (g+(h+ -h)) (plus_assoc ????));
 102 apply (le_rewr ??? (g+(-h+h)) (plus_comm ??h));
 103 apply (le_rewr ??? (g+0) (opp_inverse ??));
 104 apply (le_rewr ??? (0+g) (plus_comm ???));
 105 apply (le_rewr ??? (g) (zero_neutral ??) H);
 106 qed.
 107
 108 lemma fle_plusr: ∀G:pogroup. ∀f,g,h:G. f≤g → f+h≤g+h.
 109 intros (G f g h H); apply (le_rewl ???? (plus_comm ???));
 110 apply (le_rewr ???? (plus_comm ???)); apply fle_plusl; assumption;
 111 qed.
 112
 113 lemma plus_cancl_le:
 114   ∀G:pogroup.∀x,y,z:G.z+x ≤ z+y → x ≤ y.
 115 intros 5 (G x y z L);
 116 apply (le_rewl ??? (0+x) (zero_neutral ??));
 117 apply (le_rewl ??? ((-z+z)+x) (opp_inverse ??));
 118 apply (le_rewl ??? (-z+(z+x)) (plus_assoc ????));
 119 apply (le_rewr ??? (0+y) (zero_neutral ??));
 120 apply (le_rewr ??? ((-z+z)+y) (opp_inverse ??));
 121 apply (le_rewr ??? (-z+(z+y)) (plus_assoc ????));
 122 apply (fle_plusl ??? (-z) L);
 123 qed.
 124
 125 lemma plus_cancl_lt:
 126   ∀G:pogroup.∀x,y,z:G.z+x < z+y → x < y.
 127 intros 5 (G x y z L); elim L (A LE); split; [apply plus_cancl_le; assumption]
 128 apply (plus_cancl_ap ???? LE);
 129 qed.
 130
 131 lemma plus_cancr_lt:
 132   ∀G:pogroup.∀x,y,z:G.x+z < y+z → x < y.
 133 intros 5 (G x y z L); elim L (A LE); split; [apply plus_cancr_le; assumption]
 134 apply (plus_cancr_ap ???? LE);
 135 qed.
 136
 137
 138 lemma exc_opp_x_zero_to_exc_zero_x:
 139   ∀G:pogroup.∀x:G.-x ≰ 0 → 0 ≰ x.
 140 intros (G x H); apply (plus_cancr_exc ??? (-x));
 141 apply (exc_rewr ???? (plus_comm ???));
 142 apply (exc_rewr ???? (opp_inverse ??));
 143 apply (exc_rewl ???? (zero_neutral ??) H);
 144 qed.
 145
 146 lemma le_zero_x_to_le_opp_x_zero:
 147   ∀G:pogroup.∀x:G.0 ≤ x → -x ≤ 0.
 148 intros (G x Px); apply (plus_cancr_le ??? x);
 149 apply (le_rewl ??? 0 (opp_inverse ??));
 150 apply (le_rewr ??? x (zero_neutral ??) Px);
 151 qed.
 152
 153 lemma lt_zero_x_to_lt_opp_x_zero:
 154   ∀G:pogroup.∀x:G.0 < x → -x < 0.
 155 intros (G x Px); apply (plus_cancr_lt ??? x);
 156 apply (lt_rewl ??? 0 (opp_inverse ??));
 157 apply (lt_rewr ??? x (zero_neutral ??) Px);
 158 qed.
 159
 160 lemma exc_zero_opp_x_to_exc_x_zero:
 161   ∀G:pogroup.∀x:G. 0 ≰ -x → x ≰ 0.
 162 intros (G x H); apply (plus_cancl_exc ??? (-x));
 163 apply (exc_rewr ???? (plus_comm ???));
 164 apply (exc_rewl ???? (opp_inverse ??));
 165 apply (exc_rewr ???? (zero_neutral ??) H);
 166 qed.
 167
 168 lemma le_x_zero_to_le_zero_opp_x:
 169   ∀G:pogroup.∀x:G. x ≤ 0 → 0 ≤ -x.
 170 intros (G x Lx0); apply (plus_cancr_le ??? x);
 171 apply (le_rewr ??? 0 (opp_inverse ??));
 172 apply (le_rewl ??? x (zero_neutral ??));
 173 assumption;
 174 qed.
 175
 176 lemma lt_x_zero_to_lt_zero_opp_x:
 177   ∀G:pogroup.∀x:G. x < 0 → 0 < -x.
 178 intros (G x Lx0); apply (plus_cancr_lt ??? x);
 179 apply (lt_rewr ??? 0 (opp_inverse ??));
 180 apply (lt_rewl ??? x (zero_neutral ??));
 181 assumption;
 182 qed.
 183
 184
 185 lemma lt0plus_orlt:
 186   ∀G:pogroup. ∀x,y:G. 0 ≤ x → 0 ≤ y → 0 < x + y → 0 < x ∨ 0 < y.
 187 intros (G x y LEx LEy LT); cases LT (H1 H2); cases (ap_cotransitive ??? y H2);
 188 [right; split; assumption|left;split;[assumption]]
 189 apply (plus_cancr_ap ??? y); apply (ap_rewl ???? (zero_neutral ??));
 190 assumption;
 191 qed.
 192
 193 lemma le0plus_le:
 194   ∀G:pogroup.∀a,b,c:G. 0 ≤ b →  a + b ≤ c → a ≤ c.
 195 intros (G a b c L H); apply (le_transitive ????? H);
 196 apply (plus_cancl_le ??? (-a));
 197 apply (le_rewl ??? 0 (opp_inverse ??));
 198 apply (le_rewr ??? (-a + a + b) (plus_assoc ????));
 199 apply (le_rewr ??? (0 + b) (opp_inverse ??));
 200 apply (le_rewr ??? b (zero_neutral ??));
 201 assumption;
 202 qed.
 203
 204 lemma le_le0plus:
 205   ∀G:pogroup.∀a,b:G. 0 ≤ a → 0 ≤ b → 0 ≤ a + b.
 206 intros (G a b L1 L2); apply (le_transitive ???? L1);
 207 apply (plus_cancl_le ??? (-a));
 208 apply (le_rewl ??? 0 (opp_inverse ??));
 209 apply (le_rewr ??? (-a + a + b) (plus_assoc ????));
 210 apply (le_rewr ??? (0 + b) (opp_inverse ??));
 211 apply (le_rewr ??? b (zero_neutral ??));
 212 assumption;
 213 qed.
 214
 215 lemma flt_plusl:
 216   ∀G:pogroup.∀x,y,z:G.x < y → z + x < z + y.
 217 intros (G x y z H); cases H; split; [apply fle_plusl; assumption]
 218 apply fap_plusl; assumption;
 219 qed.
 220
 221 lemma flt_plusr:
 222   ∀G:pogroup.∀x,y,z:G.x < y → x + z < y + z.
 223 intros (G x y z H); cases H; split; [apply fle_plusr; assumption]
 224 apply fap_plusr; assumption;
 225 qed.
 226
 227
 228 lemma ltxy_ltyyxx: ∀G:pogroup.∀x,y:G. y < x → y+y < x+x.
 229 intros; apply (lt_transitive ?? (y+x));[2:
 230   apply (lt_rewl ???? (plus_comm ???));
 231   apply (lt_rewr ???? (plus_comm ???));]
 232 apply flt_plusl;assumption;
 233 qed.
 234
 235 lemma lew_opp : ∀O:pogroup.∀a,b,c:O.0 ≤ b → a ≤ c → a + -b ≤ c.
 236 intros (O a b c L0 L);
 237 apply (le_transitive ????? L);
 238 apply (plus_cancl_le ??? (-a));
 239 apply (le_rewr ??? 0 (opp_inverse ??));
 240 apply (le_rewl ??? (-a+a+-b) (plus_assoc ????));
 241 apply (le_rewl ??? (0+-b) (opp_inverse ??));
 242 apply (le_rewl ??? (-b) (zero_neutral ?(-b)));
 243 apply le_zero_x_to_le_opp_x_zero;
 244 assumption;
 245 qed.
 246
 247 lemma ltw_opp : ∀O:pogroup.∀a,b,c:O.0 < b → a < c → a + -b < c.
 248 intros (O a b c P L);
 249 apply (lt_transitive ????? L);
 250 apply (plus_cancl_lt ??? (-a));
 251 apply (lt_rewr ??? 0 (opp_inverse ??));
 252 apply (lt_rewl ??? (-a+a+-b) (plus_assoc ????));
 253 apply (lt_rewl ??? (0+-b) (opp_inverse ??));
 254 apply (lt_rewl ??? ? (zero_neutral ??));
 255 apply lt_zero_x_to_lt_opp_x_zero;
 256 assumption;
 257 qed.
 258
 259 record togroup : Type ≝ {
 260   tog_carr:> pogroup;
 261   tog_total: ∀x,y:tog_carr.x≰y → y < x
 262 }.
 263
 264 lemma lexxyy_lexy: ∀G:togroup. ∀x,y:G. x+x ≤ y+y → x ≤ y.
 265 intros (G x y H); intro H1; lapply (tog_total ??? H1) as H2;
 266 lapply (ltxy_ltyyxx ??? H2) as H3; lapply (lt_to_excede ??? H3) as H4;
 267 cases (H H4);
 268 qed.
 269
 270 lemma eqxxyy_eqxy: ∀G:togroup.∀x,y:G. x + x ≈ y + y → x ≈ y.
 271 intros (G x y H); cases (eq_le_le ??? H); apply le_le_eq;
 272 apply lexxyy_lexy; assumption;
 273 qed.
 274
 275 lemma applus_orap: ∀G:abelian_group. ∀x,y:G. 0 # x + y → 0 #x ∨ 0#y.
 276 intros; cases (ap_cotransitive ??? y a); [right; assumption]
 277 left; apply (plus_cancr_ap ??? y); apply (ap_rewl ???y (zero_neutral ??));
 278 assumption;
 279 qed.
 280
 281 lemma ltplus: ∀G:pogroup.∀a,b,c,d:G. a < b → c < d → a+c < b + d.
 282 intros (G a b c d H1 H2);
 283 lapply (flt_plusr ??? c H1) as H3;
 284 apply (lt_transitive ???? H3);
 285 apply flt_plusl; assumption;
 286 qed.
 287
 288 lemma excplus_orexc: ∀G:pogroup.∀a,b,c,d:G. a+c ≰ b + d →  a ≰ b ∨ c ≰ d.
 289 intros (G a b c d H1 H2);
 290 cases (exc_cotransitive ??? (a + d) H1); [
 291   right; apply (plus_cancl_exc ??? a); assumption]
 292 left; apply (plus_cancr_exc ??? d); assumption;
 293 qed.
 294
 295 lemma leplus: ∀G:pogroup.∀a,b,c,d:G. a ≤ b → c ≤ d → a+c ≤ b + d.
 296 intros (G a b c d H1 H2); intro H3; cases (excplus_orexc ????? H3);
 297 [apply H1|apply H2] assumption;
 298 qed.
 299
 300 lemma leplus_lt_le: ∀G:togroup.∀x,y:G. 0 ≤ x + y → x < 0 → 0 ≤ y.
 301 intros; intro; apply H; lapply (lt_to_excede ??? l);
 302 lapply (tog_total ??? e);
 303 lapply (tog_total ??? Hletin);
 304 lapply (ltplus ????? Hletin2 Hletin1);
 305 apply (exc_rewl ??? (0+0)); [apply eq_sym; apply zero_neutral]
 306 apply lt_to_excede; assumption;
 307 qed.
 308
 309 lemma ltplus_orlt: ∀G:togroup.∀a,b,c,d:G. a+c < b + d →  a < b ∨ c < d.
 310 intros (G a b c d H1 H2); lapply (lt_to_excede ??? H1);
 311 cases (excplus_orexc ????? Hletin); [left|right] apply tog_total; assumption;
 312 qed.
 313
 314 lemma excplus: ∀G:togroup.∀a,b,c,d:G.a ≰ b → c ≰ d → a + c ≰ b + d.
 315 intros (G a b c d L1 L2);
 316 lapply (fexc_plusr ??? (c) L1) as L3;
 317 elim (exc_cotransitive ??? (b+d) L3); [assumption]
 318 lapply (plus_cancl_exc ???? t); lapply (tog_total ??? Hletin);
 319 cases Hletin1; cases (H L2);
 320 qed.