From 944b1f7b762774a6f8d99a2c2846f865b6788712 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 28 Feb 2014 13:48:27 +0000 Subject: [PATCH] - some corrections and additions - lsubr moved from "relocation" to "static" --- .../lambdadelta/basic_2/grammar/leq.ma | 16 ++++++++++++++-- .../lambdadelta/basic_2/grammar/leq_leq.ma | 17 +++++++++++++++++ .../lambdadelta/basic_2/reduction/cpr.ma | 2 +- .../basic_2/relocation/ldrop_leq.ma | 12 ++++++++++++ .../lambdadelta/basic_2/static/lsuba.ma | 2 +- .../lambdadelta/basic_2/static/lsubd.ma | 2 +- .../basic_2/{relocation => static}/lsubr.ma | 0 .../{relocation => static}/lsubr_lsubr.ma | 2 +- .../basic_2/substitution/lleq_alt.ma | 3 +++ .../basic_2/substitution/lleq_lleq.ma | 18 +++++++++++++----- .../lambdadelta/basic_2/web/basic_2_src.tbl | 8 ++++---- 11 files changed, 67 insertions(+), 15 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => static}/lsubr.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => static}/lsubr_lsubr.ma (98%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma index 1745c00e4..6578c4cd9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma @@ -120,6 +120,12 @@ lemma leq_inv_pair1: ∀I,K1,L2,V,e. K1.ⓑ{I}V ≃[0, e] L2 → 0 < e → ∃∃K2. K1 ≃[0, ⫰e] K2 & L2 = K2.ⓑ{I}V. /2 width=6 by leq_inv_pair1_aux/ qed-. +lemma leq_inv_pair: ∀I1,I2,L1,L2,V1,V2,e. L1.ⓑ{I1}V1 ≃[0, e] L2.ⓑ{I2}V2 → 0 < e → + ∧∧ L1 ≃[0, ⫰e] L2 & I1 = I2 & V1 = V2. +#I1 #I2 #L1 #L2 #V1 #V2 #e #H #He elim (leq_inv_pair1 … H) -H // +#Y #HL12 #H destruct /2 width=1 by and3_intro/ +qed-. + fact leq_inv_succ1_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 → ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → 0 < d → ∃∃J2,K2,W2. K1 ≃[⫰d, e] K2 & L2 = K2.ⓑ{J2}W2. @@ -142,6 +148,12 @@ lemma leq_inv_atom2: ∀L1,d,e. L1 ≃[d, e] ⋆ → L1 = ⋆. /3 width=3 by leq_inv_atom1, leq_sym/ qed-. +lemma leq_inv_succ: ∀I1,I2,L1,L2,V1,V2,d,e. L1.ⓑ{I1}V1 ≃[d, e] L2.ⓑ{I2}V2 → 0 < d → + L1 ≃[⫰d, e] L2. +#I1 #I2 #L1 #L2 #V1 #V2 #d #e #H #Hd elim (leq_inv_succ1 … H) -H // +#Z #Y #X #HL12 #H destruct // +qed-. + lemma leq_inv_zero2: ∀I2,K2,L1,V2. L1 ≃[0, 0] K2.ⓑ{I2}V2 → ∃∃I1,K1,V1. K1 ≃[0, 0] K2 & L1 = K1.ⓑ{I1}V1. #I2 #K2 #L1 #V2 #H elim (leq_inv_zero1 … (leq_sym … H)) -H @@ -162,8 +174,8 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma leq_fwd_length: ∀L1,L2,d,e. L1 ≃[d, e] L2 → |L2| ≤ |L1|. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize /2 width=1 by le_S_S/ +lemma leq_fwd_length: ∀L1,L2,d,e. L1 ≃[d, e] L2 → |L2| = |L1|. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize // qed-. (* Advanced inversion lemmas ************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/leq_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/leq_leq.ma index 1a2095517..d07a5f2e6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/leq_leq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/leq_leq.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/ynat/ynat_plus.ma". include "basic_2/grammar/leq.ma". (* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************) @@ -30,3 +31,19 @@ theorem leq_trans: ∀d,e. Transitive … (leq d e). #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by leq_succ/ ] qed-. + +theorem leq_canc_sn: ∀d,e,L,L1,L2. L ≃[d, e] L1 → L ≃[d, e] L2 → L1 ≃[d, e] L2. +/3 width=3 by leq_trans, leq_sym/ qed-. + +theorem leq_canc_dx: ∀d,e,L,L1,L2. L1 ≃[d, e] L → L2 ≃[d, e] L → L1 ≃[d, e] L2. +/3 width=3 by leq_trans, leq_sym/ qed-. + +theorem leq_join: ∀L1,L2,d,i. L1 ≃[d, i] L2 → + ∀e. L1 ≃[i+d, e] L2 → L1 ≃[d, i+e] L2. +#L1 #L2 #d #i #H elim H -L1 -L2 -d -i // +[ #I #L1 #L2 #V #e #_ #IHL12 #e #H + lapply (leq_inv_succ … H ?) -H // >ypred_succ /3 width=1 by leq_pair/ +| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #e #H + lapply (leq_inv_succ … H ?) -H // >yplus_succ2 >ypred_succ /3 width=1 by leq_succ/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma index ba37c86ba..c68911d4f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma @@ -14,7 +14,7 @@ include "basic_2/notation/relations/pred_4.ma". include "basic_2/grammar/genv.ma". -include "basic_2/relocation/lsubr.ma". +include "basic_2/static/lsubr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma index e5a755531..1355827f7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma @@ -68,3 +68,15 @@ lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R). /3 width=6 by leq_trans, step, ex3_intro/ ] qed-. + +(* Inversion lemmas on equivalence ******************************************) + +lemma ldrop_O_inj: ∀i,L1,L2,K. ⇩[i] L1 ≡ K → ⇩[i] L2 ≡ K → L1 ≃[i, ∞] L2. +#i @(nat_ind_plus … i) -i +[ #L1 #L2 #K #H <(ldrop_inv_O2 … H) -K #H <(ldrop_inv_O2 … H) -L1 // +| #i #IHi * [2: #L1 #I1 #V1 ] * [2,4: #L2 #I2 #V2 ] #K #HLK1 #HLK2 // + lapply (ldrop_fwd_length … HLK1) + <(ldrop_fwd_length … HLK2) [ /4 width=5 by ldrop_inv_drop1, leq_succ/ ] + normalize