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