X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Fldrop.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Fldrop.ma;h=c3219f4f46903d059f139f7179fc771beaf96f4c;hb=0aa60d67f17b528b896e05bbd01038cbc195f69d;hp=b4d3355d6bd4c38d249a9f9246b08343f37d18fe;hpb=62a926c1a14562bf158941156c6032c0c8d86fbe;p=helm.git diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma index b4d3355d6..c3219f4f4 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma @@ -20,19 +20,19 @@ include "Basic_2/substitution/lift.ma". (* Basic_1: includes: ldrop_skip_bind *) inductive ldrop: nat → nat → relation lenv ≝ -| ldrop_atom: ∀d,e. ldrop d e (⋆) (⋆) -| ldrop_pair: ∀L,I,V. ldrop 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V) +| ldrop_atom : ∀d,e. ldrop d e (⋆) (⋆) +| ldrop_pair : ∀L,I,V. ldrop 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V) | ldrop_ldrop: ∀L1,L2,I,V,e. ldrop 0 e L1 L2 → ldrop 0 (e + 1) (L1. 𝕓{I} V) L2 -| ldrop_skip: ∀L1,L2,I,V1,V2,d,e. - ldrop d e L1 L2 → ↑[d,e] V2 ≡ V1 → - ldrop (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2) +| ldrop_skip : ∀L1,L2,I,V1,V2,d,e. + ldrop d e L1 L2 → ⇑[d,e] V2 ≡ V1 → + ldrop (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2) . -interpretation "local slicing" 'RDrop d e L1 L2 = (ldrop d e L1 L2). +interpretation "local slicing" 'RLDrop d e L1 L2 = (ldrop d e L1 L2). (* Basic inversion lemmas ***************************************************) -fact ldrop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2. +fact ldrop_inv_refl_aux: ∀d,e,L1,L2. ⇓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2. #d #e #L1 #L2 * -d -e -L1 -L2 [ // | // @@ -42,10 +42,10 @@ fact ldrop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 qed. (* Basic_1: was: ldrop_gen_refl *) -lemma ldrop_inv_refl: ∀L1,L2. ↓[0, 0] L1 ≡ L2 → L1 = L2. +lemma ldrop_inv_refl: ∀L1,L2. ⇓[0, 0] L1 ≡ L2 → L1 = L2. /2 width=5/ qed-. -fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ → +fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ⇓[d, e] L1 ≡ L2 → L1 = ⋆ → L2 = ⋆. #d #e #L1 #L2 * -d -e -L1 -L2 [ // @@ -56,13 +56,13 @@ fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ → qed. (* Basic_1: was: ldrop_gen_sort *) -lemma ldrop_inv_atom1: ∀d,e,L2. ↓[d, e] ⋆ ≡ L2 → L2 = ⋆. +lemma ldrop_inv_atom1: ∀d,e,L2. ⇓[d, e] ⋆ ≡ L2 → L2 = ⋆. /2 width=5/ qed-. -fact ldrop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → +fact ldrop_inv_O1_aux: ∀d,e,L1,L2. ⇓[d, e] L1 ≡ L2 → d = 0 → ∀K,I,V. L1 = K. 𝕓{I} V → (e = 0 ∧ L2 = K. 𝕓{I} V) ∨ - (0 < e ∧ ↓[d, e - 1] K ≡ L2). + (0 < e ∧ ⇓[d, e - 1] K ≡ L2). #d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #K #I #V #H destruct | #L #I #V #_ #K #J #W #HX destruct /3 width=1/ @@ -71,23 +71,23 @@ fact ldrop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → ] qed. -lemma ldrop_inv_O1: ∀e,K,I,V,L2. ↓[0, e] K. 𝕓{I} V ≡ L2 → +lemma ldrop_inv_O1: ∀e,K,I,V,L2. ⇓[0, e] K. 𝕓{I} V ≡ L2 → (e = 0 ∧ L2 = K. 𝕓{I} V) ∨ - (0 < e ∧ ↓[0, e - 1] K ≡ L2). + (0 < e ∧ ⇓[0, e - 1] K ≡ L2). /2 width=3/ qed-. (* Basic_1: was: ldrop_gen_ldrop *) lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2. - ↓[0, e] K. 𝕓{I} V ≡ L2 → 0 < e → ↓[0, e - 1] K ≡ L2. + ⇓[0, e] K. 𝕓{I} V ≡ L2 → 0 < e → ⇓[0, e - 1] K ≡ L2. #e #K #I #V #L2 #H #He elim (ldrop_inv_O1 … H) -H * // #H destruct elim (lt_refl_false … He) qed-. -fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → +fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ⇓[d, e] L1 ≡ L2 → 0 < d → ∀I,K1,V1. L1 = K1. 𝕓{I} V1 → - ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 & - ↑[d - 1, e] V2 ≡ V1 & + ∃∃K2,V2. ⇓[d - 1, e] K1 ≡ K2 & + ⇑[d - 1, e] V2 ≡ V1 & L2 = K2. 𝕓{I} V2. #d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #I #K #V #H destruct @@ -98,16 +98,16 @@ fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → qed. (* Basic_1: was: ldrop_gen_skip_l *) -lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ↓[d, e] K1. 𝕓{I} V1 ≡ L2 → 0 < d → - ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 & - ↑[d - 1, e] V2 ≡ V1 & +lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ⇓[d, e] K1. 𝕓{I} V1 ≡ L2 → 0 < d → + ∃∃K2,V2. ⇓[d - 1, e] K1 ≡ K2 & + ⇑[d - 1, e] V2 ≡ V1 & L2 = K2. 𝕓{I} V2. /2 width=3/ qed-. -fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → +fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ⇓[d, e] L1 ≡ L2 → 0 < d → ∀I,K2,V2. L2 = K2. 𝕓{I} V2 → - ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & - ↑[d - 1, e] V2 ≡ V1 & + ∃∃K1,V1. ⇓[d - 1, e] K1 ≡ K2 & + ⇑[d - 1, e] V2 ≡ V1 & L1 = K1. 𝕓{I} V1. #d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #I #K #V #H destruct @@ -118,28 +118,28 @@ fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → qed. (* Basic_1: was: ldrop_gen_skip_r *) -lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d → - ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & ↑[d - 1, e] V2 ≡ V1 & +lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ⇓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d → + ∃∃K1,V1. ⇓[d - 1, e] K1 ≡ K2 & ⇑[d - 1, e] V2 ≡ V1 & L1 = K1. 𝕓{I} V1. /2 width=3/ qed-. (* Basic properties *********************************************************) (* Basic_1: was by definition: ldrop_refl *) -lemma ldrop_refl: ∀L. ↓[0, 0] L ≡ L. +lemma ldrop_refl: ∀L. ⇓[0, 0] L ≡ L. #L elim L -L // qed. lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e. - ↓[0, e - 1] L1 ≡ L2 → 0 < e → ↓[0, e] L1. 𝕓{I} V ≡ L2. + ⇓[0, e - 1] L1 ≡ L2 → 0 < e → ⇓[0, e] L1. 𝕓{I} V ≡ L2. #L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/ qed. lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → - ∀K1,V,i. ↓[0, i] L1 ≡ K1. 𝕓{Abbr} V → + ∀K1,V,i. ⇓[0, i] L1 ≡ K1. 𝕓{Abbr} V → d ≤ i → i < d + e → ∃∃K2. K1 [0, d + e - i - 1] ≼ K2 & - ↓[0, i] L2 ≡ K2. 𝕓{Abbr} V. + ⇓[0, i] L2 ≡ K2. 𝕓{Abbr} V. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e [ #d #e #K1 #V #i #H lapply (ldrop_inv_atom1 … H) -H #H destruct @@ -167,8 +167,8 @@ qed. (* Basic forvard lemmas *****************************************************) (* Basic_1: was: ldrop_S *) -lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ↓[O, e] L1 ≡ K2. 𝕓{I2} V2 → - ↓[O, e + 1] L1 ≡ K2. +lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇓[O, e] L1 ≡ K2. 𝕓{I2} V2 → + ⇓[O, e + 1] L1 ≡ K2. #L1 elim L1 -L1 [ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct | #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H @@ -179,7 +179,7 @@ lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ↓[O, e] L1 ≡ K2. 𝕓{I2} V2 → ] qed-. -lemma ldrop_fwd_lw: ∀L1,L2,d,e. ↓[d, e] L1 ≡ L2 → #[L2] ≤ #[L1]. +lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇓[d, e] L1 ≡ L2 → #[L2] ≤ #[L1]. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize [ /2 width=3/ | #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 @@ -188,7 +188,7 @@ lemma ldrop_fwd_lw: ∀L1,L2,d,e. ↓[d, e] L1 ≡ L2 → #[L2] ≤ #[L1]. qed-. lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e. - ↓[0, e] L1 ≡ K2. 𝕓{I2} V2 → e < |L1|. + ⇓[0, e] L1 ≡ K2. 𝕓{I2} V2 → e < |L1|. #L1 elim L1 -L1 [ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct | #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H @@ -199,7 +199,7 @@ lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e. ] qed-. -lemma ldrop_fwd_O1_length: ∀L1,L2,e. ↓[0, e] L1 ≡ L2 → |L2| = |L1| - e. +lemma ldrop_fwd_O1_length: ∀L1,L2,e. ⇓[0, e] L1 ≡ L2 → |L2| = |L1| - e. #L1 elim L1 -L1 [ #L2 #e #H >(ldrop_inv_atom1 … H) -H // | #K1 #I1 #V1 #IHL1 #L2 #e #H