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 eq Z z OZ
  55 |false \Rightarrow \lnot (eq Z 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. eq 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. eq 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 (plus m n)))
 112          | (neg n) \Rightarrow
 113               match nat_compare m n with
 114                 [ LT \Rightarrow (neg (pred (minus n m)))
 115                 | EQ \Rightarrow OZ
 116                 | GT \Rightarrow (pos (pred (minus 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 (minus n m)))
 123                 | EQ \Rightarrow OZ
 124                 | GT \Rightarrow (neg (pred (minus m n)))]
 125          | (neg n) \Rightarrow (neg (S (plus 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. Zplus 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. eq Z (Zplus x y) (Zplus 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. eq Z (Zpred z) (Zplus (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. eq Z (Zsucc z) (Zplus (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. eq Z (Zplus (pos n) (pos m)) (Zplus (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. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))).
 188 intros.reflexivity.
 189 qed.
 190
 191 theorem Zplus_neg_pos :
 192 \forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (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. eq Z (Zplus (neg n) (neg m)) (Zplus (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. eq Z (Zplus x y) (Zplus (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. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))).
 234 intros.reflexivity.
 235 qed.
 236
 237 theorem Zplus_Zsucc_pos_neg:
 238 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))).
 239 intros.
 240 apply nat_elim2
 241 (\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (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. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))).
 256 intros.
 257 apply nat_elim2
 258 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (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. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))).
 273 intros.
 274 apply nat_elim2
 275 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (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. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus 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. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)).
 304 intros.
 305 cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (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. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)).
 317 (* simplify. *)
 318 intros.elim x.simplify.reflexivity.
 319 elim n.rewrite < (Zpred_Zplus_neg_O (Zplus 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 (Zplus (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 (Zplus (pos n1) y).
 334 apply eq_f.assumption.
 335 qed.
 336
 337 variant assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus 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 theorem Zplus_Zopp: \forall x:Z. (eq Z (Zplus x (Zopp x)) OZ).
 348 intro.elim x.
 349 apply refl_eq.
 350 simplify.
 351 rewrite > nat_compare_n_n.
 352 simplify.apply refl_eq.
 353 simplify.
 354 rewrite > nat_compare_n_n.
 355 simplify.apply refl_eq.
 356 qed.
 357