From: Ferruccio Guidi Date: Sun, 1 Jun 2014 18:44:03 +0000 (+0000) Subject: - advances on hereditarily free variables: now "frees" is primitive X-Git-Tag: make_still_working~915 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c671743a83bbc7fff114e3e3694f628c0ec6685b;p=helm.git - advances on hereditarily free variables: now "frees" is primitive - some refactoring in etc --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/append/cpy2.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/append/cpy2.etc new file mode 100644 index 000000000..e941c9653 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/append/cpy2.etc @@ -0,0 +1,27 @@ +include "basic_2/grammar/cl_shift.ma". +include "basic_2/relocation/ldrop_append.ma". + +lemma cpy_append: ∀G,d,e. l_appendable_sn … (cpy d e G). +#G #d #e #K #T1 #T2 #H elim H -G -K -T1 -T2 -d -e +/2 width=1 by cpy_atom, cpy_bind, cpy_flat/ +#I #G #K #K0 #V #W #i #d #e #Hdi #Hide #HK0 #HVW #L +lapply (ldrop_fwd_length_lt2 … HK0) #H +@(cpy_subst I … (L@@K0) … HVW) // (**) (* /4/ does not work *) +@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ +qed-. + +lemma cpy_fwd_shift1: ∀G,L1,L,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶[d, e] T → + ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. +#G #L1 @(lenv_ind_dx … L1) -L1 normalize +[ #L #T1 #T #d #e #HT1 + @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *) +| #I #L1 #V1 #IH #L #T1 #X #d #e + >shift_append_assoc normalize #H + elim (cpy_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 ] (**) (* explicit constructor *) + /2 width=3 by trans_eq/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/append/cpys0.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/append/cpys0.etc new file mode 100644 index 000000000..fa9bcf6de --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/append/cpys0.etc @@ -0,0 +1,24 @@ +include "basic_2/grammar/cl_shift.ma". +include "basic_2/relocation/ldrop_append.ma". + +lemma cpys_append: ∀G. l_appendable_sn … (cpys G). +#G #K #T1 #T2 #H elim H -G -K -T1 -T2 +/2 width=3 by cpys_bind, cpys_flat/ +#I #G #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L +lapply (ldrop_fwd_length_lt2 … HK0) #H +@(cpys_delta … I … (L@@K0) V1 … HVW2) // +@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ (**) (* /3/ does not work *) +qed. + +lemma cpys_fwd_shift1: ∀G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*× T → + ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. +#G #L1 @(lenv_ind_dx … L1) -L1 normalize +[ #L #T1 #T #HT1 @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *) +| #I #L1 #V1 #IH #L #T1 #X >shift_append_assoc normalize + #H elim (cpys_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 by trans_eq/ (**) (* explicit constructor *) +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/append/cpys2.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/append/cpys2.etc new file mode 100644 index 000000000..22f74d0a8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/append/cpys2.etc @@ -0,0 +1,14 @@ +lemma cpys_append: ∀G,d,e. l_appendable_sn … (cpys d e G). +#G #d #e #K #T1 #T2 #H @(cpys_ind … H) -T2 +/3 width=3 by cpys_strap1, cpy_append/ +qed-. + +lemma cpys_fwd_shift1: ∀G,L,L1,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*[d, e] T → + ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. +#G #L #L1 #T1 #T #d #e #H @(cpys_ind … H) -T +[ /2 width=4 by ex2_2_intro/ +| #T #X #_ #HX * #L0 #T0 #HL10 #H destruct + elim (cpy_fwd_shift1 … HX) -HX #L2 #T2 #HL02 #H destruct + /2 width=4 by ex2_2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/append/lpys0.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/append/lpys0.etc new file mode 100644 index 000000000..cb3dfd037 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/append/lpys0.etc @@ -0,0 +1,29 @@ +lemma lpys_append: ∀G,K1,K2. ⦃G, K1⦄ ⊢ ▶*× K2 → ∀L1,L2. ⦃G, L1⦄ ⊢ ▶*× L2 → + ⦃G, L1 @@ K1⦄ ⊢ ▶*× L2 @@ K2. +/3 width=1 by lpx_sn_append, cpys_append/ qed. + +(* Advanced forward lemmas **************************************************) + +lemma lpys_fwd_append1: ∀G,K1,L1,L. ⦃G, K1 @@ L1⦄ ⊢ ▶*× L → + ∃∃K2,L2. ⦃G, K1⦄ ⊢ ▶*× K2 & L = K2 @@ L2. +/2 width=2 by lpx_sn_fwd_append1/ qed-. + +lemma lpys_fwd_append2: ∀G,L,K2,L2. ⦃G, L⦄ ⊢ ▶*× K2 @@ L2 → + ∃∃K1,L1. ⦃G, K1⦄ ⊢ ▶*× K2 & L = K1 @@ L1. +/2 width=2 by lpx_sn_fwd_append2/ qed-. + +(* Advanced forward lemmas **************************************************) + +lemma cpys_fwd_shift1_ext: ∀G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*× T → + ∃∃L2,T2. ⦃G, L @@ L1⦄ ⊢ ▶*× L @@ L2 & ⦃G, L @@ L1⦄ ⊢ T1 ▶*× T2 & + T = L2 @@ T2. +#G #L1 @(lenv_ind_dx … L1) -L1 +[ #L #T1 #T #HT1 @ex3_2_intro + [3: // |4,5: // |1,2: skip ] (**) (* auto does not work *) +| #I #L1 #V1 #IH #L #T1 #T >shift_append_assoc #H (cpys_inv_sort1 … H) -X /2 width=2 by ex_intro/ +qed. + +lemma cofrees_gref: ∀L,i,p. L ⊢ i ~ϵ 𝐅*⦃§p⦄. +#L #i #p #X #H >(cpys_inv_gref1 … H) -X /2 width=2 by ex_intro/ +qed. + +lemma cofrees_bind: ∀L,V,i. L ⊢ i ~ϵ 𝐅*⦃V⦄ → + ∀I,T. L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*⦃T⦄ → + ∀a. L ⊢ i ~ϵ 𝐅*⦃ⓑ{a,I}V.T⦄. +#L #W1 #i #HW1 #I #U1 #HU1 #a #X #H elim (cpys_inv_bind1 … H) -H +#W2 #U2 #HW12 #HU12 #H destruct +elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_bind, ex_intro/ +qed. + +lemma cofrees_flat: ∀L,V,i. L ⊢ i ~ϵ 𝐅*⦃V⦄ → ∀T. L ⊢ i ~ϵ 𝐅*⦃T⦄ → + ∀I. L ⊢ i ~ϵ 𝐅*⦃ⓕ{I}V.T⦄. +#L #W1 #i #HW1 #U1 #HU1 #I #X #H elim (cpys_inv_flat1 … H) -H +#W2 #U2 #HW12 #HU12 #H destruct +elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_flat, ex_intro/ +qed. + +axiom cofrees_dec: ∀L,T,i. Decidable (L ⊢ i ~ϵ 𝐅*⦃T⦄). + +(* Basic negated inversion lemmas *******************************************) + +lemma frees_inv_bind: ∀a,I,L,V,T,i. (L ⊢ i ~ϵ 𝐅*⦃ⓑ{a,I}V.T⦄ → ⊥) → + (L ⊢ i ~ϵ 𝐅*⦃V⦄ → ⊥) ∨ (L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*⦃T⦄ → ⊥). +#a #I #L #W #U #i #H elim (cofrees_dec L W i) +/4 width=8 by cofrees_bind, or_intror, or_introl/ +qed-. + +lemma frees_inv_flat: ∀I,L,V,T,i. (L ⊢ i ~ϵ 𝐅*⦃ⓕ{I}V.T⦄ → ⊥) → + (L ⊢ i ~ϵ 𝐅*⦃V⦄ → ⊥) ∨ (L ⊢ i ~ϵ 𝐅*⦃T⦄ → ⊥). +#I #L #W #U #i #H elim (cofrees_dec L W i) +/4 width=7 by cofrees_flat, or_intror, or_introl/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees_alt.etc new file mode 100644 index 000000000..8443f38e3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees_alt.etc @@ -0,0 +1,104 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/lift_neg.ma". +include "basic_2/relocation/lift_lift.ma". +include "basic_2/substitution/cpys.ma". +include "basic_2/substitution/cofrees_lift.ma". + +(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************) + +(* Alternative definition of frees_ge ***************************************) + +(* +lemma cpys_fwd_nlift2: ∀G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ▶* U2 → + ∀i. (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) → + (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥) ∨ + ∃∃I,K,W,j. j < i & ⇩[j]L ≡ K.ⓑ{I}W & + (∀V. ⇧[i-j-1, 1] V ≡ W → ⊥) & (∀T1. ⇧[j, 1] T1 ≡ U1 → ⊥). +#G #L #U1 #U2 #H elim H -G -L -U1 -U2 +[ /3 width=2 by or_introl/ +| #I #G #L #K #V1 #V2 #W2 #j #HLK #_ #HVW2 #IHV12 #i #HnW2 + elim (lt_or_ge j i) #Hij + [ @or_intror (**) @(ex4_4_intro … HLK) // + [ #X #HXV elim (lift_trans_le … HXV … HVW ?) -V // + #Y #HXY >minus_plus minus_plus in ⊢ (??(?(?%?)?)??→?); >minus_plus in ⊢ (??(?(??%)?)??→?); >arith_b1 /2 width=1 by/ +] +qed-. + +lemma frees_ind_ge: ∀R:relation4 ynat nat lenv term. + (∀d,i,L,U. d ≤ yinj i → (∀T. ⇧[i, 1] T ≡ U → ⊥) → R d i L U) → + (∀d,i,j,I,L,K,W,U. d ≤ yinj j → j < i → ⇩[j]L ≡ K.ⓑ{I}W → (K ⊢ i-j-1 ~ϵ 𝐅*[0]⦃W⦄ → ⊥) → (∀T. ⇧[j, 1] T ≡ U → ⊥) → R 0 (i-j-1) K W → R d i L U) → + ∀d,i,L,U. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R d i L U. +#R #IH1 #IH2 #d #i #L #U +generalize in match d; -d generalize in match i; -i +@(f2_ind … rfw … L U) -L -U +#n #IHn #L #U #Hn #i #d #Hdi #H elim (frees_inv_ge … H) -H /3 width=2 by/ +-IH1 * #I #K #W #j #Hdj #Hji #HLK #HnW #HnU destruct /4 width=12 by ldrop_fwd_rfw/ +qed-. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees_lift.etc new file mode 100644 index 000000000..02f227a7a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees0/cofrees_lift.etc @@ -0,0 +1,148 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpys_lift.ma". +include "basic_2/substitution/cofrees.ma". + +(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************) + +(* Advanced inversion lemmas ************************************************) + +lemma cofrees_inv_lref_lt: ∀L,i,j. L ⊢ i ~ϵ 𝐅*⦃#j⦄ → j < i → + ∀I,K,W. ⇩[j]L ≡ K.ⓑ{I}W → K ⊢ i-j-1 ~ϵ 𝐅*⦃W⦄. +#L #i #j #Hj #Hji #I #K #W1 #HLK #W2 #HW12 elim (lift_total W2 0 (j+1)) +#X2 #HWX2 elim (Hj X2) /2 width=7 by cpys_delta/ -I -L -K -W1 +#Z2 #HZX2 elim (lift_div_le … HWX2 (i-j-1) 1 Z2) -HWX2 /2 width=2 by ex_intro/ +>minus_plus minus_plus_plus_l // +| #J #W #U #Hn #i #H1 #j #H2 #I #K #V #HLK #Hji destruct + elim (cofrees_inv_flat … H1) -H1 #HW #HU + elim (nlift_inv_flat … H2) -H2 [ /3 width=7 by/ ] + #HnU @(IH … HU … HnU … HLK) // (**) (* full auto fails *) +] +qed-. + +(* Advanced properties ******************************************************) + +lemma cofrees_lref_gt: ∀L,i,j. i < j → L ⊢ i ~ϵ 𝐅*⦃#j⦄. +#L #i #j #Hij #X #H elim (cpys_inv_lref1 … H) -H +[ #H destruct /3 width=2 by lift_lref_ge_minus, ex_intro/ +| * #I #K #V1 #V2 #_ #_ #H -I -L -K -V1 + elim (lift_split … H i j) /2 width=2 by lt_to_le, ex_intro/ +] +qed. + +lemma cofrees_lref_lt: ∀I,L,K,W,i,j. j < i → ⇩[j] L ≡ K.ⓑ{I}W → + K ⊢ (i-j-1) ~ϵ 𝐅*⦃W⦄ → L ⊢ i ~ϵ 𝐅*⦃#j⦄. +#I #L #K #W1 #i #j #Hji #HLK #HW1 #X #H elim (cpys_inv_lref1 … H) -H +[ #H destruct /3 width=2 by lift_lref_lt, ex_intro/ +| * #I0 #K0 #W0 #W2 #HLK0 #HW12 #HW2 lapply (ldrop_mono … HLK0 … HLK) -L + #H destruct elim (HW1 … HW12) -I -K -W1 + #V2 #HVW2 elim (lift_trans_le … HVW2 … HW2) -W2 // + >minus_plus minus_plus (cpys_inv_sort1 … H) -X /2 width=2 by ex_intro/ +qed. + +lemma cofrees_gref: ∀L,d,i,p. L ⊢ i ~ϵ 𝐅*[d]⦃§p⦄. +#L #d #i #p #X #H >(cpys_inv_gref1 … H) -X /2 width=2 by ex_intro/ +qed. + +lemma cofrees_bind: ∀L,V,d,i. L ⊢ i ~ϵ 𝐅*[d] ⦃V⦄ → + ∀I,T. L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃T⦄ → + ∀a. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}V.T⦄. +#L #W1 #d #i #HW1 #I #U1 #HU1 #a #X #H elim (cpys_inv_bind1 … H) -H +#W2 #U2 #HW12 #HU12 #H destruct +elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_bind, ex_intro/ +qed. + +lemma cofrees_flat: ∀L,V,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ∀T. L ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → + ∀I. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}V.T⦄. +#L #W1 #d #i #HW1 #U1 #HU1 #I #X #H elim (cpys_inv_flat1 … H) -H +#W2 #U2 #HW12 #HU12 #H destruct +elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_flat, ex_intro/ +qed. + +lemma cofrees_cpy_trans: ∀L,U1,U2,d. ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 → + ∀i. L ⊢ i ~ϵ 𝐅*[d]⦃U1⦄ → L ⊢ i ~ϵ 𝐅*[d]⦃U2⦄. +/3 width=3 by cpys_strap2/ qed-. + +axiom cofrees_dec: ∀L,T,d,i. Decidable (L ⊢ i ~ϵ 𝐅*[d]⦃T⦄). + +(* Basic negated properties *************************************************) + +lemma frees_cpy_div: ∀L,U1,U2,d. ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 → + ∀i. (L ⊢ i ~ϵ 𝐅*[d]⦃U2⦄ → ⊥) → (L ⊢ i ~ϵ 𝐅*[d]⦃U1⦄ → ⊥). +/3 width=7 by cofrees_cpy_trans/ qed-. + +(* Basic negated inversion lemmas *******************************************) + +lemma frees_inv_bind: ∀a,I,L,V,T,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}V.T⦄ → ⊥) → + (L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ⊥) ∨ (L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃T⦄ → ⊥). +#a #I #L #W #U #d #i #H elim (cofrees_dec L W d i) +/4 width=9 by cofrees_bind, or_intror, or_introl/ +qed-. + +lemma frees_inv_flat: ∀I,L,V,T,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}V.T⦄ → ⊥) → + (L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ⊥) ∨ (L ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥). +#I #L #W #U #d #H elim (cofrees_dec L W d) +/4 width=8 by cofrees_flat, or_intror, or_introl/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees1/cofrees_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees1/cofrees_alt.etc new file mode 100644 index 000000000..7bb9c9ca7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees1/cofrees_alt.etc @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/cpy_nlift.ma". +include "basic_2/substitution/cofrees_lift.ma". + +(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************) + +(* Alternative definition of frees_ge ***************************************) + +lemma nlift_frees: ∀L,U,d,i. (∀T. ⇧[i, 1] T ≡ U → ⊥) → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥). +#L #U #d #i #HnTU #H elim (cofrees_fwd_lift … H) -H /2 width=2 by/ +qed-. + +lemma frees_inv_ge: ∀L,U,d,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → + (∀T. ⇧[i, 1] T ≡ U → ⊥) ∨ + ∃∃I,K,W,j. d ≤ yinj j & j < i & ⇩[j]L ≡ K.ⓑ{I}W & + (K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄ → ⊥) & (∀T. ⇧[j, 1] T ≡ U → ⊥). +#L #U #d #i #Hdi #H @(frees_ind … H) -U /3 width=2 by or_introl/ +#U1 #U2 #HU12 #HU2 * +[ #HnU2 elim (cpy_fwd_nlift2_ge … HU12 … HnU2) -HU12 -HnU2 /3 width=2 by or_introl/ + * /5 width=9 by nlift_frees, ex5_4_intro, or_intror/ +| * #I2 #K2 #W2 #j2 #Hdj2 #Hj2i #HLK2 #HnW2 #HnU2 elim (cpy_fwd_nlift2_ge … HU12 … HnU2) -HU12 -HnU2 /4 width=9 by ex5_4_intro, or_intror/ + * #I1 #K1 #W1 #j1 #Hdj1 #Hj12 #HLK1 #HnW1 #HnU1 + lapply (ldrop_conf_ge … HLK1 … HLK2 ?) -HLK2 /2 width=1 by lt_to_le/ + #HK12 lapply (ldrop_inv_drop1_lt … HK12 ?) /2 width=1 by lt_plus_to_minus_r/ -HK12 + #HK12 + @or_intror @(ex5_4_intro … HLK1 … HnU1) -HLK1 -HnU1 /2 width=3 by transitive_lt/ + @(frees_be … HK12 … HnW1) /2 width=1 by arith_k_sn/ -HK12 -HnW1 + >minus_plus in ⊢ (??(?(?%?)?)??→?); >minus_plus in ⊢ (??(?(??%)?)??→?); >arith_b1 /2 width=1 by/ +] +qed-. + +lemma frees_ind_ge: ∀R:relation4 ynat nat lenv term. + (∀d,i,L,U. d ≤ yinj i → (∀T. ⇧[i, 1] T ≡ U → ⊥) → R d i L U) → + (∀d,i,j,I,L,K,W,U. d ≤ yinj j → j < i → ⇩[j]L ≡ K.ⓑ{I}W → (K ⊢ i-j-1 ~ϵ 𝐅*[0]⦃W⦄ → ⊥) → (∀T. ⇧[j, 1] T ≡ U → ⊥) → R 0 (i-j-1) K W → R d i L U) → + ∀d,i,L,U. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R d i L U. +#R #IH1 #IH2 #d #i #L #U +generalize in match d; -d generalize in match i; -i +@(f2_ind … rfw … L U) -L -U +#n #IHn #L #U #Hn #i #d #Hdi #H elim (frees_inv_ge … H) -H /3 width=2 by/ +-IH1 * #I #K #W #j #Hdj #Hji #HLK #HnW #HnU destruct /4 width=12 by ldrop_fwd_rfw/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees1/cofrees_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees1/cofrees_lift.etc new file mode 100644 index 000000000..f93f72216 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cofrees1/cofrees_lift.etc @@ -0,0 +1,180 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpys_lift.ma". +include "basic_2/substitution/cofrees.ma". + +(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************) + +(* Advanced inversion lemmas ************************************************) + +lemma cofrees_inv_lref_be: ∀L,d,i,j. L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄ → d ≤ yinj j → j < i → + ∀I,K,W. ⇩[j]L ≡ K.ⓑ{I}W → K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄. +#L #d #i #j #Hj #Hdj #Hji #I #K #W1 #HLK #W2 #HW12 elim (lift_total W2 0 (j+1)) +#X2 #HWX2 elim (Hj X2) /2 width=7 by cpys_subst_Y2/ -I -L -K -W1 -d +#Z2 #HZX2 elim (lift_div_le … HWX2 (i-j-1) 1 Z2) -HWX2 /2 width=2 by ex_intro/ +>minus_plus minus_plus_plus_l // +| #J #W #U #Hn #d #i #H1 #j #H2 #I #K #V #HLK #Hdj #Hji destruct + elim (cofrees_inv_flat … H1) -H1 #HW #HU + elim (nlift_inv_flat … H2) -H2 [ /3 width=9 by/ ] + #HnU @(IH … HU … HnU … HLK) // (**) (* full auto fails *) +] +qed-. + +(* Advanced properties ******************************************************) + +lemma cofrees_lref_skip: ∀L,d,i,j. j < i → yinj j < d → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄. +#L #d #i #j #Hji #Hjd #X #H elim (cpys_inv_lref1_Y2 … H) -H +[ #H destruct /3 width=2 by lift_lref_lt, ex_intro/ +| * #I #K #W1 #W2 #Hdj elim (ylt_yle_false … Hdj) -i -I -L -K -W1 -W2 -X // +] +qed. + +lemma cofrees_lref_lt: ∀L,d,i,j. i < j → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄. +#L #d #i #j #Hij #X #H elim (cpys_inv_lref1_Y2 … H) -H +[ #H destruct /3 width=2 by lift_lref_ge_minus, ex_intro/ +| * #I #K #V1 #V2 #_ #_ #_ #H -I -L -K -V1 -d + elim (lift_split … H i j) /2 width=2 by lt_to_le, ex_intro/ +] +qed. + +lemma cofrees_lref_gt: ∀I,L,K,W,d,i,j. j < i → ⇩[j] L ≡ K.ⓑ{I}W → + K ⊢ (i-j-1) ~ϵ 𝐅*[O]⦃W⦄ → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄. +#I #L #K #W1 #d #i #j #Hji #HLK #HW1 #X #H elim (cpys_inv_lref1_Y2 … H) -H +[ #H destruct /3 width=2 by lift_lref_lt, ex_intro/ +| * #I0 #K0 #W0 #W2 #Hdj #HLK0 #HW12 #HW2 lapply (ldrop_mono … HLK0 … HLK) -L + #H destruct elim (HW1 … HW12) -I -K -W1 -d + #V2 #HVW2 elim (lift_trans_le … HVW2 … HW2) -W2 // + >minus_plus minus_plus yplus_inj >yminus_Y_inj #T2 #HT12 + lapply (cpys_weak … HT12 (d-yinj e0) (∞) ? ?) /2 width=1 by yle_plus2_to_minus_inj2/ -HT12 + | elim (cpys_inv_lift1_ge … HU12 … HLK … HTU1) // #T2 + ] +| elim (cpys_inv_lift1_be … HU12 … HLK … HTU1) // >yminus_Y_inj #T2 #HT12 + lapply (cpys_weak … HT12 (d-yinj e0) (∞) ? ?) // -HT12 +] +-s -L #HT12 #HTU2 +elim (HT1 … HT12) -T1 #V2 #HVT2 +elim (lift_trans_le … HVT2 … HTU2 ?) // (cpy_inv_sort1 … H) -X /2 width=2 by cpx_sort/ -| #I #G #L #K #V1 #V #W #i #HLK #_ #HVW #IHV1 #X #d #e #H - lapply (ldrop_fwd_drop2 … HLK) #H0 - lapply (cpy_weak … H 0 (∞) ? ?) -H // #H - elim (cpy_inv_lift1_be … H … H0 … HVW) -H -H0 -HVW - /3 width=7 by cpx_delta/ -| #a #I #G #L #V1 #V #T1 #T #_ #_ #IHV1 #IHT1 #X #d #e #H elim (cpy_inv_bind1 … H) -H - #V2 #T2 #HV2 #HT2 #H destruct - /5 width=7 by cpx_bind, lsuby_cpy_trans, lsuby_succ/ -| #I #G #L #V1 #V #T1 #T #_ #_ #IHV1 #IHT1 #X #d #e #H elim (cpy_inv_flat1 … H) -H - #V2 #T2 #HV2 #HT2 #H destruct /3 width=3 by cpx_flat/ -| #G #L #V1 #U1 #U #T #_ #HTU #IHU1 #T2 #d #e #HT2 - lapply (cpy_weak … HT2 0 (∞) ? ?) -HT2 // #HT2 - elim (lift_total T2 0 1) #U2 #HTU2 - lapply (cpy_lift_be … HT2 (L.ⓓV1) … (Ⓕ) … HTU … HTU2 ? ?) -T - /3 width=3 by cpx_zeta, ldrop_drop/ -| /3 width=3 by cpx_tau/ -| /3 width=3 by cpx_ti/ -| #a #G #L #V1 #V #W1 #W #T1 #T #_ #_ #_ #IHV1 #IHW1 #IHT1 #X #d #e #HX - elim (cpy_inv_bind1 … HX) -HX #Y #T2 #HY #HT2 #H destruct - elim (cpy_inv_flat1 … HY) -HY #W2 #V2 #HW2 #HV2 #H destruct - /5 width=7 by cpx_beta, lsuby_cpy_trans, lsuby_succ/ -| #a #G #L #V1 #V #U #W1 #W #T1 #T #_ #HVU #_ #_ #IHV1 #IHW1 #IHT1 #X #d #e #HX - elim (cpy_inv_bind1 … HX) -HX #W2 #Y #HW2 #HY #H destruct - elim (cpy_inv_flat1 … HY) -HY #U2 #T2 #HU2 #HT2 #H destruct - lapply (cpy_weak … HU2 0 (∞) ? ?) -HU2 // #HU2 - elim (cpy_inv_lift1_be … HU2 L … HVU) -U - /5 width=7 by cpx_theta, lsuby_cpy_trans, lsuby_succ, ldrop_drop/ -] -qed-. - -lemma cpx_cpys_trans: ∀h,g,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T → - ∀T2,d,e. ⦃G, L⦄ ⊢ T ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2. -#h #g #G #L #T1 #T #HT1 #T2 #d #e #H @(cpys_ind … H) -T2 -/2 width=5 by cpx_cpy_trans/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpxs_cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpxs_cpys.etc deleted file mode 100644 index 881030572..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpxs_cpys.etc +++ /dev/null @@ -1,24 +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/reduction/cpx_cpys.ma". -include "basic_2/computation/cpxs.ma". - -(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) - -(* Properties on local environment refinement for extended substitution *****) - -lemma lsuby_cpxs_trans: ∀h,g,G. lsub_trans … (cpxs h g G) (lsuby 0 (∞)). -/3 width=5 by lsuby_cpx_trans, LTC_lsub_trans/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpy.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpy.etc deleted file mode 100644 index e941c9653..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpy.etc +++ /dev/null @@ -1,27 +0,0 @@ -include "basic_2/grammar/cl_shift.ma". -include "basic_2/relocation/ldrop_append.ma". - -lemma cpy_append: ∀G,d,e. l_appendable_sn … (cpy d e G). -#G #d #e #K #T1 #T2 #H elim H -G -K -T1 -T2 -d -e -/2 width=1 by cpy_atom, cpy_bind, cpy_flat/ -#I #G #K #K0 #V #W #i #d #e #Hdi #Hide #HK0 #HVW #L -lapply (ldrop_fwd_length_lt2 … HK0) #H -@(cpy_subst I … (L@@K0) … HVW) // (**) (* /4/ does not work *) -@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ -qed-. - -lemma cpy_fwd_shift1: ∀G,L1,L,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶[d, e] T → - ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. -#G #L1 @(lenv_ind_dx … L1) -L1 normalize -[ #L #T1 #T #d #e #HT1 - @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *) -| #I #L1 #V1 #IH #L #T1 #X #d #e - >shift_append_assoc normalize #H - elim (cpy_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 ] (**) (* explicit constructor *) - /2 width=3 by trans_eq/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpys.etc deleted file mode 100644 index 22f74d0a8..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/cpys.etc +++ /dev/null @@ -1,14 +0,0 @@ -lemma cpys_append: ∀G,d,e. l_appendable_sn … (cpys d e G). -#G #d #e #K #T1 #T2 #H @(cpys_ind … H) -T2 -/3 width=3 by cpys_strap1, cpy_append/ -qed-. - -lemma cpys_fwd_shift1: ∀G,L,L1,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*[d, e] T → - ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. -#G #L #L1 #T1 #T #d #e #H @(cpys_ind … H) -T -[ /2 width=4 by ex2_2_intro/ -| #T #X #_ #HX * #L0 #T0 #HL10 #H destruct - elim (cpy_fwd_shift1 … HX) -HX #L2 #T2 #HL02 #H destruct - /2 width=4 by ex2_2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/lpx_cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/lpx_cpys.etc deleted file mode 100644 index d3c490a89..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/lpx_cpys.etc +++ /dev/null @@ -1,69 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/relocation/cpy_lift.ma". -include "basic_2/substitution/cpys.ma". -include "basic_2/reduction/lpx_ldrop.ma". - -(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) - -(* Properties on context-sensitive extended substitution for terms **********) - -lemma cpx_cpy_trans_lpx: ∀h,g,G,L1,T1,T. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T → - ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → - ∀T2,d,e. ⦃G, L2⦄ ⊢ T ▶[d, e] T2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2. -#h #g #G #L1 #T1 #T #H elim H -G -L1 -T1 -T -[ #J #G #L1 #L2 #HL12 #T2 #d #e #H elim (cpy_inv_atom1 … H) -H // - * #I #K2 #V2 #i #_ #_ #HLK2 #HVT2 #H destruct - elim (lpx_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H - elim (lpx_inv_pair2 … H) -H #K1 #V1 #_ #HV12 #H destruct - /2 width=7 by cpx_delta/ -| #G #L1 #k #l #Hkl #L2 #_ #X #d #e #H >(cpy_inv_sort1 … H) -X /2 width=2 by cpx_sort/ -| #I #G #L1 #K1 #V1 #V #T #i #HLK1 #_ #HVT #IHV1 #L2 #HL12 #T2 #d #e #HT2 - elim (lpx_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 - elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct - lapply (ldrop_fwd_drop2 … HLK2) -V0 #HLK2 - lapply (cpy_weak … HT2 0 (∞) ? ?) -HT2 // #HT2 - elim (cpy_inv_lift1_be … HT2 … HLK2 … HVT) -HT2 -HLK2 -HVT - /3 width=7 by cpx_delta/ -| #a #I #G #L1 #V1 #V #T1 #T #HV1 #_ #IHV1 #IHT1 #L2 #HL12 #X #d #e #H elim (cpy_inv_bind1 … H) -H - #V2 #T2 #HV2 #HT2 #H destruct /4 width=5 by lpx_pair, cpx_bind/ -| #I #G #L1 #V1 #V #T1 #T #_ #_ #IHV1 #IHT1 #L2 #HL12 #X #d #e #H elim (cpy_inv_flat1 … H) -H - #V2 #T2 #HV2 #HT2 #H destruct /3 width=5 by cpx_flat/ -| #G #L1 #V1 #U1 #U #T #_ #HTU #IHU1 #L2 #HL12 #T2 #d #e #HT2 - lapply (cpy_weak … HT2 0 (∞) ? ?) -HT2 // #HT2 - elim (lift_total T2 0 1) #U2 #HTU2 - lapply (cpy_lift_be … HT2 (L2.ⓓV1) … (Ⓕ) … HTU … HTU2 ? ?) -T - /4 width=5 by cpx_zeta, lpx_pair, ldrop_drop/ -| /3 width=5 by cpx_tau/ -| /3 width=5 by cpx_ti/ -| #a #G #L1 #V1 #V #W1 #W #T1 #T #HV1 #HW1 #_ #IHV1 #IHW1 #IHT1 #L2 #HL12 #X #d #e #HX - elim (cpy_inv_bind1 … HX) -HX #Y #T2 #HY #HT2 #H destruct - elim (cpy_inv_flat1 … HY) -HY #W2 #V2 #HW2 #HV2 #H destruct - /5 width=11 by lpx_pair, cpx_beta, lsuby_cpy_trans, lsuby_succ/ -| #a #G #L1 #V1 #V #U #W1 #W #T1 #T #_ #HVU #HW1 #_ #IHV1 #IHW1 #IHT1 #L2 #HL12 #X #d #e #HX - elim (cpy_inv_bind1 … HX) -HX #W2 #Y #HW2 #HY #H destruct - elim (cpy_inv_flat1 … HY) -HY #U2 #T2 #HU2 #HT2 #H destruct - lapply (cpy_weak … HU2 0 (∞) ? ?) -HU2 // #HU2 - elim (cpy_inv_lift1_be … HU2 L2 … HVU) -U - /4 width=7 by lpx_pair, cpx_theta, ldrop_drop/ -] -qed-. - -lemma cpx_cpys_trans_lpx: ∀h,g,G,L1,T1,T. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T → - ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → - ∀T2,d,e. ⦃G, L2⦄ ⊢ T ▶*[d, e] T2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2. -#h #g #G #L1 #T1 #T #HT1 #L2 #HL12 #T2 #d #e #H @(cpys_ind … H) -T2 -/2 width=7 by cpx_cpy_trans_lpx/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/lsuby.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/lsuby.etc deleted file mode 100644 index 657ad6b6e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpy/lsuby.etc +++ /dev/null @@ -1,15 +0,0 @@ -(* -lemma lsuby_weak: ∀L1,L2,d1,e1. L1 ⊑×[d1, e1] L2 → - ∀d2,e2. d1 ≤ d2 → e2 ≤ e1 → L1 ⊑×[d2, e2] L2. -#L1 #L2 #d1 #e1 #H elim H -L1 -L2 -d1 -e1 // -[ #I1 #I2 #L1 #L2 #V1 #V2 #HL12 #_ #d2 #e2 #_ #He21 - >(yle_inv_O2 … He21) -He21 - /4 width=3 by lsuby_fwd_length, lsuby_O1, monotonic_le_plus_l/ -| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #d2 #e2 #_ #He21 - elim (ynat_cases e2) /4 width=3 by lsuby_fwd_length, lsuby_O1, monotonic_le_plus_l/ - * #e0 #H destruct lapply (yle_inv_succ … He21) -He21 #He21 - elim (ynat_cases d2) /3 width=1 by lsuby_pair/ - * #d0 #H destruct @lsuby_succ @IHL12 // - [ destruct - -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys.etc deleted file mode 100644 index a0603f13e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys.etc +++ /dev/null @@ -1,200 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/extpsubststar_4.ma". -include "basic_2/grammar/genv.ma". -include "basic_2/grammar/cl_shift.ma". -include "basic_2/relocation/ldrop_append.ma". -include "basic_2/relocation/lsuby.ma". - -(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************) - -(* avtivate genv *) -inductive cpys: relation4 genv lenv term term ≝ -| cpys_atom : ∀I,G,L. cpys G L (⓪{I}) (⓪{I}) -| cpys_delta: ∀I,G,L,K,V,V2,W2,i. - ⇩[0, i] L ≡ K.ⓑ{I}V → cpys G K V V2 → - ⇧[0, i + 1] V2 ≡ W2 → cpys G L (#i) W2 -| cpys_bind : ∀a,I,G,L,V1,V2,T1,T2. - cpys G L V1 V2 → cpys G (L.ⓑ{I}V1) T1 T2 → - cpys G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2) -| cpys_flat : ∀I,G,L,V1,V2,T1,T2. - cpys G L V1 V2 → cpys G L T1 T2 → - cpys G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) -. - -interpretation - "context-sensitive extended multiple substitution (term)" - 'ExtPSubstStar G L T1 T2 = (cpys G L T1 T2). - -(* Basic properties *********************************************************) - -lemma lsuby_cpys_trans: ∀G. lsub_trans … (cpys G) lsuby. -#G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 -[ // -| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 - elim (lsuby_fwd_ldrop2_pair … HL12 … HLK1) -HL12 -HLK1 * - /3 width=7 by cpys_delta/ -| /4 width=1 by lsuby_pair, cpys_bind/ -| /3 width=1 by cpys_flat/ -] -qed-. - -(* Note: this is "∀L. reflexive … (cpys L)" *) -lemma cpys_refl: ∀G,T,L. ⦃G, L⦄ ⊢ T ▶*× T. -#G #T elim T -T // * /2 width=1 by cpys_bind, cpys_flat/ -qed. - -lemma cpys_pair_sn: ∀I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ▶*× V2 → - ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ▶*× ②{I}V2.T. -* /2 width=1 by cpys_bind, cpys_flat/ -qed. - -lemma cpys_bind_ext: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ▶*× V2 → - ∀J,T1,T2. ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶*× T2 → - ∀a,I. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*× ⓑ{a,I}V2.T2. -/4 width=4 by lsuby_cpys_trans, cpys_bind, lsuby_pair/ qed. - -lemma cpys_delift: ∀I,G,K,V,T1,L,d. ⇩[0, d] L ≡ (K.ⓑ{I}V) → - ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ▶*× T2 & ⇧[d, 1] T ≡ T2. -#I #G #K #V #T1 elim T1 -T1 -[ * /2 width=4 by cpys_atom, lift_sort, lift_gref, ex2_2_intro/ - #i #L #d elim (lt_or_eq_or_gt i d) #Hid [1,3: /3 width=4 by cpys_atom, lift_lref_ge_minus, lift_lref_lt, ex2_2_intro/ ] - destruct - elim (lift_total V 0 (i+1)) #W #HVW - elim (lift_split … HVW i i) /3 width=7 by cpys_delta, ex2_2_intro/ -| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK - elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2 - [ elim (IHU1 (L. ⓑ{I}W1) (d+1)) -IHU1 /3 width=9 by cpys_bind, ldrop_ldrop, lift_bind, ex2_2_intro/ - | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpys_flat, lift_flat, ex2_2_intro/ - ] -] -qed-. - -lemma cpys_append: ∀G. l_appendable_sn … (cpys G). -#G #K #T1 #T2 #H elim H -G -K -T1 -T2 -/2 width=3 by cpys_bind, cpys_flat/ -#I #G #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L -lapply (ldrop_fwd_length_lt2 … HK0) #H -@(cpys_delta … I … (L@@K0) V1 … HVW2) // -@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ (**) (* /3/ does not work *) -qed. - -(* Basic inversion lemmas ***************************************************) - -fact cpys_inv_atom1_aux: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*× T2 → ∀J. T1 = ⓪{J} → - T2 = ⓪{J} ∨ - ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶*× V2 & - ⇧[O, i + 1] V2 ≡ T2 & J = LRef i. -#G #L #T1 #T2 * -L -T1 -T2 -[ #I #G #L #J #H destruct /2 width=1 by or_introl/ -| #I #G #L #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #J #H destruct /3 width=9 by ex4_5_intro, or_intror/ -| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct -| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct -] -qed-. - -lemma cpys_inv_atom1: ∀J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ▶*× T2 → - T2 = ⓪{J} ∨ - ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶*× V2 & - ⇧[O, i + 1] V2 ≡ T2 & J = LRef i. -/2 width=3 by cpys_inv_atom1_aux/ qed-. - -lemma cpys_inv_sort1: ∀G,L,T2,k. ⦃G, L⦄ ⊢ ⋆k ▶*× T2 → T2 = ⋆k. -#G #L #T2 #k #H elim (cpys_inv_atom1 … H) -H // * -#I #K #V #V2 #i #_ #_ #_ #H destruct -qed-. - -lemma cpys_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ▶*× T2 → - T2 = #i ∨ - ∃∃I,K,V,V2. ⇩[O, i] L ≡ K. ⓑ{I}V & ⦃G, K⦄ ⊢ V ▶*× V2 & - ⇧[O, i + 1] V2 ≡ T2. -#G #L #T2 #i #H elim (cpys_inv_atom1 … H) -H /2 width=1 by or_introl/ * -#I #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=7 by ex3_4_intro, or_intror/ -qed-. - -lemma cpys_inv_lref1_ge: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ▶*× T2 → |L| ≤ i → T2 = #i. -#G #L #T2 #i #H elim (cpys_inv_lref1 … H) -H // * -#I #K #V1 #V2 #HLK #_ #_ #HL -V2 lapply (ldrop_fwd_length_lt2 … HLK) -K -I -V1 -#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/ -qed-. - -lemma cpys_inv_gref1: ∀G,L,T2,p. ⦃G, L⦄ ⊢ §p ▶*× T2 → T2 = §p. -#G #L #T2 #p #H elim (cpys_inv_atom1 … H) -H // * -#I #K #V #V2 #i #_ #_ #_ #H destruct -qed-. - -fact cpys_inv_bind1_aux: ∀G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ▶*× U2 → - ∀a,J,V1,T1. U1 = ⓑ{a,J}V1.T1 → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶*× T2 & - U2 = ⓑ{a,J}V2.T2. -#G #L #U1 #U2 * -L -U1 -U2 -[ #I #G #L #b #J #W #U1 #H destruct -| #I #G #L #K #V #V2 #W2 #i #_ #_ #_ #b #J #W #U1 #H destruct -| #a #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #b #J #W #U1 #H destruct /2 width=5 by ex3_2_intro/ -| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W #U1 #H destruct -] -qed-. - -lemma cpys_inv_bind1: ∀a,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*× U2 → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*× T2 & - U2 = ⓑ{a,I}V2.T2. -/2 width=3 by cpys_inv_bind1_aux/ qed-. - -lemma cpys_inv_bind1_ext: ∀a,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*× U2 → ∀J. - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ▶*× T2 & - U2 = ⓑ{a,I}V2.T2. -#a #I #G #L #V1 #T1 #U2 #H #J elim (cpys_inv_bind1 … H) -H -#V2 #T2 #HV12 #HT12 #H destruct -/4 width=5 by lsuby_cpys_trans, lsuby_pair, ex3_2_intro/ -qed-. - -fact cpys_inv_flat1_aux: ∀G,L,U,U2. ⦃G, L⦄ ⊢ U ▶*× U2 → - ∀J,V1,U1. U = ⓕ{J}V1.U1 → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L⦄ ⊢ U1 ▶*× T2 & - U2 = ⓕ{J}V2.T2. -#G #L #U #U2 * -L -U -U2 -[ #I #G #L #J #W #U1 #H destruct -| #I #G #L #K #V #V2 #W2 #i #_ #_ #_ #J #W #U1 #H destruct -| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #W #U1 #H destruct -| #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W #U1 #H destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma cpys_inv_flat1: ∀I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ▶*× U2 → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*× V2 & ⦃G, L⦄ ⊢ U1 ▶*× T2 & - U2 = ⓕ{I}V2.T2. -/2 width=3 by cpys_inv_flat1_aux/ qed-. - -(* Basic forward lemmas *****************************************************) - -lemma cpys_fwd_bind1: ∀a,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*× T → ∀b,J. - ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{b,J}V1.T1 ▶*× ⓑ{b,J}V2.T2 & - T = ⓑ{a,I}V2.T2. -#a #I #G #L #V1 #T1 #T #H #b #J elim (cpys_inv_bind1_ext … H J) -H -#V2 #T2 #HV12 #HT12 #H destruct /3 width=4 by cpys_bind, ex2_2_intro/ -qed-. - -lemma cpys_fwd_shift1: ∀G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ▶*× T → - ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. -#G #L1 @(lenv_ind_dx … L1) -L1 normalize -[ #L #T1 #T #HT1 @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *) -| #I #L1 #V1 #IH #L #T1 #X >shift_append_assoc normalize - #H elim (cpys_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 by trans_eq/ (**) (* explicit constructor *) -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_cpys.etc deleted file mode 100644 index e0abed64d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_cpys.etc +++ /dev/null @@ -1,72 +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/grammar/lpx_sn_lpx_sn.ma". -include "basic_2/substitution/fqup.ma". -include "basic_2/substitution/lpys_ldrop.ma". - -(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************) - -(* Main properties **********************************************************) - -theorem cpys_antisym: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*× T2 → ⦃G, L⦄ ⊢ T2 ▶*× T1 → T1 = T2. -#G #L #T1 #T2 #H elim H -G -L -T1 -T2 // -[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #_ #HW2 lapply (ldrop_fwd_ldrop2 … HLK) -I -V1 - #HLK elim (cpys_inv_lift1 … HW2 … HLK … HVW2) -L -HVW2 - #X #H #_ elim (lift_inv_lref2_be … H) -G -K -V2 -W2 -X // -| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #H elim (cpys_inv_bind1 … H) -H - #V #T #HV2 #HT2 #H destruct - lapply (IHV12 HV2) #H destruct -IHV12 -HV2 /3 width=1 by eq_f2/ -| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #H elim (cpys_inv_flat1 … H) -H - #V #T #HV2 #HT2 #H destruct /3 width=1 by eq_f2/ -] -qed-. - -theorem cpys_trans_lpys: ∀G. lpx_sn_transitive (cpys G) (cpys G). -#G0 #L0 #T0 @(fqup_wf_ind_eq … G0 L0 T0) -G0 -L0 -T0 #G0 #L0 #T0 #IH #G1 #L1 * [|*] -[ #I #HG #HL #HT #T #H1 #L2 #HL12 #T2 #HT2 destruct - elim (cpys_inv_atom1 … H1) -H1 - [ #H destruct - elim (cpys_inv_atom1 … HT2) -HT2 - [ #H destruct // - | * #I2 #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct - elim (lpys_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H - elim (lpys_inv_pair2 … H) -H #K1 #V1 #HK12 #HV1 #H destruct - lapply (fqup_lref … G1 … HLK1) /3 width=10 by cpys_delta/ - ] - | * #I1 #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct - elim (lpys_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 - elim (lpys_inv_pair1 … H) -H #K2 #W2 #HK12 #_ #H destruct - lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 - elim (cpys_inv_lift1 … HT2 … HLK2 … HVT) -L2 -T - lapply (fqup_lref … G1 … HLK1) /3 width=10 by cpys_delta/ - ] -| #a #I #V1 #T1 #HG #HL #HT #X1 #H1 #L2 #HL12 #X2 #H2 - elim (cpys_inv_bind1 … H1) -H1 #V #T #HV1 #HT1 #H destruct - elim (cpys_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct - /4 width=5 by cpys_bind, lpys_pair/ -| #I #V1 #T1 #HG #HL #HT #X1 #H1 #L2 #HL12 #X2 #H2 - elim (cpys_inv_flat1 … H1) -H1 #V #T #HV1 #HT1 #H destruct - elim (cpys_inv_flat1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct - /3 width=5 by cpys_flat/ -] -qed-. - -theorem cpys_trans: ∀G,L. Transitive … (cpys G L). -/2 width=5 by cpys_trans_lpys/ qed-. - -(* Advanced properties ******************************************************) - -lemma lpys_cpys_trans: ∀G. lsub_trans … (cpys G) (lpys G). -/2 width=5 by cpys_trans_lpys/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_lift.etc deleted file mode 100644 index d798c8a62..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys/cpys_lift.etc +++ /dev/null @@ -1,176 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/relocation/ldrop_ldrop.ma". -include "basic_2/substitution/fqus_alt.ma". -include "basic_2/substitution/cpys.ma". - -(* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************) - -(* Relocation properties ****************************************************) - -lemma cpys_lift: ∀G. l_liftable (cpys G). -#G #K #T1 #T2 #H elim H -G -K -T1 -T2 -[ #I #G #K #L #d #e #_ #U1 #H1 #U2 #H2 - >(lift_mono … H1 … H2) -H1 -H2 // -| #I #G #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 /3 width=7 by cpys_delta/ - ] -| #a #I #G #K #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 by cpys_bind, ldrop_skip/ -| #I #G #K #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 by cpys_flat/ -] -qed. - -lemma cpys_inv_lift1: ∀G. l_deliftable_sn (cpys G). -#G #L #U1 #U2 #H elim H -G -L -U1 -U2 -[ * #G #L #i #K #d #e #_ #T1 #H - [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpys_atom, lift_sort, ex2_intro/ - | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by cpys_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/ - | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpys_atom, lift_gref, ex2_intro/ - ] -| #I #G #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 // shift_append_assoc #H (lift_mono … H1 … H2) -H1 -H2 // +| #I #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #s #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 /3 width=7 by cpys_delta, ldrop_inv_gen/ + ] +| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #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=6 by cpys_bind, ldrop_skip/ +| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #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 by cpys_flat/ +] +qed. + +lemma cpys_inv_lift1: ∀G. l_deliftable_sn (cpys G). +#G #L #U1 #U2 #H elim H -G -L -U1 -U2 +[ * #G #L #i #K #s #d #e #_ #T1 #H + [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpys_atom, lift_sort, ex2_intro/ + | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by cpys_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/ + | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpys_atom, lift_gref, ex2_intro/ + ] +| #I #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #s #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 // (length_inv_zero_dx … H) -L1 // +| #I1 #I2 #L1 #L2 #V #_ #IHL12 #H lapply (injective_plus_l … H) -H + /3 width=1 by lsuby_pair/ +] +qed-. + +(* Basic inversion lemmas ***************************************************) + +fact lsuby_inv_atom1_aux: ∀L1,L2. L1 ⊆ L2 → L1 = ⋆ → L2 = ⋆. +#L1 #L2 * -L1 -L2 // +#I1 #I2 #L1 #L2 #V #_ #H destruct +qed-. + +lemma lsuby_inv_atom1: ∀L2. ⋆ ⊆ L2 → L2 = ⋆. +/2 width=3 by lsuby_inv_atom1_aux/ qed-. + +fact lsuby_inv_pair1_aux: ∀L1,L2. L1 ⊆ L2 → ∀J1,K1,W. L1 = K1.ⓑ{J1}W → + L2 = ⋆ ∨ ∃∃I2,K2. K1 ⊆ K2 & L2 = K2.ⓑ{I2}W. +#L1 #L2 * -L1 -L2 +[ #L #J1 #K1 #W #H destruct /2 width=1 by or_introl/ +| #I1 #I2 #L1 #L2 #V #HL12 #J1 #K1 #W #H destruct /3 width=4 by ex2_2_intro, or_intror/ +] +qed-. + +lemma lsuby_inv_pair1: ∀I1,K1,L2,W. K1.ⓑ{I1}W ⊆ L2 → + L2 = ⋆ ∨ ∃∃I2,K2. K1 ⊆ K2 & L2 = K2.ⓑ{I2}W. +/2 width=4 by lsuby_inv_pair1_aux/ qed-. + +fact lsuby_inv_pair2_aux: ∀L1,L2. L1 ⊆ L2 → ∀J2,K2,W. L2 = K2.ⓑ{J2}W → + ∃∃I1,K1. K1 ⊆ K2 & L1 = K1.ⓑ{I1}W. +#L1 #L2 * -L1 -L2 +[ #L #J2 #K2 #W #H destruct +| #I1 #I2 #L1 #L2 #V #HL12 #J2 #K2 #W #H destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lsuby_inv_pair2: ∀I2,L1,K2,W. L1 ⊆ K2.ⓑ{I2}W → + ∃∃I1,K1. K1 ⊆ K2 & L1 = K1.ⓑ{I1}W. +/2 width=4 by lsuby_inv_pair2_aux/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lsuby_fwd_length: ∀L1,L2. L1 ⊆ L2 → |L2| ≤ |L1|. +#L1 #L2 #H elim H -L1 -L2 /2 width=1 by monotonic_le_plus_l/ +qed-. + +lemma lsuby_ldrop_trans: ∀L1,L2. L1 ⊆ L2 → + ∀I2,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I2}W → + ∃∃I1,K1. K1 ⊆ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I1}W. +#L1 #L2 #H elim H -L1 -L2 +[ #L #J2 #K2 #W #s #i #H + elim (ldrop_inv_atom1 … H) -H #H destruct +| #I1 #I2 #L1 #L2 #V #HL12 #IHL12 #J2 #K2 #W #s #i #H + elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ] + [ /3 width=4 by ldrop_pair, ex2_2_intro/ + | elim (IHL12 … HLK2) -IHL12 -HLK2 * /3 width=4 by ldrop_drop_lt, ex2_2_intro/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys0/lsuby_lsuby.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys0/lsuby_lsuby.etc new file mode 100644 index 000000000..254d62928 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys0/lsuby_lsuby.etc @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/lsuby.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED SUBSTITUTION *******************) + +(* Main properties **********************************************************) + +theorem lsuby_trans: Transitive … lsuby. +#L1 #L #H elim H -L1 -L +[ #L1 #X #H lapply (lsuby_inv_atom1 … H) -H // +| #I1 #I #L1 #L #V #_ #IHL1 #X #H elim (lsuby_inv_pair1 … H) -H // * + #I2 #L2 #HL2 #H destruct /3 width=1 by lsuby_pair/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys0/psubstsnstar_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys0/psubstsnstar_3.etc new file mode 100644 index 000000000..0d6dffee6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys0/psubstsnstar_3.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ▶ * break term 46 L2 )" + non associative with precedence 45 + for @{ 'PSubstSnStar $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys0/psubststar_4.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys0/psubststar_4.etc new file mode 100644 index 000000000..0e76c6f71 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys0/psubststar_4.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 break ▶ * break term 46 T2 )" + non associative with precedence 45 + for @{ 'PSubstStar $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/cpx_cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/cpx_cpys.etc new file mode 100644 index 000000000..3b38ee6ab --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/cpx_cpys.etc @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpys_alt.ma". +include "basic_2/reduction/cpx.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) + +(* Properties on local environment refinement for extended substitution *****) + +lemma lsuby_cpx_trans: ∀h,g,G. lsub_trans … (cpx h g G) (lsuby 0 (∞)). +#h #g #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 +[ // +| /2 width=2 by cpx_sort/ +| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 + elim (lsuby_ldrop_trans_be … HL12 … HLK1) // -HL12 -HLK1 /3 width=7 by cpx_delta/ +|4,9: /4 width=1 by cpx_bind, cpx_beta, lsuby_pair_O_Y/ +|5,7,8: /3 width=1 by cpx_flat, cpx_tau, cpx_ti/ +|6,10: /4 width=3 by cpx_zeta, cpx_theta, lsuby_pair_O_Y/ +] +qed-. + +(* Properties on context-sensitive extended multiple substitution for terms *) + +lemma cpys_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2. +#h #g #G #L #T1 #T2 #d #e #H @(cpys_ind_alt … H) -G -L -T1 -T2 -d -e +/2 width=7 by cpx_delta, cpx_bind, cpx_flat/ +qed. + +lemma cpy_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2. +/3 width=3 by cpy_cpys, cpys_cpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/cpx_cpys2.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/cpx_cpys2.etc new file mode 100644 index 000000000..46abd5464 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/cpx_cpys2.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/substitution/cpys_alt.ma". +include "basic_2/reduction/cpx.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) + +(* Properties on context-sensitive extended multiple substitution for terms *) + +lemma cpys_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2. +#h #g #G #L #T1 #T2 #d #e #H @(cpys_ind_alt … H) -G -L -T1 -T2 -d -e +/2 width=7 by cpx_delta, cpx_bind, cpx_flat/ +qed. + +lemma cpy_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2. +/3 width=3 by cpy_cpys, cpys_cpx/ qed. + +lemma cpx_cpy_trans: ∀h,g,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T → + ∀T2,d,e. ⦃G, L⦄ ⊢ T ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2. +#h #g #G #L #T1 #T #H elim H -G -L -T1 -T +[ #I #G #L #X #d #e #H elim (cpy_inv_atom1 … H) // + * /2 width=3 by cpy_cpx/ +| #G #L #k #l #Hkl #X #d #e #H >(cpy_inv_sort1 … H) -X /2 width=2 by cpx_sort/ +| #I #G #L #K #V1 #V #W #i #HLK #_ #HVW #IHV1 #X #d #e #H + lapply (ldrop_fwd_drop2 … HLK) #H0 + lapply (cpy_weak … H 0 (∞) ? ?) -H // #H + elim (cpy_inv_lift1_be … H … H0 … HVW) -H -H0 -HVW + /3 width=7 by cpx_delta/ +| #a #I #G #L #V1 #V #T1 #T #_ #_ #IHV1 #IHT1 #X #d #e #H elim (cpy_inv_bind1 … H) -H + #V2 #T2 #HV2 #HT2 #H destruct + /5 width=7 by cpx_bind, lsuby_cpy_trans, lsuby_succ/ +| #I #G #L #V1 #V #T1 #T #_ #_ #IHV1 #IHT1 #X #d #e #H elim (cpy_inv_flat1 … H) -H + #V2 #T2 #HV2 #HT2 #H destruct /3 width=3 by cpx_flat/ +| #G #L #V1 #U1 #U #T #_ #HTU #IHU1 #T2 #d #e #HT2 + lapply (cpy_weak … HT2 0 (∞) ? ?) -HT2 // #HT2 + elim (lift_total T2 0 1) #U2 #HTU2 + lapply (cpy_lift_be … HT2 (L.ⓓV1) … (Ⓕ) … HTU … HTU2 ? ?) -T + /3 width=3 by cpx_zeta, ldrop_drop/ +| /3 width=3 by cpx_tau/ +| /3 width=3 by cpx_ti/ +| #a #G #L #V1 #V #W1 #W #T1 #T #_ #_ #_ #IHV1 #IHW1 #IHT1 #X #d #e #HX + elim (cpy_inv_bind1 … HX) -HX #Y #T2 #HY #HT2 #H destruct + elim (cpy_inv_flat1 … HY) -HY #W2 #V2 #HW2 #HV2 #H destruct + /5 width=7 by cpx_beta, lsuby_cpy_trans, lsuby_succ/ +| #a #G #L #V1 #V #U #W1 #W #T1 #T #_ #HVU #_ #_ #IHV1 #IHW1 #IHT1 #X #d #e #HX + elim (cpy_inv_bind1 … HX) -HX #W2 #Y #HW2 #HY #H destruct + elim (cpy_inv_flat1 … HY) -HY #U2 #T2 #HU2 #HT2 #H destruct + lapply (cpy_weak … HU2 0 (∞) ? ?) -HU2 // #HU2 + elim (cpy_inv_lift1_be … HU2 L … HVU) -U + /5 width=7 by cpx_theta, lsuby_cpy_trans, lsuby_succ, ldrop_drop/ +] +qed-. + +lemma cpx_cpys_trans: ∀h,g,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T → + ∀T2,d,e. ⦃G, L⦄ ⊢ T ▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2. +#h #g #G #L #T1 #T #HT1 #T2 #d #e #H @(cpys_ind … H) -T2 +/2 width=5 by cpx_cpy_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/cpxs_cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/cpxs_cpys.etc new file mode 100644 index 000000000..881030572 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/cpxs_cpys.etc @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reduction/cpx_cpys.ma". +include "basic_2/computation/cpxs.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) + +(* Properties on local environment refinement for extended substitution *****) + +lemma lsuby_cpxs_trans: ∀h,g,G. lsub_trans … (cpxs h g G) (lsuby 0 (∞)). +/3 width=5 by lsuby_cpx_trans, LTC_lsub_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/lpx_cpys.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/lpx_cpys.etc new file mode 100644 index 000000000..d3c490a89 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/lpx_cpys.etc @@ -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/relocation/cpy_lift.ma". +include "basic_2/substitution/cpys.ma". +include "basic_2/reduction/lpx_ldrop.ma". + +(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) + +(* Properties on context-sensitive extended substitution for terms **********) + +lemma cpx_cpy_trans_lpx: ∀h,g,G,L1,T1,T. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T → + ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → + ∀T2,d,e. ⦃G, L2⦄ ⊢ T ▶[d, e] T2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2. +#h #g #G #L1 #T1 #T #H elim H -G -L1 -T1 -T +[ #J #G #L1 #L2 #HL12 #T2 #d #e #H elim (cpy_inv_atom1 … H) -H // + * #I #K2 #V2 #i #_ #_ #HLK2 #HVT2 #H destruct + elim (lpx_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H + elim (lpx_inv_pair2 … H) -H #K1 #V1 #_ #HV12 #H destruct + /2 width=7 by cpx_delta/ +| #G #L1 #k #l #Hkl #L2 #_ #X #d #e #H >(cpy_inv_sort1 … H) -X /2 width=2 by cpx_sort/ +| #I #G #L1 #K1 #V1 #V #T #i #HLK1 #_ #HVT #IHV1 #L2 #HL12 #T2 #d #e #HT2 + elim (lpx_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 + elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct + lapply (ldrop_fwd_drop2 … HLK2) -V0 #HLK2 + lapply (cpy_weak … HT2 0 (∞) ? ?) -HT2 // #HT2 + elim (cpy_inv_lift1_be … HT2 … HLK2 … HVT) -HT2 -HLK2 -HVT + /3 width=7 by cpx_delta/ +| #a #I #G #L1 #V1 #V #T1 #T #HV1 #_ #IHV1 #IHT1 #L2 #HL12 #X #d #e #H elim (cpy_inv_bind1 … H) -H + #V2 #T2 #HV2 #HT2 #H destruct /4 width=5 by lpx_pair, cpx_bind/ +| #I #G #L1 #V1 #V #T1 #T #_ #_ #IHV1 #IHT1 #L2 #HL12 #X #d #e #H elim (cpy_inv_flat1 … H) -H + #V2 #T2 #HV2 #HT2 #H destruct /3 width=5 by cpx_flat/ +| #G #L1 #V1 #U1 #U #T #_ #HTU #IHU1 #L2 #HL12 #T2 #d #e #HT2 + lapply (cpy_weak … HT2 0 (∞) ? ?) -HT2 // #HT2 + elim (lift_total T2 0 1) #U2 #HTU2 + lapply (cpy_lift_be … HT2 (L2.ⓓV1) … (Ⓕ) … HTU … HTU2 ? ?) -T + /4 width=5 by cpx_zeta, lpx_pair, ldrop_drop/ +| /3 width=5 by cpx_tau/ +| /3 width=5 by cpx_ti/ +| #a #G #L1 #V1 #V #W1 #W #T1 #T #HV1 #HW1 #_ #IHV1 #IHW1 #IHT1 #L2 #HL12 #X #d #e #HX + elim (cpy_inv_bind1 … HX) -HX #Y #T2 #HY #HT2 #H destruct + elim (cpy_inv_flat1 … HY) -HY #W2 #V2 #HW2 #HV2 #H destruct + /5 width=11 by lpx_pair, cpx_beta, lsuby_cpy_trans, lsuby_succ/ +| #a #G #L1 #V1 #V #U #W1 #W #T1 #T #_ #HVU #HW1 #_ #IHV1 #IHW1 #IHT1 #L2 #HL12 #X #d #e #HX + elim (cpy_inv_bind1 … HX) -HX #W2 #Y #HW2 #HY #H destruct + elim (cpy_inv_flat1 … HY) -HY #U2 #T2 #HU2 #HT2 #H destruct + lapply (cpy_weak … HU2 0 (∞) ? ?) -HU2 // #HU2 + elim (cpy_inv_lift1_be … HU2 L2 … HVU) -U + /4 width=7 by lpx_pair, cpx_theta, ldrop_drop/ +] +qed-. + +lemma cpx_cpys_trans_lpx: ∀h,g,G,L1,T1,T. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T → + ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → + ∀T2,d,e. ⦃G, L2⦄ ⊢ T ▶*[d, e] T2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2. +#h #g #G #L1 #T1 #T #HT1 #L2 #HL12 #T2 #d #e #H @(cpys_ind … H) -T2 +/2 width=7 by cpx_cpy_trans_lpx/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/lsuby.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/lsuby.etc new file mode 100644 index 000000000..657ad6b6e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpys2/lsuby.etc @@ -0,0 +1,15 @@ +(* +lemma lsuby_weak: ∀L1,L2,d1,e1. L1 ⊑×[d1, e1] L2 → + ∀d2,e2. d1 ≤ d2 → e2 ≤ e1 → L1 ⊑×[d2, e2] L2. +#L1 #L2 #d1 #e1 #H elim H -L1 -L2 -d1 -e1 // +[ #I1 #I2 #L1 #L2 #V1 #V2 #HL12 #_ #d2 #e2 #_ #He21 + >(yle_inv_O2 … He21) -He21 + /4 width=3 by lsuby_fwd_length, lsuby_O1, monotonic_le_plus_l/ +| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #d2 #e2 #_ #He21 + elim (ynat_cases e2) /4 width=3 by lsuby_fwd_length, lsuby_O1, monotonic_le_plus_l/ + * #e0 #H destruct lapply (yle_inv_succ … He21) -He21 #He21 + elim (ynat_cases d2) /3 width=1 by lsuby_pair/ + * #d0 #H destruct @lsuby_succ @IHL12 // + [ destruct + +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cofreestar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cofreestar_4.ma deleted file mode 100644 index e73167c3f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cofreestar_4.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( L ⊢ break term 46 i ~ ϵ 𝐅 * [ break term 46 d ] ⦃ break term 46 T ⦄ )" - non associative with precedence 45 - for @{ 'CoFreeStar $L $i $d $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_4.ma new file mode 100644 index 000000000..4ce6d2dc7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_4.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( L ⊢ break term 46 i ϵ 𝐅 * [ break term 46 d ] ⦃ break term 46 T ⦄ )" + non associative with precedence 45 + for @{ 'FreeStar $L $i $d $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_frees.ma new file mode 100644 index 000000000..e303b8386 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_frees.ma @@ -0,0 +1,82 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fqup.ma". +include "basic_2/substitution/frees_lift.ma". +include "basic_2/reduction/lpx_ldrop.ma". + +(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) +(* +lemma yle_plus2_to_minus_inj2: ∀x,y:ynat. ∀z:nat. x ≤ y + z → x - z ≤ y. +/2 width=1 by monotonic_yle_minus_dx/ qed-. + +lemma yle_plus2_to_minus_inj1: ∀x,y:ynat. ∀z:nat. x ≤ z + y → x - z ≤ y. +/2 width=1 by yle_plus2_to_minus_inj2/ qed-. + +lemma cofrees_lsuby_conf: ∀L1,U,i. L1 ⊢ i ~ϵ 𝐅*⦃U⦄ → + ∀L2. lsuby L1 L2 → L2 ⊢ i ~ϵ 𝐅*⦃U⦄. +/3 width=3 by lsuby_cpys_trans/ qed-. + +lemma lpx_cpx_cofrees_conf: ∀h,g,G,L1,U1,U2. ⦃G, L1⦄ ⊢ U1 ➡[h, g] U2 → + ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → + ∀i. L1 ⊢ i ~ϵ 𝐅*⦃U1⦄ → L2 ⊢ i ~ϵ 𝐅*⦃U2⦄. +#h #g #G #L1 #U1 @(fqup_wf_ind_eq … G L1 U1) -G -L1 -U1 +#G0 #L0 #U0 #IH #G #L1 * * +[ -IH #k #HG #HL #HU #U2 #H elim (cpx_inv_sort1 … H) -H + [| * #l #_ ] #H destruct // +| #j #HG #HL #HU #U2 #H #L2 #HL12 #i #Hi elim (cpx_inv_lref1 … H) -H + [ #H destruct elim (lt_or_eq_or_gt i j) #Hji + [ -IH -HL12 /2 width=4 by cofrees_lref_gt/ + | -IH -HL12 destruct elim (cofrees_inv_lref_eq … Hi) + | elim (lt_or_ge j (|L2|)) /2 width=5 by cofrees_lref_free/ #Hj + elim (ldrop_O1_lt (Ⓕ) L1 j) [2: >(lpx_fwd_length … HL12) // ] #I #K1 #W1 #HLK1 + elim (lpx_ldrop_conf … HLK1 … HL12) -HL12 #Y #H #HLK2 + elim (lpx_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct + lapply (cofrees_inv_lref_lt … Hi … HLK1) -Hi // #HW1 + lapply (IH … HW12 … HK12 … HW1) /2 width=2 by fqup_lref/ -L1 -K1 -W1 #HW2 + /2 width=9 by cofrees_lref_lt/ (**) (* full auto too slow *) + ] + | * #I #K1 #W1 #W0 #HLK1 #HW10 #HW0U2 elim (lt_or_ge j i) #Hji + [ lapply (ldrop_fwd_drop2 … HLK1) #H0 + elim (lpx_ldrop_conf … H0 … HL12) #K2 #HK12 #HLK2 + @(cofrees_lift_ge … HLK2 … HW0U2) // + @(IH … HW10) /2 width=2 by fqup_lref/ -L2 -K2 -W0 -U2 -IH + (cpys_inv_sort1 … H) -X /2 width=2 by ex_intro/ -qed. - -lemma cofrees_gref: ∀L,d,i,p. L ⊢ i ~ϵ 𝐅*[d]⦃§p⦄. -#L #d #i #p #X #H >(cpys_inv_gref1 … H) -X /2 width=2 by ex_intro/ -qed. - -lemma cofrees_bind: ∀L,V,d,i. L ⊢ i ~ϵ 𝐅*[d] ⦃V⦄ → - ∀I,T. L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃T⦄ → - ∀a. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}V.T⦄. -#L #W1 #d #i #HW1 #I #U1 #HU1 #a #X #H elim (cpys_inv_bind1 … H) -H -#W2 #U2 #HW12 #HU12 #H destruct -elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_bind, ex_intro/ -qed. - -lemma cofrees_flat: ∀L,V,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ∀T. L ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → - ∀I. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}V.T⦄. -#L #W1 #d #i #HW1 #U1 #HU1 #I #X #H elim (cpys_inv_flat1 … H) -H -#W2 #U2 #HW12 #HU12 #H destruct -elim (HW1 … HW12) elim (HU1 … HU12) -W1 -U1 /3 width=2 by lift_flat, ex_intro/ -qed. - -lemma cofrees_cpy_trans: ∀L,U1,U2,d. ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 → - ∀i. L ⊢ i ~ϵ 𝐅*[d]⦃U1⦄ → L ⊢ i ~ϵ 𝐅*[d]⦃U2⦄. -/3 width=3 by cpys_strap2/ qed-. - -axiom cofrees_dec: ∀L,T,d,i. Decidable (L ⊢ i ~ϵ 𝐅*[d]⦃T⦄). - -(* Basic negated properties *************************************************) - -lemma frees_cpy_div: ∀L,U1,U2,d. ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 → - ∀i. (L ⊢ i ~ϵ 𝐅*[d]⦃U2⦄ → ⊥) → (L ⊢ i ~ϵ 𝐅*[d]⦃U1⦄ → ⊥). -/3 width=7 by cofrees_cpy_trans/ qed-. - -(* Basic negated inversion lemmas *******************************************) - -lemma frees_inv_bind: ∀a,I,L,V,T,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}V.T⦄ → ⊥) → - (L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ⊥) ∨ (L.ⓑ{I}V ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃T⦄ → ⊥). -#a #I #L #W #U #d #i #H elim (cofrees_dec L W d i) -/4 width=9 by cofrees_bind, or_intror, or_introl/ -qed-. - -lemma frees_inv_flat: ∀I,L,V,T,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}V.T⦄ → ⊥) → - (L ⊢ i ~ϵ 𝐅*[d]⦃V⦄ → ⊥) ∨ (L ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥). -#I #L #W #U #d #H elim (cofrees_dec L W d) -/4 width=8 by cofrees_flat, or_intror, or_introl/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees_alt.ma deleted file mode 100644 index 7bb9c9ca7..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees_alt.ma +++ /dev/null @@ -1,54 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/relocation/cpy_nlift.ma". -include "basic_2/substitution/cofrees_lift.ma". - -(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************) - -(* Alternative definition of frees_ge ***************************************) - -lemma nlift_frees: ∀L,U,d,i. (∀T. ⇧[i, 1] T ≡ U → ⊥) → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥). -#L #U #d #i #HnTU #H elim (cofrees_fwd_lift … H) -H /2 width=2 by/ -qed-. - -lemma frees_inv_ge: ∀L,U,d,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → - (∀T. ⇧[i, 1] T ≡ U → ⊥) ∨ - ∃∃I,K,W,j. d ≤ yinj j & j < i & ⇩[j]L ≡ K.ⓑ{I}W & - (K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄ → ⊥) & (∀T. ⇧[j, 1] T ≡ U → ⊥). -#L #U #d #i #Hdi #H @(frees_ind … H) -U /3 width=2 by or_introl/ -#U1 #U2 #HU12 #HU2 * -[ #HnU2 elim (cpy_fwd_nlift2_ge … HU12 … HnU2) -HU12 -HnU2 /3 width=2 by or_introl/ - * /5 width=9 by nlift_frees, ex5_4_intro, or_intror/ -| * #I2 #K2 #W2 #j2 #Hdj2 #Hj2i #HLK2 #HnW2 #HnU2 elim (cpy_fwd_nlift2_ge … HU12 … HnU2) -HU12 -HnU2 /4 width=9 by ex5_4_intro, or_intror/ - * #I1 #K1 #W1 #j1 #Hdj1 #Hj12 #HLK1 #HnW1 #HnU1 - lapply (ldrop_conf_ge … HLK1 … HLK2 ?) -HLK2 /2 width=1 by lt_to_le/ - #HK12 lapply (ldrop_inv_drop1_lt … HK12 ?) /2 width=1 by lt_plus_to_minus_r/ -HK12 - #HK12 - @or_intror @(ex5_4_intro … HLK1 … HnU1) -HLK1 -HnU1 /2 width=3 by transitive_lt/ - @(frees_be … HK12 … HnW1) /2 width=1 by arith_k_sn/ -HK12 -HnW1 - >minus_plus in ⊢ (??(?(?%?)?)??→?); >minus_plus in ⊢ (??(?(??%)?)??→?); >arith_b1 /2 width=1 by/ -] -qed-. - -lemma frees_ind_ge: ∀R:relation4 ynat nat lenv term. - (∀d,i,L,U. d ≤ yinj i → (∀T. ⇧[i, 1] T ≡ U → ⊥) → R d i L U) → - (∀d,i,j,I,L,K,W,U. d ≤ yinj j → j < i → ⇩[j]L ≡ K.ⓑ{I}W → (K ⊢ i-j-1 ~ϵ 𝐅*[0]⦃W⦄ → ⊥) → (∀T. ⇧[j, 1] T ≡ U → ⊥) → R 0 (i-j-1) K W → R d i L U) → - ∀d,i,L,U. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R d i L U. -#R #IH1 #IH2 #d #i #L #U -generalize in match d; -d generalize in match i; -i -@(f2_ind … rfw … L U) -L -U -#n #IHn #L #U #Hn #i #d #Hdi #H elim (frees_inv_ge … H) -H /3 width=2 by/ --IH1 * #I #K #W #j #Hdj #Hji #HLK #HnW #HnU destruct /4 width=12 by ldrop_fwd_rfw/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees_lift.ma deleted file mode 100644 index 7dea71858..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees_lift.ma +++ /dev/null @@ -1,144 +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/cpys_lift.ma". -include "basic_2/substitution/cofrees.ma". - -(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************) - -(* Advanced inversion lemmas ************************************************) - -lemma cofrees_inv_lref_be: ∀L,d,i,j. L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄ → d ≤ yinj j → j < i → - ∀I,K,W. ⇩[j]L ≡ K.ⓑ{I}W → K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄. -#L #d #i #j #Hj #Hdj #Hji #I #K #W1 #HLK #W2 #HW12 elim (lift_total W2 0 (j+1)) -#X2 #HWX2 elim (Hj X2) /2 width=7 by cpys_subst_Y2/ -I -L -K -W1 -d -#Z2 #HZX2 elim (lift_div_le … HWX2 (i-j-1) 1 Z2) -HWX2 /2 width=2 by ex_intro/ ->minus_plus minus_plus_plus_l // -| #J #W #U #Hn #d #i #H1 #j #H2 #I #K #V #HLK #Hdj #Hji destruct - elim (cofrees_inv_flat … H1) -H1 #HW #HU - elim (nlift_inv_flat … H2) -H2 [ /3 width=9 by/ ] - #HnU @(IH … HU … HnU … HLK) // (**) (* full auto fails *) -] -qed-. - -(* Advanced properties ******************************************************) - -lemma cofrees_lref_skip: ∀L,d,i,j. j < i → yinj j < d → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄. -#L #d #i #j #Hji #Hjd #X #H elim (cpys_inv_lref1_Y2 … H) -H -[ #H destruct /3 width=2 by lift_lref_lt, ex_intro/ -| * #I #K #W1 #W2 #Hdj elim (ylt_yle_false … Hdj) -i -I -L -K -W1 -W2 -X // -] -qed. - -lemma cofrees_lref_lt: ∀L,d,i,j. i < j → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄. -#L #d #i #j #Hij #X #H elim (cpys_inv_lref1_Y2 … H) -H -[ #H destruct /3 width=2 by lift_lref_ge_minus, ex_intro/ -| * #I #K #V1 #V2 #_ #_ #_ #H -I -L -K -V1 -d - elim (lift_split … H i j) /2 width=2 by lt_to_le, ex_intro/ -] -qed. - -lemma cofrees_lref_gt: ∀I,L,K,W,d,i,j. j < i → ⇩[j] L ≡ K.ⓑ{I}W → - K ⊢ (i-j-1) ~ϵ 𝐅*[O]⦃W⦄ → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄. -#I #L #K #W1 #d #i #j #Hji #HLK #HW1 #X #H elim (cpys_inv_lref1_Y2 … H) -H -[ #H destruct /3 width=2 by lift_lref_lt, ex_intro/ -| * #I0 #K0 #W0 #W2 #Hdj #HLK0 #HW12 #HW2 lapply (ldrop_mono … HLK0 … HLK) -L - #H destruct elim (HW1 … HW12) -I -K -W1 -d - #V2 #HVW2 elim (lift_trans_le … HVW2 … HW2) -W2 // - >minus_plus minus_plus (nlift_inv_lref_be_SO … Hnx) -x /3 width=5 by ex4_3_intro, or_intror/ +] +qed-. + +lemma frees_inv_lref_free: ∀L,d,j,i. L ⊢ i ϵ 𝐅*[d]⦃#j⦄ → |L| ≤ j → j = i. +#L #d #j #i #H #Hj elim (frees_inv_lref … H) -H // +* #I #K #W #_ #_ #HLK lapply (ldrop_fwd_length_lt2 … HLK) -I +#H elim (lt_refl_false j) /2 width=3 by lt_to_le_to_lt/ +qed-. + +lemma frees_inv_lref_skip: ∀L,d,j,i. L ⊢ i ϵ 𝐅*[d]⦃#j⦄ → yinj j < d → j = i. +#L #d #j #i #H #Hjd elim (frees_inv_lref … H) -H // +* #I #K #W #Hdj elim (ylt_yle_false … Hdj) -Hdj // +qed-. + +lemma frees_inv_lref_ge: ∀L,d,j,i. L ⊢ i ϵ 𝐅*[d]⦃#j⦄ → i ≤ j → j = i. +#L #d #j #i #H #Hij elim (frees_inv_lref … H) -H // +* #I #K #W #_ #Hji elim (lt_refl_false j) -I -L -K -W -d /2 width=3 by lt_to_le_to_lt/ +qed-. + +lemma frees_inv_lref_lt: ∀L,d,j,i.L ⊢ i ϵ 𝐅*[d]⦃#j⦄ → j < i → + ∃∃I,K,W. d ≤ yinj j & ⇩[j] L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄. +#L #d #j #i #H #Hji elim (frees_inv_lref … H) -H +[ #H elim (lt_refl_false j) // +| * /2 width=5 by ex3_3_intro/ +] +qed-. + +lemma frees_inv_bind: ∀a,I,L,W,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄ → + L ⊢ i ϵ 𝐅*[d]⦃W⦄ ∨ L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[⫯d]⦃U⦄ . +#a #J #L #V #U #d #i #H elim (frees_inv … H) -H +[ #HnX elim (nlift_inv_bind … HnX) -HnX + /4 width=2 by frees_eq, or_intror, or_introl/ +| * #I #K #W #j #Hdj #Hji #HnX #HLK #HW elim (nlift_inv_bind … HnX) -HnX + [ /4 width=9 by frees_be, or_introl/ + | #HnT @or_intror @(frees_be … HnT) -HnT + [4,5,6: /2 width=1 by ldrop_drop, yle_succ, lt_minus_to_plus/ + |7: >minus_plus_plus_l // + |*: skip + ] + ] +] +qed-. + +lemma frees_inv_flat: ∀I,L,W,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄ → + L ⊢ i ϵ 𝐅*[d]⦃W⦄ ∨ L ⊢ i ϵ 𝐅*[d]⦃U⦄ . +#J #L #V #U #d #i #H elim (frees_inv … H) -H +[ #HnX elim (nlift_inv_flat … HnX) -HnX + /4 width=2 by frees_eq, or_intror, or_introl/ +| * #I #K #W #j #Hdj #Hji #HnX #HLK #HW elim (nlift_inv_flat … HnX) -HnX + /4 width=9 by frees_be, or_intror, or_introl/ +] +qed-. + +(* Basic properties *********************************************************) + +lemma frees_lref_eq: ∀L,d,i. L ⊢ i ϵ 𝐅*[d]⦃#i⦄. +/3 width=7 by frees_eq, lift_inv_lref2_be/ qed. + +lemma frees_lref_be: ∀I,L,K,W,d,i,j. d ≤ yinj j → j < i → ⇩[j]L ≡ K.ⓑ{I}W → + K ⊢ i-j-1 ϵ 𝐅*[0]⦃W⦄ → L ⊢ i ϵ 𝐅*[d]⦃#j⦄. +/3 width=9 by frees_be, lift_inv_lref2_be/ qed. + +lemma frees_bind_sn: ∀a,I,L,W,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃W⦄ → + L ⊢ i ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄. +#a #I #L #W #U #d #i #H elim (frees_inv … H) -H [|*] +/4 width=9 by frees_be, frees_eq, nlift_bind_sn/ +qed. + +lemma frees_bind_dx: ∀a,I,L,W,U,d,i. L.ⓑ{I}W ⊢ i+1 ϵ 𝐅*[⫯d]⦃U⦄ → + L ⊢ i ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄. +#a #J #L #V #U #d #i #H elim (frees_inv … H) -H +[ /4 width=9 by frees_eq, nlift_bind_dx/ +| * #I #K #W #j #Hdj #Hji #HnU #HLK #HW + elim (yle_inv_succ1 … Hdj) -Hdj (plus_minus_m_m j 1) in HnU; //