From: Ferruccio Guidi Date: Sun, 11 Oct 2015 14:39:30 +0000 (+0000) Subject: ground_2 milestone: multiple relocation with lists of booleans X-Git-Tag: make_still_working~688 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5102e7f780e83c7fef1d3826f81dfd37ee4028bc ground_2 milestone: multiple relocation with lists of booleans basic_2: simplified formalization starts: partial commit of the grammar component --- 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 new file mode 100644 index 000000000..fd7ba1c91 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.ma @@ -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_append.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_append.ma new file mode 100644 index 000000000..ee8324cc9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_append.ma @@ -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_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lift.ma new file mode 100644 index 000000000..65b629206 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lift.ma @@ -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_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lreq.ma new file mode 100644 index 000000000..606c95cfb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_lreq.ma @@ -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/lenv/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_append.ma new file mode 100644 index 000000000..4f5f26fc9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_append.ma @@ -0,0 +1,145 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/notation/functions/append_2.ma". +include "ground_2/ynat/ynat_plus.ma". +include "basic_2/notation/functions/snbind2_3.ma". +include "basic_2/notation/functions/snabbr_2.ma". +include "basic_2/notation/functions/snabst_2.ma". +include "basic_2/grammar/lenv_length.ma". + +(* LOCAL ENVIRONMENTS *******************************************************) + +let rec append L K on K ≝ match K with +[ LAtom ⇒ L +| LPair K I V ⇒ (append L K). ⓑ{I} V +]. + +interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2). + +interpretation "local environment tail binding construction (binary)" + 'SnBind2 I T L = (append (LPair LAtom I T) L). + +interpretation "tail abbreviation (local environment)" + 'SnAbbr T L = (append (LPair LAtom Abbr T) L). + +interpretation "tail abstraction (local environment)" + 'SnAbst L T = (append (LPair LAtom Abst T) L). + +definition d_appendable_sn: predicate (lenv→relation term) ≝ λR. + ∀K,T1,T2. R K T1 T2 → ∀L. R (L @@ K) T1 T2. + +(* Basic properties *********************************************************) + +lemma append_atom: ∀L. L @@ ⋆ = L. +// qed. + +lemma append_pair: ∀I,L,K,V. L @@ (K.ⓑ{I}V) = (L @@ K).ⓑ{I}V. +// qed. + +lemma append_atom_sn: ∀L. ⋆ @@ L = L. +#L elim L -L // +#L #I #V >append_pair // +qed. + +lemma append_assoc: associative … append. +#L1 #L2 #L3 elim L3 -L3 // +qed. + +lemma append_length: ∀L1,L2. |L1 @@ L2| = |L1| + |L2|. +#L1 #L2 elim L2 -L2 // +#L2 #I #V2 >append_pair >length_pair >length_pair // +qed. + +lemma ltail_length: ∀I,L,V. |ⓑ{I}V.L| = ⫯|L|. +#I #L #V >append_length // +qed. + +(* Basic_1: was just: chead_ctail *) +lemma lpair_ltail: ∀L,I,V. ∃∃J,K,W. L.ⓑ{I}V = ⓑ{J}W.K & |L| = |K|. +#L elim L -L /2 width=5 by ex2_3_intro/ +#L #Z #X #IHL #I #V elim (IHL Z X) -IHL +#J #K #W #H #_ >H -H >ltail_length +@(ex2_3_intro … J (K.ⓑ{I}V) W) // +qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| → + L1 = L2 ∧ K1 = K2. +#K1 elim K1 -K1 +[ * /2 width=1 by conj/ + #K2 #I2 #V2 #L1 #L2 #_ >length_atom >length_pair + #H elim (ysucc_inv_O_sn … H) +| #K1 #I1 #V1 #IH * + [ #L1 #L2 #_ >length_atom >length_pair + #H elim (ysucc_inv_O_dx … H) + | #K2 #I2 #V2 #L1 #L2 #H1 #H2 + elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *) + elim (IH … H1) -IH -H1 /3 width=1 by ysucc_inv_inj, conj/ + ] +] +qed-. + +(* Note: lemma 750 *) +lemma append_inj_dx: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |L1| = |L2| → + L1 = L2 ∧ K1 = K2. +#K1 elim K1 -K1 +[ * /2 width=1 by conj/ + #K2 #I2 #V2 #L1 #L2 >append_atom >append_pair #H destruct + >length_pair >append_length append_pair >append_atom #H destruct + >length_pair >append_length append_pair >append_pair #H1 #H2 + elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *) + elim (IH … H1) -IH -H1 /2 width=1 by conj/ + ] +] +qed-. + +lemma append_inv_refl_dx: ∀L,K. L @@ K = L → K = ⋆. +#L #K #H elim (append_inj_dx … (⋆) … H) // +qed-. + +lemma append_inv_pair_dx: ∀I,L,K,V. L @@ K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V. +#I #L #K #V #H elim (append_inj_dx … (⋆.ⓑ{I}V) … H) // +qed-. + +lemma length_inv_pos_dx_ltail: ∀L,l. |L| = ⫯l → + ∃∃I,K,V. |K| = l & L = ⓑ{I}V.K. +#Y #l #H elim (length_inv_pos_dx … H) -H #I #L #V #Hl #HLK destruct +elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/ +qed-. + +lemma length_inv_pos_sn_ltail: ∀L,l. ⫯l = |L| → + ∃∃I,K,V. l = |K| & L = ⓑ{I}V.K. +#Y #l #H elim (length_inv_pos_sn … H) -H #I #L #V #Hl #HLK destruct +elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/ +qed-. + +(* Basic eliminators ********************************************************) + +(* Basic_1: was: c_tail_ind *) +lemma lenv_ind_alt: ∀R:predicate lenv. + R (⋆) → (∀I,L,T. R L → R (ⓑ{I}T.L)) → + ∀L. R L. +#R #IH1 #IH2 #L @(ynat_f_ind … length … L) -L #x #IHx * // -IH1 +#L #I #V #H destruct elim (lpair_ltail L I V) +/4 width=1 by monotonic_ylt_plus_sn/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.ma new file mode 100644 index 000000000..7a0cdfc92 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.ma @@ -0,0 +1,59 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/lenv.ma". + +(* LENGTH OF A LOCAL ENVIRONMENT ********************************************) + +let rec length L ≝ match L with +[ LAtom ⇒ 0 +| LPair L _ _ ⇒ ⫯(length L) +]. + +interpretation "length (local environment)" 'card L = (length L). + +(* Basic properties *********************************************************) + +lemma length_atom: |⋆| = 0. +// qed. + +lemma length_pair: ∀I,L,V. |L.ⓑ{I}V| = ⫯|L|. +// qed. + +lemma length_inj: ∀L. |L| < ∞. +#L elim L -L /2 width=1 by ylt_succ_Y/ +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma length_inv_zero_dx: ∀L. |L| = 0 → L = ⋆. +* // #L #I #V >length_pair +#H elim (ysucc_inv_O_dx … H) +qed-. + +lemma length_inv_zero_sn: ∀L. yinj 0 = |L| → L = ⋆. +/2 width=1 by length_inv_zero_dx/ qed-. + +lemma length_inv_pos_dx: ∀l,L. |L| = ⫯l → + ∃∃I,K,V. |K| = l & L = K. ⓑ{I}V. +#l * /3 width=5 by ysucc_inj, ex2_3_intro/ +>length_atom #H elim (ysucc_inv_O_sn … H) +qed-. + +lemma length_inv_pos_sn: ∀l,L. ⫯l = |L| → + ∃∃I,K,V. l = |K| & L = K. ⓑ{I}V. +#l #L #H lapply (sym_eq ??? H) -H +#H elim (length_inv_pos_dx … H) -H /2 width=5 by ex2_3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma index 97207c56c..cb69d3687 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma @@ -52,8 +52,8 @@ qed-. lemma eq_item0_dec: ∀I1,I2:item0. Decidable (I1 = I2). * #i1 * #i2 [2,3,4,6,7,8: @or_intror #H destruct ] -elim (eq_nat_dec i1 i2) /2 width=1 by or_introl/ -#Hni12 @or_intror #H destruct /2 width=1 by/ +[2: elim (eq_nat_dec i1 i2) |1,3: elim (eq_nat_dec i1 i2) ] /2 width=1 by or_introl/ +#Hni12 @or_intror #H destruct /2 width=1 by/ qed-. (* Basic_1: was: bind_dec *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma deleted file mode 100644 index 0afb82db5..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma +++ /dev/null @@ -1,131 +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/notation/functions/append_2.ma". -include "basic_2/notation/functions/snbind2_3.ma". -include "basic_2/notation/functions/snabbr_2.ma". -include "basic_2/notation/functions/snabst_2.ma". -include "basic_2/grammar/lenv_length.ma". - -(* LOCAL ENVIRONMENTS *******************************************************) - -let rec append L K on K ≝ match K with -[ LAtom ⇒ L -| LPair K I V ⇒ (append L K). ⓑ{I} V -]. - -interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2). - -interpretation "local environment tail binding construction (binary)" - 'SnBind2 I T L = (append (LPair LAtom I T) L). - -interpretation "tail abbreviation (local environment)" - 'SnAbbr T L = (append (LPair LAtom Abbr T) L). - -interpretation "tail abstraction (local environment)" - 'SnAbst L T = (append (LPair LAtom Abst T) L). - -definition d_appendable_sn: predicate (lenv→relation term) ≝ λR. - ∀K,T1,T2. R K T1 T2 → ∀L. R (L @@ K) T1 T2. - -(* Basic properties *********************************************************) - -lemma append_atom_sn: ∀L. ⋆ @@ L = L. -#L elim L -L normalize // -qed. - -lemma append_assoc: associative … append. -#L1 #L2 #L3 elim L3 -L3 normalize // -qed. - -lemma append_length: ∀L1,L2. |L1 @@ L2| = |L1| + |L2|. -#L1 #L2 elim L2 -L2 normalize // -qed. - -lemma ltail_length: ∀I,L,V. |ⓑ{I}V.L| = |L| + 1. -#I #L #V >append_length // -qed. - -(* Basic_1: was just: chead_ctail *) -lemma lpair_ltail: ∀L,I,V. ∃∃J,K,W. L.ⓑ{I}V = ⓑ{J}W.K & |L| = |K|. -#L elim L -L /2 width=5 by ex2_3_intro/ -#L #Z #X #IHL #I #V elim (IHL Z X) -IHL -#J #K #W #H #_ >H -H >ltail_length -@(ex2_3_intro … J (K.ⓑ{I}V) W) // -qed-. - -(* Basic inversion lemmas ***************************************************) - -lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| → - L1 = L2 ∧ K1 = K2. -#K1 elim K1 -K1 -[ * normalize /2 width=1 by conj/ - #K2 #I2 #V2 #L1 #L2 #_ append_length in H2; #H - elim (plus_xySz_x_false … H) -| #K1 #I1 #V1 #IH * normalize - [ #L1 #L2 #H1 #H2 destruct - normalize in H2; >append_length in H2; #H - elim (plus_xySz_x_false … (sym_eq … H)) - | #K2 #I2 #V2 #L1 #L2 #H1 #H2 - elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *) - elim (IH … H1) -IH -H1 /2 width=1 by conj/ - ] -] -qed-. - -lemma append_inv_refl_dx: ∀L,K. L @@ K = L → K = ⋆. -#L #K #H elim (append_inj_dx … (⋆) … H) // -qed-. - -lemma append_inv_pair_dx: ∀I,L,K,V. L @@ K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V. -#I #L #K #V #H elim (append_inj_dx … (⋆.ⓑ{I}V) … H) // -qed-. - -lemma length_inv_pos_dx_ltail: ∀L,l. |L| = l + 1 → - ∃∃I,K,V. |K| = l & L = ⓑ{I}V.K. -#Y #l #H elim (length_inv_pos_dx … H) -H #I #L #V #Hl #HLK destruct -elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/ -qed-. - -lemma length_inv_pos_sn_ltail: ∀L,l. l + 1 = |L| → - ∃∃I,K,V. l = |K| & L = ⓑ{I}V.K. -#Y #l #H elim (length_inv_pos_sn … H) -H #I #L #V #Hl #HLK destruct -elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/ -qed-. - -(* Basic eliminators ********************************************************) - -(* Basic_1: was: c_tail_ind *) -lemma lenv_ind_alt: ∀R:predicate lenv. - R (⋆) → (∀I,L,T. R L → R (ⓑ{I}T.L)) → - ∀L. R L. -#R #IH1 #IH2 #L @(f_ind … length … L) -L #x #IHx * // -IH1 -#L #I #V normalize #H destruct elim (lpair_ltail L I V) /3 width=1 by/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma deleted file mode 100644 index 7c31b59e7..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma +++ /dev/null @@ -1,52 +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/lenv.ma". - -(* LENGTH OF A LOCAL ENVIRONMENT ********************************************) - -let rec length L ≝ match L with -[ LAtom ⇒ 0 -| LPair L _ _ ⇒ length L + 1 -]. - -interpretation "length (local environment)" 'card L = (length L). - -(* Basic inversion lemmas ***************************************************) - -lemma length_inv_zero_dx: ∀L. |L| = 0 → L = ⋆. -* // #L #I #V normalize 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). @@ -168,14 +171,14 @@ 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 +#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 normalize // +#L1 #L2 #l #m #H elim H -L1 -L2 -l -m // qed-. (* Advanced inversion lemmas ************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees.ma deleted file mode 100644 index fd7ba1c91..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/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/multiple/frees_append.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_append.ma deleted file mode 100644 index ee8324cc9..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/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/multiple/frees_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lift.ma deleted file mode 100644 index 65b629206..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/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/multiple/frees_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/frees_lreq.ma deleted file mode 100644 index 606c95cfb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/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/multiple/mr2.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma deleted file mode 100644 index 71869b02b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2.ma +++ /dev/null @@ -1,73 +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/rat_3.ma". -include "basic_2/grammar/term_vector.ma". - -(* MULTIPLE RELOCATION WITH PAIRS *******************************************) - -inductive at: list2 ynat nat → relation nat ≝ -| at_nil: ∀i. at (◊) i i -| at_lt : ∀cs,l,m,i1,i2. yinj i1 < l → - at cs i1 i2 → at ({l, m} @ cs) i1 i2 -| at_ge : ∀cs,l,m,i1,i2. l ≤ yinj i1 → - at cs (i1 + m) i2 → at ({l, m} @ cs) i1 i2 -. - -interpretation "application (multiple relocation with pairs)" - 'RAt i1 cs i2 = (at cs i1 i2). - -(* Basic inversion lemmas ***************************************************) - -fact at_inv_nil_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → cs = ◊ → i1 = i2. -#cs #i1 #i2 * -cs -i1 -i2 -[ // -| #cs #l #m #i1 #i2 #_ #_ #H destruct -| #cs #l #m #i1 #i2 #_ #_ #H destruct -] -qed-. - -lemma at_inv_nil: ∀i1,i2. @⦃i1, ◊⦄ ≡ i2 → i1 = i2. -/2 width=3 by at_inv_nil_aux/ qed-. - -fact at_inv_cons_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → - ∀l,m,cs0. cs = {l, m} @ cs0 → - i1 < l ∧ @⦃i1, cs0⦄ ≡ i2 ∨ - l ≤ i1 ∧ @⦃i1 + m, cs0⦄ ≡ i2. -#cs #i1 #i2 * -cs -i1 -i2 -[ #i #l #m #cs #H destruct -| #cs1 #l1 #m1 #i1 #i2 #Hil1 #Hi12 #l2 #m2 #cs2 #H destruct /3 width=1 by or_introl, conj/ -| #cs1 #l1 #m1 #i1 #i2 #Hli1 #Hi12 #l2 #m2 #cs2 #H destruct /3 width=1 by or_intror, conj/ -] -qed-. - -lemma at_inv_cons: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 → - i1 < l ∧ @⦃i1, cs⦄ ≡ i2 ∨ - l ≤ i1 ∧ @⦃i1 + m, cs⦄ ≡ i2. -/2 width=3 by at_inv_cons_aux/ qed-. - -lemma at_inv_cons_lt: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 → - i1 < l → @⦃i1, cs⦄ ≡ i2. -#cs #l #m #i1 #m2 #H -elim (at_inv_cons … H) -H * // #Hli1 #_ #Hi1l -elim (ylt_yle_false … Hi1l Hli1) -qed-. - -lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 → - l ≤ i1 → @⦃i1 + m, cs⦄ ≡ i2. -#cs #l #m #i1 #m2 #H -elim (at_inv_cons … H) -H * // #Hi1l #_ #Hli1 -elim (ylt_yle_false … Hi1l Hli1) -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma deleted file mode 100644 index 3c5f8da5c..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_minus.ma +++ /dev/null @@ -1,75 +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_minus.ma". -include "basic_2/notation/relations/rminus_3.ma". -include "basic_2/multiple/mr2.ma". - -(* MULTIPLE RELOCATION WITH PAIRS *******************************************) - -inductive minuss: nat → relation (list2 ynat nat) ≝ -| minuss_nil: ∀i. minuss i (◊) (◊) -| minuss_lt : ∀cs1,cs2,l,m,i. yinj i < l → minuss i cs1 cs2 → - minuss i ({l, m} @ cs1) ({l - i, m} @ cs2) -| minuss_ge : ∀cs1,cs2,l,m,i. l ≤ yinj i → minuss (m + i) cs1 cs2 → - minuss i ({l, m} @ cs1) cs2 -. - -interpretation "minus (multiple relocation with pairs)" - 'RMinus cs1 i cs2 = (minuss i cs1 cs2). - -(* Basic inversion lemmas ***************************************************) - -fact minuss_inv_nil1_aux: ∀cs1,cs2,i. cs1 ▭ i ≡ cs2 → cs1 = ◊ → cs2 = ◊. -#cs1 #cs2 #i * -cs1 -cs2 -i -[ // -| #cs1 #cs2 #l #m #i #_ #_ #H destruct -| #cs1 #cs2 #l #m #i #_ #_ #H destruct -] -qed-. - -lemma minuss_inv_nil1: ∀cs2,i. ◊ ▭ i ≡ cs2 → cs2 = ◊. -/2 width=4 by minuss_inv_nil1_aux/ qed-. - -fact minuss_inv_cons1_aux: ∀cs1,cs2,i. cs1 ▭ i ≡ cs2 → - ∀l,m,cs. cs1 = {l, m} @ cs → - l ≤ i ∧ cs ▭ m + i ≡ cs2 ∨ - ∃∃cs0. i < l & cs ▭ i ≡ cs0 & - cs2 = {l - i, m} @ cs0. -#cs1 #cs2 #i * -cs1 -cs2 -i -[ #i #l #m #cs #H destruct -| #cs1 #cs #l1 #m1 #i1 #Hil1 #Hcs #l2 #m2 #cs2 #H destruct /3 width=3 by ex3_intro, or_intror/ -| #cs1 #cs #l1 #m1 #i1 #Hli1 #Hcs #l2 #m2 #cs2 #H destruct /3 width=1 by or_introl, conj/ -] -qed-. - -lemma minuss_inv_cons1: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 → - l ≤ i ∧ cs1 ▭ m + i ≡ cs2 ∨ - ∃∃cs. i < l & cs1 ▭ i ≡ cs & - cs2 = {l - i, m} @ cs. -/2 width=3 by minuss_inv_cons1_aux/ qed-. - -lemma minuss_inv_cons1_ge: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 → - l ≤ i → cs1 ▭ m + i ≡ cs2. -#cs1 #cs2 #l #m #i #H -elim (minuss_inv_cons1 … H) -H * // #cs #Hil #_ #_ #Hli -elim (ylt_yle_false … Hil Hli) -qed-. - -lemma minuss_inv_cons1_lt: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 → - i < l → - ∃∃cs. cs1 ▭ i ≡ cs & cs2 = {l - i, m} @ cs. -#cs1 #cs2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/ -#Hli #_ #Hil elim (ylt_yle_false … Hil Hli) -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_mr2.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_mr2.ma deleted file mode 100644 index 858773399..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_mr2.ma +++ /dev/null @@ -1,29 +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/mr2.ma". - -(* MULTIPLE RELOCATION WITH PAIRS *******************************************) - -(* Main properties **********************************************************) - -theorem at_mono: ∀cs,i,i1. @⦃i, cs⦄ ≡ i1 → ∀i2. @⦃i, cs⦄ ≡ i2 → i1 = i2. -#cs #i #i1 #H elim H -cs -i -i1 -[ #i #x #H <(at_inv_nil … H) -x // -| #cs #l #m #i #i1 #Hil #_ #IHi1 #x #H - lapply (at_inv_cons_lt … H Hil) -H -Hil /2 width=1 by/ -| #cs #l #m #i #i1 #Hli #_ #IHi1 #x #H - lapply (at_inv_cons_ge … H Hli) -H -Hli /2 width=1 by/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma deleted file mode 100644 index 455b669be..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/mr2_plus.ma +++ /dev/null @@ -1,47 +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/multiple/mr2.ma". - -(* MULTIPLE RELOCATION WITH PAIRS *******************************************) - -let rec pluss (cs:list2 ynat nat) (i:nat) on cs ≝ match cs with -[ nil2 ⇒ ◊ -| cons2 l m cs ⇒ {l + i, m} @ pluss cs i -]. - -interpretation "plus (multiple relocation with pairs)" - 'plus x y = (pluss x y). - -(* Basic properties *********************************************************) - -lemma pluss_SO2: ∀l,m,cs. ({l, m} @ cs) + 1 = {⫯l, m} @ cs + 1. -// qed. - -(* Basic inversion lemmas ***************************************************) - -lemma pluss_inv_nil2: ∀i,cs. cs + i = ◊ → cs = ◊. -#i * // normalize -#l #m #cs #H destruct -qed. - -lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = {l, m} @ cs2 → - ∃∃cs1. cs1 + i = cs2 & cs = {l - i, m} @ cs1. -#i #l #m #cs2 * -[ normalize #H destruct -| #l1 #m1 #cs1 whd in ⊢ (??%?→?); #H destruct - >yplus_minus_inj /2 width=3 by ex2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_3.ma new file mode 100644 index 000000000..d9cfb81bd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_3.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 T ⦄ ≡ break term 46 f )" + non associative with precedence 45 + for @{ 'FreeStar $L $T $f }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rat_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rat_3.ma deleted file mode 100644 index a63dc95f2..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rat_3.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( @ ⦃ term 46 T1 , break term 46 f ⦄ ≡ break term 46 T2 )" - non associative with precedence 45 - for @{ 'RAt $T1 $f $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rminus_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rminus_3.ma deleted file mode 100644 index c896a982f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rminus_3.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( T1 ▭ break term 46 T2 ≡ break term 46 T )" - non associative with precedence 45 - for @{ 'RMinus $T1 $T2 $T }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index b23fb9de8..5f8451a27 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -12,11 +12,17 @@ (* *) (**************************************************************************) +include "ground_2/notation/functions/successor_1.ma". +include "ground_2/notation/functions/predecessor_1.ma". include "arithmetics/nat.ma". include "ground_2/lib/star.ma". (* ARITHMETICAL PROPERTIES **************************************************) +interpretation "nat successor" 'Successor m = (S m). + +interpretation "nat predecessor" 'Predecessor m = (pred m). + (* Iota equations ***********************************************************) lemma pred_O: pred 0 = 0. @@ -133,6 +139,9 @@ lemma lt_zero_false: ∀n. n < 0 → ⊥. #n #H elim (lt_to_not_le … H) -H /2 width=1 by/ qed-. +lemma lt_le_false: ∀x,y. x < y → y ≤ x → ⊥. +/3 width=4 by lt_refl_false, lt_to_le_to_lt/ qed-. + lemma pred_inv_refl: ∀m. pred m = m → m = 0. * // normalize #m #H elim (lt_refl_false m) // qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma index 9355f9c56..e72b54531 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma @@ -28,6 +28,14 @@ interpretation "nil (list)" 'Nil = (nil ?). interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl). +let rec length (A:Type[0]) (l:list A) on l ≝ match l with +[ nil ⇒ 0 +| cons _ l ⇒ length A l + 1 +]. + +interpretation "length (list)" + 'card l = (length ? l). + let rec all A (R:predicate A) (l:list A) on l ≝ match l with [ nil ⇒ ⊤ diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rafter_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rafter_3.ma new file mode 100644 index 000000000..d36582711 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rafter_3.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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( f1 ⊚ break term 46 f2 ≡ break term 46 f )" + non associative with precedence 45 + for @{ 'RAfter $f1 $f2 $f }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rat_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rat_3.ma new file mode 100644 index 000000000..8b99f61cd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rat_3.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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( @ ⦃ term 46 T1 , break term 46 f ⦄ ≡ break term 46 T2 )" + non associative with precedence 45 + for @{ 'RAt $T1 $f $T2 }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rminus_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rminus_3.ma new file mode 100644 index 000000000..1d397e536 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/rminus_3.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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( T1 ▭ break term 46 T2 ≡ break term 46 T )" + non associative with precedence 45 + for @{ 'RMinus $T1 $T2 $T }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/runion_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/runion_3.ma new file mode 100644 index 000000000..16120c08d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/runion_3.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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( L1 ⋓ break term 46 L2 ≡ break term 46 L )" + non associative with precedence 45 + for @{ 'RUnion $L1 $L2 $L }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_at.ma new file mode 100644 index 000000000..b3517a77b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_at.ma @@ -0,0 +1,84 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/rat_3.ma". +include "ground_2/relocation/mr2.ma". + +(* MULTIPLE RELOCATION WITH PAIRS *******************************************) + +inductive at: mr2 → relation nat ≝ +| at_nil: ∀i. at (◊) i i +| at_lt : ∀cs,l,m,i1,i2. i1 < l → + at cs i1 i2 → at ({l, m} @ cs) i1 i2 +| at_ge : ∀cs,l,m,i1,i2. l ≤ i1 → + at cs (i1 + m) i2 → at ({l, m} @ cs) i1 i2 +. + +interpretation "application (multiple relocation with pairs)" + 'RAt i1 cs i2 = (at cs i1 i2). + +(* Basic inversion lemmas ***************************************************) + +fact at_inv_nil_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → cs = ◊ → i1 = i2. +#cs #i1 #i2 * -cs -i1 -i2 +[ // +| #cs #l #m #i1 #i2 #_ #_ #H destruct +| #cs #l #m #i1 #i2 #_ #_ #H destruct +] +qed-. + +lemma at_inv_nil: ∀i1,i2. @⦃i1, ◊⦄ ≡ i2 → i1 = i2. +/2 width=3 by at_inv_nil_aux/ qed-. + +fact at_inv_cons_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → + ∀l,m,cs0. cs = {l, m} @ cs0 → + i1 < l ∧ @⦃i1, cs0⦄ ≡ i2 ∨ + l ≤ i1 ∧ @⦃i1 + m, cs0⦄ ≡ i2. +#cs #i1 #i2 * -cs -i1 -i2 +[ #i #l #m #cs #H destruct +| #cs1 #l1 #m1 #i1 #i2 #Hil1 #Hi12 #l2 #m2 #cs2 #H destruct /3 width=1 by or_introl, conj/ +| #cs1 #l1 #m1 #i1 #i2 #Hli1 #Hi12 #l2 #m2 #cs2 #H destruct /3 width=1 by or_intror, conj/ +] +qed-. + +lemma at_inv_cons: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 → + i1 < l ∧ @⦃i1, cs⦄ ≡ i2 ∨ + l ≤ i1 ∧ @⦃i1 + m, cs⦄ ≡ i2. +/2 width=3 by at_inv_cons_aux/ qed-. + +lemma at_inv_cons_lt: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 → + i1 < l → @⦃i1, cs⦄ ≡ i2. +#cs #l #m #i1 #m2 #H +elim (at_inv_cons … H) -H * // #Hli1 #_ #Hi1l +elim (lt_le_false … Hi1l Hli1) +qed-. + +lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 → + l ≤ i1 → @⦃i1 + m, cs⦄ ≡ i2. +#cs #l #m #i1 #m2 #H +elim (at_inv_cons … H) -H * // #Hi1l #_ #Hli1 +elim (lt_le_false … Hi1l Hli1) +qed-. + +(* Main properties **********************************************************) + +theorem at_mono: ∀cs,i,i1. @⦃i, cs⦄ ≡ i1 → ∀i2. @⦃i, cs⦄ ≡ i2 → i1 = i2. +#cs #i #i1 #H elim H -cs -i -i1 +[ #i #x #H <(at_inv_nil … H) -x // +| #cs #l #m #i #i1 #Hil #_ #IHi1 #x #H + lapply (at_inv_cons_lt … H Hil) -H -Hil /2 width=1 by/ +| #cs #l #m #i #i1 #Hli #_ #IHi1 #x #H + lapply (at_inv_cons_ge … H Hli) -H -Hli /2 width=1 by/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_minus.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_minus.ma new file mode 100644 index 000000000..9fd40ad6b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_minus.ma @@ -0,0 +1,74 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/rminus_3.ma". +include "ground_2/relocation/mr2.ma". + +(* MULTIPLE RELOCATION WITH PAIRS *******************************************) + +inductive minuss: nat → relation mr2 ≝ +| minuss_nil: ∀i. minuss i (◊) (◊) +| minuss_lt : ∀cs1,cs2,l,m,i. i < l → minuss i cs1 cs2 → + minuss i ({l, m} @ cs1) ({l - i, m} @ cs2) +| minuss_ge : ∀cs1,cs2,l,m,i. l ≤ i → minuss (m + i) cs1 cs2 → + minuss i ({l, m} @ cs1) cs2 +. + +interpretation "minus (multiple relocation with pairs)" + 'RMinus cs1 i cs2 = (minuss i cs1 cs2). + +(* Basic inversion lemmas ***************************************************) + +fact minuss_inv_nil1_aux: ∀cs1,cs2,i. cs1 ▭ i ≡ cs2 → cs1 = ◊ → cs2 = ◊. +#cs1 #cs2 #i * -cs1 -cs2 -i +[ // +| #cs1 #cs2 #l #m #i #_ #_ #H destruct +| #cs1 #cs2 #l #m #i #_ #_ #H destruct +] +qed-. + +lemma minuss_inv_nil1: ∀cs2,i. ◊ ▭ i ≡ cs2 → cs2 = ◊. +/2 width=4 by minuss_inv_nil1_aux/ qed-. + +fact minuss_inv_cons1_aux: ∀cs1,cs2,i. cs1 ▭ i ≡ cs2 → + ∀l,m,cs. cs1 = {l, m} @ cs → + l ≤ i ∧ cs ▭ m + i ≡ cs2 ∨ + ∃∃cs0. i < l & cs ▭ i ≡ cs0 & + cs2 = {l - i, m} @ cs0. +#cs1 #cs2 #i * -cs1 -cs2 -i +[ #i #l #m #cs #H destruct +| #cs1 #cs #l1 #m1 #i1 #Hil1 #Hcs #l2 #m2 #cs2 #H destruct /3 width=3 by ex3_intro, or_intror/ +| #cs1 #cs #l1 #m1 #i1 #Hli1 #Hcs #l2 #m2 #cs2 #H destruct /3 width=1 by or_introl, conj/ +] +qed-. + +lemma minuss_inv_cons1: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 → + l ≤ i ∧ cs1 ▭ m + i ≡ cs2 ∨ + ∃∃cs. i < l & cs1 ▭ i ≡ cs & + cs2 = {l - i, m} @ cs. +/2 width=3 by minuss_inv_cons1_aux/ qed-. + +lemma minuss_inv_cons1_ge: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 → + l ≤ i → cs1 ▭ m + i ≡ cs2. +#cs1 #cs2 #l #m #i #H +elim (minuss_inv_cons1 … H) -H * // #cs #Hil #_ #_ #Hli +elim (lt_le_false … Hil Hli) +qed-. + +lemma minuss_inv_cons1_lt: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 → + i < l → + ∃∃cs. cs1 ▭ i ≡ cs & cs2 = {l - i, m} @ cs. +#cs1 #cs2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/ +#Hli #_ #Hil elim (lt_le_false … Hil Hli) +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma new file mode 100644 index 000000000..11ffaa407 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/mr2.ma". + +(* MULTIPLE RELOCATION WITH PAIRS *******************************************) + +let rec pluss (cs:mr2) (i:nat) on cs ≝ match cs with +[ nil2 ⇒ ◊ +| cons2 l m cs ⇒ {l + i, m} @ pluss cs i +]. + +interpretation "plus (multiple relocation with pairs)" + 'plus x y = (pluss x y). + +(* Basic properties *********************************************************) + +lemma pluss_SO2: ∀l,m,cs. ({l, m} @ cs) + 1 = {⫯l, m} @ cs + 1. +normalize // qed. + +(* Basic inversion lemmas ***************************************************) + +lemma pluss_inv_nil2: ∀i,cs. cs + i = ◊ → cs = ◊. +#i * // normalize +#l #m #cs #H destruct +qed. + +lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = {l, m} @ cs2 → + ∃∃cs1. cs1 + i = cs2 & cs = {l - i, m} @ cs1. +#i #l #m #cs2 * +[ normalize #H destruct +| #l1 #m1 #cs1 whd in ⊢ (??%?→?); #H destruct + (IH … Htl) -tl -cs1 -x // +| #cs1 #cs2 #x #_ #IH #y #H elim (after_inv_false1 … H) -H + #tly #H #Htl destruct >(IH … Htl) -cs1 -cs2 -x // +] +qed-. + +theorem after_inj: ∀cs1,x,cs. cs1 ⊚ x ≡ cs → ∀y. cs1 ⊚ y ≡ cs → x = y. +#cs1 #x #cs #H elim H -cs1 -x -cs +[ #y #H elim (after_inv_empty1 … H) -H // +| #cs1 #x #cs #_ #b #IH #y #H elim (after_inv_true1 … H) -H + #tly #tl #b0 #H1 #H2 #Htl destruct >(IH … Htl) -tl -cs1 -x // +| #cs1 #x #cs #_ #IH #y #H elim (after_inv_false1 … H) -H + #tl #H #Htl destruct >(IH … Htl) -tl -cs1 -x // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma new file mode 100644 index 000000000..f4b6f8d3a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma @@ -0,0 +1,193 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/rat_3.ma". +include "ground_2/relocation/trace.ma". + +(* RELOCATION TRACE *********************************************************) + +inductive at: trace → relation nat ≝ + | at_zero : ∀cs. at (Ⓣ @ cs) 0 0 + | at_succ : ∀cs,i,j. at cs i j → at (Ⓣ @ cs) (⫯i) (⫯j) + | at_false: ∀cs,i,j. at cs i j → at (Ⓕ @ cs) i (⫯j). + +interpretation "relocation (trace)" + 'RAt i1 cs i2 = (at cs i1 i2). + +(* Basic inversion lemmas ***************************************************) + +fact at_inv_empty_aux: ∀cs,i,j. @⦃i, cs⦄ ≡ j → cs = ◊ → ⊥. +#cs #i #j * -cs -i -j +#cs [2,3: #i #j #_ ] #H destruct +qed-. + +lemma at_inv_empty: ∀i,j. @⦃i, ◊⦄ ≡ j → ⊥. +/2 width=5 by at_inv_empty_aux/ qed-. + +fact at_inv_true_aux: ∀cs,i,j. @⦃i, cs⦄ ≡ j → ∀tl. cs = Ⓣ @ tl → + (i = 0 ∧ j = 0) ∨ + ∃∃i0,j0. i = ⫯i0 & j = ⫯j0 & @⦃i0, tl⦄ ≡ j0. +#cs #i #j * -cs -i -j +#cs [2,3: #i #j #Hij ] #tl #H destruct +/3 width=5 by ex3_2_intro, or_introl, or_intror, conj/ +qed-. + +lemma at_inv_true: ∀cs,i,j. @⦃i, Ⓣ @ cs⦄ ≡ j → + (i = 0 ∧ j = 0) ∨ + ∃∃i0,j0. i = ⫯i0 & j = ⫯j0 & @⦃i0, cs⦄ ≡ j0. +/2 width=3 by at_inv_true_aux/ qed-. + +lemma at_inv_true_zero_sn: ∀cs,j. @⦃0, Ⓣ @ cs⦄ ≡ j → j = 0. +#cs #j #H elim (at_inv_true … H) -H * // +#i0 #j0 #H destruct +qed-. + +lemma at_inv_true_zero_dx: ∀cs,i. @⦃i, Ⓣ @ cs⦄ ≡ 0 → i = 0. +#cs #i #H elim (at_inv_true … H) -H * // +#i0 #j0 #_ #H destruct +qed-. + +lemma at_inv_true_succ_sn: ∀cs,i,j. @⦃⫯i, Ⓣ @ cs⦄ ≡ j → + ∃∃j0. j = ⫯j0 & @⦃i, cs⦄ ≡ j0. +#cs #i #j #H elim (at_inv_true … H) -H * +[ #H destruct +| #i0 #j0 #H1 #H2 destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma at_inv_true_succ_dx: ∀cs,i,j. @⦃i, Ⓣ @ cs⦄ ≡ ⫯j → + ∃∃i0. i = ⫯i0 & @⦃i0, cs⦄ ≡ j. +#cs #i #j #H elim (at_inv_true … H) -H * +[ #_ #H destruct +| #i0 #j0 #H1 #H2 destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma at_inv_true_succ: ∀cs,i,j. @⦃⫯i, Ⓣ @ cs⦄ ≡ ⫯j → + @⦃i, cs⦄ ≡ j. +#cs #i #j #H elim (at_inv_true … H) -H * +[ #H destruct +| #i0 #j0 #H1 #H2 destruct // +] +qed-. + +lemma at_inv_true_O_S: ∀cs,j. @⦃0, Ⓣ @ cs⦄ ≡ ⫯j → ⊥. +#cs #j #H elim (at_inv_true … H) -H * +[ #_ #H destruct +| #i0 #j0 #H1 destruct +] +qed-. + +lemma at_inv_true_S_O: ∀cs,i. @⦃⫯i, Ⓣ @ cs⦄ ≡ 0 → ⊥. +#cs #i #H elim (at_inv_true … H) -H * +[ #H destruct +| #i0 #j0 #_ #H1 destruct +] +qed-. + +fact at_inv_false_aux: ∀cs,i,j. @⦃i, cs⦄ ≡ j → ∀tl. cs = Ⓕ @ tl → + ∃∃j0. j = ⫯j0 & @⦃i, tl⦄ ≡ j0. +#cs #i #j * -cs -i -j +#cs [2,3: #i #j #Hij ] #tl #H destruct +/2 width=3 by ex2_intro/ +qed-. + +lemma at_inv_false: ∀cs,i,j. @⦃i, Ⓕ @ cs⦄ ≡ j → + ∃∃j0. j = ⫯j0 & @⦃i, cs⦄ ≡ j0. +/2 width=3 by at_inv_false_aux/ qed-. + +lemma at_inv_false_S: ∀cs,i,j. @⦃i, Ⓕ @ cs⦄ ≡ ⫯j → @⦃i, cs⦄ ≡ j. +#cs #i #j #H elim (at_inv_false … H) -H +#j0 #H destruct // +qed-. + +lemma at_inv_false_O: ∀cs,i. @⦃i, Ⓕ @ cs⦄ ≡ 0 → ⊥. +#cs #i #H elim (at_inv_false … H) -H +#j0 #H destruct +qed-. + +(* Basic properties *********************************************************) + +lemma at_monotonic: ∀cs,i2,j2. @⦃i2, cs⦄ ≡ j2 → ∀i1. i1 < i2 → + ∃∃j1. @⦃i1, cs⦄ ≡ j1 & j1 < j2. +#cs #i2 #j2 #H elim H -cs -i2 -j2 +[ #cs #i1 #H elim (lt_zero_false … H) +| #cs #i #j #Hij #IH * /2 width=3 by ex2_intro, at_zero/ + #i1 #H lapply (lt_S_S_to_lt … H) -H + #H elim (IH … H) -i + #j1 #Hij1 #H /3 width=3 by le_S_S, ex2_intro, at_succ/ +| #cs #i #j #_ #IH #i1 #H elim (IH … H) -i + /3 width=3 by le_S_S, ex2_intro, at_false/ +] +qed-. + +lemma at_at_dec: ∀cs,i,j. Decidable (@⦃i, cs⦄ ≡ j). +#cs elim cs -cs [ | * #cs #IH ] +[ /3 width=3 by at_inv_empty, or_intror/ +| * [2: #i ] * [2,4: #j ] + [ elim (IH i j) -IH + /4 width=1 by at_inv_true_succ, at_succ, or_introl, or_intror/ + | -IH /3 width=3 by at_inv_true_O_S, or_intror/ + | -IH /3 width=3 by at_inv_true_S_O, or_intror/ + | -IH /2 width=1 by or_introl, at_zero/ + ] +| #i * [2: #j ] + [ elim (IH i j) -IH + /4 width=1 by at_inv_false_S, at_false, or_introl, or_intror/ + | -IH /3 width=3 by at_inv_false_O, or_intror/ + ] +] +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma at_increasing: ∀cs,i,j. @⦃i, cs⦄ ≡ j → i ≤ j. +#cs #i elim i -i // +#i0 #IHi #j #H elim (at_monotonic … H i0) -H +/3 width=3 by le_to_lt_to_lt/ +qed-. + +lemma at_length_lt: ∀cs,i,j. @⦃i, cs⦄ ≡ j → j < |cs|. +#cs elim cs -cs [ | * #cs #IH ] #i #j #H normalize +[ elim (at_inv_empty … H) +| elim (at_inv_true … H) * -H // + #i0 #j0 #H1 #H2 #Hij0 destruct /3 width=2 by le_S_S/ +| elim (at_inv_false … H) -H + #j0 #H #H0 destruct /3 width=2 by le_S_S/ +] +qed-. + +(* Main properties **********************************************************) + +theorem at_mono: ∀cs,i,j1. @⦃i, cs⦄ ≡ j1 → ∀j2. @⦃i, cs⦄ ≡ j2 → j1 = j2. +#cs #i #j1 #H elim H -cs -i -j1 +#cs [ |2,3: #i #j1 #_ #IH ] #j2 #H +[ lapply (at_inv_true_zero_sn … H) -H // +| elim (at_inv_true_succ_sn … H) -H + #j0 #H destruct #H >(IH … H) -cs -i -j1 // +| elim (at_inv_false … H) -H + #j0 #H destruct #H >(IH … H) -cs -i -j1 // +] +qed-. + +theorem at_inj: ∀cs,i1,j. @⦃i1, cs⦄ ≡ j → ∀i2. @⦃i2, cs⦄ ≡ j → i1 = i2. +#cs #i1 #j #H elim H -cs -i1 -j +#cs [ |2,3: #i1 #j #_ #IH ] #i2 #H +[ lapply (at_inv_true_zero_dx … H) -H // +| elim (at_inv_true_succ_dx … H) -H + #i0 #H destruct #H >(IH … H) -cs -i1 -j // +| elim (at_inv_false … H) -H + #j0 #H destruct #H >(IH … H) -cs -i1 -j0 // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sor.ma new file mode 100644 index 000000000..f4e79a6ce --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_sor.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/runion_3.ma". +include "ground_2/relocation/trace.ma". + +(* RELOCATION TRACE *********************************************************) + +inductive sor: relation3 trace trace trace ≝ + | sor_empty: sor (◊) (◊) (◊) + | sor_inh : ∀cs1,cs2,cs. sor cs1 cs2 cs → + ∀b1,b2. sor (b1 @ cs1) (b2 @ cs2) ((b1 ∨ b2) @ cs). + +interpretation + "union (trace)" + 'RUnion L1 L2 L = (sor L2 L1 L). + +(* Basic properties *********************************************************) + +lemma sor_sym: ∀cs1,cs2,cs. cs1 ⋓ cs2 ≡ cs → cs2 ⋓ cs1 ≡ cs. +#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs /2 width=1 by sor_inh/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml index af06ffa1d..19c11b207 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml @@ -12,6 +12,9 @@ and its timeline. + + Multiple relocation with lists of booleans. + Natural numbers with infinity. diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index 0ba823065..2c23eacc1 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -9,6 +9,15 @@ table { ] } ] + class "green" + [ { "multiple relocation" * } { + [ { "" * } { + [ "trace" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" * ] + [ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ] + } + ] + } + ] class "grass" [ { "natural numbers with infinity" * } { [ { "" * } { @@ -23,7 +32,7 @@ table { class "yellow" [ { "extensions to the library" * } { [ { "" * } { - [ "star" "lstar" "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? )" + [ "star" "lstar" "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ⫯? ) ( ⫰? )" "list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" * ] } diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma index 613a9793c..1a986f03c 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_le.ma @@ -83,7 +83,7 @@ qed-. (* Inversion lemmas on successor ********************************************) -fact yle_inv_succ1_aux: ∀x,y. x ≤ y → ∀m. x = ⫯m → m ≤ ⫰y ∧ ⫯⫰y = y. +fact yle_inv_succ1_aux: ∀x,y:ynat. x ≤ y → ∀m. x = ⫯m → m ≤ ⫰y ∧ ⫯⫰y = y. #x #y * -x -y [ #x #y #Hxy #m #H elim (ysucc_inv_inj_sn … H) -H #n #H1 #H2 destruct elim (le_inv_S1 … Hxy) -Hxy @@ -92,7 +92,7 @@ fact yle_inv_succ1_aux: ∀x,y. x ≤ y → ∀m. x = ⫯m → m ≤ ⫰y ∧ ] qed-. -lemma yle_inv_succ1: ∀m,y. ⫯m ≤ y → m ≤ ⫰y ∧ ⫯⫰y = y. +lemma yle_inv_succ1: ∀m,y:ynat. ⫯m ≤ y → m ≤ ⫰y ∧ ⫯⫰y = y. /2 width=3 by yle_inv_succ1_aux/ qed-. lemma yle_inv_succ: ∀m,n. ⫯m ≤ ⫯n → m ≤ n. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma index 2a9fbb515..664510dda 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma @@ -64,14 +64,14 @@ lemma ylt_inv_Y2: ∀x:ynat. x < ∞ → ∃n. x = yinj n. #H elim (ylt_inv_Y1 … H) qed-. -lemma ylt_inv_O1: ∀n. 0 < n → ⫯⫰n = n. +lemma ylt_inv_O1: ∀n:ynat. 0 < n → ⫯⫰n = n. * // #n #H lapply (ylt_inv_inj … H) -H normalize /3 width=1 by S_pred, eq_f/ qed-. (* Inversion lemmas on successor ********************************************) -fact ylt_inv_succ1_aux: ∀x,y. x < y → ∀m. x = ⫯m → m < ⫰y ∧ ⫯⫰y = y. +fact ylt_inv_succ1_aux: ∀x,y:ynat. x < y → ∀m. x = ⫯m → m < ⫰y ∧ ⫯⫰y = y. #x #y * -x -y [ #x #y #Hxy #m #H elim (ysucc_inv_inj_sn … H) -H #n #H1 #H2 destruct elim (le_inv_S1 … Hxy) -Hxy @@ -81,7 +81,7 @@ fact ylt_inv_succ1_aux: ∀x,y. x < y → ∀m. x = ⫯m → m < ⫰y ∧ ⫯⫰ ] qed-. -lemma ylt_inv_succ1: ∀m,y. ⫯m < y → m < ⫰y ∧ ⫯⫰y = y. +lemma ylt_inv_succ1: ∀m,y:ynat. ⫯m < y → m < ⫰y ∧ ⫯⫰y = y. /2 width=3 by ylt_inv_succ1_aux/ qed-. lemma ylt_inv_succ: ∀m,n. ⫯m < ⫯n → m < n. @@ -130,14 +130,14 @@ qed-. (* Basic properties *********************************************************) -lemma ylt_O1: ∀x. ⫯⫰x = x → 0 < x. +lemma ylt_O1: ∀x:ynat. ⫯⫰x = x → 0 < x. * // * /2 width=1 by ylt_inj/ normalize #H destruct qed. (* Properties on predecessor ************************************************) -lemma ylt_pred: ∀m,n. m < n → 0 < m → ⫰m < ⫰n. +lemma ylt_pred: ∀m,n:ynat. m < n → 0 < m → ⫰m < ⫰n. #m #n * -m -n /4 width=1 by ylt_inv_inj, ylt_inj, monotonic_lt_pred/ qed. @@ -155,10 +155,14 @@ qed. lemma ylt_succ_Y: ∀x. x < ∞ → ⫯x < ∞. * /2 width=1 by/ qed. -lemma yle_succ1_inj: ∀x,y. ⫯yinj x ≤ y → x < y. +lemma yle_succ1_inj: ∀x. ∀y:ynat. ⫯yinj x ≤ y → x < y. #x * /3 width=1 by yle_inv_inj, ylt_inj/ qed. +lemma ylt_succ2_refl: ∀x,y:ynat. x < y → x < ⫯x. +#x #y #H elim (ylt_fwd_gen … H) -y /2 width=1 by ylt_inj/ +qed. + (* Properties on order ******************************************************) lemma yle_split_eq: ∀m,n:ynat. m ≤ n → m < n ∨ m = n. @@ -195,7 +199,7 @@ lemma yle_ylt_trans: ∀x:ynat. ∀y:ynat. ∀z:ynat. y < z → x ≤ y → x < ] qed-. -lemma yle_inv_succ1_lt: ∀x,y. ⫯x ≤ y → 0 < y ∧ x ≤ ⫰y. +lemma yle_inv_succ1_lt: ∀x,y:ynat. ⫯x ≤ y → 0 < y ∧ x ≤ ⫰y. #x #y #H elim (yle_inv_succ1 … H) -H /3 width=1 by ylt_O1, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma index e710032b0..16a933acf 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma @@ -93,12 +93,12 @@ qed. (* Inversion lemmas on successor *********************************************) -lemma yplus_inv_succ_lt_dx: ∀x,y,z. 0 < y → x + y = ⫯z → x + ⫰y = z. +lemma yplus_inv_succ_lt_dx: ∀x,y,z:ynat. 0 < y → x + y = ⫯z → x + ⫰y = z. #x #y #z #H <(ylt_inv_O1 y) // >yplus_succ2 /2 width=1 by ysucc_inv_inj/ qed-. -lemma yplus_inv_succ_lt_sn: ∀x,y,z. 0 < x → x + y = ⫯z → ⫰x + y = z. +lemma yplus_inv_succ_lt_sn: ∀x,y,z:ynat. 0 < x → x + y = ⫯z → ⫰x + y = z. #x #y #z #H <(ylt_inv_O1 x) // >yplus_succ1 /2 width=1 by ysucc_inv_inj/ diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma index 1f14ea6c0..8d17df7ff 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma @@ -20,16 +20,16 @@ include "ground_2/ynat/ynat.ma". (* the predecessor function *) definition ypred: ynat → ynat ≝ λm. match m with -[ yinj m ⇒ pred m +[ yinj m ⇒ ⫰m | Y ⇒ Y ]. interpretation "ynat predecessor" 'Predecessor m = (ypred m). -lemma ypred_O: ⫰0 = 0. +lemma ypred_O: ⫰(yinj 0) = yinj 0. // qed. -lemma ypred_S: ∀m:nat. ⫰(S m) = m. +lemma ypred_S: ∀m:nat. ⫰(⫯m) = yinj m. // qed. lemma ypred_Y: (⫰∞) = ∞. @@ -37,7 +37,7 @@ lemma ypred_Y: (⫰∞) = ∞. (* Inversion lemmas *********************************************************) -lemma ypred_inv_refl: ∀m. ⫰m = m → m = 0 ∨ m = ∞. +lemma ypred_inv_refl: ∀m:ynat. ⫰m = m → m = 0 ∨ m = ∞. * // #m #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *) /4 width=1 by pred_inv_refl, or_introl, eq_f/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma index c4c989f77..be5bef707 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma @@ -19,13 +19,13 @@ include "ground_2/ynat/ynat_pred.ma". (* the successor function *) definition ysucc: ynat → ynat ≝ λm. match m with -[ yinj m ⇒ S m +[ yinj m ⇒ ⫯m | Y ⇒ Y ]. interpretation "ynat successor" 'Successor m = (ysucc m). -lemma ysucc_inj: ∀m:nat. ⫯m = S m. +lemma ysucc_inj: ∀m:nat. ⫯(yinj m) = yinj (⫯m). // qed. lemma ysucc_Y: ⫯(∞) = ∞. @@ -36,7 +36,7 @@ lemma ysucc_Y: ⫯(∞) = ∞. lemma ypred_succ: ∀m. ⫰⫯m = m. * // qed. -lemma ynat_cases: ∀n:ynat. n = 0 ∨ ∃m. n = ⫯m. +lemma ynat_cases: ∀n:ynat. n = 0 ∨ ∃m:ynat. n = ⫯m. * [ * /2 width=1 by or_introl/ #n @or_intror @(ex_intro … n) // (**) (* explicit constructor *) @@ -86,7 +86,7 @@ lemma ysucc_inv_O_sn: ∀m. yinj 0 = ⫯m → ⊥. (**) (* explicit coercion *) #n #_ #H destruct qed-. -lemma ysucc_inv_O_dx: ∀m. ⫯m = 0 → ⊥. +lemma ysucc_inv_O_dx: ∀m:ynat. ⫯m = 0 → ⊥. /2 width=2 by ysucc_inv_O_sn/ qed-. (* Eliminators **************************************************************) diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 3b04c75b3..7d0ab3a8e 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1561,7 +1561,7 @@ let predefined_classes = [ ["M"; "ℳ"; "𝕄"; "𝐌"; "Ⓜ"; ] ; ["n"; "𝕟"; "𝐧"; "𝛈"; "ⓝ"; ] ; ["N"; "ℕ"; "№"; "𝐍"; "Ⓝ"; ] ; - ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "ø"; "○"; "𝐨"; "𝛉"; "ⓞ"; ] ; + ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "⊚"; "ø"; "○"; "𝐨"; "𝛉"; "ⓞ"; ] ; ["O"; "Θ"; "𝕆"; "𝐎"; "𝚯"; "𝚹"; "Ⓞ"; ] ; ["p"; "π"; "𝕡"; "𝐩"; "𝛑"; "ⓟ"; ] ; ["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; ] ;