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