From: Ferruccio Guidi Date: Wed, 8 Mar 2017 21:17:06 +0000 (+0000) Subject: cpxs_lfpx completed X-Git-Tag: make_still_working~489 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cbc645186c8836c88c559c787a4deea63b7a12b0;p=helm.git cpxs_lfpx completed --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss.ma deleted file mode 100644 index 757d3e684..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss.ma +++ /dev/null @@ -1,234 +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/notation/relations/relationstarstar_4.ma". -include "basic_2/static/lfxs.ma". - -(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) - -definition lfxss (R) (T): relation lenv ≝ TC … (lfxs R T). - -interpretation "tc of generic extension on referred entries (local environment)" - 'RelationStarStar R T L1 L2 = (lfxss R T L1 L2). - -(* Basic properties ***********************************************************) - -lemma lfxss_atom: ∀R,I. ⋆ ⦻**[R, ⓪{I}] ⋆. -/2 width=1 by inj/ qed. - -lemma lfxss_sort: ∀R,I,L1,L2,V1,V2,s. - L1 ⦻**[R, ⋆s] L2 → L1.ⓑ{I}V1 ⦻**[R, ⋆s] L2.ⓑ{I}V2. -#R #I #L1 #L2 #V1 #V2 #s #H elim H -L2 -/3 width=4 by lfxs_sort, step, inj/ -qed. - -lemma lfxss_lref: ∀R,I,L1,L2,V1,V2,i. - L1 ⦻**[R, #i] L2 → L1.ⓑ{I}V1 ⦻**[R, #⫯i] L2.ⓑ{I}V2. -#R #I #L1 #L2 #V1 #V2 #i #H elim H -L2 -/3 width=4 by lfxs_lref, step, inj/ -qed. - -lemma lfxss_gref: ∀R,I,L1,L2,V1,V2,l. - L1 ⦻**[R, §l] L2 → L1.ⓑ{I}V1 ⦻**[R, §l] L2.ⓑ{I}V2. -#R #I #L1 #L2 #V1 #V2 #l #H elim H -L2 -/3 width=4 by lfxs_gref, step, inj/ -qed. - -lemma lfxss_sym: ∀R. lexs_frees_confluent R cfull → - (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → - ∀T. symmetric … (lfxss R T). -#R #H1R #H2R #T #L1 #L2 #H elim H -L2 -/4 width=3 by lfxs_sym, TC_strap, inj/ -qed-. - -lemma lfxss_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 #H elim H -L2 -/4 width=5 by lfxs_co, step, inj/ -qed-. -(* -(* Basic inversion lemmas ***************************************************) - -lemma lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻*[R, ⓪{I}] Y2 → Y2 = ⋆. -#R #I #Y2 * /2 width=4 by lexs_inv_atom1/ -qed-. - -lemma lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻*[R, ⓪{I}] ⋆ → 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 = ⋆) ∨ - ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, ⋆s] L2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. -#R * [ | #Y1 #I #V1 ] #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 - elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct - elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct - /5 width=8 by frees_sort_gen, ex3_5_intro, ex2_intro, or_intror/ -] -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. -#R #Y1 #Y2 * #f #H1 #H2 elim (frees_inv_zero … H1) -H1 * -[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/ -| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_next1_aux … H2 … HY1 Hg) -H2 -Hg - /4 width=9 by ex4_5_intro, ex2_intro, or_intror/ -] -qed-. - -lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⦻*[R, #⫯i] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, #i] L2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. -#R #Y1 #Y2 #i * #f #H1 #H2 elim (frees_inv_lref … H1) -H1 * -[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/ -| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_push1_aux … H2 … HY1 Hg) -H2 -Hg - /4 width=8 by ex3_5_intro, ex2_intro, or_intror/ -] -qed-. - -lemma lfxs_inv_gref: ∀R,Y1,Y2,l. Y1 ⦻*[R, §l] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, §l] L2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. -#R * [ | #Y1 #I #V1 ] #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 - elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct - elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct - /5 width=8 by frees_gref_gen, ex3_5_intro, ex2_intro, or_intror/ -] -qed-. - -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, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ -qed-. - -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_pair_sn: ∀R,I,Y2,L1,V1,s. L1.ⓑ{I}V1 ⦻*[R, ⋆s] Y2 → - ∃∃L2,V2. L1 ⦻*[R, ⋆s] L2 & Y2 = L2.ⓑ{I}V2. -#R #I #Y2 #L1 #V1 #s #H elim (lfxs_inv_sort … H) -H * -[ #H destruct -| #J #Y1 #L2 #X1 #V2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/ -] -qed-. - -lemma lfxs_inv_sort_pair_dx: ∀R,I,Y1,L2,V2,s. Y1 ⦻*[R, ⋆s] L2.ⓑ{I}V2 → - ∃∃L1,V1. L1 ⦻*[R, ⋆s] L2 & Y1 = L1.ⓑ{I}V1. -#R #I #Y1 #L2 #V2 #s #H elim (lfxs_inv_sort … H) -H * -[ #_ #H destruct -| #J #L1 #Y2 #V1 #X2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/ -] -qed-. - -lemma lfxs_inv_zero_pair_sn: ∀R,I,Y2,L1,V1. L1.ⓑ{I}V1 ⦻*[R, #0] Y2 → - ∃∃L2,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & - Y2 = L2.ⓑ{I}V2. -#R #I #Y2 #L1 #V1 #H elim (lfxs_inv_zero … H) -H * -[ #H destruct -| #J #Y1 #L2 #X1 #V2 #HV1 #HV12 #H1 #H2 destruct - /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma lfxs_inv_zero_pair_dx: ∀R,I,Y1,L2,V2. Y1 ⦻*[R, #0] L2.ⓑ{I}V2 → - ∃∃L1,V1. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & - Y1 = L1.ⓑ{I}V1. -#R #I #Y1 #L2 #V2 #H elim (lfxs_inv_zero … H) -H * -[ #_ #H destruct -| #J #L1 #Y2 #V1 #X2 #HV1 #HV12 #H1 #H2 destruct - /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma lfxs_inv_lref_pair_sn: ∀R,I,Y2,L1,V1,i. L1.ⓑ{I}V1 ⦻*[R, #⫯i] Y2 → - ∃∃L2,V2. L1 ⦻*[R, #i] L2 & Y2 = L2.ⓑ{I}V2. -#R #I #Y2 #L1 #V1 #i #H elim (lfxs_inv_lref … H) -H * -[ #H destruct -| #J #Y1 #L2 #X1 #V2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ -] -qed-. - -lemma lfxs_inv_lref_pair_dx: ∀R,I,Y1,L2,V2,i. Y1 ⦻*[R, #⫯i] L2.ⓑ{I}V2 → - ∃∃L1,V1. L1 ⦻*[R, #i] L2 & Y1 = L1.ⓑ{I}V1. -#R #I #Y1 #L2 #V2 #i #H elim (lfxs_inv_lref … H) -H * -[ #_ #H destruct -| #J #L1 #Y2 #V1 #X2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ -] -qed-. - -lemma lfxs_inv_gref_pair_sn: ∀R,I,Y2,L1,V1,l. L1.ⓑ{I}V1 ⦻*[R, §l] Y2 → - ∃∃L2,V2. L1 ⦻*[R, §l] L2 & Y2 = L2.ⓑ{I}V2. -#R #I #Y2 #L1 #V1 #l #H elim (lfxs_inv_gref … H) -H * -[ #H destruct -| #J #Y1 #L2 #X1 #V2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/ -] -qed-. - -lemma lfxs_inv_gref_pair_dx: ∀R,I,Y1,L2,V2,l. Y1 ⦻*[R, §l] L2.ⓑ{I}V2 → - ∃∃L1,V1. L1 ⦻*[R, §l] L2 & Y1 = L1.ⓑ{I}V1. -#R #I #Y1 #L2 #V2 #l #H elim (lfxs_inv_gref … H) -H * -[ #_ #H destruct -| #J #L1 #Y2 #V1 #X2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/ -] -qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lfxs_fwd_bind_sn: ∀R,p,I,L1,L2,V,T. L1 ⦻*[R, ⓑ{p,I}V.T] L2 → L1 ⦻*[R, V] L2. -#R #p #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_bind … Hf) -Hf -/4 width=6 by sle_lexs_trans, sor_inv_sle_sn, ex2_intro/ -qed-. - -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-. - -lemma lfxs_fwd_flat_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, V] L2. -#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H // -qed-. - -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_pair_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ②{I}V.T] L2 → L1 ⦻*[R, V] L2. -#R * /2 width=4 by lfxs_fwd_flat_sn, lfxs_fwd_bind_sn/ -qed-. - -(* Basic_2A1: removed theorems 24: - llpx_sn_sort llpx_sn_skip llpx_sn_lref llpx_sn_free llpx_sn_gref - llpx_sn_bind llpx_sn_flat - llpx_sn_inv_bind llpx_sn_inv_flat - llpx_sn_fwd_lref llpx_sn_fwd_pair_sn llpx_sn_fwd_length - llpx_sn_fwd_bind_sn llpx_sn_fwd_bind_dx llpx_sn_fwd_flat_sn llpx_sn_fwd_flat_dx - llpx_sn_refl llpx_sn_Y llpx_sn_bind_O llpx_sn_ge_up llpx_sn_ge llpx_sn_co - llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx -*) -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma new file mode 100644 index 000000000..4c30dc0a9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma @@ -0,0 +1,260 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relationstarstar_4.ma". +include "basic_2/static/lfxs.ma". + +(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***) + +definition tc_lfxs (R) (T): relation lenv ≝ TC … (lfxs R T). + +interpretation "iterated extension on referred entries (local environment)" + 'RelationStarStar R T L1 L2 = (tc_lfxs R T L1 L2). + +(* Basic properties *********************************************************) + +lemma tc_lfxs_atom: ∀R,I. ⋆ ⦻**[R, ⓪{I}] ⋆. +/2 width=1 by inj/ qed. + +lemma tc_lfxs_sort: ∀R,I,L1,L2,V1,V2,s. + L1 ⦻**[R, ⋆s] L2 → L1.ⓑ{I}V1 ⦻**[R, ⋆s] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 #s #H elim H -L2 +/3 width=4 by lfxs_sort, step, inj/ +qed. + +lemma tc_lfxs_lref: ∀R,I,L1,L2,V1,V2,i. + L1 ⦻**[R, #i] L2 → L1.ⓑ{I}V1 ⦻**[R, #⫯i] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 #i #H elim H -L2 +/3 width=4 by lfxs_lref, step, inj/ +qed. + +lemma tc_lfxs_gref: ∀R,I,L1,L2,V1,V2,l. + L1 ⦻**[R, §l] L2 → L1.ⓑ{I}V1 ⦻**[R, §l] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 #l #H elim H -L2 +/3 width=4 by lfxs_gref, step, inj/ +qed. + +lemma tc_lfxs_sym: ∀R. lexs_frees_confluent R cfull → + (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → + ∀T. symmetric … (tc_lfxs R T). +#R #H1R #H2R #T #L1 #L2 #H elim H -L2 +/4 width=3 by lfxs_sym, TC_strap, inj/ +qed-. + +lemma tc_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 #H elim H -L2 +/4 width=5 by lfxs_co, step, inj/ +qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma tc_lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻**[R, ⓪{I}] Y2 → Y2 = ⋆. +#R #I #Y2 #H elim H -Y2 /3 width=3 by inj, lfxs_inv_atom_sn/ +qed-. + +lemma tc_lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻**[R, ⓪{I}] ⋆ → Y1 = ⋆. +#R #I #Y1 #H @(TC_ind_dx ??????? H) -Y1 +/3 width=3 by inj, lfxs_inv_atom_dx/ +qed-. + +lemma tc_lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⦻**[R, ⋆s] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻**[R, ⋆s] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R #Y1 #Y2 #s #H elim H -Y2 +[ #Y2 #H elim (lfxs_inv_sort … H) -H * + /4 width=8 by ex3_5_intro, inj, or_introl, or_intror, conj/ +| #Y #Y2 #_ #H elim (lfxs_inv_sort … H) -H * + [ #H #H2 * * /3 width=8 by ex3_5_intro, or_introl, or_intror, conj/ + | #I #L #L2 #V #V2 #HL2 #H #H2 * * + [ #H1 #H0 destruct + | #I0 #L1 #L0 #V1 #V0 #HL10 #H1 #H0 destruct + /4 width=8 by ex3_5_intro, step, or_intror/ + ] + ] +] +qed-. +(* +lemma tc_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. +#R #Y1 #Y2 #H elim H -Y2 +[ #Y2 #H elim (lfxs_inv_zero … H) -H * + /4 width=9 by ex4_5_intro, inj, or_introl, or_intror, conj/ +| #Y #Y2 #_ #H elim (lfxs_inv_zero … H) -H * + [ #H #H2 * * /3 width=9 by ex4_5_intro, or_introl, or_intror, conj/ + | #I #L #L2 #V #V2 #HL2 #HV2 #H #H2 * * + [ #H1 #H0 destruct + | #I0 #L1 #L0 #V1 #V0 #HL10 #HV10 #H1 #H0 destruct + @or_intror @ex4_5_intro [6,7: |*: /width=7/ ] + + /4 width=8 by ex3_5_intro, step, or_intror/ + ] + ] +] +qed-. + + + + + +#R #Y1 #Y2 * #f #H1 #H2 elim (frees_inv_zero … H1) -H1 * +[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/ +| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_next1_aux … H2 … HY1 Hg) -H2 -Hg + /4 width=9 by ex4_5_intro, ex2_intro, or_intror/ +] +qed-. + +lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⦻*[R, #⫯i] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, #i] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R #Y1 #Y2 #i * #f #H1 #H2 elim (frees_inv_lref … H1) -H1 * +[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/ +| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_push1_aux … H2 … HY1 Hg) -H2 -Hg + /4 width=8 by ex3_5_intro, ex2_intro, or_intror/ +] +qed-. + +lemma lfxs_inv_gref: ∀R,Y1,Y2,l. Y1 ⦻*[R, §l] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, §l] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R * [ | #Y1 #I #V1 ] #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 + elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct + elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct + /5 width=8 by frees_gref_gen, ex3_5_intro, ex2_intro, or_intror/ +] +qed-. + +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, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ +qed-. + +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_pair_sn: ∀R,I,Y2,L1,V1,s. L1.ⓑ{I}V1 ⦻*[R, ⋆s] Y2 → + ∃∃L2,V2. L1 ⦻*[R, ⋆s] L2 & Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #s #H elim (lfxs_inv_sort … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_sort_pair_dx: ∀R,I,Y1,L2,V2,s. Y1 ⦻*[R, ⋆s] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻*[R, ⋆s] L2 & Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #s #H elim (lfxs_inv_sort … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_zero_pair_sn: ∀R,I,Y2,L1,V1. L1.ⓑ{I}V1 ⦻*[R, #0] Y2 → + ∃∃L2,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & + Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #H elim (lfxs_inv_zero … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #HV1 #HV12 #H1 #H2 destruct + /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lfxs_inv_zero_pair_dx: ∀R,I,Y1,L2,V2. Y1 ⦻*[R, #0] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & + Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #H elim (lfxs_inv_zero … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #HV1 #HV12 #H1 #H2 destruct + /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lfxs_inv_lref_pair_sn: ∀R,I,Y2,L1,V1,i. L1.ⓑ{I}V1 ⦻*[R, #⫯i] Y2 → + ∃∃L2,V2. L1 ⦻*[R, #i] L2 & Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #i #H elim (lfxs_inv_lref … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_lref_pair_dx: ∀R,I,Y1,L2,V2,i. Y1 ⦻*[R, #⫯i] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻*[R, #i] L2 & Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #i #H elim (lfxs_inv_lref … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_gref_pair_sn: ∀R,I,Y2,L1,V1,l. L1.ⓑ{I}V1 ⦻*[R, §l] Y2 → + ∃∃L2,V2. L1 ⦻*[R, §l] L2 & Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #l #H elim (lfxs_inv_gref … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_gref_pair_dx: ∀R,I,Y1,L2,V2,l. Y1 ⦻*[R, §l] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻*[R, §l] L2 & Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #l #H elim (lfxs_inv_gref … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lfxs_fwd_bind_sn: ∀R,p,I,L1,L2,V,T. L1 ⦻*[R, ⓑ{p,I}V.T] L2 → L1 ⦻*[R, V] L2. +#R #p #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_bind … Hf) -Hf +/4 width=6 by sle_lexs_trans, sor_inv_sle_sn, ex2_intro/ +qed-. + +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-. + +lemma lfxs_fwd_flat_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, V] L2. +#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H // +qed-. + +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_pair_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ②{I}V.T] L2 → L1 ⦻*[R, V] L2. +#R * /2 width=4 by lfxs_fwd_flat_sn, lfxs_fwd_bind_sn/ +qed-. + +(* Basic_2A1: removed theorems 24: + llpx_sn_sort llpx_sn_skip llpx_sn_lref llpx_sn_free llpx_sn_gref + llpx_sn_bind llpx_sn_flat + llpx_sn_inv_bind llpx_sn_inv_flat + llpx_sn_fwd_lref llpx_sn_fwd_pair_sn llpx_sn_fwd_length + llpx_sn_fwd_bind_sn llpx_sn_fwd_bind_dx llpx_sn_fwd_flat_sn llpx_sn_fwd_flat_dx + llpx_sn_refl llpx_sn_Y llpx_sn_bind_O llpx_sn_ge_up llpx_sn_ge llpx_sn_co + llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx +*) +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma new file mode 100644 index 000000000..26fb988b5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma @@ -0,0 +1,89 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpx_drops.ma". +include "basic_2/rt_computation/cpxs.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) + +(* Advanced properties ******************************************************) + +lemma cpxs_delta: ∀h,I,G,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 → + ∀W2. ⬆*[1] V2 ≡ W2 → ⦃G, K.ⓑ{I}V1⦄ ⊢ #0 ⬈*[h] W2. +#h #I #G #K #V1 #V2 #H @(cpxs_ind … H) -V2 +[ /3 width=3 by cpx_cpxs, cpx_delta/ +| #V #V2 #_ #HV2 #IH #W2 #HVW2 + elim (lifts_total V (𝐔❴1❵)) #W #HVW + elim (cpx_lifts … HV2 (Ⓣ) … (K.ⓑ{I}V1) … HVW) -HV2 + [ #V0 #HV20 <(lifts_mono … HVW2 … HV20) -V2 -V0 /3 width=3 by cpxs_strap1/ + | /3 width=1 by drops_refl, drops_drop/ + ] +] +qed. + +lemma cpxs_lref: ∀h,I,G,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈*[h] T → + ∀U. ⬆*[1] T ≡ U → ⦃G, K.ⓑ{I}V⦄ ⊢ #⫯i ⬈*[h] U. +#h #I #G #K #V #T #i #H @(cpxs_ind … H) -T +[ /3 width=3 by cpx_cpxs, cpx_lref/ +| #T0 #T #_ #HT2 #IH #U #HTU + elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0 + elim (cpx_lifts … HT2 (Ⓣ) … (K.ⓑ{I}V) … HTU0) -HT2 + [ #X #HTX <(lifts_mono … HTU … HTX) -T -X /3 width=3 by cpxs_strap1/ + | /3 width=1 by drops_refl, drops_drop/ + ] +] +qed. + +(* Basic_2A1: was: cpxs_delta *) +lemma cpxs_delta_drops: ∀h,I,G,L,K,V1,V2,i. + ⬇*[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 → + ∀W2. ⬆*[⫯i] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ⬈*[h] W2. +#h #I #G #L #K #V1 #V2 #i #HLK #H @(cpxs_ind … H) -V2 +[ /3 width=7 by cpx_cpxs, cpx_delta_drops/ +| #V #V2 #_ #HV2 #IH #W2 #HVW2 + elim (lifts_total V (𝐔❴⫯i❵)) #W #HVW + elim (cpx_lifts … HV2 (Ⓣ) … L … HVW) -HV2 + [ #V0 #HV20 <(lifts_mono … HVW2 … HV20) -V2 -V0 /3 width=3 by cpxs_strap1/ + | /2 width=3 by drops_isuni_fwd_drop2/ + ] +] +qed. +(* +(* Advanced inversion lemmas ************************************************) + +lemma cpxs_inv_lref1: ∀h,o,G,L,T2,i. ⦃G, L⦄ ⊢ #i ⬈*[h, o] T2 → + T2 = #i ∨ + ∃∃I,K,V1,T1. ⬇[i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ⬈*[h, o] T1 & + ⬆[0, i+1] T1 ≡ T2. +#h #o #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/ +#T #T2 #_ #HT2 * +[ #H destruct + elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/ + * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/ +| * #I #K #V1 #T1 #HLK #HVT1 #HT1 + lapply (drop_fwd_drop2 … HLK) #H0LK + elim (cpx_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T + /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/ +] +qed-. + +(* Relocation properties ****************************************************) + +lemma cpxs_lift: ∀h,o,G. d_liftable (cpxs h o G). +/3 width=10 by cpx_lift, cpxs_strap1, d_liftable_LTC/ qed. + +lemma cpxs_inv_lift1: ∀h,o,G. d_deliftable_sn (cpxs h o G). +/3 width=6 by d_deliftable_sn_LTC, cpx_inv_lift1/ +qed-. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma new file mode 100644 index 000000000..4bacb47f6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma @@ -0,0 +1,70 @@ +include "basic_2/computation/cpxs_lift.ma". +include "basic_2/multiple/fqus_fqus.ma". + +(* Advanced properties ******************************************************) + +lemma lstas_cpxs: ∀h,o,G,L,T1,T2,d2. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 → + ∀d1. ⦃G, L⦄ ⊢ T1 ▪[h, o] d1 → d2 ≤ d1 → ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2. +#h #o #G #L #T1 #T2 #d2 #H elim H -G -L -T1 -T2 -d2 // +[ /3 width=3 by cpxs_sort, da_inv_sort/ +| #G #L #K #V1 #V2 #W2 #i #d2 #HLK #_ #HVW2 #IHV12 #d1 #H #Hd21 + elim (da_inv_lref … H) -H * #K0 #V0 [| #d0 ] #HLK0 + lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct /3 width=7 by cpxs_delta/ +| #G #L #K #V1 #V2 #W2 #i #d2 #HLK #_ #HVW2 #IHV12 #d1 #H #Hd21 + elim (da_inv_lref … H) -H * #K0 #V0 [| #d0 ] #HLK0 + lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct + #HV1 #H destruct lapply (le_plus_to_le_c … Hd21) -Hd21 + /3 width=7 by cpxs_delta/ +| /4 width=3 by cpxs_bind_dx, da_inv_bind/ +| /4 width=3 by cpxs_flat_dx, da_inv_flat/ +| /4 width=3 by cpxs_eps, da_inv_flat/ +] +qed. + +(* Properties on supclosure *************************************************) + +lemma fqu_cpxs_trans: ∀h,o,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h, o] U2 → + ∀T1. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 /2 width=3 by ex2_intro/ +#T #T2 #HT2 #_ #IHTU2 #T1 #HT1 elim (fqu_cpx_trans … HT1 … HT2) -T +#T #HT1 #HT2 elim (IHTU2 … HT2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/ +qed-. + +lemma fquq_cpxs_trans: ∀h,o,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h, o] U2 → + ∀T1. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T2 #U2 #HTU2 #T1 #H elim (fquq_inv_gen … H) -H +[ #HT12 elim (fqu_cpxs_trans … HTU2 … HT12) /3 width=3 by fqu_fquq, ex2_intro/ +| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma fquq_lstas_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ∀U2,d1. ⦃G2, L2⦄ ⊢ T2 •*[h, d1] U2 → + ∀d2. ⦃G2, L2⦄ ⊢ T2 ▪[h, o] d2 → d1 ≤ d2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. +/3 width=5 by fquq_cpxs_trans, lstas_cpxs/ qed-. + +lemma fqup_cpxs_trans: ∀h,o,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h, o] U2 → + ∀T1. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 /2 width=3 by ex2_intro/ +#T #T2 #HT2 #_ #IHTU2 #T1 #HT1 elim (fqup_cpx_trans … HT1 … HT2) -T +#U1 #HTU1 #H2 elim (IHTU2 … H2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/ +qed-. + +lemma fqus_cpxs_trans: ∀h,o,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h, o] U2 → + ∀T1. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T2 #U2 #HTU2 #T1 #H elim (fqus_inv_gen … H) -H +[ #HT12 elim (fqup_cpxs_trans … HTU2 … HT12) /3 width=3 by fqup_fqus, ex2_intro/ +| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma fqus_lstas_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ∀U2,d1. ⦃G2, L2⦄ ⊢ T2 •*[h, d1] U2 → + ∀d2. ⦃G2, L2⦄ ⊢ T2 ▪[h, o] d2 → d1 ≤ d2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. +/3 width=6 by fqus_cpxs_trans, lstas_cpxs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma new file mode 100644 index 000000000..b54ea1582 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lfpx.ma". +include "basic_2/rt_computation/cpxs_drops.ma". +include "basic_2/rt_computation/cpxs_cpxs.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) + +(* Properties with uncounted parallel rt-transition on referred entries *****) + +lemma lfpx_cpxs_conf: ∀h,G. s_r_confluent1 … (cpxs h G) (lfpx h G). +/3 width=5 by lfpx_cpx_conf, s_r_conf1_LTC1/ qed-. + +lemma lfpx_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (lfpx h G). +#h #G #L2 #T1 #T2 #H @(cpx_ind … H) -G -L2 -T1 -T2 // +[ #G #L2 #s1 #L1 #H elim (lfpx_inv_sort … H) -H * /2 width=1 by cpx_cpxs/ +| #I #G #L2 #V #V2 #W2 #_ #IH #HVW2 #Y1 #H + elim (lfpx_inv_zero_pair_dx … H) -H #L1 #V1 #HL1 #HV1 #H destruct + /5 width=3 by lfpx_cpx_conf, cpxs_delta, cpxs_strap2/ +| #I #G #L2 #V #V2 #W2 #i #_ #IH #HVW2 #Y1 #H + elim (lfpx_inv_lref_pair_dx … H) -H #L1 #V1 #HL1 #HV1 + /4 width=3 by cpxs_lref, cpxs_strap2/ +| #p #I #G #L2 #V #V2 #T #T2 #_ #_ #IHV #IHT #L1 #H + elim (lfpx_inv_bind … H) -H /3 width=1 by cpxs_bind/ +| #I #G #L2 #V #V2 #T #T2 #_ #_ #IHV #IHT #L1 #H + elim (lfpx_inv_flat … H) -H /3 width=1 by cpxs_flat/ +| #G #L2 #V #T #T2 #T0 #_ #IH #HT02 #L1 #H + elim (lfpx_inv_bind … H) -H /3 width=3 by cpxs_zeta/ +| #G #L2 #V #T #T2 #_ #IH #L1 #H + elim (lfpx_inv_flat … H) -H /3 width=1 by cpxs_eps/ +| #G #L2 #V #V2 #T #_ #IH #L1 #H + elim (lfpx_inv_flat … H) -H /3 width=1 by cpxs_ee/ +| #p #G #L2 #V #V2 #W #W2 #T #T2 #_ #_ #_ #IHV #IHW #IHT #L1 #H + elim (lfpx_inv_flat … H) -H #HV #H + elim (lfpx_inv_bind … H) -H /3 width=1 by cpxs_beta/ +| #p #G #L2 #V #V2 #V0 #W #W2 #T #T2 #_ #_ #_ #IHV #IHW #IHT #HV20 #L1 #H + elim (lfpx_inv_flat … H) -H #HV #H + elim (lfpx_inv_bind … H) -H /3 width=3 by cpxs_theta/ +] +qed. + +lemma lfpx_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (lfpx h G). +#h #G #L2 #T1 #T2 #H #L1 #HL12 @(cpxs_ind … H) -T2 +/4 width=7 by lfpx_cpx_trans, cpxs_trans, lfpx_cpxs_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lift.ma deleted file mode 100644 index 9b4822e58..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lift.ma +++ /dev/null @@ -1,124 +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/multiple/fqus_fqus.ma". -include "basic_2/reduction/cpx_lift.ma". -include "basic_2/computation/cpxs.ma". - -(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) - -(* Advanced properties ******************************************************) - -lemma cpxs_delta: ∀h,o,I,G,L,K,V,V2,i. - ⬇[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ⬈*[h, o] V2 → - ∀W2. ⬆[0, i+1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ⬈*[h, o] W2. -#h #o #I #G #L #K #V #V2 #i #HLK #H elim H -V2 -[ /3 width=9 by cpx_cpxs, cpx_delta/ -| #V1 lapply (drop_fwd_drop2 … HLK) -HLK - elim (lift_total V1 0 (i+1)) /4 width=12 by cpx_lift, cpxs_strap1/ -] -qed. - -lemma lstas_cpxs: ∀h,o,G,L,T1,T2,d2. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 → - ∀d1. ⦃G, L⦄ ⊢ T1 ▪[h, o] d1 → d2 ≤ d1 → ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2. -#h #o #G #L #T1 #T2 #d2 #H elim H -G -L -T1 -T2 -d2 // -[ /3 width=3 by cpxs_sort, da_inv_sort/ -| #G #L #K #V1 #V2 #W2 #i #d2 #HLK #_ #HVW2 #IHV12 #d1 #H #Hd21 - elim (da_inv_lref … H) -H * #K0 #V0 [| #d0 ] #HLK0 - lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct /3 width=7 by cpxs_delta/ -| #G #L #K #V1 #V2 #W2 #i #d2 #HLK #_ #HVW2 #IHV12 #d1 #H #Hd21 - elim (da_inv_lref … H) -H * #K0 #V0 [| #d0 ] #HLK0 - lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct - #HV1 #H destruct lapply (le_plus_to_le_c … Hd21) -Hd21 - /3 width=7 by cpxs_delta/ -| /4 width=3 by cpxs_bind_dx, da_inv_bind/ -| /4 width=3 by cpxs_flat_dx, da_inv_flat/ -| /4 width=3 by cpxs_eps, da_inv_flat/ -] -qed. - -(* Advanced inversion lemmas ************************************************) - -lemma cpxs_inv_lref1: ∀h,o,G,L,T2,i. ⦃G, L⦄ ⊢ #i ⬈*[h, o] T2 → - T2 = #i ∨ - ∃∃I,K,V1,T1. ⬇[i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ⬈*[h, o] T1 & - ⬆[0, i+1] T1 ≡ T2. -#h #o #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/ -#T #T2 #_ #HT2 * -[ #H destruct - elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/ - * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/ -| * #I #K #V1 #T1 #HLK #HVT1 #HT1 - lapply (drop_fwd_drop2 … HLK) #H0LK - elim (cpx_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T - /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/ -] -qed-. - -(* Relocation properties ****************************************************) - -lemma cpxs_lift: ∀h,o,G. d_liftable (cpxs h o G). -/3 width=10 by cpx_lift, cpxs_strap1, d_liftable_LTC/ qed. - -lemma cpxs_inv_lift1: ∀h,o,G. d_deliftable_sn (cpxs h o G). -/3 width=6 by d_deliftable_sn_LTC, cpx_inv_lift1/ -qed-. - -(* Properties on supclosure *************************************************) - -lemma fqu_cpxs_trans: ∀h,o,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h, o] U2 → - ∀T1. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄. -#h #o #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 /2 width=3 by ex2_intro/ -#T #T2 #HT2 #_ #IHTU2 #T1 #HT1 elim (fqu_cpx_trans … HT1 … HT2) -T -#T #HT1 #HT2 elim (IHTU2 … HT2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/ -qed-. - -lemma fquq_cpxs_trans: ∀h,o,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h, o] U2 → - ∀T1. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. -#h #o #G1 #G2 #L1 #L2 #T2 #U2 #HTU2 #T1 #H elim (fquq_inv_gen … H) -H -[ #HT12 elim (fqu_cpxs_trans … HTU2 … HT12) /3 width=3 by fqu_fquq, ex2_intro/ -| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ -] -qed-. - -lemma fquq_lstas_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ∀U2,d1. ⦃G2, L2⦄ ⊢ T2 •*[h, d1] U2 → - ∀d2. ⦃G2, L2⦄ ⊢ T2 ▪[h, o] d2 → d1 ≤ d2 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. -/3 width=5 by fquq_cpxs_trans, lstas_cpxs/ qed-. - -lemma fqup_cpxs_trans: ∀h,o,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h, o] U2 → - ∀T1. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄. -#h #o #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 /2 width=3 by ex2_intro/ -#T #T2 #HT2 #_ #IHTU2 #T1 #HT1 elim (fqup_cpx_trans … HT1 … HT2) -T -#U1 #HTU1 #H2 elim (IHTU2 … H2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/ -qed-. - -lemma fqus_cpxs_trans: ∀h,o,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h, o] U2 → - ∀T1. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. -#h #o #G1 #G2 #L1 #L2 #T2 #U2 #HTU2 #T1 #H elim (fqus_inv_gen … H) -H -[ #HT12 elim (fqup_cpxs_trans … HTU2 … HT12) /3 width=3 by fqup_fqus, ex2_intro/ -| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ -] -qed-. - -lemma fqus_lstas_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ∀U2,d1. ⦃G2, L2⦄ ⊢ T2 •*[h, d1] U2 → - ∀d2. ⦃G2, L2⦄ ⊢ T2 ▪[h, o] d2 → d1 ≤ d2 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h, o] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. -/3 width=6 by fqus_cpxs_trans, lstas_cpxs/ 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 cb191dab1..7118b99b9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,4 +1,4 @@ -cpxs.ma cpxs_tdeq.ma cpxs_cpxs.ma +cpxs.ma cpxs_tdeq.ma cpxs_drops.ma cpxs_lfpx.ma cpxs_cpxs.ma lfpxs.ma lfpxs_fqup.ma csx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma csx_vector.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfpx.ma new file mode 100644 index 000000000..bf7dda13c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfpx.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpx_lfxs.ma". +include "basic_2/rt_transition/lfpx.ma". + +(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****) + +(* Advanced properties ******************************************************) + +lemma lfpx_cpx_conf: ∀h,G. s_r_confluent1 … (cpx h G) (lfpx h G). +/2 width=5 by cpx_lfxs_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt index 1adc75c38..67ed58697 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt @@ -1,6 +1,6 @@ cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma cpx.ma cpx_simple.ma cpx_drops.ma cpx_fqus.ma cpx_lsubr.ma cpx_lfxs.ma -lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_lfdeq.ma lfpx_aaa.ma +lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_lfdeq.ma lfpx_aaa.ma lfpx_lfpx.ma cnx.ma cnx_simple.ma cnx_drops.ma cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_lfxs.ma cpm_cpx.ma cpr.ma cpr_drops.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma index a2f681634..a1d50e69f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -43,7 +43,7 @@ definition R_confluent2_lfxs: relation4 (relation3 lenv term term) ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 → ∃∃T. R2 L1 T1 T & R1 L2 T2 T. -(* Basic properties ***********************************************************) +(* Basic properties *********************************************************) lemma lfxs_atom: ∀R,I. ⋆ ⦻*[R, ⓪{I}] ⋆. /3 width=3 by lexs_atom, frees_atom, ex2_intro/ 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 f3d9d6021..fe1040d58 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 @@ -116,7 +116,7 @@ table { [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx" + "csx_cpxs" + "csx_csx" * ] [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" * ] - [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_cpxs" * ] + [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_drops" + "cpxs_lfpx" + "cpxs_cpxs" * ] } ] } @@ -143,7 +143,7 @@ table { ] [ { "uncounted context-sensitive rt-transition" * } { [ "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" * ] - [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" * ] + [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lfpx" * ] [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ] } ] diff --git a/matita/matita/contribs/lambdadelta/partial.txt b/matita/matita/contribs/lambdadelta/partial.txt index 7596031ba..48819214f 100644 --- a/matita/matita/contribs/lambdadelta/partial.txt +++ b/matita/matita/contribs/lambdadelta/partial.txt @@ -5,3 +5,4 @@ basic_2/s_transition basic_2/s_computation basic_2/static basic_2/i_static +apps_2/examples/ex_cpr_omega.ma