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/xoa/ex_4_3.ma".
16 include "ground_2/steps/rtc_ist_shift.ma".
17 include "ground_2/steps/rtc_ist_plus.ma".
18 include "ground_2/steps/rtc_ist_max.ma".
19 include "basic_2/notation/relations/pty_6.ma".
20 include "basic_2/rt_transition/cpg.ma".
22 (* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
24 definition cpt (h) (G) (L) (n): relation2 term term ≝
25 λT1,T2. ∃∃c. 𝐓❪n,c❫ & ❪G,L❫ ⊢ T1 ⬈[eq …,c,h] T2.
28 "t-bound context-sensitive parallel t-transition (term)"
29 'PTy h n G L T1 T2 = (cpt h G L n T1 T2).
31 (* Basic properties *********************************************************)
33 lemma cpt_ess (h) (G) (L):
34 ∀s. ❪G,L❫ ⊢ ⋆s ⬆[h,1] ⋆(⫯[h]s).
35 /2 width=3 by cpg_ess, ex2_intro/ qed.
37 lemma cpt_delta (h) (n) (G) (K):
38 ∀V1,V2. ❪G,K❫ ⊢ V1 ⬆[h,n] V2 →
39 ∀W2. ⇧[1] V2 ≘ W2 → ❪G,K.ⓓV1❫ ⊢ #0 ⬆[h,n] W2.
41 /3 width=5 by cpg_delta, ex2_intro/
44 lemma cpt_ell (h) (n) (G) (K):
45 ∀V1,V2. ❪G,K❫ ⊢ V1 ⬆[h,n] V2 →
46 ∀W2. ⇧[1] V2 ≘ W2 → ❪G,K.ⓛV1❫ ⊢ #0 ⬆[h,↑n] W2.
48 /3 width=5 by cpg_ell, ex2_intro, ist_succ/
51 lemma cpt_lref (h) (n) (G) (K):
52 ∀T,i. ❪G,K❫ ⊢ #i ⬆[h,n] T → ∀U. ⇧[1] T ≘ U →
53 ∀I. ❪G,K.ⓘ[I]❫ ⊢ #↑i ⬆[h,n] U.
55 /3 width=5 by cpg_lref, ex2_intro/
58 lemma cpt_bind (h) (n) (G) (L):
59 ∀V1,V2. ❪G,L❫ ⊢ V1 ⬆[h,0] V2 → ∀I,T1,T2. ❪G,L.ⓑ[I]V1❫ ⊢ T1 ⬆[h,n] T2 →
60 ∀p. ❪G,L❫ ⊢ ⓑ[p,I]V1.T1 ⬆[h,n] ⓑ[p,I]V2.T2.
61 #h #n #G #L #V1 #V2 * #cV #HcV #HV12 #I #T1 #T2 *
62 /3 width=5 by cpg_bind, ist_max_O1, ex2_intro/
65 lemma cpt_appl (h) (n) (G) (L):
66 ∀V1,V2. ❪G,L❫ ⊢ V1 ⬆[h,0] V2 →
67 ∀T1,T2. ❪G,L❫ ⊢ T1 ⬆[h,n] T2 → ❪G,L❫ ⊢ ⓐV1.T1 ⬆[h,n] ⓐV2.T2.
68 #h #n #G #L #V1 #V2 * #cV #HcV #HV12 #T1 #T2 *
69 /3 width=5 by ist_max_O1, cpg_appl, ex2_intro/
72 lemma cpt_cast (h) (n) (G) (L):
73 ∀U1,U2. ❪G,L❫ ⊢ U1 ⬆[h,n] U2 →
74 ∀T1,T2. ❪G,L❫ ⊢ T1 ⬆[h,n] T2 → ❪G,L❫ ⊢ ⓝU1.T1 ⬆[h,n] ⓝU2.T2.
75 #h #n #G #L #U1 #U2 * #cU #HcU #HU12 #T1 #T2 *
76 /3 width=6 by cpg_cast, ex2_intro/
79 lemma cpt_ee (h) (n) (G) (L):
80 ∀U1,U2. ❪G,L❫ ⊢ U1 ⬆[h,n] U2 → ∀T. ❪G,L❫ ⊢ ⓝU1.T ⬆[h,↑n] U2.
82 /3 width=3 by cpg_ee, ist_succ, ex2_intro/
85 lemma cpt_refl (h) (G) (L): reflexive … (cpt h G L 0).
86 /3 width=3 by cpg_refl, ex2_intro/ qed.
88 (* Advanced properties ******************************************************)
90 lemma cpt_sort (h) (G) (L):
91 ∀n. n ≤ 1 → ∀s. ❪G,L❫ ⊢ ⋆s ⬆[h,n] ⋆((next h)^n s).
93 #n #H #s <(le_n_O_to_eq n) /2 width=1 by le_S_S_to_le/
96 (* Basic inversion lemmas ***************************************************)
98 lemma cpt_inv_atom_sn (h) (n) (J) (G) (L):
99 ∀X2. ❪G,L❫ ⊢ ⓪[J] ⬆[h,n] X2 →
100 ∨∨ ∧∧ X2 = ⓪[J] & n = 0
101 | ∃∃s. X2 = ⋆(⫯[h]s) & J = Sort s & n =1
102 | ∃∃K,V1,V2. ❪G,K❫ ⊢ V1 ⬆[h,n] V2 & ⇧[1] V2 ≘ X2 & L = K.ⓓV1 & J = LRef 0
103 | ∃∃m,K,V1,V2. ❪G,K❫ ⊢ V1 ⬆[h,m] V2 & ⇧[1] V2 ≘ X2 & L = K.ⓛV1 & J = LRef 0 & n = ↑m
104 | ∃∃I,K,T,i. ❪G,K❫ ⊢ #i ⬆[h,n] T & ⇧[1] T ≘ X2 & L = K.ⓘ[I] & J = LRef (↑i).
105 #h #n #J #G #L #X2 * #c #Hc #H
106 elim (cpg_inv_atom1 … H) -H *
107 [ #H1 #H2 destruct /3 width=1 by or5_intro0, conj/
108 | #s #H1 #H2 #H3 destruct /3 width=3 by or5_intro1, ex3_intro/
109 | #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 #H3 destruct
110 /4 width=6 by or5_intro2, ex4_3_intro, ex2_intro/
111 | #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 #H3 destruct
112 elim (ist_inv_plus_SO_dx … H3) -H3 [| // ] #m #Hc #H destruct
113 /4 width=9 by or5_intro3, ex5_4_intro, ex2_intro/
114 | #I #K #V2 #i #HV2 #HVT2 #H1 #H2 destruct
115 /4 width=8 by or5_intro4, ex4_4_intro, ex2_intro/
119 lemma cpt_inv_sort_sn (h) (n) (G) (L) (s):
120 ∀X2. ❪G,L❫ ⊢ ⋆s ⬆[h,n] X2 →
121 ∧∧ X2 = ⋆(((next h)^n) s) & n ≤ 1.
122 #h #n #G #L #s #X2 * #c #Hc #H
123 elim (cpg_inv_sort1 … H) -H * #H1 #H2 destruct
127 lemma cpt_inv_zero_sn (h) (n) (G) (L):
128 ∀X2. ❪G,L❫ ⊢ #0 ⬆[h,n] X2 →
129 ∨∨ ∧∧ X2 = #0 & n = 0
130 | ∃∃K,V1,V2. ❪G,K❫ ⊢ V1 ⬆[h,n] V2 & ⇧[1] V2 ≘ X2 & L = K.ⓓV1
131 | ∃∃m,K,V1,V2. ❪G,K❫ ⊢ V1 ⬆[h,m] V2 & ⇧[1] V2 ≘ X2 & L = K.ⓛV1 & n = ↑m.
132 #h #n #G #L #X2 * #c #Hc #H elim (cpg_inv_zero1 … H) -H *
133 [ #H1 #H2 destruct /4 width=1 by ist_inv_00, or3_intro0, conj/
134 | #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct
135 /4 width=8 by or3_intro1, ex3_3_intro, ex2_intro/
136 | #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct
137 elim (ist_inv_plus_SO_dx … H2) -H2 // #m #Hc #H destruct
138 /4 width=8 by or3_intro2, ex4_4_intro, ex2_intro/
142 lemma cpt_inv_zero_sn_unit (h) (n) (I) (K) (G):
143 ∀X2. ❪G,K.ⓤ[I]❫ ⊢ #0 ⬆[h,n] X2 → ∧∧ X2 = #0 & n = 0.
144 #h #n #I #G #K #X2 #H
145 elim (cpt_inv_zero_sn … H) -H *
146 [ #H1 #H2 destruct /2 width=1 by conj/
147 | #Y #X1 #X2 #_ #_ #H destruct
148 | #m #Y #X1 #X2 #_ #_ #H destruct
152 lemma cpt_inv_lref_sn (h) (n) (G) (L) (i):
153 ∀X2. ❪G,L❫ ⊢ #↑i ⬆[h,n] X2 →
154 ∨∨ ∧∧ X2 = #(↑i) & n = 0
155 | ∃∃I,K,T. ❪G,K❫ ⊢ #i ⬆[h,n] T & ⇧[1] T ≘ X2 & L = K.ⓘ[I].
156 #h #n #G #L #i #X2 * #c #Hc #H elim (cpg_inv_lref1 … H) -H *
157 [ #H1 #H2 destruct /4 width=1 by ist_inv_00, or_introl, conj/
158 | #I #K #V2 #HV2 #HVT2 #H destruct
159 /4 width=6 by ex3_3_intro, ex2_intro, or_intror/
163 lemma cpt_inv_lref_sn_ctop (n) (h) (G) (i):
164 ∀X2. ❪G,⋆❫ ⊢ #i ⬆[h,n] X2 → ∧∧ X2 = #i & n = 0.
165 #h #n #G * [| #i ] #X2 #H
166 [ elim (cpt_inv_zero_sn … H) -H *
167 [ #H1 #H2 destruct /2 width=1 by conj/
168 | #Y #X1 #X2 #_ #_ #H destruct
169 | #m #Y #X1 #X2 #_ #_ #H destruct
171 | elim (cpt_inv_lref_sn … H) -H *
172 [ #H1 #H2 destruct /2 width=1 by conj/
173 | #Z #Y #X0 #_ #_ #H destruct
178 lemma cpt_inv_gref_sn (h) (n) (G) (L) (l):
179 ∀X2. ❪G,L❫ ⊢ §l ⬆[h,n] X2 → ∧∧ X2 = §l & n = 0.
180 #h #n #G #L #l #X2 * #c #Hc #H elim (cpg_inv_gref1 … H) -H
181 #H1 #H2 destruct /2 width=1 by conj/
184 lemma cpt_inv_bind_sn (h) (n) (p) (I) (G) (L) (V1) (T1):
185 ∀X2. ❪G,L❫ ⊢ ⓑ[p,I]V1.T1 ⬆[h,n] X2 →
186 ∃∃V2,T2. ❪G,L❫ ⊢ V1 ⬆[h,0] V2 & ❪G,L.ⓑ[I]V1❫ ⊢ T1 ⬆[h,n] T2
188 #h #n #p #I #G #L #V1 #T1 #X2 * #c #Hc #H
189 elim (cpg_inv_bind1 … H) -H *
190 [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
191 elim (ist_inv_max … H2) -H2 #nV #nT #HcV #HcT #H destruct
192 elim (ist_inv_shift … HcV) -HcV #HcV #H destruct
193 /3 width=5 by ex3_2_intro, ex2_intro/
194 | #cT #T2 #_ #_ #_ #_ #H destruct
195 elim (ist_inv_plus_10_dx … H)
199 lemma cpt_inv_appl_sn (h) (n) (G) (L) (V1) (T1):
200 ∀X2. ❪G,L❫ ⊢ ⓐV1.T1 ⬆[h,n] X2 →
201 ∃∃V2,T2. ❪G,L❫ ⊢ V1 ⬆[h,0] V2 & ❪G,L❫ ⊢ T1 ⬆[h,n] T2 & X2 = ⓐV2.T2.
202 #h #n #G #L #V1 #T1 #X2 * #c #Hc #H elim (cpg_inv_appl1 … H) -H *
203 [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
204 elim (ist_inv_max … H2) -H2 #nV #nT #HcV #HcT #H destruct
205 elim (ist_inv_shift … HcV) -HcV #HcV #H destruct
206 /3 width=5 by ex3_2_intro, ex2_intro/
207 | #cV #cW #cU #p #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #_ #H destruct
208 elim (ist_inv_plus_10_dx … H)
209 | #cV #cW #cU #p #V #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #_ #_ #H destruct
210 elim (ist_inv_plus_10_dx … H)
214 lemma cpt_inv_cast_sn (h) (n) (G) (L) (V1) (T1):
215 ∀X2. ❪G,L❫ ⊢ ⓝV1.T1 ⬆[h,n] X2 →
216 ∨∨ ∃∃V2,T2. ❪G,L❫ ⊢ V1 ⬆[h,n] V2 & ❪G,L❫ ⊢ T1 ⬆[h,n] T2 & X2 = ⓝV2.T2
217 | ∃∃m. ❪G,L❫ ⊢ V1 ⬆[h,m] X2 & n = ↑m.
218 #h #n #G #L #V1 #T1 #X2 * #c #Hc #H elim (cpg_inv_cast1 … H) -H *
219 [ #cV #cT #V2 #T2 #HV12 #HT12 #HcVT #H1 #H2 destruct
220 elim (ist_inv_max … H2) -H2 #nV #nT #HcV #HcT #H destruct
222 /4 width=5 by or_introl, ex3_2_intro, ex2_intro/
224 elim (ist_inv_plus_10_dx … H)
225 | #cV #H12 #H destruct
226 elim (ist_inv_plus_SO_dx … H) -H [| // ] #m #Hm #H destruct
227 /4 width=3 by ex2_intro, or_intror/