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