From: Ferruccio Guidi Date: Fri, 26 Jul 2019 14:52:57 +0000 (+0200) Subject: still more additions and corrections for the article X-Git-Tag: make_still_working~241 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=f76594123e375bd7852c9421fe260a7bec693a92 still more additions and corrections for the article + new proof of csx_rsx + more results on jsx + extra parameter removed from jsx + minor corrections on lsubr + some renaming --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma index 472d81e84..5f1bf31a8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma @@ -31,7 +31,7 @@ generalize in match HT1; -HT1 | #i #H1i #IH #H2i elim (drops_ldec_dec L i) [ * #K #W #HLK | -H1i -IH #HnX ] [ lapply (cnv_inv_lref_pair … H2i … HLK) -H2i #H2W - lapply (csx_inv_lref_pair … HLK H1i) -H1i #H1W + lapply (csx_inv_lref_pair_drops … HLK H1i) -H1i #H1W elim (cpue_total_csx … H1W) -H1W #X elim (abst_dec X) [ * | -IH ] [ #p #V1 #U #H destruct * #n #HWU #_ diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/topredtysnstrong_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/topredtysnstrong_4.ma new file mode 100644 index 000000000..7b0f2e412 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/topredtysnstrong_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( G ⊢ break term 46 L1 ⊒[ break term 46 h] break term 46 L2 )" + non associative with precedence 45 + for @{ 'ToPRedTySNStrong $h $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/topredtysnstrong_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/topredtysnstrong_5.ma deleted file mode 100644 index a8ae47923..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/topredtysnstrong_5.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( G ⊢ break term 46 L1 ⊒[ break term 46 h, break term 46 f ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'ToPRedTySNStrong $h $f $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma index 456f38417..b0921440d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma @@ -19,22 +19,25 @@ include "basic_2/rt_computation/csx_drops.ma". (* Advanced properties ******************************************************) -lemma csx_tdeq_trans: ∀h,G,L,T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → - ∀T2. T1 ≛ T2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄. +lemma csx_tdeq_trans (h) (G): + ∀L,T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → + ∀T2. T1 ≛ T2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄. #h #G #L #T1 #H @(csx_ind … H) -T1 #T #_ #IH #T2 #HT2 @csx_intro #T1 #HT21 #HnT21 elim (tdeq_cpx_trans … HT2 … HT21) -HT21 /4 width=5 by tdeq_repl/ qed-. -lemma csx_cpx_trans: ∀h,G,L,T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → - ∀T2. ⦃G,L⦄ ⊢ T1 ⬈[h] T2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄. +lemma csx_cpx_trans (h) (G): + ∀L,T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → + ∀T2. ⦃G,L⦄ ⊢ T1 ⬈[h] T2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄. #h #G #L #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IHT1 #T2 #HLT12 elim (tdeq_dec T1 T2) /3 width=4 by csx_tdeq_trans/ qed-. (* Basic_1: was just: sn3_cast *) -lemma csx_cast: ∀h,G,L,W. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃W⦄ → - ∀T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓝW.T⦄. +lemma csx_cast (h) (G): + ∀L,W. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃W⦄ → + ∀T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓝW.T⦄. #h #G #L #W #HW @(csx_ind … HW) -W #W #HW #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT @csx_intro @@ -51,9 +54,10 @@ qed. (* Basic_1: was just: sn3_abbr *) (* Basic_2A1: was: csx_lref_bind *) -lemma csx_lref_pair: ∀h,I,G,L,K,V,i. ⬇*[i] L ≘ K.ⓑ{I}V → - ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄. -#h #I #G #L #K #V #i #HLK #HV +lemma csx_lref_pair_drops (h) (G): + ∀I,L,K,V,i. ⬇*[i] L ≘ K.ⓑ{I}V → + ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄. +#h #G #I #L #K #V #i #HLK #HV @csx_intro #X #H #Hi elim (cpx_inv_lref1_drops … H) -H [ #H destruct elim Hi // | -Hi * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HV1 @@ -66,17 +70,19 @@ qed. (* Basic_1: was: sn3_gen_def *) (* Basic_2A1: was: csx_inv_lref_bind *) -lemma csx_inv_lref_pair: ∀h,I,G,L,K,V,i. ⬇*[i] L ≘ K.ⓑ{I}V → - ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄ → ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄. -#h #I #G #L #K #V #i #HLK #Hi +lemma csx_inv_lref_pair_drops (h) (G): + ∀I,L,K,V,i. ⬇*[i] L ≘ K.ⓑ{I}V → + ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄ → ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄. +#h #G #I #L #K #V #i #HLK #Hi elim (lifts_total V (𝐔❴↑i❵)) /4 width=9 by csx_inv_lifts, csx_cpx_trans, cpx_delta_drops, drops_isuni_fwd_drop2/ qed-. -lemma csx_inv_lref: ∀h,G,L,i. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄ → - ∨∨ ⬇*[Ⓕ,𝐔❴i❵] L ≘ ⋆ - | ∃∃I,K. ⬇*[i] L ≘ K.ⓤ{I} - | ∃∃I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V & ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄. +lemma csx_inv_lref_drops (h) (G): + ∀L,i. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄ → + ∨∨ ⬇*[Ⓕ,𝐔❴i❵] L ≘ ⋆ + | ∃∃I,K. ⬇*[i] L ≘ K.ⓤ{I} + | ∃∃I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V & ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄. #h #G #L #i #H elim (drops_F_uni L i) /2 width=1 by or3_intro0/ -* * /4 width=9 by csx_inv_lref_pair, ex2_3_intro, ex1_2_intro, or3_intro2, or3_intro1/ +* * /4 width=9 by csx_inv_lref_pair_drops, ex2_3_intro, ex1_2_intro, or3_intro2, or3_intro1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma index 889eddcfe..054fb100b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma @@ -23,9 +23,10 @@ include "basic_2/rt_computation/csx_vector.ma". (* Advanced properties ************************************* ****************) (* Basic_1: was just: sn3_appls_beta *) -lemma csx_applv_beta: ∀h,p,G,L,Vs,V,W,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.ⓓ{p}ⓝW.V.T⦄ → - ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.ⓐV.ⓛ{p}W.T⦄. -#h #p #G #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/ +lemma csx_applv_beta (h) (G): + ∀p,L,Vs,V,W,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.ⓓ{p}ⓝW.V.T⦄ → + ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.ⓐV.ⓛ{p}W.T⦄. +#h #G #p #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/ #V0 #Vs #IHV #V #W #T #H1T lapply (csx_fwd_pair_sn … H1T) #HV0 lapply (csx_fwd_flat_dx … H1T) #H2T @@ -37,11 +38,12 @@ elim (cpxs_fwd_beta_vector … H) -H #H ] qed. -lemma csx_applv_delta: ∀h,I,G,L,K,V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 → - ∀V2. ⬆*[↑i] V1 ≘ V2 → - ∀Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.V2⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.#i⦄. -#h #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs -[ /4 width=11 by csx_inv_lifts, csx_lref_pair, drops_isuni_fwd_drop2/ +lemma csx_applv_delta_drops (h) (G): + ∀I,L,K,V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 → + ∀V2. ⬆*[↑i] V1 ≘ V2 → + ∀Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.V2⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.#i⦄. +#h #G #I #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs +[ /4 width=11 by csx_inv_lifts, csx_lref_pair_drops, drops_isuni_fwd_drop2/ | #V #Vs #IHV #H1T lapply (csx_fwd_pair_sn … H1T) #HV lapply (csx_fwd_flat_dx … H1T) #H2T @@ -55,10 +57,10 @@ lemma csx_applv_delta: ∀h,I,G,L,K,V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 → qed. (* Basic_1: was just: sn3_appls_abbr *) -lemma csx_applv_theta: ∀h,p,G,L,V1b,V2b. ⬆*[1] V1b ≘ V2b → - ∀V,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}V.ⒶV2b.T⦄ → - ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶV1b.ⓓ{p}V.T⦄. -#h #p #G #L #V1b #V2b * -V1b -V2b /2 width=1 by/ +lemma csx_applv_theta (h) (G): + ∀p,L,V1b,V2b. ⬆*[1] V1b ≘ V2b → + ∀V,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}V.ⒶV2b.T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶV1b.ⓓ{p}V.T⦄. +#h #G #p #L #V1b #V2b * -V1b -V2b /2 width=1 by/ #V1b #V2b #V1 #V2 #HV12 #H generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1 elim H -V1b -V2b /2 width=3 by csx_appl_theta/ @@ -74,8 +76,9 @@ elim (cpxs_fwd_theta_vector … (V2⨮V2b) … H1) -H1 /2 width=1 by liftsv_cons qed. (* Basic_1: was just: sn3_appls_cast *) -lemma csx_applv_cast: ∀h,G,L,Vs,U. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.U⦄ → - ∀T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.ⓝU.T⦄. +lemma csx_applv_cast (h) (G): + ∀L,Vs,U. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.U⦄ → + ∀T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.ⓝU.T⦄. #h #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/ #V #Vs #IHV #U #H1U #T #H1T lapply (csx_fwd_pair_sn … H1U) #HV diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma index acef276fa..c35a584bb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma @@ -19,10 +19,11 @@ include "basic_2/rt_computation/csx_lsubr.ma". (* Properties with extended supclosure **************************************) -lemma csx_fqu_conf: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂[b] ⦃G2,L2,T2⦄ → - ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄. +lemma csx_fqu_conf (h) (b): + ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂[b] ⦃G2,L2,T2⦄ → + ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄. #h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -[ /3 width=5 by csx_inv_lref_pair, drops_refl/ +[ /3 width=5 by csx_inv_lref_pair_drops, drops_refl/ | /2 width=3 by csx_fwd_pair_sn/ | /2 width=2 by csx_fwd_bind_dx/ | /2 width=4 by csx_fwd_bind_dx_unit/ @@ -31,20 +32,23 @@ lemma csx_fqu_conf: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂[b] ⦃G2,L2,T2 ] qed-. -lemma csx_fquq_conf: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂⸮[b] ⦃G2,L2,T2⦄ → - ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄. +lemma csx_fquq_conf (h) (b): + ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂⸮[b] ⦃G2,L2,T2⦄ → + ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄. #h #b #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=6 by csx_fqu_conf/ * #HG #HL #HT destruct // qed-. -lemma csx_fqup_conf: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂+[b] ⦃G2,L2,T2⦄ → - ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄. +lemma csx_fqup_conf (h) (b): + ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂+[b] ⦃G2,L2,T2⦄ → + ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄. #h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 /3 width=6 by csx_fqu_conf/ qed-. -lemma csx_fqus_conf: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂*[b] ⦃G2,L2,T2⦄ → - ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄. +lemma csx_fqus_conf (h) (b): + ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂*[b] ⦃G2,L2,T2⦄ → + ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄. #h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -H /3 width=6 by csx_fquq_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma index a757a9374..d0644bbf5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma @@ -20,13 +20,13 @@ include "basic_2/rt_computation/csx_csx_vector.ma". (* Main properties with generic candidates of reducibility ******************) -theorem csx_gcr: ∀h. gcr (cpx h) tdeq (csx h) (csx h). +theorem csx_gcr (h): gcr (cpx h) tdeq (csx h) (csx h). #h @mk_gcr [ // | #G #L #Vs #Hvs #T #HT #H @(csx_applv_cnx … H) -H // (**) (* auto fails *) | /2 width=1 by csx_applv_beta/ -| /2 width=7 by csx_applv_delta/ +| /2 width=7 by csx_applv_delta_drops/ | /3 width=3 by csx_applv_theta, csx_abbr/ | /2 width=1 by csx_applv_cast/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma index ed06dcdea..8c4f35b6c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma @@ -19,17 +19,19 @@ include "basic_2/rt_computation/csx_cpxs.ma". (* Properties with unbound parallel rt-transition on all entries ************) -lemma csx_lpx_conf: ∀h,G,L1,T. ⦃G,L1⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → - ∀L2. ⦃G,L1⦄ ⊢ ⬈[h] L2 → ⦃G,L2⦄ ⊢ ⬈*[h] 𝐒⦃T⦄. +lemma csx_lpx_conf (h) (G): + ∀L1,T. ⦃G,L1⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → + ∀L2. ⦃G,L1⦄ ⊢ ⬈[h] L2 → ⦃G,L2⦄ ⊢ ⬈*[h] 𝐒⦃T⦄. #h #G #L1 #T #H @(csx_ind_cpxs … H) -T /4 width=3 by csx_intro, lpx_cpx_trans/ qed-. (* Advanced properties ******************************************************) -lemma csx_abst: ∀h,p,G,L,W. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃W⦄ → - ∀T. ⦃G,L.ⓛW⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓛ{p}W.T⦄. -#h #p #G #L #W #HW +lemma csx_abst (h) (G): + ∀p,L,W. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃W⦄ → + ∀T. ⦃G,L.ⓛW⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓛ{p}W.T⦄. +#h #G #p #L #W #HW @(csx_ind … HW) -W #W #_ #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT @csx_intro #X #H1 #H2 @@ -42,9 +44,10 @@ elim (tdneq_inv_pair … H2) -H2 ] qed. -lemma csx_abbr: ∀h,p,G,L,V. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → - ∀T. ⦃G,L.ⓓV⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}V.T⦄. -#h #p #G #L #V #HV +lemma csx_abbr (h) (G): + ∀p,L,V. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → + ∀T. ⦃G,L.ⓓV⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}V.T⦄. +#h #G #p #L #V #HV @(csx_ind … HV) -V #V #_ #IHV #T #HT @(csx_ind_cpxs … HT) -T #T #HT #IHT @csx_intro #X #H1 #H2 @@ -60,9 +63,17 @@ elim (cpx_inv_abbr1 … H1) -H1 * ] qed. -fact csx_appl_theta_aux: ∀h,p,G,L,U. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃U⦄ → ∀V1,V2. ⬆*[1] V1 ≘ V2 → - ∀V,T. U = ⓓ{p}V.ⓐV2.T → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄. -#h #p #G #L #X #H +lemma csx_bind (h) (G): + ∀p,I,L,V. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → + ∀T. ⦃G,L.ⓑ{I}V⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓑ{p,I}V.T⦄. +#h #G #p * #L #V #HV #T #HT +/2 width=1 by csx_abbr, csx_abst/ +qed. + +fact csx_appl_theta_aux (h) (G): + ∀p,L,U. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃U⦄ → ∀V1,V2. ⬆*[1] V1 ≘ V2 → + ∀V,T. U = ⓓ{p}V.ⓐV2.T → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄. +#h #G #p #L #X #H @(csx_ind_cpxs … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct lapply (csx_fwd_pair_sn … HVT) #HV lapply (csx_fwd_bind_dx … HVT) -HVT #HVT @@ -94,6 +105,7 @@ elim (cpx_inv_appl1 … HL) -HL * ] qed-. -lemma csx_appl_theta: ∀h,p,G,L,V,V2,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}V.ⓐV2.T⦄ → - ∀V1. ⬆*[1] V1 ≘ V2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄. +lemma csx_appl_theta (h) (G): + ∀p,L,V,V2,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}V.ⓐV2.T⦄ → + ∀V1. ⬆*[1] V1 ≘ V2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄. /2 width=5 by csx_appl_theta_aux/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma index 07226df19..5e32b0e6d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lsubr.ma @@ -19,9 +19,10 @@ include "basic_2/rt_computation/csx_csx.ma". (* Advanced properties ******************************************************) -fact csx_appl_beta_aux: ∀h,p,G,L,U1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃U1⦄ → - ∀V,W,T1. U1 = ⓓ{p}ⓝW.V.T1 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.ⓛ{p}W.T1⦄. -#h #p #G #L #X #H @(csx_ind … H) -X +fact csx_appl_beta_aux (h) (G): + ∀p,L,U1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃U1⦄ → + ∀V,W,T1. U1 = ⓓ{p}ⓝW.V.T1 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.ⓛ{p}W.T1⦄. +#h #G #p #L #X #H @(csx_ind … H) -X #X #HT1 #IHT1 #V #W #T1 #H1 destruct @csx_intro #X #H1 #H2 elim (cpx_inv_appl1 … H1) -H1 * @@ -42,23 +43,37 @@ elim (cpx_inv_appl1 … H1) -H1 * qed-. (* Basic_1: was just: sn3_beta *) -lemma csx_appl_beta: ∀h,p,G,L,V,W,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}ⓝW.V.T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.ⓛ{p}W.T⦄. +lemma csx_appl_beta (h) (G): + ∀p,L,V,W,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}ⓝW.V.T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.ⓛ{p}W.T⦄. /2 width=3 by csx_appl_beta_aux/ qed. (* Advanced forward lemmas **************************************************) -fact csx_fwd_bind_dx_unit_aux: ∀h,G,L,U. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃U⦄ → - ∀p,I,J,V,T. U = ⓑ{p,I}V.T → ⦃G,L.ⓤ{J}⦄ ⊢ ⬈*[h] 𝐒⦃T⦄. +fact csx_fwd_bind_dx_unit_aux (h) (G): + ∀L,U. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃U⦄ → + ∀p,I,J,V,T. U = ⓑ{p,I}V.T → ⦃G,L.ⓤ{J}⦄ ⊢ ⬈*[h] 𝐒⦃T⦄. #h #G #L #U #H elim H -H #U0 #_ #IH #p #I #J #V #T #H destruct @csx_intro #T2 #HLT2 #HT2 @(IH (ⓑ{p, I}V.T2)) -IH /2 width=4 by cpx_bind_unit/ -HLT2 #H elim (tdeq_inv_pair … H) -H /2 width=1 by/ qed-. -lemma csx_fwd_bind_dx_unit: ∀h,p,I,G,L,V,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓑ{p,I}V.T⦄ → - ∀J. ⦃G,L.ⓤ{J}⦄ ⊢ ⬈*[h] 𝐒⦃T⦄. +lemma csx_fwd_bind_dx_unit (h) (G): + ∀p,I,L,V,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓑ{p,I}V.T⦄ → + ∀J. ⦃G,L.ⓤ{J}⦄ ⊢ ⬈*[h] 𝐒⦃T⦄. /2 width=6 by csx_fwd_bind_dx_unit_aux/ qed-. -lemma csx_fwd_bind_unit: ∀h,p,I,G,L,V,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓑ{p,I}V.T⦄ → - ∀J. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ ∧ ⦃G,L.ⓤ{J}⦄ ⊢ ⬈*[h] 𝐒⦃T⦄. +lemma csx_fwd_bind_unit (h) (G): + ∀p,I,L,V,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓑ{p,I}V.T⦄ → + ∀J. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ ∧ ⦃G,L.ⓤ{J}⦄ ⊢ ⬈*[h] 𝐒⦃T⦄. /3 width=4 by csx_fwd_pair_sn, csx_fwd_bind_dx_unit, conj/ qed-. + +(* Properties with restricted refinement for local environments *************) + +lemma csx_lsubr_conf (h) (G): + ∀L1,T. ⦃G,L1⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ∀L2. L1 ⫃ L2 → ⦃G,L2⦄ ⊢ ⬈*[h] 𝐒⦃T⦄. +#h #G #L1 #T #H +@(csx_ind … H) -T #T1 #_ #IH #L2 #HL12 +@csx_intro #T2 #HT12 #HnT12 +/3 width=3 by lsubr_cpx_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx.ma index 94a1ec855..9521a9b27 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx.ma @@ -12,151 +12,91 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/topredtysnstrong_5.ma". +include "basic_2/notation/relations/topredtysnstrong_4.ma". include "basic_2/rt_computation/rsx.ma". (* COMPATIBILITY OF STRONG NORMALIZATION FOR UNBOUND RT-TRANSITION **********) (* Note: this should be an instance of a more general sex *) (* Basic_2A1: uses: lcosx *) -inductive jsx (h) (G): rtmap → relation lenv ≝ -| jsx_atom: ∀f. jsx h G f (⋆) (⋆) -| jsx_push: ∀f,I,K1,K2. jsx h G f K1 K2 → - jsx h G (⫯f) (K1.ⓘ{I}) (K2.ⓘ{I}) -| jsx_unit: ∀f,I,K1,K2. jsx h G f K1 K2 → - jsx h G (↑f) (K1.ⓤ{I}) (K2.ⓧ) -| jsx_pair: ∀f,I,K1,K2,V. G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ → - jsx h G f K1 K2 → jsx h G (↑f) (K1.ⓑ{I}V) (K2.ⓧ) +inductive jsx (h) (G): relation lenv ≝ +| jsx_atom: jsx h G (⋆) (⋆) +| jsx_bind: ∀I,K1,K2. jsx h G K1 K2 → + jsx h G (K1.ⓘ{I}) (K2.ⓘ{I}) +| jsx_pair: ∀I,K1,K2,V. jsx h G K1 K2 → + G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ → jsx h G (K1.ⓑ{I}V) (K2.ⓧ) . interpretation "strong normalization for unbound parallel rt-transition (compatibility)" - 'ToPRedTySNStrong h f G L1 L2 = (jsx h G f L1 L2). + 'ToPRedTySNStrong h G L1 L2 = (jsx h G L1 L2). (* Basic inversion lemmas ***************************************************) fact jsx_inv_atom_sn_aux (h) (G): - ∀g,L1,L2. G ⊢ L1 ⊒[h,g] L2 → L1 = ⋆ → L2 = ⋆. -#h #G #g #L1 #L2 * -g -L1 -L2 // -[ #f #I #K1 #K2 #_ #H destruct -| #f #I #K1 #K2 #_ #H destruct -| #f #I #K1 #K2 #V #_ #_ #H destruct + ∀L1,L2. G ⊢ L1 ⊒[h] L2 → L1 = ⋆ → L2 = ⋆. +#h #G #L1 #L2 * -L1 -L2 +[ // +| #I #K1 #K2 #_ #H destruct +| #I #K1 #K2 #V #_ #_ #H destruct ] qed-. -lemma jsx_inv_atom_sn (h) (G): ∀g,L2. G ⊢ ⋆ ⊒[h,g] L2 → L2 = ⋆. -/2 width=7 by jsx_inv_atom_sn_aux/ qed-. - -fact jsx_inv_push_sn_aux (h) (G): - ∀g,L1,L2. G ⊢ L1 ⊒[h,g] L2 → - ∀f,I,K1. g = ⫯f → L1 = K1.ⓘ{I} → - ∃∃K2. G ⊢ K1 ⊒[h,f] K2 & L2 = K2.ⓘ{I}. -#h #G #g #L1 #L2 * -g -L1 -L2 -[ #f #g #J #L1 #_ #H destruct -| #f #I #K1 #K2 #HK12 #g #J #L1 #H1 #H2 destruct - <(injective_push … H1) -g /2 width=3 by ex2_intro/ -| #f #I #K1 #K2 #_ #g #J #L1 #H - elim (discr_next_push … H) -| #f #I #K1 #K2 #V #_ #_ #g #J #L1 #H - elim (discr_next_push … H) +lemma jsx_inv_atom_sn (h) (G): ∀L2. G ⊢ ⋆ ⊒[h] L2 → L2 = ⋆. +/2 width=5 by jsx_inv_atom_sn_aux/ qed-. + +fact jsx_inv_bind_sn_aux (h) (G): + ∀L1,L2. G ⊢ L1 ⊒[h] L2 → + ∀I,K1. L1 = K1.ⓘ{I} → + ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓘ{I} + | ∃∃J,K2,V. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ & I = BPair J V & L2 = K2.ⓧ. +#h #G #L1 #L2 * -L1 -L2 +[ #J #L1 #H destruct +| #I #K1 #K2 #HK12 #J #L1 #H destruct /3 width=3 by ex2_intro, or_introl/ +| #I #K1 #K2 #V #HK12 #HV #J #L1 #H destruct /3 width=7 by ex4_3_intro, or_intror/ ] qed-. -lemma jsx_inv_push_sn (h) (G): - ∀f,I,K1,L2. G ⊢ K1.ⓘ{I} ⊒[h,⫯f] L2 → - ∃∃K2. G ⊢ K1 ⊒[h,f] K2 & L2 = K2.ⓘ{I}. -/2 width=5 by jsx_inv_push_sn_aux/ qed-. - -fact jsx_inv_unit_sn_aux (h) (G): - ∀g,L1,L2. G ⊢ L1 ⊒[h,g] L2 → - ∀f,I,K1. g = ↑f → L1 = K1.ⓤ{I} → - ∃∃K2. G ⊢ K1 ⊒[h,f] K2 & L2 = K2.ⓧ. -#h #G #g #L1 #L2 * -g -L1 -L2 -[ #f #g #J #L1 #_ #H destruct -| #f #I #K1 #K2 #_ #g #J #L1 #H - elim (discr_push_next … H) -| #f #I #K1 #K2 #HK12 #g #J #L1 #H1 #H2 destruct - <(injective_next … H1) -g /2 width=3 by ex2_intro/ -| #f #I #K1 #K2 #V #_ #_ #g #J #L1 #_ #H destruct -] -qed-. +lemma jsx_inv_bind_sn (h) (G): + ∀I,K1,L2. G ⊢ K1.ⓘ{I} ⊒[h] L2 → + ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓘ{I} + | ∃∃J,K2,V. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ & I = BPair J V & L2 = K2.ⓧ. +/2 width=3 by jsx_inv_bind_sn_aux/ qed-. -lemma jsx_inv_unit_sn (h) (G): - ∀f,I,K1,L2. G ⊢ K1.ⓤ{I} ⊒[h,↑f] L2 → - ∃∃K2. G ⊢ K1 ⊒[h,f] K2 & L2 = K2.ⓧ. -/2 width=6 by jsx_inv_unit_sn_aux/ qed-. - -fact jsx_inv_pair_sn_aux (h) (G): - ∀g,L1,L2. G ⊢ L1 ⊒[h,g] L2 → - ∀f,I,K1,V. g = ↑f → L1 = K1.ⓑ{I}V → - ∃∃K2. G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ & G ⊢ K1 ⊒[h,f] K2 & L2 = K2.ⓧ. -#h #G #g #L1 #L2 * -g -L1 -L2 -[ #f #g #J #L1 #W #_ #H destruct -| #f #I #K1 #K2 #_ #g #J #L1 #W #H - elim (discr_push_next … H) -| #f #I #K1 #K2 #_ #g #J #L1 #W #_ #H destruct -| #f #I #K1 #K2 #V #HV #HK12 #g #J #L1 #W #H1 #H2 destruct - <(injective_next … H1) -g /2 width=4 by ex3_intro/ -] -qed-. +(* Advanced inversion lemmas ************************************************) (* Basic_2A1: uses: lcosx_inv_pair *) lemma jsx_inv_pair_sn (h) (G): - ∀f,I,K1,L2,V. G ⊢ K1.ⓑ{I}V ⊒[h,↑f] L2 → - ∃∃K2. G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ & G ⊢ K1 ⊒[h,f] K2 & L2 = K2.ⓧ. -/2 width=6 by jsx_inv_pair_sn_aux/ qed-. - -(* Advanced inversion lemmas ************************************************) - -lemma jsx_inv_pair_sn_gen (h) (G): ∀g,I,K1,L2,V. G ⊢ K1.ⓑ{I}V ⊒[h,g] L2 → - ∨∨ ∃∃f,K2. G ⊢ K1 ⊒[h,f] K2 & g = ⫯f & L2 = K2.ⓑ{I}V - | ∃∃f,K2. G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ & G ⊢ K1 ⊒[h,f] K2 & g = ↑f & L2 = K2.ⓧ. -#h #G #g #I #K1 #L2 #V #H -elim (pn_split g) * #f #Hf destruct -[ elim (jsx_inv_push_sn … H) -H /3 width=5 by ex3_2_intro, or_introl/ -| elim (jsx_inv_pair_sn … H) -H /3 width=6 by ex4_2_intro, or_intror/ + ∀I,K1,L2,V. G ⊢ K1.ⓑ{I}V ⊒[h] L2 → + ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓑ{I}V + | ∃∃K2. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ & L2 = K2.ⓧ. +#h #G #I #K1 #L2 #V #H elim (jsx_inv_bind_sn … H) -H * +[ /3 width=3 by ex2_intro, or_introl/ +| #J #K2 #X #HK12 #HX #H1 #H2 destruct /3 width=4 by ex3_intro, or_intror/ ] qed-. +lemma jsx_inv_void_sn (h) (G): + ∀K1,L2. G ⊢ K1.ⓧ ⊒[h] L2 → + ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓧ. +#h #G #K1 #L2 #H elim (jsx_inv_bind_sn … H) -H * +/2 width=3 by ex2_intro/ +qed-. + (* Advanced forward lemmas **************************************************) lemma jsx_fwd_bind_sn (h) (G): - ∀g,I1,K1,L2. G ⊢ K1.ⓘ{I1} ⊒[h,g] L2 → - ∃∃I2,K2. G ⊢ K1 ⊒[h,⫱g] K2 & L2 = K2.ⓘ{I2}. -#h #G #g #I1 #K1 #L2 -elim (pn_split g) * #f #Hf destruct -[ #H elim (jsx_inv_push_sn … H) -H -| cases I1 -I1 #I1 - [ #H elim (jsx_inv_unit_sn … H) -H - | #V #H elim (jsx_inv_pair_sn … H) -H - ] -] + ∀I1,K1,L2. G ⊢ K1.ⓘ{I1} ⊒[h] L2 → + ∃∃I2,K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓘ{I2}. +#h #G #I1 #K1 #L2 #H elim (jsx_inv_bind_sn … H) -H * /2 width=4 by ex2_2_intro/ qed-. -(* Basic properties *********************************************************) - -lemma jsx_eq_repl_back (h) (G): ∀L1,L2. eq_repl_back … (λf. G ⊢ L1 ⊒[h,f] L2). -#h #G #L1 #L2 #f1 #H elim H -L1 -L2 -f1 // -[ #f #I #L1 #L2 #_ #IH #x #H - elim (eq_inv_px … H) -H /3 width=3 by jsx_push/ -| #f #I #L1 #L2 #_ #IH #x #H - elim (eq_inv_nx … H) -H /3 width=3 by jsx_unit/ -| #f #I #L1 #L2 #V #HV #_ #IH #x #H - elim (eq_inv_nx … H) -H /3 width=3 by jsx_pair/ -] -qed-. - -lemma jsx_eq_repl_fwd (h) (G): ∀L1,L2. eq_repl_fwd … (λf. G ⊢ L1 ⊒[h,f] L2). -#h #G #L1 #L2 @eq_repl_sym /2 width=3 by jsx_eq_repl_back/ -qed-. - (* Advanced properties ******************************************************) (* Basic_2A1: uses: lcosx_O *) -lemma jsx_refl (h) (G): ∀f. 𝐈⦃f⦄ → reflexive … (jsx h G f). -#h #G #f #Hf #L elim L -L -/3 width=3 by jsx_eq_repl_back, jsx_push, eq_push_inv_isid/ +lemma jsx_refl (h) (G): reflexive … (jsx h G). +#h #G #L elim L -L /2 width=1 by jsx_atom, jsx_bind/ qed. (* Basic_2A1: removed theorems 2: diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma new file mode 100644 index 000000000..b8e919b73 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_csx.ma @@ -0,0 +1,61 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rsx_csx.ma". +include "basic_2/rt_computation/jsx_drops.ma". +include "basic_2/rt_computation/jsx_lsubr.ma". + +(* COMPATIBILITY OF STRONG NORMALIZATION FOR UNBOUND RT-TRANSITION **********) + +(* Properties with strongly rt-normalizing terms ****************************) + +lemma jsx_csx_conf (h) (G): + ∀L1,L2. G ⊢ L1 ⊒[h] L2 → + ∀T. ⦃G,L1⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L2⦄ ⊢ ⬈*[h] 𝐒⦃T⦄. +/3 width=5 by jsx_fwd_lsubr, csx_lsubr_conf/ qed-. + +(* Properties with strongly rt-normalizing referred local environments ******) + +(* Note: Try by induction on the 2nd premise by generalizing V with f *) +lemma rsx_jsx_trans (h) (G): + ∀L1,V. G ⊢ ⬈*[h,V] 𝐒⦃L1⦄ → + ∀L2. G ⊢ L1 ⊒[h] L2 → G ⊢ ⬈*[h,V] 𝐒⦃L2⦄. +#h #G #L1 #V @(fqup_wf_ind_eq (Ⓕ) … G L1 V) -G -L1 -V +#G0 #L0 #V0 #IH #G #L1 * * +[ // +| #i #HG #HL #HV #H #L2 #HL12 destruct + elim (rsx_inv_lref_drops … H) -H [|*: * ] + [ #HL1 -IH + lapply (jsx_fwd_drops_atom_sn … HL12 … HL1) -L1 + /2 width=1 by rsx_lref_atom_drops/ + | #I #K1 #HLK1 -IH + elim (jsx_fwd_drops_unit_sn … HL12 … HLK1) -L1 [| // ] #K2 #HK12 #HLK2 + /2 width=3 by rsx_lref_unit_drops/ + | #I #K1 #V1 #HLK1 #HV1 #HK1 + elim (jsx_fwd_drops_pair_sn … HL12 … HLK1) -HL12 [3: // |*: * ] + [ #K2 #HK12 #HLK2 + /4 width=6 by rsx_lref_pair_drops, jsx_csx_conf, fqup_lref/ + | #K2 #_ #HLK2 #_ + /2 width=3 by rsx_lref_unit_drops/ + ] + ] +| // +| #p #I #V #T #HG #HL #HV #H #L2 #HL12 destruct + elim (rsx_inv_bind_void … H) -H #HV #HT + /4 width=4 by jsx_bind, rsx_bind_void/ +| #I #V #T #HG #HL #HV #H #L2 #HL12 destruct + elim (rsx_inv_flat … H) -H #HV #HT + /3 width=4 by rsx_flat/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma new file mode 100644 index 000000000..93368d554 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma @@ -0,0 +1,75 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/relocation/drops.ma". +include "basic_2/rt_computation/jsx.ma". + +(* COMPATIBILITY OF STRONG NORMALIZATION FOR UNBOUND RT-TRANSITION **********) + +(* Forward lemmas with uniform slicing for local environments ***************) + +lemma jsx_fwd_drops_atom_sn (h) (b) (G): + ∀L1,L2. G ⊢ L1 ⊒[h] L2 → + ∀f. 𝐔⦃f⦄ → ⬇*[b,f]L1 ≘ ⋆ → ⬇*[b,f]L2 ≘ ⋆. +#h #b #G #L1 #L2 #H elim H -L1 -L2 +[ #f #_ #H // +| #I #K1 #K2 #_ #IH #f #Hf #H +| #I #K1 #K2 #V #_ #HV #IH #f #Hf #H +] +elim (drops_inv_bind1_isuni … H) -H [3,6: // |*: * -Hf ] +[1,3: #_ #H destruct +|2,4: #g #Hg #HK1 #H destruct /3 width=1 by drops_drop/ +] +qed-. + +lemma jsx_fwd_drops_unit_sn (h) (b) (G): + ∀L1,L2. G ⊢ L1 ⊒[h] L2 → + ∀f. 𝐔⦃f⦄ → ∀I,K1. ⬇*[b,f]L1 ≘ K1.ⓤ{I} → + ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⬇*[b,f]L2 ≘ K2.ⓤ{I}. +#h #b #G #L1 #L2 #H elim H -L1 -L2 +[ #f #_ #J #Y1 #H + lapply (drops_inv_atom1 … H) -H * #H #_ destruct +| #I #K1 #K2 #HK12 #IH #f #Hf #J #Y1 #H +| #I #K1 #K2 #V #HK12 #HV #IH #f #Hf #J #Y1 #H +] +elim (drops_inv_bind1_isuni … H) -H [3,6: // |*: * -Hf ] +[1,3: #Hf #H destruct -IH /3 width=3 by drops_refl, ex2_intro/ +|2,4: + #g #Hg #HK1 #H destruct + elim (IH … Hg … HK1) -K1 -Hg #Y2 #HY12 #HKY2 + /3 width=3 by drops_drop, ex2_intro/ +] +qed-. + +lemma jsx_fwd_drops_pair_sn (h) (b) (G): + ∀L1,L2. G ⊢ L1 ⊒[h] L2 → + ∀f. 𝐔⦃f⦄ → ∀I,K1,V. ⬇*[b,f]L1 ≘ K1.ⓑ{I}V → + ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⬇*[b,f]L2 ≘ K2.ⓑ{I}V + | ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⬇*[b,f]L2 ≘ K2.ⓧ & G ⊢ ⬈*[h,V] 𝐒⦃K2⦄. +#h #b #G #L1 #L2 #H elim H -L1 -L2 +[ #f #_ #J #Y1 #X1 #H + lapply (drops_inv_atom1 … H) -H * #H #_ destruct +| #I #K1 #K2 #HK12 #IH #f #Hf #J #Y1 #X1 #H +| #I #K1 #K2 #V #HK12 #HV #IH #f #Hf #J #Y1 #X1 #H +] +elim (drops_inv_bind1_isuni … H) -H [3,6: // |*: * -Hf ] +[1,3: + #Hf #H destruct -IH + /4 width=4 by drops_refl, ex3_intro, ex2_intro, or_introl, or_intror/ +|2,4: + #g #Hg #HK1 #H destruct + elim (IH … Hg … HK1) -K1 -Hg * #Y2 #HY12 #HKY2 [2,4: #HX1 ] + /4 width=4 by drops_drop, ex3_intro, ex2_intro, or_introl, or_intror/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_jsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_jsx.ma index 7431ea44d..b53d0d6f7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_jsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_jsx.ma @@ -12,27 +12,23 @@ (* *) (**************************************************************************) -include "basic_2/rt_computation/jsx.ma". +include "basic_2/rt_computation/jsx_csx.ma". (* COMPATIBILITY OF STRONG NORMALIZATION FOR UNBOUND RT-TRANSITION **********) (* Main properties **********************************************************) -theorem jsx_fix (h) (G): - ∀f,L1,L. G ⊢ L1 ⊒[h,f] L → ∀L2. G ⊢ L ⊒[h,f] L2 → L = L2. -#h #G #f #L1 #L #H elim H -f -L1 -L -[ #f #L2 #H +theorem jsx_trans (h) (G): Transitive … (jsx h G). +#h #G #L1 #L #H elim H -L1 -L +[ #L2 #H >(jsx_inv_atom_sn … H) -L2 // -| #f #I #K1 #K2 #_ #IH #L2 #H - elim (jsx_inv_push_sn … H) -H /3 width=1 by eq_f2/ -| #f #I #K1 #K2 #_ #IH #L2 #H - elim (jsx_inv_unit_sn … H) -H /3 width=1 by eq_f2/ -| #f #I #K1 #K2 #V #_ #_ #IH #L2 #H - elim (jsx_inv_unit_sn … H) -H /3 width=1 by eq_f2/ +| #I #K1 #K #_ #IH #L2 #H + elim (jsx_inv_bind_sn … H) -H * + [ #K2 #HK2 #H destruct /3 width=1 by jsx_bind/ + | #J #K2 #V #HK2 #HV #H1 #H2 destruct /3 width=1 by jsx_pair/ + ] +| #I #K1 #K #V #_ #HV #IH #L2 #H + elim (jsx_inv_void_sn … H) -H #K2 #HK2 #H destruct + /3 width=3 by rsx_jsx_trans, jsx_pair/ ] qed-. - -theorem jsx_trans (h) (G): ∀f. Transitive … (jsx h G f). -#h #G #f #L1 #L #H1 #L2 #H2 -<(jsx_fix … H1 … H2) -L2 // -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_lsubr.ma new file mode 100644 index 000000000..6fc723294 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_lsubr.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 "static_2/static/lsubr.ma". +include "basic_2/rt_computation/jsx.ma". + +(* COMPATIBILITY OF STRONG NORMALIZATION FOR UNBOUND RT-TRANSITION **********) + +(* Forward lemmas with restricted refinement for local environments *********) + +lemma jsx_fwd_lsubr (h) (G): ∀L1,L2. G ⊢ L1 ⊒[h] L2 → L1 ⫃ L2. +#h #G #L1 #L2 #H elim H -L1 -L2 +/2 width=1 by lsubr_bind, lsubr_unit/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_rsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_rsx.ma index e5e662dc6..4d294b2e2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_rsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_rsx.ma @@ -23,38 +23,37 @@ include "basic_2/rt_computation/jsx.ma". (* Basic_2A1: uses: lsx_cpx_trans_lcosx *) lemma rsx_cpx_trans_jsx (h) (G): ∀L0,T1,T2. ⦃G,L0⦄ ⊢ T1 ⬈[h] T2 → - ∀f,L. G ⊢ L0 ⊒[h,f] L → - G ⊢ ⬈*[h,T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h,T2] 𝐒⦃L⦄. + ∀L. G ⊢ L0 ⊒[h] L → G ⊢ ⬈*[h,T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h,T2] 𝐒⦃L⦄. #h #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 (jsx_inv_pair_sn_gen … HK0) -HK0 * - [ #f #K #HK0 #H1 #H2 destruct +| #I0 #G #K0 #V1 #V2 #W2 #_ #IH #HVW2 #L #HK0 #HL + elim (jsx_inv_pair_sn … HK0) -HK0 * + [ #K #HK0 #H destruct /4 width=8 by rsx_lifts, rsx_fwd_pair, drops_refl, drops_drop/ - | #f #K #HV1 #HK0 #H1 #H2 destruct + | #K #HK0 #HV1 #H destruct /4 width=8 by rsx_lifts, drops_refl, drops_drop/ ] -| #I0 #G #K0 #T #U #i #_ #IH #HTU #g #L #HK0 #HL +| #I0 #G #K0 #T #U #i #_ #IH #HTU #L #HK0 #HL elim (jsx_fwd_bind_sn … HK0) -HK0 #I #K #HK0 #H destruct /6 width=8 by rsx_inv_lifts, rsx_lifts, drops_refl, drops_drop/ -| #p #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #f #L #HL0 #HL +| #p #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #HL0 #HL elim (rsx_inv_bind_void … HL) -HL /4 width=2 by jsx_pair, rsx_bind_void/ -| #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #f #L #HL0 #HL +| #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #HL0 #HL elim (rsx_inv_flat … HL) -HL /3 width=2 by rsx_flat/ -| #G #L0 #V #U1 #T1 #T2 #HTU1 #_ #IHT12 #f #L #HL0 #HL +| #G #L0 #V #U1 #T1 #T2 #HTU1 #_ #IHT12 #L #HL0 #HL elim (rsx_inv_bind_void … HL) -HL #HV #HU1 /5 width=8 by rsx_inv_lifts, drops_refl, drops_drop/ -| #G #L0 #V #T1 #T2 #_ #IHT12 #f #L #HL0 #HL +| #G #L0 #V #T1 #T2 #_ #IHT12 #L #HL0 #HL elim (rsx_inv_flat … HL) -HL /2 width=2 by/ -| #G #L0 #V1 #V2 #T #_ #IHV12 #f #L #HL0 #HL +| #G #L0 #V1 #V2 #T #_ #IHV12 #L #HL0 #HL elim (rsx_inv_flat … HL) -HL /2 width=2 by/ -| #p #G #L0 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #f #L #HL0 #HL +| #p #G #L0 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #HL0 #HL elim (rsx_inv_flat … HL) -HL #HV1 #HL elim (rsx_inv_bind_void … HL) -HL #HW1 #HT1 /4 width=2 by jsx_pair, rsx_bind_void, rsx_flat/ -| #p #G #L0 #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #HVU2 #f #L #HL0 #HL +| #p #G #L0 #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #HVU2 #L #HL0 #HL elim (rsx_inv_flat … HL) -HL #HV1 #HL elim (rsx_inv_bind_void … HL) -HL #HW1 #HT1 /6 width=8 by jsx_pair, rsx_lifts, rsx_bind_void, rsx_flat, drops_refl, drops_drop/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma index 64eeba55e..2e129485d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma @@ -18,11 +18,65 @@ include "basic_2/rt_computation/jsx_rsx.ma". (* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******) -(* Advanced properties ******************************************************) +(* Forward lemmas with strongly rt-normalizing terms ************************) + +fact rsx_fwd_lref_pair_csx_aux (h) (G): + ∀L. G ⊢ ⬈*[h,#0] 𝐒⦃L⦄ → + ∀I,K,V. L = K.ⓑ{I}V → ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄. +#h #G #L #H +@(rsx_ind … H) -L #L #_ #IH #I #K #V1 #H destruct +@csx_intro #V2 #HV12 #HnV12 +@(IH … I) -IH [1,4: // | -HnV12 | -G #H ] +[ /2 width=1 by lpx_pair/ +| elim (rdeq_inv_zero_pair_sn … H) -H #Y #X #_ #H1 #H2 destruct -I + /2 width=1 by/ +] +qed-. + +lemma rsx_fwd_lref_pair_csx (h) (G): + ∀I,K,V. G ⊢ ⬈*[h,#0] 𝐒⦃K.ⓑ{I}V⦄ → ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄. +/2 width=4 by rsx_fwd_lref_pair_csx_aux/ qed-. + +lemma rsx_fwd_lref_pair_csx_drops (h) (G): + ∀I,K,V,i,L. ⬇*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ → ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄. +#h #G #I #K #V #i elim i -i +[ #L #H >(drops_fwd_isid … H) -H + /2 width=2 by rsx_fwd_lref_pair_csx/ +| #i #IH #L #H1 #H2 + elim (drops_inv_bind2_isuni_next … H1) -H1 // #J #Y #HY #H destruct + lapply (rsx_inv_lifts … H2 … (𝐔❴1❵) ?????) -H2 + /3 width=6 by drops_refl, drops_drop/ +] +qed-. + +(* Inversion lemmas with strongly rt-normalizing terms **********************) + +lemma rsx_inv_lref_pair (h) (G): + ∀I,K,V. G ⊢ ⬈*[h,#0] 𝐒⦃K.ⓑ{I}V⦄ → + ∧∧ ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ & G ⊢ ⬈*[h,V] 𝐒⦃K⦄. +/3 width=2 by rsx_fwd_lref_pair_csx, rsx_fwd_pair, conj/ qed-. + +lemma rsx_inv_lref_pair_drops (h) (G): + ∀I,K,V,i,L. ⬇*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ → + ∧∧ ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ & G ⊢ ⬈*[h,V] 𝐒⦃K⦄. +/3 width=5 by rsx_fwd_lref_pair_csx_drops, rsx_fwd_lref_pair_drops, conj/ qed-. + +lemma rsx_inv_lref_drops (h) (G): + ∀L,i. G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ → + ∨∨ ⬇*[Ⓕ,𝐔❴i❵] L ≘ ⋆ + | ∃∃I,K. ⬇*[i] L ≘ K.ⓤ{I} + | ∃∃I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V & ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ & G ⊢ ⬈*[h,V] 𝐒⦃K⦄. +#h #G #L #i #H elim (drops_F_uni L i) +[ /2 width=1 by or3_intro0/ +| * * /4 width=10 by rsx_fwd_lref_pair_csx_drops, rsx_fwd_lref_pair_drops, ex3_3_intro, ex1_2_intro, or3_intro2, or3_intro1/ +] +qed-. + +(* Properties with strongly rt-normalizing terms ****************************) (* Note: swapping the eliminations to avoid rsx_cpx_trans: no solution found *) (* Basic_2A1: uses: lsx_lref_be_lpxs *) -lemma rsx_pair_lpxs (h) (G): +lemma rsx_lref_pair_lpxs (h) (G): ∀K1,V. ⦃G,K1⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → ∀K2. G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ → ⦃G,K1⦄ ⊢ ⬈*[h] K2 → ∀I. G ⊢ ⬈*[h,#0] 𝐒⦃K2.ⓑ{I}V⦄. @@ -41,32 +95,38 @@ elim (tdeq_dec V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 | -IHK0 -HnY ] ] qed. +lemma rsx_lref_pair (h) (G): + ∀K,V. ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → G ⊢ ⬈*[h,V] 𝐒⦃K⦄ → ∀I. G ⊢ ⬈*[h,#0] 𝐒⦃K.ⓑ{I}V⦄. +/2 width=3 by rsx_lref_pair_lpxs/ qed. + (* Basic_2A1: uses: lsx_lref_be *) lemma rsx_lref_pair_drops (h) (G): ∀K,V. ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → G ⊢ ⬈*[h,V] 𝐒⦃K⦄ → ∀I,i,L. ⬇*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄. #h #G #K #V #HV #HK #I #i elim i -i -[ #L #H >(drops_fwd_isid … H) -H /2 width=3 by rsx_pair_lpxs/ +[ #L #H >(drops_fwd_isid … H) -H /2 width=1 by rsx_lref_pair/ | #i #IH #L #H elim (drops_inv_bind2_isuni_next … H) -H // #J #Y #HY #H destruct @(rsx_lifts … (𝐔❴1❵)) /3 width=6 by drops_refl, drops_drop/ (**) (* full auto fails *) ] qed. -(* Main properties **********************************************************) +(* Main properties with strongly rt-normalizing terms ***********************) (* Basic_2A1: uses: csx_lsx *) -theorem csx_rsx (h): ∀G,L,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → G ⊢ ⬈*[h,T] 𝐒⦃L⦄. -#h #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 rsx_lref_atom/ - | /2 width=3 by rsx_lref_unit/ +theorem csx_rsx (h) (G): ∀L,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → G ⊢ ⬈*[h,T] 𝐒⦃L⦄. +#h #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_drops … H) -H [ |*: * ] + [ /2 width=1 by rsx_lref_atom_drops/ + | /2 width=3 by rsx_lref_unit_drops/ | /4 width=6 by rsx_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 rsx_bind_void/ + elim (csx_fwd_bind … H) -H /3 width=1 by rsx_bind/ | #I #V #T #HG #HL #HT #H destruct elim (csx_fwd_flat … H) -H /3 width=1 by rsx_flat/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma index 80cc2f1f7..64ebcd666 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma @@ -43,13 +43,13 @@ qed-. (* Advanced properties ******************************************************) (* Basic_2A1: uses: lsx_lref_free *) -lemma rsx_lref_atom (h) (G): ∀L,i. ⬇*[Ⓕ,𝐔❴i❵] L ≘ ⋆ → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄. +lemma rsx_lref_atom_drops (h) (G): ∀L,i. ⬇*[Ⓕ,𝐔❴i❵] L ≘ ⋆ → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄. #h #G #L1 #i #HL1 @(rsx_lifts … (#0) … HL1) -HL1 // qed. (* Basic_2A1: uses: lsx_lref_skip *) -lemma rsx_lref_unit (h) (G): ∀I,L,K,i. ⬇*[i] L ≘ K.ⓤ{I} → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄. +lemma rsx_lref_unit_drops (h) (G): ∀I,L,K,i. ⬇*[i] L ≘ K.ⓤ{I} → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄. #h #G #I #L1 #K1 #i #HL1 @(rsx_lifts … (#0) … HL1) -HL1 // qed. @@ -57,7 +57,7 @@ qed. (* Advanced forward lemmas **************************************************) (* Basic_2A1: uses: lsx_fwd_lref_be *) -lemma rsx_fwd_lref_pair (h) (G): +lemma rsx_fwd_lref_pair_drops (h) (G): ∀L,i. G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ → ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h,V] 𝐒⦃K⦄. #h #G #L #i #HL #I #K #V #HLK 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 39cf1ed8b..48785b62b 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 @@ -81,7 +81,7 @@ table { } ] [ { "unbound context-sensitive parallel rt-computation" * } { - [ [ "compatibility for lenvs on selected entries" ] "jsx" + "( ? ⊢ ? ⊒[?,?] ? )" "jsx_rsx" + "jsx_jsx" * ] + [ [ "compatibility for lenvs" ] "jsx" + "( ? ⊢ ? ⊒[?] ? )" "jsx_drops" + "jsx_lsubr" + "jsx_csx" + "jsx_rsx" + "jsx_jsx" * ] [ [ "strongly normalizing for lenvs on referred entries" ] "rsx" + "( ? ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "rsx_length" + "rsx_drops" + "rsx_fqup" + "rsx_cpxs" + "rsx_csx" + "rsx_rsx" * ] [ [ "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_rdeq" + "csx_fdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lpxs" + "csx_csx" * ] diff --git a/matita/matita/contribs/lambdadelta/static_2/static/lsubr.ma b/matita/matita/contribs/lambdadelta/static_2/static/lsubr.ma index 5ec8a33f1..5ff763dcb 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/lsubr.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/lsubr.ma @@ -49,12 +49,11 @@ qed-. lemma lsubr_inv_atom1: ∀L2. ⋆ ⫃ L2 → L2 = ⋆. /2 width=3 by lsubr_inv_atom1_aux/ qed-. -fact lsubr_inv_bind1_aux: ∀L1,L2. L1 ⫃ L2 → ∀I,K1. L1 = K1.ⓘ{I} → - ∨∨ ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓘ{I} - | ∃∃K2,V,W. K1 ⫃ K2 & L2 = K2.ⓛW & - I = BPair Abbr (ⓝW.V) - | ∃∃J1,J2,K2,V. K1 ⫃ K2 & L2 = K2.ⓤ{J2} & - I = BPair J1 V. +fact lsubr_inv_bind1_aux: + ∀L1,L2. L1 ⫃ L2 → ∀I,K1. L1 = K1.ⓘ{I} → + ∨∨ ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓘ{I} + | ∃∃K2,V,W. K1 ⫃ K2 & L2 = K2.ⓛW & I = BPair Abbr (ⓝW.V) + | ∃∃J1,J2,K2,V. K1 ⫃ K2 & L2 = K2.ⓤ{J2} & I = BPair J1 V. #L1 #L2 * -L1 -L2 [ #J #K1 #H destruct | #I #L1 #L2 #HL12 #J #K1 #H destruct /3 width=3 by or3_intro0, ex2_intro/ @@ -64,12 +63,11 @@ fact lsubr_inv_bind1_aux: ∀L1,L2. L1 ⫃ L2 → ∀I,K1. L1 = K1.ⓘ{I} → qed-. (* Basic_2A1: uses: lsubr_inv_pair1 *) -lemma lsubr_inv_bind1: ∀I,K1,L2. K1.ⓘ{I} ⫃ L2 → - ∨∨ ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓘ{I} - | ∃∃K2,V,W. K1 ⫃ K2 & L2 = K2.ⓛW & - I = BPair Abbr (ⓝW.V) - | ∃∃J1,J2,K2,V. K1 ⫃ K2 & L2 = K2.ⓤ{J2} & - I = BPair J1 V. +lemma lsubr_inv_bind1: + ∀I,K1,L2. K1.ⓘ{I} ⫃ L2 → + ∨∨ ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓘ{I} + | ∃∃K2,V,W. K1 ⫃ K2 & L2 = K2.ⓛW & I = BPair Abbr (ⓝW.V) + | ∃∃J1,J2,K2,V. K1 ⫃ K2 & L2 = K2.ⓤ{J2} & I = BPair J1 V. /2 width=3 by lsubr_inv_bind1_aux/ qed-. fact lsubr_inv_atom2_aux: ∀L1,L2. L1 ⫃ L2 → L2 = ⋆ → L1 = ⋆. @@ -83,10 +81,11 @@ qed-. lemma lsubr_inv_atom2: ∀L1. L1 ⫃ ⋆ → L1 = ⋆. /2 width=3 by lsubr_inv_atom2_aux/ qed-. -fact lsubr_inv_bind2_aux: ∀L1,L2. L1 ⫃ L2 → ∀I,K2. L2 = K2.ⓘ{I} → - ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓘ{I} - | ∃∃K1,W,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V & I = BPair Abst W - | ∃∃J1,J2,K1,V. K1 ⫃ K2 & L1 = K1.ⓑ{J1}V & I = BUnit J2. +fact lsubr_inv_bind2_aux: + ∀L1,L2. L1 ⫃ L2 → ∀I,K2. L2 = K2.ⓘ{I} → + ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓘ{I} + | ∃∃K1,W,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V & I = BPair Abst W + | ∃∃J1,J2,K1,V. K1 ⫃ K2 & L1 = K1.ⓑ{J1}V & I = BUnit J2. #L1 #L2 * -L1 -L2 [ #J #K2 #H destruct | #I #L1 #L2 #HL12 #J #K2 #H destruct /3 width=3 by ex2_intro, or3_intro0/ @@ -95,82 +94,91 @@ fact lsubr_inv_bind2_aux: ∀L1,L2. L1 ⫃ L2 → ∀I,K2. L2 = K2.ⓘ{I} → ] qed-. -lemma lsubr_inv_bind2: ∀I,L1,K2. L1 ⫃ K2.ⓘ{I} → - ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓘ{I} - | ∃∃K1,W,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V & I = BPair Abst W - | ∃∃J1,J2,K1,V. K1 ⫃ K2 & L1 = K1.ⓑ{J1}V & I = BUnit J2. +lemma lsubr_inv_bind2: + ∀I,L1,K2. L1 ⫃ K2.ⓘ{I} → + ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓘ{I} + | ∃∃K1,W,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V & I = BPair Abst W + | ∃∃J1,J2,K1,V. K1 ⫃ K2 & L1 = K1.ⓑ{J1}V & I = BUnit J2. /2 width=3 by lsubr_inv_bind2_aux/ qed-. (* Advanced inversion lemmas ************************************************) -lemma lsubr_inv_abst1: ∀K1,L2,W. K1.ⓛW ⫃ L2 → - ∨∨ ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓛW - | ∃∃I2,K2. K1 ⫃ K2 & L2 = K2.ⓤ{I2}. +lemma lsubr_inv_abst1: + ∀K1,L2,W. K1.ⓛW ⫃ L2 → + ∨∨ ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓛW + | ∃∃I2,K2. K1 ⫃ K2 & L2 = K2.ⓤ{I2}. #K1 #L2 #W #H elim (lsubr_inv_bind1 … H) -H * /3 width=4 by ex2_2_intro, ex2_intro, or_introl, or_intror/ #K2 #V2 #W2 #_ #_ #H destruct qed-. -lemma lsubr_inv_unit1: ∀I,K1,L2. K1.ⓤ{I} ⫃ L2 → - ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓤ{I}. +lemma lsubr_inv_unit1: + ∀I,K1,L2. K1.ⓤ{I} ⫃ L2 → + ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓤ{I}. #I #K1 #L2 #H elim (lsubr_inv_bind1 … H) -H * [ #K2 #HK12 #H destruct /2 width=3 by ex2_intro/ | #K2 #V #W #_ #_ #H destruct -| #I1 #I2 #K2 #V #_ #_ #H destruct +| #J1 #J2 #K2 #V #_ #_ #H destruct ] qed-. -lemma lsubr_inv_pair2: ∀I,L1,K2,W. L1 ⫃ K2.ⓑ{I}W → - ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓑ{I}W - | ∃∃K1,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V & I = Abst. +lemma lsubr_inv_pair2: + ∀I,L1,K2,W. L1 ⫃ K2.ⓑ{I}W → + ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓑ{I}W + | ∃∃K1,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V & I = Abst. #I #L1 #K2 #W #H elim (lsubr_inv_bind2 … H) -H * [ /3 width=3 by ex2_intro, or_introl/ -| #K2 #X #V #HK12 #H1 #H2 destruct /3 width=4 by ex3_2_intro, or_intror/ -| #I1 #I1 #K2 #V #_ #_ #H destruct +| #K1 #X #V #HK12 #H1 #H2 destruct /3 width=4 by ex3_2_intro, or_intror/ +| #J1 #J1 #K1 #V #_ #_ #H destruct ] qed-. -lemma lsubr_inv_abbr2: ∀L1,K2,V. L1 ⫃ K2.ⓓV → - ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓓV. +lemma lsubr_inv_abbr2: + ∀L1,K2,V. L1 ⫃ K2.ⓓV → + ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓓV. #L1 #K2 #V #H elim (lsubr_inv_pair2 … H) -H * [ /2 width=3 by ex2_intro/ | #K1 #X #_ #_ #H destruct ] qed-. -lemma lsubr_inv_abst2: ∀L1,K2,W. L1 ⫃ K2.ⓛW → - ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓛW - | ∃∃K1,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V. +lemma lsubr_inv_abst2: + ∀L1,K2,W. L1 ⫃ K2.ⓛW → + ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓛW + | ∃∃K1,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V. #L1 #K2 #W #H elim (lsubr_inv_pair2 … H) -H * /3 width=4 by ex2_2_intro, ex2_intro, or_introl, or_intror/ qed-. -lemma lsubr_inv_unit2: ∀I,L1,K2. L1 ⫃ K2.ⓤ{I} → - ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓤ{I} - | ∃∃J,K1,V. K1 ⫃ K2 & L1 = K1.ⓑ{J}V. +lemma lsubr_inv_unit2: + ∀I,L1,K2. L1 ⫃ K2.ⓤ{I} → + ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓤ{I} + | ∃∃J,K1,V. K1 ⫃ K2 & L1 = K1.ⓑ{J}V. #I #L1 #K2 #H elim (lsubr_inv_bind2 … H) -H * [ /3 width=3 by ex2_intro, or_introl/ | #K1 #W #V #_ #_ #H destruct -| #I1 #I2 #K1 #V #HK12 #H1 #H2 destruct /3 width=5 by ex2_3_intro, or_intror/ +| #J1 #J2 #K1 #V #HK12 #H1 #H2 destruct /3 width=5 by ex2_3_intro, or_intror/ ] qed-. (* Basic forward lemmas *****************************************************) -lemma lsubr_fwd_bind1: ∀I1,K1,L2. K1.ⓘ{I1} ⫃ L2 → - ∃∃I2,K2. K1 ⫃ K2 & L2 = K2.ⓘ{I2}. +lemma lsubr_fwd_bind1: + ∀I1,K1,L2. K1.ⓘ{I1} ⫃ L2 → + ∃∃I2,K2. K1 ⫃ K2 & L2 = K2.ⓘ{I2}. #I1 #K1 #L2 #H elim (lsubr_inv_bind1 … H) -H * [ #K2 #HK12 #H destruct /3 width=4 by ex2_2_intro/ | #K2 #W1 #V1 #HK12 #H1 #H2 destruct /3 width=4 by ex2_2_intro/ -| #I1 #I2 #K2 #V1 #HK12 #H1 #H2 destruct /3 width=4 by ex2_2_intro/ +| #J1 #J2 #K2 #V1 #HK12 #H1 #H2 destruct /3 width=4 by ex2_2_intro/ ] qed-. -lemma lsubr_fwd_bind2: ∀I2,L1,K2. L1 ⫃ K2.ⓘ{I2} → - ∃∃I1,K1. K1 ⫃ K2 & L1 = K1.ⓘ{I1}. +lemma lsubr_fwd_bind2: + ∀I2,L1,K2. L1 ⫃ K2.ⓘ{I2} → + ∃∃I1,K1. K1 ⫃ K2 & L1 = K1.ⓘ{I1}. #I2 #L1 #K2 #H elim (lsubr_inv_bind2 … H) -H * [ #K1 #HK12 #H destruct /3 width=4 by ex2_2_intro/ | #K1 #W1 #V1 #HK12 #H1 #H2 destruct /3 width=4 by ex2_2_intro/ -| #I1 #I2 #K1 #V1 #HK12 #H1 #H2 destruct /3 width=4 by ex2_2_intro/ +| #J1 #J2 #K1 #V1 #HK12 #H1 #H2 destruct /3 width=4 by ex2_2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/lsubr_drops.ma b/matita/matita/contribs/lambdadelta/static_2/static/lsubr_drops.ma index 4009cdd29..ac9e9e41f 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/lsubr_drops.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/lsubr_drops.ma @@ -20,11 +20,12 @@ include "static_2/static/lsubr.ma". (* Forward lemmas with generic slicing for local environments ***************) (* Basic_2A1: includes: lsubr_fwd_drop2_pair *) -lemma lsubr_fwd_drops2_bind: ∀L1,L2. L1 ⫃ L2 → - ∀b,f,I,K2. 𝐔⦃f⦄ → ⬇*[b,f] L2 ≘ K2.ⓘ{I} → - ∨∨ ∃∃K1. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓘ{I} - | ∃∃K1,W,V. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓓⓝW.V & I = BPair Abst W - | ∃∃J1,J2,K1,V. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓑ{J1}V & I = BUnit J2. +lemma lsubr_fwd_drops2_bind: + ∀L1,L2. L1 ⫃ L2 → + ∀b,f,I,K2. 𝐔⦃f⦄ → ⬇*[b,f] L2 ≘ K2.ⓘ{I} → + ∨∨ ∃∃K1. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓘ{I} + | ∃∃K1,W,V. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓓⓝW.V & I = BPair Abst W + | ∃∃J1,J2,K1,V. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓑ{J1}V & I = BUnit J2. #L1 #L2 #H elim H -L1 -L2 [ #b #f #I #K2 #_ #H elim (drops_inv_atom1 … H) -H #H destruct @@ -41,9 +42,10 @@ elim (drops_inv_bind1_isuni … Hf H) -Hf -H * qed-. (* Basic_2A1: includes: lsubr_fwd_drop2_abbr *) -lemma lsubr_fwd_drops2_abbr: ∀L1,L2. L1 ⫃ L2 → - ∀b,f,K2,V. 𝐔⦃f⦄ → ⬇*[b,f] L2 ≘ K2.ⓓV → - ∃∃K1. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓓV. +lemma lsubr_fwd_drops2_abbr: + ∀L1,L2. L1 ⫃ L2 → + ∀b,f,K2,V. 𝐔⦃f⦄ → ⬇*[b,f] L2 ≘ K2.ⓓV → + ∃∃K1. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓓV. #L1 #L2 #HL12 #b #f #K2 #V #Hf #HLK2 elim (lsubr_fwd_drops2_bind … HL12 … Hf HLK2) -L2 -Hf // * [ #K1 #W #V #_ #_ #H destruct diff --git a/matita/matita/contribs/lambdadelta/static_2/static/lsubr_lsubr.ma b/matita/matita/contribs/lambdadelta/static_2/static/lsubr_lsubr.ma index 3bf83b81e..2aba1cf65 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/lsubr_lsubr.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/lsubr_lsubr.ma @@ -21,12 +21,12 @@ include "static_2/static/lsubr.ma". theorem lsubr_trans: Transitive … lsubr. #L1 #L #H elim H -L1 -L // [ #I #L1 #L #_ #IH #X #H elim (lsubr_inv_bind1 … H) -H * - [ #L2 #HL2 #H | #L2 #V #W #HL2 #H1 #H2 | #I1 #I2 #L2 #V #Hl2 #H1 #H2 ] + [ #L2 #HL2 #H | #L2 #V #W #HL2 #H1 #H2 | #I1 #I2 #L2 #V #HL2 #H1 #H2 ] destruct /3 width=1 by lsubr_bind, lsubr_beta, lsubr_unit/ | #L1 #L #V #W #_ #IH #X #H elim (lsubr_inv_abst1 … H) -H * [ #L2 #HL2 #H | #I #L2 #HL2 #H ] destruct /3 width=1 by lsubr_beta, lsubr_unit/ | #I1 #I2 #L1 #L #V #_ #IH #X #H elim (lsubr_inv_unit1 … H) -H - /4 width=1 by lsubr_unit/ + #L2 #HL2 #H destruct /4 width=1 by lsubr_unit/ ] qed-.