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