]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_succ.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "ground/arith/nat.ma".
16
17 (* SUCCESSOR FOR NON-NEGATIVE INTEGERS **************************************)
18
19 definition npsucc (m): pnat ≝
20 match m with
21 [ nzero  ⇒ 𝟏
22 | ninj p ⇒ ↑p
23 ].
24
25 interpretation
26   "positive successor (non-negative integers)"
27   'UpArrow m = (npsucc m).
28
29 definition nsucc (m): nat ≝
30            ninj (↑m).
31
32 interpretation
33   "successor (non-negative integers)"
34   'UpArrow m = (nsucc m).
35
36 (* Basic constructions ******************************************************)
37
38 lemma npsucc_zero: (𝟏) = ↑𝟎.
39 // qed.
40
41 lemma npsucc_inj (p): (↑p) = ↑(ninj p).
42 // qed.
43
44 lemma nsucc_zero: ninj (𝟏) = ↑𝟎.
45 // qed.
46
47 lemma nsucc_inj (p): ninj (↑p) = ↑(ninj p).
48 // qed.
49
50 lemma npsucc_succ (n): psucc (npsucc n) = npsucc (nsucc n).
51 // qed.
52
53 (* Basic eliminations *******************************************************)
54
55 (*** nat_ind *)
56 lemma nat_ind_succ (Q:predicate …):
57       Q (𝟎) → (∀n. Q n → Q (↑n)) → ∀n. Q n.
58 #Q #IH1 #IH2 * //
59 #p elim p -p /2 width=1 by/
60 qed-.
61
62 (*** nat_elim2 *)
63 lemma nat_ind_2_succ (Q:relation2 …):
64       (∀n. Q (𝟎) n) →
65       (∀m. Q m (𝟎) → Q (↑m) (𝟎)) →
66       (∀m,n. Q m n → Q (↑m) (↑n)) →
67       ∀m,n. Q m n.
68 #Q #IH1 #IH2 #IH3 #m @(nat_ind_succ … m) -m [ // ]
69 #m #IH #n @(nat_ind_succ … n) -n /2 width=1 by/
70 qed-.
71
72 (* Basic inversions *********************************************************)
73
74 lemma eq_inv_npsucc_bi: injective … npsucc.
75 * [| #p1 ] * [2,4: #p2 ]
76 [ 1,4: <npsucc_zero <npsucc_inj #H destruct
77 | <npsucc_inj <npsucc_inj #H destruct //
78 | //
79 ]
80 qed-.
81
82 (*** injective_S *)
83 lemma eq_inv_nsucc_bi: injective … nsucc.
84 #n1 #n2 #H
85 @eq_inv_npsucc_bi @eq_inv_ninj_bi @H
86 qed-.
87
88 lemma eq_inv_nsucc_zero (m): ↑m = 𝟎 → ⊥.
89 * [ <nsucc_zero | #p <nsucc_inj ] #H destruct
90 qed-.
91
92 lemma eq_inv_zero_nsucc (m): 𝟎 = ↑m → ⊥.
93 * [ <nsucc_zero | #p <nsucc_inj ] #H destruct
94 qed-.
95
96 (*** succ_inv_refl_sn *)
97 lemma nsucc_inv_refl (n): n = ↑n → ⊥.
98 #n @(nat_ind_succ … n) -n
99 [ /2 width=2 by eq_inv_zero_nsucc/
100 | #n #IH #H /3 width=1 by eq_inv_nsucc_bi/
101 ]
102 qed-.