From: Ferruccio Guidi Date: Mon, 27 Nov 2017 15:45:35 +0000 (+0000) Subject: - free variables innclusion (fle) encapsulates some complexity X-Git-Tag: make_still_working~396 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=02128ad2d07f4763e311a7f449d87aa022014c1f - free variables innclusion (fle) encapsulates some complexity in the proof of a generalization of frees_lfxs_conf - a refactoring solves a bug in dependences --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/subseteq_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/subseteq_4.ma new file mode 100644 index 000000000..f7a000112 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/subseteq_4.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊆ ⦃ break term 46 L2, break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'SubSetEq $L1 $T1 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lfxs.ma index 4ce37d910..e9785d6a3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lfxs.ma @@ -14,9 +14,18 @@ include "basic_2/rt_transition/cpx_lfxs.ma". include "basic_2/rt_transition/cpm_cpx.ma". +include "basic_2/rt_transition/cpr_ext.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) +(* Properties with context-sensitive free variables *************************) + +lemma cpm_frees_conf: ∀n,h,G. R_frees_confluent (cpm n h G). +/3 width=6 by cpm_fwd_cpx, cpx_frees_conf/ qed-. + +lemma lfpr_frees_conf: ∀h,G. lexs_frees_confluent (cpr_ext h G) cfull. +/5 width=9 by cpm_fwd_cpx, lfpx_frees_conf, lexs_co, cext2_co/ qed-. + (* Properties with generic extension on referred entries ********************) (* Basic_2A1: was just: cpr_llpx_sn_conf *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma index b47cd88bf..7d5c920c7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma @@ -12,14 +12,163 @@ (* *) (**************************************************************************) -include "basic_2/rt_transition/lfpx_frees.ma". +include "basic_2/relocation/drops_lexs.ma". +include "basic_2/static/frees_drops.ma". +include "basic_2/static/lsubf_frees.ma". +include "basic_2/static/lfxs.ma". +include "basic_2/rt_transition/cpx_drops.ma". +include "basic_2/rt_transition/cpx_ext.ma". (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************) +(* Properties with context-sensitive free variables *************************) + +(* Basic_2A1: uses: lpx_cpx_frees_trans *) +lemma cpx_frees_conf_lexs: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → + ∀L2. L1 ⪤*[cpx_ext h G, cfull, f1] L2 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 → + ∃∃f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1. +#h #G #L1 #T1 @(fqup_wf_ind_eq (Ⓣ) … G L1 T1) -G -L1 -T1 +#G0 #L0 #U0 #IH #G #L1 * * +[ -IH #s #HG #HL #HU #g1 #H1 #L2 #_ #U2 #H0 destruct + lapply (frees_inv_sort … H1) -H1 #Hg1 + elim (cpx_inv_sort1 … H0) -H0 #H destruct + /3 width=3 by frees_sort, sle_refl, ex2_intro/ +| #i #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct + elim (frees_inv_lref_drops … H1) -H1 * + [ -IH #f1 #HL1 #Hf1 #H destruct + elim (cpx_inv_lref1_drops … H0) -H0 + [ #H destruct + /4 width=9 by frees_atom_drops, drops_atom2_lexs_conf, sle_refl, ex2_intro/ + | * -H2 -Hf1 #I #K1 #V1 #V2 #HLK1 + lapply (drops_TF … HLK1) -HLK1 #HLK1 + lapply (drops_mono … HLK1 … HL1) -L1 #H destruct + ] + | #f1 #I #K1 #V1 #Hf1 #HLK1 #H destruct + elim (cpx_inv_lref1_drops … H0) -H0 + [ #H destruct + elim (lexs_drops_conf_next … H2 … HLK1) -H2 [ |*: // ] #Z #K2 #HLK2 #HK12 #H + elim (ext2_inv_pair_sn … H) -H #V2 #HV12 #H destruct + elim (IH … Hf1 … HK12 … HV12) /2 width=2 by fqup_lref/ -L1 -K1 -V1 #f2 #Hf2 #Hf21 + /4 width=7 by frees_lref_pushs, frees_pair_drops, drops_refl, sle_pushs, sle_next, ex2_intro/ + | * #Z #Y #X #V2 #H #HV12 #HVU2 + lapply (drops_mono … H … HLK1) -H #H destruct + elim (lexs_drops_conf_next … H2 … HLK1) -H2 [ |*: // ] #I2 #K2 #HLK2 #HK12 #H + elim (ext2_inv_pair_sn … H) -H #V0 #_ #H destruct + lapply (drops_isuni_fwd_drop2 … HLK2) // -V0 #HLK2 + elim (IH … Hf1 … HK12 … HV12) /2 width=2 by fqup_lref/ -I -L1 -K1 -V1 #f2 #Hf2 #Hf21 + lapply (frees_lifts … Hf2 … HLK2 … HVU2 ??) /4 width=7 by sle_weak, ex2_intro, sle_pushs/ + ] + | #f1 #I #K1 #HLK1 #Hf1 #H destruct + elim (cpx_inv_lref1_drops … H0) -H0 + [ -IH #H destruct + elim (lexs_drops_conf_next … H2 … HLK1) -H2 -HLK1 [ |*: // ] #Z #K2 #HLK2 #_ #H + lapply (ext2_inv_unit_sn … H) -H #H destruct + /3 width=3 by frees_unit_drops, sle_refl, ex2_intro/ + | * -H2 -Hf1 #Z #Y1 #X1 #X2 #HLY1 + lapply (drops_mono … HLK1 … HLY1) -L1 #H destruct + ] + ] +| -IH #l #HG #HL #HU #g1 #H1 #L2 #_ #U2 #H0 destruct + lapply (frees_inv_gref … H1) -H1 #Hg1 + lapply (cpx_inv_gref1 … H0) -H0 #H destruct + /3 width=3 by frees_gref, sle_refl, ex2_intro/ +| #p #I #V1 #T1 #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct + elim (frees_inv_bind … H1) -H1 #gV1 #gT1 #HgV1 #HgT1 #Hg1 + elim (cpx_inv_bind1 … H0) -H0 * + [ #V2 #T2 #HV12 #HT12 #H destruct + lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V + lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T + lapply (lexs_inv_tl … (BPair I V1) (BPair I V2) … HL12T ??) /2 width=1 by ext2_pair/ -HL12T #HL12T + elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21 + elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21 + elim (sor_isfin_ex gV2 (⫱gT2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ + /4 width=10 by frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/ + | #T2 #HT12 #HUT2 #H0 #H1 destruct -HgV1 + lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T + lapply (lexs_inv_tl … (BPair Abbr V1) (BPair Abbr V1) … HL12T ??) /2 width=1 by ext2_pair/ -HL12T #HL12T + elim (IH … HgT1 … HL12T … HT12) // -L1 -T1 #gT2 #HgT2 #HgT21 + lapply (frees_inv_lifts_SO (Ⓣ) … HgT2 … L2 … HUT2) [ /3 width=1 by drops_refl, drops_drop/ ] -V1 -T2 + /5 width=6 by sor_inv_sle_dx, sle_trans, sle_tl, ex2_intro/ + ] +| #I #V1 #T0 #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct + elim (frees_inv_flat … H1) -H1 #gV1 #gT0 #HgV1 #HgT0 #Hg1 + elim (cpx_inv_flat1 … H0) -H0 * + [ #V2 #T2 #HV12 #HT12 #H destruct + lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V + lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T + elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21 + elim (IH … HgT0 … HL12T … HT12) // -IH -HgT0 -HL12T -HT12 #gT2 #HgT2 #HgT21 + elim (sor_isfin_ex gV2 gT2) /2 width=3 by frees_fwd_isfin/ + /3 width=10 by frees_flat, monotonic_sle_sor, ex2_intro/ + | #HU2 #H destruct -HgV1 + lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T + elim (IH … HgT0 … HL12T … HU2) // -L1 -T0 -V1 + /4 width=6 by sor_inv_sle_dx, sle_trans, ex2_intro/ + | #HU2 #H destruct -HgT0 + lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ -H2 #HL12V + elim (IH … HgV1 … HL12V … HU2) // -L1 -T0 -V1 + /4 width=6 by sor_inv_sle_sn, sle_trans, ex2_intro/ + | #p #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #H0 #H1 #H destruct + elim (frees_inv_bind … HgT0) -HgT0 #gW1 #gT1 #HgW1 #HgT1 #HgT0 + lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V + lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2 + lapply (sle_lexs_trans … H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W + lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T + lapply (lexs_inv_tl … (BPair Abst W1) (BPair Abst W2) … HL12T ??) /2 width=1 by ext2_pair, I/ -HL12T #HL12T + elim (sor_isfin_ex gV1 gW1) /2 width=3 by frees_fwd_isfin/ #g0 #Hg0 #_ + lapply (sor_assoc_sn … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1 + lapply (sor_comm … Hg0) -Hg0 #Hg0 + elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21 + elim (IH … HgW1 … HL12W … HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21 + elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21 + elim (sor_isfin_ex (⫱gT2) gV2) /3 width=3 by frees_fwd_isfin, isfin_tl/ #gVT2 #HgVT2 #_ + elim (lsubf_beta_tl_dx … HgV2 … HgVT2 … W2) [ |*: /1 width=3 by lsubf_refl/ ] #gT0 #HL2 #HgT02 + lapply (lsubf_frees_trans … HgT2 … HL2) -HgT2 -HL2 #HgT0 + lapply (sor_comm … HgVT2) -HgVT2 #HgVT2 (**) (* this should be removed *) + elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #gV0 #HgV0 #H + elim (sor_isfin_ex gV0 (⫱gT0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_ + @(ex2_intro … g2) /3 width=5 by frees_flat, frees_bind/ -h -p -G -L1 -L2 -V1 -V2 -W1 -W2 -T1 -T2 + @(sor_inv_sle … Hg2) -Hg2 + [ /3 width=11 by sor_inv_sle_sn_trans, monotonic_sle_sor/ + | @(sle_trans … HgT02) -HgT02 + /3 width=8 by monotonic_sle_sor, sor_inv_sle_dx_trans, sle_tl/ + ] (**) (* full auto too slow *) + | #p #V2 #V #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #H0 #H1 #H destruct + elim (frees_inv_bind … HgT0) -HgT0 #gW1 #gT1 #HgW1 #HgT1 #HgT0 + lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V + lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2 + lapply (sle_lexs_trans … H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W + lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T + lapply (lexs_inv_tl … (BPair Abbr W1) (BPair Abbr W2) … HL12T ??) /2 width=1 by ext2_pair, I/ -HL12T #HL12T + elim (sor_isfin_ex gV1 gW1) /2 width=3 by frees_fwd_isfin/ #g0 #Hg0 #_ + lapply (sor_assoc_sn … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1 + elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21 + elim (IH … HgW1 … HL12W … HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21 + elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21 + elim (sor_isfin_ex (↑gV2) gT2) /3 width=3 by frees_fwd_isfin, isfin_push/ #gV0 #HgV0 #H + elim (sor_isfin_ex gW2 (⫱gV0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_ + elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_ + lapply (sor_assoc_sn … Hg2 … (⫱gT2) … Hg) /2 width=1 by sor_tl/ #Hg2 + lapply (frees_lifts (Ⓣ) … HgV2 … (L2.ⓓW2) … HV2 ??) + [4: lapply (sor_comm … Hg) |*: /3 width=3 by drops_refl, drops_drop/ ] -V2 (**) (* full auto too slow *) + /4 width=10 by frees_flat, frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/ + ] +] +qed-. + +(* Basic_2A1: uses: cpx_frees_trans *) +lemma cpx_frees_conf: ∀h,G. R_frees_confluent (cpx h G). +/4 width=7 by cpx_frees_conf_lexs, lexs_refl, ext2_refl/ qed-. + +(* Basic_2A1: uses: lpx_frees_trans *) +lemma lfpx_frees_conf: ∀h,G. lexs_frees_confluent (cpx_ext h G) cfull. +/2 width=7 by cpx_frees_conf_lexs/ qed-. + (* Properties with generic extension on referred entries ********************) (* Note: lemma 1000 *) -(* Basic_2A1: was just: cpx_llpx_sn_conf *) +(* Basic_2A1: uses: cpx_llpx_sn_conf *) lemma cpx_lfxs_conf: ∀R,h,G. s_r_confluent1 … (cpx h G) (lfxs R). #R #h #G #L1 #T1 #T2 #H #L2 * #f1 #Hf1 elim (cpx_frees_conf … Hf1 … H) -T1 /3 width=5 by sle_lexs_trans, ex2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_frees.ma deleted file mode 100644 index b79a65745..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_frees.ma +++ /dev/null @@ -1,27 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/lfpx_frees.ma". -include "basic_2/rt_transition/cpm_cpx.ma". -include "basic_2/rt_transition/cpr_ext.ma". - -(* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************) - -(* Properties with context-sensitive free variables *************************) - -lemma cpm_frees_conf: ∀n,h,G. R_frees_confluent (cpm n h G). -/3 width=6 by cpm_fwd_cpx, cpx_frees_conf/ qed-. - -lemma lfpr_frees_conf: ∀h,G. lexs_frees_confluent (cpr_ext h G) cfull. -/5 width=9 by cpm_fwd_cpx, lfpx_frees_conf, lexs_co, cext2_co/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma index 9f1831141..ee7978c14 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma @@ -14,11 +14,11 @@ include "basic_2/static/lfxs_lfxs.ma". include "basic_2/rt_transition/cpm_lsubr.ma". +include "basic_2/rt_transition/cpm_lfxs.ma". include "basic_2/rt_transition/cpr.ma". include "basic_2/rt_transition/cpr_drops.ma". include "basic_2/rt_transition/lfpr_drops.ma". include "basic_2/rt_transition/lfpr_fqup.ma". -include "basic_2/rt_transition/lfpr_frees.ma". (* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma deleted file mode 100644 index 15004fe7f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma +++ /dev/null @@ -1,167 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/relocation/drops_lexs.ma". -include "basic_2/static/frees_drops.ma". -include "basic_2/static/lsubf_frees.ma". -include "basic_2/static/lfxs.ma". -include "basic_2/rt_transition/cpx_drops.ma". -include "basic_2/rt_transition/cpx_ext.ma". - -(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****) - -(* Properties with context-sensitive free variables *************************) - -(* Basic_2A1: uses: lpx_cpx_frees_trans *) -(* check sle_refl *) -lemma cpx_frees_conf_lfpx: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → - ∀L2. L1 ⪤*[cpx_ext h G, cfull, f1] L2 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 → - ∃∃f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1. -#h #G #L1 #T1 @(fqup_wf_ind_eq (Ⓣ) … G L1 T1) -G -L1 -T1 -#G0 #L0 #U0 #IH #G #L1 * * -[ -IH #s #HG #HL #HU #g1 #H1 #L2 #_ #U2 #H0 destruct - lapply (frees_inv_sort … H1) -H1 #Hg1 - elim (cpx_inv_sort1 … H0) -H0 #H destruct - /3 width=3 by frees_sort, sle_refl, ex2_intro/ -| #i #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct - elim (frees_inv_lref_drops … H1) -H1 * - [ -IH #f1 #HL1 #Hf1 #H destruct - elim (cpx_inv_lref1_drops … H0) -H0 - [ #H destruct - /4 width=9 by frees_atom_drops, drops_atom2_lexs_conf, sle_refl, ex2_intro/ - | * -H2 -Hf1 #I #K1 #V1 #V2 #HLK1 - lapply (drops_TF … HLK1) -HLK1 #HLK1 - lapply (drops_mono … HLK1 … HL1) -L1 #H destruct - ] - | #f1 #I #K1 #V1 #Hf1 #HLK1 #H destruct - elim (cpx_inv_lref1_drops … H0) -H0 - [ #H destruct - elim (lexs_drops_conf_next … H2 … HLK1) -H2 [ |*: // ] #Z #K2 #HLK2 #HK12 #H - elim (ext2_inv_pair_sn … H) -H #V2 #HV12 #H destruct - elim (IH … Hf1 … HK12 … HV12) /2 width=2 by fqup_lref/ -L1 -K1 -V1 #f2 #Hf2 #Hf21 - /4 width=7 by frees_lref_pushs, frees_pair_drops, drops_refl, sle_pushs, sle_next, ex2_intro/ - | * #Z #Y #X #V2 #H #HV12 #HVU2 - lapply (drops_mono … H … HLK1) -H #H destruct - elim (lexs_drops_conf_next … H2 … HLK1) -H2 [ |*: // ] #I2 #K2 #HLK2 #HK12 #H - elim (ext2_inv_pair_sn … H) -H #V0 #_ #H destruct - lapply (drops_isuni_fwd_drop2 … HLK2) // -V0 #HLK2 - elim (IH … Hf1 … HK12 … HV12) /2 width=2 by fqup_lref/ -I -L1 -K1 -V1 #f2 #Hf2 #Hf21 - lapply (frees_lifts … Hf2 … HLK2 … HVU2 ??) /4 width=7 by sle_weak, ex2_intro, sle_pushs/ - ] - | #f1 #I #K1 #HLK1 #Hf1 #H destruct - elim (cpx_inv_lref1_drops … H0) -H0 - [ -IH #H destruct - elim (lexs_drops_conf_next … H2 … HLK1) -H2 -HLK1 [ |*: // ] #Z #K2 #HLK2 #_ #H - lapply (ext2_inv_unit_sn … H) -H #H destruct - /3 width=3 by frees_unit_drops, sle_refl, ex2_intro/ - | * -H2 -Hf1 #Z #Y1 #X1 #X2 #HLY1 - lapply (drops_mono … HLK1 … HLY1) -L1 #H destruct - ] - ] -| -IH #l #HG #HL #HU #g1 #H1 #L2 #_ #U2 #H0 destruct - lapply (frees_inv_gref … H1) -H1 #Hg1 - lapply (cpx_inv_gref1 … H0) -H0 #H destruct - /3 width=3 by frees_gref, sle_refl, ex2_intro/ -| #p #I #V1 #T1 #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct - elim (frees_inv_bind … H1) -H1 #gV1 #gT1 #HgV1 #HgT1 #Hg1 - elim (cpx_inv_bind1 … H0) -H0 * - [ #V2 #T2 #HV12 #HT12 #H destruct - lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V - lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T - lapply (lexs_inv_tl … (BPair I V1) (BPair I V2) … HL12T ??) /2 width=1 by ext2_pair/ -HL12T #HL12T - elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21 - elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21 - elim (sor_isfin_ex gV2 (⫱gT2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ - /4 width=10 by frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/ - | #T2 #HT12 #HUT2 #H0 #H1 destruct -HgV1 - lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T - lapply (lexs_inv_tl … (BPair Abbr V1) (BPair Abbr V1) … HL12T ??) /2 width=1 by ext2_pair/ -HL12T #HL12T - elim (IH … HgT1 … HL12T … HT12) // -L1 -T1 #gT2 #HgT2 #HgT21 - lapply (frees_inv_lifts_SO (Ⓣ) … HgT2 … L2 … HUT2) [ /3 width=1 by drops_refl, drops_drop/ ] -V1 -T2 - /5 width=6 by sor_inv_sle_dx, sle_trans, sle_tl, ex2_intro/ - ] -| #I #V1 #T0 #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct - elim (frees_inv_flat … H1) -H1 #gV1 #gT0 #HgV1 #HgT0 #Hg1 - elim (cpx_inv_flat1 … H0) -H0 * - [ #V2 #T2 #HV12 #HT12 #H destruct - lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V - lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T - elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21 - elim (IH … HgT0 … HL12T … HT12) // -IH -HgT0 -HL12T -HT12 #gT2 #HgT2 #HgT21 - elim (sor_isfin_ex gV2 gT2) /2 width=3 by frees_fwd_isfin/ - /3 width=10 by frees_flat, monotonic_sle_sor, ex2_intro/ - | #HU2 #H destruct -HgV1 - lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T - elim (IH … HgT0 … HL12T … HU2) // -L1 -T0 -V1 - /4 width=6 by sor_inv_sle_dx, sle_trans, ex2_intro/ - | #HU2 #H destruct -HgT0 - lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ -H2 #HL12V - elim (IH … HgV1 … HL12V … HU2) // -L1 -T0 -V1 - /4 width=6 by sor_inv_sle_sn, sle_trans, ex2_intro/ - | #p #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #H0 #H1 #H destruct - elim (frees_inv_bind … HgT0) -HgT0 #gW1 #gT1 #HgW1 #HgT1 #HgT0 - lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V - lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2 - lapply (sle_lexs_trans … H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W - lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T - lapply (lexs_inv_tl … (BPair Abst W1) (BPair Abst W2) … HL12T ??) /2 width=1 by ext2_pair, I/ -HL12T #HL12T - elim (sor_isfin_ex gV1 gW1) /2 width=3 by frees_fwd_isfin/ #g0 #Hg0 #_ - lapply (sor_assoc_sn … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1 - lapply (sor_comm … Hg0) -Hg0 #Hg0 - elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21 - elim (IH … HgW1 … HL12W … HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21 - elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21 - elim (sor_isfin_ex (⫱gT2) gV2) /3 width=3 by frees_fwd_isfin, isfin_tl/ #gVT2 #HgVT2 #_ - elim (lsubf_beta_tl_dx … HgV2 … HgVT2 … W2) [ |*: /1 width=3 by lsubf_refl/ ] #gT0 #HL2 #HgT02 - lapply (lsubf_frees_trans … HgT2 … HL2) -HgT2 -HL2 #HgT0 - lapply (sor_comm … HgVT2) -HgVT2 #HgVT2 (**) (* this should be removed *) - elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #gV0 #HgV0 #H - elim (sor_isfin_ex gV0 (⫱gT0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_ - @(ex2_intro … g2) /3 width=5 by frees_flat, frees_bind/ -h -p -G -L1 -L2 -V1 -V2 -W1 -W2 -T1 -T2 - @(sor_inv_sle … Hg2) -Hg2 - [ /3 width=11 by sor_inv_sle_sn_trans, monotonic_sle_sor/ - | @(sle_trans … HgT02) -HgT02 - /3 width=8 by monotonic_sle_sor, sor_inv_sle_dx_trans, sle_tl/ - ] (**) (* full auto too slow *) - | #p #V2 #V #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #H0 #H1 #H destruct - elim (frees_inv_bind … HgT0) -HgT0 #gW1 #gT1 #HgW1 #HgT1 #HgT0 - lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V - lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2 - lapply (sle_lexs_trans … H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W - lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T - lapply (lexs_inv_tl … (BPair Abbr W1) (BPair Abbr W2) … HL12T ??) /2 width=1 by ext2_pair, I/ -HL12T #HL12T - elim (sor_isfin_ex gV1 gW1) /2 width=3 by frees_fwd_isfin/ #g0 #Hg0 #_ - lapply (sor_assoc_sn … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1 - elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21 - elim (IH … HgW1 … HL12W … HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21 - elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21 - elim (sor_isfin_ex (↑gV2) gT2) /3 width=3 by frees_fwd_isfin, isfin_push/ #gV0 #HgV0 #H - elim (sor_isfin_ex gW2 (⫱gV0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_ - elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_ - lapply (sor_assoc_sn … Hg2 … (⫱gT2) … Hg) /2 width=1 by sor_tl/ #Hg2 - lapply (frees_lifts (Ⓣ) … HgV2 … (L2.ⓓW2) … HV2 ??) - [4: lapply (sor_comm … Hg) |*: /3 width=3 by drops_refl, drops_drop/ ] -V2 (**) (* full auto too slow *) - /4 width=10 by frees_flat, frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/ - ] -] -qed-. - -(* Basic_2A1: uses: cpx_frees_trans *) -lemma cpx_frees_conf: ∀h,G. R_frees_confluent (cpx h G). -/4 width=7 by cpx_frees_conf_lfpx, lexs_refl, ext2_refl/ qed-. - -(* Basic_2A1: uses: lpx_frees_trans *) -lemma lfpx_frees_conf: ∀h,G. lexs_frees_confluent (cpx_ext h G) cfull. -/2 width=7 by cpx_frees_conf_lfpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma index 22fe953b4..e7eae9096 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma @@ -15,8 +15,8 @@ include "basic_2/relocation/lifts_tdeq.ma". include "basic_2/static/lfxs_lfxs.ma". include "basic_2/static/lfdeq_fqup.ma". -include "basic_2/rt_transition/lfpx_frees.ma". -include "basic_2/rt_transition/lfpx.ma". (**) (* should be in lfpx_frees.ma *) +include "basic_2/rt_transition/cpx_lfxs.ma". +include "basic_2/rt_transition/lfpx.ma". (* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma new file mode 100644 index 000000000..1ba1b6c01 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma @@ -0,0 +1,51 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/relocation/rtmap_id.ma". +include "basic_2/notation/relations/subseteq_4.ma". +include "basic_2/static/frees.ma". + +(* FREE VARIABLES INCLUSION FOR RESTRICTED CLOSURES *************************) + +definition fle: bi_relation lenv term ≝ λL1,T1,L2,T2. + ∃∃f1,f2. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 & L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f1 ⊆ f2. + +interpretation "free variables inclusion (restricted closure)" + 'SubSetEq L1 T1 L2 T2 = (fle L1 T1 L2 T2). + +(* Basic properties *********************************************************) + +lemma fle_sort: ∀L1,L2,s1,s2. ⦃L1, ⋆s1⦄ ⊆ ⦃L2, ⋆s2⦄. +/3 width=5 by frees_sort, sle_refl, ex3_2_intro/ qed. + +lemma fle_gref: ∀L1,L2,l1,l2. ⦃L1, §l1⦄ ⊆ ⦃L2, §l2⦄. +/3 width=5 by frees_gref, sle_refl, ex3_2_intro/ qed. + +lemma fle_bind: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ → + ∀I1,I2,T1,T2. ⦃L1.ⓑ{I1}V1, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄ → + ∀p. ⦃L1, ⓑ{p,I1}V1.T1⦄ ⊆ ⦃L2, ⓑ{p,I2}V2.T2⦄. +#L1 #L2 #V1 #V2 * #f1 #g1 #HV1 #HV2 #Hfg1 #I1 #I2 #T1 #T2 * #f2 #g2 #Hf2 #Hg2 #Hfg2 #p +elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_ +elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_ +/4 width=12 by frees_bind, monotonic_sle_sor, sle_tl, ex3_2_intro/ +qed. + +lemma fle_flat: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ → + ∀T1,T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ → + ∀I1,I2. ⦃L1, ⓕ{I1}V1.T1⦄ ⊆ ⦃L2, ⓕ{I2}V2.T2⦄. +#L1 #L2 #V1 #V2 * #f1 #g1 #HV1 #HV2 #Hfg1 #T1 #T2 * #f2 #g2 #Hf2 #Hg2 #Hfg2 #I1 #I2 +elim (sor_isfin_ex f1 f2) /2 width=3 by frees_fwd_isfin/ #f #Hf #_ +elim (sor_isfin_ex g1 g2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_ +/3 width=12 by frees_flat, monotonic_sle_sor, ex3_2_intro/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle_drops.ma new file mode 100644 index 000000000..ca9549a06 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/fle_drops.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/frees_drops.ma". +include "basic_2/static/fle.ma". + +(* FREE VARIABLES INCLUSION FOR RESTRICTED CLOSURES *************************) + +(* Advanced properties ******************************************************) + +lemma fle_bind_dx: ∀T,U. ⬆*[1] T ≡ U → + ∀p,I,L,V. ⦃L, T⦄ ⊆ ⦃L, ⓑ{p,I}V.U⦄. +#T #U #HTU #p #I #L #V +elim (frees_total L V) #f1 #Hf1 +elim (frees_total L T) #f2 #Hf2 +elim (sor_isfin_ex f1 f2) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #H #_ +lapply (sor_inv_sle_dx … H) #Hf0 +>(tl_push_rew f) in H; #Hf +/6 width=6 by frees_lifts_SO, frees_bind, drops_refl, drops_drop, ex3_2_intro/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma new file mode 100644 index 000000000..77b284b11 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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/frees_frees.ma". +include "basic_2/static/fle.ma". + +(* FREE VARIABLES INCLUSION FOR RESTRICTED CLOSURES *************************) + +(* Main properties **********************************************************) + +theorem fle_trans: bi_transitive … fle. +#L1 #L #T1 #T * #f1 #f #HT1 #HT #Hf1 #L2 #T2 * #g #f2 #Hg #HT2 #Hf2 +/5 width=8 by frees_mono, sle_trans, sle_eq_repl_back2, ex3_2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fqup.ma new file mode 100644 index 000000000..23e460341 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fqup.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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/frees_fqup.ma". +include "basic_2/static/fle.ma". + +(* FREE VARIABLES INCLUSION FOR RESTRICTED CLOSURES *************************) + +(* Advanced properties ******************************************************) + +lemma fle_refl: bi_reflexive … fle. +#L #T elim (frees_total L T) /2 width=5 by sle_refl, ex3_2_intro/ +qed. + +lemma fle_bind_sn: ∀p,I,L,V,T. ⦃L, V⦄ ⊆ ⦃L, ⓑ{p,I}V.T⦄. +#p #I #L #V #T +elim (frees_total L V) #f1 #Hf1 +elim (frees_total (L.ⓑ{I}V) T) #f2 #Hf2 +elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_ +/3 width=6 by frees_bind, sor_inv_sle_sn, ex3_2_intro/ +qed. + +lemma fle_flat_sn: ∀I,L,V,T. ⦃L, V⦄ ⊆ ⦃L, ⓕ{I}V.T⦄. +#I #L #V #T +elim (frees_total L V) #f1 #Hf1 +elim (frees_total L T) #f2 #Hf2 +elim (sor_isfin_ex f1 f2) /2 width=3 by frees_fwd_isfin/ #f #Hf #_ +/3 width=6 by frees_flat, sor_inv_sle_sn, ex3_2_intro/ +qed. + +lemma fle_flat_dx: ∀I,L,V,T. ⦃L, T⦄ ⊆ ⦃L, ⓕ{I}V.T⦄. +#I #L #V #T +elim (frees_total L V) #f1 #Hf1 +elim (frees_total L T) #f2 #Hf2 +elim (sor_isfin_ex f1 f2) /2 width=3 by frees_fwd_isfin/ #f #Hf #_ +/3 width=6 by frees_flat, sor_inv_sle_dx, ex3_2_intro/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma index 0e1ae0e21..f24e50785 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma @@ -154,6 +154,12 @@ lemma frees_lifts: ∀b,f1,K,T. K ⊢ 𝐅*⦃T⦄ ≡ f1 → ] qed-. +lemma frees_lifts_SO: ∀b,L,K. ⬇*[b, 𝐔❴1❵] L ≡ K → ∀T,U. ⬆*[1] T ≡ U → + ∀f. K ⊢ 𝐅*⦃T⦄ ≡ f → L ⊢ 𝐅*⦃U⦄ ≡ ↑f. +#b #L #K #HLK #T #U #HTU #f #Hf +@(frees_lifts b … Hf … HTU) // (**) (* auto fails *) +qed. + (* Forward lemmas with generic slicing for local environments ***************) lemma frees_fwd_coafter: ∀b,f2,L,U. L ⊢ 𝐅*⦃U⦄ ≡ f2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fle.ma new file mode 100644 index 000000000..df8aec011 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fle.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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/frees_frees.ma". +include "basic_2/static/fle.ma". +include "basic_2/static/lfxs_lfxs.ma". + +(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) + +(* Properties with free variables inclusion for restricted closures *********) + +lemma fle_lfxs_trans: ∀R,L1,T1,T2. ⦃L1, T1⦄ ⊆ ⦃L1, T2⦄ → + ∀L2. L1 ⪤*[R, T2] L2 → L1 ⪤*[R, T1] L2. +#R #L1 #T1 #T2 * #f1 #f2 #Hf1 #Hf2 #Hf12 #L2 #HL12 +/4 width=5 by lfxs_inv_frees, sle_lexs_trans, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma new file mode 100644 index 000000000..11b3ca476 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/lex.ma". +include "basic_2/static/lfxs_fqup.ma". + +(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) + +(* Properties with generic extension of a context-sensitive relation ********) + +lemma lfxs_lex: ∀R,L1,L2. L1 ⪤[R] L2 → ∀T. L1 ⪤*[R, T] L2. +#R #L1 #L2 * #f #Hf #HL12 #T +elim (frees_total L1 T) #g #Hg +/4 width=5 by lexs_sdj, sdj_isid_sn, ex2_intro/ +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 dd6ed3880..ff9f5ecf7 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 @@ -126,7 +126,7 @@ table { } ] [ { "context-sensitive parallel r-transition" * } { - [ [ "for lenvs on referred entries" ] "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fquq" + "lfpr_fqup" + "lfpr_frees" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ] + [ [ "for lenvs on referred entries" ] "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fquq" + "lfpr_fqup" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ] [ [ "for binders" ] "cpr_ext ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" * ] [ [ "for terms" ] "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" * ] } @@ -137,7 +137,7 @@ table { ] [ { "uncounted context-sensitive parallel rt-transition" * } { [ [ "normal form for terms" ] "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ] - [ [ "for lenvs on referred entries" ] "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_cpx" + "lfpx_lfpx" * ] + [ [ "for lenvs on referred entries" ] "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_cpx" + "lfpx_lfpx" * ] [ [ "for lenvs on all entries" ] "lpx ( ⦃?,?⦄ ⊢ ⬈[?] ? )" * ] [ [ "for binders" ] "cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ] [ [ "for terms" ] "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" + "cpx_lfeq" * ] @@ -180,10 +180,11 @@ table { } ] [ { "generic extension of a context-sensitive relation" * } { - [ [ "for lenvs on referred entries" ] "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ] + [ [ "for lenvs on referred entries" ] "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_lex" + "lfxs_drops" + "lfxs_fqup" + "flxs_fle" + "lfxs_lfxs" * ] } ] [ { "context-sensitive free variables" * } { + [ [ "inclusion for restricted closures" ] "fle ( ⦃?,?⦄ ⊆ ⦃?,?⦄ )" "fle_drops" + "fle_fqup" + "fle_fle" * ] [ [ "restricted refinement for lenvs" ] "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_lsubr" + "lsubf_frees" + "lsubf_lsubf" * ] [ [ "for terms" ] "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_drops" + "frees_fqup" + "frees_frees" * ] }