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 inversion lemmas ****************************************************)
  20
  21 theorem lveq_inv_pair_sn: ∀K1,K2,n. K1 ≋ⓧ*[n, n] K2 →
  22                           ∀I1,I2,V,m1,m2. K1.ⓑ{I1}V ≋ⓧ*[m1, m2] K2.ⓘ{I2} →
  23                           ∧∧ 0 = m1 & 0 = m2.
  24 #K1 #K2 #n #HK #I1 #I2 #V #m1 #m2 #H
  25 lapply (lveq_fwd_length_eq … HK) -HK #HK
  26 lapply (lveq_fwd_pair_sn … H) #H0 destruct
  27 <(lveq_inj_length … H) -H normalize /3 width=1 by conj, eq_f/
  28 qed-.
  29
  30 theorem lveq_inv_pair_dx: ∀K1,K2,n. K1 ≋ⓧ*[n, n] K2 →
  31                           ∀I1,I2,V,m1,m2. K1.ⓘ{I1} ≋ⓧ*[m1, m2] K2.ⓑ{I2}V →
  32                           ∧∧ 0 = m1 & 0 = m2.
  33 /4 width=8 by lveq_inv_pair_sn, lveq_sym, commutative_and/ qed-.
  34 (*
  35 theorem lveq_inv_void_sn: ∀K1,K2,n1,n2. K1 ≋ⓧ*[n1, n2] K2 →
  36                           ∀m1,m2. K1.ⓧ ≋ⓧ*[m1, m2] K2 →
  37                           0 < m1.
  38 *)
  39 (*
  40 theorem lveq_inj: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
  41                   ∀m1,m2. L1 ≋ⓧ*[m1, m2] L2 →
  42                   ∧∧ n1 = m1 & n2 = m2.
  43 #L1 #L2 @(f2_ind ?? length2 ?? L1 L2) -L1 -L2
  44 #x #IH #L1 #L2 #Hx #n1 #n2 #H
  45 generalize in match Hx; -Hx
  46 cases H -L1 -L2 -n1 -n2
  47 /2 width=8 by lveq_inv_pair_dx, lveq_inv_pair_sn, lveq_inv_atom/
  48 #K1 #K2 #n1 #n2 #HK #Hx #m1 #m2 #H destruct
  49
  50
  51
  52 [ #_ #m1 #m2 #HL -x /2 width=1 by lveq_inv_atom/
  53 | #I1 #I2 #K1 #K2 #V1 #n #HK #_ #m1 #m2 #H -x
  54
  55
  56
  57 theorem lveq_inj: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
  58                   ∀m1,m2. L1 ≋ⓧ*[m1, m2] L2 →
  59                   ∧∧ n1 = m1 & n2 = m2.
  60 #L1 #L2 #n1 #n2 #H @(lveq_ind_voids … H) -H -L1 -L2 -n1 -n2
  61 [ #n1 #n2 #m1 #m2 #H elim (lveq_inv_voids … H) -H *
  62   [ /3 width=1 by voids_inj, conj/ ]
  63   #J1 #J2 #K1 #K2 #W #m #_ [ #H #_ | #_ #H ]
  64   elim (voids_inv_pair_sn … H) -H #H #_
  65   elim (voids_atom_inv … H) -H #H #_ destruct
  66 ]
  67 #I1 #I2 #L1 #L2 #V #n1 #n2 #n #HL #IH #m1 #m2 #H
  68 elim (lveq_inv_voids … H) -H *
  69 [1,4: [ #H #_ | #_ #H ]
  70   elim (voids_inv_atom_sn … H) -H #H #_
  71   elim (voids_pair_inv … H) -H #H #_ destruct
  72 ]
  73 #J1 #J2 #K1 #K2 #W #m #HK [1,3: #H1 #H2 |*: #H2 #H1 ]
  74 elim (voids_inv_pair_sn … H1) -H1 #H #Hnm
  75 [1,4: -IH -Hnm elim (voids_pair_inv … H) -H #H1 #H2 destruct
  76 |2,3: elim (voids_inv_pair_dx … H2) -H2 #H2 #_
  77
  78   elim (IH … HK)
  79
  80
  81 (*
  82 /3 width=3 by lveq_inv_atom, lveq_inv_voids/
  83 |
  84   lapply (lveq_inv_voids … H) -H #H
  85   elim (lveq_inv_pair_sn … H) -H * /2 width=1 by conj/
  86   #Y2 #y2 #HY2 #H1 #H2 #H3 destruct
  87 *)
  88
  89 (*
  90 fact lveq_inv_pair_bind_aux: ∀L1,L2,n1,n2. L1 ≋ ⓧ*[n1, n2] L2 →
  91                              ∀I1,I2,K1,K2,V1. K1.ⓑ{I1}V1 = L1 → K2.ⓘ{I2} = L2 →
  92                              ∨∨ ∃∃m. K1 ≋ ⓧ*[m, m] K2 & 0 = n1 & 0 = n2
  93                               | ∃∃m1,m2. K1 ≋ ⓧ*[m1, m2] K2 &
  94                                          BUnit Void = I2 & ⫯m2 = n2.
  95 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
  96 [ #J1 #J2 #L1 #L2 #V1 #H1 #H2 destruct
  97 |2,3: #I1 #I2 #K1 #K2 #V #n #HK #_ #J1 #J2 #L1 #L2 #V1 #H1 #H2 destruct /3 width=2 by or_introl, ex3_intro/
  98 |4,5: #K1 #K2 #n1 #n2 #HK #IH #J1 #J2 #L1 #L2 #V1 #H1 #H2 destruct
  99  /3 width=4 by _/
 100 ]
 101 qed-.
 102
 103 lemma voids_inv_pair_bind: ∀I1,I2,K1,K2,V1,n1,n2. ⓧ*[n1]K1.ⓑ{I1}V1 ≋ ⓧ*[n2]K2.ⓘ{I2} →
 104                            ∨∨ ∃∃n. ⓧ*[n]K1 ≋ ⓧ*[n]K2 & 0 = n1 & 0 = n2
 105                             | ∃∃m2. ⓧ*[n1]K1.ⓑ{I1}V1 ≋ ⓧ*[m2]K2 &
 106                                     BUnit Void = I2 & ⫯m2 = n2.
 107 /2 width=5 by voids_inv_pair_bind_aux/ qed-.
 108
 109 fact voids_inv_bind_pair_aux: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 →
 110                               ∀I1,I2,K1,K2,V2. K1.ⓘ{I1} = L1 → K2.ⓑ{I2}V2 = L2 →
 111                               ∨∨ ∃∃n. ⓧ*[n]K1 ≋ ⓧ*[n]K2 & 0 = n1 & 0 = n2
 112                                | ∃∃m1. ⓧ*[m1]K1 ≋ ⓧ*[n2]K2.ⓑ{I2}V2 &
 113                                        BUnit Void = I1 & ⫯m1 = n1.
 114 #L1 #L2 #n1 #n2 * -L1 -L2 -n1 -n2
 115 [ #J1 #J2 #L1 #L2 #V1 #H1 #H2 destruct
 116 |2,3: #I1 #I2 #K1 #K2 #V #n #HK #J1 #J2 #L1 #L2 #V2 #H1 #H2 destruct /3 width=2 by or_introl, ex3_intro/
 117 |4,5: #K1 #K2 #n1 #n2 #HK #J1 #J2 #L1 #L2 #V2 #H1 #H2 destruct /3 width=3 by or_intror, ex3_intro/
 118 ]
 119 qed-.
 120
 121 lemma voids_inv_bind_pair: ∀I1,I2,K1,K2,V2,n1,n2. ⓧ*[n1]K1.ⓘ{I1} ≋ ⓧ*[n2]K2.ⓑ{I2}V2 →
 122                            ∨∨ ∃∃n. ⓧ*[n]K1 ≋ ⓧ*[n]K2 & 0 = n1 & 0 = n2
 123                             | ∃∃m1. ⓧ*[m1]K1 ≋ ⓧ*[n2]K2.ⓑ{I2}V2 &
 124                                     BUnit Void = I1 & ⫯m1 = n1.
 125 /2 width=5 by voids_inv_bind_pair_aux/ qed-.
 126 *)
 127 *)