From 0c7cb3c503c0fcab104ad89ebc88683dc9830d06 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 27 Jun 2016 18:54:28 +0000 Subject: [PATCH] lfpx_drops completed! --- .../basic_2/etc_new/llpx_sn/llpx_sn_drop.etc | 240 ------------------ .../lambdadelta/basic_2/relocation/drops.ma | 130 +++++----- .../basic_2/relocation/drops_ceq.ma | 2 +- .../basic_2/relocation/drops_lexs.ma | 73 +++--- .../basic_2/relocation/drops_lreq.ma | 13 +- .../basic_2/relocation/drops_lstar.ma | 10 +- .../lambdadelta/basic_2/rt_transition/cpx.ma | 8 +- .../basic_2/rt_transition/lfpx_drops.ma | 18 +- .../basic_2/rt_transition/partial.txt | 2 +- .../lambdadelta/basic_2/static/frees_drops.ma | 10 +- .../lambdadelta/basic_2/static/lfxs_drops.ma | 80 ++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 +- .../ground_2/relocation/rtmap_coafter.ma | 2 +- 13 files changed, 229 insertions(+), 363 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_drop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_drop.etc index 02e70f4fd..9bb605e39 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_drop.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_drop.etc @@ -167,246 +167,6 @@ lemma llpx_sn_dec: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) → -x /4 width=4 by llpx_sn_fwd_length, or_intror/ qed-. -(* Properties on relocation *************************************************) - -lemma llpx_sn_lift_le: ∀R. d_liftable R → - ∀K1,K2,T,l0. llpx_sn R l0 T K1 K2 → - ∀L1,L2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → - ∀U. ⬆[l, k] T ≡ U → l0 ≤ l → llpx_sn R l0 U L1 L2. -#R #HR #K1 #K2 #T #l0 #H elim H -K1 -K2 -T -l0 -[ #K1 #K2 #l0 #s #HK12 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X - lapply (drop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -l - /2 width=1 by llpx_sn_sort/ -| #K1 #K2 #l0 #i #HK12 #Hil0 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref1 … H) -H - * #Hli #H destruct - [ lapply (drop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -l - /2 width=1 by llpx_sn_skip/ - | elim (ylt_yle_false … Hil0) -L1 -L2 -K1 -K2 -k -Hil0 - /3 width=3 by yle_trans, yle_inj/ - ] -| #I #K1 #K2 #K11 #K22 #V1 #V2 #l0 #i #Hil0 #HK11 #HK22 #HK12 #HV12 #IHK12 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref1 … H) -H - * #Hli #H destruct [ -HK12 | -IHK12 ] - [ elim (drop_trans_lt … HLK1 … HK11) // -K1 - elim (drop_trans_lt … HLK2 … HK22) // -Hli -K2 - /3 width=18 by llpx_sn_lref/ - | lapply (drop_trans_ge_comm … HLK1 … HK11 ?) // -K1 - lapply (drop_trans_ge_comm … HLK2 … HK22 ?) // -Hli -Hl0 -K2 - /3 width=9 by llpx_sn_lref, yle_plus_dx1_trans/ - ] -| #K1 #K2 #l0 #i #HK1 #HK2 #HK12 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref1 … H) -H - * #Hil #H destruct - lapply (drop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12 - [ /3 width=7 by llpx_sn_free, drop_fwd_be/ - | lapply (drop_fwd_length … HLK1) -HLK1 #HLK1 - lapply (drop_fwd_length … HLK2) -HLK2 #HLK2 - @llpx_sn_free [ >HLK1 | >HLK2 ] -Hil -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *) - ] -| #K1 #K2 #l0 #p #HK12 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X - lapply (drop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -l -k - /2 width=1 by llpx_sn_gref/ -| #a #I #K1 #K2 #V #T #l0 #_ #_ #IHV #IHT #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_bind1 … H) -H - #W #U #HVW #HTU #H destruct /4 width=6 by llpx_sn_bind, drop_skip, yle_succ/ -| #I #K1 #K2 #V #T #l0 #_ #_ #IHV #IHT #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_flat1 … H) -H - #W #U #HVW #HTU #H destruct /3 width=6 by llpx_sn_flat/ -] -qed-. - -lemma llpx_sn_lift_ge: ∀R,K1,K2,T,l0. llpx_sn R l0 T K1 K2 → - ∀L1,L2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → - ∀U. ⬆[l, k] T ≡ U → l ≤ l0 → llpx_sn R (l0+k) U L1 L2. -#R #K1 #K2 #T #l0 #H elim H -K1 -K2 -T -l0 -[ #K1 #K2 #l0 #s #HK12 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X - lapply (drop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -l - /2 width=1 by llpx_sn_sort/ -| #K1 #K2 #l0 #i #HK12 #Hil0 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #_ elim (lift_inv_lref1 … H) -H - * #_ #H destruct - lapply (drop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 - [ /3 width=3 by llpx_sn_skip, ylt_plus_dx2_trans/ - | /3 width=3 by llpx_sn_skip, monotonic_ylt_plus_dx/ - ] -| #I #K1 #K2 #K11 #K22 #V1 #V2 #l0 #i #Hil0 #HK11 #HK22 #HK12 #HV12 #_ #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref1 … H) -H - * #Hil #H destruct - [ elim (ylt_yle_false … Hil0) -I -L1 -L2 -K1 -K2 -K11 -K22 -V1 -V2 -k -Hil0 - /3 width=3 by ylt_yle_trans, ylt_inj/ - | lapply (drop_trans_ge_comm … HLK1 … HK11 ?) // -K1 - lapply (drop_trans_ge_comm … HLK2 … HK22 ?) // -Hil -Hl0 -K2 - /3 width=9 by llpx_sn_lref, monotonic_yle_plus_dx/ - ] -| #K1 #K2 #l0 #i #HK1 #HK2 #HK12 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref1 … H) -H - * #Hil #H destruct - lapply (drop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12 - [ /3 width=7 by llpx_sn_free, drop_fwd_be/ - | lapply (drop_fwd_length … HLK1) -HLK1 #HLK1 - lapply (drop_fwd_length … HLK2) -HLK2 #HLK2 - @llpx_sn_free [ >HLK1 | >HLK2 ] -Hil -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *) - ] -| #K1 #K2 #l0 #p #HK12 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X - lapply (drop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -l - /2 width=1 by llpx_sn_gref/ -| #a #I #K1 #K2 #V #T #l0 #_ #_ #IHV #IHT #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_bind1 … H) -H - #W #U #HVW #HTU #H destruct /4 width=5 by llpx_sn_bind, drop_skip, yle_succ/ -| #I #K1 #K2 #V #T #l0 #_ #_ #IHV #IHT #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_flat1 … H) -H - #W #U #HVW #HTU #H destruct /3 width=5 by llpx_sn_flat/ -] -qed-. - -(* Inversion lemmas on relocation *******************************************) - -lemma llpx_sn_inv_lift_le: ∀R. d_deliftable_sn R → - ∀L1,L2,U,l0. llpx_sn R l0 U L1 L2 → - ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → - ∀T. ⬆[l, k] T ≡ U → l0 ≤ l → llpx_sn R l0 T K1 K2. -#R #HR #L1 #L2 #U #l0 #H elim H -L1 -L2 -U -l0 -[ #L1 #L2 #l0 #s #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X - lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l -k - /2 width=1 by llpx_sn_sort/ -| #L1 #L2 #l0 #i #HL12 #Hil0 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #_ elim (lift_inv_lref2 … H) -H - * #_ #H destruct - lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 - [ /2 width=1 by llpx_sn_skip/ - | /3 width=3 by llpx_sn_skip, yle_ylt_trans/ - ] -| #I #L1 #L2 #K11 #K22 #W1 #W2 #l0 #i #Hil0 #HLK11 #HLK22 #HK12 #HW12 #IHK12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref2 … H) -H - * #Hil #H destruct [ -HK12 | -IHK12 ] - [ elim (drop_conf_lt … HLK1 … HLK11) // -L1 #L1 #V1 #HKL1 #HKL11 #HVW1 - elim (drop_conf_lt … HLK2 … HLK22) // -Hil -L2 #L2 #V2 #HKL2 #HKL22 #HVW2 - elim (HR … HW12 … HKL11 … HVW1) -HR #V0 #HV0 #HV12 - lapply (lift_inj … HV0 … HVW2) -HV0 -HVW2 #H destruct - /3 width=10 by llpx_sn_lref/ - | lapply (drop_conf_ge … HLK1 … HLK11 ?) // -L1 - lapply (drop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hil0 - elim (yle_inv_plus_inj2 … Hil) -Hil /4 width=9 by llpx_sn_lref, yle_trans, yle_inj/ (**) (* slow *) - ] -| #L1 #L2 #l0 #i #HL1 #HL2 #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref2 … H) -H - * #_ #H destruct - lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) - [ lapply (drop_fwd_length_le4 … HLK1) -HLK1 - lapply (drop_fwd_length_le4 … HLK2) -HLK2 - #HKL2 #HKL1 #HK12 @llpx_sn_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *) - | lapply (drop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H - lapply (drop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H - /3 width=1 by llpx_sn_free, le_plus_to_minus_r/ - ] -| #L1 #L2 #l0 #p #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X - lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l -k - /2 width=1 by llpx_sn_gref/ -| #a #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_bind2 … H) -H - #V #T #HVW #HTU #H destruct /4 width=6 by llpx_sn_bind, drop_skip, yle_succ/ -| #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_flat2 … H) -H - #V #T #HVW #HTU #H destruct /3 width=6 by llpx_sn_flat/ -] -qed-. - -lemma llpx_sn_inv_lift_be: ∀R,L1,L2,U,l0. llpx_sn R l0 U L1 L2 → - ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → - ∀T. ⬆[l, k] T ≡ U → l ≤ l0 → l0 ≤ l + k → llpx_sn R l T K1 K2. -#R #L1 #L2 #U #l0 #H elim H -L1 -L2 -U -l0 -[ #L1 #L2 #l0 #s #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_sort2 … H) -X - lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l0 -k - /2 width=1 by llpx_sn_sort/ -| #L1 #L2 #l0 #i #HL12 #Hil0 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 #Hl0k elim (lift_inv_lref2 … H) -H - * #Hil #H destruct - [ lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 - -Hil0 /3 width=1 by llpx_sn_skip, ylt_inj/ - | elim (ylt_yle_false … Hil0) -L1 -L2 -Hl0 -Hil0 - /3 width=3 by yle_trans, yle_inj/ (**) (* slow *) - ] -| #I #L1 #L2 #K11 #K22 #W1 #W2 #l0 #i #Hil0 #HLK11 #HLK22 #HK12 #HW12 #_ #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 #Hl0k elim (lift_inv_lref2 … H) -H - * #Hil #H destruct - [ elim (ylt_yle_false … Hil0) -I -L1 -L2 -K11 -K22 -W1 -W2 -Hl0k -Hil0 - /3 width=3 by ylt_yle_trans, ylt_inj/ - | lapply (drop_conf_ge … HLK1 … HLK11 ?) // -L1 - lapply (drop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hil0 -Hl0 -Hl0k - elim (yle_inv_plus_inj2 … Hil) -Hil /3 width=9 by llpx_sn_lref, yle_inj/ - ] -| #L1 #L2 #l0 #i #HL1 #HL2 #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 #Hl0k elim (lift_inv_lref2 … H) -H - * #_ #H destruct - lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) - [ lapply (drop_fwd_length_le4 … HLK1) -HLK1 - lapply (drop_fwd_length_le4 … HLK2) -HLK2 - #HKL2 #HKL1 #HK12 @llpx_sn_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *) - | lapply (drop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H - lapply (drop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H - /3 width=1 by llpx_sn_free, le_plus_to_minus_r/ - ] -| #L1 #L2 #l0 #p #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_gref2 … H) -X - lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l0 -k - /2 width=1 by llpx_sn_gref/ -| #a #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 #Hl0k elim (lift_inv_bind2 … H) -H - #V #T #HVW #HTU #H destruct - @llpx_sn_bind [ /2 width=5 by/ ] -IHW (**) (* explicit constructor *) - @(IHU … HTU) -IHU -HTU /2 width=1 by drop_skip, yle_succ/ -| #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 #Hl0k elim (lift_inv_flat2 … H) -H - #V #T #HVW #HTU #H destruct /3 width=6 by llpx_sn_flat/ -] -qed-. - -lemma llpx_sn_inv_lift_ge: ∀R,L1,L2,U,l0. llpx_sn R l0 U L1 L2 → - ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → - ∀T. ⬆[l, k] T ≡ U → l + k ≤ l0 → llpx_sn R (l0-k) T K1 K2. -#R #L1 #L2 #U #l0 #H elim H -L1 -L2 -U -l0 -[ #L1 #L2 #l0 #s #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X - lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l - /2 width=1 by llpx_sn_sort/ -| #L1 #L2 #l0 #i #HL12 #Hil0 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hlml0 elim (lift_inv_lref2 … H) -H - * #Hil #H destruct [ -Hil0 | -Hlml0 ] - lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 - [ /4 width=3 by llpx_sn_skip, yle_plus1_to_minus_inj2, ylt_yle_trans, ylt_inj/ - | elim (yle_inv_plus_inj2 … Hil) -Hil - /3 width=1 by llpx_sn_skip, monotonic_ylt_minus_dx/ - ] -| #I #L1 #L2 #K11 #K22 #W1 #W2 #l0 #i #Hil0 #HLK11 #HLK22 #HK12 #HW12 #_ #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hlml0 elim (lift_inv_lref2 … H) -H - * #Hil #H destruct - [ elim (ylt_yle_false … Hil0) -I -L1 -L2 -K11 -K22 -W1 -W2 -Hil0 - /3 width=3 by yle_fwd_plus_sn1, ylt_yle_trans, ylt_inj/ - | lapply (drop_conf_ge … HLK1 … HLK11 ?) // -L1 - lapply (drop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hlml0 -Hil - /3 width=9 by llpx_sn_lref, monotonic_yle_minus_dx/ - ] -| #L1 #L2 #l0 #i #HL1 #HL2 #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hlml0 elim (lift_inv_lref2 … H) -H - * #_ #H destruct - lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) - [ lapply (drop_fwd_length_le4 … HLK1) -HLK1 - lapply (drop_fwd_length_le4 … HLK2) -HLK2 - #HKL2 #HKL1 #HK12 @llpx_sn_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *) - | lapply (drop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H - lapply (drop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H - /3 width=1 by llpx_sn_free, le_plus_to_minus_r/ - ] -| #L1 #L2 #l0 #p #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X - lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l - /2 width=1 by llpx_sn_gref/ -| #a #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hlml0 elim (lift_inv_bind2 … H) -H - #V #T #HVW #HTU #H destruct - @llpx_sn_bind [ /2 width=5 by/ ] -IHW (**) (* explicit constructor *) - (lexs_inv_atom1 … H) -X +(* Basic_2A1: includes: lpx_sn_deliftable_dropable *) (**) (* changed after commit 13218 *) +lemma lexs_co_dropable_sn: ∀RN,RP. co_dropable_sn (lexs RN RP). +#RN #RP #b #f #L1 #K1 #H elim H -f -L1 -K1 +[ #f #Hf #_ #f2 #X #H #f1 #Hf2 >(lexs_inv_atom1 … H) -X /4 width=3 by lexs_atom, drops_atom, ex2_intro/ -| #f #I #L1 #K1 #V1 #_ #IH #X #f2 #H #f1 #Hf2 elim (coafter_inv_nxx … Hf2) -Hf2 [2,3: // ] - #g2 #Hg2 #H2 destruct elim (lexs_inv_push1 … H) -H - #L2 #V2 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -g2 - /3 width=3 by drops_drop, ex2_intro/ -| #f #I #L1 #K1 #V1 #W1 #HLK #HWV #IH #X #f2 #H #f1 #Hf2 elim (coafter_inv_pxx … Hf2) -Hf2 [1,3:* |*: // ] - #g1 #g2 #Hg2 #H1 #H2 destruct - [ elim (lexs_inv_push1 … H) | elim (lexs_inv_next1 … H) ] -H - #L2 #V2 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -g2 - [ elim (HP … HV12 … HLK … HWV) | elim (HN … HV12 … HLK … HWV) ] -V1 - /3 width=5 by lexs_next, lexs_push, drops_skip, ex2_intro/ +| #f #I #L1 #K1 #V1 #_ #IH #Hf #f2 #X #H #f1 #Hf2 + elim (coafter_inv_nxx … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H2 destruct + elim (lexs_inv_push1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct + elim (IH … HL12 … Hg2) -g2 + /3 width=3 by isuni_inv_next, drops_drop, ex2_intro/ +| #f #I #L1 #K1 #V1 #W1 #HLK #HWV #IH #Hf #f2 #X #H #f1 #Hf2 + lapply (isuni_inv_push … Hf ??) -Hf [3: |*: // ] #Hf + lapply (drops_fwd_isid … HLK … Hf) -HLK #H0 destruct + lapply (lifts_fwd_isid … HWV … Hf) -HWV #H0 destruct + elim (coafter_inv_pxx … Hf2) -Hf2 [1,3:* |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct + [ elim (lexs_inv_push1 … H) | elim (lexs_inv_next1 … H) ] -H #L2 #V2 #HL12 #HV12 #H destruct + elim (IH … HL12 … Hg2) -g2 -IH /2 width=1 by isuni_isid/ #K2 #HK12 #HLK2 + lapply (drops_fwd_isid … HLK2 … Hf) -HLK2 #H0 destruct + /4 width=3 by drops_refl, lexs_next, lexs_push, isid_push, ex2_intro/ ] qed-. (* Basic_2A1: includes: lpx_sn_liftable_dedropable *) -lemma lexs_liftable_dedropable: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) → - d_liftable2 RN → d_liftable2 RP → dedropable_sn (lexs RN RP). +lemma lexs_liftable_co_dedropable: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) → + d_liftable2 RN → d_liftable2 RP → co_dedropable_sn (lexs RN RP). #RN #RP #H1RN #H1RP #H2RN #H2RP #b #f #L1 #K1 #H elim H -f -L1 -K1 [ #f #Hf #X #f1 #H #f2 #Hf2 >(lexs_inv_atom1 … H) -X /4 width=4 by drops_atom, lexs_atom, ex3_intro/ @@ -56,9 +59,9 @@ lemma lexs_liftable_dedropable: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. ] qed-. -fact lexs_dropable_aux: ∀RN,RP,b,f,L2,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ → - ∀f2,L1. L1 ⦻*[RN, RP, f2] L2 → ∀f1. f ~⊚ f1 ≡ f2 → - ∃∃K1. ⬇*[b, f] L1 ≡ K1 & K1 ⦻*[RN, RP, f1] K2. +fact lexs_dropable_dx_aux: ∀RN,RP,b,f,L2,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ → + ∀f2,L1. L1 ⦻*[RN, RP, f2] L2 → ∀f1. f ~⊚ f1 ≡ f2 → + ∃∃K1. ⬇*[b, f] L1 ≡ K1 & K1 ⦻*[RN, RP, f1] K2. #RN #RP #b #f #L2 #K2 #H elim H -f -L2 -K2 [ #f #Hf #_ #f2 #X #H #f1 #Hf2 lapply (lexs_inv_atom2 … H) -H #H destruct /4 width=3 by lexs_atom, drops_atom, ex2_intro/ @@ -79,28 +82,28 @@ fact lexs_dropable_aux: ∀RN,RP,b,f,L2,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ qed-. (* Basic_2A1: includes: lpx_sn_dropable *) -lemma lexs_dropable: ∀RN,RP. dropable_dx (lexs RN RP). -/2 width=5 by lexs_dropable_aux/ qed-. +lemma lexs_co_dropable_dx: ∀RN,RP. co_dropable_dx (lexs RN RP). +/2 width=5 by lexs_dropable_dx_aux/ qed-. -(* Basic_2A1: includes: lpx_sn_drop_conf *) -lemma lexs_drops_conf_next: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_sn RP → +(* Basic_2A1: includes: lpx_sn_drop_conf *) (**) +lemma lexs_drops_conf_next: ∀RN,RP. ∀f2,L1,L2. L1 ⦻*[RN, RP, f2] L2 → - ∀b,f,I,K1,V1. ⬇*[b,f] L1 ≡ K1.ⓑ{I}V1 → + ∀b,f,I,K1,V1. ⬇*[b,f] L1 ≡ K1.ⓑ{I}V1 → 𝐔⦃f⦄ → ∀f1. f ~⊚ ⫯f1 ≡ f2 → ∃∃K2,V2. ⬇*[b,f] L2 ≡ K2.ⓑ{I}V2 & K1 ⦻*[RN, RP, f1] K2 & RN K1 V1 V2. -#RN #RP #HRN #HRP #f2 #L1 #L2 #HL12 #b #f #I #K1 #V1 #HLK1 #f1 #Hf2 -elim (lexs_deliftable_dropable … HRN HRP … HLK1 … HL12 … Hf2) -L1 -f2 -HRN -HRP +#RN #RP #f2 #L1 #L2 #HL12 #b #f #I #K1 #V1 #HLK1 #Hf #f1 #Hf2 +elim (lexs_co_dropable_sn … HLK1 … Hf … HL12 … Hf2) -L1 -f2 -Hf #X #HX #HLK2 elim (lexs_inv_next1 … HX) -HX #K2 #V2 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/ qed-. -lemma lexs_drops_conf_push: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_sn RP → +lemma lexs_drops_conf_push: ∀RN,RP. ∀f2,L1,L2. L1 ⦻*[RN, RP, f2] L2 → - ∀b,f,I,K1,V1. ⬇*[b,f] L1 ≡ K1.ⓑ{I}V1 → + ∀b,f,I,K1,V1. ⬇*[b,f] L1 ≡ K1.ⓑ{I}V1 → 𝐔⦃f⦄ → ∀f1. f ~⊚ ↑f1 ≡ f2 → ∃∃K2,V2. ⬇*[b,f] L2 ≡ K2.ⓑ{I}V2 & K1 ⦻*[RN, RP, f1] K2 & RP K1 V1 V2. -#RN #RP #HRN #HRP #f2 #L1 #L2 #HL12 #b #f #I #K1 #V1 #HLK1 #f1 #Hf2 -elim (lexs_deliftable_dropable … HRN HRP … HLK1 … HL12 … Hf2) -L1 -f2 -HRN -HRP +#RN #RP #f2 #L1 #L2 #HL12 #b #f #I #K1 #V1 #HLK1 #Hf #f1 #Hf2 +elim (lexs_co_dropable_sn … HLK1 … Hf … HL12 … Hf2) -L1 -f2 -Hf #X #HX #HLK2 elim (lexs_inv_push1 … HX) -HX #K2 #V2 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/ qed-. @@ -111,7 +114,7 @@ lemma lexs_drops_trans_next: ∀RN,RP,f2,L1,L2. L1 ⦻*[RN, RP, f2] L2 → ∀f1. f ~⊚ ⫯f1 ≡ f2 → ∃∃K1,V1. ⬇*[b,f] L1 ≡ K1.ⓑ{I}V1 & K1 ⦻*[RN, RP, f1] K2 & RN K1 V1 V2. #RN #RP #f2 #L1 #L2 #HL12 #b #f #I #K1 #V1 #HLK1 #Hf #f1 #Hf2 -elim (lexs_dropable … HL12 … HLK1 … Hf … Hf2) -L2 -f2 -Hf +elim (lexs_co_dropable_dx … HL12 … HLK1 … Hf … Hf2) -L2 -f2 -Hf #X #HLK1 #HX elim (lexs_inv_next2 … HX) -HX #K1 #V1 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/ qed-. @@ -121,7 +124,7 @@ lemma lexs_drops_trans_push: ∀RN,RP,f2,L1,L2. L1 ⦻*[RN, RP, f2] L2 → ∀f1. f ~⊚ ↑f1 ≡ f2 → ∃∃K1,V1. ⬇*[b,f] L1 ≡ K1.ⓑ{I}V1 & K1 ⦻*[RN, RP, f1] K2 & RP K1 V1 V2. #RN #RP #f2 #L1 #L2 #HL12 #b #f #I #K1 #V1 #HLK1 #Hf #f1 #Hf2 -elim (lexs_dropable … HL12 … HLK1 … Hf … Hf2) -L2 -f2 -Hf +elim (lexs_co_dropable_dx … HL12 … HLK1 … Hf … Hf2) -L2 -f2 -Hf #X #HLK1 #HX elim (lexs_inv_push2 … HX) -HX #K1 #V1 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/ qed-. @@ -133,7 +136,7 @@ lemma drops_lexs_trans_next: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. ref ∀f2. f ~⊚ f1 ≡ ⫯f2 → ∃∃L2,V2. ⬇*[b,f] L2.ⓑ{I}V2 ≡ K2 & L1 ⦻*[RN, RP, f2] L2 & RN L1 V1 V2 & L1.ⓑ{I}V1≡[f]L2.ⓑ{I}V2. #RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I #L1 #V1 #HLK1 #f2 #Hf2 -elim (lexs_liftable_dedropable … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP +elim (lexs_liftable_co_dedropable … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP #X #HX #HLK2 #H1L12 elim (lexs_inv_next1 … HX) -HX #L2 #V2 #H2L12 #HV12 #H destruct /2 width=6 by ex4_2_intro/ qed-. @@ -145,7 +148,7 @@ lemma drops_lexs_trans_push: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. ref ∀f2. f ~⊚ f1 ≡ ↑f2 → ∃∃L2,V2. ⬇*[b,f] L2.ⓑ{I}V2 ≡ K2 & L1 ⦻*[RN, RP, f2] L2 & RP L1 V1 V2 & L1.ⓑ{I}V1≡[f]L2.ⓑ{I}V2. #RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I #L1 #V1 #HLK1 #f2 #Hf2 -elim (lexs_liftable_dedropable … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP +elim (lexs_liftable_co_dedropable … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP #X #HX #HLK2 #H1L12 elim (lexs_inv_push1 … HX) -HX #L2 #V2 #H2L12 #HV12 #H destruct /2 width=6 by ex4_2_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma index 485200949..c6899fd3e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma @@ -19,13 +19,16 @@ include "basic_2/relocation/drops_lexs.ma". (* Properties with ranged equivalence for local environments ****************) -lemma lreq_dedropable: dedropable_sn lreq. -@lexs_liftable_dedropable +lemma lreq_co_dedropable: co_dedropable_sn lreq. +@lexs_liftable_co_dedropable /2 width=6 by cfull_lift, ceq_lift, cfull_refl, ceq_refl/ qed-. -lemma lreq_dropable: ∀RN,RP. dropable_dx (lexs RN RP). -@lexs_dropable qed-. +lemma lreq_co_dropable_sn: co_dropable_sn lreq. +@lexs_co_dropable_sn qed-. + +lemma lreq_co_dropable_dx: co_dropable_dx lreq. +@lexs_co_dropable_dx qed-. (* Basic_2A1: includes: lreq_drop_trans_be *) lemma lreq_drops_trans_next: ∀f2,L1,L2. L1 ≡[f2] L2 → @@ -50,7 +53,7 @@ qed-. lemma drops_lreq_trans_next: ∀f1,K1,K2. K1 ≡[f1] K2 → ∀b,f,I,L1,V. ⬇*[b,f] L1.ⓑ{I}V ≡ K1 → ∀f2. f ~⊚ f1 ≡ ⫯f2 → - ∃∃L2. ⬇*[b,f] L2.ⓑ{I}V ≡ K2 & L1 ≡[f2] L2 & L1.ⓑ{I}V≡[f]L2.ⓑ{I}V. + ∃∃L2. ⬇*[b,f] L2.ⓑ{I}V ≡ K2 & L1 ≡[f2] L2 & L1.ⓑ{I}V ≡[f] L2.ⓑ{I}V. #f1 #K1 #K2 #HK12 #b #f #I #L1 #V #HLK1 #f2 #Hf2 elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -f1 -K1 /2 width=6 by cfull_lift, ceq_lift, cfull_refl, ceq_refl, ex3_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma index c377b6028..f4734a9b0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma @@ -42,9 +42,9 @@ lemma d2_deliftable_sn_LTC: ∀R. d_deliftable2_sn R → d_deliftable2_sn (LTC ] qed-. -lemma dropable_sn_TC: ∀R. dropable_sn R → dropable_sn (LTC … R). -#R #HR #b #f #L1 #K1 #HLK1 #f2 #L2 #H elim H -L2 -[ #L2 #HL12 #f1 #H elim (HR … HLK1 … HL12 … H) -HR -f2 -L1 +lemma co_dropable_sn_TC: ∀R. co_dropable_sn R → co_dropable_sn (LTC … R). +#R #HR #b #f #L1 #K1 #HLK1 #Hf #f2 #L2 #H elim H -L2 +[ #L2 #HL12 #f1 #H elim (HR … HLK1 … Hf … HL12 … H) -HR -Hf -f2 -L1 /3 width=3 by inj, ex2_intro/ | #L #L2 #_ #HL2 #IH #f1 #H elim (IH … H) -IH #K #HK1 #HLK elim (HR … HLK … HL2 … H) -HR -f2 -L @@ -73,7 +73,7 @@ lemma d2_deliftable_sn_llstar: ∀R. d_deliftable2_sn R → ] qed-. -lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (LTC … R). +lemma co_dropable_dx_TC: ∀R. co_dropable_dx R → co_dropable_dx (LTC … R). #R #HR #f2 #L1 #L2 #H elim H -L2 [ #L2 #HL12 #b #f #K2 #HLK2 #Hf #f1 #Hf2 elim (HR … HL12 … HLK2 … Hf … Hf2) -HR -Hf -f2 -L2 /3 width=3 by inj, ex2_intro/ @@ -83,7 +83,7 @@ lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (LTC … R). ] qed-. -lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (LTC … R). +lemma co_dedropable_sn_TC: ∀R. co_dedropable_sn R → co_dedropable_sn (LTC … R). #R #HR #b #f #L1 #K1 #HLK1 #f1 #K2 #H elim H -K2 [ #K2 #HK12 #f2 #Hf elim (HR … HLK1 … HK12 … Hf) -HR -f1 -K1 /3 width=4 by inj, ex3_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma index c7dde663e..966e4a17e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma @@ -46,15 +46,15 @@ lemma cpx_lref: ∀h,I,G,K,V,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T → qed. lemma cpx_bind: ∀h,p,I,G,L,V1,V2,T1,T2. - ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 → - ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[h] ⓑ{p,I}V2.T2. + ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 → + ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[h] ⓑ{p,I}V2.T2. #h #p #I #G #L #V1 #V2 #T1 #T2 * #cV #HV12 * /3 width=2 by cpg_bind, ex_intro/ qed. lemma cpx_flat: ∀h,I,G,L,V1,V2,T1,T2. - ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → - ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈[h] ⓕ{I}V2.T2. + ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → + ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈[h] ⓕ{I}V2.T2. #h #I #G #L #V1 #V2 #T1 #T2 * #cV #HV12 * /3 width=2 by cpg_flat, ex_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma index 258d0c81b..55c405162 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma @@ -12,19 +12,21 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lpx_sn_drop.ma". +include "basic_2/static/lfxs_drops.ma". include "basic_2/rt_transition/cpx_drops.ma". include "basic_2/rt_transition/lfpx.ma". (* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****) -(* Properties on local environment slicing ***********************************) +(* Properties with generic slicing for local environments *******************) -lemma lpx_drop_conf: ∀h,o,G. dropable_sn (lpx h o G). -/3 width=6 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-. +lemma drops_lfpx_trans: ∀h,G. dedropable_sn (cpx h G). +/3 width=6 by lfxs_liftable_dedropable, cpx_lifts/ qed-. -lemma drop_lpx_trans: ∀h,o,G. dedropable_sn (lpx h o G). -/3 width=10 by lpx_sn_liftable_dedropable, cpx_lift/ qed-. +(* Inversion lemmas with generic slicing for local environments *************) -lemma lpx_drop_trans_O1: ∀h,o,G. dropable_dx (lpx h o G). -/2 width=3 by lpx_sn_dropable/ qed-. +lemma lfpx_drops_conf: ∀h,G. dropable_sn (cpx h G). +/2 width=5 by lfxs_dropable_sn/ qed-. + +lemma lfpx_drops_trans: ∀h,G. dropable_dx (cpx h G). +/2 width=5 by lfxs_dropable_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt index 207e1e218..4e25194d8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt @@ -1,3 +1,3 @@ cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma cpx.ma cpx_simple.ma cpx_drops.ma cpx_lsubr.ma -lfpx.ma lfpx_length.ma lfpx_fqup.ma +lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma index 47b1eec39..441d3c51f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma @@ -12,8 +12,9 @@ (* *) (**************************************************************************) +include "ground_2/relocation/nstream_coafter.ma". include "basic_2/relocation/drops_drops.ma". -include "basic_2/static/frees.ma". +include "basic_2/static/frees_frees.ma". (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) @@ -142,6 +143,13 @@ lemma frees_lifts: ∀b,f1,K,T. K ⊢ 𝐅*⦃T⦄ ≡ f1 → ] qed-. +(* Forward lemmas with generic slicing for local environments ***************) + +lemma frees_fwd_coafter: ∀b,f2,L,U. L ⊢ 𝐅*⦃U⦄ ≡ f2 → + ∀f,K. ⬇*[b, f] L ≡ K → ∀T. ⬆*[f] T ≡ U → + ∀f1. K ⊢ 𝐅*⦃T⦄ ≡ f1 → f ~⊚ f1 ≡ f2. +/4 width=11 by frees_lifts, frees_mono, coafter_eq_repl_back0/ qed-. + (* Inversion lemmas with generic slicing for local environments *************) lemma frees_inv_lifts: ∀b,f2,L,U. L ⊢ 𝐅*⦃U⦄ ≡ f2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma new file mode 100644 index 000000000..0a64c396b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma @@ -0,0 +1,80 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/drops_ceq.ma". +include "basic_2/relocation/drops_lexs.ma". +include "basic_2/static/frees_fqup.ma". +include "basic_2/static/frees_drops.ma". +include "basic_2/static/lfxs.ma". + +(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) + +definition dedropable_sn: predicate (relation3 lenv term term) ≝ + λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → + ∀K2,T. K1 ⦻*[R, T] K2 → ∀U. ⬆*[f] T ≡ U → + ∃∃L2. L1 ⦻*[R, U] L2 & ⬇*[b, f] L2 ≡ K2 & L1 ≡[f] L2. + +definition dropable_sn: predicate (relation3 lenv term term) ≝ + λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → 𝐔⦃f⦄ → + ∀L2,U. L1 ⦻*[R, U] L2 → ∀T. ⬆*[f] T ≡ U → + ∃∃K2. K1 ⦻*[R, T] K2 & ⬇*[b, f] L2 ≡ K2. + +definition dropable_dx: predicate (relation3 lenv term term) ≝ + λR. ∀L1,L2,U. L1 ⦻*[R, U] L2 → + ∀b,f,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ → ∀T. ⬆*[f] T ≡ U → + ∃∃K1. ⬇*[b, f] L1 ≡ K1 & K1 ⦻*[R, T] K2. + +(* Properties with generic slicing for local environments *******************) + +(* Basic_2A1: includes: llpx_sn_lift_le llpx_sn_lift_ge *) +lemma lfxs_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) → + d_liftable2 R → dedropable_sn R. +#R #H1R #H2R #b #f #L1 #K1 #HLK1 #K2 #T * #f1 #Hf1 #HK12 #U #HTU +elim (frees_total L1 U) #f2 #Hf2 +lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #Hf +elim (lexs_liftable_co_dedropable … H1R … H2R … HLK1 … HK12 … Hf) -f1 -K1 +/3 width=6 by cfull_lift, ex3_intro, ex2_intro/ +qed-. + +(* Inversion lemmas with generic slicing for local environments *************) + +(* Basic_2A1: restricts: llpx_sn_inv_lift_le llpx_sn_inv_lift_be llpx_sn_inv_lift_ge *) +(* Basic_2A1: was: llpx_sn_drop_conf_O *) +lemma lfxs_dropable_sn: ∀R. dropable_sn R. +#R #b #f #L1 #K1 #HLK1 #H1f #L2 #U * #f2 #Hf2 #HL12 #T #HTU +elim (frees_total K1 T) #f1 #Hf1 +lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #H2f +elim (lexs_co_dropable_sn … HLK1 … HL12 … H2f) -f2 -L1 +/3 width=3 by ex2_intro/ +qed-. + +(* Basic_2A1: was: llpx_sn_drop_trans_O *) +(* Note: the proof might be simplified *) +lemma lfxs_dropable_dx: ∀R. dropable_dx R. +#R #L1 #L2 #U * #f2 #Hf2 #HL12 #b #f #K2 #HLK2 #H1f #T #HTU +elim (drops_isuni_ex … H1f L1) #K1 #HLK1 +elim (frees_total K1 T) #f1 #Hf1 +lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -K1 #H2f +elim (lexs_co_dropable_dx … HL12 … HLK2 … H2f) -L2 +/4 width=9 by frees_inv_lifts, ex2_intro/ +qed-. + +(* Basic_2A1: was: llpx_sn_inv_lift_O *) +lemma lfxs_inv_lift_bi: ∀R,L1,L2,U. L1 ⦻*[R, U] L2 → + ∀K1,K2,i. ⬇*[i] L1 ≡ K1 → ⬇*[i] L2 ≡ K2 → + ∀T. ⬆*[i] T ≡ U → K1 ⦻*[R, T] K2. +#R #L1 #L2 #U #HL12 #K1 #K2 #i #HLK1 #HLK2 #T #HTU +elim (lfxs_dropable_sn … HLK1 … HL12 … HTU) -L1 -U // #Y #HK12 #HY +lapply (drops_mono … HY … HLK2) -L2 -i #H destruct // +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 56c217b56..2aa5021d1 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 @@ -149,7 +149,7 @@ table { ] *) [ { "uncounted context-sensitive rt-transition" * } { - [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_fqup" * ] + [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" * ] [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_lsubr" * ] } ] @@ -186,7 +186,7 @@ table { } ] [ { "generic extension on referred entries" * } { - [ "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_fqup" + "lfxs_lfxs" * ] + [ "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ] } ] [ { "context-sensitive free variables" * } { diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma index e7ea1927d..cb5ede22b 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma @@ -611,7 +611,7 @@ elim (Hg1 0) #n #Hn qed-. fact coafter_isfin2_fwd_aux: (∀f1. @⦃0, f1⦄ ≡ 0 → H_coafter_isfin2_fwd f1) → - ∀i2,f1. @⦃0, f1⦄ ≡ i2 → H_coafter_isfin2_fwd f1. + ∀i2,f1. @⦃0, f1⦄ ≡ i2 → H_coafter_isfin2_fwd f1. #H0 #i2 elim i2 -i2 /2 width=1 by/ -H0 #i2 #IH #f1 #H1f1 #f2 #Hf2 #H2f1 #f #Hf elim (at_inv_pxn … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1 -- 2.39.2