From: Ferruccio Guidi Date: Wed, 7 Nov 2012 16:18:41 +0000 (+0000) Subject: - predefined_virtuals: nwe characters X-Git-Tag: make_still_working~1485 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=53f874fba5b9c39a788085515a4fefe5d29281da;p=helm.git - predefined_virtuals: nwe characters - lib: some additions - lambda_delta: commit of the components gramma, substitution, unfold - we parked the support for the "bt-reduction" - some renaming ... --- diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup.etc new file mode 100644 index 000000000..dcfe086e9 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup.etc @@ -0,0 +1,157 @@ +(**************************************************************************) +(* ___ *) +(* ||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/ +#I #L1 #K1 #V1 #i #HLK1 +lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /3 width=2/ +qed-. + +(* Advanced forward lemmas **************************************************) + +lemma lift_csup_trans_eq: ∀T1,U1,d,e. ⇧[d, e] T1 ≡ U1 → + ∀L,U2. ⦃L, U1⦄ > ⦃L, U2⦄ → + ∃T2. ⇧[d, e] T2 ≡ U2. +#T1 #U1 #d #e * -T1 -U1 -d -e +[5: #a #I #V1 #W1 #T1 #U1 #d #e #HVW1 #_ #L #X #H + elim (csup_inv_bind1 … H) -H * + [ #_ #H destruct /2 width=2/ + | #H elim (discr_lpair_x_xy … H) + ] +|6: #I #V1 #W1 #T1 #U1 #d #e #HVW1 #HUT1 #L #X #H + elim (csup_inv_flat1 … H) -H #_ * #H destruct /2 width=2/ +] +#i #d #e [2,3: #_ ] #L #X #H +elim (csup_inv_atom1 … H) -H #I #j #HL #H destruct +lapply (ldrop_pair2_fwd_cw … HL X) -HL #H +elim (lt_refl_false … H) +qed-. +(* +lemma lift_csup_trans_gt: ∀L1,L2,U1,U2. ⦃L1, U1⦄ > ⦃L2, U2⦄ → + ⇩[0, 1] L2 ≡ L1 → ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → + ∃T2. ⇧[d + 1, e] T2 ≡ U2. +#L1 #L2 #U1 #U2 * -L1 -L2 -U1 -U2 +[ #I #L1 #K1 #V #i #HLK1 #HKL1 + lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1 + lapply (ldrop_fwd_lw … HKL1) -HKL1 #HKL1 + lapply (transitive_le … HLK1 HKL1) -L1 normalize #H + + +| #a +| #a +] +#I #L1 #W1 #U1 #HL1 + + + + #X #d #e #H + lapply (ldrop_inv_refl … HL1) -HL1 +| #a #I #L1 #W1 #U1 #j #HL1 #X #d #e #H + lapply (ldrop_inv_ldrop1 … HL1) + + elim (lift_inv_bind2 … H) -H #W2 #U2 #HW21 #HU21 #H destruct + + + /3 width=2/ /4 width=2/ + +*) + + + +(* Advanced inversion lemmas ************************************************) + +lemma csup_inv_lref2_be: ∀L,U,i. ⦃L, U⦄ > ⦃L, #i⦄ → + ∀T,d,e. ⇧[d, e] T ≡ U → d ≤ i → i < d + e → ⊥. +#L #U #i #H #T #d #e #HTU #Hdi #Hide +elim (lift_csup_trans_eq … HTU … H) -H -T #T #H +elim (lift_inv_lref2_be … H ? ?) // +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup_csup.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup_csup.etc new file mode 100644 index 000000000..813cb969d --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csup_csup.etc @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||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/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⦄ → + ∀T3. ⦃L0, T2⦄ > ⦃L, T3⦄ → + L = L0 ∨ ⦃L, T1⦄ > ⦃L, T3⦄. +#L #L0 #T1 #T2 * -L -L0 -T1 -T2 /2 width=1/ +[ #I #L0 #K0 #V0 #i #HLK0 #T3 #H + lapply (ldrop_pair2_fwd_cw … HLK0 T3) -HLK0 #H1 + lapply (csup_fwd_cw … H) -H #H2 + lapply (transitive_lt … H1 H2) -H1 -H2 #H + elim (lt_refl_false … H) +| #a #I #L0 #V2 #T2 #T3 #HT23 + elim (csup_inv_ldrop … HT23 I V2 0 ?) -HT23 // #H1 #H2 destruct /2 width=1/ + qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csupp.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csupp.etc new file mode 100644 index 000000000..c28eaea73 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csupp.etc @@ -0,0 +1,64 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lambda_delta/basic_2/etc/csup/csupp_csupp.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csupp_csupp.etc new file mode 100644 index 000000000..5afdb68d4 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csupp_csupp.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/csupp.ma". + +(* PLUS-ITERATED SUPCLOSURE *************************************************) + +(* Main propertis ***********************************************************) + +theorem csupp_trans: bi_transitive … csupp. +/2 width=4/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups.etc new file mode 100644 index 000000000..7f5879426 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups.etc @@ -0,0 +1,107 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lambda_delta/basic_2/etc/csup/csups_csups.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups_csups.etc new file mode 100644 index 000000000..aa54d9bef --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/csups_csups.etc @@ -0,0 +1,62 @@ +(**************************************************************************) +(* ___ *) +(* ||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/csup_csup.ma". +include "basic_2/unfold/csups.ma". + +(* STAR-ITERATED SUPCLOSURE *************************************************) + +(* Advanced forward lemmas **************************************************) + +(* +lemma csupp_strap2_fwd_refl: ∀L,L0,T1,T2. ⦃L, T1⦄ > ⦃L0, T2⦄ → + ∀T3. ⦃L0, T2⦄ >+ ⦃L, T3⦄ → + L = L0 ∨ ⦃L, T1⦄ >+ ⦃L, T3⦄. +#L #L0 #T1 #T2 * -L -L0 -T1 -T2 /2 width=1/ +[ #I #L0 #K0 #V0 #i #HLK0 #T3 #H + lapply (ldrop_pair2_fwd_cw … HLK0 T3) -HLK0 #H1 + lapply (csupp_fwd_cw … H) -H #H2 + lapply (transitive_lt … H1 H2) -H1 -H2 #H + elim (lt_refl_false … H) +| #a #I #L0 #V2 #T2 #T3 #HT23 + /3 width=5/ + + elim (csup_inv_ldrop … HT23 I V2 0 ?) -HT23 // #H1 #H2 destruct /2 width=1/ + qed-. + + + + + + + + +lemma csups_strap1_fwd_refl: ∀L,L0,T1,T2. ⦃L, T1⦄ >* ⦃L0, T2⦄ → + ∀T3. ⦃L0, T2⦄ > ⦃L, T3⦄ → L = L0. +#L #L0 #T1 #T2 #H @(csups_ind_dx … H) -L -T1 // +#L1 #L #T1 #T #HL1 #_ #IHL0 #T3 #HL0 +lapply (csup_trans_fwd_refl … HL10) … HL0) -T2 +*) +lemma lift_csups_trans_aux: ∀T1,U1,d,e. ⇧[d, e] T1 ≡ U1 → + ∀L1,L2,U2. ⦃L1, U1⦄ >* ⦃L2, U2⦄ → L1 = L2 → + ∃T2. ⇧[d, e] T2 ≡ U2. +#T1 #U1 #d #e #HTU1 #L1 #L2 #U2 #H @(csups_ind … H) -L2 -U2 /2 width=2/ -T1 +#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/lambda_delta/basic_2/etc/csup/ypr.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ypr.etc new file mode 100644 index 000000000..f1510ab7e --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ypr.etc @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||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( h ⊢ break ⦃ L1, break T1 ⦄ • ⥸ break [ g ] break ⦃ L2 , break T2 ⦄ )" + non associative with precedence 45 + for @{ 'YPRed $h $g $L1 $T1 $L2 $T2 }. + +include "basic_2/substitution/csup.ma". +include "basic_2/reducibility/xpr.ma". + +(* HYPER PARALLEL REDUCTION ON CLOSURES *************************************) + +inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝ +| ypr_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → ypr h g L1 T1 L1 T2 +| ypr_ssta: ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g, l + 1] T2 → ypr h g L1 T1 L1 T2 +| ypr_csup: ∀L2,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → ypr h g L1 T1 L2 T2 +. + +interpretation + "hyper parallel reduction (closure)" + 'YPRed h g L1 T1 L2 T2 = (ypr h g L1 T1 L2 T2). + +(* Basic properties *********************************************************) + +lemma ypr_refl: ∀h,g. bi_reflexive … (ypr h g). +/2 width=1/ qed. + +lemma xpr_ypr: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •➡[g] T2 → h ⊢ ⦃L, T1⦄ •⥸[g] ⦃L, T2⦄. +#h #g #L #T1 #T2 * /2 width=1/ /2 width=2/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs.etc new file mode 100644 index 000000000..86dc0c135 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs.etc @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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( h ⊢ break ⦃ L1, break T1 ⦄ • ⥸ * break [ g ] break ⦃ L2 , break T2 ⦄ )" + non associative with precedence 45 + for @{ 'YPRedStar $h $g $L1 $T1 $L2 $T2 }. + +include "basic_2/reducibility/ypr.ma". + +(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************) + +definition yprs: ∀h. sd h → bi_relation lenv term ≝ + λh,g. bi_TC … (ypr h g). + +interpretation "hyper parallel computation (closure)" + 'YPRedStar h g L1 T1 L2 T2 = (yprs h g L1 T1 L2 T2). + +(* Basic eliminators ********************************************************) + +lemma yprs_ind: ∀h,g,L1,T1. ∀R:relation2 lenv term. R L1 T1 → + (∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ •⥸[g] ⦃L2, T2⦄ → R L T → R L2 T2) → + ∀L2,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → R L2 T2. +/3 width=7 by bi_TC_star_ind/ qed-. + +lemma yprs_ind_dx: ∀h,g,L2,T2. ∀R:relation2 lenv term. R L2 T2 → + (∀L1,L,T1,T. h ⊢ ⦃L1, T1⦄ •⥸[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ •⥸*[g] ⦃L2, T2⦄ → R L T → R L1 T1) → + ∀L1,T1. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → R L1 T1. +/3 width=7 by bi_TC_star_ind_dx/ qed-. + +(* Basic properties *********************************************************) + +lemma yprs_refl: ∀h,g. bi_reflexive … (yprs h g). +/2 width=1/ qed. + +lemma yprs_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L, T⦄ → + h ⊢ ⦃L, T⦄ •⥸[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄. +/2 width=4/ qed. + +lemma yprs_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ •⥸[g] ⦃L, T⦄ → + h ⊢ ⦃L, T⦄ •⥸*[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄. +/2 width=4/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_csups.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_csups.etc new file mode 100644 index 000000000..08c939d8d --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_csups.etc @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/unfold/csups.ma". +include "basic_2/computation/yprs.ma". + +(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************) + +(* Properties on iterated supclosure ****************************************) + +lemma csups_yprs: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → + h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄. +#h #g #L1 #L2 #T1 #T2 #H @(csups_ind … H) -L2 -T2 /3 width=1/ /3 width=4/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_xprs.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_xprs.etc new file mode 100644 index 000000000..2feb88a2f --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_xprs.etc @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/xprs_cprs.ma". +include "basic_2/computation/yprs.ma". + +(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************) + +(* Properties on extended parallel computation for terms ********************) + +lemma xprs_yprs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •➡*[g] T2 → + h ⊢ ⦃L, T1⦄ •⥸*[g] ⦃L, T2⦄. +#h #g #L #T1 #T2 #H @(xprs_ind … H) -T2 // /3 width=4/ +qed. + +lemma cprs_yprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → h ⊢ ⦃L, T1⦄ •⥸*[g] ⦃L, T2⦄. +/3 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_yprs.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_yprs.etc new file mode 100644 index 000000000..d737dd817 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/yprs_yprs.etc @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/yprs.ma". + +(* HYPER PARALLEL COMPUTATION ON TERMS **************************************) + +theorem yprs_trans: ∀h,g. bi_transitive … (yprs h g). +/2 width=4/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps.etc new file mode 100644 index 000000000..149e7895b --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps.etc @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||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( h ⊢ break ⦃ L1, break T1 ⦄ • ⭃ * break [ g ] break ⦃ L2 , break T2 ⦄ )" + non associative with precedence 45 + for @{ 'YPRedStepStar $h $g $L1 $T1 $L2 $T2 }. + +include "basic_2/substitution/csup.ma". +include "basic_2/computation/yprs.ma". + +(* ITERATED STEP OF HYPER PARALLEL COMPUTATION ON CLOSURES ******************) + +inductive ysteps (h) (g) (L1) (T1) (L2) (T2): Prop ≝ +| ysteps_intro: h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → (L1 = L2 → T1 = T2 → ⊥) → + ysteps h g L1 T1 L2 T2 +. + +interpretation "iterated step of hyper parallel computation (closure)" + 'YPRedStepStar h g L1 T1 L2 T2 = (ysteps h g L1 T1 L2 T2). + +(* Basic properties *********************************************************) + +lemma ssta_ysteps: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U → + h ⊢ ⦃L, T⦄ •⭃*[g] ⦃L, U⦄. +#h #g #L #T #U #l #HTU +@ysteps_intro /3 width=2/ #_ #H destruct +elim (ssta_inv_refl … HTU) +qed. + +lemma csup_ysteps: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → + h ⊢ ⦃L1, T1⦄ •⭃*[g] ⦃L2, T2⦄. +#h #g #L1 #L2 #T1 #T2 #H +lapply (csup_fwd_cw … H) #H1 +@ysteps_intro /3 width=1/ -H #H2 #H3 destruct +elim (lt_refl_false … H1) +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps_csups.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps_csups.etc new file mode 100644 index 000000000..2e48f396d --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/csup/ysteps_csups.etc @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/yprs_csups.ma". +include "basic_2/computation/ysteps.ma". + +(* ITERATED STEP OF HYPER PARALLEL COMPUTATION ON CLOSURES ******************) + +(* Properties on iterated supclosure ****************************************) + +lemma csups_ysteps: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → + h ⊢ ⦃L1, T1⦄ •⭃*[g] ⦃L2, T2⦄. +#h #g #L1 #L2 #T1 #T2 #H +lapply (csups_fwd_cw … H) #H1 +@ysteps_intro /2 width=1/ -H #H2 #H3 destruct +elim (lt_refl_false … H1) +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma index 40a364a44..478911825 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma @@ -17,21 +17,21 @@ include "basic_2/grammar/cl_shift.ma". (* WEIGHT OF A CLOSURE ******************************************************) -definition cw: lenv → term → ? ≝ λL,T. #{L} + #{T}. +definition fw: lenv → term → ? ≝ λL,T. #{L} + #{T}. -interpretation "weight (closure)" 'Weight L T = (cw L T). +interpretation "weight (closure)" 'Weight L T = (fw L T). (* Basic properties *********************************************************) (* Basic_1: was: flt_wf__q_ind *) (* Basic_1: was: flt_wf_ind *) -axiom cw_wf_ind: ∀R:lenv→predicate term. - (∀L2,T2. (∀L1,T1. #{L1,T1} < #{L2,T2} → R L1 T1) → R L2 T2) → - ∀L,T. R L T. +axiom fw_ind: ∀R:relation2 lenv term. + (∀L2,T2. (∀L1,T1. #{L1,T1} < #{L2,T2} → R L1 T1) → R L2 T2) → + ∀L,T. R L T. (* Basic_1: was: flt_shift *) -lemma cw_shift: ∀a,K,I,V,T. #{K. ⓑ{I} V, T} < #{K, ⓑ{a,I} V. T}. +lemma fw_shift: ∀a,K,I,V,T. #{K. ⓑ{I} V, T} < #{K, ⓑ{a,I} V. T}. normalize // qed. @@ -41,19 +41,19 @@ lemma tw_shift: ∀L,T. #{L, T} ≤ #{L @@ T}. @transitive_le [3: @IHL |2: /2 width=2/ | skip ] qed. -lemma cw_tpair_sn: ∀I,L,V,T. #{L, V} < #{L, ②{I}V.T}. +lemma fw_tpair_sn: ∀I,L,V,T. #{L, V} < #{L, ②{I}V.T}. #I #L #V #T normalize in ⊢ (? % %); // qed. -lemma cw_tpair_dx: ∀I,L,V,T. #{L, T} < #{L, ②{I}V.T}. +lemma fw_tpair_dx: ∀I,L,V,T. #{L, T} < #{L, ②{I}V.T}. #I #L #V #T normalize in ⊢ (? % %); // qed. -lemma cw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. #{L, V2} < #{L, ②{I1}V1.②{I2}V2.T}. +lemma fw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. #{L, V2} < #{L, ②{I1}V1.②{I2}V2.T}. #I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/ qed. -lemma cw_tpair_dx_sn_shift: ∀a2,I1,I2,L,V1,V2,T. +lemma fw_tpair_dx_sn_shift: ∀a2,I1,I2,L,V1,V2,T. #{L.ⓑ{I2}V2, T} < #{L, ②{I1}V1.ⓑ{a2,I2}V2.T}. #a2 #I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma index ba94738a8..9988b3d4c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma @@ -37,4 +37,19 @@ interpretation "abbreviation (local environment)" interpretation "abstraction (local environment)" 'DxAbst L T = (LPair L Abst T). +(* Basic inversion lemmas ***************************************************) + +lemma destruct_lpair_lpair: ∀I1,I2,L1,L2,V1,V2. L1.ⓑ{I1}V1 = L2.ⓑ{I2}V2 → + ∧∧L1 = L2 & I1 = I2 & V1 = V2. +#I1 #I2 #L1 #L2 #V1 #V2 #H destruct /2 width=1/ +qed-. + +lemma discr_lpair_x_xy: ∀I,V,L. L = L.ⓑ{I}V → ⊥. +#I #V #L elim L -L +[ #H destruct +| #L #J #W #IHL #H + elim (destruct_lpair_lpair … H) -H #H1 #H2 #H3 destruct /2 width=1/ (**) (* destruct lemma needed *) +] +qed-. + (* Basic_1: removed theorems 2: chead_ctail c_tail_ind *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma index f58f96076..ab90ddf29 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma @@ -46,9 +46,9 @@ lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| → #K2 #I2 #V2 #L1 #L2 #_ append_length in H2; #H elim (plus_xySz_x_false … (sym_eq … H)) - | #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct (**) (* destruct does not simplify well *) - -H1 (**) (* destruct: the destucted equality is not erased *) - elim (IH … e0 ?) -IH // -H2 #H1 #H2 destruct /2 width=1/ + | #K2 #I2 #V2 #L1 #L2 #H1 #H2 + elim (destruct_lpair_lpair … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *) + elim (IH … H1 ?) -IH -H1 // -H2 /2 width=1/ ] ] qed-. +lemma append_inv_refl_dx: ∀L,K. L @@ K = L → K = ⋆. +#L #K #H +elim (append_inj_dx … (⋆) … H ?) // +qed-. + +lemma append_inv_pair_dx: ∀I,L,K,V. L @@ K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V. +#I #L #K #V #H +elim (append_inj_dx … (⋆.ⓑ{I}V) … H ?) // +qed-. + lemma length_inv_pos_dx_append: ∀d,L. |L| = d + 1 → ∃∃I,K,V. |K| = d & L = ⋆.ⓑ{I}V @@ K. #d @(nat_ind_plus … d) -d [ #L #H elim (length_inv_pos_dx … H) -H #I #K #V #H >(length_inv_zero_dx … H) -H #H destruct - @ex2_3_intro [4: /2 width=2/ |5: // |1,2,3: skip ] (* /3/ does not work *) + @ex2_3_intro [4: /2 width=2/ |5: // |1,2,3: skip ] (**) (* /3/ does not work *) | #d #IHd #L #H elim (length_inv_pos_dx … H) -H #I #K #V #H elim (IHd … H) -IHd -H #I0 #K0 #V0 #H1 #H2 #H3 destruct diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma index d277ed00e..59e2e6172 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma @@ -31,9 +31,9 @@ lemma lw_pair: ∀I,L,V. #{L} < #{(L.ⓑ{I}V)}. (* Basic eliminators ********************************************************) -axiom lw_wf_ind: ∀R:predicate lenv. - (∀L2. (∀L1. #{L1} < #{L2} → R L1) → R L2) → - ∀L. R L. +axiom lw_ind: ∀R:predicate lenv. + (∀L2. (∀L1. #{L1} < #{L2} → R L1) → R L2) → + ∀L. R L. (* Basic_1: removed theorems 2: clt_cong clt_head clt_thead *) (* Basic_1: note: clt_thead should be renamed clt_ctail *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma index ce05e436e..d8f39a3a1 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma @@ -32,9 +32,9 @@ qed. (* Basic eliminators ********************************************************) -axiom tw_wf_ind: ∀R:predicate term. - (∀T2. (∀T1. #{T1} < #{T2} → R T1) → R T2) → - ∀T. R T. +axiom tw_ind: ∀R:predicate term. + (∀T2. (∀T1. #{T1} < #{T2} → R T1) → R T2) → + ∀T. R T. (* Basic_1: removed theorems 11: wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/csup.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/csup.ma deleted file mode 100644 index 01a676616..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/csup.ma +++ /dev/null @@ -1,35 +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/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 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-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/frsup.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/frsup.ma new file mode 100644 index 000000000..31d6c9fee --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/frsup.ma @@ -0,0 +1,119 @@ +(**************************************************************************) +(* ___ *) +(* ||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/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/lambda_delta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma index c93d3cd18..9511648aa 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma @@ -266,7 +266,7 @@ lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #{L2} ≤ #{L1}. ] qed-. -lemma ldrop_pair2_fwd_cw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V → +lemma ldrop_pair2_fwd_fw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V → ∀T. #{K, V} < #{L, T}. #I #L #K #V #d #e #H #T lapply (ldrop_fwd_lw … H) -H #H diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma index b7862fcbf..07d9c53e4 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma @@ -158,3 +158,19 @@ lemma ldrop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L. ⇩[0, e2 + e1] L1 ≡ L2. #e1 #e1 #e2 >commutative_plus /2 width=5/ qed. + +lemma ldrop_conf_div: ∀I1,L,K,V1,e1. ⇩[0, e1] L ≡ K. ⓑ{I1} V1 → + ∀I2,V2,e2. ⇩[0, e2] L ≡ K. ⓑ{I2} V2 → + ∧∧ e1 = e2 & I1 = I2 & V1 = V2. +#I1 #L #K #V1 #e1 #HLK1 #I2 #V2 #e2 #HLK2 +elim (le_or_ge e1 e2) #He +[ lapply (ldrop_conf_ge … HLK1 … HLK2 ?) +| lapply (ldrop_conf_ge … HLK2 … HLK1 ?) +] -HLK1 -HLK2 // #HK +lapply (ldrop_fwd_O1_length … HK) #H +elim (discr_minus_x_xy … H) -H +[1,3: normalize H in HK; #HK +lapply (ldrop_inv_refl … HK) -HK #H destruct +lapply (inv_eq_minus_O … H) -H /3 width=1/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/csups.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/csups.ma deleted file mode 100644 index 56cfa9ee8..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/csups.ma +++ /dev/null @@ -1,57 +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/csup.ma". - -(* ITERATED SUPCLOSURE ******************************************************) - -definition csups: bi_relation lenv term ≝ bi_TC … csup. - -interpretation "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. - (∀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 csups_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 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. - -(* 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 -/3 width=3 by csup_fwd_cw, transitive_lt/ -qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/csups_csups.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/csups_csups.ma deleted file mode 100644 index 1446246c3..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/csups_csups.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/csups.ma". - -(* ITERATED SUPCLOSURE ******************************************************) - -(* Main propertis ***********************************************************) - -theorem csups_trans: bi_transitive … csups. -/2 width=4/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma index 84c8bee70..9a3eb1b7c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma @@ -49,12 +49,12 @@ lemma delifta_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼▼*[d, e] T1 ≡ T2 → qed. lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼▼*[d, e] T1 ≡ T2. -#L #T1 @(cw_wf_ind … L T1) -L -T1 #L #T1 elim T1 -T1 +#L #T1 @(fw_ind … L T1) -L -T1 #L #T1 elim T1 -T1 [ * #i #IH #T2 #d #e #H [ >(delift_inv_sort1 … H) -H // | elim (delift_inv_lref1 … H) -H * /2 width=1/ #K #V1 #V2 #Hdi #Hide #HLK #HV12 #HVT2 - lapply (ldrop_pair2_fwd_cw … HLK) #H + lapply (ldrop_pair2_fwd_fw … HLK) #H lapply (IH … HV12) // -H /2 width=6/ | >(delift_inv_gref1 … H) -H // ] diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma index a53033aa0..01ee6108e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma @@ -32,14 +32,14 @@ qed. fact sfr_delift_aux: ∀L,T,T1,d,e. d + e ≤ |L| → ≽ [d, e] L → T = T1 → ∃T2. L ⊢ ▼*[d, e] T1 ≡ T2. -#L #T @(cw_wf_ind … L T) -L -T #L #T #IH * * /2 width=2/ +#L #T @(fw_ind … L T) -L -T #L #T #IH * * /2 width=2/ [ #i #d #e #Hde #HL #H destruct elim (lt_or_ge i d) #Hdi [ /3 width=2/ ] elim (lt_or_ge i (d+e)) #Hide [2: /3 width=2/ ] lapply (lt_to_le_to_lt … Hide Hde) #Hi elim (ldrop_O1_lt … Hi) -Hi #I #K #V1 #HLK lapply (sfr_inv_ldrop … HLK … HL ? ?) // #H destruct - lapply (ldrop_pair2_fwd_cw … HLK (#i)) #HKL + lapply (ldrop_pair2_fwd_fw … HLK (#i)) #HKL lapply (ldrop_fwd_ldrop2 … HLK) #HLK0 lapply (ldrop_fwd_O1_length … HLK0) #H lapply (sfr_ldrop_trans_be_up … HLK0 … HL ? ?) -HLK0 -HL diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/frsupp.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/frsupp.ma new file mode 100644 index 000000000..9cfee7cfd --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/frsupp.ma @@ -0,0 +1,107 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. + +(* 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 **************************************************) + +fact lift_frsupp_trans_aux: ∀L2,U0. ( + ∀L,K,U1,U2. ⦃L, U1⦄ ⧁+ ⦃L @@ K, U2⦄ → + ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → + #{L, U1} < #{L2, U0} → + ∃T2. ⇧[d + |K|, e] T2 ≡ U2 + ) → + ∀L1,K,U1,U2. ⦃L1, U1⦄ ⧁+ ⦃L2 @@ K, U2⦄ → + ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → + L2 = L1 → U0 = U1 → + ∃T2. ⇧[d + |K|, e] T2 ≡ U2. +#L2 #U0 #IH #L1 #X #U1 #U2 #H @(frsupp_ind_dx … H) -L1 -U1 /2 width=5 by lift_frsup_trans/ +#L1 #L #U1 #U #HL1 #HL2 #_ #T1 #d #e #HTU1 #H1 #H2 destruct +elim (frsup_fwd_append … HL1) #K1 #H destruct +elim (frsupp_fwd_append … HL2) #K >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/lambda_delta/basic_2/unfold/frsups_frsups.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/frsups_frsups.ma new file mode 100644 index 000000000..e7b7de26e --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/frsups_frsups.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/frsups.ma". + +(* STAR-ITERATED RESTRICTED SUPCLOSURE **************************************) + +(* Main propertis ***********************************************************) + +theorem frsups_trans: bi_transitive … frsups. +/2 width=4/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_ltpss_dx.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_ltpss_dx.ma index 22fa61ffc..5ea9f6bd6 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_ltpss_dx.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx_ltpss_dx.ma @@ -46,7 +46,7 @@ qed. fact ltpss_dx_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 → ∀L0. L0 ▶* [d, e] L1 → Y1 = L1 → X2 = T2 → L0 ⊢ T2 ▶* [d, e] U2. -#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH +#Y1 #X2 @(fw_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH #L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e [ // | #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL01 #H1 #H2 destruct @@ -82,7 +82,7 @@ lemma ltpss_dx_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 ▶* [d, e] L1 → fact ltpss_dx_conf_aux: ∀K,K1,L1,d1,e1. K1 ▶* [d1, e1] L1 → ∀K2,L2,d2,e2. K2 ▶* [d2, e2] L2 → K1 = K → K2 = K → ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L. -#K @(lw_wf_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1 +#K @(lw_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1 [ -IH /2 width=3/ | -IH #K1 #I1 #V1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2 [ /2 width=3/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma index 95eb9efd9..0d13a5a3f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn.ma @@ -200,7 +200,8 @@ lemma ltpss_sn_weak: ∀L1,L2,d1,e1. L1 ⊢ ▶* [d1, e1] L2 → lapply (le_plus_to_minus … Hd21) -Hd21 #Hd21 /3 width=5/ | -Hd21 normalize in Hde12; lapply (lt_to_le_to_lt 0 … Hde12) // #He2 - lapply (le_plus_to_minus_r … Hde12) -Hde12 /3 width=5/ + lapply (le_plus_to_minus_r … Hde12) -Hde12 + /3 width=5 by ltpss_sn_tpss2_lt, tpss_weak/ (**) (* /3 width=5/ used to work *) ] ] qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma index 7aa2c5df2..10a190143 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_sn_ltpss_sn.ma @@ -23,7 +23,7 @@ include "basic_2/unfold/ltpss_sn_tpss.ma". fact ltpss_sn_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 → ∀L0. L0 ⊢ ▶* [d, e] L1 → Y1 = L1 → X2 = T2 → L0 ⊢ T2 ▶* [d, e] U2. -#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH +#Y1 #X2 @(fw_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH #L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e [ // | #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL01 #H1 #H2 destruct diff --git a/matita/matita/contribs/lambda_delta/ground_2/arith.ma b/matita/matita/contribs/lambda_delta/ground_2/arith.ma index f7f5e35c4..ad3ab4a3d 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/arith.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/arith.ma @@ -69,13 +69,17 @@ lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x. #Hxy elim (H Hxy) qed-. -lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥. -#z #x elim x -x normalize -[ #y eqOS // qed. @@ -299,6 +299,12 @@ theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b. #a #b #c #H @(le_plus_to_le_r … b) /2/ qed. +lemma lt_to_le: ∀x,y. x < y → x ≤ y. +/2 width=2/ qed. + +lemma inv_eq_minus_O: ∀x,y. x - y = 0 → x ≤ y. +// qed-. + (* lt *) theorem transitive_lt: transitive nat lt. @@ -600,6 +606,9 @@ lemma le_plus_compatible: ∀x1,x2,y1,y2. x1 ≤ y1 → x2 ≤ y2 → x1 + x2 #x1 #y1 #x2 #y2 #H1 #H2 /2/ @le_plus // /2/ /3 by le_minus_to_plus, monotonic_le_plus_r, transitive_le/ qed. *) +lemma minus_le: ∀x,y. x - y ≤ x. +/2 width=1/ qed. + (* lt *) theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n"; "⭃"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ; + [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ; ["≥"; "≽"; "⥸"; ]; ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ; ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ;