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.
  31 (eq nat n (pred (S n))).
  32 intros; reflexivity.
  33 qed.
  34
  35 theorem injective_S : injective nat nat S.
  36 simplify.
  37 intros.
  38 rewrite > pred_Sn.
  39 rewrite > pred_Sn y.
  40 apply eq_f. assumption.
  41 qed.
  42
  43 theorem inj_S : \forall n,m:nat.
  44 (eq nat (S n) (S m)) \to (eq nat n m)
  45 \def injective_S.
  46
  47 theorem not_eq_S  : \forall n,m:nat.
  48 Not (eq nat n m) \to Not (eq nat (S n) (S m)).
  49 intros. simplify. intros.
  50 apply H. apply injective_S. assumption.
  51 qed.
  52
  53 definition not_zero : nat \to Prop \def
  54 \lambda n: nat.
  55   match n with
  56   [ O \Rightarrow False
  57   | (S p) \Rightarrow True ].
  58
  59 theorem not_eq_O_S : \forall n:nat. Not (eq nat O (S n)).
  60 intros. simplify. intros.
  61 cut (not_zero O).
  62 exact Hcut.
  63 rewrite > H.exact I.
  64 qed.
  65
  66 theorem not_eq_n_Sn : \forall n:nat. Not (eq nat n (S n)).
  67 intros.elim n.
  68 apply not_eq_O_S.
  69 apply not_eq_S.assumption.
  70 qed.
  71
  72 theorem nat_case:
  73 \forall n:nat.\forall P:nat \to Prop.
  74 P O \to  (\forall m:nat. P (S m)) \to P n.
  75 intros.elim n.assumption.apply H1.
  76 qed.
  77
  78 theorem nat_elim2 :
  79 \forall R:nat \to nat \to Prop.
  80 (\forall n:nat. R O n) \to
  81 (\forall n:nat. R (S n) O) \to
  82 (\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m.
  83 intros 5.elim n.
  84 apply H.
  85 apply nat_case m.apply H1.
  86 intros.apply H2. apply H3.
  87 qed.
  88