From: Ferruccio Guidi Date: Mon, 28 Mar 2016 16:04:59 +0000 (+0000) Subject: minor additions ... X-Git-Tag: make_still_working~620 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=50997cb3042073d58c2a16885ef0c82217367e63;p=helm.git minor additions ... --- 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 deleted file mode 100644 index fd7ba1c91..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.etc +++ /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_lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lreq.etc deleted file mode 100644 index 606c95cfb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lreq.etc +++ /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/llor/llor.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llor/llor.etc deleted file mode 100644 index a2d1e61a7..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llor/llor.etc +++ /dev/null @@ -1,40 +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/lazyor_5.ma". -include "basic_2/multiple/frees.ma". - -(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************) - -definition llor: ynat → relation4 term lenv lenv lenv ≝ λl,T,L2,L1,L. - ∧∧ |L1| = |L2| & |L1| = |L| - & (∀I1,I2,I,K1,K2,K,V1,V2,V,i. - ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 → ⬇[i] L ≡ K.ⓑ{I}V → ∨∨ - (∧∧ yinj i < l & I1 = I & V1 = V) | - (∧∧ (L1 ⊢ i ϵ 𝐅*[l]⦃T⦄ → ⊥) & I1 = I & V1 = V) | - (∧∧ l ≤ yinj i & L1 ⊢ i ϵ 𝐅*[l]⦃T⦄ & I2 = I & V2 = V) - ). - -interpretation - "lazy union (local environment)" - 'LazyOr L1 T l L2 L = (llor l T L2 L1 L). - -(* Basic properties *********************************************************) - -(* Note: this can be proved by llor_skip *) -lemma llor_atom: ∀T,l. ⋆ ⋓[T, l] ⋆ ≡ ⋆. -#T #l @and3_intro // -#I1 #I2 #I #K1 #K2 #K #V1 #V2 #V #i #HLK1 -elim (drop_inv_atom1 … HLK1) -HLK1 #H destruct -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llor/llor_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llor/llor_alt.etc deleted file mode 100644 index 700cd7ce3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llor/llor_alt.etc +++ /dev/null @@ -1,74 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/multiple/frees_append.ma". -include "basic_2/multiple/llor.ma". - -(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************) - -(* Alternative definition ***************************************************) - -lemma llor_tail_frees: ∀L1,L2,L,U,l. L1 ⋓[U, l] L2 ≡ L → l ≤ yinj (|L1|) → - ∀I1,W1. ⓑ{I1}W1.L1 ⊢ |L1| ϵ 𝐅*[l]⦃U⦄ → - ∀I2,W2. ⓑ{I1}W1.L1 ⋓[U, l] ⓑ{I2}W2.L2 ≡ ⓑ{I2}W2.L. -#L1 #L2 #L #U #l * #HL12 #HL1 #IH #Hl #I1 #W1 #HU #I2 #W2 -@and3_intro [1,2: >ltail_length /2 width=1 by le_S_S/ ] -#J1 #J2 #J #K1 #K2 #K #V1 #V2 #V #i #HLK1 #HLK2 #HLK -lapply (drop_fwd_length_lt2 … HLK1) >ltail_length #H -lapply (lt_plus_SO_to_le … H) -H #H -elim (le_to_or_lt_eq … H) -H #H -[ elim (drop_O1_lt (Ⓕ) … H) #Z1 #Y1 #X1 #HLY1 - elim (drop_O1_lt (Ⓕ) L2 i) // #Z2 #Y2 #X2 #HLY2 - elim (drop_O1_lt (Ⓕ) L i) // #Z #Y #X #HLY - lapply (drop_O1_inv_append1_le … HLK1 … HLY1) /2 width=1 by lt_to_le/ -HLK1 normalize #H destruct - lapply (drop_O1_inv_append1_le … HLK2 … HLY2) /2 width=1 by lt_to_le/ -HLK2 normalize #H destruct - lapply (drop_O1_inv_append1_le … HLK … HLY) /2 width=1 by lt_to_le/ -HLK normalize #H destruct - elim (IH … HLY1 HLY2 HLY) -IH -HLY1 -HLY2 -HLY * - [ /3 width=1 by and3_intro, or3_intro0/ - | /7 width=2 by frees_inv_append, yle_inj, lt_to_le, or3_intro1, and3_intro/ - | /6 width=1 by frees_append, yle_inj, lt_to_le, or3_intro2, and4_intro/ - ] -| -IH -HLK1 destruct - lapply (drop_O1_inv_append1_le … HLK2 … (⋆) ?) // -HLK2 normalize #H destruct - lapply (drop_O1_inv_append1_le … HLK … (⋆) ?) // -HLK normalize #H destruct - /3 width=1 by or3_intro2, and4_intro/ -] -qed. - -lemma llor_tail_cofrees: ∀L1,L2,L,U,l. L1 ⋓[U, l] L2 ≡ L → - ∀I1,W1. (ⓑ{I1}W1.L1 ⊢ |L1| ϵ 𝐅*[l]⦃U⦄ → ⊥) → - ∀I2,W2. ⓑ{I1}W1.L1 ⋓[U, l] ⓑ{I2}W2.L2 ≡ ⓑ{I1}W1.L. -#L1 #L2 #L #U #l * #HL12 #HL1 #IH #I1 #W1 #HU #I2 #W2 -@and3_intro [1,2: >ltail_length /2 width=1 by le_S_S/ ] -#J1 #J2 #J #K1 #K2 #K #V1 #V2 #V #i #HLK1 #HLK2 #HLK -lapply (drop_fwd_length_lt2 … HLK1) >ltail_length #H -lapply (lt_plus_SO_to_le … H) -H #H -elim (le_to_or_lt_eq … H) -H #H -[ elim (drop_O1_lt (Ⓕ) … H) #Z1 #Y1 #X1 #HLY1 - elim (drop_O1_lt (Ⓕ) L2 i) // #Z2 #Y2 #X2 #HLY2 - elim (drop_O1_lt (Ⓕ) L i) // #Z #Y #X #HLY - lapply (drop_O1_inv_append1_le … HLK1 … HLY1) /2 width=1 by lt_to_le/ -HLK1 normalize #H destruct - lapply (drop_O1_inv_append1_le … HLK2 … HLY2) /2 width=1 by lt_to_le/ -HLK2 normalize #H destruct - lapply (drop_O1_inv_append1_le … HLK … HLY) /2 width=1 by lt_to_le/ -HLK normalize #H destruct - elim (IH … HLY1 HLY2 HLY) -IH -HLY1 -HLY2 -HLY * - [ /3 width=1 by and3_intro, or3_intro0/ - | /7 width=2 by frees_inv_append, yle_inj, lt_to_le, or3_intro1, and3_intro/ - | /6 width=1 by frees_append, yle_inj, lt_to_le, or3_intro2, and4_intro/ - ] -| -IH -HLK2 destruct - lapply (drop_O1_inv_append1_le … HLK1 … (⋆) ?) // -HLK1 normalize #H destruct - lapply (drop_O1_inv_append1_le … HLK … (⋆) ?) // -HLK normalize #H destruct - /4 width=1 by or3_intro1, and3_intro/ -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llor/llor_drop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llor/llor_drop.etc deleted file mode 100644 index cbeab4a59..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llor/llor_drop.etc +++ /dev/null @@ -1,45 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/multiple/frees_lift.ma". -include "basic_2/multiple/llor_alt.ma". - -(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************) - -(* Advanced properties ******************************************************) - -lemma llor_skip: ∀L1,L2,U,l. |L1| = |L2| → yinj (|L1|) ≤ l → L1 ⋓[U, l] L2 ≡ L1. -#L1 #L2 #U #l #HL12 #Hl @and3_intro // -HL12 -#I1 #I2 #I #K1 #K2 #K #W1 #W2 #W #i #HLK1 #_ #HLK -L2 -K2 -lapply (drop_mono … HLK … HLK1) -HLK #H destruct -lapply (drop_fwd_length_lt2 … HLK1) -K1 -/5 width=3 by ylt_yle_trans, ylt_inj, or3_intro0, and3_intro/ -qed. - -(* Note: lemma 1400 concludes the "big tree" theorem *) -lemma llor_total: ∀L1,L2,T,l. |L1| = |L2| → ∃L. L1 ⋓[T, l] L2 ≡ L. -#L1 @(lenv_ind_alt … L1) -L1 -[ #L2 #T #l #H >(length_inv_zero_sn … H) -L2 /2 width=2 by ex_intro/ -| #I1 #L1 #V1 #IHL1 #Y #T #l >ltail_length #H - elim (length_inv_pos_sn_ltail … H) -H #I2 #L2 #V2 #HL12 #H destruct - elim (ylt_split l (|ⓑ{I1}V1.L1|)) - [ elim (frees_dec (ⓑ{I1}V1.L1) T l (|L1|)) #HnU - elim (IHL1 L2 T l) // -IHL1 -HL12 - [ #L #HL12 >ltail_length /4 width=2 by llor_tail_frees, ylt_fwd_succ2, ex_intro/ - | /4 width=2 by llor_tail_cofrees, ex_intro/ - ] - | -IHL1 /4 width=3 by llor_skip, plus_to_minus, ex_intro/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma index e5e5b098c..d9e583225 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma @@ -184,3 +184,15 @@ lemma frees_gref_gen: ∀L,p,f. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃§p⦄ ≡ f. #L elim L -L /4 width=3 by frees_eq_repl_back, frees_gref, frees_atom, eq_push_inv_isid/ qed. + +(* Basic_2A1: removed theorems 27: + frees_eq frees_be frees_inv + frees_inv_sort frees_inv_gref frees_inv_lref frees_inv_lref_free + frees_inv_lref_skip frees_inv_lref_ge frees_inv_lref_lt + frees_inv_bind frees_inv_flat frees_inv_bind_O + frees_lref_eq frees_lref_be frees_weak + frees_bind_sn frees_bind_dx frees_flat_sn frees_flat_dx + lreq_frees_trans frees_lreq_conf + llor_atom llor_skip llor_total + llor_tail_frees llor_tail_cofrees +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_weight.ma index c8b3b7f46..04e8c370f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_weight.ma @@ -20,6 +20,7 @@ include "basic_2/relocation/frees.ma". (* Advanced properties ******************************************************) +(* Notes: this replaces lemma 1400 concluding the "big tree" theorem *) lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅*⦃T⦄ ≡ f. @(f2_ind … rfw) #n #IH #L * [ cases L -L /3 width=2 by frees_atom, ex_intro/