matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_length.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "basic_2/syntax/lenv_length.ma".
  16 include "basic_2/syntax/lveq.ma".
  17
  18 (* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
  19
  20 lemma lveq_eq_ex: ∀L1,L2. |L1| = |L2| → ∃n. L1 ≋ⓧ*[n, n] L2.
  21 #L1 elim L1 -L1
  22 [ #Y2 #H >(length_inv_zero_sn … H) -Y2 /2 width=3 by lveq_atom, ex_intro/
  23 | #K1 * [ * | #I1 #V1 ] #IH #Y2 #H
  24   elim (length_inv_succ_sn … H) -H * [1,3: * |*: #I2 #V2 ] #K2 #HK #H destruct
  25   elim (IH … HK) -IH -HK #n #HK
  26   /4 width=3 by lveq_pair_sn, lveq_pair_dx, lveq_void_sn, lveq_void_dx, ex_intro/
  27 ]
  28 qed-.
  29
  30 (* Forward lemmas with length for local environments ************************)
  31
  32 lemma lveq_fwd_length_le_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → n1 ≤ |L1|.
  33 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
  34 /2 width=1 by le_S_S/
  35 qed-.
  36
  37 lemma lveq_fwd_length_le_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → n2 ≤ |L2|.
  38 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
  39 /2 width=1 by le_S_S/
  40 qed-.
  41
  42 lemma lveq_fwd_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
  43                        |L1| + n2 = |L2| + n1.
  44 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
  45 /2 width=2 by injective_plus_r/
  46 qed-.
  47
  48 lemma lveq_fwd_length_eq: ∀L1,L2,n. L1 ≋ⓧ*[n, n] L2 → |L1| = |L2|.
  49 /3 width=2 by lveq_fwd_length, injective_plus_l/ qed-.
  50
  51 lemma lveq_fwd_length_minus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
  52                              |L1| - n1 = |L2| - n2.
  53 /3 width=3 by lveq_fwd_length, lveq_fwd_length_le_dx, lveq_fwd_length_le_sn, plus_to_minus_2/ qed-.
  54
  55 lemma lveq_inj_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
  56                        |L1| = |L2| → n1 = n2.
  57 #L1 #L2 #n1 #n2 #H #HL12
  58 lapply (lveq_fwd_length … H) -H #H
  59 /2 width=2 by injective_plus_l/
  60 qed-.
  61
  62 lemma lveq_fwd_abst_bind_length_le: ∀I1,I2,L1,L2,V1,n1,n2.
  63                                     L1.ⓑ{I1}V1 ≋ⓧ*[n1, n2] L2.ⓘ{I2} → |L1| ≤ |L2|.
  64 #I1 #I2 #L1 #L2 #V1 #n1 #n2 #HL
  65 lapply (lveq_fwd_pair_sn … HL) #H destruct
  66 lapply (lveq_fwd_length … HL) -HL >length_bind >length_bind #H
  67 /2 width=1 by monotonic_pred/
  68 qed-.
  69
  70 lemma lveq_fwd_bind_abst_length_le: ∀I1,I2,L1,L2,V2,n1,n2.
  71                                     L1.ⓘ{I1} ≋ⓧ*[n1, n2] L2.ⓑ{I2}V2 → |L2| ≤ |L1|.
  72 /3 width=6 by lveq_fwd_abst_bind_length_le, lveq_sym/ qed-.
  73
  74 (* Inversion lemmas with length for local environments **********************)
  75
  76 lemma lveq_inv_void_dx_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2.ⓧ → |L1| ≤ |L2| →
  77                                ∃∃m2. L1 ≋ ⓧ*[n1, m2] L2 & n2 = ⫯m2 & n1 ≤ m2.
  78 #L1 #L2 #n1 #n2 #H #HL12
  79 lapply (lveq_fwd_length … H) normalize >plus_n_Sm #H0
  80 lapply (plus2_inv_le_sn … H0 HL12) -H0 -HL12 #H0
  81 elim (le_inv_S1 … H0) -H0 #m2 #Hm2 #H0 destruct
  82 /3 width=4 by lveq_inv_void_succ_dx, ex3_intro/
  83 qed-.
  84
  85 lemma lveq_inv_void_sn_length: ∀L1,L2,n1,n2. L1.ⓧ ≋ⓧ*[n1, n2] L2 → |L2| ≤ |L1| →
  86                                ∃∃m1. L1 ≋ ⓧ*[m1, n2] L2 & n1 = ⫯m1 & n2 ≤ m1.
  87 #L1 #L2 #n1 #n2 #H #HL
  88 lapply (lveq_sym … H) -H #H
  89 elim (lveq_inv_void_dx_length … H HL) -H -HL
  90 /3 width=4 by lveq_sym, ex3_intro/
  91 qed-.