--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/rt_conversion/cpce_drops.ma".
+include "basic_2/rt_conversion/lpce_drops.ma".
+include "basic_2/dynamic/cnv_preserve.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+definition IH_cnv_cpce_cpm_conf (h) (a): relation3 genv lenv term ≝
+ λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] →
+ ∀n,T1. ⦃G,L0⦄ ⊢ T0 ➡[n,h] T1 → ∀T2. ⦃G,L0⦄ ⊢ T0 ⬌η[h] T2 →
+ ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ⬌η[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n,h] T.
+
+definition IH_cnv_cpce_cpms_conf (h) (a): relation3 genv lenv term ≝
+ λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] →
+ ∀n,T1. ⦃G,L0⦄ ⊢ T0 ➡*[n,h] T1 → ∀T2. ⦃G,L0⦄ ⊢ T0 ⬌η[h] T2 →
+ ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ⬌η[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n,h] T.
+
+(* Properties with eta-conversion for full local environments ***************)
+
+fact cnv_cpce_cpms_conf_sub (h) (a) (G0) (L0) (T0):
+ (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpm_conf h a G L T) →
+ ∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpms_conf h a G L T.
+#h #a #GX #LX #TX #HX #G #L0 #T0 #HX0 #HT0 #n #X1 #HX1
+@(cpms_ind_dx … HX1) -n -X1
+[ #T2 #HT02 #L1 #HL01 #L2 #HL02
+ /2 width=8 by/
+| #n1 #n2 #T3 #T1 #HT03 #IH #HT31 #T2 #HT02 #L1 #HL01 #L2 #HL02
+ lapply (cnv_cpms_trans … HT0 … HT03) -HT0 #HT3
+ elim (IH … HT02 … L0 … HL02) -IH -HT02 [| // ] #T4 #HT34 #HT24
+ elim (HX … HT3 … HT31 … HT34 … HL01 … HL02)
+ [| /2 width=4 by fpbg_cpms_trans/ ] -GX -LX -L0 -TX -T0 -T3 #T3 #HT13 #HT43
+ /3 width=5 by cpms_trans, ex2_intro/
+]
+qed-.
+
+fact cnv_cpce_cpm_conf_aux (h) (a) (G0) (L0) (T0):
+ (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH_cnv_cpce_cpm_conf h a G L T) →
+ IH_cnv_cpce_cpm_conf h a G0 L0 T0.
+#h #a #G0 #L0 * * [|||| * ]
+[ #s #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
+ elim (cpm_inv_sort1 … HX1) -HX1 #H #Hn destruct
+ lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct
+ /3 width=3 by cpce_sort, ex2_intro/
+| #i #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
+ elim (cnv_inv_lref_drops … H0) -H0 #I #K0 #W0 #HLK0 #HW0
+ elim (lpr_drops_conf … HLK0 … HL01) [| // ] #Y1 #H1 #HLK1
+ elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #HK01 #HW01 #H destruct
+ elim (lpce_drops_conf … HLK0 … HL02) [| // ] #Y2 #H2 #HLK2
+ elim (lpce_inv_pair_sn … H2) -H2 #K2 #W2 #HK02 #HW02 #H destruct
+ elim (cpm_inv_lref1_drops … HX1) -HX1 *
+ [ #H1 #H2 destruct
+ elim (cpce_inv_lref_sn_drops_pair … HX2 … HLK0) -HX2 *
+ [ #H1 #H2 destruct -L0 -K0 -W0
+ /3 width=3 by cpce_ldef_drops, ex2_intro/
+ | #H1 #HW #H2 destruct -L0 -W2 -HW0 -HK02
+ @(ex2_intro … (#i)) [| // ]
+ @(cpce_ldec_drops … HLK1) -HLK1 #n #p #V0 #U0 #HWU0
+ /4 width=10 by lpr_cpms_trans, cpms_step_sn/
+ | lapply (drops_isuni_fwd_drop2 … HLK2) [ // ] -W2 #HLK2
+ #n #p #W01 #W02 #V0 #V01 #V02 #U0 #H1 #HWU0 #HW001 #HW012 #HV001 #HV012 #H2 destruct
+ lapply (cnv_cpms_trans … HW0 … HWU0) #H
+ elim (cnv_inv_bind … H) -H #HV0 #_
+ elim (cnv_cpms_conf_lpr … HW0 … HWU0 0 W1 … K0 … HK01) [| // ]
+ [| /2 width=1 by cpm_cpms/ ] <minus_O_n <minus_n_O #X #H #HWU1
+ elim (cpms_inv_abst_sn … H) -H #V1 #U1 #HV01 #HU01 #H destruct
+ elim (IH … HW0 … HW01 … HW001 … HK01 … HK02) -HW01 -HW001
+ [| /3 width=2 by fqup_fpbg, fqup_lref/ ] #W11 #HW11 #HW011
+ elim (cnv_cpce_cpms_conf_sub … IH … HV0 … HV01 … HV001 … HK01 … HK02) -HV0 -HV01 -HV001
+ [| /4 width=6 by fqup_cpms_fwd_fpbg, fpbg_fqu_trans, fqup_lref/ ] #V11 #HV11 #HV011
+ elim (cpms_lifts_sn … HW011 … HLK2 … HW012) -W01 #W12 #HW112 #HW012
+ elim (cpms_lifts_sn … HV011 … HLK2 … HV012) -V01 #V12 #HV112 #HV012
+ @(ex2_intro …(ⓝW12.+ⓛV12.ⓐ#O.#(↑i)))
+ [ /2 width=14 by cpce_eta_drops/ | /3 width=1 by cpms_cast, cpms_bind/ ]
+ ]
+ | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1
+ #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 -HL01 -HL02
+ lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct
+ lapply (cpce_inv_lref_sn_drops_ldef … HX2 … HLK0) -HX2 #H destruct
+ elim (IH … HW0 … HW01 … HW02 … HK01 … HK02)
+ [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
+ elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
+ /3 width=9 by cpce_lifts_bi, cpms_delta_drops, ex2_intro/
+ | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1
+ #m #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 #H destruct -HL01 -HL02
+ lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct
+ elim (cpce_inv_lref_sn_drops_ldec … HX2 … HLK0) -HX2 *
+ [ #_ #H destruct
+ elim (IH … HW0 … HW01 … HW02 … HK01 … HK02)
+ [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
+ elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
+ /3 width=9 by cpce_lifts_bi, cpms_ell_drops, ex2_intro/
+ | lapply (drops_isuni_fwd_drop2 … HLK2) [ // ] -W2 #HLK2
+ #n #p #W01 #W02 #V0 #V01 #V02 #U0 #_ #HW001 #HW012 #_ #_ #H destruct -V0 -V01 -U0
+ elim (IH … HW0 … HW01 … HW001 … HK01 … HK02)
+ [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
+ elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
+ /4 width=11 by cpce_lifts_bi, cpms_lifts_bi, cpms_ee, ex2_intro/
+ ]
+ ]
+| #l #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
+ elim (cpm_inv_gref1 … HX1) -HX1 #H1 #H2 destruct
+ lapply (cpce_inv_gref_sn … HX2) -HX2 #H destruct
+ /3 width=3 by cpce_gref, cpm_cpms, ex2_intro/
+| #p #I #V0 #T0 #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
+ elim (cnv_inv_bind … H0) -H0 #HV0 #HT0
+ elim (cpce_inv_bind_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
+ elim (cpm_inv_bind1 … HX1) -HX1 *
+ [ #V1 #T1 #HV01 #HT01 #H destruct
+ elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0
+ [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
+ elim (IH … HT0 … HT01 … HT02 … (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -HT0 -HT01 -HT02
+ [|*: /2 width=1 by lpce_pair, fqup_fpbg, lpr_pair/ ] -L0 -V0 -T0 #T #HT1 #HT2
+ /3 width=5 by cpce_bind, cpms_bind, ex2_intro/
+ | #X0 #HXT0 #HX01 #H1 #H2 destruct -HV0 -HV02
+ lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HXT0) -HT0
+ [ /3 width=1 by drops_refl, drops_drop/ ] #HX0
+ elim (cpce_inv_lifts_sn … HT02 (Ⓣ) … L0 … HXT0) -HT02
+ [| /3 width=1 by drops_refl, drops_drop/ ] #X2 #HXT2 #HX02
+ elim (IH … HX0 … HX01 … HX02 … HL01 … HL02) -HX0 -HX01 -HX02
+ [| /3 width=1 by fqup_fpbg, fqup_zeta/ ] -V0 -T0 -X0 #X #HX1 #HX2
+ /3 width=5 by cpms_zeta, ex2_intro/
+ ]
+| #V0 #T0 #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
+ elim (cnv_inv_appl … H0) -H0 #m #p #W0 #U0 #_ #HV0 #HT0 #_ #_ -m -p -W0 -U0
+ elim (cpce_inv_flat_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
+ elim (cpm_inv_appl1 … HX1) -HX1 *
+ [ #V1 #T1 #HV01 #HT01 #H destruct
+ elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
+ [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
+ elim (IH … HT0 … HT01 … HT02 … HL01 … HL02) -HT0 -HT01 -HT02
+ [|*: /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #T #HT1 #HT2
+ /3 width=5 by cpce_flat, cpms_appl, ex2_intro/
+ | #p #V1 #W0 #W1 #X0 #T1 #HV01 #HW01 #HT01 #H1 #H2 destruct
+ elim (cnv_inv_bind … HT0) -HT0 #HW0 #HT0
+ elim (cpce_inv_bind_sn … HT02) -HT02 #W2 #X2 #HW02 #HT02 #H destruct
+ elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
+ [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
+ elim (IH … HW0 … HW01 … HW02 … HL01 … HL02) -HW0
+ [| /2 width=1 by fqup_fpbg/ ] #W #HW1 #HW2
+ elim (IH … HT0 … HT01 … HT02 … (L1.ⓛW1) … (L2.ⓛW2)) -HT0 -HT01 -HT02
+ [|*: /2 width=1 by lpce_pair, fqup_fpbg, lpr_pair/ ] -L0 -V0 -X0 #T #HT1 #HT2
+ @(ex2_intro … (ⓓ{p}ⓝW.V.T))
+ [ @cpce_bind [ /2 width=1 by cpce_flat/ ]
+ | @(cpms_beta) //
+ ]
+ | #p #V1 #U1 #W0 #W1 #X0 #T1 #HV01 #HVU1 #HW01 #HT01 #H1 #H2 destruct
+ elim (cnv_inv_bind … HT0) -HT0 #HW0 #HT0
+ elim (cpce_inv_bind_sn … HT02) -HT02 #W2 #X2 #HW02 #HT02 #H destruct
+ elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
+ [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
+ elim (IH … HW0 … HW01 … HW02 … HL01 … HL02) -HW0
+ [| /2 width=1 by fqup_fpbg/ ] #W #HW1 #HW2
+ elim (IH … HT0 … HT01 … HT02 … (L1.ⓓW1) … (L2.ⓓW2)) -HT0 -HT01 -HT02
+ [|*: /2 width=1 by lpce_pair, fqup_fpbg, lpr_pair/ ] -L0 -V0 -X0 #T #HT1 #HT2
+ elim (cpce_lifts_sn … HV1 (Ⓣ) … (L1.ⓓW1) … HVU1) -V1
+ [| /3 width=1 by drops_refl, drops_drop/ ] #U #HVU #HU1
+ /4 width=9 by cpms_theta, cpce_bind, cpce_flat, ex2_intro/
+ ]
+| #V0 #T0 #IH #H0 #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
+ elim (cnv_inv_cast … H0) -H0 #U0 #HV0 #HT0 #_ #_ -U0
+ elim (cpce_inv_flat_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
+ elim (cpm_inv_cast1 … HX1) -HX1 [ * || * ]
+ [ #V1 #T1 #HV01 #HT01 #H destruct
+ elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
+ [| /2 width=1 by fqup_fpbg/ ] #V #HV1 #HV2
+ elim (IH … HT0 … HT01 … HT02 … HL01 … HL02) -HT0 -HT01 -HT02
+ [|*: /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #T #HT1 #HT2
+ /3 width=5 by cpce_flat, cpms_cast, ex2_intro/
+ | #HT01 -HV0 -HV02
+ elim (IH … HT0 … HT01 … HT02 … HL01 … HL02) -HT0 -HT01 -HT02
+ [|*: /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #T #HT1 #HT2
+ /3 width=3 by cpms_eps, ex2_intro/
+ | #m #HV01 #H destruct -HT0 -HT02
+ elim (IH … HV0 … HV01 … HV02 … HL01 … HL02) -HV0 -HV01 -HV02
+ [| /2 width=1 by fqup_fpbg/ ] -L0 -V0 -T0 #V #HV1 #HV2
+ /3 width=3 by cpms_ee, ex2_intro/
+ ]
+]
projects / helm.git / blobdiff