From: Ferruccio Guidi Date: Fri, 5 Apr 2013 11:56:45 +0000 (+0000) Subject: - parallel substitution reaxiomatized X-Git-Tag: make_still_working~1202 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eb4b3b1b307fc392c36f0be253e6a111553259bc;p=helm.git - parallel substitution reaxiomatized - supclosure reaxiomatixed (now commutes with parallel substitution) - some refactoring --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma index aec82cd5a..7ededf2af 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma @@ -19,7 +19,7 @@ include "basic_2/computation/ltprs.ma". (* Advanced properties ******************************************************) -lemma ltprs_strip: ∀L1. ∀L:term. L ➡* L1 → ∀L2. L ➡ L2 → +lemma ltprs_strip: ∀L1. ∀L:lenv. L ➡* L1 → ∀L2. L ➡ L2 → ∃∃L0. L1 ➡ L0 & L2 ➡* L0. /3 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma index ec3c9cc57..87a4a71ab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma @@ -22,7 +22,7 @@ include "basic_2/computation/tprs.ma". (* Basic_1: was: pr1_strip *) lemma tprs_strip: ∀T1,T. T ➡* T1 → ∀T2. T ➡ T2 → ∃∃T0. T1 ➡ T0 & T2 ➡* T0. -/3 width=3/ qed. +/3 width=3 by TC_strip1, tpr_conf/ qed. (* Main propertis ***********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup.etc index dcfe086e9..0a980f6a7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup.etc @@ -1,94 +1,5 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "hvbox( ⦃ L1, break T1 ⦄ > break ⦃ L2 , break T2 ⦄ )" - non associative with precedence 45 - for @{ 'SupTerm $L1 $T1 $L2 $T2 }. - -include "basic_2/substitution/ldrop.ma". - -(* SUPCLOSURE ***************************************************************) - -inductive csup: bi_relation lenv term ≝ -| csup_lref : ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → csup L (#i) K V -| csup_bind_sn: ∀a,I,L,V,T. csup L (ⓑ{a,I}V.T) L V -| csup_bind_dx: ∀a,I,L,V,T. csup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T -| csup_flat_sn: ∀I,L,V,T. csup L (ⓕ{I}V.T) L V -| csup_flat_dx: ∀I,L,V,T. csup L (ⓕ{I}V.T) L T -. - -interpretation - "structural predecessor (closure)" - 'SupTerm L1 T1 L2 T2 = (csup L1 T1 L2 T2). - -(* Basic inversion lemmas ***************************************************) - -fact csup_inv_atom1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → ∀J. T1 = ⓪{J} → - ∃∃I,i. ⇩[0, i] L1 ≡ L2.ⓑ{I}T2 & J = LRef i. -#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 -[ #I #L #K #V #i #HLK #J #H destruct /2 width=4/ -| #a #I #L #V #T #J #H destruct -| #a #I #L #V #T #J #H destruct -| #I #L #V #T #J #H destruct -| #I #L #V #T #J #H destruct -] -qed-. - -lemma csup_inv_atom1: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ > ⦃L2, T2⦄ → - ∃∃I,i. ⇩[0, i] L1 ≡ L2.ⓑ{I}T2 & J = LRef i. -/2 width=3 by csup_inv_atom1_aux/ qed-. - -fact csup_inv_bind1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → - ∀b,J,W,U. T1 = ⓑ{b,J}W.U → - (L2 = L1 ∧ T2 = W) ∨ - (L2 = L1.ⓑ{J}W ∧ T2 = U). -#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 -[ #I #L #K #V #i #_ #b #J #W #U #H destruct -| #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/ -| #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/ -| #I #L #V #T #b #J #W #U #H destruct -| #I #L #V #T #b #J #W #U #H destruct -] -qed-. - -lemma csup_inv_bind1: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ > ⦃L2, T2⦄ → - (L2 = L1 ∧ T2 = W) ∨ - (L2 = L1.ⓑ{J}W ∧ T2 = U). -/2 width=4 by csup_inv_bind1_aux/ qed-. - -fact csup_inv_flat1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → - ∀J,W,U. T1 = ⓕ{J}W.U → - L2 = L1 ∧ (T2 = W ∨ T2 = U). -#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 -[ #I #L #K #V #i #_ #J #W #U #H destruct -| #a #I #L #V #T #J #W #U #H destruct -| #a #I #L #V #T #J #W #U #H destruct -| #I #L #V #T #J #W #U #H destruct /3 width=1/ -| #I #L #V #T #J #W #U #H destruct /3 width=1/ -] -qed-. - -lemma csup_inv_flat1: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ > ⦃L2, T2⦄ → - L2 = L1 ∧ (T2 = W ∨ T2 = U). -/2 width=4 by csup_inv_flat1_aux/ qed-. - (* Basic forward lemmas *****************************************************) -lemma csup_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → #{L2, T2} < #{L1, T1}. -#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/ /2 width=4 by ldrop_pair2_fwd_cw/ -qed-. - lemma csup_fwd_ldrop: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → ∃i. ⇩[0, i] L1 ≡ L2 ∨ ⇩[0, i] L2 ≡ L1. #L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /3 width=2/ /4 width=2/ @@ -155,3 +66,23 @@ lemma csup_inv_lref2_be: ∀L,U,i. ⦃L, U⦄ > ⦃L, #i⦄ → elim (lift_csup_trans_eq … HTU … H) -H -T #T #H elim (lift_inv_lref2_be … H ? ?) // qed-. + + +fact csup_inv_all4_refl_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → L1 = L2 → + ∨∨ ∃∃a,I,U. T1 = ⓑ{a,I}T2.U + | ∃∃I,W. T1 = ⓕ{I}W.T2 + | ∃∃I,U. T1 = ⓕ{I}T2.U. +#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /3 width=3/ /3 width=4/ +[ #I #L #K #V #i #HLK #H destruct + lapply (ldrop_pair2_fwd_cw … HLK V) -HLK #H + elim (lt_refl_false … H) +| #a #I #L #V #T #H + elim (discr_lpair_x_xy … H) +] +qed-. + +lemma csup_inv_all4_refl: ∀L,T1,T2. ⦃L, T1⦄ > ⦃L, T2⦄ → + ∨∨ ∃∃a,I,U. T1 = ⓑ{a,I}T2.U + | ∃∃I,W. T1 = ⓕ{I}W.T2 + | ∃∃I,U. T1 = ⓕ{I}T2.U. +/2 width=4 by csup_inv_all4_refl_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup_csup.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup_csup.etc index 813cb969d..661d89697 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup_csup.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csup_csup.etc @@ -17,22 +17,6 @@ include "basic_2/substitution/csup.ma". (* SUPCLOSURE ***************************************************************) -(* Advanced inversion lemmas ************************************************) - -lemma csup_inv_ldrop: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → - ∀J,W,j. ⇩[0, j] L1 ≡ L2.ⓑ{J}W → T1 = #j ∧ T2 = W. -#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 -[ #I #L #K #V #i #HLKV #J #W #j #HLKW - elim (ldrop_conf_div … HLKV … HLKW) -L /2 width=1/ -| #a -| #a -] -#I #L #V #T #J #W #j #H -lapply (ldrop_pair2_fwd_cw … H W) -H #H -[2: lapply (transitive_lt (#{L,W}) … H) /2 width=1/ -H #H ] -elim (lt_refl_false … H) -qed-. - (* Main forward lemmas ******************************************************) theorem csup_trans_fwd_refl: ∀L,L0,T1,T2. ⦃L, T1⦄ > ⦃L0, T2⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp.etc deleted file mode 100644 index c28eaea73..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp.etc +++ /dev/null @@ -1,64 +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 "hvbox( ⦃ L1, break T1 ⦄ > + break ⦃ L2 , break T2 ⦄ )" - non associative with precedence 45 - for @{ 'SupTermPlus $L1 $T1 $L2 $T2 }. - -include "basic_2/substitution/csup.ma". - -(* PLUS-ITERATED SUPCLOSURE *************************************************) - -definition csupp: bi_relation lenv term ≝ bi_TC … csup. - -interpretation "plus-iterated structural predecessor (closure)" - 'SupTermPlus L1 T1 L2 T2 = (csupp L1 T1 L2 T2). - -(* Basic eliminators ********************************************************) - -lemma csupp_ind: ∀L1,T1. ∀R:relation2 lenv term. - (∀L2,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → R L2 T2) → - (∀L,T,L2,T2. ⦃L1, T1⦄ >+ ⦃L, T⦄ → ⦃L, T⦄ > ⦃L2, T2⦄ → R L T → R L2 T2) → - ∀L2,T2. ⦃L1, T1⦄ >+ ⦃L2, T2⦄ → R L2 T2. -#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H -@(bi_TC_ind … IH1 IH2 ? ? H) -qed-. - -lemma csupp_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. - (∀L1,T1. ⦃L1, T1⦄ > ⦃L2, T2⦄ → R L1 T1) → - (∀L1,L,T1,T. ⦃L1, T1⦄ > ⦃L, T⦄ → ⦃L, T⦄ >+ ⦃L2, T2⦄ → R L T → R L1 T1) → - ∀L1,T1. ⦃L1, T1⦄ >+ ⦃L2, T2⦄ → R L1 T1. -#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H -@(bi_TC_ind_dx … IH1 IH2 ? ? H) -qed-. - -(* Basic properties *********************************************************) - -lemma csup_csupp: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → ⦃L1, T1⦄ >+ ⦃L2, T2⦄. -/2 width=1/ qed. - -lemma csupp_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ >+ ⦃L, T⦄ → ⦃L, T⦄ > ⦃L2, T2⦄ → - ⦃L1, T1⦄ >+ ⦃L2, T2⦄. -/2 width=4/ qed. - -lemma csupp_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ > ⦃L, T⦄ → ⦃L, T⦄ >+ ⦃L2, T2⦄ → - ⦃L1, T1⦄ >+ ⦃L2, T2⦄. -/2 width=4/ qed. - -(* Basic forward lemmas *****************************************************) - -lemma csupp_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ >+ ⦃L2, T2⦄ → #{L2, T2} < #{L1, T1}. -#L1 #L2 #T1 #T2 #H @(csupp_ind … H) -L2 -T2 -/3 width=3 by csup_fwd_cw, transitive_lt/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp_csupp.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp_csupp.etc deleted file mode 100644 index 5afdb68d4..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csupp_csupp.etc +++ /dev/null @@ -1,22 +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/unfold/csupp.ma". - -(* PLUS-ITERATED SUPCLOSURE *************************************************) - -(* Main propertis ***********************************************************) - -theorem csupp_trans: bi_transitive … csupp. -/2 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups.etc deleted file mode 100644 index 7f5879426..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups.etc +++ /dev/null @@ -1,107 +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 "hvbox( ⦃ L1, break T1 ⦄ > * break ⦃ L2 , break T2 ⦄ )" - non associative with precedence 45 - for @{ 'SupTermStar $L1 $T1 $L2 $T2 }. - -include "basic_2/substitution/csup.ma". -include "basic_2/unfold/csupp.ma". - -(* STAR-ITERATED SUPCLOSURE *************************************************) - -definition csups: bi_relation lenv term ≝ bi_star … csup. - -interpretation "star-iterated structural predecessor (closure)" - 'SupTermStar L1 T1 L2 T2 = (csups L1 T1 L2 T2). - -(* Basic eliminators ********************************************************) - -lemma csups_ind: ∀L1,T1. ∀R:relation2 lenv term. R L1 T1 → - (∀L,L2,T,T2. ⦃L1, T1⦄ >* ⦃L, T⦄ → ⦃L, T⦄ > ⦃L2, T2⦄ → R L T → R L2 T2) → - ∀L2,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → R L2 T2. -#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H -@(bi_star_ind … IH1 IH2 ? ? H) -qed-. - -lemma csups_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. R L2 T2 → - (∀L1,L,T1,T. ⦃L1, T1⦄ > ⦃L, T⦄ → ⦃L, T⦄ >* ⦃L2, T2⦄ → R L T → R L1 T1) → - ∀L1,T1. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → R L1 T1. -#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H -@(bi_star_ind_dx … IH1 IH2 ? ? H) -qed-. - -(* Basic properties *********************************************************) - -lemma csups_refl: bi_reflexive … csups. -/2 width=1/ qed. - -lemma csupp_csups: ∀L1,L2,T1,T2. ⦃L1, T1⦄ >+ ⦃L2, T2⦄ → ⦃L1, T1⦄ >* ⦃L2, T2⦄. -/2 width=1/ qed. - -lemma csup_csups: ∀L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → ⦃L1, T1⦄ >* ⦃L2, T2⦄. -/2 width=1/ qed. - -lemma csups_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ >* ⦃L, T⦄ → ⦃L, T⦄ > ⦃L2, T2⦄ → - ⦃L1, T1⦄ >* ⦃L2, T2⦄. -/2 width=4/ qed. - -lemma csups_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ > ⦃L, T⦄ → ⦃L, T⦄ >* ⦃L2, T2⦄ → - ⦃L1, T1⦄ >* ⦃L2, T2⦄. -/2 width=4/ qed. - -lemma csups_csupp_csupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ >* ⦃L, T⦄ → - ⦃L, T⦄ >+ ⦃L2, T2⦄ → ⦃L1, T1⦄ >+ ⦃L2, T2⦄. -/2 width=4/ qed. - -lemma csupp_csups_csupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ >+ ⦃L, T⦄ → - ⦃L, T⦄ >* ⦃L2, T2⦄ → ⦃L1, T1⦄ >+ ⦃L2, T2⦄. -/2 width=4/ qed. - -(* Basic forward lemmas *****************************************************) - -lemma csups_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → #{L2, T2} ≤ #{L1, T1}. -#L1 #L2 #T1 #T2 #H @(csups_ind … H) -L2 -T2 // -/4 width=3 by csup_fwd_cw, lt_to_le_to_lt, lt_to_le/ (**) (* slow even with trace *) -qed-. - -(* Advanced inversion lemmas for csupp **************************************) - -lemma csupp_inv_atom1_csups: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ >+ ⦃L2, T2⦄ → - ∃∃I,K,V,i. ⇩[0, i] L1 ≡ K.ⓑ{I}V & - ⦃K, V⦄ >* ⦃L2, T2⦄ & J = LRef i. -#J #L1 #L2 #T2 #H @(csupp_ind … H) -L2 -T2 -[ #L2 #T2 #H - elim (csup_inv_atom1 … H) -H * #i #HL12 #H destruct /2 width=7/ -| #L #T #L2 #T2 #_ #HT2 * #I #K #V #i #HLK #HVT #H destruct /3 width=8/ -] -qed-. - -lemma csupp_inv_bind1_csups: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ >+ ⦃L2, T2⦄ → - ⦃L1, W⦄ >* ⦃L2, T2⦄ ∨ ⦃L1.ⓑ{J}W, U⦄ >* ⦃L2, T2⦄. -#b #J #L1 #L2 #W #U #T2 #H @(csupp_ind … H) -L2 -T2 -[ #L2 #T2 #H - elim (csup_inv_bind1 … H) -H * #H1 #H2 destruct /2 width=1/ -| #L #T #L2 #T2 #_ #HT2 * /3 width=4/ -] -qed-. - -lemma csupp_inv_flat1_csups: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ >+ ⦃L2, T2⦄ → - ⦃L1, W⦄ >* ⦃L2, T2⦄ ∨ ⦃L1, U⦄ >* ⦃L2, T2⦄. -#J #L1 #L2 #W #U #T2 #H @(csupp_ind … H) -L2 -T2 -[ #L2 #T2 #H - elim (csup_inv_flat1 … H) -H #H1 * #H2 destruct /2 width=1/ -| #L #T #L2 #T2 #_ #HT2 * /3 width=4/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups_csups.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups_csups.etc index aa54d9bef..9978429d7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups_csups.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/csup/csups_csups.etc @@ -55,8 +55,3 @@ lemma lift_csups_trans_aux: ∀T1,U1,d,e. ⇧[d, e] T1 ≡ U1 → #L #L2 #U #U2 #HL1 #HL2 #IHL1 #H destruct * -T1 -U1 -d -e - -(* Main propertis ***********************************************************) - -theorem csups_trans: bi_transitive … csups. -/2 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsup.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsup.etc new file mode 100644 index 000000000..077fd7422 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsup.etc @@ -0,0 +1,123 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⧁ break ⦃ term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'RestSupTerm $L1 $T1 $L2 $T2 }. + +include "basic_2/grammar/cl_weight.ma". +include "basic_2/substitution/lift.ma". + +(* RESTRICTED SUPCLOSURE ****************************************************) + +inductive frsup: bi_relation lenv term ≝ +| frsup_bind_sn: ∀a,I,L,V,T. frsup L (ⓑ{a,I}V.T) L V +| frsup_bind_dx: ∀a,I,L,V,T. frsup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T +| frsup_flat_sn: ∀I,L,V,T. frsup L (ⓕ{I}V.T) L V +| frsup_flat_dx: ∀I,L,V,T. frsup L (ⓕ{I}V.T) L T +. + +interpretation + "restricted structural predecessor (closure)" + 'RestSupTerm L1 T1 L2 T2 = (frsup L1 T1 L2 T2). + +(* Basic inversion lemmas ***************************************************) + +fact frsup_inv_atom1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → + ∀J. T1 = ⓪{J} → ⊥. +#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 +[ #a #I #L #V #T #J #H destruct +| #a #I #L #V #T #J #H destruct +| #I #L #V #T #J #H destruct +| #I #L #V #T #J #H destruct +] +qed-. + +lemma frsup_inv_atom1: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ ⧁ ⦃L2, T2⦄ → ⊥. +/2 width=7 by frsup_inv_atom1_aux/ qed-. + +fact frsup_inv_bind1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → + ∀b,J,W,U. T1 = ⓑ{b,J}W.U → + (L2 = L1 ∧ T2 = W) ∨ + (L2 = L1.ⓑ{J}W ∧ T2 = U). +#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 +[ #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/ +| #a #I #L #V #T #b #J #W #U #H destruct /3 width=1/ +| #I #L #V #T #b #J #W #U #H destruct +| #I #L #V #T #b #J #W #U #H destruct +] +qed-. + +lemma frsup_inv_bind1: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ ⧁ ⦃L2, T2⦄ → + (L2 = L1 ∧ T2 = W) ∨ + (L2 = L1.ⓑ{J}W ∧ T2 = U). +/2 width=4 by frsup_inv_bind1_aux/ qed-. + +fact frsup_inv_flat1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → + ∀J,W,U. T1 = ⓕ{J}W.U → + L2 = L1 ∧ (T2 = W ∨ T2 = U). +#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 +[ #a #I #L #V #T #J #W #U #H destruct +| #a #I #L #V #T #J #W #U #H destruct +| #I #L #V #T #J #W #U #H destruct /3 width=1/ +| #I #L #V #T #J #W #U #H destruct /3 width=1/ +] +qed-. + +lemma frsup_inv_flat1: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⧁ ⦃L2, T2⦄ → + L2 = L1 ∧ (T2 = W ∨ T2 = U). +/2 width=4 by frsup_inv_flat1_aux/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma frsup_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}. +#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/ +qed-. + +lemma frsup_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ♯{L1} ≤ ♯{L2}. +#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/ +qed-. + +lemma frsup_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ♯{T2} < ♯{T1}. +#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/ /2 width=1 by le_minus_to_plus/ +qed-. + +lemma frsup_fwd_append: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ∃L. L2 = L1 @@ L. +#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 +[ #a +| #a #I #L #V #_ @(ex_intro … (⋆.ⓑ{I}V)) // +] +#I #L #V #T @(ex_intro … (⋆)) // +qed-. + +(* Advanced forward lemmas **************************************************) + +lemma lift_frsup_trans: ∀T1,U1,d,e. ⇧[d, e] T1 ≡ U1 → + ∀L,K,U2. ⦃L, U1⦄ ⧁ ⦃L @@ K, U2⦄ → + ∃T2. ⇧[d + |K|, e] T2 ≡ U2. +#T1 #U1 #d #e * -T1 -U1 -d -e +[5: #a #I #V1 #W1 #T1 #U1 #d #e #HVW1 #HTU1 #L #K #X #H + elim (frsup_inv_bind1 … H) -H * + [ -HTU1 #H1 #H2 destruct + >(append_inv_refl_dx … H1) -L -K normalize /2 width=2/ + | -HVW1 #H1 #H2 destruct + >(append_inv_pair_dx … H1) -L -K normalize /2 width=2/ + ] +|6: #I #V1 #W1 #T1 #U1 #d #e #HVW1 #HUT1 #L #K #X #H + elim (frsup_inv_flat1 … H) -H #H1 * #H2 destruct + >(append_inv_refl_dx … H1) -L -K normalize /2 width=2/ +] +#i #d #e [2,3: #_ ] #L #K #X #H +elim (frsup_inv_atom1 … H) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsupp.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsupp.etc new file mode 100644 index 000000000..9f7a8dc9d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsupp.etc @@ -0,0 +1,110 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⧁ + break ⦃ term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'RestSupTermPlus $L1 $T1 $L2 $T2 }. + +include "basic_2/substitution/frsup.ma". + +(* PLUS-ITERATED RESTRICTED SUPCLOSURE **************************************) + +definition frsupp: bi_relation lenv term ≝ bi_TC … frsup. + +interpretation "plus-iterated restricted structural predecessor (closure)" + 'RestSupTermPlus L1 T1 L2 T2 = (frsupp L1 T1 L2 T2). + +(* Basic eliminators ********************************************************) + +lemma frsupp_ind: ∀L1,T1. ∀R:relation2 lenv term. + (∀L2,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → R L2 T2) → + (∀L,T,L2,T2. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ → ⦃L, T⦄ ⧁ ⦃L2, T2⦄ → R L T → R L2 T2) → + ∀L2,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → R L2 T2. +#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H +@(bi_TC_ind … IH1 IH2 ? ? H) +qed-. + +lemma frsupp_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. + (∀L1,T1. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → R L1 T1) → + (∀L1,L,T1,T. ⦃L1, T1⦄ ⧁ ⦃L, T⦄ → ⦃L, T⦄ ⧁+ ⦃L2, T2⦄ → R L T → R L1 T1) → + ∀L1,T1. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → R L1 T1. +#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H +@(bi_TC_ind_dx … IH1 IH2 ? ? H) +qed-. + +(* Baic inversion lemmas ****************************************************) + +lemma frsupp_inv_dx: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ ∨ + ∃∃L,T. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ & ⦃L, T⦄ ⧁ ⦃L2, T2⦄. +/2 width=1 by bi_TC_decomp_r/ qed-. + +lemma frsupp_inv_sn: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ ∨ + ∃∃L,T. ⦃L1, T1⦄ ⧁ ⦃L, T⦄ & ⦃L, T⦄ ⧁+ ⦃L2, T2⦄. +/2 width=1 by bi_TC_decomp_l/ qed-. + +(* Basic properties *********************************************************) + +lemma frsup_frsupp: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄. +/2 width=1/ qed. + +lemma frsupp_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ → ⦃L, T⦄ ⧁ ⦃L2, T2⦄ → + ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄. +/2 width=4/ qed. + +lemma frsupp_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁ ⦃L, T⦄ → ⦃L, T⦄ ⧁+ ⦃L2, T2⦄ → + ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄. +/2 width=4/ qed. + +(* Basic forward lemmas *****************************************************) + +lemma frsupp_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}. +#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2 +/3 width=3 by frsup_fwd_fw, transitive_lt/ +qed-. + +lemma frsupp_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{L1} ≤ ♯{L2}. +#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2 +/2 width=3 by frsup_fwd_lw/ (**) (* /3 width=5 by frsup_fwd_lw, transitive_le/ is too slow *) +#L #T #L2 #T2 #_ #HL2 #HL1 +lapply (frsup_fwd_lw … HL2) -HL2 /2 width=3 by transitive_le/ +qed-. + +lemma frsupp_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{T2} < ♯{T1}. +#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2 +/3 width=3 by frsup_fwd_tw, transitive_lt/ +qed-. + +lemma frsupp_fwd_append: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ∃L. L2 = L1 @@ L. +#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2 /2 width=3 by frsup_fwd_append/ +#L #T #L2 #T2 #_ #HL2 * #K1 #H destruct +elim (frsup_fwd_append … HL2) -HL2 #K2 #H destruct /2 width=2/ +qed-. + +(* Advanced forward lemmas **************************************************) + +lemma lift_frsupp_trans: ∀L,U1,K,U2. ⦃L, U1⦄ ⧁+ ⦃L @@ K, U2⦄ → + ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → + ∃T2. ⇧[d + |K|, e] T2 ≡ U2. +#L #U1 @(f2_ind … fw … L U1) -L -U1 #n #IH +#L #U1 #Hn #K #U2 #H #T1 #d #e #HTU1 destruct +elim (frsupp_inv_sn … H) -H /2 width=5 by lift_frsup_trans/ * +#L0 #U0 #HL0 #HL +elim (frsup_fwd_append … HL0) #K0 #H destruct +elim (frsupp_fwd_append … HL) #L0 >append_assoc #H +elim (append_inj_dx … H ?) -H // #_ #H destruct +(append_inv_refl_dx … (sym_eq … H1)) -H1 normalize /2 width=2/ +| /2 width=5 by lift_frsupp_trans/ +] +qed-. + +(* Advanced inversion lemmas for frsupp **************************************) + +lemma frsupp_inv_atom1_frsups: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ ⧁+ ⦃L2, T2⦄ → ⊥. +#J #L1 #L2 #T2 #H @(frsupp_ind … H) -L2 -T2 // +#L2 #T2 #H elim (frsup_inv_atom1 … H) +qed-. + +lemma frsupp_inv_bind1_frsups: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ ⧁+ ⦃L2, T2⦄ → + ⦃L1, W⦄ ⧁* ⦃L2, T2⦄ ∨ ⦃L1.ⓑ{J}W, U⦄ ⧁* ⦃L2, T2⦄. +#b #J #L1 #L2 #W #U #T2 #H @(frsupp_ind … H) -L2 -T2 +[ #L2 #T2 #H + elim (frsup_inv_bind1 … H) -H * #H1 #H2 destruct /2 width=1/ +| #L #T #L2 #T2 #_ #HT2 * /3 width=4/ +] +qed-. + +lemma frsupp_inv_flat1_frsups: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⧁+ ⦃L2, T2⦄ → + ⦃L1, W⦄ ⧁* ⦃L2, T2⦄ ∨ ⦃L1, U⦄ ⧁* ⦃L2, T2⦄. +#J #L1 #L2 #W #U #T2 #H @(frsupp_ind … H) -L2 -T2 +[ #L2 #T2 #H + elim (frsup_inv_flat1 … H) -H #H1 * #H2 destruct /2 width=1/ +| #L #T #L2 #T2 #_ #HT2 * /3 width=4/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsups_frsups.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsups_frsups.etc new file mode 100644 index 000000000..e7b7de26e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/frsups_frsups.etc @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/frsups.ma". + +(* STAR-ITERATED RESTRICTED SUPCLOSURE **************************************) + +(* Main propertis ***********************************************************) + +theorem frsups_trans: bi_transitive … frsups. +/2 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/ssta_frsups.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/ssta_frsups.etc new file mode 100644 index 000000000..9eb1fbd8b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/frsup/ssta_frsups.etc @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/frsups.ma". +include "basic_2/static/ssta.ma". + +(* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************) + +(* Advanced inversion lemmas ************************************************) + +lemma ssta_inv_frsupp: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ⦃L, U⦄ ⧁+ ⦃L, T⦄ → ⊥. +#h #g #L #T #U #l #H elim H -L -T -U -l +[ #L #k #l #_ #H + elim (frsupp_inv_atom1_frsups … H) +| #L #K #V #W #U #i #l #_ #_ #HWU #_ #H + elim (lift_frsupp_trans … (⋆) … H … HWU) -U #X #H + elim (lift_inv_lref2_be … H ? ?) -H // +| #L #K #W #V #U #i #l #_ #_ #HWU #_ #H + elim (lift_frsupp_trans … (⋆) … H … HWU) -U #X #H + elim (lift_inv_lref2_be … H ? ?) -H // +| #a #I #L #V #T #U #l #_ #IHTU #H + elim (frsupp_inv_bind1_frsups … H) -H #H [2: /4 width=4/ ] -IHTU + lapply (frsups_fwd_fw … H) -H normalize + (ltpr_fwd_length … HL12) in HT2; #HT2 -elim (tpr_tpss_ltpr … HL12 … HT2) -L1 /3 width=3/ +elim (ltpr_tpr_tpss_conf … HL12 … HT2) -L1 /3 width=3/ qed. lemma cpr_ltpr_conf_tpss: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡ T2 → @@ -42,5 +42,5 @@ lemma cpr_ltpr_conf_tpss: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L1 ⊢ T1 ➡ T2 → #L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 elim (cpr_ltpr_conf_eq … HT12 … HL12) -HT12 #T #HT1 #HT2 elim (cpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 -HT1 #U2 #HU12 #HTU2 -lapply (tpss_weak_all … HTU2) -HTU2 #HTU2 /3 width=5/ (**) (* /4 width=5/ is too slow *) +lapply (tpss_weak_full … HTU2) -HTU2 #HTU2 /3 width=5/ (**) (* /4 width=5/ is too slow *) qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpss_sn.ma index 49ec47f77..f946e4cfb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpss_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_ltpss_sn.ma @@ -22,7 +22,7 @@ include "basic_2/reducibility/cpr.ma". lemma ltpss_sn_cpr_trans: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2. #L1 #L2 #d #e #HL12 #T1 #T2 * -lapply (ltpss_sn_weak_all … HL12) +lapply (ltpss_sn_weak_full … HL12) <(ltpss_sn_fwd_length … HL12) -HL12 /3 width=5/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_tpss.ma index fc4f2b8c5..d8c7225d9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_tpss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_tpss.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/tpr_tpss.ma". +include "basic_2/reducibility/ltpr_tpss.ma". include "basic_2/reducibility/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) @@ -22,7 +22,7 @@ include "basic_2/reducibility/cpr.ma". lemma cpr_tpss_trans: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2,d,e. L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ➡ T2. #L #T1 #T * #T0 #HT10 #HT0 #T2 #d #e #HT2 -lapply (tpss_weak_all … HT2) -HT2 #HT2 +lapply (tpss_weak_full … HT2) -HT2 #HT2 lapply (tpss_trans_eq … HT0 HT2) -T /2 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma index 007681d0b..baa630f5b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/fpr_cpr.ma @@ -36,7 +36,7 @@ elim (le_or_ge (|K|) d) #Hd [ elim (ldrop_ltpss_sn_trans_ge … HLK … HK2 …) | elim (ldrop_ltpss_sn_trans_be … HLK … HK2 …) ] // -Hd #L2 #HL2 #HLK2 -lapply (ltpss_sn_weak_all … HL2) -K /3 width=4/ +lapply (ltpss_sn_weak_full … HL2) -K /3 width=4/ qed-. (* Advanced properties ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma index 04686f960..8a01f263a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_cpr.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/unfold/ltpss_sn_ltpss_sn.ma". +include "basic_2/reducibility/ltpr_ldrop.ma". include "basic_2/reducibility/cpr.ma". include "basic_2/reducibility/lfpr.ma". @@ -27,3 +28,25 @@ lemma lfpr_pair_cpr: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 ➡ lapply (ltpss_sn_tpss_trans_eq … HV2 … HL2) -HV2 #V2 @(ex2_intro … (L.ⓑ{I}V)) /2 width=1/ (**) (* explicit constructor *) qed. + +(* Properties on supclosure *************************************************) +(* +lamma fsub_cpr_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ➡ U2 → + ∃∃L,U1. ⦃L1⦄ ➡ ⦃L⦄ & L ⊢ T1 ➡ U1 & ⦃L, U1⦄ ⊃ ⦃L2, U2⦄. +#L1 #L2 #T1 #T2 #HT12 #U2 * #T #H1 #H2 +elim (fsub_tpr_trans … HT12 … H1) -T2 #L #U #HL1 #HT1U #HUT +elim (fsup_tpss_trans_full … HUT … H2) -T -HUT -H2 #L #U #HL1 #HT1U #HUT + + + + + + + #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ] +#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2 +elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HK2 +elim (lift_total T d e) #U #HTU +elim (ldrop_ltpr_trans … HLK1 … HK1) -HLK1 -HK1 #L #HL1 #HLK +lapply (tpr_lift … HT1 … HTU1 … HTU) -HT1 -HTU1 /3 width=11/ +qed-. +*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ldrop.ma index 945279795..02404a11d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ldrop.ma @@ -13,11 +13,14 @@ (**************************************************************************) include "basic_2/substitution/ldrop_lpx.ma". +include "basic_2/substitution/fsup.ma". include "basic_2/reducibility/tpr_lift.ma". include "basic_2/reducibility/ltpr.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) +(* Properies on local environment slicing ***********************************) + (* Basic_1: was: wcpr0_drop *) lemma ltpr_ldrop_conf: dropable_sn ltpr. /3 width=3 by lpx_deliftable_dropable, tpr_inv_lift1/ qed. @@ -28,3 +31,15 @@ lemma ldrop_ltpr_trans: dedropable_sn ltpr. lemma ltpr_ldrop_trans_O1: dropable_dx ltpr. /2 width=3/ qed. + +(* Properties on supclosure *************************************************) + +lemma fsub_tpr_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. T2 ➡ U2 → + ∃∃L,U1. L1 ➡ L & T1 ➡ U1 & ⦃L, U1⦄ ⊃ ⦃L2, U2⦄. +#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ] +#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2 +elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HK2 +elim (lift_total T d e) #U #HTU +elim (ldrop_ltpr_trans … HLK1 … HK1) -HLK1 -HK1 #L #HL1 #HLK +lapply (tpr_lift … HT1 … HTU1 … HTU) -HT1 -HTU1 /3 width=11/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_dx.ma index cee1cb49e..00730b732 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_dx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_dx.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/tpr_tpss.ma". +include "basic_2/reducibility/ltpr_tpss.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) @@ -27,10 +27,10 @@ lemma ltpr_ltpss_dx_conf: ∀L1,K1,d,e. L1 ▶* [d, e] K1 → ∀L2. L1 ➡ L2 | #L1 #K1 #I #V1 #W1 #e #_ #HVW1 #IHLK1 #X #H elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12 - elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/ + elim (ltpr_tpr_tpss_conf … HK12 … HV12 … HVW1) -V1 /3 width=5/ | #L1 #K1 #I #V1 #W1 #d #e #_ #HVW1 #IHLK1 #X #H elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12 - elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/ + elim (ltpr_tpr_tpss_conf … HK12 … HV12 … HVW1) -V1 /3 width=5/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tps.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tps.ma index 75792eef0..7f08be62b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tps.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tps.ma @@ -18,24 +18,7 @@ include "basic_2/reducibility/ltpr_ldrop.ma". (* Properties concerning parallel substitution on terms *********************) -lemma ltpr_tps_trans: ∀L2,T1,T2,d,e. L2 ⊢ T1 ▶ [d, e] T2 → ∀L1. L1 ➡ L2 → - ∃∃T. L1 ⊢ T1 ▶ [d, e] T & T ➡ T2. -#L2 #T1 #T2 #d #e #H elim H -L2 -T1 -T2 -d -e -[ /2 width=3/ -| #L2 #K2 #V2 #W2 #i #d #e #Hdi #Hide #HLK2 #HVW2 #L1 #HL12 - elim (ltpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H - elim (ltpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct -K2 - elim (lift_total V1 0 (i+1)) #W1 #HVW1 - lapply (tpr_lift … HV12 … HVW1 … HVW2) -V2 /3 width=4/ -| #L2 #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L1 #HL12 - elim (IHV12 … HL12) -IHV12 #V #HV1 #HV2 - elim (IHT12 (L1.ⓑ{I}V) ?) /2 width=1/ -L2 /3 width=5/ -| #L2 #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L1 #HL12 - elim (IHV12 … HL12) -IHV12 - elim (IHT12 … HL12) -L2 /3 width=5/ -] -qed. - +(* Basic_1: was: pr0_subst1_fwd *) lemma ltpr_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 → ∀L2. L1 ➡ L2 → ∃∃T. L2 ⊢ T1 ▶ [d, e] T & T2 ➡ T. #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e @@ -52,4 +35,23 @@ lemma ltpr_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 → ∀L2. L1 ➡ elim (IHV12 … HL12) -IHV12 elim (IHT12 … HL12) -L1 /3 width=5/ ] -qed. +qed-. + +(* Basic_1: was: pr0_subst1_back *) +lemma ltpr_tps_trans: ∀L2,T1,T2,d,e. L2 ⊢ T1 ▶ [d, e] T2 → ∀L1. L1 ➡ L2 → + ∃∃T. L1 ⊢ T1 ▶ [d, e] T & T ➡ T2. +#L2 #T1 #T2 #d #e #H elim H -L2 -T1 -T2 -d -e +[ /2 width=3/ +| #L2 #K2 #V2 #W2 #i #d #e #Hdi #Hide #HLK2 #HVW2 #L1 #HL12 + elim (ltpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H + elim (ltpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct -K2 + elim (lift_total V1 0 (i+1)) #W1 #HVW1 + lapply (tpr_lift … HV12 … HVW1 … HVW2) -V2 /3 width=4/ +| #L2 #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L1 #HL12 + elim (IHV12 … HL12) -IHV12 #V #HV1 #HV2 + elim (IHT12 (L1.ⓑ{I}V) ?) /2 width=1/ -L2 /3 width=5/ +| #L2 #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #L1 #HL12 + elim (IHV12 … HL12) -IHV12 + elim (IHT12 … HL12) -L2 /3 width=5/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tpss.ma new file mode 100644 index 000000000..71586fa36 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_tpss.ma @@ -0,0 +1,91 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/unfold/ltpss_dx_ltpss_dx.ma". +include "basic_2/reducibility/ltpr_tps.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) + +(* Properties on partial unfold for terms ***********************************) + +(* Basic_1: was: pr0_subst1 *) +lemma ltpr_tpr_tps_conf: ∀T1,T2. T1 ➡ T2 → + ∀L1,d,e,U1. L1 ⊢ T1 ▶ [d, e] U1 → + ∀L2. L1 ➡ L2 → + ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2. +#T1 #T2 #H elim H -T1 -T2 +[ #I #L1 #d #e #U1 #H #L2 #HL12 + elim (ltpr_tps_conf … H … HL12) -L1 /3 width=3/ +| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 + elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct + elim (IHV12 … HVW1 … HL12) -V1 + elim (IHT12 … HTU1 … HL12) -T1 -HL12 /3 width=5/ +| #a #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 + elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct + elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct + elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2 + elim (IHT12 … HTT1 (L2. ⓛWW) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2 + lapply (tpss_lsubr_trans … HTT2 (L2. ⓓVV2) ?) -HTT2 /3 width=5/ +| #a #I #V1 #V2 #T1 #T #T2 #HV12 #_ #HT2 #IHV12 #IHT1 #L1 #d #e #X #H #L2 #HL12 + elim (tps_inv_bind1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct + elim (IHV12 … HVW1 … HL12) -V1 #W2 #HW12 #HVW2 + elim (IHT1 … HTU1 (L2. ⓑ{I} W2) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU + elim (tpss_strip_neq … HTU … HT2 ?) -T /2 width=1/ #U2 #HU2 #HTU2 + lapply (tps_lsubr_trans … HU2 (L2. ⓑ{I} V2) ?) -HU2 /2 width=1/ #HU2 + elim (ltpss_dx_tps_conf … HU2 (L2. ⓑ{I} W2) (d + 1) e ?) -HU2 /2 width=1/ #U3 #HU3 #HU23 + lapply (tps_lsubr_trans … HU3 (⋆. ⓑ{I} W2) ?) -HU3 /2 width=1/ #HU3 + lapply (tpss_lsubr_trans … HU23 (L2. ⓑ{I} W2) ?) -HU23 /2 width=1/ #HU23 + lapply (tpss_trans_eq … HTU2 … HU23) -U2 /3 width=5/ +| #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12 + elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct + elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct + elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2 + elim (IHW12 … HWW1 … HL12) -W1 #WW2 #HWW12 #HWW2 + elim (IHT12 … HTT1 (L2. ⓓWW2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2 + elim (lift_total VV2 0 1) #VV #H2VV + lapply (tpss_lift_ge … HVV2 (L2. ⓓWW2) … HV2 … H2VV) -V2 /2 width=1/ #HVV + @ex2_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *) +| #V #T1 #T #T2 #_ #HT2 #IHT1 #L1 #d #e #X #H #L2 #HL12 + elim (tps_inv_bind1 … H) -H #W #U1 #_ #HTU1 #H destruct -V + elim (IHT1 … HTU1 (L2.ⓓW) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU + elim (tpss_inv_lift1_ge … HTU L2 … HT2 ?) -T (append_inv_refl_dx … H1) -L -K normalize /2 width=2/ - | -HVW1 #H1 #H2 destruct - >(append_inv_pair_dx … H1) -L -K normalize /2 width=2/ - ] -|6: #I #V1 #W1 #T1 #U1 #d #e #HVW1 #HUT1 #L #K #X #H - elim (frsup_inv_flat1 … H) -H #H1 * #H2 destruct - >(append_inv_refl_dx … H1) -L -K normalize /2 width=2/ -] -#i #d #e [2,3: #_ ] #L #K #X #H -elim (frsup_inv_atom1 … H) -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsup.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsup.ma new file mode 100644 index 000000000..c8e78d9a9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsup.ma @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/ldrop.ma". + +(* SUPCLOSURE ***************************************************************) + +inductive fsup: bi_relation lenv term ≝ +| fsup_lref : ∀I,L,V. fsup (L.ⓑ{I}V) (#0) L V +| fsup_bind_sn: ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) L V +| fsup_bind_dx: ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T +| fsup_flat_sn: ∀I,L,V,T. fsup L (ⓕ{I}V.T) L V +| fsup_flat_dx: ∀I,L,V,T. fsup L (ⓕ{I}V.T) L T +| fsup_ldrop : ∀L1,K1,K2,T1,T2,U1,d,e. + ⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 → + fsup K1 T1 K2 T2 → fsup L1 U1 K2 T2 +. + +interpretation + "structural successor (closure)" + 'SupTerm L1 T1 L2 T2 = (fsup L1 T1 L2 T2). + +(* Basic properties *********************************************************) + +lemma fsup_lref_S_lt: ∀I,L,K,V,T,i. 0 < i → ⦃L, #(i-1)⦄ ⊃ ⦃K, T⦄ → ⦃L.ⓑ{I}V, #i⦄ ⊃ ⦃K, T⦄. +/3 width=7/ qed. + +lemma fsup_lref: ∀I,K,V,i,L. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃L, #i⦄ ⊃ ⦃K, V⦄. +#I #K #V #i @(nat_elim1 i) -i #i #IH #L #H +elim (ldrop_inv_O1_pair2 … H) -H * +[ #H1 #H2 destruct // +| #I1 #K1 #V1 #HK1 #H #Hi destruct + lapply (IH … HK1) /2 width=1/ +] +qed. + +(* Basic forward lemmas *****************************************************) + +lemma fsup_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}. +#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // +#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 +lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1 +lapply (lift_fwd_tw … HTU1) -HTU1 #HTU1 +@(lt_to_le_to_lt … IHT12) -IHT12 /2 width=1/ +qed-. + +fact fsup_fwd_length_lref1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀i. T1 = #i → |L2| < |L1|. +#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 +[ 6: #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct + lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1 + elim (lift_inv_lref2 … HTU1) -HTU1 * #Hdei #H destruct + @(lt_to_le_to_lt … HLK1) /2 width=2/ +| normalize // |2,3: #a +] #I #L #V #T #j #H destruct +qed-. + +lemma fsup_fwd_length_lref1: ∀L1,L2,T2,i. ⦃L1, #i⦄ ⊃ ⦃L2, T2⦄ → |L2| < |L1|. +/2 width=5 by fsup_fwd_length_lref1_aux/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma index f1bc18f7d..8782fa93d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma @@ -131,6 +131,19 @@ lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ⇩[d, e] K1. ⓑ{I} V1 ≡ L2 → 0 < L2 = K2. ⓑ{I} V2. /2 width=3/ qed-. +lemma ldrop_inv_O1_pair2: ∀I,K,V,e,L1. ⇩[0, e] L1 ≡ K. ⓑ{I} V → + (e = 0 ∧ L1 = K. ⓑ{I} V) ∨ + ∃∃I1,K1,V1. ⇩[0, e - 1] K1 ≡ K. ⓑ{I} V & L1 = K1.ⓑ{I1}V1 & 0 < e. +#I #K #V #e * +[ #H lapply (ldrop_inv_atom1 … H) -H #H destruct +| #L1 #I1 #V1 #H + elim (ldrop_inv_O1 … H) -H * + [ #H1 #H2 destruct /3 width=1/ + | /3 width=5/ + ] +] +qed-. + fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → ∃∃K1,V1. ⇩[d - 1, e] K1 ≡ K2 & @@ -258,11 +271,15 @@ lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇩[O, e] L1 ≡ K2. ⓑ{I2} V2 → ] qed-. +lemma ldrop_fwd_length: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → |L2| ≤ |L1|. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize /2 width=1/ +qed-. + lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize [ /2 width=3/ | #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 - >(tw_lift … HV21) -HV21 /2 width=1/ + >(lift_fwd_tw … HV21) -HV21 /2 width=1/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma index 2605b921c..f972cb2b2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma @@ -62,7 +62,7 @@ fact lpx_dropable_aux: ∀R,L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. lpx R L1 L | #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_ >commutative_plus normalize #H destruct ] -qed. +qed-. -lemma ltpr_dropable: ∀R. dropable_dx (lpx R). -/2 width=5/ qed. +lemma ltpx_dropable: ∀R. dropable_dx (lpx R). +/2 width=5 by lpx_dropable_aux/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma index 84babbdc8..7e7961eab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma @@ -276,7 +276,7 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma tw_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ♯{T1} = ♯{T2}. +lemma lift_fwd_tw: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ♯{T1} = ♯{T2}. #d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize // qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma index af450e34d..7d89243d5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma @@ -12,6 +12,10 @@ (* *) (**************************************************************************) +notation "hvbox( L ⊢ break term 46 T1 break ▶ [ term 46 d , break term 46 e ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PSubst $L $T1 $d $e $T2 }. + include "basic_2/substitution/ldrop_append.ma". (* PARALLEL SUBSTITUTION ON TERMS *******************************************) @@ -91,8 +95,8 @@ lemma tps_weak_top: ∀L,T1,T2,d,e. ] qed. -lemma tps_weak_all: ∀L,T1,T2,d,e. - L ⊢ T1 ▶ [d, e] T2 → L ⊢ T1 ▶ [0, |L|] T2. +lemma tps_weak_full: ∀L,T1,T2,d,e. + L ⊢ T1 ▶ [d, e] T2 → L ⊢ T1 ▶ [0, |L|] T2. #L #T1 #T2 #d #e #HT12 lapply (tps_weak … HT12 0 (d + e) ? ?) -HT12 // #HT12 lapply (tps_weak_top … HT12) // diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss.ma new file mode 100644 index 000000000..fa8f4fb4e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss.ma @@ -0,0 +1,183 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/ldrop_append.ma". + +(* CONTEXT-SENSITIVE PARALLEL UNFOLD FOR TERMS ******************************) + +inductive cpss: lenv → relation term ≝ +| cpss_atom : ∀L,I. cpss L (⓪{I}) (⓪{I}) +| cpss_subst: ∀L,K,V,V2,W2,i. + ⇩[0, i] L ≡ K. ⓓV → cpss K V V2 → + ⇧[0, i + 1] V2 ≡ W2 → cpss L (#i) W2 +| cpss_bind : ∀L,a,I,V1,V2,T1,T2. + cpss L V1 V2 → cpss (L. ⓑ{I} V1) T1 T2 → + cpss L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2) +| cpss_flat : ∀L,I,V1,V2,T1,T2. + cpss L V1 V2 → cpss L T1 T2 → + cpss L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2) +. + +interpretation "context-sensitive parallel unfold (term)" + 'PSubstStar L T1 T2 = (cpss L T1 T2). + +(* Basic properties *********************************************************) + +(* Note: it does not hold replacing |L1| with |L2| *) +lemma cpss_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ▶* T2 → + ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ▶* T2. +#L1 #T1 #T2 #H elim H -L1 -T1 -T2 +[ // +| #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 + lapply (ldrop_fwd_ldrop2_length … HLK1) #Hi + lapply (ldrop_fwd_O1_length … HLK1) #H2i + elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // -Hi + shift_append_assoc normalize #H + elim (cpss_inv_bind1 … H) -H + #V0 #T0 #_ #HT10 #H destruct + elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct + >append_length >HL12 -HL12 + @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *) +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss_lift.ma new file mode 100644 index 000000000..616ea63c7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/cpss_lift.ma @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/ldrop_ldrop.ma". +include "basic_2/unfold/cpss.ma". + +(* CONTEXT-SENSITIVE PARALLEL UNFOLD FOR TERMS ******************************) + +(* Relocation properties ****************************************************) + +lemma cpss_lift: l_liftable cpss. +#K #T1 #T2 #H elim H -K -T1 -T2 +[ #K #I #L #d #e #_ #U1 #H1 #U2 #H2 + >(lift_mono … H1 … H2) -H1 -H2 // +| #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2 + elim (lift_inv_lref1 … H) * #Hid #H destruct + [ elim (lift_trans_ge … HVW2 … HWU2 ?) -W2 // plus_plus_comm_23 #HVU2 + lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=6/ + ] +| #K #a #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 + elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct + elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5/ +| #K #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 + elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct + elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/ +] +qed. + +lemma cpss_inv_lift1: l_deliftable_sn cpss. +#L #U1 #U2 #H elim H -L -U1 -U2 +[ #L * #i #K #d #e #_ #T1 #H + [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/ + | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/ + | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/ + ] +| #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H + elim (lift_inv_lref2 … H) -H * #Hid #H destruct + [ elim (ldrop_conf_lt … HLK … HLV ?) -L // #L #U #HKL #HLV #HUV + elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2 + elim (lift_trans_le … HUV2 … HVW2 ?) -V2 // >minus_plus plus_minus // (tw_lift … HT2) -T2 /2 width=4 by tpss_fwd_tw/ +>(lift_fwd_tw … HT2) -T2 /2 width=4 by tpss_fwd_tw/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp.ma deleted file mode 100644 index add56ba3d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/frsupp.ma +++ /dev/null @@ -1,106 +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/substitution/frsup.ma". - -(* PLUS-ITERATED RESTRICTED SUPCLOSURE **************************************) - -definition frsupp: bi_relation lenv term ≝ bi_TC … frsup. - -interpretation "plus-iterated restricted structural predecessor (closure)" - 'RestSupTermPlus L1 T1 L2 T2 = (frsupp L1 T1 L2 T2). - -(* Basic eliminators ********************************************************) - -lemma frsupp_ind: ∀L1,T1. ∀R:relation2 lenv term. - (∀L2,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → R L2 T2) → - (∀L,T,L2,T2. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ → ⦃L, T⦄ ⧁ ⦃L2, T2⦄ → R L T → R L2 T2) → - ∀L2,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → R L2 T2. -#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H -@(bi_TC_ind … IH1 IH2 ? ? H) -qed-. - -lemma frsupp_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. - (∀L1,T1. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → R L1 T1) → - (∀L1,L,T1,T. ⦃L1, T1⦄ ⧁ ⦃L, T⦄ → ⦃L, T⦄ ⧁+ ⦃L2, T2⦄ → R L T → R L1 T1) → - ∀L1,T1. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → R L1 T1. -#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H -@(bi_TC_ind_dx … IH1 IH2 ? ? H) -qed-. - -(* Baic inversion lemmas ****************************************************) - -lemma frsupp_inv_dx: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ ∨ - ∃∃L,T. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ & ⦃L, T⦄ ⧁ ⦃L2, T2⦄. -/2 width=1 by bi_TC_decomp_r/ qed-. - -lemma frsupp_inv_sn: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ ∨ - ∃∃L,T. ⦃L1, T1⦄ ⧁ ⦃L, T⦄ & ⦃L, T⦄ ⧁+ ⦃L2, T2⦄. -/2 width=1 by bi_TC_decomp_l/ qed-. - -(* Basic properties *********************************************************) - -lemma frsup_frsupp: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄. -/2 width=1/ qed. - -lemma frsupp_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁+ ⦃L, T⦄ → ⦃L, T⦄ ⧁ ⦃L2, T2⦄ → - ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄. -/2 width=4/ qed. - -lemma frsupp_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⧁ ⦃L, T⦄ → ⦃L, T⦄ ⧁+ ⦃L2, T2⦄ → - ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄. -/2 width=4/ qed. - -(* Basic forward lemmas *****************************************************) - -lemma frsupp_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}. -#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2 -/3 width=3 by frsup_fwd_fw, transitive_lt/ -qed-. - -lemma frsupp_fwd_lw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{L1} ≤ ♯{L2}. -#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2 -/2 width=3 by frsup_fwd_lw/ (**) (* /3 width=5 by frsup_fwd_lw, transitive_le/ is too slow *) -#L #T #L2 #T2 #_ #HL2 #HL1 -lapply (frsup_fwd_lw … HL2) -HL2 /2 width=3 by transitive_le/ -qed-. - -lemma frsupp_fwd_tw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ♯{T2} < ♯{T1}. -#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2 -/3 width=3 by frsup_fwd_tw, transitive_lt/ -qed-. - -lemma frsupp_fwd_append: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⧁+ ⦃L2, T2⦄ → ∃L. L2 = L1 @@ L. -#L1 #L2 #T1 #T2 #H @(frsupp_ind … H) -L2 -T2 /2 width=3 by frsup_fwd_append/ -#L #T #L2 #T2 #_ #HL2 * #K1 #H destruct -elim (frsup_fwd_append … HL2) -HL2 #K2 #H destruct /2 width=2/ -qed-. - -(* Advanced forward lemmas **************************************************) - -lemma lift_frsupp_trans: ∀L,U1,K,U2. ⦃L, U1⦄ ⧁+ ⦃L @@ K, U2⦄ → - ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → - ∃T2. ⇧[d + |K|, e] T2 ≡ U2. -#L #U1 @(f2_ind … fw … L U1) -L -U1 #n #IH -#L #U1 #Hn #K #U2 #H #T1 #d #e #HTU1 destruct -elim (frsupp_inv_sn … H) -H /2 width=5 by lift_frsup_trans/ * -#L0 #U0 #HL0 #HL -elim (frsup_fwd_append … HL0) #K0 #H destruct -elim (frsupp_fwd_append … HL) #L0 >append_assoc #H -elim (append_inj_dx … H ?) -H // #_ #H destruct -(append_inv_refl_dx … (sym_eq … H1)) -H1 normalize /2 width=2/ -| /2 width=5 by lift_frsupp_trans/ -] -qed-. - -(* Advanced inversion lemmas for frsupp **************************************) - -lemma frsupp_inv_atom1_frsups: ∀J,L1,L2,T2. ⦃L1, ⓪{J}⦄ ⧁+ ⦃L2, T2⦄ → ⊥. -#J #L1 #L2 #T2 #H @(frsupp_ind … H) -L2 -T2 // -#L2 #T2 #H elim (frsup_inv_atom1 … H) -qed-. - -lemma frsupp_inv_bind1_frsups: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ ⧁+ ⦃L2, T2⦄ → - ⦃L1, W⦄ ⧁* ⦃L2, T2⦄ ∨ ⦃L1.ⓑ{J}W, U⦄ ⧁* ⦃L2, T2⦄. -#b #J #L1 #L2 #W #U #T2 #H @(frsupp_ind … H) -L2 -T2 -[ #L2 #T2 #H - elim (frsup_inv_bind1 … H) -H * #H1 #H2 destruct /2 width=1/ -| #L #T #L2 #T2 #_ #HT2 * /3 width=4/ -] -qed-. - -lemma frsupp_inv_flat1_frsups: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⧁+ ⦃L2, T2⦄ → - ⦃L1, W⦄ ⧁* ⦃L2, T2⦄ ∨ ⦃L1, U⦄ ⧁* ⦃L2, T2⦄. -#J #L1 #L2 #W #U #T2 #H @(frsupp_ind … H) -L2 -T2 -[ #L2 #T2 #H - elim (frsup_inv_flat1 … H) -H #H1 * #H2 destruct /2 width=1/ -| #L #T #L2 #T2 #_ #HT2 * /3 width=4/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/frsups_frsups.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/frsups_frsups.ma deleted file mode 100644 index e7b7de26e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/frsups_frsups.ma +++ /dev/null @@ -1,22 +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/unfold/frsups.ma". - -(* STAR-ITERATED RESTRICTED SUPCLOSURE **************************************) - -(* Main propertis ***********************************************************) - -theorem frsups_trans: bi_transitive … frsups. -/2 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp.ma new file mode 100644 index 000000000..f0fde0f1f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp.ma @@ -0,0 +1,60 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/fsup.ma". + +(* PLUS-ITERATED SUPCLOSURE *************************************************) + +definition fsupp: bi_relation lenv term ≝ bi_TC … fsup. + +interpretation "plus-iterated structural successor (closure)" + 'SupTermPlus L1 T1 L2 T2 = (fsupp L1 T1 L2 T2). + +(* Basic eliminators ********************************************************) + +lemma fsupp_ind: ∀L1,T1. ∀R:relation2 lenv term. + (∀L2,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → R L2 T2) → + (∀L,T,L2,T2. ⦃L1, T1⦄ ⊃+ ⦃L, T⦄ → ⦃L, T⦄ ⊃ ⦃L2, T2⦄ → R L T → R L2 T2) → + ∀L2,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → R L2 T2. +#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H +@(bi_TC_ind … IH1 IH2 ? ? H) +qed-. + +lemma fsupp_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. + (∀L1,T1. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → R L1 T1) → + (∀L1,L,T1,T. ⦃L1, T1⦄ ⊃ ⦃L, T⦄ → ⦃L, T⦄ ⊃+ ⦃L2, T2⦄ → R L T → R L1 T1) → + ∀L1,T1. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → R L1 T1. +#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H +@(bi_TC_ind_dx … IH1 IH2 ? ? H) +qed-. + +(* Basic properties *********************************************************) + +lemma fsup_fsupp: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄. +/2 width=1/ qed. + +lemma fsupp_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃+ ⦃L, T⦄ → ⦃L, T⦄ ⊃ ⦃L2, T2⦄ → + ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄. +/2 width=4/ qed. + +lemma fsupp_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃ ⦃L, T⦄ → ⦃L, T⦄ ⊃+ ⦃L2, T2⦄ → + ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄. +/2 width=4/ qed. + +(* Basic forward lemmas *****************************************************) + +lemma fsupp_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}. +#L1 #L2 #T1 #T2 #H @(fsupp_ind … H) -L2 -T2 +/3 width=3 by fsup_fwd_cw, transitive_lt/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp_fsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp_fsupp.ma new file mode 100644 index 000000000..a546fc265 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/fsupp_fsupp.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/fsupp.ma". + +(* PLUS-ITERATED SUPCLOSURE *************************************************) + +(* Main propertis ***********************************************************) + +theorem fsupp_trans: bi_transitive … fsupp. +/2 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss.ma new file mode 100644 index 000000000..3570a2d80 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss.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/unfold/cpss.ma". + +(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************) + +inductive lcpss: relation lenv ≝ +| lcpss_atom: lcpss (⋆) (⋆) +| lcpss_pair: ∀I,L1,L2,V1,V2. lcpss L1 L2 → L1 ⊢ V1 ▶* V2 → + lcpss (L1. ⓑ{I} V1) (L2. ⓑ{I} V2) +. + +interpretation "parallel unfold (local environment, sn variant)" + 'PSubstStarSn L1 L2 = (lcpss L1 L2). + +(* Basic inversion lemmas ***************************************************) + +fact lcpss_inv_atom1_aux: ∀L1,L2. L1 ⊢ ▶* L2 → L1 = ⋆ → L2 = ⋆. +#L1 #L2 * -L1 -L2 +[ // +| #I #L1 #L2 #V1 #V2 #_ #_ #H destruct +] +qed-. + +lemma lcpss_inv_atom1: ∀L2. ⋆ ⊢ ▶* L2 → L2 = ⋆. +/2 width=5 by lcpss_inv_atom1_aux/ qed-. + +fact lcpss_inv_pair1_aux: ∀L1,L2. L1 ⊢ ▶* L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → + ∃∃K2,V2. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L2 = K2. ⓑ{I} V2. +#L1 #L2 * -L1 -L2 +[ #I #K1 #V1 #H destruct +| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #J #K1 #W1 #H destruct /2 width=5/ +] +qed-. + +lemma lcpss_inv_pair1: ∀I,K1,V1,L2. K1. ⓑ{I} V1 ⊢ ▶* L2 → + ∃∃K2,V2. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L2 = K2. ⓑ{I} V2. +/2 width=5 by lcpss_inv_pair1_aux/ qed-. + +fact lcpss_inv_atom2_aux: ∀L1,L2. L1 ⊢ ▶* L2 → L2 = ⋆ → L1 = ⋆. +#L1 #L2 * -L1 -L2 +[ // +| #I #L1 #L2 #V1 #V2 #_ #_ #H destruct +] +qed-. + +lemma lcpss_inv_atom2: ∀L1. L1 ⊢ ▶* ⋆ → L1 = ⋆. +/2 width=5 by lcpss_inv_atom2_aux/ qed-. + +fact lcpss_inv_pair2_aux: ∀L1,L2. L1 ⊢ ▶* L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → + ∃∃K1,V1. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L1 = K1. ⓑ{I} V1. +#L1 #L2 * -L1 -L2 +[ #I #K1 #V1 #H destruct +| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #J #K2 #W2 #H destruct /2 width=5/ +] +qed-. + +lemma lcpss_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ▶* K2. ⓑ{I} V2 → + ∃∃K1,V1. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L1 = K1. ⓑ{I} V1. +/2 width=5 by lcpss_inv_pair2_aux/ qed-. + +(* Basic properties *********************************************************) + +lemma lcpss_refl: ∀L. L ⊢ ▶* L. +#L elim L -L // /2 width=1/ +qed. + +lemma lcpss_append: ∀K1,K2. K1 ⊢ ▶* K2 → ∀L1,L2. L1 ⊢ ▶* L2 → + L1 @@ K1 ⊢ ▶* L2 @@ K2. +#K1 #K2 #H elim H -K1 -K2 // /3 width=1/ +qed. + +(* Basic forward lemmas *****************************************************) + +lemma lcpss_fwd_length: ∀L1,L2. L1 ⊢ ▶* L2 → |L1| = |L2|. +#L1 #L2 #H elim H -L1 -L2 normalize // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_cpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_cpss.ma new file mode 100644 index 000000000..aee1d7fcb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_cpss.ma @@ -0,0 +1,145 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/fsup.ma". +include "basic_2/unfold/lcpss_ldrop.ma". + +(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************) + +(* Main properties on context-sensitive parallel unfold for terms ***********) + +fact cpss_conf_lcpss_aux: ∀L0,i. ( + ∀L,T0.♯{L, T0} < ♯{L0, #i} → + ∀T1. L ⊢ T0 ▶* T1 → ∀T2. L ⊢ T0 ▶* T2 → + ∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 → + ∃∃T. L1 ⊢ T1 ▶* T & L2 ⊢ T2 ▶* T + ) → + ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 → + ∀V2. K0 ⊢ V0 ▶* V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 → + ∀L1. L0 ⊢ ▶* L1 → ∀L2. L0 ⊢ ▶* L2 → + ∃∃T. L1 ⊢ #i ▶* T & L2 ⊢ T2 ▶* T. +#L0 #i #IH #K0 #V0 #HLK0 #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02 +elim (lcpss_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1 +elim (lcpss_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct +elim (lcpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 +elim (lcpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct +lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 +lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 +elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 +elim (lift_total V 0 (i+1)) #T #HVT +lapply (cpss_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/ +qed-. + +theorem cpss_conf_lcpss: ∀L0,T0,T1. L0 ⊢ T0 ▶* T1 → ∀T2. L0 ⊢ T0 ▶* T2 → + ∀L1. L0 ⊢ ▶* L1 → ∀L2. L0 ⊢ ▶* L2 → + ∃∃T. L1 ⊢ T1 ▶* T & L2 ⊢ T2 ▶* T. +#L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*] +[ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct + elim (cpss_inv_atom1 … H1) -H1 + elim (cpss_inv_atom1 … H2) -H2 + [ #H2 #H1 destruct /2 width=3/ + | * #K0 #V0 #V2 #i2 #HLK0 #HV02 #HVT2 #H2 #H1 destruct + /3 width=10 by cpss_conf_lcpss_aux/ + | #H2 * #K0 #V0 #V1 #i1 #HLK0 #HV01 #HVT1 #H1 destruct + /4 width=10 by ex2_commute, cpss_conf_lcpss_aux/ + | * #X #Y #V2 #z #H #HV02 #HVT2 #H2 + * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct + lapply (ldrop_mono … H … HLK0) -H #H destruct + elim (lcpss_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1 + elim (lcpss_inv_pair1 … H1) -H1 #K1 #W1 #HK01 #_ #H destruct + lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1 + elim (lcpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 + elim (lcpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 + lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0 + elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 + elim (lift_total V 0 (i+1)) #T #HVT + lapply (cpss_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1 + lapply (cpss_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 -V /2 width=3/ + ] +| #a #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct + elim (cpss_inv_bind1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct + elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct + elim (IH … HV01 … HV02 … HL01 … HL02) // + elim (IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -IH // /2 width=1/ /3 width=5/ +| #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct + elim (cpss_inv_flat1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct + elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct + elim (IH … HV01 … HV02 … HL01 … HL02) // + elim (IH … HT01 … HT02 … HL01 … HL02) // /3 width=5/ +] +qed-. + +theorem cpss_conf: ∀L. confluent … (cpss L). +/2 width=6 by cpss_conf_lcpss/ qed-. + +theorem cpss_trans_lcpss: ∀L1,T1,T. L1 ⊢ T1 ▶* T → ∀L2. L1 ⊢ ▶* L2 → + ∀T2. L2 ⊢ T ▶* T2 → L1 ⊢ T1 ▶* T2. +#L1 #T1 @(f2_ind … fw … L1 T1) -L1 -T1 #n #IH #L1 * [|*] +[ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct + elim (cpss_inv_atom1 … H1) -H1 + [ #H destruct + elim (cpss_inv_atom1 … HT2) -HT2 + [ #H destruct // + | * #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct + elim (lcpss_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H + elim (lcpss_inv_pair2 … H) -H #K1 #V1 #HK12 #HV1 #H destruct + lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/ + ] + | * #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct + elim (lcpss_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 + elim (lcpss_inv_pair1 … H) -H #K2 #W2 #HK12 #_ #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 + elim (cpss_inv_lift1 … HT2 … HLK2 … HVT) -L2 -T + lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/ + ] +| #a #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2 + elim (cpss_inv_bind1 … H1) -H1 #V #T #HV1 #HT1 #H destruct + elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/ +| #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2 + elim (cpss_inv_flat1 … H1) -H1 #V #T #HV1 #HT1 #H destruct + elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/ +] +qed-. + +theorem cpss_trans: ∀L. Transitive … (cpss L). +/2 width=5 by cpss_trans_lcpss/ qed-. + +(* Properties on context-sensitive parallel unfold for terms ****************) + +lemma lcpss_cpss_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ▶* T1 → ∀L1. L0 ⊢ ▶* L1 → + ∃∃T. L1 ⊢ T0 ▶* T & L1 ⊢ T1 ▶* T. +#L0 #T0 #T1 #HT01 #L1 #HL01 +elim (cpss_conf_lcpss … HT01 T0 … HL01 … HL01) // -L0 /2 width=3/ +qed-. + +lemma lcpss_cpss_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ▶* T1 → ∀L1. L0 ⊢ ▶* L1 → + ∃∃T. L1 ⊢ T0 ▶* T & L0 ⊢ T1 ▶* T. +#L0 #T0 #T1 #HT01 #L1 #HL01 +elim (cpss_conf_lcpss … HT01 T0 … L0 … HL01) // -HT01 -HL01 /2 width=3/ +qed-. + +lemma lcpss_cpss_trans: ∀L1,L2. L1 ⊢ ▶* L2 → + ∀T1,T2. L2 ⊢ T1 ▶* T2 → L1 ⊢ T1 ▶* T2. +/2 width=5 by cpss_trans_lcpss/ qed-. + +lemma fsup_cpss_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶* U2 → + ∃∃L,U1. L1 ⊢ ▶* L & L ⊢ T1 ▶* U1 & ⦃L, U1⦄ ⊃ ⦃L2, U2⦄. +#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ] +#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2 +elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2 +elim (lift_total T d e) #U #HTU +elim (ldrop_lcpss_trans … HLK1 … HK1) -HLK1 -HK1 #L2 #HL12 #HL2K +lapply (cpss_lift … HT1 … HL2K … HTU1 … HTU) -HT1 -HTU1 /3 width=11/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_lcpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_lcpss.ma new file mode 100644 index 000000000..5397ca3a4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss_lcpss.ma @@ -0,0 +1,55 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/lcpss_cpss.ma". + +(* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************) + +(* Main properties **********************************************************) + +theorem lcpss_conf: confluent … lcpss. +#L0 @(f_ind … length … L0) -L0 #n #IH * +[ #_ #X1 #H1 #X2 #H2 -n + >(lcpss_inv_atom1 … H1) -X1 + >(lcpss_inv_atom1 … H2) -X2 /2 width=3/ +| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct + elim (lcpss_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct + elim (lcpss_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct + elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2 + elim (cpss_conf_lcpss … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/ +] +qed-. + +theorem lcpss_trans: Transitive … lcpss. +#L1 #L #H elim H -L1 -L // +#I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H +elim (lcpss_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct +lapply (cpss_trans_lcpss … HV1 … HL1 … HV2) -V -HL1 /3 width=1/ +qed-. + +(* Advanced forward lemmas **************************************************) + +lemma cpss_fwd_shift1: ∀L1,L,T1,T. L ⊢ L1 @@ T1 ▶* T → + ∃∃L2,T2. L @@ L1 ⊢ ▶* L @@ L2 & L @@ L1 ⊢ T1 ▶* T2 & + T = L2 @@ T2. +#L1 @(lenv_ind_dx … L1) -L1 +[ #L #T1 #T #HT1 + @ex3_2_intro [3: // |4,5: // |1,2: skip ] (**) (* /2 width=4/ does not work *) +| #I #L1 #V1 #IH #L #T1 #T >shift_append_assoc #H (lcpss_inv_atom2 … H) -H /2 width=3/ +| #K2 #I #V2 #X #H + elim (lcpss_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/ +| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_ + elim (lcpss_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct + elim (IHLK2 … HL12 ?) -L2 // /3 width=3/ +| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_ + >commutative_plus normalize #H destruct +] +qed-. + +lemma lcpss_ldrop_trans_O1: dropable_dx lcpss. +/2 width=5 by lcpss_ldrop_trans_O1_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx.ma index 1beef1bb7..753c948cc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx.ma @@ -12,6 +12,10 @@ (* *) (**************************************************************************) +notation "hvbox( T1 break ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PSubstStar $T1 $d $e $T2 }. + include "basic_2/unfold/tpss.ma". (* DX PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************) @@ -208,7 +212,7 @@ lemma ltpss_dx_weak: ∀L1,L2,d1,e1. L1 ▶* [d1, e1] L2 → ] qed. -lemma ltpss_dx_weak_all: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → L1 ▶* [0, |L2|] L2. +lemma ltpss_dx_weak_full: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → L1 ▶* [0, |L2|] L2. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e // /3 width=2/ /3 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ldrop.ma index 4aa2f573e..0b6c504c2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_ldrop.ma @@ -12,10 +12,14 @@ (* *) (**************************************************************************) +include "basic_2/substitution/fsup.ma". +include "basic_2/unfold/tpss_lift.ma". include "basic_2/unfold/ltpss_dx.ma". (* DX PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************) +(* Properies on local environment slicing ***********************************) + lemma ltpss_dx_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 → ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2. @@ -129,3 +133,98 @@ lemma ltpss_dx_ldrop_trans_le: ∀L1,L0,d1,e1. L1 ▶* [d1, e1] L0 → ] ] qed. + +lemma ldrop_ltpss_dx_trans_le: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 → + ∀K2,d2,e2. K1 ▶* [d2, e2] K2 → d1 ≤ d2 → + ∃∃L2. L1 ▶* [d2 + e1, e2] L2 & ⇩[d1, e1] L2 ≡ K2. +#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1 +[ #d1 #e1 #K2 #d2 #e2 #H #_ + >(ltpss_dx_inv_atom1 … H) -H /2 width=3/ +| /2 width=3/ +| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #Hd + elim (IHLK1 … HK12 Hd) -K1 -Hd /3 width=5/ +| #L1 #K1 #I #V1 #W1 #d1 #e1 #_ #HWV1 #IHLK1 #X #d2 #e2 #H #Hd12 + elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hd2 + elim (ltpss_dx_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct + elim (IHLK1 … HK12 … Hd12) -IHLK1 -HK12 (ltpss_dx_inv_atom1 … H) -H /2 width=3/ +| #K1 #I #V1 #K2 #d2 #e2 #HK12 #H #_ + lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3/ +| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H1 #H2 + elim (IHLK1 … HK12 H1 H2) -K1 -H2 + lapply (le_n_O_to_eq … H1) -H1 #H destruct /3 width=5/ +| #L1 #K1 #I #V1 #W1 #d1 #e1 #_ #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21 #Hd12 + elim (eq_or_gt d2) #Hd2 [ -Hd21 elim (eq_or_gt e2) #He2 ] destruct + [ lapply (le_n_O_to_eq … Hd12) -Hd12 plus_minus_commutative // #L2 #HL12 #HLK2 + elim (lift_total W2 d1 e1) #V2 #HWV2 + lapply (tpss_lift_be … HW12 … HLK2 HWV1 … HWV2) -W1 // /2 width=1/ + >plus_minus // >commutative_plus /4 width=5/ + | elim (ltpss_dx_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct + elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // ] /2 width=1/ #L2 #HL12 #HLK2 + elim (lift_total W2 d1 e1) #V2 #HWV2 + lapply (tpss_lift_be … HW12 … HLK2 HWV1 … HWV2) -W1 [ >plus_minus // ] /2 width=1/ + >commutative_plus /3 width=5/ + ] +] +qed-. + +lemma ldrop_ltpss_dx_trans_ge: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 → + ∀K2,d2,e2. K1 ▶* [d2, e2] K2 → d2 + e2 ≤ d1 → + ∃∃L2. L1 ▶* [d2, e2] L2 & ⇩[d1, e1] L2 ≡ K2. +#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1 +[ #d1 #e1 #K2 #d2 #e2 #H #_ + >(ltpss_dx_inv_atom1 … H) -H /2 width=3/ +| #K1 #I #V1 #K2 #d2 #e2 #HK12 #H + elim (plus_le_0 … H) -H #H1 #H2 destruct /2 width=3/ +| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H + elim (IHLK1 … HK12 H) -K1 + elim (plus_le_0 … H) -H #H1 #H2 destruct #L2 #HL12 + >(ltpss_dx_inv_refl_O2 … HL12) -L1 /3 width=5/ +| #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21 + elim (eq_or_gt d2) #Hd2 [ elim (eq_or_gt e2) #He2 ] destruct + [ -IHLK1 -Hd21 <(ltpss_dx_inv_refl_O2 … H) -X /3 width=5/ + | elim (ltpss_dx_inv_tpss21 … H He2) -H #K2 #W2 #HK12 #HW12 #H destruct + elim (IHLK1 … HK12 …) -IHLK1 /2 width=1/ #L2 #HL12 #HLK2 + elim (lift_total W2 d1 e1) #V2 #HWV2 + lapply (tpss_lift_le … HW12 … HLK2 HWV1 … HWV2) -W1 /2 width=1/ /3 width=5/ + | elim (ltpss_dx_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct + elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // /2 width=1/ ] #L2 #HL12 #HLK2 + elim (lift_total W2 d1 e1) #V2 #HWV2 + lapply (tpss_lift_le … HW12 … HLK2 HWV1 … HWV2) -W1 [ >plus_minus // /2 width=1/ ] /3 width=5/ + ] +] +qed-. + +(* Properties on supclosure *************************************************) + +lemma fsup_tps_trans_full: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶[0,|L2|] U2 → + ∃∃L,U1. L1 ▶*[0,|L|] L & L ⊢ T1 ▶[0,|L|] U1 & ⦃L, U1⦄ ⊃ ⦃L2, T2⦄. +#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ] +#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2 +elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2 +elim (lift_total T d e) #U #HTU +elim (le_or_ge d (|K|)) #Hd +[ elim (ldrop_ltpss_dx_trans_be … HLK1 … HK1 … Hd) // -HLK1 -HK1 #L2 #HL12 #HL2K + lapply (tps_lift_be … HT1 … HL2K … HTU1 HTU … Hd) // -HT1 -HTU1 #HU1 +| elim (ldrop_ltpss_dx_trans_ge … HLK1 … HK1 Hd) -HLK1 -HK1 #L2 #HL12 #HL2K + lapply (tps_lift_le … HT1 … HL2K … HTU1 HTU Hd) -HT1 -HTU1 #HU1 +] +lapply (ltpss_dx_weak_full … HL12) -HL12 #HL12 +lapply (tps_weak_full … HU1) -HU1 #HU1 +@(ex3_2_intro … L2 U) // /2 width=7/ (**) (* explicit constructor: auto /3 width=14/ too slow *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tpss.ma index 04af50c8c..9c7875927 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tpss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx_tpss.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/unfold/tpss_lift.ma". include "basic_2/unfold/ltpss_dx_tps.ma". (* DX PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn.ma index e09cf12c5..577c1506d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn.ma @@ -12,6 +12,10 @@ (* *) (**************************************************************************) +notation "hvbox( T1 break ⊢ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PSubstStarSn $T1 $d $e $T2 }. + include "basic_2/unfold/tpss.ma". (* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************) @@ -206,7 +210,7 @@ lemma ltpss_sn_weak: ∀L1,L2,d1,e1. L1 ⊢ ▶* [d1, e1] L2 → ] qed. -lemma ltpss_sn_weak_all: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → L1 ⊢ ▶* [0, |L1|] L2. +lemma ltpss_sn_weak_full: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → L1 ⊢ ▶* [0, |L1|] L2. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e // /3 width=2/ /3 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma index 8b414d203..d2cdba023 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_alt.ma @@ -12,6 +12,10 @@ (* *) (**************************************************************************) +notation "hvbox( T1 break ⊢ ▶ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PSubstStarSnAlt $T1 $d $e $T2 }. + include "basic_2/unfold/ltpss_dx_ltpss_dx.ma". include "basic_2/unfold/ltpss_sn_ltpss_sn.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma index bc4d73f3e..70167dfdd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma @@ -12,11 +12,14 @@ (* *) (**************************************************************************) +include "basic_2/substitution/fsup.ma". include "basic_2/unfold/tpss_lift.ma". include "basic_2/unfold/ltpss_sn.ma". (* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************) +(* Properies on local environment slicing ***********************************) + lemma ltpss_sn_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 → ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2. @@ -131,6 +134,25 @@ lemma ltpss_sn_ldrop_trans_le: ∀L1,L0,d1,e1. L1 ⊢ ▶* [d1, e1] L0 → ] qed. +lemma ldrop_ltpss_sn_trans_le: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 → + ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 → d1 ≤ d2 → + ∃∃L2. L1 ⊢ ▶* [d2 + e1, e2] L2 & ⇩[d1, e1] L2 ≡ K2. +#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1 +[ #d1 #e1 #K2 #d2 #e2 #H #_ + >(ltpss_sn_inv_atom1 … H) -H /2 width=3/ +| /2 width=3/ +| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #Hd + elim (IHLK1 … HK12 Hd) -K1 -Hd /3 width=5/ +| #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd12 + elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hd2 + elim (ltpss_sn_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct + elim (IHLK1 … HK12 … Hd12) -IHLK1 -HK12 H in HK1; -H #HK1 +elim (le_or_ge d (|K|)) #Hd +[ elim (ldrop_ltpss_sn_trans_be … HLK1 … HK1 … Hd) // -HLK1 -HK1 #L2 #HL12 #HL2K + lapply (tpss_lift_be … HT1 … Hd HL2K HTU1 … HTU) // -HT1 -HTU1 #HU1 +| elim (ldrop_ltpss_sn_trans_ge … HLK1 … HK1 Hd) -HLK1 -HK1 #L2 #HL12 #HL2K + lapply (tpss_lift_le … HT1 … Hd HL2K HTU1 … HTU) -HT1 -HTU1 #HU1 +] +lapply (ltpss_sn_weak_full … HL12) -HL12 #HL12 +lapply (tpss_weak_full … HU1) -HU1 #HU1 +@(ex3_2_intro … L2 U) // /2 width=7/ (**) (* explicit constructor: auto /3 width=14/ too slow *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma index 1fdae13f4..433718803 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma @@ -12,6 +12,10 @@ (* *) (**************************************************************************) +notation "hvbox( L ⊢ break term 46 T1 break ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PSubstStar $L $T1 $d $e $T2 }. + include "basic_2/substitution/tps.ma". (* PARTIAL UNFOLD ON TERMS **************************************************) @@ -104,8 +108,8 @@ lemma tpss_weak_top: ∀L,T1,T2,d,e. ] qed. -lemma tpss_weak_all: ∀L,T1,T2,d,e. - L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ▶* [0, |L|] T2. +lemma tpss_weak_full: ∀L,T1,T2,d,e. + L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ▶* [0, |L|] T2. #L #T1 #T2 #d #e #HT12 lapply (tpss_weak … HT12 0 (d + e) ? ?) -HT12 // #HT12 lapply (tpss_weak_top … HT12) // diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma index 6fe188a7c..f7670eaa8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma @@ -12,6 +12,10 @@ (* *) (**************************************************************************) +notation "hvbox( L ⊢ break term 46 T1 break ▶ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }. + include "basic_2/unfold/tpss_lift.ma". (* PARALLEL UNFOLD ON TERMS *************************************************) 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 2b88582a7..b1f440f2e 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 @@ -154,8 +154,8 @@ table { } ] [ { "context-free reduction" * } { - [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" + "ltpr_tps" + "ltpr_ltpss_dx" + "ltpr_ltpss_sn" + "ltpr_aaa" + "ltpr_ltpr" * ] - [ "tpr ( ? ➡ ? )" "tpr_lift" + "tpr_tps" + "tpr_tpss" + "tpr_delift" + "tpr_tpr" * ] + [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" + "ltpr_tps" + "ltpr_tpss" + "ltpr_ltpss_dx" + "ltpr_ltpss_sn" + "ltpr_aaa" + "ltpr_ltpr" * ] + [ "tpr ( ? ➡ ? )" "tpr_lift" + "tpr_delift" + "tpr_tpr" * ] } ] } @@ -198,19 +198,23 @@ table { [ "delift ( ? ⊢ ? ▼*[?,?] ≡ ? )" "delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )" "delift_lift" + "delift_tpss" + "delift_ltpss" + "delift_delift" * ] } ] - [ { "partial unfold" * } { + [ { "revised parallel substitution" * } { + [ "lcpss ( ? ⊢ ▶* ? )" "lcpss_ldrop" + "lcpss_cpss" + "lcpss_lcpss" * ] + [ "cpss ( ? ⊢ ? ▶* ? )" "cpss_lift" * ] + } + ] + [ { "partial unfold" * } { [ "ltpss_sn ( ? ⊢ ▶*[?,?] ? )" "ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )" "ltpss_sn_ldrop" + "ltpss_sn_tps" + "ltpss_sn_tpss" + "ltpss_sn_ltpss_sn" * ] [ "ltpss_dx ( ? ▶*[?,?] ? )" "ltpss_dx_ldrop" + "ltpss_dx_tps" + "ltpss_dx_tpss" + "ltpss_dx_ltpss_dx" * ] [ "tpss ( ? ⊢ ? ▶*[?,?] ? )" "tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )" "tpss_lift" "tpss_tpss" * ] } ] - [ { "generic local env. slicing" * } { - [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ] + [ { "iterated structural successor for closures" * } { + [ "fsupp ( ⦃?,?⦄ ⊃+ ⦃?,?⦄ )" "fsupp_fsupp" * ] } ] - [ { "iterated restricted structural predecessor for closures" * } { - [ "frsups ( ⦃?,?⦄ ⧁* ⦃?,?⦄ )" "frsups_frsups" * ] - [ "frsupp ( ⦃?,?⦄ ⧁+ ⦃?,?⦄ )" "frsupp_frsupp" * ] + [ { "generic local env. slicing" * } { + [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ] } ] [ { "generic term relocation" * } { @@ -230,6 +234,10 @@ table { [ "tps ( ? ⊢ ? ▶[?,?] ? )" "tps_lift" + "tps_tps" * ] } ] + [ { "structural successor for closures" * } { + [ "fsup ( ⦃?,?⦄ ⊃ ⦃?,?⦄ )" * ] + } + ] [ { "global env. slicing" * } { [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ] } @@ -242,10 +250,6 @@ table { [ "lsubr ( ? ⊑[?,?] ? )" "(lsubr_lsubr)" "lsubr_lbotr ( ⊒[?,?] ? )" * ] } ] - [ { "restricted structural predecessor for closures" * } { - [ "frsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ )" * ] - } - ] [ { "basic term relocation" * } { [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ] [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ]