matita/matita/contribs/lambdadelta/static_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 "ground/arith/nat_le_minus_plus.ma".
  16 include "static_2/syntax/lenv_length.ma".
  17 include "static_2/syntax/lveq.ma".
  18
  19 (* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
  20
  21 (* Properties with length for local environments ****************************)
  22
  23 lemma lveq_length_eq: ∀L1,L2. |L1| = |L2| → L1 ≋ⓧ*[𝟎,𝟎] L2.
  24 #L1 elim L1 -L1
  25 [ #Y2 #H >(length_inv_zero_sn … H) -Y2 /2 width=3 by lveq_atom, ex_intro/
  26 | #K1 #I1 #IH #Y2 #H
  27   elim (length_inv_succ_sn … H) -H #I2 #K2 #HK #H destruct
  28   /3 width=1 by lveq_bind/
  29 ]
  30 qed.
  31
  32 (* Forward lemmas with length for local environments ************************)
  33
  34 lemma lveq_fwd_length_le_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → n1 ≤ |L1|.
  35 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
  36 /2 width=1 by nle_succ_bi/
  37 qed-.
  38
  39 lemma lveq_fwd_length_le_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → n2 ≤ |L2|.
  40 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
  41 /2 width=1 by nle_succ_bi/
  42 qed-.
  43
  44 lemma lveq_fwd_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
  45                        ∧∧ |L1|-|L2| = n1 & |L2|-|L1| = n2.
  46 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
  47 [ /2 width=1 by conj/
  48 | #I1 #I2 #K1 #K2 #_ #IH >length_bind >length_bind //
  49 ]
  50 #K1 #K2 #n #_ * #H1 #H2 destruct
  51 >length_bind <nminus_succ_dx <nminus_succ_sn
  52 /2 width=1 by nle_eq_zero_minus, conj/
  53 qed-.
  54
  55 lemma lveq_length_fwd_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L1| ≤ |L2| → 𝟎 = n1.
  56 #L1 #L2 #n1 #n2 #H #HL
  57 elim (lveq_fwd_length … H) -H
  58 >(nle_inv_eq_zero_minus … HL) //
  59 qed-.
  60
  61 lemma lveq_length_fwd_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L2| ≤ |L1| → 𝟎 = n2.
  62 #L1 #L2 #n1 #n2 #H #HL
  63 elim (lveq_fwd_length … H) -H
  64 >(nle_inv_eq_zero_minus … HL) //
  65 qed-.
  66
  67 lemma lveq_inj_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
  68                        |L1| = |L2| → ∧∧ 𝟎 = n1 & 𝟎 = n2.
  69 #L1 #L2 #n1 #n2 #H #HL
  70 elim (lveq_fwd_length … H) -H
  71 >HL -HL /2 width=1 by conj/
  72 qed-.
  73
  74 lemma lveq_fwd_length_plus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
  75                             |L1| + n2 = |L2| + n1.
  76 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 //
  77 #k1 #K2 #n #_ #IH <nplus_succ_dx //
  78 qed-.
  79
  80 lemma lveq_fwd_length_eq: ∀L1,L2. L1 ≋ⓧ*[𝟎,𝟎] L2 → |L1| = |L2|.
  81 /3 width=2 by lveq_fwd_length_plus, eq_inv_nplus_bi_dx/ qed-.
  82
  83 lemma lveq_fwd_length_minus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
  84                              |L1| - n1 = |L2| - n2.
  85 /3 width=3 by lveq_fwd_length_plus, lveq_fwd_length_le_dx, lveq_fwd_length_le_sn, nminus_plus_swap/ qed-.
  86
  87 lemma lveq_fwd_abst_bind_length_le: ∀I1,I2,L1,L2,V1,n1,n2.
  88                                     L1.ⓑ[I1]V1 ≋ⓧ*[n1,n2] L2.ⓘ[I2] → |L1| ≤ |L2|.
  89 #I1 #I2 #L1 #L2 #V1 #n1 #n2 #HL
  90 lapply (lveq_fwd_pair_sn … HL) #H destruct
  91 elim (lveq_fwd_length … HL) -HL >length_bind >length_bind
  92 <nminus_succ_bi <nminus_succ_bi //
  93 qed-.
  94
  95 lemma lveq_fwd_bind_abst_length_le: ∀I1,I2,L1,L2,V2,n1,n2.
  96                                     L1.ⓘ[I1] ≋ⓧ*[n1,n2] L2.ⓑ[I2]V2 → |L2| ≤ |L1|.
  97 /3 width=6 by lveq_fwd_abst_bind_length_le, lveq_sym/ qed-.
  98
  99 (* Inversion lemmas with length for local environments **********************)
 100
 101 (**) (* state with m2 ≝ ↓n2 *)
 102 lemma lveq_inv_void_dx_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2.ⓧ → |L1| ≤ |L2| →
 103                                ∃∃m2. L1 ≋ ⓧ*[n1,m2] L2 & 𝟎 = n1 & ↑m2 = n2.
 104 #L1 #L2 #n1 #n2 #H #HL12
 105 lapply (lveq_fwd_length_plus … H) >length_bind >nplus_succ_shift #H0
 106 lapply (nplus_2_des_le_sn_sn … H0 HL12) -H0 -HL12 #H0
 107 elim (nle_inv_succ_sn … H0) -H0 #_ #H0 >H0 in H; -H0 #H
 108 elim (lveq_inv_void_succ_dx … H) -H /2 width=3 by ex3_intro/
 109 qed-.
 110
 111 (**) (* state with m1 ≝ ↓n1 *)
 112 lemma lveq_inv_void_sn_length: ∀L1,L2,n1,n2. L1.ⓧ ≋ⓧ*[n1,n2] L2 → |L2| ≤ |L1| →
 113                                ∃∃m1. L1 ≋ ⓧ*[m1,n2] L2 & ↑m1 = n1 & 𝟎 = n2.
 114 #L1 #L2 #n1 #n2 #H #HL
 115 lapply (lveq_sym … H) -H #H
 116 elim (lveq_inv_void_dx_length … H HL) -H -HL
 117 /3 width=4 by lveq_sym, ex3_intro/
 118 qed-.