From: Ferruccio Guidi Date: Tue, 14 Feb 2012 20:07:50 +0000 (+0000) Subject: - more properties on strongly normalizing terms X-Git-Tag: make_still_working~1951 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fcd30dfead2fbc2889aa993fba0577dce8a90c88;p=helm.git - more properties on strongly normalizing terms - bugfix in Basic_1 annotations --- diff --git a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt index 0570c48b3..f7e55be63 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt +++ b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt @@ -290,7 +290,6 @@ sn3/props sn3_shift sn3/props sn3_change sn3/props sn3_gen_def sn3/props sn3_cdelta -sn3/props sn3_beta sn3/props sn3_appl_lref sn3/props sn3_appl_abbr sn3/props sn3_appl_cast @@ -302,7 +301,6 @@ sn3/props sn3_appls_lref sn3/props sn3_appls_cast sn3/props sn3_appls_bind sn3/props sn3_appls_beta -sn3/props sn3_abbr sn3/props sn3_appls_abbr sn3/props sns3_lifts diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma index 20bf4ebe5..e19800104 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma @@ -36,3 +36,9 @@ lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 → #L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 // #T #T2 #_ #HT2 #IHT2 /3 width=5/ qed. + +lemma cpr_abbr: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡ T2 → + L ⊢ ⓓV1. T1 ➡* ⓓV2. T2. +#L #V1 #V2 #HV12 #T1 #T2 #HT12 +@(cprs_strap2 … (ⓓV1.T2)) /2 width=1/ /3 width=1/ +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma index b41060472..f5d8b7390 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma @@ -72,19 +72,14 @@ qed. (* Basic forward lemmas *****************************************************) -fact csn_fwd_flat2_aux: ∀L,U. L ⊢ ⬇* U → ∀I,V,T. U = ⓕ{I} V. T → L ⊢ ⬇* T. +fact csn_fwd_flat_dx_aux: ∀L,U. L ⊢ ⬇* U → ∀I,V,T. U = ⓕ{I} V. T → L ⊢ ⬇* T. #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct @csn_intro #T2 #HLT2 #HT2 @(IH (ⓕ{I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/ qed. (* Basic_1: was: sn3_gen_flat *) -lemma csn_fwd_flat2: ∀I,L,V,T. L ⊢ ⬇* ⓕ{I} V. T → L ⊢ ⬇* T. +lemma csn_fwd_flat_dx: ∀I,L,V,T. L ⊢ ⬇* ⓕ{I} V. T → L ⊢ ⬇* T. /2 width=5/ qed-. -(* -sn3/fwd sn3_gen_bind -sn3/fwd sn3_gen_head -*) - (* Basic_1: removed theorems 3: sn3_gen_cflat sn3_cflat sn3_bind *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cpr.ma new file mode 100644 index 000000000..11647e9dc --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cpr.ma @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/cpr_cpr.ma". +include "Basic_2/computation/csn.ma". + +(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) + +(* Advanced forvard lemmas **************************************************) + +fact csn_fwd_pair_sn_aux: ∀L,U. L ⊢ ⬇* U → ∀I,V,T. U = ②{I} V. T → L ⊢ ⬇* V. +#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct +@csn_intro #V2 #HLV2 #HV2 +@(IH (②{I} V2. T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/ +qed. + +(* Basic_1: was: sn3_gen_head *) +lemma csn_fwd_pair_sn: ∀I,L,V,T. L ⊢ ⬇* ②{I} V. T → L ⊢ ⬇* V. +/2 width=5/ qed. + +fact csn_fwd_bind_dx_aux: ∀L,U. L ⊢ ⬇* U → + ∀I,V,T. U = ⓑ{I} V. T → L. ⓑ{I} V ⊢ ⬇* T. +#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct +@csn_intro #T2 #HLT2 #HT2 +@(IH (ⓑ{I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/ +qed. + +(* Basic_1: was: sn3_gen_bind *) +lemma csn_fwd_bind_dx: ∀I,L,V,T. L ⊢ ⬇* ⓑ{I} V. T → L. ⓑ{I} V ⊢ ⬇* T. +/2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cprs.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cprs.ma index ace3b9fea..4a936f607 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cprs.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cprs.ma @@ -25,10 +25,6 @@ interpretation "context-sensitive strong normalization (term)" 'SNStar L T = (csns L T). -notation "hvbox( L ⊢ ⬇ * * T )" - non associative with precedence 45 - for @{ 'SNStar $L $T }. - (* Basic eliminators ********************************************************) lemma csns_ind: ∀L. ∀R:predicate term. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma index 88c492779..8121a0ac1 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma @@ -13,22 +13,23 @@ (**************************************************************************) include "Basic_2/reducibility/lcpr_cpr.ma". -include "Basic_2/computation/cprs_lcpr.ma". -include "Basic_2/computation/csn_cprs.ma". +include "Basic_2/computation/cprs_cprs.ma". include "Basic_2/computation/csn_lift.ma". +include "Basic_2/computation/csn_cpr.ma". +include "Basic_2/computation/csn_cprs.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) (* Advanced properties ******************************************************) -lemma csn_lcpr_trans: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬇* T → L2 ⊢ ⬇* T. +lemma csn_lcpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬇* T → L2 ⊢ ⬇* T. #L1 #L2 #HL12 #T #H @(csn_ind_cprs … H) -T #T #_ #IHT @csn_intro #T0 #HLT0 #HT0 @IHT /2 width=2/ -IHT -HT0 /2 width=3/ qed. lemma csn_abbr: ∀L,V. L ⊢ ⬇* V → ∀T. L. ⓓV ⊢ ⬇* T → L ⊢ ⬇* ⓓV. T. -#L #V #HV @(csn_ind … HV) -V #V #_ #IHV #T #HT @(csn_ind_cprs … HT) -T #T #HT #IHT +#L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_cprs … HT) -T #T #HT #IHT @csn_intro #X #H1 #H2 elim (cpr_inv_abbr1 … H1) -H1 * [ #V0 #V1 #T1 #HLV0 #HLV01 #HLT1 #H destruct @@ -36,10 +37,39 @@ elim (cpr_inv_abbr1 … H1) -H1 * lapply (ltpr_cpr_trans (L. ⓓV) … HLT1) /2 width=1/ -V0 #HLT1 elim (eq_false_inv_tpair … H2) -H2 [ #HV1 @IHV // /2 width=1/ -HV1 - @(csn_lcpr_trans (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/ + @(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/ | -IHV -HLV1 * #H destruct /3 width=1/ ] | -IHV -IHT -H2 #T0 #HT0 #HLT0 lapply (csn_inv_lift … HT … HT0) -HT /2 width=3/ ] qed. + +fact csn_appl_beta_aux: ∀L,W. L ⊢ ⬇* W → ∀U. L ⊢ ⬇* U → + ∀V,T. U = ⓓV. T → L ⊢ ⬇* ⓐV. ⓛW. T. +#L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_cprs … H) -X #X #HVT #IHVT #V #T #H destruct +lapply (csn_fwd_pair_sn … HVT) #HV +lapply (csn_fwd_bind_dx … HVT) #HT -HVT +@csn_intro #X #H #H2 +elim (cpr_inv_appl1 … H) -H * +[ #V0 #Y #HLV0 #H #H0 destruct + elim (cpr_inv_abst1 … H Abbr V) -H #W0 #T0 #HLW0 #HLT0 #H destruct + elim (eq_false_inv_beta … H2) -H2 + [ -IHVT #HW0 @IHW -IHW [1,5: // |3: skip ] -HLW0 /2 width=1/ -HW0 + @csn_abbr /2 width=3/ -HV + @(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/ + | -IHW -HLW0 -HV -HT * #H #HVT0 destruct + @(IHVT … HVT0) -IHVT -HVT0 // /2 width=1/ + ] +| -IHW -IHVT -H2 #V0 #W0 #T0 #T1 #HLV0 #HLT01 #H1 #H2 destruct + lapply (lcpr_cpr_trans (L. ⓓV) … HLT01) -HLT01 /2 width=1/ #HLT01 + @csn_abbr /2 width=3/ -HV + @(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/ +| -IHW -IHVT -HV -HT -H2 #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #_ #H destruct +] +qed. + +(* Basic_1: was: sn3_beta *) +lemma csn_appl_beta: ∀L,W. L ⊢ ⬇* W → ∀V,T. L ⊢ ⬇* (ⓓV. T) → (**) + L ⊢ ⬇* ⓐV. ⓛW. T. +/2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma index 605e78db1..29872f929 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma @@ -18,28 +18,6 @@ include "Basic_2/computation/csn.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) -(* Advanced properties ******************************************************) - -lemma csn_acp: acp cpr (eq …) (csn …). -@mk_acp -[ /2 width=1/ -| /2 width=3/ -| /2 width=5/ -| @cnf_lift -] -qed. - -lemma csn_abst: ∀L,W. L ⊢ ⬇* W → ∀I,V,T. L. ⓑ{I} V ⊢ ⬇* T → L ⊢ ⬇* ⓛW. T. -#L #W #HW elim HW -W #W #_ #IHW #I #V #T #HT @(csn_ind … HT) -T #T #HT #IHT -@csn_intro #X #H1 #H2 -elim (cpr_inv_abst1 … H1 I V) -H1 -#W0 #T0 #HLW0 #HLT0 #H destruct -elim (eq_false_inv_tpair … H2) -H2 -[ /3 width=5/ -| -HLW0 * #H destruct /3 width=1/ -] -qed. - (* Relocation properties ****************************************************) (* Basic_1: was: sn3_lift *) @@ -62,3 +40,40 @@ lapply (cpr_lift … HL12 … HT21 … HT0 HLT2) -HLT2 #HLT10 @(IHT1 … HLT10) // -L1 -L2 #H destruct >(lift_inj … HT0 … HT21) in HT2; -T0 /2 width=1/ qed. + +(* Advanced properties ******************************************************) + +lemma csn_acp: acp cpr (eq …) (csn …). +@mk_acp +[ /2 width=1/ +| /2 width=3/ +| /2 width=5/ +| @cnf_lift +] +qed. + +(* Basic_1: was: sn3_abbr *) +lemma csn_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → K ⊢ ⬇* V → L ⊢ ⬇* #i. +#L #K #V #i #HLK #HV +@csn_intro #X #H #Hi +elim (cpr_inv_lref1 … H) -H +[ #H destruct elim (Hi ?) // +| -Hi * #K0 #V0 #V1 #HLK0 #HV01 #HV1 #_ + lapply (ldrop_mono … HLK0 … HLK) -HLK #H destruct + lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #HLK + @(csn_lift … HLK HV1) -HLK -HV1 + @(csn_cpr_trans … HV) -HV + @(cpr_intro … HV01) -HV01 // +] +qed. + +lemma csn_abst: ∀L,W. L ⊢ ⬇* W → ∀I,V,T. L. ⓑ{I} V ⊢ ⬇* T → L ⊢ ⬇* ⓛW. T. +#L #W #HW elim HW -W #W #_ #IHW #I #V #T #HT @(csn_ind … HT) -T #T #HT #IHT +@csn_intro #X #H1 #H2 +elim (cpr_inv_abst1 … H1 I V) -H1 +#W0 #T0 #HLW0 #HLT0 #H destruct +elim (eq_false_inv_tpair … H2) -H2 +[ /3 width=5/ +| -HLW0 * #H destruct /3 width=1/ +] +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma index 7a5a9d91d..32f8272dc 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma @@ -89,6 +89,21 @@ elim (term_eq_dec V1 V2) /3 width=1/ #HV12 destruct @or_intror @conj // #HT12 destruct /2 width=1/ qed-. +lemma eq_false_inv_beta: ∀V1,V2,W1,W2,T1,T2. + (ⓐV1. ⓛW1. T1 = ⓐV2. ⓛW2 .T2 →False) → + (W1 = W2 → False) ∨ + (W1 = W2 ∧ (ⓓV1. T1 = ⓓV2. T2 → False)). +#V1 #V2 #W1 #W2 #T1 #T2 #H +elim (eq_false_inv_tpair … H) -H +[ #HV12 elim (term_eq_dec W1 W2) /3 width=1/ + #H destruct @or_intror @conj // #H destruct /2 width=1/ +| * #H1 #H2 destruct + elim (eq_false_inv_tpair … H2) -H2 /3 width=1/ + * #H #HT12 destruct + @or_intror @conj // #H destruct /2 width=1/ +] +qed. + (* Basic_1: removed theorems 3: not_void_abst not_abbr_void not_abst_void *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index 9f2d54df0..08ff46477 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -278,6 +278,10 @@ notation "hvbox( L ⊢ ⬇ * T )" non associative with precedence 45 for @{ 'SN $L $T }. +notation "hvbox( L ⊢ ⬇ * * T )" + non associative with precedence 45 + for @{ 'SNStar $L $T }. + notation "hvbox( ⦃ L, break T ⦄ break [ R ] ϵ break 〚 A 〛 )" non associative with precedence 45 for @{ 'InEInt $R $L $T $A }. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma index fca70da65..0ad09e4b4 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma @@ -107,8 +107,8 @@ elim (tpr_inv_cast1 … H) -H /3 width=3/ elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/ qed-. -(* Basic_1: removed theorems 5: - pr2_head_1 pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans +(* Basic_1: removed theorems 4: + pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans Basic_1: removed local theorems 3: pr2_free_free pr2_free_delta pr2_delta_delta *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma index 555344994..236b953d8 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma @@ -21,7 +21,7 @@ include "Basic_2/reducibility/cpr.ma". lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ➡ V2 → T1 ➡ T2 → L ⊢ ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2. -#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12 +#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12 @ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2 width=3/ (* /3 width=5/ is too slow *) qed. @@ -35,6 +35,13 @@ lapply (tpss_tps … HT0) -HT0 #HT0 @ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *) qed. + +(* Basic_1: was only: pr2_head_1 *) +lemma cpr_pair_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ➡ V2 → T1 ➡ T2 → + L ⊢ ②{I} V1. T1 ➡ ②{I} V2. T2. +* /2 width=1/ /3 width=1/ +qed. + (* Advanced forward lemmas **************************************************) lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L @ T1 ➡ L @ T2. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma index ae26fa75d..fcf4de993 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma @@ -17,7 +17,7 @@ include "Basic_2/reducibility/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) -(* Unfold properties ********************************************************) +(* Properties concerning parallel unfold on terms ***************************) (* Note: we could invoke tpss_weak_all instead of ltpr_fwd_length *) (* Basic_1: was only: pr2_subst1 *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma index 5c725a948..090e8cfbf 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma @@ -17,7 +17,7 @@ include "Basic_2/reducibility/ltpr.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) -(* Basic_1: was: wcpr0_ldrop *) +(* Basic_1: was: wcpr0_drop *) lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀L2. L1 ➡ L2 → ∃∃K2. ⇩[d, e] L2 ≡ K2 & K1 ➡ K2. #L1 #K1 #d #e #H elim H -L1 -K1 -d -e @@ -34,7 +34,7 @@ lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀L2. L1 ➡ L2 ] qed. -(* Basic_1: was: wcpr0_ldrop_back *) +(* Basic_1: was: wcpr0_drop_back *) lemma ldrop_ltpr_trans: ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. K1 ➡ K2 → ∃∃L2. ⇩[d, e] L2 ≡ K2 & L1 ➡ L2. #L1 #K1 #d #e #H elim H -L1 -K1 -d -e diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_tps.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_tps.ma index 32ddb3a1f..91b30b014 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_tps.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_tps.ma @@ -35,3 +35,21 @@ lemma ltpr_tps_trans: ∀L2,T1,T2,d,e. L2 ⊢ T1 [d, e] ▶ T2 → ∀L1. L1 ➡ elim (IHT12 … HL12) -L2 /3 width=5/ ] qed. + +lemma ltpr_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶ T2 → ∀L2. L1 ➡ L2 → + ∃∃T. L2 ⊢ T1 [d, e] ▶ T & T2 ➡ T. +#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e +[ /2 width=3/ +| #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L2 #HL12 + elim (ltpr_ldrop_conf … HLK1 … HL12) -L1 #X #HLK2 #H + elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct -K1 + elim (lift_total V2 0 (i+1)) #W2 #HVW2 + lapply (tpr_lift … HV12 … HVW1 … HVW2) -V1 /3 width=4/ +| #L1 #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L2 #HL12 + elim (IHV12 … HL12) -IHV12 #V #HV1 #HV2 + elim (IHT12 (L2.ⓑ{I}V) ?) /2 width=1/ -L1 /3 width=5/ +| #L1 #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L2 #HL12 + elim (IHV12 … HL12) -IHV12 + elim (IHT12 … HL12) -L1 /3 width=5/ +] +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma index c7fc055e7..c00819a74 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma @@ -18,7 +18,7 @@ include "Basic_2/substitution/lift.ma". (* LOCAL ENVIRONMENT SLICING ************************************************) -(* Basic_1: includes: ldrop_skip_bind *) +(* Basic_1: includes: drop_skip_bind *) inductive ldrop: nat → nat → relation lenv ≝ | ldrop_atom : ∀d,e. ldrop d e (⋆) (⋆) | ldrop_pair : ∀L,I,V. ldrop 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V) @@ -41,7 +41,7 @@ fact ldrop_inv_refl_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → d = 0 → e = 0 ] qed. -(* Basic_1: was: ldrop_gen_refl *) +(* Basic_1: was: drop_gen_refl *) lemma ldrop_inv_refl: ∀L1,L2. ⇩[0, 0] L1 ≡ L2 → L1 = L2. /2 width=5/ qed-. @@ -55,7 +55,7 @@ fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → L1 = ⋆ → ] qed. -(* Basic_1: was: ldrop_gen_sort *) +(* Basic_1: was: drop_gen_sort *) lemma ldrop_inv_atom1: ∀d,e,L2. ⇩[d, e] ⋆ ≡ L2 → L2 = ⋆. /2 width=5/ qed-. @@ -76,7 +76,7 @@ lemma ldrop_inv_O1: ∀e,K,I,V,L2. ⇩[0, e] K. ⓑ{I} V ≡ L2 → (0 < e ∧ ⇩[0, e - 1] K ≡ L2). /2 width=3/ qed-. -(* Basic_1: was: ldrop_gen_ldrop *) +(* Basic_1: was: drop_gen_drop *) lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2. ⇩[0, e] K. ⓑ{I} V ≡ L2 → 0 < e → ⇩[0, e - 1] K ≡ L2. #e #K #I #V #L2 #H #He @@ -97,7 +97,7 @@ fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d → ] qed. -(* Basic_1: was: ldrop_gen_skip_l *) +(* Basic_1: was: drop_gen_skip_l *) lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ⇩[d, e] K1. ⓑ{I} V1 ≡ L2 → 0 < d → ∃∃K2,V2. ⇩[d - 1, e] K1 ≡ K2 & ⇧[d - 1, e] V2 ≡ V1 & @@ -117,7 +117,7 @@ fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d → ] qed. -(* Basic_1: was: ldrop_gen_skip_r *) +(* Basic_1: was: drop_gen_skip_r *) lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ⇩[d, e] L1 ≡ K2. ⓑ{I} V2 → 0 < d → ∃∃K1,V1. ⇩[d - 1, e] K1 ≡ K2 & ⇧[d - 1, e] V2 ≡ V1 & L1 = K1. ⓑ{I} V1. @@ -125,7 +125,7 @@ lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ⇩[d, e] L1 ≡ K2. ⓑ{I} V2 → 0 < (* Basic properties *********************************************************) -(* Basic_1: was by definition: ldrop_refl *) +(* Basic_1: was by definition: drop_refl *) lemma ldrop_refl: ∀L. ⇩[0, 0] L ≡ L. #L elim L -L // qed. @@ -166,7 +166,7 @@ qed. (* Basic forvard lemmas *****************************************************) -(* Basic_1: was: ldrop_S *) +(* Basic_1: was: drop_S *) lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇩[O, e] L1 ≡ K2. ⓑ{I2} V2 → ⇩[O, e + 1] L1 ≡ K2. #L1 elim L1 -L1 @@ -212,16 +212,16 @@ lemma ldrop_fwd_O1_length: ∀L1,L2,e. ⇩[0, e] L1 ≡ L2 → |L2| = |L1| - e. qed-. (* Basic_1: removed theorems 49: - ldrop_skip_flat + drop_skip_flat cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf - ldrop_clear ldrop_clear_O ldrop_clear_S + drop_clear drop_clear_O drop_clear_S clear_gen_sort clear_gen_bind clear_gen_flat clear_gen_flat_r clear_gen_all clear_clear clear_mono clear_trans clear_ctail clear_cle getl_ctail_clen getl_gen_tail clear_getl_trans getl_clear_trans - getl_clear_bind getl_clear_conf getl_dec getl_ldrop getl_ldrop_conf_lt - getl_ldrop_conf_ge getl_conf_ge_ldrop getl_ldrop_conf_rev - ldrop_getl_trans_lt ldrop_getl_trans_le ldrop_getl_trans_ge - getl_ldrop_trans getl_flt getl_gen_all getl_gen_sort getl_gen_O + getl_clear_bind getl_clear_conf getl_dec getl_drop getl_drop_conf_lt + getl_drop_conf_ge getl_conf_ge_drop getl_drop_conf_rev + drop_getl_trans_lt drop_getl_trans_le drop_getl_trans_ge + getl_drop_trans getl_flt getl_gen_all getl_gen_sort getl_gen_O getl_gen_S getl_gen_2 getl_gen_flat getl_gen_bind getl_conf_le getl_trans getl_refl getl_head getl_flat getl_ctail getl_mono *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma index 91c0c6b70..90f724ad3 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma @@ -19,7 +19,7 @@ include "Basic_2/substitution/ldrop.ma". (* Main properties **********************************************************) -(* Basic_1: was: ldrop_mono *) +(* Basic_1: was: drop_mono *) theorem ldrop_mono: ∀d,e,L,L1. ⇩[d, e] L ≡ L1 → ∀L2. ⇩[d, e] L ≡ L2 → L1 = L2. #d #e #L #L1 #H elim H -d -e -L -L1 @@ -36,7 +36,7 @@ theorem ldrop_mono: ∀d,e,L,L1. ⇩[d, e] L ≡ L1 → ] qed-. -(* Basic_1: was: ldrop_conf_ge *) +(* Basic_1: was: drop_conf_ge *) theorem ldrop_conf_ge: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 → ∀e2,L2. ⇩[0, e2] L ≡ L2 → d1 + e1 ≤ e2 → ⇩[0, e2 - e1] L1 ≡ L2. @@ -55,7 +55,7 @@ theorem ldrop_conf_ge: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 → ] qed. -(* Basic_1: was: ldrop_conf_lt *) +(* Basic_1: was: drop_conf_lt *) theorem ldrop_conf_lt: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 → ∀e2,K2,I,V2. ⇩[0, e2] L ≡ K2. ⓑ{I} V2 → e2 < d1 → let d ≝ d1 - e2 - 1 in @@ -77,7 +77,7 @@ theorem ldrop_conf_lt: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 → ] qed. -(* Basic_1: was: ldrop_trans_le *) +(* Basic_1: was: drop_trans_le *) theorem ldrop_trans_le: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L → ∀e2,L2. ⇩[0, e2] L ≡ L2 → e2 ≤ d1 → ∃∃L0. ⇩[0, e2] L1 ≡ L0 & ⇩[d1 - e2, e1] L0 ≡ L2. @@ -99,7 +99,7 @@ theorem ldrop_trans_le: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L → ] qed. -(* Basic_1: was: ldrop_trans_ge *) +(* Basic_1: was: drop_trans_ge *) theorem ldrop_trans_ge: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L → ∀e2,L2. ⇩[0, e2] L ≡ L2 → d1 ≤ e2 → ⇩[0, e1 + e2] L1 ≡ L2. #d1 #e1 #L1 #L #H elim H -d1 -e1 -L1 -L @@ -121,6 +121,6 @@ theorem ldrop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L. #e1 #e1 #e2 >commutative_plus /2 width=5/ qed. -(* Basic_1: was: ldrop_conf_rev *) +(* Basic_1: was: drop_conf_rev *) axiom ldrop_div: ∀e1,L1,L. ⇩[0, e1] L1 ≡ L → ∀e2,L2. ⇩[0, e2] L2 ≡ L → ∃∃L0. ⇩[0, e1] L0 ≡ L2 & ⇩[e1, e2] L0 ≡ L1. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma index c4b6c87f0..4f30025d3 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma @@ -179,9 +179,9 @@ lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ▶ K2. ⓑ{I} V2 → 0 < d /2 width=3/ qed-. (* Basic_1: removed theorems 27: - csubst0_clear_O csubst0_ldrop_lt csubst0_ldrop_gt csubst0_ldrop_eq + csubst0_clear_O csubst0_drop_lt csubst0_drop_gt csubst0_drop_eq csubst0_clear_O_back csubst0_clear_S csubst0_clear_trans - csubst0_ldrop_gt_back csubst0_ldrop_eq_back csubst0_ldrop_lt_back + csubst0_drop_gt_back csubst0_drop_eq_back csubst0_drop_lt_back csubst0_gen_sort csubst0_gen_head csubst0_getl_ge csubst0_getl_lt csubst0_gen_S_bind_2 csubst0_getl_ge_back csubst0_getl_lt_back csubst0_snd_bind csubst0_fst_bind csubst0_both_bind