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_conversion/cpce_drops.ma".
16 include "basic_2/rt_conversion/lpce_drops.ma".
17 include "basic_2/dynamic/cnv_preserve.ma".
19 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
21 definition IH_cnv_cpce_cpm_conf (h) (a): relation3 genv lenv term ≝
22 λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] →
23 ∀n,T1. ⦃G,L0⦄ ⊢ T0 ➡[n,h] T1 → ∀T2. ⦃G,L0⦄ ⊢ T0 ⬌η[h] T2 →
24 ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ⬌η[h] L2 →
25 ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n,h] T.
27 definition IH_cnv_cpce_cpms_conf (h) (a): relation3 genv lenv term ≝
28 λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] →
29 ∀n,T1. ⦃G,L0⦄ ⊢ T0 ➡*[n,h] T1 → ∀T2. ⦃G,L0⦄ ⊢ T0 ⬌η[h] T2 →
30 ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ⬌η[h] L2 →
31 ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n,h] T.
33 (* Properties with eta-conversion for full local environments ***************)
35 fact cnv_cpce_cpms_conf_sub (h) (a) (G0) (L0) (T0):
36 (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpm_conf h a G L T) →
37 ∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpms_conf h a G L T.
38 #h #a #GX #LX #TX #HX #G #L0 #T0 #HX0 #HT0 #n #X1 #HX1
39 @(cpms_ind_dx … HX1) -n -X1
40 [ #T2 #HT02 #L1 #HL01 #L2 #HL02
42 | #n1 #n2 #T3 #T1 #HT03 #IH #HT31 #T2 #HT02 #L1 #HL01 #L2 #HL02
43 lapply (cnv_cpms_trans … HT0 … HT03) -HT0 #HT3
44 elim (IH … HT02 … L0 … HL02) -IH -HT02 [| // ] #T4 #HT34 #HT24
45 elim (HX … HT3 … HT31 … HT34 … HL01 … HL02)
46 [| /2 width=4 by fpbg_cpms_trans/ ] -GX -LX -L0 -TX -T0 -T3 #T3 #HT13 #HT43
47 /3 width=5 by cpms_trans, ex2_intro/
51 fact cnv_cpce_cpm_conf_aux (h) (a) (G0) (L0) (T0):
52 (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpm_conf h a G L T) →
53 IH_cnv_cpce_cpm_conf h a G0 L0 T0.
54 #h #a #G0 #L0 * * [|||| * ]
55 [ #s #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
56 elim (cpm_inv_sort1 … HX1) -HX1 #H #Hn destruct
57 lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct
58 /3 width=3 by cpce_sort, ex2_intro/
59 | #i #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
60 elim (cnv_inv_lref_drops … H0) -H0 #I #K0 #W0 #HLK0 #HW0
61 elim (lpr_drops_conf … HLK0 … HL01) [| // ] #Y1 #H1 #HLK1
62 elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #HK01 #HW01 #H destruct
63 elim (lpce_drops_conf … HLK0 … HL02) [| // ] #Y2 #H2 #HLK2
64 elim (lpce_inv_pair_sn … H2) -H2 #K2 #W2 #HK02 #HW02 #H destruct
65 elim (cpm_inv_lref1_drops … HX1) -HX1 *
67 elim (cpce_inv_lref_sn_drops_pair … HX2 … HLK0) -HX2 *
68 [ #H1 #H2 destruct -L0 -K0 -W0
69 /3 width=3 by cpce_ldef_drops, ex2_intro/
70 | #H1 #HW #H2 destruct -L0 -W2 -HW0 -HK02
71 @(ex2_intro … (#i)) [| // ]
72 @(cpce_ldec_drops … HLK1) -HLK1 #n #p #V0 #U0 #HWU0
73 /4 width=10 by lpr_cpms_trans, cpms_step_sn/
74 | lapply (drops_isuni_fwd_drop2 … HLK2) [ // ] -W2 #HLK2
75 #n #p #W01 #W02 #V0 #V01 #V02 #U0 #H1 #HWU0 #HW001 #HW012 #HV001 #HV012 #H2 destruct
76 lapply (cnv_cpms_trans … HW0 … HWU0) #H
77 elim (cnv_inv_bind … H) -H #HV0 #_
78 elim (cnv_cpms_conf_lpr … HW0 … HWU0 0 W1 … K0 … HK01) [| // ]
79 [| /2 width=1 by cpm_cpms/ ] <minus_O_n <minus_n_O #X #H #HWU1
80 elim (cpms_inv_abst_sn … H) -H #V1 #U1 #HV01 #HU01 #H destruct
81 elim (IH … HW0 … HW01 … HW001 … HK01 … HK02) -HW01 -HW001
82 [| /3 width=2 by fqup_fpbg, fqup_lref/ ] #W11 #HW11 #HW011
83 elim (cnv_cpce_cpms_conf_sub … IH … HV0 … HV01 … HV001 … HK01 … HK02) -HV0 -HV01 -HV001
84 [| /4 width=6 by fqup_cpms_fwd_fpbg, fpbg_fqu_trans, fqup_lref/ ] #V11 #HV11 #HV011
85 elim (cpms_lifts_sn … HW011 … HLK2 … HW012) -W01 #W12 #HW112 #HW012
86 elim (cpms_lifts_sn … HV011 … HLK2 … HV012) -V01 #V12 #HV112 #HV012
87 @(ex2_intro …(ⓝW12.+ⓛV12.ⓐ#O.#(↑i)))
88 [ /2 width=14 by cpce_eta_drops/ | /3 width=1 by cpms_cast, cpms_bind/ ]
90 | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1
91 #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 -HL01 -HL02
92 lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct
93 lapply (cpce_inv_lref_sn_drops_ldef … HX2 … HLK0) -HX2 #H destruct
94 elim (IH … HW0 … HW01 … HW02 … HK01 … HK02)
95 [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
96 elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
97 /3 width=9 by cpce_lifts_bi, cpms_delta_drops, ex2_intro/
98 | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1
99 #m #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 #H destruct -HL01 -HL02
100 lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct
101 elim (cpce_inv_lref_sn_drops_ldec … HX2 … HLK0) -HX2 *
103 elim (IH … HW0 … HW01 … HW02 … HK01 … HK02)
104 [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
105 elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
106 /3 width=9 by cpce_lifts_bi, cpms_ell_drops, ex2_intro/
107 | lapply (drops_isuni_fwd_drop2 … HLK2) [ // ] -W2 #HLK2
108 #n #p #W01 #W02 #V0 #V01 #V02 #U0 #_ #HW001 #HW012 #_ #_ #H destruct -V0 -V01 -U0
109 elim (IH … HW0 … HW01 … HW001 … HK01 … HK02)
110 [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
111 elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
112 /4 width=11 by cpce_lifts_bi, cpms_lifts_bi, cpms_ee, ex2_intro/
115 | #l #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
116 elim (cpm_inv_gref1 … HX1) -HX1 #H1 #H2 destruct
117 lapply (cpce_inv_gref_sn … HX2) -HX2 #H destruct
118 /3 width=3 by cpce_gref, cpm_cpms, ex2_intro/
119 | #p #I #V0 #T0 #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
120 elim (cnv_inv_bind … H0) -H0 #HV0 #HT0
121 elim (cpce_inv_bind_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
122 elim (cpm_inv_bind1 … HX1) -HX1 *
123 [ #V1 #T1 #HV01 #HT01 #H destruct
124 elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0
125 [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
126 elim (IH … HT0 … HT01 … HT02 … (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -HT0 -HT01 -HT02
127 [|*: /2 width=1 by lpce_pair, fqup_fpbg, lpr_pair/ ] -L0 -V0 -T0 #T #HT1 #HT2
128 /3 width=5 by cpce_bind, cpms_bind, ex2_intro/
129 | #X0 #HXT0 #HX01 #H1 #H2 destruct -HV0 -HV02
130 lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HXT0) -HT0
131 [ /3 width=1 by drops_refl, drops_drop/ ] #HX0
132 elim (cpce_inv_lifts_sn … HT02 (Ⓣ) … L0 … HXT0) -HT02
133 [| /3 width=1 by drops_refl, drops_drop/ ] #X2 #HXT2 #HX02
134 elim (IH … HX0 … HX01 … HX02 … HL01 … HL02) -HX0 -HX01 -HX02
135 [| /3 width=1 by fqup_fpbg, fqup_zeta/ ] -V0 -T0 -X0 #X #HX1 #HX2
136 /3 width=5 by cpms_zeta, ex2_intro/
138 | #V0 #T0 #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
139 elim (cnv_inv_appl … H0) -H0 #m #p #W0 #U0 #_ #HV0 #HT0 #_ #_ -m -p -W0 -U0
140 elim (cpce_inv_flat_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
141 elim (cpm_inv_appl1 … HX1) -HX1 *
142 [ #V1 #T1 #HV01 #HT01 #H destruct
143 elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
144 [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
145 elim (IH … HT0 … HT01 … HT02 … HL01 … HL02) -HT0 -HT01 -HT02
146 [|*: /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #T #HT1 #HT2
147 /3 width=5 by cpce_flat, cpms_appl, ex2_intro/
148 | #p #V1 #W0 #W1 #X0 #T1 #HV01 #HW01 #HT01 #H1 #H2 destruct
149 elim (cnv_inv_bind … HT0) -HT0 #HW0 #HT0
150 elim (cpce_inv_bind_sn … HT02) -HT02 #W2 #X2 #HW02 #HT02 #H destruct
151 elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
152 [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
153 elim (IH … HW0 … HW01 … HW02 … HL01 … HL02) -HW0
154 [| /2 width=1 by fqup_fpbg/ ] #W #HW1 #HW2
155 elim (IH … HT0 … HT01 … HT02 … (L1.ⓛW1) … (L2.ⓛW2)) -HT0 -HT01 -HT02
156 [|*: /2 width=1 by lpce_pair, fqup_fpbg, lpr_pair/ ] -L0 -V0 -X0 #T #HT1 #HT2
157 @(ex2_intro … (ⓓ{p}ⓝW.V.T))
158 [ @cpce_bind [ /2 width=1 by cpce_flat/ ]
161 | #p #V1 #U1 #W0 #W1 #X0 #T1 #HV01 #HVU1 #HW01 #HT01 #H1 #H2 destruct
162 elim (cnv_inv_bind … HT0) -HT0 #HW0 #HT0
163 elim (cpce_inv_bind_sn … HT02) -HT02 #W2 #X2 #HW02 #HT02 #H destruct
164 elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
165 [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
166 elim (IH … HW0 … HW01 … HW02 … HL01 … HL02) -HW0
167 [| /2 width=1 by fqup_fpbg/ ] #W #HW1 #HW2
168 elim (IH … HT0 … HT01 … HT02 … (L1.ⓓW1) … (L2.ⓓW2)) -HT0 -HT01 -HT02
169 [|*: /2 width=1 by lpce_pair, fqup_fpbg, lpr_pair/ ] -L0 -V0 -X0 #T #HT1 #HT2
170 elim (cpce_lifts_sn … HV1 (Ⓣ) … (L1.ⓓW1) … HVU1) -V1
171 [| /3 width=1 by drops_refl, drops_drop/ ] #U #HVU #HU1
172 /4 width=9 by cpms_theta, cpce_bind, cpce_flat, ex2_intro/
174 | #V0 #T0 #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
175 elim (cnv_inv_cast … H0) -H0 #U0 #HV0 #HT0 #_ #_ -U0
176 elim (cpce_inv_flat_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
177 elim (cpm_inv_cast1 … HX1) -HX1 [ * || * ]
178 [ #V1 #T1 #HV01 #HT01 #H destruct
179 elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
180 [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
181 elim (IH … HT0 … HT01 … HT02 … HL01 … HL02) -HT0 -HT01 -HT02
182 [|*: /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #T #HT1 #HT2
183 /3 width=5 by cpce_flat, cpms_cast, ex2_intro/
185 elim (IH … HT0 … HT01 … HT02 … HL01 … HL02) -HT0 -HT01 -HT02
186 [|*: /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #T #HT1 #HT2
187 /3 width=3 by cpms_eps, ex2_intro/
188 | #m #HV01 #H destruct -HT0 -HT02
189 elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
190 [| /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #V #HV1 #HV2
191 /3 width=3 by cpms_ee, ex2_intro/