From: Ferruccio Guidi Date: Sun, 7 Apr 2013 21:36:03 +0000 (+0000) Subject: - new component for restricted computation (delta, zeta and tau only) X-Git-Tag: make_still_working~1200 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6d3e67a714d59ff5d0da7aff72323a6d2ac07db4;p=helm.git - new component for restricted computation (delta, zeta and tau only) - subclosure preseves native validity asexpected - some renaming --- diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl index 556df99a7..627c05d6e 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl @@ -9,7 +9,7 @@ table { ] } ] - class "orange" + class "yellow" [ { "MLTT1" * } { [ { "" * } { [ "genv_primitive" "judgement" * ] @@ -17,7 +17,7 @@ table { ] } ] - class "red" + class "orange" [ { "functional" * } { [ { "reduction and type machine" * } { [ "rtm" "rtm_step ( ? ⇨ ? )" * ] @@ -28,6 +28,14 @@ table { } ] } + ] + class "red" + [ { "examples" * } { + [ { "" * } { + [ "" * ] + } + ] + } ] } diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma index 854fff7f3..e40d8a282 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma @@ -77,3 +77,20 @@ lemma snv_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊢ U ¡[g] → ∀K,d,e. ⇩[d, e] L lapply (cpcs_inv_lift … HLK … HVW … HVW0 ?) // -W /3 width=4/ ] qed-. + +(* Advanced properties ******************************************************) + +lemma snv_fsup_conf: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → + ⦃h, L1⦄ ⊢ T1 ¡[g] → ⦃h, L2⦄ ⊢ T2 ¡[g]. +#h #g #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 +[ #I1 #L1 #V1 #H + elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2 + lapply (ldrop_inv_refl … H) -H #H destruct // +|2,3: #a #I #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H // +|4,5: * #L1 #V1 #T1 #H + [1,3: elim (snv_inv_appl … H) -H // + |2,4: elim (snv_inv_cast … H) -H // + ] +| /3 width=7 by snv_inv_lift/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma index c7d7ac9ca..0e8ec22fa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma @@ -23,6 +23,9 @@ let rec append L K on K ≝ match K with interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2). +definition l_appendable_sn: predicate (lenv→relation term) ≝ λR. + ∀K,T1,T2. R K T1 T2 → ∀L. R (L @@ K) T1 T2. + (* Basic properties *********************************************************) lemma append_atom_sn: ∀L. ⋆ @@ L = L. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma new file mode 100644 index 000000000..e3f661cfc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma @@ -0,0 +1,117 @@ +(**************************************************************************) +(* ___ *) +(* ||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_append.ma". + +(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) + +inductive lpx_sn (R:lenv→relation term): relation lenv ≝ +| lpx_sn_stom: lpx_sn R (⋆) (⋆) +| lpx_sn_pair: ∀I,K1,K2,V1,V2. + lpx_sn R K1 K2 → R K1 V1 V2 → + lpx_sn R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) +. + +definition lpx_sn_confluent: predicate (lenv→relation term) ≝ λR. + ∀L0,T0,T1. R L0 T0 T1 → ∀T2. R L0 T0 T2 → + ∀L1. lpx_sn R L0 L1 → ∀L2. lpx_sn R L0 L2 → + ∃∃T. R L1 T1 T & R L2 T2 T. + +definition lpx_sn_transitive: predicate (lenv→relation term) ≝ λR. + ∀L1,T1,T. R L1 T1 T → ∀L2. lpx_sn R L1 L2 → + ∀T2. R L2 T T2 → R L1 T1 T2. + + +(* Basic inversion lemmas ***************************************************) + +fact lpx_sn_inv_atom1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L1 = ⋆ → L2 = ⋆. +#R #L1 #L2 * -L1 -L2 +[ // +| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct +] +qed-. + +lemma lpx_sn_inv_atom1: ∀R,L2. lpx_sn R (⋆) L2 → L2 = ⋆. +/2 width=4 by lpx_sn_inv_atom1_aux/ qed-. + +fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → + ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +#R #L1 #L2 * -L1 -L2 +[ #J #K1 #V1 #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/ +] +qed-. + +lemma lpx_sn_inv_pair1: ∀R,I,K1,V1,L2. lpx_sn R (K1. ⓑ{I} V1) L2 → + ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +/2 width=3 by lpx_sn_inv_pair1_aux/ qed-. + +fact lpx_sn_inv_atom2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L2 = ⋆ → L1 = ⋆. +#R #L1 #L2 * -L1 -L2 +[ // +| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct +] +qed-. + +lemma lpx_sn_inv_atom2: ∀R,L1. lpx_sn R L1 (⋆) → L1 = ⋆. +/2 width=4 by lpx_sn_inv_atom2_aux/ qed-. + +fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → + ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. +#R #L1 #L2 * -L1 -L2 +[ #J #K2 #V2 #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/ +] +qed-. + +lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2. ⓑ{I} V2) → + ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. +/2 width=3 by lpx_sn_inv_pair2_aux/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lpx_sn_fwd_length: ∀R,L1,L2. lpx_sn R L1 L2 → |L1| = |L2|. +#R #L1 #L2 #H elim H -L1 -L2 normalize // +qed-. + +(* Basic properties *********************************************************) + +lemma lpx_sn_refl: ∀R. (∀L. reflexive ? (R L)) → reflexive … (lpx_sn R). +#R #HR #L elim L -L // /2 width=1/ +qed-. + +lemma lpx_sn_append: ∀R. l_appendable_sn R → + ∀K1,K2. lpx_sn R K1 K2 → ∀L1,L2. lpx_sn R L1 L2 → + lpx_sn R (L1 @@ K1) (L2 @@ K2). +#R #HR #K1 #K2 #H elim H -K1 -K2 // /3 width=1/ +qed-. + +lemma lpx_sn_trans: ∀R. lpx_sn_transitive R → Transitive … (lpx_sn R). +#R #HR #L1 #L #H elim H -L1 -L // +#I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H +elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct /3 width=5/ +qed-. + +lemma lpx_sn_conf: ∀R. lpx_sn_confluent R → confluent … (lpx_sn R). +#R #HR #L0 @(f_ind … length … L0) -L0 #n #IH * +[ #_ #X1 #H1 #X2 #H2 -n + >(lpx_sn_inv_atom1 … H1) -X1 + >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3/ +| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct + elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct + elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct + elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2 + elim (HR … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index 6c34328b4..1e1fc78cc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -46,3 +46,31 @@ d: abbreviation f: flat l: abstraction n: native type annotation + +NAMING CONVENTIONS FOR TRANSFORMATIONS + +- first letter + +f: context-freee for closures +l: sn contex-sensitive for terms +r: dx contex-sensitive for terms +t: context-free for terms + +-second letter + +p: parallel +s: sequential + +- third letter + +c: conversion +d: decomposed extended reduction +q: restricted reduction +r: reduction +s: substitution +x: extended reduction + +- forth letter (if present) + +p: non-reflexive transitive closure +s: reflexive transitive closure diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma index 9c9c19209..5e730aec2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma @@ -252,6 +252,16 @@ notation "hvbox( L1 ⊢ ⧫ * break term 46 T ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'Unwind $L1 $T $L2 }. +(* Restricted ***************************************************************) + +notation "hvbox( L ⊢ break term 46 T1 ➤ * break term 46 T2 )" + non associative with precedence 45 + for @{ 'PRestStar $L $T1 $T2 }. + +notation "hvbox( T1 ⊢ ➤ * break term 46 T2 )" + non associative with precedence 45 + for @{ 'PRestStarSn $T1 $T2 }. + (* Reducibility *************************************************************) notation "hvbox( L ⊢ break 𝐑 ⦃ term 46 T ⦄ )" diff --git a/matita/matita/contribs/lambdadelta/basic_2/restricted/cpqs.ma b/matita/matita/contribs/lambdadelta/basic_2/restricted/cpqs.ma new file mode 100644 index 000000000..9d5983292 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/restricted/cpqs.ma @@ -0,0 +1,229 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/cpss.ma". + +(* CONTEXT-SENSITIVE RESTRICTED PARALLEL COMPUTATION FOR TERMS **************) + +inductive cpqs: lenv → relation term ≝ +| cpqs_atom : ∀I,L. cpqs L (⓪{I}) (⓪{I}) +| cpqs_delta: ∀L,K,V,V2,W2,i. + ⇩[0, i] L ≡ K. ⓓV → cpqs K V V2 → + ⇧[0, i + 1] V2 ≡ W2 → cpqs L (#i) W2 +| cpqs_bind : ∀a,I,L,V1,V2,T1,T2. + cpqs L V1 V2 → cpqs (L. ⓑ{I} V1) T1 T2 → + cpqs L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2) +| cpqs_flat : ∀I,L,V1,V2,T1,T2. + cpqs L V1 V2 → cpqs L T1 T2 → + cpqs L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2) +| cpqs_zeta : ∀L,V,T1,T,T2. cpqs (L.ⓓV) T1 T → + ⇧[0, 1] T2 ≡ T → cpqs L (+ⓓV. T1) T2 +| cpqs_tau : ∀L,V,T1,T2. cpqs L T1 T2 → cpqs L (ⓝV. T1) T2 +. + +interpretation "context-sensitive restricted parallel computation (term)" + 'PRestStar L T1 T2 = (cpqs L T1 T2). + +(* Basic properties *********************************************************) + +(* Note: it does not hold replacing |L1| with |L2| *) +lemma cpqs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➤* T2 → + ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ➤* T2. +#L1 #T1 #T2 #H elim H -L1 -T1 -T2 +[ // +| #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 + lapply (ldrop_fwd_ldrop2_length … HLK1) #Hi + lapply (ldrop_fwd_O1_length … HLK1) #H2i + elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // -Hi + shift_append_assoc normalize #H + elim (cpqs_inv_bind1 … H) -H * + [ #V0 #T0 #_ #HT10 #H destruct + elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct + >append_length >HL12 -HL12 + @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *) + | #T #_ #_ #H destruct + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/restricted/cpqs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/restricted/cpqs_lift.ma new file mode 100644 index 000000000..abdd99d8f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/restricted/cpqs_lift.ma @@ -0,0 +1,81 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/ldrop_ldrop.ma". +include "basic_2/restricted/cpqs.ma". + +(* CONTEXT-SENSITIVE RESTRICTED PARALLEL COMPUTATION FOR TERMS **************) + +(* Relocation properties ****************************************************) + +lemma cpqs_lift: l_liftable cpqs. +#K #T1 #T2 #H elim H -K -T1 -T2 +[ #I #K #L #d #e #_ #U1 #H1 #U2 #H2 + >(lift_mono … H1 … H2) -H1 -H2 // +| #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2 + elim (lift_inv_lref1 … H) * #Hid #H destruct + [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // plus_plus_comm_23 #HVU2 + lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=6/ + ] +| #a #I #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 + elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct + elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5/ +| #I #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 + elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct + elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/ +| #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #H #U2 #HTU2 + elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct + elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=5/ +| #K #V #T1 #T2 #_ #IHT12 #L #d #e #HLK #U1 #H #U2 #HTU2 + elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5/ +] +qed. + +lemma cpqs_inv_lift1: l_deliftable_sn cpqs. +#L #U1 #U2 #H elim H -L -U1 -U2 +[ * #L #i #K #d #e #_ #T1 #H + [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/ + | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/ + | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/ + ] +| #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H + elim (lift_inv_lref2 … H) -H * #Hid #H destruct + [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV + elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2 + elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus plus_minus // shift_append_assoc #H (lpx_sn_inv_atom1 … H) -H /2 width=3/ +| #K1 #I #V1 #X #H + elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/ +| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H + elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct + elim (IHLK1 … HL12) -L1 /3 width=3/ +| #L1 #K1 #I #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H + elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct + elim (HR … HV12 … HLK1 … HWV1) -V1 + elim (IHLK1 … HL12) -L1 /3 width=5/ +] +qed-. + +lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) → + l_liftable R → dedropable_sn (lpx_sn R). +#R #H1R #H2R #L1 #K1 #d #e #H elim H -L1 -K1 -d -e +[ #d #e #X #H >(lpx_sn_inv_atom1 … H) -H /2 width=3/ +| #K1 #I #V1 #X #H + elim (lpx_sn_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/ +| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12 + elim (IHLK1 … HK12) -K1 /3 width=5/ +| #L1 #K1 #I #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H + elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct + elim (lift_total W2 d e) #V2 #HWV2 + lapply (H2R … HW12 … HLK1 … HWV1 … HWV2) -W1 + elim (IHLK1 … HK12) -K1 /3 width=5/ +] +qed-. + +fact lpx_sn_dropable_aux: ∀R,L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 → + d = 0 → ∃∃K1. ⇩[0, e] L1 ≡ K1 & lpx_sn R K1 K2. +#R #L2 #K2 #d #e #H elim H -L2 -K2 -d -e +[ #d #e #X #H >(lpx_sn_inv_atom2 … H) -H /2 width=3/ +| #K2 #I #V2 #X #H + elim (lpx_sn_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/ +| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_ + elim (lpx_sn_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct + elim (IHLK2 … HL12 ?) -L2 // /3 width=3/ +| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_ + >commutative_plus normalize #H destruct +] +qed-. + +lemma lpx_sn_dropable: ∀R. dropable_dx (lpx_sn R). +/2 width=5 by lpx_sn_dropable_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss.ma index fa8f4fb4e..4bbf47bdf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss.ma @@ -17,14 +17,14 @@ include "basic_2/substitution/ldrop_append.ma". (* CONTEXT-SENSITIVE PARALLEL UNFOLD FOR TERMS ******************************) inductive cpss: lenv → relation term ≝ -| cpss_atom : ∀L,I. cpss L (⓪{I}) (⓪{I}) -| cpss_subst: ∀L,K,V,V2,W2,i. +| cpss_atom : ∀I,L. cpss L (⓪{I}) (⓪{I}) +| cpss_delta: ∀L,K,V,V2,W2,i. ⇩[0, i] L ≡ K. ⓓV → cpss K V V2 → ⇧[0, i + 1] V2 ≡ W2 → cpss L (#i) W2 -| cpss_bind : ∀L,a,I,V1,V2,T1,T2. +| cpss_bind : ∀a,I,L,V1,V2,T1,T2. cpss L V1 V2 → cpss (L. ⓑ{I} V1) T1 T2 → cpss L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2) -| cpss_flat : ∀L,I,V1,V2,T1,T2. +| cpss_flat : ∀I,L,V1,V2,T1,T2. cpss L V1 V2 → cpss L T1 T2 → cpss L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2) . @@ -49,11 +49,13 @@ lemma cpss_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ▶* T2 → ] qed-. +(* Basic_1: was by definition: subst1_refl *) lemma cpss_refl: ∀T,L. L ⊢ T ▶* T. #T elim T -T // #I elim I -I /2 width=1/ qed. +(* Basic_1: was only: subst1_ex *) lemma cpss_delift: ∀K,V,T1,L,d. ⇩[0, d] L ≡ (K. ⓓV) → ∃∃T2,T. L ⊢ T1 ▶* T2 & ⇧[d, 1] T ≡ T2. #K #V #T1 elim T1 -T1 @@ -70,11 +72,11 @@ lemma cpss_delift: ∀K,V,T1,L,d. ⇩[0, d] L ≡ (K. ⓓV) → ] qed-. -lemma cpss_append: ∀K,T1,T2. K ⊢ T1 ▶* T2 → ∀L. L @@ K ⊢ T1 ▶* T2. +lemma cpss_append: l_appendable_sn … cpss. #K #T1 #T2 #H elim H -K -T1 -T2 // /2 width=1/ #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L lapply (ldrop_fwd_ldrop2_length … HK0) #H -@(cpss_subst … (L@@K0) V1 … HVW2) // +@(cpss_delta … (L@@K0) V1 … HVW2) // @(ldrop_O1_append_sn_le … HK0) /2 width=2/ (**) (* /3/ does not work *) qed. @@ -87,14 +89,14 @@ fact cpss_inv_atom1_aux: ∀L,T1,T2. L ⊢ T1 ▶* T2 → ∀I. T1 = ⓪{I} → ⇧[O, i + 1] V2 ≡ T2 & I = LRef i. #L #T1 #T2 * -L -T1 -T2 -[ #L #I #J #H destruct /2 width=1/ +[ #I #L #J #H destruct /2 width=1/ | #L #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #I #H destruct /3 width=8/ -| #L #a #I #V1 #V2 #T1 #T2 #_ #_ #J #H destruct -| #L #I #V1 #V2 #T1 #T2 #_ #_ #J #H destruct +| #a #I #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct +| #I #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct ] qed-. -lemma cpss_inv_atom1: ∀L,T2,I. L ⊢ ⓪{I} ▶* T2 → +lemma cpss_inv_atom1: ∀I,L,T2. L ⊢ ⓪{I} ▶* T2 → T2 = ⓪{I} ∨ ∃∃K,V,V2,i. ⇩[O, i] L ≡ K. ⓓV & K ⊢ V ▶* V2 & @@ -102,12 +104,14 @@ lemma cpss_inv_atom1: ∀L,T2,I. L ⊢ ⓪{I} ▶* T2 → I = LRef i. /2 width=3 by cpss_inv_atom1_aux/ qed-. +(* Basic_1: was only: subst1_gen_sort *) lemma cpss_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ▶* T2 → T2 = ⋆k. #L #T2 #k #H elim (cpss_inv_atom1 … H) -H // * #K #V #V2 #i #_ #_ #_ #H destruct qed-. +(* Basic_1: was only: subst1_gen_lref *) lemma cpss_inv_lref1: ∀L,T2,i. L ⊢ #i ▶* T2 → T2 = #i ∨ ∃∃K,V,V2. ⇩[O, i] L ≡ K. ⓓV & @@ -130,14 +134,14 @@ fact cpss_inv_bind1_aux: ∀L,U1,U2. L ⊢ U1 ▶* U2 → L. ⓑ{I} V1 ⊢ T1 ▶* T2 & U2 = ⓑ{a,I} V2. T2. #L #U1 #U2 * -L -U1 -U2 -[ #L #k #a #I #V1 #T1 #H destruct -| #L #K #V #V2 #W2 #i #_ #_ #_ #a #I #V1 #T1 #H destruct -| #L #b #J #V1 #V2 #T1 #T2 #HV12 #HT12 #a #I #V #T #H destruct /2 width=5/ -| #L #J #V1 #V2 #T1 #T2 #_ #_ #a #I #V #T #H destruct +[ #I #L #b #J #W1 #U1 #H destruct +| #L #K #V #V2 #W2 #i #_ #_ #_ #b #J #W1 #U1 #H destruct +| #a #I #L #V1 #V2 #T1 #T2 #HV12 #HT12 #b #J #W1 #U1 #H destruct /2 width=5/ +| #I #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W1 #U1 #H destruct ] qed-. -lemma cpss_inv_bind1: ∀L,a,I,V1,T1,U2. L ⊢ ⓑ{a,I} V1. T1 ▶* U2 → +lemma cpss_inv_bind1: ∀a,I,L,V1,T1,U2. L ⊢ ⓑ{a,I} V1. T1 ▶* U2 → ∃∃V2,T2. L ⊢ V1 ▶* V2 & L. ⓑ{I} V1 ⊢ T1 ▶* T2 & U2 = ⓑ{a,I} V2. T2. @@ -148,14 +152,14 @@ fact cpss_inv_flat1_aux: ∀L,U1,U2. L ⊢ U1 ▶* U2 → ∃∃V2,T2. L ⊢ V1 ▶* V2 & L ⊢ T1 ▶* T2 & U2 = ⓕ{I} V2. T2. #L #U1 #U2 * -L -U1 -U2 -[ #L #k #I #V1 #T1 #H destruct -| #L #K #V #V2 #W2 #i #_ #_ #_ #I #V1 #T1 #H destruct -| #L #a #J #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct -| #L #J #V1 #V2 #T1 #T2 #HV12 #HT12 #I #V #T #H destruct /2 width=5/ +[ #I #L #J #W1 #U1 #H destruct +| #L #K #V #V2 #W2 #i #_ #_ #_ #J #W1 #U1 #H destruct +| #a #I #L #V1 #V2 #T1 #T2 #_ #_ #J #W1 #U1 #H destruct +| #I #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W1 #U1 #H destruct /2 width=5/ ] qed-. -lemma cpss_inv_flat1: ∀L,I,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 ▶* U2 → +lemma cpss_inv_flat1: ∀I,L,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 ▶* U2 → ∃∃V2,T2. L ⊢ V1 ▶* V2 & L ⊢ T1 ▶* T2 & U2 = ⓕ{I} V2. T2. /2 width=3 by cpss_inv_flat1_aux/ qed-. @@ -164,7 +168,7 @@ lemma cpss_inv_flat1: ∀L,I,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 ▶* U2 → lemma cpss_fwd_tw: ∀L,T1,T2. L ⊢ T1 ▶* T2 → ♯{T1} ≤ ♯{T2}. #L #T1 #T2 #H elim H -L -T1 -T2 normalize -/3 by monotonic_le_plus_l, le_plus/ (**) (* just /3 width=1/ is too slow *) +/3 width=1 by monotonic_le_plus_l, le_plus/ (**) (* auto is too slow without trace *) qed-. lemma cpss_fwd_shift1: ∀L1,L,T1,T. L ⊢ L1 @@ T1 ▶* T → @@ -181,3 +185,14 @@ lemma cpss_fwd_shift1: ∀L1,L,T1,T. L ⊢ L1 @@ T1 ▶* T → @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *) ] qed-. + +(* Basic_1: removed theorems 27: + subst0_gen_sort subst0_gen_lref subst0_gen_head subst0_gen_lift_lt + subst0_gen_lift_false subst0_gen_lift_ge subst0_refl subst0_trans + subst0_lift_lt subst0_lift_ge subst0_lift_ge_S subst0_lift_ge_s + subst0_subst0 subst0_subst0_back subst0_weight_le subst0_weight_lt + subst0_confluence_neq subst0_confluence_eq subst0_tlt_head + subst0_confluence_lift subst0_tlt + subst1_head subst1_gen_head subst1_lift_S subst1_confluence_lift + subst1_gen_lift_eq subst1_confluence_neq +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss_lift.ma index 616ea63c7..d41e0ac18 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss_lift.ma @@ -19,49 +19,51 @@ include "basic_2/unfold/cpss.ma". (* Relocation properties ****************************************************) +(* Basic_1: was only: subst1_lift_lt subst1_lift_ge *) lemma cpss_lift: l_liftable cpss. #K #T1 #T2 #H elim H -K -T1 -T2 -[ #K #I #L #d #e #_ #U1 #H1 #U2 #H2 +[ #I #K #L #d #e #_ #U1 #H1 #U2 #H2 >(lift_mono … H1 … H2) -H1 -H2 // | #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2 elim (lift_inv_lref1 … H) * #Hid #H destruct - [ elim (lift_trans_ge … HVW2 … HWU2 ?) -W2 // plus_plus_comm_23 #HVU2 lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=6/ ] -| #K #a #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 +| #a #I #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5/ -| #K #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 +| #I #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/ ] qed. +(* Basic_1: was only: subst1_gen_lift_lt subst1_gen_lift_ge *) lemma cpss_inv_lift1: l_deliftable_sn cpss. #L #U1 #U2 #H elim H -L -U1 -U2 -[ #L * #i #K #d #e #_ #T1 #H +[ * #L #i #K #d #e #_ #T1 #H [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/ | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/ | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/ ] | #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H elim (lift_inv_lref2 … H) -H * #Hid #H destruct - [ elim (ldrop_conf_lt … HLK … HLV ?) -L // #L #U #HKL #HLV #HUV + [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2 - elim (lift_trans_le … HUV2 … HVW2 ?) -V2 // >minus_plus minus_plus plus_minus // (lcpss_inv_atom1 … H1) -X1 - >(lcpss_inv_atom1 … H2) -X2 /2 width=3/ -| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct - elim (lcpss_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct - elim (lcpss_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct - elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2 - elim (cpss_conf_lcpss … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/ -] -qed-. - -theorem lcpss_trans: Transitive … lcpss. -#L1 #L #H elim H -L1 -L // -#I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H -elim (lcpss_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct -lapply (cpss_trans_lcpss … HV1 … HL1 … HV2) -V -HL1 /3 width=1/ -qed-. - -(* Advanced forward lemmas **************************************************) - -lemma cpss_fwd_shift1: ∀L1,L,T1,T. L ⊢ L1 @@ T1 ▶* T → - ∃∃L2,T2. L @@ L1 ⊢ ▶* L @@ L2 & L @@ L1 ⊢ T1 ▶* T2 & - T = L2 @@ T2. -#L1 @(lenv_ind_dx … L1) -L1 -[ #L #T1 #T #HT1 - @ex3_2_intro [3: // |4,5: // |1,2: skip ] (**) (* /2 width=4/ does not work *) -| #I #L1 #V1 #IH #L #T1 #T >shift_append_assoc #H (lcpss_inv_atom2 … H) -H /2 width=3/ -| #K2 #I #V2 #X #H - elim (lcpss_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/ -| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_ - elim (lcpss_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct - elim (IHLK2 … HL12 ?) -L2 // /3 width=3/ -| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_ - >commutative_plus normalize #H destruct -] -qed-. - -lemma lcpss_ldrop_trans_O1: dropable_dx lcpss. -/2 width=5 by lcpss_ldrop_trans_O1_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss.ma new file mode 100644 index 000000000..7d3145367 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss.ma @@ -0,0 +1,67 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/grammar/lenv_px_sn.ma". +include "basic_2/unfold/cpss.ma". + +(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************) + +(* Basic_1: includes: csubst1_bind *) +definition lpss: relation lenv ≝ lpx_sn cpss. + +interpretation "parallel unfold (local environment, sn variant)" + 'PSubstStarSn L1 L2 = (lpss L1 L2). + +(* Basic inversion lemmas ***************************************************) + +lemma lpss_inv_atom1: ∀L2. ⋆ ⊢ ▶* L2 → L2 = ⋆. +/2 width=4 by lpx_sn_inv_atom1_aux/ qed-. + +lemma lpss_inv_pair1: ∀I,K1,V1,L2. K1. ⓑ{I} V1 ⊢ ▶* L2 → + ∃∃K2,V2. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L2 = K2. ⓑ{I} V2. +/2 width=3 by lpx_sn_inv_pair1_aux/ qed-. + +lemma lpss_inv_atom2: ∀L1. L1 ⊢ ▶* ⋆ → L1 = ⋆. +/2 width=4 by lpx_sn_inv_atom2_aux/ qed-. + +lemma lpss_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ▶* K2. ⓑ{I} V2 → + ∃∃K1,V1. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L1 = K1. ⓑ{I} V1. +/2 width=3 by lpx_sn_inv_pair2_aux/ qed-. + +(* Basic properties *********************************************************) + +(* Basic_1: was by definition: csubst1_refl *) +lemma lpss_refl: ∀L. L ⊢ ▶* L. +/2 width=1 by lpx_sn_refl/ qed. + +lemma lpss_append: ∀K1,K2. K1 ⊢ ▶* K2 → ∀L1,L2. L1 ⊢ ▶* L2 → + L1 @@ K1 ⊢ ▶* L2 @@ K2. +/3 width=1 by lpx_sn_append, cpss_append/ qed. + +(* Basic forward lemmas *****************************************************) + +lemma lpss_fwd_length: ∀L1,L2. L1 ⊢ ▶* L2 → |L1| = |L2|. +/2 width=2 by lpx_sn_fwd_length/ qed-. + +(* Basic_1: removed theorems 28: + csubst0_clear_O csubst0_drop_lt csubst0_drop_gt csubst0_drop_eq + csubst0_clear_O_back csubst0_clear_S csubst0_clear_trans + csubst0_drop_gt_back csubst0_drop_eq_back csubst0_drop_lt_back + csubst0_gen_sort csubst0_gen_head csubst0_getl_ge csubst0_getl_lt + csubst0_gen_S_bind_2 csubst0_getl_ge_back csubst0_getl_lt_back + csubst0_snd_bind csubst0_fst_bind csubst0_both_bind + csubst1_head csubst1_flat csubst1_gen_head + csubst1_getl_ge csubst1_getl_lt csubst1_getl_ge_back getl_csubst1 + fsubst0_gen_base +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_cpss.ma new file mode 100644 index 000000000..0e23bfce5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_cpss.ma @@ -0,0 +1,202 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fsup.ma". +include "basic_2/unfold/lpss_ldrop.ma". + +(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************) + +(* Main properties on context-sensitive parallel unfold for terms ***********) + +fact cpss_conf_lpss_atom_atom: + ∀I,L1,L2. ∃∃T. L1 ⊢ ⓪{I} ▶* T & L2 ⊢ ⓪{I} ▶* T. +/2 width=3/ qed-. + +fact cpss_conf_lpss_atom_delta: + ∀L0,i. ( + ∀L,T.♯{L, T} < ♯{L0, #i} → + ∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 → + ∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 → + ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0 + ) → + ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 → + ∀V2. K0 ⊢ V0 ▶* V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 → + ∀L1. L0 ⊢ ▶* L1 → ∀L2. L0 ⊢ ▶* L2 → + ∃∃T. L1 ⊢ #i ▶* T & L2 ⊢ T2 ▶* T. +#L0 #i #IH #K0 #V0 #HLK0 #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02 +elim (lpss_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1 +elim (lpss_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct +elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 +elim (lpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct +lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 +lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 +elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 +elim (lift_total V 0 (i+1)) #T #HVT +lapply (cpss_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/ +qed-. + +fact cpss_conf_lpss_delta_delta: + ∀L0,i. ( + ∀L,T.♯{L, T} < ♯{L0, #i} → + ∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 → + ∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 → + ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0 + ) → + ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 → + ∀V1. K0 ⊢ V0 ▶* V1 → ∀T1. ⇧[O, i + 1] V1 ≡ T1 → + ∀KX,VX. ⇩[O, i] L0 ≡ KX.ⓓVX → + ∀V2. KX ⊢ VX ▶* V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 → + ∀L1. L0 ⊢ ▶* L1 → ∀L2. L0 ⊢ ▶* L2 → + ∃∃T. L1 ⊢ T1 ▶* T & L2 ⊢ T2 ▶* T. +#L0 #i #IH #K0 #V0 #HLK0 #V1 #HV01 #T1 #HVT1 +#KX #VX #H #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02 +lapply (ldrop_mono … H … HLK0) -H #H destruct +elim (lpss_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1 +elim (lpss_inv_pair1 … H1) -H1 #K1 #W1 #HK01 #_ #H destruct +lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1 +elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 +elim (lpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct +lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 +lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 +elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 +elim (lift_total V 0 (i+1)) #T #HVT +lapply (cpss_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1 +lapply (cpss_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 -V /2 width=3/ +qed-. + +fact cpss_conf_lpss_bind_bind: + ∀a,I,L0,V0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,ⓑ{a,I}V0.T0} → + ∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 → + ∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 → + ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0 + ) → + ∀V1. L0 ⊢ V0 ▶* V1 → ∀T1. L0.ⓑ{I}V0 ⊢ T0 ▶* T1 → + ∀V2. L0 ⊢ V0 ▶* V2 → ∀T2. L0.ⓑ{I}V0 ⊢ T0 ▶* T2 → + ∀L1. L0 ⊢ ▶* L1 → ∀L2. L0 ⊢ ▶* L2 → + ∃∃T. L1 ⊢ ⓑ{a,I}V1.T1 ▶* T & L2 ⊢ ⓑ{a,I}V2.T2 ▶* T. +#a #I #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 +#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02 +elim (IH … HV01 … HV02 … HL01 … HL02) // +elim (IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -IH // /2 width=1/ /3 width=5/ +qed-. + +fact cpss_conf_lpss_flat_flat: + ∀I,L0,V0,T0. ( + ∀L,T.♯{L,T} < ♯{L0,ⓕ{I}V0.T0} → + ∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 → + ∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 → + ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0 + ) → + ∀V1. L0 ⊢ V0 ▶* V1 → ∀T1. L0 ⊢ T0 ▶* T1 → + ∀V2. L0 ⊢ V0 ▶* V2 → ∀T2. L0 ⊢ T0 ▶* T2 → + ∀L1. L0 ⊢ ▶* L1 → ∀L2. L0 ⊢ ▶* L2 → + ∃∃T. L1 ⊢ ⓕ{I}V1.T1 ▶* T & L2 ⊢ ⓕ{I}V2.T2 ▶* T. +#I #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 +#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02 +elim (IH … HV01 … HV02 … HL01 … HL02) // +elim (IH … HT01 … HT02 … HL01 … HL02) // /3 width=5/ +qed-. + +theorem cpss_conf_lpss: lpx_sn_confluent cpss. +#L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*] +[ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct + elim (cpss_inv_atom1 … H1) -H1 + elim (cpss_inv_atom1 … H2) -H2 + [ #H2 #H1 destruct + /2 width=1 by cpss_conf_lpss_atom_atom/ + | * #K0 #V0 #V2 #i2 #HLK0 #HV02 #HVT2 #H2 #H1 destruct + /3 width=10 by cpss_conf_lpss_atom_delta/ + | #H2 * #K0 #V0 #V1 #i1 #HLK0 #HV01 #HVT1 #H1 destruct + /4 width=10 by ex2_commute, cpss_conf_lpss_atom_delta/ + | * #X #Y #V2 #z #H #HV02 #HVT2 #H2 + * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct + /3 width=17 by cpss_conf_lpss_delta_delta/ + ] +| #a #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct + elim (cpss_inv_bind1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct + elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct + /3 width=10 by cpss_conf_lpss_bind_bind/ +| #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct + elim (cpss_inv_flat1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct + elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct + /3 width=10 by cpss_conf_lpss_flat_flat/ +] +qed-. + +(* Basic_1: was only: subst1_confluence_eq *) +theorem cpss_conf: ∀L. confluent … (cpss L). +/2 width=6 by cpss_conf_lpss/ qed-. + +theorem cpss_trans_lpss: lpx_sn_transitive cpss. +#L1 #T1 @(f2_ind … fw … L1 T1) -L1 -T1 #n #IH #L1 * [|*] +[ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct + elim (cpss_inv_atom1 … H1) -H1 + [ #H destruct + elim (cpss_inv_atom1 … HT2) -HT2 + [ #H destruct // + | * #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct + elim (lpss_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H + elim (lpss_inv_pair2 … H) -H #K1 #V1 #HK12 #HV1 #H destruct + lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/ + ] + | * #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct + elim (lpss_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 + elim (lpss_inv_pair1 … H) -H #K2 #W2 #HK12 #_ #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 + elim (cpss_inv_lift1 … HT2 … HLK2 … HVT) -L2 -T + lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/ + ] +| #a #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2 + elim (cpss_inv_bind1 … H1) -H1 #V #T #HV1 #HT1 #H destruct + elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/ +| #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2 + elim (cpss_inv_flat1 … H1) -H1 #V #T #HV1 #HT1 #H destruct + elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/ +] +qed-. + +(* Basic_1: was only: subst1_trans *) +theorem cpss_trans: ∀L. Transitive … (cpss L). +/2 width=5 by cpss_trans_lpss/ qed-. + +(* Properties on context-sensitive parallel unfold for terms ****************) + +(* Basic_1: was only: subst1_subst1_back *) +lemma lpss_cpss_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ▶* T1 → ∀L1. L0 ⊢ ▶* L1 → + ∃∃T. L1 ⊢ T0 ▶* T & L1 ⊢ T1 ▶* T. +#L0 #T0 #T1 #HT01 #L1 #HL01 +elim (cpss_conf_lpss … HT01 T0 … HL01 … HL01) // -L0 /2 width=3/ +qed-. + +lemma lpss_cpss_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ▶* T1 → ∀L1. L0 ⊢ ▶* L1 → + ∃∃T. L1 ⊢ T0 ▶* T & L0 ⊢ T1 ▶* T. +#L0 #T0 #T1 #HT01 #L1 #HL01 +elim (cpss_conf_lpss … HT01 T0 … L0 … HL01) // -HT01 -HL01 /2 width=3/ +qed-. + +(* Basic_1: was only: subst1_subst1 *) +lemma lpss_cpss_trans: ∀L1,L2. L1 ⊢ ▶* L2 → + ∀T1,T2. L2 ⊢ T1 ▶* T2 → L1 ⊢ T1 ▶* T2. +/2 width=5 by cpss_trans_lpss/ qed-. + +lemma fsup_cpss_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶* U2 → + ∃∃L,U1. L1 ⊢ ▶* L & L ⊢ T1 ▶* U1 & ⦃L, U1⦄ ⊃ ⦃L2, U2⦄. +#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ] +#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2 +elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2 +elim (lift_total T d e) #U #HTU +elim (ldrop_lpss_trans … HLK1 … HK1) -HLK1 -HK1 #L2 #HL12 #HL2K +lapply (cpss_lift … HT1 … HL2K … HTU1 … HTU) -HT1 -HTU1 /3 width=11/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_ldrop.ma new file mode 100644 index 000000000..06a1f0569 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_ldrop.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/ldrop_lpx_sn.ma". +include "basic_2/unfold/cpss_lift.ma". +include "basic_2/unfold/lpss.ma". + +(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************) + +(* Properies on local environment slicing ***********************************) + +lemma lpss_ldrop_conf: dropable_sn lpss. +/3 width=5 by lpx_sn_deliftable_dropable, cpss_inv_lift1/ qed-. + +lemma ldrop_lpss_trans: dedropable_sn lpss. +/3 width=9 by lpx_sn_liftable_dedropable, cpss_lift/ qed-. + +lemma lpss_ldrop_trans_O1: dropable_dx lpss. +/2 width=3 by lpx_sn_dropable/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_lpss.ma new file mode 100644 index 000000000..8f0225255 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lpss_lpss.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/lpss_cpss.ma". + +(* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************) + +(* Main properties **********************************************************) + +theorem lpss_conf: confluent … lpss. +/3 width=6 by lpx_sn_conf, cpss_conf_lpss/ +qed-. + +theorem lpss_trans: Transitive … lpss. +/3 width=5 by lpx_sn_trans, cpss_trans_lpss/ +qed-. + +(* Advanced forward lemmas **************************************************) + +lemma cpss_fwd_shift1: ∀L1,L,T1,T. L ⊢ L1 @@ T1 ▶* T → + ∃∃L2,T2. L @@ L1 ⊢ ▶* L @@ L2 & L @@ L1 ⊢ T1 ▶* T2 & + T = L2 @@ T2. +#L1 @(lenv_ind_dx … L1) -L1 +[ #L #T1 #T #HT1 + @ex3_2_intro [3: // |4,5: // |1,2: skip ] (**) (* /2 width=4/ does not work *) +| #I #L1 #V1 #IH #L #T1 #T >shift_append_assoc #H