From 514f515ecb8765c68720e880460c2457898d74dc Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 28 Feb 2013 18:14:27 +0000 Subject: [PATCH] - lambdadelta: first recursive part of preservation finally proved! - lambda: bugfix in include paths, now they are relative to the root - matita.lang: keyword "fact" added (used in lambdadelta) --- .../lambdadelta/basic_2/computation/cprs.ma | 5 +- .../lambdadelta/basic_2/computation/fprs.ma | 3 + .../lambdadelta/basic_2/computation/lfprs.ma | 3 + .../lambdadelta/basic_2/computation/ltprs.ma | 3 + .../lambdadelta/basic_2/computation/tprs.ma | 3 + .../lambdadelta/basic_2/dynamic/snv_cpcs.ma | 123 ++++++++++++ .../lambdadelta/basic_2/dynamic/snv_cpr.ma | 113 ----------- .../basic_2/dynamic/snv_cpr_ssta.ma | 190 ------------------ .../lambdadelta/basic_2/dynamic/snv_dxprs.ma | 69 ------- .../lambdadelta/basic_2/dynamic/snv_ltpr.ma | 62 ++++++ .../basic_2/dynamic/snv_ltpr_ssta.ma | 121 +++++++++++ .../lambdadelta/basic_2/equivalence/cpcs.ma | 3 + .../lambdadelta/basic_2/equivalence/fpcs.ma | 3 + .../lambdadelta/basic_2/equivalence/lfpcs.ma | 5 +- .../basic_2/equivalence/lfpcs_lfpcs.ma | 4 +- .../lambdadelta/basic_2/unfold/ldrops.ma | 3 +- .../lambdadelta/basic_2/unfold/tpss.ma | 3 + .../matita/lib/lambda/background/preamble.ma | 6 +- .../paths/alternative_standard_order.ma | 2 +- .../lib/lambda/paths/decomposed_trace.ma | 2 +- .../lib/lambda/paths/dst_computation.ma | 4 +- .../paths/labeled_sequential_computation.ma | 6 +- .../paths/labeled_sequential_reduction.ma | 4 +- .../lambda/paths/labeled_st_computation.ma | 6 +- .../lib/lambda/paths/labeled_st_reduction.ma | 6 +- matita/matita/lib/lambda/paths/path.ma | 2 +- .../matita/lib/lambda/paths/standard_order.ma | 2 +- .../lib/lambda/paths/standard_precedence.ma | 2 +- .../matita/lib/lambda/paths/standard_trace.ma | 4 +- matita/matita/lib/lambda/paths/trace.ma | 2 +- matita/matita/lib/lambda/subterms/boolean.ma | 2 +- .../matita/lib/lambda/subterms/booleanized.ma | 2 +- matita/matita/lib/lambda/subterms/carrier.ma | 4 +- .../subterms/relocating_substitution.ma | 2 +- .../matita/lib/lambda/subterms/relocation.ma | 2 +- matita/matita/lib/lambda/subterms/subterms.ma | 2 +- .../terms/labeled_sequential_computation.ma | 2 +- .../matita/lib/lambda/terms/multiplicity.ma | 2 +- .../lib/lambda/terms/parallel_computation.ma | 2 +- .../lib/lambda/terms/parallel_reduction.ma | 4 +- .../lambda/terms/relocating_substitution.ma | 2 +- matita/matita/lib/lambda/terms/relocation.ma | 2 +- .../lambda/terms/sequential_computation.ma | 2 +- .../lib/lambda/terms/sequential_reduction.ma | 2 +- matita/matita/lib/lambda/terms/size.ma | 2 +- matita/matita/lib/lambda/terms/term.ma | 2 +- matita/matita/matita.lang | 3 +- 47 files changed, 382 insertions(+), 421 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpr.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpr_ssta.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_dxprs.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_ssta.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma index 40608cf5c..e20ce0559 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma @@ -17,7 +17,6 @@ include "basic_2/computation/tprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) -(* Basic_1: includes: pr3_pr2 *) definition cprs: lenv → relation term ≝ λL. TC … (cpr L). @@ -42,6 +41,10 @@ qed-. (* Basic properties *********************************************************) +(* Basic_1: was: pr3_pr2 *) +lemma cpr_cprs: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L ⊢ T1 ➡* T2. +/2 width=1/ qed. + (* Basic_1: was: pr3_refl *) lemma cprs_refl: ∀L,T. L ⊢ T ➡* T. /2 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs.ma index 61c720754..27ea45c33 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs.ma @@ -35,6 +35,9 @@ lemma fprs_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. R L2 T2 → (* Basic properties *********************************************************) +lemma fpr_fprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄. +/2 width=1/ qed. + lemma fprs_refl: bi_reflexive … fprs. /2 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs.ma index a193f3c0a..c27e7673b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs.ma @@ -40,6 +40,9 @@ qed-. (* Basic properties *********************************************************) +lemma lfpr_lfprs: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄. +/2 width=1/ qed. + lemma lfprs_refl: ∀L. ⦃L⦄ ➡* ⦃L⦄. /2 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma index 34ad45039..8e0c32e26 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma @@ -44,6 +44,9 @@ qed-. lemma ltprs_refl: reflexive … ltprs. /2 width=1/ qed. +lemma ltpr_ltprs: ∀L1,L2. L1 ➡ L2 → L1 ➡* L2. +/2 width=1/ qed. + lemma ltprs_strap1: ∀L1,L,L2. L1 ➡* L → L ➡ L2 → L1 ➡* L2. /2 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs.ma index b094e66c1..22f09eda0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs.ma @@ -43,6 +43,9 @@ qed-. lemma tprs_refl: reflexive … tprs. /2 width=1/ qed. +lemma tpr_tprs: ∀T1,T2. T1 ➡ T2 → T2 ➡* T2. +/2 width=1/ qed. + lemma tprs_strap1: ∀T1,T,T2. T1 ➡* T → T ➡ T2 → T1 ➡* T2. /2 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma new file mode 100644 index 000000000..b1430bd59 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma @@ -0,0 +1,123 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/ssta_ssta.ma". +include "basic_2/computation/ygt.ma". +include "basic_2/equivalence/fpcs_cpcs.ma". +include "basic_2/dynamic/snv_ltpss_dx.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* Inductive premises for the preservation results **************************) +(* +definition IH_ssta_cprs: ∀h:sh. sd h → relation2 lenv term ≝ + λh,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 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄. + +definition IH_snv_dxprs: ∀h:sh. sd h → relation2 lenv term ≝ + λh,g,L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] → + ∀L2. L1 ➡ L2 → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L2⦄ ⊩ T2 :[g]. + +fact ssta_cpcs_aux: ∀h,g,L,T1,T2. IH_ssta_cprs h g L T1 → IH_ssta_cprs h 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 #L #T1 #T2 #IH1 #IH2 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #H +elim (cpcs_inv_cprs … H) -H #T #H1 #H2 +elim (IH1 … HT1 … HTU1 … H1) -T1 // #W1 #H1 #HUW1 +elim (IH2 … HT2 … HTU2 … H2) -T2 // #W2 #H2 #HUW2 +elim (ssta_mono … H1 … H2) -T #H1 #H2 destruct +lapply (fpcs_canc_dx … HUW1 … HUW2) -W2 #HU12 +lapply (fpcs_inv_cpcs … HU12) -HU12 /2 width=1/ +qed-. +*) +definition IH_ssta_ltpr_tpr: ∀h:sh. sd h → relation2 lenv term ≝ + λh,g,L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] → + ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → + ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄. + +definition IH_snv_ltpr_tpr: ∀h:sh. sd h → relation2 lenv term ≝ + λh,g,L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] → + ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊩ T2 :[g]. + +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]. + +fact ssta_ltpr_cpr_aux: ∀h,g,L1,T1. IH_ssta_ltpr_tpr h 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 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄. +#h #g #L1 #T1 #IH #HT1 #U1 #l #HTU1 #L2 #HL12 #T2 * #T #HT1T #HTT2 +elim (IH … HTU1 … HL12 … HT1T) // -HL12 -T1 #U #HTU #HU1 +elim (ssta_tpss_conf … HTU … HTT2) -T #U2 #HTU2 #HU2 +lapply (fpcs_fpr_strap1 … HU1 L2 U2 ?) -HU1 /2 width=3/ /3 width=3/ +qed-. + +fact snv_ltpr_cpr_aux: ∀h,g,L1,T1. IH_snv_ltpr_tpr h g L1 T1 → + ⦃h, L1⦄ ⊩ T1 :[g] → + ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 → ⦃h, L2⦄ ⊩ T2 :[g]. +#h #g #L1 #T1 #IH #HT1 #L2 #HL12 #T2 * #T #HT1T #HTT2 +lapply (IH … HL12 … HT1T) -HL12 // -T1 #HT0 +lapply (snv_tpss_conf … HT0 … HTT2) -T // +qed-. + +fact snv_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⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → + ∀T2. L1 ⊢ T1 ➡* T2 → ⦃h, L1⦄ ⊩ T2 :[g]. +#h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #T2 #H +@(cprs_ind … H) -T2 // -HT1 +/4 width=6 by snv_ltpr_cpr_aux, ygt_cprs_trans/ +qed-. + +fact ssta_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 → ∀T2. L1 ⊢ T1 ➡* T2 → + ∃∃U2. ⦃h, L1⦄ ⊢ T2 •[g, l] U2 & L1 ⊢ U1 ⬌* U2. +#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #l #HTU1 #T2 #H +@(cprs_ind … H) -T2 [ /2 width=3/ ] +#T #T2 #HT1T #HTT2 * #U #HTU #HU1 +elim (ssta_ltpr_cpr_aux … HTU … HTT2) // +[2: /3 width=7 by snv_cprs_aux, ygt_cprs_trans/ +|3: /3 width=3 by ygt_cprs_trans/ +] -L0 -T0 -T1 -T #U2 #HTU2 #HU2 +lapply (fpcs_inv_cpcs … HU2) -HU2 #HU2 +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_ltpr_tpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr 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 +elim (cpcs_inv_cprs … H) -H #T #H1 #H2 +elim (ssta_cprs_aux … HLT01 HT1 … HTU1 … H1) -T1 /2 width=1/ #W1 #H1 #HUW1 +elim (ssta_cprs_aux … HLT02 HT2 … HTU2 … H2) -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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpr.ma deleted file mode 100644 index a4850ff61..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpr.ma +++ /dev/null @@ -1,113 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/snv_ltpss_sn.ma". -include "basic_2/dynamic/snv_cpr_ssta.ma". - -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) - -(* Properties on context-free parallel reduction for closures ***************) - -axiom snv_ltpr_tpr_aux: ∀h,g,n. ( - ∀L1,T1. ♯{L1, T1} < n → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → - ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄ - ) → ( - ∀L1,T1. ♯{L1, T1} < n → ⦃h, L1⦄ ⊩ T1 :[g] → - ∀L2. L1 ➡ L2 → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L2⦄ ⊩ T2 :[g] - ) → - ∀L1,T1. ♯{L1, T1} = n → ⦃h, L1⦄ ⊩ T1 :[g] → - ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊩ T2 :[g]. -(* -#h #g #n #IH2 #IH1 #L1 * * [||||*] -[ #k #Hn #H1 #L2 #_ #X #H2 destruct -IH2 -IH1 -L1 - >(tpr_inv_atom1 … H2) -X // -| #i #Hn #H1 #L2 #HL12 #X #H2 destruct -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 … HV1 … HK12 V2 ?) -IH1 -HV1 -HK12 // - [ @cprs_dxprs /3 width=1/ (**) (* auto: /4 width=1/ fails *) - ] -HV12 /2 width=5/ -| #p #Hn #H1 #L2 #HL12 #X #H2 destruct -IH2 - elim (snv_inv_gref … H1) -| #a #I #V1 #T1 #Hn #H1 #L2 #HL12 #X #H2 destruct -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_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02 - lapply (cpr_intro (L2.ⓑ{I}V2) … T2 0 1 HT10 ?) -HT10 /2 width=1/ -HT02 #HT12 - lapply (IH1 … HV1 … HL12 V2 ?) -HV1 // - [ @cprs_dxprs /3 width=1/ (**) (* auto: /4 width=1/ fails *) - ] #HV2 - lapply (IH1 … HT1 (L2.ⓑ{I}V2) … T2 ?) -IH1 -HT1 /3 width=1/ - | #T2 #HT12 #HXT2 #H1 #H2 destruct - lapply (IH1 … HT1 (L2.ⓓV1) … T2 ?) -IH1 -HT1 // /2 width=2/ - [ @cprs_dxprs /3 width=1/ (**) (* auto: /4 width=1/ fails *) - ] -HT12 -HL12 #HT2 - lapply (snv_inv_lift … HT2 L2 … HXT2) -T2 // /2 width=1/ - ] -| #V1 #T1 #Hn #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 - lapply (IH1 … HV1 … HL12 V2 ?) - [ @cprs_dxprs /3 width=1/ (**) (* auto: /4 width=1/ fails *) - | // - ] #HV2 - lapply (IH1 … HT1 … HL12 T2 ?) - [ @cprs_dxprs /3 width=1/ (**) (* auto: /4 width=1/ fails *) - | // - ] #HT2 - lapply (IH1 … HT1 … HTU1) -IH1 // #H - elim (snv_inv_bind … H) -H #HW1 #HU1 - elim (IH2 … HVW1 … HL12 … HV12 HV1) -IH2 -HVW1 -HV12 -HV1 // #W2 #HVW2 #HW12 - lapply (fpcs_canc_sn L1 L1 … W10 W1 … HW12) -HW12 /3 width=1/ -W10 #HW12 - @(snv_appl … HV2 HT2 HVW2) -*) - -fact snv_cpr_aux: ∀h,g,n. ( - ∀L1,T1. ♯{L1, T1} < n → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → - ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. L2 ⊢ T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄ - ) → ( - ∀L1,T1. ♯{L1, T1} < n → ⦃h, L1⦄ ⊩ T1 :[g] → - ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L2⦄ ⊩ T2 :[g] - ) → - ∀L1,T1. ♯{L1, T1} = n → ⦃h, L1⦄ ⊩ T1 :[g] → - ∀T2. L1 ⊢ T1 ➡ T2 → ⦃h, L1⦄ ⊩ T2 :[g]. -#h #g #n #IH2 #IH1 #L1 #T1 #Hn #HT1 #T2 * #T0 #HT10 #HT02 -lapply (snv_ltpr_tpr_aux … Hn HT1 … HT10) -Hn -HT1 -HT10 [ // | skip | /3 width=6/ | /3 width=5/ ] -n -T1 #HT0 -lapply (snv_tpss_conf … HT0 … HT02) -T0 // -qed-. - -fact snv_lfpr_aux: ∀h,g,n. ( - ∀L1,T1. ♯{L1, T1} < n → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → - ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. L2 ⊢ T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄ - ) → ( - ∀L1,T1. ♯{L1, T1} < n → ⦃h, L1⦄ ⊩ T1 :[g] → - ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L2⦄ ⊩ T2 :[g] - ) → - ∀L1,T1. ♯{L1, T1} = n → ⦃h, L1⦄ ⊩ T1 :[g] → - ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ⦃h, L2⦄ ⊩ T1 :[g]. -#h #g #n #IH2 #IH1 #L1 #T1 #Hn #HT1 #L2 * #L #HL1 #HL2 -lapply (snv_ltpr_tpr_aux … Hn HT1 … HL1 ??) -Hn -HT1 -HL1 [ // | skip | /3 width=6/ | /3 width=5/ ] -n -L1 #HT1 -lapply (snv_ltpss_sn_conf … HL2 … HT1) -L // -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpr_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpr_ssta.ma deleted file mode 100644 index 9aa991939..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpr_ssta.ma +++ /dev/null @@ -1,190 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/static/ssta_ltpss_sn.ma". -include "basic_2/computation/dxprs_lift.ma". -include "basic_2/equivalence/lsubse_ssta.ma". -include "basic_2/equivalence/fpcs_cpcs.ma". -include "basic_2/equivalence/lfpcs_fpcs.ma". -include "basic_2/dynamic/snv_ssta.ma". - -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) - -(* Properties on context-sensitive parallel reduction for terms *************) - -fact ssta_ltpr_tpr_aux: ∀h,g,n. ( - ∀L,T2. ♯{L,T2} < n → - ∀T1. L ⊢ T1 ⬌* 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 ⊢ U1 ⬌* U2 ∧ l1 = l2 - ) → ( - ∀L,T. ♯{L,T} < n → ⦃h, L⦄ ⊩ T :[g] → - ∀U,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U → ⦃h, L⦄ ⊩ U :[g] - ) → ( - ∀L1,T1. ♯{L1,T1} < n → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → - ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄ - ) → - ∀L1,T1. ♯{L1,T1} = n → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → - ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄. -#h #g #n #IH3 #IH2 #IH1 #L1 * * [|||| *] -[ #k #_ #Y #l #H1 #L2 #HL12 #X #H2 #_ -IH3 -IH2 -IH1 - elim (ssta_inv_sort1 … H1) -H1 #Hkl #H destruct - >(tpr_inv_atom1 … H2) -X /4 width=6/ -| #i #Hn #U1 #l #H1 #L2 #HL12 #X #H2 #H3 destruct -IH3 -IH2 - elim (ssta_inv_lref1 … H1) -H1 * #K1 - >(tpr_inv_atom1 … H2) -X - elim (snv_inv_lref … H3) -H3 #I0 #K0 #V0 #H #HV1 - [ #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) #X #H #HLK2 - elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - elim (IH1 … HVW1 K2 … HV12) -IH1 -HVW1 -HV12 // -HV1 -HKV1 #W2 #HVW2 #HW12 - lapply (ldrop_fwd_ldrop2 … HLK1) -V1 #H1 - lapply (ldrop_fwd_ldrop2 … HLK2) #H2 - elim (lift_total W2 0 (i+1)) #U2 #HWU2 - lapply (fpcs_lift … HW12 … H1 H2 … HWU1 … HWU2) -H1 -H2 -W1 [ /3 width=1/ ] /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 K2 … HV12) -IH1 -HVW1 // -HV1 -HK12 -HKV1 #W2 #HVW2 #_ -W1 - elim (lift_total V2 0 (i+1)) #U2 #HVU2 - lapply (tpr_lift … HV12 … HVU1 … HVU2) -V1 /4 width=6/ - ] -| #p #Hn #U1 #l #H1 -IH3 -IH1 - elim (ssta_inv_gref1 … H1) -| #a #I #V1 #T1 #Hn #Y #l #H1 #L2 #HL12 #X #H2 #H3 destruct -IH3 -IH2 - elim (ssta_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct - elim (snv_inv_bind … H3) -H3 #_ #HT1 - elim (tpr_inv_bind1 … H2) -H2 * - [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct - elim (IH1 … HTU1 (L2.ⓑ{I}V2) … HT10) -IH1 -HTU1 -HT10 // -T1 /3 width=1/ -HL12 #U0 #HTU0 #HU10 - lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 [ /2 width=1/ ] #HT02 - elim (ssta_tps_conf … HTU0 … HT02) -T0 #U2 #HTU2 #HU02 - lapply (cpr_intro … U0 … HU02) -HU02 // #HU02 - lapply (fpcs_fpr_strap1 … HU10 (L2.ⓑ{I}V2) U2 ?) [ /2 width=1/ ] -U0 #HU12 - lapply (fpcs_fwd_shift … HU12 a) -HU12 /3 width=3/ - | #T2 #HT12 #HT2 #H1 #H2 destruct - elim (IH1 … HTU1 (L2.ⓓV1) … HT12) -IH1 -HTU1 -HT12 // -T1 [2: /3 width=1/ ] -HL12 #U2 #HTU2 #HU12 - lapply (fpcs_fwd_shift … HU12 true) -HU12 #HU12 - elim (ssta_inv_lift1 … HTU2 … HT2) -T2 [3: /2 width=1/ |2: skip ] #U #HXU #HU2 - lapply (fpcs_fpr_strap1 … HU12 L2 U ?) -HU12 [ /3 width=3/ ] -U2 /2 width=3/ - ] -| #V1 #T1 #Hn #Y #l #H1 #L2 #HL12 #X #H2 #H3 destruct - elim (ssta_inv_appl1 … H1) -H1 #U1 #HTU1 #H destruct - elim (snv_inv_appl … H3) -H3 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #HVW1 #HW10 #HTU10 - elim (tpr_inv_appl1 … H2) -H2 * - [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH3 -IH2 - elim (IH1 … HTU1 … HL12 … HT12 HT1) -IH1 -HTU1 -HL12 -HT12 -HT1 // /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 #HW1 - elim (ssta_fwd_correct … HVW1) [g] ⦃L, T2⦄ → - ∀T1. L ⊢ T1 ⬌* 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 ⊢ U1 ⬌* U2 ∧ l1 = l2 - ) → ( - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → - ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L2⦄ ⊩ T2 :[g] - ) → ( - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → ⦃h, L1⦄ ⊩ T1 :[g] → - ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. L2 ⊢ T1 ➡* T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄ - ) → - ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 → L0 = L1 → T0 = T1 → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → ⦃h, L1⦄ ⊩ T1 :[g] → - ∃∃U2. ⦃h, L1⦄ ⊢ T2 •[g, l] U2 & L1 ⊢ U1 ⬌* U2. -#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #T2 #H -@(cprs_ind_dx … H) -T1 [ /2 width=3/ ] -#T1 #T #HT1T #HTT2 #IH #H1 #H2 #U1 #l #HTU1 #HT1 destruct -elim (term_eq_dec T1 T) #H destruct [ /2 width=1/ ] -IH -elim (ssta_cpr_aux … HTU1 … HT1T HT1) -HTU1 -[2: // |3: skip |4,5,6: /3 width=9 by inj, dxprs_strap2, fw_ygt/ ] -IH3 #U #HTU #HU1 -lapply (snv_cpr_aux … HT1 … HT1T) -HT1 -[ // | skip |3,4: /3 width=6 by inj, fw_ygt/ ] -IH2 #HT -elim (IH1 … HTU HT … HTT2) -IH1 -HTU -HT -HTT2 // [2: /3 width=1/ ] -T #U2 #HTU2 #HU2 -lapply (fpcs_inv_cpcs … HU2) -HU2 #HU2 -lapply (cpcs_trans … HU1 … HU2) -U /2 width=3/ -qed-. - -fact snv_cprs_aux: ∀h,g,L0,T0. ( - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → - ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. L2 ⊢ T1 ➡* T2 → ⦃h, L1⦄ ⊩ T1 :[g] → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄ - ) → ( - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → - ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L2⦄ ⊩ T2 :[g] - ) → - ∀L1,T1. L0 = L1 → T0 = T1 → ⦃h, L1⦄ ⊩ T1 :[g] → - ∀T2. L1 ⊢ T1 ➡* T2 → ⦃h, L1⦄ ⊩ T2 :[g]. -#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H1 #H2 #HT1 #T2 #H -@(cprs_ind … H) -T2 // -HT1 -#T #T2 #HT1T #HTT2 #HT destruct -lapply (snv_cpr_aux … HT … HTT2) -HT -HTT2 [1,5: // |2: skip ] -/4 width=6 by cprs_ygt_trans, inj, fw_ygt/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma new file mode 100644 index 000000000..4bcfa9889 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma @@ -0,0 +1,62 @@ +(**************************************************************************) +(* ___ *) +(* ||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/snv_ltpr_ssta.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_ssta_ltpr_tpr 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 #IH2 #IH1 #L1 * * [||||*] +[ #k #HL0 #HT0 #H1 #L2 #_ #X #H2 destruct -IH2 -IH1 -L1 + >(tpr_inv_atom1 … H2) -X // +| #i #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -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 -IH2 -IH1 + elim (snv_inv_gref … H1) +| #a #I #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -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_lsubs_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 + lapply (IH1 … HV1 … HL12 … HV12) [ /2 width=1/ ] #HV2 + lapply (IH1 … HT1 … HL12 … HT12) [ /2 width=1/ ] #HT2 + elim (IH2 … HVW1 … HL12 … HV12) -IH2 -HVW1 -HV12 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12 + lapply (fpcs_canc_sn L1 L1 … W10 W1 … HW12) -HW12 /3 width=1/ -W10 #HW12 + @(snv_appl … HV2 HT2 HVW2) +(* + lapply (IH1 … HT1 … HTU1) -IH1 // #H + elim (snv_inv_bind … H) -H #HW1 #HU1 + elim (IH2 … HVW1 … HL12 … HV12 HV1) -IH2 -HVW1 -HV12 -HV1 // #W2 #HVW2 #HW12 +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_ssta.ma new file mode 100644 index 000000000..cabeceb25 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_ssta.ma @@ -0,0 +1,121 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/ssta_ltpss_sn.ma". +include "basic_2/equivalence/lsubse_ssta.ma". +include "basic_2/equivalence/lfpcs_fpcs.ma". +include "basic_2/dynamic/snv_ssta.ma". +include "basic_2/dynamic/snv_cpcs.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* Properties on context-free parallel reduction for local environments *****) + +fact ssta_ltpr_tpr_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. 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) #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/ ] -HV1 -HKV1 #W2 #HVW2 #HW12 + lapply (ldrop_fwd_ldrop2 … HLK1) -V1 #H1 + lapply (ldrop_fwd_ldrop2 … HLK2) #H2 + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (fpcs_lift … HW12 … H1 H2 … HWU1 … HWU2) -H1 -H2 -W1 [ /3 width=1/ ] /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_lsubs_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 -HV12 #U2 #HTU2 #HU12 + lapply (fpcs_fwd_shift … HU12 a) -HU12 /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 (fpcs_fwd_shift … HU12 true) -HU12 #HU12 + elim (ssta_inv_lift1 … HTU2 … HT2) -T2 [3: /2 width=1/ |2: skip ] #U #HXU #HU2 + lapply (fpcs_fpr_strap1 … HU12 L2 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 /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) inductive coinductive let - lemma + fact + lemma remark axiom -- 2.39.2