From: Ferruccio Guidi Date: Wed, 16 May 2012 20:28:10 +0000 (+0000) Subject: - a caracterization of the top elements of the local evironment X-Git-Tag: make_still_working~1730 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=78d4844bcccb3deb58a3179151c3045298782b18;p=helm.git - a caracterization of the top elements of the local evironment refinement for substitution - notation update for subsstitution and unfold - added notation for True and False --- diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/notation.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/notation.ma index 031b745e4..8a7274651 100644 --- a/matita/matita/contribs/lambda_delta/apps_2/functional/notation.ma +++ b/matita/matita/contribs/lambda_delta/apps_2/functional/notation.ma @@ -14,14 +14,14 @@ (* NOTATION FOR THE "functional" COMPONENT ********************************) -notation "hvbox( ↑ [ d , break e ] break T )" +notation "hvbox( ↑ [ d , break e ] break term 60 T )" non associative with precedence 60 for @{ 'Lift $d $e $T }. -notation "hvbox( [ d ← break V ] break T )" +notation "hvbox( [ d ← break V ] break term 60 T )" non associative with precedence 60 for @{ 'Subst $V $d $T }. -notation "hvbox( T1 ⇨ break T2 )" +notation "hvbox( T1 ⇨ break term 46 T2 )" non associative with precedence 45 for @{ 'SRed $T1 $T2 }. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma index 6314894c2..7bfe24895 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma @@ -56,7 +56,7 @@ lemma cprs_strap2: ∀L,T1,T,T2. (* Note: it does not hold replacing |L1| with |L2| *) lemma cprs_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 → - ∀L2. L1 [0, |L1|] ≼ L2 → L2 ⊢ T1 ➡* T2. + ∀L2. L1 ≼ [0, |L1|] L2 → L2 ⊢ T1 ➡* T2. /3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma index 14bcfd5c4..86f2a13ea 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma @@ -21,8 +21,8 @@ include "basic_2/computation/cprs.ma". (* Properties concerning context-sensitive parallel reduction on lenv's *****) -lemma ltpr_tpss_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2,d,e. L2 ⊢ T1 [d, e] ▶* T2 → - ∃∃T. L1 ⊢ T1 [d, e] ▶* T & L1 ⊢ T ➡* T2. +lemma ltpr_tpss_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2,d,e. L2 ⊢ T1 ▶* [d, e] T2 → + ∃∃T. L1 ⊢ T1 ▶* [d, e] T & L1 ⊢ T ➡* T2. #L1 #L2 #HL12 #T1 #T2 #d #e #H @(tpss_ind … H) -T2 [ /2 width=3/ | #T #T2 #_ #HT2 * #T0 #HT10 #HT0 diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_ltpr.ma index 8859a46d6..2682a7609 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_ltpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_ltpr.ma @@ -20,9 +20,9 @@ include "basic_2/computation/cprs.ma". (* Properties concerning parallel unfold on terms ***************************) (* Basic_1: was only: pr3_subst1 *) -lemma cprs_tpss_ltpr: ∀L1,T1,U1,d,e. L1 ⊢ T1 [d, e] ▶* U1 → +lemma cprs_tpss_ltpr: ∀L1,T1,U1,d,e. L1 ⊢ T1 ▶* [d, e] U1 → ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → - ∃∃U2. L2 ⊢ U1 ➡* U2 & L2 ⊢ T2 [d, e] ▶* U2. + ∃∃U2. L2 ⊢ U1 ➡* U2 & L2 ⊢ T2 ▶* [d, e] U2. #L1 #T1 #U1 #d #e #HTU1 #L2 #HL12 #T2 #HT12 elim HT12 -T2 [ #T2 #HT12 elim (cpr_tpss_ltpr … HL12 … HT12 … HTU1) -L1 -T1 /3 width=3/ 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 27c79d1b6..903c62ea2 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma @@ -27,7 +27,7 @@ interpretation lemma csn_ind: ∀L. ∀R:predicate term. (∀T1. L ⊢ ⬇* T1 → - (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → R T2) → + (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → R T2) → R T1 ) → ∀T. L ⊢ ⬇* T → R T. @@ -39,10 +39,8 @@ qed-. (* Basic_1: was: sn3_pr2_intro *) lemma csn_intro: ∀L,T1. - (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇* T2) → L ⊢ ⬇* T1. -#L #T1 #H -@(SN_intro … H) -qed. + (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬇* T2) → L ⊢ ⬇* T1. +/4 width=1/ qed. (* Basic_1: was: sn3_nf2 *) lemma csn_cnf: ∀L,T. L ⊢ 𝐍[T] → L ⊢ ⬇* T. @@ -84,7 +82,7 @@ lemma csn_fwd_flat_dx: ∀I,L,V,T. L ⊢ ⬇* ⓕ{I} V. T → L ⊢ ⬇* T. (* Basic_1: removed theorems 14: sn3_cdelta - sn3_gen_cflat sn3_cflat sn3_cpr3_trans sn3_shift sn3_change - sn3_appl_cast sn3_appl_beta sn3_appl_lref sn3_appl_abbr - sn3_appl_appls sn3_bind sn3_appl_bind sn3_appls_bind + sn3_gen_cflat sn3_cflat sn3_cpr3_trans sn3_shift sn3_change + sn3_appl_cast sn3_appl_beta sn3_appl_lref sn3_appl_abbr + sn3_appl_appls sn3_bind sn3_appl_bind sn3_appls_bind *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_alt.ma index 6b4b61ae6..980b4b700 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_alt.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_alt.ma @@ -28,7 +28,7 @@ interpretation lemma csna_ind: ∀L. ∀R:predicate term. (∀T1. L ⊢ ⬇⬇* T1 → - (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → R T2) → R T1 + (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → R T2) → R T1 ) → ∀T. L ⊢ ⬇⬇* T → R T. #L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1 @@ -39,13 +39,11 @@ qed-. (* Basic_1: was: sn3_intro *) lemma csna_intro: ∀L,T1. - (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → L ⊢ ⬇⬇* T2) → L ⊢ ⬇⬇* T1. -#L #T1 #H -@(SN_intro … H) -qed. + (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → L ⊢ ⬇⬇* T2) → L ⊢ ⬇⬇* T1. +/4 width=1/ qed. fact csna_intro_aux: ∀L,T1. - (∀T,T2. L ⊢ T ➡* T2 → T1 = T → (T1 = T2 → False) → L ⊢ ⬇⬇* T2) → L ⊢ ⬇⬇* T1. + (∀T,T2. L ⊢ T ➡* T2 → T1 = T → (T1 = T2 → ⊥) → L ⊢ ⬇⬇* T2) → L ⊢ ⬇⬇* T1. /4 width=3/ qed-. (* Basic_1: was: sn3_pr3_trans (old version) *) @@ -59,7 +57,7 @@ qed. (* Basic_1: was: sn3_pr2_intro (old version) *) lemma csna_intro_cpr: ∀L,T1. - (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇⬇* T2) → + (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬇⬇* T2) → L ⊢ ⬇⬇* T1. #L #T1 #H @csna_intro_aux #T #T2 #H @(cprs_ind_dx … H) -T @@ -91,7 +89,7 @@ lemma csn_cprs_trans: ∀L,T1. L ⊢ ⬇* T1 → ∀T2. L ⊢ T1 ➡* T2 → L lemma csn_ind_alt: ∀L. ∀R:predicate term. (∀T1. L ⊢ ⬇* T1 → - (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → R T2) → R T1 + (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → R T2) → R T1 ) → ∀T. L ⊢ ⬇* T → R T. #L #R #H0 #T1 #H @(csna_ind … (csn_csna … H)) -T1 #T1 #HT1 #IHT1 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 169073516..33c6455dc 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 @@ -120,7 +120,7 @@ lemma csn_appl_theta: ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → (* Basic_1: was only: sn3_appl_appl *) lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬇* V → ∀T1. L ⊢ ⬇* T1 → - (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → False) → L ⊢ ⬇* ⓐV. T2) → + (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → ⊥) → L ⊢ ⬇* ⓐV. T2) → 𝐒[T1] → L ⊢ ⬇* ⓐV. T1. #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1 @csn_intro #X #HL #H 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 93e22f77a..71b4d3380 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 @@ -27,7 +27,7 @@ lemma csn_lift: ∀L2,L1,T1,d,e. L1 ⊢ ⬇* T1 → @csn_intro #T #HLT2 #HT2 elim (cpr_inv_lift … HL21 … HT12 … HLT2) -HLT2 #T0 #HT0 #HLT10 @(IHT1 … HLT10) // -L1 -L2 #H destruct ->(lift_mono … HT0 … HT12) in HT2; -T0 /2 width=1/ +>(lift_mono … HT0 … HT12) in HT2; -T1 /2 width=1/ qed. (* Basic_1: was: sn3_gen_lift *) @@ -38,7 +38,7 @@ lemma csn_inv_lift: ∀L2,L1,T1,d,e. L1 ⊢ ⬇* T1 → elim (lift_total T d e) #T0 #HT0 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/ +>(lift_inj … HT0 … HT21) in HT2; -T1 /2 width=1/ qed. (* Advanced properties ******************************************************) @@ -70,7 +70,7 @@ elim (eq_false_inv_tpair_sn … H2) -H2 qed. lemma csn_appl_simple: ∀L,V. L ⊢ ⬇* V → ∀T1. - (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇* ⓐV. T2) → + (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬇* ⓐV. T2) → 𝐒[T1] → L ⊢ ⬇* ⓐV. T1. #L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1 @csn_intro #X #H1 #H2 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 index e36695081..c123668b7 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_delift.ma @@ -12,21 +12,23 @@ (* *) (**************************************************************************) -include "basic_2/unfold/delift_lift.ma". -include "basic_2/unfold/thin_ldrop.ma". +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_nta.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,X1. ⦃h, L1⦄ ⊢ T1 : X1 → - ∀L2,d,e. L1 [d, e] ≡ L2 → - ∀T2. L1 ⊢ T1 [d, e] ≡ T2 → - ∃∃U1,U2. ⦃h, L2⦄ ⊢ T2 : U2 & L1 ⊢ U1 [d, e] ≡ U2 & - L1 ⊢ U1 ⬌* X1. +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 @@ -51,13 +53,19 @@ axiom thin_nta_delift_conf: ∀h,L1,T1,X1. ⦃h, L1⦄ ⊢ T1 : X1 → | | | -| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHVW1 #L2 #d #e #HL12 #X #H +| #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 (IHTU1 … HL12 … HT12) -T1 #U2 #HTU2 #HU12 - elim (IHVW1 … HL12 (ⓐV2.U2) ?) -IHVW1 -HL12 + 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 @@ -68,17 +76,13 @@ axiom thin_nta_delift_conf: ∀h,L1,T1,X1. ⦃h, L1⦄ ⊢ T1 : X1 → lapply (cpcs_trans … HUX211 … HX112) -X11 /2 width=5/ ] *) -lemma nta_inv_lift1_delift: ∀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 & L1 ⊢ U1 [d, e] ≡ U2 & - L1 ⊢ U1 ⬌* X. -/3 width=3/ qed-. - -lemma nta_inv_lift1: ∀h,L1,T1,X. ⦃h, L1⦄ ⊢ T1 : X → +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/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma index ddf9e7865..b5ebbe8af 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma @@ -42,7 +42,7 @@ lapply (cprs_inv_sort1 … H2) -L #H destruct // qed-. (* Basic_1: was: pc3_gen_sort_abst *) -lemma cpcs_inv_sort_abst: ∀L,W,T,k. L ⊢ ⋆k ⬌* ⓛW.T → False. +lemma cpcs_inv_sort_abst: ∀L,W,T,k. L ⊢ ⋆k ⬌* ⓛW.T → ⊥. #L #W #T #k #H elim (cpcs_inv_cprs … H) -H #X #H1 >(cprs_inv_sort1 … H1) -X #H2 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 0d7db6beb..3f5fb80d4 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma @@ -41,7 +41,7 @@ interpretation "aarity construction (binary)" (* Basic inversion lemmas ***************************************************) -lemma discr_apair_xy_x: ∀A,B. ②B. A = B → False. +lemma discr_apair_xy_x: ∀A,B. ②B. A = B → ⊥. #A #B elim B -B [ #H destruct | #Y #X #IHY #_ #H destruct @@ -50,7 +50,7 @@ lemma discr_apair_xy_x: ∀A,B. ②B. A = B → False. ] qed-. -lemma discr_tpair_xy_y: ∀B,A. ②B. A = A → False. +lemma discr_tpair_xy_y: ∀B,A. ②B. A = A → ⊥. #B #A elim A -A [ #H destruct | #Y #X #_ #IHX #H destruct diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lsubs.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lsubs.ma deleted file mode 100644 index ed8404355..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lsubs.ma +++ /dev/null @@ -1,96 +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/grammar/lenv_length.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************) - -inductive lsubs: nat → nat → relation lenv ≝ -| lsubs_sort: ∀d,e. lsubs d e (⋆) (⋆) -| lsubs_OO: ∀L1,L2. lsubs 0 0 L1 L2 -| lsubs_abbr: ∀L1,L2,V,e. lsubs 0 e L1 L2 → - lsubs 0 (e + 1) (L1. ⓓV) (L2.ⓓV) -| lsubs_abst: ∀L1,L2,I,V1,V2,e. lsubs 0 e L1 L2 → - lsubs 0 (e + 1) (L1. ⓛV1) (L2.ⓑ{I} V2) -| lsubs_skip: ∀L1,L2,I1,I2,V1,V2,d,e. - lsubs d e L1 L2 → lsubs (d + 1) e (L1. ⓑ{I1} V1) (L2. ⓑ{I2} V2) -. - -interpretation - "local environment refinement (substitution)" - 'SubEq L1 d e L2 = (lsubs d e L1 L2). - -definition lsubs_conf: ∀S. (lenv → relation S) → Prop ≝ λS,R. - ∀L1,s1,s2. R L1 s1 s2 → - ∀L2,d,e. L1 [d, e] ≼ L2 → R L2 s1 s2. - -(* Basic properties *********************************************************) - -lemma TC_lsubs_conf: ∀S,R. lsubs_conf S R → lsubs_conf S (λL. (TC … (R L))). -#S #R #HR #L1 #s1 #s2 #H elim H -s2 -[ /3 width=5/ -| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12 - lapply (HR … Hs2 … HL12) -HR -Hs2 -HL12 /3 width=3/ -] -qed. - -lemma lsubs_bind_eq: ∀L1,L2,e. L1 [0, e] ≼ L2 → ∀I,V. - L1. ⓑ{I} V [0, e + 1] ≼ L2.ⓑ{I} V. -#L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/ -qed. - -lemma lsubs_refl: ∀d,e,L. L [d, e] ≼ L. -#d elim d -d -[ #e elim e -e // #e #IHe #L elim L -L // /2 width=1/ -| #d #IHd #e #L elim L -L // /2 width=1/ -] -qed. - -lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≼ L2 → 0 < d → - ∀I1,I2,V1,V2. L1. ⓑ{I1} V1 [d, e] ≼ L2. ⓑ{I2} V2. - -#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/ -qed. - -(* Basic inversion lemmas ***************************************************) - -(* Basic forward lemmas ***************************************************) - -fact lsubs_fwd_length_full1_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → - d = 0 → e = |L1| → |L1| ≤ |L2|. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize -[ // -| /2 width=1/ -| /3 width=1/ -| /3 width=1/ -| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct -] -qed. - -lemma lsubs_fwd_length_full1: ∀L1,L2. L1 [0, |L1|] ≼ L2 → |L1| ≤ |L2|. -/2 width=5/ qed-. - -fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → - d = 0 → e = |L2| → |L2| ≤ |L1|. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize -[ // -| /2 width=1/ -| /3 width=1/ -| /3 width=1/ -| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct -] -qed. - -lemma lsubs_fwd_length_full2: ∀L1,L2. L1 [0, |L2|] ≼ L2 → |L2| ≤ |L1|. -/2 width=5/ 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 44e303691..0cfa1b024 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term.ma @@ -62,7 +62,7 @@ axiom term_eq_dec: ∀T1,T2:term. Decidable (T1 = T2). (* Basic inversion lemmas ***************************************************) -lemma discr_tpair_xy_x: ∀I,T,V. ②{I} V. T = V → False. +lemma discr_tpair_xy_x: ∀I,T,V. ②{I} V. T = V → ⊥. #I #T #V elim V -V [ #J #H destruct | #J #W #U #IHW #_ #H destruct @@ -72,7 +72,7 @@ lemma discr_tpair_xy_x: ∀I,T,V. ②{I} V. T = V → False. qed-. (* Basic_1: was: thead_x_y_y *) -lemma discr_tpair_xy_y: ∀I,V,T. ②{I} V. T = T → False. +lemma discr_tpair_xy_y: ∀I,V,T. ②{I} V. T = T → ⊥. #I #V #T elim T -T [ #J #H destruct | #J #W #U #_ #IHU #H destruct @@ -82,25 +82,25 @@ lemma discr_tpair_xy_y: ∀I,V,T. ②{I} V. T = T → False. qed-. lemma eq_false_inv_tpair_sn: ∀I,V1,T1,V2,T2. - (②{I} V1. T1 = ②{I} V2. T2 → False) → - (V1 = V2 → False) ∨ (V1 = V2 ∧ (T1 = T2 → False)). + (②{I} V1. T1 = ②{I} V2. T2 → ⊥) → + (V1 = V2 → ⊥) ∨ (V1 = V2 ∧ (T1 = T2 → ⊥)). #I #V1 #T1 #V2 #T2 #H elim (term_eq_dec V1 V2) /3 width=1/ #HV12 destruct @or_intror @conj // #HT12 destruct /2 width=1/ qed-. lemma eq_false_inv_tpair_dx: ∀I,V1,T1,V2,T2. - (②{I} V1. T1 = ②{I} V2. T2 → False) → - (T1 = T2 → False) ∨ (T1 = T2 ∧ (V1 = V2 → False)). + (②{I} V1. T1 = ②{I} V2. T2 → ⊥) → + (T1 = T2 → ⊥) ∨ (T1 = T2 ∧ (V1 = V2 → ⊥)). #I #V1 #T1 #V2 #T2 #H elim (term_eq_dec T1 T2) /3 width=1/ #HT12 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. ⓛW1. T1 = ⓐV2. ⓛW2 .T2 →⊥) → + (W1 = W2 → ⊥) ∨ + (W1 = W2 ∧ (ⓓV1. T1 = ⓓV2. T2 → ⊥)). #V1 #V2 #W1 #W2 #T1 #T2 #H elim (eq_false_inv_tpair_sn … H) -H [ #HV12 elim (term_eq_dec W1 W2) /3 width=1/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma index b51523544..f32ae0e7e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma @@ -25,14 +25,14 @@ interpretation "simple (term)" 'Simple T = (simple T). (* Basic inversion lemmas ***************************************************) -fact simple_inv_bind_aux: ∀T. 𝐒[T] → ∀J,W,U. T = ⓑ{J} W. U → False. +fact simple_inv_bind_aux: ∀T. 𝐒[T] → ∀J,W,U. T = ⓑ{J} W. U → ⊥. #T * -T [ #I #J #W #U #H destruct | #I #V #T #J #W #U #H destruct ] qed. -lemma simple_inv_bind: ∀I,V,T. 𝐒[ⓑ{I} V. T] → False. +lemma simple_inv_bind: ∀I,V,T. 𝐒[ⓑ{I} V. T] → ⊥. /2 width=6/ qed-. lemma simple_inv_pair: ∀I,V,T. 𝐒[②{I}V.T] → ∃J. I = Flat2 J. diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma index 0b7895923..1ded6dd5d 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma @@ -21,7 +21,7 @@ include "basic_2/grammar/tstc.ma". (* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *) lemma tstc_inv_bind_appls_simple: ∀I,Vs,V2,T1,T2. ⒶVs.T1 ≃ ⓑ{I} V2. T2 → - 𝐒[T1] → False. + 𝐒[T1] → ⊥. #I #Vs #V2 #T1 #T2 #H elim (tstc_inv_pair2 … H) -H #V0 #T0 elim Vs -Vs normalize diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index 3051f1e11..e56344d7d 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -16,7 +16,7 @@ (* Grammar ******************************************************************) -notation "hvbox( ⓪ )" +notation "⓪" non associative with precedence 90 for @{ 'Item0 }. @@ -24,7 +24,7 @@ notation "hvbox( ⓪ { I } )" non associative with precedence 90 for @{ 'Item0 $I }. -notation "hvbox( ⋆ )" +notation "⋆" non associative with precedence 90 for @{ 'Star }. @@ -104,7 +104,7 @@ notation "hvbox( # [ x , break y ] )" non associative with precedence 90 for @{ 'Weight $x $y }. -notation "hvbox( 𝐒 [ T ] )" +notation "hvbox( 𝐒 [ T ] )" non associative with precedence 45 for @{ 'Simple $T }. @@ -116,21 +116,17 @@ notation "hvbox( T1 ≃ break term 46 T2 )" non associative with precedence 45 for @{ 'Iso $T1 $T2 }. -notation "hvbox( T1 break [ d , break e ] ≼ break term 46 T2 )" - non associative with precedence 45 - for @{ 'SubEq $T1 $d $e $T2 }. - (* Substitution *************************************************************) -notation "hvbox( L ⊢ break [ d , break e ] break 𝐑 [ T ] )" +notation "hvbox( L ⊢ break 𝐑 [ d , break e ] break ⦃ T ⦄ )" non associative with precedence 45 for @{ 'Reducible $L $d $e $T }. -notation "hvbox( L ⊢ break [ d , break e ] break 𝐈 [ T ] )" +notation "hvbox( L ⊢ break 𝐈 [ d , break e ] break ⦃ T ⦄ )" non associative with precedence 45 for @{ 'NotReducible $L $d $e $T }. -notation "hvbox( L ⊢ break [ d , break e ] break 𝐍 [ T ] )" +notation "hvbox( L ⊢ break 𝐍 [ d , break e ] break ⦃ T ⦄ )" non associative with precedence 45 for @{ 'Normal $L $d $e $T }. @@ -138,6 +134,14 @@ notation "hvbox( ⇧ [ d , break e ] break term 46 T1 ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'RLift $d $e $T1 $T2 }. +notation "hvbox( T1 break ≼ [ d , break e ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'SubEq $T1 $d $e $T2 }. + +notation "hvbox( ≼ [ d , break e ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'SubEqTop $d $e $T2 }. + notation "hvbox( ⇩ [ e ] break term 46 L1 ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'RDrop $e $L1 $L2 }. @@ -146,11 +150,11 @@ notation "hvbox( ⇩ [ d , break e ] break term 46 L1 ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'RDrop $d $e $L1 $L2 }. -notation "hvbox( L ⊢ break ⌘ [ T ] ≡ break term 46 k )" +notation "hvbox( L ⊢ break ⌘ ⦃ T ⦄ ≡ break term 46 k )" non associative with precedence 45 for @{ 'ICM $L $T $k }. -notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ▶ break term 46 T2 )" +notation "hvbox( L ⊢ break term 46 T1 break ▶ [ d , break e ] break term 46 T2 )" non associative with precedence 45 for @{ 'PSubst $L $T1 $d $e $T2 }. @@ -172,15 +176,15 @@ notation "hvbox( ⇩ * [ e ] break term 46 L1 ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'RDropStar $e $L1 $L2 }. -notation "hvbox( T1 break [ d , break e ] ▶* break term 46 T2 )" +notation "hvbox( T1 break ▶* [ d , break e ] break term 46 T2 )" non associative with precedence 45 for @{ 'PSubstStar $T1 $d $e $T2 }. -notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ▶* break term 46 T2 )" +notation "hvbox( L ⊢ break term 46 T1 break ▶* [ d , break e ] break term 46 T2 )" non associative with precedence 45 for @{ 'PSubstStar $L $T1 $d $e $T2 }. -notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ▶▶* break term 46 T2 )" +notation "hvbox( L ⊢ break term 46 T1 break ▶▶* [ d , break e ] break term 46 T2 )" non associative with precedence 45 for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }. @@ -192,11 +196,11 @@ notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ≡ break term 46 non associative with precedence 45 for @{ 'TSubst $L $T1 $d $e $T2 }. -notation "hvbox( T1 break [ d , break e ] ≡≡ break term 46 T2 )" +notation "hvbox( T1 break [ d , break e ] ≡ ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubstAlt $T1 $d $e $T2 }. -notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ≡≡ break term 46 T2 )" +notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ≡ ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubstAlt $L $T1 $d $e $T2 }. @@ -230,7 +234,7 @@ notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 •* break term 46 T2 (* Reducibility *************************************************************) -notation "hvbox( 𝐑 [ T ] )" +notation "hvbox( 𝐑 [ T ] )" non associative with precedence 45 for @{ 'Reducible $T }. @@ -238,7 +242,7 @@ notation "hvbox( L ⊢ break 𝐑 [ T ] )" non associative with precedence 45 for @{ 'Reducible $L $T }. -notation "hvbox( 𝐈 [ T ] )" +notation "hvbox( 𝐈 [ T ] )" non associative with precedence 45 for @{ 'NotReducible $T }. @@ -246,7 +250,7 @@ notation "hvbox( L ⊢ break 𝐈 [ T ] )" non associative with precedence 45 for @{ 'NotReducible $L $T }. -notation "hvbox( 𝐍 [ T ] )" +notation "hvbox( 𝐍 [ T ] )" non associative with precedence 45 for @{ 'Normal $T }. @@ -258,11 +262,11 @@ notation "hvbox( 𝐖𝐇𝐑 [ T ] )" non associative with precedence 45 for @{ 'WHdReducible $T }. -notation "hvbox( L ⊢ break 𝐖𝐇𝐑 [ T ] )" +notation "hvbox( L ⊢ break 𝐖𝐇𝐑 [ T ] )" non associative with precedence 45 for @{ 'WHdReducible $L $T }. -notation "hvbox( 𝐖𝐇𝐈 [ T ] )" +notation "hvbox( 𝐖𝐇𝐈 [ T ] )" non associative with precedence 45 for @{ 'NotWHdReducible $T }. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma index 00647e43c..1156dcf68 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma @@ -32,6 +32,6 @@ qed. (* Basic_1: was: nf2_dec *) axiom cnf_dec: ∀L,T1. L ⊢ 𝐍[T1] ∨ - ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → False). + ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → ⊥). (* Basic_1: removed theorems 1: nf2_abst_shift *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma index 43007c98a..e0d8d57bb 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma @@ -39,14 +39,14 @@ qed. lemma cnf_abst: ∀I,L,V,W,T. L ⊢ 𝐍[W] → L. ⓑ{I} V ⊢ 𝐍[T] → L ⊢ 𝐍[ⓛW.T]. #I #L #V #W #T #HW #HT #X #H elim (cpr_inv_abst1 … H I V) -H #W0 #T0 #HW0 #HT0 #H destruct ->(HW … HW0) -W >(HT … HT0) -T // +>(HW … HW0) -W0 >(HT … HT0) -T0 // qed. (* Basic_1: was only: nf2_appl_lref *) lemma cnf_appl_simple: ∀L,V,T. L ⊢ 𝐍[V] → L ⊢ 𝐍[T] → 𝐒[T] → L ⊢ 𝐍[ⓐV.T]. #L #V #T #HV #HT #HS #X #H elim (cpr_inv_appl1_simple … H ?) -H // #V0 #T0 #HV0 #HT0 #H destruct ->(HV … HV0) -V >(HT … HT0) -T // +>(HV … HV0) -V0 >(HT … HT0) -T0 // qed. (* Relocation properties ****************************************************) @@ -56,6 +56,6 @@ lemma cnf_lift: ∀L0,L,T,T0,d,e. L ⊢ 𝐍[T] → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → L0 ⊢ 𝐍[T0]. #L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H elim (cpr_inv_lift … HL0 … HT0 … H) -L0 #T1 #HT10 #HT1 ->(HLT … HT1) in HT0; -L #HT0 +<(HLT … HT1) in HT0; -L #HT0 >(lift_mono … HT10 … HT0) -T1 -X // qed. 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 34ad5d844..caa36dfd5 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma @@ -20,7 +20,7 @@ include "basic_2/reducibility/tpr.ma". (* Basic_1: includes: pr2_delta1 *) definition cpr: lenv → relation term ≝ - λL,T1,T2. ∃∃T. T1 ➡ T & L ⊢ T [0, |L|] ▶* T2. + λL,T1,T2. ∃∃T. T1 ➡ T & L ⊢ T ▶* [0, |L|] T2. interpretation "context-sensitive parallel reduction (term)" @@ -28,14 +28,14 @@ interpretation (* Basic properties *********************************************************) -lemma cpr_intro: ∀L,T1,T,T2,d,e. T1 ➡ T → L ⊢ T [d, e] ▶* T2 → L ⊢ T1 ➡ T2. +lemma cpr_intro: ∀L,T1,T,T2,d,e. T1 ➡ T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ➡ T2. /4 width=3/ qed-. (* Basic_1: was by definition: pr2_free *) lemma cpr_tpr: ∀T1,T2. T1 ➡ T2 → ∀L. L ⊢ T1 ➡ T2. /2 width=3/ qed. -lemma cpr_tpss: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T1 ➡ T2. +lemma cpr_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ➡ T2. /3 width=5/ qed. lemma cpr_refl: ∀L,T. L ⊢ T ➡ T. @@ -56,7 +56,7 @@ qed. (* Note: it does not hold replacing |L1| with |L2| *) (* Basic_1: was only: pr2_change *) lemma cpr_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 → - ∀L2. L1 [0, |L1|] ≼ L2 → L2 ⊢ T1 ➡ T2. + ∀L2. L1 ≼ [0, |L1|] L2 → L2 ⊢ T1 ➡ T2. #L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12 lapply (tpss_lsubs_conf … HT2 … HL12) -HT2 -HL12 /3 width=4/ qed. @@ -78,7 +78,7 @@ qed-. (* Basic_1: was pr2_gen_abbr *) lemma cpr_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡ U2 → - (∃∃V,V2,T2. V1 ➡ V & L ⊢ V [O, |L|] ▶* V2 & + (∃∃V,V2,T2. V1 ➡ V & L ⊢ V ▶* [O, |L|] V2 & L. ⓓV ⊢ T1 ➡ T2 & U2 = ⓓV2. T2 ) ∨ diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma index eb5fb1471..120946cb1 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma @@ -21,7 +21,7 @@ include "basic_2/reducibility/cpr.ma". (* Advanced properties ******************************************************) lemma cpr_cdelta: ∀L,K,V1,W1,W2,i. - ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 [0, |L| - i - 1] ▶* W1 → + ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 ▶* [0, |L| - i - 1] W1 → ⇧[0, i + 1] W1 ≡ W2 → L ⊢ #i ➡ W2. #L #K #V1 #W1 #W2 #i #HLK #HVW1 #HW12 lapply (ldrop_fwd_ldrop2_length … HLK) #Hi @@ -43,7 +43,7 @@ qed. lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ➡ T2 → T2 = #i ∨ ∃∃K,V1,T1. ⇩[0, i] L ≡ K. ⓓV1 & - K ⊢ V1 [0, |L| - i - 1] ▶* T1 & + K ⊢ V1 ▶* [0, |L| - i - 1] T1 & ⇧[0, i + 1] T1 ≡ T2 & i < |L|. #L #T2 #i * #X #H 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 72b714a62..d3e75f8c0 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 @@ -22,8 +22,8 @@ include "basic_2/reducibility/cpr.ma". (* Note: we could invoke tpss_weak_all instead of ltpr_fwd_length *) (* Basic_1: was only: pr2_subst1 *) lemma cpr_tpss_ltpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → - ∀d,e,U1. L1 ⊢ T1 [d, e] ▶* U1 → - ∃∃U2. L2 ⊢ U1 ➡ U2 & L2 ⊢ T2 [d, e] ▶* U2. + ∀d,e,U1. L1 ⊢ T1 ▶* [d, e] U1 → + ∃∃U2. L2 ⊢ U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2. #L1 #L2 #HL12 #T1 #T2 * #T #HT1 #HT2 #d #e #U1 #HTU1 elim (tpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 -HT1 #U #HU1 #HTU elim (tpss_conf_eq … HT2 … HTU) -T /3 width=3/ @@ -37,7 +37,7 @@ elim (tpr_tpss_ltpr … HL12 … HT2) -L1 /3 width=3/ qed. lemma cpr_ltpr_conf_tpss: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡ T2 → - ∀d,e,U1. L1 ⊢ T1 [d, e] ▶* U1 → + ∀d,e,U1. L1 ⊢ T1 ▶* [d, e] U1 → ∃∃U2. L2 ⊢ U1 ➡ U2 & L2 ⊢ T2 ➡ U2. #L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 elim (cpr_ltpr_conf_eq … HT12 … HL12) -HT12 #T #HT1 #HT2 diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma index a3b31f225..08da2e373 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma @@ -19,7 +19,7 @@ include "basic_2/reducibility/cpr.ma". (* Properties concerning partial unfold on local environments ***************) -lemma ltpss_cpr_trans: ∀L1,L2,d,e. L1 [d, e] ▶* L2 → +lemma ltpss_cpr_trans: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2. #L1 #L2 #d #e #HL12 #T1 #T2 * lapply (ltpss_weak_all … HL12) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma index 51028c240..6f0527b33 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma @@ -18,7 +18,7 @@ include "basic_2/reducibility/ltpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************) definition lcpr: relation lenv ≝ - λL1,L2. ∃∃L. L1 ➡ L & L [0, |L|] ▶* L2 + λL1,L2. ∃∃L. L1 ➡ L & L ▶* [0, |L|] L2 . interpretation diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss.ma index ecc2d7443..34221e4c5 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpss.ma @@ -18,8 +18,8 @@ include "basic_2/reducibility/tpr_tpss.ma". (* Properties concerning parallel unfold on local environments **************) -lemma ltpr_ltpss_conf: ∀L1,K1,d,e. L1 [d, e] ▶* K1 → ∀L2. L1 ➡ L2 → - ∃∃K2. L2 [d, e] ▶* K2 & K1 ➡ K2. +lemma ltpr_ltpss_conf: ∀L1,K1,d,e. L1 ▶* [d, e] K1 → ∀L2. L1 ➡ L2 → + ∃∃K2. L2 ▶* [d, e] K2 & K1 ➡ K2. #L1 #K1 #d #e #H elim H -L1 -K1 -d -e [ /2 width=3/ | #L1 #I #V1 #X #H 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 bcf566f26..ac9dc55d8 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 @@ -18,8 +18,8 @@ include "basic_2/reducibility/ltpr_ldrop.ma". (* Properties concerning parallel substitution on terms *********************) -lemma ltpr_tps_trans: ∀L2,T1,T2,d,e. L2 ⊢ T1 [d, e] ▶ T2 → ∀L1. L1 ➡ L2 → - ∃∃T. L1 ⊢ T1 [d, e] ▶ T & T ➡ T2. +lemma ltpr_tps_trans: ∀L2,T1,T2,d,e. L2 ⊢ T1 ▶ [d, e] T2 → ∀L1. L1 ➡ L2 → + ∃∃T. L1 ⊢ T1 ▶ [d, e] T & T ➡ T2. #L2 #T1 #T2 #d #e #H elim H -L2 -T1 -T2 -d -e [ /2 width=3/ | #L2 #K2 #V2 #W2 #i #d #e #Hdi #Hide #HLK2 #HVW2 #L1 #HL12 @@ -36,8 +36,8 @@ lemma ltpr_tps_trans: ∀L2,T1,T2,d,e. L2 ⊢ T1 [d, e] ▶ T2 → ∀L1. L1 ➡ ] 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. +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 diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma index d3e010818..653ed4700 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma @@ -16,14 +16,14 @@ include "basic_2/reducibility/trf.ma". (* CONTEXT-FREE IRREDUCIBLE TERMS *******************************************) -definition tif: predicate term ≝ λT. 𝐑[T] → False. +definition tif: predicate term ≝ λT. 𝐑[T] → ⊥. interpretation "context-free irreducibility (term)" 'NotReducible T = (tif T). (* Basic inversion lemmas ***************************************************) -lemma tif_inv_abbr: ∀V,T. 𝐈[ⓓV.T] → False. +lemma tif_inv_abbr: ∀V,T. 𝐈[ⓓV.T] → ⊥. /2 width=1/ qed-. lemma tif_inv_abst: ∀V,T. 𝐈[ⓛV.T] → 𝐈[V] ∧ 𝐈[T]. @@ -35,7 +35,7 @@ generalize in match HVT; -HVT elim T -T // * // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/ qed-. -lemma tif_inv_cast: ∀V,T. 𝐈[ⓣV.T] → False. +lemma tif_inv_cast: ∀V,T. 𝐈[ⓣV.T] → ⊥. /2 width=1/ qed-. (* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma index a5f2e4407..6f6d99096 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma @@ -42,7 +42,7 @@ lemma tnf_inv_appl: ∀V,T. 𝐍[ⓐV.T] → ∧∧ 𝐍[V] & 𝐍[T] & 𝐒[T]. ] qed-. -lemma tnf_inv_abbr: ∀V,T. 𝐍[ⓓV.T] → False. +lemma tnf_inv_abbr: ∀V,T. 𝐍[ⓓV.T] → ⊥. #V #T #H elim (is_lift_dec T 0 1) [ * #U #HTU lapply (H U ?) -H /2 width=3/ #H destruct @@ -53,7 +53,7 @@ lemma tnf_inv_abbr: ∀V,T. 𝐍[ⓓV.T] → False. ] qed. -lemma tnf_inv_cast: ∀V,T. 𝐍[ⓣV.T] → False. +lemma tnf_inv_cast: ∀V,T. 𝐍[ⓣV.T] → ⊥. #V #T #H lapply (H T ?) -H /2 width=1/ #H -@(discr_tpair_xy_y … H) +@discr_tpair_xy_y // qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma index ef9ecca4c..ecfc2f160 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma @@ -48,10 +48,10 @@ lemma tpr_tif_eq: ∀T1,T2. T1 ➡ T2 → 𝐈[T1] → T1 = T2. qed. theorem tif_tnf: ∀T1. 𝐈[T1] → 𝐍[T1]. -/2 width=1/ qed. +/3 width=1/ qed. (* Note: this property is unusual *) -lemma tnf_trf_false: ∀T1. 𝐑[T1] → 𝐍[T1] → False. +lemma tnf_trf_false: ∀T1. 𝐑[T1] → 𝐍[T1] → ⊥. #T1 #H elim H -T1 [ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2 width=1/ | #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2 width=1/ 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 db2e187c2..3bab61adf 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma @@ -24,7 +24,7 @@ inductive tpr: relation term ≝ | tpr_beta : ∀V1,V2,W,T1,T2. tpr V1 V2 → tpr T1 T2 → tpr (ⓐV1. ⓛW. T1) (ⓓV2. T2) | tpr_delta: ∀I,V1,V2,T1,T2,T. - tpr V1 V2 → tpr T1 T2 → ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T → + tpr V1 V2 → tpr T1 T2 → ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T → tpr (ⓑ{I} V1. T1) (ⓑ{I} V2. T) | tpr_theta: ∀V,V1,V2,W1,W2,T1,T2. tpr V1 V2 → ⇧[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 → @@ -39,8 +39,7 @@ interpretation (* Basic properties *********************************************************) -lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ➡ V2 → T1 ➡ T2 → - ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2. +lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ➡ V2 → T1 ➡ T2 → ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2. /2 width=3/ qed. (* Basic_1: was by definition: pr0_refl *) @@ -69,7 +68,7 @@ lemma tpr_inv_atom1: ∀I,U2. ⓪{I} ➡ U2 → U2 = ⓪{I}. fact tpr_inv_bind1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,T1. U1 = ⓑ{I} V1. T1 → (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 & - ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T & + ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T & U2 = ⓑ{I} V2. T ) ∨ ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr. @@ -86,7 +85,7 @@ qed. lemma tpr_inv_bind1: ∀V1,T1,U2,I. ⓑ{I} V1. T1 ➡ U2 → (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 & - ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T & + ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] T & U2 = ⓑ{I} V2. T ) ∨ ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr. @@ -95,7 +94,7 @@ lemma tpr_inv_bind1: ∀V1,T1,U2,I. ⓑ{I} V1. T1 ➡ U2 → (* Basic_1: was pr0_gen_abbr *) lemma tpr_inv_abbr1: ∀V1,T1,U2. ⓓV1. T1 ➡ U2 → (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 & - ⋆. ⓓV2 ⊢ T2 [0, 1] ▶ T & + ⋆. ⓓV2 ⊢ T2 ▶ [0, 1] T & U2 = ⓓV2. T ) ∨ ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma index fefd6023d..2082ab368 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma @@ -123,8 +123,8 @@ fact tpr_conf_delta_delta: ∃∃X. X1 ➡ X & X2 ➡ X ) → V0 ➡ V1 → V0 ➡ V2 → T0 ➡ T1 → T0 ➡ T2 → - ⋆. ⓑ{I1} V1 ⊢ T1 [O, 1] ▶ TT1 → - ⋆. ⓑ{I1} V2 ⊢ T2 [O, 1] ▶ TT2 → + ⋆. ⓑ{I1} V1 ⊢ T1 ▶ [O, 1] TT1 → + ⋆. ⓑ{I1} V2 ⊢ T2 ▶ [O, 1] TT2 → ∃∃X. ⓑ{I1} V1. TT1 ➡ X & ⓑ{I1} V2. TT2 ➡ X. #I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2 elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2 @@ -141,7 +141,7 @@ fact tpr_conf_delta_zeta: ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → - V0 ➡ V1 → T0 ➡ T1 → ⋆. ⓓV1 ⊢ T1 [O,1] ▶ TT1 → + V0 ➡ V1 → T0 ➡ T1 → ⋆. ⓓV1 ⊢ T1 ▶ [O,1] TT1 → T2 ➡ X2 → ⇧[O, 1] T2 ≡ T0 → ∃∃X. ⓓV1. TT1 ➡ X & X2 ➡ X. #X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HTX2 #HTT20 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 40032ef8a..ebbc21330 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 @@ -21,9 +21,9 @@ include "basic_2/reducibility/ltpr_ldrop.ma". (* Basic_1: was: pr0_subst1 *) lemma tpr_tps_ltpr: ∀T1,T2. T1 ➡ T2 → - ∀L1,d,e,U1. L1 ⊢ T1 [d, e] ▶ U1 → + ∀L1,d,e,U1. L1 ⊢ T1 ▶ [d, e] U1 → ∀L2. L1 ➡ L2 → - ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 [d, e] ▶* U2. + ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2. #T1 #T2 #H elim H -T1 -T2 [ #I #L1 #d #e #X #H elim (tps_inv_atom1 … H) -H @@ -75,15 +75,15 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ➡ T2 → qed. lemma tpr_tps_bind: ∀I,V1,V2,T1,T2,U1. V1 ➡ V2 → T1 ➡ T2 → - ⋆. ⓑ{I} V1 ⊢ T1 [0, 1] ▶ U1 → - ∃∃U2. U1 ➡ U2 & ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ U2. + ⋆. ⓑ{I} V1 ⊢ T1 ▶ [0, 1] U1 → + ∃∃U2. U1 ➡ U2 & ⋆. ⓑ{I} V2 ⊢ T2 ▶ [0, 1] U2. #I #V1 #V2 #T1 #T2 #U1 #HV12 #HT12 #HTU1 elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. ⓑ{I} V2) ?) -T1 /2 width=1/ /3 width=3/ qed. lemma tpr_tpss_ltpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. T1 ➡ T2 → - ∀d,e,U1. L1 ⊢ T1 [d, e] ▶* U1 → - ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 [d, e] ▶* U2. + ∀d,e,U1. L1 ⊢ T1 ▶* [d, e] U1 → + ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2. #L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 @(tpss_ind … HTU1) -U1 [ /2 width=3/ | -HT12 #U #U1 #_ #HU1 * #T #HUT #HT2 @@ -93,6 +93,6 @@ lemma tpr_tpss_ltpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. T1 ➡ T2 → qed. lemma tpr_tpss_conf: ∀T1,T2. T1 ➡ T2 → - ∀L,U1,d,e. L ⊢ T1 [d, e] ▶* U1 → - ∃∃U2. U1 ➡ U2 & L ⊢ T2 [d, e] ▶* U2. + ∀L,U1,d,e. L ⊢ T1 ▶* [d, e] U1 → + ∃∃U2. U1 ➡ U2 & L ⊢ T2 ▶* [d, e] U2. /2 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma index 83306d2de..84b640831 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma @@ -33,7 +33,7 @@ interpretation (* Basic inversion lemmas ***************************************************) -fact trf_inv_atom_aux: ∀I,T. 𝐑[T] → T = ⓪{I} → False. +fact trf_inv_atom_aux: ∀I,T. 𝐑[T] → T = ⓪{I} → ⊥. #I #T * -T [ #V #T #_ #H destruct | #V #T #_ #H destruct @@ -45,7 +45,7 @@ fact trf_inv_atom_aux: ∀I,T. 𝐑[T] → T = ⓪{I} → False. ] qed. -lemma trf_inv_atom: ∀I. 𝐑[⓪{I}] → False. +lemma trf_inv_atom: ∀I. 𝐑[⓪{I}] → ⊥. /2 width=4/ qed-. fact trf_inv_abst_aux: ∀W,U,T. 𝐑[T] → T = ⓛW. U → 𝐑[W] ∨ 𝐑[U]. @@ -64,7 +64,7 @@ lemma trf_inv_abst: ∀V,T. 𝐑[ⓛV.T] → 𝐑[V] ∨ 𝐑[T]. /2 width=3/ qed-. fact trf_inv_appl_aux: ∀W,U,T. 𝐑[T] → T = ⓐW. U → - ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → False). + ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → ⊥). #W #U #T * -T [ #V #T #_ #H destruct | #V #T #_ #H destruct @@ -77,5 +77,5 @@ fact trf_inv_appl_aux: ∀W,U,T. 𝐑[T] → T = ⓐW. U → ] qed. -lemma trf_inv_appl: ∀W,U. 𝐑[ⓐW.U] → ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → False). +lemma trf_inv_appl: ∀W,U. 𝐑[ⓐW.U] → ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → ⊥). /2 width=3/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma index 687893b90..2a5e62f34 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma @@ -53,4 +53,4 @@ lemma tpr_tshf: ∀T1,T2. T1 ➡ T2 → T1 ≈ T1 → T1 ≈ T2. qed. lemma twhnf_tshf: ∀T. T ≈ T → 𝐖𝐇𝐍[T]. -/2 width=1/ qed. +/3 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma index ed624a9df..6ed513c41 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma @@ -21,8 +21,8 @@ include "basic_2/static/aaa_lift.ma". (* Properties about parallel unfold *****************************************) (* Note: lemma 500 *) -lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. L1 [d, e] ▶* L2 → - ∀T2. L2 ⊢ T1 [d, e] ▶* T2 → L2 ⊢ T2 ⁝ A. +lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → L2 ⊢ T2 ⁝ A. #L1 #T1 #A #H elim H -L1 -T1 -A [ #L1 #k #L2 #d #e #_ #T2 #H >(tpss_inv_sort1 … H) -H // @@ -59,18 +59,18 @@ lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. L1 [d, e] ] qed. -lemma aaa_ltpss_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. L1 [d, e] ▶* L2 → - ∀T2. L2 ⊢ T1 [d, e] ▶ T2 → L2 ⊢ T2 ⁝ A. +lemma aaa_ltpss_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → L2 ⊢ T2 ⁝ A. /3 width=7/ qed. lemma aaa_ltpss_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → - ∀L2,d,e. L1 [d, e] ▶* L2 → L2 ⊢ T ⁝ A. + ∀L2,d,e. L1 ▶* [d, e] L2 → L2 ⊢ T ⁝ A. /2 width=7/ qed. lemma aaa_tpss_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → - ∀T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T2 ⁝ A. + ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 → L ⊢ T2 ⁝ A. /2 width=7/ qed. lemma aaa_tps_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → - ∀T2,d,e. L ⊢ T1 [d, e] ▶ T2 → L ⊢ T2 ⁝ A. + ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 → L ⊢ T2 ⁝ A. /2 width=7/ 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 7ac2c8657..9ab903f1e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma @@ -13,8 +13,8 @@ (**************************************************************************) include "basic_2/grammar/cl_weight.ma". -include "basic_2/grammar/lsubs.ma". include "basic_2/substitution/lift.ma". +include "basic_2/substitution/lsubs.ma". (* LOCAL ENVIRONMENT SLICING ************************************************) @@ -150,10 +150,10 @@ lemma ldrop_O1: ∀L,i. i < |L| → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V. ] qed. -lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → +lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → ∀K1,V,i. ⇩[0, i] L1 ≡ K1. ⓓV → d ≤ i → i < d + e → - ∃∃K2. K1 [0, d + e - i - 1] ≼ K2 & + ∃∃K2. K1 ≼ [0, d + e - i - 1] K2 & ⇩[0, i] L2 ≡ K2. ⓓV. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e [ #d #e #K1 #V #i #H diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_sfr.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_sfr.ma new file mode 100644 index 000000000..e9befe700 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_sfr.ma @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/ldrop.ma". + +(* DROPPING *****************************************************************) + +(* Properties about local env. full refinement for substitution *************) + +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. + +(* Inversion lemmas about local env. full refinement for substitution *******) + +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 +[ #K #V #i #H + lapply (ldrop_inv_atom1 … H) -H #H destruct +| #L #J #W #IHL #K #V #i #H + elim (ldrop_inv_O1 … H) -H * + [ -IHL #H1 #H2 #d #e #HL #Hdi #Hide destruct + lapply (le_n_O_to_eq … Hdi) -Hdi #H destruct + lapply (HL … (L.ⓓW) ?) -HL /2 width=1/ #H + elim (lsubs_inv_abbr1 … H ?) -H // -Hide #K #_ #H destruct // + | #Hi #HLK #d @(nat_ind_plus … d) -d + [ #e #H #_ #Hide + elim (sfr_inv_bind … H ?) -H [2: /2 width=2/ ] #HL #H destruct + @(IHL … HLK … HL) -IHL -HLK -HL // /2 width=1/ + | #d #_ #e #H #Hdi #Hide + lapply (sfr_inv_skip … H ?) -H // #HL + @(IHL … HLK … HL) -IHL -HLK -HL /2 width=1/ + ] + ] +] +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 5dfca806a..643da9c05 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma @@ -171,7 +171,7 @@ qed-. (* Basic_1: was: lift_gen_lref_false *) lemma lift_inv_lref2_be: ∀d,e,T1,i. ⇧[d,e] T1 ≡ #i → - d ≤ i → i < d + e → False. + d ≤ i → i < d + e → ⊥. #d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * [ #H1 #_ #H2 #_ | #H2 #_ #_ #H1 ] lapply (le_to_lt_to_lt … H2 H1) -H2 -H1 #H @@ -237,7 +237,7 @@ lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ⇧[d,e] T1 ≡ ⓕ{I} V2. U2 → T1 = ⓕ{I} V1. U1. /2 width=3/ qed-. -lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇧[d, e] ②{I} V. T ≡ V → False. +lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇧[d, e] ②{I} V. T ≡ V → ⊥. #d #e #J #V elim V -V [ * #i #T #H [ lapply (lift_inv_sort2 … H) -H #H destruct @@ -251,7 +251,7 @@ lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇧[d, e] ②{I} V. T ≡ V → False. ] qed-. -lemma lift_inv_pair_xy_y: ∀I,T,V,d,e. ⇧[d, e] ②{I} V. T ≡ T → False. +lemma lift_inv_pair_xy_y: ∀I,T,V,d,e. ⇧[d, e] ②{I} V. T ≡ T → ⊥. #J #T elim T -T [ * #i #V #d #e #H [ lapply (lift_inv_sort2 … H) -H #H destruct diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs.ma new file mode 100644 index 000000000..fb6468c90 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs.ma @@ -0,0 +1,160 @@ +(**************************************************************************) +(* ___ *) +(* ||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". + +(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************) + +inductive lsubs: nat → nat → relation lenv ≝ +| lsubs_sort: ∀d,e. lsubs d e (⋆) (⋆) +| lsubs_OO: ∀L1,L2. lsubs 0 0 L1 L2 +| lsubs_abbr: ∀L1,L2,V,e. lsubs 0 e L1 L2 → + lsubs 0 (e + 1) (L1. ⓓV) (L2.ⓓV) +| lsubs_abst: ∀L1,L2,I,V1,V2,e. lsubs 0 e L1 L2 → + lsubs 0 (e + 1) (L1. ⓛV1) (L2.ⓑ{I} V2) +| lsubs_skip: ∀L1,L2,I1,I2,V1,V2,d,e. + lsubs d e L1 L2 → lsubs (d + 1) e (L1. ⓑ{I1} V1) (L2. ⓑ{I2} V2) +. + +interpretation + "local environment refinement (substitution)" + 'SubEq L1 d e L2 = (lsubs d e L1 L2). + +definition lsubs_conf: ∀S. (lenv → relation S) → Prop ≝ λS,R. + ∀L1,s1,s2. R L1 s1 s2 → + ∀L2,d,e. L1 ≼ [d, e] L2 → R L2 s1 s2. + +(* Basic properties *********************************************************) + +lemma lsubs_bind_eq: ∀L1,L2,e. L1 ≼ [0, e] L2 → ∀I,V. + L1. ⓑ{I} V ≼ [0, e + 1] L2.ⓑ{I} V. +#L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/ +qed. + +lemma lsubs_abbr_lt: ∀L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e → + L1. ⓓV ≼ [0, e] L2.ⓓV. +#L1 #L2 #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/ +qed. + +lemma lsubs_abst_lt: ∀L1,L2,I,V1,V2,e. L1 ≼ [0, e - 1] L2 → 0 < e → + L1. ⓛV1 ≼ [0, e] L2.ⓑ{I} V2. +#L1 #L2 #I #V1 #V2 #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/ +qed. + +lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 ≼ [d - 1, e] L2 → 0 < d → + ∀I1,I2,V1,V2. L1. ⓑ{I1} V1 ≼ [d, e] L2. ⓑ{I2} V2. +#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/ +qed. + +lemma lsubs_bind_lt: ∀I,L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e → + L1. ⓑ{I}V ≼ [0, e] L2.ⓓV. +* /2 width=1/ qed. + +lemma lsubs_refl: ∀d,e,L. L ≼ [d, e] L. +#d elim d -d +[ #e elim e -e // #e #IHe #L elim L -L // /2 width=1/ +| #d #IHd #e #L elim L -L // /2 width=1/ +] +qed. + +lemma TC_lsubs_conf: ∀S,R. lsubs_conf S R → lsubs_conf S (λL. (TC … (R L))). +#S #R #HR #L1 #s1 #s2 #H elim H -s2 +[ /3 width=5/ +| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12 + lapply (HR … Hs2 … HL12) -HR -Hs2 -HL12 /3 width=3/ +] +qed. + +(* Basic inversion lemmas ***************************************************) + +fact lsubs_inv_atom1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L1 = ⋆ → + L2 = ⋆ ∨ (d = 0 ∧ e = 0). +#L1 #L2 #d #e * -L1 -L2 -d -e +[ /2 width=1/ +| /3 width=1/ +| #L1 #L2 #W #e #_ #H destruct +| #L1 #L2 #I #W1 #W2 #e #_ #H destruct +| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct +] +qed. + +lemma lsubs_inv_atom1: ∀L2,d,e. ⋆ ≼ [d, e] L2 → + L2 = ⋆ ∨ (d = 0 ∧ e = 0). +/2 width=3/ qed-. + +fact lsubs_inv_abbr1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → + ∀K1,V. L1 = K1.ⓓV → d = 0 → 0 < e → + ∃∃K2. K1 ≼ [0, e - 1] K2 & L2 = K2.ⓓV. +#L1 #L2 #d #e * -L1 -L2 -d -e +[ #d #e #K1 #V #H destruct +| #L1 #L2 #K1 #V #_ #_ #H + elim (lt_zero_false … H) +| #L1 #L2 #W #e #HL12 #K1 #V #H #_ #_ destruct /2 width=3/ +| #L1 #L2 #I #W1 #W2 #e #_ #K1 #V #H destruct +| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #K1 #V #_ >commutative_plus normalize #H destruct +] +qed. + +lemma lsubs_inv_abbr1: ∀K1,L2,V,e. K1.ⓓV ≼ [0, e] L2 → 0 < e → + ∃∃K2. K1 ≼ [0, e - 1] K2 & L2 = K2.ⓓV. +/2 width=5/ qed-. + +fact lsubs_inv_skip1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → + ∀I1,K1,V1. L1 = K1.ⓑ{I1}V1 → 0 < d → + ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2. +#L1 #L2 #d #e * -L1 -L2 -d -e +[ #d #e #I1 #K1 #V1 #H destruct +| #L1 #L2 #I1 #K1 #V1 #_ #H + elim (lt_zero_false … H) +| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H + elim (lt_zero_false … H) +| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H + elim (lt_zero_false … H) +| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/ +] +qed. + +lemma lsubs_inv_skip1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ≼ [d, e] L2 → 0 < d → + ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2. +/2 width=5/ qed-. + +(* Basic forward lemmas *****************************************************) + +fact lsubs_fwd_length_full1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → + d = 0 → e = |L1| → |L1| ≤ |L2|. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize +[ // +| /2 width=1/ +| /3 width=1/ +| /3 width=1/ +| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct +] +qed. + +lemma lsubs_fwd_length_full1: ∀L1,L2. L1 ≼ [0, |L1|] L2 → |L1| ≤ |L2|. +/2 width=5/ qed-. + +fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → + d = 0 → e = |L2| → |L2| ≤ |L1|. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize +[ // +| /2 width=1/ +| /3 width=1/ +| /3 width=1/ +| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct +] +qed. + +lemma lsubs_fwd_length_full2: ∀L1,L2. L1 ≼ [0, |L2|] L2 → |L2| ≤ |L1|. +/2 width=5/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma new file mode 100644 index 000000000..fb71a175c --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.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/substitution/lsubs.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************) + +(* top element of the refinement *) +definition sfr: nat → nat → predicate lenv ≝ + λd,e. NF … (lsubs d e) (lsubs d e …). + +interpretation + "local environment full refinement (substitution)" + 'SubEqTop d e L = (sfr d e L). + +(* Basic properties *********************************************************) + +lemma sfr_atom: ∀d,e. ≼ [d, e] ⋆. +#d #e #L #H +elim (lsubs_inv_atom1 … H) -H +[ #H destruct // +| * #H1 #H2 destruct // +] +qed. + +lemma sfr_OO: ∀L. ≼ [0, 0] L. +// qed. + +lemma sfr_abbr: ∀L,V,e. ≼ [0, e] L → ≼ [0, e + 1] L.ⓓV. +#L #V #e #HL #K #H +elim (lsubs_inv_abbr1 … H ?) -H // (lift_mono … H1 … H2) -H1 -H2 // @@ -74,11 +74,11 @@ lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶ T2 → ] qed. -lemma tps_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶ T2 → +lemma tps_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 ▶ [dt, et] T2 → ∀L,U1,U2,d,e. ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → dt ≤ d → d ≤ dt + et → - L ⊢ U1 [dt, et + e] ▶ U2. + L ⊢ U1 ▶ [dt, et + e] U2. #K #T1 #T2 #dt #et #H elim H -K -T1 -T2 -dt -et [ #K #I #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_ #_ >(lift_mono … H1 … H2) -H1 -H2 // @@ -107,11 +107,11 @@ lemma tps_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶ T2 → qed. (* Basic_1: was: subst1_lift_ge *) -lemma tps_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶ T2 → +lemma tps_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 ▶ [dt, et] T2 → ∀L,U1,U2,d,e. ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → d ≤ dt → - L ⊢ U1 [dt + e, et] ▶ U2. + L ⊢ U1 ▶ [dt + e, et] U2. #K #T1 #T2 #dt #et #H elim H -K -T1 -T2 -dt -et [ #K #I #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_ >(lift_mono … H1 … H2) -H1 -H2 // @@ -131,10 +131,10 @@ lemma tps_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶ T2 → qed. (* Basic_1: was: subst1_gen_lift_lt *) -lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 → +lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 ▶ [dt, et] U2 → ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → dt + et ≤ d → - ∃∃T2. K ⊢ T1 [dt, et] ▶ T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 ▶ [dt, et] T2 & ⇧[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H elim H -L -U1 -U2 -dt -et [ #L * #i #dt #et #K #d #e #_ #T1 #H #_ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/ @@ -158,10 +158,10 @@ lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 → ] qed. -lemma tps_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 → +lemma tps_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 ▶ [dt, et] U2 → ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → dt ≤ d → d + e ≤ dt + et → - ∃∃T2. K ⊢ T1 [dt, et - e] ▶ T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 ▶ [dt, et - e] T2 & ⇧[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H elim H -L -U1 -U2 -dt -et [ #L * #i #dt #et #K #d #e #_ #T1 #H #_ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/ @@ -196,10 +196,10 @@ lemma tps_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 → qed. (* Basic_1: was: subst1_gen_lift_ge *) -lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 → +lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 ▶ [dt, et] U2 → ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → d + e ≤ dt → - ∃∃T2. K ⊢ T1 [dt - e, et] ▶ T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 ▶ [dt - e, et] T2 & ⇧[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H elim H -L -U1 -U2 -dt -et [ #L * #i #dt #et #K #d #e #_ #T1 #H #_ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/ @@ -230,7 +230,7 @@ qed. (* Basic_1: was: subst1_gen_lift_eq *) lemma tps_inv_lift1_eq: ∀L,U1,U2,d,e. - L ⊢ U1 [d, e] ▶ U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2. + L ⊢ U1 ▶ [d, e] U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2. #L #U1 #U2 #d #e #H elim H -L -U1 -U2 -d -e [ // | #L #K #V #W #i #d #e #Hdi #Hide #_ #_ #T1 #H @@ -262,10 +262,10 @@ qed. (le d i) -> (lt i (plus d h)) -> (EX u1 | t1 = (lift (minus (plus d h) (S i)) (S i) u1)). *) -lemma tps_inv_lift1_ge_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶ U2 → +lemma tps_inv_lift1_ge_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶ [dt, et] U2 → ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → d ≤ dt → dt ≤ d + e → d + e ≤ dt + et → - ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ▶ T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 ▶ [d, dt + et - (d + e)] T2 & ⇧[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet elim (tps_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2 lapply (tps_weak … HU1 d e ? ?) -HU1 // [ >commutative_plus /2 width=1/ ] -Hddt -Hdtde #HU1 @@ -273,19 +273,19 @@ lapply (tps_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct elim (tps_inv_lift1_ge … HU2 … HLK … HTU1 ?) -U -L // commutative_plus /2 width=1/ ] -Hdtd #T #HT1 #HTU diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma index 3155fe64f..98f34529b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma @@ -19,9 +19,9 @@ include "basic_2/substitution/tps_lift.ma". (* Main properties **********************************************************) (* Basic_1: was: subst1_confluence_eq *) -theorem tps_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ▶ T1 → - ∀T2,d2,e2. L ⊢ T0 [d2, e2] ▶ T2 → - ∃∃T. L ⊢ T1 [d2, e2] ▶ T & L ⊢ T2 [d1, e1] ▶ T. +theorem tps_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 ▶ [d1, e1] T1 → + ∀T2,d2,e2. L ⊢ T0 ▶ [d2, e2] T2 → + ∃∃T. L ⊢ T1 ▶ [d2, e2] T & L ⊢ T2 ▶ [d1, e1] T. #L #T0 #T1 #d1 #e1 #H elim H -L -T0 -T1 -d1 -e1 [ /2 width=3/ | #L #K1 #V1 #T1 #i0 #d1 #e1 #Hd1 #Hde1 #HLK1 #HVT1 #T2 #d2 #e2 #H @@ -46,10 +46,10 @@ theorem tps_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ▶ T1 → qed. (* Basic_1: was: subst1_confluence_neq *) -theorem tps_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ▶ T1 → - ∀L2,T2,d2,e2. L2 ⊢ T0 [d2, e2] ▶ T2 → +theorem tps_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 ▶ [d1, e1] T1 → + ∀L2,T2,d2,e2. L2 ⊢ T0 ▶ [d2, e2] T2 → (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) → - ∃∃T. L2 ⊢ T1 [d2, e2] ▶ T & L1 ⊢ T2 [d1, e1] ▶ T. + ∃∃T. L2 ⊢ T1 ▶ [d2, e2] T & L1 ⊢ T2 ▶ [d1, e1] T. #L1 #T0 #T1 #d1 #e1 #H elim H -L1 -T0 -T1 -d1 -e1 [ /2 width=3/ | #L1 #K1 #V1 #T1 #i0 #d1 #e1 #Hd1 #Hde1 #HLK1 #HVT1 #L2 #T2 #d2 #e2 #H1 #H2 @@ -85,9 +85,9 @@ qed. (* Note: the constant 1 comes from tps_subst *) (* Basic_1: was: subst1_trans *) -theorem tps_trans_ge: ∀L,T1,T0,d,e. L ⊢ T1 [d, e] ▶ T0 → - ∀T2. L ⊢ T0 [d, 1] ▶ T2 → 1 ≤ e → - L ⊢ T1 [d, e] ▶ T2. +theorem tps_trans_ge: ∀L,T1,T0,d,e. L ⊢ T1 ▶ [d, e] T0 → + ∀T2. L ⊢ T0 ▶ [d, 1] T2 → 1 ≤ e → + L ⊢ T1 ▶ [d, e] T2. #L #T1 #T0 #d #e #H elim H -L -T1 -T0 -d -e [ #L #I #d #e #T2 #H #He elim (tps_inv_atom1 … H) -H @@ -108,9 +108,9 @@ theorem tps_trans_ge: ∀L,T1,T0,d,e. L ⊢ T1 [d, e] ▶ T0 → ] qed. -theorem tps_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ▶ T0 → - ∀T2,d2,e2. L ⊢ T0 [d2, e2] ▶ T2 → d2 + e2 ≤ d1 → - ∃∃T. L ⊢ T1 [d2, e2] ▶ T & L ⊢ T [d1, e1] ▶ T2. +theorem tps_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 ▶ [d1, e1] T0 → + ∀T2,d2,e2. L ⊢ T0 ▶ [d2, e2] T2 → d2 + e2 ≤ d1 → + ∃∃T. L ⊢ T1 ▶ [d2, e2] T & L ⊢ T ▶ [d1, e1] T2. #L #T1 #T0 #d1 #e1 #H elim H -L -T1 -T0 -d1 -e1 [ /2 width=3/ | #L #K #V #W #i1 #d1 #e1 #Hdi1 #Hide1 #HLK #HVW #T2 #d2 #e2 #HWT2 #Hde2d1 diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma index eb9124089..f0935a041 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma @@ -17,7 +17,7 @@ include "basic_2/unfold/tpss.ma". (* INVERSE BASIC TERM RELOCATION *******************************************) definition delift: nat → nat → lenv → relation term ≝ - λd,e,L,T1,T2. ∃∃T. L ⊢ T1 [d, e] ▶* T & ⇧[d, e] T2 ≡ T. + λd,e,L,T1,T2. ∃∃T. L ⊢ T1 ▶* [d, e] T & ⇧[d, e] T2 ≡ T. interpretation "inverse basic relocation (term)" 'TSubst L T1 d e T2 = (delift d e L T1 T2). @@ -32,7 +32,7 @@ lemma delift_refl_O2: ∀L,T,d. L ⊢ T [d, 0] ≡ T. /2 width=3/ qed. lemma delift_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡ T2 → - ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≡ T2. + ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 [d, e] ≡ T2. #L1 #T1 #T2 #d #e * /3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma index 25d13702a..34b2d2c20 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma @@ -39,7 +39,7 @@ interpretation "inverse basic relocation (term) alternative" (* Basic properties *********************************************************) lemma delifta_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡≡ T2 → - ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≡≡ T2. + ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 [d, e] ≡≡ T2. #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e // /2 width=1/ [ #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma index a6d39c1c9..02efff1fa 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma @@ -20,13 +20,13 @@ include "basic_2/unfold/delift.ma". (* Properties on partial unfold on local environments ***********************) lemma delift_ltpss_conf_eq: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≡ T2 → - ∀K. L [d, e] ▶* K → K ⊢ T1 [d, e] ≡ T2. + ∀K. L ▶* [d, e] K → K ⊢ T1 [d, e] ≡ T2. #L #T1 #T2 #d #e * #T #HT1 #HT2 #K #HLK elim (ltpss_tpss_conf … HT1 … HLK) -L #T0 #HT10 #HT0 lapply (tpss_inv_lift1_eq … HT0 … HT2) -HT0 #H destruct /2 width=3/ qed. -lemma ltpss_delift_trans_eq: ∀L,K,d,e. L [d, e] ▶* K → +lemma ltpss_delift_trans_eq: ∀L,K,d,e. L ▶* [d, e] K → ∀T1,T2. K ⊢ T1 [d, e] ≡ T2 → L ⊢ T1 [d, e] ≡ T2. #L #K #d #e #HLK #T1 #T2 * #T #HT1 #HT2 lapply (ltpss_tpss_trans_eq … HT1 … HLK) -K /2 width=3/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma index 5ba077c6d..c706163a9 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma @@ -19,74 +19,74 @@ include "basic_2/unfold/delift.ma". (* Properties on partial unfold on terms ************************************) -lemma delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 → +lemma delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d + e ≤ dd → - ∃∃T2. K ⊢ T1 [d, e] ▶* T2 & L ⊢ U2 [dd, ee] ≡ T2. + ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ U2 [dd, ee] ≡ T2. #L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1 elim (tpss_inv_lift1_le … HXU1 … HLK … HTX1 ?) -X1 -HLK // -H1 /3 width=5/ qed. -lemma delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 → +lemma delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d + e ≤ dd → - ∃∃T2. K ⊢ T1 [d, e] ▶* T2 & L ⊢ U2 [dd, ee] ≡ T2. + ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ U2 [dd, ee] ≡ T2. /3 width=3/ qed. -lemma delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 → +lemma delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee → - ∃∃T2. K ⊢ T1 [d, dd - d] ▶* T2 & + ∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 & L ⊢ U2 [dd, ee] ≡ T2. #L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 #H2 #H3 elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1 elim (tpss_inv_lift1_le_up … HXU1 … HLK … HTX1 ? ? ?) -X1 -HLK // -H1 -H2 -H3 /3 width=5/ qed. -lemma delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 → +lemma delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee → - ∃∃T2. K ⊢ T1 [d, dd - d] ▶* T2 & + ∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 & L ⊢ U2 [dd, ee] ≡ T2. /3 width=6/ qed. -lemma delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 → +lemma delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e → - ∃∃T2. K ⊢ T1 [d, e - ee] ▶* T2 & + ∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 & L ⊢ U2 [dd, ee] ≡ T2. #L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 #H2 elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1 elim (tpss_inv_lift1_be … HXU1 … HLK … HTX1 ? ?) -X1 -HLK // -H1 -H2 /3 width=5/ qed. -lemma delift_tps_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 → +lemma delift_tps_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e → - ∃∃T2. K ⊢ T1 [d, e - ee] ▶* T2 & + ∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 & L ⊢ U2 [dd, ee] ≡ T2. /3 width=3/ qed. -lemma delift_tpss_conf_eq: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 → +lemma delift_tpss_conf_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → ∀T. L ⊢ U1 [d, e] ≡ T → L ⊢ U2 [d, e] ≡ T. #L #U1 #U2 #d #e #HU12 #T * #X1 #HUX1 #HTX1 elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1 lapply (tpss_inv_lift1_eq … HXU1 … HTX1) -HXU1 #H destruct /2 width=3/ qed. -lemma delift_tps_conf_eq: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 → +lemma delift_tps_conf_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → ∀T. L ⊢ U1 [d, e] ≡ T → L ⊢ U2 [d, e] ≡ T. /3 width=3/ qed. -lemma tpss_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 → +lemma tpss_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → ∀T. L ⊢ U2 [d, e] ≡ T → L ⊢ U1 [d, e] ≡ T. #L #U1 #U2 #d #e #HU12 #T * #X1 #HUX1 #HTX1 lapply (tpss_trans_eq … HU12 … HUX1) -U2 /2 width=3/ qed. -lemma tps_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 → +lemma tps_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → ∀T. L ⊢ U2 [d, e] ≡ T → L ⊢ U1 [d, e] ≡ T. /3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma index 6b44d74f6..169f0e276 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma @@ -21,10 +21,10 @@ inductive ltpss: nat → nat → relation lenv ≝ | ltpss_atom : ∀d,e. ltpss d e (⋆) (⋆) | ltpss_pair : ∀L,I,V. ltpss 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V) | ltpss_tpss2: ∀L1,L2,I,V1,V2,e. - ltpss 0 e L1 L2 → L2 ⊢ V1 [0, e] ▶* V2 → + ltpss 0 e L1 L2 → L2 ⊢ V1 ▶* [0, e] V2 → ltpss 0 (e + 1) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2) | ltpss_tpss1: ∀L1,L2,I,V1,V2,d,e. - ltpss d e L1 L2 → L2 ⊢ V1 [d, e] ▶* V2 → + ltpss d e L1 L2 → L2 ⊢ V1 ▶* [d, e] V2 → ltpss (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2) . @@ -34,47 +34,47 @@ interpretation "parallel unfold (local environment)" (* Basic properties *********************************************************) lemma ltpss_tps2: ∀L1,L2,I,V1,V2,e. - L1 [0, e] ▶* L2 → L2 ⊢ V1 [0, e] ▶ V2 → - L1. ⓑ{I} V1 [0, e + 1] ▶* L2. ⓑ{I} V2. + L1 ▶* [0, e] L2 → L2 ⊢ V1 ▶ [0, e] V2 → + L1. ⓑ{I} V1 ▶* [0, e + 1] L2. ⓑ{I} V2. /3 width=1/ qed. lemma ltpss_tps1: ∀L1,L2,I,V1,V2,d,e. - L1 [d, e] ▶* L2 → L2 ⊢ V1 [d, e] ▶ V2 → - L1. ⓑ{I} V1 [d + 1, e] ▶* L2. ⓑ{I} V2. + L1 ▶* [d, e] L2 → L2 ⊢ V1 ▶ [d, e] V2 → + L1. ⓑ{I} V1 ▶* [d + 1, e] L2. ⓑ{I} V2. /3 width=1/ qed. lemma ltpss_tpss2_lt: ∀L1,L2,I,V1,V2,e. - L1 [0, e - 1] ▶* L2 → L2 ⊢ V1 [0, e - 1] ▶* V2 → - 0 < e → L1. ⓑ{I} V1 [0, e] ▶* L2. ⓑ{I} V2. + L1 ▶* [0, e - 1] L2 → L2 ⊢ V1 ▶* [0, e - 1] V2 → + 0 < e → L1. ⓑ{I} V1 ▶* [0, e] L2. ⓑ{I} V2. #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He >(plus_minus_m_m e 1) /2 width=1/ qed. lemma ltpss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e. - L1 [d - 1, e] ▶* L2 → L2 ⊢ V1 [d - 1, e] ▶* V2 → - 0 < d → L1. ⓑ{I} V1 [d, e] ▶* L2. ⓑ{I} V2. + L1 ▶* [d - 1, e] L2 → L2 ⊢ V1 ▶* [d - 1, e] V2 → + 0 < d → L1. ⓑ{I} V1 ▶* [d, e] L2. ⓑ{I} V2. #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd >(plus_minus_m_m d 1) /2 width=1/ qed. lemma ltpss_tps2_lt: ∀L1,L2,I,V1,V2,e. - L1 [0, e - 1] ▶* L2 → L2 ⊢ V1 [0, e - 1] ▶ V2 → - 0 < e → L1. ⓑ{I} V1 [0, e] ▶* L2. ⓑ{I} V2. + L1 ▶* [0, e - 1] L2 → L2 ⊢ V1 ▶ [0, e - 1] V2 → + 0 < e → L1. ⓑ{I} V1 ▶* [0, e] L2. ⓑ{I} V2. /3 width=1/ qed. lemma ltpss_tps1_lt: ∀L1,L2,I,V1,V2,d,e. - L1 [d - 1, e] ▶* L2 → L2 ⊢ V1 [d - 1, e] ▶ V2 → - 0 < d → L1. ⓑ{I} V1 [d, e] ▶* L2. ⓑ{I} V2. + L1 ▶* [d - 1, e] L2 → L2 ⊢ V1 ▶ [d - 1, e] V2 → + 0 < d → L1. ⓑ{I} V1 ▶* [d, e] L2. ⓑ{I} V2. /3 width=1/ qed. (* Basic_1: was by definition: csubst1_refl *) -lemma ltpss_refl: ∀L,d,e. L [d, e] ▶* L. +lemma ltpss_refl: ∀L,d,e. L ▶* [d, e] L. #L elim L -L // #L #I #V #IHL * /2 width=1/ * /2 width=1/ qed. -lemma ltpss_weak: ∀L1,L2,d1,e1. L1 [d1, e1] ▶* L2 → - ∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 → L1 [d2, e2] ▶* L2. +lemma ltpss_weak: ∀L1,L2,d1,e1. L1 ▶* [d1, e1] L2 → + ∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 → L1 ▶* [d2, e2] L2. #L1 #L2 #d1 #e1 #H elim H -L1 -L2 -d1 -e1 // [ #L1 #L2 #I #V1 #V2 #e1 #_ #HV12 #IHL12 #d2 #e2 #Hd2 #Hde2 lapply (le_n_O_to_eq … Hd2) #H destruct normalize in Hde2; @@ -92,21 +92,21 @@ lemma ltpss_weak: ∀L1,L2,d1,e1. L1 [d1, e1] ▶* L2 → ] qed. -lemma ltpss_weak_all: ∀L1,L2,d,e. L1 [d, e] ▶* L2 → L1 [0, |L2|] ▶* L2. +lemma ltpss_weak_all: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → L1 ▶* [0, |L2|] L2. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e // /3 width=2/ /3 width=3/ qed. (* Basic forward lemmas *****************************************************) -lemma ltpss_fwd_length: ∀L1,L2,d,e. L1 [d, e] ▶* L2 → |L1| = |L2|. +lemma ltpss_fwd_length: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → |L1| = |L2|. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize // qed-. (* Basic inversion lemmas ***************************************************) -fact ltpss_inv_refl_O2_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → e = 0 → L1 = L2. +fact ltpss_inv_refl_O2_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → e = 0 → L1 = L2. #d #e #L1 #L2 #H elim H -d -e -L1 -L2 // [ #L1 #L2 #I #V1 #V2 #e #_ #_ #_ >commutative_plus normalize #H destruct | #L1 #L2 #I #V1 #V2 #d #e #_ #HV12 #IHL12 #He destruct @@ -114,11 +114,11 @@ fact ltpss_inv_refl_O2_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → e = 0 → L1 = L ] qed. -lemma ltpss_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ▶* L2 → L1 = L2. +lemma ltpss_inv_refl_O2: ∀d,L1,L2. L1 ▶* [d, 0] L2 → L1 = L2. /2 width=4/ qed-. fact ltpss_inv_atom1_aux: ∀d,e,L1,L2. - L1 [d, e] ▶* L2 → L1 = ⋆ → L2 = ⋆. + L1 ▶* [d, e] L2 → L1 = ⋆ → L2 = ⋆. #d #e #L1 #L2 * -d -e -L1 -L2 [ // | #L #I #V #H destruct @@ -127,13 +127,13 @@ fact ltpss_inv_atom1_aux: ∀d,e,L1,L2. ] qed. -lemma ltpss_inv_atom1: ∀d,e,L2. ⋆ [d, e] ▶* L2 → L2 = ⋆. +lemma ltpss_inv_atom1: ∀d,e,L2. ⋆ ▶* [d, e] L2 → L2 = ⋆. /2 width=5/ qed-. -fact ltpss_inv_tpss21_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → d = 0 → 0 < e → +fact ltpss_inv_tpss21_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → d = 0 → 0 < e → ∀K1,I,V1. L1 = K1. ⓑ{I} V1 → - ∃∃K2,V2. K1 [0, e - 1] ▶* K2 & - K2 ⊢ V1 [0, e - 1] ▶* V2 & + ∃∃K2,V2. K1 ▶* [0, e - 1] K2 & + K2 ⊢ V1 ▶* [0, e - 1] V2 & L2 = K2. ⓑ{I} V2. #d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #_ #K1 #I #V1 #H destruct @@ -143,15 +143,16 @@ fact ltpss_inv_tpss21_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → d = 0 → 0 < e ] qed. -lemma ltpss_inv_tpss21: ∀e,K1,I,V1,L2. K1. ⓑ{I} V1 [0, e] ▶* L2 → 0 < e → - ∃∃K2,V2. K1 [0, e - 1] ▶* K2 & K2 ⊢ V1 [0, e - 1] ▶* V2 & +lemma ltpss_inv_tpss21: ∀e,K1,I,V1,L2. K1. ⓑ{I} V1 ▶* [0, e] L2 → 0 < e → + ∃∃K2,V2. K1 ▶* [0, e - 1] K2 & + K2 ⊢ V1 ▶* [0, e - 1] V2 & L2 = K2. ⓑ{I} V2. /2 width=5/ qed-. -fact ltpss_inv_tpss11_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → 0 < d → +fact ltpss_inv_tpss11_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → 0 < d → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → - ∃∃K2,V2. K1 [d - 1, e] ▶* K2 & - K2 ⊢ V1 [d - 1, e] ▶* V2 & + ∃∃K2,V2. K1 ▶* [d - 1, e] K2 & + K2 ⊢ V1 ▶* [d - 1, e] V2 & L2 = K2. ⓑ{I} V2. #d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #I #K1 #V1 #H destruct @@ -161,14 +162,14 @@ fact ltpss_inv_tpss11_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → 0 < d → ] qed. -lemma ltpss_inv_tpss11: ∀d,e,I,K1,V1,L2. K1. ⓑ{I} V1 [d, e] ▶* L2 → 0 < d → - ∃∃K2,V2. K1 [d - 1, e] ▶* K2 & - K2 ⊢ V1 [d - 1, e] ▶* V2 & +lemma ltpss_inv_tpss11: ∀d,e,I,K1,V1,L2. K1. ⓑ{I} V1 ▶* [d, e] L2 → 0 < d → + ∃∃K2,V2. K1 ▶* [d - 1, e] K2 & + K2 ⊢ V1 ▶* [d - 1, e] V2 & L2 = K2. ⓑ{I} V2. /2 width=3/ qed-. fact ltpss_inv_atom2_aux: ∀d,e,L1,L2. - L1 [d, e] ▶* L2 → L2 = ⋆ → L1 = ⋆. + L1 ▶* [d, e] L2 → L2 = ⋆ → L1 = ⋆. #d #e #L1 #L2 * -d -e -L1 -L2 [ // | #L #I #V #H destruct @@ -177,13 +178,13 @@ fact ltpss_inv_atom2_aux: ∀d,e,L1,L2. ] qed. -lemma ltpss_inv_atom2: ∀d,e,L1. L1 [d, e] ▶* ⋆ → L1 = ⋆. +lemma ltpss_inv_atom2: ∀d,e,L1. L1 ▶* [d, e] ⋆ → L1 = ⋆. /2 width=5/ qed-. -fact ltpss_inv_tpss22_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → d = 0 → 0 < e → +fact ltpss_inv_tpss22_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → d = 0 → 0 < e → ∀K2,I,V2. L2 = K2. ⓑ{I} V2 → - ∃∃K1,V1. K1 [0, e - 1] ▶* K2 & - K2 ⊢ V1 [0, e - 1] ▶* V2 & + ∃∃K1,V1. K1 ▶* [0, e - 1] K2 & + K2 ⊢ V1 ▶* [0, e - 1] V2 & L1 = K1. ⓑ{I} V1. #d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #_ #K1 #I #V1 #H destruct @@ -193,16 +194,17 @@ fact ltpss_inv_tpss22_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → d = 0 → 0 < e ] qed. -lemma ltpss_inv_tpss22: ∀e,L1,K2,I,V2. L1 [0, e] ▶* K2. ⓑ{I} V2 → 0 < e → - ∃∃K1,V1. K1 [0, e - 1] ▶* K2 & K2 ⊢ V1 [0, e - 1] ▶* V2 & +lemma ltpss_inv_tpss22: ∀e,L1,K2,I,V2. L1 ▶* [0, e] K2. ⓑ{I} V2 → 0 < e → + ∃∃K1,V1. K1 ▶* [0, e - 1] K2 & + K2 ⊢ V1 ▶* [0, e - 1] V2 & L1 = K1. ⓑ{I} V1. /2 width=5/ qed-. -fact ltpss_inv_tpss12_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → 0 < d → +fact ltpss_inv_tpss12_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → 0 < d → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → - ∃∃K1,V1. K1 [d - 1, e] ▶* K2 & - K2 ⊢ V1 [d - 1, e] ▶* V2 & - L1 = K1. ⓑ{I} V1. + ∃∃K1,V1. K1 ▶* [d - 1, e] K2 & + K2 ⊢ V1 ▶* [d - 1, e] V2 & + L1 = K1. ⓑ{I} V1. #d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #I #K2 #V2 #H destruct | #L #I #V #H elim (lt_refl_false … H) @@ -211,9 +213,9 @@ fact ltpss_inv_tpss12_aux: ∀d,e,L1,L2. L1 [d, e] ▶* L2 → 0 < d → ] qed. -lemma ltpss_inv_tpss12: ∀L1,K2,I,V2,d,e. L1 [d, e] ▶* K2. ⓑ{I} V2 → 0 < d → - ∃∃K1,V1. K1 [d - 1, e] ▶* K2 & - K2 ⊢ V1 [d - 1, e] ▶* V2 & +lemma ltpss_inv_tpss12: ∀L1,K2,I,V2,d,e. L1 ▶* [d, e] K2. ⓑ{I} V2 → 0 < d → + ∃∃K1,V1. K1 ▶* [d - 1, e] K2 & + K2 ⊢ V1 ▶* [d - 1, e] V2 & L1 = K1. ⓑ{I} V1. /2 width=3/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ldrop.ma index 4d223834e..8787d594e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ldrop.ma @@ -16,7 +16,7 @@ include "basic_2/unfold/ltpss.ma". (* PARALLEL UNFOLD ON LOCAL ENVIRONMENTS ************************************) -lemma ltpss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 → +lemma ltpss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 → ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2. #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1 @@ -33,7 +33,7 @@ lemma ltpss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 → ] qed. -lemma ltpss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 → +lemma ltpss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 ▶* [d1, e1] L0 → ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2. #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1 @@ -50,9 +50,9 @@ lemma ltpss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 → ] qed. -lemma ltpss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 → +lemma ltpss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 → ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → - ∃∃L. L2 [0, d1 + e1 - e2] ▶* L & ⇩[0, e2] L1 ≡ L. + ∃∃L. L2 ▶* [0, d1 + e1 - e2] L & ⇩[0, e2] L1 ≡ L. #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ | normalize #L #I #V #L2 #e2 #HL2 #_ #He2 @@ -72,9 +72,9 @@ lemma ltpss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 → ] qed. -lemma ltpss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 → +lemma ltpss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 ▶* [d1, e1] L0 → ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → - ∃∃L. L [0, d1 + e1 - e2] ▶* L2 & ⇩[0, e2] L1 ≡ L. + ∃∃L. L ▶* [0, d1 + e1 - e2] L2 & ⇩[0, e2] L1 ≡ L. #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ | normalize #L #I #V #L2 #e2 #HL2 #_ #He2 @@ -94,9 +94,9 @@ lemma ltpss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 → ] qed. -lemma ltpss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 → +lemma ltpss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 → ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 → - ∃∃L. L2 [d1 - e2, e1] ▶* L & ⇩[0, e2] L1 ≡ L. + ∃∃L. L2 ▶* [d1 - e2, e1] L & ⇩[0, e2] L1 ≡ L. #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ | /2 width=3/ @@ -112,9 +112,9 @@ lemma ltpss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 → ] qed. -lemma ltpss_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 → +lemma ltpss_ldrop_trans_le: ∀L1,L0,d1,e1. L1 ▶* [d1, e1] L0 → ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 → - ∃∃L. L [d1 - e2, e1] ▶* L2 & ⇩[0, e2] L1 ≡ L. + ∃∃L. L ▶* [d1 - e2, e1] L2 & ⇩[0, e2] L1 ≡ L. #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/ | /2 width=3/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma index d928491c2..cb8b981c6 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma @@ -20,10 +20,10 @@ include "basic_2/unfold/ltpss_tpss.ma". (* Advanced properties ******************************************************) -lemma ltpss_tpss_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 → - ∀L1,d1,e1. L0 [d1, e1] ▶* L1 → - ∃∃T. L1 ⊢ T2 [d2, e2] ▶* T & - L1 ⊢ U2 [d1, e1] ▶* T. +lemma ltpss_tpss_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 → + ∀L1,d1,e1. L0 ▶* [d1, e1] L1 → + ∃∃T. L1 ⊢ T2 ▶* [d2, e2] T & + L1 ⊢ U2 ▶* [d1, e1] T. #L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 @(tpss_ind … H) -U2 /2 width=3/ #U #U2 #_ #HU2 * #X2 #HTX2 #HUX2 elim (ltpss_tps_conf … HU2 … HL01) -L0 #X1 #HUX1 #HU2X1 @@ -32,8 +32,8 @@ lapply (tpss_trans_eq … HU2X1 … HX1) -X1 /3 width=3/ qed. lemma ltpss_tpss_trans_down: ∀L0,L1,T2,U2,d1,e1,d2,e2. d2 + e2 ≤ d1 → - L1 [d1, e1] ▶* L0 → L0 ⊢ T2 [d2, e2] ▶* U2 → - ∃∃T. L1 ⊢ T2 [d2, e2] ▶* T & L0 ⊢ T [d1, e1] ▶* U2. + L1 ▶* [d1, e1] L0 → L0 ⊢ T2 ▶* [d2, e2] U2 → + ∃∃T. L1 ⊢ T2 ▶* [d2, e2] T & L0 ⊢ T ▶* [d1, e1] U2. #L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde2d1 #HL10 #H @(tpss_ind … H) -U2 [ /2 width=3/ | #U #U2 #_ #HU2 * #T #HT2 #HTU @@ -44,8 +44,8 @@ lemma ltpss_tpss_trans_down: ∀L0,L1,T2,U2,d1,e1,d2,e2. d2 + e2 ≤ d1 → qed. fact ltpss_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e. - L1 ⊢ T2 [d, e] ▶* U2 → ∀L0. L0 [d, e] ▶* L1 → - Y1 = L1 → X2 = T2 → L0 ⊢ T2 [d, e] ▶* U2. + L1 ⊢ T2 ▶* [d, e] U2 → ∀L0. L0 ▶* [d, e] L1 → + Y1 = L1 → X2 = T2 → L0 ⊢ T2 ▶* [d, e] U2. #Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH #L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e [ // @@ -69,19 +69,19 @@ fact ltpss_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e. ] qed. -lemma ltpss_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 [d, e] ▶* U2 → - ∀L0. L0 [d, e] ▶* L1 → L0 ⊢ T2 [d, e] ▶* U2. +lemma ltpss_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 → + ∀L0. L0 ▶* [d, e] L1 → L0 ⊢ T2 ▶* [d, e] U2. /2 width=5/ qed. -lemma ltpss_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 [d, e] ▶* L1 → - L1 ⊢ T2 [d, e] ▶ U2 → L0 ⊢ T2 [d, e] ▶* U2. +lemma ltpss_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 ▶* [d, e] L1 → + L1 ⊢ T2 ▶ [d, e] U2 → L0 ⊢ T2 ▶* [d, e] U2. /3 width=3/ qed. (* Main properties **********************************************************) -fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 [d1, e1] ▶* L1 → - ∀K2,L2,d2,e2. K2 [d2, e2] ▶* L2 → K1 = K → K2 = K → - ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L. +fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 ▶* [d1, e1] L1 → + ∀K2,L2,d2,e2. K2 ▶* [d2, e2] L2 → K1 = K → K2 = K → + ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L. #K @(lw_wf_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1 [ -IH /2 width=3/ | -IH #K1 #I1 #V1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2 @@ -129,7 +129,7 @@ fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 [d1, e1] ▶* L1 → ] qed. -lemma ltpss_conf: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 → - ∀L2,d2,e2. L0 [d2, e2] ▶* L2 → - ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L. +lemma ltpss_conf: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 → + ∀L2,d2,e2. L0 ▶* [d2, e2] L2 → + ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L. /2 width=7/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tps.ma index 9c670a893..df8a73c5a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tps.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tps.ma @@ -18,9 +18,9 @@ include "basic_2/unfold/ltpss_ldrop.ma". (* Properties concerning partial substitution on terms **********************) -lemma ltpss_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 → - ∀L1,d1,e1. L0 [d1, e1] ▶* L1 → d1 + e1 ≤ d2 → - L1 ⊢ T2 [d2, e2] ▶ U2. +lemma ltpss_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 → + ∀L1,d1,e1. L0 ▶* [d1, e1] L1 → d1 + e1 ≤ d2 → + L1 ⊢ T2 ▶ [d2, e2] U2. #L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2 [ // | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01 #Hde1d2 @@ -32,9 +32,9 @@ lemma ltpss_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 → ] qed. -lemma ltpss_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 → - ∀L1,d1,e1. L1 [d1, e1] ▶* L0 → d1 + e1 ≤ d2 → - L1 ⊢ T2 [d2, e2] ▶ U2. +lemma ltpss_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 → + ∀L1,d1,e1. L1 ▶* [d1, e1] L0 → d1 + e1 ≤ d2 → + L1 ⊢ T2 ▶ [d2, e2] U2. #L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2 [ // | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 #Hde1d2 diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma index 0a49ef849..52b52e55d 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma @@ -19,19 +19,19 @@ include "basic_2/unfold/ltpss_tps.ma". (* Properties concerning partial unfold on terms ****************************) -lemma ltpss_tpss_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 → - ∀L1,d1,e1. L0 [d1, e1] ▶* L1 → d1 + e1 ≤ d2 → - L1 ⊢ T2 [d2, e2] ▶* U2. +lemma ltpss_tpss_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 → + ∀L1,d1,e1. L0 ▶* [d1, e1] L1 → d1 + e1 ≤ d2 → + L1 ⊢ T2 ▶* [d2, e2] U2. #L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 // #U #U2 #_ #HU2 #IHU lapply (ltpss_tps_conf_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/ qed. (* Basic_1: was: subst1_subst1_back *) -lemma ltpss_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 → - ∀L1,d1,e1. L0 [d1, e1] ▶* L1 → - ∃∃T. L1 ⊢ T2 [d2, e2] ▶ T & - L1 ⊢ U2 [d1, e1] ▶* T. +lemma ltpss_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 → + ∀L1,d1,e1. L0 ▶* [d1, e1] L1 → + ∃∃T. L1 ⊢ T2 ▶ [d2, e2] T & + L1 ⊢ U2 ▶* [d1, e1] T. #L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2 [ /2 width=3/ | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01 @@ -60,19 +60,19 @@ lemma ltpss_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 → ] qed. -lemma ltpss_tpss_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 → - ∀L1,d1,e1. L1 [d1, e1] ▶* L0 → d1 + e1 ≤ d2 → - L1 ⊢ T2 [d2, e2] ▶* U2. +lemma ltpss_tpss_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 → + ∀L1,d1,e1. L1 ▶* [d1, e1] L0 → d1 + e1 ≤ d2 → + L1 ⊢ T2 ▶* [d2, e2] U2. #L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 // #U #U2 #_ #HU2 #IHU lapply (ltpss_tps_trans_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/ qed. (* Basic_1: was: subst1_subst1 *) -lemma ltpss_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 → - ∀L1,d1,e1. L1 [d1, e1] ▶* L0 → - ∃∃T. L1 ⊢ T2 [d2, e2] ▶ T & - L0 ⊢ T [d1, e1] ▶* U2. +lemma ltpss_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 → + ∀L1,d1,e1. L1 ▶* [d1, e1] L0 → + ∃∃T. L1 ⊢ T2 ▶ [d2, e2] T & + L0 ⊢ T ▶* [d1, e1] U2. #L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2 [ /2 width=3/ | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma index d3eb56c8e..aaead6136 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma @@ -17,7 +17,7 @@ include "basic_2/unfold/ltpss.ma". (* BASIC LOCAL ENVIRONMENT THINNING *****************************************) definition thin: nat → nat → relation lenv ≝ - λd,e,L1,L2. ∃∃L. L1 [d, e] ▶* L & ⇩[d, e] L ≡ L2. + λd,e,L1,L2. ∃∃L. L1 ▶* [d, e] L & ⇩[d, e] L ≡ L2. interpretation "basic thinning (local environment)" 'TSubst L1 d e L2 = (thin d e L1 L2). diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma index 0653266ee..606c77022 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma @@ -41,10 +41,10 @@ lapply (tpss_inv_refl_O2 … H1) -H1 #H destruct lapply (lift_mono … H2 … HV2) -H2 #H destruct /3 width=5/ qed. -lemma thin_delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 → +lemma thin_delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → ∀K. L [dd, ee] ≡ K → d + e ≤ dd → - ∃∃T2. K ⊢ T1 [d, e] ▶* T2 & + ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ U2 [dd, ee] ≡ T2. #L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdedd lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1 @@ -54,18 +54,18 @@ lapply (tpss_delift_trans_eq … HU2 … HUT) -U #HU2T lapply (ltpss_delift_trans_eq … HLY … HU2T) -Y /2 width=3/ qed. -lemma thin_delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 → +lemma thin_delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → ∀K. L [dd, ee] ≡ K → d + e ≤ dd → - ∃∃T2. K ⊢ T1 [d, e] ▶* T2 & + ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ U2 [dd, ee] ≡ T2. /3 width=3/ qed. -lemma thin_delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 → +lemma thin_delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → ∀K. L [dd, ee] ≡ K → d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee → - ∃∃T2. K ⊢ T1 [d, dd - d] ▶* T2 & + ∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 & L ⊢ U2 [dd, ee] ≡ T2. #L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdd #Hdde #Hddee lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1 @@ -75,18 +75,18 @@ lapply (tpss_delift_trans_eq … HU2 … HUT) -U #HU2T lapply (ltpss_delift_trans_eq … HLY … HU2T) -Y /2 width=3/ qed. -lemma thin_delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 → +lemma thin_delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → ∀K. L [dd, ee] ≡ K → d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee → - ∃∃T2. K ⊢ T1 [d, dd - d] ▶* T2 & + ∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 & L ⊢ U2 [dd, ee] ≡ T2. /3 width=6 by thin_delift_tpss_conf_le_up, tpss_strap/ qed. (**) (* too slow without trace *) -lemma thin_delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 → +lemma thin_delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → ∀K. L [dd, ee] ≡ K → d ≤ dd → dd + ee ≤ d + e → - ∃∃T2. K ⊢ T1 [d, e - ee] ▶* T2 & + ∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 & L ⊢ U2 [dd, ee] ≡ T2. #L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdd #Hddee lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1 @@ -96,9 +96,9 @@ lapply (tpss_delift_trans_eq … HU2 … HUT) -U #HU2T lapply (ltpss_delift_trans_eq … HLY … HU2T) -Y /2 width=3/ qed. -lemma thin_delift_tps_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶ U2 → +lemma thin_delift_tps_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → ∀K. L [dd, ee] ≡ K → d ≤ dd → dd + ee ≤ d + e → - ∃∃T2. K ⊢ T1 [d, e - ee] ▶* T2 & + ∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 & L ⊢ U2 [dd, ee] ≡ T2. /3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma index fc74d802c..6405ffeac 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma @@ -25,27 +25,27 @@ interpretation "partial unfold (term)" (* Basic eliminators ********************************************************) lemma tpss_ind: ∀d,e,L,T1. ∀R:predicate term. R T1 → - (∀T,T2. L ⊢ T1 [d, e] ▶* T → L ⊢ T [d, e] ▶ T2 → R T → R T2) → - ∀T2. L ⊢ T1 [d, e] ▶* T2 → R T2. + (∀T,T2. L ⊢ T1 ▶* [d, e] T → L ⊢ T ▶ [d, e] T2 → R T → R T2) → + ∀T2. L ⊢ T1 ▶* [d, e] T2 → R T2. #d #e #L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) // qed-. (* Basic properties *********************************************************) -lemma tpss_strap: ∀L,T1,T,T2,d,e. - L ⊢ T1 [d, e] ▶ T → L ⊢ T [d, e] ▶* T2 → L ⊢ T1 [d, e] ▶* T2. +lemma tpss_strap: ∀L,T1,T,T2,d,e. + L ⊢ T1 ▶ [d, e] T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2. /2 width=3/ qed. -lemma tpss_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶* T2 → - ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ▶* T2. +lemma tpss_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 → + ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 ▶* [d, e] T2. /3 width=3/ qed. -lemma tpss_refl: ∀d,e,L,T. L ⊢ T [d, e] ▶* T. +lemma tpss_refl: ∀d,e,L,T. L ⊢ T ▶* [d, e] T. /2 width=1/ qed. -lemma tpss_bind: ∀L,V1,V2,d,e. L ⊢ V1 [d, e] ▶* V2 → - ∀I,T1,T2. L. ⓑ{I} V2 ⊢ T1 [d + 1, e] ▶* T2 → - L ⊢ ⓑ{I} V1. T1 [d, e] ▶* ⓑ{I} V2. T2. +lemma tpss_bind: ∀L,V1,V2,d,e. L ⊢ V1 ▶* [d, e] V2 → + ∀I,T1,T2. L. ⓑ{I} V2 ⊢ T1 ▶* [d + 1, e] T2 → + L ⊢ ⓑ{I} V1. T1 ▶* [d, e] ⓑ{I} V2. T2. #L #V1 #V2 #d #e #HV12 elim HV12 -V2 [ #V2 #HV12 #I #T1 #T2 #HT12 elim HT12 -T2 [ /3 width=5/ @@ -58,8 +58,8 @@ lemma tpss_bind: ∀L,V1,V2,d,e. L ⊢ V1 [d, e] ▶* V2 → qed. lemma tpss_flat: ∀L,I,V1,V2,T1,T2,d,e. - L ⊢ V1 [d, e] ▶ * V2 → L ⊢ T1 [d, e] ▶* T2 → - L ⊢ ⓕ{I} V1. T1 [d, e] ▶* ⓕ{I} V2. T2. + L ⊢ V1 ▶* [d, e] V2 → L ⊢ T1 ▶* [d, e] T2 → + L ⊢ ⓕ{I} V1. T1 ▶* [d, e] ⓕ{I} V2. T2. #L #I #V1 #V2 #T1 #T2 #d #e #HV12 elim HV12 -V2 [ #V2 #HV12 #HT12 elim HT12 -T2 [ /3 width=1/ @@ -70,9 +70,9 @@ lemma tpss_flat: ∀L,I,V1,V2,T1,T2,d,e. ] qed. -lemma tpss_weak: ∀L,T1,T2,d1,e1. L ⊢ T1 [d1, e1] ▶* T2 → +lemma tpss_weak: ∀L,T1,T2,d1,e1. L ⊢ T1 ▶* [d1, e1] T2 → ∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 → - L ⊢ T1 [d2, e2] ▶* T2. + L ⊢ T1 ▶* [d2, e2] T2. #L #T1 #T2 #d1 #e1 #H #d1 #d2 #Hd21 #Hde12 @(tpss_ind … H) -T2 [ // | #T #T2 #_ #HT12 #IHT @@ -81,7 +81,7 @@ lemma tpss_weak: ∀L,T1,T2,d1,e1. L ⊢ T1 [d1, e1] ▶* T2 → qed. lemma tpss_weak_top: ∀L,T1,T2,d,e. - L ⊢ T1 [d, e] ▶* T2 → L ⊢ T1 [d, |L| - d] ▶* T2. + L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ▶* [d, |L| - d] T2. #L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 [ // | #T #T2 #_ #HT12 #IHT @@ -90,7 +90,7 @@ lemma tpss_weak_top: ∀L,T1,T2,d,e. qed. lemma tpss_weak_all: ∀L,T1,T2,d,e. - L ⊢ T1 [d, e] ▶* T2 → L ⊢ T1 [0, |L|] ▶* T2. + L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ▶* [0, |L|] T2. #L #T1 #T2 #d #e #HT12 lapply (tpss_weak … HT12 0 (d + e) ? ?) -HT12 // #HT12 lapply (tpss_weak_top … HT12) // @@ -99,7 +99,7 @@ qed. (* Basic inversion lemmas ***************************************************) (* Note: this can be derived from tpss_inv_atom1 *) -lemma tpss_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k [d, e] ▶* T2 → T2 = ⋆k. +lemma tpss_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k ▶* [d, e] T2 → T2 = ⋆k. #L #T2 #k #d #e #H @(tpss_ind … H) -T2 [ // | #T #T2 #_ #HT2 #IHT destruct @@ -108,7 +108,7 @@ lemma tpss_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k [d, e] ▶* T2 → T2 = ⋆k. qed-. (* Note: this can be derived from tpss_inv_atom1 *) -lemma tpss_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p [d, e] ▶* T2 → T2 = §p. +lemma tpss_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p ▶* [d, e] T2 → T2 = §p. #L #T2 #p #d #e #H @(tpss_ind … H) -T2 [ // | #T #T2 #_ #HT2 #IHT destruct @@ -116,9 +116,9 @@ lemma tpss_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p [d, e] ▶* T2 → T2 = §p. ] qed-. -lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓑ{I} V1. T1 [d, e] ▶* U2 → - ∃∃V2,T2. L ⊢ V1 [d, e] ▶* V2 & - L. ⓑ{I} V2 ⊢ T1 [d + 1, e] ▶* T2 & +lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓑ{I} V1. T1 ▶* [d, e] U2 → + ∃∃V2,T2. L ⊢ V1 ▶* [d, e] V2 & + L. ⓑ{I} V2 ⊢ T1 ▶* [d + 1, e] T2 & U2 = ⓑ{I} V2. T2. #d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2 [ /2 width=5/ @@ -128,8 +128,8 @@ lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓑ{I} V1. T1 [d, e] ▶* U2 ] qed-. -lemma tpss_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 [d, e] ▶* U2 → - ∃∃V2,T2. L ⊢ V1 [d, e] ▶* V2 & L ⊢ T1 [d, e] ▶* T2 & +lemma tpss_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 ▶* [d, e] U2 → + ∃∃V2,T2. L ⊢ V1 ▶* [d, e] V2 & L ⊢ T1 ▶* [d, e] T2 & U2 = ⓕ{I} V2. T2. #d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2 [ /2 width=5/ @@ -138,7 +138,7 @@ lemma tpss_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 [d, e] ▶* U2 ] qed-. -lemma tpss_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ▶* T2 → T1 = T2. +lemma tpss_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 ▶* [d, 0] T2 → T1 = T2. #L #T1 #T2 #d #H @(tpss_ind … H) -T2 [ // | #T #T2 #_ #HT2 #IHT <(tps_inv_refl_O2 … HT2) -HT2 // @@ -147,7 +147,7 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶* T2 → #[T1] ≤ #[T2]. +lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → #[T1] ≤ #[T2]. #L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 // #T #T2 #_ #HT2 #IHT1 lapply (tps_fwd_tw … HT2) -HT2 #HT2 diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma index 725dc57f1..0a5a5c290 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_alt.ma @@ -35,8 +35,8 @@ interpretation "parallel unfold (term) alternative" (* Basic properties *********************************************************) -lemma tpssa_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶▶* T2 → - ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ▶▶* T2. +lemma tpssa_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶▶* [d, e] T2 → + ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 ▶▶* [d, e] T2. #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e [ // | #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 @@ -46,13 +46,13 @@ lemma tpssa_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶▶* T2 → ] qed. -lemma tpssa_refl: ∀T,L,d,e. L ⊢ T [d, e] ▶▶* T. +lemma tpssa_refl: ∀T,L,d,e. L ⊢ T ▶▶* [d, e] T. #T elim T -T // #I elim I -I /2 width=1/ qed. -lemma tpssa_tps_trans: ∀L,T1,T,d,e. L ⊢ T1 [d, e] ▶▶* T → - ∀T2. L ⊢ T [d, e] ▶ T2 → L ⊢ T1 [d, e] ▶▶* T2. +lemma tpssa_tps_trans: ∀L,T1,T,d,e. L ⊢ T1 ▶▶* [d, e] T → + ∀T2. L ⊢ T ▶ [d, e] T2 → L ⊢ T1 ▶▶* [d, e] T2. #L #T1 #T #d #e #H elim H -L -T1 -T -d -e [ #L #I #d #e #X #H elim (tps_inv_atom1 … H) -H // * /2 width=6/ @@ -71,31 +71,31 @@ lemma tpssa_tps_trans: ∀L,T1,T,d,e. L ⊢ T1 [d, e] ▶▶* T → ] qed. -lemma tpss_tpssa: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T1 [d, e] ▶▶* T2. +lemma tpss_tpssa: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ▶▶* [d, e] T2. #L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 // /2 width=3/ qed. (* Basic inversion lemmas ***************************************************) -lemma tpssa_tpss: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶▶* T2 → L ⊢ T1 [d, e] ▶* T2. +lemma tpssa_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2. #L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=6/ qed-. lemma tpss_ind_alt: ∀R:ℕ→ℕ→lenv→relation term. (∀L,I,d,e. R d e L (⓪{I}) (⓪{I})) → (∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e → - ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 [O, d + e - i - 1] ▶* V2 → + ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 ▶* [O, d + e - i - 1] V2 → ⇧[O, i + 1] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2 ) → - (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ▶* V2 → - L.ⓑ{I}V2 ⊢ T1 [d + 1, e] ▶* T2 → R d e L V1 V2 → + (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 ▶* [d, e] V2 → + L.ⓑ{I}V2 ⊢ T1 ▶* [d + 1, e] T2 → R d e L V1 V2 → R (d+1) e (L.ⓑ{I}V2) T1 T2 → R d e L (ⓑ{I}V1.T1) (ⓑ{I}V2.T2) ) → - (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ▶* V2 → - L⊢ T1 [d, e] ▶* T2 → R d e L V1 V2 → + (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 ▶* [d, e] V2 → + L ⊢ T1 ▶* [d, e] T2 → R d e L V1 V2 → R d e L T1 T2 → R d e L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) ) → - ∀d,e,L,T1,T2. L ⊢ T1 [d, e] ▶* T2 → R d e L T1 T2. + ∀d,e,L,T1,T2. L ⊢ T1 ▶* [d, e] T2 → R d e L T1 T2. #R #H1 #H2 #H3 #H4 #d #e #L #T1 #T2 #H elim (tpss_tpssa … H) -L -T1 -T2 -d -e // /3 width=1 by tpssa_tpss/ /3 width=7 by tpssa_tpss/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma index b52444300..a68f86e32 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma @@ -21,8 +21,8 @@ include "basic_2/unfold/tpss.ma". lemma tpss_subst: ∀L,K,V,U1,i,d,e. d ≤ i → i < d + e → - ⇩[0, i] L ≡ K. ⓓV → K ⊢ V [0, d + e - i - 1] ▶* U1 → - ∀U2. ⇧[0, i + 1] U1 ≡ U2 → L ⊢ #i [d, e] ▶* U2. + ⇩[0, i] L ≡ K. ⓓV → K ⊢ V ▶* [0, d + e - i - 1] U1 → + ∀U2. ⇧[0, i + 1] U1 ≡ U2 → L ⊢ #i ▶* [d, e] U2. #L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(tpss_ind … H) -U1 [ /3 width=4/ | #U #U1 #_ #HU1 #IHU #U2 #HU12 @@ -36,11 +36,11 @@ qed. (* Advanced inverion lemmas *************************************************) -lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ ⓪{I} [d, e] ▶* T2 → +lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ ⓪{I} ▶* [d, e] T2 → T2 = ⓪{I} ∨ ∃∃K,V1,V2,i. d ≤ i & i < d + e & ⇩[O, i] L ≡ K. ⓓV1 & - K ⊢ V1 [0, d + e - i - 1] ▶* V2 & + K ⊢ V1 ▶* [0, d + e - i - 1] V2 & ⇧[O, i + 1] V2 ≡ T2 & I = LRef i. #L #T2 #I #d #e #H @(tpss_ind … H) -T2 @@ -56,25 +56,25 @@ lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ ⓪{I} [d, e] ▶* T2 → ] qed-. -lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ▶* T2 → +lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i ▶* [d, e] T2 → T2 = #i ∨ ∃∃K,V1,V2. d ≤ i & i < d + e & ⇩[O, i] L ≡ K. ⓓV1 & - K ⊢ V1 [0, d + e - i - 1] ▶* V2 & + K ⊢ V1 ▶* [0, d + e - i - 1] V2 & ⇧[O, i + 1] V2 ≡ T2. #L #T2 #i #d #e #H elim (tpss_inv_atom1 … H) -H /2 width=1/ * #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=6/ qed-. -lemma tpss_inv_S2: ∀L,T1,T2,d,e. L ⊢ T1 [d, e + 1] ▶* T2 → - ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 [d + 1, e] ▶* T2. +lemma tpss_inv_S2: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e + 1] T2 → + ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 ▶* [d + 1, e] T2. #L #T1 #T2 #d #e #H #K #V #HLK @(tpss_ind … H) -T2 // #T #T2 #_ #HT2 #IHT lapply (tps_inv_S2 … HT2 … HLK) -HT2 -HLK /2 width=3/ qed-. -lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ▶* T2 → +lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 ▶* [d, 1] T2 → ∀K,V. ⇩[0, d] L ≡ K. ⓛV → T1 = T2. #L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -T2 // #T #T2 #_ #HT2 #IHT <(tps_inv_refl_SO2 … HT2 … HLK) // @@ -82,10 +82,10 @@ qed-. (* Relocation properties ****************************************************) -lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 → +lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 ▶* [dt, et] T2 → ∀L,U1,d,e. dt + et ≤ d → ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → - L ⊢ U1 [dt, et] ▶* U2. + L ⊢ U1 ▶* [dt, et] U2. #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdetd #HLK #HTU1 @(tpss_ind … H) -T2 [ #U2 #H >(lift_mono … HTU1 … H) -H // | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2 @@ -95,10 +95,10 @@ lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 → ] qed. -lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 → +lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 ▶* [dt, et] T2 → ∀L,U1,d,e. dt ≤ d → d ≤ dt + et → ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → - ∀U2. ⇧[d, e] T2 ≡ U2 → L ⊢ U1 [dt, et + e] ▶* U2. + ∀U2. ⇧[d, e] T2 ≡ U2 → L ⊢ U1 ▶* [dt, et + e] U2. #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 @(tpss_ind … H) -T2 [ #U2 #H >(lift_mono … HTU1 … H) -H // | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2 @@ -108,10 +108,10 @@ lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 → ] qed. -lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 → +lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 ▶* [dt, et] T2 → ∀L,U1,d,e. d ≤ dt → ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → - L ⊢ U1 [dt + e, et] ▶* U2. + L ⊢ U1 ▶* [dt + e, et] U2. #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hddt #HLK #HTU1 @(tpss_ind … H) -T2 [ #U2 #H >(lift_mono … HTU1 … H) -H // | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2 @@ -121,10 +121,10 @@ lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 → ] qed. -lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 → +lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 → ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → dt + et ≤ d → - ∃∃T2. K ⊢ T1 [dt, et] ▶* T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 ▶* [dt, et] T2 & ⇧[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(tpss_ind … H) -U2 [ /2 width=3/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU @@ -132,10 +132,10 @@ lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 → ] qed. -lemma tpss_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 → +lemma tpss_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 → ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → dt ≤ d → d + e ≤ dt + et → - ∃∃T2. K ⊢ T1 [dt, et - e] ▶* T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 ▶* [dt, et - e] T2 & ⇧[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(tpss_ind … H) -U2 [ /2 width=3/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU @@ -143,10 +143,10 @@ lemma tpss_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 → ] qed. -lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 → +lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 → ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → d + e ≤ dt → - ∃∃T2. K ⊢ T1 [dt - e, et] ▶* T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 ▶* [dt - e, et] T2 & ⇧[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(tpss_ind … H) -U2 [ /2 width=3/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU @@ -155,16 +155,16 @@ lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 → qed. lemma tpss_inv_lift1_eq: ∀L,U1,U2,d,e. - L ⊢ U1 [d, e] ▶* U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2. + L ⊢ U1 ▶* [d, e] U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2. #L #U1 #U2 #d #e #H #T1 #HTU1 @(tpss_ind … H) -U2 // #U #U2 #_ #HU2 #IHU destruct <(tps_inv_lift1_eq … HU2 … HTU1) -HU2 -HTU1 // qed. -lemma tpss_inv_lift1_ge_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 → +lemma tpss_inv_lift1_ge_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 → ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → d ≤ dt → dt ≤ d + e → d + e ≤ dt + et → - ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ▶* T2 & + ∃∃T2. K ⊢ T1 ▶* [d, dt + et - (d + e)] T2 & ⇧[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(tpss_ind … H) -U2 [ /2 width=3/ @@ -173,10 +173,10 @@ lemma tpss_inv_lift1_ge_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 → ] qed. -lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 → +lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 → ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → dt ≤ d → dt + et ≤ d + e → - ∃∃T2. K ⊢ T1 [dt, d - dt] ▶* T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 ▶* [dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(tpss_ind … H) -U2 [ /2 width=3/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU @@ -184,10 +184,10 @@ lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 → ] qed. -lemma tpss_inv_lift1_le_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 → +lemma tpss_inv_lift1_le_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 → ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → dt ≤ d → d ≤ dt + et → dt + et ≤ d + e → - ∃∃T2. K ⊢ T1 [dt, d - dt] ▶* T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 ▶* [dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(tpss_ind … H) -U2 [ /2 width=3/ | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_tpss.ma index b0d28be56..7ec6dc07b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_tpss.ma @@ -19,36 +19,36 @@ include "basic_2/unfold/tpss_lift.ma". (* Advanced properties ******************************************************) -lemma tpss_tps: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ▶* T2 → L ⊢ T1 [d, 1] ▶ T2. +lemma tpss_tps: ∀L,T1,T2,d. L ⊢ T1 ▶* [d, 1] T2 → L ⊢ T1 ▶ [d, 1] T2. #L #T1 #T2 #d #H @(tpss_ind … H) -T2 // #T #T2 #_ #HT2 #IHT1 lapply (tps_trans_ge … IHT1 … HT2 ?) // qed. -lemma tpss_strip_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ▶* T1 → - ∀T2,d2,e2. L ⊢ T0 [d2, e2] ▶ T2 → - ∃∃T. L ⊢ T1 [d2, e2] ▶ T & L ⊢ T2 [d1, e1] ▶* T. +lemma tpss_strip_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 ▶* [d1, e1] T1 → + ∀T2,d2,e2. L ⊢ T0 ▶ [d2, e2] T2 → + ∃∃T. L ⊢ T1 ▶ [d2, e2] T & L ⊢ T2 ▶* [d1, e1] T. /3 width=3/ qed. -lemma tpss_strip_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ▶* T1 → - ∀L2,T2,d2,e2. L2 ⊢ T0 [d2, e2] ▶ T2 → +lemma tpss_strip_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 ▶* [d1, e1] T1 → + ∀L2,T2,d2,e2. L2 ⊢ T0 ▶ [d2, e2] T2 → (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) → - ∃∃T. L2 ⊢ T1 [d2, e2] ▶ T & L1 ⊢ T2 [d1, e1] ▶* T. + ∃∃T. L2 ⊢ T1 ▶ [d2, e2] T & L1 ⊢ T2 ▶* [d1, e1] T. /3 width=3/ qed. -lemma tpss_strap1_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ▶* T0 → - ∀T2,d2,e2. L ⊢ T0 [d2, e2] ▶ T2 → d2 + e2 ≤ d1 → - ∃∃T. L ⊢ T1 [d2, e2] ▶ T & L ⊢ T [d1, e1] ▶* T2. +lemma tpss_strap1_down: ∀L,T1,T0,d1,e1. L ⊢ T1 ▶* [d1, e1] T0 → + ∀T2,d2,e2. L ⊢ T0 ▶ [d2, e2] T2 → d2 + e2 ≤ d1 → + ∃∃T. L ⊢ T1 ▶ [d2, e2] T & L ⊢ T ▶* [d1, e1] T2. /3 width=3/ qed. -lemma tpss_strap2_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ▶ T0 → - ∀T2,d2,e2. L ⊢ T0 [d2, e2] ▶* T2 → d2 + e2 ≤ d1 → - ∃∃T. L ⊢ T1 [d2, e2] ▶* T & L ⊢ T [d1, e1] ▶ T2. +lemma tpss_strap2_down: ∀L,T1,T0,d1,e1. L ⊢ T1 ▶ [d1, e1] T0 → + ∀T2,d2,e2. L ⊢ T0 ▶* [d2, e2] T2 → d2 + e2 ≤ d1 → + ∃∃T. L ⊢ T1 ▶* [d2, e2] T & L ⊢ T ▶ [d1, e1] T2. /3 width=3/ qed. -lemma tpss_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶* T2 → +lemma tpss_split_up: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → ∀i. d ≤ i → i ≤ d + e → - ∃∃T. L ⊢ T1 [d, i - d] ▶* T & L ⊢ T [i, d + e - i] ▶* T2. + ∃∃T. L ⊢ T1 ▶* [d, i - d] T & L ⊢ T ▶* [i, d + e - i] T2. #L #T1 #T2 #d #e #H #i #Hdi #Hide @(tpss_ind … H) -T2 [ /2 width=3/ | #T #T2 #_ #HT12 * #T3 #HT13 #HT3 @@ -58,10 +58,11 @@ lemma tpss_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶* T2 → ] qed. -lemma tpss_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 → +lemma tpss_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 → ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → d ≤ dt → dt ≤ d + e → d + e ≤ dt + et → - ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ▶* T2 & ⇧[d, e] T2 ≡ U2. + ∃∃T2. K ⊢ T1 ▶* [d, dt + et - (d + e)] T2 & + ⇧[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet elim (tpss_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2 lapply (tpss_weak … HU1 d e ? ?) -HU1 // [ >commutative_plus /2 width=1/ ] -Hddt -Hdtde #HU1 @@ -71,23 +72,23 @@ qed. (* Main properties **********************************************************) -theorem tpss_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ▶* T1 → - ∀T2,d2,e2. L ⊢ T0 [d2, e2] ▶* T2 → - ∃∃T. L ⊢ T1 [d2, e2] ▶* T & L ⊢ T2 [d1, e1] ▶* T. +theorem tpss_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 ▶* [d1, e1] T1 → + ∀T2,d2,e2. L ⊢ T0 ▶* [d2, e2] T2 → + ∃∃T. L ⊢ T1 ▶* [d2, e2] T & L ⊢ T2 ▶* [d1, e1] T. /3 width=3/ qed. -theorem tpss_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ▶* T1 → - ∀L2,T2,d2,e2. L2 ⊢ T0 [d2, e2] ▶* T2 → +theorem tpss_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 ▶* [d1, e1] T1 → + ∀L2,T2,d2,e2. L2 ⊢ T0 ▶* [d2, e2] T2 → (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) → - ∃∃T. L2 ⊢ T1 [d2, e2] ▶* T & L1 ⊢ T2 [d1, e1] ▶* T. + ∃∃T. L2 ⊢ T1 ▶* [d2, e2] T & L1 ⊢ T2 ▶* [d1, e1] T. /3 width=3/ qed. theorem tpss_trans_eq: ∀L,T1,T,T2,d,e. - L ⊢ T1 [d, e] ▶* T → L ⊢ T [d, e] ▶* T2 → - L ⊢ T1 [d, e] ▶* T2. + L ⊢ T1 ▶* [d, e] T → L ⊢ T ▶* [d, e] T2 → + L ⊢ T1 ▶* [d, e] T2. /2 width=3/ qed. -theorem tpss_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ▶* T0 → - ∀T2,d2,e2. L ⊢ T0 [d2, e2] ▶* T2 → d2 + e2 ≤ d1 → - ∃∃T. L ⊢ T1 [d2, e2] ▶* T & L ⊢ T [d1, e1] ▶* T2. +theorem tpss_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 ▶* [d1, e1] T0 → + ∀T2,d2,e2. L ⊢ T0 ▶* [d2, e2] T2 → d2 + e2 ≤ d1 → + ∃∃T. L ⊢ T1 ▶* [d2, e2] T & L ⊢ T ▶* [d1, e1] T2. /3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/ground_2/arith.ma b/matita/matita/contribs/lambda_delta/ground_2/arith.ma index 0bdcd748f..c65a47bcc 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/arith.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/arith.ma @@ -53,15 +53,15 @@ lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m. #m #Hm * #H /2 width=1/ /3 width=1/ qed-. -lemma lt_refl_false: ∀n. n < n → False. +lemma lt_refl_false: ∀n. n < n → ⊥. #n #H elim (lt_to_not_eq … H) -H /2 width=1/ qed-. -lemma lt_zero_false: ∀n. n < 0 → False. +lemma lt_zero_false: ∀n. n < 0 → ⊥. #n #H elim (lt_to_not_le … H) -H /2 width=1/ qed-. -lemma false_lt_to_le: ∀x,y. (x < y → False) → y ≤ x. +lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x. #x #y #H elim (decidable_lt x y) /2 width=1/ #Hxy elim (H Hxy) qed-. diff --git a/matita/matita/contribs/lambda_delta/ground_2/list.ma b/matita/matita/contribs/lambda_delta/ground_2/list.ma index 0d15cfe4f..9a5ac0aeb 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/list.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/list.ma @@ -26,7 +26,7 @@ interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl). let rec all A (R:predicate A) (l:list A) on l ≝ match l with - [ nil ⇒ True + [ nil ⇒ ⊤ | cons hd tl ⇒ R hd ∧ all A R tl ]. diff --git a/matita/matita/contribs/lambda_delta/ground_2/notation.ma b/matita/matita/contribs/lambda_delta/ground_2/notation.ma index 574bd3c59..4ac2e6e64 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/notation.ma @@ -14,9 +14,19 @@ (* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) +(* Logic ********************************************************************) + +notation "⊥" + non associative with precedence 90 + for @{'false}. + +notation "⊤" + non associative with precedence 90 + for @{'true}. + (* Lists ********************************************************************) -notation "hvbox( ◊ )" +notation "◊" non associative with precedence 90 for @{'Nil}. @@ -28,7 +38,7 @@ notation "hvbox( l1 @@ break l2 )" right associative with precedence 47 for @{'Append $l1 $l2 }. -notation "hvbox( ⟠ )" +notation "⟠" non associative with precedence 90 for @{'Nil2}. diff --git a/matita/matita/contribs/lambda_delta/ground_2/star.ma b/matita/matita/contribs/lambda_delta/ground_2/star.ma index c183111dd..c951ddac0 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/star.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/star.ma @@ -18,7 +18,7 @@ include "ground_2/notation.ma". (* PROPERTIES OF RELATIONS **************************************************) -definition Decidable: Prop → Prop ≝ λR. R ∨ (R → False). +definition Decidable: Prop → Prop ≝ λR. R ∨ (R → ⊥). definition confluent2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2. ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 → @@ -99,10 +99,10 @@ lemma TC_transitive2: ∀A,R1,R2. qed. definition NF: ∀A. relation A → relation A → predicate A ≝ - λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2. + λA,R,S,a1. ∀a2. R a1 a2 → S a2 a1. inductive SN (A) (R,S:relation A): predicate A ≝ -| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → False) → SN A R S a2) → SN A R S a1 +| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a2 a1 → ⊥) → SN A R S a2) → SN A R S a1 . lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a. diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa_props.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa_props.ma index e212a60e5..71216d1c4 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/xoa_props.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/xoa_props.ma @@ -12,9 +12,14 @@ (* *) (**************************************************************************) +include "basics/logic.ma". include "ground_2/xoa_notation.ma". include "ground_2/xoa.ma". +interpretation "logical false" 'false = False. + +interpretation "logical true" 'true = True. + lemma ex2_1_comm: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0. #A0 #P0 #P1 * /2 width=3/ qed.