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/".
  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 Not (eq Z z OZ)].
  56 intros.elim z.
  57 simplify.reflexivity.
  58 simplify.intros.
  59 cut match neg e1 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 e2 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 e1.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 e2.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 theorem Zplus_z_OZ:  \forall z:Z. eq Z (Zplus z OZ) z.
 128 intro.elim z.
 129 simplify.reflexivity.
 130 simplify.reflexivity.
 131 simplify.reflexivity.
 132 qed.
 133
 134 (* theorem symmetric_Zplus: symmetric Z Zplus. *)
 135
 136 theorem sym_Zplus : \forall x,y:Z. eq Z (Zplus x y) (Zplus y x).
 137 intros.elim x.rewrite > Zplus_z_OZ.reflexivity.
 138 elim y.simplify.reflexivity.
 139 simplify.
 140 rewrite < sym_plus.reflexivity.
 141 simplify.
 142 rewrite > nat_compare_n_m_m_n.
 143 simplify.elim nat_compare ? ?.simplify.reflexivity.
 144 simplify. reflexivity.
 145 simplify. reflexivity.
 146 elim y.simplify.reflexivity.
 147 simplify.rewrite > nat_compare_n_m_m_n.
 148 simplify.elim nat_compare ? ?.simplify.reflexivity.
 149 simplify. reflexivity.
 150 simplify. reflexivity.
 151 simplify.rewrite < sym_plus.reflexivity.
 152 qed.
 153
 154 theorem Zpred_Zplus_neg_O : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z).
 155 intros.elim z.
 156 simplify.reflexivity.
 157 simplify.reflexivity.
 158 elim e2.simplify.reflexivity.
 159 simplify.reflexivity.
 160 qed.
 161
 162 theorem Zsucc_Zplus_pos_O : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z).
 163 intros.elim z.
 164 simplify.reflexivity.
 165 elim e1.simplify.reflexivity.
 166 simplify.reflexivity.
 167 simplify.reflexivity.
 168 qed.
 169
 170 theorem Zplus_pos_pos:
 171 \forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))).
 172 intros.
 173 elim n.elim m.
 174 simplify.reflexivity.
 175 simplify.reflexivity.
 176 elim m.
 177 simplify.
 178 rewrite < plus_n_O.reflexivity.
 179 simplify.
 180 rewrite < plus_n_Sm.reflexivity.
 181 qed.
 182
 183 theorem Zplus_pos_neg:
 184 \forall n,m. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))).
 185 intros.reflexivity.
 186 qed.
 187
 188 theorem Zplus_neg_pos :
 189 \forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (Zsucc (neg n)) (Zpred (pos m))).
 190 intros.
 191 elim n.elim m.
 192 simplify.reflexivity.
 193 simplify.reflexivity.
 194 elim m.
 195 simplify.reflexivity.
 196 simplify.reflexivity.
 197 qed.
 198
 199 theorem Zplus_neg_neg:
 200 \forall n,m. eq Z (Zplus (neg n) (neg m)) (Zplus (Zsucc (neg n)) (Zpred (neg m))).
 201 intros.
 202 elim n.elim m.
 203 simplify.reflexivity.
 204 simplify.reflexivity.
 205 elim m.
 206 simplify.rewrite < plus_n_Sm.reflexivity.
 207 simplify.rewrite > plus_n_Sm.reflexivity.
 208 qed.
 209
 210 theorem Zplus_Zsucc_Zpred:
 211 \forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)).
 212 intros.
 213 elim x. elim y.
 214 simplify.reflexivity.
 215 simplify.reflexivity.
 216 rewrite < Zsucc_Zplus_pos_O.
 217 rewrite > Zsucc_Zpred.reflexivity.
 218 elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ).
 219 rewrite < Zpred_Zplus_neg_O.
 220 rewrite > Zpred_Zsucc.
 221 simplify.reflexivity.
 222 rewrite < Zplus_neg_neg.reflexivity.
 223 apply Zplus_neg_pos.
 224 elim y.simplify.reflexivity.
 225 apply Zplus_pos_neg.
 226 apply Zplus_pos_pos.
 227 qed.
 228
 229 theorem Zplus_Zsucc_pos_pos :
 230 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))).
 231 intros.reflexivity.
 232 qed.
 233
 234 theorem Zplus_Zsucc_pos_neg:
 235 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))).
 236 intros.
 237 apply nat_elim2
 238 (\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro.
 239 intros.elim n1.
 240 simplify. reflexivity.
 241 elim e1.simplify. reflexivity.
 242 simplify. reflexivity.
 243 intros. elim n1.
 244 simplify. reflexivity.
 245 simplify.reflexivity.
 246 intros.
 247 rewrite < (Zplus_pos_neg ? m1).
 248 elim H.reflexivity.
 249 qed.
 250
 251 theorem Zplus_Zsucc_neg_neg :
 252 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))).
 253 intros.
 254 apply nat_elim2
 255 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro.
 256 intros.elim n1.
 257 simplify. reflexivity.
 258 elim e1.simplify. reflexivity.
 259 simplify. reflexivity.
 260 intros. elim n1.
 261 simplify. reflexivity.
 262 simplify.reflexivity.
 263 intros.
 264 rewrite < (Zplus_neg_neg ? m1).
 265 reflexivity.
 266 qed.
 267
 268 theorem Zplus_Zsucc_neg_pos:
 269 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))).
 270 intros.
 271 apply nat_elim2
 272 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))).
 273 intros.elim n1.
 274 simplify. reflexivity.
 275 elim e1.simplify. reflexivity.
 276 simplify. reflexivity.
 277 intros. elim n1.
 278 simplify. reflexivity.
 279 simplify.reflexivity.
 280 intros.
 281 rewrite < H.
 282 rewrite < (Zplus_neg_pos ? (S m1)).
 283 reflexivity.
 284 qed.
 285
 286 theorem Zplus_Zsucc : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)).
 287 intros.elim x.elim y.
 288 simplify. reflexivity.
 289 rewrite < Zsucc_Zplus_pos_O.reflexivity.
 290 simplify.reflexivity.
 291 elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity.
 292 apply Zplus_Zsucc_neg_neg.
 293 apply Zplus_Zsucc_neg_pos.
 294 elim y.
 295 rewrite < sym_Zplus OZ.reflexivity.
 296 apply Zplus_Zsucc_pos_neg.
 297 apply Zplus_Zsucc_pos_pos.
 298 qed.
 299
 300 theorem Zplus_Zpred: \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)).
 301 intros.
 302 cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)).
 303 rewrite > Hcut.
 304 rewrite > Zplus_Zsucc.
 305 rewrite > Zpred_Zsucc.
 306 reflexivity.
 307 rewrite > Zsucc_Zpred.
 308 reflexivity.
 309 qed.
 310
 311
 312 theorem associative_Zplus: associative Z Zplus.
 313 (* change with (\forall x,y,z. eq ?(Zplus (Zplus x y) z) (Zplus x (Zplus y z))).*)
 314 simplify.
 315 intros.elim x.simplify.reflexivity.
 316 elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)).
 317 drop.
 318 rewrite < (Zpred_Zplus_neg_O y).
 319 rewrite < Zplus_Zpred.
 320 reflexivity.
 321 rewrite > Zplus_Zpred (neg e).
 322 rewrite > Zplus_Zpred (neg e).
 323 rewrite > Zplus_Zpred (Zplus (neg e) y).
 324 apply eq_f.assumption.
 325 elim e2.rewrite < Zsucc_Zplus_pos_O.
 326 rewrite < Zsucc_Zplus_pos_O.
 327 rewrite > Zplus_Zsucc.
 328 reflexivity.
 329 rewrite > Zplus_Zsucc (pos e1).
 330 rewrite > Zplus_Zsucc (pos e1).
 331 rewrite > Zplus_Zsucc (Zplus (pos e1) y).
 332 apply eq_f.assumption.
 333 qed.
 334
 335 theorem assoc_Zplus :
 336 \forall x,y,z:Z. eq Z (Zplus x (Zplus y z)) (Zplus (Zplus x y) z).
 337 intros.elim x.simplify.reflexivity.
 338 elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)).
 339 rewrite < (Zpred_Zplus_neg_O y).
 340 rewrite < Zplus_Zpred.
 341 reflexivity.
 342 rewrite > Zplus_Zpred (neg e).
 343 rewrite > Zplus_Zpred (neg e).
 344 rewrite > Zplus_Zpred (Zplus (neg e) y).
 345 apply eq_f.assumption.
 346 elim e2.rewrite < Zsucc_Zplus_pos_O.
 347 rewrite < Zsucc_Zplus_pos_O.
 348 rewrite > Zplus_Zsucc.
 349 reflexivity.
 350 rewrite > Zplus_Zsucc (pos e1).
 351 rewrite > Zplus_Zsucc (pos e1).
 352 rewrite > Zplus_Zsucc (Zplus (pos e1) y).
 353 apply eq_f.assumption.
 354 qed.