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