matitaB/matita/contribs/ng_assembly2/common/nat.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "common/comp.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* ******** *)
  27 (* NATURALI *)
  28 (* ******** *)
  29
  30 ninductive nat : Type ≝
  31   O : nat
  32 | S : nat → nat.
  33
  34 (*
  35 interpretation "Natural numbers" 'N = nat.
  36
  37 default "natural numbers" cic:/matita/common/nat/nat.ind.
  38
  39 alias num (instance 0) = "natural number".
  40 *)
  41
  42 nlet rec nat_it (T:Type) (f:T → T) (arg:T) (n:nat) on n ≝
  43  match n with
  44   [ O ⇒ arg
  45   | S n' ⇒ nat_it T f (f arg) n'
  46   ].
  47
  48 ndefinition nat1 ≝ S O.
  49 ndefinition nat2 ≝ S nat1.
  50 ndefinition nat3 ≝ S nat2.
  51 ndefinition nat4 ≝ S nat3.
  52 ndefinition nat5 ≝ S nat4.
  53 ndefinition nat6 ≝ S nat5.
  54 ndefinition nat7 ≝ S nat6.
  55 ndefinition nat8 ≝ S nat7.
  56 ndefinition nat9 ≝ S nat8.
  57 ndefinition nat10 ≝ S nat9.
  58 ndefinition nat11 ≝ S nat10.
  59 ndefinition nat12 ≝ S nat11.
  60 ndefinition nat13 ≝ S nat12.
  61 ndefinition nat14 ≝ S nat13.
  62 ndefinition nat15 ≝ S nat14.
  63 ndefinition nat16 ≝ S nat15.
  64 ndefinition nat17 ≝ S nat16.
  65 ndefinition nat18 ≝ S nat17.
  66 ndefinition nat19 ≝ S nat18.
  67 ndefinition nat20 ≝ S nat19.
  68 ndefinition nat21 ≝ S nat20.
  69 ndefinition nat22 ≝ S nat21.
  70 ndefinition nat23 ≝ S nat22.
  71 ndefinition nat24 ≝ S nat23.
  72 ndefinition nat25 ≝ S nat24.
  73 ndefinition nat26 ≝ S nat25.
  74 ndefinition nat27 ≝ S nat26.
  75 ndefinition nat28 ≝ S nat27.
  76 ndefinition nat29 ≝ S nat28.
  77 ndefinition nat30 ≝ S nat29.
  78 ndefinition nat31 ≝ S nat30.
  79 ndefinition nat32 ≝ S nat31.
  80 ndefinition nat33 ≝ S nat32.
  81 ndefinition nat34 ≝ S nat33.
  82 ndefinition nat35 ≝ S nat34.
  83 ndefinition nat36 ≝ S nat35.
  84 ndefinition nat37 ≝ S nat36.
  85 ndefinition nat38 ≝ S nat37.
  86 ndefinition nat39 ≝ S nat38.
  87 ndefinition nat40 ≝ S nat39.
  88 ndefinition nat41 ≝ S nat40.
  89 ndefinition nat42 ≝ S nat41.
  90 ndefinition nat43 ≝ S nat42.
  91 ndefinition nat44 ≝ S nat43.
  92 ndefinition nat45 ≝ S nat44.
  93 ndefinition nat46 ≝ S nat45.
  94 ndefinition nat47 ≝ S nat46.
  95 ndefinition nat48 ≝ S nat47.
  96 ndefinition nat49 ≝ S nat48.
  97 ndefinition nat50 ≝ S nat49.
  98 ndefinition nat51 ≝ S nat50.
  99 ndefinition nat52 ≝ S nat51.
 100 ndefinition nat53 ≝ S nat52.
 101 ndefinition nat54 ≝ S nat53.
 102 ndefinition nat55 ≝ S nat54.
 103 ndefinition nat56 ≝ S nat55.
 104 ndefinition nat57 ≝ S nat56.
 105 ndefinition nat58 ≝ S nat57.
 106 ndefinition nat59 ≝ S nat58.
 107 ndefinition nat60 ≝ S nat59.
 108 ndefinition nat61 ≝ S nat60.
 109 ndefinition nat62 ≝ S nat61.
 110 ndefinition nat63 ≝ S nat62.
 111 ndefinition nat64 ≝ S nat63.
 112 ndefinition nat65 ≝ S nat64.
 113 ndefinition nat66 ≝ S nat65.
 114 ndefinition nat67 ≝ S nat66.
 115 ndefinition nat68 ≝ S nat67.
 116 ndefinition nat69 ≝ S nat68.
 117 ndefinition nat70 ≝ S nat69.
 118 ndefinition nat71 ≝ S nat70.
 119 ndefinition nat72 ≝ S nat71.
 120 ndefinition nat73 ≝ S nat72.
 121 ndefinition nat74 ≝ S nat73.
 122 ndefinition nat75 ≝ S nat74.
 123 ndefinition nat76 ≝ S nat75.
 124 ndefinition nat77 ≝ S nat76.
 125 ndefinition nat78 ≝ S nat77.
 126 ndefinition nat79 ≝ S nat78.
 127 ndefinition nat80 ≝ S nat79.
 128 ndefinition nat81 ≝ S nat80.
 129 ndefinition nat82 ≝ S nat81.
 130 ndefinition nat83 ≝ S nat82.
 131 ndefinition nat84 ≝ S nat83.
 132 ndefinition nat85 ≝ S nat84.
 133 ndefinition nat86 ≝ S nat85.
 134 ndefinition nat87 ≝ S nat86.
 135 ndefinition nat88 ≝ S nat87.
 136 ndefinition nat89 ≝ S nat88.
 137 ndefinition nat90 ≝ S nat89.
 138 ndefinition nat91 ≝ S nat90.
 139 ndefinition nat92 ≝ S nat91.
 140 ndefinition nat93 ≝ S nat92.
 141 ndefinition nat94 ≝ S nat93.
 142 ndefinition nat95 ≝ S nat94.
 143 ndefinition nat96 ≝ S nat95.
 144 ndefinition nat97 ≝ S nat96.
 145 ndefinition nat98 ≝ S nat97.
 146 ndefinition nat99 ≝ S nat98.
 147 ndefinition nat100 ≝ S nat99.
 148
 149 nlet rec eq_nat (n1,n2:nat) on n1 ≝
 150  match n1 with
 151   [ O ⇒ match n2 with [ O ⇒ true | S _ ⇒ false ]
 152   | S n1' ⇒ match n2 with [ O ⇒ false | S n2' ⇒ eq_nat n1' n2' ]
 153   ].
 154
 155 nlet rec le_nat n m ≝
 156  match n with
 157   [ O ⇒ true
 158   | (S p) ⇒ match m with
 159    [ O ⇒ false | (S q) ⇒ le_nat p q ]
 160   ].
 161
 162 interpretation "natural 'less or equal to'" 'leq x y = (le_nat x y).
 163
 164 ndefinition lt_nat ≝ λn1,n2:nat.(le_nat n1 n2) ⊗ (⊖ (eq_nat n1 n2)).
 165
 166 interpretation "natural 'less than'" 'lt x y = (lt_nat x y).
 167
 168 ndefinition ge_nat ≝ λn1,n2:nat.(⊖ (le_nat n1 n2)) ⊕ (eq_nat n1 n2).
 169
 170 interpretation "natural 'greater or equal to'" 'geq x y = (ge_nat x y).
 171
 172 ndefinition gt_nat ≝ λn1,n2:nat.⊖ (le_nat n1 n2).
 173
 174 interpretation "natural 'greater than'" 'gt x y = (gt_nat x y).
 175
 176 nlet rec plus (n1,n2:nat) on n1 ≝
 177  match n1 with
 178   [ O ⇒ n2
 179   | (S n1') ⇒ S (plus n1' n2) ].
 180
 181 interpretation "natural plus" 'plus x y = (plus x y).
 182
 183 nlet rec times (n1,n2:nat) on n1 ≝
 184  match n1 with
 185   [ O ⇒ O
 186   | (S n1') ⇒ n2 + (times n1' n2) ].
 187
 188 interpretation "natural times" 'times x y = (times x y).
 189
 190 nlet rec minus n m ≝
 191  match n with
 192  [ O ⇒ O
 193  | (S p) ⇒
 194         match m with
 195         [O ⇒ (S p)
 196   | (S q) ⇒ minus p q ]].
 197
 198 interpretation "natural minus" 'minus x y = (minus x y).
 199
 200 nlet rec div_aux p m n : nat ≝
 201 match (le_nat m n) with
 202 [ true ⇒ O
 203 | false ⇒
 204   match p with
 205   [ O ⇒ O
 206   | (S q) ⇒ S (div_aux q (m-(S n)) n)]].
 207
 208 ndefinition div : nat → nat → nat ≝
 209 λn,m.match m with
 210  [ O ⇒ S n
 211  | (S p) ⇒ div_aux n n p].
 212
 213 interpretation "natural divide" 'divide x y = (div x y).
 214
 215 ndefinition pred ≝ λn.match n with [ O ⇒ O | S n ⇒ n ].
 216
 217 ndefinition nat128 ≝ nat64 + nat64.
 218 ndefinition nat256 ≝ nat128 + nat128.
 219 ndefinition nat512 ≝ nat256 + nat256.
 220 ndefinition nat1024 ≝ nat512 + nat512.
 221 ndefinition nat2048 ≝ nat1024 + nat1024.
 222 ndefinition nat4096 ≝ nat2048 + nat2048.
 223 ndefinition nat8192 ≝ nat4096 + nat4096.
 224 ndefinition nat16384 ≝ nat8192 + nat8192.
 225 ndefinition nat32768 ≝ nat16384 + nat16384.
 226 ndefinition nat65536 ≝ nat32768 + nat32768.
 227
 228 nlemma nat_destruct_S_S : ∀n1,n2:nat.S n1 = S n2 → n1 = n2.
 229  #n1; #n2; #H;
 230  nchange with (match S n2 with [ O ⇒ False | S a ⇒ n1 = a ]);
 231  nrewrite < H;
 232  nnormalize;
 233  napply refl_eq.
 234 nqed.
 235
 236 nlemma nat_destruct_0_S : ∀n:nat.O = S n → False.
 237  #n; #H;
 238  nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
 239  nrewrite < H;
 240  nnormalize;
 241  napply I.
 242 nqed.
 243
 244 nlemma nat_destruct_S_0 : ∀n:nat.S n = O → False.
 245  #n; #H;
 246  nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
 247  nrewrite > H;
 248  nnormalize;
 249  napply I.
 250 nqed.
 251
 252 nlemma eq_to_eqnat : ∀n1,n2:nat.n1 = n2 → eq_nat n1 n2 = true.
 253  #n1;
 254  nelim n1;
 255  ##[ ##1: #n2;
 256           nelim n2;
 257           nnormalize;
 258           ##[ ##1: #H; napply refl_eq
 259           ##| ##2: #n3; #H; #H1; ndestruct (*nelim (nat_destruct_0_S ? H1)*)
 260           ##]
 261  ##| ##2: #n2; #H; #n3; #H1;
 262           ncases n3 in H1:(%) ⊢ %;
 263           nnormalize;
 264           ##[ ##1: #H1; ndestruct (*nelim (nat_destruct_S_0 ? H1)*)
 265           ##| ##2: #n4; #H1;
 266                    napply (H n4 (nat_destruct_S_S … H1))
 267           ##]
 268  ##]
 269 nqed.
 270
 271 nlemma neqnat_to_neq : ∀n1,n2:nat.(eq_nat n1 n2 = false → n1 ≠ n2).
 272  #n1; #n2; #H;
 273  napply (not_to_not (n1 = n2) (eq_nat n1 n2 = true) …);
 274  ##[ ##1: napply (eq_to_eqnat n1 n2)
 275  ##| ##2: napply (eqfalse_to_neqtrue … H)
 276  ##]
 277 nqed.
 278
 279 nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2).
 280  #n1;
 281  nelim n1;
 282  ##[ ##1: #n2;
 283           nelim n2;
 284           nnormalize;
 285           ##[ ##1: #H; napply refl_eq
 286           ##| ##2: #n3; #H; #H1; ndestruct (*napply (bool_destruct … (O = S n3) H1)*)
 287           ##]
 288  ##| ##2: #n2; #H; #n3; #H1;
 289           ncases n3 in H1:(%) ⊢ %;
 290           nnormalize;
 291           ##[ ##1: #H1; ndestruct (*napply (bool_destruct … (S n2 = O) H1)*)
 292           ##| ##2: #n4; #H1;
 293                    nrewrite > (H n4 H1);
 294                    napply refl_eq
 295           ##]
 296  ##]
 297 nqed.
 298
 299 nlemma neq_to_neqnat : ∀n1,n2:nat.n1 ≠ n2 → eq_nat n1 n2 = false.
 300  #n1; #n2; #H;
 301  napply (neqtrue_to_eqfalse (eq_nat n1 n2));
 302  napply (not_to_not (eq_nat n1 n2 = true) (n1 = n2) ? H);
 303  napply (eqnat_to_eq n1 n2).
 304 nqed.
 305
 306 nlemma decidable_nat : ∀x,y:nat.decidable (x = y).
 307  #x; #y; nnormalize;
 308  napply (or2_elim (eq_nat x y = true) (eq_nat x y = false) ? (decidable_bexpr ?));
 309  ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqnat_to_eq … H))
 310  ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqnat_to_neq … H))
 311  ##]
 312 nqed.
 313
 314 nlemma symmetric_eqnat : symmetricT nat bool eq_nat.
 315  #n1; #n2;
 316  napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_nat n1 n2));
 317  ##[ ##1: #H; nrewrite > H; napply refl_eq
 318  ##| ##2: #H; nrewrite > (neq_to_neqnat n1 n2 H);
 319           napply (symmetric_eq ? (eq_nat n2 n1) false);
 320           napply (neq_to_neqnat n2 n1 (symmetric_neq ? n1 n2 H))
 321  ##]
 322 nqed.
 323
 324 nlemma Sn_p_n_to_S_npn : ∀n1,n2.(S n1) + n2 = S (n1 + n2).
 325  #n1;
 326  nelim n1;
 327  ##[ ##1: nnormalize; #n2; napply refl_eq
 328  ##| ##2: #n; #H; #n2; nrewrite > (H n2);
 329           ncases n in H:(%) ⊢ %;
 330           ##[ ##1: nnormalize; #H; napply refl_eq
 331           ##| ##2: #n3; nnormalize; #H; napply refl_eq
 332           ##]
 333  ##]
 334 nqed.
 335
 336 nlemma n_p_Sn_to_S_npn : ∀n1,n2.n1 + (S n2) = S (n1 + n2).
 337  #n1;
 338  nelim n1;
 339  ##[ ##1: nnormalize; #n2; napply refl_eq
 340  ##| ##2: #n; #H; #n2;
 341           nrewrite > (Sn_p_n_to_S_npn n (S n2));
 342           nrewrite > (H n2);
 343           napply refl_eq
 344  ##]
 345 nqed.
 346
 347 nlemma Opn_to_n : ∀n.O + n = n.
 348  #n; nnormalize; napply refl_eq.
 349 nqed.
 350
 351 nlemma npO_to_n : ∀n.n + O = n.
 352  #n;
 353  nelim n;
 354  ##[ ##1: nnormalize; napply refl_eq
 355  ##| ##2: #n1; #H;
 356           nrewrite > (Sn_p_n_to_S_npn n1 O);
 357           nrewrite > H;
 358           napply refl_eq
 359  ##]
 360 nqed.
 361
 362 nlemma symmetric_plusnat : symmetricT nat nat plus.
 363  #n1;
 364  nelim n1;
 365  ##[ ##1: #n2; nrewrite > (npO_to_n n2); nnormalize; napply refl_eq
 366  ##| ##2: #n2; #H; #n3;
 367           nrewrite > (Sn_p_n_to_S_npn n2 n3);
 368           nrewrite > (n_p_Sn_to_S_npn n3 n2);
 369           nrewrite > (H n3);
 370           napply refl_eq
 371  ##]
 372 nqed.
 373
 374 nlemma nat_is_comparable : comparable.
 375  napply (mk_comparable nat);
 376  ##[ napply O
 377  ##| napply (λx.false)
 378  ##| napply eq_nat
 379  ##| napply eqnat_to_eq
 380  ##| napply eq_to_eqnat
 381  ##| napply neqnat_to_neq
 382  ##| napply neq_to_neqnat
 383  ##| napply decidable_nat
 384  ##| napply symmetric_eqnat
 385  ##]
 386 nqed.
 387
 388 unification hint 0 ≔ ⊢ carr nat_is_comparable ≡ nat.