From ec261374a2990bebeded039a64c0be0795ad9e93 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 29 May 2018 15:26:17 +0200 Subject: [PATCH] partial commit in basic_2 + rdsx (was lsx) reconstructed: replaces lfsx --- .../lambdadelta/basic_2/etc/lsx/lsx.etc | 6 +- .../lfsx.ma => etc/referred/lfsx.etc} | 0 .../lfsx_csx.ma => etc/referred/lfsx_csx.etc} | 0 .../referred/lfsx_drops.etc} | 0 .../referred/lfsx_fqup.etc} | 0 .../referred/lfsx_lfpxs.etc} | 0 .../referred/lfsx_lfsx.etc} | 0 .../lfsx_lpx.ma => etc/referred/lfsx_lpx.etc} | 0 .../referred/lfsx_lpxs.etc} | 0 .../basic_2/rt_computation/lfprs_lfpxs.ma | 3 - .../{lfprs_aaa.ma => lprs_aaa.ma} | 0 .../basic_2/rt_computation/lprs_lpxs.ma | 4 + .../basic_2/rt_computation/lsubsx.ma | 2 +- .../{lsubsx_lfsx.ma => lsubsx_rdsx.ma} | 60 +++---- .../basic_2/rt_computation/partial.txt | 2 +- .../basic_2/rt_computation/rdsx.ma | 94 +++++++++++ .../basic_2/rt_computation/rdsx_csx.ma | 72 ++++++++ .../basic_2/rt_computation/rdsx_drops.ma | 66 ++++++++ .../basic_2/rt_computation/rdsx_fqup.ma | 50 ++++++ .../basic_2/rt_computation/rdsx_length.ma | 40 +++++ .../basic_2/rt_computation/rdsx_lpxs.ma | 154 +++++++++++++++++ .../basic_2/rt_computation/rdsx_rdsx.ma | 38 +++++ .../lambdadelta/basic_2/static/lfdeq.ma | 124 +++++++------- .../basic_2/static/lfdeq_length.ma | 23 ++- .../lambdadelta/basic_2/static/lfxs.ma | 158 +++++++++--------- .../lambdadelta/basic_2/static/lfxs_length.ma | 43 +++-- .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 27 files changed, 741 insertions(+), 200 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfsx.ma => etc/referred/lfsx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfsx_csx.ma => etc/referred/lfsx_csx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfsx_drops.ma => etc/referred/lfsx_drops.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfsx_fqup.ma => etc/referred/lfsx_fqup.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfsx_lfpxs.ma => etc/referred/lfsx_lfpxs.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfsx_lfsx.ma => etc/referred/lfsx_lfsx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfsx_lpx.ma => etc/referred/lfsx_lpx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfsx_lpxs.ma => etc/referred/lfsx_lpxs.etc} (100%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfprs_lfpxs.ma rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{lfprs_aaa.ma => lprs_aaa.ma} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpxs.ma rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{lsubsx_lfsx.ma => lsubsx_rdsx.ma} (54%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_csx.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_drops.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_fqup.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_length.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_lpxs.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_rdsx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsx/lsx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsx/lsx.etc index b5407abdf..f09dc1da8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lsx/lsx.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsx/lsx.etc @@ -6,7 +6,7 @@ lemma lsx_lreq_conf: ∀h,o,G,L1,T,l. G ⊢ ⬊*[h, o, T, l] L1 → #L0 #HL03 #HL10 #H elim (H T) -H /4 width=4 by/ qed-. -(* these two are better expressed with the binder \chi *) +(* this is better expressed with the binder \chi *) lemma lsx_fwd_bind_dx: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓑ{a,I}V.T, l] L → G ⊢ ⬈*[h, o, T, ⫯l] L.ⓑ{I}V. @@ -19,7 +19,3 @@ lemma lsx_fwd_bind_dx: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓑ{a,I}V.T, l] L @(lleq_lreq_trans … (L2.ⓑ{I}V1)) /2 width=2 by lleq_fwd_bind_dx, lreq_succ/ qed-. - -lemma lsx_inv_bind: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓑ{a, I}V.T, l] L → - G ⊢ ⬈*[h, o, V, l] L ∧ G ⊢ ⬈*[h, o, T, ⫯l] L.ⓑ{I}V. -/3 width=4 by lsx_fwd_bind_sn, lsx_fwd_bind_dx, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfsx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfsx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfsx_csx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfsx_csx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfsx_drops.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_drops.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfsx_drops.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfsx_fqup.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqup.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfsx_fqup.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfsx_lfpxs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfsx_lfpxs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfsx_lfsx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfsx_lfsx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfsx_lpx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpx.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfsx_lpx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfsx_lpxs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfsx_lpxs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfprs_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfprs_lfpxs.ma deleted file mode 100644 index 8c8679a47..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfprs_lfpxs.ma +++ /dev/null @@ -1,3 +0,0 @@ -(* Basic_2A1: was just: lprs_lpxs *) -lemma lprs_lfpxs: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2. -/3 width=3 by lpr_lpx, monotonic_TC/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_aaa.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfprs_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_aaa.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpxs.ma new file mode 100644 index 000000000..3844f8620 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpxs.ma @@ -0,0 +1,4 @@ +include "basic_2/rt_computation/lprs.ma". + +lemma lprs_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2. +/3 width=3 by lpr_lpx, monotonic_TC/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx.ma index d7d552461..66104ff6a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/lsubeqx_6.ma". -include "basic_2/rt_computation/lfsx.ma". +include "basic_2/rt_computation/rdsx.ma". (* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNBOUND RT-TRANSITION **********) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_rdsx.ma similarity index 54% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_rdsx.ma index 511e62369..5448d58ff 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_rdsx.ma @@ -12,62 +12,62 @@ (* *) (**************************************************************************) -include "basic_2/rt_computation/lfsx_drops.ma". -include "basic_2/rt_computation/lfsx_lfpxs.ma". +include "basic_2/rt_computation/rdsx_drops.ma". +include "basic_2/rt_computation/rdsx_lpxs.ma". include "basic_2/rt_computation/lsubsx.ma". (* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNBOUND RT-TRANSITION **********) -(* Properties with strong normalizing env's for unbound rt-transition *******) +(* Properties with strongly normalizing referred local environments *********) (* Basic_2A1: uses: lsx_cpx_trans_lcosx *) -lemma lfsx_cpx_trans_lsubsx: ∀h,o,G,L0,T1,T2. ⦃G, L0⦄ ⊢ T1 ⬈[h] T2 → - ∀f,L. G ⊢ L0 ⊆ⓧ[h, o, f] L → - G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄. +lemma rdsx_cpx_trans_lsubsx (h) (o): ∀G,L0,T1,T2. ⦃G, L0⦄ ⊢ T1 ⬈[h] T2 → + ∀f,L. G ⊢ L0 ⊆ⓧ[h, o, f] L → + G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄. #h #o #G #L0 #T1 #T2 #H @(cpx_ind … H) -G -L0 -T1 -T2 // [ #I0 #G #K0 #V1 #V2 #W2 #_ #IH #HVW2 #g #L #HK0 #HL elim (lsubsx_inv_pair_sn_gen … HK0) -HK0 * [ #f #K #HK0 #H1 #H2 destruct - /4 width=8 by lfsx_lifts, lfsx_fwd_pair, drops_refl, drops_drop/ + /4 width=8 by rdsx_lifts, rdsx_fwd_pair, drops_refl, drops_drop/ | #f #K #HV1 #HK0 #H1 #H2 destruct - /4 width=8 by lfsx_lifts, drops_refl, drops_drop/ + /4 width=8 by rdsx_lifts, drops_refl, drops_drop/ ] | #I0 #G #K0 #T #U #i #_ #IH #HTU #g #L #HK0 #HL elim (lsubsx_fwd_bind_sn … HK0) -HK0 #I #K #HK0 #H destruct - /6 width=8 by lfsx_inv_lifts, lfsx_lifts, drops_refl, drops_drop/ + /6 width=8 by rdsx_inv_lifts, rdsx_lifts, drops_refl, drops_drop/ | #p #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #f #L #HL0 #HL - elim (lfsx_inv_bind … HL) -HL - /4 width=2 by lsubsx_pair, lfsx_bind_void/ + elim (rdsx_inv_bind … HL) -HL + /4 width=2 by lsubsx_pair, rdsx_bind_void/ | #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #f #L #HL0 #HL - elim (lfsx_inv_flat … HL) -HL /3 width=2 by lfsx_flat/ + elim (rdsx_inv_flat … HL) -HL /3 width=2 by rdsx_flat/ | #G #L0 #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #f #L #HL0 #HL - elim (lfsx_inv_bind … HL) -HL #HV #HU1 - /4 width=8 by lsubsx_pair, lfsx_inv_lifts, drops_refl, drops_drop/ + elim (rdsx_inv_bind … HL) -HL #HV #HU1 + /4 width=8 by lsubsx_pair, rdsx_inv_lifts, drops_refl, drops_drop/ | #G #L0 #V #T1 #T2 #_ #IHT12 #f #L #HL0 #HL - elim (lfsx_inv_flat … HL) -HL /2 width=2 by/ + elim (rdsx_inv_flat … HL) -HL /2 width=2 by/ | #G #L0 #V1 #V2 #T #_ #IHV12 #f #L #HL0 #HL - elim (lfsx_inv_flat … HL) -HL /2 width=2 by/ + elim (rdsx_inv_flat … HL) -HL /2 width=2 by/ | #p #G #L0 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #f #L #HL0 #HL - elim (lfsx_inv_flat … HL) -HL #HV1 #HL - elim (lfsx_inv_bind … HL) -HL #HW1 #HT1 - /4 width=2 by lsubsx_pair, lfsx_bind_void, lfsx_flat/ + elim (rdsx_inv_flat … HL) -HL #HV1 #HL + elim (rdsx_inv_bind … HL) -HL #HW1 #HT1 + /4 width=2 by lsubsx_pair, rdsx_bind_void, rdsx_flat/ | #p #G #L0 #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #HVU2 #f #L #HL0 #HL - elim (lfsx_inv_flat … HL) -HL #HV1 #HL - elim (lfsx_inv_bind … HL) -HL #HW1 #HT1 - /6 width=8 by lsubsx_pair, lfsx_lifts, lfsx_bind_void, lfsx_flat, drops_refl, drops_drop/ + elim (rdsx_inv_flat … HL) -HL #HV1 #HL + elim (rdsx_inv_bind … HL) -HL #HW1 #HT1 + /6 width=8 by lsubsx_pair, rdsx_lifts, rdsx_bind_void, rdsx_flat, drops_refl, drops_drop/ ] qed-. -(* Basic_2A1: uses: lsx_cpx_trans_O *) -lemma lfsx_cpx_trans: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → - G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄. -/3 width=6 by lfsx_cpx_trans_lsubsx, lsubsx_refl/ qed-. +(* Advanced properties of strongly normalizing referred local environments **) -(* Properties with strong normalizing env's for unbound rt-computation ******) +(* Basic_2A1: uses: lsx_cpx_trans_O *) +lemma rdsx_cpx_trans (h) (o): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → + G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄. +/3 width=6 by rdsx_cpx_trans_lsubsx, lsubsx_refl/ qed-. -lemma lfsx_cpxs_trans: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → - G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄. +lemma rdsx_cpxs_trans (h) (o): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → + G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄. #h #o #G #L #T1 #T2 #H @(cpxs_ind_dx ???????? H) -T1 // -/3 width=3 by lfsx_cpx_trans/ +/3 width=3 by rdsx_cpx_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 05ddbc263..4092f79d3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -3,7 +3,7 @@ cpxs_ext.ma lpxs.ma lpxs_length.ma lpxs_drops.ma lpxs_lfdeq.ma lpxs_ffdeq.ma lpxs_aaa.ma lpxs_lpx.ma lpxs_cpxs.ma lpxs_lpxs.ma csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_fqus.ma csx_lsubr.ma csx_lfdeq.ma csx_ffdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_fpbq.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma -lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lpx.ma lfsx_lpxs.ma lfsx_lfpxs.ma lfsx_csx.ma lfsx_lfsx.ma +rdsx.ma rdsx_length.ma rdsx_drops.ma rdsx_fqup.ma rdsx_lpxs.ma rdsx_csx.ma rdsx_rdsx.ma lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma fpbs.ma fpbs_fqup.ma fpbs_fqus.ma fpbs_aaa.ma fpbs_cpx.ma fpbs_fpb.ma fpbs_cpxs.ma fpbs_lpxs.ma fpbs_lfpxs.ma fpbs_csx.ma fpbs_fpbs.ma fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_lfpxs.ma fpbg_fpbs.ma fpbg_fpbg.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx.ma new file mode 100644 index 000000000..ff62c4d6b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx.ma @@ -0,0 +1,94 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/predtysnstrong_5.ma". +include "basic_2/static/lfdeq.ma". +include "basic_2/rt_transition/lpx.ma". + +(* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******) + +definition rdsx (h) (o) (G) (T): predicate lenv ≝ + SN … (lpx h G) (lfdeq h o T). + +interpretation + "strong normalization for unbound context-sensitive parallel rt-transition on referred entries (local environment)" + 'PRedTySNStrong h o T G L = (rdsx h o G T L). + +(* Basic eliminators ********************************************************) + +(* Basic_2A1: uses: lsx_ind *) +lemma rdsx_ind (h) (o) (G) (T): + ∀R:predicate lenv. + (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → + (∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) → + R L1 + ) → + ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L. +#h #o #G #T #R #H0 #L1 #H elim H -L1 +/5 width=1 by SN_intro/ +qed-. + +(* Basic properties *********************************************************) + +(* Basic_2A1: uses: lsx_intro *) +lemma rdsx_intro (h) (o) (G) (T): + ∀L1. + (∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) → + G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄. +/5 width=1 by SN_intro/ qed. + +(* Basic forward lemmas *****************************************************) + +(* Basic_2A1: uses: lsx_fwd_pair_sn lsx_fwd_bind_sn lsx_fwd_flat_sn *) +lemma rdsx_fwd_pair_sn (h) (o) (G): + ∀I,L,V,T. G ⊢ ⬈*[h, o, ②{I}V.T] 𝐒⦃L⦄ → + G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄. +#h #o #G #I #L #V #T #H +@(rdsx_ind … H) -L #L1 #_ #IHL1 +@rdsx_intro #L2 #HL12 #HnL12 +/4 width=3 by lfdeq_fwd_pair_sn/ +qed-. + +(* Basic_2A1: uses: lsx_fwd_flat_dx *) +lemma rdsx_fwd_flat_dx (h) (o) (G): + ∀I,L,V,T. G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L⦄ → + G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄. +#h #o #G #I #L #V #T #H +@(rdsx_ind … H) -L #L1 #_ #IHL1 +@rdsx_intro #L2 #HL12 #HnL12 +/4 width=3 by lfdeq_fwd_flat_dx/ +qed-. + +fact rdsx_fwd_pair_aux (h) (o) (G): ∀L. G ⊢ ⬈*[h, o, #0] 𝐒⦃L⦄ → + ∀I,K,V. L = K.ⓑ{I}V → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄. +#h #o #G #L #H +@(rdsx_ind … H) -L #L1 #_ #IH #I #K1 #V #H destruct +/5 width=5 by lpx_pair, rdsx_intro, lfdeq_fwd_zero_pair/ +qed-. + +lemma rdsx_fwd_pair (h) (o) (G): + ∀I,K,V. G ⊢ ⬈*[h, o, #0] 𝐒⦃K.ⓑ{I}V⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄. +/2 width=4 by rdsx_fwd_pair_aux/ qed-. + +(* Basic inversion lemmas ***************************************************) + +(* Basic_2A1: uses: lsx_inv_flat *) +lemma rdsx_inv_flat (h) (o) (G): ∀I,L,V,T. G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L⦄ → + ∧∧ G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ & G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄. +/3 width=3 by rdsx_fwd_pair_sn, rdsx_fwd_flat_dx, conj/ qed-. + +(* Basic_2A1: removed theorems 9: + lsx_ge_up lsx_ge + lsxa_ind lsxa_intro lsxa_lleq_trans lsxa_lpxs_trans lsxa_intro_lpx lsx_lsxa lsxa_inv_lsx +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_csx.ma new file mode 100644 index 000000000..390ebe3ce --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_csx.ma @@ -0,0 +1,72 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_computation/csx_lsubr.ma". +include "basic_2/rt_computation/csx_cpxs.ma". +include "basic_2/rt_computation/lsubsx_rdsx.ma". + +(* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******) + +(* Advanced properties ******************************************************) + +(* Basic_2A1: uses: lsx_lref_be_lpxs *) +lemma rdsx_pair_lpxs (h) (o) (G): + ∀K1,V. ⦃G, K1⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → + ∀K2. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ → ⦃G, K1⦄ ⊢ ⬈*[h] K2 → + ∀I. G ⊢ ⬈*[h, o, #0] 𝐒⦃K2.ⓑ{I}V⦄. +#h #o #G #K1 #V #H +@(csx_ind_cpxs … H) -V #V0 #_ #IHV0 #K2 #H +@(rdsx_ind … H) -K2 #K0 #HK0 #IHK0 #HK10 #I +@rdsx_intro #Y #HY #HnY +elim (lpx_inv_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct +elim (tdeq_dec h o V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 | -IHK0 -HnY ] +[ /5 width=5 by rdsx_lfdeq_trans, lpxs_step_dx, lfdeq_pair/ +| @(IHV0 … HnV02) -IHV0 -HnV02 + [ /2 width=3 by lpxs_cpx_trans/ + | /3 width=3 by rdsx_lpx_trans, rdsx_cpx_trans/ + | /2 width=3 by lpxs_step_dx/ + ] +] +qed. + +(* Basic_2A1: uses: lsx_lref_be *) +lemma rdsx_lref_pair_drops (h) (o) (G): + ∀K,V. ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄ → + ∀I,i,L. ⬇*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄. +#h #o #G #K #V #HV #HK #I #i elim i -i +[ #L #H >(drops_fwd_isid … H) -H /2 width=3 by rdsx_pair_lpxs/ +| #i #IH #L #H + elim (drops_inv_bind2_isuni_next … H) -H // #J #Y #HY #H destruct + @(rdsx_lifts … (𝐔❴1❵)) /3 width=6 by drops_refl, drops_drop/ (**) (* full auto fails *) +] +qed. + +(* Main properties **********************************************************) + +(* Basic_2A1: uses: csx_lsx *) +theorem csx_rdsx (h) (o): ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄. +#h #o #G #L #T @(fqup_wf_ind_eq (Ⓕ) … G L T) -G -L -T +#Z #Y #X #IH #G #L * * // +[ #i #HG #HL #HT #H destruct + elim (csx_inv_lref … H) -H [ |*: * ] + [ /2 width=1 by rdsx_lref_atom/ + | /2 width=3 by rdsx_lref_unit/ + | /4 width=6 by rdsx_lref_pair_drops, fqup_lref/ + ] +| #p #I #V #T #HG #HL #HT #H destruct + elim (csx_fwd_bind_unit … H Void) -H /3 width=1 by rdsx_bind_void/ +| #I #V #T #HG #HL #HT #H destruct + elim (csx_fwd_flat … H) -H /3 width=1 by rdsx_flat/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_drops.ma new file mode 100644 index 000000000..db1bd5144 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_drops.ma @@ -0,0 +1,66 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/lfdeq_drops.ma". +include "basic_2/rt_transition/lpx_drops.ma". +include "basic_2/rt_computation/rdsx_length.ma". +include "basic_2/rt_computation/rdsx_fqup.ma". + +(* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******) + +(* Properties with generic relocation ***************************************) + +(* Note: this uses length *) +(* Basic_2A1: uses: lsx_lift_le lsx_lift_ge *) +lemma rdsx_lifts (h) (o) (G): d_liftable1_isuni … (λL,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄). +#h #o #G #K #T #H @(rdsx_ind … H) -K +#K1 #_ #IH #b #f #L1 #HLK1 #Hf #U #HTU @rdsx_intro +#L2 #HL12 #HnL12 elim (lpx_drops_conf … HLK1 … HL12) +/5 width=9 by lfdeq_lifts_bi, lpx_fwd_length/ +qed-. + +(* Inversion lemmas on relocation *******************************************) + +(* Basic_2A1: uses: lsx_inv_lift_le lsx_inv_lift_be lsx_inv_lift_ge *) +lemma rdsx_inv_lifts (h) (o) (G): d_deliftable1_isuni … (λL,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄). +#h #o #G #L #U #H @(rdsx_ind … H) -L +#L1 #_ #IH #b #f #K1 #HLK1 #Hf #T #HTU @rdsx_intro +#K2 #HK12 #HnK12 elim (drops_lpx_trans … HLK1 … HK12) -HK12 +/4 width=10 by lfdeq_inv_lifts_bi/ +qed-. + +(* Advanced properties ******************************************************) + +(* Basic_2A1: uses: lsx_lref_free *) +lemma rdsx_lref_atom (h) (o) (G): ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≘ ⋆ → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄. +#h #o #G #L1 #i #HL1 +@(rdsx_lifts … (#0) … HL1) -HL1 // +qed. + +(* Basic_2A1: uses: lsx_lref_skip *) +lemma rdsx_lref_unit (h) (o) (G): ∀I,L,K,i. ⬇*[i] L ≘ K.ⓤ{I} → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄. +#h #o #G #I #L1 #K1 #i #HL1 +@(rdsx_lifts … (#0) … HL1) -HL1 // +qed. + +(* Advanced forward lemmas **************************************************) + +(* Basic_2A1: uses: lsx_fwd_lref_be *) +lemma rdsx_fwd_lref_pair (h) (o) (G): + ∀L,i. G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄ → + ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄. +#h #o #G #L #i #HL #I #K #V #HLK +lapply (rdsx_inv_lifts … HL … HLK … (#0) ?) -L +/2 width=2 by rdsx_fwd_pair/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_fqup.ma new file mode 100644 index 000000000..2748790e7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_fqup.ma @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/lfdeq_fqup.ma". +include "basic_2/rt_computation/rdsx.ma". + +(* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******) + +(* Advanced properties ******************************************************) + +(* Basic_2A1: uses: lsx_atom *) +lemma lfsx_atom (h) (o) (G) (T): G ⊢ ⬈*[h, o, T] 𝐒⦃⋆⦄. +#h #o #G #T +@rdsx_intro #Y #H #HnT +lapply (lpx_inv_atom_sn … H) -H #H destruct +elim HnT -HnT // +qed. + +(* Advanced forward lemmas **************************************************) + +(* Basic_2A1: uses: lsx_fwd_bind_dx *) +(* Note: the exclusion binder (ⓧ) makes this more elegant and much simpler *) +(* Note: the old proof without the exclusion binder requires lreq *) +lemma rdsx_fwd_bind_dx (h) (o) (G): + ∀p,I,L,V,T. G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄ → + G ⊢ ⬈*[h, o, T] 𝐒⦃L.ⓧ⦄. +#h #o #G #p #I #L #V #T #H +@(rdsx_ind … H) -L #L1 #_ #IH +@rdsx_intro #Y #H #HT +elim (lpx_inv_unit_sn … H) -H #L2 #HL12 #H destruct +/4 width=4 by lfdeq_fwd_bind_dx_void/ +qed-. + +(* Advanced inversion lemmas ************************************************) + +(* Basic_2A1: uses: lsx_inv_bind *) +lemma rdsx_inv_bind (h) (o) (G): ∀p,I,L,V,T. G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄ → + ∧∧ G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ & G ⊢ ⬈*[h, o, T] 𝐒⦃L.ⓧ⦄. +/3 width=4 by rdsx_fwd_pair_sn, rdsx_fwd_bind_dx, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_length.ma new file mode 100644 index 000000000..7063209b5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_length.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/lfdeq_length.ma". +include "basic_2/rt_transition/lpx_length.ma". +include "basic_2/rt_computation/rdsx.ma". + +(* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******) + +(* Advanced properties ******************************************************) + +(* Basic_2A1: uses: lsx_sort *) +lemma rdsx_sort (h) (o) (G): ∀L,s. G ⊢ ⬈*[h, o, ⋆s] 𝐒⦃L⦄. +#h #o #G #L1 #s @rdsx_intro #L2 #H #Hs +elim Hs -Hs /3 width=3 by lpx_fwd_length, lfdeq_sort_length/ +qed. + +(* Basic_2A1: uses: lsx_gref *) +lemma rdsx_gref (h) (o) (G): ∀L,l. G ⊢ ⬈*[h, o, §l] 𝐒⦃L⦄. +#h #o #G #L1 #s @rdsx_intro #L2 #H #Hs +elim Hs -Hs /3 width=3 by lpx_fwd_length, lfdeq_gref_length/ +qed. + +lemma rdsx_unit (h) (o) (G): ∀I,L. G ⊢ ⬈*[h, o, #0] 𝐒⦃L.ⓤ{I}⦄. +#h #o #G #I #L1 @rdsx_intro +#Y #HY #HnY elim HnY -HnY +elim (lpx_inv_unit_sn … HY) -HY #L2 #HL12 #H destruct +/3 width=3 by lpx_fwd_length, lfdeq_unit_length/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_lpxs.ma new file mode 100644 index 000000000..6279463b0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_lpxs.ma @@ -0,0 +1,154 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_computation/lpxs_lfdeq.ma". +include "basic_2/rt_computation/lpxs_lpx.ma". +include "basic_2/rt_computation/lpxs_lpxs.ma". +include "basic_2/rt_computation/rdsx_rdsx.ma". + +(* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******) + +(* Properties with unbound rt-computation for full local environments *******) + +(* Basic_2A1: uses: lsx_intro_alt *) +lemma rdsx_intro_lpxs (h) (o) (G): + ∀L1,T. (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) → + G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄. +/4 width=1 by lpx_lpxs, rdsx_intro/ qed-. + +(* Basic_2A1: uses: lsx_lpxs_trans *) +lemma rdsx_lpxs_trans (h) (o) (G): ∀L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → + ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄. +#h #o #G #L1 #T #HL1 #L2 #H @(lpxs_ind_dx … H) -L2 +/2 width=3 by rdsx_lpx_trans/ +qed-. + +(* Eliminators with unbound rt-computation for full local environments ******) + +lemma rdsx_ind_lpxs_lfdeq (h) (o) (G): + ∀T. ∀R:predicate lenv. + (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → + (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) → + R L1 + ) → + ∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → + ∀L0. ⦃G, L1⦄ ⊢ ⬈*[h] L0 → ∀L2. L0 ≛[h, o, T] L2 → R L2. +#h #o #G #T #R #IH #L1 #H @(rdsx_ind … H) -L1 +#L1 #HL1 #IH1 #L0 #HL10 #L2 #HL02 +@IH -IH /3 width=3 by rdsx_lpxs_trans, rdsx_lfdeq_trans/ -HL1 #K2 #HLK2 #HnLK2 +lapply (lfdeq_lfdneq_trans … HL02 … HnLK2) -HnLK2 #H +elim (lfdeq_lpxs_trans … HLK2 … HL02) -L2 #K0 #HLK0 #HK02 +lapply (lfdneq_lfdeq_canc_dx … H … HK02) -H #HnLK0 +elim (lfdeq_dec h o L1 L0 T) #H +[ lapply (lfdeq_lfdneq_trans … H … HnLK0) -H -HnLK0 #Hn10 + lapply (lpxs_trans … HL10 … HLK0) -L0 #H10 + elim (lpxs_lfdneq_inv_step_sn … H10 … Hn10) -H10 -Hn10 + /3 width=8 by lfdeq_trans/ +| elim (lpxs_lfdneq_inv_step_sn … HL10 … H) -HL10 -H #L #K #HL1 #HnL1 #HLK #HKL0 + elim (lfdeq_lpxs_trans … HLK0 … HKL0) -L0 + /3 width=8 by lpxs_trans, lfdeq_trans/ +] +qed-. + +(* Basic_2A1: uses: lsx_ind_alt *) +lemma rdsx_ind_lpxs (h) (o) (G): + ∀T. ∀R:predicate lenv. + (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → + (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) → + R L1 + ) → + ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L. +#h #o #G #T #R #IH #L #HL +@(rdsx_ind_lpxs_lfdeq … IH … HL) -IH -HL // (**) (* full auto fails *) +qed-. + +(* Advanced properties ******************************************************) + +fact rdsx_bind_lpxs_aux (h) (o) (G): + ∀p,I,L1,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L1⦄ → + ∀Y,T. G ⊢ ⬈*[h, o, T] 𝐒⦃Y⦄ → + ∀L2. Y = L2.ⓑ{I}V → ⦃G, L1⦄ ⊢ ⬈*[h] L2 → + G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L2⦄. +#h #o #G #p #I #L1 #V #H @(rdsx_ind_lpxs … H) -L1 +#L1 #_ #IHL1 #Y #T #H @(rdsx_ind_lpxs … H) -Y +#Y #HY #IHY #L2 #H #HL12 destruct +@rdsx_intro_lpxs #L0 #HL20 +lapply (lpxs_trans … HL12 … HL20) #HL10 #H +elim (lfdneq_inv_bind … H) -H [ -IHY | -HY -IHL1 -HL12 ] +[ #HnV elim (lfdeq_dec h o L1 L2 V) + [ #HV @(IHL1 … HL10) -IHL1 -HL12 -HL10 + /3 width=4 by rdsx_lpxs_trans, lpxs_bind_refl_dx, lfdeq_canc_sn/ (**) (* full auto too slow *) + | -HnV -HL10 /4 width=4 by rdsx_lpxs_trans, lpxs_bind_refl_dx/ + ] +| /3 width=4 by lpxs_bind_refl_dx/ +] +qed-. + +(* Basic_2A1: uses: lsx_bind *) +lemma rdsx_bind (h) (o) (G): + ∀p,I,L,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ → + ∀T. G ⊢ ⬈*[h, o, T] 𝐒⦃L.ⓑ{I}V⦄ → + G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄. +/2 width=3 by rdsx_bind_lpxs_aux/ qed. + +(* Basic_2A1: uses: lsx_flat_lpxs *) +lemma rdsx_flat_lpxs (h) (o) (G): + ∀I,L1,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L1⦄ → + ∀L2,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄ → ⦃G, L1⦄ ⊢ ⬈*[h] L2 → + G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L2⦄. +#h #o #G #I #L1 #V #H @(rdsx_ind_lpxs … H) -L1 +#L1 #HL1 #IHL1 #L2 #T #H @(rdsx_ind_lpxs … H) -L2 +#L2 #HL2 #IHL2 #HL12 @rdsx_intro_lpxs +#L0 #HL20 lapply (lpxs_trans … HL12 … HL20) +#HL10 #H elim (lfdneq_inv_flat … H) -H [ -HL1 -IHL2 | -HL2 -IHL1 ] +[ #HnV elim (lfdeq_dec h o L1 L2 V) + [ #HV @(IHL1 … HL10) -IHL1 -HL12 -HL10 + /3 width=5 by rdsx_lpxs_trans, lfdeq_canc_sn/ (**) (* full auto too slow: 47s *) + | -HnV -HL10 /3 width=4 by rdsx_lpxs_trans/ + ] +| /3 width=3 by/ +] +qed-. + +(* Basic_2A1: uses: lsx_flat *) +lemma rdsx_flat (h) (o) (G): + ∀I,L,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ → + ∀T. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L⦄. +/2 width=3 by rdsx_flat_lpxs/ qed. + +fact rdsx_bind_lpxs_void_aux (h) (o) (G): + ∀p,I,L1,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L1⦄ → + ∀Y,T. G ⊢ ⬈*[h, o, T] 𝐒⦃Y⦄ → + ∀L2. Y = L2.ⓧ → ⦃G, L1⦄ ⊢ ⬈*[h] L2 → + G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L2⦄. +#h #o #G #p #I #L1 #V #H @(rdsx_ind_lpxs … H) -L1 +#L1 #_ #IHL1 #Y #T #H @(rdsx_ind_lpxs … H) -Y +#Y #HY #IHY #L2 #H #HL12 destruct +@rdsx_intro_lpxs #L0 #HL20 +lapply (lpxs_trans … HL12 … HL20) #HL10 #H +elim (lfdneq_inv_bind_void … H) -H [ -IHY | -HY -IHL1 -HL12 ] +[ #HnV elim (lfdeq_dec h o L1 L2 V) + [ #HV @(IHL1 … HL10) -IHL1 -HL12 -HL10 + /3 width=6 by rdsx_lpxs_trans, lpxs_bind_refl_dx, lfdeq_canc_sn/ (**) (* full auto too slow *) + | -HnV -HL10 /4 width=4 by rdsx_lpxs_trans, lpxs_bind_refl_dx/ + ] +| /3 width=4 by lpxs_bind_refl_dx/ +] +qed-. + +lemma rdsx_bind_void (h) (o) (G): + ∀p,I,L,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ → + ∀T. G ⊢ ⬈*[h, o, T] 𝐒⦃L.ⓧ⦄ → + G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄. +/2 width=3 by rdsx_bind_lpxs_void_aux/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_rdsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_rdsx.ma new file mode 100644 index 000000000..efdf72af6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_rdsx.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_transition/lpx_lfdeq.ma". +include "basic_2/rt_computation/rdsx.ma". + +(* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******) + +(* Advanced properties ******************************************************) + +(* Basic_2A1: uses: lsx_lleq_trans *) +lemma rdsx_lfdeq_trans (h) (o) (G): + ∀L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → + ∀L2. L1 ≛[h, o, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄. +#h #o #G #L1 #T #H @(rdsx_ind … H) -L1 +#L1 #_ #IHL1 #L2 #HL12 @rdsx_intro +#L #HL2 #HnL2 elim (lfdeq_lpx_trans … HL2 … HL12) -HL2 +/4 width=5 by lfdeq_repl/ +qed-. + +(* Basic_2A1: uses: lsx_lpx_trans *) +lemma rdsx_lpx_trans (h) (o) (G): + ∀L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → + ∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄. +#h #o #G #L1 #T #H @(rdsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12 +elim (lfdeq_dec h o L1 L2 T) /3 width=4 by rdsx_lfdeq_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma index 47c5a38ba..4103c54c5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma @@ -18,8 +18,8 @@ include "basic_2/static/lfxs.ma". (* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******) -definition lfdeq: ∀h. sd h → relation3 term lenv lenv ≝ - λh,o. lfxs (cdeq h o). +definition lfdeq (h) (o): relation3 term lenv lenv ≝ + lfxs (cdeq h o). interpretation "degree-based equivalence on referred entries (local environment)" @@ -31,8 +31,8 @@ interpretation (* Basic properties ***********************************************************) -lemma frees_tdeq_conf_lfdeq: ∀h,o,f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≘ f → ∀T2. T1 ≛[h, o] T2 → - ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T2⦄ ≘ f. +lemma frees_tdeq_conf_lfdeq (h) (o): ∀f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≘ f → ∀T2. T1 ≛[h, o] T2 → + ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T2⦄ ≘ f. #h #o #f #L1 #T1 #H elim H -f -L1 -T1 [ #f #L1 #s1 #Hf #X #H1 #L2 #_ elim (tdeq_inv_sort1 … H1) -H1 #s2 #d #_ #_ #H destruct @@ -65,132 +65,130 @@ lemma frees_tdeq_conf_lfdeq: ∀h,o,f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≘ f → ∀T ] qed-. -lemma frees_tdeq_conf: ∀h,o,f,L,T1. L ⊢ 𝐅*⦃T1⦄ ≘ f → - ∀T2. T1 ≛[h, o] T2 → L ⊢ 𝐅*⦃T2⦄ ≘ f. +lemma frees_tdeq_conf (h) (o): ∀f,L,T1. L ⊢ 𝐅*⦃T1⦄ ≘ f → + ∀T2. T1 ≛[h, o] T2 → L ⊢ 𝐅*⦃T2⦄ ≘ f. /4 width=7 by frees_tdeq_conf_lfdeq, lexs_refl, ext2_refl/ qed-. -lemma frees_lfdeq_conf: ∀h,o,f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≘ f → - ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≘ f. +lemma frees_lfdeq_conf (h) (o): ∀f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≘ f → + ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≘ f. /2 width=7 by frees_tdeq_conf_lfdeq, tdeq_refl/ qed-. -lemma tdeq_lfxs_conf: ∀R,h,o. s_r_confluent1 … (cdeq h o) (lfxs R). +lemma tdeq_lfxs_conf (R) (h) (o): s_r_confluent1 … (cdeq h o) (lfxs R). #R #h #o #L1 #T1 #T2 #HT12 #L2 * /3 width=5 by frees_tdeq_conf, ex2_intro/ qed-. -lemma tdeq_lfxs_div: ∀R,h,o,T1,T2. T1 ≛[h, o] T2 → - ∀L1,L2. L1 ⪤*[R, T2] L2 → L1 ⪤*[R, T1] L2. +lemma tdeq_lfxs_div (R) (h) (o): ∀T1,T2. T1 ≛[h, o] T2 → + ∀L1,L2. L1 ⪤*[R, T2] L2 → L1 ⪤*[R, T1] L2. /3 width=5 by tdeq_lfxs_conf, tdeq_sym/ qed-. -lemma tdeq_lfdeq_conf: ∀h,o. s_r_confluent1 … (cdeq h o) (lfdeq h o). +lemma tdeq_lfdeq_conf (h) (o): s_r_confluent1 … (cdeq h o) (lfdeq h o). /2 width=5 by tdeq_lfxs_conf/ qed-. -lemma tdeq_lfdeq_div: ∀h,o,T1,T2. T1 ≛[h, o] T2 → - ∀L1,L2. L1 ≛[h, o, T2] L2 → L1 ≛[h, o, T1] L2. +lemma tdeq_lfdeq_div (h) (o): ∀T1,T2. T1 ≛[h, o] T2 → + ∀L1,L2. L1 ≛[h, o, T2] L2 → L1 ≛[h, o, T1] L2. /2 width=5 by tdeq_lfxs_div/ qed-. -lemma lfdeq_atom: ∀h,o,I. ⋆ ≛[h, o, ⓪{I}] ⋆. +lemma lfdeq_atom (h) (o): ∀I. ⋆ ≛[h, o, ⓪{I}] ⋆. /2 width=1 by lfxs_atom/ qed. -(* Basic_2A1: uses: lleq_sort *) -lemma lfdeq_sort: ∀h,o,I1,I2,L1,L2,s. - L1 ≛[h, o, ⋆s] L2 → L1.ⓘ{I1} ≛[h, o, ⋆s] L2.ⓘ{I2}. +lemma lfdeq_sort (h) (o): ∀I1,I2,L1,L2,s. + L1 ≛[h, o, ⋆s] L2 → L1.ⓘ{I1} ≛[h, o, ⋆s] L2.ⓘ{I2}. /2 width=1 by lfxs_sort/ qed. -lemma lfdeq_pair: ∀h,o,I,L1,L2,V1,V2. L1 ≛[h, o, V1] L2 → V1 ≛[h, o] V2 → - L1.ⓑ{I}V1 ≛[h, o, #0] L2.ⓑ{I}V2. +lemma lfdeq_pair (h) (o): ∀I,L1,L2,V1,V2. L1 ≛[h, o, V1] L2 → V1 ≛[h, o] V2 → + L1.ⓑ{I}V1 ≛[h, o, #0] L2.ⓑ{I}V2. /2 width=1 by lfxs_pair/ qed. (* -lemma lfdeq_unit: ∀h,o,f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cdeq_ext h o, cfull, f] L2 → - L1.ⓤ{I} ≛[h, o, #0] L2.ⓤ{I}. +lemma lfdeq_unit (h) (o): ∀f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cdeq_ext h o, cfull, f] L2 → + L1.ⓤ{I} ≛[h, o, #0] L2.ⓤ{I}. /2 width=3 by lfxs_unit/ qed. *) -lemma lfdeq_lref: ∀h,o,I1,I2,L1,L2,i. - L1 ≛[h, o, #i] L2 → L1.ⓘ{I1} ≛[h, o, #↑i] L2.ⓘ{I2}. +lemma lfdeq_lref (h) (o): ∀I1,I2,L1,L2,i. + L1 ≛[h, o, #i] L2 → L1.ⓘ{I1} ≛[h, o, #↑i] L2.ⓘ{I2}. /2 width=1 by lfxs_lref/ qed. -(* Basic_2A1: uses: lleq_gref *) -lemma lfdeq_gref: ∀h,o,I1,I2,L1,L2,l. - L1 ≛[h, o, §l] L2 → L1.ⓘ{I1} ≛[h, o, §l] L2.ⓘ{I2}. +lemma lfdeq_gref (h) (o): ∀I1,I2,L1,L2,l. + L1 ≛[h, o, §l] L2 → L1.ⓘ{I1} ≛[h, o, §l] L2.ⓘ{I2}. /2 width=1 by lfxs_gref/ qed. -lemma lfdeq_bind_repl_dx: ∀h,o,I,I1,L1,L2.∀T:term. - L1.ⓘ{I} ≛[h, o, T] L2.ⓘ{I1} → - ∀I2. I ≛[h, o] I2 → - L1.ⓘ{I} ≛[h, o, T] L2.ⓘ{I2}. +lemma lfdeq_bind_repl_dx (h) (o): ∀I,I1,L1,L2.∀T:term. + L1.ⓘ{I} ≛[h, o, T] L2.ⓘ{I1} → + ∀I2. I ≛[h, o] I2 → + L1.ⓘ{I} ≛[h, o, T] L2.ⓘ{I2}. /2 width=2 by lfxs_bind_repl_dx/ qed-. (* Basic inversion lemmas ***************************************************) -lemma lfdeq_inv_atom_sn: ∀h,o,Y2. ∀T:term. ⋆ ≛[h, o, T] Y2 → Y2 = ⋆. +lemma lfdeq_inv_atom_sn (h) (o): ∀Y2. ∀T:term. ⋆ ≛[h, o, T] Y2 → Y2 = ⋆. /2 width=3 by lfxs_inv_atom_sn/ qed-. -lemma lfdeq_inv_atom_dx: ∀h,o,Y1. ∀T:term. Y1 ≛[h, o, T] ⋆ → Y1 = ⋆. +lemma lfdeq_inv_atom_dx (h) (o): ∀Y1. ∀T:term. Y1 ≛[h, o, T] ⋆ → Y1 = ⋆. /2 width=3 by lfxs_inv_atom_dx/ qed-. (* -lemma lfdeq_inv_zero: ∀h,o,Y1,Y2. Y1 ≛[h, o, #0] Y2 → - ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ - | ∃∃I,L1,L2,V1,V2. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2 - | ∃∃f,I,L1,L2. 𝐈⦃f⦄ & L1 ⪤*[cdeq_ext h o, cfull, f] L2 & - Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}. +lemma lfdeq_inv_zero (h) (o): ∀Y1,Y2. Y1 ≛[h, o, #0] Y2 → + ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆ + | ∃∃I,L1,L2,V1,V2. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2 + | ∃∃f,I,L1,L2. 𝐈⦃f⦄ & L1 ⪤*[cdeq_ext h o, cfull, f] L2 & + Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}. #h #o #Y1 #Y2 #H elim (lfxs_inv_zero … H) -H * /3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_4_intro, conj/ qed-. *) -lemma lfdeq_inv_lref: ∀h,o,Y1,Y2,i. Y1 ≛[h, o, #↑i] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I1,I2,L1,L2. L1 ≛[h, o, #i] L2 & - Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}. +lemma lfdeq_inv_lref (h) (o): ∀Y1,Y2,i. Y1 ≛[h, o, #↑i] Y2 → + ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆ + | ∃∃I1,I2,L1,L2. L1 ≛[h, o, #i] L2 & + Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}. /2 width=1 by lfxs_inv_lref/ qed-. (* Basic_2A1: uses: lleq_inv_bind lleq_inv_bind_O *) -lemma lfdeq_inv_bind: ∀h,o,p,I,L1,L2,V,T. L1 ≛[h, o, ⓑ{p,I}V.T] L2 → - L1 ≛[h, o, V] L2 ∧ L1.ⓑ{I}V ≛[h, o, T] L2.ⓑ{I}V. +lemma lfdeq_inv_bind (h) (o): ∀p,I,L1,L2,V,T. L1 ≛[h, o, ⓑ{p,I}V.T] L2 → + ∧∧ L1 ≛[h, o, V] L2 & L1.ⓑ{I}V ≛[h, o, T] L2.ⓑ{I}V. /2 width=2 by lfxs_inv_bind/ qed-. (* Basic_2A1: uses: lleq_inv_flat *) -lemma lfdeq_inv_flat: ∀h,o,I,L1,L2,V,T. L1 ≛[h, o, ⓕ{I}V.T] L2 → - L1 ≛[h, o, V] L2 ∧ L1 ≛[h, o, T] L2. +lemma lfdeq_inv_flat (h) (o): ∀I,L1,L2,V,T. L1 ≛[h, o, ⓕ{I}V.T] L2 → + ∧∧ L1 ≛[h, o, V] L2 & L1 ≛[h, o, T] L2. /2 width=2 by lfxs_inv_flat/ qed-. (* Advanced inversion lemmas ************************************************) -lemma lfdeq_inv_zero_pair_sn: ∀h,o,I,Y2,L1,V1. L1.ⓑ{I}V1 ≛[h, o, #0] Y2 → - ∃∃L2,V2. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 & Y2 = L2.ⓑ{I}V2. +lemma lfdeq_inv_zero_pair_sn (h) (o): ∀I,Y2,L1,V1. L1.ⓑ{I}V1 ≛[h, o, #0] Y2 → + ∃∃L2,V2. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 & Y2 = L2.ⓑ{I}V2. /2 width=1 by lfxs_inv_zero_pair_sn/ qed-. -lemma lfdeq_inv_zero_pair_dx: ∀h,o,I,Y1,L2,V2. Y1 ≛[h, o, #0] L2.ⓑ{I}V2 → - ∃∃L1,V1. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 & Y1 = L1.ⓑ{I}V1. +lemma lfdeq_inv_zero_pair_dx (h) (o): ∀I,Y1,L2,V2. Y1 ≛[h, o, #0] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ≛[h, o, V1] L2 & V1 ≛[h, o] V2 & Y1 = L1.ⓑ{I}V1. /2 width=1 by lfxs_inv_zero_pair_dx/ qed-. -lemma lfdeq_inv_lref_bind_sn: ∀h,o,I1,Y2,L1,i. L1.ⓘ{I1} ≛[h, o, #↑i] Y2 → - ∃∃I2,L2. L1 ≛[h, o, #i] L2 & Y2 = L2.ⓘ{I2}. +lemma lfdeq_inv_lref_bind_sn (h) (o): ∀I1,Y2,L1,i. L1.ⓘ{I1} ≛[h, o, #↑i] Y2 → + ∃∃I2,L2. L1 ≛[h, o, #i] L2 & Y2 = L2.ⓘ{I2}. /2 width=2 by lfxs_inv_lref_bind_sn/ qed-. -lemma lfdeq_inv_lref_bind_dx: ∀h,o,I2,Y1,L2,i. Y1 ≛[h, o, #↑i] L2.ⓘ{I2} → - ∃∃I1,L1. L1 ≛[h, o, #i] L2 & Y1 = L1.ⓘ{I1}. +lemma lfdeq_inv_lref_bind_dx (h) (o): ∀I2,Y1,L2,i. Y1 ≛[h, o, #↑i] L2.ⓘ{I2} → + ∃∃I1,L1. L1 ≛[h, o, #i] L2 & Y1 = L1.ⓘ{I1}. /2 width=2 by lfxs_inv_lref_bind_dx/ qed-. (* Basic forward lemmas *****************************************************) -lemma lfdeq_fwd_zero_pair: ∀h,o,I,K1,K2,V1,V2. - K1.ⓑ{I}V1 ≛[h, o, #0] K2.ⓑ{I}V2 → K1 ≛[h, o, V1] K2. +lemma lfdeq_fwd_zero_pair (h) (o): ∀I,K1,K2,V1,V2. + K1.ⓑ{I}V1 ≛[h, o, #0] K2.ⓑ{I}V2 → K1 ≛[h, o, V1] K2. /2 width=3 by lfxs_fwd_zero_pair/ qed-. (* Basic_2A1: uses: lleq_fwd_bind_sn lleq_fwd_flat_sn *) -lemma lfdeq_fwd_pair_sn: ∀h,o,I,L1,L2,V,T. L1 ≛[h, o, ②{I}V.T] L2 → L1 ≛[h, o, V] L2. +lemma lfdeq_fwd_pair_sn (h) (o): ∀I,L1,L2,V,T. L1 ≛[h, o, ②{I}V.T] L2 → L1 ≛[h, o, V] L2. /2 width=3 by lfxs_fwd_pair_sn/ qed-. (* Basic_2A1: uses: lleq_fwd_bind_dx lleq_fwd_bind_O_dx *) -lemma lfdeq_fwd_bind_dx: ∀h,o,p,I,L1,L2,V,T. - L1 ≛[h, o, ⓑ{p,I}V.T] L2 → L1.ⓑ{I}V ≛[h, o, T] L2.ⓑ{I}V. +lemma lfdeq_fwd_bind_dx (h) (o): ∀p,I,L1,L2,V,T. + L1 ≛[h, o, ⓑ{p,I}V.T] L2 → L1.ⓑ{I}V ≛[h, o, T] L2.ⓑ{I}V. /2 width=2 by lfxs_fwd_bind_dx/ qed-. (* Basic_2A1: uses: lleq_fwd_flat_dx *) -lemma lfdeq_fwd_flat_dx: ∀h,o,I,L1,L2,V,T. L1 ≛[h, o, ⓕ{I}V.T] L2 → L1 ≛[h, o, T] L2. +lemma lfdeq_fwd_flat_dx (h) (o): ∀I,L1,L2,V,T. L1 ≛[h, o, ⓕ{I}V.T] L2 → L1 ≛[h, o, T] L2. /2 width=3 by lfxs_fwd_flat_dx/ qed-. -lemma lfdeq_fwd_dx: ∀h,o,I2,L1,K2. ∀T:term. L1 ≛[h, o, T] K2.ⓘ{I2} → - ∃∃I1,K1. L1 = K1.ⓘ{I1}. +lemma lfdeq_fwd_dx (h) (o): ∀I2,L1,K2. ∀T:term. L1 ≛[h, o, T] K2.ⓘ{I2} → + ∃∃I1,K1. L1 = K1.ⓘ{I1}. /2 width=5 by lfxs_fwd_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma index 33d6c459b..40f2812cc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma @@ -21,7 +21,7 @@ include "basic_2/static/lfdeq.ma". (* Advanved properties with free variables inclusion ************************) -lemma lfdeq_fsge_comp: ∀h,o. lfxs_fsge_compatible (cdeq h o). +lemma lfdeq_fsge_comp (h) (o): lfxs_fsge_compatible (cdeq h o). #h #o #L1 #L2 #T * #f1 #Hf1 #HL12 lapply (frees_lfdeq_conf h o … Hf1 … HL12) lapply (lexs_fwd_length … HL12) @@ -30,15 +30,26 @@ qed-. (* Properties with length for local environments ****************************) +(* Basic_2A1: uses: lleq_sort *) +lemma lfdeq_sort_length (h) (o): ∀L1,L2. |L1| = |L2| → ∀s. L1 ≛[h, o, ⋆s] L2. +/2 width=1 by lfxs_sort_length/ qed. + +(* Basic_2A1: uses: lleq_gref *) +lemma lfdeq_gref_length (h) (o): ∀L1,L2. |L1| = |L2| → ∀l. L1 ≛[h, o, §l] L2. +/2 width=1 by lfxs_gref_length/ qed. + +lemma lfdeq_unit_length (h) (o): ∀L1,L2. |L1| = |L2| → + ∀I. L1.ⓤ{I} ≛[h, o, #0] L2.ⓤ{I}. +/2 width=1 by lfxs_unit_length/ qed. + (* Basic_2A1: uses: lleq_lift_le lleq_lift_ge *) -lemma lfdeq_lifts_bi: ∀L1,L2. |L1| = |L2| → ∀h,o,K1,K2,T. K1 ≛[h, o, T] K2 → - ∀b,f. ⬇*[b, f] L1 ≘ K1 → ⬇*[b, f] L2 ≘ K2 → - ∀U. ⬆*[f] T ≘ U → L1 ≛[h, o, U] L2. +lemma lfdeq_lifts_bi (h) (o): ∀L1,L2. |L1| = |L2| → ∀K1,K2,T. K1 ≛[h, o, T] K2 → + ∀b,f. ⬇*[b, f] L1 ≘ K1 → ⬇*[b, f] L2 ≘ K2 → + ∀U. ⬆*[f] T ≘ U → L1 ≛[h, o, U] L2. /3 width=9 by lfxs_lifts_bi, tdeq_lifts_sn/ qed-. (* Forward lemmas with length for local environments ************************) (* Basic_2A1: lleq_fwd_length *) -lemma lfdeq_fwd_length: ∀h,o,L1,L2. ∀T:term. L1 ≛[h, o, T] L2 → |L1| = |L2|. +lemma lfdeq_fwd_length (h) (o): ∀L1,L2. ∀T:term. L1 ≛[h, o, T] L2 → |L1| = |L2|. /2 width=3 by lfxs_fwd_length/ qed-. - diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma index 5daeedab0..cc5b1e623 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -45,18 +45,18 @@ definition lfxs_transitive: relation3 ? (relation3 ?? term) … ≝ (* Basic inversion lemmas ***************************************************) -lemma lfxs_inv_atom_sn: ∀R,Y2,T. ⋆ ⪤*[R, T] Y2 → Y2 = ⋆. +lemma lfxs_inv_atom_sn (R): ∀Y2,T. ⋆ ⪤*[R, T] Y2 → Y2 = ⋆. #R #Y2 #T * /2 width=4 by lexs_inv_atom1/ qed-. -lemma lfxs_inv_atom_dx: ∀R,Y1,T. Y1 ⪤*[R, T] ⋆ → Y1 = ⋆. +lemma lfxs_inv_atom_dx (R): ∀Y1,T. Y1 ⪤*[R, T] ⋆ → Y1 = ⋆. #R #I #Y1 * /2 width=4 by lexs_inv_atom2/ qed-. -lemma lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⪤*[R, ⋆s] Y2 → - ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ - | ∃∃I1,I2,L1,L2. L1 ⪤*[R, ⋆s] L2 & - Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}. +lemma lfxs_inv_sort (R): ∀Y1,Y2,s. Y1 ⪤*[R, ⋆s] Y2 → + ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ + | ∃∃I1,I2,L1,L2. L1 ⪤*[R, ⋆s] L2 & + Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}. #R * [ | #Y1 #I1 ] #Y2 #s * #f #H1 #H2 [ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/ | lapply (frees_inv_sort … H1) -H1 #Hf @@ -66,12 +66,12 @@ lemma lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⪤*[R, ⋆s] Y2 → ] qed-. -lemma lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⪤*[R, #0] Y2 → - ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ - | ∃∃I,L1,L2,V1,V2. L1 ⪤*[R, V1] L2 & R L1 V1 V2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2 - | ∃∃f,I,L1,L2. 𝐈⦃f⦄ & L1 ⪤*[cext2 R, cfull, f] L2 & - Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}. +lemma lfxs_inv_zero (R): ∀Y1,Y2. Y1 ⪤*[R, #0] Y2 → + ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ + | ∃∃I,L1,L2,V1,V2. L1 ⪤*[R, V1] L2 & R L1 V1 V2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2 + | ∃∃f,I,L1,L2. 𝐈⦃f⦄ & L1 ⪤*[cext2 R, cfull, f] L2 & + Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}. #R * [ | #Y1 * #I1 [ | #X ] ] #Y2 * #f #H1 #H2 [ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or3_intro0, conj/ | elim (frees_inv_unit … H1) -H1 #g #HX #H destruct @@ -84,10 +84,10 @@ lemma lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⪤*[R, #0] Y2 → ] qed-. -lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⪤*[R, #↑i] Y2 → - ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ - | ∃∃I1,I2,L1,L2. L1 ⪤*[R, #i] L2 & - Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}. +lemma lfxs_inv_lref (R): ∀Y1,Y2,i. Y1 ⪤*[R, #↑i] Y2 → + ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ + | ∃∃I1,I2,L1,L2. L1 ⪤*[R, #i] L2 & + Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}. #R * [ | #Y1 #I1 ] #Y2 #i * #f #H1 #H2 [ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/ | elim (frees_inv_lref … H1) -H1 #g #Hg #H destruct @@ -96,10 +96,10 @@ lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⪤*[R, #↑i] Y2 → ] qed-. -lemma lfxs_inv_gref: ∀R,Y1,Y2,l. Y1 ⪤*[R, §l] Y2 → - ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ - | ∃∃I1,I2,L1,L2. L1 ⪤*[R, §l] L2 & - Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}. +lemma lfxs_inv_gref (R): ∀Y1,Y2,l. Y1 ⪤*[R, §l] Y2 → + ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ + | ∃∃I1,I2,L1,L2. L1 ⪤*[R, §l] L2 & + Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}. #R * [ | #Y1 #I1 ] #Y2 #l * #f #H1 #H2 [ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/ | lapply (frees_inv_gref … H1) -H1 #Hf @@ -110,40 +110,40 @@ lemma lfxs_inv_gref: ∀R,Y1,Y2,l. Y1 ⪤*[R, §l] Y2 → qed-. (* Basic_2A1: uses: llpx_sn_inv_bind llpx_sn_inv_bind_O *) -lemma lfxs_inv_bind: ∀R,p,I,L1,L2,V1,V2,T. L1 ⪤*[R, ⓑ{p,I}V1.T] L2 → R L1 V1 V2 → - L1 ⪤*[R, V1] L2 ∧ L1.ⓑ{I}V1 ⪤*[R, T] L2.ⓑ{I}V2. +lemma lfxs_inv_bind (R): ∀p,I,L1,L2,V1,V2,T. L1 ⪤*[R, ⓑ{p,I}V1.T] L2 → R L1 V1 V2 → + ∧∧ L1 ⪤*[R, V1] L2 & L1.ⓑ{I}V1 ⪤*[R, T] L2.ⓑ{I}V2. #R #p #I #L1 #L2 #V1 #V2 #T * #f #Hf #HL #HV elim (frees_inv_bind … Hf) -Hf /6 width=6 by sle_lexs_trans, lexs_inv_tl, ext2_pair, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ qed-. (* Basic_2A1: uses: llpx_sn_inv_flat *) -lemma lfxs_inv_flat: ∀R,I,L1,L2,V,T. L1 ⪤*[R, ⓕ{I}V.T] L2 → - L1 ⪤*[R, V] L2 ∧ L1 ⪤*[R, T] L2. +lemma lfxs_inv_flat (R): ∀I,L1,L2,V,T. L1 ⪤*[R, ⓕ{I}V.T] L2 → + ∧∧ L1 ⪤*[R, V] L2 & L1 ⪤*[R, T] L2. #R #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_flat … Hf) -Hf /5 width=6 by sle_lexs_trans, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ qed-. (* Advanced inversion lemmas ************************************************) -lemma lfxs_inv_sort_bind_sn: ∀R,I1,K1,L2,s. K1.ⓘ{I1} ⪤*[R, ⋆s] L2 → - ∃∃I2,K2. K1 ⪤*[R, ⋆s] K2 & L2 = K2.ⓘ{I2}. +lemma lfxs_inv_sort_bind_sn (R): ∀I1,K1,L2,s. K1.ⓘ{I1} ⪤*[R, ⋆s] L2 → + ∃∃I2,K2. K1 ⪤*[R, ⋆s] K2 & L2 = K2.ⓘ{I2}. #R #I1 #K1 #L2 #s #H elim (lfxs_inv_sort … H) -H * [ #H destruct | #Z1 #I2 #Y1 #K2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/ ] qed-. -lemma lfxs_inv_sort_bind_dx: ∀R,I2,K2,L1,s. L1 ⪤*[R, ⋆s] K2.ⓘ{I2} → - ∃∃I1,K1. K1 ⪤*[R, ⋆s] K2 & L1 = K1.ⓘ{I1}. +lemma lfxs_inv_sort_bind_dx (R): ∀I2,K2,L1,s. L1 ⪤*[R, ⋆s] K2.ⓘ{I2} → + ∃∃I1,K1. K1 ⪤*[R, ⋆s] K2 & L1 = K1.ⓘ{I1}. #R #I2 #K2 #L1 #s #H elim (lfxs_inv_sort … H) -H * [ #_ #H destruct | #I1 #Z2 #K1 #Y2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/ ] qed-. -lemma lfxs_inv_zero_pair_sn: ∀R,I,L2,K1,V1. K1.ⓑ{I}V1 ⪤*[R, #0] L2 → - ∃∃K2,V2. K1 ⪤*[R, V1] K2 & R K1 V1 V2 & - L2 = K2.ⓑ{I}V2. +lemma lfxs_inv_zero_pair_sn (R): ∀I,L2,K1,V1. K1.ⓑ{I}V1 ⪤*[R, #0] L2 → + ∃∃K2,V2. K1 ⪤*[R, V1] K2 & R K1 V1 V2 & + L2 = K2.ⓑ{I}V2. #R #I #L2 #K1 #V1 #H elim (lfxs_inv_zero … H) -H * [ #H destruct | #Z #Y1 #K2 #X1 #V2 #HK12 #HV12 #H1 #H2 destruct @@ -152,9 +152,9 @@ lemma lfxs_inv_zero_pair_sn: ∀R,I,L2,K1,V1. K1.ⓑ{I}V1 ⪤*[R, #0] L2 → ] qed-. -lemma lfxs_inv_zero_pair_dx: ∀R,I,L1,K2,V2. L1 ⪤*[R, #0] K2.ⓑ{I}V2 → - ∃∃K1,V1. K1 ⪤*[R, V1] K2 & R K1 V1 V2 & - L1 = K1.ⓑ{I}V1. +lemma lfxs_inv_zero_pair_dx (R): ∀I,L1,K2,V2. L1 ⪤*[R, #0] K2.ⓑ{I}V2 → + ∃∃K1,V1. K1 ⪤*[R, V1] K2 & R K1 V1 V2 & + L1 = K1.ⓑ{I}V1. #R #I #L1 #K2 #V2 #H elim (lfxs_inv_zero … H) -H * [ #_ #H destruct | #Z #K1 #Y2 #V1 #X2 #HK12 #HV12 #H1 #H2 destruct @@ -163,9 +163,9 @@ lemma lfxs_inv_zero_pair_dx: ∀R,I,L1,K2,V2. L1 ⪤*[R, #0] K2.ⓑ{I}V2 → ] qed-. -lemma lfxs_inv_zero_unit_sn: ∀R,I,K1,L2. K1.ⓤ{I} ⪤*[R, #0] L2 → - ∃∃f,K2. 𝐈⦃f⦄ & K1 ⪤*[cext2 R, cfull, f] K2 & - L2 = K2.ⓤ{I}. +lemma lfxs_inv_zero_unit_sn (R): ∀I,K1,L2. K1.ⓤ{I} ⪤*[R, #0] L2 → + ∃∃f,K2. 𝐈⦃f⦄ & K1 ⪤*[cext2 R, cfull, f] K2 & + L2 = K2.ⓤ{I}. #R #I #K1 #L2 #H elim (lfxs_inv_zero … H) -H * [ #H destruct | #Z #Y1 #Y2 #X1 #X2 #_ #_ #H destruct @@ -173,9 +173,9 @@ lemma lfxs_inv_zero_unit_sn: ∀R,I,K1,L2. K1.ⓤ{I} ⪤*[R, #0] L2 → ] qed-. -lemma lfxs_inv_zero_unit_dx: ∀R,I,L1,K2. L1 ⪤*[R, #0] K2.ⓤ{I} → - ∃∃f,K1. 𝐈⦃f⦄ & K1 ⪤*[cext2 R, cfull, f] K2 & - L1 = K1.ⓤ{I}. +lemma lfxs_inv_zero_unit_dx (R): ∀I,L1,K2. L1 ⪤*[R, #0] K2.ⓤ{I} → + ∃∃f,K1. 𝐈⦃f⦄ & K1 ⪤*[cext2 R, cfull, f] K2 & + L1 = K1.ⓤ{I}. #R #I #L1 #K2 #H elim (lfxs_inv_zero … H) -H * [ #_ #H destruct | #Z #Y1 #Y2 #X1 #X2 #_ #_ #_ #H destruct @@ -183,32 +183,32 @@ lemma lfxs_inv_zero_unit_dx: ∀R,I,L1,K2. L1 ⪤*[R, #0] K2.ⓤ{I} → ] qed-. -lemma lfxs_inv_lref_bind_sn: ∀R,I1,K1,L2,i. K1.ⓘ{I1} ⪤*[R, #↑i] L2 → - ∃∃I2,K2. K1 ⪤*[R, #i] K2 & L2 = K2.ⓘ{I2}. +lemma lfxs_inv_lref_bind_sn (R): ∀I1,K1,L2,i. K1.ⓘ{I1} ⪤*[R, #↑i] L2 → + ∃∃I2,K2. K1 ⪤*[R, #i] K2 & L2 = K2.ⓘ{I2}. #R #I1 #K1 #L2 #i #H elim (lfxs_inv_lref … H) -H * [ #H destruct | #Z1 #I2 #Y1 #K2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ ] qed-. -lemma lfxs_inv_lref_bind_dx: ∀R,I2,K2,L1,i. L1 ⪤*[R, #↑i] K2.ⓘ{I2} → - ∃∃I1,K1. K1 ⪤*[R, #i] K2 & L1 = K1.ⓘ{I1}. +lemma lfxs_inv_lref_bind_dx (R): ∀I2,K2,L1,i. L1 ⪤*[R, #↑i] K2.ⓘ{I2} → + ∃∃I1,K1. K1 ⪤*[R, #i] K2 & L1 = K1.ⓘ{I1}. #R #I2 #K2 #L1 #i #H elim (lfxs_inv_lref … H) -H * [ #_ #H destruct | #I1 #Z2 #K1 #Y2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ ] qed-. -lemma lfxs_inv_gref_bind_sn: ∀R,I1,K1,L2,l. K1.ⓘ{I1} ⪤*[R, §l] L2 → - ∃∃I2,K2. K1 ⪤*[R, §l] K2 & L2 = K2.ⓘ{I2}. +lemma lfxs_inv_gref_bind_sn (R): ∀I1,K1,L2,l. K1.ⓘ{I1} ⪤*[R, §l] L2 → + ∃∃I2,K2. K1 ⪤*[R, §l] K2 & L2 = K2.ⓘ{I2}. #R #I1 #K1 #L2 #l #H elim (lfxs_inv_gref … H) -H * [ #H destruct | #Z1 #I2 #Y1 #K2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/ ] qed-. -lemma lfxs_inv_gref_bind_dx: ∀R,I2,K2,L1,l. L1 ⪤*[R, §l] K2.ⓘ{I2} → - ∃∃I1,K1. K1 ⪤*[R, §l] K2 & L1 = K1.ⓘ{I1}. +lemma lfxs_inv_gref_bind_dx (R): ∀I2,K2,L1,l. L1 ⪤*[R, §l] K2.ⓘ{I2} → + ∃∃I1,K1. K1 ⪤*[R, §l] K2 & L1 = K1.ⓘ{I1}. #R #I2 #K2 #L1 #l #H elim (lfxs_inv_gref … H) -H * [ #_ #H destruct | #I1 #Z2 #K1 #Y2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/ @@ -217,32 +217,32 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma lfxs_fwd_zero_pair: ∀R,I,K1,K2,V1,V2. - K1.ⓑ{I}V1 ⪤*[R, #0] K2.ⓑ{I}V2 → K1 ⪤*[R, V1] K2. +lemma lfxs_fwd_zero_pair (R): ∀I,K1,K2,V1,V2. + K1.ⓑ{I}V1 ⪤*[R, #0] K2.ⓑ{I}V2 → K1 ⪤*[R, V1] K2. #R #I #K1 #K2 #V1 #V2 #H elim (lfxs_inv_zero_pair_sn … H) -H #Y #X #HK12 #_ #H destruct // qed-. (* Basic_2A1: uses: llpx_sn_fwd_pair_sn llpx_sn_fwd_bind_sn llpx_sn_fwd_flat_sn *) -lemma lfxs_fwd_pair_sn: ∀R,I,L1,L2,V,T. L1 ⪤*[R, ②{I}V.T] L2 → L1 ⪤*[R, V] L2. +lemma lfxs_fwd_pair_sn (R): ∀I,L1,L2,V,T. L1 ⪤*[R, ②{I}V.T] L2 → L1 ⪤*[R, V] L2. #R * [ #p ] #I #L1 #L2 #V #T * #f #Hf #HL [ elim (frees_inv_bind … Hf) | elim (frees_inv_flat … Hf) ] -Hf /4 width=6 by sle_lexs_trans, sor_inv_sle_sn, ex2_intro/ qed-. (* Basic_2A1: uses: llpx_sn_fwd_bind_dx llpx_sn_fwd_bind_O_dx *) -lemma lfxs_fwd_bind_dx: ∀R,p,I,L1,L2,V1,V2,T. L1 ⪤*[R, ⓑ{p,I}V1.T] L2 → - R L1 V1 V2 → L1.ⓑ{I}V1 ⪤*[R, T] L2.ⓑ{I}V2. +lemma lfxs_fwd_bind_dx (R): ∀p,I,L1,L2,V1,V2,T. L1 ⪤*[R, ⓑ{p,I}V1.T] L2 → + R L1 V1 V2 → L1.ⓑ{I}V1 ⪤*[R, T] L2.ⓑ{I}V2. #R #p #I #L1 #L2 #V1 #V2 #T #H #HV elim (lfxs_inv_bind … H HV) -H -HV // qed-. (* Basic_2A1: uses: llpx_sn_fwd_flat_dx *) -lemma lfxs_fwd_flat_dx: ∀R,I,L1,L2,V,T. L1 ⪤*[R, ⓕ{I}V.T] L2 → L1 ⪤*[R, T] L2. +lemma lfxs_fwd_flat_dx (R): ∀I,L1,L2,V,T. L1 ⪤*[R, ⓕ{I}V.T] L2 → L1 ⪤*[R, T] L2. #R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H // qed-. -lemma lfxs_fwd_dx: ∀R,I2,L1,K2,T. L1 ⪤*[R, T] K2.ⓘ{I2} → - ∃∃I1,K1. L1 = K1.ⓘ{I1}. +lemma lfxs_fwd_dx (R): ∀I2,L1,K2,T. L1 ⪤*[R, T] K2.ⓘ{I2} → + ∃∃I1,K1. L1 = K1.ⓘ{I1}. #R #I2 #L1 #K2 #T * #f elim (pn_split f) * #g #Hg #_ #Hf destruct [ elim (lexs_inv_push2 … Hf) | elim (lexs_inv_next2 … Hf) ] -Hf #I1 #K1 #_ #_ #H destruct /2 width=3 by ex1_2_intro/ @@ -250,65 +250,63 @@ qed-. (* Basic properties *********************************************************) -lemma lfxs_atom: ∀R,I. ⋆ ⪤*[R, ⓪{I}] ⋆. +lemma lfxs_atom (R): ∀I. ⋆ ⪤*[R, ⓪{I}] ⋆. #R * /3 width=3 by frees_sort, frees_atom, frees_gref, lexs_atom, ex2_intro/ qed. -(* Basic_2A1: uses: llpx_sn_sort *) -lemma lfxs_sort: ∀R,I1,I2,L1,L2,s. - L1 ⪤*[R, ⋆s] L2 → L1.ⓘ{I1} ⪤*[R, ⋆s] L2.ⓘ{I2}. +lemma lfxs_sort (R): ∀I1,I2,L1,L2,s. + L1 ⪤*[R, ⋆s] L2 → L1.ⓘ{I1} ⪤*[R, ⋆s] L2.ⓘ{I2}. #R #I1 #I2 #L1 #L2 #s * #f #Hf #H12 lapply (frees_inv_sort … Hf) -Hf /4 width=3 by frees_sort, lexs_push, isid_push, ex2_intro/ qed. -lemma lfxs_pair: ∀R,I,L1,L2,V1,V2. L1 ⪤*[R, V1] L2 → - R L1 V1 V2 → L1.ⓑ{I}V1 ⪤*[R, #0] L2.ⓑ{I}V2. +lemma lfxs_pair (R): ∀I,L1,L2,V1,V2. L1 ⪤*[R, V1] L2 → + R L1 V1 V2 → L1.ⓑ{I}V1 ⪤*[R, #0] L2.ⓑ{I}V2. #R #I1 #I2 #L1 #L2 #V1 * /4 width=3 by ext2_pair, frees_pair, lexs_next, ex2_intro/ qed. -lemma lfxs_unit: ∀R,f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cext2 R, cfull, f] L2 → - L1.ⓤ{I} ⪤*[R, #0] L2.ⓤ{I}. +lemma lfxs_unit (R): ∀f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cext2 R, cfull, f] L2 → + L1.ⓤ{I} ⪤*[R, #0] L2.ⓤ{I}. /4 width=3 by frees_unit, lexs_next, ext2_unit, ex2_intro/ qed. -lemma lfxs_lref: ∀R,I1,I2,L1,L2,i. +lemma lfxs_lref (R): ∀I1,I2,L1,L2,i. L1 ⪤*[R, #i] L2 → L1.ⓘ{I1} ⪤*[R, #↑i] L2.ⓘ{I2}. #R #I1 #I2 #L1 #L2 #i * /3 width=3 by lexs_push, frees_lref, ex2_intro/ qed. -(* Basic_2A1: uses: llpx_sn_gref *) -lemma lfxs_gref: ∀R,I1,I2,L1,L2,l. - L1 ⪤*[R, §l] L2 → L1.ⓘ{I1} ⪤*[R, §l] L2.ⓘ{I2}. +lemma lfxs_gref (R): ∀I1,I2,L1,L2,l. + L1 ⪤*[R, §l] L2 → L1.ⓘ{I1} ⪤*[R, §l] L2.ⓘ{I2}. #R #I1 #I2 #L1 #L2 #l * #f #Hf #H12 lapply (frees_inv_gref … Hf) -Hf /4 width=3 by frees_gref, lexs_push, isid_push, ex2_intro/ qed. -lemma lfxs_bind_repl_dx: ∀R,I,I1,L1,L2,T. - L1.ⓘ{I} ⪤*[R, T] L2.ⓘ{I1} → - ∀I2. cext2 R L1 I I2 → - L1.ⓘ{I} ⪤*[R, T] L2.ⓘ{I2}. +lemma lfxs_bind_repl_dx (R): ∀I,I1,L1,L2,T. + L1.ⓘ{I} ⪤*[R, T] L2.ⓘ{I1} → + ∀I2. cext2 R L1 I I2 → + L1.ⓘ{I} ⪤*[R, T] L2.ⓘ{I2}. #R #I #I1 #L1 #L2 #T * #f #Hf #HL12 #I2 #HR /3 width=5 by lexs_pair_repl, ex2_intro/ qed-. (* Basic_2A1: uses: llpx_sn_co *) -lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → - ∀L1,L2,T. L1 ⪤*[R1, T] L2 → L1 ⪤*[R2, T] L2. +lemma lfxs_co (R1) (R2): (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → + ∀L1,L2,T. L1 ⪤*[R1, T] L2 → L1 ⪤*[R2, T] L2. #R1 #R2 #HR #L1 #L2 #T * /5 width=7 by lexs_co, cext2_co, ex2_intro/ qed-. -lemma lfxs_isid: ∀R1,R2,L1,L2,T1,T2. - (∀f. L1 ⊢ 𝐅*⦃T1⦄ ≘ f → 𝐈⦃f⦄) → - (∀f. 𝐈⦃f⦄ → L1 ⊢ 𝐅*⦃T2⦄ ≘ f) → - L1 ⪤*[R1, T1] L2 → L1 ⪤*[R2, T2] L2. +lemma lfxs_isid (R1) (R2): ∀L1,L2,T1,T2. + (∀f. L1 ⊢ 𝐅*⦃T1⦄ ≘ f → 𝐈⦃f⦄) → + (∀f. 𝐈⦃f⦄ → L1 ⊢ 𝐅*⦃T2⦄ ≘ f) → + L1 ⪤*[R1, T1] L2 → L1 ⪤*[R2, T2] L2. #R1 #R2 #L1 #L2 #T1 #T2 #H1 #H2 * /4 width=7 by lexs_co_isid, ex2_intro/ qed-. -lemma lfxs_unit_sn: ∀R1,R2,I,K1,L2. - K1.ⓤ{I} ⪤*[R1, #0] L2 → K1.ⓤ{I} ⪤*[R2, #0] L2. +lemma lfxs_unit_sn (R1) (R2): + ∀I,K1,L2. K1.ⓤ{I} ⪤*[R1, #0] L2 → K1.ⓤ{I} ⪤*[R2, #0] L2. #R1 #R2 #I #K1 #L2 #H elim (lfxs_inv_zero_unit_sn … H) -H #f #K2 #Hf #HK12 #H destruct /3 width=7 by lfxs_unit, lexs_co_isid/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma index 2d2b51d81..bba7867c7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma @@ -20,17 +20,40 @@ include "basic_2/static/lfxs_drops.ma". (* Forward lemmas with length for local environments ************************) (* Basic_2A1: uses: llpx_sn_fwd_length *) -lemma lfxs_fwd_length: ∀R,L1,L2,T. L1 ⪤*[R, T] L2 → |L1| = |L2|. +lemma lfxs_fwd_length (R): ∀L1,L2,T. L1 ⪤*[R, T] L2 → |L1| = |L2|. #R #L1 #L2 #T * /2 width=4 by lexs_fwd_length/ qed-. (* Properties with length for local environments ****************************) +(* Basic_2A1: uses: llpx_sn_sort *) +lemma lfxs_sort_length (R): ∀L1,L2. |L1| = |L2| → ∀s. L1 ⪤*[R, ⋆s] L2. +#R #L1 elim L1 -L1 +[ #Y #H #s >(length_inv_zero_sn … H) -H // +| #K1 #I1 #IH #Y #H #s + elim (length_inv_succ_sn … H) -H #I2 #K2 #HK12 #H destruct + /3 width=1 by lfxs_sort/ +] +qed. + +(* Basic_2A1: uses: llpx_sn_gref *) +lemma lfxs_gref_length (R): ∀L1,L2. |L1| = |L2| → ∀l. L1 ⪤*[R, §l] L2. +#R #L1 elim L1 -L1 +[ #Y #H #s >(length_inv_zero_sn … H) -H // +| #K1 #I1 #IH #Y #H #s + elim (length_inv_succ_sn … H) -H #I2 #K2 #HK12 #H destruct + /3 width=1 by lfxs_gref/ +] +qed. + +lemma lfxs_unit_length (R): ∀L1,L2. |L1| = |L2| → ∀I. L1.ⓤ{I} ⪤*[R, #0] L2.ⓤ{I}. +/3 width=3 by lfxs_unit, lexs_length_isid/ qed. + (* Basic_2A1: uses: llpx_sn_lift_le llpx_sn_lift_ge *) -lemma lfxs_lifts_bi: ∀R.d_liftable2_sn … lifts R → - ∀L1,L2. |L1| = |L2| → ∀K1,K2,T. K1 ⪤*[R, T] K2 → - ∀b,f. ⬇*[b, f] L1 ≘ K1 → ⬇*[b, f] L2 ≘ K2 → - ∀U. ⬆*[f] T ≘ U → L1 ⪤*[R, U] L2. +lemma lfxs_lifts_bi (R): d_liftable2_sn … lifts R → + ∀L1,L2. |L1| = |L2| → ∀K1,K2,T. K1 ⪤*[R, T] K2 → + ∀b,f. ⬇*[b, f] L1 ≘ K1 → ⬇*[b, f] L2 ≘ K2 → + ∀U. ⬆*[f] T ≘ U → L1 ⪤*[R, U] L2. #R #HR #L1 #L2 #HL12 #K1 #K2 #T * #f1 #Hf1 #HK12 #b #f #HLK1 #HLK2 #U #HTU elim (frees_total L1 U) #f2 #Hf2 lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #Hf @@ -39,11 +62,11 @@ qed-. (* Inversion lemmas with length for local environment ***********************) -lemma lfxs_inv_zero_length: ∀R,Y1,Y2. Y1 ⪤*[R, #0] Y2 → - ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ - | ∃∃I,L1,L2,V1,V2. L1 ⪤*[R, V1] L2 & R L1 V1 V2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2 - | ∃∃I,L1,L2. |L1| = |L2| & Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}. +lemma lfxs_inv_zero_length (R): ∀Y1,Y2. Y1 ⪤*[R, #0] Y2 → + ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆ + | ∃∃I,L1,L2,V1,V2. L1 ⪤*[R, V1] L2 & R L1 V1 V2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2 + | ∃∃I,L1,L2. |L1| = |L2| & Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}. #R #Y1 #Y2 #H elim (lfxs_inv_zero … H) -H * /4 width=9 by lexs_fwd_length, ex4_5_intro, ex3_3_intro, or3_intro2, or3_intro1, or3_intro0, conj/ qed-. 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 33aa9459d..f40c15814 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 @@ -91,7 +91,7 @@ table { ] [ { "unbound context-sensitive parallel rt-computation" * } { [ [ "refinement for lenvs on selected entries" ] "lsubsx" + "( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ] - [ [ "strongly normalizing for lenvs on referred entries" ] "lfsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_cpx" + "lfsx_cpxs" + "lfsx_lfpxs" + "lfsx_lfsx" * ] + [ [ "strongly normalizing for lenvs on referred entries" ] "rdsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "rdsx_length" + "rdsx_drops" + "rdsx_fqup" + "rdsx_cpxs" + "rdsx_csx" + "rdsx_rdsx" * ] [ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_lfdeq" + "csx_ffdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ] [ [ "for lenvs on referred entries" ] "lfpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_ffdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ] -- 2.39.2