]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/arith/ynat_succ.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / ynat_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_succ.ma".
16 include "ground/arith/ynat_nat.ma".
17
18 (* SUCCESSOR FOR NON-NEGATIVE INTEGERS WITH INFINITY ************************)
19
20 definition ysucc_aux (n): ynat ≝
21            yinj_nat (↑n).
22
23 (*** ysucc *)
24 definition ysucc: ynat → ynat ≝
25            ynat_bind_nat ysucc_aux (∞).
26
27 interpretation
28   "successor (non-negative integers with infinity)"
29   'UpArrow x = (ysucc x).
30
31 (* Constructions ************************************************************)
32
33 (*** ysucc_inj *)
34 lemma ysucc_inj (n): yinj_nat (↑n) = ↑(yinj_nat n).
35 @(ynat_bind_nat_inj ysucc_aux)
36 qed.
37
38 (*** ysucc_Y *)
39 lemma ysucc_inf: ∞ = ↑(∞).
40 // qed.
41
42 (* Inversions ***************************************************************)
43
44 (*** ysucc_inv_inj_sn *)
45 lemma eq_inv_inj_ysucc (n1) (x2):
46       yinj_nat n1 = ↑x2 →
47       ∃∃n2. yinj_nat n2 = x2 & ↑n2 = n1.
48 #n1 #x2 @(ynat_split_nat_inf … x2) -x2
49 [ /3 width=3 by eq_inv_yinj_nat_bi, ex2_intro/
50 | #H elim (eq_inv_yinj_nat_inf … H)
51 ]
52 qed-.
53
54 (*** ysucc_inv_inj_dx *)
55 lemma eq_inv_ysucc_inj (x1) (n2):
56       ↑x1 = yinj_nat n2  →
57       ∃∃n1. yinj_nat n1 = x1 & ↑n1 = n2.
58 /2 width=1 by eq_inv_inj_ysucc/ qed-.
59
60 (*** ysucc_inv_Y_sn *)
61 lemma eq_inv_inf_ysucc (x2): ∞ = ↑x2 → ∞ = x2.
62 #x2 @(ynat_split_nat_inf … x2) -x2 //
63 #n1 <ysucc_inj #H elim (eq_inv_inf_yinj_nat … H)
64 qed-.
65
66 (*** ysucc_inv_Y_dx *)
67 lemma eq_inv_ysucc_inf (x1): ↑x1 = ∞ → ∞ = x1.
68 /2 width=1 by eq_inv_inf_ysucc/ qed-.
69
70 (*** ysucc_inv_inj *)
71 lemma eq_inv_ysucc_bi: injective … ysucc.
72 #x1 @(ynat_split_nat_inf … x1) -x1
73 [ #n1 #x2 <ysucc_inj #H
74   elim (eq_inv_inj_ysucc … H) -H #n2 #H1 #H2 destruct
75   <(eq_inv_nsucc_bi … H2) -H2 //
76 | #x2 #H <(eq_inv_inf_ysucc … H) -H //
77 ]
78 qed-.
79
80 (*** ysucc_inv_refl *)
81 lemma ysucc_inv_refl (x): x = ↑x → ∞ = x.
82 #x @(ynat_split_nat_inf … x) -x //
83 #n <ysucc_inj #H
84 lapply (eq_inv_yinj_nat_bi … H) -H #H
85 elim (nsucc_inv_refl … H)
86 qed-.
87
88 (*** ysucc_inv_O_sn *)
89 lemma eq_inv_zero_ysucc (x): 𝟎 = ↑x → ⊥.
90 #x #H
91 elim (eq_inv_inj_ysucc (𝟎) ? H) -H #n #_ #H
92 /2 width=2 by eq_inv_zero_nsucc/
93 qed-.
94
95 (*** ysucc_inv_O_dx *)
96 lemma eq_inv_ysucc_zero (x): ↑x = 𝟎 → ⊥.
97 /2 width=2 by eq_inv_zero_ysucc/ qed-.
98
99 (* Eliminations *************************************************************)
100
101 (*** ynat_ind *)
102 lemma ynat_ind_succ (Q:predicate …):
103       Q (𝟎) → (∀n:nat. Q (yinj_nat n) → Q (↑(yinj_nat n))) → Q (∞) → ∀x. Q x.
104 #Q #IH1 #IH2 #IH3 #x @(ynat_split_nat_inf … x) -x //
105 #n @(nat_ind_succ … n) -n /2 width=1 by/
106 qed-.