--- /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_computation/cpms_fpbg.ma".
+include "basic_2/rt_computation/cprs_cprs.ma".
+include "basic_2/rt_computation/lprs_cpms.ma".
+include "basic_2/dynamic/cnv_drops.ma".
+include "basic_2/dynamic/cnv_etc.ma".
+include "basic_2/dynamic/lsubv_cnv.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Properties with context-free parallel reduction for local environments *****)
+
+fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = Ⓕ →
+ ∀G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
+ ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_trans_lpr a h G1 L1 T1.
+#a #h #o #Ha #G0 #L0 #T0 #IH2 #IH1 #G1 #L1 * * [|||| * ]
+[ #s #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #_ destruct -IH2 -IH1 -H1
+ elim (cpm_inv_sort1 … H2) -H2 * #H1 #H2 destruct //
+| #i #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2
+ elim (cnv_inv_lref_drops … H1) -H1 #I #K1 #V1 #HLK1 #HV1
+ elim (lpr_drops_conf … HLK1 … HL12) -HL12 // #Y #H #HLK2
+ elim (lpr_inv_pair_sn … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+ lapply (fqup_lref (Ⓣ) … G1 … HLK1) #HKL
+ elim (cpm_inv_lref1_drops … H2) -H2 *
+ [ #H1 #H2 destruct -HLK1 /4 width=7 by fqup_fpbg, cnv_lref_drops/
+ | #K0 #V0 #W0 #H #HVW0 #W0 -HV12
+ lapply (drops_mono … H … HLK1) -HLK1 -H #H destruct
+ lapply (drops_isuni_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, cnv_lifts/
+ | #n #K0 #V0 #W0 #H #HVW0 #W0 #H destruct -HV12
+ lapply (drops_mono … H … HLK1) -HLK1 -H #H destruct
+ lapply (drops_isuni_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, cnv_lifts/
+ ]
+| #l #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2 -IH1
+ elim (cnv_inv_gref … H1)
+| #p #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2
+ elim (cnv_inv_bind … H1) -H1 #HV1 #HT1
+ elim (cpm_inv_bind1 … H2) -H2 *
+ [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=9 by fqup_fpbg, cnv_bind, lpr_pair/
+ | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1
+ /4 width=11 by fqup_fpbg, cnv_inv_lifts, lpr_pair, drops_refl, drops_drop/
+ ]
+| #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct
+ elim (cnv_inv_appl … H1) -H1 #n #p #W1 #U1 #Hn #HV1 #HT1 #HVW1 #HTU1
+ elim (cpm_inv_appl1 … H2) -H2 *
+ [ #V2 #T2 #HV12 #HT12 #H destruct
+ lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
+ lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
+ elim (cnv_cpms_strip_lpr_far … IH2 … HVW1 … HV12 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV12
+ <minus_n_O <minus_O_n #XW1 #HXW1 #HXV2
+ elim (cnv_cpms_strip_lpr_far … IH2 … HTU1 … HT12 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HTU1 -HT12
+ #X #H #HTU2 -IH2 -IH1 -L1 -V1 -T1
+ elim (cpms_inv_abst_sn … H) -H #W2 #U2 #HW12 #_ #H destruct
+ elim (cprs_conf … HXW1 … HW12) -W1 #W1 #HXW1 #HW21
+ lapply (cpms_trans … HXV2 … HXW1) -XW1 <plus_n_O #HV2W1
+ lapply (cpms_trans … HTU2 … (ⓛ{p}W1.U2) ?)
+ [3:|*: /2 width=2 by cpms_bind/ ] -W2 <plus_n_O #HTU2
+ @(cnv_appl … HV2W1 HTU2) // #H destruct
+ | #q #V2 #W10 #W20 #T10 #T20 #HV12 #HW120 #HT120 #H1 #H2 destruct
+ elim (cnv_inv_bind … HT1) -HT1 #HW10 #HT10
+ elim (cpms_inv_abst_sn … HTU1) -HTU1 #W30 #T30 #HW130 #_ #H destruct -T30
+ lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
+ lapply (IH1 … HW120 … HL12) /2 width=1 by fqup_fpbg/ #HW20
+ lapply (IH1 … HT10 … HT120 … (L2.ⓛW20) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT10 -HT120 #HT20
+ elim (cnv_cpms_strip_lpr_far … IH2 … HVW1 … HV12 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV12
+ <minus_n_O <minus_O_n #XW1 #HXW1 #HXV2
+ elim (cnv_cpms_strip_lpr_far … IH2 … HW130 … HW120 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HW130 -HW120
+ <minus_n_O #XW30 #HXW30 #HW230 -IH2 -IH1 -L1 -V1 -W10 -T10
+ elim (cprs_conf … HXW1 … HXW30) -W30 #W30 #HXW1 #HXW30
+ lapply (cpms_trans … HXV2 … HXW1) -XW1 <plus_n_O #HV2W30
+ lapply (cprs_trans … HW230 … HXW30) -XW30 #HW230
+ /5 width=4 by lsubv_cnv_trans, lsubv_beta, cnv_cast, cnv_bind/
+ | #q #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct
+ elim (cnv_inv_bind … HT1) -HT1 #HW0 #HT0
+ elim (cpms_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct
+ elim (lifts_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct
+ lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ #HW2
+ lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ #HV0
+ lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ #HT2
+ elim (cnv_cpms_strip_lpr_far … IH2 … HVW1 … HV10 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV10
+ <minus_n_O <minus_O_n #XW1 #HXW1 #HXV0
+ elim (cnv_cpms_strip_lpr_far … IH2 … HTU0 … HT02 … (L2.ⓓW2) … (L2.ⓓW2)) [|*: /2 width=2 by fqup_fpbg, lpr_pair/ ] -HTU0 -HT02 -HW02
+ #X #H #HTU2 -IH2 -IH1 -L1 -W0 -T0 -U1
+ elim (cpms_inv_abst_sn … H) -H #W #U2 #HW3 #_ #H destruct -U3
+ lapply (cnv_lifts … HV0 (Ⓣ) … (L2.ⓓW2) … HV02) /3 width=1 by drops_refl, drops_drop/ -HV0 #HV2
+ elim (cpms_lifts_sn … HXV0 (Ⓣ) … (L2.ⓓW2) … HV02) /3 width=1 by drops_refl, drops_drop/ -V0 #XW2 #HXW12 #HXVW2
+ lapply (cpms_lifts_bi … HXW1 (Ⓣ) … (L2.ⓓW2) … HW13 … HXW12) /3 width=1 by drops_refl, drops_drop/ -W1 -XW1 #HXW32
+ elim (cprs_conf … HXW32 … HW3) -W3 #W3 #HXW23 #HW3
+ lapply (cpms_trans … HXVW2 … HXW23) -XW2 <plus_n_O #H1
+ lapply (cpms_trans … HTU2 ? (ⓛ{p}W3.U2) ?) [3:|*:/2 width=2 by cpms_bind/ ] -W #H2
+ @cnv_bind // @(cnv_appl … H1 H2) // #H destruct
+ ]
+| #W1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct
+ elim (cnv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1
+ elim (cpm_inv_cast1 … H2) -H2
+ [ * #W2 #T2 #HW12 #HT12 #H destruct
+ lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbg/ #HW2
+ lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
+ lapply (cnv_cpms_trans_lpr_far … IH1 … HTU1 L1 ?) /2 width=1 by fqup_fpbg/ #HU1
+ elim (cnv_cpms_strip_lpr_far … IH2 … HWU1 … HW12 … L1 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HW12
+ <minus_n_O <minus_O_n #XW1 #HXUW1 #HXW21
+ elim (cnv_cpms_strip_lpr_far … IH2 … HTU1 … HT12 … L1 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HTU1 -HT12
+ #XT1 #HXUT1 #HXT21
+ elim (IH2 … HXUW1 … HXUT1 … HL12 … HL12) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ] -HXUW1 -HXUT1 -HWU1
+ >eq_minus_O // #W0 #H1 #H2 -IH2 -IH1 -L1 -W1 -T1 -U1
+ lapply (cprs_trans … HXW21 … H1) -XW1 #H1
+ lapply (cpms_trans … HXT21 … H2) -XT1 <arith_l #H2
+ /2 width=3 by cnv_cast/
+ | #HX -IH2 -HW1 -U1
+ lapply (IH1 … HX … HL12) /2 width=1 by fqup_fpbg/
+ | * #n #HX #H destruct -IH2 -HT1 -U1
+ lapply (IH1 … HX … HL12) /2 width=1 by fqup_fpbg/
+ ]
+]
+qed-.
∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
-(* Auxiliary properties for preservation ************************************)
+(* Properties for preservation **********************************************)
-fact cnv_cpms_trans_lpr_aux (a) (h) (o):
- ∀G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
- ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_trans_lpr a h G1 L1 T1.
+lemma cnv_cpms_trans_lpr_far (a) (h) (o):
+ ∀G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
+ ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_trans_lpr a h G1 L1 T1.
#a #h #o #G0 #L0 #T0 #IH #G1 #L1 #T1 #H01 #HT1 #n #T2 #H
@(cpms_ind_dx … H) -n -T2
/4 width=7 by cpms_fwd_fpbs, fpbg_fpbs_trans/
qed-.
+
+lemma cnv_cpms_strip_lpr_far (a) (h) (o):
+ ∀G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
+ ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_strip_lpr a h G1 L1 T1.
+/3 width=8 by cpm_cpms/ qed-.
+
(*
fact cnv_cpms_strip_lpr_aux (a) (h) (o):
∀G0,L0,T0.
+++ /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_computation/cpms_fpbg.ma".
-include "basic_2/rt_computation/cprs_cprs.ma".
-include "basic_2/rt_computation/lprs_cpms.ma".
-include "basic_2/dynamic/cnv_drops.ma".
-(*
-include "basic_2/dynamic/snv_aaa.ma".
-*)
-include "basic_2/dynamic/cnv_etc.ma".
-(*
-include "basic_2/dynamic/lsubsv_snv.ma".
-*)
-(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-
-(* Properties with context-free parallel reduction for local environments *****)
-
-fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = Ⓕ →
- ∀G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
- ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_trans_lpr a h G1 L1 T1.
-#a #h #o #Ha #G0 #L0 #T0 (* #IH4 #IH3 *) #IH2 #IH1 #G1 #L1 * * [|||| * ]
-[ #s #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #_ destruct (* -IH4 -IH3 *) -IH2 -IH1 -H1
- elim (cpm_inv_sort1 … H2) -H2 * #H1 #H2 destruct //
-| #i #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct (* -IH4 -IH3 *) -IH2
- elim (cnv_inv_lref_drops … H1) -H1 #I #K1 #V1 #HLK1 #HV1
- elim (lpr_drops_conf … HLK1 … HL12) -HL12 // #Y #H #HLK2
- elim (lpr_inv_pair_sn … H) -H #K2 #V2 #HK12 #HV12 #H destruct
- lapply (fqup_lref (Ⓣ) … G1 … HLK1) #HKL
- elim (cpm_inv_lref1_drops … H2) -H2 *
- [ #H1 #H2 destruct -HLK1 /4 width=7 by fqup_fpbg, cnv_lref_drops/
- | #K0 #V0 #W0 #H #HVW0 #W0 -HV12
- lapply (drops_mono … H … HLK1) -HLK1 -H #H destruct
- lapply (drops_isuni_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, cnv_lifts/
- | #n #K0 #V0 #W0 #H #HVW0 #W0 #H destruct -HV12
- lapply (drops_mono … H … HLK1) -HLK1 -H #H destruct
- lapply (drops_isuni_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, cnv_lifts/
- ]
-| #l #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct (* -IH4 -IH3 *) -IH2 -IH1
- elim (cnv_inv_gref … H1)
-| #p #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct (* -IH4 -IH3 *) -IH2
- elim (cnv_inv_bind … H1) -H1 #HV1 #HT1
- elim (cpm_inv_bind1 … H2) -H2 *
- [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=9 by fqup_fpbg, cnv_bind, lpr_pair/
- | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1
- /4 width=11 by fqup_fpbg, cnv_inv_lifts, lpr_pair, drops_refl, drops_drop/
- ]
-| #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct
- elim (cnv_inv_appl … H1) -H1 #n #p #W1 #U1 #Hn #HV1 #HT1 #HVW1 #HTU1
- elim (cpm_inv_appl1 … H2) -H2 *
- [ #V2 #T2 #HV12 #HT12 #H destruct (* -IH4 *)
- lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
- lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
- elim (IH2 … HVW1 … V2 … L2 … L2) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HVW1 -HV12
- <minus_n_O <minus_O_n #XW1 #HXW1 #HXV2
- elim (IH2 … HTU1 … T2 … L2 … L2) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HTU1 -HT12
- #X #H #HTU2 (* -IH3 *) -IH2 -IH1 -L1 -V1 -T1
- elim (cpms_inv_abst_sn … H) -H #W2 #U2 #HW12 #_ #H destruct
- elim (cprs_conf … HXW1 … HW12) -W1 #W1 #HXW1 #HW21
- lapply (cpms_trans … HXV2 … HXW1) -XW1 <plus_n_O #HV2W1
- lapply (cpms_trans … HTU2 … (ⓛ{p}W1.U2) ?)
- [3:|*: /2 width=2 by cpms_bind/ ] -W2 <plus_n_O #HTU2
- @(cnv_appl … HV2W1 HTU2) // #H destruct
- | #q #V2 #W10 #W20 #T10 #T20 #HV12 #HW120 #HT120 #H1 #H2 destruct
- elim (cnv_inv_bind … HT1) -HT1 #HW10 #HT10
- elim (cpms_inv_abst_sn … HTU1) -HTU1 #W30 #T30 #HW130 #_ #H destruct -T30
- lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
- lapply (IH1 … HW120 … HL12) /2 width=1 by fqup_fpbg/ #HW20
- lapply (IH1 … HT10 … HT120 … (L2.ⓛW20) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT10 -HT120 #HT20
- elim (IH2 … HVW1 … V2 … L2 … L2) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HVW1 -HV12
- <minus_n_O <minus_O_n #XW1 #HXW1 #HXV2
- elim (IH2 … HW130 … W20 … L2 … L2) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HW130 -HW120
- <minus_n_O #XW30 #HXW30 #HW230
- elim (cprs_conf … HXW1 … HXW30) -W30 #W30 #HXW1 #HXW30
- lapply (cpms_trans … HXV2 … HXW1) -XW1 <plus_n_O #HV2W30
- lapply (cprs_trans … HW230 … HXW30) -XW30 #HW230
- @cnv_bind [ /2 width=3 by cnv_cast/ ]
-(*
- @(lsubsv_snv_trans … HT20) -HT20
- @(lsubsv_beta … (d-1)) //
- @shnv_cast [1,2: // ] #d0 #Hd0
- lapply (scpes_le_aux … IH4 IH1 IH2 IH3 … HW20d … HV2d … d0 … HVW20) -IH4 -IH3 -IH2 -IH1 -HW20d -HV2d -HVW20
- /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/
-*)
- | #q #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct (* -IH4 *)
- elim (cnv_inv_bind … HT1) -HT1 #HW0 #HT0
- elim (cpms_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct
- elim (lifts_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct
- lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ #HW2
- lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ #HV0
- lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ #HT2
- elim (IH2 … HVW1 … V0 … L2 … L2) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HVW1 -HV10
- <minus_n_O <minus_O_n #XW1 #HXW1 #HXV0
- elim (IH2 … HTU0 … T2 … (L2.ⓓW2) … (L2.ⓓW2)) [|*: /2 width=2 by fqup_fpbg, cpm_cpms, lpr_pair/ ] -HT02 -HTU0 -HW02
- #X #H #HTU2 -IH2 -IH1
- elim (cpms_inv_abst_sn … H) -H #W #U2 #HW3 #_ #H destruct -U3
- lapply (cnv_lifts … HV0 (Ⓣ) … (L2.ⓓW2) … HV02) /3 width=1 by drops_refl, drops_drop/ -HV0 #HV2
- elim (cpms_lifts_sn … HXV0 (Ⓣ) … (L2.ⓓW2) … HV02) /3 width=1 by drops_refl, drops_drop/ -V0 #XW2 #HXW12 #HXVW2
- lapply (cpms_lifts_bi … HXW1 (Ⓣ) … (L2.ⓓW2) … HW13 … HXW12) /3 width=1 by drops_refl, drops_drop/ -W1 -XW1 #HXW32
- elim (cprs_conf … HXW32 … HW3) -W3 #W3 #HXW23 #HW3
- lapply (cpms_trans … HXVW2 … HXW23) -XW2 <plus_n_O #H1
- lapply (cpms_trans … HTU2 ? (ⓛ{p}W3.U2) ?) [3:|*:/2 width=2 by cpms_bind/ ] -W #H2
- @cnv_bind // @(cnv_appl … H1 H2) // #H destruct
- ]
-| #W1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct (* -IH4 *)
- elim (cnv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1
- elim (cpm_inv_cast1 … H2) -H2
- [ * #W2 #T2 #HW12 #HT12 #H destruct
- lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbg/ #HW2
- lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
- lapply (cnv_cpms_trans_lpr_aux … IH1 … HTU1 L1 ?) /2 width=1 by fqup_fpbg/ #HU1
- elim (IH2 … HWU1 … W2 … L1 … HL12) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HW12
- <minus_n_O <minus_O_n #XW1 #HXUW1 #HXW21
- elim (IH2 … HTU1 … T2 … L1 … HL12) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HTU1 -HT12
- #XT1 #HXUT1 #HXT21
- elim (IH2 … HXUW1 … HXUT1 … HL12 … HL12) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ] -HXUW1 -HXUT1 -HWU1
- >eq_minus_O // #W0 #H1 #H2
- lapply (cprs_trans … HXW21 … H1) -XW1 #H1
- lapply (cpms_trans … HXT21 … H2) -XT1 <arith_l #H2
- /2 width=3 by cnv_cast/
- | #HX (* -IH3 *) -IH2 -HW1 -U1
- lapply (IH1 … HX … HL12) /2 width=1 by fqup_fpbg/
- | * #n #HX #H destruct -IH2 -HT1 -U1
- lapply (IH1 … HX … HL12) /2 width=1 by fqup_fpbg/
- ]
-]
-(*
-qed-.
-*)
+++ /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/notation/relations/lrsubeqv_5.ma".
-include "basic_2/dynamic/shnv.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Note: this is not transitive *)
-inductive lsubsv (h) (o) (G): relation lenv ≝
-| lsubsv_atom: lsubsv h o G (⋆) (⋆)
-| lsubsv_pair: ∀I,L1,L2,V. lsubsv h o G L1 L2 →
- lsubsv h o G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| lsubsv_beta: ∀L1,L2,W,V,d1. ⦃G, L1⦄ ⊢ ⓝW.V ¡[h, o, d1] → ⦃G, L2⦄ ⊢ W ¡[h, o] →
- ⦃G, L1⦄ ⊢ V ▪[h, o] d1+1 → ⦃G, L2⦄ ⊢ W ▪[h, o] d1 →
- lsubsv h o G L1 L2 → lsubsv h o G (L1.ⓓⓝW.V) (L2.ⓛW)
-.
-
-interpretation
- "local environment refinement (stratified native validity)"
- 'LRSubEqV h o G L1 L2 = (lsubsv h o G L1 L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lsubsv_inv_atom1_aux: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → L1 = ⋆ → L2 = ⋆.
-#h #o #G #L1 #L2 * -L1 -L2
-[ //
-| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #W #V #d1 #_ #_ #_ #_ #_ #H destruct
-]
-qed-.
-
-lemma lsubsv_inv_atom1: ∀h,o,G,L2. G ⊢ ⋆ ⫃¡[h, o] L2 → L2 = ⋆.
-/2 width=6 by lsubsv_inv_atom1_aux/ qed-.
-
-fact lsubsv_inv_pair1_aux: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
- ∀I,K1,X. L1 = K1.ⓑ{I}X →
- (∃∃K2. G ⊢ K1 ⫃¡[h, o] K2 & L2 = K2.ⓑ{I}X) ∨
- ∃∃K2,W,V,d1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, o, d1] & ⦃G, K2⦄ ⊢ W ¡[h, o] &
- ⦃G, K1⦄ ⊢ V ▪[h, o] d1+1 & ⦃G, K2⦄ ⊢ W ▪[h, o] d1 &
- G ⊢ K1 ⫃¡[h, o] K2 &
- I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
-#h #o #G #L1 #L2 * -L1 -L2
-[ #J #K1 #X #H destruct
-| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3 by ex2_intro, or_introl/
-| #L1 #L2 #W #V #d1 #HWV #HW #HVd1 #HWd1 #HL12 #J #K1 #X #H destruct /3 width=11 by or_intror, ex8_4_intro/
-]
-qed-.
-
-lemma lsubsv_inv_pair1: ∀h,o,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⫃¡[h, o] L2 →
- (∃∃K2. G ⊢ K1 ⫃¡[h, o] K2 & L2 = K2.ⓑ{I}X) ∨
- ∃∃K2,W,V,d1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, o, d1] & ⦃G, K2⦄ ⊢ W ¡[h, o] &
- ⦃G, K1⦄ ⊢ V ▪[h, o] d1+1 & ⦃G, K2⦄ ⊢ W ▪[h, o] d1 &
- G ⊢ K1 ⫃¡[h, o] K2 &
- I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
-/2 width=3 by lsubsv_inv_pair1_aux/ qed-.
-
-fact lsubsv_inv_atom2_aux: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → L2 = ⋆ → L1 = ⋆.
-#h #o #G #L1 #L2 * -L1 -L2
-[ //
-| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #W #V #d1 #_ #_ #_ #_ #_ #H destruct
-]
-qed-.
-
-lemma lsubsv_inv_atom2: ∀h,o,G,L1. G ⊢ L1 ⫃¡[h, o] ⋆ → L1 = ⋆.
-/2 width=6 by lsubsv_inv_atom2_aux/ qed-.
-
-fact lsubsv_inv_pair2_aux: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
- ∀I,K2,W. L2 = K2.ⓑ{I}W →
- (∃∃K1. G ⊢ K1 ⫃¡[h, o] K2 & L1 = K1.ⓑ{I}W) ∨
- ∃∃K1,V,d1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, o, d1] & ⦃G, K2⦄ ⊢ W ¡[h, o] &
- ⦃G, K1⦄ ⊢ V ▪[h, o] d1+1 & ⦃G, K2⦄ ⊢ W ▪[h, o] d1 &
- G ⊢ K1 ⫃¡[h, o] K2 & I = Abst & L1 = K1.ⓓⓝW.V.
-#h #o #G #L1 #L2 * -L1 -L2
-[ #J #K2 #U #H destruct
-| #I #L1 #L2 #V #HL12 #J #K2 #U #H destruct /3 width=3 by ex2_intro, or_introl/
-| #L1 #L2 #W #V #d1 #HWV #HW #HVd1 #HWd1 #HL12 #J #K2 #U #H destruct /3 width=8 by or_intror, ex7_3_intro/
-]
-qed-.
-
-lemma lsubsv_inv_pair2: ∀h,o,I,G,L1,K2,W. G ⊢ L1 ⫃¡[h, o] K2.ⓑ{I}W →
- (∃∃K1. G ⊢ K1 ⫃¡[h, o] K2 & L1 = K1.ⓑ{I}W) ∨
- ∃∃K1,V,d1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, o, d1] & ⦃G, K2⦄ ⊢ W ¡[h, o] &
- ⦃G, K1⦄ ⊢ V ▪[h, o] d1+1 & ⦃G, K2⦄ ⊢ W ▪[h, o] d1 &
- G ⊢ K1 ⫃¡[h, o] K2 & I = Abst & L1 = K1.ⓓⓝW.V.
-/2 width=3 by lsubsv_inv_pair2_aux/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lsubsv_fwd_lsubr: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → L1 ⫃ L2.
-#h #o #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lsubsv_refl: ∀h,o,G,L. G ⊢ L ⫃¡[h, o] L.
-#h #o #G #L elim L -L /2 width=1 by lsubsv_pair/
-qed.
-
-lemma lsubsv_cprs_trans: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
- ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ➡* T2 → ⦃G, L1⦄ ⊢ T1 ➡* T2.
-/3 width=6 by lsubsv_fwd_lsubr, lsubr_cprs_trans/
-qed-.
-
-(* Note: the constant 0 cannot be generalized *)
-lemma lsubsv_drop_O1_conf: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
- ∀K1,b,k. ⬇[b, 0, k] L1 ≘ K1 →
- ∃∃K2. G ⊢ K1 ⫃¡[h, o] K2 & ⬇[b, 0, k] L2 ≘ K2.
-#h #o #G #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3 by ex2_intro/
-| #I #L1 #L2 #V #_ #IHL12 #K1 #b #k #H
- elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1
- [ destruct
- elim (IHL12 L1 b 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, drop_pair, ex2_intro/
- | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
- ]
-| #L1 #L2 #W #V #d1 #HWV #HW #HVd1 #HWd1 #_ #IHL12 #K1 #b #k #H
- elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1
- [ destruct
- elim (IHL12 L1 b 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_beta, drop_pair, ex2_intro/
- | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
- ]
-]
-qed-.
-
-(* Note: the constant 0 cannot be generalized *)
-lemma lsubsv_drop_O1_trans: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
- ∀K2,b, k. ⬇[b, 0, k] L2 ≘ K2 →
- ∃∃K1. G ⊢ K1 ⫃¡[h, o] K2 & ⬇[b, 0, k] L1 ≘ K1.
-#h #o #G #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3 by ex2_intro/
-| #I #L1 #L2 #V #_ #IHL12 #K2 #b #k #H
- elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2
- [ destruct
- elim (IHL12 L2 b 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, drop_pair, ex2_intro/
- | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
- ]
-| #L1 #L2 #W #V #d1 #HWV #HW #HVd1 #HWd1 #_ #IHL12 #K2 #b #k #H
- elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2
- [ destruct
- elim (IHL12 L2 b 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_beta, drop_pair, ex2_intro/
- | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
- ]
-]
-qed-.
+++ /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/equivalence/cpcs_cpcs.ma".
-include "basic_2/dynamic/lsubsv.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Properties on context-sensitive parallel equivalence for terms ***********)
-
-lemma lsubsv_cpcs_trans: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
- ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2.
-/3 width=6 by lsubsv_fwd_lsubr, lsubr_cpcs_trans/
-qed-.
+++ /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/equivalence/scpes_cpcs.ma".
-include "basic_2/dynamic/lsubsv.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Properties on nat-iterated static type assignment ************************)
-
-lemma lsubsv_lstas_trans: ∀h,o,G,L2,T,U2,d2. ⦃G, L2⦄ ⊢ T •*[h, d2] U2 →
- ∀d1. d2 ≤ d1 → ⦃G, L2⦄ ⊢ T ▪[h, o] d1 →
- ∀L1. G ⊢ L1 ⫃¡[h, o] L2 →
- ∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, d2] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2.
-#h #o #G #L2 #T #U #d2 #H elim H -G -L2 -T -U -d2
-[ /2 width=3 by ex2_intro/
-| #G #L2 #K2 #V #W #U #i #d2 #HLK2 #_ #HWU #IHVW #d1 #Hd21 #Hd1 #L1 #HL12
- elim (da_inv_lref … Hd1) -Hd1 * #K0 #V0 [| #d0 ] #HK0 #HV0
- lapply (drop_mono … HK0 … HLK2) -HK0 #H destruct
- elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #Y #H #HLK1
- elim (lsubsv_inv_pair2 … H) -H * #K1 [ | -HWU -IHVW -HLK1 ]
- [ #HK12 #H destruct
- elim (IHVW … Hd21 HV0 … HK12) -K2 -d1 #T #HVT #HTW
- lapply (drop_fwd_drop2 … HLK1) #H
- elim (lift_total T 0 (i+1))
- /3 width=12 by lstas_ldef, cpcs_lift, ex2_intro/
- | #V0 #d0 #_ #_ #_ #_ #_ #H destruct
- ]
-| #G #L2 #K2 #V #W #i #HLK2 #_ #IHVW #d1 #_ #Hd1 #L1 #HL12
- elim (da_inv_lref … Hd1) -Hd1 * #K0 #V0 [| #d0 ] #HK0 #HV0 [| #H1 ]
- lapply (drop_mono … HK0 … HLK2) -HK0 #H2 destruct
- elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #Y #H #HLK1
- elim (lsubsv_inv_pair2 … H) -H * #K1
- [ #HK12 #H destruct
- elim (IHVW … HV0 … HK12) -K2 /3 width=5 by lstas_zero, ex2_intro/
- | #V1 #d1 #_ #_ #HV1 #HV #HK12 #_ #H destruct
- lapply (da_mono … HV0 … HV) -HV #H destruct
- elim (da_lstas … HV1 0) -HV1 #W1 #HVW1 #_
- elim (lift_total W1 0 (i+1)) #U1 #HWU1
- elim (IHVW … HV0 … HK12) -K2 // #X #HVX #_ -W
- @(ex2_intro … U1) /3 width=6 by lstas_cast, lstas_ldef/ (**) (* full auto too slow *)
- @cpcs_cprs_sn @(cprs_delta … HLK1 … HWU1)
- /4 width=2 by cprs_strap1, cpr_cprs, lstas_cpr, cpr_eps/
- ]
-| #G #L2 #K2 #V #W #U #i #d2 #HLK2 #_ #HWU #IHVW #d1 #Hd21 #Hd1 #L1 #HL12
- elim (da_inv_lref … Hd1) -Hd1 * #K0 #V0 [| #d0 ] #HK0 #HV0 [| #H1 ]
- lapply (drop_mono … HK0 … HLK2) -HK0 #H2 destruct
- lapply (le_plus_to_le_c … Hd21) -Hd21 #Hd21
- elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #Y #H #HLK1
- elim (lsubsv_inv_pair2 … H) -H * #K1
- [ #HK12 #H destruct
- elim (IHVW … Hd21 HV0 … HK12) -K2 -Hd21 #X
- lapply (drop_fwd_drop2 … HLK1)
- elim (lift_total X 0 (i+1))
- /3 width=12 by lstas_succ, cpcs_lift, ex2_intro/
- | #V1 #d1 #H0 #_ #HV1 #HV #HK12 #_ #H destruct
- lapply (da_mono … HV0 … HV) -HV #H destruct
- elim (shnv_inv_cast … H0) -H0 #_ #_ #H
- lapply (H … Hd21) -H #HVV1
- elim (IHVW … Hd21 HV0 … HK12) -K2 -Hd21 #X #HVX #HXW
- elim (da_lstas … HV1 (d2+1)) -HV1 #X1 #HVX1 #_
- lapply (scpes_inv_lstas_eq … HVV1 … HVX … HVX1) -HVV1 -HVX #HXX1
- lapply (cpcs_canc_sn … HXX1 … HXW) -X
- elim (lift_total X1 0 (i+1))
- lapply (drop_fwd_drop2 … HLK1)
- /4 width=12 by cpcs_lift, lstas_cast, lstas_ldef, ex2_intro/
- ]
-| #a #I #G #L2 #V2 #T2 #U2 #d1 #_ #IHTU2 #d2 #Hd12 #Hd2 #L1 #HL12
- lapply (da_inv_bind … Hd2) -Hd2 #Hd2
- elim (IHTU2 … Hd2 (L1.ⓑ{I}V2) …)
- /3 width=3 by lsubsv_pair, lstas_bind, cpcs_bind_dx, ex2_intro/
-| #G #L2 #V2 #T2 #U2 #d1 #_ #IHTU2 #d2 #Hd12 #Hd2 #L1 #HL12
- lapply (da_inv_flat … Hd2) -Hd2 #Hd2
- elim (IHTU2 … Hd2 … HL12) -L2
- /3 width=5 by lstas_appl, cpcs_flat, ex2_intro/
-| #G #L2 #W2 #T2 #U2 #d1 #_ #IHTU2 #d2 #Hd12 #Hd2 #L1 #HL12
- lapply (da_inv_flat … Hd2) -Hd2 #Hd2
- elim (IHTU2 … Hd2 … HL12) -L2
- /3 width=3 by lstas_cast, ex2_intro/
-]
-qed-.
-
-lemma lsubsv_sta_trans: ∀h,o,G,L2,T,U2. ⦃G, L2⦄ ⊢ T •*[h, 1] U2 →
- ∀d. ⦃G, L2⦄ ⊢ T ▪[h, o] d+1 →
- ∀L1. G ⊢ L1 ⫃¡[h, o] L2 →
- ∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, 1] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2.
-/2 width=7 by lsubsv_lstas_trans/ qed-.
+++ /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/equivalence/scpes_aaa.ma".
-include "basic_2/dynamic/snv_aaa.ma".
-include "basic_2/dynamic/lsubsv.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Forward lemmas on lenv refinement for atomic arity assignment ************)
-
-lemma lsubsv_fwd_lsuba: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → G ⊢ L1 ⫃⁝ L2.
-#h #o #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsuba_pair/
-#L1 #L2 #W #V #d1 #H #_ #_ #_ #_ #IHL12
-elim (shnv_inv_cast … H) -H #HW #HV #H
-lapply (H 0 ?) // -d1 #HWV
-elim (snv_fwd_aaa … HW) -HW #B #HW
-elim (snv_fwd_aaa … HV) -HV #A #HV
-lapply (scpes_aaa_mono … HWV … HW … HV) #H destruct
-/4 width=5 by lsuba_aaa_conf, lsuba_beta, aaa_cast/
-qed-.
+++ /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 "static_2/static/lsubd.ma".
-include "basic_2/dynamic/lsubsv.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Forward lemmas on lenv refinement for degree assignment ******************)
-
-lemma lsubsv_fwd_lsubd: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → G ⊢ L1 ⫃▪[h, o] L2.
-#h #o #G #L1 #L2 #H elim H -L1 -L2 /2 width=3 by lsubd_pair, lsubd_beta/
-qed-.
+++ /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 "static_2/static/lsubd_da.ma".
-include "basic_2/dynamic/lsubsv_lsubd.ma".
-include "basic_2/dynamic/lsubsv_lstas.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Properties on decomposed extended parallel computation on terms **********)
-
-lemma lsubsv_scpds_trans: ∀h,o,G,L2,T1,T2,d. ⦃G, L2⦄ ⊢ T1 •*➡*[h, o, d] T2 →
- ∀L1. G ⊢ L1 ⫃¡[h, o] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ T1 •*➡*[h, o, d] T & ⦃G, L1⦄ ⊢ T2 ➡* T.
-#h #o #G #L2 #T1 #T2 #d2 * #T #d1 #Hd21 #Hd1 #HT1 #HT2 #L1 #HL12
-lapply (lsubsv_cprs_trans … HL12 … HT2) -HT2 #HT2
-elim (lsubsv_lstas_trans … HT1 … Hd1 … HL12) // #T0 #HT10 #HT0
-lapply (cpcs_cprs_strap1 … HT0 … HT2) -T #HT02
-elim (cpcs_inv_cprs … HT02) -HT02
-/5 width=5 by lsubsv_fwd_lsubd, lsubd_da_trans, ex4_2_intro, ex2_intro/
-qed-.
+++ /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/dynamic/lsubsv_scpds.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Properties concerning stratified native validity *************************)
-
-lemma lsubsv_snv_trans: ∀h,o,G,L2,T. ⦃G, L2⦄ ⊢ T ¡[h, o] →
- ∀L1. G ⊢ L1 ⫃¡[h, o] L2 → ⦃G, L1⦄ ⊢ T ¡[h, o].
-#h #o #G #L2 #T #H elim H -G -L2 -T //
-[ #I #G #L2 #K2 #V #i #HLK2 #_ #IHV #L1 #HL12
- elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
- elim (lsubsv_inv_pair2 … H) -H * #K1
- [ #HK12 #H destruct /3 width=5 by snv_lref/
- | #W #d #HVW #_ #_ #_ #_ #H1 #H2 destruct -IHV
- /3 width=6 by shnv_inv_snv, snv_lref/
- ]
-| #a #I #G #L2 #V #T #_ #_ #IHV #IHT #L1 #HL12 destruct
- /4 width=1 by snv_bind, lsubsv_pair/
-| #a #G #L2 #V #W0 #T #U0 #d #_ #_ #HVW0 #HTU0 #IHV #IHT #L1 #HL12
- elim (lsubsv_scpds_trans … HVW0 … HL12) -HVW0 #V0 #HV0 #HWV0
- elim (lsubsv_scpds_trans … HTU0 … HL12) -HTU0 #X #HT0 #H
- elim (cprs_inv_abst1 … H) -H #W #T0 #HW0 #_ #H destruct
- elim (cprs_conf … HWV0 … HW0) -W0
- /4 width=10 by snv_appl, scpds_cprs_trans, cprs_bind/
-| #G #L2 #U #T #U0 #_ #_ #HU0 #HTU0 #IHU #IHT #L1 #HL12
- elim (lsubsv_scpds_trans … HTU0 … HL12) -HTU0 #X0 #HTX0 #H1
- elim (lsubsv_scpds_trans … HU0 … HL12) -HU0 #X #HUX #H2
- elim (cprs_conf … H1 … H2) -U0 /3 width=5 by snv_cast, scpds_cprs_trans/
-]
-qed-.
--- /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/notation/relations/lrsubeqv_5.ma".
+include "basic_2/dynamic/cnv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Note: this is not transitive *)
+inductive lsubv (a) (h) (G): relation lenv ≝
+| lsubv_atom: lsubv a h G (⋆) (⋆)
+| lsubv_bind: ∀I,L1,L2. lsubv a h G L1 L2 → lsubv a h G (L1.ⓘ{I}) (L2.ⓘ{I})
+| lsubv_beta: ∀L1,L2,W,V. ⦃G, L1⦄ ⊢ ⓝW.V ![a,h] → ⦃G, L2⦄ ⊢ W ![a,h] →
+ lsubv a h G L1 L2 → lsubv a h G (L1.ⓓⓝW.V) (L2.ⓛW)
+.
+
+interpretation
+ "local environment refinement (native validity)"
+ 'LRSubEqV a h G L1 L2 = (lsubv a h G L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubv_inv_atom_sn_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L1 = ⋆ → L2 = ⋆.
+#a #h #G #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #_ #H destruct
+| #L1 #L2 #W #V #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Basic_2A1: uses: lsubsv_inv_atom1 *)
+lemma lsubv_inv_atom_sn (a) (h) (G): ∀L2. G ⊢ ⋆ ⫃![a,h] L2 → L2 = ⋆.
+/2 width=6 by lsubv_inv_atom_sn_aux/ qed-.
+
+fact lsubv_inv_bind_sn_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
+ ∀I,K1. L1 = K1.ⓘ{I} →
+ ∨∨ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓘ{I}
+ | ∃∃K2,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] & ⦃G, K2⦄ ⊢ W ![a,h] &
+ G ⊢ K1 ⫃![a,h] K2 &
+ I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW.
+#a #h #G #L1 #L2 * -L1 -L2
+[ #J #K1 #H destruct
+| #I #L1 #L2 #HL12 #J #K1 #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #W #V #HWV #HW #HL12 #J #K1 #H destruct /3 width=8 by ex5_3_intro, or_intror/
+]
+qed-.
+
+(* Basic_2A1: uses: lsubsv_inv_pair1 *)
+lemma lsubv_inv_bind_sn (a) (h) (G): ∀I,K1,L2. G ⊢ K1.ⓘ{I} ⫃![a,h] L2 →
+ ∨∨ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓘ{I}
+ | ∃∃K2,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] & ⦃G, K2⦄ ⊢ W ![a,h] &
+ G ⊢ K1 ⫃![a,h] K2 &
+ I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW.
+/2 width=3 by lsubv_inv_bind_sn_aux/ qed-.
+
+fact lsubv_inv_atom_dx_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L2 = ⋆ → L1 = ⋆.
+#a #h #G #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #_ #H destruct
+| #L1 #L2 #W #V #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Basic_2A1: uses: lsubsv_inv_atom2 *)
+lemma lsubv_inv_atom2 (a) (h) (G): ∀L1. G ⊢ L1 ⫃![a,h] ⋆ → L1 = ⋆.
+/2 width=6 by lsubv_inv_atom_dx_aux/ qed-.
+
+fact lsubv_inv_bind_dx_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
+ ∀I,K2. L2 = K2.ⓘ{I} →
+ ∨∨ ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & L1 = K1.ⓘ{I}
+ | ∃∃K1,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] & ⦃G, K2⦄ ⊢ W ![a,h] &
+ G ⊢ K1 ⫃![a,h] K2 & I = BPair Abst W & L1 = K1.ⓓⓝW.V.
+#a #h #G #L1 #L2 * -L1 -L2
+[ #J #K2 #H destruct
+| #I #L1 #L2 #HL12 #J #K2 #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #W #V #HWV #HW #HL12 #J #K2 #H destruct /3 width=8 by ex5_3_intro, or_intror/
+]
+qed-.
+
+(* Basic_2A1: uses: lsubsv_inv_pair2 *)
+lemma lsubv_inv_bind_dx (a) (h) (G): ∀I,L1,K2. G ⊢ L1 ⫃![a,h] K2.ⓘ{I} →
+ ∨∨ ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & L1 = K1.ⓘ{I}
+ | ∃∃K1,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] & ⦃G, K2⦄ ⊢ W ![a,h] &
+ G ⊢ K1 ⫃![a,h] K2 & I = BPair Abst W & L1 = K1.ⓓⓝW.V.
+/2 width=3 by lsubv_inv_bind_dx_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_2A1: uses: lsubsv_refl *)
+lemma lsubv_refl (a) (h) (G): reflexive … (lsubv a h G).
+#a #h #G #L elim L -L /2 width=1 by lsubv_atom, lsubv_bind/
+qed.
--- /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/dynamic/lsubv_cpms.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Forward lemmas with native validity **************************************)
+
+(* Basic_2A1: uses: lsubsv_snv_trans *)
+lemma lsubv_cnv_trans (a) (h) (G):
+ ∀L2,T. ⦃G, L2⦄ ⊢ T ![a,h] →
+ ∀L1. G ⊢ L1 ⫃![a,h] L2 → ⦃G, L1⦄ ⊢ T ![a,h].
+#a #h #G #L2 #T #H elim H -G -L2 -T //
+[ #I #G #K2 #V #HV #IH #L1 #H
+ elim (lsubv_inv_bind_dx … H) -H * /3 width=1 by cnv_zero/
+| #I #G #K2 #i #_ #IH #L1 #H
+ elim (lsubv_inv_bind_dx … H) -H * /3 width=1 by cnv_lref/
+| #p #I #G #L2 #V #T #_ #_ #IHV #IHT #L1 #HL12
+ /4 width=1 by cnv_bind, lsubv_bind/
+| #n #p #G #L2 #V #W #T #U #Ha #_ #_ #HVW #HTU #IHV #IHT #L1 #HL
+ /4 width=10 by lsubv_cpms_trans, cnv_appl/
+| #G #L2 #U #T #U0 #_ #_ #HU0 #HTU0 #IHU #IHT #L1 #HL12
+ /4 width=6 by lsubv_cpms_trans, cnv_cast/
+]
+qed-.
--- /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_equivalence/cpcs_lsubr.ma".
+include "basic_2/dynamic/lsubv_lsubr.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Forward lemmas with context-sensitive r-equivalence for terms ************)
+
+(* Basic_2A1: uses: lsubsv_cprs_trans *)
+lemma lsubv_cpcs_trans (a) (h) (G): lsub_trans … (cpcs h G) (lsubv a h G).
+/3 width=6 by lsubv_fwd_lsubr, lsubr_cpcs_trans/
+qed-.
--- /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_computation/cpms_lsubr.ma".
+include "basic_2/dynamic/lsubv_lsubr.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Forward lemmas with t-bound contex-sensitive rt-computation for terms ****)
+
+(* Basic_2A1: uses: lsubsv_cprs_trans lsubsv_scpds_trans *)
+lemma lsubv_cpms_trans (a) (n) (h) (G): lsub_trans … (λL. cpms h G L n) (lsubv a h G).
+/3 width=6 by lsubv_fwd_lsubr, lsubr_cpms_trans/
+qed-.
--- /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 "static_2/relocation/drops.ma".
+include "basic_2/dynamic/lsubv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Properties with generic slicing for local environments *******************)
+
+(* Note: the premise 𝐔⦃f⦄ cannot be removed *)
+(* Basic_2A1: includes: lsubsv_drop_O1_conf *)
+lemma lsubv_drops_conf_isuni (a) (h) (G):
+ ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
+ ∀b,f,K1. 𝐔⦃f⦄ → ⬇*[b,f] L1 ≘ K1 →
+ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & ⬇*[b,f] L2 ≘ K2.
+#a #h #G #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3 by ex2_intro/
+| #I #L1 #L2 #HL12 #IH #b #f #K1 #Hf #H
+ elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
+ [ #Hf #H destruct -IH
+ /3 width=3 by lsubv_bind, drops_refl, ex2_intro/
+ | #g #Hg #HLK1 #H destruct -HL12
+ elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
+ ]
+| #L1 #L2 #W #V #HVW #HW #HL12 #IH #b #f #K1 #Hf #H
+ elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
+ [ #Hf #H destruct -IH
+ /3 width=3 by drops_refl, lsubv_beta, ex2_intro/
+ | #g #Hg #HLK1 #H destruct -HL12
+ elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
+ ]
+]
+qed-.
+
+(* Note: the premise 𝐔⦃f⦄ cannot be removed *)
+(* Basic_2A1: includes: lsubsv_drop_O1_trans *)
+lemma lsubv_drops_trans_isuni (a) (h) (G):
+ ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
+ ∀b,f,K2. 𝐔⦃f⦄ → ⬇*[b,f] L2 ≘ K2 →
+ ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & ⬇*[b,f] L1 ≘ K1.
+#a #h #G #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3 by ex2_intro/
+| #I #L1 #L2 #HL12 #IH #b #f #K2 #Hf #H
+ elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
+ [ #Hf #H destruct -IH
+ /3 width=3 by lsubv_bind, drops_refl, ex2_intro/
+ | #g #Hg #HLK2 #H destruct -HL12
+ elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
+ ]
+| #L1 #L2 #W #V #HWV #HW #HL12 #IH #b #f #K2 #Hf #H
+ elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
+ [ #Hf #H destruct -IH
+ /3 width=3 by drops_refl, lsubv_beta, ex2_intro/
+ | #g #Hg #HLK2 #H destruct -HL12
+ elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
+ ]
+]
+qed-.
--- /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/dynamic/cnv_aaa.ma".
+include "basic_2/dynamic/lsubv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Forward lemmas with lenv refinement for atomic arity assignment **********)
+
+(* Basic_2A1: uses: lsubsv_fwd_lsuba *)
+lemma lsubsv_fwd_lsuba (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → G ⊢ L1 ⫃⁝ L2.
+#a #h #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsuba_bind/
+#L1 #L2 #W #V #H #_ #_ #IH
+elim (cnv_inv_cast … H) -H #W0 #HW #HV #HW0 #HVW0
+elim (cnv_fwd_aaa … HW) -HW #B #HW
+elim (cnv_fwd_aaa … HV) -HV #A #HV
+lapply (cpms_aaa_conf … HW … HW0) -HW0 #H
+lapply (cpms_aaa_conf … HV … HVW0) -HVW0 #HW0
+lapply (aaa_mono … H … HW0) -W0 #H destruct
+/4 width=5 by lsuba_aaa_conf, lsuba_beta, aaa_cast/
+qed-.
--- /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 "static_2/static/lsubr.ma".
+include "basic_2/dynamic/lsubv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Forward lemmas with restricted refinement for local environments *********)
+
+(* Basic_2A1: uses: lsubsv_fwd_lsubr *)
+lemma lsubv_fwd_lsubr (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L1 ⫃ L2.
+#a #h #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_bind, lsubr_beta/
+qed-.
cnv.ma cnv_drops.ma cnv_fqus.ma cnv_aaa.ma cnv_fsb.ma
-cnv_etc.ma cnv_lpr.ma
+cnv_etc.ma cnv_cpm_trans.ma
+lsubv.ma lsubv_drops.ma lsubv_lsubr.ma lsubv_lsuba.ma lsubv_cpms.ma lsubv_cpcs.ma lsubv_cnv.ma
+++ /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/notation/relations/nativevalid_6.ma".
-include "basic_2/equivalence/scpes.ma".
-include "basic_2/dynamic/snv.ma".
-
-(* STRATIFIED HIGHER NATIVE VALIDITY FOR TERMS ******************************)
-
-inductive shnv (h) (o) (d1) (G) (L): predicate term ≝
-| shnv_cast: ∀U,T. ⦃G, L⦄ ⊢ U ¡[h, o] → ⦃G, L⦄ ⊢ T ¡[h, o] →
- (∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ U •*⬌*[h, o, d2, d2+1] T) →
- shnv h o d1 G L (ⓝU.T)
-.
-
-interpretation "stratified higher native validity (term)"
- 'NativeValid h o d G L T = (shnv h o d G L T).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact shnv_inv_cast_aux: ∀h,o,G,L,X,d1. ⦃G, L⦄ ⊢ X ¡[h, o, d1] → ∀U,T. X = ⓝU.T →
- ∧∧ ⦃G, L⦄ ⊢ U ¡[h, o] & ⦃G, L⦄ ⊢ T ¡[h, o]
- & (∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ U •*⬌*[h, o, d2, d2+1] T).
-#h #o #G #L #X #d1 * -X
-#U #T #HU #HT #HUT #U1 #T1 #H destruct /3 width=1 by and3_intro/
-qed-.
-
-lemma shnv_inv_cast: ∀h,o,G,L,U,T,d1. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, o, d1] →
- ∧∧ ⦃G, L⦄ ⊢ U ¡[h, o] & ⦃G, L⦄ ⊢ T ¡[h, o]
- & (∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ U •*⬌*[h, o, d2, d2+1] T).
-/2 width=3 by shnv_inv_cast_aux/ qed-.
-
-lemma shnv_inv_snv: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ¡[h, o, d] → ⦃G, L⦄ ⊢ T ¡[h, o].
-#h #o #G #L #T #d * -T
-#U #T #HU #HT #HUT elim (HUT 0) -HUT /2 width=3 by snv_cast/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma snv_shnv_cast: ∀h,o,G,L,U,T. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, o] → ⦃G, L⦄ ⊢ ⓝU.T ¡[h, o, 0].
-#h #o #G #L #U #T #H elim (snv_inv_cast … H) -H
-#U0 #HU #HT #HU0 #HTU0 @shnv_cast // -HU -HT
-#d #H <(le_n_O_to_eq … H) -d /2 width=3 by scpds_div/
-qed.
--- /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/notation/relations/lrsubeqv_5.ma".
+include "basic_2/dynamic/shnv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Note: this is not transitive *)
+inductive lsubsv (h) (o) (G): relation lenv ≝
+| lsubsv_atom: lsubsv h o G (⋆) (⋆)
+| lsubsv_pair: ∀I,L1,L2,V. lsubsv h o G L1 L2 →
+ lsubsv h o G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| lsubsv_beta: ∀L1,L2,W,V,d1. ⦃G, L1⦄ ⊢ ⓝW.V ¡[h, o, d1] → ⦃G, L2⦄ ⊢ W ¡[h, o] →
+ ⦃G, L1⦄ ⊢ V ▪[h, o] d1+1 → ⦃G, L2⦄ ⊢ W ▪[h, o] d1 →
+ lsubsv h o G L1 L2 → lsubsv h o G (L1.ⓓⓝW.V) (L2.ⓛW)
+.
+
+interpretation
+ "local environment refinement (stratified native validity)"
+ 'LRSubEqV h o G L1 L2 = (lsubsv h o G L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubsv_inv_atom1_aux: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → L1 = ⋆ → L2 = ⋆.
+#h #o #G #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #W #V #d1 #_ #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+lemma lsubsv_inv_atom1: ∀h,o,G,L2. G ⊢ ⋆ ⫃¡[h, o] L2 → L2 = ⋆.
+/2 width=6 by lsubsv_inv_atom1_aux/ qed-.
+
+fact lsubsv_inv_pair1_aux: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
+ ∀I,K1,X. L1 = K1.ⓑ{I}X →
+ (∃∃K2. G ⊢ K1 ⫃¡[h, o] K2 & L2 = K2.ⓑ{I}X) ∨
+ ∃∃K2,W,V,d1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, o, d1] & ⦃G, K2⦄ ⊢ W ¡[h, o] &
+ ⦃G, K1⦄ ⊢ V ▪[h, o] d1+1 & ⦃G, K2⦄ ⊢ W ▪[h, o] d1 &
+ G ⊢ K1 ⫃¡[h, o] K2 &
+ I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
+#h #o #G #L1 #L2 * -L1 -L2
+[ #J #K1 #X #H destruct
+| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #W #V #d1 #HWV #HW #HVd1 #HWd1 #HL12 #J #K1 #X #H destruct /3 width=11 by or_intror, ex8_4_intro/
+]
+qed-.
+
+lemma lsubsv_inv_pair1: ∀h,o,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⫃¡[h, o] L2 →
+ (∃∃K2. G ⊢ K1 ⫃¡[h, o] K2 & L2 = K2.ⓑ{I}X) ∨
+ ∃∃K2,W,V,d1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, o, d1] & ⦃G, K2⦄ ⊢ W ¡[h, o] &
+ ⦃G, K1⦄ ⊢ V ▪[h, o] d1+1 & ⦃G, K2⦄ ⊢ W ▪[h, o] d1 &
+ G ⊢ K1 ⫃¡[h, o] K2 &
+ I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
+/2 width=3 by lsubsv_inv_pair1_aux/ qed-.
+
+fact lsubsv_inv_atom2_aux: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → L2 = ⋆ → L1 = ⋆.
+#h #o #G #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #W #V #d1 #_ #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+lemma lsubsv_inv_atom2: ∀h,o,G,L1. G ⊢ L1 ⫃¡[h, o] ⋆ → L1 = ⋆.
+/2 width=6 by lsubsv_inv_atom2_aux/ qed-.
+
+fact lsubsv_inv_pair2_aux: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
+ ∀I,K2,W. L2 = K2.ⓑ{I}W →
+ (∃∃K1. G ⊢ K1 ⫃¡[h, o] K2 & L1 = K1.ⓑ{I}W) ∨
+ ∃∃K1,V,d1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, o, d1] & ⦃G, K2⦄ ⊢ W ¡[h, o] &
+ ⦃G, K1⦄ ⊢ V ▪[h, o] d1+1 & ⦃G, K2⦄ ⊢ W ▪[h, o] d1 &
+ G ⊢ K1 ⫃¡[h, o] K2 & I = Abst & L1 = K1.ⓓⓝW.V.
+#h #o #G #L1 #L2 * -L1 -L2
+[ #J #K2 #U #H destruct
+| #I #L1 #L2 #V #HL12 #J #K2 #U #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #W #V #d1 #HWV #HW #HVd1 #HWd1 #HL12 #J #K2 #U #H destruct /3 width=8 by or_intror, ex7_3_intro/
+]
+qed-.
+
+lemma lsubsv_inv_pair2: ∀h,o,I,G,L1,K2,W. G ⊢ L1 ⫃¡[h, o] K2.ⓑ{I}W →
+ (∃∃K1. G ⊢ K1 ⫃¡[h, o] K2 & L1 = K1.ⓑ{I}W) ∨
+ ∃∃K1,V,d1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, o, d1] & ⦃G, K2⦄ ⊢ W ¡[h, o] &
+ ⦃G, K1⦄ ⊢ V ▪[h, o] d1+1 & ⦃G, K2⦄ ⊢ W ▪[h, o] d1 &
+ G ⊢ K1 ⫃¡[h, o] K2 & I = Abst & L1 = K1.ⓓⓝW.V.
+/2 width=3 by lsubsv_inv_pair2_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lsubsv_fwd_lsubr: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → L1 ⫃ L2.
+#h #o #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lsubsv_refl: ∀h,o,G,L. G ⊢ L ⫃¡[h, o] L.
+#h #o #G #L elim L -L /2 width=1 by lsubsv_pair/
+qed.
+
+lemma lsubsv_cprs_trans: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
+ ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ➡* T2 → ⦃G, L1⦄ ⊢ T1 ➡* T2.
+/3 width=6 by lsubsv_fwd_lsubr, lsubr_cprs_trans/
+qed-.
+
+(* Note: the constant 0 cannot be generalized *)
+lemma lsubsv_drop_O1_conf: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
+ ∀K1,b,k. ⬇[b, 0, k] L1 ≘ K1 →
+ ∃∃K2. G ⊢ K1 ⫃¡[h, o] K2 & ⬇[b, 0, k] L2 ≘ K2.
+#h #o #G #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3 by ex2_intro/
+| #I #L1 #L2 #V #_ #IHL12 #K1 #b #k #H
+ elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1
+ [ destruct
+ elim (IHL12 L1 b 0) -IHL12 // #X #HL12 #H
+ <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, drop_pair, ex2_intro/
+ | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
+ ]
+| #L1 #L2 #W #V #d1 #HWV #HW #HVd1 #HWd1 #_ #IHL12 #K1 #b #k #H
+ elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1
+ [ destruct
+ elim (IHL12 L1 b 0) -IHL12 // #X #HL12 #H
+ <(drop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_beta, drop_pair, ex2_intro/
+ | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
+ ]
+]
+qed-.
+
+(* Note: the constant 0 cannot be generalized *)
+lemma lsubsv_drop_O1_trans: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
+ ∀K2,b, k. ⬇[b, 0, k] L2 ≘ K2 →
+ ∃∃K1. G ⊢ K1 ⫃¡[h, o] K2 & ⬇[b, 0, k] L1 ≘ K1.
+#h #o #G #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3 by ex2_intro/
+| #I #L1 #L2 #V #_ #IHL12 #K2 #b #k #H
+ elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2
+ [ destruct
+ elim (IHL12 L2 b 0) -IHL12 // #X #HL12 #H
+ <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, drop_pair, ex2_intro/
+ | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
+ ]
+| #L1 #L2 #W #V #d1 #HWV #HW #HVd1 #HWd1 #_ #IHL12 #K2 #b #k #H
+ elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2
+ [ destruct
+ elim (IHL12 L2 b 0) -IHL12 // #X #HL12 #H
+ <(drop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_beta, drop_pair, ex2_intro/
+ | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
+ ]
+]
+qed-.
--- /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/equivalence/cpcs_cpcs.ma".
+include "basic_2/dynamic/lsubsv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Properties on context-sensitive parallel equivalence for terms ***********)
+
+lemma lsubsv_cpcs_trans: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
+ ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2.
+/3 width=6 by lsubsv_fwd_lsubr, lsubr_cpcs_trans/
+qed-.
--- /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/equivalence/scpes_cpcs.ma".
+include "basic_2/dynamic/lsubsv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Properties on nat-iterated static type assignment ************************)
+
+lemma lsubsv_lstas_trans: ∀h,o,G,L2,T,U2,d2. ⦃G, L2⦄ ⊢ T •*[h, d2] U2 →
+ ∀d1. d2 ≤ d1 → ⦃G, L2⦄ ⊢ T ▪[h, o] d1 →
+ ∀L1. G ⊢ L1 ⫃¡[h, o] L2 →
+ ∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, d2] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2.
+#h #o #G #L2 #T #U #d2 #H elim H -G -L2 -T -U -d2
+[ /2 width=3 by ex2_intro/
+| #G #L2 #K2 #V #W #U #i #d2 #HLK2 #_ #HWU #IHVW #d1 #Hd21 #Hd1 #L1 #HL12
+ elim (da_inv_lref … Hd1) -Hd1 * #K0 #V0 [| #d0 ] #HK0 #HV0
+ lapply (drop_mono … HK0 … HLK2) -HK0 #H destruct
+ elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #Y #H #HLK1
+ elim (lsubsv_inv_pair2 … H) -H * #K1 [ | -HWU -IHVW -HLK1 ]
+ [ #HK12 #H destruct
+ elim (IHVW … Hd21 HV0 … HK12) -K2 -d1 #T #HVT #HTW
+ lapply (drop_fwd_drop2 … HLK1) #H
+ elim (lift_total T 0 (i+1))
+ /3 width=12 by lstas_ldef, cpcs_lift, ex2_intro/
+ | #V0 #d0 #_ #_ #_ #_ #_ #H destruct
+ ]
+| #G #L2 #K2 #V #W #i #HLK2 #_ #IHVW #d1 #_ #Hd1 #L1 #HL12
+ elim (da_inv_lref … Hd1) -Hd1 * #K0 #V0 [| #d0 ] #HK0 #HV0 [| #H1 ]
+ lapply (drop_mono … HK0 … HLK2) -HK0 #H2 destruct
+ elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #Y #H #HLK1
+ elim (lsubsv_inv_pair2 … H) -H * #K1
+ [ #HK12 #H destruct
+ elim (IHVW … HV0 … HK12) -K2 /3 width=5 by lstas_zero, ex2_intro/
+ | #V1 #d1 #_ #_ #HV1 #HV #HK12 #_ #H destruct
+ lapply (da_mono … HV0 … HV) -HV #H destruct
+ elim (da_lstas … HV1 0) -HV1 #W1 #HVW1 #_
+ elim (lift_total W1 0 (i+1)) #U1 #HWU1
+ elim (IHVW … HV0 … HK12) -K2 // #X #HVX #_ -W
+ @(ex2_intro … U1) /3 width=6 by lstas_cast, lstas_ldef/ (**) (* full auto too slow *)
+ @cpcs_cprs_sn @(cprs_delta … HLK1 … HWU1)
+ /4 width=2 by cprs_strap1, cpr_cprs, lstas_cpr, cpr_eps/
+ ]
+| #G #L2 #K2 #V #W #U #i #d2 #HLK2 #_ #HWU #IHVW #d1 #Hd21 #Hd1 #L1 #HL12
+ elim (da_inv_lref … Hd1) -Hd1 * #K0 #V0 [| #d0 ] #HK0 #HV0 [| #H1 ]
+ lapply (drop_mono … HK0 … HLK2) -HK0 #H2 destruct
+ lapply (le_plus_to_le_c … Hd21) -Hd21 #Hd21
+ elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #Y #H #HLK1
+ elim (lsubsv_inv_pair2 … H) -H * #K1
+ [ #HK12 #H destruct
+ elim (IHVW … Hd21 HV0 … HK12) -K2 -Hd21 #X
+ lapply (drop_fwd_drop2 … HLK1)
+ elim (lift_total X 0 (i+1))
+ /3 width=12 by lstas_succ, cpcs_lift, ex2_intro/
+ | #V1 #d1 #H0 #_ #HV1 #HV #HK12 #_ #H destruct
+ lapply (da_mono … HV0 … HV) -HV #H destruct
+ elim (shnv_inv_cast … H0) -H0 #_ #_ #H
+ lapply (H … Hd21) -H #HVV1
+ elim (IHVW … Hd21 HV0 … HK12) -K2 -Hd21 #X #HVX #HXW
+ elim (da_lstas … HV1 (d2+1)) -HV1 #X1 #HVX1 #_
+ lapply (scpes_inv_lstas_eq … HVV1 … HVX … HVX1) -HVV1 -HVX #HXX1
+ lapply (cpcs_canc_sn … HXX1 … HXW) -X
+ elim (lift_total X1 0 (i+1))
+ lapply (drop_fwd_drop2 … HLK1)
+ /4 width=12 by cpcs_lift, lstas_cast, lstas_ldef, ex2_intro/
+ ]
+| #a #I #G #L2 #V2 #T2 #U2 #d1 #_ #IHTU2 #d2 #Hd12 #Hd2 #L1 #HL12
+ lapply (da_inv_bind … Hd2) -Hd2 #Hd2
+ elim (IHTU2 … Hd2 (L1.ⓑ{I}V2) …)
+ /3 width=3 by lsubsv_pair, lstas_bind, cpcs_bind_dx, ex2_intro/
+| #G #L2 #V2 #T2 #U2 #d1 #_ #IHTU2 #d2 #Hd12 #Hd2 #L1 #HL12
+ lapply (da_inv_flat … Hd2) -Hd2 #Hd2
+ elim (IHTU2 … Hd2 … HL12) -L2
+ /3 width=5 by lstas_appl, cpcs_flat, ex2_intro/
+| #G #L2 #W2 #T2 #U2 #d1 #_ #IHTU2 #d2 #Hd12 #Hd2 #L1 #HL12
+ lapply (da_inv_flat … Hd2) -Hd2 #Hd2
+ elim (IHTU2 … Hd2 … HL12) -L2
+ /3 width=3 by lstas_cast, ex2_intro/
+]
+qed-.
+
+lemma lsubsv_sta_trans: ∀h,o,G,L2,T,U2. ⦃G, L2⦄ ⊢ T •*[h, 1] U2 →
+ ∀d. ⦃G, L2⦄ ⊢ T ▪[h, o] d+1 →
+ ∀L1. G ⊢ L1 ⫃¡[h, o] L2 →
+ ∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, 1] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2.
+/2 width=7 by lsubsv_lstas_trans/ qed-.
--- /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/equivalence/scpes_aaa.ma".
+include "basic_2/dynamic/snv_aaa.ma".
+include "basic_2/dynamic/lsubsv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Forward lemmas on lenv refinement for atomic arity assignment ************)
+
+lemma lsubsv_fwd_lsuba: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → G ⊢ L1 ⫃⁝ L2.
+#h #o #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsuba_pair/
+#L1 #L2 #W #V #d1 #H #_ #_ #_ #_ #IHL12
+elim (shnv_inv_cast … H) -H #HW #HV #H
+lapply (H 0 ?) // -d1 #HWV
+elim (snv_fwd_aaa … HW) -HW #B #HW
+elim (snv_fwd_aaa … HV) -HV #A #HV
+lapply (scpes_aaa_mono … HWV … HW … HV) #H destruct
+/4 width=5 by lsuba_aaa_conf, lsuba_beta, aaa_cast/
+qed-.
--- /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 "static_2/static/lsubd.ma".
+include "basic_2/dynamic/lsubsv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Forward lemmas on lenv refinement for degree assignment ******************)
+
+lemma lsubsv_fwd_lsubd: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → G ⊢ L1 ⫃▪[h, o] L2.
+#h #o #G #L1 #L2 #H elim H -L1 -L2 /2 width=3 by lsubd_pair, lsubd_beta/
+qed-.
--- /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 "static_2/static/lsubd_da.ma".
+include "basic_2/dynamic/lsubsv_lsubd.ma".
+include "basic_2/dynamic/lsubsv_lstas.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Properties on decomposed extended parallel computation on terms **********)
+
+lemma lsubsv_scpds_trans: ∀h,o,G,L2,T1,T2,d. ⦃G, L2⦄ ⊢ T1 •*➡*[h, o, d] T2 →
+ ∀L1. G ⊢ L1 ⫃¡[h, o] L2 →
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 •*➡*[h, o, d] T & ⦃G, L1⦄ ⊢ T2 ➡* T.
+#h #o #G #L2 #T1 #T2 #d2 * #T #d1 #Hd21 #Hd1 #HT1 #HT2 #L1 #HL12
+lapply (lsubsv_cprs_trans … HL12 … HT2) -HT2 #HT2
+elim (lsubsv_lstas_trans … HT1 … Hd1 … HL12) // #T0 #HT10 #HT0
+lapply (cpcs_cprs_strap1 … HT0 … HT2) -T #HT02
+elim (cpcs_inv_cprs … HT02) -HT02
+/5 width=5 by lsubsv_fwd_lsubd, lsubd_da_trans, ex4_2_intro, ex2_intro/
+qed-.
--- /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/dynamic/lsubsv_scpds.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Properties concerning stratified native validity *************************)
+
+lemma lsubsv_snv_trans: ∀h,o,G,L2,T. ⦃G, L2⦄ ⊢ T ¡[h, o] →
+ ∀L1. G ⊢ L1 ⫃¡[h, o] L2 → ⦃G, L1⦄ ⊢ T ¡[h, o].
+#h #o #G #L2 #T #H elim H -G -L2 -T //
+[ #I #G #L2 #K2 #V #i #HLK2 #_ #IHV #L1 #HL12
+ elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
+ elim (lsubsv_inv_pair2 … H) -H * #K1
+ [ #HK12 #H destruct /3 width=5 by snv_lref/
+ | #W #d #HVW #_ #_ #_ #_ #H1 #H2 destruct -IHV
+ /3 width=6 by shnv_inv_snv, snv_lref/
+ ]
+| #a #I #G #L2 #V #T #_ #_ #IHV #IHT #L1 #HL12 destruct
+ /4 width=1 by snv_bind, lsubsv_pair/
+| #a #G #L2 #V #W0 #T #U0 #d #_ #_ #HVW0 #HTU0 #IHV #IHT #L1 #HL12
+ elim (lsubsv_scpds_trans … HVW0 … HL12) -HVW0 #V0 #HV0 #HWV0
+ elim (lsubsv_scpds_trans … HTU0 … HL12) -HTU0 #X #HT0 #H
+ elim (cprs_inv_abst1 … H) -H #W #T0 #HW0 #_ #H destruct
+ elim (cprs_conf … HWV0 … HW0) -W0
+ /4 width=10 by snv_appl, scpds_cprs_trans, cprs_bind/
+| #G #L2 #U #T #U0 #_ #_ #HU0 #HTU0 #IHU #IHT #L1 #HL12
+ elim (lsubsv_scpds_trans … HTU0 … HL12) -HTU0 #X0 #HTX0 #H1
+ elim (lsubsv_scpds_trans … HU0 … HL12) -HU0 #X #HUX #H2
+ elim (cprs_conf … H1 … H2) -U0 /3 width=5 by snv_cast, scpds_cprs_trans/
+]
+qed-.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T ¡ [ break term 46 h, break term 46 o, break term 46 d ] )"
+ non associative with precedence 45
+ for @{ 'NativeValid $h $o $d $G $L $T }.
--- /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/notation/relations/nativevalid_6.ma".
+include "basic_2/equivalence/scpes.ma".
+include "basic_2/dynamic/snv.ma".
+
+(* STRATIFIED HIGHER NATIVE VALIDITY FOR TERMS ******************************)
+
+inductive shnv (h) (o) (d1) (G) (L): predicate term ≝
+| shnv_cast: ∀U,T. ⦃G, L⦄ ⊢ U ¡[h, o] → ⦃G, L⦄ ⊢ T ¡[h, o] →
+ (∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ U •*⬌*[h, o, d2, d2+1] T) →
+ shnv h o d1 G L (ⓝU.T)
+.
+
+interpretation "stratified higher native validity (term)"
+ 'NativeValid h o d G L T = (shnv h o d G L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact shnv_inv_cast_aux: ∀h,o,G,L,X,d1. ⦃G, L⦄ ⊢ X ¡[h, o, d1] → ∀U,T. X = ⓝU.T →
+ ∧∧ ⦃G, L⦄ ⊢ U ¡[h, o] & ⦃G, L⦄ ⊢ T ¡[h, o]
+ & (∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ U •*⬌*[h, o, d2, d2+1] T).
+#h #o #G #L #X #d1 * -X
+#U #T #HU #HT #HUT #U1 #T1 #H destruct /3 width=1 by and3_intro/
+qed-.
+
+lemma shnv_inv_cast: ∀h,o,G,L,U,T,d1. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, o, d1] →
+ ∧∧ ⦃G, L⦄ ⊢ U ¡[h, o] & ⦃G, L⦄ ⊢ T ¡[h, o]
+ & (∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ U •*⬌*[h, o, d2, d2+1] T).
+/2 width=3 by shnv_inv_cast_aux/ qed-.
+
+lemma shnv_inv_snv: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ¡[h, o, d] → ⦃G, L⦄ ⊢ T ¡[h, o].
+#h #o #G #L #T #d * -T
+#U #T #HU #HT #HUT elim (HUT 0) -HUT /2 width=3 by snv_cast/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma snv_shnv_cast: ∀h,o,G,L,U,T. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, o] → ⦃G, L⦄ ⊢ ⓝU.T ¡[h, o, 0].
+#h #o #G #L #U #T #H elim (snv_inv_cast … H) -H
+#U0 #HU #HT #HU0 #HTU0 @shnv_cast // -HU -HT
+#d #H <(le_n_O_to_eq … H) -d /2 width=3 by scpds_div/
+qed.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( G ⊢ break term 46 L1 ⫃ ¡ [ break term 46 h, break term 46 o ] break term 46 L2 )"
+notation "hvbox( G ⊢ break term 46 L1 ⫃![ break term 46 a, break term 46 h ] break term 46 L2 )"
non associative with precedence 45
- for @{ 'LRSubEqV $h $o $G $L1 $L2 }.
+ for @{ 'LRSubEqV $a $h $G $L1 $L2 }.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T ¡ [ break term 46 h, break term 46 o, break term 46 d ] )"
- non associative with precedence 45
- for @{ 'NativeValid $h $o $d $G $L $T }.
[ [ "" ] "nta ( ⦃?,?⦄ ⊢ ? : ? )" "nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_aaa" "nta_sta" "nta_ltpr" "nta_nta" * ]
}
]
- [ { "local env. ref. for stratified native validity" * } {
- [ [ "" ] "lsubsv ( ? ⊢ ? ⫃¡[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_scpds" + "lsubsv_cpcs" + "lsubsv_snv" * ]
- }
- ]
-*)
- [ { "context-sensitive native validity" * } {
-(*
- [ [ "" ] "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ]
*)
- [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" (* + "snv_lpr" + "snv_scpes" + "snv_preserve" *) * ]
+ [ { "context-sensitive native validity" * } {
+ [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" * ]
+ [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "snv_cpm_trans" (* + "snv_scpes" + "snv_preserve" *) * ]
}
]
}
class "italic" { 2 }
(*
+ [ [ "" ] "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ]
[ { "decomposed rt-equivalence" * } {
[ [ "" ] "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ]
}
projects / helm.git / commitdiff