]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/relocation/pr_nat.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_nat.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/notation/relations/ratsucc_3.ma".
16 include "ground/arith/nat_pred_succ.ma".
17 include "ground/relocation/pr_pat.ma".
18
19 (* NON-NEGATIVE APPLICATION FOR PARTIAL RELOCATION MAPS *********************)
20
21 definition pr_nat: relation3 pr_map nat nat ≝
22            λf,l1,l2. @❨↑l1,f❩ ≘ ↑l2.
23
24 interpretation
25   "relational non-negative application (partial relocation maps)"
26   'RAtSucc l1 f l2 = (pr_nat f l1 l2).
27
28 (* Basic constructions ******************************************************)
29
30 lemma pr_nat_refl (f) (g) (k1) (k2):
31       (⫯f) = g → 𝟎 = k1 → 𝟎 = k2 → @↑❨k1,g❩ ≘ k2.
32 #f #g #k1 #k2 #H1 #H2 #H3 destruct
33 /2 width=2 by pr_pat_refl/
34 qed.
35
36 lemma pr_nat_push (f) (l1) (l2) (g) (k1) (k2):
37       @↑❨l1,f❩ ≘ l2 → ⫯f = g → ↑l1 = k1 → ↑l2 = k2 → @↑❨k1,g❩ ≘ k2.
38 #f #l1 #l2 #g #k1 #k2 #Hf #H1 #H2 #H3 destruct
39 /2 width=7 by pr_pat_push/
40 qed.
41
42 lemma pr_nat_next (f) (l1) (l2) (g) (k2):
43       @↑❨l1,f❩ ≘ l2 → ↑f = g → ↑l2 = k2 → @↑❨l1,g❩ ≘ k2.
44 #f #l1 #l2 #g #k2 #Hf #H1 #H2 destruct
45 /2 width=5 by pr_pat_next/
46 qed.
47
48 lemma pr_nat_pred_bi (f) (i1) (i2):
49       @❨i1,f❩ ≘ i2 → @↑❨↓i1,f❩ ≘ ↓i2.
50 #f #i1 #i2
51 >(npsucc_pred i1) in ⊢ (%→?); >(npsucc_pred i2) in ⊢ (%→?);
52 //
53 qed.
54
55 (* Basic inversions *********************************************************)
56
57 (*** pr_nat_inv_ppx *)
58 lemma pr_nat_inv_zero_push (f) (l1) (l2):
59       @↑❨l1,f❩ ≘ l2 → ∀g. 𝟎 = l1 → ⫯g = f → 𝟎 = l2.
60 #f #l1 #l2 #H #g #H1 #H2 destruct
61 lapply (pr_pat_inv_unit_push … H ???) -H
62 /2 width=2 by eq_inv_npsucc_bi/
63 qed-.
64
65 (*** pr_nat_inv_npx *)
66 lemma pr_nat_inv_succ_push (f) (l1) (l2):
67       @↑❨l1,f❩ ≘ l2 → ∀g,k1. ↑k1 = l1 → ⫯g = f →
68       ∃∃k2. @↑❨k1,g❩ ≘ k2 & ↑k2 = l2.
69 #f #l1 #l2 #H #g #k1 #H1 #H2 destruct
70 elim (pr_pat_inv_succ_push … H) -H [|*: // ] #k2 #Hg
71 >(npsucc_pred (↑l2)) #H
72 @(ex2_intro … (↓k2)) //
73 qed-.
74
75 (*** pr_nat_inv_xnx *)
76 lemma pr_nat_inv_next (f) (l1) (l2):
77       @↑❨l1,f❩ ≘ l2 → ∀g. ↑g = f →
78       ∃∃k2. @↑❨l1,g❩ ≘ k2 & ↑k2 = l2.
79 #f #l1 #l2 #H #g #H1 destruct
80 elim (pr_pat_inv_next … H) -H [|*: // ] #k2
81 >(npsucc_pred (k2)) in ⊢ (%→?→?); #Hg #H
82 @(ex2_intro … (↓k2)) //
83 qed-.
84
85 (* Advanced inversions ******************************************************)
86
87 (*** pr_nat_inv_ppn *)
88 lemma pr_nat_inv_zero_push_succ (f) (l1) (l2):
89       @↑❨l1,f❩ ≘ l2 → ∀g,k2. 𝟎 = l1 → ⫯g = f → ↑k2 = l2 → ⊥.
90 #f #l1 #l2 #Hf #g #k2 #H1 #H <(pr_nat_inv_zero_push … Hf … H1 H) -f -g -l1 -l2
91 /2 width=3 by eq_inv_nsucc_zero/
92 qed-.
93
94 (*** pr_nat_inv_npp *)
95 lemma pr_nat_inv_succ_push_zero (f) (l1) (l2):
96       @↑❨l1,f❩ ≘ l2 → ∀g,k1. ↑k1 = l1 → ⫯g = f → 𝟎 = l2 → ⊥.
97 #f #l1 #l2 #Hf #g #k1 #H1 #H elim (pr_nat_inv_succ_push … Hf … H1 H) -f -l1
98 #x2 #Hg * -l2 /2 width=3 by eq_inv_zero_nsucc/
99 qed-.
100
101 (*** pr_nat_inv_npn *)
102 lemma pr_nat_inv_succ_push_succ (f) (l1) (l2):
103       @↑❨l1,f❩ ≘ l2 → ∀g,k1,k2. ↑k1 = l1 → ⫯g = f → ↑k2 = l2 → @↑❨k1,g❩ ≘ k2.
104 #f #l1 #l2 #Hf #g #k1 #k2 #H1 #H elim (pr_nat_inv_succ_push … Hf … H1 H) -f -l1
105 #x2 #Hg * -l2 #H >(eq_inv_nsucc_bi … H) -k2 //
106 qed-.
107
108 (*** pr_nat_inv_xnp *)
109 lemma pr_nat_inv_next_zero (f) (l1) (l2):
110       @↑❨l1,f❩ ≘ l2 → ∀g. ↑g = f → 𝟎 = l2 → ⊥.
111 #f #l1 #l2 #Hf #g #H elim (pr_nat_inv_next … Hf … H) -f
112 #x2 #Hg * -l2 /2 width=3 by eq_inv_zero_nsucc/
113 qed-.
114
115 (*** pr_nat_inv_xnn *)
116 lemma pr_nat_inv_next_succ (f) (l1) (l2):
117       @↑❨l1,f❩ ≘ l2 → ∀g,k2. ↑g = f → ↑k2 = l2 → @↑❨l1,g❩ ≘ k2.
118 #f #l1 #l2 #Hf #g #k2 #H elim (pr_nat_inv_next … Hf … H) -f
119 #x2 #Hg * -l2 #H >(eq_inv_nsucc_bi … H) -k2 //
120 qed-.
121
122 (*** pr_nat_inv_pxp *)
123 lemma pr_nat_inv_zero_bi (f) (l1) (l2):
124       @↑❨l1,f❩ ≘ l2 → 𝟎 = l1 → 𝟎 = l2 → ∃g. ⫯g = f.
125 #f elim (pr_map_split_tl … f) /2 width=2 by ex_intro/
126 #H #l1 #l2 #Hf #H1 #H2 cases (pr_nat_inv_next_zero … Hf … H H2)
127 qed-.
128
129 (*** pr_nat_inv_pxn *)
130 lemma pr_nat_inv_zero_succ (f) (l1) (l2):
131       @↑❨l1,f❩ ≘ l2 → ∀k2. 𝟎 = l1 → ↑k2 = l2 →
132       ∃∃g. @↑❨l1,g❩ ≘ k2 & ↑g = f.
133 #f elim (pr_map_split_tl … f)
134 #H #l1 #l2 #Hf #k2 #H1 #H2
135 [ elim (pr_nat_inv_zero_push_succ … Hf … H1 H H2)
136 | /3 width=5 by pr_nat_inv_next_succ, ex2_intro/
137 ]
138 qed-.
139
140 (*** pr_nat_inv_nxp *)
141 lemma pr_nat_inv_succ_zero (f) (l1) (l2):
142       @↑❨l1,f❩ ≘ l2 → ∀k1. ↑k1 = l1 → 𝟎 = l2 → ⊥.
143 #f elim (pr_map_split_tl f)
144 #H #l1 #l2 #Hf #k1 #H1 #H2
145 [ elim (pr_nat_inv_succ_push_zero … Hf … H1 H H2)
146 | elim (pr_nat_inv_next_zero … Hf … H H2)
147 ]
148 qed-.
149
150 (*** pr_nat_inv_nxn *)
151 lemma pr_nat_inv_succ_bi (f) (l1) (l2):
152       @↑❨l1,f❩ ≘ l2 → ∀k1,k2. ↑k1 = l1 → ↑k2 = l2 →
153       ∨∨ ∃∃g. @↑❨k1,g❩ ≘ k2 & ⫯g = f
154        | ∃∃g. @↑❨l1,g❩ ≘ k2 & ↑g = f.
155 #f elim (pr_map_split_tl f) *
156 /4 width=7 by pr_nat_inv_next_succ, pr_nat_inv_succ_push_succ, ex2_intro, or_intror, or_introl/
157 qed-.
158
159 (* Note: the following inversion lemmas must be checked *)
160 (*** pr_nat_inv_xpx *)
161 lemma pr_nat_inv_push (f) (l1) (l2):
162       @↑❨l1,f❩ ≘ l2 → ∀g. ⫯g = f →
163       ∨∨ ∧∧ 𝟎 = l1 & 𝟎 = l2
164        | ∃∃k1,k2. @↑❨k1,g❩ ≘ k2 & ↑k1 = l1 & ↑k2 = l2.
165 #f * [2: #l1 ] #l2 #Hf #g #H
166 [ elim (pr_nat_inv_succ_push … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/
167 | >(pr_nat_inv_zero_push … Hf … H) -f /3 width=1 by conj, or_introl/
168 ]
169 qed-.
170
171 (*** pr_nat_inv_xpp *)
172 lemma pr_nat_inv_push_zero (f) (l1) (l2):
173       @↑❨l1,f❩ ≘ l2 → ∀g. ⫯g = f → 𝟎 = l2 → 𝟎 = l1.
174 #f #l1 #l2 #Hf #g #H elim (pr_nat_inv_push … Hf … H) -f * //
175 #k1 #k2 #_ #_ * -l2 #H elim (eq_inv_zero_nsucc … H)
176 qed-.
177
178 (*** pr_nat_inv_xpn *)
179 lemma pr_nat_inv_push_succ (f) (l1) (l2):
180       @↑❨l1,f❩ ≘ l2 → ∀g,k2. ⫯g = f → ↑k2 = l2 →
181       ∃∃k1. @↑❨k1,g❩ ≘ k2 & ↑k1 = l1.
182 #f #l1 #l2 #Hf #g #k2 #H elim (pr_nat_inv_push … Hf … H) -f *
183 [ #_ * -l2 #H elim (eq_inv_nsucc_zero … H)
184 | #x1 #x2 #Hg #H1 * -l2 #H
185   lapply (eq_inv_nsucc_bi … H) -H #H destruct
186   /2 width=3 by ex2_intro/
187 ]
188 qed-.
189
190 (*** pr_nat_inv_xxp *)
191 lemma pr_nat_inv_zero_dx (f) (l1) (l2):
192       @↑❨l1,f❩ ≘ l2 → 𝟎 = l2 → ∃∃g. 𝟎 = l1 & ⫯g = f.
193 #f elim (pr_map_split_tl f)
194 #H #l1 #l2 #Hf #H2
195 [ /3 width=6 by pr_nat_inv_push_zero, ex2_intro/
196 | elim (pr_nat_inv_next_zero … Hf … H H2)
197 ]
198 qed-.
199
200 (*** pr_nat_inv_xxn *)
201 lemma pr_nat_inv_succ_dx (f) (l1) (l2): @↑❨l1,f❩ ≘ l2 → ∀k2.  ↑k2 = l2 →
202       ∨∨ ∃∃g,k1. @↑❨k1,g❩ ≘ k2 & ↑k1 = l1 & ⫯g = f
203        | ∃∃g. @↑❨l1,g❩ ≘ k2 & ↑g = f.
204 #f elim (pr_map_split_tl f)
205 #H #l1 #l2 #Hf #k2 #H2
206 [ elim (pr_nat_inv_push_succ … Hf … H H2) -l2 /3 width=5 by or_introl, ex3_2_intro/
207 | lapply (pr_nat_inv_next_succ … Hf … H H2) -l2 /3 width=3 by or_intror, ex2_intro/
208 ]
209 qed-.