- some corrections and additions

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / lleq_lleq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
index 0694be69cc970278d774ac50c88c392e0a9bef36..2a8873d9b7b1675865c06d5d693a41e24232d456 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
@@ -20,8 +20,8 @@ include "basic_2/substitution/lleq_ldrop.ma".
 lemma lleq_fwd_lref: ∀L1,L2. ∀d:ynat. ∀i:nat. L1 ⋕[#i, d] L2 →
                      ∨∨ |L1| ≤ i ∧ |L2| ≤ i
                       | yinj i < d
-                      | ∃∃I1,I2,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V &
-                                         ⇩[0, i] L2 ≡ K2.ⓑ{I2}V &
+                      | ∃∃I1,I2,K1,K2,V. ⇩[i] L1 ≡ K1.ⓑ{I1}V &
+                                         ⇩[i] L2 ≡ K2.ⓑ{I2}V &
                                          K1 ⋕[V, yinj 0] K2 & d ≤ yinj i.
 #L1 #L2 #d #i * #HL12 #IH elim (lt_or_ge i (|L1|)) /3 width=3 by or3_intro0, conj/
 elim (ylt_split i d) /2 width=1 by or3_intro1/ #Hdi #Hi
@@ -46,9 +46,9 @@ lapply (cpys_antisym_eq … H12 … H21) -H12 -H21 #H destruct
 qed-.
 
 lemma lleq_fwd_lref_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 →
-                        ∀I2,K2,V. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V →
+                        ∀I2,K2,V. ⇩[i] L2 ≡ K2.ⓑ{I2}V →
                         i < d ∨
-                        ∃∃I1,K1. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V & K1 ⋕[V, 0] K2 & d ≤ i.
+                        ∃∃I1,K1. ⇩[i] L1 ≡ K1.ⓑ{I1}V & K1 ⋕[V, 0] K2 & d ≤ i.
 #L1 #L2 #d #i #H #I2 #K2 #V #HLK2 elim (lleq_fwd_lref … H) -H [ * || * ]
 [ #_ #H elim (lt_refl_false i)
   lapply (ldrop_fwd_length_lt2 … HLK2) -HLK2
@@ -60,9 +60,9 @@ lemma lleq_fwd_lref_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 →
 qed-.
 
 lemma lleq_fwd_lref_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 →
-                        ∀I1,K1,V. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V →
+                        ∀I1,K1,V. ⇩[i] L1 ≡ K1.ⓑ{I1}V →
                         i < d ∨
-                        ∃∃I2,K2. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V & K1 ⋕[V, 0] K2 & d ≤ i.
+                        ∃∃I2,K2. ⇩[i] L2 ≡ K2.ⓑ{I2}V & K1 ⋕[V, 0] K2 & d ≤ i.
 #L1 #L2 #d #i #HL12 #I1 #K1 #V #HLK1 elim (lleq_fwd_lref_dx L2 … d … HLK1) -HLK1
 [2: * ] /4 width=6 by lleq_sym, ex3_2_intro, or_introl, or_intror/
 qed-.
@@ -70,8 +70,8 @@ qed-.
 (* Advanced inversion lemmas ************************************************)
 
 lemma lleq_inv_lref_ge_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
-                           ∀I2,K2,V. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V →
-                           ∃∃I1,K1. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V & K1 ⋕[V, 0] K2.
+                           ∀I2,K2,V. ⇩[i] L2 ≡ K2.ⓑ{I2}V →
+                           ∃∃I1,K1. ⇩[i] L1 ≡ K1.ⓑ{I1}V & K1 ⋕[V, 0] K2.
 #L1 #L2 #d #i #H #Hdi #I2 #K2 #V #HLK2 elim (lleq_fwd_lref_dx … H … HLK2) -L2
 [ #H elim (ylt_yle_false … H Hdi)
 | * /2 width=4 by ex2_2_intro/
@@ -79,12 +79,28 @@ lemma lleq_inv_lref_ge_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
 qed-.
 
 lemma lleq_inv_lref_ge_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
-                           ∀I1,K1,V. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V →
-                           ∃∃I2,K2. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V & K1 ⋕[V, 0] K2.
+                           ∀I1,K1,V. ⇩[i] L1 ≡ K1.ⓑ{I1}V →
+                           ∃∃I2,K2. ⇩[i] L2 ≡ K2.ⓑ{I2}V & K1 ⋕[V, 0] K2.
 #L1 #L2 #d #i #HL12 #Hdi #I1 #K1 #V #HLK1 elim (lleq_inv_lref_ge_dx L2 … Hdi … HLK1) -Hdi -HLK1
 /3 width=4 by lleq_sym, ex2_2_intro/
 qed-.
 
+lemma lleq_inv_lref_ge_gen: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
+                            ∀I1,I2,K1,K2,V1,V2.
+                            ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+                            V1 = V2 ∧ K1 ⋕[V2, 0] K2.
+#L1 #L2 #d #i #HL12 #Hdi #I1 #I2 #K1 #K2 #V1 #V2 #HLK1 #HLK2
+elim (lleq_inv_lref_ge_sn … HL12 … HLK1) // -L1 -d
+#J #Y #HY lapply (ldrop_mono … HY … HLK2) -L2 -i #H destruct /2 width=1 by conj/
+qed-.
+
+lemma lleq_inv_lref_ge: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
+                        ∀I,K1,K2,V. ⇩[i] L1 ≡ K1.ⓑ{I}V → ⇩[i] L2 ≡ K2.ⓑ{I}V →
+                        K1 ⋕[V, 0] K2.
+#L1 #L2 #d #i #HL12 #Hdi #I #K1 #K2 #V #HLK1 #HLK2
+elim (lleq_inv_lref_ge_gen … HL12 … HLK1 HLK2) //
+qed-.
+
 (* Advanced properties ******************************************************)
 
 lemma lleq_dec: ∀T,L1,L2,d. Decidable (L1 ⋕[T, d] L2).
@@ -137,3 +153,23 @@ theorem lleq_canc_sn: ∀L,L1,L2,T,d. L ⋕[d, T] L1→ L ⋕[d, T] L2 → L1 
 
 theorem lleq_canc_dx: ∀L1,L2,L,T,d. L1 ⋕[d, T] L → L2 ⋕[d, T] L → L1 ⋕[d, T] L2.
 /3 width=3 by lleq_trans, lleq_sym/ qed-.
+
+(* Inversion lemmas on negated lazy quivalence for local environments *******)
+
+lemma nlleq_inv_bind: ∀a,I,L1,L2,V,T,d. (L1 ⋕[ⓑ{a,I}V.T, d] L2 → ⊥) →
+                      (L1 ⋕[V, d] L2 → ⊥) ∨ (L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V → ⊥).
+#a #I #L1 #L2 #V #T #d #H elim (lleq_dec V L1 L2 d)
+/4 width=1 by lleq_bind, or_intror, or_introl/
+qed-.
+
+lemma nlleq_inv_flat: ∀I,L1,L2,V,T,d. (L1 ⋕[ⓕ{I}V.T, d] L2 → ⊥) →
+                      (L1 ⋕[V, d] L2 → ⊥) ∨ (L1 ⋕[T, d] L2 → ⊥).
+#I #L1 #L2 #V #T #d #H elim (lleq_dec V L1 L2 d)
+/4 width=1 by lleq_flat, or_intror, or_introl/
+qed-.
+
+(* Note: lleq_nlleq_trans: ∀d,T,L1,L. L1⋕[T, d] L →
+                           ∀L2. (L ⋕[T, d] L2 → ⊥) → (L1 ⋕[T, d] L2 → ⊥).
+/3 width=3 by lleq_canc_sn/ qed-.
+works with /4 width=8/ so lleq_canc_sn is more convenient
+*)