From: Ferruccio Guidi Date: Sun, 8 Jun 2014 17:40:37 +0000 (+0000) Subject: - some work on append X-Git-Tag: make_still_working~910 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=a2092f7ba4c7c566ea90653ff57e4623ab94d8d5 - some work on append - some corrections and some annotations --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/append/ldrop_append.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/append/ldrop_append.etc deleted file mode 100644 index 1fa09a012..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/append/ldrop_append.etc +++ /dev/null @@ -1,60 +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_append.ma". -include "basic_2/relocation/ldrop.ma". - -(* DROPPING *****************************************************************) - -(* Properties on append for local environments ******************************) - -fact ldrop_O1_append_sn_le_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → - d = 0 → e ≤ |L1| → - ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2. -#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e normalize -[2,3,4: /4 width=1 by ldrop_skip_lt, ldrop_drop, arith_b1, lt_minus_to_plus_r, monotonic_pred/ ] -#d #e #_ #_ #H <(le_n_O_to_eq … H) -H // -qed-. - -lemma ldrop_O1_append_sn_le: ∀L1,L2,s,e. ⇩[s, 0, e] L1 ≡ L2 → e ≤ |L1| → - ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2. -/2 width=3 by ldrop_O1_append_sn_le_aux/ qed. - -(* Inversion lemmas on append for local environments ************************) - -lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K → - |L2| ≤ e → ⇩[s, 0, e - |L2|] L1 ≡ K. -#K #L1 #L2 elim L2 -L2 normalize // -#L2 #I #V #IHL2 #s #e #H #H1e -elim (ldrop_inv_O1_pair1 … H) -H * #H2e #HL12 destruct -[ lapply (le_n_O_to_eq … H1e) -H1e -IHL2 - >commutative_plus normalize #H destruct -| minus_minus_comm /3 width=1 by monotonic_pred/ -] -qed-. - -lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K → e ≤ |L2| → - ∀K2. ⇩[s, 0, e] L2 ≡ K2 → K = L1 @@ K2. -#K #L1 #L2 elim L2 -L2 normalize -[ #s #e #H1 #H2 #K2 #H3 lapply (le_n_O_to_eq … H2) -H2 - #H2 elim (ldrop_inv_atom1 … H3) -H3 #H3 #_ destruct - >(ldrop_inv_O2 … H1) -H1 // -| #L2 #I #V #IHL2 #s #e @(nat_ind_plus … e) -e [ -IHL2 ] - [ #H1 #_ #K2 #H2 - lapply (ldrop_inv_O2 … H1) -H1 #H1 - lapply (ldrop_inv_O2 … H2) -H2 #H2 destruct // - | /4 width=7 by ldrop_inv_drop1, le_plus_to_le_r/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/append/lenv_append.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/append/lenv_append.etc new file mode 100644 index 000000000..234c2666b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/append/lenv_append.etc @@ -0,0 +1,27 @@ +lemma length_inv_pos_dx_append: ∀d,L. |L| = d + 1 → + ∃∃I,K,V. |K| = d & L = ⋆.ⓑ{I}V @@ K. +#d @(nat_ind_plus … d) -d +[ #L #H + elim (length_inv_pos_dx … H) -H #I #K #V #H + >(length_inv_zero_dx … H) -H #H destruct + @ex2_3_intro [4: /2 width=2/ |5: // |1,2,3: skip ] (**) (* /3/ does not work *) +| #d #IHd #L #H + elim (length_inv_pos_dx … H) -H #I #K #V #H + elim (IHd … H) -IHd -H #I0 #K0 #V0 #H1 #H2 #H3 destruct + @(ex2_3_intro … (K0.ⓑ{I}V)) // +] +qed-. + +lemma length_inv_pos_sn_append: ∀d,L. 1 + d = |L| → + ∃∃I,K,V. d = |K| & L = ⋆. ⓑ{I}V @@ K. +#d >commutative_plus @(nat_ind_plus … d) -d +[ #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct + >(length_inv_zero_sn … H1) -K + @(ex2_3_intro … (⋆)) // (**) (* explicit constructor *) +| #d #IHd #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct + >H1 in IHd; -H1 #IHd + elim (IHd K) -IHd // #J #L #W #H1 #H2 destruct + @(ex2_3_intro … (L.ⓑ{I}V)) // (**) (* explicit constructor *) + >append_length /2 width=1/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma index 95e155b74..c34238632 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma @@ -46,15 +46,13 @@ axiom eq_lenv_dec: ∀L1,L2:lenv. Decidable (L1 = L2). lemma destruct_lpair_lpair: ∀I1,I2,L1,L2,V1,V2. L1.ⓑ{I1}V1 = L2.ⓑ{I2}V2 → ∧∧L1 = L2 & I1 = I2 & V1 = V2. -#I1 #I2 #L1 #L2 #V1 #V2 #H destruct /2 width=1/ +#I1 #I2 #L1 #L2 #V1 #V2 #H destruct /2 width=1 by and3_intro/ qed-. lemma discr_lpair_x_xy: ∀I,V,L. L = L.ⓑ{I}V → ⊥. #I #V #L elim L -L [ #H destruct | #L #J #W #IHL #H - elim (destruct_lpair_lpair … H) -H #H1 #H2 #H3 destruct /2 width=1/ (**) (* destruct lemma needed *) + elim (destruct_lpair_lpair … H) -H #H1 #H2 #H3 destruct /2 width=1 by/ (**) (* destruct lemma needed *) ] qed-. - -(* Basic_1: removed theorems 2: chead_ctail c_tail_ind *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma index 8771d46fb..61b0648b6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma @@ -13,6 +13,9 @@ (**************************************************************************) 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 *******************************************************) @@ -24,6 +27,15 @@ let rec append L K on K ≝ match K with 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 l_appendable_sn: predicate (lenv→relation term) ≝ λR. ∀K,T1,T2. R K T1 T2 → ∀L. R (L @@ K) T1 T2. @@ -41,18 +53,30 @@ 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/ +[ * normalize /2 width=1 by conj/ #K2 #I2 #V2 #L1 #L2 #_ append_length in H2; #H elim (plus_xySz_x_false … H) @@ -71,64 +95,25 @@ lemma append_inj_dx: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |L1| = |L2| → elim (plus_xySz_x_false … (sym_eq … H)) | #K2 #I2 #V2 #L1 #L2 #H1 #H2 elim (destruct_lpair_lpair … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *) - elim (IH … H1) -IH -H1 // -H2 /2 width=1/ + 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) // +#L #K #H elim (append_inj_dx … (⋆) … H) // qed-. lemma append_inv_pair_dx: ∀I,L,K,V. L @@ K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V. -#I #L #K #V #H -elim (append_inj_dx … (⋆.ⓑ{I}V) … H) // -qed-. - -lemma length_inv_pos_dx_append: ∀d,L. |L| = d + 1 → - ∃∃I,K,V. |K| = d & L = ⋆.ⓑ{I}V @@ K. -#d @(nat_ind_plus … d) -d -[ #L #H - elim (length_inv_pos_dx … H) -H #I #K #V #H - >(length_inv_zero_dx … H) -H #H destruct - @ex2_3_intro [4: /2 width=2/ |5: // |1,2,3: skip ] (**) (* /3/ does not work *) -| #d #IHd #L #H - elim (length_inv_pos_dx … H) -H #I #K #V #H - elim (IHd … H) -IHd -H #I0 #K0 #V0 #H1 #H2 #H3 destruct - @(ex2_3_intro … (K0.ⓑ{I}V)) // -] +#I #L #K #V #H elim (append_inj_dx … (⋆.ⓑ{I}V) … H) // qed-. (* Basic_eliminators ********************************************************) -fact lenv_ind_dx_aux: ∀R:predicate lenv. R (⋆) → - (∀I,L,V. R L → R (⋆.ⓑ{I}V @@ L)) → - ∀d,L. |L| = d → R L. -#R #Hatom #Hpair #d @(nat_ind_plus … d) -d -[ #L #H >(length_inv_zero_dx … H) -H // -| #d #IH #L #H - elim (length_inv_pos_dx_append … H) -H #I #K #V #H1 #H2 destruct /3 width=1/ -] -qed-. - -lemma lenv_ind_dx: ∀R:predicate lenv. R (⋆) → - (∀I,L,V. R L → R (⋆.ⓑ{I}V @@ L)) → - ∀L. R L. -/3 width=2 by lenv_ind_dx_aux/ qed-. - -(* Advanced inversion lemmas ************************************************) - -lemma length_inv_pos_sn_append: ∀d,L. 1 + d = |L| → - ∃∃I,K,V. d = |K| & L = ⋆. ⓑ{I}V @@ K. -#d >commutative_plus @(nat_ind_plus … d) -d -[ #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct - >(length_inv_zero_sn … H1) -K - @(ex2_3_intro … (⋆)) // (**) (* explicit constructor *) -| #d #IHd #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct - >H1 in IHd; -H1 #IHd - elim (IHd K) -IHd // #J #L #W #H1 #H2 destruct - @(ex2_3_intro … (L.ⓑ{I}V)) // (**) (* explicit constructor *) - >append_length /2 width=1/ -] +(* 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 #n #IHn * // -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/multiple/llor.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor.ma index df157a990..4f3d948de 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor.ma @@ -23,7 +23,7 @@ definition llor: ynat → relation4 term lenv lenv lenv ≝ λd,T,L2,L1,L. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → ⇩[i] L ≡ K.ⓑ{I}V → ∨∨ (∧∧ yinj i < d & I1 = I & V1 = V) | (∧∧ (L1 ⊢ i ϵ 𝐅*[d]⦃T⦄ → ⊥) & I1 = I & V1 = V) | - (∧∧ d ≤ yinj i & L1 ⊢ i ϵ 𝐅*[d]⦃T⦄ & I1 = I & V2 = V) + (∧∧ d ≤ yinj i & L1 ⊢ i ϵ 𝐅*[d]⦃T⦄ & I1 = I & V2 = V) ). interpretation diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_etc.ma new file mode 100644 index 000000000..4ed8f333d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_etc.ma @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/ldrop_append.ma". +include "basic_2/multiple/llor_ldrop.ma". + +(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************) + +lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y. +/2 width=1 by monotonic_pred/ qed-. + +(* +lemma llor_tail_frees: ∀L1,L2,L,U,d. L1 ⩖[U, d] L2 ≡ L → d < yinj (|L1|) → + ∀I1,W1. ⓑ{I1}W1.L1 ⊢ |L1| ϵ 𝐅*[d]⦃U⦄ → + ∀I2,W2. ⓑ{I1}W1.L1 ⩖[U, d] ⓑ{I2}W2.L2 ≡ ⓑ{I1}W2.L. +#L1 #L2 #L #U #d * #HL12 #HL1 #IH #Hd #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 (ldrop_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 (ldrop_O1_lt (Ⓕ) … H) #Z1 #Y1 #X1 #HLY1 + elim (ldrop_O1_lt (Ⓕ) L2 i) [2: /2 width=3 by lt_to_le_to_lt/ ] #Z2 #Y2 #X2 #HLY2 + elim (ldrop_O1_lt (Ⓕ) L i) // #Z #Y #X #HLY + lapply (ldrop_O1_inv_append1_le … HLK1 … HLY1) /2 width=1 by lt_to_le/ -HLK1 normalize #H destruct + lapply (ldrop_O1_inv_append1_le … HLK2 … HLY2) /3 width=3 by lt_to_le_to_lt, lt_to_le/ -HLK2 normalize #H destruct + lapply (ldrop_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/ + | #HnU #HZ #HX + | #Hdi #H2U #HZ #HX + ] +| -IH destruct + lapply (ldrop_O1_inv_append1_le … HLK1 … (⋆) ?) // -HLK1 normalize #H destruct + lapply (ldrop_O1_inv_append1_le … HLK2 … HL12) + lapply (ldrop_O1_inv_append1_le … HLK … (⋆) ?) // -HLK normalize #H destruct + @or3_intro2 @and4_intro /2 width=1 by ylt_fwd_le/ +] +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma index b766269e7..f24744291 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_ldrop.ma @@ -19,4 +19,12 @@ include "basic_2/multiple/llor.ma". (* Advanced properties ******************************************************) +lemma llor_skip: ∀L1,L2,U,d. |L1| ≤ |L2| → yinj (|L1|) ≤ d → L1 ⩖[U, d] L2 ≡ L1. +#L1 #L2 #U #d #HL12 #Hd @and3_intro // -HL12 +#I1 #I2 #I #K1 #K2 #K #W1 #W2 #W #i #HLK1 #_ #HLK -I2 -L2 -K2 +lapply (ldrop_mono … HLK … HLK1) -HLK #H destruct +lapply (ldrop_fwd_length_lt2 … HLK1) -K1 +/5 width=3 by ylt_yle_trans, ylt_inj, or3_intro0, and3_intro/ +qed. + axiom llor_total: ∀L1,L2,T,d. |L1| ≤ |L2| → ∃L. L1 ⩖[T, d] L2 ≡ L. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snabbr_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snabbr_2.ma new file mode 100644 index 000000000..4051c2085 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snabbr_2.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( ⓓ term 55 T . break term 55 L )" + non associative with precedence 55 + for @{ 'SnAbbr $T $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snabst_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snabst_2.ma new file mode 100644 index 000000000..838bd007f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snabst_2.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( ⓛ term 55 T . break term 55 L )" + non associative with precedence 55 + for @{ 'SnAbst $T $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snbind2_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snbind2_3.ma new file mode 100644 index 000000000..fa44f2928 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snbind2_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( ⓑ { term 46 I } break term 55 T . break term 55 L )" + non associative with precedence 55 + for @{ 'SnBind2 $I $T $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma index 97eab47d4..c8b2b11f2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma @@ -233,6 +233,10 @@ lemma ldrop_O1_ge: ∀L,e. |L| ≤ e → ⇩[Ⓣ, 0, e] L ≡ ⋆. normalize /4 width=1 by ldrop_drop, monotonic_pred/ qed. +lemma ldrop_O1_eq: ∀L,s. ⇩[s, 0, |L|] L ≡ ⋆. +#L elim L -L /2 width=1 by ldrop_drop, ldrop_atom/ +qed. + lemma ldrop_split: ∀L1,L2,d,e2,s. ⇩[s, d, e2] L1 ≡ L2 → ∀e1. e1 ≤ e2 → ∃∃L. ⇩[s, d, e2 - e1] L1 ≡ L & ⇩[s, d, e1] L ≡ L2. #L1 #L2 #d #e2 #s #H elim H -L1 -L2 -d -e2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma new file mode 100644 index 000000000..bbc493ebb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma @@ -0,0 +1,60 @@ +(**************************************************************************) +(* ___ *) +(* ||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_append.ma". +include "basic_2/substitution/ldrop.ma". + +(* DROPPING *****************************************************************) + +(* Properties on append for local environments ******************************) + +fact ldrop_O1_append_sn_le_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → + d = 0 → e ≤ |L1| → + ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2. +#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e normalize +[2,3,4: /4 width=1 by ldrop_skip_lt, ldrop_drop, arith_b1, lt_minus_to_plus_r, monotonic_pred/ ] +#d #e #_ #_ #H <(le_n_O_to_eq … H) -H // +qed-. + +lemma ldrop_O1_append_sn_le: ∀L1,L2,s,e. ⇩[s, 0, e] L1 ≡ L2 → e ≤ |L1| → + ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2. +/2 width=3 by ldrop_O1_append_sn_le_aux/ qed. + +(* Inversion lemmas on append for local environments ************************) + +lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K → + |L2| ≤ e → ⇩[s, 0, e - |L2|] L1 ≡ K. +#K #L1 #L2 elim L2 -L2 normalize // +#L2 #I #V #IHL2 #s #e #H #H1e +elim (ldrop_inv_O1_pair1 … H) -H * #H2e #HL12 destruct +[ lapply (le_n_O_to_eq … H1e) -H1e -IHL2 + >commutative_plus normalize #H destruct +| minus_minus_comm /3 width=1 by monotonic_pred/ +] +qed-. + +lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K → e ≤ |L2| → + ∀K2. ⇩[s, 0, e] L2 ≡ K2 → K = L1 @@ K2. +#K #L1 #L2 elim L2 -L2 normalize +[ #s #e #H1 #H2 #K2 #H3 lapply (le_n_O_to_eq … H2) -H2 + #H2 elim (ldrop_inv_atom1 … H3) -H3 #H3 #_ destruct + >(ldrop_inv_O2 … H1) -H1 // +| #L2 #I #V #IHL2 #s #e @(nat_ind_plus … e) -e [ -IHL2 ] + [ #H1 #_ #K2 #H2 + lapply (ldrop_inv_O2 … H1) -H1 #H1 + lapply (ldrop_inv_O2 … H2) -H2 #H2 destruct // + | /4 width=7 by ldrop_inv_drop1, le_plus_to_le_r/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 4df84d5c8..ea0a44131 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -274,7 +274,7 @@ table { } ] [ { "basic local env. slicing" * } { - [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_leq" + "ldrop_ldrop" * ] + [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_append" + "ldrop_leq" + "ldrop_ldrop" * ] } ] [ { "basic term relocation" * } {