weblib/lroversi/nat.ma

   1 include "hints_declaration.ma".
   2 include "basics/eq.ma".
   3
   4 ninductive nat : Type ≝
   5   | O : nat
   6   | S : nat → nat.
   7
   8 interpretation "Natural numbers" 'N = nat.
   9
  10 alias num (instance 0) = "nnatural number".
  11
  12 (*
  13 nrecord pos : Type ≝
  14  {n:>nat; is_pos: n ≠ 0}.
  15
  16 ncoercion nat_to_pos: ∀n:nat. n ≠0 →pos ≝ mk_pos on
  17 *)
  18
  19 (* default "natural numbers" cic:/matita/ng/arithmetics/nat/nat.ind.
  20 *)
  21
  22 ndefinition pred ≝
  23  λn. match n with [ O ⇒ O | S p ⇒ p].
  24
  25 ntheorem pred_Sn : ∀n. n = pred (S n).
  26 //; nqed.
  27
  28 ntheorem injective_S : injective nat nat S.
  29 //; nqed.
  30
  31 (*
  32 ntheorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m.
  33 //. nqed. *)
  34
  35 ntheorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
  36 /3/; nqed.
  37
  38 ndefinition not_zero: nat → Prop ≝
  39  λn: nat. match n with
  40   [ O ⇒ False | (S p) ⇒ True ].
  41
  42 ntheorem not_eq_O_S : ∀n:nat. O ≠ S n.
  43 #n; napply nmk; #eqOS; nchange with (not_zero O);
  44 nrewrite > eqOS; //.
  45 nqed.
  46
  47 ntheorem not_eq_n_Sn: ∀n:nat. n ≠ S n.
  48 #n; nelim n;/2/; nqed.
  49
  50 ntheorem nat_case:
  51  ∀n:nat.∀P:nat → Prop.
  52   (n=O → P O) → (∀m:nat. (n=(S m) → P (S m))) → P n.
  53 #n; #P; nelim n; /2/; nqed.
  54
  55 ntheorem nat_elim2 :
  56  ∀R:nat → nat → Prop.
  57   (∀n:nat. R O n)
  58   → (∀n:nat. R (S n) O)
  59   → (∀n,m:nat. R n m → R (S n) (S m))
  60   → ∀n,m:nat. R n m.
  61 #R; #ROn; #RSO; #RSS; #n; nelim n;//;
  62 #n0; #Rn0m; #m; ncases m;/2/; nqed.
  63
  64 ntheorem decidable_eq_nat : ∀n,m:nat.decidable (n=m).
  65 napply nat_elim2; #n;
  66  ##[ ncases n; /2/;
  67  ##| /3/;
  68  ##| #m; #Hind; ncases Hind;/3/;
  69  ##]
  70 nqed.