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 "basic_2/rt_transition/cpg_drops.ma".
16 include "basic_2/rt_transition/cpt_fqu.ma".
18 (* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
20 (* Properties with generic slicing for local environments *******************)
22 lemma cpt_lifts_sn (h) (n) (G):
23 d_liftable2_sn … lifts (λL. cpt h G L n).
24 #h #n #G #K #T1 #T2 * #c #Hc #HT12 #b #f #L #HLK #U1 #HTU1
25 elim (cpg_lifts_sn … HT12 … HLK … HTU1) -K -T1
26 /3 width=5 by ex2_intro/
29 lemma cpt_lifts_bi (h) (n) (G):
30 d_liftable2_bi … lifts (λL. cpt h G L n).
31 #h #n #G #K #T1 #T2 * /3 width=11 by cpg_lifts_bi, ex2_intro/
34 (* Inversion lemmas with generic slicing for local environments *************)
36 lemma cpt_inv_lifts_sn (h) (n) (G):
37 d_deliftable2_sn … lifts (λL. cpt h G L n).
38 #h #n #G #L #U1 #U2 * #c #Hc #HU12 #b #f #K #HLK #T1 #HTU1
39 elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1
40 /3 width=5 by ex2_intro/
43 lemma cpt_inv_lifts_bi (h) (n) (G):
44 d_deliftable2_bi … lifts (λL. cpt h G L n).
45 #h #n #G #L #U1 #U2 * /3 width=11 by cpg_inv_lifts_bi, ex2_intro/
48 (* Advanced properties ******************************************************)
50 lemma cpt_delta_drops (h) (n) (G):
51 ∀L,K,V,i. ⇩[i] L ≘ K.ⓓV → ∀V2. ❨G,K❩ ⊢ V ⬆[h,n] V2 →
52 ∀W2. ⇧[↑i] V2 ≘ W2 → ❨G,L❩ ⊢ #i ⬆[h,n] W2.
53 #h #n #G #L #K #V #i #HLK #V2 *
54 /3 width=8 by cpg_delta_drops, ex2_intro/
57 lemma cpt_ell_drops (h) (n) (G):
58 ∀L,K,V,i. ⇩[i] L ≘ K.ⓛV → ∀V2. ❨G,K❩ ⊢ V ⬆[h,n] V2 →
59 ∀W2. ⇧[↑i] V2 ≘ W2 → ❨G,L❩ ⊢ #i ⬆[h,↑n] W2.
60 #h #n #G #L #K #V #i #HLK #V2 *
61 /3 width=8 by cpg_ell_drops, ist_succ, ex2_intro/
64 (* Advanced inversion lemmas ************************************************)
66 lemma cpt_inv_atom_sn_drops (h) (n) (I) (G) (L):
67 ∀X2. ❨G,L❩ ⊢ ⓪[I] ⬆[h,n] X2 →
68 ∨∨ ∧∧ X2 = ⓪[I] & n = 0
69 | ∃∃s. X2 = ⋆(⫯[h]s) & I = Sort s & n = 1
70 | ∃∃K,V,V2,i. ⇩[i] L ≘ K.ⓓV & ❨G,K❩ ⊢ V ⬆[h,n] V2 & ⇧[↑i] V2 ≘ X2 & I = LRef i
71 | ∃∃m,K,V,V2,i. ⇩[i] L ≘ K.ⓛV & ❨G,K❩ ⊢ V ⬆[h,m] V2 & ⇧[↑i] V2 ≘ X2 & I = LRef i & n = ↑m.
72 #h #n #I #G #L #X2 * #c #Hc #H elim (cpg_inv_atom1_drops … H) -H *
74 /3 width=1 by or4_intro0, conj/
75 | #s1 #s2 #H1 #H2 #H3 #H4 destruct
76 /3 width=3 by or4_intro1, ex3_intro/
77 | #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
78 /4 width=8 by ex4_4_intro, ex2_intro, or4_intro2/
79 | #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
80 elim (ist_inv_plus_SO_dx … H2) -H2
81 /4 width=10 by ex5_5_intro, ex2_intro, or4_intro3/
85 lemma cpt_inv_lref_sn_drops (h) (n) (G) (L) (i):
86 ∀X2. ❨G,L❩ ⊢ #i ⬆[h,n] X2 →
88 | ∃∃K,V,V2. ⇩[i] L ≘ K.ⓓV & ❨G,K❩ ⊢ V ⬆[h,n] V2 & ⇧[↑i] V2 ≘ X2
89 | ∃∃m,K,V,V2. ⇩[i] L ≘ K. ⓛV & ❨G,K❩ ⊢ V ⬆[h,m] V2 & ⇧[↑i] V2 ≘ X2 & n = ↑m.
90 #h #n #G #L #i #X2 * #c #Hc #H elim (cpg_inv_lref1_drops … H) -H *
92 /3 width=1 by or3_intro0, conj/
93 | #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct
94 /4 width=6 by ex3_3_intro, ex2_intro, or3_intro1/
95 | #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct
96 elim (ist_inv_plus_SO_dx … H) -H
97 /4 width=8 by ex4_4_intro, ex2_intro, or3_intro2/
101 (* Advanced forward lemmas **************************************************)
103 fact cpt_fwd_plus_aux (h) (n) (G) (L):
104 ∀T1,T2. ❨G,L❩ ⊢ T1 ⬆[h,n] T2 → ∀n1,n2. n1+n2 = n →
105 ∃∃T. ❨G,L❩ ⊢ T1 ⬆[h,n1] T & ❨G,L❩ ⊢ T ⬆[h,n2] T2.
106 #h #n #G #L #T1 #T2 #H @(cpt_ind … H) -G -L -T1 -T2 -n
107 [ #I #G #L #n1 #n2 #H
108 elim (plus_inv_O3 … H) -H #H1 #H2 destruct
109 /2 width=3 by ex2_intro/
110 | #G #L #s #x1 #n2 #H
111 elim (plus_inv_S3_sn … H) -H *
112 [ #H1 #H2 destruct /2 width=3 by ex2_intro/
113 | #n1 #H1 #H elim (plus_inv_O3 … H) -H #H2 #H3 destruct
114 /2 width=3 by ex2_intro/
116 | #n #G #K #V1 #V2 #W2 #_ #IH #HVW2 #n1 #n2 #H destruct
117 elim IH [|*: // ] -IH #V #HV1 #HV2
118 elim (lifts_total V 𝐔❨↑O❩) #W #HVW
119 /5 width=11 by cpt_lifts_bi, cpt_delta, drops_refl, drops_drop, ex2_intro/
120 | #n #G #K #V1 #V2 #W2 #HV12 #IH #HVW2 #x1 #n2 #H
121 elim (plus_inv_S3_sn … H) -H *
122 [ #H1 #H2 destruct -IH /3 width=3 by cpt_ell, ex2_intro/
123 | #n1 #H1 #H2 destruct -HV12
124 elim (IH n1) [|*: // ] -IH #V #HV1 #HV2
125 elim (lifts_total V 𝐔❨↑O❩) #W #HVW
126 /5 width=11 by cpt_lifts_bi, cpt_ell, drops_refl, drops_drop, ex2_intro/
128 | #n #I #G #K #T2 #U2 #i #_ #IH #HTU2 #n1 #n2 #H destruct
129 elim IH [|*: // ] -IH #T #HT1 #HT2
130 elim (lifts_total T 𝐔❨↑O❩) #U #HTU
131 /5 width=11 by cpt_lifts_bi, cpt_lref, drops_refl, drops_drop, ex2_intro/
132 | #n #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ #IHT #n1 #n2 #H destruct
133 elim IHT [|*: // ] -IHT #T #HT1 #HT2
134 /3 width=5 by cpt_bind, ex2_intro/
135 | #n #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ #IHT #n1 #n2 #H destruct
136 elim IHT [|*: // ] -IHT #T #HT1 #HT2
137 /3 width=5 by cpt_appl, ex2_intro/
138 | #n #G #L #U1 #U2 #T1 #T2 #_ #_ #IHU #IHT #n1 #n2 #H destruct
139 elim IHU [|*: // ] -IHU #U #HU1 #HU2
140 elim IHT [|*: // ] -IHT #T #HT1 #HT2
141 /3 width=5 by cpt_cast, ex2_intro/
142 | #n #G #L #U1 #U2 #T #HU12 #IH #x1 #n2 #H
143 elim (plus_inv_S3_sn … H) -H *
144 [ #H1 #H2 destruct -IH /3 width=4 by cpt_ee, cpt_cast, ex2_intro/
145 | #n1 #H1 #H2 destruct -HU12
146 elim (IH n1) [|*: // ] -IH #U #HU1 #HU2
147 /3 width=3 by cpt_ee, ex2_intro/
152 lemma cpt_fwd_plus (h) (n1) (n2) (G) (L):
153 ∀T1,T2. ❨G,L❩ ⊢ T1 ⬆[h,n1+n2] T2 →
154 ∃∃T. ❨G,L❩ ⊢ T1 ⬆[h,n1] T & ❨G,L❩ ⊢ T ⬆[h,n2] T2.
155 /2 width=3 by cpt_fwd_plus_aux/ qed-.