From b405363d37a437e86705bd85f5b549a36878e7d5 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 27 Jul 2012 19:00:53 +0000 Subject: [PATCH] - support for pointwise extensions of a term relation started ... - we now support abstract liftable relations --- .../lambda_delta/basic_2/grammar/aarity.ma | 2 + .../lambda_delta/basic_2/grammar/lenv_px.ma | 81 +++++++++++++++++++ .../lambda_delta/basic_2/reducibility/ltpr.ma | 53 +++--------- .../basic_2/reducibility/ltpr_aaa.ma | 2 +- .../basic_2/reducibility/ltpr_ldrop.ma | 54 ++----------- .../basic_2/reducibility/ltpr_tps.ma | 2 +- .../lambda_delta/basic_2/reducibility/tpr.ma | 2 +- .../basic_2/reducibility/tpr_lift.ma | 41 +++++----- .../basic_2/reducibility/tpr_tpss.ma | 2 +- .../basic_2/substitution/ldrop.ma | 21 +++++ .../basic_2/substitution/ldrop_lpx.ma | 68 ++++++++++++++++ .../lambda_delta/basic_2/substitution/lift.ma | 26 ++++++ 12 files changed, 237 insertions(+), 117 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_lpx.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma index 2f5f7b495..4d5d308fa 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma @@ -15,6 +15,8 @@ (* THE FORMAL SYSTEM λδ: MATITA SOURCE FILES * Suggested invocation to start formal specifications with: * - Patience on me to gain peace and perfection! - + * 2012 July 26: + * term binders polarized to control ζ reduction. * 2012 April 16 (anniversary milestone): * context-sensitive subject equivalence for atomic arity assignment. * 2012 March 15: diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma new file mode 100644 index 000000000..fd3034456 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma @@ -0,0 +1,81 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/lenv_length.ma". + +(* POINTWISE EXTENSION OF A CONTEXT-FREE REALTION FOR TERMS *****************) + +inductive lpx (R:relation term): relation lenv ≝ +| lpx_stom: lpx R (⋆) (⋆) +| lpx_pair: ∀K1,K2,I,V1,V2. + lpx R K1 K2 → R V1 V2 → lpx R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) +. + +(* Basic properties *********************************************************) + +lemma lpx_refl: ∀R. reflexive ? R → reflexive … (lpx R). +#R #HR #L elim L -L // /2 width=1/ +qed. + +(* Basic inversion lemmas ***************************************************) + +fact lpx_inv_atom1_aux: ∀R,L1,L2. lpx R L1 L2 → L1 = ⋆ → L2 = ⋆. +#R #L1 #L2 * -L1 -L2 +[ // +| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct +] +qed-. + +lemma lpx_inv_atom1: ∀R,L2. lpx R (⋆) L2 → L2 = ⋆. +/2 width=4 by lpx_inv_atom1_aux/ qed-. + +fact lpx_inv_pair1_aux: ∀R,L1,L2. lpx R L1 L2 → ∀K1,I,V1. L1 = K1. ⓑ{I} V1 → + ∃∃K2,V2. lpx R K1 K2 & R V1 V2 & L2 = K2. ⓑ{I} V2. +#R #L1 #L2 * -L1 -L2 +[ #K1 #I #V1 #H destruct +| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct /2 width=5/ +] +qed-. + +lemma lpx_inv_pair1: ∀R,K1,I,V1,L2. lpx R (K1. ⓑ{I} V1) L2 → + ∃∃K2,V2. lpx R K1 K2 & R V1 V2 & L2 = K2. ⓑ{I} V2. +/2 width=3 by lpx_inv_pair1_aux/ qed-. + +fact lpx_inv_atom2_aux: ∀R,L1,L2. lpx R L1 L2 → L2 = ⋆ → L1 = ⋆. +#R #L1 #L2 * -L1 -L2 +[ // +| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct +] +qed-. + +lemma lpx_inv_atom2: ∀R,L1. lpx R L1 (⋆) → L1 = ⋆. +/2 width=4 by lpx_inv_atom2_aux/ qed-. + +fact lpx_inv_pair2_aux: ∀R,L1,L2. lpx R L1 L2 → ∀K2,I,V2. L2 = K2. ⓑ{I} V2 → + ∃∃K1,V1. lpx R K1 K2 & R V1 V2 & L1 = K1. ⓑ{I} V1. +#R #L1 #L2 * -L1 -L2 +[ #K2 #I #V2 #H destruct +| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct /2 width=5/ +] +qed-. + +lemma lpx_inv_pair2: ∀R,L1,K2,I,V2. lpx R L1 (K2. ⓑ{I} V2) → + ∃∃K1,V1. lpx R K1 K2 & R V1 V2 & L1 = K1. ⓑ{I} V1. +/2 width=3 by lpx_inv_pair2_aux/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lpx_fwd_length: ∀R,L1,L2. lpx R L1 L2 → |L1| = |L2|. +#R #L1 #L2 #H elim H -L1 -L2 normalize // +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma index 8009cbeb7..67986d336 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma @@ -12,15 +12,12 @@ (* *) (**************************************************************************) +include "basic_2/grammar/lenv_px.ma". include "basic_2/reducibility/tpr.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) -inductive ltpr: relation lenv ≝ -| ltpr_stom: ltpr (⋆) (⋆) -| ltpr_pair: ∀K1,K2,I,V1,V2. - ltpr K1 K2 → V1 ➡ V2 → ltpr (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) (*ⓑ*) -. +definition ltpr: relation lenv ≝ lpx tpr. interpretation "context-free parallel reduction (environment)" @@ -28,62 +25,30 @@ interpretation (* Basic properties *********************************************************) -lemma ltpr_refl: ∀L:lenv. L ➡ L. -#L elim L -L // /2 width=1/ -qed. +lemma ltpr_refl: reflexive … ltpr. +/2 width=1/ qed. (* Basic inversion lemmas ***************************************************) -fact ltpr_inv_atom1_aux: ∀L1,L2. L1 ➡ L2 → L1 = ⋆ → L2 = ⋆. -#L1 #L2 * -L1 -L2 -[ // -| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct -] -qed. - (* Basic_1: was: wcpr0_gen_sort *) lemma ltpr_inv_atom1: ∀L2. ⋆ ➡ L2 → L2 = ⋆. -/2 width=3/ qed-. - -fact ltpr_inv_pair1_aux: ∀L1,L2. L1 ➡ L2 → ∀K1,I,V1. L1 = K1. ⓑ{I} V1 → - ∃∃K2,V2. K1 ➡ K2 & V1 ➡ V2 & L2 = K2. ⓑ{I} V2. -#L1 #L2 * -L1 -L2 -[ #K1 #I #V1 #H destruct -| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct /2 width=5/ -] -qed. +/2 width=2 by lpx_inv_atom1/ qed-. (* Basic_1: was: wcpr0_gen_head *) lemma ltpr_inv_pair1: ∀K1,I,V1,L2. K1. ⓑ{I} V1 ➡ L2 → ∃∃K2,V2. K1 ➡ K2 & V1 ➡ V2 & L2 = K2. ⓑ{I} V2. -/2 width=3/ qed-. - -fact ltpr_inv_atom2_aux: ∀L1,L2. L1 ➡ L2 → L2 = ⋆ → L1 = ⋆. -#L1 #L2 * -L1 -L2 -[ // -| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct -] -qed. +/2 width=1 by lpx_inv_pair1/ qed-. lemma ltpr_inv_atom2: ∀L1. L1 ➡ ⋆ → L1 = ⋆. -/2 width=3/ qed-. - -fact ltpr_inv_pair2_aux: ∀L1,L2. L1 ➡ L2 → ∀K2,I,V2. L2 = K2. ⓑ{I} V2 → - ∃∃K1,V1. K1 ➡ K2 & V1 ➡ V2 & L1 = K1. ⓑ{I} V1. -#L1 #L2 * -L1 -L2 -[ #K2 #I #V2 #H destruct -| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct /2 width=5/ -] -qed. +/2 width=2 by lpx_inv_atom2/ qed-. lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ➡ K2. ⓑ{I} V2 → ∃∃K1,V1. K1 ➡ K2 & V1 ➡ V2 & L1 = K1. ⓑ{I} V1. -/2 width=3/ qed-. +/2 width=1 by lpx_inv_pair2/ qed-. (* Basic forward lemmas *****************************************************) lemma ltpr_fwd_length: ∀L1,L2. L1 ➡ L2 → |L1| = |L2|. -#L1 #L2 #H elim H -L1 -L2 normalize // -qed-. +/2 width=2 by lpx_fwd_length/ qed-. (* Basic_1: removed theorems 2: wcpr0_getl wcpr0_getl_back *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma index 1a551cec2..df0ecca47 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma @@ -29,7 +29,7 @@ fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ⁝ A → L = L1 → T = T | #I #L1 #K1 #V1 #B #i #HLK1 #HK1 #H1 #H2 #L2 #HL12 #T2 #H destruct >(tpr_inv_atom1 … H) -T2 lapply (ldrop_pair2_fwd_cw … HLK1 (#i)) #HKV1 - elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H + elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct lapply (IH … HKV1 … HK1 … HK12 … HV12) // -L1 -K1 -V1 /2 width=5/ | #a #L1 #V1 #T1 #B #A #HB #HA #H1 #H2 #L2 #HL12 #X #H destruct 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 91ba46c60..945279795 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 @@ -12,59 +12,19 @@ (* *) (**************************************************************************) +include "basic_2/substitution/ldrop_lpx.ma". include "basic_2/reducibility/tpr_lift.ma". include "basic_2/reducibility/ltpr.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) (* 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 -[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2 width=3/ -| #K1 #I #V1 #X #H - elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/ -| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H - elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct - elim (IHLK1 … HL12) -L1 /3 width=3/ -| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H - elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct - elim (tpr_inv_lift1 … HV12 … HWV1) -V1 - elim (IHLK1 … HL12) -L1 /3 width=5/ -] -qed. +lemma ltpr_ldrop_conf: dropable_sn ltpr. +/3 width=3 by lpx_deliftable_dropable, tpr_inv_lift1/ qed. (* 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 -[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2 width=3/ -| #K1 #I #V1 #X #H - elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/ -| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12 - elim (IHLK1 … HK12) -K1 /3 width=5/ -| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H - elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct - elim (lift_total W2 d e) #V2 #HWV2 - lapply (tpr_lift … HW12 … HWV1 … HWV2) -W1 - elim (IHLK1 … HK12) -K1 /3 width=5/ -] -qed. +lemma ldrop_ltpr_trans: dedropable_sn ltpr. +/2 width=3/ qed. -fact ltpr_ldrop_trans_O1_aux: ∀L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. L1 ➡ L2 → - d = 0 → ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 ➡ K2. -#L2 #K2 #d #e #H elim H -L2 -K2 -d -e -[ #d #e #X #H >(ltpr_inv_atom2 … H) -H /2 width=3/ -| #K2 #I #V2 #X #H - elim (ltpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/ -| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_ - elim (ltpr_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct - elim (IHLK2 … HL12 ?) -L2 // /3 width=3/ -| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_ - >commutative_plus normalize #H destruct -] -qed. - -lemma ltpr_ldrop_trans_O1: ∀L1,L2. L1 ➡ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 → - ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 ➡ K2. -/2 width=5/ qed. +lemma ltpr_ldrop_trans_O1: dropable_dx ltpr. +/2 width=3/ qed. 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 5ac8a1f71..75792eef0 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 @@ -41,7 +41,7 @@ lemma ltpr_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 → ∀L2. L1 ➡ #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_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2 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/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma index fbe5f3dcc..d204eba79 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma @@ -43,7 +43,7 @@ lemma tpr_bind: ∀a,I,V1,V2,T1,T2. V1 ➡ V2 → T1 ➡ T2 → ⓑ{a,I} V1. T1 /2 width=3/ qed. (* Basic_1: was by definition: pr0_refl *) -lemma tpr_refl: ∀T. T ➡ T. +lemma tpr_refl: reflexive … tpr. #T elim T -T // #I elim I -I /2 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_lift.ma index a161723ab..b4d76066a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_lift.ma @@ -20,68 +20,65 @@ include "basic_2/reducibility/tpr.ma". (* Relocation properties ****************************************************) (* Basic_1: was: pr0_lift *) -lemma tpr_lift: ∀T1,T2. T1 ➡ T2 → - ∀d,e,U1. ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → U1 ➡ U2. +lemma tpr_lift: t_liftable tpr. #T1 #T2 #H elim H -T1 -T2 -[ * #i #d #e #U1 #HU1 #U2 #HU2 +[ * #i #U1 #d #e #HU1 #U2 #HU2 lapply (lift_mono … HU1 … HU2) -HU1 #H destruct [ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct // | lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct // | lapply (lift_inv_gref1 … HU2) -HU2 #H destruct // ] -| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 +| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #X1 #d #e #HX1 #X2 #HX2 elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct /3 width=4/ -| #a #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 +| #a #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #X1 #d #e #HX1 #X2 #HX2 elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct /3 width=4/ -| #a #I #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV12 #IHT1 #d #e #X1 #HX1 #X2 #HX2 +| #a #I #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV12 #IHT1 #X1 #d #e #HX1 #X2 #HX2 elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct elim (lift_inv_bind1 … HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct elim (lift_total T (d + 1) e) #U #HTU @tpr_delta [4: @(tps_lift_le … HT2 … HTU HTU0 ?) /2 width=1/ |1: skip |2: /2 width=4/ |3: /2 width=4/ ] (**) (*/3. is too slow *) -| #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 +| #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #X1 #d #e #HX1 #X2 #HX2 elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct elim (lift_trans_ge … HV2 … HV3 ?) -V // /3 width=4/ -| #V #T1 #T #T2 #_ #HT2 #IHT1 #d #e #X #H #U2 #HTU2 +| #V #T1 #T #T2 #_ #HT2 #IHT1 #X #d #e #H #U2 #HTU2 elim (lift_inv_bind1 … H) -H #V3 #T3 #_ #HT13 #H destruct -V elim (lift_conf_O1 … HTU2 … HT2) -T2 /3 width=4/ -| #V #T1 #T2 #_ #IHT12 #d #e #X #HX #T #HT2 +| #V #T1 #T2 #_ #IHT12 #X #d #e #HX #T #HT2 elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct /3 width=4/ ] qed. (* Basic_1: was: pr0_gen_lift *) -lemma tpr_inv_lift1: ∀T1,T2. T1 ➡ T2 → - ∀d,e,U1. ⇧[d, e] U1 ≡ T1 → - ∃∃U2. ⇧[d, e] U2 ≡ T2 & U1 ➡ U2. +lemma tpr_inv_lift1: t_deliftable_sn tpr. #T1 #T2 #H elim H -T1 -T2 -[ * #i #d #e #U1 #HU1 - [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct /2 width=3/ - | lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct /3 width=3/ - | lapply (lift_inv_gref2 … HU1) -HU1 #H destruct /2 width=3/ +[ * #i #X #d #e #HX + [ lapply (lift_inv_sort2 … HX) -HX #H destruct /2 width=3/ + | lapply (lift_inv_lref2 … HX) -HX * * #Hid #H destruct /3 width=3/ + | lapply (lift_inv_gref2 … HX) -HX #H destruct /2 width=3/ ] -| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX +| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #X #d #e #HX elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct elim (IHV12 … HV01) -V1 elim (IHT12 … HT01) -T1 /3 width=5/ -| #a #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX +| #a #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #X #d #e #HX elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct elim (IHV12 … HV01) -V1 elim (IHT12 … HT01) -T1 /3 width=5/ -| #a #I #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV12 #IHT1 #d #e #X #HX +| #a #I #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV12 #IHT1 #X #d #e #HX elim (lift_inv_bind2 … HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct elim (IHV12 … HWV1) -V1 #W2 #HWV2 #HW12 elim (IHT1 … HUT1) -T1 #U #HUT #HU1 elim (tps_inv_lift1_le … HT2 … HUT ?) -T // [3: /2 width=5/ |2: skip ] #U2 #HU2 #HUT2 @ex2_1_intro [2: /2 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /3 width=5/ is slow *) -| #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X #HX +| #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #X #d #e #HX elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct elim (IHV12 … HV01) -V1 #V3 #HV32 #HV03 @@ -89,11 +86,11 @@ lemma tpr_inv_lift1: ∀T1,T2. T1 ➡ T2 → elim (IHT12 … HT01) -T1 #T3 #HT32 #HT03 elim (lift_trans_le … HV32 … HV2 ?) -V2 // #V2 #HV32 #HV2 @ex2_1_intro [2: /3 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /4 width=5/ is slow *) -| #V #T1 #T #T2 #_ #HT2 #IHT1 #d #e #X #HX +| #V #T1 #T #T2 #_ #HT2 #IHT1 #X #d #e #HX elim (lift_inv_bind2 … HX) -HX #V3 #T3 #_ #HT31 #H destruct elim (IHT1 … HT31) -T1 #T1 #HT1 #HT31 elim (lift_div_le … HT2 … HT1 ?) -T // /3 width=5/ -| #V #T1 #T2 #_ #IHT12 #d #e #X #HX +| #V #T1 #T2 #_ #IHT12 #X #d #e #HX elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct elim (IHT12 … HT01) -T1 /3 width=3/ ] diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma index 5a00eaf55..19f737b09 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma @@ -29,7 +29,7 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ➡ T2 → elim (tps_inv_atom1 … H) -H [ #H destruct /2 width=3/ | * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct - elim (ltpr_ldrop_conf … HLK1 … HL12) -L1 #X #HLK2 #H + elim (ltpr_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2 elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct elim (lift_total V2 0 (i+1)) #U2 #HVU2 lapply (tpr_lift … HV12 … HVU1 … HVU2) -V1 #HU12 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 9ab513458..e7353d7de 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma @@ -30,6 +30,27 @@ inductive ldrop: nat → nat → relation lenv ≝ interpretation "local slicing" 'RDrop d e L1 L2 = (ldrop d e L1 L2). +definition l_liftable: (lenv → relation term) → Prop ≝ + λR. ∀K,T1,T2. R K T1 T2 → ∀L,d,e. ⇩[d, e] L ≡ K → + ∀U1. ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → R L U1 U2. + +definition l_deliftable_sn: (lenv → relation term) → Prop ≝ + λR. ∀L,U1,U2. R L U1 U2 → ∀K,d,e. ⇩[d, e] L ≡ K → + ∀T1. ⇧[d, e] T1 ≡ U1 → + ∃∃T2. ⇧[d, e] T2 ≡ U2 & R K T1 T2. + +definition dropable_sn: relation lenv → Prop ≝ + λR. ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀L2. R L1 L2 → + ∃∃K2. R K1 K2 & ⇩[d, e] L2 ≡ K2. + +definition dedropable_sn: relation lenv → Prop ≝ + λR. ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. R K1 K2 → + ∃∃L2. R L1 L2 & ⇩[d, e] L2 ≡ K2. + +definition dropable_dx: relation lenv → Prop ≝ + λR. ∀L1,L2. R L1 L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 → + ∃∃K1. ⇩[0, e] L1 ≡ K1 & R K1 K2. + (* Basic inversion lemmas ***************************************************) fact ldrop_inv_refl_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2. diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_lpx.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_lpx.ma new file mode 100644 index 000000000..2605b921c --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_lpx.ma @@ -0,0 +1,68 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/lenv_px.ma". +include "basic_2/substitution/ldrop.ma". + +(* DROPPING *****************************************************************) + +(* Properties on pointwise extension ****************************************) + +lemma lpx_deliftable_dropable: ∀R. t_deliftable_sn R → dropable_sn (lpx R). +#R #HR #L1 #K1 #d #e #H elim H -L1 -K1 -d -e +[ #d #e #X #H >(lpx_inv_atom1 … H) -H /2 width=3/ +| #K1 #I #V1 #X #H + elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/ +| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H + elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct + elim (IHLK1 … HL12) -L1 /3 width=3/ +| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H + elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct + elim (HR … HV12 … HWV1) -V1 + elim (IHLK1 … HL12) -L1 /3 width=5/ +] +qed. + +lemma lpx_liftable_dedropable: ∀R. reflexive ? R → + t_liftable R → dedropable_sn (lpx R). +#R #H1R #H2R #L1 #K1 #d #e #H elim H -L1 -K1 -d -e +[ #d #e #X #H >(lpx_inv_atom1 … H) -H /2 width=3/ +| #K1 #I #V1 #X #H + elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/ +| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12 + elim (IHLK1 … HK12) -K1 /3 width=5/ +| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H + elim (lpx_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct + elim (lift_total W2 d e) #V2 #HWV2 + lapply (H2R … HW12 … HWV1 … HWV2) -W1 + elim (IHLK1 … HK12) -K1 /3 width=5/ +] +qed. + +fact lpx_dropable_aux: ∀R,L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. lpx R L1 L2 → + d = 0 → ∃∃K1. ⇩[0, e] L1 ≡ K1 & lpx R K1 K2. +#R #L2 #K2 #d #e #H elim H -L2 -K2 -d -e +[ #d #e #X #H >(lpx_inv_atom2 … H) -H /2 width=3/ +| #K2 #I #V2 #X #H + elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/ +| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_ + elim (lpx_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct + elim (IHLK2 … HL12 ?) -L2 // /3 width=3/ +| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_ + >commutative_plus normalize #H destruct +] +qed. + +lemma ltpr_dropable: ∀R. dropable_dx (lpx R). +/2 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma index 3f3f6b0ff..36c353ba9 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma @@ -35,6 +35,14 @@ inductive lift: nat → nat → relation term ≝ interpretation "relocation" 'RLift d e T1 T2 = (lift d e T1 T2). +definition t_liftable: relation term → Prop ≝ + λR. ∀T1,T2. R T1 T2 → ∀U1,d,e. ⇧[d, e] T1 ≡ U1 → + ∀U2. ⇧[d, e] T2 ≡ U2 → R U1 U2. + +definition t_deliftable_sn: relation term → Prop ≝ + λR. ∀U1,U2. R U1 U2 → ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → + ∃∃T2. ⇧[d, e] T2 ≡ U2 & R T1 T2. + (* Basic inversion lemmas ***************************************************) fact lift_inv_refl_O2_aux: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → e = 0 → T1 = T2. @@ -369,6 +377,24 @@ lemma is_lift_dec: ∀T2,d,e. Decidable (∃T1. ⇧[d,e] T1 ≡ T2). ] qed. +lemma t_liftable_TC: ∀R. t_liftable R → t_liftable (TC … R). +#R #HR #T1 #T2 #H elim H -T2 +[ /3 width=7/ +| #T #T2 #_ #HT2 #IHT1 #U1 #d #e #HTU1 #U2 #HTU2 + elim (lift_total T d e) /3 width=9/ +] +qed. + +lemma t_deliftable_sn_TC: ∀R. t_deliftable_sn R → t_deliftable_sn (TC … R). +#R #HR #U1 #U2 #H elim H -U2 +[ #U2 #HU12 #T1 #d #e #HTU1 + elim (HR … HU12 … HTU1) -U1 /3 width=3/ +| #U #U2 #_ #HU2 #IHU1 #T1 #d #e #HTU1 + elim (IHU1 … HTU1) -U1 #T #HTU #HT1 + elim (HR … HU2 … HTU) -U /3 width=5/ +] +qed-. + (* Basic_1: removed theorems 7: lift_head lift_gen_head lift_weight_map lift_weight lift_weight_add lift_weight_add_O -- 2.39.2