From: Ferruccio Guidi Date: Thu, 16 May 2013 14:35:06 +0000 (+0000) Subject: - some renaming X-Git-Tag: make_still_working~1154 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=947126ce0618ffdfc39cdc7e198c1edbf3b1a926;p=helm.git - some renaming - finally we issue the "dynamic" component --- diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma index 1c60d6c18..f830afff1 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/notation.ma @@ -14,6 +14,10 @@ (* NOTATION FOR THE "functional" COMPONENT ********************************) +notation "hvbox( T . break ④ { term 46 I } break { term 46 T1 , break term 46 T2 , break term 46 T3 } )" + non associative with precedence 50 + for @{ 'DxItem4 $T $I $T1 $T2 $T3 }. + notation "hvbox( ↑ [ term 46 d , break term 46 e ] break term 46 T )" non associative with precedence 46 for @{ 'Lift $d $e $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma index 9666bffdd..04af871fe 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma @@ -19,9 +19,9 @@ include "basic_2/dynamic/lsubsv_ssta.ma". (* Properties for the preservation results **********************************) -fact sstas_lsubsv_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → +fact lsubsv_sstas_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) → ∀L2,T. h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T⦄ → ⦃h, L2⦄ ⊢ T ¡[g] → @@ -35,14 +35,14 @@ lapply (snv_sstas_aux … IH2 … HTU2) // #H lapply (IH1 … H … HL12) [ /3 width=4 by ygt_yprs_trans, sstas_yprs/ ] -H #HU2 elim (snv_fwd_ssta … HU1) #l1 #W1 #HUW1 elim (lsubsv_ssta_trans … HU2W … HL12) -HU2W #W2 #HUW2 #HW2 -elim (ssta_ltpr_cpcs_aux … IH4 IH3 … HU1 HU2 … HUW1 … HUW2 … HU12) -HU1 -HU2 -HUW2 -HU12 // +elim (ssta_cpcs_lpr_aux … IH4 IH3 … HU1 HU2 … HUW1 … HUW2 … HU12 L1) -HU1 -HU2 -HUW2 -HU12 // [2,3: /4 width=4 by ygt_yprs_trans, sstas_yprs, lsubsv_yprs/ ] -L2 -L0 -T0 -U2 #H #HW12 destruct lapply (cpcs_trans … HW12 … HW2) -W2 /3 width=4/ qed-. -fact dxprs_lsubsv_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → +fact lsubsv_dxprs_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) → ∀L2,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T1⦄ → ⦃h, L2⦄ ⊢ T1 ¡[g] → @@ -50,7 +50,7 @@ fact dxprs_lsubsv_aux: ∀h,g,L0,T0. ∃∃T. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T & L1 ⊢ T2 ➡* T. #h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 #T1 #HLT0 #HT1 #L1 #HL12 #T2 * #T #HT1T #HTT2 lapply (lsubsv_cprs_trans … HL12 … HTT2) -HTT2 #HTT2 -elim (sstas_lsubsv_aux … IH4 IH3 IH2 IH1 … HLT0 … HL12 … HT1T) // -L2 -L0 -T0 #T0 #HT10 #HT0 +elim (lsubsv_sstas_aux … IH4 IH3 IH2 IH1 … HLT0 … HL12 … HT1T) // -L2 -L0 -T0 #T0 #HT10 #HT0 lapply (cpcs_cprs_strap1 … HT0 … HTT2) -T #HT02 elim (cpcs_inv_cprs … HT02) -HT02 /3 width=3/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma index 1482dd986..896875371 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma @@ -22,8 +22,8 @@ include "basic_2/dynamic/lsubsv_cpcs.ma". (* Properties concerning stratified native validity *************************) fact snv_lsubsv_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) → ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_lsubsv h g L1 T1. @@ -45,8 +45,8 @@ fact snv_lsubsv_aux: ∀h,g,L0,T0. lapply (lsubsv_cprs_trans … HL12 … HW0) -HW0 #HW0 elim (lsubsv_ssta_trans … HVW … HL12) -HVW #W1 #HVW1 #HW1 lapply (cpcs_cprs_strap1 … HW1 … HW0) -W #HW10 - elim (dxprs_lsubsv_aux … IH4 IH3 IH2 IH1 … HL12 … HTU) -IH4 -IH3 -IH2 -HTU // /2 width=1/ #X #HTU #H - elim (cprs_inv_abst1 Abst W0 … H) -H #W #U2 #HW0 #HU2 #H destruct + elim (lsubsv_dxprs_aux … IH4 IH3 IH2 IH1 … HL12 … HTU) -IH4 -IH3 -IH2 -HTU // /2 width=1/ #X #HTU #H + elim (cprs_fwd_abst1 … H Abst W0) -H #W #U2 #HW0 #HU2 #H destruct lapply (cpcs_cprs_strap1 … HW10 … HW0) -W0 #H elim (cpcs_inv_cprs … H) -H #W0 #HW10 #HW0 lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU ?) [ /2 width=1/ ] -HTU -HW0 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma index 643bf6569..f00ae1832 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma @@ -29,11 +29,11 @@ definition IH_ssta_cpr_lpr: ∀h:sh. sd h → relation2 lenv term ≝ λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[g] → ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → ∀T2. L1 ⊢ T1 ➡ T2 → ∀L2. L1 ⊢ ➡ L2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L1 ⊢ U1 ⬌* U2. + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2. definition IH_snv_ssta: ∀h:sh. sd h → relation2 lenv term ≝ - λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[g] → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ⦃h, L1⦄ ⊢ U1 ¡[g]. + λh,g,L,T. ⦃h, L⦄ ⊢ T ¡[g] → + ∀U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄ → ⦃h, L⦄ ⊢ U ¡[g]. definition IH_snv_lsubsv: ∀h:sh. sd h → relation2 lenv term ≝ λh,g,L2,T. ⦃h, L2⦄ ⊢ T ¡[g] → @@ -55,41 +55,51 @@ fact ssta_cprs_lpr_aux: ∀h,g,L0,T0. (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → - ∀T2. L1 ⊢ T1 ➡* T2 → ∀L2. L1 ⊢ ➡ L2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L1 ⊢ U1 ⬌* U2. + ∀T2. L1 ⊢ T1 ➡* T2 → ∀L2. L1 ⊢ ➡ L2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2. #h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #l #HTU1 #T2 #H -elim H -T2 [ /2 width=5/ ] +elim H -T2 [ /2 width=7/ ] #T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12 elim (IHT1 L1) // -IHT1 #U #HTU #HU1 -elim (IH1 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2 -HL12 +elim (IH1 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2 [2: /3 width=9 by snv_cprs_lpr_aux/ |3: /5 width=6 by ygt_yprs_trans, cprs_yprs/ ] -L0 -T0 -T1 -T #U2 #HTU2 #HU2 +lapply (cpcs_lpr_conf … HL12 … HU1) -L1 #HU1 lapply (cpcs_trans … HU1 … HU2) -U /2 width=3/ qed-. -fact ssta_cpcs_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → - ∀L,T1,T2. h ⊢ ⦃L0, T0⦄ >[g] ⦃L, T1⦄ → h ⊢ ⦃L0, T0⦄ >[g] ⦃L, T2⦄ → - ⦃h, L⦄ ⊢ T1 ¡[g] → ⦃h, L⦄ ⊢ T2 ¡[g] → - ∀U1,l1. ⦃h, L⦄ ⊢ T1 •[g] ⦃l1, U1⦄ → - ∀U2,l2. ⦃h, L⦄ ⊢ T2 •[g] ⦃l2, U2⦄ → - L ⊢ T1 ⬌* T2 → l1 = l2 ∧ L ⊢ U1 ⬌* U2. -#h #g #L0 #T0 #IH2 #IH1 #L #T1 #T2 #HLT01 #HLT02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #H +fact ssta_cpcs_lpr_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → + ∀L1,T1,T2. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T2⦄ → + ⦃h, L1⦄ ⊢ T1 ¡[g] → ⦃h, L1⦄ ⊢ T2 ¡[g] → + ∀U1,l1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l1, U1⦄ → + ∀U2,l2. ⦃h, L1⦄ ⊢ T2 •[g] ⦃l2, U2⦄ → + L1 ⊢ T1 ⬌* T2 → ∀L2. L1 ⊢ ➡ L2 → + l1 = l2 ∧ L2 ⊢ U1 ⬌* U2. +#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #T2 #H01 #H02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #H #L2 #HL12 elim (cpcs_inv_cprs … H) -H #T #H1 #H2 -elim (ssta_cprs_lpr_aux … HLT01 HT1 … HTU1 … H1 L) -T1 // /2 width=1/ #W1 #H1 #HUW1 -elim (ssta_cprs_lpr_aux … HLT02 HT2 … HTU2 … H2 L) -T2 // /2 width=1/ #W2 #H2 #HUW2 -L0 -T0 +elim (ssta_cprs_lpr_aux … H01 HT1 … HTU1 … H1 … HL12) -T1 /2 width=1/ #W1 #H1 #HUW1 +elim (ssta_cprs_lpr_aux … H02 HT2 … HTU2 … H2 … HL12) -T2 /2 width=1/ #W2 #H2 #HUW2 -L0 -T0 elim (ssta_mono … H1 … H2) -h -T #H1 #H2 destruct lapply (cpcs_canc_dx … HUW1 … HUW2) -W2 /2 width=1/ qed-. fact snv_sstas_aux: ∀h,g,L0,T0. (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → - ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → ⦃h, L1⦄ ⊢ U1 ¡[g]. -#h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #U1 #H -@(sstas_ind … H) -U1 // -HT1 /4 width=5 by ygt_yprs_trans, sstas_yprs/ + ∀L,T. h ⊢ ⦃L0, T0⦄ >[g] ⦃L, T⦄ → ⦃h, L⦄ ⊢ T ¡[g] → + ∀U. ⦃h, L⦄ ⊢ T •*[g] U → ⦃h, L⦄ ⊢ U ¡[g]. +#h #g #L0 #T0 #IH #L #T #H01 #HT #U #H +@(sstas_ind … H) -U // -HT /4 width=5 by ygt_yprs_trans, sstas_yprs/ +qed-. + +fact snv_sstas_lpr_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → + ∀L1,T. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T⦄ → ⦃h, L1⦄ ⊢ T ¡[g] → + ∀U. ⦃h, L1⦄ ⊢ T •*[g] U → ∀L2. L1 ⊢ ➡ L2 → ⦃h, L2⦄ ⊢ U ¡[g]. +/4 width=7 by snv_sstas_aux, ygt_yprs_trans, sstas_yprs/ qed-. fact sstas_cprs_lpr_aux: ∀h,g,L0,T0. @@ -97,45 +107,50 @@ fact sstas_cprs_lpr_aux: ∀h,g,L0,T0. (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → - ∀T2. L1 ⊢ T1 ➡* T2 → ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → ∀L2. L1 ⊢ ➡ L2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L1 ⊢ U1 ⬌* U2. -#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #L2 #HL12 #T2 #HT12 #U1 #H -@(sstas_ind … H) -U1 [ /3 width=3/ ] -#U1 #W1 #l1 #HTU1 #HUW1 * #U2 #HTU2 #HU12 -lapply (snv_ltpr_cprs_aux … IH2 … HT1 … HT12) // #HT2 + ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → ∀T2. L1 ⊢ T1 ➡* T2 → ∀L2. L1 ⊢ ➡ L2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L2 ⊢ U1 ⬌* U2. +#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #H +@(sstas_ind … H) -U1 [ /3 width=5 by cprs_lpr_conf, ex2_intro/ ] +#U1 #W1 #l1 #HTU1 #HUW1 #IHTU1 #T2 #HT12 #L2 #HL12 +elim (IHTU1 … HT12 … HL12) -IHTU1 #U2 #HTU2 #HU12 +lapply (snv_cprs_lpr_aux … IH2 … HT1 … HT12 … HL12) // #HT2 elim (snv_sstas_fwd_correct … HTU2) // #W2 #l2 #HUW2 -elim (ssta_ltpr_cpcs_aux … IH2 IH1 … HUW1 … HUW2 … HU12) -IH2 -IH1 -HUW1 -HU12 // -[2: /4 width=8 by snv_sstas_aux, ygt_yprs_trans, ltpr_cprs_yprs/ -|3: /3 width=7 by snv_sstas_aux, ygt_yprs_trans, cprs_yprs/ -|4: /4 width=5 by ygt_yprs_trans, ltpr_cprs_yprs, sstas_yprs/ -|5: /3 width=4 by ygt_yprs_trans, cprs_yprs, sstas_yprs/ -] -L0 -T0 -T1 -HT2 #H #HW12 destruct /3 width=4/ +elim (IH1 … HUW1 U1 … HL12) -HUW1 // +[2: /3 width=7 by snv_sstas_aux/ +|3: /3 width=4 by ygt_yprs_trans, sstas_yprs/ +] #W #HU1W #HW1 +elim (ssta_cpcs_lpr_aux … IH2 IH1 … HU1W … HUW2 … HU12 L2) // -IH1 -HU1W -HU12 +[2: /4 width=8 by snv_sstas_aux, ygt_yprs_trans, cprs_lpr_yprs/ +|3: /3 width=10 by snv_sstas_lpr_aux/ +|4,5: /4 width=5 by ygt_yprs_trans, cprs_lpr_yprs, sstas_yprs/ +] -L0 -T0 -L1 -T1 -HT2 #H #HW12 destruct +lapply (cpcs_trans … HW1 … HW12) -W /3 width=4/ qed-. -fact dxprs_ltpr_cprs_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → - ∀U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 → - ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[g] U2 & L2 ⊢ U1 ➡* U2. -#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 * #W1 #HTW1 #HWU1 #L2 #HL12 #T2 #HT12 -elim (sstas_ltpr_cprs_aux … IH3 IH2 IH1 … H01 … HT12 … HTW1) // -L0 -T0 -T1 #W2 #HTW2 #HW12 -lapply (ltpr_cprs_conf … HL12 … HWU1) -L1 #HWU1 +fact dxprs_cprs_lpr_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → + ∀U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 → + ∀T2. L1 ⊢ T1 ➡* T2 → ∀L2. L1 ⊢ ➡ L2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[g] U2 & L2 ⊢ U1 ➡* U2. +#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 * #W1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12 +elim (sstas_cprs_lpr_aux … IH3 IH2 IH1 … H01 … HTW1 … HT12 … HL12) // -L0 -T0 -T1 #W2 #HTW2 #HW12 +lapply (cprs_lpr_conf … HL12 … HWU1) -L1 #HWU1 lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H elim (cpcs_inv_cprs … H) -H /3 width=3/ qed-. fact ssta_dxprs_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → - ∀l,U1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ∀T2. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2 → - ∃∃U,U2. ⦃h, L1⦄ ⊢ U1 •*[g] U & ⦃h, L1⦄ ⊢ T2 •*[g] U2 & L1 ⊢ U ⬌* U2. -#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2 + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → + ∀L,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L, T1⦄ → ⦃h, L⦄ ⊢ T1 ¡[g] → + ∀l,U1. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ∀T2. ⦃h, L⦄ ⊢ T1 •*➡*[g] T2 → + ∃∃U,U2. ⦃h, L⦄ ⊢ U1 •*[g] U & ⦃h, L⦄ ⊢ T2 •*[g] U2 & L ⊢ U ⬌* U2. +#h #g #L0 #T0 #IH2 #IH1 #L #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2 elim (sstas_strip … HT1T … HTU1) #HU1T destruct [ -HT1T | -L0 -T0 -T1 ] -[ elim (ssta_ltpr_cprs_aux … IH2 IH1 … HTU1 L1 … HTT2) // -L0 -T0 -T /3 width=5/ +[ elim (ssta_cprs_lpr_aux … IH2 IH1 … HTU1 … HTT2 L) // -L0 -T0 -T /3 width=5/ | @(ex3_2_intro …T2 HU1T) // /2 width=1/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma new file mode 100644 index 000000000..44a77627c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma @@ -0,0 +1,140 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/dxprs_dxprs.ma". +include "basic_2/dynamic/snv_lift.ma". +include "basic_2/dynamic/snv_cpcs.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* Properties on context-free parallel reduction for local environments *****) + +fact snv_cpr_lpr_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → + ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_cpr_lpr h g L1 T1. +#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L1 * * [||||*] +[ #k #HL0 #HT0 #H1 #X #H2 #L2 #_ destruct -IH4 -IH3 -IH2 -IH1 -H1 + >(cpr_inv_sort1 … H2) -X // +| #i #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 + elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1 + elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 + elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct + lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKL + elim (cpr_inv_lref1 … H2) -H2 + [ #H destruct -HLK1 + lapply (IH1 … HV12 … HK12) -IH1 -HV12 -HK12 // -HV1 [ /2 width=1/ ] -HKL /2 width=5/ + | * #K0 #V0 #W0 #H #HVW0 #W0 -HV12 + lapply (ldrop_mono … H … HLK1) -HLK1 -H #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2 + lapply (IH1 … HVW0 … HK12) -IH1 -HVW0 -HK12 // -HV1 [ /2 width=1/ ] -HKL /3 width=7/ + ] +| #p #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1 + elim (snv_inv_gref … H1) +| #a #I #V1 #T1 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 + elim (snv_inv_bind … H1) -H1 #HV1 #HT1 + elim (cpr_inv_bind1 … H2) -H2 * + [ #V2 #T2 #HV12 #HT12 #H destruct + lapply (IH1 … HV12 … HL12) // -HV1 [ /2 width=1/ ] #HV2 + lapply (IH1 … HT12 (L2.ⓑ{I}V2) ?) // -IH1 /2 width=1/ + | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1 + lapply (IH1 … HT1 … HT12 (L2.ⓓV1) ?) -IH1 [1,2: /2 width=1/ ] -L1 -T1 #HT2 + lapply (snv_inv_lift … HT2 L2 … HXT2) -T2 // /2 width=1/ + ] +| #V1 #T1 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct + elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1 + elim (cpr_inv_appl1 … H2) -H2 * + [ #V2 #T2 #HV12 #HT12 #H destruct -IH4 + lapply (IH1 … HV1 … HV12 … HL12) [ /2 width=1/ ] #HV2 + lapply (IH1 … HT1 … HT12 … HL12) [ /2 width=1/ ] #HT2 + elim (IH3 … HVW1 … HV12 … HL12) -HVW1 -HV12 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12 + elim (dxprs_cprs_lpr_aux … IH2 IH1 IH3 … HTU1 … T2 … HL12) // [2,3: /2 width=1/ ] -IH2 -IH1 -IH3 -HT1 -HT12 -HTU1 #X #HTU2 #H + elim (cprs_fwd_abst1 … H Abst W1) -H #W20 #U2 #HW120 #_ #H destruct + lapply (cprs_lpr_conf … HL12 … HW10) -L1 #HW10 + lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120 + lapply (cpcs_canc_sn … HW12 HW120) -W10 #HW20 + elim (cpcs_inv_cprs … HW20) -HW20 #W0 #HW20 #HW200 + lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?) [ /2 width=1/ ] -HW200 -HTU2 /2 width=8/ + | #b #V2 #W20 #T20 #T2 #HV12 #HT202 #H1 #H2 destruct + elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20 + elim (dxprs_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30 + lapply (cprs_div … HW10 … HW230) -W30 #HW120 + lapply (cpcs_lpr_conf … HL12 … HW120) -HW120 #HW120 + elim (IH3 … HVW1 … HV12 … HL12) // [2: /2 width=1/ ] -HVW1 #W2 #HVW2 #HW102 + lapply (cpcs_canc_sn … HW102 … HW120) -W10 #HW220 + lapply (IH1 … HV12 … HL12) // [ /2 width=1/ ] #HV2 -HV1 + lapply (IH1 … HW20 … W20 … HL12) // [ /2 width=1/ ] -HW20 #HW20 + lapply (IH1 … HT20 … HT202 … (L2.ⓛW20) ?) [1,2: /2 width=1/ ] -HT20 #HT2 + lapply (IH2 … HVW2) // + [ @(ygt_yprs_trans … L1 L1 … V1) (**) (* auto /4 width=5/ is a bit slow even with trace *) + [ /2 width=1 by fw_ygt/ + | /3 width=1 by cprs_lpr_yprs, cpr_cprs/ + ] + ] #HW2 + elim (snv_fwd_ssta … HW20) #l0 #U20 #HWU20 + elim (ssta_fwd_correct … HVW2) [g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → - ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_ltpr_tpr h g L1 T1. -#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L1 * * [||||*] -[ #k #HL0 #HT0 #H1 #L2 #_ #X #H2 destruct -IH4 -IH3 -IH2 -IH1 -L1 - >(tpr_inv_atom1 … H2) -X // -| #i #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2 - elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1 - >(tpr_inv_atom1 … H2) -X - elim (ltpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 - elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) -HLK1 #HLK1 - lapply (IH1 … HK12 … HV12) -IH1 -HV12 -HK12 // -HV1 [ /2 width=1/ ] -HLK1 /2 width=5/ -| #p #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2 -IH1 - elim (snv_inv_gref … H1) -| #a #I #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2 - elim (snv_inv_bind … H1) -H1 #HV1 #HT1 - elim (tpr_inv_bind1 … H2) -H2 * - [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct - lapply (tps_lsubr_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02 - lapply (IH1 … HL12 … HV12) // [ /2 width=1/ ] #HV2 - lapply (snv_ltpr_cpr_aux … HT1 (L2.ⓑ{I}V2) … T2 ?) -HT1 - [ /3 width=5 by cpr_intro, tps_tpss/ | /2 width=1/ | /3 width=1/ ] -IH1 -T0 /2 width=1/ - | #T2 #HT12 #HXT2 #H1 #H2 destruct - lapply (IH1 … HT1 (L2.ⓓV1) … HT12) -IH1 -HT1 -HT12 [1,2: /2 width=1/ ] -HL12 #HT2 - lapply (snv_inv_lift … HT2 L2 … HXT2) -T2 // /2 width=1/ - ] -| #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct - elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1 - elim (tpr_inv_appl1 … H2) -H2 * - [ #V2 #T2 #HV12 #HT12 #H destruct -IH4 - lapply (IH1 … HV1 … HL12 … HV12) [ /2 width=1/ ] #HV2 - lapply (IH1 … HT1 … HL12 … HT12) [ /2 width=1/ ] #HT2 - elim (IH3 … HVW1 … HL12 … HV12) -HVW1 -HV12 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12 - elim (dxprs_ltpr_cprs_aux … IH2 IH1 IH3 … HTU1 … HL12 T2) // [2: /3 width=1/ |3: /2 width=1/ ] -IH2 -IH1 -IH3 -HT1 -HT12 -HTU1 #X #HTU2 #H - elim (cprs_inv_abst1 Abst W1 … H) -H #W20 #U2 #HW120 #_ #H destruct - lapply (ltpr_cprs_conf … HL12 … HW10) -L1 #HW10 - lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120 - lapply (cpcs_canc_sn … HW12 HW120) -W10 #HW20 - elim (cpcs_inv_cprs … HW20) -HW20 #W0 #HW20 #HW200 - lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?) [ /2 width=1/ ] -HW200 -HTU2 /2 width=8/ - | #b #V2 #W20 #T20 #T2 #HV12 #HT202 #H1 #H2 destruct - elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20 - elim (dxprs_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30 - lapply (cprs_div … HW10 … HW230) -W30 #HW120 - elim (snv_fwd_ssta … HW20) #l0 #U20 #HWU20 - elim (ssta_fwd_correct … HVW1) [g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_ssta h g L1 T1. #h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [||||*] @@ -44,7 +45,7 @@ fact snv_ssta_aux: ∀h,g,L0,T0. elim (ssta_dxprs_aux … IH3 IH2 … HTU1 … HT10) -IH3 -IH2 // /2 width=2/ -T1 #U #X #HU1U #H #HU0 elim (sstas_inv_bind1 … H) -H #U0 #HTU0 #H destruct elim (cpcs_inv_abst2 … HU0) -HU0 #W2 #U2 #HU2 #HU02 - elim (cprs_inv_abst … HU02 Abst W0) -HU02 #HW02 #_ + elim (cprs_fwd_abst … HU02 Abst W0) -HU02 #HW02 #_ lapply (cprs_trans … HW10 … HW02) -W0 /3 width=10 by snv_appl, ex2_intro/ (**) (* auto is too slow without trace *) | #W1 #T1 #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2 elim (snv_inv_cast … H1) -H1 #U1 #l0 #HW1 #HT1 #HTU1 #HUW1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma new file mode 100644 index 000000000..e03920285 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma @@ -0,0 +1,126 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lsubss_ssta.ma". +include "basic_2/dynamic/snv_cpcs.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* Properties on sn parallel reduction for local environments ***************) + +fact ssta_cpr_lpr_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → + ∀L1,T1. L0 = L1 → T0 = T1 → IH_ssta_cpr_lpr h g L1 T1. +#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [|||| *] +[ #k #_ #_ #_ #X2 #l #H2 #X3 #H3 #L2 #HL12 -IH3 -IH2 -IH1 + elim (ssta_inv_sort1 … H2) -H2 #Hkl #H destruct + >(cpr_inv_sort1 … H3) -X3 /4 width=6/ +| #i #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2 + elim (snv_inv_lref … H1) -H1 #I0 #K0 #V0 #H #HV1 + elim (ssta_inv_lref1 … H2) -H2 * #K1 + #V1 #W1 [| #l0 ] #HLK1 #HVW1 #HWU1 [| #H destruct ] + lapply (ldrop_mono … H … HLK1) -H #H destruct + lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 + elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 + elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) #H2 + elim (cpr_inv_lref1 … H3) -H3 + [1,3: #H destruct -HLK1 + |2,4: * #K0 #V0 #W0 #H #HVW0 #HW0 + lapply (ldrop_mono … H … HLK1) -H -HLK1 #H destruct + ] + [ elim (IH1 … HVW1 … HV12 … HK12) -IH1 -HVW1 // [2: /2 width=1/ ] -K1 -V1 #W2 #HVW2 #HW12 + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (cpcs_lift … H2 … HWU1 … HWU2 HW12) -H2 -W1 /3 width=6/ + | elim (IH1 … HVW1 … HV12 … HK12) -IH1 -HVW1 // [2: /2 width=1/ ] #W2 #HVW2 #_ + elim (lift_total V2 0 (i+1)) #U2 #HVU2 + lapply (lpr_cpr_conf … HK12 … HV12) -HV12 #HV12 + lapply (cpcs_lift … H2 … HWU1 … HVU2 HV12) -H2 -V1 /3 width=6/ + | elim (IH1 … HVW1 … HVW0 … HK12) -IH1 -HVW1 // [2: /2 width=1/ ] -K1 -V1 #W2 #HVW2 #HW12 + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (ssta_lift … HVW2 … H2 … HW0 … HWU2) -HVW2 -HW0 + lapply (cpcs_lift … H2 … HWU1 … HWU2 HW12) -H2 -W1 /3 width=6/ + ] +| #p #_ #HT0 #H1 destruct -IH3 -IH2 -IH1 + elim (snv_inv_gref … H1) +| #a #I #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2 + elim (snv_inv_bind … H1) -H1 #_ #HT1 + elim (ssta_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct + elim (cpr_inv_bind1 … H3) -H3 * + [ #V2 #T2 #HV12 #HT12 #H destruct + elim (IH1 … HTU1 … HT12 (L2.ⓑ{I}V2)) // [2,3: /2 width=1/ ] -T1 + lapply (lpr_cpr_conf … HL12 … HV12) -L1 /3 width=5/ + | #T2 #HT12 #HT2 #H1 #H2 destruct + elim (IH1 … HTU1 … HT12 (L2.ⓓV1)) -IH1 -HTU1 // [2,3: /2 width=1/ ] -T1 -HL12 #U2 #HTU2 #HU12 + elim (ssta_inv_lift1 … HTU2 … HT2) -T2 [3: /2 width=1/ |2: skip ] #U #HXU #HU2 + lapply (cpcs_bind1 true … V1 V1 … HU12) // -HU12 #HU12 + lapply (cpcs_cpr_strap1 … HU12 U ?) -HU12 /2 width=3/ + ] +| #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct + elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #HVW1 #HW10 #HTU10 + elim (ssta_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct + elim (cpr_inv_appl1 … H3) -H3 * + [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH3 -IH2 + elim (IH1 … HTU1 … HT12 … HL12) -IH1 -HTU1 // [2: /2 width=1/ ] -T1 #U2 #HTU2 #HU12 + lapply (lpr_cpr_conf … HL12 … HV12) -L1 /3 width=5/ + | #b #V2 #W #T2 #T20 #HV12 #HT20 #H1 #H2 destruct + elim (snv_inv_bind … HT1) -HT1 #HW #HT2 + elim (ssta_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct + elim (dxprs_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW0 #_ #H destruct + lapply (cprs_div … HW10 … HW0) -W0 #HW1W + elim (ssta_fwd_correct … HVW1) [g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → - ∀L1,T1. L0 = L1 → T0 = T1 → IH_ssta_ltpr_tpr h g L1 T1. -#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [|||| *] -[ #k #_ #_ #_ #X2 #l #H2 #L2 #HL12 #X3 #H3 -IH3 -IH2 -IH1 - elim (ssta_inv_sort1 … H2) -H2 #Hkl #H destruct - >(tpr_inv_atom1 … H3) -X3 /4 width=6/ -| #i #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct -IH3 -IH2 - elim (snv_inv_lref … H1) -H1 #I0 #K0 #V0 #H #HV1 - elim (ssta_inv_lref1 … H2) -H2 * #K1 - >(tpr_inv_atom1 … H3) -X3 - [ #V1 #W1 #HLK1 #HVW1 #HWU1 - lapply (ldrop_mono … H … HLK1) -H #H destruct - lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 - elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 - elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - elim (IH1 … HVW1 … HK12 … HV12) -IH1 -HVW1 -HV12 // [2: /2 width=1/ ] -V1 #W2 #HVW2 #HW12 - lapply (ldrop_fwd_ldrop2 … HLK2) #H2 - elim (lift_total W2 0 (i+1)) #U2 #HWU2 - lapply (cpcs_lift … H2 … HWU1 … HWU2 HW12) -H2 -W1 /3 width=6/ - | #V1 #W1 #l0 #HLK1 #HVW1 #HVU1 #H destruct - lapply (ldrop_mono … H … HLK1) -H #H destruct - lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 - elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 #X #H #HLK2 - elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - elim (IH1 … HVW1 … HK12 … HV12) -IH1 -HVW1 -HK12 // [2: /2 width=1/ ] -HV1 -HKV1 #W2 #HVW2 #_ -W1 - elim (lift_total V2 0 (i+1)) #U2 #HVU2 - lapply (tpr_lift … HV12 … HVU1 … HVU2) -V1 /4 width=6/ - ] -| #p #_ #HT0 #H1 destruct -IH3 -IH2 -IH1 - elim (snv_inv_gref … H1) -| #a #I #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct -IH3 -IH2 - elim (snv_inv_bind … H1) -H1 #_ #HT1 - elim (ssta_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct - elim (tpr_inv_bind1 … H3) -H3 * - [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct - lapply (tps_lsubr_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 [ /2 width=1/ ] #HT02 - elim (ssta_ltpr_cpr_aux … HT1 … HTU1 (L2.ⓑ{I}V2) … T2) -HT1 -HTU1 - [2: /3 width=5 by cpr_intro, tps_tpss/ |3: /2 width=1/ |4: /3 width=1/ ] -IH1 -T0 -HL12 #U2 #HTU2 #HU12 - lapply (cpcs_bind2 … V1 … HU12 … a) -HU12 [ /2 width=1/ ] -HV12 /3 width=3/ - | #T2 #HT12 #HT2 #H1 #H2 destruct - elim (IH1 … HTU1 (L2.ⓓV1) … T2) -IH1 -HTU1 // [2,3: /2 width=1/ ] -T1 -HL12 #U2 #HTU2 #HU12 - lapply (cpcs_bind1 … HU12 … V1 … true) // -HU12 #HU12 - elim (ssta_inv_lift1 … HTU2 … HT2) -T2 [3: /2 width=1/ |2: skip ] #U #HXU #HU2 - lapply (cpcs_cpr_strap1 … HU12 U ?) -HU12 [ /3 width=3/ ] -U2 /2 width=3/ - ] -| #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct - elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #HVW1 #HW10 #HTU10 - elim (ssta_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct - elim (tpr_inv_appl1 … H3) -H3 * - [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH3 -IH2 - elim (IH1 … HTU1 … HL12 … HT12) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -T1 #U2 #HTU2 #HU12 - lapply (cpcs_flat … V1 V2 … HU12) -HU12 [ /2 width=1/ ] -HV12 /3 width=3/ - | #b #V2 #W #T2 #T20 #HV12 #HT20 #H1 #H2 destruct - elim (snv_inv_bind … HT1) -HT1 #HW #HT2 - elim (ssta_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct - elim (dxprs_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW0 #_ #H destruct - lapply (cprs_div … HW10 … HW0) -W0 #HW1W - elim (ssta_fwd_correct … HVW1) [g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → + ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊢ T2 ¡[g]. +#h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #L2 #HL12 #T2 #H +@(cprs_ind … H) -T2 [ /2 width=6 by snv_ltpr_cpr_aux/ ] -HT1 +/5 width=6 by snv_ltpr_cpr_aux, ygt_yprs_trans, ltpr_cprs_yprs/ +qed-. + +fact ssta_ltpr_cprs_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → + ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → + ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2. +#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #l #HTU1 #L2 #HL12 #T2 #H +@(cprs_ind … H) -T2 [ /2 width=7 by ssta_ltpr_cpr_aux/ ] +#T #T2 #HT1T #HTT2 * #U #HTU #HU1 +elim (ssta_ltpr_cpr_aux … HTU … HTT2) // +[2: /3 width=9 by snv_ltpr_cprs_aux/ +|3: /5 width=6 by ygt_yprs_trans, ltpr_cprs_yprs/ +] -L0 -L1 -T0 -T1 -T #U2 #HTU2 #HU2 +lapply (cpcs_trans … HU1 … HU2) -U /2 width=3/ +qed-. + +fact ssta_ltpr_cpcs_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → + ∀L1,L2,T1,T2. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T2⦄ → + ⦃h, L1⦄ ⊢ T1 ¡[g] → ⦃h, L2⦄ ⊢ T2 ¡[g] → + ∀U1,l1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l1, U1⦄ → + ∀U2,l2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l2, U2⦄ → + L1 ➡ L2 → L2 ⊢ T1 ⬌* T2 → + l1 = l2 ∧ L2 ⊢ U1 ⬌* U2. +#h #g #L0 #T0 #IH2 #IH1 #L1 #L2 #T1 #T2 #HLT01 #HLT02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #HL12 #H +elim (cpcs_inv_cprs … H) -H #T #H1 #H2 +elim (ssta_ltpr_cprs_aux … HLT01 HT1 … HTU1 … H1) -T1 /2 width=1/ #W1 #H1 #HUW1 +elim (ssta_ltpr_cprs_aux … HLT02 HT2 … HTU2 … H2) -T2 /2 width=1/ #W2 #H2 #HUW2 -L1 -L0 -T0 +elim (ssta_mono … H1 … H2) -h -T #H1 #H2 destruct +lapply (cpcs_canc_dx … HUW1 … HUW2) -W2 /2 width=1/ +qed-. + +fact snv_sstas_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → + ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → ⦃h, L1⦄ ⊢ U1 ¡[g]. +#h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #U1 #H +@(sstas_ind … H) -U1 // -HT1 /4 width=5 by ygt_yprs_trans, sstas_yprs/ +qed-. + +fact sstas_ltpr_cprs_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → + ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L2 ⊢ U1 ⬌* U2. +#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #L2 #HL12 #T2 #HT12 #U1 #H +@(sstas_ind … H) -U1 [ /3 width=3/ ] +#U1 #W1 #l1 #HTU1 #HUW1 * #U2 #HTU2 #HU12 +lapply (snv_ltpr_cprs_aux … IH2 … HT1 … HT12) // #HT2 +elim (snv_sstas_fwd_correct … HTU2) // #W2 #l2 #HUW2 +elim (ssta_ltpr_cpcs_aux … IH2 IH1 … HUW1 … HUW2 … HU12) -IH2 -IH1 -HUW1 -HU12 // +[2: /4 width=8 by snv_sstas_aux, ygt_yprs_trans, ltpr_cprs_yprs/ +|3: /3 width=7 by snv_sstas_aux, ygt_yprs_trans, cprs_yprs/ +|4: /4 width=5 by ygt_yprs_trans, ltpr_cprs_yprs, sstas_yprs/ +|5: /3 width=4 by ygt_yprs_trans, cprs_yprs, sstas_yprs/ +] -L0 -T0 -T1 -HT2 #H #HW12 destruct /3 width=4/ +qed-. + +fact dxprs_ltpr_cprs_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → + ∀U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 → + ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[g] U2 & L2 ⊢ U1 ➡* U2. +#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 * #W1 #HTW1 #HWU1 #L2 #HL12 #T2 #HT12 +elim (sstas_ltpr_cprs_aux … IH3 IH2 IH1 … H01 … HT12 … HTW1) // -L0 -T0 -T1 #W2 #HTW2 #HW12 +lapply (ltpr_cprs_conf … HL12 … HWU1) -L1 #HWU1 +lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H +elim (cpcs_inv_cprs … H) -H /3 width=3/ +qed-. + +fact ssta_dxprs_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → + ∀l,U1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ∀T2. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2 → + ∃∃U,U2. ⦃h, L1⦄ ⊢ U1 •*[g] U & ⦃h, L1⦄ ⊢ T2 •*[g] U2 & L1 ⊢ U ⬌* U2. +#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2 +elim (sstas_strip … HT1T … HTU1) #HU1T destruct [ -HT1T | -L0 -T0 -T1 ] +[ elim (ssta_ltpr_cprs_aux … IH2 IH1 … HTU1 L1 … HTT2) // -L0 -T0 -T /3 width=5/ +| @(ex3_2_intro …T2 HU1T) // /2 width=1/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ltpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ltpr.etc new file mode 100644 index 000000000..6a0be5953 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ltpr.etc @@ -0,0 +1,113 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/dxprs_dxprs.ma". +include "basic_2/dynamic/snv_cpcs.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* Properties on context-free parallel reduction for local environments *****) + +fact snv_ltpr_tpr_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → + ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_ltpr_tpr h g L1 T1. +#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L1 * * [||||*] +[ #k #HL0 #HT0 #H1 #L2 #_ #X #H2 destruct -IH4 -IH3 -IH2 -IH1 -L1 + >(tpr_inv_atom1 … H2) -X // +| #i #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2 + elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1 + >(tpr_inv_atom1 … H2) -X + elim (ltpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 + elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct + lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) -HLK1 #HLK1 + lapply (IH1 … HK12 … HV12) -IH1 -HV12 -HK12 // -HV1 [ /2 width=1/ ] -HLK1 /2 width=5/ +| #p #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2 -IH1 + elim (snv_inv_gref … H1) +| #a #I #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2 + elim (snv_inv_bind … H1) -H1 #HV1 #HT1 + elim (tpr_inv_bind1 … H2) -H2 * + [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct + lapply (tps_lsubr_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02 + lapply (IH1 … HL12 … HV12) // [ /2 width=1/ ] #HV2 + lapply (snv_ltpr_cpr_aux … HT1 (L2.ⓑ{I}V2) … T2 ?) -HT1 + [ /3 width=5 by cpr_intro, tps_tpss/ | /2 width=1/ | /3 width=1/ ] -IH1 -T0 /2 width=1/ + | #T2 #HT12 #HXT2 #H1 #H2 destruct + lapply (IH1 … HT1 (L2.ⓓV1) … HT12) -IH1 -HT1 -HT12 [1,2: /2 width=1/ ] -HL12 #HT2 + lapply (snv_inv_lift … HT2 L2 … HXT2) -T2 // /2 width=1/ + ] +| #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct + elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1 + elim (tpr_inv_appl1 … H2) -H2 * + [ #V2 #T2 #HV12 #HT12 #H destruct -IH4 + lapply (IH1 … HV1 … HL12 … HV12) [ /2 width=1/ ] #HV2 + lapply (IH1 … HT1 … HL12 … HT12) [ /2 width=1/ ] #HT2 + elim (IH3 … HVW1 … HL12 … HV12) -HVW1 -HV12 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12 + elim (dxprs_ltpr_cprs_aux … IH2 IH1 IH3 … HTU1 … HL12 T2) // [2: /3 width=1/ |3: /2 width=1/ ] -IH2 -IH1 -IH3 -HT1 -HT12 -HTU1 #X #HTU2 #H + elim (cprs_inv_abst1 Abst W1 … H) -H #W20 #U2 #HW120 #_ #H destruct + lapply (ltpr_cprs_conf … HL12 … HW10) -L1 #HW10 + lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120 + lapply (cpcs_canc_sn … HW12 HW120) -W10 #HW20 + elim (cpcs_inv_cprs … HW20) -HW20 #W0 #HW20 #HW200 + lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?) [ /2 width=1/ ] -HW200 -HTU2 /2 width=8/ + | #b #V2 #W20 #T20 #T2 #HV12 #HT202 #H1 #H2 destruct + elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20 + elim (dxprs_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30 + lapply (cprs_div … HW10 … HW230) -W30 #HW120 + elim (snv_fwd_ssta … HW20) #l0 #U20 #HWU20 + elim (ssta_fwd_correct … HVW1) [g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → + ∀L1,T1. L0 = L1 → T0 = T1 → IH_ssta_ltpr_tpr h g L1 T1. +#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [|||| *] +[ #k #_ #_ #_ #X2 #l #H2 #L2 #HL12 #X3 #H3 -IH3 -IH2 -IH1 + elim (ssta_inv_sort1 … H2) -H2 #Hkl #H destruct + >(tpr_inv_atom1 … H3) -X3 /4 width=6/ +| #i #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct -IH3 -IH2 + elim (snv_inv_lref … H1) -H1 #I0 #K0 #V0 #H #HV1 + elim (ssta_inv_lref1 … H2) -H2 * #K1 + >(tpr_inv_atom1 … H3) -X3 + [ #V1 #W1 #HLK1 #HVW1 #HWU1 + lapply (ldrop_mono … H … HLK1) -H #H destruct + lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 + elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 + elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct + elim (IH1 … HVW1 … HK12 … HV12) -IH1 -HVW1 -HV12 // [2: /2 width=1/ ] -V1 #W2 #HVW2 #HW12 + lapply (ldrop_fwd_ldrop2 … HLK2) #H2 + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (cpcs_lift … H2 … HWU1 … HWU2 HW12) -H2 -W1 /3 width=6/ + | #V1 #W1 #l0 #HLK1 #HVW1 #HVU1 #H destruct + lapply (ldrop_mono … H … HLK1) -H #H destruct + lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 + elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 #X #H #HLK2 + elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct + elim (IH1 … HVW1 … HK12 … HV12) -IH1 -HVW1 -HK12 // [2: /2 width=1/ ] -HV1 -HKV1 #W2 #HVW2 #_ -W1 + elim (lift_total V2 0 (i+1)) #U2 #HVU2 + lapply (tpr_lift … HV12 … HVU1 … HVU2) -V1 /4 width=6/ + ] +| #p #_ #HT0 #H1 destruct -IH3 -IH2 -IH1 + elim (snv_inv_gref … H1) +| #a #I #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct -IH3 -IH2 + elim (snv_inv_bind … H1) -H1 #_ #HT1 + elim (ssta_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct + elim (tpr_inv_bind1 … H3) -H3 * + [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct + lapply (tps_lsubr_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 [ /2 width=1/ ] #HT02 + elim (ssta_ltpr_cpr_aux … HT1 … HTU1 (L2.ⓑ{I}V2) … T2) -HT1 -HTU1 + [2: /3 width=5 by cpr_intro, tps_tpss/ |3: /2 width=1/ |4: /3 width=1/ ] -IH1 -T0 -HL12 #U2 #HTU2 #HU12 + lapply (cpcs_bind2 … V1 … HU12 … a) -HU12 [ /2 width=1/ ] -HV12 /3 width=3/ + | #T2 #HT12 #HT2 #H1 #H2 destruct + elim (IH1 … HTU1 (L2.ⓓV1) … T2) -IH1 -HTU1 // [2,3: /2 width=1/ ] -T1 -HL12 #U2 #HTU2 #HU12 + lapply (cpcs_bind1 … HU12 … V1 … true) // -HU12 #HU12 + elim (ssta_inv_lift1 … HTU2 … HT2) -T2 [3: /2 width=1/ |2: skip ] #U #HXU #HU2 + lapply (cpcs_cpr_strap1 … HU12 U ?) -HU12 [ /3 width=3/ ] -U2 /2 width=3/ + ] +| #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct + elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #HVW1 #HW10 #HTU10 + elim (ssta_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct + elim (tpr_inv_appl1 … H3) -H3 * + [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH3 -IH2 + elim (IH1 … HTU1 … HL12 … HT12) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -T1 #U2 #HTU2 #HU12 + lapply (cpcs_flat … V1 V2 … HU12) -HU12 [ /2 width=1/ ] -HV12 /3 width=3/ + | #b #V2 #W #T2 #T20 #HV12 #HT20 #H1 #H2 destruct + elim (snv_inv_bind … HT1) -HT1 #HW #HT2 + elim (ssta_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct + elim (dxprs_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW0 #_ #H destruct + lapply (cprs_div … HW10 … HW0) -W0 #HW1W + elim (ssta_fwd_correct … HVW1)