matita/matita/contribs/lambdadelta/basic_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 "basic_2/syntax/lveq_length.ma".
  16
  17 (* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
  18
  19 (* Main forward lemmas ******************************************************)
  20
  21 theorem lveq_fwd_inj_succ_zero: ∀L1,L2,n1. L1 ≋ⓧ*[⫯n1, 0] L2 →
  22                                 ∀m1,m2. L1 ≋ⓧ*[m1, m2] L2 → ∃x1. ⫯x1 = m1.
  23 #L1 #L2 #n1 #Hn #m1 #m2 #Hm
  24 lapply (lveq_fwd_length … Hn) -Hn <plus_n_O #Hn
  25 lapply (lveq_fwd_length … Hm) -Hm >Hn >associative_plus -Hn #Hm
  26 lapply (injective_plus_r … Hm) -Hm
  27 <plus_S1 /2 width=2 by ex_intro/
  28 qed-.
  29
  30 theorem lveq_fwd_inj_zero_succ: ∀L1,L2,n2. L1 ≋ⓧ*[0, ⫯n2] L2 →
  31                                 ∀m1,m2. L1 ≋ⓧ*[m1, m2] L2 → ∃x2. ⫯x2 = m2.
  32 /4 width=6 by lveq_fwd_inj_succ_zero, lveq_sym/ qed-. (* auto: 2x lveq_sym *)
  33
  34 theorem lveq_fwd_inj_succ_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[⫯n1, n2] L2 →
  35                               ∀m1,m2. L1 ≋ⓧ*[m1, m2] L2 →
  36                               ∨∨ ∃x. ⫯x = n2 | ∃x. ⫯x = m1.
  37 #L1 #L2 #n1 * [2: #n2 ] /3 width=2 by ex_intro, or_introl/
  38 #Hn #m1 #m2 #Hm @or_intror @lveq_fwd_inj_succ_zero /width=6 by/ (**) (* auto fails *)
  39 qed-.
  40
  41 theorem lveq_fwd_inj_succ_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, ⫯n2] L2 →
  42                               ∀m1,m2. L1 ≋ⓧ*[m1, m2] L2 →
  43                               ∨∨ ∃x. ⫯x = n1 | ∃x. ⫯x = m2.
  44 /4 width=6 by lveq_fwd_inj_succ_sn, lveq_sym/ qed-. (* auto: 2x lveq_sym *)
  45
  46 (* Main inversion lemmas ****************************************************)
  47
  48 theorem lveq_inv_pair_sn: ∀K1,K2,n. K1 ≋ⓧ*[n, n] K2 →
  49                           ∀I1,I2,V,m1,m2. K1.ⓑ{I1}V ≋ⓧ*[m1, m2] K2.ⓘ{I2} →
  50                           ∧∧ 0 = m1 & 0 = m2.
  51 #K1 #K2 #n #HK #I1 #I2 #V #m1 #m2 #H
  52 lapply (lveq_fwd_length_eq … HK) -HK #HK
  53 lapply (lveq_fwd_pair_sn … H) #H0 destruct
  54 <(lveq_inj_length … H) -H normalize /3 width=1 by conj, eq_f/
  55 qed-.
  56
  57 theorem lveq_inv_pair_dx: ∀K1,K2,n. K1 ≋ⓧ*[n, n] K2 →
  58                           ∀I1,I2,V,m1,m2. K1.ⓘ{I1} ≋ⓧ*[m1, m2] K2.ⓑ{I2}V →
  59                           ∧∧ 0 = m1 & 0 = m2.
  60 /4 width=8 by lveq_inv_pair_sn, lveq_sym, commutative_and/ qed-.
  61
  62 theorem lveq_inj: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
  63                   ∀m1,m2. L1 ≋ⓧ*[m1, m2] L2 →
  64                   ∧∧ n1 = m1 & n2 = m2.
  65 #L1 #L2 @(f2_ind ?? length2 ?? L1 L2) -L1 -L2
  66 #x #IH * [2: #L1 #I1 ] * [2,4: #L2 #I2 ]
  67 [ cases I1 -I1 [ * | #I1 #V1 ] cases I2 -I2 [1,3: * |*: #I2 #V2 ] ]
  68 #Hx #n1 #n2 #Hn #m1 #m2 #Hm destruct
  69 [ elim (lveq_fwd_void_void … Hn) * #x #H destruct
  70   elim (lveq_fwd_void_void … Hm) * #y #H destruct
  71   [ lapply (lveq_inv_void_succ_sn … Hn) -Hn #Hn
  72     lapply (lveq_inv_void_succ_sn … Hm) -Hm #Hm
  73     elim (IH … Hn … Hm) -IH -Hn -Hm // #H1 #H2 destruct
  74     /2 width=1 by conj/
  75   | elim (lveq_fwd_inj_succ_sn … Hn … Hm) * #z #H destruct
  76     [ lapply (lveq_inv_void_succ_dx … Hn) -Hn #Hn
  77       lapply (lveq_inv_void_succ_dx … Hm) -Hm #Hm
  78       elim (IH … Hn … Hm) -IH -Hn -Hm [2: normalize // ] #H1 #H2 destruct (**) (* avoid normalize *)
  79       /2 width=1 by conj/
  80     | lapply (lveq_inv_void_succ_sn … Hn) -Hn #Hn
  81       lapply (lveq_inv_void_succ_sn … Hm) -Hm #Hm
  82       elim (IH … Hn … Hm) -IH -Hn -Hm // #H1 #H2 destruct
  83       /2 width=1 by conj/
  84     ]
  85   | elim (lveq_fwd_inj_succ_dx … Hn … Hm) * #z #H destruct
  86     [ lapply (lveq_inv_void_succ_sn … Hn) -Hn #Hn
  87       lapply (lveq_inv_void_succ_sn … Hm) -Hm #Hm
  88       elim (IH … Hn … Hm) -IH -Hn -Hm // #H1 #H2 destruct
  89       /2 width=1 by conj/
  90     | lapply (lveq_inv_void_succ_dx … Hn) -Hn #Hn
  91       lapply (lveq_inv_void_succ_dx … Hm) -Hm #Hm
  92       elim (IH … Hn … Hm) -IH -Hn -Hm [2: normalize // ] #H1 #H2 destruct (**) (* avoid normalize *)
  93       /2 width=1 by conj/
  94     ]
  95   | lapply (lveq_inv_void_succ_dx … Hn) -Hn #Hn
  96     lapply (lveq_inv_void_succ_dx … Hm) -Hm #Hm
  97     elim (IH … Hn … Hm) -IH -Hn -Hm [2: normalize // ] #H1 #H2 destruct (**) (* avoid normalize *)
  98     /2 width=1 by conj/
  99   ]
 100 | lapply (lveq_fwd_abst_bind_length_le … Hn) #HL
 101   elim (le_to_or_lt_eq … HL) -HL #HL
 102   [ elim (lveq_inv_void_dx_length … Hn) -Hn // #x1 #Hn #H #_ destruct
 103     elim (lveq_inv_void_dx_length … Hm) -Hm // #y1 #Hm #H #_ destruct
 104     elim (IH … Hn … Hm) -IH -Hn -Hm -HL [2: normalize // ] #H1 #H2 destruct (**) (* avoid normalize *)
 105     /2 width=1 by conj/
 106   | elim (lveq_eq_ex … HL) -HL #x #HL
 107     elim (lveq_inv_pair_sn … HL … Hn) -Hn #H1 #H2 destruct
 108     elim (lveq_inv_pair_sn … HL … Hm) -Hm #H1 #H2 destruct
 109     /2 width=1 by conj/
 110   ]
 111 | lapply (lveq_fwd_bind_abst_length_le … Hn) #HL
 112   elim (le_to_or_lt_eq … HL) -HL #HL
 113   [ elim (lveq_inv_void_sn_length … Hn) -Hn // #x1 #Hn #H #_ destruct
 114     elim (lveq_inv_void_sn_length … Hm) -Hm // #y1 #Hm #H #_ destruct
 115     elim (IH … Hn … Hm) -IH -Hn -Hm -HL // #H1 #H2 destruct
 116     /2 width=1 by conj/
 117   | lapply (sym_eq ??? HL) -HL #HL
 118     elim (lveq_eq_ex … HL) -HL #x #HL
 119     elim (lveq_inv_pair_dx … HL … Hn) -Hn #H1 #H2 destruct
 120     elim (lveq_inv_pair_dx … HL … Hm) -Hm #H1 #H2 destruct
 121     /2 width=1 by conj/
 122   ]
 123 | elim (lveq_inv_pair_pair… Hn) -Hn #x #_ #H1 #H2 destruct
 124   elim (lveq_inv_pair_pair… Hm) -Hm #y #_ #H1 #H2 destruct
 125   /2 width=1 by conj/
 126 | elim (lveq_inv_atom_bind … Hn) -Hn #x #Hn #H1 #H2 destruct
 127   elim (lveq_inv_atom_bind … Hm) -Hm #y #Hm #H1 #H2 destruct
 128   elim (IH … Hn … Hm) -IH -Hn -Hm /2 width=1 by conj/
 129 | elim (lveq_inv_bind_atom … Hn) -Hn #x #Hn #H1 #H2 destruct
 130   elim (lveq_inv_bind_atom … Hm) -Hm #y #Hm #H1 #H2 destruct
 131   elim (IH … Hn … Hm) -IH -Hn -Hm /2 width=1 by conj/
 132 | elim (lveq_inv_atom_atom … Hn) -Hn #H1 #H2 destruct
 133   elim (lveq_inv_atom_atom … Hm) -Hm #H1 #H2 destruct
 134   /2 width=1 by conj/
 135 ]
 136 qed-.
 137
 138 theorem lveq_inj_void_sn: ∀K1,K2,n1,n2. K1 ≋ⓧ*[n1, n2] K2 →
 139                           ∀m1,m2. K1.ⓧ ≋ⓧ*[m1, m2] K2 →
 140                           ∧∧ ⫯n1 = m1 & n2 = m2.
 141 /3 width=4 by lveq_inj, lveq_void_sn/ qed-.
 142
 143 theorem lveq_inj_void_dx: ∀K1,K2,n1,n2. K1 ≋ⓧ*[n1, n2] K2 →
 144                           ∀m1,m2. K1 ≋ⓧ*[m1, m2] K2.ⓧ →
 145                           ∧∧ n1 = m1 & ⫯n2 = m2.
 146 /3 width=4 by lveq_inj, lveq_void_dx/ qed-.