From fbf441911bcc80fde66896005a0090a117106d88 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 7 Jun 2014 19:32:38 +0000 Subject: [PATCH] - advances on free variables allow to reduce lleq_lpx_trans to llor_total :) - lazy union of local environments need a depth argument - Makefile bugfixed --- matita/matita/contribs/lambdadelta/Makefile | 6 +- .../lambdadelta/basic_2/multiple/frees.ma | 3 + .../lambdadelta/basic_2/multiple/frees_leq.ma | 32 ++++++ .../basic_2/multiple/frees_lift.ma | 87 ++++++++++++++ .../lambdadelta/basic_2/multiple/lleq_llor.ma | 17 ++- .../lambdadelta/basic_2/multiple/llor.ma | 17 +-- .../basic_2/multiple/llor_ldrop.ma | 2 +- .../basic_2/multiple/llpx_sn_frees.ma | 36 ++++++ .../basic_2/multiple/llpx_sn_llor.ma | 8 +- .../relations/{lazyor_4.ma => lazyor_5.ma} | 4 +- .../basic_2/reduction/lpx_frees.ma | 108 ++++++++++-------- .../lambdadelta/basic_2/reduction/lpx_lleq.ma | 23 +++- .../lambdadelta/basic_2/web/basic_2_src.tbl | 12 +- 13 files changed, 275 insertions(+), 80 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/multiple/frees_leq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_frees.ma rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{lazyor_4.ma => lazyor_5.ma} (88%) diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 16c000e67..10b7261cf 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -115,7 +115,7 @@ define STATS_TEMPLATE STT_$(1) := $(1).stats STTS += $$(STT_$(1)) - $$(STT_$(1)): S0 = $$(shell cat $(1)/$(1)_probe.txt) + $$(STT_$(1)): S0 = $$(shell cat $(1)/$(1)_probe.txt) $$(STT_$(1)): S1 = $$(shell cat $(1)/$(1)_mac.txt) $$(STT_$(1)): S4 = $$(shell ls $$(MAS_$(1)) | wc -l) $$(STT_$(1)): P1 = $$(shell grep "^theorem " $$(MAS_$(1)) | wc -l) @@ -177,9 +177,9 @@ define SUMMARY_TEMPLATE SUM_$(1) := $(1)/web/$(1)_sum.tbl SUMS += $$(SUM_$(1)) - $$(SUM_$(1)): S0 = $$(shell cat $(1)/$(1)_probe.txt) + $$(SUM_$(1)): S0 = $$(shell cat $(1)/$(1)_probe.txt) $$(SUM_$(1)): S1 = $$(shell cat $(1)/$(1)_mac.txt) - $$(SUM_$(1)): S4 = $$(shell ls $$(MAS_$(1)) | wc -l) + $$(SUM_$(1)): S4 = $$(shell ls $$(MAS_$(1)) | wc -l) $$(SUM_$(1)): C1 = $$(shell grep "^inductive \|^record " $$(MAS_$(1)) | wc -l) $$(SUM_$(1)): C2 = $$(shell grep "^definition \|^let rec " $$(MAS_$(1)) | wc -l) $$(SUM_$(1)): C3 = $$(shell grep "^inductive \|^record \|^definition \|^let rec " $$(MAS_$(1)) | wc -l) diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees.ma index 16c2af962..f5e8f1c88 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees.ma @@ -29,6 +29,9 @@ interpretation "context-sensitive free variables (term)" 'FreeStar L i d U = (frees d L U i). +definition frees_trans: predicate (relation3 lenv term term) ≝ + λR. ∀L,U1,U2,i. R L U1 U2 → L ⊢ i ϵ 𝐅*[0]⦃U2⦄ → L ⊢ i ϵ 𝐅*[0]⦃U1⦄. + (* Basic inversion lemmas ***************************************************) lemma frees_inv: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_leq.ma new file mode 100644 index 000000000..bb387ad10 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_leq.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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_leq.ma". +include "basic_2/multiple/frees.ma". + +(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) + +(* Properties on equivalence for local environments *************************) + +lemma leq_frees_trans: ∀L2,U,d,i. L2 ⊢ i ϵ 𝐅*[d]⦃U⦄ → + ∀L1. L1 ≃[d, ∞] L2 → L1 ⊢ i ϵ 𝐅*[d]⦃U⦄. +#L2 #U #d #i #H elim H -L2 -U -d -i /3 width=2 by frees_eq/ +#I2 #L2 #K2 #U #W2 #d #i #j #Hdj #Hji #HnU #HLK2 #_ #IHW2 #L1 #HL12 +elim (leq_ldrop_trans_be … HL12 … HLK2) -L2 // >yminus_Y_inj #K1 #HK12 #HLK1 +lapply (leq_inv_O_Y … HK12) -HK12 #H destruct /3 width=9 by frees_be/ +qed-. + +lemma frees_leq_conf: ∀L1,U,d,i. L1 ⊢ i ϵ 𝐅*[d]⦃U⦄ → + ∀L2. L1 ≃[d, ∞] L2 → L2 ⊢ i ϵ 𝐅*[d]⦃U⦄. +/3 width=3 by leq_sym, leq_frees_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma index 3eda7ab58..8b295524d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma @@ -71,3 +71,90 @@ lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[0]⦃U⦄ → #a #I #L #W #U #i #HU elim (frees_dec L W 0 i) /4 width=5 by frees_S, frees_bind_dx, frees_bind_sn/ qed. + +(* Properties on relocation *************************************************) + +lemma frees_lift_ge: ∀K,T,d,i. K ⊢ i ϵ𝐅*[d]⦃T⦄ → + ∀L,s,d0,e0. ⇩[s, d0, e0] L ≡ K → + ∀U. ⇧[d0, e0] T ≡ U → d0 ≤ i → + L ⊢ i+e0 ϵ 𝐅*[d]⦃U⦄. +#K #T #d #i #H elim H -K -T -d -i +[ #K #T #d #i #HnT #L #s #d0 #e0 #_ #U #HTU #Hd0i -K -s + @frees_eq #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/ +| #I #K #K0 #T #V #d #i #j #Hdj #Hji #HnT #HK0 #HV #IHV #L #s #d0 #e0 #HLK #U #HTU #Hd0i + elim (lt_or_ge j d0) #H1 + [ elim (ldrop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 #HLK0 #HVW + @(frees_be … HL0) -HL0 -HV + /3 width=3 by lt_plus_to_minus_r, lt_to_le_to_lt/ + [ #X #HXU >(plus_minus_m_m d0 1) in HTU; /2 width=2 by ltn_to_ltO/ #HTU + elim (lift_div_le … HXU … HTU ?) -U /2 width=2 by monotonic_pred/ + | >minus_plus commutative_plus -HLK0 #HLK0 + @(frees_be … HLK0) -HLK0 -IHV + /2 width=1 by yle_plus_dx1_trans, lt_minus_to_plus/ + #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/ + ] +] +qed. + +(* Inversion lemmas on relocation *******************************************) + +lemma frees_inv_lift_be: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ → + ∀K,s,d0,e0. ⇩[s, d0, e0+1] L ≡ K → + ∀T. ⇧[d0, e0+1] T ≡ U → d0 ≤ i → i ≤ d0 + e0 → ⊥. +#L #U #d #i #H elim H -L -U -d -i +[ #L #U #d #i #HnU #K #s #d0 #e0 #_ #T #HTU #Hd0i #Hide0 + elim (lift_split … HTU i e0) -HTU /2 width=2 by/ +| #I #L #K0 #U #W #d #i #j #Hdi #Hij #HnU #HLK0 #_ #IHW #K #s #d0 #e0 #HLK #T #HTU #Hd0i #Hide0 + elim (lt_or_ge j d0) #H1 + [ elim (ldrop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW + @(IHW … HKL0 … HVW) + [ /2 width=1 by monotonic_le_minus_l2/ + | >minus_plus >minus_plus >plus_minus /2 width=1 by monotonic_le_minus_l/ + ] + | elim (lift_split … HTU j e0) -HTU /3 width=3 by lt_to_le_to_lt, lt_to_le/ + ] +] +qed-. + +lemma frees_inv_lift_ge: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ → + ∀K,s,d0,e0. ⇩[s, d0, e0] L ≡ K → + ∀T. ⇧[d0, e0] T ≡ U → d0 + e0 ≤ i → + K ⊢ i-e0 ϵ𝐅*[d-yinj e0]⦃T⦄. +#L #U #d #i #H elim H -L -U -d -i +[ #L #U #d #i #HnU #K #s #d0 #e0 #HLK #T #HTU #Hde0i -L -s + elim (le_inv_plus_l … Hde0i) -Hde0i #Hd0ie0 #He0i @frees_eq #X #HXT -K + elim (lift_trans_le … HXT … HTU) -T // minus_plus >minus_plus >plus_minus /2 width=1 by monotonic_le_minus_l/ + ] + | elim (lt_or_ge j (d0+e0)) [ >commutative_plus |] #H2 + [ -L -I -W lapply (lt_plus_to_minus ???? H2) // -H2 #H2 + elim (lift_split … HTU j (e0-1)) -HTU // + [ >minus_minus_associative /2 width=2 by ltn_to_ltO/ commutative_plus /3 width=1 by le_minus_to_plus, monotonic_pred/ + ] + | lapply (ldrop_conf_ge … HLK … HLK0 ?) // -L #HK0 + elim (le_inv_plus_l … H2) -H2 #H2 #He0j + @(frees_be … HK0) + [ /2 width=1 by monotonic_yle_minus_dx/ + | /2 width=1 by monotonic_lt_minus_l/ + | #X #HXT elim (lift_trans_le … HXT … HTU) -T // arith_b1 /2 width=5 by/ + ] + ] + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_llor.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_llor.ma index 2a31fece3..253cb294a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_llor.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_llor.ma @@ -13,16 +13,17 @@ (**************************************************************************) include "basic_2/multiple/llor.ma". +include "basic_2/multiple/llpx_sn_frees.ma". include "basic_2/multiple/lleq_alt.ma". (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) (* Properties on poinwise union for local environments **********************) -lemma llpx_sn_llor_dx: ∀R,L1,L2. - (∀U,i. L2 ⊢ i ϵ 𝐅*[0]⦃U⦄ → L1 ⊢ i ϵ 𝐅*[0]⦃U⦄) → - ∀T. llpx_sn R 0 T L1 L2 → ∀L. L1 ⩖[T] L2 ≡ L → L2 ≡[T, 0] L. -#R #L1 #L2 #HR #T #H1 #L #H2 +lemma llpx_sn_llor_dx: ∀R. (s_r_confluent1 … R (llpx_sn R 0)) → (frees_trans R) → + ∀L1,L2,T,d. llpx_sn R d T L1 L2 → ∀L. L1 ⩖[T, d] L2 ≡ L → L2 ≡[T, d] L. +#R #H1R #H2R #L1 #L2 #T #d #H1 #L #H2 +lapply (llpx_sn_frees_trans … H1R H2R … H1) -H1R -H2R #HR elim (llpx_sn_llpx_sn_alt … H1) -H1 #HL12 #IH1 elim H2 -H2 #_ #HL1 #IH2 @lleq_intro_alt // #I2 #I #K2 #K #V2 #V #i #Hi #HnT #HLK2 #HLK @@ -30,5 +31,11 @@ lapply (ldrop_fwd_length_lt2 … HLK) #HiL elim (ldrop_O1_lt (Ⓕ) L1 i) // -HiL #I1 #K1 #V1 #HLK1 elim (IH1 … HLK1 HLK2) -IH1 /2 width=1 by/ #H #_ destruct elim (IH2 … HLK1 HLK2 HLK) -IH2 -HLK1 -HLK2 -HLK * /2 width=1 by conj/ #H -elim H -H /2 width=1 by/ +[ elim (ylt_yle_false … H) -H // +| elim H -H /2 width=1 by/ +] qed. + +lemma llpx_sn_llor_dx_sym: ∀R. (s_r_confluent1 … R (llpx_sn R 0)) → (frees_trans R) → + ∀L1,L2,T,d. llpx_sn R d T L1 L2 → ∀L. L1 ⩖[T, d] L2 ≡ L → L ≡[T, d] L2. +/3 width=6 by llpx_sn_llor_dx, lleq_sym/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor.ma index eda4c00d6..df157a990 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor.ma @@ -12,27 +12,28 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazyor_4.ma". +include "basic_2/notation/relations/lazyor_5.ma". include "basic_2/multiple/frees.ma". (* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************) -definition llor: relation4 term lenv lenv lenv ≝ λT,L2,L1,L. +definition llor: ynat → relation4 term lenv lenv lenv ≝ λd,T,L2,L1,L. ∧∧ |L1| ≤ |L2| & |L1| = |L| & (∀I1,I2,I,K1,K2,K,V1,V2,V,i. - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → ⇩[i] L ≡ K.ⓑ{I}V → - (∧∧ (L1 ⊢ i ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) & I1 = I & V1 = V) ∨ - (∧∧ L1 ⊢ i ϵ 𝐅*[yinj 0]⦃T⦄ & I1 = I & V2 = V) + ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → ⇩[i] L ≡ K.ⓑ{I}V → ∨∨ + (∧∧ yinj i < d & I1 = I & V1 = V) | + (∧∧ (L1 ⊢ i ϵ 𝐅*[d]⦃T⦄ → ⊥) & I1 = I & V1 = V) | + (∧∧ d ≤ yinj i & L1 ⊢ i ϵ 𝐅*[d]⦃T⦄ & I1 = I & V2 = V) ). interpretation "lazy union (local environment)" - 'LazyOr L1 T L2 L = (llor T L2 L1 L). + 'LazyOr L1 T d L2 L = (llor d T L2 L1 L). (* Basic properties *********************************************************) -lemma llor_atom: ∀T,L2. ⋆ ⩖[T] L2 ≡ ⋆. -#T #L2 @and3_intro // +lemma llor_atom: ∀L2,T,d. ⋆ ⩖[T, d] L2 ≡ ⋆. +#L2 #T #d @and3_intro // #I1 #I2 #I #K1 #K2 #K #V1 #V2 #V #i #HLK1 elim (ldrop_inv_atom1 … HLK1) -HLK1 #H destruct qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma index d8a4789b0..b766269e7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma @@ -19,4 +19,4 @@ include "basic_2/multiple/llor.ma". (* Advanced properties ******************************************************) -axiom llor_total: ∀L1,L2,T. |L1| ≤ |L2| → ∃L. L1 ⩖[T] L2 ≡ L. +axiom llor_total: ∀L1,L2,T,d. |L1| ≤ |L2| → ∃L. L1 ⩖[T, d] L2 ≡ L. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_frees.ma new file mode 100644 index 000000000..f00bd071a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_frees.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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/multiple/frees.ma". +include "basic_2/multiple/llpx_sn_alt_rec.ma". + +(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) + +(* Properties on context-sensitive free variables ***************************) + +fact llpx_sn_frees_trans_aux: ∀R. (s_r_confluent1 … R (llpx_sn R 0)) → (frees_trans R) → + ∀L2,U,d,i. L2 ⊢ i ϵ 𝐅*[d]⦃U⦄ → + ∀L1. llpx_sn R d U L1 L2 → L1 ⊢ i ϵ 𝐅*[d]⦃U⦄. +#R #H1R #H2R #L2 #U #d #i #H elim H -L2 -U -d -i /3 width=2 by frees_eq/ +#I2 #L2 #K2 #U #W2 #d #i #j #Hdj #Hji #HnU #HLK2 #_ #IHW2 #L1 #HL12 +elim (llpx_sn_inv_alt_r … HL12) -HL12 #HL12 #IH +lapply (ldrop_fwd_length_lt2 … HLK2) #Hj +elim (ldrop_O1_lt (Ⓕ) L1 j) // -Hj -HL12 #I1 #K1 #W1 #HLK1 +elim (IH … HnU HLK1 HLK2) // -IH -HLK2 /5 width=11 by frees_be/ +qed-. + +lemma llpx_sn_frees_trans: ∀R. (s_r_confluent1 … R (llpx_sn R 0)) → (frees_trans R) → + ∀L1,L2,U,d. llpx_sn R d U L1 L2 → + ∀i. L2 ⊢ i ϵ 𝐅*[d]⦃U⦄ → L1 ⊢ i ϵ 𝐅*[d]⦃U⦄. +/2 width=6 by llpx_sn_frees_trans_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_llor.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_llor.ma index 4828b7b75..6f27ec9b0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_llor.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_llor.ma @@ -21,14 +21,14 @@ include "basic_2/multiple/lleq_alt.ma". (* Inversion lemmas on poinwise union for local environments ****************) lemma llpx_sn_llor_fwd_sn: ∀R. (∀L. reflexive … (R L)) → - ∀L1,L2,T. llpx_sn R 0 T L1 L2 → - ∀L. L1 ⩖[T] L2 ≡ L → lpx_sn R L1 L. -#R #HR #L1 #L2 #T #H1 #L #H2 + ∀L1,L2,T,d. llpx_sn R d T L1 L2 → + ∀L. L1 ⩖[T, d] L2 ≡ L → lpx_sn R L1 L. +#R #HR #L1 #L2 #T #d #H1 #L #H2 elim (llpx_sn_llpx_sn_alt … H1) -H1 #HL12 #IH1 elim H2 -H2 #_ #HL1 #IH2 @lpx_sn_intro_alt // #I1 #I #K1 #K #V1 #V #i #HLK1 #HLK lapply (ldrop_fwd_length_lt2 … HLK) #HiL elim (ldrop_O1_lt (Ⓕ) L2 i) // -HiL -HL1 -HL12 #I2 #K2 #V2 #HLK2 -elim (IH2 … HLK1 HLK2 HLK) -IH2 -HLK * [ /2 width=1 by conj/ ] +elim (IH2 … HLK1 HLK2 HLK) -IH2 -HLK * /2 width=1 by conj/ #HnT #H1 #H2 elim (IH1 … HnT … HLK1 HLK2) -IH1 -HnT -HLK1 -HLK2 /2 width=1 by conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyor_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyor_5.ma similarity index 88% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyor_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyor_5.ma index cc97e6bbe..509089ddb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyor_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyor_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L1 ⩖ break [ term 46 T ] break term 46 L2 ≡ break term 46 L )" +notation "hvbox( L1 ⩖ break [ term 46 T , break term 46 d ] break term 46 L2 ≡ break term 46 L )" non associative with precedence 45 - for @{ 'LazyOr $L1 $T $L2 $L }. + for @{ 'LazyOr $L1 $T $d $L2 $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_frees.ma index 1458cf3fa..b44d88504 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_frees.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_frees.ma @@ -12,65 +12,77 @@ (* *) (**************************************************************************) -include "basic_2/multiple/fqup.ma". +include "basic_2/multiple/frees_leq.ma". include "basic_2/multiple/frees_lift.ma". include "basic_2/reduction/lpx_ldrop.ma". (* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) -(* -lemma cofrees_lsuby_conf: ∀L1,U,i. L1 ⊢ i ~ϵ 𝐅*⦃U⦄ → - ∀L2. lsuby L1 L2 → L2 ⊢ i ~ϵ 𝐅*⦃U⦄. -/3 width=3 by lsuby_cpys_trans/ qed-. -lemma lpx_cpx_cofrees_conf: ∀h,g,G,L1,U1,U2. ⦃G, L1⦄ ⊢ U1 ➡[h, g] U2 → - ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → - ∀i. L1 ⊢ i ~ϵ 𝐅*⦃U1⦄ → L2 ⊢ i ~ϵ 𝐅*⦃U2⦄. +(* Properties on context-sensitive free variables ***************************) + +lemma lpx_cpx_frees_trans: ∀h,g,G,L1,U1,U2. ⦃G, L1⦄ ⊢ U1 ➡[h, g] U2 → + ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → + ∀i. L2 ⊢ i ϵ 𝐅*[0]⦃U2⦄ → L1 ⊢ i ϵ 𝐅*[0]⦃U1⦄. #h #g #G #L1 #U1 @(fqup_wf_ind_eq … G L1 U1) -G -L1 -U1 #G0 #L0 #U0 #IH #G #L1 * * -[ -IH #k #HG #HL #HU #U2 #H elim (cpx_inv_sort1 … H) -H - [| * #l #_ ] #H destruct // -| #j #HG #HL #HU #U2 #H #L2 #HL12 #i #Hi elim (cpx_inv_lref1 … H) -H - [ #H destruct elim (lt_or_eq_or_gt i j) #Hji - [ -IH -HL12 /2 width=4 by cofrees_lref_gt/ - | -IH -HL12 destruct elim (cofrees_inv_lref_eq … Hi) - | elim (lt_or_ge j (|L2|)) /2 width=5 by cofrees_lref_free/ #Hj - elim (ldrop_O1_lt (Ⓕ) L1 j) [2: >(lpx_fwd_length … HL12) // ] #I #K1 #W1 #HLK1 - elim (lpx_ldrop_conf … HLK1 … HL12) -HL12 #Y #H #HLK2 - elim (lpx_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct - lapply (cofrees_inv_lref_lt … Hi … HLK1) -Hi // #HW1 - lapply (IH … HW12 … HK12 … HW1) /2 width=2 by fqup_lref/ -L1 -K1 -W1 #HW2 - /2 width=9 by cofrees_lref_lt/ (**) (* full auto too slow *) - ] - | * #I #K1 #W1 #W0 #HLK1 #HW10 #HW0U2 elim (lt_or_ge j i) #Hji - [ lapply (ldrop_fwd_drop2 … HLK1) #H0 - elim (lpx_ldrop_conf … H0 … HL12) #K2 #HK12 #HLK2 - @(cofrees_lift_ge … HLK2 … HW0U2) // - @(IH … HW10) /2 width=2 by fqup_lref/ -L2 -K2 -W0 -U2 -IH - (cpx_inv_gref1 … H1) -H1 destruct + #L2 #_ #i #H2 elim (frees_inv_gref … H2) | #a #I #W1 #U1 #HG #HL #HU #X #HX #L2 #HL12 #i #Hi destruct - elim (cofrees_inv_bind … Hi) -Hi #HW1 #HU1 - elim (cpx_inv_bind1 … HX) -HX - [ * #W2 #U2 #HW12 #HU12 #H destruct /4 width=8 by cofrees_bind, lpx_pair/ - | + elim (cpx_inv_bind1 … HX) -HX * + [ #W2 #U2 #HW12 #HU12 #H destruct + elim (frees_inv_bind_O … Hi) -Hi + /4 width=7 by frees_bind_dx_O, frees_bind_sn, lpx_pair/ + | #U2 #HU12 #HXU2 #H1 #H2 destruct + lapply (frees_lift_ge … Hi (L2.ⓓW1) (Ⓕ) … HXU2 ?) + /4 width=7 by frees_bind_dx_O, lpx_pair, ldrop_drop/ ] | #I #W1 #X1 #HG #HL #HU #X2 #HX2 #L2 #HL12 #i #Hi destruct - elim (cofrees_inv_flat … Hi) -Hi #HW1 #HX1 elim (cpx_inv_flat1 … HX2) -HX2 * - [ #W2 #U2 #HW12 #HU12 #H destruct /3 width=7 by cofrees_flat/ - | #HU12 #H destruct /2 width=7 by/ - | #HW12 #H destruct /2 width=7 by/ + [ #W2 #U2 #HW12 #HU12 #H destruct + elim (frees_inv_flat … Hi) -Hi /3 width=7 by frees_flat_dx, frees_flat_sn/ + | #HU12 #H destruct /3 width=7 by frees_flat_dx/ + | #HW12 #H destruct /3 width=7 by frees_flat_sn/ | #b #W2 #V1 #V2 #U1 #U2 #HW12 #HV12 #HU12 #H1 #H2 #H3 destruct - elim (cofrees_inv_bind … HX1) -HX1 #HV1 #HU1 - @cofrees_bind [ /3 width=7 by cofrees_flat/ ] - @(cofrees_lsuby_conf (L2.ⓛV2)) /3 width=7 by lpx_pair, lsuby_succ/ - | - - -*) + elim (frees_inv_bind … Hi) -Hi #Hi + [ elim (frees_inv_flat … Hi) -Hi + /4 width=7 by frees_flat_dx, frees_flat_sn, frees_bind_sn/ + | lapply (leq_frees_trans … Hi (L2.ⓛV2) ?) /2 width=1 by leq_succ/ -Hi #HU2 + lapply (frees_weak … HU2 0 ?) -HU2 + /5 width=7 by frees_bind_dx_O, frees_flat_dx, lpx_pair/ + ] + | #b #W2 #W0 #V1 #V2 #U1 #U2 #HW12 #HW20 #HV12 #HU12 #H1 #H2 #H3 destruct + elim (frees_inv_bind_O … Hi) -Hi #Hi + [ /4 width=7 by frees_flat_dx, frees_bind_sn/ + | elim (frees_inv_flat … Hi) -Hi + [ #HW0 lapply (frees_inv_lift_ge … HW0 L2 (Ⓕ) … HW20 ?) -W0 + /3 width=7 by frees_flat_sn, ldrop_drop/ + | /5 width=7 by frees_bind_dx_O, frees_flat_dx, lpx_pair/ + ] + ] + ] +] +qed-. + +lemma cpx_frees_trans: ∀h,g,G. frees_trans (cpx h g G). +/2 width=8 by lpx_cpx_frees_trans/ qed-. + +lemma lpx_frees_trans: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → + ∀U,i. L2 ⊢ i ϵ 𝐅*[0]⦃U⦄ → L1 ⊢ i ϵ 𝐅*[0]⦃U⦄. +/2 width=8 by lpx_cpx_frees_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma index 08918429b..36eb55361 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma @@ -12,18 +12,35 @@ (* *) (**************************************************************************) +include "basic_2/multiple/llor_ldrop.ma". +include "basic_2/multiple/llpx_sn_llor.ma". +include "basic_2/multiple/llpx_sn_lpx_sn.ma". include "basic_2/multiple/lleq_leq.ma". -include "basic_2/multiple/lleq_ldrop.ma". +include "basic_2/multiple/lleq_llor.ma". include "basic_2/reduction/cpx_leq.ma". -include "basic_2/reduction/lpx_ldrop.ma". +include "basic_2/reduction/cpx_lleq.ma". +include "basic_2/reduction/lpx_frees.ma". (* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) (* Properties on lazy equivalence for local environments ********************) -axiom lleq_lpx_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 → +(* Note: contains a proof of llpx_cpx_conf *) +lemma lleq_lpx_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 → ∀L1,T,d. L1 ≡[T, d] L2 → ∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & K1 ≡[T, d] K2. +#h #g #G #L2 #K2 #HLK2 #L1 #T #d #HL12 +lapply (lpx_fwd_length … HLK2) #H1 +lapply (lleq_fwd_length … HL12) #H2 +lapply (lpx_sn_llpx_sn … T … d HLK2) // -HLK2 #H +lapply (lleq_llpx_sn_trans … HL12 … H) /2 width=3 by lleq_cpx_trans/ -HL12 -H #H +elim (llor_total L1 K2 T d) // -H1 -H2 #K1 #HLK1 +lapply (llpx_sn_llor_dx_sym … H … HLK1) +[ /2 width=6 by cpx_frees_trans/ +| /3 width=10 by cpx_llpx_sn_conf, cpx_inv_lift1, cpx_lift/ +| /3 width=5 by llpx_sn_llor_fwd_sn, ex2_intro/ +] +qed-. lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ≡[T1, 0] L1 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 525a89592..7e845ff65 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -21,7 +21,7 @@ table { class "magenta" [ { "higher order dynamic typing" * } { [ { "higher order native type assignment" * } { - [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ] + [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ]basic_2/multiple/frees_leq.ma } ] } @@ -195,7 +195,7 @@ table { ] [ { "degree assignment" * } { [ "da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )" "da_lift" + "da_da" * ] - } + }basic_2/multiple/frees_leq.ma ] [ { "parameters" * } { [ "sh" "sd" * ] @@ -215,15 +215,15 @@ table { } ] [ { "lazy pointwise extension of a relation" * } { - [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" + "llpx_sn_llor" * ] + [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" + "llpx_sn_frees" + "llpx_sn_llor" * ] } ] [ { "pointwise union for local environments" * } { - [ "llor ( ? ⩖[?] ? ≡ ? )" "llor_ldrop" * ] + [ "llor ( ? ⩖[?,?] ? ≡ ? )" "llor_ldrop" * ] } ] [ { "context-sensitive exclusion from free variables" * } { - [ "frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )" "frees_lift" * ] + [ "frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )" "frees_leq" + "frees_lift" * ] } ] [ { "contxt-sensitive extended multiple substitution" * } { @@ -273,7 +273,7 @@ table { [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_ldrop" + "lpx_sn_lpx_sn" * ] } ] - [ { "basic local env. slicing" * } { + [ { "basic local env. slicing" * } { [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_leq" + "ldrop_ldrop" * ] } ] -- 2.39.2