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 Zplus_z_OZ:  \forall z:Z. z+OZ = z.
  44 intro.elim z.
  45 simplify.reflexivity.
  46 simplify.reflexivity.
  47 simplify.reflexivity.
  48 qed.
  49
  50 (* theorem symmetric_Zplus: symmetric Z Zplus. *)
  51
  52 theorem sym_Zplus : \forall x,y:Z. x+y = y+x.
  53 intros.elim x.rewrite > Zplus_z_OZ.reflexivity.
  54 elim y.simplify.reflexivity.
  55 simplify.
  56 rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
  57 simplify.
  58 rewrite > nat_compare_n_m_m_n.
  59 simplify.elim nat_compare.simplify.reflexivity.
  60 simplify. reflexivity.
  61 simplify. reflexivity.
  62 elim y.simplify.reflexivity.
  63 simplify.rewrite > nat_compare_n_m_m_n.
  64 simplify.elim nat_compare.simplify.reflexivity.
  65 simplify. reflexivity.
  66 simplify. reflexivity.
  67 simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
  68 qed.
  69
  70 theorem Zpred_Zplus_neg_O : \forall z:Z. Zpred z = (neg O)+z.
  71 intros.elim z.
  72   simplify.reflexivity.
  73   elim n.
  74     simplify.reflexivity.
  75     simplify.reflexivity.
  76   simplify.reflexivity.
  77 qed.
  78
  79 theorem Zsucc_Zplus_pos_O : \forall z:Z. Zsucc z = (pos O)+z.
  80 intros.elim z.
  81   simplify.reflexivity.
  82   simplify.reflexivity.
  83   elim n.
  84     simplify.reflexivity.
  85     simplify.reflexivity.
  86 qed.
  87
  88 theorem Zplus_pos_pos:
  89 \forall n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)).
  90 intros.
  91 elim n.elim m.
  92 simplify.reflexivity.
  93 simplify.reflexivity.
  94 elim m.
  95 simplify.rewrite < plus_n_Sm.
  96 rewrite < plus_n_O.reflexivity.
  97 simplify.rewrite < plus_n_Sm.
  98 rewrite < plus_n_Sm.reflexivity.
  99 qed.
 100
 101 theorem Zplus_pos_neg:
 102 \forall n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)).
 103 intros.reflexivity.
 104 qed.
 105
 106 theorem Zplus_neg_pos :
 107 \forall n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)).
 108 intros.
 109 elim n.elim m.
 110 simplify.reflexivity.
 111 simplify.reflexivity.
 112 elim m.
 113 simplify.reflexivity.
 114 simplify.reflexivity.
 115 qed.
 116
 117 theorem Zplus_neg_neg:
 118 \forall n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)).
 119 intros.
 120 elim n.elim m.
 121 simplify.reflexivity.
 122 simplify.reflexivity.
 123 elim m.
 124 simplify.rewrite > plus_n_Sm.reflexivity.
 125 simplify.rewrite > plus_n_Sm.reflexivity.
 126 qed.
 127
 128 theorem Zplus_Zsucc_Zpred:
 129 \forall x,y. x+y = (Zsucc x)+(Zpred y).
 130 intros.elim x.
 131   elim y.
 132     simplify.reflexivity.
 133     rewrite < Zsucc_Zplus_pos_O.rewrite > Zsucc_Zpred.reflexivity.
 134     simplify.reflexivity.
 135   elim y.
 136     simplify.reflexivity.
 137     apply Zplus_pos_pos.
 138     apply Zplus_pos_neg.
 139   elim y.
 140     rewrite < sym_Zplus.rewrite < (sym_Zplus (Zpred OZ)).
 141      rewrite < Zpred_Zplus_neg_O.rewrite > Zpred_Zsucc.simplify.reflexivity.
 142     apply Zplus_neg_pos.
 143     rewrite < Zplus_neg_neg.reflexivity.
 144 qed.
 145
 146 theorem Zplus_Zsucc_pos_pos :
 147 \forall n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)).
 148 intros.reflexivity.
 149 qed.
 150
 151 theorem Zplus_Zsucc_pos_neg:
 152 \forall n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))).
 153 intros.
 154 apply (nat_elim2
 155 (\lambda n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))))).intro.
 156 intros.elim n1.
 157 simplify. reflexivity.
 158 elim n2.simplify. reflexivity.
 159 simplify. reflexivity.
 160 intros. elim n1.
 161 simplify. reflexivity.
 162 simplify.reflexivity.
 163 intros.
 164 rewrite < (Zplus_pos_neg ? m1).
 165 elim H.reflexivity.
 166 qed.
 167
 168 theorem Zplus_Zsucc_neg_neg :
 169 \forall n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
 170 intros.
 171 apply (nat_elim2
 172 (\lambda n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m))).intro.
 173 intros.elim n1.
 174 simplify. reflexivity.
 175 elim n2.simplify. reflexivity.
 176 simplify. reflexivity.
 177 intros. elim n1.
 178 simplify. reflexivity.
 179 simplify.reflexivity.
 180 intros.
 181 rewrite < (Zplus_neg_neg ? m1).
 182 reflexivity.
 183 qed.
 184
 185 theorem Zplus_Zsucc_neg_pos:
 186 \forall n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
 187 intros.
 188 apply (nat_elim2
 189 (\lambda n,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m))).
 190 intros.elim n1.
 191 simplify. reflexivity.
 192 elim n2.simplify. reflexivity.
 193 simplify. reflexivity.
 194 intros. elim n1.
 195 simplify. reflexivity.
 196 simplify.reflexivity.
 197 intros.
 198 rewrite < H.
 199 rewrite < (Zplus_neg_pos ? (S m1)).
 200 reflexivity.
 201 qed.
 202
 203 theorem Zplus_Zsucc : \forall x,y:Z. (Zsucc x)+y = Zsucc (x+y).
 204 intros.elim x.
 205   elim y.
 206     simplify. reflexivity.
 207     simplify.reflexivity.
 208     rewrite < Zsucc_Zplus_pos_O.reflexivity.
 209   elim y.
 210     rewrite < (sym_Zplus OZ).reflexivity.
 211     apply Zplus_Zsucc_pos_pos.
 212     apply Zplus_Zsucc_pos_neg.
 213   elim y.
 214     rewrite < sym_Zplus.rewrite < (sym_Zplus OZ).simplify.reflexivity.
 215     apply Zplus_Zsucc_neg_pos.
 216     apply Zplus_Zsucc_neg_neg.
 217 qed.
 218
 219 theorem Zplus_Zpred: \forall x,y:Z. (Zpred x)+y = Zpred (x+y).
 220 intros.
 221 cut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y)).
 222 rewrite > Hcut.
 223 rewrite > Zplus_Zsucc.
 224 rewrite > Zpred_Zsucc.
 225 reflexivity.
 226 rewrite > Zsucc_Zpred.
 227 reflexivity.
 228 qed.
 229
 230
 231 theorem associative_Zplus: associative Z Zplus.
 232 change with (\forall x,y,z:Z. (x + y) + z = x + (y + z)).
 233 (* simplify. *)
 234 intros.elim x.
 235   simplify.reflexivity.
 236   elim n.
 237     rewrite < Zsucc_Zplus_pos_O.rewrite < Zsucc_Zplus_pos_O.
 238      rewrite > Zplus_Zsucc.reflexivity.
 239     rewrite > (Zplus_Zsucc (pos n1)).rewrite > (Zplus_Zsucc (pos n1)).
 240      rewrite > (Zplus_Zsucc ((pos n1)+y)).apply eq_f.assumption.
 241   elim n.
 242     rewrite < (Zpred_Zplus_neg_O (y+z)).rewrite < (Zpred_Zplus_neg_O y).
 243      rewrite < Zplus_Zpred.reflexivity.
 244     rewrite > (Zplus_Zpred (neg n1)).rewrite > (Zplus_Zpred (neg n1)).
 245      rewrite > (Zplus_Zpred ((neg n1)+y)).apply eq_f.assumption.
 246 qed.
 247
 248 variant assoc_Zplus : \forall x,y,z:Z.  (x+y)+z = x+(y+z)
 249 \def associative_Zplus.
 250
 251 (* Zopp *)
 252 definition Zopp : Z \to Z \def
 253 \lambda x:Z. match x with
 254 [ OZ \Rightarrow OZ
 255 | (pos n) \Rightarrow (neg n)
 256 | (neg n) \Rightarrow (pos n) ].
 257
 258 interpretation "integer unary minus" 'uminus x = (Zopp x).
 259
 260 theorem eq_OZ_Zopp_OZ : OZ = (- OZ).
 261 reflexivity.
 262 qed.
 263
 264 theorem Zopp_Zplus: \forall x,y:Z. -(x+y) = -x + -y.
 265 intros.
 266 elim x.elim y.
 267 simplify. reflexivity.
 268 simplify. reflexivity.
 269 simplify. reflexivity.
 270 elim y.
 271 simplify. reflexivity.
 272 simplify. reflexivity.
 273 simplify. apply nat_compare_elim.
 274 intro.simplify.reflexivity.
 275 intro.simplify.reflexivity.
 276 intro.simplify.reflexivity.
 277 elim y.
 278 simplify. reflexivity.
 279 simplify. apply nat_compare_elim.
 280 intro.simplify.reflexivity.
 281 intro.simplify.reflexivity.
 282 intro.simplify.reflexivity.
 283 simplify.reflexivity.
 284 qed.
 285
 286 theorem Zopp_Zopp: \forall x:Z. --x = x.
 287 intro. elim x.
 288 reflexivity.reflexivity.reflexivity.
 289 qed.
 290
 291 theorem Zplus_Zopp: \forall x:Z. x+ -x = OZ.
 292 intro.elim x.
 293 apply refl_eq.
 294 simplify.
 295 rewrite > nat_compare_n_n.
 296 simplify.apply refl_eq.
 297 simplify.
 298 rewrite > nat_compare_n_n.
 299 simplify.apply refl_eq.
 300 qed.
 301
 302 theorem injective_Zplus_l: \forall x:Z.injective Z Z (\lambda y.y+x).
 303 intro.simplify.intros (z y).
 304 rewrite < Zplus_z_OZ.
 305 rewrite < (Zplus_z_OZ y).
 306 rewrite < (Zplus_Zopp x).
 307 rewrite < assoc_Zplus.
 308 rewrite < assoc_Zplus.
 309 apply eq_f2
 310   [assumption|reflexivity]
 311 qed.
 312
 313 theorem injective_Zplus_r: \forall x:Z.injective Z Z (\lambda y.x+y).
 314 intro.simplify.intros (z y).
 315 apply (injective_Zplus_l x).
 316 rewrite < sym_Zplus.
 317 rewrite > H.
 318 apply sym_Zplus.
 319 qed.
 320
 321 (* minus *)
 322 definition Zminus : Z \to Z \to Z \def \lambda x,y:Z. x + (-y).
 323
 324 interpretation "integer minus" 'minus x y = (Zminus x y).