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 "datatypes/bool.ma".
  20 include "higher_order_defs/functions.ma".
  21
  22 inductive nat : Set \def
  23   | O : nat
  24   | S : nat \to nat.
  25
  26 definition pred: nat \to nat \def
  27 \lambda n:nat. match n with
  28 [ O \Rightarrow  O
  29 | (S p) \Rightarrow p ].
  30
  31 theorem pred_Sn : \forall n: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.(S n)=(S m) \to n=m
  44 \def injective_S.
  45
  46 theorem not_eq_S  : \forall n,m:nat.
  47 \lnot n=m \to \lnot (S n = S m).
  48 intros. simplify. intros.
  49 apply H. apply injective_S. assumption.
  50 qed.
  51
  52 definition not_zero : nat \to Prop \def
  53 \lambda n: nat.
  54   match n with
  55   [ O \Rightarrow False
  56   | (S p) \Rightarrow True ].
  57
  58 theorem not_eq_O_S : \forall n:nat. \lnot O=S n.
  59 intros. simplify. intros.
  60 cut (not_zero O).
  61 exact Hcut.
  62 rewrite > H.exact I.
  63 qed.
  64
  65 theorem not_eq_n_Sn : \forall n:nat. \lnot n=S n.
  66 intros.elim n.
  67 apply not_eq_O_S.
  68 apply not_eq_S.assumption.
  69 qed.
  70
  71 theorem nat_case:
  72 \forall n:nat.\forall P:nat \to Prop.
  73 P O \to  (\forall m:nat. P (S m)) \to P n.
  74 intros.elim n.assumption.apply H1.
  75 qed.
  76
  77 theorem nat_elim2 :
  78 \forall R:nat \to nat \to Prop.
  79 (\forall n:nat. R O n) \to
  80 (\forall n:nat. R (S n) O) \to
  81 (\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m.
  82 intros 5.elim n.
  83 apply H.
  84 apply nat_case m.apply H1.
  85 intros.apply H2. apply H3.
  86 qed.
  87
  88 theorem decidable_eq_nat : \forall n,m:nat.decidable (n=m).
  89 intros.simplify.
  90 apply nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False))).
  91 intro.elim n1.
  92 left.reflexivity.
  93 right.apply not_eq_O_S.
  94 intro.right.intro.
  95 apply not_eq_O_S n1 ?.
  96 apply sym_eq.assumption.
  97 intros.elim H.
  98 left.apply eq_f. assumption.
  99 right.intro.apply H1.apply inj_S.assumption.
 100 qed.
 101