1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground_2/steps/rtc_ist_shift.ma".
16 include "ground_2/steps/rtc_ist_plus.ma".
17 include "ground_2/steps/rtc_ist_max.ma".
18 include "basic_2/notation/relations/pty_6.ma".
19 include "basic_2/rt_transition/cpg.ma".
21 (* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
23 definition cpt (h) (G) (L) (n): relation2 term term ≝
24 λT1,T2. ∃∃c. 𝐓⦃n,c⦄ & ⦃G,L⦄ ⊢ T1 ⬈[eq …,c,h] T2.
27 "t-bound context-sensitive parallel t-transition (term)"
28 'PTy h n G L T1 T2 = (cpt h G L n T1 T2).
30 (* Basic properties *********************************************************)
32 lemma cpt_ess (h) (G) (L):
33 ∀s. ⦃G,L⦄ ⊢ ⋆s ⬆[h,1] ⋆(⫯[h]s).
34 /2 width=3 by cpg_ess, ex2_intro/ qed.
36 lemma cpt_delta (h) (n) (G) (K):
37 ∀V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 →
38 ∀W2. ⇧*[1] V2 ≘ W2 → ⦃G,K.ⓓV1⦄ ⊢ #0 ⬆[h,n] W2.
40 /3 width=5 by cpg_delta, ex2_intro/
43 lemma cpt_ell (h) (n) (G) (K):
44 ∀V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 →
45 ∀W2. ⇧*[1] V2 ≘ W2 → ⦃G,K.ⓛV1⦄ ⊢ #0 ⬆[h,↑n] W2.
47 /3 width=5 by cpg_ell, ex2_intro, ist_succ/
50 lemma cpt_lref (h) (n) (G) (K):
51 ∀T,i. ⦃G,K⦄ ⊢ #i ⬆[h,n] T → ∀U. ⇧*[1] T ≘ U →
52 ∀I. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬆[h,n] U.
54 /3 width=5 by cpg_lref, ex2_intro/
57 lemma cpt_bind (h) (n) (G) (L):
58 ∀V1,V2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 → ∀I,T1,T2. ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ⬆[h,n] T2 →
59 ∀p. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ⬆[h,n] ⓑ{p,I}V2.T2.
60 #h #n #G #L #V1 #V2 * #cV #HcV #HV12 #I #T1 #T2 *
61 /3 width=5 by cpg_bind, ist_max_O1, ex2_intro/
64 lemma cpt_appl (h) (n) (G) (L):
65 ∀V1,V2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 →
66 ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ ⓐV1.T1 ⬆[h,n] ⓐV2.T2.
67 #h #n #G #L #V1 #V2 * #cV #HcV #HV12 #T1 #T2 *
68 /3 width=5 by ist_max_O1, cpg_appl, ex2_intro/
71 lemma cpt_cast (h) (n) (G) (L):
72 ∀U1,U2. ⦃G,L⦄ ⊢ U1 ⬆[h,n] U2 →
73 ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ ⓝU1.T1 ⬆[h,n] ⓝU2.T2.
74 #h #n #G #L #U1 #U2 * #cU #HcU #HU12 #T1 #T2 *
75 /3 width=6 by cpg_cast, ex2_intro/
78 lemma cpt_ee (h) (n) (G) (L):
79 ∀U1,U2. ⦃G,L⦄ ⊢ U1 ⬆[h,n] U2 → ∀T. ⦃G,L⦄ ⊢ ⓝU1.T ⬆[h,↑n] U2.
81 /3 width=3 by cpg_ee, ist_succ, ex2_intro/
84 lemma cpt_refl (h) (G) (L): reflexive … (cpt h G L 0).
85 /3 width=3 by cpg_refl, ex2_intro/ qed.
87 (* Advanced properties ******************************************************)
89 lemma cpt_sort (h) (G) (L):
90 ∀n. n ≤ 1 → ∀s. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] ⋆((next h)^n s).
92 #n #H #s <(le_n_O_to_eq n) /2 width=1 by le_S_S_to_le/
95 (* Basic inversion lemmas ***************************************************)
97 lemma cpt_inv_atom_sn (h) (n) (J) (G) (L):
98 ∀X2. ⦃G,L⦄ ⊢ ⓪{J} ⬆[h,n] X2 →
99 ∨∨ ∧∧ X2 = ⓪{J} & n = 0
100 | ∃∃s. X2 = ⋆(⫯[h]s) & J = Sort s & n =1
101 | ∃∃K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓓV1 & J = LRef 0
102 | ∃∃m,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,m] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓛV1 & J = LRef 0 & n = ↑m
103 | ∃∃I,K,T,i. ⦃G,K⦄ ⊢ #i ⬆[h,n] T & ⇧*[1] T ≘ X2 & L = K.ⓘ{I} & J = LRef (↑i).
104 #h #n #J #G #L #X2 * #c #Hc #H
105 elim (cpg_inv_atom1 … H) -H *
106 [ #H1 #H2 destruct /3 width=1 by or5_intro0, conj/
107 | #s #H1 #H2 #H3 destruct /3 width=3 by or5_intro1, ex3_intro/
108 | #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 #H3 destruct
109 /4 width=6 by or5_intro2, ex4_3_intro, ex2_intro/
110 | #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 #H3 destruct
111 elim (ist_inv_plus_SO_dx … H3) -H3 [| // ] #m #Hc #H destruct
112 /4 width=9 by or5_intro3, ex5_4_intro, ex2_intro/
113 | #I #K #V2 #i #HV2 #HVT2 #H1 #H2 destruct
114 /4 width=8 by or5_intro4, ex4_4_intro, ex2_intro/
118 lemma cpt_inv_sort_sn (h) (n) (G) (L) (s):
119 ∀X2. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] X2 →
120 ∧∧ X2 = ⋆(((next h)^n) s) & n ≤ 1.
121 #h #n #G #L #s #X2 * #c #Hc #H
122 elim (cpg_inv_sort1 … H) -H * #H1 #H2 destruct
126 lemma cpt_inv_zero_sn (h) (n) (G) (L):
127 ∀X2. ⦃G,L⦄ ⊢ #0 ⬆[h,n] X2 →
128 ∨∨ ∧∧ X2 = #0 & n = 0
129 | ∃∃K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓓV1
130 | ∃∃m,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,m] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓛV1 & n = ↑m.
131 #h #n #G #L #X2 * #c #Hc #H elim (cpg_inv_zero1 … H) -H *
132 [ #H1 #H2 destruct /4 width=1 by isrt_inv_00, or3_intro0, conj/
133 | #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct
134 /4 width=8 by or3_intro1, ex3_3_intro, ex2_intro/
135 | #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct
136 elim (ist_inv_plus_SO_dx … H2) -H2 // #m #Hc #H destruct
137 /4 width=8 by or3_intro2, ex4_4_intro, ex2_intro/
141 lemma cpt_inv_zero_sn_unit (h) (n) (I) (K) (G):
142 ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ⬆[h,n] X2 → ∧∧ X2 = #0 & n = 0.
143 #h #n #I #G #K #X2 #H
144 elim (cpt_inv_zero_sn … H) -H *
145 [ #H1 #H2 destruct /2 width=1 by conj/
146 | #Y #X1 #X2 #_ #_ #H destruct
147 | #m #Y #X1 #X2 #_ #_ #H destruct
151 lemma cpt_inv_lref_sn (h) (n) (G) (L) (i):
152 ∀X2. ⦃G,L⦄ ⊢ #↑i ⬆[h,n] X2 →
153 ∨∨ ∧∧ X2 = #(↑i) & n = 0
154 | ∃∃I,K,T. ⦃G,K⦄ ⊢ #i ⬆[h,n] T & ⇧*[1] T ≘ X2 & L = K.ⓘ{I}.
155 #h #n #G #L #i #X2 * #c #Hc #H elim (cpg_inv_lref1 … H) -H *
156 [ #H1 #H2 destruct /4 width=1 by isrt_inv_00, or_introl, conj/
157 | #I #K #V2 #HV2 #HVT2 #H destruct
158 /4 width=6 by ex3_3_intro, ex2_intro, or_intror/
162 lemma cpt_inv_lref_sn_ctop (n) (h) (G) (i):
163 ∀X2. ⦃G,⋆⦄ ⊢ #i ⬆[h,n] X2 → ∧∧ X2 = #i & n = 0.
164 #h #n #G * [| #i ] #X2 #H
165 [ elim (cpt_inv_zero_sn … H) -H *
166 [ #H1 #H2 destruct /2 width=1 by conj/
167 | #Y #X1 #X2 #_ #_ #H destruct
168 | #m #Y #X1 #X2 #_ #_ #H destruct
170 | elim (cpt_inv_lref_sn … H) -H *
171 [ #H1 #H2 destruct /2 width=1 by conj/
172 | #Z #Y #X0 #_ #_ #H destruct
177 lemma cpt_inv_gref_sn (h) (n) (G) (L) (l):
178 ∀X2. ⦃G,L⦄ ⊢ §l ⬆[h,n] X2 → ∧∧ X2 = §l & n = 0.
179 #h #n #G #L #l #X2 * #c #Hc #H elim (cpg_inv_gref1 … H) -H
180 #H1 #H2 destruct /2 width=1 by conj/
183 lemma cpt_inv_bind_sn (h) (n) (p) (I) (G) (L) (V1) (T1):
184 ∀X2. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ⬆[h,n] X2 →
185 ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 & ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ⬆[h,n] T2
187 #h #n #p #I #G #L #V1 #T1 #X2 * #c #Hc #H
188 elim (cpg_inv_bind1 … H) -H *
189 [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
190 elim (ist_inv_max … H2) -H2 #nV #nT #HcV #HcT #H destruct
191 elim (ist_inv_shift … HcV) -HcV #HcV #H destruct
192 /3 width=5 by ex3_2_intro, ex2_intro/
193 | #cT #T2 #_ #_ #_ #_ #H destruct
194 elim (ist_inv_plus_10_dx … H)
198 lemma cpt_inv_appl_sn (h) (n) (G) (L) (V1) (T1):
199 ∀X2. ⦃G,L⦄ ⊢ ⓐV1.T1 ⬆[h,n] X2 →
200 ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 & ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 & X2 = ⓐV2.T2.
201 #h #n #G #L #V1 #T1 #X2 * #c #Hc #H elim (cpg_inv_appl1 … H) -H *
202 [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
203 elim (ist_inv_max … H2) -H2 #nV #nT #HcV #HcT #H destruct
204 elim (ist_inv_shift … HcV) -HcV #HcV #H destruct
205 /3 width=5 by ex3_2_intro, ex2_intro/
206 | #cV #cW #cU #p #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #_ #H destruct
207 elim (ist_inv_plus_10_dx … H)
208 | #cV #cW #cU #p #V #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #_ #_ #H destruct
209 elim (ist_inv_plus_10_dx … H)
213 lemma cpt_inv_cast_sn (h) (n) (G) (L) (V1) (T1):
214 ∀X2. ⦃G,L⦄ ⊢ ⓝV1.T1 ⬆[h,n] X2 →
215 ∨∨ ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,n] V2 & ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 & X2 = ⓝV2.T2
216 | ∃∃m. ⦃G,L⦄ ⊢ V1 ⬆[h,m] X2 & n = ↑m.
217 #h #n #G #L #V1 #T1 #X2 * #c #Hc #H elim (cpg_inv_cast1 … H) -H *
218 [ #cV #cT #V2 #T2 #HV12 #HT12 #HcVT #H1 #H2 destruct
219 elim (ist_inv_max … H2) -H2 #nV #nT #HcV #HcT #H destruct
221 /4 width=5 by or_introl, ex3_2_intro, ex2_intro/
223 elim (ist_inv_plus_10_dx … H)
224 | #cV #H12 #H destruct
225 elim (ist_inv_plus_SO_dx … H) -H [| // ] #m #Hm #H destruct
226 /4 width=3 by ex2_intro, or_intror/