X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsyntax%2Flveq_length.ma;h=eca38567c48c93075ad6a1e1992bd00c0d4794ed;hp=006f680205161ee537dec7cef751550e5e216ef0;hb=222044da28742b24584549ba86b1805a87def070;hpb=1c8e230b1d81491b38126900d76201fb84303ced

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_length.ma
index 006f68020..eca38567c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_length.ma
@@ -17,15 +17,16 @@ include "basic_2/syntax/lveq.ma".
 
 (* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
 
-lemma lveq_eq_ex: ∀L1,L2. |L1| = |L2| → ∃n. L1 ≋ⓧ*[n, n] L2.
+(* Properties with length for local environments ****************************)
+
+lemma lveq_length_eq: ∀L1,L2. |L1| = |L2| → L1 ≋ⓧ*[0, 0] L2.
 #L1 elim L1 -L1
 [ #Y2 #H >(length_inv_zero_sn … H) -Y2 /2 width=3 by lveq_atom, ex_intro/
-| #K1 * [ * | #I1 #V1 ] #IH #Y2 #H
-  elim (length_inv_succ_sn … H) -H * [1,3: * |*: #I2 #V2 ] #K2 #HK #H destruct 
-  elim (IH … HK) -IH -HK #n #HK
-  /4 width=3 by lveq_pair_sn, lveq_pair_dx, lveq_void_sn, lveq_void_dx, ex_intro/
+| #K1 #I1 #IH #Y2 #H
+  elim (length_inv_succ_sn … H) -H #I2 #K2 #HK #H destruct
+  /3 width=1 by lveq_bind/
 ]
-qed-.
+qed.
 
 (* Forward lemmas with length for local environments ************************)
 
@@ -40,33 +41,69 @@ lemma lveq_fwd_length_le_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → n2 ≤ |L
 qed-.
 
 lemma lveq_fwd_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
-                       |L1| + n2 = |L2| + n1.
+                       ∧∧ |L1|-|L2| = n1 & |L2|-|L1| = n2.
+#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 /2 width=1 by conj/
+#K1 #K2 #n #_ * #H1 #H2 >length_bind /3 width=1 by minus_Sn_m, conj/
+qed-.
+
+lemma lveq_length_fwd_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → |L1| ≤ |L2| → 0 = n1.
+#L1 #L2 #n1 #n2 #H #HL
+elim (lveq_fwd_length … H) -H
+>(eq_minus_O … HL) //
+qed-.
+
+lemma lveq_length_fwd_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → |L2| ≤ |L1| → 0 = n2.
+#L1 #L2 #n1 #n2 #H #HL
+elim (lveq_fwd_length … H) -H
+>(eq_minus_O … HL) //
+qed-.
+
+lemma lveq_inj_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
+                       |L1| = |L2| → ∧∧ 0 = n1 & 0 = n2.
+#L1 #L2 #n1 #n2 #H #HL
+elim (lveq_fwd_length … H) -H
+>HL -HL /2 width=1 by conj/ 
+qed-.
+
+lemma lveq_fwd_length_plus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
+                            |L1| + n2 = |L2| + n1.
 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
 /2 width=2 by injective_plus_r/
 qed-.
 
-lemma lveq_fwd_length_eq: ∀L1,L2,n. L1 ≋ⓧ*[n, n] L2 → |L1| = |L2|.
-/3 width=2 by lveq_fwd_length, injective_plus_l/ qed-.
+lemma lveq_fwd_length_eq: ∀L1,L2. L1 ≋ⓧ*[0, 0] L2 → |L1| = |L2|.
+/3 width=2 by lveq_fwd_length_plus, injective_plus_l/ qed-.
 
 lemma lveq_fwd_length_minus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
                              |L1| - n1 = |L2| - n2.
-/3 width=3 by lveq_fwd_length, lveq_fwd_length_le_dx, lveq_fwd_length_le_sn, plus_to_minus_2/ qed-.
+/3 width=3 by lveq_fwd_length_plus, lveq_fwd_length_le_dx, lveq_fwd_length_le_sn, plus_to_minus_2/ qed-.
 
-lemma lveq_inj_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
-                       |L1| = |L2| → n1 = n2.
-#L1 #L2 #n1 #n2 #H #HL12
-lapply (lveq_fwd_length … H) -H #H
-/2 width=2 by injective_plus_l/
+lemma lveq_fwd_abst_bind_length_le: ∀I1,I2,L1,L2,V1,n1,n2.
+                                    L1.ⓑ{I1}V1 ≋ⓧ*[n1, n2] L2.ⓘ{I2} → |L1| ≤ |L2|.
+#I1 #I2 #L1 #L2 #V1 #n1 #n2 #HL
+lapply (lveq_fwd_pair_sn … HL) #H destruct
+elim (lveq_fwd_length … HL) -HL >length_bind >length_bind //
 qed-.
-(*
+
+lemma lveq_fwd_bind_abst_length_le: ∀I1,I2,L1,L2,V2,n1,n2.
+                                    L1.ⓘ{I1} ≋ⓧ*[n1, n2] L2.ⓑ{I2}V2 → |L2| ≤ |L1|.
+/3 width=6 by lveq_fwd_abst_bind_length_le, lveq_sym/ qed-.
+
 (* Inversion lemmas with length for local environments **********************)
-                   
+
 lemma lveq_inv_void_dx_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2.ⓧ → |L1| ≤ |L2| →
-                               ∃∃m2. L1 ≋ ⓧ*[n1, m2] L2 & n2 = ⫯m2 & n1 ≤ m2.
+                               ∃∃m2. L1 ≋ ⓧ*[n1, m2] L2 & 0 = n1 & ↑m2 = n2.
 #L1 #L2 #n1 #n2 #H #HL12
-lapply (lveq_fwd_length … H) normalize >plus_n_Sm #H0
+lapply (lveq_fwd_length_plus … H) normalize >plus_n_Sm #H0
 lapply (plus2_inv_le_sn … H0 HL12) -H0 -HL12 #H0
-elim (le_inv_S1 … H0) -H0 #m2 #Hm2 #H0 destruct
-/3 width=4 by lveq_inv_void_dx, ex3_intro/
+elim (le_inv_S1 … H0) -H0 #m2 #_ #H0 destruct
+elim (lveq_inv_void_succ_dx … H) -H /2 width=3 by ex3_intro/
+qed-.
+
+lemma lveq_inv_void_sn_length: ∀L1,L2,n1,n2. L1.ⓧ ≋ⓧ*[n1, n2] L2 → |L2| ≤ |L1| →
+                               ∃∃m1. L1 ≋ ⓧ*[m1, n2] L2 & ↑m1 = n1 & 0 = n2.
+#L1 #L2 #n1 #n2 #H #HL
+lapply (lveq_sym … H) -H #H
+elim (lveq_inv_void_dx_length … H HL) -H -HL
+/3 width=4 by lveq_sym, ex3_intro/
 qed-.
-*)
\ No newline at end of file