matita/matita/contribs/lambdadelta/static_2/syntax/lveq_lveq.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 "static_2/syntax/lveq_length.ma".
  16
  17 (* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
  18
  19 (* Main inversion lemmas ****************************************************)
  20
  21 theorem lveq_inv_bind: ∀K1,K2. K1 ≋ⓧ*[𝟎,𝟎] K2 →
  22                        ∀I1,I2,m1,m2. K1.ⓘ[I1] ≋ⓧ*[m1,m2] K2.ⓘ[I2] →
  23                        ∧∧ 𝟎 = m1 & 𝟎 = m2.
  24 #K1 #K2 #HK #I1 #I2 #m1 #m2 #H
  25 lapply (lveq_fwd_length_eq … HK) -HK #HK
  26 elim (lveq_inj_length … H) -H /3 width=1 by conj/
  27 qed-.
  28
  29 theorem lveq_inj: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
  30                   ∀m1,m2. L1 ≋ⓧ*[m1,m2] L2 →
  31                   ∧∧ n1 = m1 & n2 = m2.
  32 #L1 #L2 #n1 #n2 #Hn #m1 #m2 #Hm
  33 elim (lveq_fwd_length … Hn) -Hn #H1 #H2 destruct
  34 elim (lveq_fwd_length … Hm) -Hm #H1 #H2 destruct
  35 /2 width=1 by conj/
  36 qed-.
  37
  38 theorem lveq_inj_void_sn_ge: ∀K1,K2. |K2| ≤ |K1| →
  39                              ∀n1,n2. K1 ≋ⓧ*[n1,n2] K2 →
  40                              ∀m1,m2. K1.ⓧ ≋ⓧ*[m1,m2] K2 →
  41                              ∧∧ ↑n1 = m1 & 𝟎 = m2 & 𝟎 = n2.
  42 #L1 #L2 #HL #n1 #n2 #Hn #m1 #m2 #Hm
  43 elim (lveq_fwd_length … Hn) -Hn #H1 #H2 destruct
  44 elim (lveq_fwd_length … Hm) -Hm #H1 #H2 destruct
  45 >length_bind <nminus_succ_dx
  46 <(nminus_succ_sn … HL) <(nle_inv_eq_zero_minus … HL)
  47 /2 width=1 by and3_intro/
  48 qed-.
  49
  50 theorem lveq_inj_void_dx_le: ∀K1,K2. |K1| ≤ |K2| →
  51                              ∀n1,n2. K1 ≋ⓧ*[n1,n2] K2 →
  52                              ∀m1,m2. K1 ≋ⓧ*[m1,m2] K2.ⓧ →
  53                              ∧∧ ↑n2 = m2 & 𝟎 = m1 & 𝟎 = n1.
  54 /3 width=5 by lveq_inj_void_sn_ge, lveq_sym/ qed-. (* auto: 2x lveq_sym *)