X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Fltpss_sn_ldrop.ma;h=70167dfddeb4888a08bfaaccdce0547940620f0c;hb=520d4370a540a98f5e5e1d85acfef0c982cc1e04;hp=d92978dafceeaef32b052f55aaba8f527b7f73fe;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma
index d92978daf..70167dfdd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_sn_ldrop.ma
@@ -12,10 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/substitution/fsup.ma".
+include "basic_2/unfold/tpss_lift.ma".
 include "basic_2/unfold/ltpss_sn.ma".
 
 (* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
 
+(* Properies on local environment slicing ***********************************)
+
 lemma ltpss_sn_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
                               ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
                               d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
@@ -129,3 +133,99 @@ lemma ltpss_sn_ldrop_trans_le: ∀L1,L0,d1,e1. L1 ⊢ ▶* [d1, e1] L0 →
   ]
 ]
 qed.
+
+lemma ldrop_ltpss_sn_trans_le: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
+                               ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 → d1 ≤ d2 →
+                               ∃∃L2. L1 ⊢ ▶* [d2 + e1, e2] L2 & ⇩[d1, e1] L2 ≡ K2.
+#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
+[ #d1 #e1 #K2 #d2 #e2 #H #_
+  >(ltpss_sn_inv_atom1 … H) -H /2 width=3/
+| /2 width=3/
+| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #Hd
+  elim (IHLK1 … HK12 Hd) -K1 -Hd /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd12
+  elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hd2
+  elim (ltpss_sn_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
+  elim (IHLK1 … HK12 … Hd12) -IHLK1 -HK12 <le_plus_minus_comm // #L2 #HL12 #HLK2
+  elim (lift_total W2 d1 e1) #V2 #HWV2
+  lapply (tpss_lift_ge … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 // -Hd12
+  <le_plus_minus_comm // /4 width=5/
+]
+qed-.
+
+lemma ldrop_ltpss_sn_trans_be: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
+                               ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 →
+                               d2 ≤ d1 → d1 ≤ d2 + e2 →
+                               ∃∃L2. L1 ⊢ ▶* [d2, e1 + e2] L2 &
+                                     ⇩[d1, e1] L2 ≡ K2.
+#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
+[ #d1 #e1 #K2 #d2 #e2 #H #_ #_
+  >(ltpss_sn_inv_atom1 … H) -H /2 width=3/
+| #K1 #I #V1 #K2 #d2 #e2 #HK12 #H #_
+  lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3/
+| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H1 #H2
+  elim (IHLK1 … HK12 H1 H2) -K1 -H2
+  lapply (le_n_O_to_eq … H1) -H1 #H destruct /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21 #Hd12
+  elim (eq_or_gt d2) #Hd2 [ -Hd21 elim (eq_or_gt e2) #He2 ] destruct
+  [ lapply (le_n_O_to_eq … Hd12) -Hd12 <plus_n_Sm #H destruct
+  | elim (ltpss_sn_inv_tpss21 … H He2) -H #K2 #W2 #HK12 #HW12 #H destruct
+    elim (IHLK1 … HK12 …) -IHLK1 // /2 width=1/ >plus_minus_commutative // #L2 #HL12 #HLK2
+    elim (lift_total W2 d1 e1) #V2 #HWV2
+    lapply (tpss_lift_be … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 // /2 width=1/
+    >plus_minus // >commutative_plus /4 width=5/
+  | elim (ltpss_sn_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
+    elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // ] /2 width=1/ #L2 #HL12 #HLK2
+    elim (lift_total W2 d1 e1) #V2 #HWV2
+    lapply (tpss_lift_be … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 [ >plus_minus // ] /2 width=1/
+    >commutative_plus /3 width=5/
+  ]
+]
+qed-.
+
+lemma ldrop_ltpss_sn_trans_ge: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
+                               ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 → d2 + e2 ≤ d1 →
+                               ∃∃L2. L1 ⊢ ▶* [d2, e2] L2 & ⇩[d1, e1] L2 ≡ K2.
+#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
+[ #d1 #e1 #K2 #d2 #e2 #H #_
+  >(ltpss_sn_inv_atom1 … H) -H /2 width=3/
+| #K1 #I #V1 #K2 #d2 #e2 #HK12 #H
+  elim (plus_le_0 … H) -H #H1 #H2 destruct /2 width=3/
+| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H
+  elim (IHLK1 … HK12 H) -K1
+  elim (plus_le_0 … H) -H #H1 #H2 destruct #L2 #HL12
+  >(ltpss_sn_inv_refl_O2 … HL12) -L1 /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21
+  elim (eq_or_gt d2) #Hd2 [ elim (eq_or_gt e2) #He2 ] destruct
+  [ -IHLK1 -Hd21 <(ltpss_sn_inv_refl_O2 … H) -X /3 width=5/
+  | elim (ltpss_sn_inv_tpss21 … H He2) -H #K2 #W2 #HK12 #HW12 #H destruct
+    elim (IHLK1 … HK12 …) -IHLK1 /2 width=1/ #L2 #HL12 #HLK2
+    elim (lift_total W2 d1 e1) #V2 #HWV2
+    lapply (tpss_lift_le … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 /2 width=1/ /3 width=5/
+  | elim (ltpss_sn_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
+    elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // /2 width=1/ ] #L2 #HL12 #HLK2
+    elim (lift_total W2 d1 e1) #V2 #HWV2
+    lapply (tpss_lift_le … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 [ >plus_minus // /2 width=1/ ] /3 width=5/
+  ]
+]
+qed-.
+
+(* Properties on supclosure *************************************************)
+
+lemma fsup_tpss_trans_full: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶*[0,|L2|] U2 →
+                            ∃∃L,U1. L1 ⊢ ▶*[0,|L1|] L & L ⊢ T1 ▶*[0,|L|] U1 & ⦃L, U1⦄ ⊃ ⦃L2, T2⦄.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ]
+#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
+elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2
+elim (lift_total T d e) #U #HTU
+lapply (ltpss_sn_fwd_length … HK1) #H >H in HK1; -H #HK1
+elim (le_or_ge d (|K|)) #Hd
+[ elim (ldrop_ltpss_sn_trans_be … HLK1 … HK1 … Hd) // -HLK1 -HK1 #L2 #HL12 #HL2K
+  lapply (tpss_lift_be … HT1 … Hd HL2K HTU1 … HTU) // -HT1 -HTU1 #HU1
+| elim (ldrop_ltpss_sn_trans_ge … HLK1 … HK1 Hd) -HLK1 -HK1 #L2 #HL12 #HL2K
+  lapply (tpss_lift_le … HT1 … Hd HL2K HTU1 … HTU) -HT1 -HTU1 #HU1
+]
+lapply (ltpss_sn_weak_full … HL12) -HL12 #HL12
+lapply (tpss_weak_full … HU1) -HU1 #HU1
+@(ex3_2_intro … L2 U) // /2 width=7/ (**) (* explicit constructor: auto /3 width=14/ too slow *)
+qed-.