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/relocation/drops_ltc.ma".
16 include "basic_2/rt_transition/cpm_drops.ma".
17 include "basic_2/rt_computation/cpms.ma".
19 (* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
21 (* Properties with generic slicing for local environments *******************)
23 lemma cpms_lifts_sn: ∀n,h,G. d_liftable2_sn … lifts (λL. cpms h G L n).
24 /3 width=6 by d2_liftable_sn_ltc, cpm_lifts_sn/ qed-.
26 (* Basic_2A1: uses: scpds_lift *)
27 (* Basic_2A1: includes: cprs_lift *)
28 (* Basic_1: includes: pr3_lift *)
29 lemma cpms_lifts_bi: ∀n,h,G. d_liftable2_bi … lifts (λL. cpms h G L n).
30 #n #h #G @d_liftable2_sn_bi
31 /2 width=6 by cpms_lifts_sn, lifts_mono/
34 (* Inversion lemmas with generic slicing for local environments *************)
36 (* Basic_2A1: uses: scpds_inv_lift1 *)
37 (* Basic_2A1: includes: cprs_inv_lift1 *)
38 (* Basic_1: includes: pr3_gen_lift *)
39 lemma cpms_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn … lifts (λL. cpms h G L n).
40 /3 width=6 by d2_deliftable_sn_ltc, cpm_inv_lifts_sn/ qed-.
42 lemma cpms_inv_lifts_bi: ∀n,h,G. d_deliftable2_bi … lifts (λL. cpms h G L n).
43 #n #h #G @d_deliftable2_sn_bi
44 /2 width=6 by cpms_inv_lifts_sn, lifts_inj/
47 (* Advanced properties ******************************************************)
49 lemma cpms_delta (n) (h) (G): ∀K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡*[n, h] V2 →
50 ∀W2. ⬆*[1] V2 ≘ W2 → ⦃G, K.ⓓV1⦄ ⊢ #0 ➡*[n, h] W2.
51 #n #h #G #K #V1 #V2 #H @(cpms_ind_dx … H) -V2
52 [ /3 width=3 by cpm_cpms, cpm_delta/
53 | #n1 #n2 #V #V2 #_ #IH #HV2 #W2 #HVW2
54 elim (lifts_total V (𝐔❴1❵)) #W #HVW
55 /5 width=11 by cpms_step_dx, cpm_lifts_bi, drops_refl, drops_drop/
59 lemma cpms_ell (n) (h) (G): ∀K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡*[n, h] V2 →
60 ∀W2. ⬆*[1] V2 ≘ W2 → ⦃G, K.ⓛV1⦄ ⊢ #0 ➡*[↑n, h] W2.
61 #n #h #G #K #V1 #V2 #H @(cpms_ind_dx … H) -V2
62 [ /3 width=3 by cpm_cpms, cpm_ell/
63 | #n1 #n2 #V #V2 #_ #IH #HV2 #W2 #HVW2
64 elim (lifts_total V (𝐔❴1❵)) #W #HVW >plus_S1
65 /5 width=11 by cpms_step_dx, cpm_lifts_bi, drops_refl, drops_drop/
69 lemma cpms_lref (n) (h) (I) (G): ∀K,T,i. ⦃G, K⦄ ⊢ #i ➡*[n, h] T →
70 ∀U. ⬆*[1] T ≘ U → ⦃G, K.ⓘ{I}⦄ ⊢ #↑i ➡*[n, h] U.
71 #n #h #I #G #K #T #i #H @(cpms_ind_dx … H) -T
72 [ /3 width=3 by cpm_cpms, cpm_lref/
73 | #n1 #n2 #T #T2 #_ #IH #HT2 #U2 #HTU2
74 elim (lifts_total T (𝐔❴1❵)) #U #TU
75 /5 width=11 by cpms_step_dx, cpm_lifts_bi, drops_refl, drops_drop/
79 lemma cpms_cast_sn (n) (h) (G) (L):
80 ∀U1,U2. ⦃G, L⦄ ⊢ U1 ➡*[n, h] U2 →
81 ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
82 ⦃G, L⦄ ⊢ ⓝU1.T1 ➡*[n, h] ⓝU2.T2.
83 #n #h #G #L #U1 #U2 #H @(cpms_ind_sn … H) -U1 -n
84 [ /3 width=3 by cpm_cpms, cpm_cast/
85 | #n1 #n2 #U1 #U #HU1 #_ #IH #T1 #T2 #H
86 elim (cpm_fwd_plus … H) -H #T #HT1 #HT2
87 /3 width=3 by cpms_step_sn, cpm_cast/
91 (* Note: apparently this was missing in basic_1 *)
92 (* Basic_2A1: uses: cprs_delta *)
93 lemma cpms_delta_drops (n) (h) (G):
94 ∀L,K,V,i. ⬇*[i] L ≘ K.ⓓV →
95 ∀V2. ⦃G, K⦄ ⊢ V ➡*[n, h] V2 →
96 ∀W2. ⬆*[↑i] V2 ≘ W2 → ⦃G, L⦄ ⊢ #i ➡*[n, h] W2.
97 #n #h #G #L #K #V #i #HLK #V2 #H @(cpms_ind_dx … H) -V2
98 [ /3 width=6 by cpm_cpms, cpm_delta_drops/
99 | #n1 #n2 #V1 #V2 #_ #IH #HV12 #W2 #HVW2
100 lapply (drops_isuni_fwd_drop2 … HLK) -HLK // #HLK
101 elim (lifts_total V1 (𝐔❴↑i❵)) #W1 #HVW1
102 /3 width=11 by cpm_lifts_bi, cpms_step_dx/
106 (* Advanced inversion lemmas ************************************************)
108 lemma cpms_inv_lref1_drops (n) (h) (G):
109 ∀L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[n, h] T2 →
110 ∨∨ ∧∧ T2 = #i & n = 0
111 | ∃∃K,V,V2. ⬇*[i] L ≘ K.ⓓV & ⦃G, K⦄ ⊢ V ➡*[n, h] V2 &
113 | ∃∃m,K,V,V2. ⬇*[i] L ≘ K.ⓛV & ⦃G, K⦄ ⊢ V ➡*[m, h] V2 &
114 ⬆*[↑i] V2 ≘ T2 & n = ↑m.
115 #n #h #G #L #T2 #i #H @(cpms_ind_dx … H) -T2
116 [ /3 width=1 by or3_intro0, conj/
117 | #n1 #n2 #T #T2 #_ #IH #HT2 cases IH -IH *
119 elim (cpm_inv_lref1_drops … HT2) -HT2 *
120 [ /3 width=1 by or3_intro0, conj/
121 | /4 width=6 by cpm_cpms, or3_intro1, ex3_3_intro/
122 | /4 width=8 by cpm_cpms, or3_intro2, ex4_4_intro/
124 | #K #V0 #V #HLK #HV0 #HVT
125 lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK
126 elim (cpm_inv_lifts_sn … HT2 … H0LK … HVT) -H0LK -T
127 /4 width=6 by cpms_step_dx, ex3_3_intro, or3_intro1/
128 | #m #K #V0 #V #HLK #HV0 #HVT #H destruct
129 lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK
130 elim (cpm_inv_lifts_sn … HT2 … H0LK … HVT) -H0LK -T
131 /4 width=8 by cpms_step_dx, ex4_4_intro, or3_intro2/
136 fact cpms_inv_succ_sn (n) (h) (G) (L):
137 ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[↑n, h] T2 →
138 ∃∃T. ⦃G, L⦄ ⊢ T1 ➡*[1, h] T & ⦃G, L⦄ ⊢ T ➡*[n, h] T2.
140 @(insert_eq_0 … (↑n)) #m #H
141 @(cpms_ind_sn … H) -T1 -m
143 | #x1 #n2 #T1 #T #HT1 #HT2 #IH #H
144 elim (plus_inv_S3_sn x1 n2) [1,2: * |*: // ] -H
145 [ #H1 #H2 destruct -HT2
146 elim IH -IH // #T0 #HT0 #HT02
147 /3 width=3 by cpms_step_sn, ex2_intro/
148 | #n1 #H1 #H2 destruct -IH
149 elim (cpm_fwd_plus … 1 n1 T1 T) [|*: // ] -HT1 #T0 #HT10 #HT0
150 /3 width=5 by cpms_step_sn, cpm_cpms, ex2_intro/