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/cpm.ma".
18 (* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
20 (* Properties with generic slicing for local environments *******************)
22 (* Basic_1: includes: pr0_lift pr2_lift *)
23 (* Basic_2A1: includes: cpr_lift *)
24 lemma cpm_lifts_sn: ∀n,h,G. d_liftable2_sn … lifts (λL. cpm h G L n).
25 #n #h #G #K #T1 #T2 * #c #Hc #HT12 #b #f #L #HLK #U1 #HTU1
26 elim (cpg_lifts_sn … HT12 … HLK … HTU1) -K -T1
27 /3 width=5 by ex2_intro/
30 lemma cpm_lifts_bi: ∀n,h,G. d_liftable2_bi … lifts (λL. cpm h G L n).
31 #n #h #G #K #T1 #T2 * /3 width=11 by cpg_lifts_bi, ex2_intro/
34 (* Inversion lemmas with generic slicing for local environments *************)
36 (* Basic_1: includes: pr0_gen_lift pr2_gen_lift *)
37 (* Basic_2A1: includes: cpr_inv_lift1 *)
38 lemma cpm_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn … lifts (λL. cpm h G L n).
39 #n #h #G #L #U1 #U2 * #c #Hc #HU12 #b #f #K #HLK #T1 #HTU1
40 elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1
41 /3 width=5 by ex2_intro/
44 lemma cpm_inv_lifts_bi: ∀n,h,G. d_deliftable2_bi … lifts (λL. cpm h G L n).
45 #n #h #G #L #U1 #U2 * /3 width=11 by cpg_inv_lifts_bi, ex2_intro/
48 (* Advanced properties ******************************************************)
50 (* Basic_1: includes: pr2_delta1 *)
51 (* Basic_2A1: includes: cpr_delta *)
52 lemma cpm_delta_drops: ∀n,h,G,L,K,V,V2,W2,i.
53 ⬇*[i] L ≘ K.ⓓV → ⦃G, K⦄ ⊢ V ➡[n, h] V2 →
54 ⬆*[↑i] V2 ≘ W2 → ⦃G, L⦄ ⊢ #i ➡[n, h] W2.
55 #n #h #G #L #K #V #V2 #W2 #i #HLK *
56 /3 width=8 by cpg_delta_drops, ex2_intro/
59 lemma cpm_ell_drops: ∀n,h,G,L,K,V,V2,W2,i.
60 ⬇*[i] L ≘ K.ⓛV → ⦃G, K⦄ ⊢ V ➡[n, h] V2 →
61 ⬆*[↑i] V2 ≘ W2 → ⦃G, L⦄ ⊢ #i ➡[↑n, h] W2.
62 #n #h #G #L #K #V #V2 #W2 #i #HLK *
63 /3 width=8 by cpg_ell_drops, isrt_succ, ex2_intro/
66 (* Advanced inversion lemmas ************************************************)
68 lemma cpm_inv_atom1_drops: ∀n,h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡[n, h] T2 →
70 | ∃∃s. T2 = ⋆(next h s) & I = Sort s & n = 1
71 | ∃∃K,V,V2,i. ⬇*[i] L ≘ K.ⓓV & ⦃G, K⦄ ⊢ V ➡[n, h] V2 &
72 ⬆*[↑i] V2 ≘ T2 & I = LRef i
73 | ∃∃m,K,V,V2,i. ⬇*[i] L ≘ K.ⓛV & ⦃G, K⦄ ⊢ V ➡[m, h] V2 &
74 ⬆*[↑i] V2 ≘ T2 & I = LRef i & n = ↑m.
75 #n #h #I #G #L #T2 * #c #Hc #H elim (cpg_inv_atom1_drops … H) -H *
76 [ #H1 #H2 destruct lapply (isrt_inv_00 … Hc) -Hc
77 /3 width=1 by or4_intro0, conj/
78 | #s #H1 #H2 #H3 destruct lapply (isrt_inv_01 … Hc) -Hc
79 /4 width=3 by or4_intro1, ex3_intro, sym_eq/ (**) (* sym_eq *)
80 | #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
81 /4 width=8 by ex4_4_intro, ex2_intro, or4_intro2/
82 | #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
83 elim (isrt_inv_plus_SO_dx … Hc) -Hc
84 /4 width=10 by ex5_5_intro, ex2_intro, or4_intro3/
88 lemma cpm_inv_lref1_drops: ∀n,h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[n, h] T2 →
90 | ∃∃K,V,V2. ⬇*[i] L ≘ K.ⓓV & ⦃G, K⦄ ⊢ V ➡[n, h] V2 &
92 | ∃∃m,K,V,V2. ⬇*[i] L ≘ K. ⓛV & ⦃G, K⦄ ⊢ V ➡[m, h] V2 &
93 ⬆*[↑i] V2 ≘ T2 & n = ↑m.
94 #n #h #G #L #T2 #i * #c #Hc #H elim (cpg_inv_lref1_drops … H) -H *
95 [ #H1 #H2 destruct lapply (isrt_inv_00 … Hc) -Hc
96 /3 width=1 by or3_intro0, conj/
97 | #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct
98 /4 width=6 by ex3_3_intro, ex2_intro, or3_intro1/
99 | #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct
100 elim (isrt_inv_plus_SO_dx … Hc) -Hc
101 /4 width=8 by ex4_4_intro, ex2_intro, or3_intro2/
105 (* Advanced forward lemmas **************************************************)
107 fact cpm_fwd_plus_aux (n) (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
109 ∃∃T. ⦃G, L⦄ ⊢ T1 ➡[n1, h] T & ⦃G, L⦄ ⊢ T ➡[n2, h] T2.
110 #n #h #G #L #T1 #T2 #H @(cpm_ind … H) -G -L -T1 -T2 -n
111 [ #I #G #L #n1 #n2 #H
112 elim (plus_inv_O3 … H) -H #H1 #H2 destruct
113 /2 width=3 by ex2_intro/
114 | #G #L #s #x1 #n2 #H
115 elim (plus_inv_S3_sn … H) -H *
116 [ #H1 #H2 destruct /2 width=3 by ex2_intro/
117 | #n1 #H1 #H elim (plus_inv_O3 … H) -H #H2 #H3 destruct
118 /2 width=3 by ex2_intro/
120 | #n #G #K #V1 #V2 #W2 #_ #IH #HVW2 #n1 #n2 #H destruct
121 elim IH [|*: // ] -IH #V #HV1 #HV2
122 elim (lifts_total V 𝐔❴↑O❵) #W #HVW
123 /5 width=11 by cpm_lifts_bi, cpm_delta, drops_refl, drops_drop, ex2_intro/
124 | #n #G #K #V1 #V2 #W2 #HV12 #IH #HVW2 #x1 #n2 #H
125 elim (plus_inv_S3_sn … H) -H *
126 [ #H1 #H2 destruct -IH /3 width=3 by cpm_ell, ex2_intro/
127 | #n1 #H1 #H2 destruct -HV12
128 elim (IH n1) [|*: // ] -IH #V #HV1 #HV2
129 elim (lifts_total V 𝐔❴↑O❵) #W #HVW
130 /5 width=11 by cpm_lifts_bi, cpm_ell, drops_refl, drops_drop, ex2_intro/
132 | #n #I #G #K #T2 #U2 #i #_ #IH #HTU2 #n1 #n2 #H destruct
133 elim IH [|*: // ] -IH #T #HT1 #HT2
134 elim (lifts_total T 𝐔❴↑O❵) #U #HTU
135 /5 width=11 by cpm_lifts_bi, cpm_lref, drops_refl, drops_drop, ex2_intro/
136 | #n #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ #IHT #n1 #n2 #H destruct
137 elim IHT [|*: // ] -IHT #T #HT1 #HT2
138 /3 width=5 by cpm_bind, ex2_intro/
139 | #n #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ #IHT #n1 #n2 #H destruct
140 elim IHT [|*: // ] -IHT #T #HT1 #HT2
141 /3 width=5 by cpm_appl, ex2_intro/
142 | #n #G #L #U1 #U2 #T1 #T2 #_ #_ #IHU #IHT #n1 #n2 #H destruct
143 elim IHU [|*: // ] -IHU #U #HU1 #HU2
144 elim IHT [|*: // ] -IHT #T #HT1 #HT2
145 /3 width=5 by cpm_cast, ex2_intro/
146 | #n #G #K #V #U1 #T1 #T2 #HTU1 #_ #IH #n1 #n2 #H destruct
147 elim IH [|*: // ] -IH #T #HT1 #HT2
148 /3 width=3 by cpm_zeta, ex2_intro/
149 | #n #G #L #U #T1 #T2 #_ #IH #n1 #n2 #H destruct
150 elim IH [|*: // ] -IH #T #HT1 #HT2
151 /3 width=3 by cpm_eps, ex2_intro/
152 | #n #G #L #U1 #U2 #T #HU12 #IH #x1 #n2 #H
153 elim (plus_inv_S3_sn … H) -H *
154 [ #H1 #H2 destruct -IH /3 width=4 by cpm_ee, cpm_cast, ex2_intro/
155 | #n1 #H1 #H2 destruct -HU12
156 elim (IH n1) [|*: // ] -IH #U #HU1 #HU2
157 /3 width=3 by cpm_ee, ex2_intro/
159 | #n #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ #IH #n1 #n2 #H destruct
160 elim IH [|*: // ] -IH #T #HT1 #HT2
161 /4 width=7 by cpm_beta, cpm_appl, cpm_bind, ex2_intro/
162 | #n #p #G #L #V1 #V2 #U2 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ #IH #HVU2 #n1 #n2 #H destruct
163 elim IH [|*: // ] -IH #T #HT1 #HT2
164 /4 width=7 by cpm_theta, cpm_appl, cpm_bind, ex2_intro/
168 lemma cpm_fwd_plus (h) (G) (L): ∀n1,n2,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n1+n2, h] T2 →
169 ∃∃T. ⦃G, L⦄ ⊢ T1 ➡[n1, h] T & ⦃G, L⦄ ⊢ T ➡[n2, h] T2.
170 /2 width=3 by cpm_fwd_plus_aux/ qed-.