From: Ferruccio Guidi Date: Sun, 11 Oct 2015 15:02:58 +0000 (+0000) Subject: ground_2: added missing file X-Git-Tag: make_still_working~687 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=44211a20a89241616eca9afaf9dd8dab6139c571;p=helm.git ground_2: added missing file basic_2: commit of grammar completed --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.etc new file mode 100644 index 000000000..fd7ba1c91 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.etc @@ -0,0 +1,170 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/ynat/ynat_plus.ma". +include "basic_2/notation/relations/freestar_4.ma". +include "basic_2/substitution/lift_neg.ma". +include "basic_2/substitution/drop.ma". + +(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) + +inductive frees: relation4 ynat lenv term ynat ≝ +| frees_eq: ∀L,U,l,i. (∀T. ⬆[i, 1] T ≡ U → ⊥) → frees l L U i +| frees_be: ∀I,L,K,U,W,l,i,j. l ≤ yinj j → yinj j < i → + (∀T. ⬆[j, 1] T ≡ U → ⊥) → ⬇[j]L ≡ K.ⓑ{I}W → + frees 0 K W (⫰(i-j)) → frees l L U i. + +interpretation + "context-sensitive free variables (term)" + 'FreeStar L i l U = (frees l L U i). + +definition frees_trans: predicate (relation3 lenv term term) ≝ + λR. ∀L,U1,U2,i. R L U1 U2 → L ⊢ i ϵ 𝐅*[0]⦃U2⦄ → L ⊢ i ϵ 𝐅*[0]⦃U1⦄. + +(* Basic inversion lemmas ***************************************************) + +lemma frees_inv: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ → + (∀T. ⬆[i, 1] T ≡ U → ⊥) ∨ + ∃∃I,K,W,j. l ≤ yinj j & j < i & (∀T. ⬆[j, 1] T ≡ U → ⊥) & + ⬇[j]L ≡ K.ⓑ{I}W & K ⊢ ⫰(i-j) ϵ 𝐅*[yinj 0]⦃W⦄. +#L #U #l #i * -L -U -l -i /4 width=9 by ex5_4_intro, or_intror, or_introl/ +qed-. + +lemma frees_inv_sort: ∀L,l,i,k. L ⊢ i ϵ 𝐅*[l]⦃⋆k⦄ → ⊥. +#L #l #i #k #H elim (frees_inv … H) -H [|*] /2 width=2 by/ +qed-. + +lemma frees_inv_gref: ∀L,l,i,p. L ⊢ i ϵ 𝐅*[l]⦃§p⦄ → ⊥. +#L #l #i #p #H elim (frees_inv … H) -H [|*] /2 width=2 by/ +qed-. + +lemma frees_inv_lref: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → + yinj j = i ∨ + ∃∃I,K,W. l ≤ yinj j & yinj j < i & ⬇[j] L ≡ K.ⓑ{I}W & K ⊢ ⫰(i-j) ϵ 𝐅*[yinj 0]⦃W⦄. +#L #l #x #i #H elim (frees_inv … H) -H +[ /4 width=2 by nlift_inv_lref_be_SO, or_introl/ +| * #I #K #W #j #Hlj #Hji #Hnx #HLK #HW + lapply (nlift_inv_lref_be_SO … Hnx) -Hnx #H + lapply (yinj_inj … H) -H #H destruct + /3 width=5 by ex4_3_intro, or_intror/ +] +qed-. + +lemma frees_inv_lref_free: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → |L| ≤ j → yinj j = i. +#L #l #j #i #H #Hj elim (frees_inv_lref … H) -H // +* #I #K #W #_ #_ #HLK lapply (drop_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,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → yinj j < l → yinj j = i. +#L #l #j #i #H #Hjl elim (frees_inv_lref … H) -H // +* #I #K #W #Hlj elim (ylt_yle_false … Hlj) -Hlj // +qed-. + +lemma frees_inv_lref_ge: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → i ≤ j → yinj j = i. +#L #l #j #i #H #Hij elim (frees_inv_lref … H) -H // +* #I #K #W #_ #Hji elim (ylt_yle_false … Hji Hij) +qed-. + +lemma frees_inv_lref_lt: ∀L,l,j,i.L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → j < i → + ∃∃I,K,W. l ≤ yinj j & ⬇[j] L ≡ K.ⓑ{I}W & K ⊢ ⫰(i-j) ϵ 𝐅*[yinj 0]⦃W⦄. +#L #l #j #i #H #Hji elim (frees_inv_lref … H) -H +[ #H elim (ylt_yle_false … Hji) // +| * /2 width=5 by ex3_3_intro/ +] +qed-. + +lemma frees_inv_bind: ∀a,I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃ⓑ{a,I}W.U⦄ → + L ⊢ i ϵ 𝐅*[l]⦃W⦄ ∨ L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[⫯l]⦃U⦄ . +#a #J #L #V #U #l #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 #Hlj #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: lapply (yle_succ … Hlj) // (**) + |5: lapply (ylt_succ … Hji) // (**) + |6: /2 width=4 by drop_drop/ + |7: yminus_succ + lapply (ylt_O … Hj) -Hj #Hj #H + lapply (ylt_inv_succ … H) -H #Hji #HnU #HLK #HW + @(frees_be … Hlj Hji … HW) -HW -Hlj -Hji (**) (* explicit constructor *) + [2: #X #H lapply (nlift_bind_dx … H) /2 width=2 by/ (**) + |3: lapply (drop_inv_drop1_lt … HLK ?) -HLK // + |*: skip +] +qed. + +lemma frees_flat_sn: ∀I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃W⦄ → + L ⊢ i ϵ 𝐅*[l]⦃ⓕ{I}W.U⦄. +#I #L #W #U #l #i #H elim (frees_inv … H) -H [|*] +/4 width=9 by frees_be, frees_eq, nlift_flat_sn/ +qed. + +lemma frees_flat_dx: ∀I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ → + L ⊢ i ϵ 𝐅*[l]⦃ⓕ{I}W.U⦄. +#I #L #W #U #l #i #H elim (frees_inv … H) -H [|*] +/4 width=9 by frees_be, frees_eq, nlift_flat_dx/ +qed. + +lemma frees_weak: ∀L,U,l1,i. L ⊢ i ϵ 𝐅*[l1]⦃U⦄ → + ∀l2. l2 ≤ l1 → L ⊢ i ϵ 𝐅*[l2]⦃U⦄. +#L #U #l1 #i #H elim H -L -U -l1 -i +/3 width=9 by frees_be, frees_eq, yle_trans/ +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma frees_inv_bind_O: ∀a,I,L,W,U,i. L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄ → + L ⊢ i ϵ 𝐅*[0]⦃W⦄ ∨ L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ . +#a #I #L #W #U #i #H elim (frees_inv_bind … H) -H +/3 width=3 by frees_weak, or_intror, or_introl/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.ma deleted file mode 100644 index fd7ba1c91..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.ma +++ /dev/null @@ -1,170 +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 "ground_2/ynat/ynat_plus.ma". -include "basic_2/notation/relations/freestar_4.ma". -include "basic_2/substitution/lift_neg.ma". -include "basic_2/substitution/drop.ma". - -(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) - -inductive frees: relation4 ynat lenv term ynat ≝ -| frees_eq: ∀L,U,l,i. (∀T. ⬆[i, 1] T ≡ U → ⊥) → frees l L U i -| frees_be: ∀I,L,K,U,W,l,i,j. l ≤ yinj j → yinj j < i → - (∀T. ⬆[j, 1] T ≡ U → ⊥) → ⬇[j]L ≡ K.ⓑ{I}W → - frees 0 K W (⫰(i-j)) → frees l L U i. - -interpretation - "context-sensitive free variables (term)" - 'FreeStar L i l U = (frees l L U i). - -definition frees_trans: predicate (relation3 lenv term term) ≝ - λR. ∀L,U1,U2,i. R L U1 U2 → L ⊢ i ϵ 𝐅*[0]⦃U2⦄ → L ⊢ i ϵ 𝐅*[0]⦃U1⦄. - -(* Basic inversion lemmas ***************************************************) - -lemma frees_inv: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ → - (∀T. ⬆[i, 1] T ≡ U → ⊥) ∨ - ∃∃I,K,W,j. l ≤ yinj j & j < i & (∀T. ⬆[j, 1] T ≡ U → ⊥) & - ⬇[j]L ≡ K.ⓑ{I}W & K ⊢ ⫰(i-j) ϵ 𝐅*[yinj 0]⦃W⦄. -#L #U #l #i * -L -U -l -i /4 width=9 by ex5_4_intro, or_intror, or_introl/ -qed-. - -lemma frees_inv_sort: ∀L,l,i,k. L ⊢ i ϵ 𝐅*[l]⦃⋆k⦄ → ⊥. -#L #l #i #k #H elim (frees_inv … H) -H [|*] /2 width=2 by/ -qed-. - -lemma frees_inv_gref: ∀L,l,i,p. L ⊢ i ϵ 𝐅*[l]⦃§p⦄ → ⊥. -#L #l #i #p #H elim (frees_inv … H) -H [|*] /2 width=2 by/ -qed-. - -lemma frees_inv_lref: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → - yinj j = i ∨ - ∃∃I,K,W. l ≤ yinj j & yinj j < i & ⬇[j] L ≡ K.ⓑ{I}W & K ⊢ ⫰(i-j) ϵ 𝐅*[yinj 0]⦃W⦄. -#L #l #x #i #H elim (frees_inv … H) -H -[ /4 width=2 by nlift_inv_lref_be_SO, or_introl/ -| * #I #K #W #j #Hlj #Hji #Hnx #HLK #HW - lapply (nlift_inv_lref_be_SO … Hnx) -Hnx #H - lapply (yinj_inj … H) -H #H destruct - /3 width=5 by ex4_3_intro, or_intror/ -] -qed-. - -lemma frees_inv_lref_free: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → |L| ≤ j → yinj j = i. -#L #l #j #i #H #Hj elim (frees_inv_lref … H) -H // -* #I #K #W #_ #_ #HLK lapply (drop_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,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → yinj j < l → yinj j = i. -#L #l #j #i #H #Hjl elim (frees_inv_lref … H) -H // -* #I #K #W #Hlj elim (ylt_yle_false … Hlj) -Hlj // -qed-. - -lemma frees_inv_lref_ge: ∀L,l,j,i. L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → i ≤ j → yinj j = i. -#L #l #j #i #H #Hij elim (frees_inv_lref … H) -H // -* #I #K #W #_ #Hji elim (ylt_yle_false … Hji Hij) -qed-. - -lemma frees_inv_lref_lt: ∀L,l,j,i.L ⊢ i ϵ 𝐅*[l]⦃#j⦄ → j < i → - ∃∃I,K,W. l ≤ yinj j & ⬇[j] L ≡ K.ⓑ{I}W & K ⊢ ⫰(i-j) ϵ 𝐅*[yinj 0]⦃W⦄. -#L #l #j #i #H #Hji elim (frees_inv_lref … H) -H -[ #H elim (ylt_yle_false … Hji) // -| * /2 width=5 by ex3_3_intro/ -] -qed-. - -lemma frees_inv_bind: ∀a,I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃ⓑ{a,I}W.U⦄ → - L ⊢ i ϵ 𝐅*[l]⦃W⦄ ∨ L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[⫯l]⦃U⦄ . -#a #J #L #V #U #l #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 #Hlj #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: lapply (yle_succ … Hlj) // (**) - |5: lapply (ylt_succ … Hji) // (**) - |6: /2 width=4 by drop_drop/ - |7: yminus_succ - lapply (ylt_O … Hj) -Hj #Hj #H - lapply (ylt_inv_succ … H) -H #Hji #HnU #HLK #HW - @(frees_be … Hlj Hji … HW) -HW -Hlj -Hji (**) (* explicit constructor *) - [2: #X #H lapply (nlift_bind_dx … H) /2 width=2 by/ (**) - |3: lapply (drop_inv_drop1_lt … HLK ?) -HLK // - |*: skip -] -qed. - -lemma frees_flat_sn: ∀I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃W⦄ → - L ⊢ i ϵ 𝐅*[l]⦃ⓕ{I}W.U⦄. -#I #L #W #U #l #i #H elim (frees_inv … H) -H [|*] -/4 width=9 by frees_be, frees_eq, nlift_flat_sn/ -qed. - -lemma frees_flat_dx: ∀I,L,W,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ → - L ⊢ i ϵ 𝐅*[l]⦃ⓕ{I}W.U⦄. -#I #L #W #U #l #i #H elim (frees_inv … H) -H [|*] -/4 width=9 by frees_be, frees_eq, nlift_flat_dx/ -qed. - -lemma frees_weak: ∀L,U,l1,i. L ⊢ i ϵ 𝐅*[l1]⦃U⦄ → - ∀l2. l2 ≤ l1 → L ⊢ i ϵ 𝐅*[l2]⦃U⦄. -#L #U #l1 #i #H elim H -L -U -l1 -i -/3 width=9 by frees_be, frees_eq, yle_trans/ -qed-. - -(* Advanced inversion lemmas ************************************************) - -lemma frees_inv_bind_O: ∀a,I,L,W,U,i. L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄ → - L ⊢ i ϵ 𝐅*[0]⦃W⦄ ∨ L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ . -#a #I #L #W #U #i #H elim (frees_inv_bind … H) -H -/3 width=3 by frees_weak, or_intror, or_introl/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_append.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_append.etc new file mode 100644 index 000000000..ee8324cc9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_append.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/substitution/drop_append.ma". +include "basic_2/multiple/frees.ma". + +(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) + +(* Properties on append for local environments ******************************) + +lemma frees_append: ∀L2,U,l,i. L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ → i ≤ |L2| → + ∀L1. L1 @@ L2 ⊢ i ϵ 𝐅*[l]⦃U⦄. +#L2 #U #l #i #H elim H -L2 -U -l -i /3 width=2 by frees_eq/ +#I #L2 #K2 #U #W #l #i #j #Hlj #Hji #HnU #HLK2 #_ #IHW #Hi #L1 +lapply (drop_fwd_length_minus2 … HLK2) normalize #H0 +lapply (drop_O1_append_sn_le … HLK2 … L1) -HLK2 +[ -I -L1 -K2 -U -W -l /4 width=3 by ylt_yle_trans, ylt_inv_inj, lt_to_le/ +| #HLK2 @(frees_be … HnU HLK2) // -HnU -HLK2 @IHW -IHW + >(minus_plus_m_m (|K2|) 1) >H0 -H0 yminus_SO2 + /3 width=1 by monotonic_yle_minus_dx, yle_pred/ +] +qed. + +(* Inversion lemmas on append for local environments ************************) + +fact frees_inv_append_aux: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ → ∀L1,L2. L = L1 @@ L2 → + i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄. +#L #U #l #i #H elim H -L -U -l -i /3 width=2 by frees_eq/ +#Z #L #Y #U #X #l #i #j #Hlj #Hji #HnU #HLY #_ #IHW #L1 #L2 #H #Hi destruct +elim (drop_O1_lt (Ⓕ) L2 j) [2: -Z -Y -L1 -X -U -l /3 width=3 by ylt_yle_trans, ylt_inv_inj/ ] +#I #K2 #W #HLK2 lapply (drop_fwd_length_minus2 … HLK2) normalize #H0 +lapply (drop_O1_inv_append1_le … HLY … HLK2) -HLY +[ -Z -I -Y -K2 -L1 -X -U -W -l /4 width=3 by ylt_yle_trans, ylt_inv_inj, lt_to_le/ +| normalize #H destruct + @(frees_be … HnU HLK2) -HnU -HLK2 // @IHW -IHW // + >(minus_plus_m_m (|K2|) 1) >H0 -H0 yminus_SO2 + /3 width=1 by monotonic_yle_minus_dx, yle_pred/ +] +qed-. + +lemma frees_inv_append: ∀L1,L2,U,l,i. L1 @@ L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ → + i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄. +/2 width=4 by frees_inv_append_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_append.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_append.ma deleted file mode 100644 index ee8324cc9..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_append.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/substitution/drop_append.ma". -include "basic_2/multiple/frees.ma". - -(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) - -(* Properties on append for local environments ******************************) - -lemma frees_append: ∀L2,U,l,i. L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ → i ≤ |L2| → - ∀L1. L1 @@ L2 ⊢ i ϵ 𝐅*[l]⦃U⦄. -#L2 #U #l #i #H elim H -L2 -U -l -i /3 width=2 by frees_eq/ -#I #L2 #K2 #U #W #l #i #j #Hlj #Hji #HnU #HLK2 #_ #IHW #Hi #L1 -lapply (drop_fwd_length_minus2 … HLK2) normalize #H0 -lapply (drop_O1_append_sn_le … HLK2 … L1) -HLK2 -[ -I -L1 -K2 -U -W -l /4 width=3 by ylt_yle_trans, ylt_inv_inj, lt_to_le/ -| #HLK2 @(frees_be … HnU HLK2) // -HnU -HLK2 @IHW -IHW - >(minus_plus_m_m (|K2|) 1) >H0 -H0 yminus_SO2 - /3 width=1 by monotonic_yle_minus_dx, yle_pred/ -] -qed. - -(* Inversion lemmas on append for local environments ************************) - -fact frees_inv_append_aux: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ → ∀L1,L2. L = L1 @@ L2 → - i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄. -#L #U #l #i #H elim H -L -U -l -i /3 width=2 by frees_eq/ -#Z #L #Y #U #X #l #i #j #Hlj #Hji #HnU #HLY #_ #IHW #L1 #L2 #H #Hi destruct -elim (drop_O1_lt (Ⓕ) L2 j) [2: -Z -Y -L1 -X -U -l /3 width=3 by ylt_yle_trans, ylt_inv_inj/ ] -#I #K2 #W #HLK2 lapply (drop_fwd_length_minus2 … HLK2) normalize #H0 -lapply (drop_O1_inv_append1_le … HLY … HLK2) -HLY -[ -Z -I -Y -K2 -L1 -X -U -W -l /4 width=3 by ylt_yle_trans, ylt_inv_inj, lt_to_le/ -| normalize #H destruct - @(frees_be … HnU HLK2) -HnU -HLK2 // @IHW -IHW // - >(minus_plus_m_m (|K2|) 1) >H0 -H0 yminus_SO2 - /3 width=1 by monotonic_yle_minus_dx, yle_pred/ -] -qed-. - -lemma frees_inv_append: ∀L1,L2,U,l,i. L1 @@ L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ → - i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄. -/2 width=4 by frees_inv_append_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lift.etc new file mode 100644 index 000000000..65b629206 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lift.etc @@ -0,0 +1,170 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/ynat/ynat_max.ma". +include "basic_2/substitution/drop_drop.ma". +include "basic_2/multiple/frees.ma". + +(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) + +(* Advanced properties ******************************************************) + +lemma frees_dec: ∀L,U,l,i. Decidable (frees l L U i). +#L #U @(f2_ind … rfw … L U) -L -U +#x #IH #L * * +[ -IH /3 width=5 by frees_inv_sort, or_intror/ +| #j #Hx #l #i elim (ylt_split_eq i j) #Hji + [ -x @or_intror #H elim (ylt_yle_false … Hji) + lapply (frees_inv_lref_ge … H ?) -L -l /2 width=1 by ylt_fwd_le/ + | -x /2 width=1 by or_introl/ + | elim (ylt_split j l) #Hli + [ -x @or_intror #H elim (ylt_yle_false … Hji) + lapply (frees_inv_lref_skip … H ?) -L // + | elim (lt_or_ge j (|L|)) #Hj + [ elim (drop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct + elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, drop_fwd_rfw, or_introl/ ] #HnW + @or_intror #H elim (frees_inv_lref_lt … H) // #Z #Y #X #_ #HLY -l + lapply (drop_mono … HLY … HLK) -L #H destruct /2 width=1 by/ + | -x @or_intror #H elim (ylt_yle_false … Hji) + lapply (frees_inv_lref_free … H ?) -l // + ] + ] + ] +| -IH /3 width=5 by frees_inv_gref, or_intror/ +| #a #I #W #U #Hx #l #i destruct + elim (IH L W … l i) [1,3: /3 width=1 by frees_bind_sn, or_introl/ ] #HnW + elim (IH (L.ⓑ{I}W) U … (⫯l) (i+1)) -IH [1,3: /3 width=1 by frees_bind_dx, or_introl/ ] #HnU + @or_intror #H elim (frees_inv_bind … H) -H /2 width=1 by/ +| #I #W #U #Hx #l #i destruct + elim (IH L W … l i) [1,3: /3 width=1 by frees_flat_sn, or_introl/ ] #HnW + elim (IH L U … l i) -IH [1,3: /3 width=1 by frees_flat_dx, or_introl/ ] #HnU + @or_intror #H elim (frees_inv_flat … H) -H /2 width=1 by/ +] +qed-. + +lemma frees_S: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[yinj l]⦃U⦄ → ∀I,K,W. ⬇[l] L ≡ K.ⓑ{I}W → + (K ⊢ ⫰(i-l) ϵ 𝐅*[0]⦃W⦄ → ⊥) → L ⊢ i ϵ 𝐅*[⫯l]⦃U⦄. +#L #U #l #i #H elim (frees_inv … H) -H /3 width=2 by frees_eq/ +* #I #K #W #j #Hlj #Hji #HnU #HLK #HW #I0 #K0 #W0 #HLK0 #HnW0 +lapply (yle_inv_inj … Hlj) -Hlj #Hlj +elim (le_to_or_lt_eq … Hlj) -Hlj +[ -I0 -K0 -W0 /3 width=9 by frees_be, yle_inj/ +| -Hji -HnU #H destruct + lapply (drop_mono … HLK0 … HLK) #H destruct -I + elim HnW0 -L -U -HnW0 // +] +qed. + +(* Note: lemma 1250 *) +lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ → + L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄. +#a #I #L #W #U #i #HU elim (frees_dec L W 0 i) +/4 width=5 by frees_S, frees_bind_dx, frees_bind_sn/ +qed. + +(* Properties on relocation *************************************************) + +lemma frees_lift_ge: ∀K,T,l,i. K ⊢ i ϵ𝐅*[l]⦃T⦄ → + ∀L,s,l0,m0. ⬇[s, l0, m0] L ≡ K → + ∀U. ⬆[l0, m0] T ≡ U → l0 ≤ i → + L ⊢ i+m0 ϵ 𝐅*[l]⦃U⦄. +#K #T #l #i #H elim H -K -T -l -i +[ #K #T #l #i #HnT #L #s #l0 #m0 #_ #U #HTU #Hl0i -K -s + @frees_eq #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/ +| #I #K #K0 #T #V #l #i #j #Hlj #Hji #HnT #HK0 #HV #IHV #L #s #l0 #m0 #HLK #U #HTU #Hl0i + elim (ylt_split j l0) #H0 + [ elim (drop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 >yminus_SO2 #HLK0 #HVW + @(frees_be … HL0) -HL0 -HV /3 width=3 by ylt_plus_dx2_trans/ + [ lapply (ylt_fwd_lt_O1 … H0) #H1 + #X #HXU <(ymax_pre_sn l0 1) in HTU; /2 width=1 by ylt_fwd_le_succ1/ #HTU + <(ylt_inv_O1 l0) in H0; // -H1 #H0 + elim (lift_div_le … HXU … HTU ?) -U /2 width=2 by ylt_fwd_succ2/ + | >yplus_minus_comm_inj /2 width=1 by ylt_fwd_le/ + commutative_plus -HLK0 #HLK0 + @(frees_be … HLK0) -HLK0 -IHV + /2 width=1 by monotonic_ylt_plus_dx, yle_plus_dx1_trans/ + [ #X yplus_pred1 /2 width=1 by ylt_to_minus/ + ymax_pre_sn /2 width=2 by/ +| #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hlm0i + elim (ylt_split j l0) #H1 + [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW + elim (yle_inv_plus_inj2 … Hlm0i) #H0 #Hm0i + @(frees_be … H) -H + [ /3 width=1 by yle_plus_dx1_trans, monotonic_yle_minus_dx/ + | /2 width=3 by ylt_yle_trans/ + | #X #HXT elim (lift_trans_ge … HXT … HTU) -T /2 width=2 by ylt_fwd_le_succ1/ + | lapply (IHW … HKL0 … HVW ?) // -I -K -K0 -L0 -V -W -T -U -s + >yplus_pred1 /2 width=1 by ylt_to_minus/ + minus_minus_associative /2 width=1 by ylt_inv_inj/ yminus_SO2 >yplus_pred2 /2 width=1 by ylt_fwd_le_pred2/ + ] + | lapply (drop_conf_ge … HLK … HLK0 ?) // -L #HK0 + elim ( yle_inv_plus_inj2 … H2) -H2 #H2 #Hm0j + @(frees_be … HK0) + [ /2 width=1 by monotonic_yle_minus_dx/ + | /2 width=1 by monotonic_ylt_minus_dx/ + | #X #HXT elim (lift_trans_le … HXT … HTU) -T // + ymax_pre_sn /2 width=2 by/ + | yplus_minus_assoc_comm_inj // + >ymax_pre_sn /3 width=5 by yle_trans, ylt_fwd_le/ + ] + ] + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lift.ma deleted file mode 100644 index 65b629206..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lift.ma +++ /dev/null @@ -1,170 +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 "ground_2/ynat/ynat_max.ma". -include "basic_2/substitution/drop_drop.ma". -include "basic_2/multiple/frees.ma". - -(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) - -(* Advanced properties ******************************************************) - -lemma frees_dec: ∀L,U,l,i. Decidable (frees l L U i). -#L #U @(f2_ind … rfw … L U) -L -U -#x #IH #L * * -[ -IH /3 width=5 by frees_inv_sort, or_intror/ -| #j #Hx #l #i elim (ylt_split_eq i j) #Hji - [ -x @or_intror #H elim (ylt_yle_false … Hji) - lapply (frees_inv_lref_ge … H ?) -L -l /2 width=1 by ylt_fwd_le/ - | -x /2 width=1 by or_introl/ - | elim (ylt_split j l) #Hli - [ -x @or_intror #H elim (ylt_yle_false … Hji) - lapply (frees_inv_lref_skip … H ?) -L // - | elim (lt_or_ge j (|L|)) #Hj - [ elim (drop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct - elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, drop_fwd_rfw, or_introl/ ] #HnW - @or_intror #H elim (frees_inv_lref_lt … H) // #Z #Y #X #_ #HLY -l - lapply (drop_mono … HLY … HLK) -L #H destruct /2 width=1 by/ - | -x @or_intror #H elim (ylt_yle_false … Hji) - lapply (frees_inv_lref_free … H ?) -l // - ] - ] - ] -| -IH /3 width=5 by frees_inv_gref, or_intror/ -| #a #I #W #U #Hx #l #i destruct - elim (IH L W … l i) [1,3: /3 width=1 by frees_bind_sn, or_introl/ ] #HnW - elim (IH (L.ⓑ{I}W) U … (⫯l) (i+1)) -IH [1,3: /3 width=1 by frees_bind_dx, or_introl/ ] #HnU - @or_intror #H elim (frees_inv_bind … H) -H /2 width=1 by/ -| #I #W #U #Hx #l #i destruct - elim (IH L W … l i) [1,3: /3 width=1 by frees_flat_sn, or_introl/ ] #HnW - elim (IH L U … l i) -IH [1,3: /3 width=1 by frees_flat_dx, or_introl/ ] #HnU - @or_intror #H elim (frees_inv_flat … H) -H /2 width=1 by/ -] -qed-. - -lemma frees_S: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[yinj l]⦃U⦄ → ∀I,K,W. ⬇[l] L ≡ K.ⓑ{I}W → - (K ⊢ ⫰(i-l) ϵ 𝐅*[0]⦃W⦄ → ⊥) → L ⊢ i ϵ 𝐅*[⫯l]⦃U⦄. -#L #U #l #i #H elim (frees_inv … H) -H /3 width=2 by frees_eq/ -* #I #K #W #j #Hlj #Hji #HnU #HLK #HW #I0 #K0 #W0 #HLK0 #HnW0 -lapply (yle_inv_inj … Hlj) -Hlj #Hlj -elim (le_to_or_lt_eq … Hlj) -Hlj -[ -I0 -K0 -W0 /3 width=9 by frees_be, yle_inj/ -| -Hji -HnU #H destruct - lapply (drop_mono … HLK0 … HLK) #H destruct -I - elim HnW0 -L -U -HnW0 // -] -qed. - -(* Note: lemma 1250 *) -lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ → - L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄. -#a #I #L #W #U #i #HU elim (frees_dec L W 0 i) -/4 width=5 by frees_S, frees_bind_dx, frees_bind_sn/ -qed. - -(* Properties on relocation *************************************************) - -lemma frees_lift_ge: ∀K,T,l,i. K ⊢ i ϵ𝐅*[l]⦃T⦄ → - ∀L,s,l0,m0. ⬇[s, l0, m0] L ≡ K → - ∀U. ⬆[l0, m0] T ≡ U → l0 ≤ i → - L ⊢ i+m0 ϵ 𝐅*[l]⦃U⦄. -#K #T #l #i #H elim H -K -T -l -i -[ #K #T #l #i #HnT #L #s #l0 #m0 #_ #U #HTU #Hl0i -K -s - @frees_eq #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/ -| #I #K #K0 #T #V #l #i #j #Hlj #Hji #HnT #HK0 #HV #IHV #L #s #l0 #m0 #HLK #U #HTU #Hl0i - elim (ylt_split j l0) #H0 - [ elim (drop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 >yminus_SO2 #HLK0 #HVW - @(frees_be … HL0) -HL0 -HV /3 width=3 by ylt_plus_dx2_trans/ - [ lapply (ylt_fwd_lt_O1 … H0) #H1 - #X #HXU <(ymax_pre_sn l0 1) in HTU; /2 width=1 by ylt_fwd_le_succ1/ #HTU - <(ylt_inv_O1 l0) in H0; // -H1 #H0 - elim (lift_div_le … HXU … HTU ?) -U /2 width=2 by ylt_fwd_succ2/ - | >yplus_minus_comm_inj /2 width=1 by ylt_fwd_le/ - commutative_plus -HLK0 #HLK0 - @(frees_be … HLK0) -HLK0 -IHV - /2 width=1 by monotonic_ylt_plus_dx, yle_plus_dx1_trans/ - [ #X yplus_pred1 /2 width=1 by ylt_to_minus/ - ymax_pre_sn /2 width=2 by/ -| #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hlm0i - elim (ylt_split j l0) #H1 - [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW - elim (yle_inv_plus_inj2 … Hlm0i) #H0 #Hm0i - @(frees_be … H) -H - [ /3 width=1 by yle_plus_dx1_trans, monotonic_yle_minus_dx/ - | /2 width=3 by ylt_yle_trans/ - | #X #HXT elim (lift_trans_ge … HXT … HTU) -T /2 width=2 by ylt_fwd_le_succ1/ - | lapply (IHW … HKL0 … HVW ?) // -I -K -K0 -L0 -V -W -T -U -s - >yplus_pred1 /2 width=1 by ylt_to_minus/ - minus_minus_associative /2 width=1 by ylt_inv_inj/ yminus_SO2 >yplus_pred2 /2 width=1 by ylt_fwd_le_pred2/ - ] - | lapply (drop_conf_ge … HLK … HLK0 ?) // -L #HK0 - elim ( yle_inv_plus_inj2 … H2) -H2 #H2 #Hm0j - @(frees_be … HK0) - [ /2 width=1 by monotonic_yle_minus_dx/ - | /2 width=1 by monotonic_ylt_minus_dx/ - | #X #HXT elim (lift_trans_le … HXT … HTU) -T // - ymax_pre_sn /2 width=2 by/ - | yplus_minus_assoc_comm_inj // - >ymax_pre_sn /3 width=5 by yle_trans, ylt_fwd_le/ - ] - ] - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lreq.etc new file mode 100644 index 000000000..606c95cfb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lreq.etc @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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/drop_lreq.ma". +include "basic_2/multiple/frees.ma". + +(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) + +(* Properties on equivalence for local environments *************************) + +lemma lreq_frees_trans: ∀L2,U,l,i. L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ → + ∀L1. L1 ⩬[l, ∞] L2 → L1 ⊢ i ϵ 𝐅*[l]⦃U⦄. +#L2 #U #l #i #H elim H -L2 -U -l -i /3 width=2 by frees_eq/ +#I2 #L2 #K2 #U #W2 #l #i #j #Hlj #Hji #HnU #HLK2 #_ #IHW2 #L1 #HL12 +elim (lreq_drop_trans_be … HL12 … HLK2) -L2 // >yminus_Y_inj #K1 #HK12 #HLK1 +lapply (lreq_inv_O_Y … HK12) -HK12 #H destruct /3 width=9 by frees_be/ +qed-. + +lemma frees_lreq_conf: ∀L1,U,l,i. L1 ⊢ i ϵ 𝐅*[l]⦃U⦄ → + ∀L2. L1 ⩬[l, ∞] L2 → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄. +/3 width=3 by lreq_sym, lreq_frees_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lreq.ma deleted file mode 100644 index 606c95cfb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lreq.ma +++ /dev/null @@ -1,32 +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/drop_lreq.ma". -include "basic_2/multiple/frees.ma". - -(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) - -(* Properties on equivalence for local environments *************************) - -lemma lreq_frees_trans: ∀L2,U,l,i. L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ → - ∀L1. L1 ⩬[l, ∞] L2 → L1 ⊢ i ϵ 𝐅*[l]⦃U⦄. -#L2 #U #l #i #H elim H -L2 -U -l -i /3 width=2 by frees_eq/ -#I2 #L2 #K2 #U #W2 #l #i #j #Hlj #Hji #HnU #HLK2 #_ #IHW2 #L1 #HL12 -elim (lreq_drop_trans_be … HL12 … HLK2) -L2 // >yminus_Y_inj #K1 #HK12 #HLK1 -lapply (lreq_inv_O_Y … HK12) -HK12 #H destruct /3 width=9 by frees_be/ -qed-. - -lemma frees_lreq_conf: ∀L1,U,l,i. L1 ⊢ i ϵ 𝐅*[l]⦃U⦄ → - ∀L2. L1 ⩬[l, ∞] L2 → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄. -/3 width=3 by lreq_sym, lreq_frees_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq.etc new file mode 100644 index 000000000..b9493ad4b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq.etc @@ -0,0 +1,195 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/ynat/ynat_lt.ma". +include "basic_2/notation/relations/midiso_4.ma". +include "basic_2/grammar/lenv_length.ma". + +(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************) + +inductive lreq: relation4 ynat ynat lenv lenv ≝ +| lreq_atom: ∀l,m. lreq l m (⋆) (⋆) +| lreq_zero: ∀I1,I2,L1,L2,V1,V2. + lreq 0 0 L1 L2 → lreq 0 0 (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) +| lreq_pair: ∀I,L1,L2,V,m. lreq 0 m L1 L2 → + lreq 0 (⫯m) (L1.ⓑ{I}V) (L2.ⓑ{I}V) +| lreq_succ: ∀I1,I2,L1,L2,V1,V2,l,m. + lreq l m L1 L2 → lreq (⫯l) m (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) +. + +interpretation + "equivalence (local environment)" + 'MidIso l m L1 L2 = (lreq l m L1 L2). + +(* Basic properties *********************************************************) + +lemma lreq_pair_lt: ∀I,L1,L2,V,m. L1 ⩬[0, ⫰m] L2 → 0 < m → + L1.ⓑ{I}V ⩬[0, m] L2.ⓑ{I}V. +#I #L1 #L2 #V #m #HL12 #Hm <(ylt_inv_O1 … Hm) /2 width=1 by lreq_pair/ +qed. + +lemma lreq_succ_lt: ∀I1,I2,L1,L2,V1,V2,l,m. L1 ⩬[⫰l, m] L2 → 0 < l → + L1.ⓑ{I1}V1 ⩬[l, m] L2. ⓑ{I2}V2. +#I1 #I2 #L1 #L2 #V1 #V2 #l #m #HL12 #Hl <(ylt_inv_O1 … Hl) /2 width=1 by lreq_succ/ +qed. + +lemma lreq_pair_O_Y: ∀L1,L2. L1 ⩬[0, ∞] L2 → + ∀I,V. L1.ⓑ{I}V ⩬[0, ∞] L2.ⓑ{I}V. +#L1 #L2 #HL12 #I #V lapply (lreq_pair I … V … HL12) -HL12 // +qed. + +lemma lreq_refl: ∀L,l,m. L ⩬[l, m] L. +#L elim L -L // +#L #I #V #IHL #l elim (ynat_cases … l) [| * #x ] +#Hl destruct /2 width=1 by lreq_succ/ +#m elim (ynat_cases … m) [| * #x ] +#Hm destruct /2 width=1 by lreq_zero, lreq_pair/ +qed. + +lemma lreq_O2: ∀L1,L2,l. |L1| = |L2| → L1 ⩬[l, 0] L2. +#L1 elim L1 -L1 [| #L1 #I1 #V1 #IHL1 ] +* // [1,3: #L2 #I2 #V2 ] #l +[ #H elim (ysucc_inv_O_sn … H) +| >length_pair >length_pair #H + lapply (ysucc_inv_inj … H) -H #HL12 + elim (ynat_cases l) /3 width=1 by lreq_zero/ + * /3 width=1 by lreq_succ/ +| #H elim (ysucc_inv_O_dx … H) +] +qed. + +lemma lreq_sym: ∀l,m. symmetric … (lreq l m). +#l #m #L1 #L2 #H elim H -L1 -L2 -l -m +/2 width=1 by lreq_zero, lreq_pair, lreq_succ/ +qed-. + +(* Basic inversion lemmas ***************************************************) + +fact lreq_inv_atom1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → L1 = ⋆ → L2 = ⋆. +#L1 #L2 #l #m * -L1 -L2 -l -m // +[ #I1 #I2 #L1 #L2 #V1 #V2 #_ #H destruct +| #I #L1 #L2 #V #m #_ #H destruct +| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #H destruct +] +qed-. + +lemma lreq_inv_atom1: ∀L2,l,m. ⋆ ⩬[l, m] L2 → L2 = ⋆. +/2 width=5 by lreq_inv_atom1_aux/ qed-. + +fact lreq_inv_zero1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → + ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → l = 0 → m = 0 → + ∃∃J2,K2,W2. K1 ⩬[0, 0] K2 & L2 = K2.ⓑ{J2}W2. +#L1 #L2 #l #m * -L1 -L2 -l -m +[ #l #m #J1 #K1 #W1 #H destruct +| #I1 #I2 #L1 #L2 #V1 #V2 #HL12 #J1 #K1 #W1 #H #_ #_ destruct + /2 width=5 by ex2_3_intro/ +| #I #L1 #L2 #V #m #_ #J1 #K1 #W1 #_ #_ #H + elim (ysucc_inv_O_dx … H) +| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #J1 #K1 #W1 #_ #H + elim (ysucc_inv_O_dx … H) +] +qed-. + +lemma lreq_inv_zero1: ∀I1,K1,L2,V1. K1.ⓑ{I1}V1 ⩬[0, 0] L2 → + ∃∃I2,K2,V2. K1 ⩬[0, 0] K2 & L2 = K2.ⓑ{I2}V2. +/2 width=9 by lreq_inv_zero1_aux/ qed-. + +fact lreq_inv_pair1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → + ∀J,K1,W. L1 = K1.ⓑ{J}W → l = 0 → 0 < m → + ∃∃K2. K1 ⩬[0, ⫰m] K2 & L2 = K2.ⓑ{J}W. +#L1 #L2 #l #m * -L1 -L2 -l -m +[ #l #m #J #K1 #W #H destruct +| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J #K1 #W #_ #_ #H + elim (ylt_yle_false … H) // +| #I #L1 #L2 #V #m #HL12 #J #K1 #W #H #_ #_ destruct + /2 width=3 by ex2_intro/ +| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #J #K1 #W #_ #H + elim (ysucc_inv_O_dx … H) +] +qed-. + +lemma lreq_inv_pair1: ∀I,K1,L2,V,m. K1.ⓑ{I}V ⩬[0, m] L2 → 0 < m → + ∃∃K2. K1 ⩬[0, ⫰m] K2 & L2 = K2.ⓑ{I}V. +/2 width=6 by lreq_inv_pair1_aux/ qed-. + +lemma lreq_inv_pair: ∀I1,I2,L1,L2,V1,V2,m. L1.ⓑ{I1}V1 ⩬[0, m] L2.ⓑ{I2}V2 → 0 < m → + ∧∧ L1 ⩬[0, ⫰m] L2 & I1 = I2 & V1 = V2. +#I1 #I2 #L1 #L2 #V1 #V2 #m #H #Hm elim (lreq_inv_pair1 … H) -H // +#Y #HL12 #H destruct /2 width=1 by and3_intro/ +qed-. + +fact lreq_inv_succ1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → + ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → 0 < l → + ∃∃J2,K2,W2. K1 ⩬[⫰l, m] K2 & L2 = K2.ⓑ{J2}W2. +#L1 #L2 #l #m * -L1 -L2 -l -m +[ #l #m #J1 #K1 #W1 #H destruct +| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J1 #K1 #W1 #_ #H + elim (ylt_yle_false … H) // +| #I #L1 #L2 #V #m #_ #J1 #K1 #W1 #_ #H + elim (ylt_yle_false … H) // +| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #HL12 #J1 #K1 #W1 #H #_ destruct + /2 width=5 by ex2_3_intro/ +] +qed-. + +lemma lreq_inv_succ1: ∀I1,K1,L2,V1,l,m. K1.ⓑ{I1}V1 ⩬[l, m] L2 → 0 < l → + ∃∃I2,K2,V2. K1 ⩬[⫰l, m] K2 & L2 = K2.ⓑ{I2}V2. +/2 width=5 by lreq_inv_succ1_aux/ qed-. + +lemma lreq_inv_atom2: ∀L1,l,m. L1 ⩬[l, m] ⋆ → L1 = ⋆. +/3 width=3 by lreq_inv_atom1, lreq_sym/ +qed-. + +lemma lreq_inv_succ: ∀I1,I2,L1,L2,V1,V2,l,m. L1.ⓑ{I1}V1 ⩬[l, m] L2.ⓑ{I2}V2 → 0 < l → + L1 ⩬[⫰l, m] L2. +#I1 #I2 #L1 #L2 #V1 #V2 #l #m #H #Hl elim (lreq_inv_succ1 … H) -H // +#Z #Y #X #HL12 #H destruct // +qed-. + +lemma lreq_inv_zero2: ∀I2,K2,L1,V2. L1 ⩬[0, 0] K2.ⓑ{I2}V2 → + ∃∃I1,K1,V1. K1 ⩬[0, 0] K2 & L1 = K1.ⓑ{I1}V1. +#I2 #K2 #L1 #V2 #H elim (lreq_inv_zero1 … (lreq_sym … H)) -H +/3 width=5 by lreq_sym, ex2_3_intro/ +qed-. + +lemma lreq_inv_pair2: ∀I,K2,L1,V,m. L1 ⩬[0, m] K2.ⓑ{I}V → 0 < m → + ∃∃K1. K1 ⩬[0, ⫰m] K2 & L1 = K1.ⓑ{I}V. +#I #K2 #L1 #V #m #H #Hm elim (lreq_inv_pair1 … (lreq_sym … H)) -H +/3 width=3 by lreq_sym, ex2_intro/ +qed-. + +lemma lreq_inv_succ2: ∀I2,K2,L1,V2,l,m. L1 ⩬[l, m] K2.ⓑ{I2}V2 → 0 < l → + ∃∃I1,K1,V1. K1 ⩬[⫰l, m] K2 & L1 = K1.ⓑ{I1}V1. +#I2 #K2 #L1 #V2 #l #m #H #Hl elim (lreq_inv_succ1 … (lreq_sym … H)) -H +/3 width=5 by lreq_sym, ex2_3_intro/ +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lreq_fwd_length: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → |L1| = |L2|. +#L1 #L2 #l #m #H elim H -L1 -L2 -l -m // +qed-. + +(* Advanced inversion lemmas ************************************************) + +fact lreq_inv_O_Y_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → l = 0 → m = ∞ → L1 = L2. +#L1 #L2 #l #m #H elim H -L1 -L2 -l -m // +[ #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #_ #H destruct +| /4 width=1 by eq_f3, ysucc_inv_Y_dx/ +| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #_ #H elim (ysucc_inv_O_dx … H) +] +qed-. + +lemma lreq_inv_O_Y: ∀L1,L2. L1 ⩬[0, ∞] L2 → L1 = L2. +/2 width=5 by lreq_inv_O_Y_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq_lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq_lreq.etc new file mode 100644 index 000000000..20d6c0002 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq_lreq.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 "ground_2/ynat/ynat_plus.ma". +include "basic_2/grammar/lreq.ma". + +(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************) + +(* Main properties **********************************************************) + +theorem lreq_trans: ∀l,m. Transitive … (lreq l m). +#l #m #L1 #L2 #H elim H -L1 -L2 -l -m +[ #l #m #X #H lapply (lreq_inv_atom1 … H) -H + #H destruct // +| #I1 #I #L1 #L #V1 #V #_ #IHL1 #X #H elim (lreq_inv_zero1 … H) -H + #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by lreq_zero/ +| #I #L1 #L #V #m #_ #IHL1 #X #H elim (lreq_inv_pair1 … H) -H // + #L2 #HL2 #H destruct /3 width=1 by lreq_pair/ +| #I1 #I #L1 #L #V1 #V #l #m #_ #IHL1 #X #H elim (lreq_inv_succ1 … H) -H // + #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by lreq_succ/ +] +qed-. + +theorem lreq_canc_sn: ∀l,m,L,L1,L2. L ⩬[l, m] L1 → L ⩬[l, m] L2 → L1 ⩬[l, m] L2. +/3 width=3 by lreq_trans, lreq_sym/ qed-. + +theorem lreq_canc_dx: ∀l,m,L,L1,L2. L1 ⩬[l, m] L → L2 ⩬[l, m] L → L1 ⩬[l, m] L2. +/3 width=3 by lreq_trans, lreq_sym/ qed-. + +theorem lreq_join: ∀L1,L2,l,i. L1 ⩬[l, i] L2 → + ∀m. L1 ⩬[i+l, m] L2 → L1 ⩬[l, i+m] L2. +#L1 #L2 #l #i #H elim H -L1 -L2 -l -i // +[ #I #L1 #L2 #V #m #_ #IHL12 #m #H + lapply (lreq_inv_succ … H ?) -H // >ypred_succ /3 width=1 by lreq_pair/ +| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #IHL12 #m #H + lapply (lreq_inv_succ … H ?) -H // >yplus_succ2 >ypred_succ /3 width=1 by lreq_succ/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lreq.ma deleted file mode 100644 index b9493ad4b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lreq.ma +++ /dev/null @@ -1,195 +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 "ground_2/ynat/ynat_lt.ma". -include "basic_2/notation/relations/midiso_4.ma". -include "basic_2/grammar/lenv_length.ma". - -(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************) - -inductive lreq: relation4 ynat ynat lenv lenv ≝ -| lreq_atom: ∀l,m. lreq l m (⋆) (⋆) -| lreq_zero: ∀I1,I2,L1,L2,V1,V2. - lreq 0 0 L1 L2 → lreq 0 0 (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) -| lreq_pair: ∀I,L1,L2,V,m. lreq 0 m L1 L2 → - lreq 0 (⫯m) (L1.ⓑ{I}V) (L2.ⓑ{I}V) -| lreq_succ: ∀I1,I2,L1,L2,V1,V2,l,m. - lreq l m L1 L2 → lreq (⫯l) m (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) -. - -interpretation - "equivalence (local environment)" - 'MidIso l m L1 L2 = (lreq l m L1 L2). - -(* Basic properties *********************************************************) - -lemma lreq_pair_lt: ∀I,L1,L2,V,m. L1 ⩬[0, ⫰m] L2 → 0 < m → - L1.ⓑ{I}V ⩬[0, m] L2.ⓑ{I}V. -#I #L1 #L2 #V #m #HL12 #Hm <(ylt_inv_O1 … Hm) /2 width=1 by lreq_pair/ -qed. - -lemma lreq_succ_lt: ∀I1,I2,L1,L2,V1,V2,l,m. L1 ⩬[⫰l, m] L2 → 0 < l → - L1.ⓑ{I1}V1 ⩬[l, m] L2. ⓑ{I2}V2. -#I1 #I2 #L1 #L2 #V1 #V2 #l #m #HL12 #Hl <(ylt_inv_O1 … Hl) /2 width=1 by lreq_succ/ -qed. - -lemma lreq_pair_O_Y: ∀L1,L2. L1 ⩬[0, ∞] L2 → - ∀I,V. L1.ⓑ{I}V ⩬[0, ∞] L2.ⓑ{I}V. -#L1 #L2 #HL12 #I #V lapply (lreq_pair I … V … HL12) -HL12 // -qed. - -lemma lreq_refl: ∀L,l,m. L ⩬[l, m] L. -#L elim L -L // -#L #I #V #IHL #l elim (ynat_cases … l) [| * #x ] -#Hl destruct /2 width=1 by lreq_succ/ -#m elim (ynat_cases … m) [| * #x ] -#Hm destruct /2 width=1 by lreq_zero, lreq_pair/ -qed. - -lemma lreq_O2: ∀L1,L2,l. |L1| = |L2| → L1 ⩬[l, 0] L2. -#L1 elim L1 -L1 [| #L1 #I1 #V1 #IHL1 ] -* // [1,3: #L2 #I2 #V2 ] #l -[ #H elim (ysucc_inv_O_sn … H) -| >length_pair >length_pair #H - lapply (ysucc_inv_inj … H) -H #HL12 - elim (ynat_cases l) /3 width=1 by lreq_zero/ - * /3 width=1 by lreq_succ/ -| #H elim (ysucc_inv_O_dx … H) -] -qed. - -lemma lreq_sym: ∀l,m. symmetric … (lreq l m). -#l #m #L1 #L2 #H elim H -L1 -L2 -l -m -/2 width=1 by lreq_zero, lreq_pair, lreq_succ/ -qed-. - -(* Basic inversion lemmas ***************************************************) - -fact lreq_inv_atom1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → L1 = ⋆ → L2 = ⋆. -#L1 #L2 #l #m * -L1 -L2 -l -m // -[ #I1 #I2 #L1 #L2 #V1 #V2 #_ #H destruct -| #I #L1 #L2 #V #m #_ #H destruct -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #H destruct -] -qed-. - -lemma lreq_inv_atom1: ∀L2,l,m. ⋆ ⩬[l, m] L2 → L2 = ⋆. -/2 width=5 by lreq_inv_atom1_aux/ qed-. - -fact lreq_inv_zero1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → - ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → l = 0 → m = 0 → - ∃∃J2,K2,W2. K1 ⩬[0, 0] K2 & L2 = K2.ⓑ{J2}W2. -#L1 #L2 #l #m * -L1 -L2 -l -m -[ #l #m #J1 #K1 #W1 #H destruct -| #I1 #I2 #L1 #L2 #V1 #V2 #HL12 #J1 #K1 #W1 #H #_ #_ destruct - /2 width=5 by ex2_3_intro/ -| #I #L1 #L2 #V #m #_ #J1 #K1 #W1 #_ #_ #H - elim (ysucc_inv_O_dx … H) -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #J1 #K1 #W1 #_ #H - elim (ysucc_inv_O_dx … H) -] -qed-. - -lemma lreq_inv_zero1: ∀I1,K1,L2,V1. K1.ⓑ{I1}V1 ⩬[0, 0] L2 → - ∃∃I2,K2,V2. K1 ⩬[0, 0] K2 & L2 = K2.ⓑ{I2}V2. -/2 width=9 by lreq_inv_zero1_aux/ qed-. - -fact lreq_inv_pair1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → - ∀J,K1,W. L1 = K1.ⓑ{J}W → l = 0 → 0 < m → - ∃∃K2. K1 ⩬[0, ⫰m] K2 & L2 = K2.ⓑ{J}W. -#L1 #L2 #l #m * -L1 -L2 -l -m -[ #l #m #J #K1 #W #H destruct -| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J #K1 #W #_ #_ #H - elim (ylt_yle_false … H) // -| #I #L1 #L2 #V #m #HL12 #J #K1 #W #H #_ #_ destruct - /2 width=3 by ex2_intro/ -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #J #K1 #W #_ #H - elim (ysucc_inv_O_dx … H) -] -qed-. - -lemma lreq_inv_pair1: ∀I,K1,L2,V,m. K1.ⓑ{I}V ⩬[0, m] L2 → 0 < m → - ∃∃K2. K1 ⩬[0, ⫰m] K2 & L2 = K2.ⓑ{I}V. -/2 width=6 by lreq_inv_pair1_aux/ qed-. - -lemma lreq_inv_pair: ∀I1,I2,L1,L2,V1,V2,m. L1.ⓑ{I1}V1 ⩬[0, m] L2.ⓑ{I2}V2 → 0 < m → - ∧∧ L1 ⩬[0, ⫰m] L2 & I1 = I2 & V1 = V2. -#I1 #I2 #L1 #L2 #V1 #V2 #m #H #Hm elim (lreq_inv_pair1 … H) -H // -#Y #HL12 #H destruct /2 width=1 by and3_intro/ -qed-. - -fact lreq_inv_succ1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → - ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → 0 < l → - ∃∃J2,K2,W2. K1 ⩬[⫰l, m] K2 & L2 = K2.ⓑ{J2}W2. -#L1 #L2 #l #m * -L1 -L2 -l -m -[ #l #m #J1 #K1 #W1 #H destruct -| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J1 #K1 #W1 #_ #H - elim (ylt_yle_false … H) // -| #I #L1 #L2 #V #m #_ #J1 #K1 #W1 #_ #H - elim (ylt_yle_false … H) // -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #HL12 #J1 #K1 #W1 #H #_ destruct - /2 width=5 by ex2_3_intro/ -] -qed-. - -lemma lreq_inv_succ1: ∀I1,K1,L2,V1,l,m. K1.ⓑ{I1}V1 ⩬[l, m] L2 → 0 < l → - ∃∃I2,K2,V2. K1 ⩬[⫰l, m] K2 & L2 = K2.ⓑ{I2}V2. -/2 width=5 by lreq_inv_succ1_aux/ qed-. - -lemma lreq_inv_atom2: ∀L1,l,m. L1 ⩬[l, m] ⋆ → L1 = ⋆. -/3 width=3 by lreq_inv_atom1, lreq_sym/ -qed-. - -lemma lreq_inv_succ: ∀I1,I2,L1,L2,V1,V2,l,m. L1.ⓑ{I1}V1 ⩬[l, m] L2.ⓑ{I2}V2 → 0 < l → - L1 ⩬[⫰l, m] L2. -#I1 #I2 #L1 #L2 #V1 #V2 #l #m #H #Hl elim (lreq_inv_succ1 … H) -H // -#Z #Y #X #HL12 #H destruct // -qed-. - -lemma lreq_inv_zero2: ∀I2,K2,L1,V2. L1 ⩬[0, 0] K2.ⓑ{I2}V2 → - ∃∃I1,K1,V1. K1 ⩬[0, 0] K2 & L1 = K1.ⓑ{I1}V1. -#I2 #K2 #L1 #V2 #H elim (lreq_inv_zero1 … (lreq_sym … H)) -H -/3 width=5 by lreq_sym, ex2_3_intro/ -qed-. - -lemma lreq_inv_pair2: ∀I,K2,L1,V,m. L1 ⩬[0, m] K2.ⓑ{I}V → 0 < m → - ∃∃K1. K1 ⩬[0, ⫰m] K2 & L1 = K1.ⓑ{I}V. -#I #K2 #L1 #V #m #H #Hm elim (lreq_inv_pair1 … (lreq_sym … H)) -H -/3 width=3 by lreq_sym, ex2_intro/ -qed-. - -lemma lreq_inv_succ2: ∀I2,K2,L1,V2,l,m. L1 ⩬[l, m] K2.ⓑ{I2}V2 → 0 < l → - ∃∃I1,K1,V1. K1 ⩬[⫰l, m] K2 & L1 = K1.ⓑ{I1}V1. -#I2 #K2 #L1 #V2 #l #m #H #Hl elim (lreq_inv_succ1 … (lreq_sym … H)) -H -/3 width=5 by lreq_sym, ex2_3_intro/ -qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lreq_fwd_length: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → |L1| = |L2|. -#L1 #L2 #l #m #H elim H -L1 -L2 -l -m // -qed-. - -(* Advanced inversion lemmas ************************************************) - -fact lreq_inv_O_Y_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → l = 0 → m = ∞ → L1 = L2. -#L1 #L2 #l #m #H elim H -L1 -L2 -l -m // -[ #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #_ #H destruct -| /4 width=1 by eq_f3, ysucc_inv_Y_dx/ -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #_ #H elim (ysucc_inv_O_dx … H) -] -qed-. - -lemma lreq_inv_O_Y: ∀L1,L2. L1 ⩬[0, ∞] L2 → L1 = L2. -/2 width=5 by lreq_inv_O_Y_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lreq_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lreq_lreq.ma deleted file mode 100644 index 20d6c0002..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lreq_lreq.ma +++ /dev/null @@ -1,49 +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 "ground_2/ynat/ynat_plus.ma". -include "basic_2/grammar/lreq.ma". - -(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************) - -(* Main properties **********************************************************) - -theorem lreq_trans: ∀l,m. Transitive … (lreq l m). -#l #m #L1 #L2 #H elim H -L1 -L2 -l -m -[ #l #m #X #H lapply (lreq_inv_atom1 … H) -H - #H destruct // -| #I1 #I #L1 #L #V1 #V #_ #IHL1 #X #H elim (lreq_inv_zero1 … H) -H - #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by lreq_zero/ -| #I #L1 #L #V #m #_ #IHL1 #X #H elim (lreq_inv_pair1 … H) -H // - #L2 #HL2 #H destruct /3 width=1 by lreq_pair/ -| #I1 #I #L1 #L #V1 #V #l #m #_ #IHL1 #X #H elim (lreq_inv_succ1 … H) -H // - #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by lreq_succ/ -] -qed-. - -theorem lreq_canc_sn: ∀l,m,L,L1,L2. L ⩬[l, m] L1 → L ⩬[l, m] L2 → L1 ⩬[l, m] L2. -/3 width=3 by lreq_trans, lreq_sym/ qed-. - -theorem lreq_canc_dx: ∀l,m,L,L1,L2. L1 ⩬[l, m] L → L2 ⩬[l, m] L → L1 ⩬[l, m] L2. -/3 width=3 by lreq_trans, lreq_sym/ qed-. - -theorem lreq_join: ∀L1,L2,l,i. L1 ⩬[l, i] L2 → - ∀m. L1 ⩬[i+l, m] L2 → L1 ⩬[l, i+m] L2. -#L1 #L2 #l #i #H elim H -L1 -L2 -l -i // -[ #I #L1 #L2 #V #m #_ #IHL12 #m #H - lapply (lreq_inv_succ … H ?) -H // >ypred_succ /3 width=1 by lreq_pair/ -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #IHL12 #m #H - lapply (lreq_inv_succ … H ?) -H // >yplus_succ2 >ypred_succ /3 width=1 by lreq_succ/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2.ma new file mode 100644 index 000000000..072b07f6c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2.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 *) +(* *) +(**************************************************************************) + +include "ground_2/lib/list.ma". + +(* MULTIPLE RELOCATION WITH PAIRS *******************************************) + +definition mr2: Type[0] ≝ list2 nat nat.