matita/contribs/dama/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
  16
  17 include "group.ma".
  18
  19 record pogroup_ : Type ≝ {
  20   og_abelian_group_: abelian_group;
  21   og_excess:> excess;
  22   og_with: carr og_abelian_group_ = exc_ap og_excess
  23 }.
  24
  25 lemma og_abelian_group: pogroup_ → abelian_group.
  26 intro G; apply (mk_abelian_group G); unfold apartness_OF_pogroup_;
  27 cases (og_with G); simplify;
  28 [apply (plus (og_abelian_group_ G));|apply zero;|apply opp
  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 (Ex≪ (z+x) (plus_comm ???));
  59 apply (Ex≫ (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 (Ex≪? (plus_assoc ??z x));
  66 apply (Ex≫? (plus_assoc ??z y));
  67 apply (Ex≪ (0+x) (opp_inverse ??));
  68 apply (Ex≫ (0+y) (opp_inverse ??));
  69 apply (Ex≪? (zero_neutral ??));
  70 apply (Ex≫? (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≪ (0+x) (zero_neutral ??));
  79 apply (Le≪ (x+0) (plus_comm ???));
  80 apply (Le≪ (x+(-z+z)) (opp_inverse ??));
  81 apply (Le≪ (x+(z+ -z)) (plus_comm ??z));
  82 apply (Le≪ (x+z+ -z) (plus_assoc ????));
  83 apply (Le≫ (0+y) (zero_neutral ??));
  84 apply (Le≫ (y+0) (plus_comm ???));
  85 apply (Le≫ (y+(-z+z)) (opp_inverse ??));
  86 apply (Le≫ (y+(z+ -z)) (plus_comm ??z));
  87 apply (Le≫ (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≪ (f+h+ -h) (plus_comm ? f h));
  95 apply (Le≪ (f+(h+ -h)) (plus_assoc ????));
  96 apply (Le≪ (f+(-h+h)) (plus_comm ? h (-h)));
  97 apply (Le≪ (f+0) (opp_inverse ??));
  98 apply (Le≪ (0+f) (plus_comm ???));
  99 apply (Le≪ (f) (zero_neutral ??));
 100 apply (Le≫ (g+h+ -h) (plus_comm ? h ?));
 101 apply (Le≫ (g+(h+ -h)) (plus_assoc ????));
 102 apply (Le≫ (g+(-h+h)) (plus_comm ??h));
 103 apply (Le≫ (g+0) (opp_inverse ??));
 104 apply (Le≫ (0+g) (plus_comm ???));
 105 apply (Le≫ (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≪? (plus_comm ???));
 110 apply (Le≫? (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≪ (0+x) (zero_neutral ??));
 117 apply (Le≪ ((-z+z)+x) (opp_inverse ??));
 118 apply (Le≪ (-z+(z+x)) (plus_assoc ????));
 119 apply (Le≫ (0+y) (zero_neutral ??));
 120 apply (Le≫ ((-z+z)+y) (opp_inverse ??));
 121 apply (Le≫ (-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 (Ex≫? (plus_comm ???));
 142 apply (Ex≫? (opp_inverse ??));
 143 apply (Ex≪? (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≪ 0 (opp_inverse ??));
 150 apply (Le≫ 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≪ 0 (opp_inverse ??));
 157 apply (Lt≫ 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 (Ex≫? (plus_comm ???));
 164 apply (Ex≪? (opp_inverse ??));
 165 apply (Ex≫? (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≫ 0 (opp_inverse ??));
 172 apply (Le≪ 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≫ 0 (opp_inverse ??));
 180 apply (Lt≪ x (zero_neutral ??));
 181 assumption;
 182 qed.
 183
 184 lemma lt_opp_x_zero_to_lt_zero_x:
 185   ∀G:pogroup.∀x:G. -x < 0 → 0 < x.
 186 intros (G x Lx0); apply (plus_cancr_lt ??? (-x));
 187 apply (Lt≪ (-x) (zero_neutral ??));
 188 apply (Lt≫ (-x+x) (plus_comm ???));
 189 apply (Lt≫ 0 (opp_inverse ??));
 190 assumption;
 191 qed.
 192
 193 lemma lt0plus_orlt:
 194   ∀G:pogroup. ∀x,y:G. 0 ≤ x → 0 ≤ y → 0 < x + y → 0 < x ∨ 0 < y.
 195 intros (G x y LEx LEy LT); cases LT (H1 H2); cases (ap_cotransitive ??? y H2);
 196 [right; split; assumption|left;split;[assumption]]
 197 apply (plus_cancr_ap ??? y); apply (Ap≪? (zero_neutral ??));
 198 assumption;
 199 qed.
 200
 201 lemma le0plus_le:
 202   ∀G:pogroup.∀a,b,c:G. 0 ≤ b →  a + b ≤ c → a ≤ c.
 203 intros (G a b c L H); apply (le_transitive ????? H);
 204 apply (plus_cancl_le ??? (-a));
 205 apply (Le≪ 0 (opp_inverse ??));
 206 apply (Le≫ (-a + a + b) (plus_assoc ????));
 207 apply (Le≫ (0 + b) (opp_inverse ??));
 208 apply (Le≫ b (zero_neutral ??));
 209 assumption;
 210 qed.
 211
 212 lemma le_le0plus:
 213   ∀G:pogroup.∀a,b:G. 0 ≤ a → 0 ≤ b → 0 ≤ a + b.
 214 intros (G a b L1 L2); apply (le_transitive ???? L1);
 215 apply (plus_cancl_le ??? (-a));
 216 apply (Le≪ 0 (opp_inverse ??));
 217 apply (Le≫ (-a + a + b) (plus_assoc ????));
 218 apply (Le≫ (0 + b) (opp_inverse ??));
 219 apply (Le≫ b (zero_neutral ??));
 220 assumption;
 221 qed.
 222
 223 lemma flt_plusl:
 224   ∀G:pogroup.∀x,y,z:G.x < y → z + x < z + y.
 225 intros (G x y z H); cases H; split; [apply fle_plusl; assumption]
 226 apply fap_plusl; assumption;
 227 qed.
 228
 229 lemma flt_plusr:
 230   ∀G:pogroup.∀x,y,z:G.x < y → x + z < y + z.
 231 intros (G x y z H); cases H; split; [apply fle_plusr; assumption]
 232 apply fap_plusr; assumption;
 233 qed.
 234
 235
 236 lemma ltxy_ltyyxx: ∀G:pogroup.∀x,y:G. y < x → y+y < x+x.
 237 intros; apply (lt_transitive ?? (y+x));[2:
 238   apply (Lt≪? (plus_comm ???));
 239   apply (Lt≫? (plus_comm ???));]
 240 apply flt_plusl;assumption;
 241 qed.
 242
 243 lemma lew_opp : ∀O:pogroup.∀a,b,c:O.0 ≤ b → a ≤ c → a + -b ≤ c.
 244 intros (O a b c L0 L);
 245 apply (le_transitive ????? L);
 246 apply (plus_cancl_le ??? (-a));
 247 apply (Le≫ 0 (opp_inverse ??));
 248 apply (Le≪ (-a+a+-b) (plus_assoc ????));
 249 apply (Le≪ (0+-b) (opp_inverse ??));
 250 apply (Le≪ (-b) (zero_neutral ?(-b)));
 251 apply le_zero_x_to_le_opp_x_zero;
 252 assumption;
 253 qed.
 254
 255 lemma ltw_opp : ∀O:pogroup.∀a,b,c:O.0 < b → a < c → a + -b < c.
 256 intros (O a b c P L);
 257 apply (lt_transitive ????? L);
 258 apply (plus_cancl_lt ??? (-a));
 259 apply (Lt≫ 0 (opp_inverse ??));
 260 apply (Lt≪ (-a+a+-b) (plus_assoc ????));
 261 apply (Lt≪ (0+-b) (opp_inverse ??));
 262 apply (Lt≪ ? (zero_neutral ??));
 263 apply lt_zero_x_to_lt_opp_x_zero;
 264 assumption;
 265 qed.
 266
 267 record togroup : Type ≝ {
 268   tog_carr:> pogroup;
 269   tog_total: ∀x,y:tog_carr.x≰y → y < x
 270 }.
 271
 272 lemma lexxyy_lexy: ∀G:togroup. ∀x,y:G. x+x ≤ y+y → x ≤ y.
 273 intros (G x y H); intro H1; lapply (tog_total ??? H1) as H2;
 274 lapply (ltxy_ltyyxx ??? H2) as H3; lapply (lt_to_excess ??? H3) as H4;
 275 cases (H H4);
 276 qed.
 277
 278 lemma eqxxyy_eqxy: ∀G:togroup.∀x,y:G. x + x ≈ y + y → x ≈ y.
 279 intros (G x y H); cases (eq_le_le ??? H); apply le_le_eq;
 280 apply lexxyy_lexy; assumption;
 281 qed.
 282
 283 lemma applus_orap: ∀G:abelian_group. ∀x,y:G. 0 # x + y → 0 #x ∨ 0#y.
 284 intros; cases (ap_cotransitive ??? y a); [right; assumption]
 285 left; apply (plus_cancr_ap ??? y); apply (Ap≪y (zero_neutral ??));
 286 assumption;
 287 qed.
 288
 289 lemma ltplus: ∀G:pogroup.∀a,b,c,d:G. a < b → c < d → a+c < b + d.
 290 intros (G a b c d H1 H2);
 291 lapply (flt_plusr ??? c H1) as H3;
 292 apply (lt_transitive ???? H3);
 293 apply flt_plusl; assumption;
 294 qed.
 295
 296 lemma excplus_orexc: ∀G:pogroup.∀a,b,c,d:G. a+c ≰ b + d →  a ≰ b ∨ c ≰ d.
 297 intros (G a b c d H1 H2);
 298 cases (exc_cotransitive ??? (a + d) H1); [
 299   right; apply (plus_cancl_exc ??? a); assumption]
 300 left; apply (plus_cancr_exc ??? d); assumption;
 301 qed.
 302
 303 lemma leplus: ∀G:pogroup.∀a,b,c,d:G. a ≤ b → c ≤ d → a+c ≤ b + d.
 304 intros (G a b c d H1 H2); intro H3; cases (excplus_orexc ????? H3);
 305 [apply H1|apply H2] assumption;
 306 qed.
 307
 308 lemma leplus_lt_le: ∀G:togroup.∀x,y:G. 0 ≤ x + y → x < 0 → 0 ≤ y.
 309 intros; intro; apply H; lapply (lt_to_excess ??? l);
 310 lapply (tog_total ??? e);
 311 lapply (tog_total ??? Hletin);
 312 lapply (ltplus ????? Hletin2 Hletin1);
 313 apply (Ex≪ (0+0)); [apply eq_sym; apply zero_neutral]
 314 apply lt_to_excess; assumption;
 315 qed.
 316
 317 lemma ltplus_orlt: ∀G:togroup.∀a,b,c,d:G. a+c < b + d →  a < b ∨ c < d.
 318 intros (G a b c d H1 H2); lapply (lt_to_excess ??? H1);
 319 cases (excplus_orexc ????? Hletin); [left|right] apply tog_total; assumption;
 320 qed.
 321
 322 lemma excplus: ∀G:togroup.∀a,b,c,d:G.a ≰ b → c ≰ d → a + c ≰ b + d.
 323 intros (G a b c d L1 L2);
 324 lapply (fexc_plusr ??? (c) L1) as L3;
 325 elim (exc_cotransitive ??? (b+d) L3); [assumption]
 326 lapply (plus_cancl_exc ???? t); lapply (tog_total ??? Hletin);
 327 cases Hletin1; cases (H L2);
 328 qed.