]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/nat.ma
- libraryObjects: new default "natural numbers" with the uri of nat.
[helm.git] / 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 include "higher_order_defs/functions.ma".
16
17 inductive nat : Set \def
18   | O : nat
19   | S : nat \to nat.
20
21 interpretation "Natural numbers" 'N = nat.
22
23 default "natural numbers" cic:/matita/nat/nat/nat.ind.
24
25 alias num (instance 0) = "natural number".
26
27 definition pred: nat \to nat \def
28  \lambda n:nat. match n with
29  [ O \Rightarrow  O
30  | (S p) \Rightarrow p ].
31
32 theorem pred_Sn : \forall n:nat.n=(pred (S n)).
33  intros. simplify. reflexivity.
34 qed.
35
36 theorem injective_S : injective nat nat S.
37  unfold injective.
38  intros.
39  rewrite > pred_Sn.
40  rewrite > (pred_Sn y).
41  apply eq_f. assumption.
42 qed.
43
44 theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m \def
45  injective_S.
46
47 theorem not_eq_S  : \forall n,m:nat. 
48  \lnot n=m \to S n \neq S m.
49  intros. unfold Not. 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. O \neq S n.
60  intros. unfold Not. 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. n \neq 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
76   [ assumption
77   | apply H1 ]
78 qed.
79
80 theorem nat_case1:
81  \forall n:nat.\forall P:nat \to Prop. 
82   (n=O \to P O) \to  (\forall m:nat. (n=(S m) \to P (S m))) \to P n.
83 intros 2; elim n
84   [ apply H;reflexivity
85   | apply H2;reflexivity ]
86 qed.
87
88 theorem nat_elim2 :
89  \forall R:nat \to nat \to Prop.
90   (\forall n:nat. R O n) 
91   \to (\forall n:nat. R (S n) O) 
92   \to (\forall n,m:nat. R n m \to R (S n) (S m))
93   \to \forall n,m:nat. R n m.
94 intros 5;elim n 
95   [ apply H
96   | apply (nat_case m)
97     [ apply H1
98     | intro; apply H2; apply H3 ] ]
99 qed.
100
101 theorem decidable_eq_nat : \forall n,m:nat.decidable (n=m).
102  intros.unfold decidable.
103  apply (nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False))))
104  [ intro; elim n1
105    [ left; reflexivity
106    | right; apply not_eq_O_S ]
107  | intro; right; intro; apply (not_eq_O_S n1); apply sym_eq; assumption
108  | intros; elim H
109    [ left; apply eq_f; assumption
110    | right; intro; apply H1; apply inj_S; assumption ] ]
111 qed.