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/nat.ma".
  18 include "datatypes/bool.ma".
  19
  20 inductive Z : Set \def
  21   OZ : Z
  22 | pos : nat \to Z
  23 | neg : nat \to Z.
  24
  25 definition Z_of_nat \def
  26 \lambda n. match n with
  27 [ O \Rightarrow  OZ
  28 | (S n)\Rightarrow  pos n].
  29
  30 coercion Z_of_nat.
  31
  32 definition neg_Z_of_nat \def
  33 \lambda n. match n with
  34 [ O \Rightarrow  OZ
  35 | (S n)\Rightarrow  neg n].
  36
  37 definition absZ \def
  38 \lambda z.
  39  match z with
  40 [ OZ \Rightarrow O
  41 | (pos n) \Rightarrow n
  42 | (neg n) \Rightarrow n].
  43
  44 definition OZ_testb \def
  45 \lambda z.
  46 match z with
  47 [ OZ \Rightarrow true
  48 | (pos n) \Rightarrow false
  49 | (neg n) \Rightarrow false].
  50
  51 theorem OZ_discr :
  52 \forall z. if_then_else (OZ_testb z) (eq Z z OZ) (Not (eq Z z OZ)).
  53 intros.elim z.simplify.reflexivity.
  54 simplify.intros.
  55 cut match neg e1 with
  56 [ OZ \Rightarrow True
  57 | (pos n) \Rightarrow False
  58 | (neg n) \Rightarrow False].
  59 apply Hcut.rewrite > H.simplify.exact I.
  60 simplify.intros.
  61 cut match pos e2 with
  62 [ OZ \Rightarrow True
  63 | (pos n) \Rightarrow False
  64 | (neg n) \Rightarrow False].
  65 apply Hcut. rewrite > H.simplify.exact I.
  66 qed.
  67
  68 definition Zsucc \def
  69 \lambda z. match z with
  70 [ OZ \Rightarrow pos O
  71 | (pos n) \Rightarrow pos (S n)
  72 | (neg n) \Rightarrow
  73           match n with
  74           [ O \Rightarrow OZ
  75           | (S p) \Rightarrow neg p]].
  76
  77 definition Zpred \def
  78 \lambda z. match z with
  79 [ OZ \Rightarrow neg O
  80 | (pos n) \Rightarrow
  81           match n with
  82           [ O \Rightarrow OZ
  83           | (S p) \Rightarrow pos p]
  84 | (neg n) \Rightarrow neg (S n)].
  85
  86 theorem Zpred_succ: \forall z:Z. eq Z (Zpred (Zsucc z)) z.
  87 intros.elim z.reflexivity.
  88 elim e1.reflexivity.
  89 reflexivity.
  90 reflexivity.
  91 qed.
  92
  93 theorem Zsucc_pred: \forall z:Z. eq Z (Zsucc (Zpred z)) z.
  94 intros.elim z.reflexivity.
  95 reflexivity.
  96 elim e2.reflexivity.
  97 reflexivity.
  98 qed.
  99
 100 let rec Zplus x y : Z \def
 101   match x with
 102     [ OZ \Rightarrow y
 103     | (pos m) \Rightarrow
 104         match y with
 105          [ OZ \Rightarrow x
 106          | (pos n) \Rightarrow (pos (S (plus m n)))
 107          | (neg n) \Rightarrow
 108               match nat_compare m n with
 109                 [ LT \Rightarrow (neg (pred (minus n m)))
 110                 | EQ \Rightarrow OZ
 111                 | GT \Rightarrow (pos (pred (minus m n)))]]
 112     | (neg m) \Rightarrow
 113         match y with
 114          [ OZ \Rightarrow x
 115          | (pos n) \Rightarrow
 116               match nat_compare m n with
 117                 [ LT \Rightarrow (pos (pred (minus n m)))
 118                 | EQ \Rightarrow OZ
 119                 | GT \Rightarrow (neg (pred (minus m n)))]
 120          | (neg n) \Rightarrow (neg (S (plus m n)))]].
 121
 122 theorem Zplus_z_O:  \forall z:Z. eq Z (Zplus z OZ) z.
 123 intro.elim z.
 124 simplify.reflexivity.
 125 simplify.reflexivity.
 126 simplify.reflexivity.
 127 qed.
 128
 129 theorem sym_Zplus : \forall x,y:Z. eq Z (Zplus x y) (Zplus y x).
 130 intros.elim x.simplify.rewrite > Zplus_z_O.reflexivity.
 131 elim y.simplify.reflexivity.
 132 simplify.
 133 rewrite < sym_plus.reflexivity.
 134 simplify.
 135 rewrite > nat_compare_invert.
 136 simplify.elim nat_compare ? ?.simplify.reflexivity.
 137 simplify. reflexivity.
 138 simplify. reflexivity.
 139 elim y.simplify.reflexivity.
 140 simplify.rewrite > nat_compare_invert.
 141 simplify.elim nat_compare ? ?.simplify.reflexivity.
 142 simplify. reflexivity.
 143 simplify. reflexivity.
 144 simplify.elim (sym_plus ? ?).reflexivity.
 145 qed.
 146
 147 theorem Zpred_neg : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z).
 148 intros.elim z.
 149 simplify.reflexivity.
 150 simplify.reflexivity.
 151 elim e2.simplify.reflexivity.
 152 simplify.reflexivity.
 153 qed.
 154
 155 theorem Zsucc_pos : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z).
 156 intros.elim z.
 157 simplify.reflexivity.
 158 elim e1.simplify.reflexivity.
 159 simplify.reflexivity.
 160 simplify.reflexivity.
 161 qed.
 162
 163 theorem Zplus_succ_pred_pp :
 164 \forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))).
 165 intros.
 166 elim n.elim m.
 167 simplify.reflexivity.
 168 simplify.reflexivity.
 169 elim m.
 170 simplify.
 171 rewrite < plus_n_O.reflexivity.
 172 simplify.
 173 rewrite < plus_n_Sm.reflexivity.
 174 qed.
 175
 176 theorem Zplus_succ_pred_pn :
 177 \forall n,m. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))).
 178 intros.reflexivity.
 179 qed.
 180
 181 theorem Zplus_succ_pred_np :
 182 \forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (Zsucc (neg n)) (Zpred (pos m))).
 183 intros.
 184 elim n.elim m.
 185 simplify.reflexivity.
 186 simplify.reflexivity.
 187 elim m.
 188 simplify.reflexivity.
 189 simplify.reflexivity.
 190 qed.
 191
 192 theorem Zplus_succ_pred_nn:
 193 \forall n,m. eq Z (Zplus (neg n) (neg m)) (Zplus (Zsucc (neg n)) (Zpred (neg m))).
 194 intros.
 195 elim n.elim m.
 196 simplify.reflexivity.
 197 simplify.reflexivity.
 198 elim m.
 199 simplify.rewrite < plus_n_Sm.reflexivity.
 200 simplify.rewrite > plus_n_Sm.reflexivity.
 201 qed.
 202
 203 theorem Zplus_succ_pred:
 204 \forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)).
 205 intros.
 206 elim x. elim y.
 207 simplify.reflexivity.
 208 simplify.reflexivity.
 209 rewrite < Zsucc_pos.rewrite > Zsucc_pred.reflexivity.
 210 elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ).
 211 rewrite < Zpred_neg.rewrite > Zpred_succ.
 212 simplify.reflexivity.
 213 rewrite < Zplus_succ_pred_nn.reflexivity.
 214 apply Zplus_succ_pred_np.
 215 elim y.simplify.reflexivity.
 216 apply Zplus_succ_pred_pn.
 217 apply Zplus_succ_pred_pp.
 218 qed.
 219
 220 theorem Zsucc_plus_pp :
 221 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))).
 222 intros.reflexivity.
 223 qed.
 224
 225 theorem Zsucc_plus_pn :
 226 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))).
 227 intros.
 228 apply nat_double_ind
 229 (\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro.
 230 intros.elim n1.
 231 simplify. reflexivity.
 232 elim e1.simplify. reflexivity.
 233 simplify. reflexivity.
 234 intros. elim n1.
 235 simplify. reflexivity.
 236 simplify.reflexivity.
 237 intros.
 238 rewrite < (Zplus_succ_pred_pn ? m1).
 239 elim H.reflexivity.
 240 qed.
 241
 242 theorem Zsucc_plus_nn :
 243 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))).
 244 intros.
 245 apply nat_double_ind
 246 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro.
 247 intros.elim n1.
 248 simplify. reflexivity.
 249 elim e1.simplify. reflexivity.
 250 simplify. reflexivity.
 251 intros. elim n1.
 252 simplify. reflexivity.
 253 simplify.reflexivity.
 254 intros.
 255 rewrite < (Zplus_succ_pred_nn ? m1).
 256 reflexivity.
 257 qed.
 258
 259 theorem Zsucc_plus_np :
 260 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))).
 261 intros.
 262 apply nat_double_ind
 263 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))).
 264 intros.elim n1.
 265 simplify. reflexivity.
 266 elim e1.simplify. reflexivity.
 267 simplify. reflexivity.
 268 intros. elim n1.
 269 simplify. reflexivity.
 270 simplify.reflexivity.
 271 intros.
 272 rewrite < H.
 273 rewrite < (Zplus_succ_pred_np ? (S m1)).
 274 reflexivity.
 275 qed.
 276
 277
 278 theorem Zsucc_plus : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)).
 279 intros.elim x.elim y.
 280 simplify. reflexivity.
 281 rewrite < Zsucc_pos.reflexivity.
 282 simplify.reflexivity.
 283 elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity.
 284 apply Zsucc_plus_nn.
 285 apply Zsucc_plus_np.
 286 elim y.
 287 rewrite < sym_Zplus OZ.reflexivity.
 288 apply Zsucc_plus_pn.
 289 apply Zsucc_plus_pp.
 290 qed.
 291
 292 theorem Zpred_plus : \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)).
 293 intros.
 294 cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)).
 295 rewrite > Hcut.
 296 rewrite > Zsucc_plus.
 297 rewrite > Zpred_succ.
 298 reflexivity.
 299 rewrite > Zsucc_pred.
 300 reflexivity.
 301 qed.
 302
 303 theorem assoc_Zplus :
 304 \forall x,y,z:Z. eq Z (Zplus x (Zplus y z)) (Zplus (Zplus x y) z).
 305 intros.elim x.simplify.reflexivity.
 306 elim e1.rewrite < (Zpred_neg (Zplus y z)).
 307 rewrite < (Zpred_neg y).
 308 rewrite < Zpred_plus.
 309 reflexivity.
 310 rewrite > Zpred_plus (neg e).
 311 rewrite > Zpred_plus (neg e).
 312 rewrite > Zpred_plus (Zplus (neg e) y).
 313 apply f_equal.assumption.
 314 elim e2.rewrite < Zsucc_pos.
 315 rewrite < Zsucc_pos.
 316 rewrite > Zsucc_plus.
 317 reflexivity.
 318 rewrite > Zsucc_plus (pos e1).
 319 rewrite > Zsucc_plus (pos e1).
 320 rewrite > Zsucc_plus (Zplus (pos e1) y).
 321 apply f_equal.assumption.
 322 qed.