X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Flveq_length.ma;h=3154290ebbb942856220b42cceaed88c4f21608e;hp=da13d1248779501fe85903b5e745e4957ab6b8bc;hb=156d974ad89aa04a086fdf9d332c8b04adf279fd;hpb=8fe4dc148d50a0352313633bea61441bc817afbf

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma
index da13d1248..3154290eb 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq_length.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground/arith/nat_le_minus_plus.ma".
 include "static_2/syntax/lenv_length.ma".
 include "static_2/syntax/lveq.ma".
 
@@ -19,7 +20,7 @@ include "static_2/syntax/lveq.ma".
 
 (* Properties with length for local environments ****************************)
 
-lemma lveq_length_eq: ∀L1,L2. |L1| = |L2| → L1 ≋ⓧ*[0,0] L2.
+lemma lveq_length_eq: ∀L1,L2. |L1| = |L2| → L1 ≋ⓧ*[𝟎,𝟎] L2.
 #L1 elim L1 -L1
 [ #Y2 #H >(length_inv_zero_sn … H) -Y2 /2 width=3 by lveq_atom, ex_intro/
 | #K1 #I1 #IH #Y2 #H
@@ -31,35 +32,40 @@ qed.
 (* Forward lemmas with length for local environments ************************)
 
 lemma lveq_fwd_length_le_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → n1 ≤ |L1|.
-#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
+#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
 /2 width=1 by nle_succ_bi/
 qed-.
 
 lemma lveq_fwd_length_le_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → n2 ≤ |L2|.
-#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
+#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
 /2 width=1 by nle_succ_bi/
 qed-.
 
 lemma lveq_fwd_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
                        ∧∧ |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 nminus_succ_sn, conj/
+#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
+[ /2 width=1 by conj/
+| #I1 #I2 #K1 #K2 #_ #IH >length_bind >length_bind //
+]
+#K1 #K2 #n #_ * #H1 #H2 destruct
+>length_bind <nminus_succ_dx <nminus_succ_sn
+/2 width=1 by nle_eq_zero_minus, conj/
 qed-.
 
-lemma lveq_length_fwd_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L1| ≤ |L2| → 0 = n1.
+lemma lveq_length_fwd_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L1| ≤ |L2| → 𝟎 = n1.
 #L1 #L2 #n1 #n2 #H #HL
 elim (lveq_fwd_length … H) -H
 >(nle_inv_eq_zero_minus … HL) //
 qed-.
 
-lemma lveq_length_fwd_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L2| ≤ |L1| → 0 = n2.
+lemma lveq_length_fwd_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L2| ≤ |L1| → 𝟎 = n2.
 #L1 #L2 #n1 #n2 #H #HL
 elim (lveq_fwd_length … H) -H
 >(nle_inv_eq_zero_minus … HL) //
 qed-.
 
 lemma lveq_inj_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
-                       |L1| = |L2| → ∧∧ 0 = n1 & 0 = n2.
+                       |L1| = |L2| → ∧∧ 𝟎 = n1 & 𝟎 = n2.
 #L1 #L2 #n1 #n2 #H #HL
 elim (lveq_fwd_length … H) -H
 >HL -HL /2 width=1 by conj/
@@ -67,11 +73,11 @@ 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 eq_inv_nplus_bi_sn/
+#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 //
+#k1 #K2 #n #_ #IH <nplus_succ_dx //
 qed-.
 
-lemma lveq_fwd_length_eq: ∀L1,L2. L1 ≋ⓧ*[0,0] L2 → |L1| = |L2|.
+lemma lveq_fwd_length_eq: ∀L1,L2. L1 ≋ⓧ*[𝟎,𝟎] L2 → |L1| = |L2|.
 /3 width=2 by lveq_fwd_length_plus, eq_inv_nplus_bi_dx/ qed-.
 
 lemma lveq_fwd_length_minus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
@@ -82,7 +88,8 @@ 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 //
+elim (lveq_fwd_length … HL) -HL >length_bind >length_bind
+<nminus_succ_bi <nminus_succ_bi //
 qed-.
 
 lemma lveq_fwd_bind_abst_length_le: ∀I1,I2,L1,L2,V2,n1,n2.
@@ -91,17 +98,19 @@ lemma lveq_fwd_bind_abst_length_le: ∀I1,I2,L1,L2,V2,n1,n2.
 
 (* Inversion lemmas with length for local environments **********************)
 
+(**) (* state with m2 ≝ ↓n2 *)
 lemma lveq_inv_void_dx_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2.ⓧ → |L1| ≤ |L2| →
-                               ∃∃m2. L1 ≋ ⓧ*[n1,m2] L2 & 0 = n1 & ↑m2 = n2.
+                               ∃∃m2. L1 ≋ ⓧ*[n1,m2] L2 & 𝟎 = n1 & ↑m2 = n2.
 #L1 #L2 #n1 #n2 #H #HL12
-lapply (lveq_fwd_length_plus … H) normalize >nplus_succ_dx #H0
+lapply (lveq_fwd_length_plus … H) >length_bind >nplus_succ_shift #H0
 lapply (nplus_2_des_le_sn_sn … H0 HL12) -H0 -HL12 #H0
-elim (nle_inv_succ_sn … H0) -H0 #m2 #_ #H0 destruct
+elim (nle_inv_succ_sn … H0) -H0 #_ #H0 >H0 in H; -H0 #H
 elim (lveq_inv_void_succ_dx … H) -H /2 width=3 by ex3_intro/
 qed-.
 
+(**) (* state with m1 ≝ ↓n1 *)
 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.
+                               ∃∃m1. L1 ≋ ⓧ*[m1,n2] L2 & ↑m1 = n1 & 𝟎 = n2.
 #L1 #L2 #n1 #n2 #H #HL
 lapply (lveq_sym … H) -H #H
 elim (lveq_inv_void_dx_length … H HL) -H -HL