From 708aa01d44c67343f0dac0353b52c7c2457069b3 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 25 May 2012 17:10:54 +0000 Subject: [PATCH] - substitution lemma for native type assignmenr proved! - notation change in the support for abstract c.r.'s - some minor additions --- .../basic_2/computation/acp_aaa.ma | 6 +- .../basic_2/computation/acp_cr.ma | 4 +- .../lambda_delta/basic_2/computation/lsubc.ma | 44 +++---- .../basic_2/computation/lsubc_ldrop.ma | 8 +- .../basic_2/computation/lsubc_ldrops.ma | 4 +- .../basic_2/computation/lsubc_lsuba.ma | 2 +- .../basic_2/dynamic/nta_delift.ma | 88 ------------- .../lambda_delta/basic_2/dynamic/nta_thin.ma | 118 ++++++++++++++++++ .../lambda_delta/basic_2/grammar/aarity.ma | 22 ++-- .../contribs/lambda_delta/basic_2/notation.ma | 8 +- .../basic_2/substitution/ldrop_sfr.ma | 65 +++++++--- .../basic_2/substitution/lift_lift.ma | 8 +- .../lambda_delta/basic_2/substitution/tps.ma | 23 ++++ .../basic_2/unfold/delift_delift.ma | 1 + .../basic_2/unfold/delift_lift.ma | 15 ++- .../lambda_delta/basic_2/unfold/tpss.ma | 10 +- 16 files changed, 270 insertions(+), 156 deletions(-) delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_delift.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma index e25f2975f..1b2536c8b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma @@ -26,8 +26,8 @@ include "basic_2/computation/lsubc_ldrops.ma". theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L0,des. ⇩*[des] L0 ≡ L1 → - ∀T0. ⇧*[des] T ≡ T0 → ∀L2. L2 [RP] ⊑ L0 → - ⦃L2, T0⦄ [RP] ϵ 〚A〛. + ∀T0. ⇧*[des] T ≡ T0 → ∀L2. L2 ⊑[RP] L0 → + ⦃L2, T0⦄ ϵ[RP] 〚A〛. #RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A [ #L #k #L0 #des #HL0 #X #H #L2 #HL20 >(lifts_inv_sort1 … H) -H @@ -90,7 +90,7 @@ qed. (* Basic_1: was: sc3_arity *) lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → - ∀L,T,A. L ⊢ T ⁝ A → ⦃L, T⦄ [RP] ϵ 〚A〛. + ∀L,T,A. L ⊢ T ⁝ A → ⦃L, T⦄ ϵ[RP] 〚A〛. /2 width=8/ qed. lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma index 222f00da8..dff92c950 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma @@ -158,9 +158,9 @@ qed. lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → ∀L,W,T,A,B. RP L W → ( ∀L0,V0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[des + 1] T ≡ T0 → - ⦃L0, V0⦄ [RP] ϵ 〚B〛 → ⦃L0. ⓓV0, T0⦄ [RP] ϵ 〚A〛 + ⦃L0, V0⦄ ϵ[RP] 〚B〛 → ⦃L0. ⓓV0, T0⦄ ϵ[RP] 〚A〛 ) → - ⦃L, ⓛW. T⦄ [RP] ϵ 〚②B. A〛. + ⦃L, ⓛW. T⦄ ϵ[RP] 〚②B. A〛. #RR #RS #RP #H1RP #H2RP #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HB #HL0 #H lapply (aacr_acr … H1RP H2RP A) #HCA lapply (aacr_acr … H1RP H2RP B) #HCB diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma index 7c2ef6050..31ac81bf5 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma @@ -20,7 +20,7 @@ include "basic_2/computation/acp_cr.ma". inductive lsubc (RP:lenv→predicate term): relation lenv ≝ | lsubc_atom: lsubc RP (⋆) (⋆) | lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1. ⓑ{I} V) (L2. ⓑ{I} V) -| lsubc_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ [RP] ϵ 〚A〛 → L2 ⊢ W ⁝ A → +| lsubc_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ ϵ[RP] 〚A〛 → L2 ⊢ W ⁝ A → lsubc RP L1 L2 → lsubc RP (L1. ⓓV) (L2. ⓛW) . @@ -30,7 +30,7 @@ interpretation (* Basic inversion lemmas ***************************************************) -fact lsubc_inv_atom1_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → L1 = ⋆ → L2 = ⋆. +fact lsubc_inv_atom1_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → L1 = ⋆ → L2 = ⋆. #RP #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct @@ -39,13 +39,13 @@ fact lsubc_inv_atom1_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → L1 = ⋆ → L2 = ⋆. qed. (* Basic_1: was: csubc_gen_sort_r *) -lemma lsubc_inv_atom1: ∀RP,L2. ⋆ [RP] ⊑ L2 → L2 = ⋆. +lemma lsubc_inv_atom1: ∀RP,L2. ⋆ ⊑[RP] L2 → L2 = ⋆. /2 width=4/ qed-. -fact lsubc_inv_pair1_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V → - (∃∃K2. K1 [RP] ⊑ K2 & L2 = K2. ⓑ{I} V) ∨ - ∃∃K2,W,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ⁝ A & - K1 [RP] ⊑ K2 & +fact lsubc_inv_pair1_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V → + (∃∃K2. K1 ⊑[RP] K2 & L2 = K2. ⓑ{I} V) ∨ + ∃∃K2,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A & + K1 ⊑[RP] K2 & L2 = K2. ⓛW & I = Abbr. #RP #L1 #L2 * -L1 -L2 [ #I #K1 #V #H destruct @@ -55,14 +55,14 @@ fact lsubc_inv_pair1_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀I,K1,V. L1 = K1. qed. (* Basic_1: was: csubc_gen_head_r *) -lemma lsubc_inv_pair1: ∀RP,I,K1,L2,V. K1. ⓑ{I} V [RP] ⊑ L2 → - (∃∃K2. K1 [RP] ⊑ K2 & L2 = K2. ⓑ{I} V) ∨ - ∃∃K2,W,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ⁝ A & - K1 [RP] ⊑ K2 & +lemma lsubc_inv_pair1: ∀RP,I,K1,L2,V. K1. ⓑ{I} V ⊑[RP] L2 → + (∃∃K2. K1 ⊑[RP] K2 & L2 = K2. ⓑ{I} V) ∨ + ∃∃K2,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A & + K1 ⊑[RP] K2 & L2 = K2. ⓛW & I = Abbr. /2 width=3/ qed-. -fact lsubc_inv_atom2_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → L2 = ⋆ → L1 = ⋆. +fact lsubc_inv_atom2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → L2 = ⋆ → L1 = ⋆. #RP #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct @@ -71,13 +71,13 @@ fact lsubc_inv_atom2_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → L2 = ⋆ → L1 = ⋆. qed. (* Basic_1: was: csubc_gen_sort_l *) -lemma lsubc_inv_atom2: ∀RP,L1. L1 [RP] ⊑ ⋆ → L1 = ⋆. +lemma lsubc_inv_atom2: ∀RP,L1. L1 ⊑[RP] ⋆ → L1 = ⋆. /2 width=4/ qed-. -fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W → - (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. ⓑ{I} W) ∨ - ∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ⁝ A & - K1 [RP] ⊑ K2 & +fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W → + (∃∃K1. K1 ⊑[RP] K2 & L1 = K1. ⓑ{I} W) ∨ + ∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A & + K1 ⊑[RP] K2 & L1 = K1. ⓓV & I = Abst. #RP #L1 #L2 * -L1 -L2 [ #I #K2 #W #H destruct @@ -87,17 +87,17 @@ fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀I,K2,W. L2 = K2. qed. (* Basic_1: was: csubc_gen_head_l *) -lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 [RP] ⊑ K2. ⓑ{I} W → - (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. ⓑ{I} W) ∨ - ∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ⁝ A & - K1 [RP] ⊑ K2 & +lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 ⊑[RP] K2. ⓑ{I} W → + (∃∃K1. K1 ⊑[RP] K2 & L1 = K1. ⓑ{I} W) ∨ + ∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A & + K1 ⊑[RP] K2 & L1 = K1. ⓓV & I = Abst. /2 width=3/ qed-. (* Basic properties *********************************************************) (* Basic_1: was: csubc_refl *) -lemma lsubc_refl: ∀RP,L. L [RP] ⊑ L. +lemma lsubc_refl: ∀RP,L. L ⊑[RP] L. #RP #L elim L -L // /2 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma index 7d23f9e03..e9f8062c8 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma @@ -22,8 +22,8 @@ include "basic_2/computation/lsubc.ma". (* Basic_1: was: csubc_drop_conf_O *) (* Note: the constant 0 can not be generalized *) -lemma lsubc_ldrop_O1_trans: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 → - ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 [RP] ⊑ K2. +lemma lsubc_ldrop_O1_trans: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 → + ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 ⊑[RP] K2. #RP #L1 #L2 #H elim H -L1 -L2 [ #X #e #H >(ldrop_inv_atom1 … H) -H /2 width=3/ @@ -42,8 +42,8 @@ qed-. (* Basic_1: was: csubc_drop_conf_rev *) lemma ldrop_lsubc_trans: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → - ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 → - ∃∃L2. L1 [RP] ⊑ L2 & ⇩[d, e] L2 ≡ K2. + ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. K1 ⊑[RP] K2 → + ∃∃L2. L1 ⊑[RP] L2 & ⇩[d, e] L2 ≡ K2. #RR #RS #RP #Hacp #Hacr #L1 #K1 #d #e #H elim H -L1 -K1 -d -e [ #d #e #X #H >(lsubc_inv_atom1 … H) -H /2 width=3/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrops.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrops.ma index a61272c73..4e26322a5 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrops.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrops.ma @@ -21,8 +21,8 @@ include "basic_2/computation/lsubc_ldrop.ma". (* Basic_1: was: csubc_drop1_conf_rev *) lemma ldrops_lsubc_trans: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → - ∀L1,K1,des. ⇩*[des] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 → - ∃∃L2. L1 [RP] ⊑ L2 & ⇩*[des] L2 ≡ K2. + ∀L1,K1,des. ⇩*[des] L1 ≡ K1 → ∀K2. K1 ⊑[RP] K2 → + ∃∃L2. L1 ⊑[RP] L2 & ⇩*[des] L2 ≡ K2. #RR #RS #RP #Hacp #Hacr #L1 #K1 #des #H elim H -L1 -K1 -des [ /2 width=3/ | #L1 #L #K1 #des #d #e #_ #HLK1 #IHL #K2 #HK12 diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_lsuba.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_lsuba.ma index e9dcbe5d2..aad454f62 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_lsuba.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_lsuba.ma @@ -20,7 +20,7 @@ include "basic_2/computation/acp_aaa.ma". (* properties concerning lenv refinement for atomic arity assignment ********) lemma lsubc_lsuba: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → - ∀L1,L2. L1 ⁝⊑ L2 → L1 [RP] ⊑ L2. + ∀L1,L2. L1 ⁝⊑ L2 → L1 ⊑[RP] L2. #RR #RS #RP #H1RP #H2RP #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ /3 width=4/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_delift.ma deleted file mode 100644 index c123668b7..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_delift.ma +++ /dev/null @@ -1,88 +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/substitution/lsubs_sfr.ma". -include "basic_2/unfold/delift.ma". -include "basic_2/unfold/thin.ma". -(* -include "basic_2/equivalence/cpcs_delift.ma". -*) -include "basic_2/dynamic/nta.ma". - -(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) - -(* Properties on reverse basic term relocation ******************************) - -(* Basic_1: was only: ty3_gen_cabbr *) -axiom thin_nta_delift_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → - ∀L2,d,e. ≼ [d, e] L1 → L1 [d, e] ≡ L2 → - ∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 : U2 & - L1 ⊢ T1 [d, e] ≡ T2 & L1 ⊢ U1 [d, e] ≡ U2. -(* -#h #L1 #T1 #U1 #H @(nta_ind_alt … H) -L1 -T1 -U1 -[ #L1 #k #L2 #d #e #HL12 #X #H - >(delift_inv_sort1 … H) -X /2 width=5/ -| #L1 #K1 #V1 #W1 #U1 #i #HLK1 #_ #HWU1 #IHVW1 #L2 #d #e #HL12 #X #H -(* - elim (delift_inv_lref1 … H) -H * - [ #Hid #H destruct - elim (thin_ldrop_conf_le … HL12 … HLK1 ?) -HL12 /2 width=2/ #X #H #HLK2 - lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 #HLK1 - elim (thin_inv_delift1 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct - elim (IHVW1 … HK12 … HV12) -IHVW1 -HK12 -HV12 #W2 #HVW2 #HW12 - elim (lift_total W2 0 (i+1)) #U2 #HWU2 - @(ex2_1_intro … U2) - [ /2 width=6/ - | -HVW2 -HLK2 - ] - | - | - ] -*) -| -| -| -| #L1 #V1 #Y1 #T1 #X1 #_ #_ #IHTX1 #IHXY1 #L2 #d #e #HL12 #X #H - elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - elim (IHTX1 … HL12 … HT12) -T1 #U1 #U2 #HTU2 #HU12 #HUX1 -(* - elim (IHXY1 … HL12 (ⓐV2.U2) ?) -IHXY1 -HL12 -*) - @(ex3_2_intro … (ⓐV1.U1) (ⓐV2.U2)) - [2: /2 width=1/ |3: /2 width=1/ ] -HV12 -HU12 -HUX1 - @(nta_pure … HTU2) -HTU2 - - [ /3 width=5/ | /2 width=1/ ] -*) -(* -| #L1 #T1 #X1 #Y1 #_ #_ #IHTX1 #IHXY1 #L2 #d #e #HL12 #X #H - elim (delift_inv_flat1 … H) -H #X2 #T2 #HX12 #HT12 #H destruct - elim (IHTX1 … HL12 … HT12) -T1 #U1 #U2 #HTU2 #HU12 #HUX1 - elim (IHXY1 … HL12 … HX12) -IHXY1 #W1 #W2 #HXW2 #_ #_ -Y1 -W1 - lapply (thin_cpcs_delift_mono … HUX1 … HL12 … HU12 … HX12) -HL12 -HX12 /4 width=5/ -| #L1 #T1 #X11 #X12 #V1 #_ #HX112 #_ #IHT1 #_ #L2 #d #e #HL12 #T2 #HT12 - elim (IHT1 … HL12 … HT12) -T1 -HL12 #U21 #U22 #HTU22 #HU212 #HUX211 - lapply (cpcs_trans … HUX211 … HX112) -X11 /2 width=5/ -] -*) -axiom nta_inv_lift1: ∀h,L1,T1,X. ⦃h, L1⦄ ⊢ T1 : X → - ∀L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀T2. ⇧[d, e] T2 ≡ T1 → - ∃∃U1,U2. ⦃h, L2⦄ ⊢ T2 : U2 & ⇧[d, e] U2 ≡ U1 & - L1 ⊢ U1 ⬌* X. -(* -#h #L1 #T1 #X #H #L2 #d #e #HL12 #T2 #HT21 -elim (nta_inv_lift1_delift … H … HL12 … HT21) -T1 -HL12 #U1 #U2 #HTU2 * #U #HU1 #HU2 #HU1X -lapply (cpcs_cpr_conf … U … HU1X) -HU1X /2 width=3/ -U1 /2 width=5/ -qed-. -*) \ No newline at end of file diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma new file mode 100644 index 000000000..1c0b1f053 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma @@ -0,0 +1,118 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/ldrop_sfr.ma". +include "basic_2/unfold/delift_lift.ma". +include "basic_2/unfold/thin_ldrop.ma". +include "basic_2/equivalence/cpcs_delift.ma". +include "basic_2/dynamic/nta_lift.ma". + +(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) + +(* Properties on basic local environment thibbing ***************************) + +(* Note: this is known as the substitution lemma *) +(* Basic_1: was only: ty3_gen_cabbr *) +lemma nta_thin_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → + ∀L2,d,e. ≼ [d, e] L1 → L1 [d, e] ≡ L2 → + ∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 : U2 & + L1 ⊢ T1 [d, e] ≡ T2 & L1 ⊢ U1 [d, e] ≡ U2. +#h #L1 #T1 #U1 #H elim H -L1 -T1 -U1 +[ /2 width=5/ +| #L1 #K1 #V1 #W1 #U1 #i #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #d #e #HL1 #HL12 + elim (lt_or_ge i d) #Hdi [ -HVW1 ] + [ lapply (sfr_ldrop_trans_ge … HLK1 … HL1 ?) -HL1 /2 width=2/ #H + lapply (sfr_inv_skip … H ?) -H /2 width=1/ #HK1 + elim (thin_ldrop_conf_le … HL12 … HLK1 ?) -HL12 /2 width=2/ #X #H #HLK2 + elim (thin_inv_delift1 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct + elim (IHVW1 … HK1 HK12) -IHVW1 -HK1 -HK12 #X2 #W2 #HVW2 #H #HW12 + lapply (delift_mono … H … HV12) -H -HV12 #H destruct + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (ldrop_fwd_ldrop2 … HLK1) -V1 #HLK1 + lapply (delift_lift_ge … HW12 … HLK1 HWU1 … HWU2) -HW12 -HLK1 -HWU1 // + >minus_plus minus_plus #HU1 + lapply (lift_conf_be … HWU2 … HW2U ?) -W2 /2 width=1/ #HU2 + lapply (delift_lift_div_be … HU1 … HU2 ? ?) -U // /2 width=1/ /3 width=8/ + | lapply (transitive_le … (i+1) Hide ?) /2 width=1/ #Hdei + lapply (thin_ldrop_conf_ge … HL12 … HLK1 ?) -HL12 -HLK1 // #HL2K1 + elim (lift_split … HWU1 d (i+1-e) ? ? ?) -HWU1 // /2 width=1/ #W + commutative_plus minus_plus commutative_plus (HH I L V 0 ? ? ?) // /5 width=6/ -| /5 width=6/ -] -qed. - (* Inversion lemmas about local env. full refinement for substitution *******) +(* Note: ldrop_ldrop not needed *) lemma sfr_inv_ldrop: ∀I,L,K,V,i. ⇩[0, i] L ≡ K. ⓑ{I}V → ∀d,e. ≼ [d, e] L → d ≤ i → i < d + e → I = Abbr. #I #L elim L -L @@ -55,3 +42,51 @@ lemma sfr_inv_ldrop: ∀I,L,K,V,i. ⇩[0, i] L ≡ K. ⓑ{I}V → ∀d,e. ≼ [d ] ] qed-. + +(* Properties about local env. full refinement for substitution *************) + +(* Note: ldrop_ldrop not needed *) +lemma sfr_ldrop: ∀L,d,e. + (∀I,K,V,i. d ≤ i → i < d + e → ⇩[0, i] L ≡ K. ⓑ{I}V → I = Abbr) → + ≼ [d, e] L. +#L elim L -L // +#L #I #V #IHL #d @(nat_ind_plus … d) -d +[ #e @(nat_ind_plus … e) -e // + #e #_ #HH + >(HH I L V 0 ? ? ?) // /5 width=6/ +| /5 width=6/ +] +qed. + +lemma sfr_ldrop_trans_le: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ≼ [dd, ee] L1 → + dd + ee ≤ d → ≼ [dd, ee] L2. +#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee +@sfr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2 +lapply (lt_to_le_to_lt … Hiddee Hddee) -Hddee #Hid +elim (ldrop_trans_le … HL12 … HLK2 ?) -L2 /2 width=2/ #X #HLK1 #H +elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K1 #V1 #HK12 #HV21 #H destruct +@(sfr_inv_ldrop … HLK1 … HL1) -L1 -K1 -V1 // +qed. + +lemma sfr_ldrop_trans_be_up: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → + ∀dd,ee. ≼ [dd, ee] L1 → + dd ≤ d + e → d + e ≤ dd + ee → + ≼ [d, dd + ee - d - e] L2. +#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hdde #Hddee +@sfr_ldrop #I #K2 #V2 #i #Hdi #Hiddee #HLK2 +lapply (transitive_le ? ? (i+e)… Hdde ?) -Hdde /2 width=1/ #Hddie +>commutative_plus in Hiddee; >minus_minus_comm commutative_plus // -Hddie /2 width=1/ +qed. + +lemma sfr_ldrop_trans_ge: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ≼ [dd, ee] L1 → + d + e ≤ dd → ≼ [dd - e, ee] L2. +#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee +@sfr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2 +elim (le_inv_plus_l … Hddee) -Hddee #Hdde #Hedd +>plus_minus in Hiddee; // #Hiddee +lapply (transitive_le … Hdde Hddi) -Hdde #Hid +lapply (ldrop_trans_ge … HL12 … HLK2 ?) -L2 // -Hid #HL1K2 +@(sfr_inv_ldrop … HL1K2 … HL1) -L1 >commutative_plus /2 width=1/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma index 727d486d4..3d53cc942 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma @@ -201,9 +201,9 @@ qed. (* Advanced properties ******************************************************) -lemma lift_conf_le: ∀T,T1,d. ⇧[O, d] T ≡ T1 → ∀T2,e. ⇧[O, d + e] T ≡ T2 → - ⇧[d, e] T1 ≡ T2. -#T #T1 #d #HT1 #T2 #e #HT2 -elim (lift_split … HT2 d d ? ? ?) -HT2 // #X #H +lemma lift_conf_be: ∀T,T1,d,e1. ⇧[d, e1] T ≡ T1 → ∀T2,e2. ⇧[d, e2] T ≡ T2 → + e1 ≤ e2 → ⇧[d + e1, e2 - e1] T1 ≡ T2. +#T #T1 #d #e1 #HT1 #T2 #e2 #HT2 #He12 +elim (lift_split … HT2 (d+e1) e1 ? ? ?) -HT2 // #X #H >(lift_mono … H … HT1) -T // qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma index f60641afc..f1cc2d9ee 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma @@ -122,6 +122,29 @@ lemma tps_split_up: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ∀i. d ≤ i → ] qed. +lemma tps_split_down: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → + ∀i. d ≤ i → i ≤ d + e → + ∃∃T. L ⊢ T1 ▶ [i, d + e - i] T & + L ⊢ T ▶ [d, i - d] T2. +#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e +[ /2 width=3/ +| #L #K #V #W #i #d #e #Hdi #Hide #HLK #HVW #j #Hdj #Hjde + elim (lt_or_ge i j) + [ -Hide -Hjde >(plus_minus_m_m j d) in ⊢ (% → ?); // -Hdj /4 width=4/ + | -Hdi -Hdj + >(plus_minus_m_m (d+e) j) in Hide; // -Hjde /3 width=4/ + ] +| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide + elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2 + elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/ + -Hdi -Hide >arith_c1x #T #HT1 #HT2 + lapply (tps_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/ +| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide + elim (IHV12 i ? ?) -IHV12 // elim (IHT12 i ? ?) -IHT12 // + -Hdi -Hide /3 width=5/ +] +qed. + (* Basic inversion lemmas ***************************************************) fact tps_inv_atom1_aux: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ∀I. T1 = ⓪{I} → diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma index 753e88796..30fa27193 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/substitution/lift_lift.ma". include "basic_2/unfold/tpss_tpss.ma". include "basic_2/unfold/delift.ma". diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma index 837e160e6..490c6ac5b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma @@ -24,8 +24,9 @@ lemma delift_lref_be: ∀L,K,V1,V2,U2,i,d,e. d ≤ i → i < d + e → ⇧[0, d] V2 ≡ U2 → L ⊢ #i [d, e] ≡ U2. #L #K #V1 #V2 #U2 #i #d #e #Hdi #Hide #HLK * #V #HV1 #HV2 #HVU2 elim (lift_total V 0 (i+1)) #U #HVU -lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus minus_plus commutative_plus in ⊢ (??%??→?); (lift_mono … HTU2 … HT2) -T2 /2 width=3/ qed. + +lemma delift_lift_div_be: ∀L,T1,T,d,e,i. L ⊢ T1 [i, d + e - i] ≡ T → + ∀T2. ⇧[d, i - d] T2 ≡ T → d ≤ i → i ≤ d + e → + L ⊢ T1 [d, e] ≡ T2. +#L #T1 #T #d #e #i * #T0 #HT10 #HT0 #T2 #HT2 #Hdi #Hide +lapply (tpss_weak … HT10 d e ? ?) -HT10 // [ >commutative_plus /2 width=1/ ] #HT10 +lapply (lift_trans_be … HT2 … HT0 ? ?) -T // +>commutative_plus >commutative_plus in ⊢ (? ? (? % ?) ? ? → ?); +