helm/software/matita/library/Z/plus.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "Z/z.ma".
  16 include "nat/minus.ma".
  17
  18 definition Zplus :Z \to Z \to Z \def
  19 \lambda x,y.
  20   match x with
  21     [ OZ \Rightarrow y
  22     | (pos m) \Rightarrow
  23         match y with
  24          [ OZ \Rightarrow x
  25          | (pos n) \Rightarrow (pos (pred ((S m)+(S n))))
  26          | (neg n) \Rightarrow
  27               match nat_compare m n with
  28                 [ LT \Rightarrow (neg (pred (n-m)))
  29                 | EQ \Rightarrow OZ
  30                 | GT \Rightarrow (pos (pred (m-n)))] ]
  31     | (neg m) \Rightarrow
  32         match y with
  33          [ OZ \Rightarrow x
  34          | (pos n) \Rightarrow
  35               match nat_compare m n with
  36                 [ LT \Rightarrow (pos (pred (n-m)))
  37                 | EQ \Rightarrow OZ
  38                 | GT \Rightarrow (neg (pred (m-n)))]
  39          | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))] ].
  40
  41 interpretation "integer plus" 'plus x y = (Zplus x y).
  42
  43 theorem eq_plus_Zplus: \forall n,m:nat. Z_of_nat (n+m) =
  44 Z_of_nat n + Z_of_nat m.
  45 intro.cases n;intro
  46   [reflexivity
  47   |cases m
  48     [simplify.rewrite < plus_n_O.reflexivity
  49     |simplify.reflexivity.
  50     ]]
  51 qed.
  52
  53 theorem Zplus_z_OZ:  \forall z:Z. z+OZ = z.
  54 intro.elim z.
  55 simplify.reflexivity.
  56 simplify.reflexivity.
  57 simplify.reflexivity.
  58 qed.
  59
  60 (* theorem symmetric_Zplus: symmetric Z Zplus. *)
  61
  62 theorem sym_Zplus : \forall x,y:Z. x+y = y+x.
  63 intros.elim x.rewrite > Zplus_z_OZ.reflexivity.
  64 elim y.simplify.reflexivity.
  65 simplify.
  66 rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
  67 simplify.
  68 rewrite > nat_compare_n_m_m_n.
  69 simplify.elim nat_compare.simplify.reflexivity.
  70 simplify. reflexivity.
  71 simplify. reflexivity.
  72 elim y.simplify.reflexivity.
  73 simplify.rewrite > nat_compare_n_m_m_n.
  74 simplify.elim nat_compare.simplify.reflexivity.
  75 simplify. reflexivity.
  76 simplify. reflexivity.
  77 simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
  78 qed.
  79
  80 theorem Zpred_Zplus_neg_O : \forall z:Z. Zpred z = (neg O)+z.
  81 intros.elim z.
  82   simplify.reflexivity.
  83   elim n.
  84     simplify.reflexivity.
  85     simplify.reflexivity.
  86   simplify.reflexivity.
  87 qed.
  88
  89 theorem Zsucc_Zplus_pos_O : \forall z:Z. Zsucc z = (pos O)+z.
  90 intros.elim z.
  91   simplify.reflexivity.
  92   simplify.reflexivity.
  93   elim n.
  94     simplify.reflexivity.
  95     simplify.reflexivity.
  96 qed.
  97
  98 theorem Zplus_pos_pos:
  99 \forall n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)).
 100 intros.
 101 elim n.elim m.
 102 simplify.reflexivity.
 103 simplify.reflexivity.
 104 elim m.
 105 simplify.rewrite < plus_n_Sm.
 106 rewrite < plus_n_O.reflexivity.
 107 simplify.rewrite < plus_n_Sm.
 108 rewrite < plus_n_Sm.reflexivity.
 109 qed.
 110
 111 theorem Zplus_pos_neg:
 112 \forall n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)).
 113 intros.reflexivity.
 114 qed.
 115
 116 theorem Zplus_neg_pos :
 117 \forall n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)).
 118 intros.
 119 elim n.elim m.
 120 simplify.reflexivity.
 121 simplify.reflexivity.
 122 elim m.
 123 simplify.reflexivity.
 124 simplify.reflexivity.
 125 qed.
 126
 127 theorem Zplus_neg_neg:
 128 \forall n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)).
 129 intros.
 130 elim n.elim m.
 131 simplify.reflexivity.
 132 simplify.reflexivity.
 133 elim m.
 134 simplify.rewrite > plus_n_Sm.reflexivity.
 135 simplify.rewrite > plus_n_Sm.reflexivity.
 136 qed.
 137
 138 theorem Zplus_Zsucc_Zpred:
 139 \forall x,y. x+y = (Zsucc x)+(Zpred y).
 140 intros.elim x.
 141   elim y.
 142     simplify.reflexivity.
 143     rewrite < Zsucc_Zplus_pos_O.rewrite > Zsucc_Zpred.reflexivity.
 144     simplify.reflexivity.
 145   elim y.
 146     simplify.reflexivity.
 147     apply Zplus_pos_pos.
 148     apply Zplus_pos_neg.
 149   elim y.
 150     rewrite < sym_Zplus.rewrite < (sym_Zplus (Zpred OZ)).
 151      rewrite < Zpred_Zplus_neg_O.rewrite > Zpred_Zsucc.simplify.reflexivity.
 152     apply Zplus_neg_pos.
 153     rewrite < Zplus_neg_neg.reflexivity.
 154 qed.
 155
 156 theorem Zplus_Zsucc_pos_pos :
 157 \forall n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)).
 158 intros.reflexivity.
 159 qed.
 160
 161 theorem Zplus_Zsucc_pos_neg:
 162 \forall n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))).
 163 intros.
 164 apply (nat_elim2
 165 (\lambda n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))))).intro.
 166 intros.elim n1.
 167 simplify. reflexivity.
 168 elim n2.simplify. reflexivity.
 169 simplify. reflexivity.
 170 intros. elim n1.
 171 simplify. reflexivity.
 172 simplify.reflexivity.
 173 intros.
 174 rewrite < (Zplus_pos_neg ? m1).
 175 elim H.reflexivity.
 176 qed.
 177
 178 theorem Zplus_Zsucc_neg_neg :
 179 \forall n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
 180 intros.
 181 apply (nat_elim2
 182 (\lambda n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m))).intro.
 183 intros.elim n1.
 184 simplify. reflexivity.
 185 elim n2.simplify. reflexivity.
 186 simplify. reflexivity.
 187 intros. elim n1.
 188 simplify. reflexivity.
 189 simplify.reflexivity.
 190 intros.
 191 rewrite < (Zplus_neg_neg ? m1).
 192 reflexivity.
 193 qed.
 194
 195 theorem Zplus_Zsucc_neg_pos:
 196 \forall n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
 197 intros.
 198 apply (nat_elim2
 199 (\lambda n,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m))).
 200 intros.elim n1.
 201 simplify. reflexivity.
 202 elim n2.simplify. reflexivity.
 203 simplify. reflexivity.
 204 intros. elim n1.
 205 simplify. reflexivity.
 206 simplify.reflexivity.
 207 intros.
 208 rewrite < H.
 209 rewrite < (Zplus_neg_pos ? (S m1)).
 210 reflexivity.
 211 qed.
 212
 213 theorem Zplus_Zsucc : \forall x,y:Z. (Zsucc x)+y = Zsucc (x+y).
 214 intros.elim x.
 215   elim y.
 216     simplify. reflexivity.
 217     simplify.reflexivity.
 218     rewrite < Zsucc_Zplus_pos_O.reflexivity.
 219   elim y.
 220     rewrite < (sym_Zplus OZ).reflexivity.
 221     apply Zplus_Zsucc_pos_pos.
 222     apply Zplus_Zsucc_pos_neg.
 223   elim y.
 224     rewrite < sym_Zplus.rewrite < (sym_Zplus OZ).simplify.reflexivity.
 225     apply Zplus_Zsucc_neg_pos.
 226     apply Zplus_Zsucc_neg_neg.
 227 qed.
 228
 229 theorem Zplus_Zpred: \forall x,y:Z. (Zpred x)+y = Zpred (x+y).
 230 intros.
 231 cut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y)).
 232 rewrite > Hcut.
 233 rewrite > Zplus_Zsucc.
 234 rewrite > Zpred_Zsucc.
 235 reflexivity.
 236 rewrite > Zsucc_Zpred.
 237 reflexivity.
 238 qed.
 239
 240
 241 theorem associative_Zplus: associative Z Zplus.
 242 change with (\forall x,y,z:Z. (x + y) + z = x + (y + z)).
 243 (* simplify. *)
 244 intros.elim x.
 245   simplify.reflexivity.
 246   elim n.
 247     rewrite < Zsucc_Zplus_pos_O.rewrite < Zsucc_Zplus_pos_O.
 248      rewrite > Zplus_Zsucc.reflexivity.
 249     rewrite > (Zplus_Zsucc (pos n1)).rewrite > (Zplus_Zsucc (pos n1)).
 250      rewrite > (Zplus_Zsucc ((pos n1)+y)).apply eq_f.assumption.
 251   elim n.
 252     rewrite < (Zpred_Zplus_neg_O (y+z)).rewrite < (Zpred_Zplus_neg_O y).
 253      rewrite < Zplus_Zpred.reflexivity.
 254     rewrite > (Zplus_Zpred (neg n1)).rewrite > (Zplus_Zpred (neg n1)).
 255      rewrite > (Zplus_Zpred ((neg n1)+y)).apply eq_f.assumption.
 256 qed.
 257
 258 variant assoc_Zplus : \forall x,y,z:Z.  (x+y)+z = x+(y+z)
 259 \def associative_Zplus.
 260
 261 (* Zopp *)
 262 definition Zopp : Z \to Z \def
 263 \lambda x:Z. match x with
 264 [ OZ \Rightarrow OZ
 265 | (pos n) \Rightarrow (neg n)
 266 | (neg n) \Rightarrow (pos n) ].
 267
 268 interpretation "integer unary minus" 'uminus x = (Zopp x).
 269
 270 theorem eq_OZ_Zopp_OZ : OZ = (- OZ).
 271 reflexivity.
 272 qed.
 273
 274 theorem Zopp_Zplus: \forall x,y:Z. -(x+y) = -x + -y.
 275 intros.
 276 elim x.elim y.
 277 simplify. reflexivity.
 278 simplify. reflexivity.
 279 simplify. reflexivity.
 280 elim y.
 281 simplify. reflexivity.
 282 simplify. reflexivity.
 283 simplify. apply nat_compare_elim.
 284 intro.simplify.reflexivity.
 285 intro.simplify.reflexivity.
 286 intro.simplify.reflexivity.
 287 elim y.
 288 simplify. reflexivity.
 289 simplify. apply nat_compare_elim.
 290 intro.simplify.reflexivity.
 291 intro.simplify.reflexivity.
 292 intro.simplify.reflexivity.
 293 simplify.reflexivity.
 294 qed.
 295
 296 theorem Zopp_Zopp: \forall x:Z. --x = x.
 297 intro. elim x.
 298 reflexivity.reflexivity.reflexivity.
 299 qed.
 300
 301 theorem Zplus_Zopp: \forall x:Z. x+ -x = OZ.
 302 intro.elim x.
 303 apply refl_eq.
 304 simplify.
 305 rewrite > nat_compare_n_n.
 306 simplify.apply refl_eq.
 307 simplify.
 308 rewrite > nat_compare_n_n.
 309 simplify.apply refl_eq.
 310 qed.
 311
 312 theorem injective_Zplus_l: \forall x:Z.injective Z Z (\lambda y.y+x).
 313 intro.simplify.intros (z y).
 314 rewrite < Zplus_z_OZ.
 315 rewrite < (Zplus_z_OZ y).
 316 rewrite < (Zplus_Zopp x).
 317 rewrite < assoc_Zplus.
 318 rewrite < assoc_Zplus.
 319 apply eq_f2
 320   [assumption|reflexivity]
 321 qed.
 322
 323 theorem injective_Zplus_r: \forall x:Z.injective Z Z (\lambda y.x+y).
 324 intro.simplify.intros (z y).
 325 apply (injective_Zplus_l x).
 326 rewrite < sym_Zplus.
 327 rewrite > H.
 328 apply sym_Zplus.
 329 qed.
 330
 331 (* minus *)
 332 definition Zminus : Z \to Z \to Z \def \lambda x,y:Z. x + (-y).
 333
 334 interpretation "integer minus" 'minus x y = (Zminus x y).