From be1d03ec6889658e5acbf69a2d191e7bff80c452 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 13 Jan 2014 18:13:17 +0000 Subject: [PATCH] some improvements on the relation lsx ... --- .../lambdadelta/basic_2/computation/csx.ma | 8 ++ .../basic_2/computation/lpxs_lleq.ma | 24 +++-- .../lambdadelta/basic_2/computation/lsx.ma | 34 +++++++ .../basic_2/computation/lsx_csx.ma | 44 +++++++-- .../computation/{lsx_cpxs.ma => lsx_lpxs.ma} | 26 +++++- .../lambdadelta/basic_2/reduction/cpx_lleq.ma | 6 +- .../lambdadelta/basic_2/reduction/lpx_lleq.ma | 2 +- .../basic_2/substitution/lleq_alt.ma | 59 ------------ .../basic_2/substitution/lleq_ext.ma | 91 +++++++++++++++++++ .../basic_2/substitution/lleq_fqus.ma | 2 +- .../basic_2/substitution/lleq_lleq.ma | 20 ++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 12 files changed, 234 insertions(+), 84 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/computation/{lsx_cpxs.ma => lsx_lpxs.ma} (61%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma index c57b04713..6d55772c4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma @@ -117,6 +117,14 @@ qed-. lemma csx_fwd_flat_dx: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓕ{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] T. /2 width=5 by csx_fwd_flat_dx_aux/ qed-. +lemma csx_fwd_bind: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓑ{a,I}V.T → + ⦃G, L⦄ ⊢ ⬊*[h, g] V ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ⬊*[h, g] T. +/3 width=3 by csx_fwd_pair_sn, csx_fwd_bind_dx, conj/ qed-. + +lemma csx_fwd_flat: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓕ{I}V.T → + ⦃G, L⦄ ⊢ ⬊*[h, g] V ∧ ⦃G, L⦄ ⊢ ⬊*[h, g] T. +/3 width=3 by csx_fwd_pair_sn, csx_fwd_flat_dx, conj/ qed-. + (* Basic_1: removed theorems 14: sn3_cdelta sn3_gen_cflat sn3_cflat sn3_cpr3_trans sn3_shift sn3_change diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma index 4609675a7..a919045df 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lleq_alt.ma". +include "basic_2/substitution/lleq_ext.ma". include "basic_2/computation/lpxs_ldrop.ma". include "basic_2/computation/lpxs_cpxs.ma". @@ -20,14 +20,22 @@ include "basic_2/computation/lpxs_cpxs.ma". (* Advanced properties ******************************************************) -axiom lleq_lpxs_trans_nlleq: ∀h,g,G,L1s,L1d,T,d. L1s ⋕[T, d] L1d → - ∀L2d. ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d → (L1d ⋕[T, d] L2d → ⊥) → - ∃∃L2s. ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s & L2s ⋕[T, d] L2d & L1s ⋕[T, d] L2s → ⊥. +axiom lleq_lpxs_trans: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ∀K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 → + ∃∃K1. ⦃G, L1⦄ ⊢ ➡*[h, g] K1 & K1 ⋕[T, d] K2. +(* +#h #g #G #L1 #L2 #T #d #H @(lleq_ind_alt … H) -L1 -L2 -T -d +[ +| +| +| +| +| #a #I #L1 #L2 #V #T #d #_ #_ #IHV #IHT #K2 #HLK2 + elim (IHV … HLK2) -IHV #KV #HLKV #HV + elim (IHT (K2.ⓑ{I}V)) -IHT /2 width=1 by lpxs_pair_refl/ -HLK2 #Y #H #HT + elim (lpxs_inv_pair1 … H) -H #KT #VT #HLKT #_ #H destruct -(* Advanced inversion lemmas ************************************************) - -axiom lpxs_inv_cpxs_nlleq: ∀h,g,G,L1,L2,T1. ⦃G, L1⦄ ⊢ ➡*[h,g] L2 → (L1 ⋕[T1, 0] L2 → ⊥) → - ∃∃T2. ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 & T1 = T2 → ⊥ & ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2. +#h #g #G #L1 #L2 #T #d * #HL12 #IH #K2 #HLK2 +*) (* Properties on lazy equivalence for local environments ********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma index c842a9448..38e185a86 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma @@ -61,3 +61,37 @@ lemma lsx_gref: ∀h,g,G,L,p. G ⊢ ⋕⬊*[h, g, §p] L. #L2 #HL12 #H elim H -H /3 width=4 by lpxs_fwd_length, lleq_gref/ qed. + +(* Basic forward lemmas *****************************************************) + +lemma lsx_fwd_bind_sn: ∀h,g,a,I,G,L,V,T. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T] L → + G ⊢ ⋕⬊*[h, g, V] L. +#h #g #a #I #G #L #V #T #H @(lsx_ind … H) -L +#L1 #_ #IHL1 @lsx_intro +#L2 #HL12 #HV @IHL1 /3 width=4 by lleq_fwd_bind_sn/ +qed-. + +lemma lsx_fwd_flat_sn: ∀h,g,I,G,L,V,T. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T] L → + G ⊢ ⋕⬊*[h, g, V] L. +#h #g #I #G #L #V #T #H @(lsx_ind … H) -L +#L1 #_ #IHL1 @lsx_intro +#L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_sn/ +qed-. + +lemma lsx_fwd_flat_dx: ∀h,g,I,G,L,V,T. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T] L → + G ⊢ ⋕⬊*[h, g, T] L. +#h #g #I #G #L #V #T #H @(lsx_ind … H) -L +#L1 #_ #IHL1 @lsx_intro +#L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_dx/ +qed-. + +lemma lsx_fwd_pair_sn: ∀h,g,I,G,L,V,T. G ⊢ ⋕⬊*[h, g, ②{I}V.T] L → + G ⊢ ⋕⬊*[h, g, V] L. +#h #g * /2 width=4 by lsx_fwd_bind_sn, lsx_fwd_flat_sn/ +qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma lsx_inv_flat: ∀h,g,I,G,L,V,T. G ⊢ ⋕⬊*[h, g, ⓕ{I}V.T] L → + G ⊢ ⋕⬊*[h, g, V] L ∧ G ⊢ ⋕⬊*[h, g, T] L. +/3 width=3 by lsx_fwd_flat_sn, lsx_fwd_flat_dx, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma index 48786e5e2..670fb9473 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma @@ -14,20 +14,46 @@ include "basic_2/computation/lpxs_lleq.ma". include "basic_2/computation/csx_alt.ma". -include "basic_2/computation/lsx.ma". +include "basic_2/computation/lsx_lpxs.ma". (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) -(* Main properties **********************************************************) +(* Advanced forward lemmas **************************************************) +(* +lemma lsx_fwd_bind_dx_lpxs: ∀h,g,a,I,G,L1,V. ⦃G, L1⦄ ⊢ ⬊*[h, g] V → + ∀L2,T. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → + G ⊢ ⋕⬊*[h, g, T] L2.ⓑ{I}V. +#h #g #a #I #G #L1 #V #H @(csx_ind_alt … H) -V +#V1 #_ #IHV1 #L2 #T #H @(lsx_ind … H) -L2 +#L2 #HL2 #IHL2 #HL12 @lsx_intro +#Y #H #HnT elim (lpxs_inv_pair1 … H) -H +#L3 #V3 #HL23 #HV13 #H destruct +lapply (lpxs_trans … HL12 … HL23) #HL13 +elim (eq_term_dec V1 V3) +[ -HV13 -HL2 -IHV1 -HL12 #H destruct + @IHL2 -IHL2 // -HL23 -HL13 /3 width=2 by lleq_fwd_bind_O/ +| -IHL2 -HL23 -HnT #HnV13 + @(IHV1 … HnV13) -IHV1 -HnV13 /2 width=3 by lpxs_cpxs_trans/ -HL12 -HL13 -HV13 + @(lsx_lpxs_trans) … HL2) +*) -axiom csx_lsx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → G ⊢ ⋕⬊*[h, g, T] L. +(* Advanced inversion lemmas ************************************************) -axiom lsx_inv_csx: ∀h,g,G,L,T. G ⊢ ⋕⬊*[h, g, T] L → ⦃G, L⦄ ⊢ ⬊*[h, g] T. + +(* Main properties **********************************************************) + +axiom csx_lsx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → G ⊢ ⋕⬊*[h, g, T] L. (* -#h #g #G #L1 #T1 #H @(csx_ind_alt … H) -T1 -#T1 #_ #IHT1 @lsx_intro -#L2 #HL12 #HnT1 elim (lpxs_inv_cpxs_nlleq … HL12 HnT1) -HL12 -HnT1 -#T2 #H1T12 #HnT12 #H2T12 lapply (IHT1 … H1T12 HnT12) -IHT1 -H1T12 -HnT12 -#HT2 +#h #g #G #L #T @(fqup_wf_ind_eq … G L T) -G -L -T +#G1 #L1 #T1 #IH #G2 #L2 * * +[ #k #HG #HL #HT destruct // +| #i #HG #HL #HT destruct + #H +| #p #HG #HL #HT destruct // +| #a #I #V2 #T2 #HG #HL #HT #H destruct + elim (csx_fwd_bind … H) -H + #HV2 #HT2 +| #I #V2 #T2 #HG #HL #HT #H destruct + elim (csx_fwd_flat … H) -H /3 width=1 by lsx_flat/ *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma similarity index 61% rename from matita/matita/contribs/lambdadelta/basic_2/computation/lsx_cpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma index c877a9193..1f1ebc834 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/computation/lpxs_lleq.ma". +include "basic_2/computation/lpxs_lpxs.ma". include "basic_2/computation/lsx.ma". (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) @@ -21,8 +22,10 @@ include "basic_2/computation/lsx.ma". lemma lsx_lleq_trans: ∀h,g,T,G,L1. G ⊢ ⋕⬊*[h, g, T] L1 → ∀L2. L1 ⋕[T, 0] L2 → G ⊢ ⋕⬊*[h, g, T] L2. -#h #g #T #G #L1 #H @(lsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12 -@lsx_intro #L #HL2 #HnT elim (lleq_lpxs_trans_nlleq … HL12 … HL2 HnT) -L2 /3 width=4 by/ +#h #g #T #G #L1 #H @(lsx_ind … H) -L1 +#L1 #_ #IHL1 #L2 #HL12 @lsx_intro +#K2 #HLK2 #HnLK2 elim (lleq_lpxs_trans … HL12 … HLK2) -HLK2 +/5 width=4 by lleq_canc_sn, lleq_trans/ qed-. lemma lsx_lpxs_trans: ∀h,g,T,G,L1. G ⊢ ⋕⬊*[h, g, T] L1 → @@ -30,3 +33,22 @@ lemma lsx_lpxs_trans: ∀h,g,T,G,L1. G ⊢ ⋕⬊*[h, g, T] L1 → #h #g #T #G #L1 #H @(lsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12 elim (lleq_dec T L1 L2 0) /3 width=4 by lsx_lleq_trans/ qed-. + +lemma lsx_flat_lpxs: ∀h,g,I,G,L1,V. G ⊢ ⋕⬊*[h, g, V] L1 → + ∀L2,T. G ⊢ ⋕⬊*[h, g, T] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → + G ⊢ ⋕⬊*[h, g, ⓕ{I}T.V] L2. +#h #g #I #G #L1 #V #H @(lsx_ind … H) -L1 +#L1 #HL1 #IHL1 #L2 #T #H @(lsx_ind … H) -L2 +#L2 #HL2 #IHL2 #HL12 @lsx_intro +#L0 #HL20 lapply (lpxs_trans … HL12 … HL20) +#HL10 #H elim (nlleq_inv_flat … H) -H [ -HL2 -IHL1 | -HL1 -IHL2 ] +[ /3 width=1 by/ +| #HnV elim (lleq_dec V L1 L2 0) + [ #HV @(IHL1 … L0) /3 width=3 by lsx_lpxs_trans, lleq_canc_sn/ (**) (* full auto too slow: 47s *) + | -HnV -HL10 /3 width=4 by lsx_lpxs_trans/ +] +qed-. + +lemma lsx_flat: ∀h,g,I,G,L,V. G ⊢ ⋕⬊*[h, g, V] L → + ∀T. G ⊢ ⋕⬊*[h, g, T] L → G ⊢ ⋕⬊*[h, g, ⓕ{I}T.V] L. +/2 width=3 by lsx_flat_lpxs/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma index c3b0ae106..bc56f721e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lleq_alt.ma". +include "basic_2/substitution/lleq_ext.ma". include "basic_2/reduction/cpx.ma". (* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) @@ -55,7 +55,7 @@ lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2 @(lleq_lift_le … HLK1 HLK2 … HVW2) -HLK1 -HLK2 -HVW2 /2 width=1 by/ (**) (* full auto too slow *) | #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_bind_O … H) -H - /4 width=3 by lleq_bind_repl_SO, lleq_bind/ + /4 width=5 by lleq_bind_repl_SO, lleq_bind/ | #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H /3 width=1 by lleq_flat/ | #G #L2 #V #T1 #T2 #T #_ #HT2 #IHT12 #L1 #H elim (lleq_inv_bind_O … H) -H @@ -64,7 +64,7 @@ lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → | #G #L2 #V1 #V2 #T #_ #IHV12 #L1 #H elim (lleq_inv_flat … H) -H /2 width=1 by/ | #a #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H #HV1 #H elim (lleq_inv_bind_O … H) -H - /4 width=3 by lleq_bind_repl_SO, lleq_flat, lleq_bind/ + /4 width=5 by lleq_bind_repl_SO, lleq_flat, lleq_bind/ | #a #G #L2 #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H #HV1 #H elim (lleq_inv_bind_O … H) -H #HW1 #HT1 @lleq_bind_O /2 width=1 by/ @lleq_flat (**) (* full auto too slow *) 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 7c7bbed03..d188a5389 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lleq_alt.ma". +include "basic_2/substitution/lleq_ext.ma". include "basic_2/reduction/lpx_ldrop.ma". (* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma index 9f355b2d9..0d99e8e1e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma @@ -80,62 +80,3 @@ lemma lleq_ind_alt: ∀R:relation4 ynat term lenv lenv. ( #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #T #L1 #L2 #H elim (lleq_lleqa … H) -H /3 width=9 by lleqa_inv_lleq/ qed-. - -(* Advanced inversion lemmas ************************************************) - -fact lleq_inv_S_aux: ∀L1,L2,T,d0. L1 ⋕[T, d0] L2 → ∀d. d0 = d + 1 → - ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V → - K1 ⋕[V, 0] K2 → L1 ⋕[T, d] L2. -#L1 #L2 #T #d0 #H @(lleq_ind_alt … H) -L1 -L2 -T -d0 -/2 width=1 by lleq_gref, lleq_free, lleq_sort/ -[ #L1 #L2 #d0 #i #HL12 #Hid #d #H #K1 #K2 #I #V #HLK1 #HLK2 #HV destruct - elim (yle_split_eq i d) /2 width=1 by lleq_skip, ylt_fwd_succ2/ -HL12 -Hid - #H destruct /2 width=8 by lleq_lref/ -| #I1 #I2 #L1 #L2 #K11 #K22 #V #d0 #i #Hd0i #HLK11 #HLK22 #HV #_ #d #H #K1 #K2 #J #W #_ #_ #_ destruct - /3 width=8 by lleq_lref, yle_pred_sn/ -| #a #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct - /4 width=7 by lleq_bind, ldrop_ldrop/ -| #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct - /3 width=7 by lleq_flat/ -] -qed-. - -lemma lleq_inv_S: ∀T,L1,L2,d. L1 ⋕[T, d+1] L2 → - ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V → - K1 ⋕[V, 0] K2 → L1 ⋕[T, d] L2. -/2 width=7 by lleq_inv_S_aux/ qed-. - -lemma lleq_inv_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[ⓑ{a,I}V.T, 0] L2 → - L1 ⋕[V, 0] L2 ∧ L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V. -#a #I #L1 #L2 #V #T #H elim (lleq_inv_bind … H) -H -/3 width=7 by ldrop_pair, conj, lleq_inv_S/ -qed-. - -(* Advanced properties ******************************************************) - -lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[T, d1] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[T, d2] L2. -#L1 #L2 #T #d1 #H @(lleq_ind_alt … H) -L1 -L2 -T -d1 -/4 width=1 by lleq_sort, lleq_free, lleq_gref, lleq_bind, lleq_flat, yle_succ/ -[ /3 width=3 by lleq_skip, ylt_yle_trans/ -| #I1 #I2 #L1 #L2 #K1 #K2 #V #d1 #i #Hi #HLK1 #HLK2 #HV #IHV #d2 #Hd12 elim (ylt_split i d2) - [ lapply (lleq_fwd_length … HV) #HK12 #Hid2 - lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2) - normalize in ⊢ (%→%→?); -I1 -I2 -V -d1 /2 width=1 by lleq_skip/ - | /3 width=8 by lleq_lref, yle_trans/ - ] -] -qed-. - -lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[V, 0] L2 → L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V → - L1 ⋕[ⓑ{a,I}V.T, 0] L2. -/3 width=3 by lleq_ge, lleq_bind/ qed. - -lemma lleq_bind_repl_SO: ∀I,L1,L2,V,T. L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V → - ∀J,W. L1.ⓑ{J}W ⋕[T, 1] L2.ⓑ{J}W. -#I #L1 #L2 #V #T #HT #J #W lapply (lleq_ge … HT 1 ?) // -HT -#HT @(lleq_lsuby_repl … HT) /2 width=1 by lsuby_succ/ (**) (* full auto fails *) -qed-. - -lemma lleq_bind_repl_O: ∀I,L1,L2,V,T. L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V → - ∀J,W. L1 ⋕[W, 0] L2 → L1.ⓑ{J}W ⋕[T, 0] L2.ⓑ{J}W. -/3 width=7 by lleq_bind_repl_SO, lleq_inv_S/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma new file mode 100644 index 000000000..a1cf4458d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma @@ -0,0 +1,91 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lleq_alt.ma". + +(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) + +(* Advanced inversion lemmas ************************************************) + +fact lleq_inv_S_aux: ∀L1,L2,T,d0. L1 ⋕[T, d0] L2 → ∀d. d0 = d + 1 → + ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V → + K1 ⋕[V, 0] K2 → L1 ⋕[T, d] L2. +#L1 #L2 #T #d0 #H @(lleq_ind_alt … H) -L1 -L2 -T -d0 +/2 width=1 by lleq_gref, lleq_free, lleq_sort/ +[ #L1 #L2 #d0 #i #HL12 #Hid #d #H #K1 #K2 #I #V #HLK1 #HLK2 #HV destruct + elim (yle_split_eq i d) /2 width=1 by lleq_skip, ylt_fwd_succ2/ -HL12 -Hid + #H destruct /2 width=8 by lleq_lref/ +| #I1 #I2 #L1 #L2 #K11 #K22 #V #d0 #i #Hd0i #HLK11 #HLK22 #HV #_ #d #H #K1 #K2 #J #W #_ #_ #_ destruct + /3 width=8 by lleq_lref, yle_pred_sn/ +| #a #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct + /4 width=7 by lleq_bind, ldrop_ldrop/ +| #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct + /3 width=7 by lleq_flat/ +] +qed-. + +lemma lleq_inv_S: ∀T,L1,L2,d. L1 ⋕[T, d+1] L2 → + ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V → + K1 ⋕[V, 0] K2 → L1 ⋕[T, d] L2. +/2 width=7 by lleq_inv_S_aux/ qed-. + +lemma lleq_inv_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[ⓑ{a,I}V.T, 0] L2 → + L1 ⋕[V, 0] L2 ∧ L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V. +#a #I #L1 #L2 #V #T #H elim (lleq_inv_bind … H) -H +/3 width=7 by ldrop_pair, conj, lleq_inv_S/ +qed-. + +(* Advanced forward lemmas **************************************************) + +lemma lleq_fwd_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[ⓑ{a,I}V.T, 0] L2 → + L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V. +#a #I #L1 #L2 #V #T #H elim (lleq_inv_bind_O … H) -H // +qed-. + +(* Advanced properties ******************************************************) + +lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[T, d1] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[T, d2] L2. +#L1 #L2 #T #d1 #H @(lleq_ind_alt … H) -L1 -L2 -T -d1 +/4 width=1 by lleq_sort, lleq_free, lleq_gref, lleq_bind, lleq_flat, yle_succ/ +[ /3 width=3 by lleq_skip, ylt_yle_trans/ +| #I1 #I2 #L1 #L2 #K1 #K2 #V #d1 #i #Hi #HLK1 #HLK2 #HV #IHV #d2 #Hd12 elim (ylt_split i d2) + [ lapply (lleq_fwd_length … HV) #HK12 #Hid2 + lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2) + normalize in ⊢ (%→%→?); -I1 -I2 -V -d1 /2 width=1 by lleq_skip/ + | /3 width=8 by lleq_lref, yle_trans/ + ] +] +qed-. + +lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[V, 0] L2 → L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V → + L1 ⋕[ⓑ{a,I}V.T, 0] L2. +/3 width=3 by lleq_ge, lleq_bind/ qed. + +lemma lleq_bind_repl_SO: ∀I1,I2,L1,L2,V1,V2,T. L1.ⓑ{I1}V1 ⋕[T, 0] L2.ⓑ{I2}V2 → + ∀J1,J2,W1,W2. L1.ⓑ{J1}W1 ⋕[T, 1] L2.ⓑ{J2}W2. +#I1 #I2 #L1 #L2 #V1 #V2 #T #HT #J1 #J2 #W1 #W2 lapply (lleq_ge … HT 1 ?) // -HT +#HT @(lleq_lsuby_repl … HT) /2 width=1 by lsuby_succ/ (**) (* full auto fails *) +qed-. + +lemma lleq_bind_repl_O: ∀I,L1,L2,V,T. L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V → + ∀J,W. L1 ⋕[W, 0] L2 → L1.ⓑ{J}W ⋕[T, 0] L2.ⓑ{J}W. +/3 width=7 by lleq_bind_repl_SO, lleq_inv_S/ qed-. + +(* Inversion lemmas on negated lazy quivalence for local environments *******) + +lemma nlleq_inv_bind_O: ∀a,I,L1,L2,V,T. (L1 ⋕[ⓑ{a,I}V.T, 0] L2 → ⊥) → + (L1 ⋕[V, 0] L2 → ⊥) ∨ (L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V → ⊥). +#a #I #L1 #L2 #V #T #H elim (lleq_dec V L1 L2 0) +/4 width=1 by lleq_bind_O, or_intror, or_introl/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma index e4c64833f..18744a539 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/substitution/fqus_alt.ma". -include "basic_2/substitution/lleq_alt.ma". +include "basic_2/substitution/lleq_ext.ma". (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma index 0694be69c..97f2dd675 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma @@ -137,3 +137,23 @@ theorem lleq_canc_sn: ∀L,L1,L2,T,d. L ⋕[d, T] L1→ L ⋕[d, T] L2 → L1 theorem lleq_canc_dx: ∀L1,L2,L,T,d. L1 ⋕[d, T] L → L2 ⋕[d, T] L → L1 ⋕[d, T] L2. /3 width=3 by lleq_trans, lleq_sym/ qed-. + +(* Inversion lemmas on negated lazy quivalence for local environments *******) + +lemma nlleq_inv_bind: ∀a,I,L1,L2,V,T,d. (L1 ⋕[ⓑ{a,I}V.T, d] L2 → ⊥) → + (L1 ⋕[V, d] L2 → ⊥) ∨ (L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V → ⊥). +#a #I #L1 #L2 #V #T #d #H elim (lleq_dec V L1 L2 d) +/4 width=1 by lleq_bind, or_intror, or_introl/ +qed-. + +lemma nlleq_inv_flat: ∀I,L1,L2,V,T,d. (L1 ⋕[ⓕ{I}V.T, d] L2 → ⊥) → + (L1 ⋕[V, d] L2 → ⊥) ∨ (L1 ⋕[T, d] L2 → ⊥). +#I #L1 #L2 #V #T #d #H elim (lleq_dec V L1 L2 d) +/4 width=1 by lleq_flat, or_intror, or_introl/ +qed-. + +(* Note: lleq_nlleq_trans: ∀d,T,L1,L. L1⋕[T, d] L → + ∀L2. (L ⋕[T, d] L2 → ⊥) → (L1 ⋕[T, d] L2 → ⊥). +/3 width=3 by lleq_canc_sn/ qed-. +works with /4 width=8/ so lleq_canc_sn is more convenient +*) 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 e920ea057..920657dd2 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 @@ -209,7 +209,7 @@ table { class "yellow" [ { "substitution" * } { [ { "lazy equivalence for local environments" * } { - [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt ( ? ⋕⋕[?,?] ? )" "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" * ] + [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt ( ? ⋕⋕[?,?] ? )" "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" + "lleq_ext" * ] } ] [ { "contxt-sensitive extended multiple substitution" * } { -- 2.39.2