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