matita/matita/contribs/lambdadelta/basic_2/syntax/voids_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/voids.ma".
  17
  18 (* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
  19
  20 (* Forward lemmas with length for local environments ************************)
  21
  22 lemma voids_fwd_length_le_sn: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 → n1 ≤ |L1|.
  23 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
  24 /2 width=1 by le_S_S/
  25 qed-.
  26
  27 lemma voids_fwd_length_le_dx: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 → n2 ≤ |L2|.
  28 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
  29 /2 width=1 by le_S_S/
  30 qed-.
  31
  32 lemma voids_fwd_length: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 →
  33                         |L1| + n2 = |L2| + n1.
  34 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
  35 /2 width=2 by injective_plus_r/
  36 qed-.
  37
  38 lemma voids_fwd_length_minus: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 →
  39                               |L1| - n1 = |L2| - n2.
  40 /3 width=3 by voids_fwd_length, voids_fwd_length_le_dx, voids_fwd_length_le_sn, plus_to_minus_2/ qed-.
  41
  42 lemma voids_inj_length: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 →
  43                         |L1| = |L2| → n1 = n2.
  44 #L1 #L2 #n1 #n2 #H #HL12
  45 lapply (voids_fwd_length … H) -H #H
  46 /2 width=2 by injective_plus_l/
  47 qed-.
  48
  49 (* Inversion lemmas with length for local environments **********************)
  50
  51 lemma voids_inv_void_dx_length: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2.ⓧ → |L1| ≤ |L2| →
  52                                 ∃∃m2. ⓧ*[n1]L1 ≋ ⓧ*[m2]L2 & n2 = ⫯m2 & n1 ≤ m2.
  53 #L1 #L2 #n1 #n2 #H #HL12
  54 lapply (voids_fwd_length … H) normalize >plus_n_Sm #H0
  55 lapply (plus2_inv_le_sn … H0 HL12) -H0 -HL12 #H0
  56 elim (le_inv_S1 … H0) -H0 #m2 #Hm2 #H0 destruct
  57 /3 width=4 by voids_inv_void_dx, ex3_intro/
  58 qed-.