helm/matita/library/nat/nat.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/nat/nat".
  16
  17 include "logic/equality.ma".
  18 include "logic/connectives.ma".
  19 include "higher_order_defs/functions.ma".
  20
  21 inductive nat : Set \def
  22   | O : nat
  23   | S : nat \to nat.
  24
  25 definition pred: nat \to nat \def
  26 \lambda n:nat. match n with
  27 [ O \Rightarrow  O
  28 | (S p) \Rightarrow p ].
  29
  30 theorem pred_Sn : \forall n:nat.n=(pred (S n)).
  31 intros; reflexivity.
  32 qed.
  33
  34 theorem injective_S : injective nat nat S.
  35 simplify.
  36 intros.
  37 rewrite > pred_Sn.
  38 rewrite > pred_Sn y.
  39 apply eq_f. assumption.
  40 qed.
  41
  42 theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m
  43 \def injective_S.
  44
  45 theorem not_eq_S  : \forall n,m:nat.
  46 \lnot n=m \to \lnot (S n = S m).
  47 intros. simplify. intros.
  48 apply H. apply injective_S. assumption.
  49 qed.
  50
  51 definition not_zero : nat \to Prop \def
  52 \lambda n: nat.
  53   match n with
  54   [ O \Rightarrow False
  55   | (S p) \Rightarrow True ].
  56
  57 theorem not_eq_O_S : \forall n:nat. \lnot O=S n.
  58 intros. simplify. intros.
  59 cut (not_zero O).
  60 exact Hcut.
  61 rewrite > H.exact I.
  62 qed.
  63
  64 theorem not_eq_n_Sn : \forall n:nat. \lnot n=S n.
  65 intros.elim n.
  66 apply not_eq_O_S.
  67 apply not_eq_S.assumption.
  68 qed.
  69
  70 theorem nat_case:
  71 \forall n:nat.\forall P:nat \to Prop.
  72 P O \to  (\forall m:nat. P (S m)) \to P n.
  73 intros.elim n.assumption.apply H1.
  74 qed.
  75
  76 theorem nat_elim2 :
  77 \forall R:nat \to nat \to Prop.
  78 (\forall n:nat. R O n) \to
  79 (\forall n:nat. R (S n) O) \to
  80 (\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m.
  81 intros 5.elim n.
  82 apply H.
  83 apply nat_case m.apply H1.
  84 intros.apply H2. apply H3.
  85 qed.
  86